[STATEMENT]
lemma bind_game_le_inv_q:
  shows "spmf (rivest_commit.bind_game \<A>) True \<le> 1 / q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
let ?eq = "\<lambda>a a' b b'. (=)
   (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 (state)
goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
have "spmf (rivest_commit.bind_game \<A>) True = spmf (do {
    (ck,(x1,y1)) \<leftarrow> key_gen;
    (c, m, (a,b), m', (a',b')) \<leftarrow> \<A> ck;
    _ :: unit \<leftarrow> assert_spmf(m \<noteq> m' \<and> valid_msg m \<and> valid_msg m');
    let b = verify (x1,y1) m c (a,b);
    let b' = verify (x1,y1) m' c (a',b');
    _ :: unit \<leftarrow> assert_spmf (b \<and> b');
    return_spmf True}) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True = spmf (key_gen \<bind> (\<lambda>(ck, x1, y1). \<A> ck \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. let b = verify (x1, y1) m c (a, b); b' = verify (x1, y1) m' c (a', b') in assert_spmf (b \<and> b') \<bind> (\<lambda>_. return_spmf True))))) True
[PROOF STEP]
by(simp add: abstract_commitment.bind_game_alt_def split_def spmf_try_spmf del: verify.simps)
[PROOF STATE]
proof (state)
this:
spmf (rivest_commit.bind_game \<A>) True = spmf (key_gen \<bind> (\<lambda>(ck, x1, y1). \<A> ck \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. let b = verify (x1, y1) m c (a, b); b' = verify (x1, y1) m' c (a', b') in assert_spmf (b \<and> b') \<bind> (\<lambda>_. return_spmf True))))) True

goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
spmf (rivest_commit.bind_game \<A>) True = spmf (key_gen \<bind> (\<lambda>(ck, x1, y1). \<A> ck \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. let b = verify (x1, y1) m c (a, b); b' = verify (x1, y1) m' c (a', b') in assert_spmf (b \<and> b') \<bind> (\<lambda>_. return_spmf True))))) True

goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
have "... = spmf (do {
    a' :: nat \<leftarrow> sample_uniform q;
    b' :: nat \<leftarrow> sample_uniform q;
    x1 :: nat \<leftarrow> sample_uniform q;
    let y1 = (a' * x1 + b') mod q;
    (c, m, (a,b), m', (a',b')) \<leftarrow> \<A> (a',b');
    _ :: unit \<leftarrow> assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m');
    _ :: unit \<leftarrow> assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q);
    return_spmf True}) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (key_gen \<bind> (\<lambda>(ck, x1, y1). \<A> ck \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. let b = verify (x1, y1) m c (a, b); b' = verify (x1, y1) m' c (a', b') in assert_spmf (b \<and> b') \<bind> (\<lambda>_. return_spmf True))))) True = spmf (sample_uniform q \<bind> (\<lambda>a'. sample_uniform q \<bind> (\<lambda>b'. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a' * x1 + b') mod q in \<A> (a', b') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf True))))))) True
[PROOF STEP]
by(simp add: key_gen_def Let_def)
[PROOF STATE]
proof (state)
this:
spmf (key_gen \<bind> (\<lambda>(ck, x1, y1). \<A> ck \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. let b = verify (x1, y1) m c (a, b); b' = verify (x1, y1) m' c (a', b') in assert_spmf (b \<and> b') \<bind> (\<lambda>_. return_spmf True))))) True = spmf (sample_uniform q \<bind> (\<lambda>a'. sample_uniform q \<bind> (\<lambda>b'. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a' * x1 + b') mod q in \<A> (a', b') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf True))))))) True

goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
spmf (key_gen \<bind> (\<lambda>(ck, x1, y1). \<A> ck \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. let b = verify (x1, y1) m c (a, b); b' = verify (x1, y1) m' c (a', b') in assert_spmf (b \<and> b') \<bind> (\<lambda>_. return_spmf True))))) True = spmf (sample_uniform q \<bind> (\<lambda>a'. sample_uniform q \<bind> (\<lambda>b'. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a' * x1 + b') mod q in \<A> (a', b') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf True))))))) True

goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
have "... = spmf (do {
    a'' :: nat \<leftarrow> sample_uniform q;
    b'' :: nat \<leftarrow> sample_uniform q;
    x1 :: nat \<leftarrow> sample_uniform q;
    let y1 = (a'' * x1 + b'') mod q;
    (c, m, (a,b), m', (a',b')) \<leftarrow> \<A> (a'',b'');
    _ :: unit \<leftarrow> assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m');
    _ :: unit \<leftarrow> assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q);
    return_spmf (?eq a a' b b' x1)}) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>a'. sample_uniform q \<bind> (\<lambda>b'. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a' * x1 + b') mod q in \<A> (a', b') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf True))))))) True = spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a'' * x1 + b'') mod q in \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf ((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)) = x1)))))))) True
[PROOF STEP]
unfolding split_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>a'. sample_uniform q \<bind> (\<lambda>b'. sample_uniform q \<bind> (\<lambda>x1. \<A> (a', b') \<bind> (\<lambda>p. assert_spmf (fst (snd p) \<noteq> fst (snd (snd (snd p))) \<and> valid_msg (fst (snd p)) \<and> valid_msg (fst (snd (snd (snd p))))) \<bind> (\<lambda>_. assert_spmf (fst p = (fst (snd p) + fst (fst (snd (snd p)))) mod q \<and> (a' * x1 + b') mod q = (fst (fst (snd (snd p))) * x1 + snd (fst (snd (snd p)))) mod q \<and> fst p = (fst (snd (snd (snd p))) + fst (snd (snd (snd (snd p))))) mod q \<and> (a' * x1 + b') mod q = (fst (snd (snd (snd (snd p)))) * x1 + snd (snd (snd (snd (snd p))))) mod q) \<bind> (\<lambda>_. return_spmf True))))))) True = spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. sample_uniform q \<bind> (\<lambda>x1. \<A> (a'', b'') \<bind> (\<lambda>p. assert_spmf (fst (snd p) \<noteq> fst (snd (snd (snd p))) \<and> valid_msg (fst (snd p)) \<and> valid_msg (fst (snd (snd (snd p))))) \<bind> (\<lambda>_. assert_spmf (fst p = (fst (snd p) + fst (fst (snd (snd p)))) mod q \<and> (a'' * x1 + b'') mod q = (fst (fst (snd (snd p))) * x1 + snd (fst (snd (snd p)))) mod q \<and> fst p = (fst (snd (snd (snd p))) + fst (snd (snd (snd (snd p))))) mod q \<and> (a'' * x1 + b'') mod q = (fst (snd (snd (snd (snd p)))) * x1 + snd (snd (snd (snd (snd p))))) mod q) \<bind> (\<lambda>_. return_spmf ((if fst (snd (snd (snd (snd p)))) mod q < fst (fst (snd (snd p))) mod q then nat ((int (snd (snd (snd (snd (snd p))))) - int (snd (fst (snd (snd p))))) * Number_Theory_Aux.inverse (nat ((int (fst (fst (snd (snd p)))) mod int q - int (fst (snd (snd (snd (snd p))))) mod int q) mod int q)) q mod int q) else nat ((int (snd (fst (snd (snd p)))) - int (snd (snd (snd (snd (snd p)))))) * Number_Theory_Aux.inverse (nat ((int (fst (snd (snd (snd (snd p))))) mod int q - int (fst (fst (snd (snd p)))) mod int q) mod int q)) q mod int q)) = x1)))))))) True
[PROOF STEP]
by(rule arg_cong2[where f=spmf, OF _ refl] bind_spmf_cong[OF refl])+
      (auto simp add: eq_commute samp_uni_break' Let_def split_def valid_msg_def cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
spmf (sample_uniform q \<bind> (\<lambda>a'. sample_uniform q \<bind> (\<lambda>b'. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a' * x1 + b') mod q in \<A> (a', b') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf True))))))) True = spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a'' * x1 + b'') mod q in \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf ((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)) = x1)))))))) True

goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
spmf (sample_uniform q \<bind> (\<lambda>a'. sample_uniform q \<bind> (\<lambda>b'. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a' * x1 + b') mod q in \<A> (a', b') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf True))))))) True = spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a'' * x1 + b'') mod q in \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf ((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)) = x1)))))))) True

goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
have "... \<le> spmf (do {
    a'' :: nat \<leftarrow> sample_uniform q;
    b'' :: nat \<leftarrow> sample_uniform q;
    (c, m, (a,(b::nat)), m', (a',b')) \<leftarrow> \<A> (a'',b'');
    map_spmf (?eq a a' b b') (sample_uniform q)}) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a'' * x1 + b'') mod q in \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf ((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)) = x1)))))))) True \<le> spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). map_spmf ((=) (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))) (sample_uniform q))))) True
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a'' * x1 + b'') mod q in \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf ((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)) = x1)))))))) True \<le> spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). map_spmf ((=) (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))) (sample_uniform q))))) True
[PROOF STEP]
unfolding split_def Let_def assert_spmf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. sample_uniform q \<bind> (\<lambda>x1. \<A> (a'', b'') \<bind> (\<lambda>p. (if fst (snd p) \<noteq> fst (snd (snd (snd p))) \<and> valid_msg (fst (snd p)) \<and> valid_msg (fst (snd (snd (snd p)))) then return_spmf () else return_pmf None) \<bind> (\<lambda>_. (if fst p = (fst (snd p) + fst (fst (snd (snd p)))) mod q \<and> (a'' * x1 + b'') mod q = (fst (fst (snd (snd p))) * x1 + snd (fst (snd (snd p)))) mod q \<and> fst p = (fst (snd (snd (snd p))) + fst (snd (snd (snd (snd p))))) mod q \<and> (a'' * x1 + b'') mod q = (fst (snd (snd (snd (snd p)))) * x1 + snd (snd (snd (snd (snd p))))) mod q then return_spmf () else return_pmf None) \<bind> (\<lambda>_. return_spmf ((if fst (snd (snd (snd (snd p)))) mod q < fst (fst (snd (snd p))) mod q then nat ((int (snd (snd (snd (snd (snd p))))) - int (snd (fst (snd (snd p))))) * Number_Theory_Aux.inverse (nat ((int (fst (fst (snd (snd p)))) mod int q - int (fst (snd (snd (snd (snd p))))) mod int q) mod int q)) q mod int q) else nat ((int (snd (fst (snd (snd p)))) - int (snd (snd (snd (snd (snd p)))))) * Number_Theory_Aux.inverse (nat ((int (fst (snd (snd (snd (snd p))))) mod int q - int (fst (fst (snd (snd p)))) mod int q) mod int q)) q mod int q)) = x1)))))))) True \<le> spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. \<A> (a'', b'') \<bind> (\<lambda>p. map_spmf ((=) (if fst (snd (snd (snd (snd p)))) mod q < fst (fst (snd (snd p))) mod q then nat ((int (snd (snd (snd (snd (snd p))))) - int (snd (fst (snd (snd p))))) * Number_Theory_Aux.inverse (nat ((int (fst (fst (snd (snd p)))) mod int q - int (fst (snd (snd (snd (snd p))))) mod int q) mod int q)) q mod int q) else nat ((int (snd (fst (snd (snd p)))) - int (snd (snd (snd (snd (snd p)))))) * Number_Theory_Aux.inverse (nat ((int (fst (snd (snd (snd (snd p))))) mod int q - int (fst (fst (snd (snd p)))) mod int q) mod int q)) q mod int q))) (sample_uniform q))))) True
[PROOF STEP]
apply(simp add: map_spmf_conv_bind_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. sample_uniform q \<bind> (\<lambda>x1. \<A> (a'', b'') \<bind> (\<lambda>p. (if fst (snd p) \<noteq> fst (snd (snd (snd p))) \<and> valid_msg (fst (snd p)) \<and> valid_msg (fst (snd (snd (snd p)))) then return_spmf () else return_pmf None) \<bind> (\<lambda>_. (if fst p = (fst (snd p) + fst (fst (snd (snd p)))) mod q \<and> (a'' * x1 + b'') mod q = (fst (fst (snd (snd p))) * x1 + snd (fst (snd (snd p)))) mod q \<and> fst p = (fst (snd (snd (snd p))) + fst (snd (snd (snd (snd p))))) mod q \<and> (a'' * x1 + b'') mod q = (fst (snd (snd (snd (snd p)))) * x1 + snd (snd (snd (snd (snd p))))) mod q then return_spmf () else return_pmf None) \<bind> (\<lambda>_. return_spmf ((if fst (snd (snd (snd (snd p)))) mod q < fst (fst (snd (snd p))) mod q then nat ((int (snd (snd (snd (snd (snd p))))) - int (snd (fst (snd (snd p))))) * Number_Theory_Aux.inverse (nat ((int (fst (fst (snd (snd p)))) mod int q - int (fst (snd (snd (snd (snd p))))) mod int q) mod int q)) q mod int q) else nat ((int (snd (fst (snd (snd p)))) - int (snd (snd (snd (snd (snd p)))))) * Number_Theory_Aux.inverse (nat ((int (fst (snd (snd (snd (snd p))))) mod int q - int (fst (fst (snd (snd p)))) mod int q) mod int q)) q mod int q)) = x1)))))))) True \<le> spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. sample_uniform q \<bind> (\<lambda>x. \<A> (a'', b'') \<bind> (\<lambda>p. return_spmf ((if fst (snd (snd (snd (snd p)))) mod q < fst (fst (snd (snd p))) mod q then nat ((int (snd (snd (snd (snd (snd p))))) - int (snd (fst (snd (snd p))))) * Number_Theory_Aux.inverse (nat ((int (fst (fst (snd (snd p)))) mod int q - int (fst (snd (snd (snd (snd p))))) mod int q) mod int q)) q mod int q) else nat ((int (snd (fst (snd (snd p)))) - int (snd (snd (snd (snd (snd p)))))) * Number_Theory_Aux.inverse (nat ((int (fst (snd (snd (snd (snd p))))) mod int q - int (fst (fst (snd (snd p)))) mod int q) mod int q)) q mod int q)) = x)))))) True
[PROOF STEP]
apply(rule ord_spmf_eq_leD ord_spmf_bind_reflI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. \<lbrakk>x \<in> set_spmf (sample_uniform q); xa \<in> set_spmf (sample_uniform q); xb \<in> set_spmf (sample_uniform q); xc \<in> set_spmf (\<A> (x, xa))\<rbrakk> \<Longrightarrow> ord_spmf (=) ((if fst (snd xc) \<noteq> fst (snd (snd (snd xc))) \<and> valid_msg (fst (snd xc)) \<and> valid_msg (fst (snd (snd (snd xc)))) then return_spmf () else return_pmf None) \<bind> (\<lambda>_. (if fst xc = (fst (snd xc) + fst (fst (snd (snd xc)))) mod q \<and> (x * xb + xa) mod q = (fst (fst (snd (snd xc))) * xb + snd (fst (snd (snd xc)))) mod q \<and> fst xc = (fst (snd (snd (snd xc))) + fst (snd (snd (snd (snd xc))))) mod q \<and> (x * xb + xa) mod q = (fst (snd (snd (snd (snd xc)))) * xb + snd (snd (snd (snd (snd xc))))) mod q then return_spmf () else return_pmf None) \<bind> (\<lambda>_. return_spmf ((if fst (snd (snd (snd (snd xc)))) mod q < fst (fst (snd (snd xc))) mod q then nat ((int (snd (snd (snd (snd (snd xc))))) - int (snd (fst (snd (snd xc))))) * Number_Theory_Aux.inverse (nat ((int (fst (fst (snd (snd xc)))) mod int q - int (fst (snd (snd (snd (snd xc))))) mod int q) mod int q)) q mod int q) else nat ((int (snd (fst (snd (snd xc)))) - int (snd (snd (snd (snd (snd xc)))))) * Number_Theory_Aux.inverse (nat ((int (fst (snd (snd (snd (snd xc))))) mod int q - int (fst (fst (snd (snd xc)))) mod int q) mod int q)) q mod int q)) = xb)))) (return_spmf ((if fst (snd (snd (snd (snd xc)))) mod q < fst (fst (snd (snd xc))) mod q then nat ((int (snd (snd (snd (snd (snd xc))))) - int (snd (fst (snd (snd xc))))) * Number_Theory_Aux.inverse (nat ((int (fst (fst (snd (snd xc)))) mod int q - int (fst (snd (snd (snd (snd xc))))) mod int q) mod int q)) q mod int q) else nat ((int (snd (fst (snd (snd xc)))) - int (snd (snd (snd (snd (snd xc)))))) * Number_Theory_Aux.inverse (nat ((int (fst (snd (snd (snd (snd xc))))) mod int q - int (fst (fst (snd (snd xc)))) mod int q) mod int q)) q mod int q)) = xb))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a'' * x1 + b'') mod q in \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf ((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)) = x1)))))))) True \<le> spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). map_spmf ((=) (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))) (sample_uniform q))))) True

goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. sample_uniform q \<bind> (\<lambda>x1. let y1 = (a'' * x1 + b'') mod q in \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). assert_spmf (m \<noteq> m' \<and> valid_msg m \<and> valid_msg m') \<bind> (\<lambda>_. assert_spmf (c = (m + a) mod q \<and> y1 = (a * x1 + b) mod q \<and> c = (m' + a') mod q \<and> y1 = (a' * x1 + b') mod q) \<bind> (\<lambda>_. return_spmf ((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)) = x1)))))))) True \<le> spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). map_spmf ((=) (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))) (sample_uniform q))))) True

goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
have "... \<le> 1/q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). map_spmf ((=) (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))) (sample_uniform q))))) True \<le> 1 / real q
[PROOF STEP]
proof((rule spmf_bind_leI)+, clarify)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>y ya a aa ab b ac ad ba. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q); (a, aa, (ab, b), ac, ad, ba) \<in> set_spmf (\<A> (y, ya))\<rbrakk> \<Longrightarrow> spmf (map_spmf ((=) (if ad mod q < ab mod q then nat ((int ba - int b) * Number_Theory_Aux.inverse (nat ((int ab mod int q - int ad mod int q) mod int q)) q mod int q) else nat ((int b - int ba) * Number_Theory_Aux.inverse (nat ((int ad mod int q - int ab mod int q) mod int q)) q mod int q))) (sample_uniform q)) True \<le> 1 / real q
 2. \<And>y ya. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q)\<rbrakk> \<Longrightarrow> 0 \<le> 1 / real q
 3. \<And>y. y \<in> set_spmf (sample_uniform q) \<Longrightarrow> 0 \<le> 1 / real q
 4. 0 \<le> 1 / real q
[PROOF STEP]
fix a a' b b'
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>y ya a aa ab b ac ad ba. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q); (a, aa, (ab, b), ac, ad, ba) \<in> set_spmf (\<A> (y, ya))\<rbrakk> \<Longrightarrow> spmf (map_spmf ((=) (if ad mod q < ab mod q then nat ((int ba - int b) * Number_Theory_Aux.inverse (nat ((int ab mod int q - int ad mod int q) mod int q)) q mod int q) else nat ((int b - int ba) * Number_Theory_Aux.inverse (nat ((int ad mod int q - int ab mod int q) mod int q)) q mod int q))) (sample_uniform q)) True \<le> 1 / real q
 2. \<And>y ya. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q)\<rbrakk> \<Longrightarrow> 0 \<le> 1 / real q
 3. \<And>y. y \<in> set_spmf (sample_uniform q) \<Longrightarrow> 0 \<le> 1 / real q
 4. 0 \<le> 1 / real q
[PROOF STEP]
define A where "A = Collect (?eq a a' b b')"
[PROOF STATE]
proof (state)
this:
A = Collect ((=) (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 (4 subgoals):
 1. \<And>y ya a aa ab b ac ad ba. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q); (a, aa, (ab, b), ac, ad, ba) \<in> set_spmf (\<A> (y, ya))\<rbrakk> \<Longrightarrow> spmf (map_spmf ((=) (if ad mod q < ab mod q then nat ((int ba - int b) * Number_Theory_Aux.inverse (nat ((int ab mod int q - int ad mod int q) mod int q)) q mod int q) else nat ((int b - int ba) * Number_Theory_Aux.inverse (nat ((int ad mod int q - int ab mod int q) mod int q)) q mod int q))) (sample_uniform q)) True \<le> 1 / real q
 2. \<And>y ya. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q)\<rbrakk> \<Longrightarrow> 0 \<le> 1 / real q
 3. \<And>y. y \<in> set_spmf (sample_uniform q) \<Longrightarrow> 0 \<le> 1 / real q
 4. 0 \<le> 1 / real q
[PROOF STEP]
define x1 where "x1 = The (?eq a a' b b')"
[PROOF STATE]
proof (state)
this:
x1 = The ((=) (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 (4 subgoals):
 1. \<And>y ya a aa ab b ac ad ba. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q); (a, aa, (ab, b), ac, ad, ba) \<in> set_spmf (\<A> (y, ya))\<rbrakk> \<Longrightarrow> spmf (map_spmf ((=) (if ad mod q < ab mod q then nat ((int ba - int b) * Number_Theory_Aux.inverse (nat ((int ab mod int q - int ad mod int q) mod int q)) q mod int q) else nat ((int b - int ba) * Number_Theory_Aux.inverse (nat ((int ad mod int q - int ab mod int q) mod int q)) q mod int q))) (sample_uniform q)) True \<le> 1 / real q
 2. \<And>y ya. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q)\<rbrakk> \<Longrightarrow> 0 \<le> 1 / real q
 3. \<And>y. y \<in> set_spmf (sample_uniform q) \<Longrightarrow> 0 \<le> 1 / real q
 4. 0 \<le> 1 / real q
[PROOF STEP]
note q_gt_0[simp del]
[PROOF STATE]
proof (state)
this:
0 < q

goal (4 subgoals):
 1. \<And>y ya a aa ab b ac ad ba. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q); (a, aa, (ab, b), ac, ad, ba) \<in> set_spmf (\<A> (y, ya))\<rbrakk> \<Longrightarrow> spmf (map_spmf ((=) (if ad mod q < ab mod q then nat ((int ba - int b) * Number_Theory_Aux.inverse (nat ((int ab mod int q - int ad mod int q) mod int q)) q mod int q) else nat ((int b - int ba) * Number_Theory_Aux.inverse (nat ((int ad mod int q - int ab mod int q) mod int q)) q mod int q))) (sample_uniform q)) True \<le> 1 / real q
 2. \<And>y ya. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q)\<rbrakk> \<Longrightarrow> 0 \<le> 1 / real q
 3. \<And>y. y \<in> set_spmf (sample_uniform q) \<Longrightarrow> 0 \<le> 1 / real q
 4. 0 \<le> 1 / real q
[PROOF STEP]
have "A \<subseteq> {x1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> {x1}
[PROOF STEP]
by(auto simp add: A_def x1_def)
[PROOF STATE]
proof (state)
this:
A \<subseteq> {x1}

goal (4 subgoals):
 1. \<And>y ya a aa ab b ac ad ba. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q); (a, aa, (ab, b), ac, ad, ba) \<in> set_spmf (\<A> (y, ya))\<rbrakk> \<Longrightarrow> spmf (map_spmf ((=) (if ad mod q < ab mod q then nat ((int ba - int b) * Number_Theory_Aux.inverse (nat ((int ab mod int q - int ad mod int q) mod int q)) q mod int q) else nat ((int b - int ba) * Number_Theory_Aux.inverse (nat ((int ad mod int q - int ab mod int q) mod int q)) q mod int q))) (sample_uniform q)) True \<le> 1 / real q
 2. \<And>y ya. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q)\<rbrakk> \<Longrightarrow> 0 \<le> 1 / real q
 3. \<And>y. y \<in> set_spmf (sample_uniform q) \<Longrightarrow> 0 \<le> 1 / real q
 4. 0 \<le> 1 / real q
[PROOF STEP]
hence "card (A \<inter> {..<q}) \<le> card {x1}"
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> {x1}

goal (1 subgoal):
 1. card (A \<inter> {..<q}) \<le> card {x1}
[PROOF STEP]
by(intro card_mono) auto
[PROOF STATE]
proof (state)
this:
card (A \<inter> {..<q}) \<le> card {x1}

goal (4 subgoals):
 1. \<And>y ya a aa ab b ac ad ba. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q); (a, aa, (ab, b), ac, ad, ba) \<in> set_spmf (\<A> (y, ya))\<rbrakk> \<Longrightarrow> spmf (map_spmf ((=) (if ad mod q < ab mod q then nat ((int ba - int b) * Number_Theory_Aux.inverse (nat ((int ab mod int q - int ad mod int q) mod int q)) q mod int q) else nat ((int b - int ba) * Number_Theory_Aux.inverse (nat ((int ad mod int q - int ab mod int q) mod int q)) q mod int q))) (sample_uniform q)) True \<le> 1 / real q
 2. \<And>y ya. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q)\<rbrakk> \<Longrightarrow> 0 \<le> 1 / real q
 3. \<And>y. y \<in> set_spmf (sample_uniform q) \<Longrightarrow> 0 \<le> 1 / real q
 4. 0 \<le> 1 / real q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (A \<inter> {..<q}) \<le> card {x1}

goal (4 subgoals):
 1. \<And>y ya a aa ab b ac ad ba. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q); (a, aa, (ab, b), ac, ad, ba) \<in> set_spmf (\<A> (y, ya))\<rbrakk> \<Longrightarrow> spmf (map_spmf ((=) (if ad mod q < ab mod q then nat ((int ba - int b) * Number_Theory_Aux.inverse (nat ((int ab mod int q - int ad mod int q) mod int q)) q mod int q) else nat ((int b - int ba) * Number_Theory_Aux.inverse (nat ((int ad mod int q - int ab mod int q) mod int q)) q mod int q))) (sample_uniform q)) True \<le> 1 / real q
 2. \<And>y ya. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q)\<rbrakk> \<Longrightarrow> 0 \<le> 1 / real q
 3. \<And>y. y \<in> set_spmf (sample_uniform q) \<Longrightarrow> 0 \<le> 1 / real q
 4. 0 \<le> 1 / real q
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {x1} = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {x1} = 1

goal (4 subgoals):
 1. \<And>y ya a aa ab b ac ad ba. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q); (a, aa, (ab, b), ac, ad, ba) \<in> set_spmf (\<A> (y, ya))\<rbrakk> \<Longrightarrow> spmf (map_spmf ((=) (if ad mod q < ab mod q then nat ((int ba - int b) * Number_Theory_Aux.inverse (nat ((int ab mod int q - int ad mod int q) mod int q)) q mod int q) else nat ((int b - int ba) * Number_Theory_Aux.inverse (nat ((int ad mod int q - int ab mod int q) mod int q)) q mod int q))) (sample_uniform q)) True \<le> 1 / real q
 2. \<And>y ya. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q)\<rbrakk> \<Longrightarrow> 0 \<le> 1 / real q
 3. \<And>y. y \<in> set_spmf (sample_uniform q) \<Longrightarrow> 0 \<le> 1 / real q
 4. 0 \<le> 1 / real q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (A \<inter> {..<q}) \<le> 1
