[STATEMENT]
lemma less_imp_ordinal_of_hmset_less: "k < l \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < l \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
proof (simp only: atomize_imp,
    rule measure_induct_rule[of "\<lambda>(k, l). {#k, l#}"
        "\<lambda>(k, l). k < l \<longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l" "(k, l)",
      simplified prod.case],
    simp only: split_paired_all prod.case atomize_imp[symmetric])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>{#aa, ba#} < {#a, b#}; aa < ba\<rbrakk> \<Longrightarrow> ordinal_of_hmset aa < ordinal_of_hmset ba; a < b\<rbrakk> \<Longrightarrow> ordinal_of_hmset a < ordinal_of_hmset b
[PROOF STEP]
fix k l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>{#aa, ba#} < {#a, b#}; aa < ba\<rbrakk> \<Longrightarrow> ordinal_of_hmset aa < ordinal_of_hmset ba; a < b\<rbrakk> \<Longrightarrow> ordinal_of_hmset a < ordinal_of_hmset b
[PROOF STEP]
assume
    ih: "\<And>ka la. {#ka, la#} < {#k, l#} \<Longrightarrow> ka < la \<Longrightarrow> ordinal_of_hmset ka < ordinal_of_hmset la" and
    k_lt_l: "k < l"
[PROOF STATE]
proof (state)
this:
\<lbrakk>{#?ka, ?la#} < {#k, l#}; ?ka < ?la\<rbrakk> \<Longrightarrow> ordinal_of_hmset ?ka < ordinal_of_hmset ?la
k < l

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>aa ba. \<lbrakk>{#aa, ba#} < {#a, b#}; aa < ba\<rbrakk> \<Longrightarrow> ordinal_of_hmset aa < ordinal_of_hmset ba; a < b\<rbrakk> \<Longrightarrow> ordinal_of_hmset a < ordinal_of_hmset b
[PROOF STEP]
show "ordinal_of_hmset k < ordinal_of_hmset l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
proof (cases "k = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
 2. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k = 0

goal (2 subgoals):
 1. k = 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
 2. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k = 0

goal (1 subgoal):
 1. ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
using k_lt_l ordinal_neq_0
[PROOF STATE]
proof (prove)
using this:
k = 0
k < l
(?x \<noteq> 0) = (0 < ?x)

goal (1 subgoal):
 1. ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset k < ordinal_of_hmset l

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
case k_nz: False
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have l_nz: "l \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> 0
[PROOF STEP]
using k_lt_l
[PROOF STATE]
proof (prove)
using this:
k < l

goal (1 subgoal):
 1. l \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<noteq> 0

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
define K where K: "K = hmsetmset k"
[PROOF STATE]
proof (state)
this:
K = hmsetmset k

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
define L where L: "L = hmsetmset l"
[PROOF STATE]
proof (state)
this:
L = hmsetmset l

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have k: "k = HMSet K" and l: "l = HMSet L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = HMSet K &&& l = HMSet L
[PROOF STEP]
by (simp_all add: K L)
[PROOF STATE]
proof (state)
this:
k = HMSet K
l = HMSet L

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have K_lt_L: "K < L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K < L
[PROOF STEP]
unfolding K L
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmsetmset k < hmsetmset l
[PROOF STEP]
using k_lt_l
[PROOF STATE]
proof (prove)
using this:
k < l

goal (1 subgoal):
 1. hmsetmset k < hmsetmset l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
K < L

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
define x where x: "x = Max_mset K"
[PROOF STATE]
proof (state)
this:
x = Max_mset K

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
define Ka where Ka: "Ka = K - {#x#}"
[PROOF STATE]
proof (state)
this:
Ka = remove1_mset x K

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have k_eq_xKa: "k = HMSet (add_mset x Ka)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = HMSet (add_mset x Ka)
[PROOF STEP]
using K x Ka k_nz
[PROOF STATE]
proof (prove)
using this:
K = hmsetmset k
x = Max_mset K
Ka = remove1_mset x K
k \<noteq> 0

goal (1 subgoal):
 1. k = HMSet (add_mset x Ka)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = HMSet (add_mset x Ka)

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have x_max: "\<forall>a \<in># Ka. a \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>#Ka. a \<le> x
[PROOF STEP]
unfolding x Ka
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>#remove1_mset (Max_mset K) K. a \<le> Max_mset K
[PROOF STEP]
by (meson Max_ge finite_set_mset in_diffD)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>#Ka. a \<le> x

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have ord_x_max: "\<forall>a \<in># Ka. ordinal_of_hmset a \<le> ordinal_of_hmset x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>#Ka. ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
assume a_in: "a \<in># Ka"
[PROOF STATE]
proof (state)
this:
a \<in># Ka

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
have a_le_x: "a \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> x
[PROOF STEP]
by (simp add: x_max a_in)
[PROOF STATE]
proof (state)
this:
a \<le> x

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<le> x

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a \<le> x

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
assume a_lt_x: "a < x"
[PROOF STATE]
proof (state)
this:
a < x

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a < x

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
have x_lt_k: "x < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < k
[PROOF STEP]
unfolding k_eq_xKa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < HMSet (add_mset x Ka)
[PROOF STEP]
by (rule mem_imp_less_HMSet) simp
[PROOF STATE]
proof (state)
this:
x < k

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a < x
x < k
[PROOF STEP]
have a_lt_k: "a < k"
[PROOF STATE]
proof (prove)
using this:
a < x
x < k

goal (1 subgoal):
 1. a < k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a < k

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
have "{#a, x#} < {#k#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#a, x#} < {#k#}
[PROOF STEP]
using x_lt_k a_lt_k
[PROOF STATE]
proof (prove)
using this:
x < k
a < k

goal (1 subgoal):
 1. {#a, x#} < {#k#}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{#a, x#} < {#k#}

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{#a, x#} < {#k#}

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
have "\<dots> < {#k, l#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#k#} < {#k, l#}
[PROOF STEP]
unfolding k_eq_xKa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#HMSet (add_mset x Ka)#} < {#HMSet (add_mset x Ka), l#}
[PROOF STEP]
using a_in
[PROOF STATE]
proof (prove)
using this:
a \<in># Ka

goal (1 subgoal):
 1. {#HMSet (add_mset x Ka)#} < {#HMSet (add_mset x Ka), l#}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{#k#} < {#k, l#}

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{#a, x#} < {#k, l#}
[PROOF STEP]
have "ordinal_of_hmset a < ordinal_of_hmset x"
[PROOF STATE]
proof (prove)
using this:
{#a, x#} < {#k, l#}

goal (1 subgoal):
 1. ordinal_of_hmset a < ordinal_of_hmset x
[PROOF STEP]
by (rule ih[OF _ a_lt_x])
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset a < ordinal_of_hmset x

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
a < x \<Longrightarrow> ordinal_of_hmset a < ordinal_of_hmset x

goal (1 subgoal):
 1. \<And>a. a \<in># Ka \<Longrightarrow> ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<le> x
a < x \<Longrightarrow> ordinal_of_hmset a < ordinal_of_hmset x
[PROOF STEP]
show "ordinal_of_hmset a \<le> ordinal_of_hmset x"
[PROOF STATE]
proof (prove)
using this:
a \<le> x
a < x \<Longrightarrow> ordinal_of_hmset a < ordinal_of_hmset x

goal (1 subgoal):
 1. ordinal_of_hmset a \<le> ordinal_of_hmset x
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset a \<le> ordinal_of_hmset x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>#Ka. ordinal_of_hmset a \<le> ordinal_of_hmset x

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
define y where y: "y = Max_mset L"
[PROOF STATE]
proof (state)
this:
y = Max_mset L

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
define La where La: "La = L - {#y#}"
[PROOF STATE]
proof (state)
this:
La = remove1_mset y L

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have l_eq_yLa: "l = HMSet (add_mset y La)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = HMSet (add_mset y La)
[PROOF STEP]
using L y La l_nz
[PROOF STATE]
proof (prove)
using this:
L = hmsetmset l
y = Max_mset L
La = remove1_mset y L
l \<noteq> 0

goal (1 subgoal):
 1. l = HMSet (add_mset y La)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = HMSet (add_mset y La)

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have y_max: "\<forall>b \<in># La. b \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>#La. b \<le> y
[PROOF STEP]
unfolding y La
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>#remove1_mset (Max_mset L) L. b \<le> Max_mset L
[PROOF STEP]
by (meson Max_ge finite_set_mset in_diffD)
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>#La. b \<le> y

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have ord_y_max: "\<forall>b \<in># La. ordinal_of_hmset b \<le> ordinal_of_hmset y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>#La. ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
assume b_in: "b \<in># La"
[PROOF STATE]
proof (state)
this:
b \<in># La

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
have b_le_y: "b \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> y
[PROOF STEP]
by (simp add: y_max b_in)
[PROOF STATE]
proof (state)
this:
b \<le> y

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b \<le> y

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
b \<le> y

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
assume b_lt_y: "b < y"
[PROOF STATE]
proof (state)
this:
b < y

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b < y

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
have y_lt_l: "y < l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y < l
[PROOF STEP]
unfolding l_eq_yLa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y < HMSet (add_mset y La)
[PROOF STEP]
by (rule mem_imp_less_HMSet) simp
[PROOF STATE]
proof (state)
this:
y < l

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b < y
y < l
[PROOF STEP]
have b_lt_l: "b < l"
[PROOF STATE]
proof (prove)
using this:
b < y
y < l

goal (1 subgoal):
 1. b < l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b < l

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
have "{#b, y#} < {#l#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#b, y#} < {#l#}
[PROOF STEP]
using y_lt_l b_lt_l
[PROOF STATE]
proof (prove)
using this:
y < l
b < l

goal (1 subgoal):
 1. {#b, y#} < {#l#}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{#b, y#} < {#l#}

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{#b, y#} < {#l#}

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
have "\<dots> < {#k, l#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#l#} < {#k, l#}
[PROOF STEP]
unfolding l_eq_yLa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#HMSet (add_mset y La)#} < {#k, HMSet (add_mset y La)#}
[PROOF STEP]
using b_in
[PROOF STATE]
proof (prove)
using this:
b \<in># La

goal (1 subgoal):
 1. {#HMSet (add_mset y La)#} < {#k, HMSet (add_mset y La)#}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{#l#} < {#k, l#}

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{#b, y#} < {#k, l#}
[PROOF STEP]
have "ordinal_of_hmset b < ordinal_of_hmset y"
[PROOF STATE]
proof (prove)
using this:
{#b, y#} < {#k, l#}

goal (1 subgoal):
 1. ordinal_of_hmset b < ordinal_of_hmset y
[PROOF STEP]
by (rule ih[OF _ b_lt_y])
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset b < ordinal_of_hmset y

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
b < y \<Longrightarrow> ordinal_of_hmset b < ordinal_of_hmset y

goal (1 subgoal):
 1. \<And>b. b \<in># La \<Longrightarrow> ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b \<le> y
b < y \<Longrightarrow> ordinal_of_hmset b < ordinal_of_hmset y
[PROOF STEP]
show "ordinal_of_hmset b \<le> ordinal_of_hmset y"
[PROOF STATE]
proof (prove)
using this:
b \<le> y
b < y \<Longrightarrow> ordinal_of_hmset b < ordinal_of_hmset y

goal (1 subgoal):
 1. ordinal_of_hmset b \<le> ordinal_of_hmset y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset b \<le> ordinal_of_hmset y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>#La. ordinal_of_hmset b \<le> ordinal_of_hmset y

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>#La. ordinal_of_hmset b \<le> ordinal_of_hmset y

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
assume x_eq_y: "x = y"
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have "ordinal_of_hmset (HMSet Ka) < ordinal_of_hmset (HMSet La)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset (HMSet Ka) < ordinal_of_hmset (HMSet La)
[PROOF STEP]
proof (rule ih)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {#HMSet Ka, HMSet La#} < {#k, l#}
 2. HMSet Ka < HMSet La
[PROOF STEP]
show "{#HMSet Ka, HMSet La#} < {#k, l#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#HMSet Ka, HMSet La#} < {#k, l#}
[PROOF STEP]
unfolding k l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#HMSet Ka, HMSet La#} < {#HMSet K, HMSet L#}
[PROOF STEP]
by (metis add_mset_add_single hmsetmset_less hmultiset.sel k k_eq_xKa l l_eq_yLa
            le_multiset_right_total mset_lt_single_iff union_less_mono)
[PROOF STATE]
proof (state)
this:
{#HMSet Ka, HMSet La#} < {#k, l#}

goal (1 subgoal):
 1. HMSet Ka < HMSet La
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HMSet Ka < HMSet La
[PROOF STEP]
have "\<omega>^x + HMSet Ka < \<omega>^y + HMSet La"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega>\<^sub>h^ x + HMSet Ka < \<omega>\<^sub>h^ y + HMSet La
[PROOF STEP]
using k_lt_l[unfolded k_eq_xKa l_eq_yLa]
[PROOF STATE]
proof (prove)
using this:
HMSet (add_mset x Ka) < HMSet (add_mset y La)

goal (1 subgoal):
 1. \<omega>\<^sub>h^ x + HMSet Ka < \<omega>\<^sub>h^ y + HMSet La
[PROOF STEP]
by (metis HMSet_plus add.commute add_mset_add_single)
[PROOF STATE]
proof (state)
this:
\<omega>\<^sub>h^ x + HMSet Ka < \<omega>\<^sub>h^ y + HMSet La

goal (1 subgoal):
 1. HMSet Ka < HMSet La
[PROOF STEP]
thus "HMSet Ka < HMSet La"
[PROOF STATE]
proof (prove)
using this:
\<omega>\<^sub>h^ x + HMSet Ka < \<omega>\<^sub>h^ y + HMSet La

goal (1 subgoal):
 1. HMSet Ka < HMSet La
[PROOF STEP]
using x_eq_y
[PROOF STATE]
proof (prove)
using this:
\<omega>\<^sub>h^ x + HMSet Ka < \<omega>\<^sub>h^ y + HMSet La
x = y

goal (1 subgoal):
 1. HMSet Ka < HMSet La
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
HMSet Ka < HMSet La

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset (HMSet Ka) < ordinal_of_hmset (HMSet La)

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
ordinal_of_hmset (HMSet Ka) < ordinal_of_hmset (HMSet La)

goal (1 subgoal):
 1. ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
unfolding k_eq_xKa l_eq_yLa
[PROOF STATE]
proof (prove)
using this:
ordinal_of_hmset (HMSet Ka) < ordinal_of_hmset (HMSet La)

goal (1 subgoal):
 1. ordinal_of_hmset (HMSet (add_mset x Ka)) < ordinal_of_hmset (HMSet (add_mset y La))
[PROOF STEP]
by (simp, subst (1 2) sorted_insort_is_snoc, simp_all add: ord_x_max ord_y_max,
          force simp: x_eq_y)
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset k < ordinal_of_hmset l

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x = y \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = y \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x = y \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
assume x_ne_y: "x \<noteq> y"
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have x_lt_y: "x < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y
[PROOF STEP]
by (metis K L head_\<omega>_def head_\<omega>_lt_imp_lt hmsetmset_less hmultiset.sel k_lt_l k_nz l_nz
          less_imp_not_less mset_lt_single_iff neqE x x_ne_y y)
[PROOF STATE]
proof (state)
this:
x < y

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have ord_y_smax_K: "ordinal_of_hmset a < ordinal_of_hmset y" if a_in_K: "a \<in># K" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset a < ordinal_of_hmset y
[PROOF STEP]
proof (rule ih)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {#a, y#} < {#k, l#}
 2. a < y
[PROOF STEP]
show "{#a, y#} < {#k, l#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#a, y#} < {#k, l#}
[PROOF STEP]
unfolding k_eq_xKa l_eq_yLa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#a, y#} < {#HMSet (add_mset x Ka), HMSet (add_mset y La)#}
[PROOF STEP]
using a_in_K k k_eq_xKa
[PROOF STATE]
proof (prove)
using this:
a \<in># K
k = HMSet K
k = HMSet (add_mset x Ka)

goal (1 subgoal):
 1. {#a, y#} < {#HMSet (add_mset x Ka), HMSet (add_mset y La)#}
[PROOF STEP]
by (metis add_mset_add_single mem_imp_less_HMSet mset_lt_single_iff union_less_mono
            union_single_eq_member)
[PROOF STATE]
proof (state)
this:
{#a, y#} < {#k, l#}

goal (1 subgoal):
 1. a < y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a < y
[PROOF STEP]
show "a < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < y
[PROOF STEP]
by (metis Max_ge finite_set_mset less_le_trans not_less_iff_gr_or_eq that x x_lt_y)
[PROOF STATE]
proof (state)
this:
a < y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?a \<in># K \<Longrightarrow> ordinal_of_hmset ?a < ordinal_of_hmset y

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have "ordinal_of_hmset k < ordinal_of_hmset (\<omega>^y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
[PROOF STEP]
proof (cases La)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. La = {#} \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
 2. \<And>x N. La = add_mset x N \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
La = {#}

goal (2 subgoals):
 1. La = {#} \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
 2. \<And>x N. La = add_mset x N \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
[PROOF STEP]
unfolding k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset (HMSet K) < ordinal_of_hmset (\<omega>\<^sub>h^ y)
[PROOF STEP]
by (auto intro!: from_cnf_less_\<omega>_exp simp: ord_y_smax_K)
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)

goal (1 subgoal):
 1. \<And>x N. La = add_mset x N \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x N. La = add_mset x N \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
[PROOF STEP]
case La: (add ya Lb)
[PROOF STATE]
proof (state)
this:
La = add_mset ya Lb

goal (1 subgoal):
 1. \<And>x N. La = add_mset x N \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
[PROOF STEP]
proof (rule ih)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {#k, \<omega>\<^sub>h^ y#} < {#k, l#}
 2. k < \<omega>\<^sub>h^ y
[PROOF STEP]
show "{#k, \<omega>^y#} < {#k, l#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#k, \<omega>\<^sub>h^ y#} < {#k, l#}
[PROOF STEP]
unfolding l_eq_yLa La
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#k, \<omega>\<^sub>h^ y#} < {#k, HMSet (add_mset y (add_mset ya Lb))#}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{#k, \<omega>\<^sub>h^ y#} < {#k, l#}

goal (1 subgoal):
 1. k < \<omega>\<^sub>h^ y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k < \<omega>\<^sub>h^ y
[PROOF STEP]
show "k < \<omega>^y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < \<omega>\<^sub>h^ y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k < \<omega>\<^sub>h^ y
[PROOF STEP]
have "\<And>m. x < Max_mset (add_mset y m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. x < Max_mset (add_mset y m)
[PROOF STEP]
by (meson Max_ge finite_set_mset less_le_trans union_single_eq_member x_lt_y)
[PROOF STATE]
proof (state)
this:
x < Max_mset (add_mset y ?m)

goal (1 subgoal):
 1. k < \<omega>\<^sub>h^ y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < Max_mset (add_mset y ?m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x < Max_mset (add_mset y ?m)

goal (1 subgoal):
 1. k < \<omega>\<^sub>h^ y
[PROOF STEP]
by (metis K x head_\<omega>_def head_\<omega>_lt_imp_lt hmsetmset_less hmultiset.sel k_nz
                mset_lt_single_iff x_lt_y)
[PROOF STATE]
proof (state)
this:
k < \<omega>\<^sub>h^ y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k < \<omega>\<^sub>h^ y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
have "\<dots> \<le> ordinal_of_hmset l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset (\<omega>\<^sub>h^ y) \<le> ordinal_of_hmset l
[PROOF STEP]
unfolding l_eq_yLa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_of_hmset (\<omega>\<^sub>h^ y) \<le> ordinal_of_hmset (HMSet (add_mset y La))
[PROOF STEP]
by (auto simp del: from_cnf.simps intro!: subseq_from_cnf_less_eq
          simp: subseq_from_cnf_less_eq sorted_insort_is_snoc ord_y_max)
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset (\<omega>\<^sub>h^ y) \<le> ordinal_of_hmset l

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
ordinal_of_hmset (\<omega>\<^sub>h^ y) \<le> ordinal_of_hmset l
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
ordinal_of_hmset k < ordinal_of_hmset (\<omega>\<^sub>h^ y)
ordinal_of_hmset (\<omega>\<^sub>h^ y) \<le> ordinal_of_hmset l

goal (1 subgoal):
 1. ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset k < ordinal_of_hmset l

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x \<noteq> y \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = y \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
x \<noteq> y \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = y \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l
x \<noteq> y \<Longrightarrow> ordinal_of_hmset k < ordinal_of_hmset l

goal (1 subgoal):
 1. ordinal_of_hmset k < ordinal_of_hmset l
[PROOF STEP]
by sat
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset k < ordinal_of_hmset l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ordinal_of_hmset k < ordinal_of_hmset l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordinal_of_hmset_less[simp]: "ordinal_of_hmset k < ordinal_of_hmset l \<longleftrightarrow> k < l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ordinal_of_hmset k < ordinal_of_hmset l) = (k < l)
[PROOF STEP]
using less_imp_not_less less_imp_ordinal_of_hmset_less neq_iff
[PROOF STATE]
proof (prove)
using this:
?x < ?y \<Longrightarrow> (\<not> ?y < ?x) = True
?k < ?l \<Longrightarrow> ordinal_of_hmset ?k < ordinal_of_hmset ?l
(?x \<noteq> ?y) = (?x < ?y \<or> ?y < ?x)

goal (1 subgoal):
 1. (ordinal_of_hmset k < ordinal_of_hmset l) = (k < l)
[PROOF STEP]
by blast


[STATEMENT]
lemma order_gt_0 [simp]: "order \<G> > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < order \<G>
[PROOF STEP]
using prime_order prime_gt_0_nat
[PROOF STATE]
proof (prove)
using this:
prime (order \<G>)
prime ?p \<Longrightarrow> 0 < ?p

goal (1 subgoal):
 1. 0 < order \<G>
[PROOF STEP]
by blast


[STATEMENT]
lemma  lossless_init: "lossless_spmf (init h w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (init h w)
[PROOF STEP]
by(simp add: init_def)


[STATEMENT]
lemma lossless_response: "lossless_spmf (response r w c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (response r w c)
[PROOF STEP]
by(simp add: response_def)


[STATEMENT]
lemma lossless_G: "lossless_spmf G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf G
[PROOF STEP]
by(simp add: G_def)


[STATEMENT]
lemma completeness: "Schnorr_\<Sigma>.completeness"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>.completeness
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Schnorr_\<Sigma>.completeness
[PROOF STEP]
have "\<^bold>g [^] y \<otimes> (\<^bold>g [^] w') [^] e = \<^bold>g [^] (y + w' * e)" for y e w' :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] y \<otimes> (\<^bold>g [^] w') [^] e = \<^bold>g [^] (y + w' * e)
[PROOF STEP]
using nat_pow_pow nat_pow_mult
[PROOF STATE]
proof (prove)
using this:
?x \<in> carrier \<G> \<Longrightarrow> (?x [^] ?n) [^] ?m = ?x [^] (?n * ?m)
?x \<in> carrier \<G> \<Longrightarrow> ?x [^] ?n \<otimes> ?x [^] ?m = ?x [^] (?n + ?m)

goal (1 subgoal):
 1. \<^bold>g [^] y \<otimes> (\<^bold>g [^] w') [^] e = \<^bold>g [^] (y + w' * e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ?y \<otimes> (\<^bold>g [^] ?w') [^] ?e = \<^bold>g [^] (?y + ?w' * ?e)

goal (1 subgoal):
 1. Schnorr_\<Sigma>.completeness
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>g [^] ?y \<otimes> (\<^bold>g [^] ?w') [^] ?e = \<^bold>g [^] (?y + ?w' * ?e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ?y \<otimes> (\<^bold>g [^] ?w') [^] ?e = \<^bold>g [^] (?y + ?w' * ?e)

goal (1 subgoal):
 1. Schnorr_\<Sigma>.completeness
[PROOF STEP]
unfolding Schnorr_\<Sigma>.completeness_game_def Schnorr_\<Sigma>.completeness_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ?y \<otimes> (\<^bold>g [^] ?w') [^] ?e = \<^bold>g [^] (?y + ?w' * ?e)

goal (1 subgoal):
 1. \<forall>h w e. (h, w) \<in> R_DL \<longrightarrow> e \<in> challenge_space \<longrightarrow> spmf (init h w \<bind> (\<lambda>(r, a). response r w e \<bind> (\<lambda>z. return_spmf (check h a e z)))) True = 1
[PROOF STEP]
by(auto simp add: init_def response_def check_def pow_generator_mod R_DL_def add.commute bind_spmf_const)
[PROOF STATE]
proof (state)
this:
Schnorr_\<Sigma>.completeness

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zr_rewrite:
  assumes z: "z = (x*c + r) mod (order \<G>)"
    and r: "r < order \<G>"
  shows "(z + (order \<G>)*x*c - x*c) mod (order \<G>) = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
proof(cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
 2. x \<noteq> 0 \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
 2. x \<noteq> 0 \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x = 0
z = (x * c + r) mod order \<G>
r < order \<G>

goal (1 subgoal):
 1. (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(z + order \<G> * x * c - x * c) mod order \<G> = r

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
case x_neq_0: False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
proof(cases "c = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> 0; c = 0\<rbrakk> \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
 2. \<lbrakk>x \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. \<lbrakk>x \<noteq> 0; c = 0\<rbrakk> \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
 2. \<lbrakk>x \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
(z + order \<G> * x * c - x * c) mod order \<G> = r

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
have cong: "[z + (order \<G>)*x*c = x*c + r] (mod (order \<G>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [z + order \<G> * x * c = x * c + r] (mod order \<G>)
[PROOF STEP]
by (simp add: cong_def mult.assoc z)
[PROOF STATE]
proof (state)
this:
[z + order \<G> * x * c = x * c + r] (mod order \<G>)

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
hence "[z + (order \<G>)*x*c - x*c = r] (mod (order \<G>))"
[PROOF STATE]
proof (prove)
using this:
[z + order \<G> * x * c = x * c + r] (mod order \<G>)

goal (1 subgoal):
 1. [z + order \<G> * x * c - x * c = r] (mod order \<G>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [z + order \<G> * x * c = x * c + r] (mod order \<G>) \<Longrightarrow> [z + order \<G> * x * c - x * c = r] (mod order \<G>)
[PROOF STEP]
have "z + (order \<G>)*x*c > x*c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * c < z + order \<G> * x * c
[PROOF STEP]
by (metis One_nat_def mult_less_cancel2 n_less_m_mult_n neq0_conv prime_gt_1_nat prime_order trans_less_add2 x_neq_0 False)
[PROOF STATE]
proof (state)
this:
x * c < z + order \<G> * x * c

goal (1 subgoal):
 1. [z + order \<G> * x * c = x * c + r] (mod order \<G>) \<Longrightarrow> [z + order \<G> * x * c - x * c = r] (mod order \<G>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x * c < z + order \<G> * x * c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x * c < z + order \<G> * x * c

goal (1 subgoal):
 1. [z + order \<G> * x * c - x * c = r] (mod order \<G>)
[PROOF STEP]
by (metis cong add_diff_inverse_nat cong_add_lcancel_nat less_imp_le linorder_not_le)
[PROOF STATE]
proof (state)
this:
[z + order \<G> * x * c - x * c = r] (mod order \<G>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[z + order \<G> * x * c - x * c = r] (mod order \<G>)

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[z + order \<G> * x * c - x * c = r] (mod order \<G>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[z + order \<G> * x * c - x * c = r] (mod order \<G>)

goal (1 subgoal):
 1. (z + order \<G> * x * c - x * c) mod order \<G> = r
[PROOF STEP]
by(simp add: cong_def r)
[PROOF STATE]
proof (state)
this:
(z + order \<G> * x * c - x * c) mod order \<G> = r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(z + order \<G> * x * c - x * c) mod order \<G> = r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma h_sub_rewrite:
  assumes "h = \<^bold>g [^] x"
    and z: "z < order \<G>"
  shows "\<^bold>g [^] ((z + (order \<G>)*x*c - x*c)) = \<^bold>g [^] z \<otimes> inv (h [^] c)"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
proof(cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
 2. x \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
 2. x \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x = 0
h = \<^bold>g [^] x
z < order \<G>

goal (1 subgoal):
 1. \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
case x_neq_0: False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
have "(z + order \<G> * x * c - x * c) = (z + (order \<G> * x * c - x * c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z + order \<G> * x * c - x * c = z + (order \<G> * x * c - x * c)
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
z < order \<G>

goal (1 subgoal):
 1. z + order \<G> * x * c - x * c = z + (order \<G> * x * c - x * c)
[PROOF STEP]
by (simp add: less_imp_le_nat mult_le_mono)
[PROOF STATE]
proof (state)
this:
z + order \<G> * x * c - x * c = z + (order \<G> * x * c - x * c)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z + order \<G> * x * c - x * c = z + (order \<G> * x * c - x * c)
[PROOF STEP]
have lhs: "?lhs = \<^bold>g [^] z \<otimes> \<^bold>g [^] ((order \<G>)*x*c - x*c)"
[PROOF STATE]
proof (prove)
using this:
z + order \<G> * x * c - x * c = z + (order \<G> * x * c - x * c)

goal (1 subgoal):
 1. \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> \<^bold>g [^] (order \<G> * x * c - x * c)
[PROOF STEP]
by(simp add: nat_pow_mult)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> \<^bold>g [^] (order \<G> * x * c - x * c)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
have " \<^bold>g [^] ((order \<G>)*x*c - x*c) =  inv (h [^] c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
proof(cases "c = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
 2. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
 2. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
hence bound: "((order \<G>)*x*c - x*c) > 0"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0

goal (1 subgoal):
 1. 0 < order \<G> * x * c - x * c
[PROOF STEP]
using assms x_neq_0 prime_gt_1_nat prime_order
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
h = \<^bold>g [^] x
z < order \<G>
x \<noteq> 0
prime ?p \<Longrightarrow> 1 < ?p
prime (order \<G>)

goal (1 subgoal):
 1. 0 < order \<G> * x * c - x * c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < order \<G> * x * c - x * c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < order \<G> * x * c - x * c
[PROOF STEP]
have "\<^bold>g [^] ((order \<G>)*x*c- x*c) = \<^bold>g [^] int ((order \<G>)*x*c - x*c)"
[PROOF STATE]
proof (prove)
using this:
0 < order \<G> * x * c - x * c

goal (1 subgoal):
 1. \<^bold>g [^] (order \<G> * x * c - x * c) = \<^bold>g [^] int (order \<G> * x * c - x * c)
[PROOF STEP]
by (simp add: int_pow_int)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (order \<G> * x * c - x * c) = \<^bold>g [^] int (order \<G> * x * c - x * c)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (order \<G> * x * c - x * c) = \<^bold>g [^] int (order \<G> * x * c - x * c)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
have "... = \<^bold>g [^] int ((order \<G>)*x*c) \<otimes> inv (\<^bold>g [^] (x*c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] int (order \<G> * x * c - x * c) = \<^bold>g [^] int (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c))
[PROOF STEP]
by (metis bound generator_closed int_ops(6) int_pow_int of_nat_eq_0_iff of_nat_less_0_iff of_nat_less_iff int_pow_diff)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] int (order \<G> * x * c - x * c) = \<^bold>g [^] int (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c))

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] int (order \<G> * x * c - x * c) = \<^bold>g [^] int (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c))

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
have "... = \<^bold>g [^] ((order \<G>)*x*c) \<otimes> inv (\<^bold>g [^] (x*c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] int (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c)) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c))
[PROOF STEP]
by (metis int_pow_int)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] int (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c)) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c))

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] int (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c)) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c))

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
have "... = \<^bold>g [^] ((order \<G>)*x*c) \<otimes> inv ((\<^bold>g [^] x) [^] c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c)) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv ((\<^bold>g [^] x) [^] c)
[PROOF STEP]
by(simp add: nat_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c)) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv ((\<^bold>g [^] x) [^] c)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (order \<G> * x * c) \<otimes> inv (\<^bold>g [^] (x * c)) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv ((\<^bold>g [^] x) [^] c)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
have "... = \<^bold>g [^] ((order \<G>)*x*c) \<otimes> inv (h [^] c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] (order \<G> * x * c) \<otimes> inv ((\<^bold>g [^] x) [^] c) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (h [^] c)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h = \<^bold>g [^] x
z < order \<G>

goal (1 subgoal):
 1. \<^bold>g [^] (order \<G> * x * c) \<otimes> inv ((\<^bold>g [^] x) [^] c) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (h [^] c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (order \<G> * x * c) \<otimes> inv ((\<^bold>g [^] x) [^] c) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (h [^] c)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (order \<G> * x * c) \<otimes> inv ((\<^bold>g [^] x) [^] c) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (h [^] c)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
have "... = \<one> \<otimes> inv (h [^] c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (h [^] c) = \<one> \<otimes> inv (h [^] c)
[PROOF STEP]
using generator_pow_order
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] order \<G> = \<one>

goal (1 subgoal):
 1. \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (h [^] c) = \<one> \<otimes> inv (h [^] c)
[PROOF STEP]
by (metis generator_closed mult_is_0 nat_pow_0 nat_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (order \<G> * x * c) \<otimes> inv (h [^] c) = \<one> \<otimes> inv (h [^] c)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>g [^] (order \<G> * x * c - x * c) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (h [^] c)
\<^bold>g [^] (order \<G> * x * c) \<otimes> inv (h [^] c) = \<one> \<otimes> inv (h [^] c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] (order \<G> * x * c - x * c) = \<^bold>g [^] (order \<G> * x * c) \<otimes> inv (h [^] c)
\<^bold>g [^] (order \<G> * x * c) \<otimes> inv (h [^] c) = \<one> \<otimes> inv (h [^] c)

goal (1 subgoal):
 1. \<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
by (simp add: assms(1))
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)

goal (1 subgoal):
 1. \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
using lhs
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] (order \<G> * x * c - x * c) = inv (h [^] c)
\<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> \<^bold>g [^] (order \<G> * x * c - x * c)

goal (1 subgoal):
 1. \<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (z + order \<G> * x * c - x * c) = \<^bold>g [^] z \<otimes> inv (h [^] c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hvzk_R_rewrite_grp:
  fixes x c r :: nat
  assumes "r < order \<G>"
  shows "\<^bold>g [^] (((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) mod order \<G>) = inv \<^bold>g [^] r"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] (((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) mod order \<G>) = inv \<^bold>g [^] r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>g [^] (((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) mod order \<G>) = inv \<^bold>g [^] r
[PROOF STEP]
have "[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r] (mod order \<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r] (mod order \<G>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r] (mod order \<G>)
[PROOF STEP]
have "[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c
              = x * c + order \<G> - r + order \<G> * x * c - x * c] (mod order \<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = x * c + order \<G> - r + order \<G> * x * c - x * c] (mod order \<G>)
[PROOF STEP]
by (smt cong_def One_nat_def add_diff_inverse_nat cong_diff_nat less_imp_le_nat linorder_not_less mod_add_left_eq mult.assoc n_less_m_mult_n prime_gt_1_nat prime_order trans_less_add2 zero_less_diff)
[PROOF STATE]
proof (state)
this:
[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = x * c + order \<G> - r + order \<G> * x * c - x * c] (mod order \<G>)

goal (1 subgoal):
 1. [(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r] (mod order \<G>)
[PROOF STEP]
hence "[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c
              =  order \<G> - r + order \<G> * x * c] (mod order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = x * c + order \<G> - r + order \<G> * x * c - x * c] (mod order \<G>)

goal (1 subgoal):
 1. [(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r + order \<G> * x * c] (mod order \<G>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = x * c + order \<G> - r + order \<G> * x * c - x * c] (mod order \<G>)
r < order \<G>

goal (1 subgoal):
 1. [(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r + order \<G> * x * c] (mod order \<G>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r + order \<G> * x * c] (mod order \<G>)

goal (1 subgoal):
 1. [(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r] (mod order \<G>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r + order \<G> * x * c] (mod order \<G>)

goal (1 subgoal):
 1. [(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r] (mod order \<G>)
[PROOF STEP]
by (simp add: cong_def mult.assoc)
[PROOF STATE]
proof (state)
this:
[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r] (mod order \<G>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r] (mod order \<G>)

goal (1 subgoal):
 1. \<^bold>g [^] (((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) mod order \<G>) = inv \<^bold>g [^] r
[PROOF STEP]
hence "\<^bold>g [^] ((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) = \<^bold>g [^] (order \<G> - r)"
[PROOF STATE]
proof (prove)
using this:
[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r] (mod order \<G>)

goal (1 subgoal):
 1. \<^bold>g [^] ((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) = \<^bold>g [^] (order \<G> - r)
[PROOF STEP]
using finite_carrier pow_generator_eq_iff_cong
[PROOF STATE]
proof (prove)
using this:
[(x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c = order \<G> - r] (mod order \<G>)
finite (carrier \<G>)
finite (carrier \<G>) \<Longrightarrow> (\<^bold>g [^] ?x = \<^bold>g [^] ?y) = [?x = ?y] (mod order \<G>)

goal (1 subgoal):
 1. \<^bold>g [^] ((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) = \<^bold>g [^] (order \<G> - r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) = \<^bold>g [^] (order \<G> - r)

goal (1 subgoal):
 1. \<^bold>g [^] (((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) mod order \<G>) = inv \<^bold>g [^] r
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) = \<^bold>g [^] (order \<G> - r)

goal (1 subgoal):
 1. \<^bold>g [^] (((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) mod order \<G>) = inv \<^bold>g [^] r
[PROOF STEP]
using neg_power_inverse
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) = \<^bold>g [^] (order \<G> - r)
\<lbrakk>?g \<in> carrier \<G>; ?x < order \<G>\<rbrakk> \<Longrightarrow> ?g [^] (order \<G> - ?x) = inv (?g [^] ?x)

goal (1 subgoal):
 1. \<^bold>g [^] (((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) mod order \<G>) = inv \<^bold>g [^] r
[PROOF STEP]
by (simp add: assms inverse_pow_pow pow_generator_mod)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (((x * c + order \<G> - r) mod order \<G> + order \<G> * x * c - x * c) mod order \<G>) = inv \<^bold>g [^] r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hv_zk:
  assumes "(h,x) \<in> R_DL"
  shows "Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c
[PROOF STEP]
have "Schnorr_\<Sigma>.R h x c = do {
      r \<leftarrow> sample_uniform (order \<G>);
      let z = (x*c + r) mod (order \<G>);
      let a = \<^bold>g [^] ((z + (order \<G>)*x*c - x*c) mod (order \<G>));
      return_spmf (a,c,z)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = sample_uniform (order \<G>) \<bind> (\<lambda>r. let z = (x * c + r) mod order \<G>; a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z))
[PROOF STEP]
apply(simp add: Let_def Schnorr_\<Sigma>.R_def init_def response_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform (order \<G>) \<bind> (\<lambda>y. return_spmf (\<^bold>g [^] y, c, (x * c + y) mod order \<G>)) = sample_uniform (order \<G>) \<bind> (\<lambda>r. return_spmf (\<^bold>g [^] (((x * c + r) mod order \<G> + order \<G> * x * c - x * c) mod order \<G>), c, (x * c + r) mod order \<G>))
[PROOF STEP]
using assms zr_rewrite R_DL_def
[PROOF STATE]
proof (prove)
using this:
(h, x) \<in> R_DL
\<lbrakk>?z = (?x * ?c + ?r) mod order \<G>; ?r < order \<G>\<rbrakk> \<Longrightarrow> (?z + order \<G> * ?x * ?c - ?x * ?c) mod order \<G> = ?r
R_DL = {(h, w). h = \<^bold>g [^] w}

goal (1 subgoal):
 1. sample_uniform (order \<G>) \<bind> (\<lambda>y. return_spmf (\<^bold>g [^] y, c, (x * c + y) mod order \<G>)) = sample_uniform (order \<G>) \<bind> (\<lambda>r. return_spmf (\<^bold>g [^] (((x * c + r) mod order \<G> + order \<G> * x * c - x * c) mod order \<G>), c, (x * c + r) mod order \<G>))
[PROOF STEP]
by(simp cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
Schnorr_\<Sigma>.R h x c = sample_uniform (order \<G>) \<bind> (\<lambda>r. let z = (x * c + r) mod order \<G>; a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z))

goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Schnorr_\<Sigma>.R h x c = sample_uniform (order \<G>) \<bind> (\<lambda>r. let z = (x * c + r) mod order \<G>; a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z))

goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c
[PROOF STEP]
have "... = do {
      z \<leftarrow> map_spmf (\<lambda> r. (x*c + r) mod (order \<G>)) (sample_uniform (order \<G>));
      let a = \<^bold>g [^] ((z + (order \<G>)*x*c - x*c) mod (order \<G>));
      return_spmf (a,c,z)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform (order \<G>) \<bind> (\<lambda>r. let z = (x * c + r) mod order \<G>; a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z)) = map_spmf (\<lambda>r. (x * c + r) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. let a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z))
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def)
[PROOF STATE]
proof (state)
this:
sample_uniform (order \<G>) \<bind> (\<lambda>r. let z = (x * c + r) mod order \<G>; a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z)) = map_spmf (\<lambda>r. (x * c + r) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. let a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z))

goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform (order \<G>) \<bind> (\<lambda>r. let z = (x * c + r) mod order \<G>; a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z)) = map_spmf (\<lambda>r. (x * c + r) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. let a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z))

goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c
[PROOF STEP]
have "... = do {
      z \<leftarrow>  (sample_uniform (order \<G>));
      let a = \<^bold>g [^] ((z + (order \<G>)*x*c - x*c));
      return_spmf (a,c,z)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>r. (x * c + r) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. let a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z)) = sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] (z + order \<G> * x * c - x * c) in return_spmf (a, c, z))
[PROOF STEP]
by(simp add: samp_uni_plus_one_time_pad pow_generator_mod)
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>r. (x * c + r) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. let a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z)) = sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] (z + order \<G> * x * c - x * c) in return_spmf (a, c, z))

goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>r. (x * c + r) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z. let a = \<^bold>g [^] ((z + order \<G> * x * c - x * c) mod order \<G>) in return_spmf (a, c, z)) = sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] (z + order \<G> * x * c - x * c) in return_spmf (a, c, z))

goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c
[PROOF STEP]
have "... = do {
      z \<leftarrow>  (sample_uniform (order \<G>));
      let a = \<^bold>g [^] z \<otimes> inv (h [^] c);
      return_spmf (a,c,z)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] (z + order \<G> * x * c - x * c) in return_spmf (a, c, z)) = sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] z \<otimes> inv (h [^] c) in return_spmf (a, c, z))
[PROOF STEP]
using h_sub_rewrite assms R_DL_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?h = \<^bold>g [^] ?x; ?z < order \<G>\<rbrakk> \<Longrightarrow> \<^bold>g [^] (?z + order \<G> * ?x * ?c - ?x * ?c) = \<^bold>g [^] ?z \<otimes> inv (?h [^] ?c)
(h, x) \<in> R_DL
R_DL = {(h, w). h = \<^bold>g [^] w}

goal (1 subgoal):
 1. sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] (z + order \<G> * x * c - x * c) in return_spmf (a, c, z)) = sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] z \<otimes> inv (h [^] c) in return_spmf (a, c, z))
[PROOF STEP]
by(simp cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] (z + order \<G> * x * c - x * c) in return_spmf (a, c, z)) = sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] z \<otimes> inv (h [^] c) in return_spmf (a, c, z))

goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Schnorr_\<Sigma>.R h x c = sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] (z + order \<G> * x * c - x * c) in return_spmf (a, c, z))
sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] (z + order \<G> * x * c - x * c) in return_spmf (a, c, z)) = sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] z \<otimes> inv (h [^] c) in return_spmf (a, c, z))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Schnorr_\<Sigma>.R h x c = sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] (z + order \<G> * x * c - x * c) in return_spmf (a, c, z))
sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] (z + order \<G> * x * c - x * c) in return_spmf (a, c, z)) = sample_uniform (order \<G>) \<bind> (\<lambda>z. let a = \<^bold>g [^] z \<otimes> inv (h [^] c) in return_spmf (a, c, z))

