theory Schedule_R

lemma findM_awesome':
  assumes x: "\<And>x xs. suffix (x # xs) xs' \<Longrightarrow>
                  corres (\<lambda>a b. if b then (\<exists>a'. a = Some a' \<and> r a' (Some x)) else a = None)
                      P (P' (x # xs))
                      ((f >>= (\<lambda>x. return (Some x))) \<sqinter> (return None)) (g x)"
  assumes y: "corres r P (P' []) f (return None)"
  assumes z: "\<And>x xs. suffix (x # xs) xs' \<Longrightarrow>
                 \<lbrace>P' (x # xs)\<rbrace> g x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P' xs s\<rbrace>"
  assumes p: "suffix xs xs'"
  shows      "corres r P (P' xs) f (findM g xs)" proof - have P: "f = do x \<leftarrow> (do x \<leftarrow> f; return (Some x) od) \<sqinter> return None; if x \<noteq> None then return (the x) else f od" apply (rule ext) apply (auto simp add: bind_def alternative_def return_def split_def prod_eq_iff) done have Q: "\<lbrace>P\<rbrace> (do x \<leftarrow> f; return (Some x) od) \<sqinter> return None \<lbrace>\<lambda>rv. if rv \<noteq> None then \<top> else P\<rbrace>" by (wp | simp)+ show ?thesis using p apply (induct xs) apply (simp add: y del: dc_simp) apply (simp only: findM.simps) apply (subst P) apply (rule corres_guard_imp) apply (rule corres_split[OF x]) apply assumption apply (rule corres_if2) apply (case_tac ra, clarsimp+)[1] apply (rule corres_trivial, clarsimp) apply (case_tac ra, simp_all)[1] apply (erule(1) meta_mp [OF _ suffix_ConsD]) apply (rule Q) apply (rule hoare_post_imp [OF _ z]) apply simp+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r P (P' xs) f (findM g xs) proof (state)
goal (1 subgoal):
 1. corres r P (P' xs) f (findM g xs) proof (prove)
goal (1 subgoal):
 1. f = do x <- do x <- f;
return (Some x)
od \<sqinter> return None;
if x \<noteq> None then return (the x) else f
od proof (prove)
goal (1 subgoal):
 1. \<And>x. f x = (do x <- do x <- f;
return (Some x)
od \<sqinter> return None;
if x \<noteq> None then return (the x) else f
od) x proof (prove)
goal:
No subgoals! proof (state)
this:
f = do x <- do x <- f;
return (Some x)
od \<sqinter> return None;
if x \<noteq> None then return (the x) else f
od

goal (1 subgoal):
 1. corres r P (P' xs) f (findM g xs) proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do x <- f;
return (Some x)
od \<sqinter> return None \<lbrace>\<lambda>rv. if rv \<noteq> None then \<lambda>_. True else P\<rbrace> proof (state)
this:
\<lbrace>P\<rbrace> do x <- f;
return (Some x)
od \<sqinter> return None \<lbrace>\<lambda>rv. if rv \<noteq> None then \<lambda>_. True else P\<rbrace>

goal (1 subgoal):
 1. corres r P (P' xs) f (findM g xs) proof (prove)
goal (1 subgoal):
 1. corres r P (P' xs) f (findM g xs) proof (prove)
using this:
suffix xs xs'

goal (1 subgoal):
 1. corres r P (P' xs) f (findM g xs) proof (prove)
goal (2 subgoals):
 1. suffix [] xs' \<Longrightarrow> corres r P (P' []) f (findM g [])
 2. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> corres r P (P' (a # xs)) f (findM g (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> corres r P (P' (a # xs)) f (findM g (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> corres r P (P' (a # xs)) f (do r <- g a;
if r then return (Some a) else findM g xs
od) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> corres r P (P' (a # xs)) (do x <- do x <- f;
return (Some x)
od \<sqinter> return None;
if x \<noteq> None then return (the x) else f
od) (do r <- g a;
if r then return (Some a) else findM g xs
od) proof (prove)
goal (3 subgoals):
 1. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> corres r (?Q3 a xs) (?Q'3 a xs) (do x <- do x <- f;
return (Some x)
od \<sqinter> return None;
if x \<noteq> None then return (the x) else f
od) (do r <- g a;
if r then return (Some a) else findM g xs
od)
 2. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P s\<rbrakk> \<Longrightarrow> ?Q3 a xs s
 3. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P' (a # xs) s\<rbrakk> \<Longrightarrow> ?Q'3 a xs s proof (prove)
goal (6 subgoals):
 1. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> suffix (a # ?xs8 a xs) xs'
 2. \<And>a xs x ra. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; if ra then \<exists>a'. x = Some a' \<and> r a' (Some a) else x = None\<rbrakk> \<Longrightarrow> corres r (?R7 a xs x) (?R'7 a xs ra) (if x \<noteq> None then return (the x) else f) (if ra then return (Some a) else findM g xs)
 3. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a xs\<rbrace> do x <- f;
return (Some x)
od \<sqinter> return None \<lbrace>?R7 a xs\<rbrace>
 4. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 a xs\<rbrace> g a \<lbrace>?R'7 a xs\<rbrace>
 5. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P s\<rbrakk> \<Longrightarrow> (P and ?Q7 a xs) s
 6. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P' (a # xs) s\<rbrakk> \<Longrightarrow> (P' (a # ?xs8 a xs) and ?Q'7 a xs) s proof (prove)
goal (5 subgoals):
 1. \<And>a xs x ra. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; if ra then \<exists>a'. x = Some a' \<and> r a' (Some a) else x = None\<rbrakk> \<Longrightarrow> corres r (?R7 a xs x) (?R'7 a xs ra) (if x \<noteq> None then return (the x) else f) (if ra then return (Some a) else findM g xs)
 2. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a xs\<rbrace> do x <- f;
return (Some x)
od \<sqinter> return None \<lbrace>?R7 a xs\<rbrace>
 3. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 a xs\<rbrace> g a \<lbrace>?R'7 a xs\<rbrace>
 4. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P s\<rbrakk> \<Longrightarrow> (P and ?Q7 a xs) s
 5. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P' (a # xs) s\<rbrakk> \<Longrightarrow> (P' (a # xs) and ?Q'7 a xs) s proof (prove)
goal (7 subgoals):
 1. \<And>a xs x ra. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; if ra then \<exists>a'. x = Some a' \<and> r a' (Some a) else x = None\<rbrakk> \<Longrightarrow> (x \<noteq> None) = ra
 2. \<And>a xs x ra. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; if ra then \<exists>a'. x = Some a' \<and> r a' (Some a) else x = None; x \<noteq> None\<rbrakk> \<Longrightarrow> corres r (?P15 a xs x) (?P'18 a xs ra) (return (the x)) (return (Some a))
 3. \<And>a xs x ra. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; if ra then \<exists>a'. x = Some a' \<and> r a' (Some a) else x = None; \<not> ra\<rbrakk> \<Longrightarrow> corres r (?Q16 a xs x) (?Q'19 a xs ra) f (findM g xs)
 4. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a xs\<rbrace> do x <- f;
return (Some x)
od \<sqinter> return None \<lbrace>\<lambda>x. if x \<noteq> None then ?P15 a xs x else ?Q16 a xs x\<rbrace>
 5. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 a xs\<rbrace> g a \<lbrace>\<lambda>r. if r then ?P'18 a xs r else ?Q'19 a xs r\<rbrace>
 6. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P s\<rbrakk> \<Longrightarrow> (P and ?Q7 a xs) s
 7. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P' (a # xs) s\<rbrakk> \<Longrightarrow> (P' (a # xs) and ?Q'7 a xs) s proof (prove)
goal (6 subgoals):
 1. \<And>a xs x ra. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; if ra then \<exists>a'. x = Some a' \<and> r a' (Some a) else x = None; x \<noteq> None\<rbrakk> \<Longrightarrow> corres r (?P15 a xs x) (?P'18 a xs ra) (return (the x)) (return (Some a))
 2. \<And>a xs x ra. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; if ra then \<exists>a'. x = Some a' \<and> r a' (Some a) else x = None; \<not> ra\<rbrakk> \<Longrightarrow> corres r (?Q16 a xs x) (?Q'19 a xs ra) f (findM g xs)
 3. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a xs\<rbrace> do x <- f;
return (Some x)
od \<sqinter> return None \<lbrace>\<lambda>x. if x \<noteq> None then ?P15 a xs x else ?Q16 a xs x\<rbrace>
 4. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 a xs\<rbrace> g a \<lbrace>\<lambda>r. if r then ?P'18 a xs r else ?Q'19 a xs r\<rbrace>
 5. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P s\<rbrakk> \<Longrightarrow> (P and ?Q7 a xs) s
 6. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P' (a # xs) s\<rbrakk> \<Longrightarrow> (P' (a # xs) and ?Q'7 a xs) s proof (prove)
goal (6 subgoals):
 1. \<And>a xs ra y s s'. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; if ra then \<exists>a'. Some y = Some a' \<and> r a' (Some a) else Some y = None; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> r y (Some a)
 2. \<And>a xs x ra. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; if ra then \<exists>a'. x = Some a' \<and> r a' (Some a) else x = None; \<not> ra\<rbrakk> \<Longrightarrow> corres r (?Q16 a xs x) (?Q'19 a xs ra) f (findM g xs)
 3. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a xs\<rbrace> do x <- f;
return (Some x)
od \<sqinter> return None \<lbrace>\<lambda>x. if x \<noteq> None then \<lambda>_. True else ?Q16 a xs x\<rbrace>
 4. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 a xs\<rbrace> g a \<lbrace>\<lambda>r. if r then \<lambda>_. True else ?Q'19 a xs r\<rbrace>
 5. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P s\<rbrakk> \<Longrightarrow> (P and ?Q7 a xs) s
 6. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P' (a # xs) s\<rbrakk> \<Longrightarrow> (P' (a # xs) and ?Q'7 a xs) s proof (prove)
goal (5 subgoals):
 1. \<And>a xs x ra. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; if ra then \<exists>a'. x = Some a' \<and> r a' (Some a) else x = None; \<not> ra\<rbrakk> \<Longrightarrow> corres r (?Q16 a xs x) (?Q'19 a xs ra) f (findM g xs)
 2. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a xs\<rbrace> do x <- f;
return (Some x)
od \<sqinter> return None \<lbrace>\<lambda>x. if x \<noteq> None then \<lambda>_. True else ?Q16 a xs x\<rbrace>
 3. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 a xs\<rbrace> g a \<lbrace>\<lambda>r. if r then \<lambda>_. True else ?Q'19 a xs r\<rbrace>
 4. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P s\<rbrakk> \<Longrightarrow> (P and ?Q7 a xs) s
 5. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P' (a # xs) s\<rbrakk> \<Longrightarrow> (P' (a # xs) and ?Q'7 a xs) s proof (prove)
goal (4 subgoals):
 1. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a xs\<rbrace> do x <- f;
return (Some x)
od \<sqinter> return None \<lbrace>\<lambda>x. if x \<noteq> None then \<lambda>_. True else P\<rbrace>
 2. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 a xs\<rbrace> g a \<lbrace>\<lambda>r. if r then \<lambda>_. True else P' xs\<rbrace>
 3. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P s\<rbrakk> \<Longrightarrow> (P and ?Q7 a xs) s
 4. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P' (a # xs) s\<rbrakk> \<Longrightarrow> (P' (a # xs) and ?Q'7 a xs) s proof (prove)
goal (3 subgoals):
 1. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 a xs\<rbrace> g a \<lbrace>\<lambda>r. if r then \<lambda>_. True else P' xs\<rbrace>
 2. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P s\<rbrakk> \<Longrightarrow> (P and P) s
 3. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P' (a # xs) s\<rbrakk> \<Longrightarrow> (P' (a # xs) and ?Q'7 a xs) s proof (prove)
goal (4 subgoals):
 1. \<And>a xs rv s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; \<not> rv \<longrightarrow> P' (?xs48 a xs) s\<rbrakk> \<Longrightarrow> (if rv then \<lambda>_. True else P' xs) s
 2. \<And>a xs. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'\<rbrakk> \<Longrightarrow> suffix (a # ?xs48 a xs) xs'
 3. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P s\<rbrakk> \<Longrightarrow> (P and P) s
 4. \<And>a xs s. \<lbrakk>suffix xs xs' \<Longrightarrow> corres r P (P' xs) f (findM g xs); suffix (a # xs) xs'; P' (a # xs) s\<rbrakk> \<Longrightarrow> (P' (a # xs) and P' (a # ?xs48 a xs)) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres r P (P' xs) f (findM g xs)

goal:
No subgoals!