theory Reader_Option_Monad

lemma option_while'_term:
  assumes "I r"
  assumes "wf M"
  assumes step_less: "\<And>r r'. \<lbrakk>I r; C r; B r = Some r'\<rbrakk> \<Longrightarrow> (r',r) \<in> M"
  assumes step_I: "\<And>r r'. \<lbrakk>I r; C r; B r = Some r'\<rbrakk> \<Longrightarrow> I r'"
  obtains sr' where "(Some r, sr') \<in> option_while' C B" apply atomize_elim using assms(2,1) proof induct case (less r) show ?case proof (cases "C r" "B r" rule: bool.exhaust[case_product option.exhaust]) case (True_Some r') then have "(r',r) \<in> M" "I r'" by (auto intro: less step_less step_I) then obtain sr' where "(Some r', sr') \<in> option_while' C B" by atomize_elim (rule less) then have "(Some r, sr') \<in> option_while' C B" using True_Some by (auto intro: option_while'.intros) then show ?thesis .. qed (auto intro: option_while'.intros) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>sr'. (Some r, sr') \<in> option_while' C B \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<exists>sr'. (Some r, sr') \<in> option_while' C B proof (prove)
using this:
wf M
I r

goal (1 subgoal):
 1. \<exists>sr'. (Some r, sr') \<in> option_while' C B proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> M; I y\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some y, sr') \<in> option_while' C B; I x\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some x, sr') \<in> option_while' C B proof (state)
this:
\<lbrakk>(?y, r) \<in> M; I ?y\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some ?y, sr') \<in> option_while' C B
I r

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> M; I y\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some y, sr') \<in> option_while' C B; I x\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some x, sr') \<in> option_while' C B proof (prove)
goal (1 subgoal):
 1. \<exists>sr'. (Some r, sr') \<in> option_while' C B proof (state)
goal (4 subgoals):
 1. \<lbrakk>C r = True; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 2. \<And>x2__. \<lbrakk>C r = True; B r = Some x2__\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 3. \<lbrakk>C r = False; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 4. \<And>x2__. \<lbrakk>C r = False; B r = Some x2__\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B proof (state)
this:
C r = True
B r = Some r'

goal (4 subgoals):
 1. \<lbrakk>C r = True; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 2. \<And>x2__. \<lbrakk>C r = True; B r = Some x2__\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 3. \<lbrakk>C r = False; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 4. \<And>x2__. \<lbrakk>C r = False; B r = Some x2__\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B proof (chain)
picking this:
C r = True
B r = Some r' proof (prove)
using this:
C r = True
B r = Some r'

goal (1 subgoal):
 1. (r', r) \<in> M &&& I r' proof (state)
this:
(r', r) \<in> M
I r'

goal (4 subgoals):
 1. \<lbrakk>C r = True; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 2. \<And>x2__. \<lbrakk>C r = True; B r = Some x2__\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 3. \<lbrakk>C r = False; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 4. \<And>x2__. \<lbrakk>C r = False; B r = Some x2__\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B proof (chain)
picking this:
(r', r) \<in> M
I r' proof (prove)
using this:
(r', r) \<in> M
I r'

goal (1 subgoal):
 1. (\<And>sr'. (Some r', sr') \<in> option_while' C B \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
(Some r', sr') \<in> option_while' C B

goal (4 subgoals):
 1. \<lbrakk>C r = True; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 2. \<And>x2__. \<lbrakk>C r = True; B r = Some x2__\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 3. \<lbrakk>C r = False; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 4. \<And>x2__. \<lbrakk>C r = False; B r = Some x2__\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B proof (chain)
picking this:
(Some r', sr') \<in> option_while' C B proof (prove)
using this:
(Some r', sr') \<in> option_while' C B

goal (1 subgoal):
 1. (Some r, sr') \<in> option_while' C B proof (prove)
using this:
(Some r', sr') \<in> option_while' C B
C r = True
B r = Some r'

goal (1 subgoal):
 1. (Some r, sr') \<in> option_while' C B proof (state)
this:
(Some r, sr') \<in> option_while' C B

goal (4 subgoals):
 1. \<lbrakk>C r = True; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 2. \<And>x2__. \<lbrakk>C r = True; B r = Some x2__\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 3. \<lbrakk>C r = False; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 4. \<And>x2__. \<lbrakk>C r = False; B r = Some x2__\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B proof (chain)
picking this:
(Some r, sr') \<in> option_while' C B proof (prove)
using this:
(Some r, sr') \<in> option_while' C B

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

goal (3 subgoals):
 1. \<lbrakk>C r = True; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 2. \<lbrakk>C r = False; B r = None\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B
 3. \<And>x2__. \<lbrakk>C r = False; B r = Some x2__\<rbrakk> \<Longrightarrow> \<exists>sr'. (Some r, sr') \<in> option_while' C B proof (state)
this:
\<exists>sr'. (Some r, sr') \<in> option_while' C B

goal:
No subgoals!