goal (1 subgoal):
 1. Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c
[PROOF STEP]
by(simp add: Schnorr_\<Sigma>.S_def S2_def map_spmf_conv_bind_spmf)
[PROOF STATE]
proof (state)
this:
Schnorr_\<Sigma>.R h x c = Schnorr_\<Sigma>.S h c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma honest_verifier_ZK:
  shows "Schnorr_\<Sigma>.HVZK"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>.HVZK
[PROOF STEP]
unfolding Schnorr_\<Sigma>.HVZK_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>challenge_space. (\<forall>(h, w)\<in>R_DL. Schnorr_\<Sigma>.R h w e = Schnorr_\<Sigma>.S h e) \<and> (\<forall>h\<in>valid_pub. \<forall>(a, z)\<in>set_spmf (S2 h e). check h a e z)
[PROOF STEP]
by(auto simp add: hv_zk R_DL_def S2_def check_def valid_pub_def challenge_space_def cyclic_group_assoc)


[STATEMENT]
lemma ss_rewrite:
  assumes "e' < e"
    and "e < order \<G>"
    and a_mem:"a  \<in> carrier \<G>"
    and h_mem: "h \<in> carrier \<G>"
    and a: "a \<otimes> h [^] e = \<^bold>g [^] z"
    and a': "a \<otimes> h [^] e' = \<^bold>g [^] z'"
  shows  "h = \<^bold>g [^] ((int z - int z') * inverse ((e - e')) (order \<G>) mod int (order \<G>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
