kings-crown/FVELER_Isabelle huggingface dataset:
theory DataIn

lemma DataIn_wrap_ptr_nf:
  "\<lbrace>\<lambda>s. (\<forall>x\<in>set (array_addrs (Ptr (symbol_table ''DataIn_data'')) 4096).
          is_valid_w8 s x) \<and>
         is_valid_dataport_ptr__C s x\<rbrace>
    DataIn_wrap_ptr' x y
   \<lbrace>\<lambda>_ s. (\<forall>x\<in>set (array_addrs (Ptr (symbol_table ''DataIn_data'')) 4096).
           is_valid_w8 s x) \<and>
          is_valid_dataport_ptr__C s x\<rbrace>!" apply (simp add:DataIn_wrap_ptr'_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x\<rbrace> DataIn_wrap_ptr' x y \<lbrace>\<lambda>_ s. (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x\<rbrace> do ya <- guard (\<lambda>s. \<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x);
condition (\<lambda>s. ptr_val y < symbol_table ''DataIn_data'' \<or> symbol_table ''DataIn_data'' + 0x1000 \<le> ptr_val y)
  (return (- 1))
  (do ya <- guard (\<lambda>s. is_valid_dataport_ptr__C s x);
ya <- modify (heap_dataport_ptr__C_update (\<lambda>a. a(x := id_C_update (\<lambda>a. 0) (a x))));
y <- modify (heap_dataport_ptr__C_update (\<lambda>a. a(x := offset_C_update (\<lambda>a. UCAST(32 \<rightarrow> 64 signed) (ptr_val y - symbol_table ''DataIn_data'')) (a x))));
return 0
od)
od \<lbrace>\<lambda>_ s. (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x \<Longrightarrow> (if ptr_val y < symbol_table ''DataIn_data'' \<or> symbol_table ''DataIn_data'' + 0x1000 \<le> ptr_val y then (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x else ((\<forall>xa\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 (heap_dataport_ptr__C_update (\<lambda>a. a(x := offset_C_update (\<lambda>a. UCAST(32 \<rightarrow> 64 signed) (ptr_val y - symbol_table ''DataIn_data'')) (a x))) (heap_dataport_ptr__C_update (\<lambda>a. a(x := id_C_update (\<lambda>a. 0) (a x))) s)) xa) \<and> is_valid_dataport_ptr__C (heap_dataport_ptr__C_update (\<lambda>a. a(x := offset_C_update (\<lambda>a. UCAST(32 \<rightarrow> 64 signed) (ptr_val y - symbol_table ''DataIn_data'')) (a x))) (heap_dataport_ptr__C_update (\<lambda>a. a(x := id_C_update (\<lambda>a. 0) (a x))) s)) x) \<and> is_valid_dataport_ptr__C s x) \<and> (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) proof (prove)
goal:
No subgoals!
theory DataIn

lemma DataIn_unwrap_ptr_nf:
  "\<lbrace>\<lambda>s. (\<forall>x\<in>set (array_addrs (Ptr (symbol_table ''DataIn_data'')) 4096).
          is_valid_w8 s x) \<and>
         is_valid_dataport_ptr__C s x\<rbrace>
    DataIn_unwrap_ptr' x
   \<lbrace>\<lambda>_ s. (\<forall>x\<in>set (array_addrs (Ptr (symbol_table ''DataIn_data'')) 4096).
           is_valid_w8 s x) \<and>
          is_valid_dataport_ptr__C s x\<rbrace>!" apply (simp add:DataIn_unwrap_ptr'_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x\<rbrace> DataIn_unwrap_ptr' x \<lbrace>\<lambda>_ s. (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x\<rbrace> do y <- guard (\<lambda>s. is_valid_dataport_ptr__C s x);
condition (\<lambda>s. id_C (heap_dataport_ptr__C s x) = 0)
  (do y <- guard (\<lambda>s. \<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x);
gets (\<lambda>s. PTR(unit) (symbol_table ''DataIn_data'' + SCAST(64 signed \<rightarrow> 32) (offset_C (heap_dataport_ptr__C s x))))
od)
  (return NULL)
od \<lbrace>\<lambda>_ s. (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x \<Longrightarrow> (if id_C (heap_dataport_ptr__C s x) = 0 then ((\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x) \<and> (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) else (\<forall>x\<in>set (array_addrs (PTR(8 word) (symbol_table ''DataIn_data'')) 4096). is_valid_w8 s x) \<and> is_valid_dataport_ptr__C s x) \<and> is_valid_dataport_ptr__C s x proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_conj_exists_left[simp]: "((\<lambda>s. \<exists>x. (P x) s) \<and>* R) \<equiv> (EXS x. (P x \<and>* R)) " apply (rule eq_reflection) by (clarsimp simp: sep_conj_def, fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<exists>x. P x s) \<and>* R \<equiv> \<lambda>s. \<exists>x. (P x \<and>* R) s proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. \<exists>x. P x s) \<and>* R) = (\<lambda>s. \<exists>x. (P x \<and>* R) s)
theory Extended_Separation_Algebra

lemma sep_substate_antisym:
  "x \<preceq> y \<Longrightarrow> y \<preceq> x \<Longrightarrow> x = (y :: 'a ::cancellative_sep_algebra)" apply (clarsimp simp: sep_substate_def) apply (rename_tac h' h) apply (subgoal_tac "h' = 0") apply (clarsimp) apply (drule_tac trans[where s=x and t="x+0"]) apply (clarsimp) apply (subgoal_tac "(x + h' + h = x + 0) \<longrightarrow> ((0 + x) = (h' + h) + x)") apply (drule mp, clarsimp) apply (metis sep_add_cancelD sep_add_disj_eq sep_disj_commuteI sep_disj_positive_zero sep_disj_zero) by (metis sep_add_assoc sep_add_commute sep_add_zero sep_add_zero_sym sep_disj_commuteI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<preceq> y; y \<preceq> x\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>z za. \<lbrakk>x ## z; y = x + z; x + z + za = x; x ## za; z ## za\<rbrakk> \<Longrightarrow> x = x + z proof (prove)
goal (1 subgoal):
 1. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x + h' + h = x; x ## h; h' ## h\<rbrakk> \<Longrightarrow> x = x + h' proof (prove)
goal (2 subgoals):
 1. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x + h' + h = x; x ## h; h' ## h; h' = (0::'a)\<rbrakk> \<Longrightarrow> x = x + h'
 2. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x + h' + h = x; x ## h; h' ## h\<rbrakk> \<Longrightarrow> h' = (0::'a) proof (prove)
goal (1 subgoal):
 1. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x + h' + h = x; x ## h; h' ## h\<rbrakk> \<Longrightarrow> h' = (0::'a) proof (prove)
goal (2 subgoals):
 1. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x ## h; h' ## h\<rbrakk> \<Longrightarrow> x = x + (0::'a)
 2. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x ## h; h' ## h; x + h' + h = x + (0::'a)\<rbrakk> \<Longrightarrow> h' = (0::'a) proof (prove)
goal (1 subgoal):
 1. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x ## h; h' ## h; x + h' + h = x + (0::'a)\<rbrakk> \<Longrightarrow> h' = (0::'a) proof (prove)
goal (2 subgoals):
 1. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x ## h; h' ## h; x + h' + h = x + (0::'a); x + h' + h = x + (0::'a) \<longrightarrow> (0::'a) + x = h' + h + x\<rbrakk> \<Longrightarrow> h' = (0::'a)
 2. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x ## h; h' ## h; x + h' + h = x + (0::'a)\<rbrakk> \<Longrightarrow> x + h' + h = x + (0::'a) \<longrightarrow> (0::'a) + x = h' + h + x proof (prove)
goal (2 subgoals):
 1. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x ## h; h' ## h; x + h' + h = x + (0::'a); (0::'a) + x = h' + h + x\<rbrakk> \<Longrightarrow> h' = (0::'a)
 2. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x ## h; h' ## h; x + h' + h = x + (0::'a)\<rbrakk> \<Longrightarrow> x + h' + h = x + (0::'a) \<longrightarrow> (0::'a) + x = h' + h + x proof (prove)
goal (1 subgoal):
 1. \<And>h' h. \<lbrakk>x ## h'; y = x + h'; x ## h; h' ## h; x + h' + h = x + (0::'a)\<rbrakk> \<Longrightarrow> x + h' + h = x + (0::'a) \<longrightarrow> (0::'a) + x = h' + h + x
theory Extended_Separation_Algebra

lemma septraction_impl1:
  "(P -* Q) s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (P' -* Q) s " apply (clarsimp simp: septraction_def pred_neg_def) using sep_impl_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P -* Q) s; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> (P' -* Q) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> (P \<longrightarrow>* (\<lambda>x. \<not> Q x)) s; \<And>s. P s \<Longrightarrow> P' s; (P' \<longrightarrow>* (\<lambda>x. \<not> Q x)) s\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
?P \<longrightarrow>* ?Q \<equiv> \<lambda>h. \<forall>h'. h ## h' \<and> ?P h' \<longrightarrow> ?Q (h + h')

goal (1 subgoal):
 1. \<lbrakk>\<not> (P \<longrightarrow>* (\<lambda>x. \<not> Q x)) s; \<And>s. P s \<Longrightarrow> P' s; (P' \<longrightarrow>* (\<lambda>x. \<not> Q x)) s\<rbrakk> \<Longrightarrow> False
