kings-crown/FVELER_Isabelle huggingface dataset:
theory Machine_Word_64

lemma ucast_not_helper:
  fixes a::"8 word"
  assumes a: "a \<noteq> 0xFF"
  shows "ucast a \<noteq> (0xFF::machine_word)" proof assume "ucast a = (0xFF::machine_word)" also have "(0xFF::machine_word) = ucast (0xFF::8 word)" by simp finally show False using a apply - apply (drule up_ucast_inj, simp) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 64) a \<noteq> 255 proof (state)
goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 64) a = 255 \<Longrightarrow> False proof (state)
this:
UCAST(8 \<rightarrow> 64) a = 255

goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 64) a = 255 \<Longrightarrow> False proof (state)
this:
UCAST(8 \<rightarrow> 64) a = 255

goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 64) a = 255 \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. 255 = UCAST(8 \<rightarrow> 64) 255 proof (state)
this:
255 = UCAST(8 \<rightarrow> 64) 255

goal (1 subgoal):
 1. UCAST(8 \<rightarrow> 64) a = 255 \<Longrightarrow> False proof (chain)
picking this:
UCAST(8 \<rightarrow> 64) a = UCAST(8 \<rightarrow> 64) 255 proof (prove)
using this:
UCAST(8 \<rightarrow> 64) a = UCAST(8 \<rightarrow> 64) 255

goal (1 subgoal):
 1. False proof (prove)
using this:
UCAST(8 \<rightarrow> 64) a = UCAST(8 \<rightarrow> 64) 255
a \<noteq> 255

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST(8 \<rightarrow> 64) a = UCAST(8 \<rightarrow> 64) 255; a \<noteq> 255\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> 255; a = 255\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
False

goal:
No subgoals!
theory Machine_Word_64

lemma unat_less_2p_word_bits:
  "unat (x :: machine_word) < 2 ^ word_bits" apply (simp only: word_bits_def) apply (rule unat_lt2p) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ LENGTH(64) proof (prove)
goal:
No subgoals!
theory Machine_Word_64

lemma unat_less_word_bits:
  fixes y :: machine_word
  shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits" unfolding word_bits_def by (rule order_less_trans [OF _ unat_lt2p])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < unat y \<Longrightarrow> x < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. x < unat y \<Longrightarrow> x < 2 ^ LENGTH(64)
theory Machine_Word_64

lemma unat_mask_2_less_4:
  "unat (p AND mask 2 :: machine_word) < 4" by (rule unat_less_helper) (simp only: take_bit_eq_mod word_mod_less_divisor flip: take_bit_eq_mask, simp add: word_mod_less_divisor)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (p && mask 2) < 4
theory Machine_Word_64