have gcd: "gcd (nat (int e - int e') mod (order \<G>)) (order \<G>) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (nat (int e - int e') mod order \<G>) (order \<G>) = 1
[PROOF STEP]
using prime_field
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime ?q; ?a < ?q; ?a \<noteq> 0\<rbrakk> \<Longrightarrow> coprime ?a ?q

goal (1 subgoal):
 1. gcd (nat (int e - int e') mod order \<G>) (order \<G>) = 1
[PROOF STEP]
by (metis Primes.prime_nat_def assms(1) assms(2) coprime_imp_gcd_eq_1 diff_is_0_eq less_imp_diff_less
            mod_less nat_minus_as_int not_less schnorr_base.prime_order schnorr_base_axioms)
[PROOF STATE]
proof (state)
this:
gcd (nat (int e - int e') mod order \<G>) (order \<G>) = 1

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
have "a = \<^bold>g [^] z \<otimes> inv (h [^] e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = \<^bold>g [^] z \<otimes> inv (h [^] e)
[PROOF STEP]
using a a_mem
[PROOF STATE]
proof (prove)
using this:
a \<otimes> h [^] e = \<^bold>g [^] z
a \<in> carrier \<G>

goal (1 subgoal):
 1. a = \<^bold>g [^] z \<otimes> inv (h [^] e)
[PROOF STEP]
by (simp add: h_mem group.inv_solve_right)
[PROOF STATE]
proof (state)
this:
a = \<^bold>g [^] z \<otimes> inv (h [^] e)

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a = \<^bold>g [^] z \<otimes> inv (h [^] e)

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
have "a = \<^bold>g [^] z' \<otimes> inv (h [^] e')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = \<^bold>g [^] z' \<otimes> inv (h [^] e')
[PROOF STEP]
using a' a_mem
[PROOF STATE]
proof (prove)
using this:
a \<otimes> h [^] e' = \<^bold>g [^] z'
a \<in> carrier \<G>

goal (1 subgoal):
 1. a = \<^bold>g [^] z' \<otimes> inv (h [^] e')
[PROOF STEP]
by (simp add: h_mem group.inv_solve_right)
[PROOF STATE]
proof (state)
this:
a = \<^bold>g [^] z' \<otimes> inv (h [^] e')

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a = \<^bold>g [^] z \<otimes> inv (h [^] e)
a = \<^bold>g [^] z' \<otimes> inv (h [^] e')
[PROOF STEP]
have "\<^bold>g [^] z \<otimes> h [^] e'  = \<^bold>g [^] z' \<otimes> h [^] e"
[PROOF STATE]
proof (prove)
using this:
a = \<^bold>g [^] z \<otimes> inv (h [^] e)
a = \<^bold>g [^] z' \<otimes> inv (h [^] e')