theory Extended_Separation_Algebra

lemma septraction_impl2:
  "(P -* Q) s \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> (P -* Q') s " apply (clarsimp simp: septraction_def pred_neg_def) using sep_impl_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P -* Q) s; \<And>s. Q s \<Longrightarrow> Q' s\<rbrakk> \<Longrightarrow> (P -* Q') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> (P \<longrightarrow>* (\<lambda>x. \<not> Q x)) s; \<And>s. Q s \<Longrightarrow> Q' s; (P \<longrightarrow>* (\<lambda>x. \<not> Q' x)) s\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
?P \<longrightarrow>* ?Q \<equiv> \<lambda>h. \<forall>h'. h ## h' \<and> ?P h' \<longrightarrow> ?Q (h + h')

goal (1 subgoal):
 1. \<lbrakk>\<not> (P \<longrightarrow>* (\<lambda>x. \<not> Q x)) s; \<And>s. Q s \<Longrightarrow> Q' s; (P \<longrightarrow>* (\<lambda>x. \<not> Q' x)) s\<rbrakk> \<Longrightarrow> False
theory Extended_Separation_Algebra

lemma sep_septraction_snake:
  "(P -* Q) s \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> (P \<leadsto>* Q') s) \<Longrightarrow>  Q' s" apply (clarsimp simp: sep_coimpl_def septraction_def pred_neg_def sep_conj_def sep_impl_def) using sep_add_commute sep_disj_commute by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P -* Q) s; \<And>s. Q s \<Longrightarrow> (P \<leadsto>* Q') s\<rbrakk> \<Longrightarrow> Q' s proof (prove)
goal (1 subgoal):
 1. \<And>h'. \<lbrakk>\<And>s. Q s \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<forall>y. s = x + y \<longrightarrow> x ## y \<longrightarrow> Q' y); s ## h'; P h'; Q (s + h')\<rbrakk> \<Longrightarrow> Q' s proof (prove)
