[STATEMENT]
lemma g_image_filter_impl:
    "map_image_filter m1.\<alpha> m1.invar m2.\<alpha> m2.invar g_image_filter"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_image_filter m1.\<alpha> m1.invar m2.\<alpha> m2.invar g_image_filter
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
fix m k' v' and f :: "('k1 \<times> 'v1) \<Rightarrow> ('k2 \<times> 'v2) option"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
assume invar_m: "m1.invar m" and
           unique_f: "transforms_to_unique_keys (m1.\<alpha> m) f"
[PROOF STATE]
proof (state)
this:
m1.invar m
transforms_to_unique_keys (m1.\<alpha> m) f

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
have A: "g_image_filter f m =
      iterate_to_map m2.empty m2.update_dj (
        set_iterator_image_filter f (m1.iteratei m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_image_filter f m = iterate_to_map m2.empty m2.update_dj (set_iterator_image_filter f (m1.iteratei m))
[PROOF STEP]
unfolding g_image_filter_def iterate_to_map_alt_def
        set_iterator_image_filter_def case_prod_beta
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m1.iterate m (\<lambda>kv \<sigma>. case f kv of None \<Rightarrow> \<sigma> | Some a \<Rightarrow> m2.update_dj (fst a) (snd a) \<sigma>) (m2.empty ()) = m1.iterate m (\<lambda>x \<sigma>. case f x of None \<Rightarrow> \<sigma> | Some x' \<Rightarrow> m2.update_dj (fst x') (snd x') \<sigma>) (m2.empty ())
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g_image_filter f m = iterate_to_map m2.empty m2.update_dj (set_iterator_image_filter f (m1.iteratei m))

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
from m1.iteratei_correct[OF invar_m]
[PROOF STATE]
proof (chain)
picking this:
map_iterator (m1.iteratei m) (m1.\<alpha> m)
[PROOF STEP]
have iti_m: "map_iterator (m1.iteratei m) (m1.\<alpha> m)"
[PROOF STATE]
proof (prove)
using this:
map_iterator (m1.iteratei m) (m1.\<alpha> m)

goal (1 subgoal):
 1. map_iterator (m1.iteratei m) (m1.\<alpha> m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_iterator (m1.iteratei m) (m1.\<alpha> m)

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
from unique_f
[PROOF STATE]
proof (chain)
picking this:
transforms_to_unique_keys (m1.\<alpha> m) f
[PROOF STEP]
have inj_on_f: "inj_on f (map_to_set (m1.\<alpha> m) \<inter> dom f)"
[PROOF STATE]
proof (prove)
using this:
transforms_to_unique_keys (m1.\<alpha> m) f

goal (1 subgoal):
 1. inj_on f (map_to_set (m1.\<alpha> m) \<inter> dom f)
[PROOF STEP]
unfolding transforms_to_unique_keys_def inj_on_def Ball_def map_to_set_def
[PROOF STATE]
proof (prove)
using this:
\<forall>k1 k2 v1 v2 k' v1' v2'. m1.\<alpha> m k1 = Some v1 \<and> m1.\<alpha> m k2 = Some v2 \<and> f (k1, v1) = Some (k', v1') \<and> f (k2, v2) = Some (k', v2') \<longrightarrow> k1 = k2

goal (1 subgoal):
 1. \<forall>x. x \<in> {(k, v). m1.\<alpha> m k = Some v} \<inter> dom f \<longrightarrow> (\<forall>xa. xa \<in> {(k, v). m1.\<alpha> m k = Some v} \<inter> dom f \<longrightarrow> f x = f xa \<longrightarrow> x = xa)
[PROOF STEP]
by auto (metis option.inject)
[PROOF STATE]
proof (state)
this:
inj_on f (map_to_set (m1.\<alpha> m) \<inter> dom f)

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
define vP where "vP k v \<longleftrightarrow> (\<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (k, v))" for k v
[PROOF STATE]
proof (state)
this:
vP ?k ?v = (\<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (?k, ?v))

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
have vP_intro: "\<And>k v. (\<exists>k' v'. m1.\<alpha> m k' = Some v'
        \<and> f (k', v') = Some (k, v)) \<longleftrightarrow> vP k v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k v. (\<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (k, v)) = vP k v
[PROOF STEP]
unfolding vP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k v. (\<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (k, v)) = (\<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (k, v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (?k3, ?v3)) = vP ?k3 ?v3

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (?k3, ?v3)) = vP ?k3 ?v3

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
fix k v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
have "Eps_Opt (vP k) = Some v \<longleftrightarrow> vP k v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Eps_Opt (vP k) = Some v) = vP k v
[PROOF STEP]
using unique_f
[PROOF STATE]
proof (prove)
using this:
transforms_to_unique_keys (m1.\<alpha> m) f

goal (1 subgoal):
 1. (Eps_Opt (vP k) = Some v) = vP k v
[PROOF STEP]
unfolding vP_def transforms_to_unique_keys_def
[PROOF STATE]
proof (prove)
using this:
\<forall>k1 k2 v1 v2 k' v1' v2'. m1.\<alpha> m k1 = Some v1 \<and> m1.\<alpha> m k2 = Some v2 \<and> f (k1, v1) = Some (k', v1') \<and> f (k2, v2) = Some (k', v2') \<longrightarrow> k1 = k2

goal (1 subgoal):
 1. (Eps_Opt (\<lambda>v. \<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (k, v)) = Some v) = (\<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (k, v))
[PROOF STEP]
apply (rule_tac Eps_Opt_eq_Some)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x'. \<lbrakk>\<forall>k1 k2 v1 v2 k' v1' v2'. m1.\<alpha> m k1 = Some v1 \<and> m1.\<alpha> m k2 = Some v2 \<and> f (k1, v1) = Some (k', v1') \<and> f (k2, v2) = Some (k', v2') \<longrightarrow> k1 = k2; \<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (k, v); \<exists>k' v'. m1.\<alpha> m k' = Some v' \<and> f (k', v') = Some (k, x')\<rbrakk> \<Longrightarrow> x' = v
[PROOF STEP]
apply (metis prod.inject option.inject)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(Eps_Opt (vP k) = Some v) = vP k v

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(Eps_Opt (vP ?k5) = Some ?v5) = vP ?k5 ?v5

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
note Eps_vP_elim[simp] = this
[PROOF STATE]
proof (state)
this:
(Eps_Opt (vP ?k5) = Some ?v5) = vP ?k5 ?v5

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
have map_intro: "{y. \<exists>x. x \<in> map_to_set (m1.\<alpha> m) \<and> f x = Some y}
      = map_to_set (\<lambda>k. Eps_Opt (vP k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x. x \<in> map_to_set (m1.\<alpha> m) \<and> f x = Some y} = map_to_set (\<lambda>k. Eps_Opt (vP k))
[PROOF STEP]
by (simp add: map_to_set_def vP_intro set_eq_iff split: prod.splits)
[PROOF STATE]
proof (state)
this:
{y. \<exists>x. x \<in> map_to_set (m1.\<alpha> m) \<and> f x = Some y} = map_to_set (\<lambda>k. Eps_Opt (vP k))

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
from set_iterator_image_filter_correct [OF iti_m, OF inj_on_f,
      unfolded map_intro]
[PROOF STATE]
proof (chain)
picking this:
map_iterator (set_iterator_image_filter f (m1.iteratei m)) (\<lambda>k. Eps_Opt (vP k))
[PROOF STEP]
have iti_filter: "map_iterator (set_iterator_image_filter f (m1.iteratei m))
          (\<lambda>k. Eps_Opt (vP k))"
[PROOF STATE]
proof (prove)
using this:
map_iterator (set_iterator_image_filter f (m1.iteratei m)) (\<lambda>k. Eps_Opt (vP k))

goal (1 subgoal):
 1. map_iterator (set_iterator_image_filter f (m1.iteratei m)) (\<lambda>k. Eps_Opt (vP k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_iterator (set_iterator_image_filter f (m1.iteratei m)) (\<lambda>k. Eps_Opt (vP k))

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
have upd: "map_update_dj m2.\<alpha> m2.invar m2.update_dj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_update_dj m2.\<alpha> m2.invar m2.update_dj
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
this:
map_update_dj m2.\<alpha> m2.invar m2.update_dj

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
have emp: "map_empty m2.\<alpha> m2.invar m2.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_empty m2.\<alpha> m2.invar m2.empty
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
this:
map_empty m2.\<alpha> m2.invar m2.empty

goal (1 subgoal):
 1. \<And>m f k' v'. \<lbrakk>m1.invar m; transforms_to_unique_keys (m1.\<alpha> m) f\<rbrakk> \<Longrightarrow> m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
from iterate_to_map_correct[OF upd emp iti_filter]
[PROOF STATE]
proof (chain)
picking this:
m2.\<alpha> (iterate_to_map m2.empty m2.update_dj (set_iterator_image_filter f (m1.iteratei m))) = (\<lambda>k. Eps_Opt (vP k)) \<and> m2.invar (iterate_to_map m2.empty m2.update_dj (set_iterator_image_filter f (m1.iteratei m)))
[PROOF STEP]
show
      "map_op_invar ops2 (g_image_filter f m) \<and>
          (map_op_\<alpha> ops2 (g_image_filter f m) k' = Some v') =
          (\<exists>k v. map_op_\<alpha> ops1 m k = Some v \<and> f (k, v) = Some (k', v'))"
[PROOF STATE]
proof (prove)
using this:
m2.\<alpha> (iterate_to_map m2.empty m2.update_dj (set_iterator_image_filter f (m1.iteratei m))) = (\<lambda>k. Eps_Opt (vP k)) \<and> m2.invar (iterate_to_map m2.empty m2.update_dj (set_iterator_image_filter f (m1.iteratei m)))

goal (1 subgoal):
 1. m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))
[PROOF STEP]
unfolding A vP_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
m2.\<alpha> (iterate_to_map m2.empty m2.update_dj (set_iterator_image_filter f (m1.iteratei m))) = (\<lambda>k. Eps_Opt (vP k)) \<and> m2.invar (iterate_to_map m2.empty m2.update_dj (set_iterator_image_filter f (m1.iteratei m)))

goal (1 subgoal):
 1. m2.invar (iterate_to_map m2.empty m2.update_dj (set_iterator_image_filter f (m1.iteratei m))) \<and> (m2.\<alpha> (iterate_to_map m2.empty m2.update_dj (set_iterator_image_filter f (m1.iteratei m))) k' = Some v') = vP k' v'
[PROOF STEP]
by (simp add: vP_intro)
[PROOF STATE]
proof (state)
this:
m2.invar (g_image_filter f m) \<and> (m2.\<alpha> (g_image_filter f m) k' = Some v') = (\<exists>k v. m1.\<alpha> m k = Some v \<and> f (k, v) = Some (k', v'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma restrict_map_dom_subset: "\<lbrakk> dom m \<subseteq> R\<rbrakk> \<Longrightarrow> m|`R = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom m \<subseteq> R \<Longrightarrow> m |` R = m
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. dom m \<subseteq> R \<Longrightarrow> (m |` R) x = m x
[PROOF STEP]
apply (auto simp: restrict_map_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>dom m \<subseteq> R; x \<notin> R\<rbrakk> \<Longrightarrow> None = m x
[PROOF STEP]
apply (case_tac "m x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>dom m \<subseteq> R; x \<notin> R; m x = None\<rbrakk> \<Longrightarrow> None = m x
 2. \<And>x a. \<lbrakk>dom m \<subseteq> R; x \<notin> R; m x = Some a\<rbrakk> \<Longrightarrow> None = m x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma g_value_image_filter_impl:
    "map_value_image_filter m1.\<alpha> m1.invar m2.\<alpha> m2.invar g_value_image_filter"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_value_image_filter m1.\<alpha> m1.invar m2.\<alpha> m2.invar g_value_image_filter
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m f. m1.invar m \<Longrightarrow> m2.invar (g_value_image_filter f m) \<and> m2.\<alpha> (g_value_image_filter f m) = (\<lambda>k. m1.\<alpha> m k \<bind> f k)
[PROOF STEP]
unfolding g_value_image_filter_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m f. m1.invar m \<Longrightarrow> m2.invar (m1.iterate m (\<lambda>(k, v) \<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) (m2.empty ())) \<and> m2.\<alpha> (m1.iterate m (\<lambda>(k, v) \<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) (m2.empty ())) = (\<lambda>k. m1.\<alpha> m k \<bind> f k)
[PROOF STEP]
apply (rule_tac I="\<lambda>it \<sigma>. m2.invar \<sigma>
      \<and> m2.\<alpha> \<sigma> = (\<lambda>k. Option.bind (map_op_\<alpha> ops1 m k) (f k)) |` it"
      in m1.old_iterate_rule_insert_P)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>m f. m1.invar m \<Longrightarrow> m1.invar m
 2. \<And>m f. m1.invar m \<Longrightarrow> m2.invar (m2.empty ()) \<and> m2.\<alpha> (m2.empty ()) = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` {}
 3. \<And>m f k v it \<sigma>. \<lbrakk>m1.invar m; k \<in> dom (m1.\<alpha> m) - it; m1.\<alpha> m k = Some v; it \<subseteq> dom (m1.\<alpha> m); m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it\<rbrakk> \<Longrightarrow> m2.invar ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) \<and> m2.\<alpha> ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` insert k it
 4. \<And>m f \<sigma>. \<lbrakk>m1.invar m; m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` dom (m1.\<alpha> m)\<rbrakk> \<Longrightarrow> m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k)
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m f. m1.invar m \<Longrightarrow> m2.invar (m2.empty ()) \<and> m2.\<alpha> (m2.empty ()) = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` {}
 2. \<And>m f k v it \<sigma>. \<lbrakk>m1.invar m; k \<in> dom (m1.\<alpha> m) - it; m1.\<alpha> m k = Some v; it \<subseteq> dom (m1.\<alpha> m); m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it\<rbrakk> \<Longrightarrow> m2.invar ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) \<and> m2.\<alpha> ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` insert k it
 3. \<And>m f \<sigma>. \<lbrakk>m1.invar m; m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` dom (m1.\<alpha> m)\<rbrakk> \<Longrightarrow> m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k)
[PROOF STEP]
apply (auto simp: m2.empty_correct) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m f k v it \<sigma>. \<lbrakk>m1.invar m; k \<in> dom (m1.\<alpha> m) - it; m1.\<alpha> m k = Some v; it \<subseteq> dom (m1.\<alpha> m); m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it\<rbrakk> \<Longrightarrow> m2.invar ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) \<and> m2.\<alpha> ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` insert k it
 2. \<And>m f \<sigma>. \<lbrakk>m1.invar m; m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` dom (m1.\<alpha> m)\<rbrakk> \<Longrightarrow> m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m f \<sigma>. \<lbrakk>m1.invar m; m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` dom (m1.\<alpha> m)\<rbrakk> \<Longrightarrow> m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k)
 2. \<And>m f k v it \<sigma>. \<lbrakk>m1.invar m; k \<in> dom (m1.\<alpha> m) - it; m1.\<alpha> m k = Some v; it \<subseteq> dom (m1.\<alpha> m); m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it\<rbrakk> \<Longrightarrow> m2.invar ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) \<and> m2.\<alpha> ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` insert k it
[PROOF STEP]
apply simp []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m f \<sigma>. \<lbrakk>m1.invar m; m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` dom (m1.\<alpha> m)\<rbrakk> \<Longrightarrow> (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` dom (m1.\<alpha> m) = (\<lambda>k. m1.\<alpha> m k \<bind> f k)
 2. \<And>m f k v it \<sigma>. \<lbrakk>m1.invar m; k \<in> dom (m1.\<alpha> m) - it; m1.\<alpha> m k = Some v; it \<subseteq> dom (m1.\<alpha> m); m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it\<rbrakk> \<Longrightarrow> m2.invar ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) \<and> m2.\<alpha> ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` insert k it
[PROOF STEP]
apply (rule restrict_map_dom_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m f \<sigma>. \<lbrakk>m1.invar m; m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` dom (m1.\<alpha> m)\<rbrakk> \<Longrightarrow> dom (\<lambda>k. m1.\<alpha> m k \<bind> f k) \<subseteq> dom (m1.\<alpha> m)
 2. \<And>m f k v it \<sigma>. \<lbrakk>m1.invar m; k \<in> dom (m1.\<alpha> m) - it; m1.\<alpha> m k = Some v; it \<subseteq> dom (m1.\<alpha> m); m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it\<rbrakk> \<Longrightarrow> m2.invar ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) \<and> m2.\<alpha> ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` insert k it
[PROOF STEP]
apply (auto) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m f \<sigma> x y. \<lbrakk>m1.invar m; m1.\<alpha> m x \<bind> f x = Some y; m2.invar \<sigma>; m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` dom (m1.\<alpha> m)\<rbrakk> \<Longrightarrow> \<exists>y. m1.\<alpha> m x = Some y
 2. \<And>m f k v it \<sigma>. \<lbrakk>m1.invar m; k \<in> dom (m1.\<alpha> m) - it; m1.\<alpha> m k = Some v; it \<subseteq> dom (m1.\<alpha> m); m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it\<rbrakk> \<Longrightarrow> m2.invar ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) \<and> m2.\<alpha> ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` insert k it
[PROOF STEP]
apply (case_tac "m1.\<alpha> m x")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m f \<sigma> x y. \<lbrakk>m1.invar m; m1.\<alpha> m x \<bind> f x = Some y; m2.invar \<sigma>; m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` dom (m1.\<alpha> m); m1.\<alpha> m x = None\<rbrakk> \<Longrightarrow> \<exists>y. m1.\<alpha> m x = Some y
 2. \<And>m f \<sigma> x y a. \<lbrakk>m1.invar m; m1.\<alpha> m x \<bind> f x = Some y; m2.invar \<sigma>; m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` dom (m1.\<alpha> m); m1.\<alpha> m x = Some a\<rbrakk> \<Longrightarrow> \<exists>y. m1.\<alpha> m x = Some y
 3. \<And>m f k v it \<sigma>. \<lbrakk>m1.invar m; k \<in> dom (m1.\<alpha> m) - it; m1.\<alpha> m k = Some v; it \<subseteq> dom (m1.\<alpha> m); m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it\<rbrakk> \<Longrightarrow> m2.invar ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) \<and> m2.\<alpha> ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` insert k it
[PROOF STEP]
apply (auto) [2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m f k v it \<sigma>. \<lbrakk>m1.invar m; k \<in> dom (m1.\<alpha> m) - it; m1.\<alpha> m k = Some v; it \<subseteq> dom (m1.\<alpha> m); m2.invar \<sigma> \<and> m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it\<rbrakk> \<Longrightarrow> m2.invar ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) \<and> m2.\<alpha> ((case (k, v) of (k, v) \<Rightarrow> \<lambda>\<sigma>. case f k v of None \<Rightarrow> \<sigma> | Some v' \<Rightarrow> m2.update_dj k v' \<sigma>) \<sigma>) = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` insert k it
[PROOF STEP]
apply (auto split: option.split simp: m2.update_dj_correct intro!: ext)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m f k v it \<sigma> x. \<lbrakk>m1.invar m; it \<subseteq> dom (m1.\<alpha> m); k \<notin> it; m1.\<alpha> m k = Some v; m2.invar \<sigma>; m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it; f k v = None\<rbrakk> \<Longrightarrow> ((\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it) x = ((\<lambda>k. m1.\<alpha> m k \<bind> f k) |` insert k it) x
 2. \<And>m f k v it \<sigma> x2 x. \<lbrakk>m1.invar m; it \<subseteq> dom (m1.\<alpha> m); k \<notin> it; m1.\<alpha> m k = Some v; m2.invar \<sigma>; m2.\<alpha> \<sigma> = (\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it; f k v = Some x2; x \<noteq> k\<rbrakk> \<Longrightarrow> ((\<lambda>k. m1.\<alpha> m k \<bind> f k) |` it) x = ((\<lambda>k. m1.\<alpha> m k \<bind> f k) |` insert k it) x
[PROOF STEP]
apply (auto simp: restrict_map_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma q_gt_0 [simp]: "q > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q
[PROOF STEP]
by (simp add: prime_q prime_gt_0_nat)


[STATEMENT]
lemma abstract_correct: "rivest_commit.correct"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rivest_commit.correct
[PROOF STEP]
unfolding abstract_commitment.correct_def abstract_commitment.correct_game_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m. valid_msg m \<longrightarrow> spmf (key_gen \<bind> (\<lambda>(ck, vk). commit ck m \<bind> (\<lambda>(c, d). return_spmf (verify vk m c d)))) True = 1
[PROOF STEP]
by(simp add: key_gen_def commit_def bind_spmf_const lossless_weight_spmfD)


[STATEMENT]
lemma rivest_hiding: "(spmf (rivest_commit.hiding_game_ind_cpa \) True - 1/2 = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
note [simp] = Let_def split_def
[PROOF STATE]
proof (state)
this:
Let ?s ?f \<equiv> ?f ?s
case_prod = (\<lambda>c p. c (fst p) (snd p))

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
obtain \1 \2 where [simp]: "\ = (\1, \2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\1 \2. \ = (\1, \2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases \)
[PROOF STATE]
proof (state)
this:
\ = (\1, \2)

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
have "rivest_commit.hiding_game_ind_cpa (\1, \2) = TRY do {
    a :: nat \<leftarrow> sample_uniform q;
    x1 :: nat \<leftarrow> sample_uniform q;
    y1 \<leftarrow> map_spmf (\<lambda> b. (a * x1 + b) mod q) (sample_uniform q);
    ((m0, m1), \<sigma>) \<leftarrow> \1 (x1,y1);
    _ :: unit \<leftarrow> assert_spmf (valid_msg m0 \<and> valid_msg m1);
    d \<leftarrow> coin_spmf;
    let c = ((if d then m0 else m1) + a) mod q;
    b' \<leftarrow> \2 c \<sigma>;
    return_spmf (b' = d)} ELSE coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rivest_commit.hiding_game_ind_cpa (\1, \2) = TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. map_spmf (\<lambda>b. (a * x1 + b) mod q) (sample_uniform q) \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf
[PROOF STEP]
unfolding abstract_commitment.hiding_game_ind_cpa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (\1, \2) of (\1, \2) \<Rightarrow> TRY key_gen \<bind> (\<lambda>(ck, vk). \1 vk \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>b. commit ck (if b then m0 else m1) \<bind> (\<lambda>(c, d). \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = b))))))) ELSE coin_spmf) = TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. map_spmf (\<lambda>b. (a * x1 + b) mod q) (sample_uniform q) \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf
[PROOF STEP]
by(simp add: commit_def key_gen_def o_def bind_map_spmf)
[PROOF STATE]
proof (state)
this:
rivest_commit.hiding_game_ind_cpa (\1, \2) = TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. map_spmf (\<lambda>b. (a * x1 + b) mod q) (sample_uniform q) \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rivest_commit.hiding_game_ind_cpa (\1, \2) = TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. map_spmf (\<lambda>b. (a * x1 + b) mod q) (sample_uniform q) \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
have "... = TRY do {
    a :: nat \<leftarrow> sample_uniform q;
    x1 :: nat \<leftarrow> sample_uniform q;
    y1 \<leftarrow> sample_uniform q;
    ((m0, m1), \<sigma>) \<leftarrow> \1 (x1,y1);
    _ :: unit \<leftarrow> assert_spmf (valid_msg m0 \<and> valid_msg m1);
    d \<leftarrow> coin_spmf;
    let c = ((if d then m0 else m1) + a) mod q;
    b' \<leftarrow> \2 c \<sigma>;
    return_spmf (b' = d)} ELSE coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. map_spmf (\<lambda>b. (a * x1 + b) mod q) (sample_uniform q) \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf
[PROOF STEP]
by(simp add: samp_uni_plus_one_time_pad)
[PROOF STATE]
proof (state)
this:
TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. map_spmf (\<lambda>b. (a * x1 + b) mod q) (sample_uniform q) \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. map_spmf (\<lambda>b. (a * x1 + b) mod q) (sample_uniform q) \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
have "... = TRY do {
    x1 :: nat \<leftarrow> sample_uniform q;
    y1 \<leftarrow> sample_uniform q;
    ((m0, m1), \<sigma>) \<leftarrow> \1 (x1,y1);
    _ :: unit \<leftarrow> assert_spmf (valid_msg m0 \<and> valid_msg m1);
    d \<leftarrow> coin_spmf;
    c \<leftarrow> map_spmf (\<lambda> a. ((if d then m0 else m1) + a) mod q) (sample_uniform q);
    b' \<leftarrow> \2 c \<sigma>;
    return_spmf (b' = d)} ELSE coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. map_spmf (\<lambda>a. ((if d then m0 else m1) + a) mod q) (sample_uniform q) \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf
[PROOF STEP]
by(simp add: o_def bind_map_spmf)
[PROOF STATE]
proof (state)
this:
TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. map_spmf (\<lambda>a. ((if d then m0 else m1) + a) mod q) (sample_uniform q) \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TRY sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. let c = ((if d then m0 else m1) + a) mod q in \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. map_spmf (\<lambda>a. ((if d then m0 else m1) + a) mod q) (sample_uniform q) \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
have "... = TRY do {
    x1 :: nat \<leftarrow> sample_uniform q;
    y1 \<leftarrow> sample_uniform q;
    ((m0, m1), \<sigma>) \<leftarrow> \1 (x1,y1);
    _ :: unit \<leftarrow> assert_spmf (valid_msg m0 \<and> valid_msg m1);
    d \<leftarrow> coin_spmf;
    c \<leftarrow> sample_uniform q;
    b' :: bool \<leftarrow> \2 c \<sigma>;
    return_spmf (b' = d)} ELSE coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. map_spmf (\<lambda>a. ((if d then m0 else m1) + a) mod q) (sample_uniform q) \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf
[PROOF STEP]
by(simp add: samp_uni_plus_one_time_pad)
[PROOF STATE]
proof (state)
this:
TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. map_spmf (\<lambda>a. ((if d then m0 else m1) + a) mod q) (sample_uniform q) \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. map_spmf (\<lambda>a. ((if d then m0 else m1) + a) mod q) (sample_uniform q) \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
have "... = TRY do {
    x1 :: nat \<leftarrow> sample_uniform q;
    y1 \<leftarrow> sample_uniform q;
    ((m0, m1), \<sigma>) \<leftarrow> \1 (x1,y1);
    _ :: unit \<leftarrow> assert_spmf (valid_msg m0 \<and> valid_msg m1);
    c :: nat \<leftarrow> sample_uniform q;
    guess :: bool \<leftarrow> \2 c \<sigma>;
    map_spmf((=) guess) coin_spmf} ELSE coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf
[PROOF STEP]
by(simp add: map_spmf_conv_bind_spmf)
[PROOF STATE]
proof (state)
this:
TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. coin_spmf \<bind> (\<lambda>d. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>b'. return_spmf (b' = d)))))))) ELSE coin_spmf = TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
have "... = coin_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf = coin_spmf
[PROOF STEP]
by(simp add: map_eq_const_coin_spmf bind_spmf_const try_bind_spmf_lossless2'
        scale_bind_spmf weight_spmf_le_1 scale_scale_spmf)
