theory Extended_Separation_Algebra

lemma cointuitionistic_def':
  "cointuitionistic P = (\<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s)" apply (rule iffI) apply (clarsimp) apply (clarsimp simp: sep_coimpl_def) apply (clarsimp simp: sep_conj_def pred_neg_def cointuitionistic_def) apply (rename_tac R x y) apply (erule_tac x="x + y" in allE) apply (erule_tac x=y in allE) apply (clarsimp) using sep_disj_commuteI sep_substate_disj_add' apply blast apply (clarsimp simp: cointuitionistic_def) apply (erule_tac x=h in allE) apply (clarsimp) apply (clarsimp simp: sep_substate_def) apply (erule_tac x="\<lambda>s. s = z" in allE) apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def) apply (fastforce simp: sep_disj_commute sep_add_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cointuitionistic P = (\<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s) proof (prove)
goal (2 subgoals):
 1. cointuitionistic P \<Longrightarrow> \<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s
 2. \<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s \<Longrightarrow> cointuitionistic P proof (prove)
goal (2 subgoals):
 1. \<And>s R. \<lbrakk>cointuitionistic P; P s\<rbrakk> \<Longrightarrow> (R \<leadsto>* P) s
 2. \<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s \<Longrightarrow> cointuitionistic P proof (prove)
goal (2 subgoals):
 1. \<And>s R. \<lbrakk>cointuitionistic P; P s; (R \<and>* not P) s\<rbrakk> \<Longrightarrow> False
 2. \<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s \<Longrightarrow> cointuitionistic P proof (prove)
goal (2 subgoals):
 1. \<And>R x y. \<lbrakk>\<forall>h h'. P h \<and> h' \<preceq> h \<longrightarrow> P h'; P (x + y); x ## y; R x; \<not> P y\<rbrakk> \<Longrightarrow> False
 2. \<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s \<Longrightarrow> cointuitionistic P proof (prove)
goal (2 subgoals):
 1. \<And>R x y. \<lbrakk>\<forall>h h'. P h \<and> h' \<preceq> h \<longrightarrow> P h'; P (x + y); x ## y; R x; \<not> P y\<rbrakk> \<Longrightarrow> False
 2. \<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s \<Longrightarrow> cointuitionistic P proof (prove)
goal (2 subgoals):
 1. \<And>R x y. \<lbrakk>P (x + y); x ## y; R x; \<not> P y; \<forall>h'. P (x + y) \<and> h' \<preceq> x + y \<longrightarrow> P h'\<rbrakk> \<Longrightarrow> False
 2. \<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s \<Longrightarrow> cointuitionistic P proof (prove)
goal (2 subgoals):
 1. \<And>R x y. \<lbrakk>P (x + y); x ## y; R x; \<not> P y; P (x + y) \<and> y \<preceq> x + y \<longrightarrow> P y\<rbrakk> \<Longrightarrow> False
 2. \<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s \<Longrightarrow> cointuitionistic P proof (prove)
goal (2 subgoals):
 1. \<And>R x y. \<lbrakk>P (x + y); x ## y; R x; \<not> P y; \<not> y \<preceq> x + y\<rbrakk> \<Longrightarrow> False
 2. \<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s \<Longrightarrow> cointuitionistic P proof (prove)
using this:
?x ## ?y \<Longrightarrow> ?y ## ?x
?x ## ?y \<Longrightarrow> ?x \<preceq> ?y + ?x

goal (2 subgoals):
 1. \<And>R x y. \<lbrakk>P (x + y); x ## y; R x; \<not> P y; \<not> y \<preceq> x + y\<rbrakk> \<Longrightarrow> False
 2. \<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s \<Longrightarrow> cointuitionistic P proof (prove)
goal (1 subgoal):
 1. \<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s \<Longrightarrow> cointuitionistic P proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>R. (R \<leadsto>* P) s); P h; h' \<preceq> h\<rbrakk> \<Longrightarrow> P h' proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>P h; h' \<preceq> h; P h \<longrightarrow> (\<forall>R. (R \<leadsto>* P) h)\<rbrakk> \<Longrightarrow> P h' proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>P h; h' \<preceq> h; \<forall>R. (R \<leadsto>* P) h\<rbrakk> \<Longrightarrow> P h' proof (prove)
goal (1 subgoal):
 1. \<And>h' z. \<lbrakk>P (h' + z); \<forall>R. (R \<leadsto>* P) (h' + z); h' ## z\<rbrakk> \<Longrightarrow> P h' proof (prove)
goal (1 subgoal):
 1. \<And>h' z. \<lbrakk>P (h' + z); h' ## z; ((\<lambda>s. s = z) \<leadsto>* P) (h' + z)\<rbrakk> \<Longrightarrow> P h' proof (prove)
goal (1 subgoal):
 1. \<And>h' z. \<lbrakk>P (h' + z); h' ## z; \<forall>y. h' + z = z + y \<longrightarrow> z ## y \<longrightarrow> P y\<rbrakk> \<Longrightarrow> P h' proof (prove)
goal:
No subgoals!