using this:
?x ## ?y \<Longrightarrow> ?x + ?y = ?y + ?x
?x ## ?y = ?y ## ?x

goal (1 subgoal):
 1. \<And>h'. \<lbrakk>\<And>s. Q s \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<forall>y. s = x + y \<longrightarrow> x ## y \<longrightarrow> Q' y); s ## h'; P h'; Q (s + h')\<rbrakk> \<Longrightarrow> Q' s
theory Extended_Separation_Algebra

lemma sep_snake_septraction:
  "Q s \<Longrightarrow> (\<And>s. (P -* Q) s \<Longrightarrow> Q' s) \<Longrightarrow> (P \<leadsto>* Q') s  " apply (clarsimp simp: sep_coimpl_def septraction_def pred_neg_def sep_conj_def sep_impl_def) using sep_add_commute sep_disj_commute by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Q s; \<And>s. (P -* Q) s \<Longrightarrow> Q' s\<rbrakk> \<Longrightarrow> (P \<leadsto>* Q') s proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>Q (x + y); \<And>s. \<exists>h'. s ## h' \<and> P h' \<and> Q (s + h') \<Longrightarrow> Q' s; P x; s = x + y; x ## y\<rbrakk> \<Longrightarrow> Q' y proof (prove)
using this:
?x ## ?y \<Longrightarrow> ?x + ?y = ?y + ?x
?x ## ?y = ?y ## ?x

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>Q (x + y); \<And>s. \<exists>h'. s ## h' \<and> P h' \<and> Q (s + h') \<Longrightarrow> Q' s; P x; s = x + y; x ## y\<rbrakk> \<Longrightarrow> Q' y
theory Extended_Separation_Algebra

lemma septraction_snake_trivial:
  "(P -* (P \<leadsto>* R)) s \<Longrightarrow> R s" by (erule sep_septraction_snake)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P -* (P \<leadsto>* R)) s \<Longrightarrow> R s
theory Extended_Separation_Algebra

lemma sep_impl_impl:
  "(P \<longrightarrow>* Q) s\<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> (P \<longrightarrow>* Q') s" by (metis sep_implD sep_implI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<longrightarrow>* Q) s; \<And>s. Q s \<Longrightarrow> Q' s\<rbrakk> \<Longrightarrow> (P \<longrightarrow>* Q') s