[PROOF STATE]
proof (state)
this:
TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf = coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rivest_commit.hiding_game_ind_cpa (\1, \2) = TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf
TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf = coin_spmf
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rivest_commit.hiding_game_ind_cpa (\1, \2) = TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf
TRY sample_uniform q \<bind> (\<lambda>x1. sample_uniform q \<bind> (\<lambda>y1. \1 (x1, y1) \<bind> (\<lambda>((m0, m1), \<sigma>). assert_spmf (valid_msg m0 \<and> valid_msg m1) \<bind> (\<lambda>_. sample_uniform q \<bind> (\<lambda>c. \2 c \<sigma> \<bind> (\<lambda>guess. map_spmf ((=) guess) coin_spmf)))))) ELSE coin_spmf = coin_spmf

goal (1 subgoal):
 1. spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0
[PROOF STEP]
by(simp add: spmf_of_set)
[PROOF STATE]
proof (state)
this:
spmf (rivest_commit.hiding_game_ind_cpa \) True - 1 / 2 = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rivest_perfect_hiding: "rivest_commit.perfect_hiding_ind_cpa \<A>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rivest_commit.perfect_hiding_ind_cpa \<A>
[PROOF STEP]
unfolding abstract_commitment.perfect_hiding_ind_cpa_def abstract_commitment.hiding_advantage_ind_cpa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (rivest_commit.hiding_game_ind_cpa \<A>) True - 1 / 2\<bar> = 0
[PROOF STEP]
by(simp add: rivest_hiding)


