theory Separation_Algebra

lemma weakest_intuitionistic:
  "\<not> (\<exists>Q. (\<forall>h. ((sep_true \<longrightarrow>* P) h \<longrightarrow> Q h)) \<and> intuitionistic Q \<and>
      Q \<noteq> (sep_true \<longrightarrow>* P) \<and> (\<forall>h. Q h \<longrightarrow> P h))" apply (clarsimp) apply (rule ext) apply (rule iffI) apply (rule sep_implI) apply (drule_tac h="x" and h'="x + h'" in intuitionisticD) apply (clarsimp simp: sep_add_ac sep_substate_disj_add)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<nexists>Q. (\<forall>h. ((\<lambda>s. True) \<longrightarrow>* P) h \<longrightarrow> Q h) \<and> intuitionistic Q \<and> Q \<noteq> ((\<lambda>s. True) \<longrightarrow>* P) \<and> (\<forall>h. Q h \<longrightarrow> P h) proof (prove)
goal (1 subgoal):
 1. \<And>Q. \<lbrakk>intuitionistic Q; \<forall>h. ((\<lambda>s. True) \<longrightarrow>* P) h \<longrightarrow> Q h; \<forall>h. Q h \<longrightarrow> P h\<rbrakk> \<Longrightarrow> Q = ((\<lambda>s. True) \<longrightarrow>* P) proof (prove)
goal (1 subgoal):
 1. \<And>Q x. \<lbrakk>intuitionistic Q; \<forall>h. ((\<lambda>s. True) \<longrightarrow>* P) h \<longrightarrow> Q h; \<forall>h. Q h \<longrightarrow> P h\<rbrakk> \<Longrightarrow> Q x = ((\<lambda>s. True) \<longrightarrow>* P) x proof (prove)
goal (2 subgoals):
 1. \<And>Q x. \<lbrakk>intuitionistic Q; \<forall>h. ((\<lambda>s. True) \<longrightarrow>* P) h \<longrightarrow> Q h; \<forall>h. Q h \<longrightarrow> P h; Q x\<rbrakk> \<Longrightarrow> ((\<lambda>s. True) \<longrightarrow>* P) x
 2. \<And>Q x. \<lbrakk>intuitionistic Q; \<forall>h. ((\<lambda>s. True) \<longrightarrow>* P) h \<longrightarrow> Q h; \<forall>h. Q h \<longrightarrow> P h; ((\<lambda>s. True) \<longrightarrow>* P) x\<rbrakk> \<Longrightarrow> Q x proof (prove)
goal (2 subgoals):
 1. \<And>Q x h'. \<lbrakk>intuitionistic Q; \<forall>h. ((\<lambda>s. True) \<longrightarrow>* P) h \<longrightarrow> Q h; \<forall>h. Q h \<longrightarrow> P h; Q x; x ## h'; True\<rbrakk> \<Longrightarrow> P (x + h')
 2. \<And>Q x. \<lbrakk>intuitionistic Q; \<forall>h. ((\<lambda>s. True) \<longrightarrow>* P) h \<longrightarrow> Q h; \<forall>h. Q h \<longrightarrow> P h; ((\<lambda>s. True) \<longrightarrow>* P) x\<rbrakk> \<Longrightarrow> Q x proof (prove)
goal (4 subgoals):
 1. \<And>Q x h'. \<lbrakk>\<forall>h. ((\<lambda>s. True) \<longrightarrow>* P) h \<longrightarrow> Q h; \<forall>h. Q h \<longrightarrow> P h; Q x; x ## h'; True\<rbrakk> \<Longrightarrow> Q x
 2. \<And>Q x h'. \<lbrakk>\<forall>h. ((\<lambda>s. True) \<longrightarrow>* P) h \<longrightarrow> Q h; \<forall>h. Q h \<longrightarrow> P h; Q x; x ## h'; True\<rbrakk> \<Longrightarrow> x \<preceq> x + h'
 3. \<And>Q x h'. \<lbrakk>\<forall>h. ((\<lambda>s. True) \<longrightarrow>* P) h \<longrightarrow> Q h; \<forall>h. Q h \<longrightarrow> P h; Q x; x ## h'; True; Q (x + h')\<rbrakk> \<Longrightarrow> P (x + h')
 4. \<And>Q x. \<lbrakk>intuitionistic Q; \<forall>h. ((\<lambda>s. True) \<longrightarrow>* P) h \<longrightarrow> Q h; \<forall>h. Q h \<longrightarrow> P h; ((\<lambda>s. True) \<longrightarrow>* P) x\<rbrakk> \<Longrightarrow> Q x proof (prove)
goal:
No subgoals!