theory Trace_Reader_Option

lemma gets_the_whileLoop:
  fixes C :: "'a \<Rightarrow> 's \<Rightarrow> bool"
  assumes terminates: "\<forall>s. whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s"
  shows "whileLoop C (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r)" proof - { fix r s r' s' ts assume "((r,s), ts, Result (r', s')) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))" then have "s = s' \<and> ts = [] \<and>(Some r, Some r') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" by (induct r s ts "Result (r', s')")
       (auto intro: option_while'.intros simp: gets_the_conv split: option.splits) } note wl'_Result = this { fix r s ts assume "((r,s), ts, Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))" then have "ts = [] \<and> (Some r, None) \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" by (induct r s ts "Failed :: (('s, 'a) tmres)")
         (auto intro: option_while'.intros simp: gets_the_conv split: option.splits) } note wl'_Failed = this { fix r s ts assume "((r,s), ts, Incomplete) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))" then have "False" by (induct r s ts "Incomplete :: (('s, 'a) tmres)")
         (auto intro: option_while'.intros simp: gets_the_conv split: option.splits) } note wl'_Incomplete = this { fix r s r' assume "(Some r, Some r') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" then have "((r,s), [], Result (r',s)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))" by (induct "Some r" "Some r'" arbitrary: r)
       (auto intro: whileLoop_results.intros simp: gets_the_conv) } note option_while'_Some = this { fix r s assume "(Some r, None) \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" then have "((r,s), [], Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))" by (induct "Some r" "None :: 'a option" arbitrary: r)
       (auto intro: whileLoop_results.intros simp: gets_the_conv) } note option_while'_None = this have "\<And>s. owhile C B r s = None
          \<Longrightarrow> whileLoop C (\<lambda>a. gets_the (B a)) r s = {([], Failed)}" using terminates by (intro subset_antisym;
        clarsimp simp: whileLoop_def owhile_def option_while_def gets_the_loop_terminates
                split: if_split_asm intro!: option_while'_None dest!: The_eqD)
       (case_tac b, auto dest!: wl'_Result wl'_Failed wl'_Incomplete option_while'_inj option_while'_THE) moreover have "\<And>s r'. owhile C B r s = Some r'
          \<Longrightarrow> whileLoop C (\<lambda>a. gets_the (B a)) r s = {([], Result (r', s))}" by (intro subset_antisym;
        clarsimp simp: whileLoop_def owhile_def option_while_def option_while'_THE
                split: if_split_asm intro!: option_while'_Some)
       (case_tac b, auto dest: wl'_Result wl'_Failed wl'_Incomplete option_while'_inj) ultimately show ?thesis by (auto simp: fun_eq_iff gets_the_conv split: option.split) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((r, s), ts, Result (r', s')) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (chain)
picking this:
((r, s), ts, Result (r', s')) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) proof (prove)
using this:
((r, s), ts, Result (r', s')) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. s = s' \<and> ts = [] \<and> (Some r, Some r') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) proof (state)
this:
s = s' \<and> ts = [] \<and> (Some r, Some r') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((?ra2, ?s2), ?ts2, Result (?r'2, ?s'2)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> ?s2 = ?s'2 \<and> ?ts2 = [] \<and> (Some ?ra2, Some ?r'2) \<in> option_while' (\<lambda>a. C a ?s2) (\<lambda>a. B a ?s2)

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((?ra2, ?s2), ?ts2, Result (?r'2, ?s'2)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> ?s2 = ?s'2 \<and> ?ts2 = [] \<and> (Some ?ra2, Some ?r'2) \<in> option_while' (\<lambda>a. C a ?s2) (\<lambda>a. B a ?s2)

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((?ra2, ?s2), ?ts2, Result (?r'2, ?s'2)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> ?s2 = ?s'2 \<and> ?ts2 = [] \<and> (Some ?ra2, Some ?r'2) \<in> option_while' (\<lambda>a. C a ?s2) (\<lambda>a. B a ?s2)

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((r, s), ts, Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (chain)
picking this:
((r, s), ts, Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) proof (prove)
using this:
((r, s), ts, Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. ts = [] \<and> (Some r, None) \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) proof (state)
this:
ts = [] \<and> (Some r, None) \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((?ra2, ?s2), ?ts2, Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> ?ts2 = [] \<and> (Some ?ra2, None) \<in> option_while' (\<lambda>a. C a ?s2) (\<lambda>a. B a ?s2)

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((?ra2, ?s2), ?ts2, Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> ?ts2 = [] \<and> (Some ?ra2, None) \<in> option_while' (\<lambda>a. C a ?s2) (\<lambda>a. B a ?s2)

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((?ra2, ?s2), ?ts2, Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> ?ts2 = [] \<and> (Some ?ra2, None) \<in> option_while' (\<lambda>a. C a ?s2) (\<lambda>a. B a ?s2)

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((r, s), ts, Incomplete) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (chain)
picking this:
((r, s), ts, Incomplete) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) proof (prove)
using this:
((r, s), ts, Incomplete) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. False proof (state)
this:
False

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((?ra2, ?s2), ?ts2, Incomplete) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> False

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((?ra2, ?s2), ?ts2, Incomplete) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> False

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
((?ra2, ?s2), ?ts2, Incomplete) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> False

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
(Some r, Some r') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (chain)
picking this:
(Some r, Some r') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) proof (prove)
using this:
(Some r, Some r') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)

goal (1 subgoal):
 1. ((r, s), [], Result (r', s)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) proof (state)
this:
((r, s), [], Result (r', s)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
(Some ?ra2, Some ?r'2) \<in> option_while' (\<lambda>a. C a ?s2) (\<lambda>a. B a ?s2) \<Longrightarrow> ((?ra2, ?s2), [], Result (?r'2, ?s2)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
(Some ?ra2, Some ?r'2) \<in> option_while' (\<lambda>a. C a ?s2) (\<lambda>a. B a ?s2) \<Longrightarrow> ((?ra2, ?s2), [], Result (?r'2, ?s2)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
(Some ?ra2, Some ?r'2) \<in> option_while' (\<lambda>a. C a ?s2) (\<lambda>a. B a ?s2) \<Longrightarrow> ((?ra2, ?s2), [], Result (?r'2, ?s2)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
(Some r, None) \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (chain)
picking this:
(Some r, None) \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) proof (prove)
using this:
(Some r, None) \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)

goal (1 subgoal):
 1. ((r, s), [], Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) proof (state)
this:
((r, s), [], Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
(Some ?ra2, None) \<in> option_while' (\<lambda>a. C a ?s2) (\<lambda>a. B a ?s2) \<Longrightarrow> ((?ra2, ?s2), [], Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
(Some ?ra2, None) \<in> option_while' (\<lambda>a. C a ?s2) (\<lambda>a. B a ?s2) \<Longrightarrow> ((?ra2, ?s2), [], Failed) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (prove)
goal (1 subgoal):
 1. \<And>s. owhile C B r s = None \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r s = {([], Failed)} proof (prove)
using this:
\<forall>s. whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s

goal (1 subgoal):
 1. \<And>s. owhile C B r s = None \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r s = {([], Failed)} proof (state)
this:
owhile C B r ?s = None \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = {([], Failed)}

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
owhile C B r ?s = None \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = {([], Failed)}

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (prove)
goal (1 subgoal):
 1. \<And>s r'. owhile C B r s = Some r' \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r s = {([], Result (r', s))} proof (state)
this:
owhile C B r ?s = Some ?r' \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = {([], Result (?r', ?s))}

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (chain)
picking this:
owhile C B r ?s = None \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = {([], Failed)}
owhile C B r ?s = Some ?r' \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = {([], Result (?r', ?s))} proof (prove)
using this:
owhile C B r ?s = None \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = {([], Failed)}
owhile C B r ?s = Some ?r' \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = {([], Result (?r', ?s))}

goal (1 subgoal):
 1. whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r) proof (state)
this:
whileLoop C
  (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r)

goal:
No subgoals!