[STATEMENT]
lemma lookup_eq_order_irrelevant:
  assumes "distinct (map fst pairs)" and "distinct (map fst pairs')" and "set pairs = set pairs'"
  shows "lookup (\<lambda>x. x=k) pairs = lookup (\<lambda>x. x=k) pairs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
proof (cases "lookup (\<lambda>x. x=k) pairs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lookup (\<lambda>x. x = k) pairs = None \<Longrightarrow> lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
 2. \<And>a. lookup (\<lambda>x. x = k) pairs = Some a \<Longrightarrow> lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) pairs = None

goal (2 subgoals):
 1. lookup (\<lambda>x. x = k) pairs = None \<Longrightarrow> lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
 2. \<And>a. lookup (\<lambda>x. x = k) pairs = Some a \<Longrightarrow> lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lookup (\<lambda>x. x = k) pairs = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>x. x = k) pairs = None

goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
using lookup_None_iff
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>x. x = k) pairs = None
(lookup ?P ?xs = None) = (\<nexists>x. x \<in> set (map fst ?xs) \<and> ?P x)

goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
by (metis assms(3) set_map)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'

goal (1 subgoal):
 1. \<And>a. lookup (\<lambda>x. x = k) pairs = Some a \<Longrightarrow> lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. lookup (\<lambda>x. x = k) pairs = Some a \<Longrightarrow> lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
case (Some v)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) pairs = Some v

goal (1 subgoal):
 1. \<And>a. lookup (\<lambda>x. x = k) pairs = Some a \<Longrightarrow> lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
hence "(k,v)\<in>set pairs"
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>x. x = k) pairs = Some v

goal (1 subgoal):
 1. (k, v) \<in> set pairs
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>x. x = k) pairs = Some v
distinct (map fst pairs)

goal (1 subgoal):
 1. (k, v) \<in> set pairs
[PROOF STEP]
by (simp add: lookup_present_eq_key)
[PROOF STATE]
proof (state)
this:
(k, v) \<in> set pairs

goal (1 subgoal):
 1. \<And>a. lookup (\<lambda>x. x = k) pairs = Some a \<Longrightarrow> lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
hence el: "(k,v)\<in>set pairs'"
[PROOF STATE]
proof (prove)
using this:
(k, v) \<in> set pairs

goal (1 subgoal):
 1. (k, v) \<in> set pairs'
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
(k, v) \<in> set pairs
set pairs = set pairs'

goal (1 subgoal):
 1. (k, v) \<in> set pairs'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(k, v) \<in> set pairs'

goal (1 subgoal):
 1. \<And>a. lookup (\<lambda>x. x = k) pairs = Some a \<Longrightarrow> lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
using lookup_present_eq_key[OF assms(2)] el Some
[PROOF STATE]
proof (prove)
using this:
((?k, ?v) \<in> set pairs') = (lookup (\<lambda>x. x = ?k) pairs' = Some ?v)
(k, v) \<in> set pairs'
lookup (\<lambda>x. x = k) pairs = Some v

goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) pairs = lookup (\<lambda>x. x = k) pairs'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lookup_Some_append_back:
  "lookup (\<lambda>x. x=k) insts = Some v \<Longrightarrow> lookup (\<lambda>x. x=k) (insts@[(k,v')]) = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) insts = Some v \<Longrightarrow> lookup (\<lambda>x. x = k) (insts @ [(k, v')]) = Some v
[PROOF STEP]
by (induction insts arbitrary: ) auto


[STATEMENT]
lemma lookup_eq_key_not_present: "key \<notin> set (map fst inst) \<Longrightarrow> lookup (\<lambda>x. x = key) inst = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. key \<notin> set (map fst inst) \<Longrightarrow> lookup (\<lambda>x. x = key) inst = None
[PROOF STEP]
by (induction inst) auto


[STATEMENT]
lemma lookup_in_empty[simp]: "lookup f [] = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup f [] = None
[PROOF STEP]
by simp


[STATEMENT]
lemma lookup_in_single[simp]: "lookup f [(k, v)] = (if f k then Some v else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup f [(k, v)] = (if f k then Some v else None)
[PROOF STEP]
by simp


[STATEMENT]
lemma lookup_present_eq_key': "lookup (\<lambda>x. x=k) al = Some v \<Longrightarrow> (k, v) \<in> set al "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) al = Some v \<Longrightarrow> (k, v) \<in> set al
[PROOF STEP]
by (induction al) (auto simp add: rev_image_eqI split: if_splits)


[STATEMENT]
lemma lookup_present_eq_key'': "distinct (map fst al) \<Longrightarrow> lookup (\<lambda>x. x=k) al = Some v \<longleftrightarrow> (k, v) \<in> set al "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst al) \<Longrightarrow> (lookup (\<lambda>x. x = k) al = Some v) = ((k, v) \<in> set al)
[PROOF STEP]
by (induction al) (auto simp add: rev_image_eqI split: if_splits)


[STATEMENT]
lemma key_present_imp_eq_lookup_finds_value: "k \<in> fst ` set al \<Longrightarrow> \<exists>v . lookup (\<lambda>x. x=k) al = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> fst ` set al \<Longrightarrow> \<exists>v. lookup (\<lambda>x. x = k) al = Some v
[PROOF STEP]
by (induction al) (auto simp add: rev_image_eqI)