goal (1 subgoal):
 1. \<^bold>g [^] z \<otimes> h [^] e' = \<^bold>g [^] z' \<otimes> h [^] e
[PROOF STEP]
using h_mem
[PROOF STATE]
proof (prove)
using this:
a = \<^bold>g [^] z \<otimes> inv (h [^] e)
a = \<^bold>g [^] z' \<otimes> inv (h [^] e')
h \<in> carrier \<G>

goal (1 subgoal):
 1. \<^bold>g [^] z \<otimes> h [^] e' = \<^bold>g [^] z' \<otimes> h [^] e
[PROOF STEP]
by (metis (no_types, lifting) a a' h_mem a_mem cyclic_group_assoc cyclic_group_commute nat_pow_closed)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z \<otimes> h [^] e' = \<^bold>g [^] z' \<otimes> h [^] e

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z \<otimes> h [^] e' = \<^bold>g [^] z' \<otimes> h [^] e

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
obtain t :: nat where  t: "h = \<^bold>g  [^] t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. h = \<^bold>g [^] t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using h_mem generatorE
[PROOF STATE]
proof (prove)
using this:
h \<in> carrier \<G>
\<lbrakk>?x \<in> carrier \<G>; \<And>n. ?x = \<^bold>g [^] n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>t. h = \<^bold>g [^] t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
h = \<^bold>g [^] t

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>g [^] z \<otimes> h [^] e' = \<^bold>g [^] z' \<otimes> h [^] e
h = \<^bold>g [^] t
[PROOF STEP]
have "\<^bold>g [^] (z + t * e')  = \<^bold>g [^] (z' +  t * e) "
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] z \<otimes> h [^] e' = \<^bold>g [^] z' \<otimes> h [^] e
h = \<^bold>g [^] t

