theory Nondet_Reader_Option

lemma gets_the_loop_terminates:
  "whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s
    \<longleftrightarrow> (\<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s))" (is "?L \<longleftrightarrow> ?R") proof assume ?L then show ?R proof (induct rule: whileLoop_terminates.induct[case_names 1 2]) case (2 r s) then show ?case by (cases "B r s") (auto simp: gets_the_conv intro: option_while'.intros) qed (auto intro: option_while'.intros) next assume ?R then show ?L proof (elim exE) fix rs' assume "(Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)" then have "whileLoop_terminates C (\<lambda>a. gets_the (B a)) (the (Some r)) s" by induct (auto intro: whileLoop_terminates.intros simp: gets_the_conv) then show ?thesis by simp qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s = (\<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)) proof (state)
goal (2 subgoals):
 1. whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s \<Longrightarrow> \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)
 2. \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) \<Longrightarrow> whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s proof (state)
this:
whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s

goal (2 subgoals):
 1. whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s \<Longrightarrow> \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)
 2. \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) \<Longrightarrow> whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s proof (chain)
picking this:
whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s proof (prove)
using this:
whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s

goal (1 subgoal):
 1. \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) proof (state)
goal (2 subgoals):
 1. \<And>r s. \<not> C r s \<Longrightarrow> \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)
 2. \<And>r s. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (gets_the (B r) s). whileLoop_terminates C (\<lambda>a. gets_the (B a)) r' s' \<and> (\<exists>rs'. (Some r', rs') \<in> option_while' (\<lambda>a. C a s') (\<lambda>a. B a s'))\<rbrakk> \<Longrightarrow> \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) proof (state)
this:
C r s
\<forall>(r', s')\<in>fst (gets_the (B r) s). whileLoop_terminates C (\<lambda>a. gets_the (B a)) r' s' \<and> (\<exists>rs'. (Some r', rs') \<in> option_while' (\<lambda>a. C a s') (\<lambda>a. B a s'))

goal (2 subgoals):
 1. \<And>r s. \<not> C r s \<Longrightarrow> \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)
 2. \<And>r s. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (gets_the (B r) s). whileLoop_terminates C (\<lambda>a. gets_the (B a)) r' s' \<and> (\<exists>rs'. (Some r', rs') \<in> option_while' (\<lambda>a. C a s') (\<lambda>a. B a s'))\<rbrakk> \<Longrightarrow> \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) proof (chain)
picking this:
C r s
\<forall>(r', s')\<in>fst (gets_the (B r) s). whileLoop_terminates C (\<lambda>a. gets_the (B a)) r' s' \<and> (\<exists>rs'. (Some r', rs') \<in> option_while' (\<lambda>a. C a s') (\<lambda>a. B a s')) proof (prove)
using this:
C r s
\<forall>(r', s')\<in>fst (gets_the (B r) s). whileLoop_terminates C (\<lambda>a. gets_the (B a)) r' s' \<and> (\<exists>rs'. (Some r', rs') \<in> option_while' (\<lambda>a. C a s') (\<lambda>a. B a s'))

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

goal (1 subgoal):
 1. \<And>r s. \<not> C r s \<Longrightarrow> \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) proof (state)
this:
\<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)

goal (1 subgoal):
 1. \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) \<Longrightarrow> whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s proof (state)
goal (1 subgoal):
 1. \<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) \<Longrightarrow> whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s proof (state)
this:
\<exists>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)

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

goal (1 subgoal):
 1. whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s proof (state)
goal (1 subgoal):
 1. \<And>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) \<Longrightarrow> whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s proof (state)
goal (1 subgoal):
 1. \<And>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) \<Longrightarrow> whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s proof (state)
this:
(Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s)

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

goal (1 subgoal):
 1. whileLoop_terminates C (\<lambda>a. gets_the (B a)) (the (Some r)) s proof (state)
this:
whileLoop_terminates C (\<lambda>a. gets_the (B a)) (the (Some r)) s

goal (1 subgoal):
 1. \<And>rs'. (Some r, rs') \<in> option_while' (\<lambda>a. C a s) (\<lambda>a. B a s) \<Longrightarrow> whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s proof (chain)
picking this:
whileLoop_terminates C (\<lambda>a. gets_the (B a)) (the (Some r)) s proof (prove)
using this:
whileLoop_terminates C (\<lambda>a. gets_the (B a)) (the (Some r)) s

goal (1 subgoal):
 1. whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s proof (state)
this:
whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s

goal:
No subgoals! proof (state)
this:
whileLoop_terminates C (\<lambda>a. gets_the (B a)) r s

goal:
No subgoals!