[STATEMENT]
lemma list_allI: "(\<And>x. x\<in>set l \<Longrightarrow> P x) \<Longrightarrow> list_all P l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> set l \<Longrightarrow> P x) \<Longrightarrow> list_all P l
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma map2_sym: "(\<And>x y . f x y = f y x) \<Longrightarrow> map2 f xs ys = map2 f ys xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. f x y = f y x) \<Longrightarrow> map2 f xs ys = map2 f ys xs
[PROOF STEP]
proof (induction xs arbitrary: ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. (\<And>x y. f x y = f y x) \<Longrightarrow> map2 f [] ys = map2 f ys []
 2. \<And>a xs ys. \<lbrakk>\<And>ys. (\<And>x y. f x y = f y x) \<Longrightarrow> map2 f xs ys = map2 f ys xs; \<And>x y. f x y = f y x\<rbrakk> \<Longrightarrow> map2 f (a # xs) ys = map2 f ys (a # xs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
f ?x ?y = f ?y ?x

goal (2 subgoals):
 1. \<And>ys. (\<And>x y. f x y = f y x) \<Longrightarrow> map2 f [] ys = map2 f ys []
 2. \<And>a xs ys. \<lbrakk>\<And>ys. (\<And>x y. f x y = f y x) \<Longrightarrow> map2 f xs ys = map2 f ys xs; \<And>x y. f x y = f y x\<rbrakk> \<Longrightarrow> map2 f (a # xs) ys = map2 f ys (a # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f ?x ?y = f ?y ?x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f ?x ?y = f ?y ?x

goal (1 subgoal):
 1. map2 f [] ys = map2 f ys []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map2 f [] ys = map2 f ys []

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. (\<And>x y. f x y = f y x) \<Longrightarrow> map2 f xs ys = map2 f ys xs; \<And>x y. f x y = f y x\<rbrakk> \<Longrightarrow> map2 f (a # xs) ys = map2 f ys (a # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. (\<And>x y. f x y = f y x) \<Longrightarrow> map2 f xs ys = map2 f ys xs; \<And>x y. f x y = f y x\<rbrakk> \<Longrightarrow> map2 f (a # xs) ys = map2 f ys (a # xs)
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
(\<And>x y. f x y = f y x) \<Longrightarrow> map2 f xs ?ys = map2 f ?ys xs
f ?x ?y = f ?y ?x

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. (\<And>x y. f x y = f y x) \<Longrightarrow> map2 f xs ys = map2 f ys xs; \<And>x y. f x y = f y x\<rbrakk> \<Longrightarrow> map2 f (a # xs) ys = map2 f ys (a # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. f x y = f y x) \<Longrightarrow> map2 f xs ?ys = map2 f ?ys xs
f ?x ?y = f ?y ?x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. f x y = f y x) \<Longrightarrow> map2 f xs ?ys = map2 f ?ys xs
f ?x ?y = f ?y ?x

goal (1 subgoal):
 1. map2 f (a # xs) ys = map2 f ys (a # xs)
[PROOF STEP]
by (induction ys) auto
[PROOF STATE]
proof (state)
this:
map2 f (a # xs) ys = map2 f ys (a # xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma idem_map2: assumes "(\<And>x. f x x = x)" shows "map2 f l l = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 f l l = l
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map2 f l l = l
[PROOF STEP]
have "length l = length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length l = length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length l = length l

goal (1 subgoal):
 1. map2 f l l = l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length l = length l
[PROOF STEP]
show "map2 f l l = l"
[PROOF STATE]
proof (prove)
using this:
length l = length l

goal (1 subgoal):
 1. map2 f l l = l
[PROOF STEP]
by (induction l l rule: list_induct2) (use assms in auto)
[PROOF STATE]
proof (state)
this:
map2 f l l = l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rev_induct2[consumes 1, case_names Nil snoc]:
  assumes "length xs = length ys"
  assumes "P [] []"
  assumes "(\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (xs @ [x]) (ys @ [y]))"
  shows "P xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P xs ys
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P xs ys
[PROOF STEP]
have "length (rev xs) = length (rev ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (rev xs) = length (rev ys)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
length xs = length ys

goal (1 subgoal):
 1. length (rev xs) = length (rev ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (rev xs) = length (rev ys)

goal (1 subgoal):
 1. P xs ys
[PROOF STEP]
hence "P (rev (rev xs)) (rev (rev ys))"
[PROOF STATE]
proof (prove)
using this:
length (rev xs) = length (rev ys)

goal (1 subgoal):
 1. P (rev (rev xs)) (rev (rev ys))
[PROOF STEP]
using assms(2-3)
[PROOF STATE]
proof (prove)
using this:
length (rev xs) = length (rev ys)
P [] []
\<lbrakk>length ?xs = length ?ys; P ?xs ?ys\<rbrakk> \<Longrightarrow> P (?xs @ [?x]) (?ys @ [?y])

goal (1 subgoal):
 1. P (rev (rev xs)) (rev (rev ys))
[PROOF STEP]
by (induction rule: list_induct2[of "rev xs" "rev ys"]) simp_all
[PROOF STATE]
proof (state)
this:
P (rev (rev xs)) (rev (rev ys))

goal (1 subgoal):
 1. P xs ys
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
P (rev (rev xs)) (rev (rev ys))

goal (1 subgoal):
 1. P xs ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P xs ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alist_map_corr: "distinct (map fst al) \<Longrightarrow> (k,v) \<in> set al \<longleftrightarrow> map_of al k = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst al) \<Longrightarrow> ((k, v) \<in> set al) = (map_of al k = Some v)
[PROOF STEP]
by simp


[STATEMENT]
lemma distinct_fst_imp_distinct: "distinct (map fst l) \<Longrightarrow> distinct l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst l) \<Longrightarrow> distinct l
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma length_alist:
  assumes "distinct (map fst al)" and "distinct (map fst al')" and "set al = set al'"
  shows "length al = length al'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length al = length al'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct (map fst al)
distinct (map fst al')
set al = set al'

goal (1 subgoal):
 1. length al = length al'
[PROOF STEP]
by (metis distinct_card length_map set_map)


[STATEMENT]
lemma same_map_of_imp_same_length:
  "distinct (map fst ars1) \<Longrightarrow> distinct (map fst ars2) \<Longrightarrow> map_of ars1 = map_of ars2
  \<Longrightarrow> length ars1 = length ars2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (map fst ars1); distinct (map fst ars2); map_of ars1 = map_of ars2\<rbrakk> \<Longrightarrow> length ars1 = length ars2
[PROOF STEP]
(* Name is a bit to specific*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct (map fst ars1); distinct (map fst ars2); map_of ars1 = map_of ars2\<rbrakk> \<Longrightarrow> length ars1 = length ars2
[PROOF STEP]
using length_alist map_of_inject_set
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (map fst ?al); distinct (map fst ?al'); set ?al = set ?al'\<rbrakk> \<Longrightarrow> length ?al = length ?al'
\<lbrakk>distinct (map fst ?xs); distinct (map fst ?ys)\<rbrakk> \<Longrightarrow> (map_of ?xs = map_of ?ys) = (set ?xs = set ?ys)

goal (1 subgoal):
 1. \<lbrakk>distinct (map fst ars1); distinct (map fst ars2); map_of ars1 = map_of ars2\<rbrakk> \<Longrightarrow> length ars1 = length ars2
[PROOF STEP]
by blast


[STATEMENT]
lemma in_range_if_ex_key: "v \<in> ran m \<longleftrightarrow> (\<exists>k. m k = Some v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<in> ran m) = (\<exists>k. m k = Some v)
[PROOF STEP]
by (auto simp add: ranI ran_def)


[STATEMENT]
lemma set_AList_delete_bound: "set (AList.delete a l) \<subseteq> set l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (AList.delete a l) \<subseteq> set l
[PROOF STEP]
by (induction l) auto


[STATEMENT]
lemma list_all_clearjunk_cons:
  "list_all P (x#(AList.clearjunk l)) \<Longrightarrow> list_all P (AList.clearjunk (x#l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all P (x # AList.clearjunk l) \<Longrightarrow> list_all P (AList.clearjunk (x # l))
[PROOF STEP]
by (induction l rule: AList.clearjunk.induct) (auto simp add: delete_twist)


[STATEMENT]
lemma lookup_AList_delete: "k'\<noteq>k \<Longrightarrow> lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.delete k' al)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' \<noteq> k \<Longrightarrow> lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.delete k' al)
[PROOF STEP]
by (induction al) auto


[STATEMENT]
lemma lookup_AList_clearjunk: "lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al)
[PROOF STEP]
proof (induction al)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lookup (\<lambda>x. x = k) [] = lookup (\<lambda>x. x = k) (AList.clearjunk [])
 2. \<And>a al. lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al) \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. lookup (\<lambda>x. x = k) [] = lookup (\<lambda>x. x = k) (AList.clearjunk [])
 2. \<And>a al. lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al) \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) [] = lookup (\<lambda>x. x = k) (AList.clearjunk [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) [] = lookup (\<lambda>x. x = k) (AList.clearjunk [])

goal (1 subgoal):
 1. \<And>a al. lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al) \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a al. lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al) \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
case (Cons a al)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al)

goal (1 subgoal):
 1. \<And>a al. lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al) \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al)

goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
proof(cases "fst a=k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a = k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
 2. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
fst a = k

goal (2 subgoals):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a = k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
 2. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst a = k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst a = k

goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
by (metis (full_types) clearjunk.simps(2) lookup.simps(2) prod.collapse)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))

goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
fst a \<noteq> k

goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
have "lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
      = lookup (\<lambda>x. x = k) (a # AList.clearjunk (AList.delete (fst a) al))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) (AList.clearjunk (a # al)) = lookup (\<lambda>x. x = k) (a # AList.clearjunk (AList.delete (fst a) al))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) (AList.clearjunk (a # al)) = lookup (\<lambda>x. x = k) (a # AList.clearjunk (AList.delete (fst a) al))

goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) (AList.clearjunk (a # al)) = lookup (\<lambda>x. x = k) (a # AList.clearjunk (AList.delete (fst a) al))

goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
have "\<dots> = lookup (\<lambda>x. x = k) (AList.clearjunk (AList.delete (fst a) al))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) (a # AList.clearjunk (AList.delete (fst a) al)) = lookup (\<lambda>x. x = k) (AList.clearjunk (AList.delete (fst a) al))
[PROOF STEP]
by (metis (full_types) False lookup.simps(2) surjective_pairing)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) (a # AList.clearjunk (AList.delete (fst a) al)) = lookup (\<lambda>x. x = k) (AList.clearjunk (AList.delete (fst a) al))

goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) (a # AList.clearjunk (AList.delete (fst a) al)) = lookup (\<lambda>x. x = k) (AList.clearjunk (AList.delete (fst a) al))

goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
have "\<dots> = lookup (\<lambda>x. x = k) (AList.clearjunk al)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) (AList.clearjunk (AList.delete (fst a) al)) = lookup (\<lambda>x. x = k) (AList.clearjunk al)
[PROOF STEP]
by (metis False clearjunk_delete lookup_AList_delete)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) (AList.clearjunk (AList.delete (fst a) al)) = lookup (\<lambda>x. x = k) (AList.clearjunk al)

goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) (AList.clearjunk (AList.delete (fst a) al)) = lookup (\<lambda>x. x = k) (AList.clearjunk al)

goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
have "\<dots> = lookup (\<lambda>x. x = k) al"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) (AList.clearjunk al) = lookup (\<lambda>x. x = k) al
[PROOF STEP]
using Cons.IH
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al)

goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) (AList.clearjunk al) = lookup (\<lambda>x. x = k) al
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) (AList.clearjunk al) = lookup (\<lambda>x. x = k) al

goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) (AList.clearjunk al) = lookup (\<lambda>x. x = k) al

goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
have "\<dots> = lookup (\<lambda>x. x = k) (a # al)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (a # al)
[PROOF STEP]
by (metis (full_types) False lookup.simps(2) surjective_pairing)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (a # al)

goal (1 subgoal):
 1. \<lbrakk>lookup (\<lambda>x. x = k) al = lookup (\<lambda>x. x = k) (AList.clearjunk al); fst a \<noteq> k\<rbrakk> \<Longrightarrow> lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lookup (\<lambda>x. x = k) (AList.clearjunk (a # al)) = lookup (\<lambda>x. x = k) (a # al)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>x. x = k) (AList.clearjunk (a # al)) = lookup (\<lambda>x. x = k) (a # al)

goal (1 subgoal):
 1. lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = k) (a # al) = lookup (\<lambda>x. x = k) (AList.clearjunk (a # al))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diff_list_set[simp]: "set (diff_list xs ys) = set xs - set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (diff_list xs ys) = set xs - set ys
[PROOF STEP]
unfolding diff_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (fold removeAll ys xs) = set xs - set ys
[PROOF STEP]
by (induction ys arbitrary: xs) auto


[STATEMENT]
lemma diff_list_set_from_Nil[simp]: "diff_list [] ys = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_list [] ys = []
[PROOF STEP]
using last_in_set
[PROOF STATE]
proof (prove)
using this:
?as \<noteq> [] \<Longrightarrow> last ?as \<in> set ?as

goal (1 subgoal):
 1. diff_list [] ys = []
[PROOF STEP]
by fastforce


[STATEMENT]
lemma diff_list_set_remove_Nil[simp]: "diff_list xs [] = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_list xs [] = xs
[PROOF STEP]
unfolding diff_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold removeAll [] xs = xs
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma diff_list_rec: "diff_list (x # xs) ys = (if x\<in>set ys then diff_list xs ys else x#diff_list xs ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_list (x # xs) ys = (if x \<in> set ys then diff_list xs ys else x # diff_list xs ys)
[PROOF STEP]
unfolding diff_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold removeAll ys (x # xs) = (if x \<in> set ys then fold removeAll ys xs else x # fold removeAll ys xs)
[PROOF STEP]
by (induction ys arbitrary: x xs) auto


[STATEMENT]
lemma diff_list_order_irr: "set ys = set ys' \<Longrightarrow> diff_list xs ys = diff_list xs ys'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ys = set ys' \<Longrightarrow> diff_list xs ys = diff_list xs ys'
[PROOF STEP]
proof (induction ys arbitrary: ys' xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys' xs. set [] = set ys' \<Longrightarrow> diff_list xs [] = diff_list xs ys'
 2. \<And>a ys ys' xs. \<lbrakk>\<And>ys' xs. set ys = set ys' \<Longrightarrow> diff_list xs ys = diff_list xs ys'; set (a # ys) = set ys'\<rbrakk> \<Longrightarrow> diff_list xs (a # ys) = diff_list xs ys'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
set [] = set ys'

goal (2 subgoals):
 1. \<And>ys' xs. set [] = set ys' \<Longrightarrow> diff_list xs [] = diff_list xs ys'
 2. \<And>a ys ys' xs. \<lbrakk>\<And>ys' xs. set ys = set ys' \<Longrightarrow> diff_list xs ys = diff_list xs ys'; set (a # ys) = set ys'\<rbrakk> \<Longrightarrow> diff_list xs (a # ys) = diff_list xs ys'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set [] = set ys'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set [] = set ys'

goal (1 subgoal):
 1. diff_list xs [] = diff_list xs ys'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
diff_list xs [] = diff_list xs ys'

goal (1 subgoal):
 1. \<And>a ys ys' xs. \<lbrakk>\<And>ys' xs. set ys = set ys' \<Longrightarrow> diff_list xs ys = diff_list xs ys'; set (a # ys) = set ys'\<rbrakk> \<Longrightarrow> diff_list xs (a # ys) = diff_list xs ys'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ys ys' xs. \<lbrakk>\<And>ys' xs. set ys = set ys' \<Longrightarrow> diff_list xs ys = diff_list xs ys'; set (a # ys) = set ys'\<rbrakk> \<Longrightarrow> diff_list xs (a # ys) = diff_list xs ys'
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
set ys = set ?ys' \<Longrightarrow> diff_list ?xs ys = diff_list ?xs ?ys'
set (y # ys) = set ys'

goal (1 subgoal):
 1. \<And>a ys ys' xs. \<lbrakk>\<And>ys' xs. set ys = set ys' \<Longrightarrow> diff_list xs ys = diff_list xs ys'; set (a # ys) = set ys'\<rbrakk> \<Longrightarrow> diff_list xs (a # ys) = diff_list xs ys'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set ys = set ?ys' \<Longrightarrow> diff_list ?xs ys = diff_list ?xs ?ys'
set (y # ys) = set ys'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set ys = set ?ys' \<Longrightarrow> diff_list ?xs ys = diff_list ?xs ?ys'
set (y # ys) = set ys'

goal (1 subgoal):
 1. diff_list xs (y # ys) = diff_list xs ys'
[PROOF STEP]
by (induction xs arbitrary: y ys ys') (simp_all add: diff_list_rec)
[PROOF STATE]
proof (state)
this:
diff_list xs (y # ys) = diff_list xs ys'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fold_Option_bind_eq_Some_start_not_None:
  "fold (\<lambda>new option . Option.bind option (f new)) list start = Some res
  \<Longrightarrow> start \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (\<lambda>new option. Option.bind option (f new)) list start = Some res \<Longrightarrow> start \<noteq> None
[PROOF STEP]
by (induction list arbitrary: start res)
    (fastforce split: option.splits if_splits simp add: bind_eq_Some_conv)+


[STATEMENT]
lemma fold_Option_bind_eq_Some_at_point_not_None:
  "fold (\<lambda>new option . Option.bind option (f new)) (l1@l2) start = Some res
  \<Longrightarrow> fold (\<lambda>new option . Option.bind option (f new)) (l1) start \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (\<lambda>new option. Option.bind option (f new)) (l1 @ l2) start = Some res \<Longrightarrow> fold (\<lambda>new option. Option.bind option (f new)) l1 start \<noteq> None
[PROOF STEP]
by (induction l1 arbitrary: start res l2) (use fold_Option_bind_eq_Some_start_not_None in
      \<open>fastforce split: option.splits if_splits simp add: bind_eq_Some_conv\<close>)+


[STATEMENT]
lemma fold_Option_bind_eq_Some_start_not_None':
  "fold (\<lambda>(x,y) option . Option.bind option (f x y)) list start = Some res
  \<Longrightarrow> start \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (\<lambda>(x, y) option. Option.bind option (f x y)) list start = Some res \<Longrightarrow> start \<noteq> None
[PROOF STEP]
proof (induction list arbitrary: start res)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>start res. fold (\<lambda>(x, y) option. Option.bind option (f x y)) [] start = Some res \<Longrightarrow> start \<noteq> None
 2. \<And>a list start res. \<lbrakk>\<And>start res. fold (\<lambda>(x, y) option. Option.bind option (f x y)) list start = Some res \<Longrightarrow> start \<noteq> None; fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # list) start = Some res\<rbrakk> \<Longrightarrow> start \<noteq> None
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) [] start = Some res

goal (2 subgoals):
 1. \<And>start res. fold (\<lambda>(x, y) option. Option.bind option (f x y)) [] start = Some res \<Longrightarrow> start \<noteq> None
 2. \<And>a list start res. \<lbrakk>\<And>start res. fold (\<lambda>(x, y) option. Option.bind option (f x y)) list start = Some res \<Longrightarrow> start \<noteq> None; fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # list) start = Some res\<rbrakk> \<Longrightarrow> start \<noteq> None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) [] start = Some res
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) [] start = Some res

goal (1 subgoal):
 1. start \<noteq> None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
start \<noteq> None

goal (1 subgoal):
 1. \<And>a list start res. \<lbrakk>\<And>start res. fold (\<lambda>(x, y) option. Option.bind option (f x y)) list start = Some res \<Longrightarrow> start \<noteq> None; fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # list) start = Some res\<rbrakk> \<Longrightarrow> start \<noteq> None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list start res. \<lbrakk>\<And>start res. fold (\<lambda>(x, y) option. Option.bind option (f x y)) list start = Some res \<Longrightarrow> start \<noteq> None; fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # list) start = Some res\<rbrakk> \<Longrightarrow> start \<noteq> None
[PROOF STEP]
case (Cons a list)
[PROOF STATE]
proof (state)
this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) list ?start = Some ?res \<Longrightarrow> ?start \<noteq> None
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (a # list) start = Some res

goal (1 subgoal):
 1. \<And>a list start res. \<lbrakk>\<And>start res. fold (\<lambda>(x, y) option. Option.bind option (f x y)) list start = Some res \<Longrightarrow> start \<noteq> None; fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # list) start = Some res\<rbrakk> \<Longrightarrow> start \<noteq> None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) list ?start = Some ?res \<Longrightarrow> ?start \<noteq> None
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (a # list) start = Some res
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) list ?start = Some ?res \<Longrightarrow> ?start \<noteq> None
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (a # list) start = Some res

goal (1 subgoal):
 1. start \<noteq> None
[PROOF STEP]
by (fastforce split: option.splits if_splits prod.splits simp add: bind_eq_Some_conv)
[PROOF STATE]
proof (state)
this:
start \<noteq> None

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fold_Option_bind_eq_None_start_None:
  "fold (\<lambda>(x,y) option . Option.bind option (f x y)) list None = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (\<lambda>(x, y) option. Option.bind option (f x y)) list None = None
[PROOF STEP]
by (induction list) (auto split: option.splits if_splits prod.splits)


[STATEMENT]
lemma fold_Option_bind_at_some_point_None_eq_None:
  "fold (\<lambda>(x,y) option . Option.bind option (f x y)) l1 start = None \<Longrightarrow>
  fold (\<lambda>(x,y) option . Option.bind option (f x y)) (l1@l2) start = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = None \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = None
[PROOF STEP]
proof (induction l1 arbitrary: start  l2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>start l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) [] start = None \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) ([] @ l2) start = None
 2. \<And>a l1 start l2. \<lbrakk>\<And>start l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = None \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = None; fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # l1) start = None\<rbrakk> \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) ((a # l1) @ l2) start = None
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) [] start = None

goal (2 subgoals):
 1. \<And>start l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) [] start = None \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) ([] @ l2) start = None
 2. \<And>a l1 start l2. \<lbrakk>\<And>start l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = None \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = None; fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # l1) start = None\<rbrakk> \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) ((a # l1) @ l2) start = None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) [] start = None
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) [] start = None

goal (1 subgoal):
 1. fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ([] @ l2) start = None
[PROOF STEP]
using fold_Option_bind_eq_Some_start_not_None'
[PROOF STATE]
proof (prove)
using this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) [] start = None
fold (\<lambda>(x, y) option. Option.bind option (?f x y)) ?list ?start = Some ?res \<Longrightarrow> ?start \<noteq> None

goal (1 subgoal):
 1. fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ([] @ l2) start = None
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ([] @ l2) start = None

goal (1 subgoal):
 1. \<And>a l1 start l2. \<lbrakk>\<And>start l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = None \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = None; fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # l1) start = None\<rbrakk> \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) ((a # l1) @ l2) start = None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l1 start l2. \<lbrakk>\<And>start l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = None \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = None; fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # l1) start = None\<rbrakk> \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) ((a # l1) @ l2) start = None
[PROOF STEP]
case (Cons a l1)
[PROOF STATE]
proof (state)
this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) l1 ?start = None \<Longrightarrow> fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (l1 @ ?l2.0) ?start = None
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (a # l1) start = None

goal (1 subgoal):
 1. \<And>a l1 start l2. \<lbrakk>\<And>start l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = None \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = None; fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # l1) start = None\<rbrakk> \<Longrightarrow> fold (\<lambda>(x, y) option. Option.bind option (f x y)) ((a # l1) @ l2) start = None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) l1 ?start = None \<Longrightarrow> fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (l1 @ ?l2.0) ?start = None
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (a # l1) start = None
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) l1 ?start = None \<Longrightarrow> fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (l1 @ ?l2.0) ?start = None
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (a # l1) start = None

goal (1 subgoal):
 1. fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ((a # l1) @ l2) start = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ((a # l1) @ l2) start = None

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fold_Option_bind_eq_Some_at_each_point_Some:
  "fold (\<lambda>(x,y) option . Option.bind option (f x y)) (l1@l2) start = Some res
  \<Longrightarrow> (\<exists>point . fold (\<lambda>(x,y) option . Option.bind option (f x y)) l1 start = Some point
    \<and> fold (\<lambda>(x,y) option . Option.bind option (f x y)) l2 (Some point) = Some res)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = Some res \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res
[PROOF STEP]
proof (induction l1 arbitrary: start res l2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>start res l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) ([] @ l2) start = Some res \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) [] start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res
 2. \<And>a l1 start res l2. \<lbrakk>\<And>start res l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = Some res \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res; fold (\<lambda>(x, y) option. Option.bind option (f x y)) ((a # l1) @ l2) start = Some res\<rbrakk> \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # l1) start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ([] @ l2) start = Some res

goal (2 subgoals):
 1. \<And>start res l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) ([] @ l2) start = Some res \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) [] start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res
 2. \<And>a l1 start res l2. \<lbrakk>\<And>start res l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = Some res \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res; fold (\<lambda>(x, y) option. Option.bind option (f x y)) ((a # l1) @ l2) start = Some res\<rbrakk> \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # l1) start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ([] @ l2) start = Some res
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ([] @ l2) start = Some res

goal (1 subgoal):
 1. \<exists>point. fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) [] start = Some point \<and> fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) l2 (Some point) = Some res
[PROOF STEP]
using fold_Option_bind_eq_Some_start_not_None'
[PROOF STATE]
proof (prove)
using this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ([] @ l2) start = Some res
fold (\<lambda>(x, y) option. Option.bind option (?f x y)) ?list ?start = Some ?res \<Longrightarrow> ?start \<noteq> None

goal (1 subgoal):
 1. \<exists>point. fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) [] start = Some point \<and> fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) l2 (Some point) = Some res
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>point. fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) [] start = Some point \<and> fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) l2 (Some point) = Some res

goal (1 subgoal):
 1. \<And>a l1 start res l2. \<lbrakk>\<And>start res l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = Some res \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res; fold (\<lambda>(x, y) option. Option.bind option (f x y)) ((a # l1) @ l2) start = Some res\<rbrakk> \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # l1) start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l1 start res l2. \<lbrakk>\<And>start res l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = Some res \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res; fold (\<lambda>(x, y) option. Option.bind option (f x y)) ((a # l1) @ l2) start = Some res\<rbrakk> \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # l1) start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res
[PROOF STEP]
case (Cons a l1)
[PROOF STATE]
proof (state)
this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (l1 @ ?l2.0) ?start = Some ?res \<Longrightarrow> \<exists>point. fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) l1 ?start = Some point \<and> fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ?l2.0 (Some point) = Some ?res
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ((a # l1) @ l2) start = Some res

goal (1 subgoal):
 1. \<And>a l1 start res l2. \<lbrakk>\<And>start res l2. fold (\<lambda>(x, y) option. Option.bind option (f x y)) (l1 @ l2) start = Some res \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) l1 start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res; fold (\<lambda>(x, y) option. Option.bind option (f x y)) ((a # l1) @ l2) start = Some res\<rbrakk> \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (f x y)) (a # l1) start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (f x y)) l2 (Some point) = Some res
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (l1 @ ?l2.0) ?start = Some ?res \<Longrightarrow> \<exists>point. fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) l1 ?start = Some point \<and> fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ?l2.0 (Some point) = Some ?res
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ((a # l1) @ l2) start = Some res
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (l1 @ ?l2.0) ?start = Some ?res \<Longrightarrow> \<exists>point. fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) l1 ?start = Some point \<and> fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ?l2.0 (Some point) = Some ?res
fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) ((a # l1) @ l2) start = Some res

goal (1 subgoal):
 1. \<exists>point. fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (a # l1) start = Some point \<and> fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) l2 (Some point) = Some res
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>point. fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) (a # l1) start = Some point \<and> fold (\<lambda>a. case a of (x, y) \<Rightarrow> \<lambda>option. Option.bind option (f x y)) l2 (Some point) = Some res

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fold_Option_bind_eq_Some_at_each_point_Some':
  assumes "fold (\<lambda>(x,y) option . Option.bind option (f x y)) (xs@ys) start = Some res"
  obtains point where
    "fold (\<lambda>(x,y) option . Option.bind option (f x y)) xs start = Some point" and
    "fold (\<lambda>(x,y) option . Option.bind option (f x y)) ys (Some point) = Some res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>point. \<lbrakk>fold (\<lambda>(x, y) option. Option.bind option (f x y)) xs start = Some point; fold (\<lambda>(x, y) option. Option.bind option (f x y)) ys (Some point) = Some res\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms fold_Option_bind_eq_Some_at_each_point_Some
[PROOF STATE]
proof (prove)
using this:
fold (\<lambda>(x, y) option. Option.bind option (f x y)) (xs @ ys) start = Some res
fold (\<lambda>(x, y) option. Option.bind option (?f x y)) (?l1.0 @ ?l2.0) ?start = Some ?res \<Longrightarrow> \<exists>point. fold (\<lambda>(x, y) option. Option.bind option (?f x y)) ?l1.0 ?start = Some point \<and> fold (\<lambda>(x, y) option. Option.bind option (?f x y)) ?l2.0 (Some point) = Some ?res

goal (1 subgoal):
 1. (\<And>point. \<lbrakk>fold (\<lambda>(x, y) option. Option.bind option (f x y)) xs start = Some point; fold (\<lambda>(x, y) option. Option.bind option (f x y)) ys (Some point) = Some res\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast


[STATEMENT]
lemma fold_matches_first_step_not_None:
  assumes
    "fold (\<lambda>(T, U) subs . Option.bind subs (f T U)) (zip (x#xs) (y#ys)) (Some subs) = Some subs'"
  obtains point where
    "f x y subs = Some point"
    "fold (\<lambda>(T, U) subs . Option.bind subs (f T U)) (zip (xs) (ys)) (Some point) = Some subs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>point. \<lbrakk>f x y subs = Some point; fold (\<lambda>(T, U) subs. Option.bind subs (f T U)) (zip xs ys) (Some point) = Some subs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms fold_Option_bind_eq_Some_start_not_None' not_None_eq
[PROOF STATE]
proof (prove)
using this:
fold (\<lambda>(T, U) subs. Option.bind subs (f T U)) (zip (x # xs) (y # ys)) (Some subs) = Some subs'
fold (\<lambda>(x, y) option. Option.bind option (?f x y)) ?list ?start = Some ?res \<Longrightarrow> ?start \<noteq> None
(?x \<noteq> None) = (\<exists>y. ?x = Some y)

goal (1 subgoal):
 1. (\<And>point. \<lbrakk>f x y subs = Some point; fold (\<lambda>(T, U) subs. Option.bind subs (f T U)) (zip xs ys) (Some point) = Some subs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce


[STATEMENT]
lemma fold_matches_last_step_not_None:
  assumes
    "length xs = length ys"
    "fold (\<lambda>(T, U) subs . Option.bind subs (f T U)) (zip (xs@[x]) (ys@[y])) (Some subs) = Some subs'"
  obtains point where
    "fold (\<lambda>(T, U) subs . Option.bind subs (f T U)) (zip (xs) (ys)) (Some subs) = Some point"
    "f x y point = Some subs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>point. \<lbrakk>fold (\<lambda>(T, U) subs. Option.bind subs (f T U)) (zip xs ys) (Some subs) = Some point; f x y point = Some subs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms fold_Option_bind_eq_Some_at_each_point_Some'[where xs="zip xs ys" and ys="[(x,y)]"
      and start="Some subs" and res="subs'" and f="f"]
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
fold (\<lambda>(T, U) subs. Option.bind subs (f T U)) (zip (xs @ [x]) (ys @ [y])) (Some subs) = Some subs'
\<lbrakk>fold (\<lambda>(x, y) option. Option.bind option (f x y)) (zip xs ys @ [(x, y)]) (Some subs) = Some subs'; \<And>point. \<lbrakk>fold (\<lambda>(x, y) option. Option.bind option (f x y)) (zip xs ys) (Some subs) = Some point; fold (\<lambda>(x, y) option. Option.bind option (f x y)) [(x, y)] (Some point) = Some subs'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>point. \<lbrakk>fold (\<lambda>(T, U) subs. Option.bind subs (f T U)) (zip xs ys) (Some subs) = Some point; f x y point = Some subs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma BenOr_trans:
  "CSHO_trans_alt BenOr_sendMsg (\<lambda>r p st msgs crd st'. BenOr_nextState r p st msgs st') HOs SHOs crds =
  BenOr_trans_step HOs SHOs next0 send0 0
  \<union> BenOr_trans_step HOs SHOs  next1 send1 1
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CSHO_trans_alt BenOr_sendMsg (\<lambda>r p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds = BenOr_trans_step HOs SHOs next0 send0 0 \<union> BenOr_trans_step HOs SHOs next1 send1 1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. CSHO_trans_alt BenOr_sendMsg (\<lambda>r p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds \<subseteq> BenOr_trans_step HOs SHOs next0 send0 0 \<union> BenOr_trans_step HOs SHOs next1 send1 1
 2. BenOr_trans_step HOs SHOs next0 send0 0 \<union> BenOr_trans_step HOs SHOs next1 send1 1 \<subseteq> CSHO_trans_alt BenOr_sendMsg (\<lambda>r p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds
[PROOF STEP]
show "CSHO_trans_alt BenOr_sendMsg (\<lambda>r p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds
    \<subseteq> BenOr_trans_step HOs SHOs next0 send0 0 \<union> BenOr_trans_step HOs SHOs next1 send1 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CSHO_trans_alt BenOr_sendMsg (\<lambda>r p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds \<subseteq> BenOr_trans_step HOs SHOs next0 send0 0 \<union> BenOr_trans_step HOs SHOs next1 send1 1
[PROOF STEP]
by(force simp add: CSHO_trans_alt_def BenOr_sendMsg_def BenOr_nextState_def BenOr_trans_step_def
    K_def dest!: two_step_less_D)
[PROOF STATE]
proof (state)
this:
CSHO_trans_alt BenOr_sendMsg (\<lambda>r p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds \<subseteq> BenOr_trans_step HOs SHOs next0 send0 0 \<union> BenOr_trans_step HOs SHOs next1 send1 1

goal (1 subgoal):
 1. BenOr_trans_step HOs SHOs next0 send0 0 \<union> BenOr_trans_step HOs SHOs next1 send1 1 \<subseteq> CSHO_trans_alt BenOr_sendMsg (\<lambda>r p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. BenOr_trans_step HOs SHOs next0 send0 0 \<union> BenOr_trans_step HOs SHOs next1 send1 1 \<subseteq> CSHO_trans_alt BenOr_sendMsg (\<lambda>r p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds
[PROOF STEP]
show " BenOr_trans_step HOs SHOs next0 send0 0 \<union>
    BenOr_trans_step HOs SHOs next1 send1 1
    \<subseteq> CSHO_trans_alt BenOr_sendMsg
        (\<lambda>r p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BenOr_trans_step HOs SHOs next0 send0 0 \<union> BenOr_trans_step HOs SHOs next1 send1 1 \<subseteq> CSHO_trans_alt BenOr_sendMsg (\<lambda>r p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds
[PROOF STEP]
by(force simp add: CSHO_trans_alt_def BenOr_sendMsg_def BenOr_nextState_def BenOr_trans_step_def)
[PROOF STATE]
proof (state)
this:
BenOr_trans_step HOs SHOs next0 send0 0 \<union> BenOr_trans_step HOs SHOs next1 send1 1 \<subseteq> CSHO_trans_alt BenOr_sendMsg (\<lambda>r p st msgs crd. BenOr_nextState r p st msgs) HOs SHOs crds

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HOs_intersect:
  "HOs r p \<inter> HOs r' q \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOs r p \<inter> HOs r' q \<noteq> {}
[PROOF STEP]
using per_rd
[PROOF STATE]
proof (prove)
using this:
\<forall>r. BenOr_commPerRd (HOs r)

goal (1 subgoal):
 1. HOs r p \<inter> HOs r' q \<noteq> {}
[PROOF STEP]
apply(simp add: BenOr_commPerRd_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r p. HOs r p \<in> Quorum \<Longrightarrow> HOs r p \<inter> HOs r' q \<noteq> {}
[PROOF STEP]
apply(blast dest: qintersect)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma HOs_nonempty:
  "HOs r p \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HOs r p \<noteq> {}
[PROOF STEP]
using HOs_intersect
[PROOF STATE]
proof (prove)
using this:
HOs ?r ?p \<inter> HOs ?r' ?q \<noteq> {}

goal (1 subgoal):
 1. HOs r p \<noteq> {}
[PROOF STEP]
by blast


[STATEMENT]
lemma vote_origin:
  assumes
  send: "\<forall>p. \<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "\<forall>p. next0 r p (cfg p) (\<mu> p) (cfg' p)"
  and step_r: "two_step r = 0"
  shows
    "vote (cfg' p) = Some v \<longleftrightarrow> (\<forall>q \<in> HOs r p. x (cfg q) = v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vote (cfg' p) = Some v) = (\<forall>q\<in>HOs r p. x (cfg q) = v)
[PROOF STEP]
using send[THEN spec, where x=p] step[THEN spec, where x=p] step_r HOs_nonempty
[PROOF STATE]
proof (prove)
using this:
\<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p
next0 r p (cfg p) (\<mu> p) (cfg' p)
two_step r = 0
HOs ?r ?p \<noteq> {}

goal (1 subgoal):
 1. (vote (cfg' p) = Some v) = (\<forall>q\<in>HOs r p. x (cfg q) = v)
[PROOF STEP]
by(auto simp add: next0_def get_msgs_benign send0_def msgRcvd_def o_def restrict_map_def)


[STATEMENT]
lemma same_new_vote:
  assumes
  send: "\<forall>p. \<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "\<forall>p. next0 r p (cfg p) (\<mu> p) (cfg' p)"
  and step_r: "two_step r = 0"
  obtains v where "\<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(cases "\<exists>p v. vote (cfg' p) = Some v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis; \<exists>p v. vote (cfg' p) = Some v\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis; \<nexists>p v. vote (cfg' p) = Some v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>p v. vote (cfg' p) = Some v

goal (2 subgoals):
 1. \<lbrakk>\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis; \<exists>p v. vote (cfg' p) = Some v\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis; \<nexists>p v. vote (cfg' p) = Some v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume asm: "\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
\<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = ?v2 \<Longrightarrow> thesis

goal (2 subgoals):
 1. \<lbrakk>\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis; \<exists>p v. vote (cfg' p) = Some v\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis; \<nexists>p v. vote (cfg' p) = Some v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
\<exists>p v. vote (cfg' p) = Some v
[PROOF STEP]
obtain p v where "vote (cfg' p) = Some v"
[PROOF STATE]
proof (prove)
using this:
\<exists>p v. vote (cfg' p) = Some v

goal (1 subgoal):
 1. (\<And>p v. vote (cfg' p) = Some v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vote (cfg' p) = Some v

goal (2 subgoals):
 1. \<lbrakk>\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis; \<exists>p v. vote (cfg' p) = Some v\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis; \<nexists>p v. vote (cfg' p) = Some v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "\<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v" (is "?LV(v)")
[PROOF STATE]
proof (prove)
using this:
vote (cfg' p) = Some v

goal (1 subgoal):
 1. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v
[PROOF STEP]
using vote_origin[OF send step step_r] HOs_intersect
[PROOF STATE]
proof (prove)
using this:
vote (cfg' p) = Some v
(vote (cfg' ?p) = Some ?v) = (\<forall>q\<in>HOs r ?p. x (cfg q) = ?v)
HOs ?r ?p \<inter> HOs ?r' ?q \<noteq> {}

goal (1 subgoal):
 1. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v
[PROOF STEP]
by(force)
[PROOF STATE]
proof (state)
this:
\<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v

goal (2 subgoals):
 1. \<lbrakk>\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis; \<exists>p v. vote (cfg' p) = Some v\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis; \<nexists>p v. vote (cfg' p) = Some v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from asm[OF this]
[PROOF STATE]
proof (chain)
picking this:
thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> thesis; \<nexists>p v. vote (cfg' p) = Some v\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
qed(auto)


[STATEMENT]
lemma no_x_change:
  assumes
  send: "\<forall>p. \<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "\<forall>p. next0 r p (cfg p) (\<mu> p) (cfg' p)"
  and step_r: "two_step r = 0"
  shows
    "x (cfg' p) = x (cfg p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x (cfg' p) = x (cfg p)
[PROOF STEP]
using send[THEN spec, where x=p] step[THEN spec, where x=p] step_r HOs_nonempty
[PROOF STATE]
proof (prove)
using this:
\<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p
next0 r p (cfg p) (\<mu> p) (cfg' p)
two_step r = 0
HOs ?r ?p \<noteq> {}

goal (1 subgoal):
 1. x (cfg' p) = x (cfg p)
[PROOF STEP]
by(auto simp add: next0_def get_msgs_benign send0_def msgRcvd_def o_def restrict_map_def)


[STATEMENT]
lemma no_vote:
  assumes
  send: "\<forall>p. \<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p"
  and step: "\<forall>p. next0 r p (cfg p) (\<mu> p) (cfg' p)"
  and step_r: "two_step r = 0"
  shows
    "no_vote_diff cfg' p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_vote_diff cfg' p
[PROOF STEP]
unfolding no_vote_diff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vote (cfg' p) = None \<longrightarrow> (\<exists>q q'. x (cfg' q) \<noteq> x (cfg' q'))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vote (cfg' p) = None \<Longrightarrow> \<exists>q q'. x (cfg' q) \<noteq> x (cfg' q')
[PROOF STEP]
assume
    "vote (cfg' p) = None"
[PROOF STATE]
proof (state)
this:
vote (cfg' p) = None

goal (1 subgoal):
 1. vote (cfg' p) = None \<Longrightarrow> \<exists>q q'. x (cfg' q) \<noteq> x (cfg' q')
[PROOF STEP]
hence "(\<exists>q q'. x (cfg q) \<noteq> x (cfg q'))"
[PROOF STATE]
proof (prove)
using this:
vote (cfg' p) = None

goal (1 subgoal):
 1. \<exists>q q'. x (cfg q) \<noteq> x (cfg q')
[PROOF STEP]
using send[THEN spec, where x=p] step[THEN spec, where x=p] step_r HOs_nonempty
[PROOF STATE]
proof (prove)
using this:
vote (cfg' p) = None
\<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p
next0 r p (cfg p) (\<mu> p) (cfg' p)
two_step r = 0
HOs ?r ?p \<noteq> {}

goal (1 subgoal):
 1. \<exists>q q'. x (cfg q) \<noteq> x (cfg q')
[PROOF STEP]
apply(clarsimp simp add: next0_def get_msgs_benign send0_def msgRcvd_def o_def restrict_map_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>v. \<exists>q. (q \<in> HOs r p \<longrightarrow> x (cfg q) \<noteq> v) \<and> q \<in> HOs r p; \<mu> p = (\<lambda>xa. if xa \<in> HOs r p then Some (Val (x (cfg xa))) else None); two_step r = 0; \<And>r p. HOs r p \<noteq> {}; cfg' p = vote_update Map.empty (cfg p)\<rbrakk> \<Longrightarrow> \<exists>q q'. x (cfg q) \<noteq> x (cfg q')
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>q q'. x (cfg q) \<noteq> x (cfg q')

goal (1 subgoal):
 1. vote (cfg' p) = None \<Longrightarrow> \<exists>q q'. x (cfg' q) \<noteq> x (cfg' q')
[PROOF STEP]
thus "(\<exists>q q'. x (cfg' q) \<noteq> x (cfg' q'))"
[PROOF STATE]
proof (prove)
using this:
\<exists>q q'. x (cfg q) \<noteq> x (cfg q')

goal (1 subgoal):
 1. \<exists>q q'. x (cfg' q) \<noteq> x (cfg' q')
[PROOF STEP]
using no_x_change[OF send step step_r]
[PROOF STATE]
proof (prove)
using this:
\<exists>q q'. x (cfg q) \<noteq> x (cfg q')
x (cfg' ?p) = x (cfg ?p)

goal (1 subgoal):
 1. \<exists>q q'. x (cfg' q) \<noteq> x (cfg' q')
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
\<exists>q q'. x (cfg' q) \<noteq> x (cfg' q')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step0_ref:
  "{ref_rel} \<Union>r S v. tso_round0 r S v,
    BenOr_trans_step HOs HOs next0 send0 0 {> ref_rel}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ref_rel} \<Union>r S. \<Union> (range (tso_round0 r S)), BenOr_trans_step HOs HOs next0 send0 0 {> ref_rel}
[PROOF STEP]
proof(clarsimp simp add: PO_rhoare_defs BenOr_trans_step_def all_conj_distrib)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
fix sa r cfg \<mu> cfg'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
assume
    R: "(sa, (r, cfg)) \<in> ref_rel"
    and step_r: "two_step r = 0"
    and send: "\<forall>p. \<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p"
    and step: "\<forall>p. next0 r p (cfg p) (\<mu> p) (cfg' p)"
[PROOF STATE]
proof (state)
this:
(sa, r, cfg) \<in> ref_rel
two_step r = 0
\<forall>p. \<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p
\<forall>p. next0 r p (cfg p) (\<mu> p) (cfg' p)

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
from R
[PROOF STATE]
proof (chain)
picking this:
(sa, r, cfg) \<in> ref_rel
[PROOF STEP]
have next_r: "next_round sa = r"
[PROOF STATE]
proof (prove)
using this:
(sa, r, cfg) \<in> ref_rel

goal (1 subgoal):
 1. opt_obsv_state.next_round sa = r
[PROOF STEP]
by(simp add: ref_rel_def)
[PROOF STATE]
proof (state)
this:
opt_obsv_state.next_round sa = r

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
from HOs_nonempty send
[PROOF STATE]
proof (chain)
picking this:
HOs ?r ?p \<noteq> {}
\<forall>p. \<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p
[PROOF STEP]
have "\<forall>p. \<exists>q. q \<in> msgRcvd (\<mu> p)"
[PROOF STATE]
proof (prove)
using this:
HOs ?r ?p \<noteq> {}
\<forall>p. \<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p

goal (1 subgoal):
 1. \<forall>p. \<exists>q. q \<in> msgRcvd (\<mu> p)
[PROOF STEP]
by(fastforce simp add: get_msgs_benign send0_def msgRcvd_def restrict_map_def)
[PROOF STATE]
proof (state)
this:
\<forall>p. \<exists>q. q \<in> msgRcvd (\<mu> p)

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
with step
[PROOF STATE]
proof (chain)
picking this:
\<forall>p. next0 r p (cfg p) (\<mu> p) (cfg' p)
\<forall>p. \<exists>q. q \<in> msgRcvd (\<mu> p)
[PROOF STEP]
have same_dec: "decide o cfg' = decide o cfg"
[PROOF STATE]
proof (prove)
using this:
\<forall>p. next0 r p (cfg p) (\<mu> p) (cfg' p)
\<forall>p. \<exists>q. q \<in> msgRcvd (\<mu> p)

goal (1 subgoal):
 1. decide \<circ> cfg' = decide \<circ> cfg
[PROOF STEP]
apply(simp add: next0_def o_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. (\<exists>v. (\<forall>q\<in>msgRcvd (\<mu> p). \<mu> p q = Some (Val v)) \<and> cfg' p = cfg p\<lparr>vote := Some v\<rparr>) \<or> (\<forall>v. \<exists>q\<in>msgRcvd (\<mu> p). \<mu> p q \<noteq> Some (Val v)) \<and> cfg' p = vote_update Map.empty (cfg p); \<forall>p. \<exists>q. q \<in> msgRcvd (\<mu> p)\<rbrakk> \<Longrightarrow> (\<lambda>x. decide (cfg' x)) = (\<lambda>x. decide (cfg x))
[PROOF STEP]
by (metis pstate.select_convs(3) pstate.surjective pstate.update_convs(2))
[PROOF STATE]
proof (state)
this:
decide \<circ> cfg' = decide \<circ> cfg

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
define S where "S = {p. \<exists>v. vote (cfg' p) = Some v}"
[PROOF STATE]
proof (state)
this:
S = {p. \<exists>v. vote (cfg' p) = Some v}

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
from same_new_vote[OF send step step_r]
[PROOF STATE]
proof (chain)
picking this:
(\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain v where v: "\<forall>p \<in> S. vote (cfg' p) = Some v"
[PROOF STATE]
proof (prove)
using this:
(\<And>v. \<forall>p w. vote (cfg' p) = Some w \<longrightarrow> w = v \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>v. \<forall>p\<in>S. vote (cfg' p) = Some v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(simp add: S_def) (metis)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>S. vote (cfg' p) = Some v

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
hence vote_const_map: "vote o cfg' = const_map v S"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>S. vote (cfg' p) = Some v

goal (1 subgoal):
 1. vote \<circ> cfg' = const_map v S
[PROOF STEP]
by(auto simp add: S_def const_map_def restrict_map_def intro!: ext)
[PROOF STATE]
proof (state)
this:
vote \<circ> cfg' = const_map v S

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
define sa' where "sa' = sa\<lparr> next_round := Suc r, r_votes := const_map v S \<rparr>"
[PROOF STATE]
proof (state)
this:
sa' = sa\<lparr>opt_obsv_state.next_round := Suc r, r_votes := const_map v S\<rparr>

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
have "\<forall>p. p \<in> S \<longrightarrow> opt_obs_safe (last_obs sa) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. p \<in> S \<longrightarrow> opt_obs_safe (last_obs sa) v
[PROOF STEP]
using vote_origin[OF send step step_r] R per_rd[THEN spec, of r] v
[PROOF STATE]
proof (prove)
using this:
(vote (cfg' ?p) = Some ?v) = (\<forall>q\<in>HOs r ?p. x (cfg q) = ?v)
(sa, r, cfg) \<in> ref_rel
BenOr_commPerRd (HOs r)
\<forall>p\<in>S. vote (cfg' p) = Some v

goal (1 subgoal):
 1. \<forall>p. p \<in> S \<longrightarrow> opt_obs_safe (last_obs sa) v
[PROOF STEP]
apply(clarsimp simp add: BenOr_commPerRd_def opt_obs_safe_def ref_rel_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<And>p v. (vote (cfg' p) = Some v) = (\<forall>q\<in>HOs (opt_obsv_state.next_round sa) p. x (cfg q) = v); \<forall>p. HOs (opt_obsv_state.next_round sa) p \<in> Quorum; \<forall>p\<in>S. \<forall>q\<in>HOs (opt_obsv_state.next_round sa) p. x (cfg q) = v; r = opt_obsv_state.next_round sa; two_step (opt_obsv_state.next_round sa) = Suc 0 \<longrightarrow> r_votes sa = vote \<circ> cfg; two_step (opt_obsv_state.next_round sa) = Suc 0 \<longrightarrow> All (no_vote_diff cfg); \<forall>p. \<exists>q. last_obs sa q = None \<or> last_obs sa q = Some (x (cfg p)); opt_obsv_state.decisions sa = decide \<circ> cfg; p \<in> S\<rbrakk> \<Longrightarrow> \<exists>p. last_obs sa p = None \<or> last_obs sa p = Some v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>p. p \<in> S \<longrightarrow> opt_obs_safe (last_obs sa) v

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
hence "(sa, sa') \<in> tso_round0 r S v"
[PROOF STATE]
proof (prove)
using this:
\<forall>p. p \<in> S \<longrightarrow> opt_obs_safe (last_obs sa) v

goal (1 subgoal):
 1. (sa, sa') \<in> tso_round0 r S v
[PROOF STEP]
using next_r step_r v R
    vote_origin[OF send step step_r]
[PROOF STATE]
proof (prove)
using this:
\<forall>p. p \<in> S \<longrightarrow> opt_obs_safe (last_obs sa) v
opt_obsv_state.next_round sa = r
two_step r = 0
\<forall>p\<in>S. vote (cfg' p) = Some v
(sa, r, cfg) \<in> ref_rel
(vote (cfg' ?p) = Some ?v) = (\<forall>q\<in>HOs r ?p. x (cfg q) = ?v)

goal (1 subgoal):
 1. (sa, sa') \<in> tso_round0 r S v
[PROOF STEP]
by(auto simp add: tso_round0_def sa'_def all_conj_distrib)
[PROOF STATE]
proof (state)
this:
(sa, sa') \<in> tso_round0 r S v

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(sa, sa') \<in> tso_round0 r S v

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
have "(sa', Suc r, cfg') \<in> ref_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sa', Suc r, cfg') \<in> ref_rel
[PROOF STEP]
using step send v R same_dec step_r next_r
[PROOF STATE]
proof (prove)
using this:
\<forall>p. next0 r p (cfg p) (\<mu> p) (cfg' p)
\<forall>p. \<mu> p \<in> get_msgs (send0 r) cfg (HOs r) (HOs r) p
\<forall>p\<in>S. vote (cfg' p) = Some v
(sa, r, cfg) \<in> ref_rel
decide \<circ> cfg' = decide \<circ> cfg
two_step r = 0
opt_obsv_state.next_round sa = r

goal (1 subgoal):
 1. (sa', Suc r, cfg') \<in> ref_rel
[PROOF STEP]
apply(auto simp add: ref_rel_def sa'_def  two_step_phase_Suc vote_const_map next0_def
      all_conj_distrib no_vote[OF send step step_r])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p. (\<exists>v. (\<forall>q\<in>msgRcvd (\<mu> p). \<mu> p q = Some (Val v)) \<and> cfg' p = cfg p\<lparr>vote := Some v\<rparr>) \<or> (\<forall>v. \<exists>q\<in>msgRcvd (\<mu> p). \<mu> p q \<noteq> Some (Val v)) \<and> cfg' p = vote_update Map.empty (cfg p); \<forall>p. \<mu> p \<in> get_msgs (send0 (opt_obsv_state.next_round sa)) cfg (HOs (opt_obsv_state.next_round sa)) (HOs (opt_obsv_state.next_round sa)) p; \<forall>p\<in>S. vote (cfg' p) = Some v; decide \<circ> cfg' = decide \<circ> cfg; two_step (opt_obsv_state.next_round sa) = 0; r = opt_obsv_state.next_round sa; \<forall>p. \<exists>q. last_obs sa q = None \<or> last_obs sa q = Some (x (cfg p)); opt_obsv_state.decisions sa = decide \<circ> cfg\<rbrakk> \<Longrightarrow> \<exists>q. last_obs sa q = None \<or> last_obs sa q = Some (x (cfg' p))
[PROOF STEP]
by (metis pstate.select_convs(1) pstate.surjective pstate.update_convs(2))
[PROOF STATE]
proof (state)
this:
(sa', Suc r, cfg') \<in> ref_rel

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; two_step ab = 0; \<forall>p. x p \<in> get_msgs (send0 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next0 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round0 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(sa, sa') \<in> tso_round0 r S v
(sa', Suc r, cfg') \<in> ref_rel
[PROOF STEP]
show
    "\<exists>sa'. (\<exists>r S v. (sa, sa') \<in> tso_round0 r S v) \<and> (sa', Suc r, cfg') \<in> ref_rel"
[PROOF STATE]
proof (prove)
using this:
(sa, sa') \<in> tso_round0 r S v
(sa', Suc r, cfg') \<in> ref_rel

goal (1 subgoal):
 1. \<exists>sa'. (\<exists>r S v. (sa, sa') \<in> tso_round0 r S v) \<and> (sa', Suc r, cfg') \<in> ref_rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>sa'. (\<exists>r S v. (sa, sa') \<in> tso_round0 r S v) \<and> (sa', Suc r, cfg') \<in> ref_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma decide_origin:
  assumes
  send: "\<forall>p. \<mu> p \<in> get_msgs (send1 r) cfg (HOs r) (HOs r) p"
  and step: "\<forall>p. next1 r p (cfg p) (\<mu> p) (cfg' p)"
  and step_r: "two_step r = Suc 0"
  shows
    "D cfg cfg' \<subseteq> {p. \<exists>v. decide (cfg' p) = Some v \<and> (\<forall>q \<in> HOs r p. vote (cfg q) = Some v)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D cfg cfg' \<subseteq> {p. \<exists>v. decide (cfg' p) = Some v \<and> (\<forall>q\<in>HOs r p. vote (cfg q) = Some v)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>p. \<mu> p \<in> get_msgs (send1 r) cfg (HOs r) (HOs r) p
\<forall>p. next1 r p (cfg p) (\<mu> p) (cfg' p)
two_step r = Suc 0

goal (1 subgoal):
 1. D cfg cfg' \<subseteq> {p. \<exists>v. decide (cfg' p) = Some v \<and> (\<forall>q\<in>HOs r p. vote (cfg q) = Some v)}
[PROOF STEP]
by(fastforce simp add: D_def next1_def get_msgs_benign send1_def msgRcvd_def o_def restrict_map_def
    x_update_def dec_update_def identicalVoteRcvd_def all_conj_distrib someVoteRcvd_def isVote_def)


[STATEMENT]
lemma BenOr_Refines_Two_Step_Obs:
  "PO_refines (ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV)
    tso_TS (BenOr_TS HOs HOs crds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PO_refines (ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV) tso_TS (BenOr_TS HOs HOs crds)
[PROOF STEP]
proof(rule refine_using_invariants)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. {ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV} TS.trans tso_TS, TS.trans (BenOr_TS HOs HOs crds) {> ref_rel}
 2. {TSO_inv1 \<inter> TSO_inv2 \<inter> Domain (ref_rel \<inter> UNIV \<times> UNIV)} TS.trans tso_TS {> TSO_inv1 \<inter> TSO_inv2}
 3. {UNIV \<inter> Range (ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV)} TS.trans (BenOr_TS HOs HOs crds) {> UNIV}
 4. init (BenOr_TS HOs HOs crds) \<subseteq> ref_rel `` init tso_TS
 5. init tso_TS \<subseteq> TSO_inv1 \<inter> TSO_inv2
 6. init (BenOr_TS HOs HOs crds) \<subseteq> UNIV
[PROOF STEP]
show "init (BenOr_TS HOs HOs crds) \<subseteq> ref_rel `` init tso_TS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init (BenOr_TS HOs HOs crds) \<subseteq> ref_rel `` init tso_TS
[PROOF STEP]
by(auto simp add: BenOr_TS_defs BenOr_HOMachine_def CHOAlgorithm.truncate_def
      tso_TS_defs ref_rel_def tso_init_def Let_def o_def)
[PROOF STATE]
proof (state)
this:
init (BenOr_TS HOs HOs crds) \<subseteq> ref_rel `` init tso_TS

goal (5 subgoals):
 1. {ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV} TS.trans tso_TS, TS.trans (BenOr_TS HOs HOs crds) {> ref_rel}
 2. {TSO_inv1 \<inter> TSO_inv2 \<inter> Domain (ref_rel \<inter> UNIV \<times> UNIV)} TS.trans tso_TS {> TSO_inv1 \<inter> TSO_inv2}
 3. {UNIV \<inter> Range (ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV)} TS.trans (BenOr_TS HOs HOs crds) {> UNIV}
 4. init tso_TS \<subseteq> TSO_inv1 \<inter> TSO_inv2
 5. init (BenOr_TS HOs HOs crds) \<subseteq> UNIV
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. {ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV} TS.trans tso_TS, TS.trans (BenOr_TS HOs HOs crds) {> ref_rel}
 2. {TSO_inv1 \<inter> TSO_inv2 \<inter> Domain (ref_rel \<inter> UNIV \<times> UNIV)} TS.trans tso_TS {> TSO_inv1 \<inter> TSO_inv2}
 3. {UNIV \<inter> Range (ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV)} TS.trans (BenOr_TS HOs HOs crds) {> UNIV}
 4. init tso_TS \<subseteq> TSO_inv1 \<inter> TSO_inv2
 5. init (BenOr_TS HOs HOs crds) \<subseteq> UNIV
[PROOF STEP]
show
    "{ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV} TS.trans tso_TS,
      TS.trans (BenOr_TS HOs HOs crds) {> ref_rel}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV} TS.trans tso_TS, TS.trans (BenOr_TS HOs HOs crds) {> ref_rel}
[PROOF STEP]
apply(simp add: tso_TS_defs BenOr_TS_defs BenOr_HOMachine_def CHOAlgorithm.truncate_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV} ((\<Union>x xa. \<Union> (range (tso_round0 x xa))) \<union> (\<Union>x xa. \<Union> (range (tso_round1 x xa))))\<^sup>=, CHO_trans \<lparr>CinitState = \<lambda>p st crd. vote st = None \<and> decide st = None, sendMsg = BenOr_sendMsg, CnextState = \<lambda>r p st msgs crd. BenOr_nextState r p st msgs\<rparr> HOs HOs (K \<circ> crds) {> ref_rel}
[PROOF STEP]
apply(auto simp add: CHO_trans_alt BenOr_trans intro!: step0_ref step1_ref)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV} TS.trans tso_TS, TS.trans (BenOr_TS HOs HOs crds) {> ref_rel}

goal (4 subgoals):
 1. {TSO_inv1 \<inter> TSO_inv2 \<inter> Domain (ref_rel \<inter> UNIV \<times> UNIV)} TS.trans tso_TS {> TSO_inv1 \<inter> TSO_inv2}
 2. {UNIV \<inter> Range (ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV)} TS.trans (BenOr_TS HOs HOs crds) {> UNIV}
 3. init tso_TS \<subseteq> TSO_inv1 \<inter> TSO_inv2
 4. init (BenOr_TS HOs HOs crds) \<subseteq> UNIV
[PROOF STEP]
qed(auto intro!: TSO_inv1_inductive TSO_inv2_inductive)