goal (1 subgoal):
 1. \<^bold>g [^] (z + t * e') = \<^bold>g [^] (z' + t * e)
[PROOF STEP]
by (simp add: monoid.nat_pow_mult nat_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (z + t * e') = \<^bold>g [^] (z' + t * e)

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[z + t * e' = z' +  t * e] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] (z + t * e') = \<^bold>g [^] (z' + t * e)

goal (1 subgoal):
 1. [z + t * e' = z' + t * e] (mod order \<G>)
[PROOF STEP]
using group_eq_pow_eq_mod order_gt_0
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] (z + t * e') = \<^bold>g [^] (z' + t * e)
\<lbrakk>\<^bold>g [^] ?a = \<^bold>g [^] ?b; 0 < order \<G>\<rbrakk> \<Longrightarrow> [?a = ?b] (mod order \<G>)
0 < order \<G>

goal (1 subgoal):
 1. [z + t * e' = z' + t * e] (mod order \<G>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[z + t * e' = z' + t * e] (mod order \<G>)

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[int z + int t * int e' = int z' +  int t * int e] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[z + t * e' = z' + t * e] (mod order \<G>)

goal (1 subgoal):
 1. [int z + int t * int e' = int z' + int t * int e] (mod int (order \<G>))
[PROOF STEP]
using cong_int_iff
[PROOF STATE]
proof (prove)
using this:
[z + t * e' = z' + t * e] (mod order \<G>)
[int ?m = int ?q] (mod int ?n) = [?m = ?q] (mod ?n)

goal (1 subgoal):
 1. [int z + int t * int e' = int z' + int t * int e] (mod int (order \<G>))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
[int z + int t * int e' = int z' + int t * int e] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[int z - int z' = int t * int e - int t * int e'] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[int z + int t * int e' = int z' + int t * int e] (mod int (order \<G>))

goal (1 subgoal):
 1. [int z - int z' = int t * int e - int t * int e'] (mod int (order \<G>))
[PROOF STEP]
by (smt cong_iff_lin)
[PROOF STATE]
proof (state)
this:
[int z - int z' = int t * int e - int t * int e'] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[int z - int z' = int t * (int e - int e')] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[int z - int z' = int t * int e - int t * int e'] (mod int (order \<G>))