theory Extended_Separation_Algebra

lemma sep_min_subtract_subtract:
  "sep_min P = sep_subtract P P" apply (clarsimp simp: sep_subtract_def sep_min_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_min P = sep_subtract P P proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_subtract_distrib_disj:
  "sep_subtract (P or Q) R = ((sep_subtract P R) or (sep_subtract Q R))" apply (rule ext, rule iffI) apply (clarsimp simp: pred_disj_def pred_conj_def sep_subtract_def) apply (clarsimp simp: pred_disj_def pred_conj_def sep_subtract_def) apply (safe) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_subtract (P or Q) R = (sep_subtract P R or sep_subtract Q R) proof (prove)
goal (2 subgoals):
 1. \<And>x. sep_subtract (P or Q) R x \<Longrightarrow> (sep_subtract P R or sep_subtract Q R) x
 2. \<And>x. (sep_subtract P R or sep_subtract Q R) x \<Longrightarrow> sep_subtract (P or Q) R x proof (prove)
goal (1 subgoal):
 1. \<And>x. (sep_subtract P R or sep_subtract Q R) x \<Longrightarrow> sep_subtract (P or Q) R x proof (prove)
goal (1 subgoal):
 1. \<And>x. P x \<and> (R \<leadsto>* \<box>) x \<or> Q x \<and> (R \<leadsto>* \<box>) x \<Longrightarrow> (P x \<or> Q x) \<and> (R \<leadsto>* \<box>) x proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_snake_mp:
  "(P \<leadsto>* Q) s \<Longrightarrow> (P \<and>* sep_true) s \<Longrightarrow>  (P \<and>* Q) s  " apply (clarsimp simp: sep_coimpl_def) apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<leadsto>* Q) s; (P \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> (P \<and>* Q) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> (P \<and>* not Q) s; (P \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> (P \<and>* Q) s proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>xa. P xa \<longrightarrow> (\<forall>ya. x + y = xa + ya \<longrightarrow> xa ## ya \<longrightarrow> Q ya); x ## y; P x; s = x + y\<rbrakk> \<Longrightarrow> \<exists>xa ya. xa ## ya \<and> x + y = xa + ya \<and> P xa \<and> Q ya proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_coimpl_contrapos:
  "(P \<leadsto>* Q) = ((not Q) \<leadsto>* (not P))" by (rule ext, rule iffI; simp add: sep_coimpl_def pred_neg_def sep_conj_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<leadsto>* Q) = (not Q \<leadsto>* not P)
theory Extended_Separation_Algebra

lemma sep_curry':
  "R s \<Longrightarrow> (P \<longrightarrow>* (P \<and>* R)) s" by (simp add: sep_wand_trivial)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R s \<Longrightarrow> (P \<longrightarrow>* P \<and>* R) s
theory Extended_Separation_Algebra

lemma sep_coimpl_mp_gen:
  "(P \<and>* Q) s \<Longrightarrow> (P' \<leadsto>* Q') s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> ((P and P') \<and>* (Q and Q')) s" apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_conj_def pred_neg_def) by (fastforce simp: sep_disj_commute sep_add_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* Q) s; (P' \<leadsto>* Q') s; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> ((P and P') \<and>* (Q and Q')) s proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>xa. P' xa \<longrightarrow> (\<forall>ya. x + y = xa + ya \<longrightarrow> xa ## ya \<longrightarrow> Q' ya); \<And>s. P s \<Longrightarrow> P' s; x ## y; s = x + y; P x; Q y\<rbrakk> \<Longrightarrow> \<exists>xa ya. xa ## ya \<and> x + y = xa + ya \<and> P xa \<and> P' xa \<and> Q ya \<and> Q' ya
theory Extended_Separation_Algebra

lemma ex_pull:
  "\<exists>h s. P h s \<and> Q h \<Longrightarrow> \<exists>h. Q h \<and> (\<exists>s. P h s)" apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>h s. P h s \<and> Q h \<Longrightarrow> \<exists>h. Q h \<and> (\<exists>s. P h s) proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_mp_snake_mp:
  "(P \<and>* (P \<longrightarrow>* (P \<leadsto>* Q))) s \<Longrightarrow> (P \<and>* Q) s" apply (clarsimp simp: sep_conj_def) apply (rename_tac x y) apply (rule_tac x=x in exI) apply (rule_tac x=y in exI) apply (clarsimp) apply (clarsimp simp: sep_impl_def) apply (erule_tac x=x in allE) apply (clarsimp simp: sep_disj_commute) apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def) by (fastforce simp: sep_disj_commute sep_add_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* (P \<longrightarrow>* (P \<leadsto>* Q))) s \<Longrightarrow> (P \<and>* Q) s proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; s = x + y; P x; (P \<longrightarrow>* (P \<leadsto>* Q)) y\<rbrakk> \<Longrightarrow> \<exists>xa ya. xa ## ya \<and> x + y = xa + ya \<and> P xa \<and> Q ya proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; s = x + y; P x; (P \<longrightarrow>* (P \<leadsto>* Q)) y\<rbrakk> \<Longrightarrow> \<exists>xa ya. xa ## ya \<and> x + y = xa + ya \<and> P xa \<and> Q ya proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; s = x + y; P x; (P \<longrightarrow>* (P \<leadsto>* Q)) y\<rbrakk> \<Longrightarrow> \<exists>ya. x ## ya \<and> x + y = x + ya \<and> P x \<and> Q ya proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; s = x + y; P x; (P \<longrightarrow>* (P \<leadsto>* Q)) y\<rbrakk> \<Longrightarrow> x ## y \<and> x + y = x + y \<and> P x \<and> Q y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; s = x + y; P x; (P \<longrightarrow>* (P \<leadsto>* Q)) y\<rbrakk> \<Longrightarrow> Q y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; s = x + y; P x; \<forall>h'. y ## h' \<and> P h' \<longrightarrow> (P \<leadsto>* Q) (y + h')\<rbrakk> \<Longrightarrow> Q y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; s = x + y; P x; y ## x \<and> P x \<longrightarrow> (P \<leadsto>* Q) (y + x)\<rbrakk> \<Longrightarrow> Q y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; s = x + y; P x; (P \<leadsto>* Q) (y + x)\<rbrakk> \<Longrightarrow> Q y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; s = x + y; P x; \<forall>xa. P xa \<longrightarrow> (\<forall>ya. y + x = xa + ya \<longrightarrow> xa ## ya \<longrightarrow> Q ya)\<rbrakk> \<Longrightarrow> Q y