[PROOF STEP]
have "spmf (map_spmf (\<lambda>x. x \<in> A) (sample_uniform q)) True \<le> 1 / q"
[PROOF STATE]
proof (prove)
using this:
card (A \<inter> {..<q}) \<le> 1

goal (1 subgoal):
 1. spmf (map_spmf (\<lambda>x. x \<in> A) (sample_uniform q)) True \<le> 1 / real q
[PROOF STEP]
using q_gt_0
[PROOF STATE]
proof (prove)
using this:
card (A \<inter> {..<q}) \<le> 1
0 < q

goal (1 subgoal):
 1. spmf (map_spmf (\<lambda>x. x \<in> A) (sample_uniform q)) True \<le> 1 / real q
[PROOF STEP]
unfolding sample_uniform_def
[PROOF STATE]
proof (prove)
using this:
card (A \<inter> {..<q}) \<le> 1
0 < q

goal (1 subgoal):
 1. spmf (map_spmf (\<lambda>x. x \<in> A) (spmf_of_set {..<q})) True \<le> 1 / real q
[PROOF STEP]
by(subst map_mem_spmf_of_set)(auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
spmf (map_spmf (\<lambda>x. x \<in> A) (sample_uniform q)) True \<le> 1 / real q

goal (4 subgoals):
 1. \<And>y ya a aa ab b ac ad ba. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q); (a, aa, (ab, b), ac, ad, ba) \<in> set_spmf (\<A> (y, ya))\<rbrakk> \<Longrightarrow> spmf (map_spmf ((=) (if ad mod q < ab mod q then nat ((int ba - int b) * Number_Theory_Aux.inverse (nat ((int ab mod int q - int ad mod int q) mod int q)) q mod int q) else nat ((int b - int ba) * Number_Theory_Aux.inverse (nat ((int ad mod int q - int ab mod int q) mod int q)) q mod int q))) (sample_uniform q)) True \<le> 1 / real q
 2. \<And>y ya. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q)\<rbrakk> \<Longrightarrow> 0 \<le> 1 / real q
 3. \<And>y. y \<in> set_spmf (sample_uniform q) \<Longrightarrow> 0 \<le> 1 / real q
 4. 0 \<le> 1 / real q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
spmf (map_spmf (\<lambda>x. x \<in> A) (sample_uniform q)) True \<le> 1 / real q
[PROOF STEP]
show "spmf (map_spmf (?eq a a' b b') (sample_uniform q)) True \<le> 1 / q"
[PROOF STATE]
proof (prove)
using this:
spmf (map_spmf (\<lambda>x. x \<in> A) (sample_uniform q)) True \<le> 1 / real q

goal (1 subgoal):
 1. spmf (map_spmf ((=) (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))) (sample_uniform q)) True \<le> 1 / real q
[PROOF STEP]
unfolding A_def mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
spmf (map_spmf ((=) (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))) (sample_uniform q)) True \<le> 1 / real q

goal (1 subgoal):
 1. spmf (map_spmf ((=) (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))) (sample_uniform q)) True \<le> 1 / real q
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
spmf (map_spmf ((=) (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))) (sample_uniform q)) True \<le> 1 / real q

