kings-crown/FVELER_Isabelle huggingface dataset:
theory Separation_Algebra

lemma sep_list_conj_distinct_filters:
  "\<lbrakk>distinct xs; \<And>x. (f x \<and> g x) = False\<rbrakk> \<Longrightarrow>
  \<And>* map P [x\<leftarrow>xs . f x \<or> g x] = (\<And>* map P [x\<leftarrow>xs . f x] \<and>* \<And>* map P [x\<leftarrow>xs . g x])" apply (subst sep_list_conj_sep_map_set_conj, simp)+ apply (subst distinct_filters, simp+) apply (subst sep.prod.union_disjoint, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; \<And>x. (f x \<and> g x) = False\<rbrakk> \<Longrightarrow> \<And>* map P (filter (\<lambda>x. f x \<or> g x) xs) = (\<And>* map P (filter f xs) \<and>* \<And>* map P (filter g xs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; \<And>x. (f x \<and> g x) = False\<rbrakk> \<Longrightarrow> sep_map_set_conj P (set (filter (\<lambda>x. f x \<or> g x) xs)) = (sep_map_set_conj P (set (filter f xs)) \<and>* sep_map_set_conj P (set (filter g xs))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; \<And>x. f x \<longrightarrow> \<not> g x\<rbrakk> \<Longrightarrow> sep_map_set_conj P ({x \<in> set xs. f x} \<union> {x \<in> set xs. g x}) = ((SETSEPCONJ x | x \<in> set xs \<and> f x. P x) \<and>* (SETSEPCONJ x | x \<in> set xs \<and> g x. P x)) proof (prove)
goal:
No subgoals!
theory Separation_Algebra

lemma sep_map_set_conj_set_disjoint:
  "\<lbrakk>finite {x. P x}; finite {x. Q x}; \<And>x. (P x \<and> Q x) = False\<rbrakk>
 \<Longrightarrow> sep_map_set_conj g {x. P x \<or> Q x} =
  (sep_map_set_conj g {x. P x} \<and>* sep_map_set_conj g {x. Q x})" apply (subst sep.prod.union_disjoint [symmetric], simp+) apply blast apply simp by (metis Collect_disj_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {x. P x}; finite {x. Q x}; \<And>x. (P x \<and> Q x) = False\<rbrakk> \<Longrightarrow> sep_map_set_conj g {x. P x \<or> Q x} = (sep_map_set_conj g {x. P x} \<and>* sep_map_set_conj g {x. Q x}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite {x. P x}; finite {x. Q x}; \<And>x. P x \<longrightarrow> \<not> Q x\<rbrakk> \<Longrightarrow> Collect P \<inter> Collect Q = {}
 2. \<lbrakk>finite {x. P x}; finite {x. Q x}; \<And>x. (P x \<and> Q x) = False\<rbrakk> \<Longrightarrow> sep_map_set_conj g {x. P x \<or> Q x} = sep_map_set_conj g (Collect P \<union> Collect Q) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {x. P x}; finite {x. Q x}; \<And>x. (P x \<and> Q x) = False\<rbrakk> \<Longrightarrow> sep_map_set_conj g {x. P x \<or> Q x} = sep_map_set_conj g (Collect P \<union> Collect Q) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {x. P x}; finite {x. Q x}; \<And>x. P x \<longrightarrow> \<not> Q x\<rbrakk> \<Longrightarrow> (SETSEPCONJ x | P x \<or> Q x. g x) = sep_map_set_conj g (Collect P \<union> Collect Q)
theory Separation_Algebra