goal (1 subgoal):
 1. [int z - int z' = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
by (simp add: \<open>[int z - int z' = int t * int e - int t * int e'] (mod int (order \<G>))\<close> right_diff_distrib)
[PROOF STATE]
proof (state)
this:
[int z - int z' = int t * (int e - int e')] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[int z - int z' = int t * (int e - int e')] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[int z - int z' = int t * (int e - int e')] (mod int (order \<G>))

goal (1 subgoal):
 1. [int z - int z' = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
by (meson cong_diff cong_mod_left cong_mult cong_refl cong_trans)
[PROOF STATE]
proof (state)
this:
[int z - int z' = int t * (int e - int e')] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence *: "[int z - int z' = int t * (int e - int e')] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[int z - int z' = int t * (int e - int e')] (mod int (order \<G>))

goal (1 subgoal):
 1. [int z - int z' = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[int z - int z' = int t * (int e - int e')] (mod int (order \<G>))
e' < e
e < order \<G>
a \<in> carrier \<G>
h \<in> carrier \<G>
a \<otimes> h [^] e = \<^bold>g [^] z
a \<otimes> h [^] e' = \<^bold>g [^] z'

goal (1 subgoal):
 1. [int z - int z' = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
by (simp add: int_ops(9) of_nat_diff)
[PROOF STATE]
proof (state)
this:
[int z - int z' = int t * (int e - int e')] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[int z - int z' = int t * nat (int e - int e')] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[int z - int z' = int t * (int e - int e')] (mod int (order \<G>))