goal (3 subgoals):
 1. \<And>y ya. \<lbrakk>y \<in> set_spmf (sample_uniform q); ya \<in> set_spmf (sample_uniform q)\<rbrakk> \<Longrightarrow> 0 \<le> 1 / real q
 2. \<And>y. y \<in> set_spmf (sample_uniform q) \<Longrightarrow> 0 \<le> 1 / real q
 3. 0 \<le> 1 / real q
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
spmf (sample_uniform q \<bind> (\<lambda>a''. sample_uniform q \<bind> (\<lambda>b''. \<A> (a'', b'') \<bind> (\<lambda>(c, m, (a, b), m', a', b'). map_spmf ((=) (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))) (sample_uniform q))))) True \<le> 1 / real q

goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q

goal (1 subgoal):
 1. spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
spmf (rivest_commit.bind_game \<A>) True \<le> 1 / real q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rivest_bind:
  shows "rivest_commit.bind_advantage \<A> \<le> 1 / q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rivest_commit.bind_advantage \<A> \<le> 1 / real q
[PROOF STEP]
using bind_game_le_inv_q rivest_commit.bind_advantage_def
[PROOF STATE]
proof (prove)
using this:
spmf (rivest_commit.bind_game ?\<A>) True \<le> 1 / real q
rivest_commit.bind_advantage ?\<A> \<equiv> spmf (rivest_commit.bind_game ?\<A>) True

goal (1 subgoal):
 1. rivest_commit.bind_advantage \<A> \<le> 1 / real q
[PROOF STEP]
by simp


[STATEMENT]
theorem rivest_correct:
  shows "rivest_commit.correct n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rivest_commit.correct n
[PROOF STEP]
using abstract_correct
[PROOF STATE]
proof (prove)
using this:
rivest_commit.correct ?\<eta>

goal (1 subgoal):
 1. rivest_commit.correct n
[PROOF STEP]
by simp


[STATEMENT]
theorem rivest_perfect_hiding_asym:
  assumes lossless_\<A>: "rivest_commit.lossless (\<A> n)"
  shows "rivest_commit.perfect_hiding_ind_cpa n (\<A> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rivest_commit.perfect_hiding_ind_cpa n (\<A> n)
[PROOF STEP]
by (simp add: lossless_\<A> rivest_perfect_hiding)


[STATEMENT]
theorem rivest_binding_asym:
  assumes "negligible (\<lambda>n. 1 / (q n))"
  shows "negligible (\<lambda>n. rivest_commit.bind_advantage n (\<A> n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. rivest_commit.bind_advantage n (\<A> n))
[PROOF STEP]
using negligible_le rivest_bind assms rivest_commit.bind_advantage_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Negligible.negligible ?g; \<And>\<eta>. \<bar>?f \<eta>\<bar> \<le> ?g \<eta>\<rbrakk> \<Longrightarrow> Negligible.negligible ?f
rivest_commit.bind_advantage ?\<eta> ?\<A> \<le> 1 / real (q ?\<eta>)
Negligible.negligible (\<lambda>n. 1 / real (q n))
rivest_commit.bind_advantage ?\<eta> ?\<A> \<equiv> spmf (rivest_commit.bind_game ?\<eta> ?\<A>) True

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


[STATEMENT]
lemma remove_abs :
    assumes f_OK: "\<And>xc. invar xc \<Longrightarrow> \<alpha> xc \<in> S0 \<Longrightarrow> fc xc = fa (\<alpha> xc)"
        and it_OK: "\<And>iti. set_iterator_genord iti S0 R \<Longrightarrow> P (iti c fa \<sigma>0)"
    shows "P (iti c fc \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c fc \<sigma>0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (iti c fc \<sigma>0)
[PROOF STEP]
from foldli_transform
[PROOF STATE]
proof (chain)
picking this:
\<exists>lc. (\<forall>xc\<in>set lc. invar xc) \<and> distinct (map \<alpha> lc) \<and> S0 = set (map \<alpha> lc) \<and> sorted_wrt R (map \<alpha> lc) \<and> iti = foldli lc
[PROOF STEP]
obtain lc where
          lc_invar: "\<And>xc. xc \<in> set lc \<Longrightarrow> invar xc"
      and \<alpha>_props: "distinct (map \<alpha> lc)" "S0 = set (map \<alpha> lc)"
                   "sorted_wrt R (map \<alpha> lc)"
      and iti_eq: "iti = foldli lc"
[PROOF STATE]
proof (prove)
using this:
\<exists>lc. (\<forall>xc\<in>set lc. invar xc) \<and> distinct (map \<alpha> lc) \<and> S0 = set (map \<alpha> lc) \<and> sorted_wrt R (map \<alpha> lc) \<and> iti = foldli lc

goal (1 subgoal):
 1. (\<And>lc. \<lbrakk>\<And>xc. xc \<in> set lc \<Longrightarrow> invar xc; distinct (map \<alpha> lc); S0 = set (map \<alpha> lc); sorted_wrt R (map \<alpha> lc); iti = foldli lc\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?xc \<in> set lc \<Longrightarrow> invar ?xc
distinct (map \<alpha> lc)
S0 = set (map \<alpha> lc)
sorted_wrt R (map \<alpha> lc)
iti = foldli lc

goal (1 subgoal):
 1. P (iti c fc \<sigma>0)
[PROOF STEP]
from \<alpha>_props
[PROOF STATE]
proof (chain)
picking this:
distinct (map \<alpha> lc)
S0 = set (map \<alpha> lc)
sorted_wrt R (map \<alpha> lc)
[PROOF STEP]
have "set_iterator_genord (foldli (map \<alpha> lc)) S0 R"
[PROOF STATE]
proof (prove)
using this:
distinct (map \<alpha> lc)
S0 = set (map \<alpha> lc)
sorted_wrt R (map \<alpha> lc)

goal (1 subgoal):
 1. set_iterator_genord (foldli (map \<alpha> lc)) S0 R
[PROOF STEP]
by (rule_tac set_iterator_genord_I [of "map \<alpha> lc"]) simp_all
[PROOF STATE]
proof (state)
this:
set_iterator_genord (foldli (map \<alpha> lc)) S0 R

goal (1 subgoal):
 1. P (iti c fc \<sigma>0)
[PROOF STEP]
with it_OK
[PROOF STATE]
proof (chain)
picking this:
set_iterator_genord ?iti S0 R \<Longrightarrow> P (?iti c fa \<sigma>0)
set_iterator_genord (foldli (map \<alpha> lc)) S0 R
[PROOF STEP]
have P_OK: "P (foldli (map \<alpha> lc) c fa \<sigma>0)"
[PROOF STATE]
proof (prove)
using this:
set_iterator_genord ?iti S0 R \<Longrightarrow> P (?iti c fa \<sigma>0)
set_iterator_genord (foldli (map \<alpha> lc)) S0 R

goal (1 subgoal):
 1. P (foldli (map \<alpha> lc) c fa \<sigma>0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P (foldli (map \<alpha> lc) c fa \<sigma>0)

goal (1 subgoal):
 1. P (iti c fc \<sigma>0)
[PROOF STEP]
from lc_invar f_OK[unfolded \<alpha>_props(2)]
[PROOF STATE]
proof (chain)
picking this:
?xc \<in> set lc \<Longrightarrow> invar ?xc
\<lbrakk>invar ?xc; \<alpha> ?xc \<in> set (map \<alpha> lc)\<rbrakk> \<Longrightarrow> fc ?xc = fa (\<alpha> ?xc)
[PROOF STEP]
have "foldli (map \<alpha> lc) c fa \<sigma>0 = foldli lc c fc \<sigma>0"
[PROOF STATE]
proof (prove)
using this:
?xc \<in> set lc \<Longrightarrow> invar ?xc
\<lbrakk>invar ?xc; \<alpha> ?xc \<in> set (map \<alpha> lc)\<rbrakk> \<Longrightarrow> fc ?xc = fa (\<alpha> ?xc)

goal (1 subgoal):
 1. foldli (map \<alpha> lc) c fa \<sigma>0 = foldli lc c fc \<sigma>0
[PROOF STEP]
by (induct lc arbitrary: \<sigma>0) simp_all
[PROOF STATE]
proof (state)
this:
foldli (map \<alpha> lc) c fa \<sigma>0 = foldli lc c fc \<sigma>0

goal (1 subgoal):
 1. P (iti c fc \<sigma>0)
[PROOF STEP]
with P_OK iti_eq
[PROOF STATE]
proof (chain)
picking this:
P (foldli (map \<alpha> lc) c fa \<sigma>0)
iti = foldli lc
foldli (map \<alpha> lc) c fa \<sigma>0 = foldli lc c fc \<sigma>0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P (foldli (map \<alpha> lc) c fa \<sigma>0)
iti = foldli lc
foldli (map \<alpha> lc) c fa \<sigma>0 = foldli lc c fc \<sigma>0

goal (1 subgoal):
 1. P (iti c fc \<sigma>0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P (iti c fc \<sigma>0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma remove_abs2 :
    "\<exists>S0'. set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y)) \<and>
           inj_on \<alpha> S0' \<and> \<alpha> ` S0' = S0 \<and> (\<forall>x \<in> S0'. invar x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S0'. set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y)) \<and> inj_on \<alpha> S0' \<and> \<alpha> ` S0' = S0 \<and> (\<forall>x\<in>S0'. invar x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>S0'. set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y)) \<and> inj_on \<alpha> S0' \<and> \<alpha> ` S0' = S0 \<and> (\<forall>x\<in>S0'. invar x)
[PROOF STEP]
from foldli_transform
[PROOF STATE]
proof (chain)
picking this:
\<exists>lc. (\<forall>xc\<in>set lc. invar xc) \<and> distinct (map \<alpha> lc) \<and> S0 = set (map \<alpha> lc) \<and> sorted_wrt R (map \<alpha> lc) \<and> iti = foldli lc
[PROOF STEP]
obtain lc where
          lc_invar: "\<And>xc. xc \<in> set lc \<Longrightarrow> invar xc"
      and \<alpha>_props: "distinct (map \<alpha> lc)" "S0 = set (map \<alpha> lc)"
                   "sorted_wrt R (map \<alpha> lc)"
      and iti_eq: "iti = foldli lc"
[PROOF STATE]
proof (prove)
using this:
\<exists>lc. (\<forall>xc\<in>set lc. invar xc) \<and> distinct (map \<alpha> lc) \<and> S0 = set (map \<alpha> lc) \<and> sorted_wrt R (map \<alpha> lc) \<and> iti = foldli lc

goal (1 subgoal):
 1. (\<And>lc. \<lbrakk>\<And>xc. xc \<in> set lc \<Longrightarrow> invar xc; distinct (map \<alpha> lc); S0 = set (map \<alpha> lc); sorted_wrt R (map \<alpha> lc); iti = foldli lc\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?xc \<in> set lc \<Longrightarrow> invar ?xc
distinct (map \<alpha> lc)
S0 = set (map \<alpha> lc)
sorted_wrt R (map \<alpha> lc)
iti = foldli lc

goal (1 subgoal):
 1. \<exists>S0'. set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y)) \<and> inj_on \<alpha> S0' \<and> \<alpha> ` S0' = S0 \<and> (\<forall>x\<in>S0'. invar x)
[PROOF STEP]
from \<alpha>_props
[PROOF STATE]
proof (chain)
picking this:
distinct (map \<alpha> lc)
S0 = set (map \<alpha> lc)
sorted_wrt R (map \<alpha> lc)
[PROOF STEP]
have it': "set_iterator_genord iti (set lc) (\<lambda>x y. R (\<alpha> x) (\<alpha> y))"
[PROOF STATE]
proof (prove)
using this:
distinct (map \<alpha> lc)
S0 = set (map \<alpha> lc)
sorted_wrt R (map \<alpha> lc)

goal (1 subgoal):
 1. set_iterator_genord iti (set lc) (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
[PROOF STEP]
apply (rule_tac set_iterator_genord_I [of lc])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>distinct (map \<alpha> lc); S0 = set (map \<alpha> lc); sorted_wrt R (map \<alpha> lc)\<rbrakk> \<Longrightarrow> distinct lc
 2. \<lbrakk>distinct (map \<alpha> lc); S0 = set (map \<alpha> lc); sorted_wrt R (map \<alpha> lc)\<rbrakk> \<Longrightarrow> set lc = set lc
 3. \<lbrakk>distinct (map \<alpha> lc); S0 = set (map \<alpha> lc); sorted_wrt R (map \<alpha> lc)\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. R (\<alpha> x) (\<alpha> y)) lc
 4. \<lbrakk>distinct (map \<alpha> lc); S0 = set (map \<alpha> lc); sorted_wrt R (map \<alpha> lc)\<rbrakk> \<Longrightarrow> iti = foldli lc
[PROOF STEP]
apply (simp_all add: distinct_map sorted_wrt_map iti_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
set_iterator_genord iti (set lc) (\<lambda>x y. R (\<alpha> x) (\<alpha> y))

goal (1 subgoal):
 1. \<exists>S0'. set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y)) \<and> inj_on \<alpha> S0' \<and> \<alpha> ` S0' = S0 \<and> (\<forall>x\<in>S0'. invar x)
[PROOF STEP]
from \<alpha>_props
[PROOF STATE]
proof (chain)
picking this:
distinct (map \<alpha> lc)
S0 = set (map \<alpha> lc)
sorted_wrt R (map \<alpha> lc)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct (map \<alpha> lc)
S0 = set (map \<alpha> lc)
sorted_wrt R (map \<alpha> lc)

goal (1 subgoal):
 1. \<exists>S0'. set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y)) \<and> inj_on \<alpha> S0' \<and> \<alpha> ` S0' = S0 \<and> (\<forall>x\<in>S0'. invar x)
[PROOF STEP]
apply (rule_tac exI[where x = "set lc"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (map \<alpha> lc); S0 = set (map \<alpha> lc); sorted_wrt R (map \<alpha> lc)\<rbrakk> \<Longrightarrow> set_iterator_genord iti (set lc) (\<lambda>x y. R (\<alpha> x) (\<alpha> y)) \<and> inj_on \<alpha> (set lc) \<and> \<alpha> ` set lc = S0 \<and> (\<forall>x\<in>set lc. invar x)
[PROOF STEP]
apply (simp add: lc_invar distinct_map it')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>S0'. set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y)) \<and> inj_on \<alpha> S0' \<and> \<alpha> ` S0' = S0 \<and> (\<forall>x\<in>S0'. invar x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iteratei_abs_simple_rule_P:
  assumes f_OK: "\<And>xc. invar xc \<Longrightarrow> \<alpha> xc \<in> S0 \<Longrightarrow> f xc = f' (\<alpha> xc)"
  assumes pre :
      "I S0 \<sigma>0"
      "\<And>S \<sigma> x. \<lbrakk> c \<sigma>; x \<in> S; I S \<sigma>; S \<subseteq> S0;
                 \<forall>y\<in>S - {x}. R x y; \<forall>y\<in>S0 - S. R y x\<rbrakk>
                 \<Longrightarrow> I (S - {x}) (f' x \<sigma>)"
      "\<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
      "\<And>\<sigma> S. \<lbrakk> S \<subseteq> S0; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>;
               \<forall>x\<in>S. \<forall>y\<in>S0-S. R y x \<rbrakk> \<Longrightarrow> P \<sigma>"
    shows "P (iti c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
apply (rule remove_abs[of f f' P c \<sigma>0])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xc. \<lbrakk>invar xc; \<alpha> xc \<in> S0\<rbrakk> \<Longrightarrow> f xc = f' (\<alpha> xc)
 2. \<And>iti. set_iterator_genord iti S0 R \<Longrightarrow> P (iti c f' \<sigma>0)
[PROOF STEP]
apply (simp add: f_OK)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>iti. set_iterator_genord iti S0 R \<Longrightarrow> P (iti c f' \<sigma>0)
[PROOF STEP]
apply (erule set_iterator_genord.iteratei_rule_P [of _ S0 R I])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>iti. I S0 \<sigma>0
 2. \<And>iti S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I S \<sigma>; S \<subseteq> S0; \<forall>y\<in>S - {x}. R x y; \<forall>y\<in>S0 - S. R y x\<rbrakk> \<Longrightarrow> I (S - {x}) (f' x \<sigma>)
 3. \<And>iti \<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>iti \<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0 - S. R y x\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply (simp_all add: pre)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iteratei_abs_simple_rule_insert_P:
  assumes f_OK: "\<And>xc. invar xc \<Longrightarrow> \<alpha> xc \<in> S0 \<Longrightarrow> f xc = f' (\<alpha> xc)"
  assumes pre :
      "I {} \<sigma>0"
      "\<And>S \<sigma> x. \<lbrakk> c \<sigma>; x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0; \<forall>y\<in>(S0 - S) - {x}. R x y;
                 \<forall>y\<in>S. R y x\<rbrakk>
                  \<Longrightarrow> I (insert x S) (f' x \<sigma>)"
      "\<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>"
      "\<And>\<sigma> S. \<lbrakk> S \<subseteq> S0; S \<noteq> S0;
              \<not> (c \<sigma>); I S \<sigma>; \<forall>x\<in>S0-S. \<forall>y\<in>S. R y x \<rbrakk> \<Longrightarrow> P \<sigma>"
  shows "P (iti c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
apply (rule remove_abs[of f f' P c \<sigma>0])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xc. \<lbrakk>invar xc; \<alpha> xc \<in> S0\<rbrakk> \<Longrightarrow> f xc = f' (\<alpha> xc)
 2. \<And>iti. set_iterator_genord iti S0 R \<Longrightarrow> P (iti c f' \<sigma>0)
[PROOF STEP]
apply (simp add: f_OK)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>iti. set_iterator_genord iti S0 R \<Longrightarrow> P (iti c f' \<sigma>0)
[PROOF STEP]
apply (erule set_iterator_genord.iteratei_rule_insert_P [of _ S0 R I])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>iti. I {} \<sigma>0
 2. \<And>iti S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0; \<forall>y\<in>S0 - S - {x}. R x y; \<forall>y\<in>S. R y x\<rbrakk> \<Longrightarrow> I (insert x S) (f' x \<sigma>)
 3. \<And>iti \<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>iti \<sigma> S. \<lbrakk>S \<subseteq> S0; S \<noteq> S0; \<not> c \<sigma>; I S \<sigma>; \<forall>x\<in>S0 - S. \<forall>y\<in>S. R y x\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply (simp_all add: pre)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iteratei_abs_rule_P:
  assumes pre :
      "I S0 \<sigma>0"
      "\<And>S \<sigma> x. \<lbrakk> c \<sigma>; invar x; \<alpha> x \<in> S; I S \<sigma>; S \<subseteq> S0;
                 \<forall>y\<in>S - {\<alpha> x}. R (\<alpha> x) y; \<forall>y\<in>S0 - S. R y (\<alpha> x)\<rbrakk>
                 \<Longrightarrow> I (S - {\<alpha> x}) (f x \<sigma>)"
      "\<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
      "\<And>\<sigma> S. \<lbrakk> S \<subseteq> S0; S \<noteq> {}; \<not> c \<sigma>; I S \<sigma>;
               \<forall>x\<in>S. \<forall>y\<in>S0-S. R y x \<rbrakk> \<Longrightarrow> P \<sigma>"
    shows "P (iti c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
obtain S0' where S0'_props: "set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))"
       "inj_on \<alpha> S0'" "S0 = \<alpha> ` S0'" "\<And>x. x \<in> S0' \<Longrightarrow> invar x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S0'. \<lbrakk>set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y)); inj_on \<alpha> S0'; S0 = \<alpha> ` S0'; \<And>x. x \<in> S0' \<Longrightarrow> invar x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis remove_abs2)
[PROOF STATE]
proof (state)
this:
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x

goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
proof (rule set_iterator_genord.iteratei_rule_P[OF S0'_props(1), of "\<lambda>S \<sigma>. I (\<alpha> ` S) \<sigma>" \<sigma>0 c], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. I (\<alpha> ` S0') \<sigma>0
 2. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` (S - {x})) (f x \<sigma>)
 3. \<And>\<sigma>. I (\<alpha> ` {}) \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. I (\<alpha> ` S0') \<sigma>0
 2. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` (S - {x})) (f x \<sigma>)
 3. \<And>\<sigma>. I (\<alpha> ` {}) \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I (\<alpha> ` S0') \<sigma>0
[PROOF STEP]
using S0'_props pre
[PROOF STATE]
proof (prove)
using this:
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
I S0 \<sigma>0
\<lbrakk>c ?\<sigma>; invar ?x; \<alpha> ?x \<in> ?S; I ?S ?\<sigma>; ?S \<subseteq> S0; \<forall>y\<in>?S - {\<alpha> ?x}. R (\<alpha> ?x) y; \<forall>y\<in>S0 - ?S. R y (\<alpha> ?x)\<rbrakk> \<Longrightarrow> I (?S - {\<alpha> ?x}) (f ?x ?\<sigma>)
I {} ?\<sigma> \<Longrightarrow> P ?\<sigma>
\<lbrakk>?S \<subseteq> S0; ?S \<noteq> {}; \<not> c ?\<sigma>; I ?S ?\<sigma>; \<forall>x\<in>?S. \<forall>y\<in>S0 - ?S. R y x\<rbrakk> \<Longrightarrow> P ?\<sigma>

goal (1 subgoal):
 1. I (\<alpha> ` S0') \<sigma>0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I (\<alpha> ` S0') \<sigma>0

goal (3 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` (S - {x})) (f x \<sigma>)
 2. \<And>\<sigma>. I (\<alpha> ` {}) \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` (S - {x})) (f x \<sigma>)
 2. \<And>\<sigma>. I (\<alpha> ` {}) \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
I (\<alpha> ` {}) \<sigma>_

goal (3 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` (S - {x})) (f x \<sigma>)
 2. \<And>\<sigma>. I (\<alpha> ` {}) \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
I (\<alpha> ` {}) \<sigma>_

goal (1 subgoal):
 1. P \<sigma>_
[PROOF STEP]
using S0'_props pre
[PROOF STATE]
proof (prove)
using this:
I (\<alpha> ` {}) \<sigma>_
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
I S0 \<sigma>0
\<lbrakk>c ?\<sigma>; invar ?x; \<alpha> ?x \<in> ?S; I ?S ?\<sigma>; ?S \<subseteq> S0; \<forall>y\<in>?S - {\<alpha> ?x}. R (\<alpha> ?x) y; \<forall>y\<in>S0 - ?S. R y (\<alpha> ?x)\<rbrakk> \<Longrightarrow> I (?S - {\<alpha> ?x}) (f ?x ?\<sigma>)
I {} ?\<sigma> \<Longrightarrow> P ?\<sigma>
\<lbrakk>?S \<subseteq> S0; ?S \<noteq> {}; \<not> c ?\<sigma>; I ?S ?\<sigma>; \<forall>x\<in>?S. \<forall>y\<in>S0 - ?S. R y x\<rbrakk> \<Longrightarrow> P ?\<sigma>

goal (1 subgoal):
 1. P \<sigma>_
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<sigma>_

goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` (S - {x})) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` (S - {x})) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case prems: (2 S \<sigma> x)
[PROOF STATE]
proof (state)
this:
c \<sigma>
x \<in> S
I (\<alpha> ` S) \<sigma>
S \<subseteq> S0'
\<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y)
\<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)

goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` (S - {x})) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
from prems S0'_props
[PROOF STATE]
proof (chain)
picking this:
c \<sigma>
x \<in> S
I (\<alpha> ` S) \<sigma>
S \<subseteq> S0'
\<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y)
\<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
[PROOF STEP]
have inv_x: "invar x"
[PROOF STATE]
proof (prove)
using this:
c \<sigma>
x \<in> S
I (\<alpha> ` S) \<sigma>
S \<subseteq> S0'
\<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y)
\<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x

goal (1 subgoal):
 1. invar x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invar x

goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` (S - {x})) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
from prems(4)
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> S0'
[PROOF STEP]
have subs_alpha: "\<alpha> ` S \<subseteq> \<alpha> ` S0'"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> S0'

goal (1 subgoal):
 1. \<alpha> ` S \<subseteq> \<alpha> ` S0'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> ` S \<subseteq> \<alpha> ` S0'

goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` (S - {x})) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
from S0'_props prems(2,4)
[PROOF STATE]
proof (chain)
picking this:
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
x \<in> S
S \<subseteq> S0'
[PROOF STEP]
have diff_alpha: "\<alpha> ` S - {\<alpha> x} = \<alpha> ` (S - {x})" "\<alpha> ` S0' - \<alpha> ` S = \<alpha> ` (S0' - S)"
[PROOF STATE]
proof (prove)
using this:
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
x \<in> S
S \<subseteq> S0'

goal (1 subgoal):
 1. \<alpha> ` S - {\<alpha> x} = \<alpha> ` (S - {x}) &&& \<alpha> ` S0' - \<alpha> ` S = \<alpha> ` (S0' - S)
[PROOF STEP]
by (auto simp add: inj_on_def subset_iff Ball_def)
[PROOF STATE]
proof (state)
this:
\<alpha> ` S - {\<alpha> x} = \<alpha> ` (S - {x})
\<alpha> ` S0' - \<alpha> ` S = \<alpha> ` (S0' - S)

goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` (S - {x})) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I (\<alpha> ` (S - {x})) (f x \<sigma>)
[PROOF STEP]
using pre(2)[of \<sigma> x "\<alpha> ` S"] S0'_props(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>c \<sigma>; invar x; \<alpha> x \<in> \<alpha> ` S; I (\<alpha> ` S) \<sigma>; \<alpha> ` S \<subseteq> S0; \<forall>y\<in>\<alpha> ` S - {\<alpha> x}. R (\<alpha> x) y; \<forall>y\<in>S0 - \<alpha> ` S. R y (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` S - {\<alpha> x}) (f x \<sigma>)
S0 = \<alpha> ` S0'

goal (1 subgoal):
 1. I (\<alpha> ` (S - {x})) (f x \<sigma>)
[PROOF STEP]
by (simp add: inv_x prems subs_alpha diff_alpha)
[PROOF STATE]
proof (state)
this:
I (\<alpha> ` (S - {x})) (f x \<sigma>)

goal (1 subgoal):
 1. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case prems: (4 \<sigma> S)
[PROOF STATE]
proof (state)
this:
S \<subseteq> S0'
S \<noteq> {}
\<not> c \<sigma>
I (\<alpha> ` S) \<sigma>
\<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)

goal (1 subgoal):
 1. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<sigma>
[PROOF STEP]
using pre(4)[of "\<alpha> ` S" \<sigma>] prems S0'_props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<alpha> ` S \<subseteq> S0; \<alpha> ` S \<noteq> {}; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>\<alpha> ` S. \<forall>y\<in>S0 - \<alpha> ` S. R y x\<rbrakk> \<Longrightarrow> P \<sigma>
S \<subseteq> S0'
S \<noteq> {}
\<not> c \<sigma>
I (\<alpha> ` S) \<sigma>
\<forall>x\<in>S. \<forall>y\<in>S0' - S. R (\<alpha> y) (\<alpha> x)
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P (iti c f \<sigma>0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iteratei_abs_rule_insert_P:
  assumes pre :
      "I {} \<sigma>0"
      "\<And>S \<sigma> x. \<lbrakk> c \<sigma>; invar x; \<alpha> x \<in> S0 - S; I S \<sigma>; S \<subseteq> S0;
                 \<forall>y\<in>(S0 - S) - {\<alpha> x}. R (\<alpha> x) y; \<forall>y\<in>S. R y (\<alpha> x)\<rbrakk>
                 \<Longrightarrow> I (insert (\<alpha> x) S) (f x \<sigma>)"
      "\<And>\<sigma>. I S0 \<sigma> \<Longrightarrow> P \<sigma>"
      "\<And>\<sigma> S. \<lbrakk> S \<subseteq> S0; S \<noteq> S0; \<not> c \<sigma>; I S \<sigma>;
               \<forall>x\<in>S0-S. \<forall>y\<in>S. R y x \<rbrakk> \<Longrightarrow> P \<sigma>"
    shows "P (iti c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
obtain S0' where S0'_props: "set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))"
       "inj_on \<alpha> S0'" "S0 = \<alpha> ` S0'" "\<And>x. x \<in> S0' \<Longrightarrow> invar x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S0'. \<lbrakk>set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y)); inj_on \<alpha> S0'; S0 = \<alpha> ` S0'; \<And>x. x \<in> S0' \<Longrightarrow> invar x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis remove_abs2)
[PROOF STATE]
proof (state)
this:
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x

goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iti c f \<sigma>0)
[PROOF STEP]
proof (rule set_iterator_genord.iteratei_rule_insert_P[OF S0'_props(1), of "\<lambda>S \<sigma>. I (\<alpha> ` S) \<sigma>" \<sigma>0 c], goal_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. I (\<alpha> ` {}) \<sigma>0
 2. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0' - S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` insert x S) (f x \<sigma>)
 3. \<And>\<sigma>. I (\<alpha> ` S0') \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. I (\<alpha> ` {}) \<sigma>0
 2. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0' - S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` insert x S) (f x \<sigma>)
 3. \<And>\<sigma>. I (\<alpha> ` S0') \<sigma> \<Longrightarrow> P \<sigma>
 4. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I (\<alpha> ` {}) \<sigma>0
[PROOF STEP]
using S0'_props pre
[PROOF STATE]
proof (prove)
using this:
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
I {} \<sigma>0
\<lbrakk>c ?\<sigma>; invar ?x; \<alpha> ?x \<in> S0 - ?S; I ?S ?\<sigma>; ?S \<subseteq> S0; \<forall>y\<in>S0 - ?S - {\<alpha> ?x}. R (\<alpha> ?x) y; \<forall>y\<in>?S. R y (\<alpha> ?x)\<rbrakk> \<Longrightarrow> I (insert (\<alpha> ?x) ?S) (f ?x ?\<sigma>)
I S0 ?\<sigma> \<Longrightarrow> P ?\<sigma>
\<lbrakk>?S \<subseteq> S0; ?S \<noteq> S0; \<not> c ?\<sigma>; I ?S ?\<sigma>; \<forall>x\<in>S0 - ?S. \<forall>y\<in>?S. R y x\<rbrakk> \<Longrightarrow> P ?\<sigma>

goal (1 subgoal):
 1. I (\<alpha> ` {}) \<sigma>0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I (\<alpha> ` {}) \<sigma>0

goal (3 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0' - S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` insert x S) (f x \<sigma>)
 2. \<And>\<sigma>. I (\<alpha> ` S0') \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0' - S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` insert x S) (f x \<sigma>)
 2. \<And>\<sigma>. I (\<alpha> ` S0') \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
I (\<alpha> ` S0') \<sigma>_

goal (3 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0' - S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` insert x S) (f x \<sigma>)
 2. \<And>\<sigma>. I (\<alpha> ` S0') \<sigma> \<Longrightarrow> P \<sigma>
 3. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
I (\<alpha> ` S0') \<sigma>_

goal (1 subgoal):
 1. P \<sigma>_
[PROOF STEP]
using S0'_props pre
[PROOF STATE]
proof (prove)
using this:
I (\<alpha> ` S0') \<sigma>_
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
I {} \<sigma>0
\<lbrakk>c ?\<sigma>; invar ?x; \<alpha> ?x \<in> S0 - ?S; I ?S ?\<sigma>; ?S \<subseteq> S0; \<forall>y\<in>S0 - ?S - {\<alpha> ?x}. R (\<alpha> ?x) y; \<forall>y\<in>?S. R y (\<alpha> ?x)\<rbrakk> \<Longrightarrow> I (insert (\<alpha> ?x) ?S) (f ?x ?\<sigma>)
I S0 ?\<sigma> \<Longrightarrow> P ?\<sigma>
\<lbrakk>?S \<subseteq> S0; ?S \<noteq> S0; \<not> c ?\<sigma>; I ?S ?\<sigma>; \<forall>x\<in>S0 - ?S. \<forall>y\<in>?S. R y x\<rbrakk> \<Longrightarrow> P ?\<sigma>

goal (1 subgoal):
 1. P \<sigma>_
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<sigma>_

goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0' - S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` insert x S) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0' - S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` insert x S) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case prems: (2 S \<sigma> x)
[PROOF STATE]
proof (state)
this:
c \<sigma>
x \<in> S0' - S
I (\<alpha> ` S) \<sigma>
S \<subseteq> S0'
\<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y)
\<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)

goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0' - S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` insert x S) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
from prems S0'_props
[PROOF STATE]
proof (chain)
picking this:
c \<sigma>
x \<in> S0' - S
I (\<alpha> ` S) \<sigma>
S \<subseteq> S0'
\<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y)
\<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
[PROOF STEP]
have inv_x: "invar x"
[PROOF STATE]
proof (prove)
using this:
c \<sigma>
x \<in> S0' - S
I (\<alpha> ` S) \<sigma>
S \<subseteq> S0'
\<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y)
\<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x

goal (1 subgoal):
 1. invar x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invar x

goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0' - S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` insert x S) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
from prems(4)
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> S0'
[PROOF STEP]
have subs_alpha: "\<alpha> ` S \<subseteq> \<alpha> ` S0'"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> S0'

goal (1 subgoal):
 1. \<alpha> ` S \<subseteq> \<alpha> ` S0'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> ` S \<subseteq> \<alpha> ` S0'

goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0' - S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` insert x S) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
from S0'_props prems(2,4)
[PROOF STATE]
proof (chain)
picking this:
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
x \<in> S0' - S
S \<subseteq> S0'
[PROOF STEP]
have diff_alpha: "\<alpha> ` (S0' - S) - {\<alpha> x} = \<alpha> ` ((S0' - S) - {x})" "\<alpha> ` S0' - \<alpha> ` S = \<alpha> ` (S0' - S)"
[PROOF STATE]
proof (prove)
using this:
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
x \<in> S0' - S
S \<subseteq> S0'

goal (1 subgoal):
 1. \<alpha> ` (S0' - S) - {\<alpha> x} = \<alpha> ` (S0' - S - {x}) &&& \<alpha> ` S0' - \<alpha> ` S = \<alpha> ` (S0' - S)
[PROOF STEP]
by (auto simp add: inj_on_def subset_iff Ball_def)
[PROOF STATE]
proof (state)
this:
\<alpha> ` (S0' - S) - {\<alpha> x} = \<alpha> ` (S0' - S - {x})
\<alpha> ` S0' - \<alpha> ` S = \<alpha> ` (S0' - S)

goal (2 subgoals):
 1. \<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S0' - S; I (\<alpha> ` S) \<sigma>; S \<subseteq> S0'; \<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y); \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> I (\<alpha> ` insert x S) (f x \<sigma>)
 2. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I (\<alpha> ` insert x S) (f x \<sigma>)
[PROOF STEP]
using pre(2)[of \<sigma> x "\<alpha> ` S"] prems S0'_props(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>c \<sigma>; invar x; \<alpha> x \<in> S0 - \<alpha> ` S; I (\<alpha> ` S) \<sigma>; \<alpha> ` S \<subseteq> S0; \<forall>y\<in>S0 - \<alpha> ` S - {\<alpha> x}. R (\<alpha> x) y; \<forall>y\<in>\<alpha> ` S. R y (\<alpha> x)\<rbrakk> \<Longrightarrow> I (insert (\<alpha> x) (\<alpha> ` S)) (f x \<sigma>)
c \<sigma>
x \<in> S0' - S
I (\<alpha> ` S) \<sigma>
S \<subseteq> S0'
\<forall>y\<in>S0' - S - {x}. R (\<alpha> x) (\<alpha> y)
\<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)
S0 = \<alpha> ` S0'

goal (1 subgoal):
 1. I (\<alpha> ` insert x S) (f x \<sigma>)
[PROOF STEP]
by (simp add: diff_alpha inv_x subs_alpha)
[PROOF STATE]
proof (state)
this:
I (\<alpha> ` insert x S) (f x \<sigma>)

goal (1 subgoal):
 1. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
case prems: (4 \<sigma> S)
[PROOF STATE]
proof (state)
this:
S \<subseteq> S0'
S \<noteq> S0'
\<not> c \<sigma>
I (\<alpha> ` S) \<sigma>
\<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)

goal (1 subgoal):
 1. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
from prems(1)
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> S0'
[PROOF STEP]
have subs_alpha: "\<alpha> ` S \<subseteq> \<alpha> ` S0'"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> S0'

goal (1 subgoal):
 1. \<alpha> ` S \<subseteq> \<alpha> ` S0'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> ` S \<subseteq> \<alpha> ` S0'

goal (1 subgoal):
 1. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
from S0'_props prems
[PROOF STATE]
proof (chain)
picking this:
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
S \<subseteq> S0'
S \<noteq> S0'
\<not> c \<sigma>
I (\<alpha> ` S) \<sigma>
\<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)
[PROOF STEP]
have diff_alpha: "\<alpha> ` S0' - \<alpha> ` S = \<alpha> ` (S0' - S)"
[PROOF STATE]
proof (prove)
using this:
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
S \<subseteq> S0'
S \<noteq> S0'
\<not> c \<sigma>
I (\<alpha> ` S) \<sigma>
\<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)

goal (1 subgoal):
 1. \<alpha> ` S0' - \<alpha> ` S = \<alpha> ` (S0' - S)
[PROOF STEP]
by (auto simp add: inj_on_def subset_iff Ball_def)
[PROOF STATE]
proof (state)
this:
\<alpha> ` S0' - \<alpha> ` S = \<alpha> ` (S0' - S)

goal (1 subgoal):
 1. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
from prems(1,2) S0'_props(2,3)
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> S0'
S \<noteq> S0'
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
[PROOF STEP]
have alpha_eq: "\<alpha> ` S \<noteq> \<alpha> ` S0'"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> S0'
S \<noteq> S0'
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'

goal (1 subgoal):
 1. \<alpha> ` S \<noteq> \<alpha> ` S0'
[PROOF STEP]
apply (simp add: inj_on_def set_eq_iff image_iff Bex_def subset_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t. t \<in> S \<longrightarrow> t \<in> S0'; \<exists>x. (x \<in> S) = (x \<notin> S0'); \<forall>x\<in>S0'. \<forall>y\<in>S0'. \<alpha> x = \<alpha> y \<longrightarrow> x = y; \<forall>x. (x \<in> S0) = (\<exists>xa. xa \<in> S0' \<and> x = \<alpha> xa)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>xa. xa \<in> S \<and> x = \<alpha> xa) = (\<forall>xa. xa \<in> S0' \<longrightarrow> x \<noteq> \<alpha> xa)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<alpha> ` S \<noteq> \<alpha> ` S0'

goal (1 subgoal):
 1. \<And>\<sigma> S. \<lbrakk>S \<subseteq> S0'; S \<noteq> S0'; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<sigma>
[PROOF STEP]
using pre(4)[of "\<alpha> ` S" \<sigma>] S0'_props prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<alpha> ` S \<subseteq> S0; \<alpha> ` S \<noteq> S0; \<not> c \<sigma>; I (\<alpha> ` S) \<sigma>; \<forall>x\<in>S0 - \<alpha> ` S. \<forall>y\<in>\<alpha> ` S. R y x\<rbrakk> \<Longrightarrow> P \<sigma>
set_iterator_genord iti S0' (\<lambda>x y. R (\<alpha> x) (\<alpha> y))
inj_on \<alpha> S0'
S0 = \<alpha> ` S0'
?x \<in> S0' \<Longrightarrow> invar ?x
S \<subseteq> S0'
S \<noteq> S0'
\<not> c \<sigma>
I (\<alpha> ` S) \<sigma>
\<forall>x\<in>S0' - S. \<forall>y\<in>S. R (\<alpha> y) (\<alpha> x)

goal (1 subgoal):
 1. P \<sigma>
[PROOF STEP]
by (auto simp add: subs_alpha diff_alpha alpha_eq)
[PROOF STATE]
proof (state)
this:
P \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P (iti c f \<sigma>0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_iterator_abs_genord_trivial:
  "set_iterator_abs_genord id (\<lambda>_. True) = set_iterator_genord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_abs_genord id (\<lambda>_. True) = set_iterator_genord
[PROOF STEP]
by (simp add: set_iterator_genord_def set_iterator_abs_genord_def fun_eq_iff)


[STATEMENT]
lemma set_iterator_abs_genord_trivial_simp [simp] :
  assumes "\<forall>x. invar x"
      and "\<forall>x. \<alpha> x = x"
shows "set_iterator_abs_genord \<alpha> invar = set_iterator_genord"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar = set_iterator_genord
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar = set_iterator_genord
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. invar x
\<forall>x. \<alpha> x = x
[PROOF STEP]
have "invar = (\<lambda>_. True)" and "\<alpha> = id"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. invar x
\<forall>x. \<alpha> x = x

goal (1 subgoal):
 1. invar = (\<lambda>_. True) &&& \<alpha> = id
[PROOF STEP]
by (simp_all add: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
invar = (\<lambda>_. True)
\<alpha> = id

goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar = set_iterator_genord
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
invar = (\<lambda>_. True)
\<alpha> = id

goal (1 subgoal):
 1. set_iterator_abs_genord \<alpha> invar = set_iterator_genord
[PROOF STEP]
by (simp add: set_iterator_abs_genord_trivial)
[PROOF STATE]
proof (state)
this:
set_iterator_abs_genord \<alpha> invar = set_iterator_genord

goal:
No subgoals!
[PROOF STEP]
qed