lemma unat_mult_simple:
  \<open>unat (x * y) = unat x * unat y\<close>
    if \<open>unat x * unat y < 2 ^ LENGTH(machine_word_len)\<close>
    for x y :: machine_word using that by (simp flip: unat_mult_lem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (x * y) = unat x * unat y proof (prove)
using this:
unat x * unat y < 2 ^ LENGTH(64)

goal (1 subgoal):
 1. unat (x * y) = unat x * unat y
theory Machine_Word_64

lemma upto_2_helper:
  "{0..<2 :: machine_word} = {0, 1}" by (safe; simp) unat_arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {0..<2} = {0, 1}
theory Machine_Word_64

lemma word_ge_min:
  \<open>- (2 ^ (word_bits - 1)) \<le> sint x\<close> for x :: machine_word using sint_ge [of x] by (simp add: word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - (2 ^ (word_bits - 1)) \<le> sint x proof (prove)
using this:
- (2 ^ (LENGTH(64) - 1)) \<le> sint x

goal (1 subgoal):
 1. - (2 ^ (word_bits - 1)) \<le> sint x
theory Machine_Word_64

lemma word_rsplit_0:
  "word_rsplit (0::machine_word) = [0, 0, 0, 0, 0, 0, 0, (0::8 word)]" by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rsplit 0 = [0, 0, 0, 0, 0, 0, 0, 0]
theory Guide

lemma bit_eq_iff:
  \<open>a = b \<longleftrightarrow> (\<forall>n. 2 ^ n \<noteq> 0 \<longrightarrow> bit a n \<longleftrightarrow> bit b n)\<close> using bit_eq_iff [of a b] by (simp add: possible_bit_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a = b) = (\<forall>n. (2::'a) ^ n \<noteq> (0::'a) \<longrightarrow> a !! n = b !! n) proof (prove)
using this:
(a = b) = (\<forall>n. possible_bit TYPE('a) n \<longrightarrow> a !! n = b !! n)

goal (1 subgoal):
 1. (a = b) = (\<forall>n. (2::'a) ^ n \<noteq> (0::'a) \<longrightarrow> a !! n = b !! n)
theory Sep_Cancel_Example

lemma "(A \<and>* B \<and>* C \<and>* D) s \<Longrightarrow> (C \<and>* D \<and>* A \<and>* B) s" apply sep_cancel apply sep_cancel done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* D) s \<Longrightarrow> (C \<and>* D \<and>* A \<and>* B) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (A \<and>* B \<and>* D) s \<Longrightarrow> (D \<and>* A \<and>* B) s proof (prove)
goal:
No subgoals!
theory Separation_Algebra_Alt

lemma disj_com: "x ## y = y ## x" by (auto simp: disjoint_def add_comm)

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

lemma disj_zero [simp]: "x ## 0" by (auto simp: disjoint_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x ## (0::'a)
theory Separation_Algebra_Alt

lemma disj_zero2 [simp]: "0 ## x" by (subst disj_com) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0::'a) ## x
theory Separation_Algebra_Alt

lemma add_zero2 [simp]: "0 \<oplus> x = Some x" by (subst add_comm) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<oplus> x = Some x
theory Separation_Algebra_Alt

lemma add2_comm:
  "a ++ b = b ++ a" by (simp add: lift2_def add_comm split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a ++ b = b ++ a
theory Separation_Algebra_Alt

lemma add2_None [simp]:
  "x ++ None = None" by (simp add: lift2_def split: option.splits)

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

lemma add2_zero [simp]:
  "Some x ++ Some 0 = Some x" by (simp add: add2_Some_Some)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Some x ++ Some (0::'a) = Some x
theory Separation_Algebra_Alt

lemma zero_add2 [simp]:
  "Some 0 ++ Some x = Some x" by (simp add: add2_Some_Some)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Some (0::'a) ++ Some x = Some x
theory Separation_Algebra_Alt

lemma sep_conjE:
  "\<lbrakk> (P ** Q) s; \<And>p q. \<lbrakk> P p; Q q; p \<oplus> q = Some s \<rbrakk> \<Longrightarrow> X \<rbrakk> \<Longrightarrow> X" by (auto simp: sep_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P ** Q) s; \<And>p q. \<lbrakk>P p; Q q; p \<oplus> q = Some s\<rbrakk> \<Longrightarrow> X\<rbrakk> \<Longrightarrow> X
theory Separation_Algebra_Alt

lemma sep_conjI:
  "\<lbrakk> P p; Q q; p \<oplus> q = Some s \<rbrakk> \<Longrightarrow> (P ** Q) s" by (auto simp: sep_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P p; Q q; p \<oplus> q = Some s\<rbrakk> \<Longrightarrow> (P ** Q) s
theory Separation_Algebra_Alt

lemma sep_conj_comI:
  "(P ** Q) s \<Longrightarrow> (Q ** P) s" by (auto intro!: sep_conjI elim!: sep_conjE simp: add_comm)

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

lemma sep_conj_com:
  "P ** Q = Q ** P" by (auto intro: sep_conj_comI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P ** Q = Q ** P
theory Separation_Algebra_Alt

lemma lift_to_add2:
  "\<lbrakk>z \<oplus> q = Some s; x \<oplus> y = Some q\<rbrakk> \<Longrightarrow> Some z ++ Some x ++ Some y = Some s" by (simp add: add2_Some_Some)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<oplus> q = Some s; x \<oplus> y = Some q\<rbrakk> \<Longrightarrow> Some z ++ Some x ++ Some y = Some s
theory Separation_Algebra_Alt

lemma lift_to_add2':
  "\<lbrakk>q \<oplus> z = Some s; x \<oplus> y = Some q\<rbrakk> \<Longrightarrow> (Some x ++ Some y) ++ Some z = Some s" by (simp add: add2_Some_Some)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q \<oplus> z = Some s; x \<oplus> y = Some q\<rbrakk> \<Longrightarrow> (Some x ++ Some y) ++ Some z = Some s
theory Separation_Algebra_Alt

lemma add2_Some:
  "(x ++ Some y = Some z) = (\<exists>x'. x = Some x' \<and> x' \<oplus> y = Some z)" by (simp add: lift2_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x ++ Some y = Some z) = (\<exists>x'. x = Some x' \<and> x' \<oplus> y = Some z)
theory Separation_Algebra_Alt

lemma Some_add2:
  "(Some x ++ y = Some z) = (\<exists>y'. y = Some y' \<and> x \<oplus> y' = Some z)" by (simp add: lift2_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Some x ++ y = Some z) = (\<exists>y'. y = Some y' \<and> x \<oplus> y' = Some z)
theory Separation_Algebra_Alt

lemma sep_true[simp]: "sep_true s" by (simp add: sep_true_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_true s
theory Separation_Algebra_Alt

lemma sep_false[simp]: "\<not>sep_false x" by (simp add: sep_false_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> sep_false x
theory Separation_Algebra_Alt

lemma sep_conj_sep_true:
  "P s \<Longrightarrow> (P ** sep_true) s" by (auto simp: sep_conjI [where q=0])

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

lemma sep_conj_sep_true':
  "P s \<Longrightarrow> (sep_true ** P) s" by (auto simp: sep_conjI [where p=0])

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

lemma disjoint_submaps_exist:
  "\<exists>h\<^sub>0 h\<^sub>1. h\<^sub>0 \<oplus> h\<^sub>1 = Some h" by (rule_tac x=0 in exI, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>h\<^sub>0 h\<^sub>1. h\<^sub>0 \<oplus> h\<^sub>1 = Some h
theory Separation_Algebra_Alt

lemma sep_conj_true[simp]:
  "(sep_true ** sep_true) = sep_true" unfolding sep_conj_def by (auto intro: disjoint_submaps_exist)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_true ** sep_true = sep_true proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<exists>p q. p \<oplus> q = Some s \<and> sep_true p \<and> sep_true q) = sep_true
theory Separation_Algebra_Alt

lemma sep_conj_false_right[simp]:
  "(P ** sep_false) = sep_false" by (force elim: sep_conjE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P ** sep_false = sep_false
theory Separation_Algebra_Alt

lemma sep_conj_false_left[simp]:
  "(sep_false ** P) = sep_false" by (subst sep_conj_com) (rule sep_conj_false_right)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_false ** P = sep_false
theory Separation_Algebra_Alt

lemma sep_conj_left_com:
  "(P ** (Q ** R)) = (Q ** (P ** R))" (is "?x = ?y") proof - have "?x = ((Q ** R) ** P)" by (simp add: sep_conj_com) also have "\<dots> = (Q ** (R ** P))" by (subst sep_conj_assoc, simp) finally show ?thesis by (simp add: sep_conj_com) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P ** (Q ** R) = Q ** (P ** R) proof (state)
goal (1 subgoal):
 1. P ** (Q ** R) = Q ** (P ** R) proof (prove)
goal (1 subgoal):
 1. P ** (Q ** R) = Q ** R ** P proof (state)
this:
P ** (Q ** R) = Q ** R ** P

goal (1 subgoal):
 1. P ** (Q ** R) = Q ** (P ** R) proof (state)
this:
P ** (Q ** R) = Q ** R ** P

goal (1 subgoal):
 1. P ** (Q ** R) = Q ** (P ** R) proof (prove)
goal (1 subgoal):
 1. Q ** R ** P = Q ** (R ** P) proof (state)
this:
Q ** R ** P = Q ** (R ** P)

goal (1 subgoal):
 1. P ** (Q ** R) = Q ** (P ** R) proof (chain)
picking this:
P ** (Q ** R) = Q ** (R ** P) proof (prove)
using this:
P ** (Q ** R) = Q ** (R ** P)

goal (1 subgoal):
 1. P ** (Q ** R) = Q ** (P ** R) proof (state)
this:
P ** (Q ** R) = Q ** (P ** R)

goal:
No subgoals!
theory Separation_Algebra_Alt

lemma empty_empty[simp]: "\<box> 0" by (simp add: emp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<box> (0::'a)
theory Separation_Algebra_Alt

lemma sep_conj_empty[simp]:
  "(P ** \<box>) = P" by (simp add: sep_conj_def emp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P ** \<box> = P
theory Separation_Algebra_Alt

lemma sep_conj_empty'[simp]:
  "(\<box> ** P) = P" by (subst sep_conj_com, rule sep_conj_empty)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<box> ** P = P
theory Separation_Algebra_Alt

lemma sep_conj_sep_emptyI:
  "P s \<Longrightarrow> (P ** \<box>) s" by simp

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

lemma sep_conj_true_P[simp]:
  "(sep_true ** (sep_true ** P)) = (sep_true ** P)" by (simp add: sep_conj_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_true ** (sep_true ** P) = sep_true ** P
theory Separation_Algebra_Alt

lemma sep_conj_disj:
  "((\<lambda>s. P s \<or> Q s) ** R) s = ((P ** R) s \<or> (Q ** R) s)" (is "?x = (?y \<or> ?z)") by (auto simp: sep_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. P s \<or> Q s) ** R) s = ((P ** R) s \<or> (Q ** R) s)
theory Separation_Algebra_Alt

lemma sep_conj_conj:
  "((\<lambda>s. P s \<and> Q s) ** R) s \<Longrightarrow> (P ** R) s \<and> (Q ** R) s" by (force intro: sep_conjI elim!: sep_conjE)

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

lemma sep_conj_exists1:
  "((\<lambda>s. \<exists>x. P x s) ** Q) s = (\<exists>x. (P x ** Q) s)" by (force intro: sep_conjI elim: sep_conjE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. \<exists>x. P x s) ** Q) s = (\<exists>x. (P x ** Q) s)
theory Separation_Algebra_Alt

lemma sep_conj_exists2:
  "(P ** (\<lambda>s. \<exists>x. Q x s)) = (\<lambda>s. (\<exists>x. (P ** Q x) s))" by (force intro!: sep_conjI elim!: sep_conjE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P ** (\<lambda>s. \<exists>x. Q x s) = (\<lambda>s. \<exists>x. (P ** Q x) s)
theory Separation_Algebra_Alt

lemma sep_conj_forall:
  "((\<lambda>s. \<forall>x. P x s) ** Q) s \<Longrightarrow> (P x ** Q) s" by (force intro: sep_conjI elim: sep_conjE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. \<forall>x. P x s) ** Q) s \<Longrightarrow> (P x ** Q) s
theory Separation_Algebra_Alt

lemma sep_conj_impl1:
  assumes P: "\<And>s. P s \<Longrightarrow> I s"
  shows "(P ** R) s \<Longrightarrow> (I ** R) s" by (auto intro: sep_conj_impl P)

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

lemma sep_conj_sep_true_left:
  "(P ** Q) s \<Longrightarrow> (sep_true ** Q) s" by (erule sep_conj_impl, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P ** Q) s \<Longrightarrow> (sep_true ** Q) s
theory Separation_Algebra_Alt

lemma sep_conj_sep_true_right:
  "(P ** Q) s \<Longrightarrow> (P ** sep_true) s" by (subst (asm) sep_conj_com, drule sep_conj_sep_true_left,
      simp add: sep_conj_ac)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P ** Q) s \<Longrightarrow> (P ** sep_true) s
theory Separation_Algebra_Alt

lemma sep_implI:
  assumes a: "\<And>h' h''. \<lbrakk> h \<oplus> h' = Some h''; P h' \<rbrakk> \<Longrightarrow> Q h''"
  shows "(P \<longrightarrow>\<^sup>* Q) h" unfolding sep_impl_def by (auto elim: a)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<longrightarrow>\<^sup>* Q) h proof (prove)
goal (1 subgoal):
 1. \<forall>h' h''. h \<oplus> h' = Some h'' \<and> P h' \<longrightarrow> Q h''
theory Separation_Algebra_Alt

lemma sep_implD:
  "(x \<longrightarrow>\<^sup>* y) h \<Longrightarrow> \<forall>h' h''. h \<oplus> h' = Some h'' \<and> x h' \<longrightarrow> y h''" by (force simp: sep_impl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<longrightarrow>\<^sup>* y) h \<Longrightarrow> \<forall>h' h''. h \<oplus> h' = Some h'' \<and> x h' \<longrightarrow> y h''
theory Separation_Algebra_Alt

lemma sep_impl_sep_true[simp]:
  "(P \<longrightarrow>\<^sup>* sep_true) = sep_true" by (force intro!: sep_implI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<longrightarrow>\<^sup>* sep_true) = sep_true
theory Separation_Algebra_Alt

lemma sep_impl_sep_false[simp]:
  "(sep_false \<longrightarrow>\<^sup>* P) = sep_true" by (force intro!: sep_implI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sep_false \<longrightarrow>\<^sup>* P) = sep_true
theory Separation_Algebra_Alt

lemma sep_impl_sep_true_P:
  "(sep_true \<longrightarrow>\<^sup>* P) s \<Longrightarrow> P s" apply (drule sep_implD) apply (erule_tac x=0 in allE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sep_true \<longrightarrow>\<^sup>* P) s \<Longrightarrow> P s proof (prove)
goal (1 subgoal):
 1. \<forall>h' h''. s \<oplus> h' = Some h'' \<and> sep_true h' \<longrightarrow> P h'' \<Longrightarrow> P s proof (prove)
goal (1 subgoal):
 1. \<forall>h''. s \<oplus> (0::'a) = Some h'' \<and> sep_true (0::'a) \<longrightarrow> P h'' \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Separation_Algebra_Alt

lemma sep_impl_sep_true_false[simp]:
  "(sep_true \<longrightarrow>\<^sup>* sep_false) = sep_false" by (force dest: sep_impl_sep_true_P)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sep_true \<longrightarrow>\<^sup>* sep_false) = sep_false
theory Separation_Algebra_Alt

lemma sep_conj_sep_impl:
  "\<lbrakk> P s; \<And>s. (P ** Q) s \<Longrightarrow> R s \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>\<^sup>* R) s" proof (rule sep_implI) fix h' h h'' assume "P h" and "h \<oplus> h' = Some h''" and "Q h'" hence "(P ** Q) h''" by (force intro: sep_conjI) moreover assume "\<And>s. (P ** Q) s \<Longrightarrow> R s" ultimately show "R h''" by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s; \<And>s. (P ** Q) s \<Longrightarrow> R s\<rbrakk> \<Longrightarrow> (Q \<longrightarrow>\<^sup>* R) s proof (state)
goal (1 subgoal):
 1. \<And>h' h''. \<lbrakk>P s; \<And>s. (P ** Q) s \<Longrightarrow> R s; s \<oplus> h' = Some h''; Q h'\<rbrakk> \<Longrightarrow> R h'' proof (state)
goal (1 subgoal):
 1. \<And>h' h''. \<lbrakk>P s; \<And>s. (P ** Q) s \<Longrightarrow> R s; s \<oplus> h' = Some h''; Q h'\<rbrakk> \<Longrightarrow> R h'' proof (state)
this:
P h
h \<oplus> h' = Some h''
Q h'

goal (1 subgoal):
 1. \<And>h' h''. \<lbrakk>P s; \<And>s. (P ** Q) s \<Longrightarrow> R s; s \<oplus> h' = Some h''; Q h'\<rbrakk> \<Longrightarrow> R h'' proof (prove)
using this:
P h
h \<oplus> h' = Some h''
Q h'

goal (1 subgoal):
 1. (P ** Q) h'' proof (state)
this:
(P ** Q) h''

goal (1 subgoal):
 1. \<And>h' h''. \<lbrakk>P s; \<And>s. (P ** Q) s \<Longrightarrow> R s; s \<oplus> h' = Some h''; Q h'\<rbrakk> \<Longrightarrow> R h'' proof (state)
this:
(P ** Q) h''

goal (1 subgoal):
 1. \<And>h' h''. \<lbrakk>P s; \<And>s. (P ** Q) s \<Longrightarrow> R s; s \<oplus> h' = Some h''; Q h'\<rbrakk> \<Longrightarrow> R h'' proof (state)
this:
(P ** Q) ?s \<Longrightarrow> R ?s

goal (1 subgoal):
 1. \<And>h' h''. \<lbrakk>P s; \<And>s. (P ** Q) s \<Longrightarrow> R s; s \<oplus> h' = Some h''; Q h'\<rbrakk> \<Longrightarrow> R h'' proof (chain)
picking this:
(P ** Q) h''
(P ** Q) ?s \<Longrightarrow> R ?s proof (prove)
using this:
(P ** Q) h''
(P ** Q) ?s \<Longrightarrow> R ?s

goal (1 subgoal):
 1. R h'' proof (state)
this:
R h''

goal:
No subgoals!
theory Separation_Algebra_Alt

lemma sep_conj_sep_impl2:
  "\<lbrakk> (P ** Q) s; \<And>s. P s \<Longrightarrow> (Q \<longrightarrow>\<^sup>* R) s \<rbrakk> \<Longrightarrow> R s" by (force dest: sep_implD elim: sep_conjE)

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

lemma sep_conj_sep_impl_sep_conj2:
  "(P ** R) s \<Longrightarrow> (P ** (Q \<longrightarrow>\<^sup>* (Q ** R))) s" by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P ** R) s \<Longrightarrow> (P ** (Q \<longrightarrow>\<^sup>* Q ** R)) s
theory Separation_Algebra_Alt

lemma sep_conj_triv_strip2:
  "Q = R \<Longrightarrow> (Q ** P) = (R ** P)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q = R \<Longrightarrow> Q ** P = R ** P
theory Sep_Eq

lemma add2_comm: "add2 x y = add2 y x" by (auto simp: add2_def sep_add_commute sep_disj_commute)

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

lemma add2_assoc:
  "lift2 add2 a (lift2 add2 b c) = lift2 add2 (lift2 add2 a b) c" by (auto simp: add2_def lift2_def sep_add_assoc
              dest: sep_disj_addD sep_disj_addI3
                    sep_add_disjD sep_disj_addI2 sep_disj_commuteI
              split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift2 Sep_Eq.add2 a (lift2 Sep_Eq.add2 b c) = lift2 Sep_Eq.add2 (lift2 Sep_Eq.add2 a b) c
theory Sep_Eq

lemma sep_disj_zero':
  "disjoint x 0" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x ## (0::'a)
theory Sep_Eq

lemma sep_disj_commuteI':
  "disjoint x y \<Longrightarrow> disjoint y x" by (clarsimp simp: disjoint_def add_comm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x ## y \<Longrightarrow> y ## x
theory Sep_Eq

lemma sep_add_zero':
  "sep_add' x 0 = x" by (simp add: sep_add'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_add' x (0::'a) = x
theory Sep_Eq

lemma sep_add_commute':
  "disjoint x y \<Longrightarrow> sep_add' x y = sep_add' y x" by (clarsimp simp: sep_add'_def disjoint_def add_comm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x ## y \<Longrightarrow> sep_add' x y = sep_add' y x
theory Sep_Eq

lemma sep_add_assoc':
  "\<lbrakk> disjoint x y; disjoint y z; disjoint x z \<rbrakk> \<Longrightarrow>
  sep_add' (sep_add' x y) z = sep_add' x (sep_add' y z)" using add_assoc [of "Some x" "Some y" "Some z"] by (clarsimp simp: disjoint_def sep_add'_def lift2_def
               split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x ## y; y ## z; x ## z\<rbrakk> \<Longrightarrow> sep_add' (sep_add' x y) z = sep_add' x (sep_add' y z) proof (prove)
using this:
Some x ++ Some y ++ Some z = (Some x ++ Some y) ++ Some z

goal (1 subgoal):
 1. \<lbrakk>x ## y; y ## z; x ## z\<rbrakk> \<Longrightarrow> sep_add' (sep_add' x y) z = sep_add' x (sep_add' y z)