goal (1 subgoal):
 1. [int z - int z' = int t * int (nat (int e - int e'))] (mod int (order \<G>))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[int z - int z' = int t * (int e - int e')] (mod int (order \<G>))
e' < e
e < order \<G>
a \<in> carrier \<G>
h \<in> carrier \<G>
a \<otimes> h [^] e = \<^bold>g [^] z
a \<otimes> h [^] e' = \<^bold>g [^] z'

goal (1 subgoal):
 1. [int z - int z' = int t * int (nat (int e - int e'))] (mod int (order \<G>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[int z - int z' = int t * int (nat (int e - int e'))] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence **: "[(int z - int z') * fst (bezw ((nat (int e - int e'))) (order \<G>))
              = int t * (nat (int e - int e')
                  * fst (bezw ((nat (int e - int e'))) (order \<G>)))] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[int z - int z' = int t * int (nat (int e - int e'))] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) = int t * (int (nat (int e - int e')) * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>))] (mod int (order \<G>))
[PROOF STEP]
by (smt \<open>[int z - int z' = int t * (int e - int e')] (mod int (order \<G>))\<close> assms(1) assms(2)
          cong_scalar_right int_nat_eq less_imp_of_nat_less mod_less more_arith_simps(11) nat_less_iff of_nat_0_le_iff)
[PROOF STATE]
proof (state)
this:
[(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) = int t * (int (nat (int e - int e')) * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>))] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[(int z - int z') * fst (bezw ((nat (int e - int e'))) (order \<G>)) = int t * 1] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) = int t * (int (nat (int e - int e')) * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>))] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) = int t * 1] (mod int (order \<G>))
[PROOF STEP]
by (metis (no_types, opaque_lifting) gcd inverse assms(2) cong_scalar_left cong_trans less_imp_diff_less mod_less mult.comm_neutral nat_minus_as_int)
[PROOF STATE]
proof (state)
this:
[(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) = int t * 1] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[(int z - int z') * fst (bezw ((nat (int e - int e'))) (order \<G>))
              = t] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) = int t * 1] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) = int t] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[ ((int z - int z') * fst (bezw ((nat (int e - int e'))) (order \<G>)))mod order \<G>
              = t] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) = int t] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
using cong_mod_left
[PROOF STATE]
proof (prove)
using this:
[(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) = int t] (mod int (order \<G>))
[?b mod ?a = ?c] (mod ?a) = [?b = ?c] (mod ?a)