lemma "precise ((=) s)" by (metis (full_types) precise_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. precise ((=) s)
theory Separation_Algebra

lemma sep_add_cancel:
  "x ## z \<Longrightarrow> y ## z \<Longrightarrow> (x + z = y + z) = (x = y)" by (metis sep_add_cancelD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x ## z; y ## z\<rbrakk> \<Longrightarrow> (x + z = y + z) = (x = y)
theory Separation_Algebra

lemma strictly_precise: "strictly_exact P \<Longrightarrow> precise P" by (metis precise_def strictly_exactD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. strictly_exact P \<Longrightarrow> precise P
theory Separation_Algebra

lemma sep_disj_positive_zero[simp]: "x ## y \<Longrightarrow> x + y = 0 \<Longrightarrow> x = 0 \<and> y = 0" by (metis (full_types) disjoint_zero_sym sep_add_cancelD sep_add_disjD
                         sep_add_zero_sym sep_disj_positive)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x ## y; x + y = (0::'a)\<rbrakk> \<Longrightarrow> x = (0::'a) \<and> y = (0::'a)
theory Sep_Select

lemma sep_eq [sep_select]: "(\<And>s. T s = (P \<and>* R) s) \<Longrightarrow> T s \<Longrightarrow> (P \<and>* R) s" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. T s = (P \<and>* R) s; T s\<rbrakk> \<Longrightarrow> (P \<and>* R) s
theory Sep_Select

lemma sep_asm_eq [sep_select_asm]: "(P \<and>* R) s \<Longrightarrow> (\<And>s. T s = (P \<and>* R) s) \<Longrightarrow> T s" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* R) s; \<And>s. T s = (P \<and>* R) s\<rbrakk> \<Longrightarrow> T s
theory Sep_Provers

lemma sep_asm_eq_erule:
  "(P \<and>* R) s \<Longrightarrow> (\<And>s. T s = (P \<and>* R) s) \<Longrightarrow> (T s \<Longrightarrow> (P' \<and>* R') s) \<Longrightarrow> (P' \<and>* R') s" by (clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* R) s; \<And>s. T s = (P \<and>* R) s; T s \<Longrightarrow> (P' \<and>* R') s\<rbrakk> \<Longrightarrow> (P' \<and>* R') s
theory Sep_Provers

lemma sep_rule:
  "(\<And>s. T s \<Longrightarrow> P s) \<Longrightarrow> (T \<and>* R) s \<Longrightarrow> (P \<and>* R) s" by (rule sep_conj_impl1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. T s \<Longrightarrow> P s; (T \<and>* R) s\<rbrakk> \<Longrightarrow> (P \<and>* R) s
theory Sep_Provers

lemma sep_erule:
  "(T \<and>* R') s  \<Longrightarrow> (\<And>s. T s \<Longrightarrow> P s) \<Longrightarrow> (\<And>s. R' s \<Longrightarrow> R s) \<Longrightarrow>  (P \<and>* R) s" by (rule sep_conj_impl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(T \<and>* R') s; \<And>s. T s \<Longrightarrow> P s; \<And>s. R' s \<Longrightarrow> R s\<rbrakk> \<Longrightarrow> (P \<and>* R) s
theory Sep_Tactic_Helpers

lemma sep_mp: "((Q \<longrightarrow>* R) \<and>* Q) s \<Longrightarrow> R s" by (rule sep_conj_sep_impl2)

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

lemma sep_mp_frame: "((Q \<longrightarrow>* R) \<and>* Q \<and>* R') s \<Longrightarrow> (R \<and>* R') s" apply (clarsimp simp: sep_conj_assoc[symmetric]) apply (erule sep_conj_impl) apply (erule (1) sep_mp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Q \<longrightarrow>* R) \<and>* Q \<and>* R') s \<Longrightarrow> (R \<and>* R') s proof (prove)
goal (1 subgoal):
 1. (((Q \<longrightarrow>* R) \<and>* Q) \<and>* R') s \<Longrightarrow> (R \<and>* R') s proof (prove)
goal (2 subgoals):
 1. \<And>h. ((Q \<longrightarrow>* R) \<and>* Q) h \<Longrightarrow> R h
 2. \<And>h. R' h \<Longrightarrow> R' h proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Helpers

lemma sep_empty_conj: "P s \<Longrightarrow> (\<box> \<and>* P) s" by clarsimp

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

lemma sep_conj_empty: "(\<box> \<and>* P)  s \<Longrightarrow> P s" by clarsimp

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

lemma sep_empty_imp: "(\<box> \<longrightarrow>* P) s \<Longrightarrow> P s" apply (clarsimp simp: sep_impl_def) apply (erule_tac x=0 in allE) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<box> \<longrightarrow>* P) s \<Longrightarrow> P s proof (prove)
goal (1 subgoal):
 1. \<forall>h'. s ## h' \<and> \<box> h' \<longrightarrow> P (s + h') \<Longrightarrow> P s proof (prove)
goal (1 subgoal):
 1. s ## (0::'a) \<and> \<box> (0::'a) \<longrightarrow> P (s + (0::'a)) \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Helpers

lemma sep_empty_imp': "(\<box> \<longrightarrow>* P) s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> Q s) \<Longrightarrow> Q s" apply (clarsimp simp: sep_impl_def) apply (erule_tac x=0 in allE) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<box> \<longrightarrow>* P) s; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> Q s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>h'. s ## h' \<and> \<box> h' \<longrightarrow> P (s + h'); \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> Q s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s \<Longrightarrow> Q s; s ## (0::'a) \<and> \<box> (0::'a) \<longrightarrow> P (s + (0::'a))\<rbrakk> \<Longrightarrow> Q s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Helpers

lemma sep_imp_empty: " P s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> Q s) \<Longrightarrow> (\<box> \<longrightarrow>* Q) s" by (erule sep_conj_sep_impl, clarsimp)

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

lemma refl_imp: "P \<Longrightarrow> P" by assumption

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> P
theory Sep_Cancel

lemma sep_curry': "\<lbrakk>(P \<and>* F) s; \<And>s. (Q \<and>* P \<and>* F) s \<Longrightarrow> R s\<rbrakk> \<Longrightarrow> (Q \<longrightarrow>* R) s" by (metis (full_types) sep.mult_commute sep_curry)

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

lemma sep_conj_sep_impl_safe:
  "(P \<longrightarrow>* P') s \<Longrightarrow> (\<And>s. ((P \<longrightarrow>* P') \<and>* Q) s \<Longrightarrow> (Q') s) \<Longrightarrow> (Q \<longrightarrow>* Q') s" by (rule sep_curry)

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

lemma  sep_conj_sep_impl_safe': "P s \<Longrightarrow> (\<And>s. (P \<and>* Q) s \<Longrightarrow> (P \<and>* R) s) \<Longrightarrow> (Q \<longrightarrow>* P \<and>* R) s" by (rule sep_curry)

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

lemma sep_wand_lens_simple: "(\<And>s. T s = (Q \<and>* R) s) \<Longrightarrow> (P \<longrightarrow>* T) s \<Longrightarrow> (P \<longrightarrow>* Q \<and>* R) s" by (clarsimp simp: sep_impl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. T s = (Q \<and>* R) s; (P \<longrightarrow>* T) s\<rbrakk> \<Longrightarrow> (P \<longrightarrow>* Q \<and>* R) s
theory Sep_MP

lemma sep_mp_gen: "((Q \<longrightarrow>* R) \<and>* Q') s \<Longrightarrow> (\<And>s. Q' s \<Longrightarrow> Q s) \<Longrightarrow> R s" by (clarsimp simp: sep_conj_def sep_impl_def)

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

lemma sep_mp_frame_gen: "\<lbrakk>((Q \<longrightarrow>* R) \<and>* Q' \<and>* R') s; (\<And>s. Q' s \<Longrightarrow> Q s)\<rbrakk> \<Longrightarrow> (R \<and>* R') s" by (metis sep_conj_left_commute sep_globalise sep_mp_frame)

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

lemma sep_impl_simpl:
     "(P \<and>* Q \<longrightarrow>* R) s \<Longrightarrow> (P \<longrightarrow>* Q \<longrightarrow>* R) s" apply (erule sep_conj_sep_impl) apply (erule sep_conj_sep_impl) apply (clarsimp simp: sep_conj_assoc) apply (erule sep_mp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q \<longrightarrow>* R) s \<Longrightarrow> (P \<longrightarrow>* Q \<longrightarrow>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>h. ((P \<and>* Q \<longrightarrow>* R) \<and>* P) h \<Longrightarrow> (Q \<longrightarrow>* R) h proof (prove)
goal (1 subgoal):
 1. \<And>h ha. (((P \<and>* Q \<longrightarrow>* R) \<and>* P) \<and>* Q) ha \<Longrightarrow> R ha proof (prove)
goal (1 subgoal):
 1. \<And>ha. ((P \<and>* Q \<longrightarrow>* R) \<and>* P \<and>* Q) ha \<Longrightarrow> R ha proof (prove)
goal:
No subgoals!
theory Sep_MP

lemma sep_wand_frame_lens: "((P \<longrightarrow>* Q) \<and>* R) s \<Longrightarrow> (\<And>s. T s = R s) ==> ((P \<longrightarrow>* Q) \<and>* T) s" by (metis sep_conj_commute sep_conj_impl1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((P \<longrightarrow>* Q) \<and>* R) s; \<And>s. T s = R s\<rbrakk> \<Longrightarrow> ((P \<longrightarrow>* Q) \<and>* T) s
theory Sep_Attribs

lemma sep_curry_atomised: "\<lbrakk>(\<And>s. (P \<and>* Q) s \<longrightarrow> R s); P s \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>* R) s" by (clarsimp simp: sep_conj_sep_impl)

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

lemma sep_remove_pure_imp_sep_imp: "( P \<longrightarrow>* (\<lambda>s. P' \<longrightarrow> Q s)) s \<Longrightarrow> P' \<Longrightarrow> (P \<longrightarrow>* Q) s" by (clarsimp)

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

lemma sep_backward: "\<lbrakk>\<And>s. P s \<longrightarrow> (Q \<and>* T) s; (P \<and>* (Q \<longrightarrow>* R)) s \<rbrakk> \<Longrightarrow> (T \<and>* R) s" by (metis sep_conj_commute sep_conj_impl1 sep_mp_frame)

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

lemma sep_remove_conj: "\<lbrakk>(P \<and>* R) s ; Q\<rbrakk> \<Longrightarrow> ((\<lambda>s. P s \<and> Q) \<and>* R) s " apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* R) s; Q\<rbrakk> \<Longrightarrow> ((\<lambda>s. P s \<and> Q) \<and>* R) s proof (prove)
goal:
No subgoals!
theory Sep_Attribs

lemma curry: "(P \<longrightarrow> Q \<longrightarrow> R) \<Longrightarrow> (P \<and> Q) \<longrightarrow> R" apply (safe) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R proof (prove)
goal:
No subgoals!
theory Sep_ImpI

lemma sep_wand_lens: "(\<And>s. T s = Q s) \<Longrightarrow> ((P \<longrightarrow>* T) \<and>* R) s \<Longrightarrow> ((P \<longrightarrow>* Q) \<and>* R) s" apply (sep_erule_full refl_imp) apply (clarsimp simp: sep_impl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. T s = Q s; ((P \<longrightarrow>* T) \<and>* R) s\<rbrakk> \<Longrightarrow> ((P \<longrightarrow>* Q) \<and>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s. T s = Q s; (P \<longrightarrow>* T) s\<rbrakk> \<Longrightarrow> (P \<longrightarrow>* Q) s proof (prove)
goal:
No subgoals!
theory Sep_ImpI

lemma sep_wand_lens': "(\<And>s. T s = Q s) \<Longrightarrow> ((T \<longrightarrow>* P) \<and>* R) s \<Longrightarrow> ((Q \<longrightarrow>* P) \<and>* R) s" apply (sep_erule_full refl_imp, erule sep_curry[rotated]) apply (clarsimp) apply (erule sep_mp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. T s = Q s; ((T \<longrightarrow>* P) \<and>* R) s\<rbrakk> \<Longrightarrow> ((Q \<longrightarrow>* P) \<and>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>s h. \<lbrakk>\<And>s. T s = Q s; ((T \<longrightarrow>* P) \<and>* Q) h\<rbrakk> \<Longrightarrow> P h proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>\<And>s. T s = Q s; ((Q \<longrightarrow>* P) \<and>* Q) h\<rbrakk> \<Longrightarrow> P h proof (prove)
goal:
No subgoals!
theory Sep_ImpI

lemma sep_wand_match:
  "(\<And>s. Q s \<Longrightarrow> Q' s)  \<Longrightarrow> (R \<longrightarrow>* R') s    ==>  (Q \<and>* R \<longrightarrow>* Q' \<and>* R') s" apply (erule sep_curry[rotated]) apply (sep_select_asm 1 3) apply (sep_drule (direct) sep_mp_frame) apply (sep_erule_full refl_imp, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. Q s \<Longrightarrow> Q' s; (R \<longrightarrow>* R') s\<rbrakk> \<Longrightarrow> (Q \<and>* R \<longrightarrow>* Q' \<and>* R') s proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>\<And>s. Q s \<Longrightarrow> Q' s; ((R \<longrightarrow>* R') \<and>* Q \<and>* R) h\<rbrakk> \<Longrightarrow> (Q' \<and>* R') h proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>\<And>s. Q s \<Longrightarrow> Q' s; ((R \<longrightarrow>* R') \<and>* R \<and>* Q) h\<rbrakk> \<Longrightarrow> (Q' \<and>* R') h proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>\<And>s. Q s \<Longrightarrow> Q' s; (R' \<and>* Q) h\<rbrakk> \<Longrightarrow> (Q' \<and>* R') h proof (prove)
goal:
No subgoals!
theory Sep_ImpI

lemma sep_wand_trivial:    "(\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> R' s            ==>   (Q \<longrightarrow>* Q' \<and>* R') s" apply (erule sep_curry[rotated]) apply (sep_erule_full refl_imp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. Q s \<Longrightarrow> Q' s; R' s\<rbrakk> \<Longrightarrow> (Q \<longrightarrow>* Q' \<and>* R') s proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>\<And>s. Q s \<Longrightarrow> Q' s; (R' \<and>* Q) h\<rbrakk> \<Longrightarrow> (Q' \<and>* R') h proof (prove)
goal (1 subgoal):
 1. \<And>h s. \<lbrakk>\<And>s. Q s \<Longrightarrow> Q' s; Q s\<rbrakk> \<Longrightarrow> Q' s proof (prove)
goal:
No subgoals!
theory Sep_ImpI

lemma sep_wand_collapse:  "(P \<and>* Q \<longrightarrow>* R) s \<Longrightarrow> (P \<longrightarrow>* Q \<longrightarrow>* R) s " apply (erule sep_curry[rotated])+ apply (clarsimp simp: sep_conj_assoc) apply (erule sep_mp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q \<longrightarrow>* R) s \<Longrightarrow> (P \<longrightarrow>* Q \<longrightarrow>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>h ha. (((P \<and>* Q \<longrightarrow>* R) \<and>* P) \<and>* Q) ha \<Longrightarrow> R ha proof (prove)
goal (1 subgoal):
 1. \<And>ha. ((P \<and>* Q \<longrightarrow>* R) \<and>* P \<and>* Q) ha \<Longrightarrow> R ha proof (prove)
goal:
No subgoals!
theory Sep_ImpI

lemma sep_wand_match_less_safe:
  assumes drule: " \<And>s. (Q' \<and>* R) s \<Longrightarrow> ((P \<longrightarrow>* R') \<and>* Q' \<and>* R'' ) s "
  shows "(Q' \<and>* R) s \<Longrightarrow> (\<And>s. Q' s \<Longrightarrow> Q s) \<Longrightarrow> ((P \<longrightarrow>* Q \<and>* R') \<and>* R'') s" apply (drule drule) apply (sep_erule_full refl_imp) apply (erule sep_conj_sep_impl) apply (clarsimp simp: sep_conj_assoc) apply (sep_select_asm 1 3) apply (sep_drule (direct) sep_mp_frame, sep_erule_full refl_imp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Q' \<and>* R) s; \<And>s. Q' s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> ((P \<longrightarrow>* Q \<and>* R') \<and>* R'') s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. Q' s \<Longrightarrow> Q s; ((P \<longrightarrow>* R') \<and>* Q' \<and>* R'') s\<rbrakk> \<Longrightarrow> ((P \<longrightarrow>* Q \<and>* R') \<and>* R'') s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s. Q' s \<Longrightarrow> Q s; ((P \<longrightarrow>* R') \<and>* Q') s\<rbrakk> \<Longrightarrow> (P \<longrightarrow>* Q \<and>* R') s proof (prove)
goal (1 subgoal):
 1. \<And>s h. \<lbrakk>\<And>s. Q' s \<Longrightarrow> Q s; (((P \<longrightarrow>* R') \<and>* Q') \<and>* P) h\<rbrakk> \<Longrightarrow> (Q \<and>* R') h proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>\<And>s. Q' s \<Longrightarrow> Q s; ((P \<longrightarrow>* R') \<and>* Q' \<and>* P) h\<rbrakk> \<Longrightarrow> (Q \<and>* R') h proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>\<And>s. Q' s \<Longrightarrow> Q s; ((P \<longrightarrow>* R') \<and>* P \<and>* Q') h\<rbrakk> \<Longrightarrow> (Q \<and>* R') h proof (prove)
goal (1 subgoal):
 1. \<And>h s. \<lbrakk>\<And>s. Q' s \<Longrightarrow> Q s; Q' s\<rbrakk> \<Longrightarrow> Q s proof (prove)
goal:
No subgoals!
theory Map_Extra

lemma None_not_eq: "(None \<noteq> x) = (\<exists>y. x = Some y)" by (cases x) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (None \<noteq> x) = (\<exists>y. x = Some y)
theory Map_Extra

lemma None_com: "(None = x) = (x = None)" by fast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (None = x) = (x = None)
theory Map_Extra

lemma Some_com: "(Some y = x) = (x = Some y)" by fast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Some y = x) = (x = Some y)
theory Map_Extra

lemma empty_forall_equiv: "(m = Map.empty) = (\<forall>x. m x = None)" by (rule fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m = (\<lambda>x. None)) = (\<forall>x. m x = None)
theory Map_Extra

lemma map_le_empty2 [simp]:
  "(m \<subseteq>\<^sub>m Map.empty) = (m = Map.empty)" by (auto simp: map_le_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m \<subseteq>\<^sub>m (\<lambda>x. None)) = (m = (\<lambda>x. None))
theory Map_Extra

lemma dom_iff:
  "(\<exists>y. m x = Some y) = (x \<in> dom m)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>y. m x = Some y) = (x \<in> dom m)
theory Map_Extra

lemma non_dom_eval:
  "x \<notin> dom m \<Longrightarrow> m x = None" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> dom m \<Longrightarrow> m x = None
theory Map_Extra

lemma non_dom_eval_eq:
  "x \<notin> dom m = (m x = None)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<notin> dom m) = (m x = None)
theory Map_Extra

lemma map_add_same_left_eq:
  "m\<^sub>1 = m\<^sub>1' \<Longrightarrow> (m\<^sub>0 ++ m\<^sub>1 = m\<^sub>0 ++ m\<^sub>1')" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m\<^sub>1 = m\<^sub>1' \<Longrightarrow> m\<^sub>0 ++ m\<^sub>1 = m\<^sub>0 ++ m\<^sub>1'
theory Map_Extra

lemma map_add_left_cancelI [intro!]:
  "m\<^sub>1 = m\<^sub>1' \<Longrightarrow> m\<^sub>0 ++ m\<^sub>1 = m\<^sub>0 ++ m\<^sub>1'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m\<^sub>1 = m\<^sub>1' \<Longrightarrow> m\<^sub>0 ++ m\<^sub>1 = m\<^sub>0 ++ m\<^sub>1'