[STATEMENT]
lemma samp_uni_break':
  assumes fst_cond: "m \<noteq> m' \<and> valid_msg m \<and> valid_msg m'"
    and c: "c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q"
    and  c': "c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q"
    and x1: "x1 < q"
  shows "x1 = (if (a mod q > a' mod q) then nat ((int b'- int b) * (inverse (nat ((int a mod q - int a' mod q) mod q)) q) mod q)  else
          nat ((int b- int b') * (inverse (nat ((int a' mod q - int a mod q) mod q)) q) mod q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
have m: "m < q \<and> m' < q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < q \<and> m' < q
[PROOF STEP]
using fst_cond valid_msg_def
[PROOF STATE]
proof (prove)
using this:
m \<noteq> m' \<and> valid_msg m \<and> valid_msg m'
valid_msg ?msg \<equiv> ?msg \<in> {..<q}

goal (1 subgoal):
 1. m < q \<and> m' < q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m < q \<and> m' < q

goal (1 subgoal):
 1. x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
have a_a': "\<not> [a = a'] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a \<noteq> a'] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a \<noteq> a'] (mod q)
[PROOF STEP]
have "[m + a = m' + a'] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [m + a = m' + a'] (mod q)
[PROOF STEP]
using assms cong_def
[PROOF STATE]
proof (prove)
using this:
m \<noteq> m' \<and> valid_msg m \<and> valid_msg m'
c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q
c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q
x1 < q
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. [m + a = m' + a'] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[m + a = m' + a'] (mod q)