theory Extended_Separation_Algebra

lemma septract_cancel:
  "(P -* Q) s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> (P' -* Q') s" apply (clarsimp simp: septraction_def sep_impl_def pred_neg_def) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P -* Q) s; \<And>s. P s \<Longrightarrow> P' s; \<And>s. Q s \<Longrightarrow> Q' s\<rbrakk> \<Longrightarrow> (P' -* Q') s proof (prove)
goal (1 subgoal):
 1. \<And>h'. \<lbrakk>\<And>s. P s \<Longrightarrow> P' s; \<And>s. Q s \<Longrightarrow> Q' s; s ## h'; P h'; Q (s + h')\<rbrakk> \<Longrightarrow> \<exists>h'. s ## h' \<and> P' h' \<and> Q' (s + h') proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_coimpl_mp_zero:
  "(P \<leadsto>* Q) s \<Longrightarrow> P s   \<Longrightarrow> Q (0)" by (clarsimp simp: sep_coimpl_def sep_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<leadsto>* Q) s; P s\<rbrakk> \<Longrightarrow> Q (0::'a)
theory Extended_Separation_Algebra

lemma sep_neg_not:
  "(P \<leadsto>* sep_false) s \<Longrightarrow> \<not>P s" apply (cases "P s") apply (drule(1) sep_coimpl_mp_zero) apply (clarsimp) apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<leadsto>* (\<lambda>s. False)) s \<Longrightarrow> \<not> P s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(P \<leadsto>* (\<lambda>s. False)) s; P s\<rbrakk> \<Longrightarrow> \<not> P s
 2. \<lbrakk>(P \<leadsto>* (\<lambda>s. False)) s; \<not> P s\<rbrakk> \<Longrightarrow> \<not> P s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P s; False\<rbrakk> \<Longrightarrow> \<not> P s
 2. \<lbrakk>(P \<leadsto>* (\<lambda>s. False)) s; \<not> P s\<rbrakk> \<Longrightarrow> \<not> P s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<leadsto>* (\<lambda>s. False)) s; \<not> P s\<rbrakk> \<Longrightarrow> \<not> P s proof (prove)
goal:
No subgoals!
theory Extended_Separation_Algebra

lemma sep_antimp':
  "P s \<Longrightarrow> (Q \<leadsto>* (Q -* P)) s \<and> P s" apply (clarsimp) apply (erule sep_snake_septraction, assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> (Q \<leadsto>* Q -* P) s \<and> P s proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> (Q \<leadsto>* Q -* P) s proof (prove)
goal:
No subgoals!