[STATEMENT]
lemma tabulate_sees_field_code [code]:
  "tabulate_sees_field P =
   Mapping.tabulate (map fst P) (\<lambda>C. Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, (D, Tfm))) (fields' P C)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tabulate_sees_field P = Mapping.tabulate (map fst P) (\<lambda>C. Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (fields' P C)))
[PROOF STEP]
apply(simp add: tabulate_sees_field_def tabulate_def is_class_def fields'_def Fields'_eq_Fields Mapping_inject)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun id (map_option mapping.Mapping) (\<lambda>C. if \<exists>a aa b. map_of P C = \<lfloor>(a, aa, b)\<rfloor> then \<lfloor>\<lambda>F. if \<exists>T fm. Ex (sees_field (Program (id P)) C F T fm) then \<lfloor>field (Program (id P)) C F\<rfloor> else None\<rfloor> else None) = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P)
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. map_fun id (map_option mapping.Mapping) (\<lambda>C. if \<exists>a aa b. map_of P C = \<lfloor>(a, aa, b)\<rfloor> then \<lfloor>\<lambda>F. if \<exists>T fm. Ex (sees_field (Program (id P)) C F T fm) then \<lfloor>field (Program (id P)) C F\<rfloor> else None\<rfloor> else None) x = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ((\<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> \<lfloor>mapping.Mapping (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None)\<rfloor> = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x) \<and> ((\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x)
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. (\<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> \<lfloor>mapping.Mapping (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None)\<rfloor> = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
 2. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(clarsimp simp add: o_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> \<lfloor>mapping.Mapping (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None)\<rfloor> = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) (fst x)) then The (Fields' P (fst x)) else [])))) P) x
 2. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(subst map_of_map2[unfolded split_def])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> \<lfloor>mapping.Mapping (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None)\<rfloor> = map_option (\<lambda>a. Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) x) then The (Fields' P x) else []))) (map_of P x)
 2. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (Ex (Fields (Program P) x) \<longrightarrow> mapping.Mapping (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x)))) \<and> ((\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> mapping.Mapping (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = Mapping.of_alist [])
 2. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (Ex (Fields (Program P) x) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x)))) \<and> ((\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of [])
 2. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> Ex (Fields (Program P) x) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x)))
 2. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of []
 3. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x a aa b P xa. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x has_fields xa\<rbrakk> \<Longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x)))
 2. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of []
 3. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x a aa b P xa F. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x has_fields xa\<rbrakk> \<Longrightarrow> (if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x))) F
 2. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of []
 3. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x a aa b P xa F. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x has_fields xa\<rbrakk> \<Longrightarrow> ((\<exists>T fm. Ex (sees_field (Program P) x F T fm)) \<longrightarrow> \<lfloor>field (Program P) x F\<rfloor> = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x))) F) \<and> ((\<forall>T fm xa. \<not> Program P \<turnstile> x sees F:T (fm) in xa) \<longrightarrow> None = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x))) F)
 2. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of []
 3. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a aa b P xa F. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x has_fields xa\<rbrakk> \<Longrightarrow> (\<exists>T fm. Ex (sees_field (Program P) x F T fm)) \<longrightarrow> \<lfloor>field (Program P) x F\<rfloor> = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x))) F
 2. \<And>x a aa b P xa F. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x has_fields xa\<rbrakk> \<Longrightarrow> (\<forall>T fm xa. \<not> Program P \<turnstile> x sees F:T (fm) in xa) \<longrightarrow> None = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x))) F
 3. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of []
 4. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(clarsimp simp add: sees_field_def Fields'_eq_Fields)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a aa b P xa F T fm xb FDTs. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x has_fields xa; Program P \<turnstile> x has_fields FDTs; map_of (map (\<lambda>((F, D), Tm). (F, D, Tm)) FDTs) F = \<lfloor>(xb, T, fm)\<rfloor>\<rbrakk> \<Longrightarrow> \<lfloor>(xb, T, fm)\<rfloor> = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) xa) F
 2. \<And>x a aa b P xa F. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x has_fields xa\<rbrakk> \<Longrightarrow> (\<forall>T fm xa. \<not> Program P \<turnstile> x sees F:T (fm) in xa) \<longrightarrow> None = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x))) F
 3. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of []
 4. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(drule (1) has_fields_fun, clarsimp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x a aa b P xa F. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x has_fields xa\<rbrakk> \<Longrightarrow> (\<forall>T fm xa. \<not> Program P \<turnstile> x sees F:T (fm) in xa) \<longrightarrow> None = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x))) F
 2. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of []
 3. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x a aa b P xa F. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x has_fields xa; \<forall>T fm xa. \<not> Program P \<turnstile> x sees F:T (fm) in xa\<rbrakk> \<Longrightarrow> None = map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x))) F
 2. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of []
 3. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(rule sym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x a aa b P xa F. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x has_fields xa; \<forall>T fm xa. \<not> Program P \<turnstile> x sees F:T (fm) in xa\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x))) F = None
 2. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of []
 3. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x a aa b P xa F. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x has_fields xa; \<forall>T fm xa. \<not> Program P \<turnstile> x sees F:T (fm) in xa; map_of (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (The (Fields' P x))) F \<noteq> None\<rbrakk> \<Longrightarrow> False
 2. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of []
 3. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(clarsimp simp add: sees_field_def Fields'_eq_Fields)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a aa b P. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>xa. \<not> Program P \<turnstile> x has_fields xa) \<longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = map_of []
 2. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a aa b P. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; \<forall>xa. \<not> Program P \<turnstile> x has_fields xa\<rbrakk> \<Longrightarrow> (\<lambda>F. if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = Map.empty
 2. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a aa b P F. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; \<forall>xa. \<not> Program P \<turnstile> x has_fields xa\<rbrakk> \<Longrightarrow> (if \<exists>T fm. Ex (sees_field (Program P) x F T fm) then \<lfloor>field (Program (id P)) (id x) F\<rfloor> else None) = None
 2. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(clarsimp simp add: sees_field_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>) \<longrightarrow> None = map_of (map ((\<lambda>k. (k, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) k) then The (Fields' P k) else [])))) \<circ> fst) P) x
[PROOF STEP]
apply(clarsimp simp add: o_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) (fst x)) then The (Fields' P (fst x)) else [])))) P) x
[PROOF STEP]
apply(subst map_of_map2[simplified split_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> None = map_option (\<lambda>a. Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) x) then The (Fields' P x) else []))) (map_of P x)
[PROOF STEP]
apply(rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> map_option (\<lambda>a. Mapping.of_alist (map (\<lambda>((F, D), Tfm). (F, D, Tfm)) (if Ex (Fields (Program P) x) then The (Fields' P x) else []))) (map_of P x) = None
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> map_of P x = None
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>a aa b. map_of P x \<noteq> \<lfloor>(a, aa, b)\<rfloor>; map_of P x \<noteq> None\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Methods'_into_Methods:
  assumes "Methods' P C Mm"
  shows "Program P \<turnstile> C sees_methods (map_of Mm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Program P \<turnstile> C sees_methods map_of Mm
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Methods' P C Mm

goal (1 subgoal):
 1. Program P \<turnstile> C sees_methods map_of Mm
[PROOF STEP]
apply induct
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>D fs ms Mm. \<lbrakk>map_of P Object = \<lfloor>(D, fs, ms)\<rfloor>; Mm = map (\<lambda>(M, rest). (M, rest, Object)) ms\<rbrakk> \<Longrightarrow> Program P \<turnstile> Object sees_methods map_of Mm
 2. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> Program P \<turnstile> C sees_methods map_of Mm'
[PROOF STEP]
apply(clarsimp simp add: o_def split_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>D fs ms. map_of P Object = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> Program P \<turnstile> Object sees_methods map_of (map (\<lambda>p. (fst p, snd p, Object)) ms)
 2. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> Program P \<turnstile> C sees_methods map_of Mm'
[PROOF STEP]
apply(rule sees_methods_Object)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>D fs ms. map_of P Object = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> class (Program P) Object = \<lfloor>(?D5 D fs ms, ?fs5 D fs ms, ?ms5 D fs ms)\<rfloor>
 2. \<And>D fs ms. map_of P Object = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> map_of (map (\<lambda>p. (fst p, snd p, Object)) ms) = map_option (\<lambda>m. (m, Object)) \<circ> map_of (?ms5 D fs ms)
 3. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> Program P \<turnstile> C sees_methods map_of Mm'
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>D fs ms. map_of P Object = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> map_of (map (\<lambda>p. (fst p, snd p, Object)) ms) = map_option (\<lambda>m. (m, Object)) \<circ> map_of ms
 2. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> Program P \<turnstile> C sees_methods map_of Mm'
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>D fs ms x. map_of P Object = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> map_of (map (\<lambda>p. (fst p, snd p, Object)) ms) x = (map_option (\<lambda>m. (m, Object)) \<circ> map_of ms) x
 2. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> Program P \<turnstile> C sees_methods map_of Mm'
[PROOF STEP]
apply(subst map_of_map2[unfolded split_def])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>D fs ms x. map_of P Object = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> map_option (\<lambda>a. (a, Object)) (map_of ms x) = (map_option (\<lambda>m. (m, Object)) \<circ> map_of ms) x
 2. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> Program P \<turnstile> C sees_methods map_of Mm'
[PROOF STEP]
apply(simp add: o_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> Program P \<turnstile> C sees_methods map_of Mm'
[PROOF STEP]
apply(rule sees_methods_rec)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> class (Program P) C = \<lfloor>(?D20 C D fs ms Mm Mm', ?fs20 C D fs ms Mm Mm', ?ms20 C D fs ms Mm Mm')\<rfloor>
 2. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> C \<noteq> Object
 3. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> Program P \<turnstile> ?D20 C D fs ms Mm Mm' sees_methods ?Mm20 C D fs ms Mm Mm'
 4. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> map_of Mm' = ?Mm20 C D fs ms Mm Mm' ++ (map_option (\<lambda>m. (m, C)) \<circ> map_of (?ms20 C D fs ms Mm Mm'))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> C \<noteq> Object
 2. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> Program P \<turnstile> D sees_methods ?Mm20 C D fs ms Mm Mm'
 3. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> map_of Mm' = ?Mm20 C D fs ms Mm Mm' ++ (map_option (\<lambda>m. (m, C)) \<circ> map_of ms)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> Program P \<turnstile> D sees_methods ?Mm20 C D fs ms Mm Mm'
 2. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> map_of Mm' = ?Mm20 C D fs ms Mm Mm' ++ (map_option (\<lambda>m. (m, C)) \<circ> map_of ms)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C D fs ms Mm Mm'. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; Program P \<turnstile> D sees_methods map_of Mm; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> map_of Mm' = map_of Mm ++ (map_option (\<lambda>m. (m, C)) \<circ> map_of ms)
[PROOF STEP]
apply(clarsimp simp add: map_add_def map_of_map2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma methods'_code [code]:
  "methods' P C =
  (let Mm = Methods'_i_i_o P C
   in if Predicate.holds (Mm \<bind> (\<lambda>_. Predicate.single ())) then Predicate.the Mm else [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. methods' P C = (let Mm = Methods'_i_i_o P C in if Predicate.holds (Mm \<bind> (\<lambda>_. Predicate.single ())) then Predicate.the Mm else [])
[PROOF STEP]
unfolding methods'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if Ex (Methods' P C) then The (Methods' P C) else []) = (let Mm = Methods'_i_i_o P C in if Predicate.holds (Mm \<bind> (\<lambda>_. Predicate.single ())) then Predicate.the Mm else [])
[PROOF STEP]
by(auto simp add: holds_eq Methods'_i_i_o_def Predicate.the_def)


[STATEMENT]
lemma Methods'_fun:
  assumes "Methods' P C Mm"
  shows "Methods' P C Mm' \<Longrightarrow> Mm = Mm'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Methods' P C Mm' \<Longrightarrow> Mm = Mm'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Methods' P C Mm

goal (1 subgoal):
 1. Methods' P C Mm' \<Longrightarrow> Mm = Mm'
[PROOF STEP]
apply(induct arbitrary: Mm')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>D fs ms Mm Mm'. \<lbrakk>map_of P Object = \<lfloor>(D, fs, ms)\<rfloor>; Mm = map (\<lambda>(M, rest). (M, rest, Object)) ms; Methods' P Object Mm'\<rbrakk> \<Longrightarrow> Mm = Mm'
 2. \<And>C D fs ms Mm Mm' Mm'a. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; \<And>Mm'. Methods' P D Mm' \<Longrightarrow> Mm = Mm'; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm; Methods' P C Mm'a\<rbrakk> \<Longrightarrow> Mm' = Mm'a
[PROOF STEP]
apply(fastforce elim: Methods'.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C D fs ms Mm Mm' Mm'a. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; \<And>Mm'. Methods' P D Mm' \<Longrightarrow> Mm = Mm'; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm; Methods' P C Mm'a\<rbrakk> \<Longrightarrow> Mm' = Mm'a
[PROOF STEP]
apply(rotate_tac -1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C D fs ms Mm Mm' Mm'a. \<lbrakk>Methods' P C Mm'a; map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; \<And>Mm'. Methods' P D Mm' \<Longrightarrow> Mm = Mm'; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm\<rbrakk> \<Longrightarrow> Mm' = Mm'a
[PROOF STEP]
apply(erule Methods'.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C D fs ms Mm Mm' Mm'a Da fsa msa Mma. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; \<And>Mm'. Methods' P D Mm' \<Longrightarrow> Mm = Mm'; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm; C = Object; Mm'a = Mma; map_of P Object = \<lfloor>(Da, fsa, msa)\<rfloor>; Mma = map (\<lambda>(M, rest). (M, rest, Object)) msa\<rbrakk> \<Longrightarrow> Mm' = Mm'a
 2. \<And>C D fs ms Mm Mm' Mm'a Ca Da fsa msa Mma Mm'b. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; \<And>Mm'. Methods' P D Mm' \<Longrightarrow> Mm = Mm'; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm; C = Ca; Mm'a = Mm'b; map_of P Ca = \<lfloor>(Da, fsa, msa)\<rfloor>; Ca \<noteq> Object; Methods' P Da Mma; Mm'b = map (\<lambda>(M, rest). (M, rest, Ca)) msa @ Mma\<rbrakk> \<Longrightarrow> Mm' = Mm'a
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C D fs ms Mm Mm' Mm'a Ca Da fsa msa Mma Mm'b. \<lbrakk>map_of P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; Methods' P D Mm; \<And>Mm'. Methods' P D Mm' \<Longrightarrow> Mm = Mm'; Mm' = map (\<lambda>(M, rest). (M, rest, C)) ms @ Mm; C = Ca; Mm'a = Mm'b; map_of P Ca = \<lfloor>(Da, fsa, msa)\<rfloor>; Ca \<noteq> Object; Methods' P Da Mma; Mm'b = map (\<lambda>(M, rest). (M, rest, Ca)) msa @ Mma\<rbrakk> \<Longrightarrow> Mm' = Mm'a
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>C D fs ms Mm Mm' Mm'a Ca Da fsa msa Mma Mm'b. \<lbrakk>map_of P Ca = \<lfloor>(D, fs, ms)\<rfloor>; Ca \<noteq> Object; Methods' P D Mm; \<And>Mm'. Methods' P D Mm' \<Longrightarrow> Mm = Mm'; map_of P Ca = \<lfloor>(Da, fsa, msa)\<rfloor>; Ca \<noteq> Object; Methods' P Da Mma\<rbrakk> \<Longrightarrow> map (\<lambda>(M, rest). (M, rest, Ca)) ms @ Mm = map (\<lambda>(M, rest). (M, rest, Ca)) msa @ Mma
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma The_Methods' [simp]: "Methods' P C Mm \<Longrightarrow> The (Methods' P C) = Mm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Methods' P C Mm \<Longrightarrow> The (Methods' P C) = Mm
[PROOF STEP]
by(auto dest: Methods'_fun)


[STATEMENT]
lemma methods_def2 [simp]: "Methods' P C Mm \<Longrightarrow> methods' P C = Mm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Methods' P C Mm \<Longrightarrow> methods' P C = Mm
[PROOF STEP]
by(auto simp add: methods'_def)


[STATEMENT]
lemma tabulate_Method_code [code]:
  "tabulate_Method P =
   Mapping.tabulate (map fst P) (\<lambda>C. Mapping.of_alist (map (\<lambda>(M, (rest, D)). (M, D, rest)) (methods' P C)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tabulate_Method P = Mapping.tabulate (map fst P) (\<lambda>C. Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P C)))
[PROOF STEP]
apply(simp add: tabulate_Method_def tabulate_def o_def lookup.rep_eq Mapping_inject)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun id (map_option mapping.Mapping) (\<lambda>C. if is_class (Program P) C then \<lfloor>\<lambda>M. if \<exists>Ts T mthd. Ex (Method (Program (id P)) C M Ts T mthd) then \<lfloor>method (Program (id P)) C M\<rfloor> else None\<rfloor> else None) = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P)
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. map_fun id (map_option mapping.Mapping) (\<lambda>C. if is_class (Program P) C then \<lfloor>\<lambda>M. if \<exists>Ts T mthd. Ex (Method (Program (id P)) C M Ts T mthd) then \<lfloor>method (Program (id P)) C M\<rfloor> else None\<rfloor> else None) x = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (is_class (Program P) x \<longrightarrow> \<lfloor>mapping.Mapping (\<lambda>M. if \<exists>Ts T mthd. Ex (Method (Program P) x M Ts T mthd) then \<lfloor>method (Program (id P)) (id x) M\<rfloor> else None)\<rfloor> = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x) \<and> (\<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x)
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. is_class (Program P) x \<longrightarrow> \<lfloor>mapping.Mapping (\<lambda>M. if \<exists>Ts T mthd. Ex (Method (Program P) x M Ts T mthd) then \<lfloor>method (Program (id P)) (id x) M\<rfloor> else None)\<rfloor> = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. is_class (Program P) x \<Longrightarrow> \<lfloor>mapping.Mapping (\<lambda>M. if \<exists>Ts T mthd. Ex (Method (Program P) x M Ts T mthd) then \<lfloor>method (Program (id P)) (id x) M\<rfloor> else None)\<rfloor> = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(rule sym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. is_class (Program P) x \<Longrightarrow> map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x = \<lfloor>mapping.Mapping (\<lambda>M. if \<exists>Ts T mthd. Ex (Method (Program P) x M Ts T mthd) then \<lfloor>method (Program (id P)) (id x) M\<rfloor> else None)\<rfloor>
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(subst map_of_map2[unfolded split_def])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. is_class (Program P) x \<Longrightarrow> map_option (\<lambda>a. Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x))) (map_of P x) = \<lfloor>mapping.Mapping (\<lambda>M. if \<exists>Ts T mthd. Ex (Method (Program P) x M Ts T mthd) then \<lfloor>method (Program (id P)) (id x) M\<rfloor> else None)\<rfloor>
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(simp add: is_class_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) = mapping.Mapping (\<lambda>M. if \<exists>Ts T mthd. Ex (Method (Program P) x M Ts T mthd) then \<lfloor>method (Program (id P)) (id x) M\<rfloor> else None)
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x P. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) = (\<lambda>M. if \<exists>Ts T mthd. Ex (Method (Program P) x M Ts T mthd) then \<lfloor>method (Program (id P)) (id x) M\<rfloor> else None)
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x P M. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = (if \<exists>Ts T mthd. Ex (Method (Program P) x M Ts T mthd) then \<lfloor>method (Program (id P)) (id x) M\<rfloor> else None)
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(simp add: map_of_map2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x P M. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> ((\<exists>Ts T mthd. Ex (Method (Program P) x M Ts T mthd)) \<longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = \<lfloor>method (Program P) x M\<rfloor>) \<and> ((\<forall>Ts T mthd xa. \<not> Program P \<turnstile> x sees M: Ts\<rightarrow>T = mthd in xa) \<longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = None)
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x P M. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<exists>Ts T mthd. Ex (Method (Program P) x M Ts T mthd)) \<longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = \<lfloor>method (Program P) x M\<rfloor>
 2. \<And>x P M. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>Ts T mthd xa. \<not> Program P \<turnstile> x sees M: Ts\<rightarrow>T = mthd in xa) \<longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = None
 3. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(clarsimp simp add: map_of_map2 Method_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x P M a aa b Ts T mthd xa Mm. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Program P \<turnstile> x sees_methods Mm; Mm M = \<lfloor>((Ts, T, mthd), xa)\<rfloor>\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = \<lfloor>(xa, Ts, T, mthd)\<rfloor>
 2. \<And>x P M. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>Ts T mthd xa. \<not> Program P \<turnstile> x sees M: Ts\<rightarrow>T = mthd in xa) \<longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = None
 3. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(drule Methods_into_Methods')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x P M a aa b Ts T mthd xa Mm. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; Mm M = \<lfloor>((Ts, T, mthd), xa)\<rfloor>; \<exists>Mm'. Methods' P x Mm' \<and> Mm = map_of Mm'\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = \<lfloor>(xa, Ts, T, mthd)\<rfloor>
 2. \<And>x P M. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>Ts T mthd xa. \<not> Program P \<turnstile> x sees M: Ts\<rightarrow>T = mthd in xa) \<longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = None
 3. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x P M a aa b Ts T mthd xa Mm'. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; map_of Mm' M = \<lfloor>((Ts, T, mthd), xa)\<rfloor>; Methods' P x Mm'\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) Mm') M = \<lfloor>(xa, Ts, T, mthd)\<rfloor>
 2. \<And>x P M. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>Ts T mthd xa. \<not> Program P \<turnstile> x sees M: Ts\<rightarrow>T = mthd in xa) \<longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = None
 3. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(simp add: split_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x P M a aa b Ts T mthd xa Mm'. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; map_of Mm' M = \<lfloor>((Ts, T, mthd), xa)\<rfloor>; Methods' P x Mm'\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>p. (fst p, snd (snd p), fst (snd p))) Mm') M = \<lfloor>(xa, Ts, T, mthd)\<rfloor>
 2. \<And>x P M. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>Ts T mthd xa. \<not> Program P \<turnstile> x sees M: Ts\<rightarrow>T = mthd in xa) \<longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = None
 3. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(subst map_of_map2[unfolded split_def])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x P M a aa b Ts T mthd xa Mm'. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; map_of Mm' M = \<lfloor>((Ts, T, mthd), xa)\<rfloor>; Methods' P x Mm'\<rbrakk> \<Longrightarrow> map_option (\<lambda>a. (snd a, fst a)) (map_of Mm' M) = \<lfloor>(xa, Ts, T, mthd)\<rfloor>
 2. \<And>x P M. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>Ts T mthd xa. \<not> Program P \<turnstile> x sees M: Ts\<rightarrow>T = mthd in xa) \<longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = None
 3. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x P M. \<exists>a aa b. map_of P x = \<lfloor>(a, aa, b)\<rfloor> \<Longrightarrow> (\<forall>Ts T mthd xa. \<not> Program P \<turnstile> x sees M: Ts\<rightarrow>T = mthd in xa) \<longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = None
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x P M a aa b. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; \<forall>Ts T mthd xa. \<not> Program P \<turnstile> x sees M: Ts\<rightarrow>T = mthd in xa\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P x)) M = None
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(clarsimp simp add: methods'_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x P M a aa b xa. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; \<forall>Ts T mthd xa. \<not> Program P \<turnstile> x sees M: Ts\<rightarrow>T = mthd in xa; Methods' P x xa\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) xa) M = None
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(frule Methods'_into_Methods)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x P M a aa b xa. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; \<forall>Ts T mthd xa. \<not> Program P \<turnstile> x sees M: Ts\<rightarrow>T = mthd in xa; Methods' P x xa; Program P \<turnstile> x sees_methods map_of xa\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) xa) M = None
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(clarsimp simp add: Method_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x P M a aa b xa. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; \<forall>Ts T mthd xa Mm. Program P \<turnstile> x sees_methods Mm \<longrightarrow> Mm M \<noteq> \<lfloor>((Ts, T, mthd), xa)\<rfloor>; Methods' P x xa; Program P \<turnstile> x sees_methods map_of xa\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(M, rest, D). (M, D, rest)) xa) M = None
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(simp add: split_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x P M a aa b xa. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; \<forall>Ts T mthd xa Mm. Program P \<turnstile> x sees_methods Mm \<longrightarrow> Mm M \<noteq> \<lfloor>((Ts, T, mthd), xa)\<rfloor>; Methods' P x xa; Program P \<turnstile> x sees_methods map_of xa\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>p. (fst p, snd (snd p), fst (snd p))) xa) M = None
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(subst map_of_map2[unfolded split_def])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x P M a aa b xa. \<lbrakk>map_of P x = \<lfloor>(a, aa, b)\<rfloor>; \<forall>Ts T mthd xa Mm. Program P \<turnstile> x sees_methods Mm \<longrightarrow> Mm M \<noteq> \<lfloor>((Ts, T, mthd), xa)\<rfloor>; Methods' P x xa; Program P \<turnstile> x sees_methods map_of xa\<rbrakk> \<Longrightarrow> map_option (\<lambda>a. (snd a, fst a)) (map_of xa M) = None
 2. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(fastforce intro: ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<not> is_class (Program P) x \<longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<not> is_class (Program P) x \<Longrightarrow> None = map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x
[PROOF STEP]
apply(rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<not> is_class (Program P) x \<Longrightarrow> map_of (map (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) P) x = None
[PROOF STEP]
apply(simp add: map_of_eq_None_iff is_class_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<notin> fst ` set P \<Longrightarrow> x \<notin> fst ` (\<lambda>x. (fst x, Mapping.of_alist (map (\<lambda>(M, rest, D). (M, D, rest)) (methods' P (fst x))))) ` set P
[PROOF STEP]
apply(simp only: set_map[symmetric] map_map o_def fst_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<notin> set (map fst P) \<Longrightarrow> \<not> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma order_gt_1: "order \<G> > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < order \<G>
[PROOF STEP]
using prime_order
[PROOF STATE]
proof (prove)
using this:
prime (order \<G>)

goal (1 subgoal):
 1. 1 < order \<G>
[PROOF STEP]
using prime_gt_1_nat
[PROOF STATE]
proof (prove)
using this:
prime (order \<G>)
prime ?p \<Longrightarrow> 1 < ?p

goal (1 subgoal):
 1. 1 < order \<G>
[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 order_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < order \<G>

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


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


[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_G: "lossless_spmf G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf G
[PROOF STEP]
by(simp add: G_def)


[STATEMENT]
lemma g'_in_carrier [simp]: "g' \<in> carrier \<G>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g' \<in> carrier \<G>
[PROOF STEP]
using g'_def
[PROOF STATE]
proof (prove)
using this:
g' = \<^bold>g [^] x

goal (1 subgoal):
 1. g' \<in> carrier \<G>
[PROOF STEP]
by auto


[STATEMENT]
lemma "\<Sigma>_protocols_base.R h w c = R2 h w c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h w c = R2 h w c
[PROOF STEP]
by(simp add: \<Sigma>_protocols_base.R_def R2_def; simp add: init_def split_def response_def)


[STATEMENT]
lemma completeness:
  shows "\<Sigma>_protocols_base.completeness"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.completeness
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.completeness
[PROOF STEP]
have "(\<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e)"
    for e y ya :: nat and w' :: "nat \<times> nat"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
have "\<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] ((y + e * fst w')) \<otimes> g' [^] ((ya + e * snd w'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] (y + e * fst w') \<otimes> g' [^] (ya + e * snd w')
[PROOF STEP]
by (simp add: cyclic_group.pow_carrier_mod cyclic_group_axioms g'_def add.commute pow_generator_mod)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] (y + e * fst w') \<otimes> g' [^] (ya + e * snd w')

goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] (y + e * fst w') \<otimes> g' [^] (ya + e * snd w')

goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
have "... = \<^bold>g [^] y \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] ya \<otimes> g' [^] (e * snd w')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] (y + e * fst w') \<otimes> g' [^] (ya + e * snd w') = \<^bold>g [^] y \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] ya \<otimes> g' [^] (e * snd w')
[PROOF STEP]
by (simp add: g'_def m_assoc nat_pow_mult)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (y + e * fst w') \<otimes> g' [^] (ya + e * snd w') = \<^bold>g [^] y \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] ya \<otimes> g' [^] (e * snd w')

goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (y + e * fst w') \<otimes> g' [^] (ya + e * snd w') = \<^bold>g [^] y \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] ya \<otimes> g' [^] (e * snd w')

goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
have "... = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] (e * snd w')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] y \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] ya \<otimes> g' [^] (e * snd w') = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] (e * snd w')
[PROOF STEP]
by (smt add.commute g'_def generator_closed m_assoc nat_pow_closed nat_pow_mult nat_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] y \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] ya \<otimes> g' [^] (e * snd w') = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] (e * snd w')

goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] y \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] ya \<otimes> g' [^] (e * snd w') = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] (e * snd w')

goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
have "... = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> ((\<^bold>g [^] fst w') [^] e \<otimes> (g' [^] snd w') [^] e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] (e * snd w') = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> ((\<^bold>g [^] fst w') [^] e \<otimes> (g' [^] snd w') [^] e)
[PROOF STEP]
by (simp add: m_assoc mult.commute nat_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] y \<otimes> g' [^] ya \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] (e * snd w') = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> ((\<^bold>g [^] fst w') [^] e \<otimes> (g' [^] snd w') [^] e)

goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] y \<otimes> g' [^] ya \<otimes> \<^bold>g [^] (e * fst w') \<otimes> g' [^] (e * snd w') = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> ((\<^bold>g [^] fst w') [^] e \<otimes> (g' [^] snd w') [^] e)

goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
have "... =  \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> ((\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> ((\<^bold>g [^] fst w') [^] e \<otimes> (g' [^] snd w') [^] e) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
by (smt power_distrib g'_def generator_closed mult.commute nat_pow_closed nat_pow_mult nat_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] y \<otimes> g' [^] ya \<otimes> ((\<^bold>g [^] fst w') [^] e \<otimes> (g' [^] snd w') [^] e) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e

goal (1 subgoal):
 1. \<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> ((\<^bold>g [^] fst w') [^] e \<otimes> (g' [^] snd w') [^] e)
\<^bold>g [^] y \<otimes> g' [^] ya \<otimes> ((\<^bold>g [^] fst w') [^] e \<otimes> (g' [^] snd w') [^] e) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ((e * fst w' + y) mod order \<G>) \<otimes> g' [^] ((e * snd w' + ya) mod order \<G>) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> ((\<^bold>g [^] fst w') [^] e \<otimes> (g' [^] snd w') [^] e)
\<^bold>g [^] y \<otimes> g' [^] ya \<otimes> ((\<^bold>g [^] fst w') [^] e \<otimes> (g' [^] snd w') [^] e) = \<^bold>g [^] y \<otimes> g' [^] ya \<otimes> (\<^bold>g [^] fst w' \<otimes> g' [^] snd w') [^] e

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((?e * fst ?w' + ?y) mod order \<G>) \<otimes> g' [^] ((?e * snd ?w' + ?ya) mod order \<G>) = \<^bold>g [^] ?y \<otimes> g' [^] ?ya \<otimes> (\<^bold>g [^] fst ?w' \<otimes> g' [^] snd ?w') [^] ?e

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.completeness
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ((?e * fst ?w' + ?y) mod order \<G>) \<otimes> g' [^] ((?e * snd ?w' + ?ya) mod order \<G>) = \<^bold>g [^] ?y \<otimes> g' [^] ?ya \<otimes> (\<^bold>g [^] fst ?w' \<otimes> g' [^] snd ?w') [^] ?e

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

goal (1 subgoal):
 1. \<forall>h w e. (h, w) \<in> R \<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(simp add: R_def challenge_space_def init_def check_def response_def split_def bind_spmf_const)
[PROOF STATE]
proof (state)
this:
local.\<Sigma>_protocols_base.completeness

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

goal (1 subgoal):
 1. x1 \<noteq> 0 \<Longrightarrow> r1 = ((r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1) mod order \<G>
[PROOF STEP]
have z1_eq: "[(r1 + c * x1) mod (order \<G>) + order \<G> * c * x1 = r1 + c * x1] (mod (order \<G>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(r1 + c * x1) mod order \<G> + order \<G> * c * x1 = r1 + c * x1] (mod order \<G>)
[PROOF STEP]
using gr_implies_not_zero order_gt_1
[PROOF STATE]
proof (prove)
using this:
?m < ?n \<Longrightarrow> ?n \<noteq> (0::?'a)
1 < order \<G>

goal (1 subgoal):
 1. [(r1 + c * x1) mod order \<G> + order \<G> * c * x1 = r1 + c * x1] (mod order \<G>)
[PROOF STEP]
by (simp add: Groups.mult_ac(1) cong_def)
[PROOF STATE]
proof (state)
this:
[(r1 + c * x1) mod order \<G> + order \<G> * c * x1 = r1 + c * x1] (mod order \<G>)

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

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

goal (2 subgoals):
 1. \<lbrakk>[(r1 + c * x1) mod order \<G> + order \<G> * c * x1 = r1 + c * x1] (mod order \<G>); c = 0\<rbrakk> \<Longrightarrow> [(r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1 = r1] (mod order \<G>)
 2. \<lbrakk>[(r1 + c * x1) mod order \<G> + order \<G> * c * x1 = r1 + c * x1] (mod order \<G>); c \<noteq> 0\<rbrakk> \<Longrightarrow> [(r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1 = r1] (mod order \<G>)
[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. [(r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1 = r1] (mod order \<G>)
[PROOF STEP]
using z1_eq
[PROOF STATE]
proof (prove)
using this:
c = 0
[(r1 + c * x1) mod order \<G> + order \<G> * c * x1 = r1 + c * x1] (mod order \<G>)

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

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

goal (1 subgoal):
 1. \<lbrakk>[(r1 + c * x1) mod order \<G> + order \<G> * c * x1 = r1 + c * x1] (mod order \<G>); c \<noteq> 0\<rbrakk> \<Longrightarrow> [(r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1 = r1] (mod order \<G>)
[PROOF STEP]
have "order \<G> * c * x1 - c * x1 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < order \<G> * c * x1 - c * x1
[PROOF STEP]
using x1_neq_0 False
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> 0
c \<noteq> 0

goal (1 subgoal):
 1. 0 < order \<G> * c * x1 - c * x1
[PROOF STEP]
using prime_gt_1_nat prime_order
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> 0
c \<noteq> 0
prime ?p \<Longrightarrow> 1 < ?p
prime (order \<G>)

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

goal (1 subgoal):
 1. \<lbrakk>[(r1 + c * x1) mod order \<G> + order \<G> * c * x1 = r1 + c * x1] (mod order \<G>); c \<noteq> 0\<rbrakk> \<Longrightarrow> [(r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1 = r1] (mod order \<G>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < order \<G> * c * x1 - c * x1

goal (1 subgoal):
 1. [(r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1 = r1] (mod order \<G>)
[PROOF STEP]
by (smt Groups.add_ac(2) add_diff_inverse_nat cong_add_lcancel_nat diff_is_0_eq le_simps(1) neq0_conv trans_less_add2 z1_eq zero_less_diff)
[PROOF STATE]
proof (state)
this:
[(r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1 = r1] (mod order \<G>)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hvzk_z1_r1_tuple_rewrite:
  assumes r1: "r1 < order \<G>"
  shows "(\<^bold>g [^] r1 \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>) =
              (\<^bold>g [^] (((r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1) mod order \<G>)
                  \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<^bold>g [^] r1 \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>) = (\<^bold>g [^] (((r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<^bold>g [^] r1 \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>) = (\<^bold>g [^] (((r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>)
[PROOF STEP]
have "\<^bold>g [^] r1 = \<^bold>g [^] (((r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1) mod order \<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] r1 = \<^bold>g [^] (((r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1) mod order \<G>)
[PROOF STEP]
using assms hvzk_z_r
[PROOF STATE]
proof (prove)
using this:
r1 < order \<G>
?r1.0 < order \<G> \<Longrightarrow> ?r1.0 = ((?r1.0 + ?c * ?x1.0) mod order \<G> + order \<G> * ?c * ?x1.0 - ?c * ?x1.0) mod order \<G>

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

goal (1 subgoal):
 1. (\<^bold>g [^] r1 \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>) = (\<^bold>g [^] (((r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] r1 = \<^bold>g [^] (((r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1) mod order \<G>)

goal (1 subgoal):
 1. (\<^bold>g [^] r1 \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>) = (\<^bold>g [^] (((r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
(\<^bold>g [^] r1 \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>) = (\<^bold>g [^] (((r1 + c * x1) mod order \<G> + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] r2, c, (r1 + c * x1) mod order \<G>, (r2 + c * x2) mod order \<G>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hvzk_z2_r2_tuple_rewrite:
  assumes "xb < order \<G>"
  shows "(\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>)
            \<otimes> g' [^] xb, xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>) =
               (\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>)
                \<otimes> g' [^] (((xb + xa * x2) mod order \<G> + order \<G> * xa * x2 - xa * x2) mod order \<G>), xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>) \<otimes> g' [^] xb, xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>) = (\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>) \<otimes> g' [^] (((xb + xa * x2) mod order \<G> + order \<G> * xa * x2 - xa * x2) mod order \<G>), xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>) \<otimes> g' [^] xb, xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>) = (\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>) \<otimes> g' [^] (((xb + xa * x2) mod order \<G> + order \<G> * xa * x2 - xa * x2) mod order \<G>), xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>)
[PROOF STEP]
have "g' [^] xb = g' [^] (((xb + xa * x2) mod order \<G> + order \<G> * xa * x2 - xa * x2) mod order \<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g' [^] xb = g' [^] (((xb + xa * x2) mod order \<G> + order \<G> * xa * x2 - xa * x2) mod order \<G>)
[PROOF STEP]
using hvzk_z_r assms
[PROOF STATE]
proof (prove)
using this:
?r1.0 < order \<G> \<Longrightarrow> ?r1.0 = ((?r1.0 + ?c * ?x1.0) mod order \<G> + order \<G> * ?c * ?x1.0 - ?c * ?x1.0) mod order \<G>
xb < order \<G>

goal (1 subgoal):
 1. g' [^] xb = g' [^] (((xb + xa * x2) mod order \<G> + order \<G> * xa * x2 - xa * x2) mod order \<G>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g' [^] xb = g' [^] (((xb + xa * x2) mod order \<G> + order \<G> * xa * x2 - xa * x2) mod order \<G>)

goal (1 subgoal):
 1. (\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>) \<otimes> g' [^] xb, xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>) = (\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>) \<otimes> g' [^] (((xb + xa * x2) mod order \<G> + order \<G> * xa * x2 - xa * x2) mod order \<G>), xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
g' [^] xb = g' [^] (((xb + xa * x2) mod order \<G> + order \<G> * xa * x2 - xa * x2) mod order \<G>)

goal (1 subgoal):
 1. (\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>) \<otimes> g' [^] xb, xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>) = (\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>) \<otimes> g' [^] (((xb + xa * x2) mod order \<G> + order \<G> * xa * x2 - xa * x2) mod order \<G>), xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
(\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>) \<otimes> g' [^] xb, xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>) = (\<^bold>g [^] (((x' + xa * x1) mod order \<G> + order \<G> * xa * x1 - xa * x1) mod order \<G>) \<otimes> g' [^] (((xb + xa * x2) mod order \<G> + order \<G> * xa * x2 - xa * x2) mod order \<G>), xa, (x' + xa * x1) mod order \<G>, (xb + xa * x2) mod order \<G>)

goal:
No subgoals!
[PROOF STEP]
qed