goal (1 subgoal):
 1. [a \<noteq> a'] (mod q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[m + a = m' + a'] (mod q)

goal (1 subgoal):
 1. [a \<noteq> a'] (mod q)
[PROOF STEP]
by (metis m fst_cond c c' add.commute cong_less_modulus_unique_nat cong_add_rcancel_nat cong_mod_right)
[PROOF STATE]
proof (state)
this:
[a \<noteq> a'] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[a \<noteq> a'] (mod q)

goal (1 subgoal):
 1. x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
have cong_y1: "[int a * int x1 + int b = int a' * int x1 + int b'] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [int a * int x1 + int b = int a' * int x1 + int b'] (mod int q)
[PROOF STEP]
by (metis c c' cong_def Num.of_nat_simps(4) Num.of_nat_simps(5) cong_int_iff)
[PROOF STATE]
proof (state)
this:
[int a * int x1 + int b = int a' * int x1 + int b'] (mod int q)

goal (1 subgoal):
 1. x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
proof(cases "a mod q > a' mod q")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a' mod q < a mod q

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence gcd: "gcd (nat ((int a mod q - int a' mod q) mod q)) q = 1"
[PROOF STATE]
proof (prove)
using this:
a' mod q < a mod q

goal (1 subgoal):
 1. gcd (nat ((int a mod int q - int a' mod int q) mod int q)) q = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a' mod q < a mod q \<Longrightarrow> gcd (nat ((int a mod int q - int a' mod int q) mod int q)) q = 1
[PROOF STEP]
have "((int a mod q - int a' mod q) mod q) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (int a mod int q - int a' mod int q) mod int q \<noteq> 0
[PROOF STEP]
by (metis True comm_monoid_add_class.add_0 diff_add_cancel mod_add_left_eq mod_diff_eq nat_mod_as_int order_less_irrefl)
[PROOF STATE]
proof (state)
this:
(int a mod int q - int a' mod int q) mod int q \<noteq> 0

goal (1 subgoal):
 1. a' mod q < a mod q \<Longrightarrow> gcd (nat ((int a mod int q - int a' mod int q) mod int q)) q = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(int a mod int q - int a' mod int q) mod int q \<noteq> 0

goal (1 subgoal):
 1. a' mod q < a mod q \<Longrightarrow> gcd (nat ((int a mod int q - int a' mod int q) mod int q)) q = 1
[PROOF STEP]
have "((int a mod q - int a' mod q) mod q) < q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (int a mod int q - int a' mod int q) mod int q < int q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(int a mod int q - int a' mod int q) mod int q < int q

goal (1 subgoal):
 1. a' mod q < a mod q \<Longrightarrow> gcd (nat ((int a mod int q - int a' mod int q) mod int q)) q = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(int a mod int q - int a' mod int q) mod int q \<noteq> 0
(int a mod int q - int a' mod int q) mod int q < int q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(int a mod int q - int a' mod int q) mod int q \<noteq> 0
(int a mod int q - int a' mod int q) mod int q < int q

goal (1 subgoal):
 1. gcd (nat ((int a mod int q - int a' mod int q) mod int q)) q = 1
[PROOF STEP]
using prime_field[of q "nat ((int a mod int q - int a' mod int q) mod int q)"] prime_q
[PROOF STATE]
proof (prove)
using this:
(int a mod int q - int a' mod int q) mod int q \<noteq> 0
(int a mod int q - int a' mod int q) mod int q < int q
\<lbrakk>prime q; nat ((int a mod int q - int a' mod int q) mod int q) < q; nat ((int a mod int q - int a' mod int q) mod int q) \<noteq> 0\<rbrakk> \<Longrightarrow> coprime (nat ((int a mod int q - int a' mod int q) mod int q)) q
prime q

goal (1 subgoal):
 1. gcd (nat ((int a mod int q - int a' mod int q) mod int q)) q = 1
[PROOF STEP]
by (smt Euclidean_Division.pos_mod_sign coprime_imp_gcd_eq_1 int_nat_eq nat_less_iff of_nat_0_less_iff q_gt_0)
[PROOF STATE]
proof (state)
this:
gcd (nat ((int a mod int q - int a' mod int q) mod int q)) q = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gcd (nat ((int a mod int q - int a' mod int q) mod int q)) q = 1

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int a * int x1 - int a' * int x1 = int b'- int b] (mod q)"
[PROOF STATE]
proof (prove)
using this:
gcd (nat ((int a mod int q - int a' mod int q) mod int q)) q = 1

goal (1 subgoal):
 1. [int a * int x1 - int a' * int x1 = int b' - int b] (mod int q)
[PROOF STEP]
by (smt cong_diff_iff_cong_0 cong_y1 cong_diff cong_diff)
[PROOF STATE]
proof (state)
this:
[int a * int x1 - int a' * int x1 = int b' - int b] (mod int q)

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int a mod q * int x1 - int a' mod q * int x1 = int b'- int b] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int a * int x1 - int a' * int x1 = int b' - int b] (mod int q)

goal (1 subgoal):
 1. [int a mod int q * int x1 - int a' mod int q * int x1 = int b' - int b] (mod int q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [int a * int x1 - int a' * int x1 = int b' - int b] (mod int q) \<Longrightarrow> [int a mod int q * int x1 - int a' mod int q * int x1 = int b' - int b] (mod int q)
[PROOF STEP]
have "[int x1 * (int a mod int q - int a' mod int q) = int x1 * (int a - int a')] (mod int q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [int x1 * (int a mod int q - int a' mod int q) = int x1 * (int a - int a')] (mod int q)
[PROOF STEP]
by (meson cong_def cong_mult cong_refl mod_diff_eq)
[PROOF STATE]
proof (state)
this:
[int x1 * (int a mod int q - int a' mod int q) = int x1 * (int a - int a')] (mod int q)

goal (1 subgoal):
 1. [int a * int x1 - int a' * int x1 = int b' - int b] (mod int q) \<Longrightarrow> [int a mod int q * int x1 - int a' mod int q * int x1 = int b' - int b] (mod int q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[int x1 * (int a mod int q - int a' mod int q) = int x1 * (int a - int a')] (mod int q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[int x1 * (int a mod int q - int a' mod int q) = int x1 * (int a - int a')] (mod int q)

goal (1 subgoal):
 1. [int a mod int q * int x1 - int a' mod int q * int x1 = int b' - int b] (mod int q)
[PROOF STEP]
by (metis (no_types, opaque_lifting) Groups.mult_ac(2) \<open>[int a * int x1 - int a' * int x1 = int b' - int b] (mod int q)\<close> cong_def mod_diff_left_eq mod_diff_right_eq mod_mult_right_eq)
[PROOF STATE]
proof (state)
this:
[int a mod int q * int x1 - int a' mod int q * int x1 = int b' - int b] (mod int q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[int a mod int q * int x1 - int a' mod int q * int x1 = int b' - int b] (mod int q)

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int x1 * (int a mod q - int a' mod q) = int b'- int b] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int a mod int q * int x1 - int a' mod int q * int x1 = int b' - int b] (mod int q)

goal (1 subgoal):
 1. [int x1 * (int a mod int q - int a' mod int q) = int b' - int b] (mod int q)
[PROOF STEP]
by(metis int_distrib(3) mult.commute)
[PROOF STATE]
proof (state)
this:
[int x1 * (int a mod int q - int a' mod int q) = int b' - int b] (mod int q)

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int x1 * (int a mod q - int a' mod q) mod q = int b'- int b] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int x1 * (int a mod int q - int a' mod int q) = int b' - int b] (mod int q)

goal (1 subgoal):
 1. [int x1 * (int a mod int q - int a' mod int q) mod int q = int b' - int b] (mod int q)
[PROOF STEP]
using cong_def
[PROOF STATE]
proof (prove)
using this:
[int x1 * (int a mod int q - int a' mod int q) = int b' - int b] (mod int q)
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. [int x1 * (int a mod int q - int a' mod int q) mod int q = int b' - int b] (mod int q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[int x1 * (int a mod int q - int a' mod int q) mod int q = int b' - int b] (mod int q)

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int x1 * nat ((int a mod q - int a' mod q) mod q) = int b'- int b] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int x1 * (int a mod int q - int a' mod int q) mod int q = int b' - int b] (mod int q)

goal (1 subgoal):
 1. [int x1 * int (nat ((int a mod int q - int a' mod int q) mod int q)) = int b' - int b] (mod int q)
[PROOF STEP]
by (simp add: True cong_def mod_mult_right_eq)
[PROOF STATE]
proof (state)
this:
[int x1 * int (nat ((int a mod int q - int a' mod int q) mod int q)) = int b' - int b] (mod int q)

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int x1 * nat ((int a mod q - int a' mod q) mod q) * inverse (nat ((int a mod q - int a' mod q) mod q)) q
              = (int b'- int b) * inverse (nat ((int a mod q - int a' mod q) mod q)) q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int x1 * int (nat ((int a mod int q - int a' mod int q) mod int q)) = int b' - int b] (mod int q)

goal (1 subgoal):
 1. [int x1 * int (nat ((int a mod int q - int a' mod int q) mod int q)) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
using cong_scalar_right
[PROOF STATE]
proof (prove)
using this:
[int x1 * int (nat ((int a mod int q - int a' mod int q) mod int q)) = int b' - int b] (mod int q)
[?b = ?c] (mod ?a) \<Longrightarrow> [?b * ?d = ?c * ?d] (mod ?a)

goal (1 subgoal):
 1. [int x1 * int (nat ((int a mod int q - int a' mod int q) mod int q)) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[int x1 * int (nat ((int a mod int q - int a' mod int q) mod int q)) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int x1 * (nat ((int a mod q - int a' mod q) mod q) * inverse (nat ((int a mod q - int a' mod q) mod q)) q)
              = (int b'- int b) * inverse (nat ((int a mod q - int a' mod q) mod q)) q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int x1 * int (nat ((int a mod int q - int a' mod int q) mod int q)) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. [int x1 * (int (nat ((int a mod int q - int a' mod int q) mod int q)) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q) = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
by (simp add: more_arith_simps(11))
[PROOF STATE]
proof (state)
this:
[int x1 * (int (nat ((int a mod int q - int a' mod int q) mod int q)) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q) = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int x1 * 1 = (int b'- int b) * inverse (nat ((int a mod q - int a' mod q) mod q)) q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int x1 * (int (nat ((int a mod int q - int a' mod int q) mod int q)) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q) = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. [int x1 * 1 = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
using inverse gcd
[PROOF STATE]
proof (prove)
using this:
[int x1 * (int (nat ((int a mod int q - int a' mod int q) mod int q)) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q) = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)
gcd ?x ?q = 1 \<Longrightarrow> [int ?x * Number_Theory_Aux.inverse ?x ?q = 1] (mod int ?q)
gcd (nat ((int a mod int q - int a' mod int q) mod int q)) q = 1

goal (1 subgoal):
 1. [int x1 * 1 = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
by (meson cong_scalar_left cong_sym_eq cong_trans)
[PROOF STATE]
proof (state)
this:
[int x1 * 1 = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int x1 = (int b'- int b) * inverse (nat ((int a mod q - int a' mod q) mod q)) q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int x1 * 1 = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. [int x1 = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[int x1 = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "int x1 mod q = ((int b'- int b) * inverse (nat ((int a mod q - int a' mod q) mod q)) q) mod q"
[PROOF STATE]
proof (prove)
using this:
[int x1 = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. int x1 mod int q = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q
[PROOF STEP]
using cong_def
[PROOF STATE]
proof (prove)
using this:
[int x1 = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q] (mod int q)
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. int x1 mod int q = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
int x1 mod int q = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q

goal (2 subgoals):
 1. a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
 2. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
int x1 mod int q = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q

goal (1 subgoal):
 1. x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
using x1 True
[PROOF STATE]
proof (prove)
using this:
int x1 mod int q = (int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q
x1 < q
a' mod q < a mod q

goal (1 subgoal):
 1. x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> a' mod q < a mod q

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence aa': "a mod q < a' mod q"
[PROOF STATE]
proof (prove)
using this:
\<not> a' mod q < a mod q

goal (1 subgoal):
 1. a mod q < a' mod q
[PROOF STEP]
using a_a' cong_refl nat_neq_iff
[PROOF STATE]
proof (prove)
using this:
\<not> a' mod q < a mod q
[a \<noteq> a'] (mod q)
[?b = ?b] (mod ?a)
(?m \<noteq> ?n) = (?m < ?n \<or> ?n < ?m)

goal (1 subgoal):
 1. a mod q < a' mod q
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
a mod q < a' mod q

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence gcd: "gcd (nat ((int a' mod q - int a mod q) mod q)) q = 1"
[PROOF STATE]
proof (prove)
using this:
a mod q < a' mod q

goal (1 subgoal):
 1. gcd (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a mod q < a' mod q \<Longrightarrow> gcd (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1
[PROOF STEP]
have "((int a' mod q - int a mod q) mod q) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (int a' mod int q - int a mod int q) mod int q \<noteq> 0
[PROOF STEP]
by (metis aa' comm_monoid_add_class.add_0 diff_add_cancel mod_add_left_eq mod_diff_eq nat_mod_as_int order_less_irrefl)
[PROOF STATE]
proof (state)
this:
(int a' mod int q - int a mod int q) mod int q \<noteq> 0

goal (1 subgoal):
 1. a mod q < a' mod q \<Longrightarrow> gcd (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(int a' mod int q - int a mod int q) mod int q \<noteq> 0

goal (1 subgoal):
 1. a mod q < a' mod q \<Longrightarrow> gcd (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1
[PROOF STEP]
have "((int a' mod q - int a mod q) mod q) < q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (int a' mod int q - int a mod int q) mod int q < int q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(int a' mod int q - int a mod int q) mod int q < int q

goal (1 subgoal):
 1. a mod q < a' mod q \<Longrightarrow> gcd (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(int a' mod int q - int a mod int q) mod int q \<noteq> 0
(int a' mod int q - int a mod int q) mod int q < int q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(int a' mod int q - int a mod int q) mod int q \<noteq> 0
(int a' mod int q - int a mod int q) mod int q < int q

goal (1 subgoal):
 1. gcd (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1
[PROOF STEP]
using prime_field[of q "nat ((int a' mod int q - int a mod int q) mod int q)"] prime_q
[PROOF STATE]
proof (prove)
using this:
(int a' mod int q - int a mod int q) mod int q \<noteq> 0
(int a' mod int q - int a mod int q) mod int q < int q
\<lbrakk>prime q; nat ((int a' mod int q - int a mod int q) mod int q) < q; nat ((int a' mod int q - int a mod int q) mod int q) \<noteq> 0\<rbrakk> \<Longrightarrow> coprime (nat ((int a' mod int q - int a mod int q) mod int q)) q
prime q

goal (1 subgoal):
 1. gcd (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1
[PROOF STEP]
by (smt Euclidean_Division.pos_mod_sign coprime_imp_gcd_eq_1 int_nat_eq nat_less_iff of_nat_0_less_iff q_gt_0)
[PROOF STATE]
proof (state)
this:
gcd (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gcd (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
have "[int b - int b' = int a' * int x1 - int a * int x1] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [int b - int b' = int a' * int x1 - int a * int x1] (mod int q)
[PROOF STEP]
by (smt cong_diff_iff_cong_0 cong_y1 cong_diff cong_diff)
[PROOF STATE]
proof (state)
this:
[int b - int b' = int a' * int x1 - int a * int x1] (mod int q)

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int b - int b' = int x1 * (int a' - int a)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int b - int b' = int a' * int x1 - int a * int x1] (mod int q)

goal (1 subgoal):
 1. [int b - int b' = int x1 * (int a' - int a)] (mod int q)
[PROOF STEP]
using int_distrib mult.commute
[PROOF STATE]
proof (prove)
using this:
[int b - int b' = int a' * int x1 - int a * int x1] (mod int q)
(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w
?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0
(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w
?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. [int b - int b' = int x1 * (int a' - int a)] (mod int q)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
[int b - int b' = int x1 * (int a' - int a)] (mod int q)

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int b - int b' = int x1 * (int a' mod q - int a mod q)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int b - int b' = int x1 * (int a' - int a)] (mod int q)

goal (1 subgoal):
 1. [int b - int b' = int x1 * (int a' mod int q - int a mod int q)] (mod int q)
[PROOF STEP]
by (metis (no_types, lifting) cong_def mod_diff_eq mod_mult_right_eq)
[PROOF STATE]
proof (state)
this:
[int b - int b' = int x1 * (int a' mod int q - int a mod int q)] (mod int q)

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int b - int b' = int x1 * (int a' mod q - int a mod q) mod q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int b - int b' = int x1 * (int a' mod int q - int a mod int q)] (mod int q)

goal (1 subgoal):
 1. [int b - int b' = int x1 * (int a' mod int q - int a mod int q) mod int q] (mod int q)
[PROOF STEP]
using cong_def
[PROOF STATE]
proof (prove)
using this:
[int b - int b' = int x1 * (int a' mod int q - int a mod int q)] (mod int q)
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. [int b - int b' = int x1 * (int a' mod int q - int a mod int q) mod int q] (mod int q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[int b - int b' = int x1 * (int a' mod int q - int a mod int q) mod int q] (mod int q)

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[(int b - int b') * inverse (nat ((int a' mod q - int a mod q) mod q)) q
               = int x1 * (int a' mod q - int a mod q) mod q *  inverse (nat ((int a' mod q - int a mod q) mod q)) q ] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int b - int b' = int x1 * (int a' mod int q - int a mod int q) mod int q] (mod int q)

goal (1 subgoal):
 1. [(int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = int x1 * (int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
using cong_scalar_right
[PROOF STATE]
proof (prove)
using this:
[int b - int b' = int x1 * (int a' mod int q - int a mod int q) mod int q] (mod int q)
[?b = ?c] (mod ?a) \<Longrightarrow> [?b * ?d = ?c * ?d] (mod ?a)

goal (1 subgoal):
 1. [(int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = int x1 * (int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = int x1 * (int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[(int b - int b') * inverse (nat ((int a' mod q - int a mod q) mod q)) q
               = int x1 * ((int a' mod q - int a mod q) mod q *  inverse (nat ((int a' mod q - int a mod q) mod q)) q)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = int x1 * (int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. [(int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = int x1 * ((int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q)] (mod int q)
[PROOF STEP]
by (metis (mono_tags, lifting) cong_def mod_mult_left_eq mod_mult_right_eq more_arith_simps(11))
[PROOF STATE]
proof (state)
this:
[(int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = int x1 * ((int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q)] (mod int q)

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence *: "[int x1 * ((int a' mod q - int a mod q) mod q * inverse (nat ((int a' mod q - int a mod q) mod q)) q)
              = (int b - int b') * inverse (nat ((int a' mod q - int a mod q) mod q)) q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[(int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = int x1 * ((int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q)] (mod int q)

goal (1 subgoal):
 1. [int x1 * ((int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q) = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
using cong_sym_eq
[PROOF STATE]
proof (prove)
using this:
[(int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = int x1 * ((int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q)] (mod int q)
[?b = ?c] (mod ?a) = [?c = ?b] (mod ?a)

goal (1 subgoal):
 1. [int x1 * ((int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q) = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[int x1 * ((int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q) = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int x1 * 1 = (int b - int b') * inverse (nat ((int a' mod q - int a mod q) mod q)) q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int x1 * ((int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q) = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. [int x1 * 1 = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [int x1 * ((int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q) = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q) \<Longrightarrow> [int x1 * 1 = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
have "[(int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1] (mod int q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1] (mod int q)
[PROOF STEP]
by (metis (no_types) Euclidean_Division.pos_mod_sign inverse gcd int_nat_eq of_nat_0_less_iff q_gt_0)
[PROOF STATE]
proof (state)
this:
[(int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1] (mod int q)

goal (1 subgoal):
 1. [int x1 * ((int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q) = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q) \<Longrightarrow> [int x1 * 1 = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1] (mod int q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[(int a' mod int q - int a mod int q) mod int q * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q = 1] (mod int q)

goal (1 subgoal):
 1. [int x1 * 1 = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
by (meson * cong_scalar_left cong_sym_eq cong_trans)
[PROOF STATE]
proof (state)
this:
[int x1 * 1 = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[int x1 * 1 = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "[int x1 = (int b - int b') * inverse (nat ((int a' mod q - int a mod q) mod q)) q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[int x1 * 1 = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. [int x1 = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[int x1 = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
hence "int x1 mod q = (int b - int b') * (inverse (nat ((int a' mod q - int a mod q) mod q)) q) mod q"
[PROOF STATE]
proof (prove)
using this:
[int x1 = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)

goal (1 subgoal):
 1. int x1 mod int q = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q
[PROOF STEP]
using cong_def
[PROOF STATE]
proof (prove)
using this:
[int x1 = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q] (mod int q)
[?b = ?c] (mod ?a) = (?b mod ?a = ?c mod ?a)

goal (1 subgoal):
 1. int x1 mod int q = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int x1 mod int q = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q

goal (1 subgoal):
 1. \<not> a' mod q < a mod q \<Longrightarrow> x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
int x1 mod int q = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q

goal (1 subgoal):
 1. x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
using x1 aa'
[PROOF STATE]
proof (prove)
using this:
int x1 mod int q = (int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q
x1 < q
a mod q < a' mod q

goal (1 subgoal):
 1. x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x1 = (if a' mod q < a mod q then nat ((int b' - int b) * Number_Theory_Aux.inverse (nat ((int a mod int q - int a' mod int q) mod int q)) q mod int q) else nat ((int b - int b') * Number_Theory_Aux.inverse (nat ((int a' mod int q - int a mod int q) mod int q)) q mod int q))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma samp_uni_spmf_mod_q:
  shows "spmf (sample_uniform q) (x mod q) = 1/q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (sample_uniform q) (x mod q) = 1 / real q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spmf (sample_uniform q) (x mod q) = 1 / real q
[PROOF STEP]
have "indicator {..< q} (x mod q) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indicator {..<q} (x mod q) = (1::'a)
[PROOF STEP]
using q_gt_0
[PROOF STATE]
proof (prove)
using this:
0 < q

goal (1 subgoal):
 1. indicator {..<q} (x mod q) = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
indicator {..<q} (x mod q) = (1::?'a2)

goal (1 subgoal):
 1. spmf (sample_uniform q) (x mod q) = 1 / real q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
indicator {..<q} (x mod q) = (1::?'a2)

goal (1 subgoal):
 1. spmf (sample_uniform q) (x mod q) = 1 / real q
[PROOF STEP]
have "real (card {..< q}) = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (card {..<q}) = real q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (card {..<q}) = real q

goal (1 subgoal):
 1. spmf (sample_uniform q) (x mod q) = 1 / real q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
indicator {..<q} (x mod q) = (1::?'a2)
real (card {..<q}) = real q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
indicator {..<q} (x mod q) = (1::?'a2)
real (card {..<q}) = real q

goal (1 subgoal):
 1. spmf (sample_uniform q) (x mod q) = 1 / real q
[PROOF STEP]
by(auto simp add: spmf_of_set sample_uniform_def)
[PROOF STATE]
proof (state)
this:
spmf (sample_uniform q) (x mod q) = 1 / real q

goal:
No subgoals!
[PROOF STEP]
qed