goal (1 subgoal):
 1. [(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence  **: "[nat (((int z - int z') * fst (bezw ((nat (int e - int e'))) (order \<G>)))mod order \<G>)
              = t] (mod  order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[(int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))

goal (1 subgoal):
 1. [nat ((int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>)) = t] (mod order \<G>)
[PROOF STEP]
by (metis Euclidean_Division.pos_mod_sign cong_int_iff int_nat_eq of_nat_0_less_iff order_gt_0)
[PROOF STATE]
proof (state)
this:
[nat ((int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>)) = t] (mod order \<G>)

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "\<^bold>g [^] (nat (((int z - int z') * fst (bezw ((nat (int e - int e'))) (order \<G>)))mod order \<G>)) = \<^bold>g [^] t"
[PROOF STATE]
proof (prove)
using this:
[nat ((int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>)) = t] (mod order \<G>)

goal (1 subgoal):
 1. \<^bold>g [^] nat ((int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
using cyclic_group.pow_generator_eq_iff_cong cyclic_group_axioms order_gt_0 order_gt_0_iff_finite
[PROOF STATE]
proof (prove)
using this:
[nat ((int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>)) = t] (mod order \<G>)
\<lbrakk>Cyclic_Group.cyclic_group ?G; finite (carrier ?G)\<rbrakk> \<Longrightarrow> (\<^bold>g\<^bsub>?G\<^esub> [^]\<^bsub>?G\<^esub> ?x = \<^bold>g\<^bsub>?G\<^esub> [^]\<^bsub>?G\<^esub> ?y) = [?x = ?y] (mod order ?G)
Cyclic_Group.cyclic_group \<G>
0 < order \<G>
(0 < order \<G>) = finite (carrier \<G>)

goal (1 subgoal):
 1. \<^bold>g [^] nat ((int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] nat ((int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] nat ((int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
using t
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] nat ((int z - int z') * Number_Theory_Aux.inverse (nat (int e - int e')) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t
h = \<^bold>g [^] t

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
by (smt Euclidean_Division.pos_mod_sign discrete_log.order_gt_0 int_pow_def2 nat_minus_as_int of_nat_0_less_iff)
[PROOF STATE]
proof (state)
this:
h = \<^bold>g [^] ((int z - int z') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma special_soundness:
  shows "Schnorr_\<Sigma>.special_soundness"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>.special_soundness
[PROOF STEP]
unfolding Schnorr_\<Sigma>.special_soundness_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h e e' a z z'. h \<in> valid_pub \<longrightarrow> e \<in> challenge_space \<longrightarrow> e' \<in> challenge_space \<longrightarrow> e \<noteq> e' \<longrightarrow> check h a e z \<longrightarrow> check h a e' z' \<longrightarrow> lossless_spmf (ss_adversary h (a, e, z) (a, e', z')) \<and> (\<forall>w'\<in>set_spmf (ss_adversary h (a, e, z) (a, e', z')). (h, w') \<in> R_DL)
[PROOF STEP]
by(auto simp add: valid_pub_def ss_rewrite challenge_space_def split_def ss_adversary_def check_def R_DL_def Let_def)


[STATEMENT]
theorem sigma_protocol:
  shows "Schnorr_\<Sigma>.\<Sigma>_protocol"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>.\<Sigma>_protocol
[PROOF STEP]
by(simp add: Schnorr_\<Sigma>.\<Sigma>_protocol_def completeness honest_verifier_ZK special_soundness)


[STATEMENT]
lemma "Schnorr_\<Sigma>_commit.abstract_com.correct"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.abstract_com.correct
[PROOF STEP]
by(fact Schnorr_\<Sigma>_commit.commit_correct)


[STATEMENT]
lemma "Schnorr_\<Sigma>_commit.abstract_com.perfect_hiding_ind_cpa \<A>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.abstract_com.perfect_hiding_ind_cpa \<A>
[PROOF STEP]
by(fact Schnorr_\<Sigma>_commit.perfect_hiding)


[STATEMENT]
lemma rel_adv_eq_dis_log_adv:
  "Schnorr_\<Sigma>_commit.rel_advantage \ = discrete_log.advantage \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.rel_advantage \ = discrete_log.advantage \
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.rel_advantage \ = discrete_log.advantage \
[PROOF STEP]
have "Schnorr_\<Sigma>_commit.rel_game \ = discrete_log.dis_log \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.rel_game \ = discrete_log.dis_log \
[PROOF STEP]
unfolding Schnorr_\<Sigma>_commit.rel_game_def discrete_log.dis_log_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY G \<bind> (\<lambda>(h, w). \ h \<bind> (\<lambda>w'. return_spmf ((h, w') \<in> R_DL))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>x. let h = \<^bold>g [^] x in \ h \<bind> (\<lambda>x'. return_spmf [x = x'] (mod order \<G>))) ELSE return_spmf False
[PROOF STEP]
by(auto intro: try_spmf_cong bind_spmf_cong[OF refl]
       simp add: G_def R_DL_def cong_less_modulus_unique_nat group_eq_pow_eq_mod finite_carrier pow_generator_eq_iff_cong)
[PROOF STATE]
proof (state)
this:
Schnorr_\<Sigma>_commit.rel_game \ = discrete_log.dis_log \

goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.rel_advantage \ = discrete_log.advantage \
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Schnorr_\<Sigma>_commit.rel_game \ = discrete_log.dis_log \

goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.rel_advantage \ = discrete_log.advantage \
[PROOF STEP]
using Schnorr_\<Sigma>_commit.rel_advantage_def discrete_log.advantage_def
[PROOF STATE]
proof (prove)
using this:
Schnorr_\<Sigma>_commit.rel_game \ = discrete_log.dis_log \
Schnorr_\<Sigma>_commit.rel_advantage ?\ \<equiv> spmf (Schnorr_\<Sigma>_commit.rel_game ?\) True
discrete_log.advantage ?\ \<equiv> spmf (discrete_log.dis_log ?\) True

goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.rel_advantage \ = discrete_log.advantage \
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Schnorr_\<Sigma>_commit.rel_advantage \ = discrete_log.advantage \

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bind_advantage_bound_dis_log:
  "Schnorr_\<Sigma>_commit.abstract_com.bind_advantage \<A> \<le> discrete_log.advantage (Schnorr_\<Sigma>_commit.adversary \<A>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.abstract_com.bind_advantage \<A> \<le> discrete_log.advantage (Schnorr_\<Sigma>_commit.adversary \<A>)
[PROOF STEP]
using Schnorr_\<Sigma>_commit.bind_advantage rel_adv_eq_dis_log_adv
[PROOF STATE]
proof (prove)
using this:
Schnorr_\<Sigma>_commit.abstract_com.bind_advantage ?\<A> \<le> Schnorr_\<Sigma>_commit.rel_advantage (Schnorr_\<Sigma>_commit.adversary ?\<A>)
Schnorr_\<Sigma>_commit.rel_advantage ?\<A> = discrete_log.advantage ?\<A>

goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.abstract_com.bind_advantage \<A> \<le> discrete_log.advantage (Schnorr_\<Sigma>_commit.adversary \<A>)
[PROOF STEP]
by simp


[STATEMENT]
theorem sigma_protocol:
  shows "Schnorr_\<Sigma>.\<Sigma>_protocol n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>.\<Sigma>_protocol n
[PROOF STEP]
by(simp add: sigma_protocol)


[STATEMENT]
lemma asymp_correct: "Schnorr_\<Sigma>_commit.abstract_com.correct n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.abstract_com.correct n
[PROOF STEP]
using  Schnorr_\<Sigma>_commit.commit_correct
[PROOF STATE]
proof (prove)
using this:
Schnorr_\<Sigma>_commit.abstract_com.correct ?\<eta>

goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.abstract_com.correct n
[PROOF STEP]
by simp


[STATEMENT]
lemma asymp_perfect_hiding: "Schnorr_\<Sigma>_commit.abstract_com.perfect_hiding_ind_cpa n (\<A> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.abstract_com.perfect_hiding_ind_cpa n (\<A> n)
[PROOF STEP]
using Schnorr_\<Sigma>_commit.perfect_hiding
[PROOF STATE]
proof (prove)
using this:
Schnorr_\<Sigma>_commit.abstract_com.perfect_hiding_ind_cpa ?\<eta> ?\<A>

goal (1 subgoal):
 1. Schnorr_\<Sigma>_commit.abstract_com.perfect_hiding_ind_cpa n (\<A> n)
[PROOF STEP]
by blast


[STATEMENT]
lemma asymp_computational_binding:
  assumes "negligible (\<lambda> n. discrete_log.advantage n (Schnorr_\<Sigma>_commit.adversary n (\<A> n)))"
  shows "negligible (\<lambda> n. Schnorr_\<Sigma>_commit.abstract_com.bind_advantage n (\<A> n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. Schnorr_\<Sigma>_commit.abstract_com.bind_advantage n (\<A> n))
[PROOF STEP]
using Schnorr_\<Sigma>_commit.bind_advantage assms Schnorr_\<Sigma>_commit.abstract_com.bind_advantage_def negligible_le bind_advantage_bound_dis_log
[PROOF STATE]
proof (prove)
using this:
Schnorr_\<Sigma>_commit.abstract_com.bind_advantage ?\<eta> ?\<A> \<le> Schnorr_\<Sigma>_commit.rel_advantage ?\<eta> (Schnorr_\<Sigma>_commit.adversary ?\<eta> ?\<A>)
Negligible.negligible (\<lambda>n. discrete_log.advantage n (Schnorr_\<Sigma>_commit.adversary n (\<A> n)))
Schnorr_\<Sigma>_commit.abstract_com.bind_advantage ?\<eta> ?\<A> \<equiv> spmf (Schnorr_\<Sigma>_commit.abstract_com.bind_game ?\<eta> ?\<A>) True
\<lbrakk>Negligible.negligible ?g; \<And>\<eta>. \<bar>?f \<eta>\<bar> \<le> ?g \<eta>\<rbrakk> \<Longrightarrow> Negligible.negligible ?f
Schnorr_\<Sigma>_commit.abstract_com.bind_advantage ?\<eta> ?\<A> \<le> discrete_log.advantage ?\<eta> (Schnorr_\<Sigma>_commit.adversary ?\<eta> ?\<A>)

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. Schnorr_\<Sigma>_commit.abstract_com.bind_advantage n (\<A> n))
[PROOF STEP]
by auto


[STATEMENT]
lemma edom_AEstack: "edom (AEstack as S) \<subseteq> fv S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edom (AEstack as S) \<subseteq> fv S
[PROOF STEP]
by (induction as S rule: AEstack.induct) (auto simp del: fun_meet_simp dest!: subsetD[OF Aexp_edom])


[STATEMENT]
lemma Sigma_transfer[transfer_rule]:
  "(rel_set A ===> (A ===> rel_set B) ===> rel_set (rel_prod A B)) Sigma Sigma"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (A ===> rel_set B) ===> rel_set (rel_prod A B)) Sigma Sigma
[PROOF STEP]
unfolding Sigma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (A ===> rel_set B) ===> rel_set (rel_prod A B)) (\<lambda>A B. \<Union>x\<in>A. \<Union>y\<in>B x. {(x, y)}) (\<lambda>A B. \<Union>x\<in>A. \<Union>y\<in>B x. {(x, y)})
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma less_transfer[transfer_rule]:
  "(A ===> A ===> (=)) less less"
  if [transfer_rule]: "bi_unique A" "(A ===> A ===> (=)) less_eq less_eq"
  for A::"'c::order \<Rightarrow> 'd::order \<Rightarrow> bool"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> A ===> (=)) (<) (<)
[PROOF STEP]
unfolding order.strict_iff_order[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> A ===> (=)) (\<lambda>a b. a \<le> b \<and> a \<noteq> b) (\<lambda>a b. a \<le> b \<and> a \<noteq> b)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma dist_transfer[transfer_rule]:
  "(A ===> A ===> (=)) dist dist"
  if [transfer_rule]: "(A ===> (=)) norm norm" "(A ===> A ===> A) (-) (-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> A ===> (=)) dist dist
[PROOF STEP]
unfolding dist_norm
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> A ===> (=)) (\<lambda>x y. norm (x - y)) (\<lambda>x y. norm (x - y))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma open_transfer[transfer_rule]:
  "(rel_set A ===> (=)) open open"
  if [transfer_rule]: "bi_unique A" "bi_total A" "(A ===> A ===> (=)) dist dist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (=)) open open
[PROOF STEP]
unfolding open_dist
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (=)) (\<lambda>S. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S) (\<lambda>S. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma closed_transfer[transfer_rule]:
  "(rel_set A ===> (=)) closed closed"
  if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (=)) closed closed
[PROOF STEP]
unfolding closed_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (=)) (\<lambda>S. open (- S)) (\<lambda>S. open (- S))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma sgn_transfer[transfer_rule]:
  "(A ===> A) sgn sgn"
  if [transfer_rule]: "(A ===> (=)) norm norm" "((=) ===> A ===> A) scaleR scaleR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> A) sgn sgn
[PROOF STEP]
unfolding sgn_div_norm
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> A) (\<lambda>x. x /\<^sub>R norm x) (\<lambda>x. x /\<^sub>R norm x)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma lipschitz_on_transfer[transfer_rule]:
  "((=) ===> (rel_set A) ===> (A ===> B) ===> (=)) lipschitz_on lipschitz_on"
  if [transfer_rule]: "(B ===> B ===> (=)) dist dist" "(A ===> A ===> (=)) dist dist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> rel_set A ===> (A ===> B) ===> (=)) lipschitz_on lipschitz_on
[PROOF STEP]
unfolding lipschitz_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> rel_set A ===> (A ===> B) ===> (=)) (\<lambda>C U f. 0 \<le> C \<and> (\<forall>x\<in>U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y)) (\<lambda>C U f. 0 \<le> C \<and> (\<forall>x\<in>U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma cball_transfer[transfer_rule]:
  "(A ===> (=) ===> rel_set A) cball cball"
  if [transfer_rule]: "bi_total A" "(A ===> A ===> (=)) dist dist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> (=) ===> rel_set A) cball cball
[PROOF STEP]
unfolding cball_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> (=) ===> rel_set A) (\<lambda>x e. {y. dist x y \<le> e}) (\<lambda>x e. {y. dist x y \<le> e})
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma ball_transfer[transfer_rule]:
  "(A ===> (=) ===> rel_set A) ball ball"
  if [transfer_rule]: "bi_total A" "(A ===> A ===> (=)) dist dist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> (=) ===> rel_set A) ball ball
[PROOF STEP]
unfolding ball_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> (=) ===> rel_set A) (\<lambda>x e. {y. dist x y < e}) (\<lambda>x e. {y. dist x y < e})
[PROOF STEP]
by transfer_prover