theory Reader_Option_Monad

lemma option_while_rule':
  assumes "option_while C B s = ss'"
  assumes "wf M"
  assumes "I (Some s)"
  assumes less: "\<And>s s'. C s \<Longrightarrow> I (Some s) \<Longrightarrow> B s = Some s' \<Longrightarrow> (s', s) \<in> M"
  assumes step: "\<And>s s'. C s \<Longrightarrow> I (Some s) \<Longrightarrow> B s = Some s' \<Longrightarrow> I (Some s')"
  assumes final: "\<And>s. C s \<Longrightarrow> I (Some s) \<Longrightarrow> B s = None \<Longrightarrow> I None"
  shows "I ss' \<and> (case ss' of Some s' \<Rightarrow> \<not> C s' | _ \<Rightarrow> True)" proof - define ss where "ss \<equiv> Some s" obtain ss1' where "(Some s, ss1') \<in> option_while' C B" using assms(3,2,4,5) by (rule option_while'_term) then have *: "(ss, ss') \<in> option_while' C B" using \<open>option_while C B s = ss'\<close> by (auto simp: option_while_simps ss_def) show ?thesis proof (cases ss') case (Some s') with * ss_def show ?thesis using \<open>I _\<close> by (induct arbitrary:s) (auto intro: step) next case None with * ss_def show ?thesis using \<open>I _\<close> by (induct arbitrary:s) (auto intro: step final) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (state)
goal (1 subgoal):
 1. I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (state)
this:
ss \<equiv> Some s

goal (1 subgoal):
 1. I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (prove)
goal (1 subgoal):
 1. (\<And>ss1'. (Some s, ss1') \<in> option_while' C B \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
I (Some s)
wf M
\<lbrakk>C ?s; I (Some ?s); B ?s = Some ?s'\<rbrakk> \<Longrightarrow> (?s', ?s) \<in> M
\<lbrakk>C ?s; I (Some ?s); B ?s = Some ?s'\<rbrakk> \<Longrightarrow> I (Some ?s')

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

goal (1 subgoal):
 1. I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (chain)
picking this:
(Some s, ss1') \<in> option_while' C B proof (prove)
using this:
(Some s, ss1') \<in> option_while' C B

goal (1 subgoal):
 1. (ss, ss') \<in> option_while' C B proof (prove)
using this:
(Some s, ss1') \<in> option_while' C B
option_while C B s = ss'

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

goal (1 subgoal):
 1. I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (prove)
goal (1 subgoal):
 1. I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (state)
goal (2 subgoals):
 1. ss' = None \<Longrightarrow> I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s')
 2. \<And>a. ss' = Some a \<Longrightarrow> I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (state)
this:
ss' = Some s'

goal (2 subgoals):
 1. ss' = None \<Longrightarrow> I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s')
 2. \<And>a. ss' = Some a \<Longrightarrow> I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (chain)
picking this:
(ss, ss') \<in> option_while' C B
ss \<equiv> Some s
ss' = Some s' proof (prove)
using this:
(ss, ss') \<in> option_while' C B
ss \<equiv> Some s
ss' = Some s'

goal (1 subgoal):
 1. I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (prove)
using this:
(ss, ss') \<in> option_while' C B
ss \<equiv> Some s
ss' = Some s'
I (Some s)

goal (1 subgoal):
 1. I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (state)
this:
I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s')

goal (1 subgoal):
 1. ss' = None \<Longrightarrow> I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (state)
goal (1 subgoal):
 1. ss' = None \<Longrightarrow> I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (state)
this:
ss' = None

goal (1 subgoal):
 1. ss' = None \<Longrightarrow> I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (chain)
picking this:
(ss, ss') \<in> option_while' C B
ss \<equiv> Some s
ss' = None proof (prove)
using this:
(ss, ss') \<in> option_while' C B
ss \<equiv> Some s
ss' = None

goal (1 subgoal):
 1. I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (prove)
using this:
(ss, ss') \<in> option_while' C B
ss \<equiv> Some s
ss' = None
I (Some s)

goal (1 subgoal):
 1. I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s') proof (state)
this:
I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s')

goal:
No subgoals! proof (state)
this:
I ss' \<and> (case ss' of None \<Rightarrow> True | Some s' \<Rightarrow> \<not> C s')

goal:
No subgoals!