theory Nondet_Reader_Option

lemma gets_the_whileLoop:
  fixes C :: "'a \<Rightarrow> 's \<Rightarrow> bool"
  shows "whileLoop C (\<lambda>a. gets_the (B a)) r = gets_the (owhile C B r)" proof - { fix r s r' s' assume "(Some (r,s), Some (r', s')) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))" then have "s = s' \<and> (Some r, Some r') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" by (induct "Some (r, s)" "Some (r', s')" arbitrary: r s)
       (auto intro: option_while'.intros simp: gets_the_conv split: option.splits) } note wl'_Inl = this { fix r s assume "(Some (r,s), None) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))" then have "(Some r, None) \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" by (induct "Some (r, s)" "None :: (('a \<times> 's) option)" arbitrary: r s)
         (auto intro: option_while'.intros simp: gets_the_conv split: option.splits) } note wl'_Inr = 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 "(Some (r,s), Some (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 "(Some (r,s), None) \<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 = ({}, True)" by (auto simp: whileLoop_def owhile_def option_while_def option_while'_THE gets_the_loop_terminates
      split: if_split_asm dest: option_while'_None wl'_Inl option_while'_inj) moreover have "\<And>s r'. owhile C B r s = Some r'
          \<Longrightarrow> whileLoop C (\<lambda>a. gets_the (B a)) r s = ({(r', s)}, False)" by (auto simp: whileLoop_def owhile_def option_while_def option_while'_THE gets_the_loop_terminates
      split: if_split_asm dest: wl'_Inl wl'_Inr option_while'_inj intro: option_while'_Some) 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:
(Some (r, s), Some (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:
(Some (r, s), Some (r', s')) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) proof (prove)
using this:
(Some (r, s), Some (r', s')) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. s = s' \<and> (Some r, Some r') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) proof (state)
this:
s = s' \<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:
(Some (?ra2, ?s2), Some (?r'2, ?s'2)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> ?s2 = ?s'2 \<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:
(Some (?ra2, ?s2), Some (?r'2, ?s'2)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> ?s2 = ?s'2 \<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:
(Some (?ra2, ?s2), Some (?r'2, ?s'2)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> ?s2 = ?s'2 \<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:
(Some (r, s), None) \<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:
(Some (r, s), None) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) proof (prove)
using this:
(Some (r, s), None) \<in> whileLoop_results C (\<lambda>a. gets_the (B a))

goal (1 subgoal):
 1. (Some r, None) \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) 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 (state)
this:
(Some (?ra2, ?s2), None) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> (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:
(Some (?ra2, ?s2), None) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> (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:
(Some (?ra2, ?s2), None) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) \<Longrightarrow> (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:
(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. (Some (r, s), Some (r', s)) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) proof (state)
this:
(Some (r, s), Some (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> (Some (?ra2, ?s2), Some (?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> (Some (?ra2, ?s2), Some (?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> (Some (?ra2, ?s2), Some (?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. (Some (r, s), None) \<in> whileLoop_results C (\<lambda>a. gets_the (B a)) proof (state)
this:
(Some (r, s), None) \<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> (Some (?ra2, ?s2), None) \<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> (Some (?ra2, ?s2), None) \<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 = ({}, True) proof (state)
this:
owhile C B r ?s = None \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = ({}, True)

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 = ({}, True)

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 = ({(r', s)}, False) proof (state)
this:
owhile C B r ?s = Some ?r' \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = ({(?r', ?s)}, False)

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 = ({}, True)
owhile C B r ?s = Some ?r' \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = ({(?r', ?s)}, False) proof (prove)
using this:
owhile C B r ?s = None \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = ({}, True)
owhile C B r ?s = Some ?r' \<Longrightarrow> whileLoop C
  (\<lambda>a. gets_the (B a)) r ?s = ({(?r', ?s)}, False)

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!