kings-crown/FVELER_Isabelle huggingface dataset:
theory Example_Valid_StateH

lemma kh0H_dom_distinct2:
  "Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> init_globals_frame"
  "Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> idle_tcb_ptr"
  "Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> High_tcb_ptr"
  "Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> Low_tcb_ptr"
  "Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> irq_cnode_ptr"
  "Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> ntfn_ptr"
  "Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> init_globals_frame"
  "Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> idle_tcb_ptr"
  "Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> High_tcb_ptr"
  "Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> Low_tcb_ptr"
  "Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> irq_cnode_ptr"
  "Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> ntfn_ptr"
  "High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> init_globals_frame"
  "High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> idle_tcb_ptr"
  "High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> High_tcb_ptr"
  "High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> Low_tcb_ptr"
  "High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> irq_cnode_ptr"
  "High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> ntfn_ptr" by (cut_tac x=x in cnode_offs_in_range2(1), fastforce simp: kh0H_dom_distinct
         | cut_tac x=x in cnode_offs_in_range2(2), fastforce simp: kh0H_dom_distinct
         | cut_tac x=x in cnode_offs_in_range2(3), fastforce simp: kh0H_dom_distinct)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> init_globals_frame &&& Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> idle_tcb_ptr) &&& Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> High_tcb_ptr &&& Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> Low_tcb_ptr) &&& (Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> irq_cnode_ptr &&& Silc_cnode_ptr + 0x10 * (x && mask 10) \<noteq> ntfn_ptr) &&& Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> init_globals_frame &&& Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> idle_tcb_ptr &&& Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> High_tcb_ptr) &&& ((Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> Low_tcb_ptr &&& Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> irq_cnode_ptr) &&& Low_cnode_ptr + 0x10 * (x && mask 10) \<noteq> ntfn_ptr &&& High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> init_globals_frame) &&& (High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> idle_tcb_ptr &&& High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> High_tcb_ptr) &&& High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> Low_tcb_ptr &&& High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> irq_cnode_ptr &&& High_cnode_ptr + 0x10 * (x && mask 10) \<noteq> ntfn_ptr
theory Example_Valid_StateH

lemma kh0H_cnode_simps2[simp]:
  "kh0H (Low_cnode_ptr + 0x10 * (x && mask 10)) = Low_cte Low_cnode_ptr (Low_cnode_ptr + 0x10 * (x && mask 10))"
  "kh0H (High_cnode_ptr + 0x10 * (x && mask 10)) = High_cte High_cnode_ptr (High_cnode_ptr + 0x10 * (x && mask 10))"
  "kh0H (Silc_cnode_ptr + 0x10 * (x && mask 10)) = Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + 0x10 * (x && mask 10))" supply option.case_cong[cong] if_cong[cong] by (clarsimp simp: kh0H_def option_update_range_def cnode_offs_in_range' s0_ptrs_aligned kh0H_dom_distinct kh0H_dom_distinct2 not_in_range_None,
         ((clarsimp simp: cnode_offs_in_range2 kh0H_dom_sets_distinct[THEN orthD1] not_in_range_None
        | clarsimp simp: cnode_offs_in_range2 kh0H_dom_sets_distinct[THEN orthD2] not_in_range_None)+),
            intro conjI,
               (clarsimp,
                drule not_disjointI,
                  (rule irq_node_offs_in_range cnode_offs_in_range2 | erule offs_in_range),
                 (rule irq_node_offs_in_range cnode_offs_in_range2 | erule offs_in_range),
                erule notE,
                rule kh0H_dom_sets_distinct
                )+,
          clarsimp split: option.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kh0H (Low_cnode_ptr + 0x10 * (x && mask 10)) = Low_cte Low_cnode_ptr (Low_cnode_ptr + 0x10 * (x && mask 10)) &&& kh0H (High_cnode_ptr + 0x10 * (x && mask 10)) = High_cte High_cnode_ptr (High_cnode_ptr + 0x10 * (x && mask 10)) &&& kh0H (Silc_cnode_ptr + 0x10 * (x && mask 10)) = Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + 0x10 * (x && mask 10)) proof (prove)
goal (1 subgoal):
 1. kh0H (Low_cnode_ptr + 0x10 * (x && mask 10)) = Low_cte Low_cnode_ptr (Low_cnode_ptr + 0x10 * (x && mask 10)) &&& kh0H (High_cnode_ptr + 0x10 * (x && mask 10)) = High_cte High_cnode_ptr (High_cnode_ptr + 0x10 * (x && mask 10)) &&& kh0H (Silc_cnode_ptr + 0x10 * (x && mask 10)) = Silc_cte Silc_cnode_ptr (Silc_cnode_ptr + 0x10 * (x && mask 10))
theory Example_Valid_StateH

lemma cnode_offs_aligned2:
  "is_aligned (Low_cnode_ptr + 0x10 * (addr && mask 10)) 4"
  "is_aligned (High_cnode_ptr + 0x10 * (addr && mask 10)) 4"
  "is_aligned (Silc_cnode_ptr + 0x10 * (addr && mask 10)) 4" by (rule is_aligned_add,
          rule is_aligned_weaken,
           rule s0_ptrs_aligned,
          simp,
         rule is_aligned_mult_triv1[where n=4, simplified])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (Low_cnode_ptr + 0x10 * (addr && mask 10)) 4 &&& is_aligned (High_cnode_ptr + 0x10 * (addr && mask 10)) 4 &&& is_aligned (Silc_cnode_ptr + 0x10 * (addr && mask 10)) 4
theory Example_Valid_StateH

lemma less_t2n_ex_ucast:
  "\<lbrakk>(x::'a::len word) < 2 ^ n; len_of TYPE('b) = n\<rbrakk> \<Longrightarrow> \<exists>y. x = ucast (y::'b::len word)" apply (rule_tac x="ucast x" in exI) apply (rule ucast_ucast_len[symmetric]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; LENGTH('b) = n\<rbrakk> \<Longrightarrow> \<exists>y. x = UCAST('b \<rightarrow> 'a) y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; LENGTH('b) = n\<rbrakk> \<Longrightarrow> x = UCAST('b \<rightarrow> 'a) (UCAST('a \<rightarrow> 'b) x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; LENGTH('b) = n\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH('b) proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma pd_offs_aligned:
  "is_aligned (Low_pd_ptr + (ucast (x::12 word) << 2)) 2"
  "is_aligned (High_pd_ptr + (ucast (x::12 word) << 2)) 2" by (rule is_aligned_add[OF _ is_aligned_shift], simp add: s0_ptr_defs is_aligned_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) x << 2)) 2 &&& is_aligned (High_pd_ptr + (UCAST(12 \<rightarrow> 32) x << 2)) 2
theory Example_Valid_StateH

lemma mdb_next_rtrancl_not_0_s0H:
  "\<lbrakk>map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>* p'; p' \<noteq> 0\<rbrakk> \<Longrightarrow> p \<noteq> 0" apply (drule rtranclD) apply clarsimp apply (simp add: mdb_next_trancl_s0H s0_ptr_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>* p'; p' \<noteq> 0\<rbrakk> \<Longrightarrow> p \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<noteq> 0; p = p' \<or> p \<noteq> p' \<and> map_to_ctes kh0H \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> p \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<noteq> 0; map_to_ctes kh0H \<turnstile> 0 \<leadsto>\<^sup>+ p'; p = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma mdb_nextI:
  "m p = Some c \<Longrightarrow> m \<turnstile> p \<leadsto> mdbNext (cteMDBNode c)" by (simp add: mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p = Some c \<Longrightarrow> m \<turnstile> p \<leadsto> mdbNext (cteMDBNode c)
theory Example_Valid_StateH

lemma shiftl_shiftr_2_word12[simp]:
  "ucast (((ucast (x:: 12 word) << 2)::word32) >> 2) = x" apply (subst shiftl_shiftr_id) apply simp apply (cut_tac ucast_less[where x=x]) apply (erule less_trans) apply simp apply simp apply (rule ucast_ucast_id) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x << 2 >> 2) = x proof (prove)
goal (3 subgoals):
 1. 2 < LENGTH(32)
 2. UCAST(12 \<rightarrow> 32) x < 2 ^ (LENGTH(32) - 2)
 3. UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x) = x proof (prove)
goal (2 subgoals):
 1. UCAST(12 \<rightarrow> 32) x < 2 ^ (LENGTH(32) - 2)
 2. UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x) = x proof (prove)
goal (3 subgoals):
 1. UCAST(12 \<rightarrow> ?'a2) x < 2 ^ LENGTH(12) \<Longrightarrow> UCAST(12 \<rightarrow> 32) x < 2 ^ (LENGTH(32) - 2)
 2. LENGTH(12) < LENGTH(?'a2)
 3. UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x) = x proof (prove)
goal (3 subgoals):
 1. 2 ^ LENGTH(12) < 2 ^ (LENGTH(32) - 2)
 2. LENGTH(12) < LENGTH(32)
 3. UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x) = x proof (prove)
goal (2 subgoals):
 1. LENGTH(12) < LENGTH(32)
 2. UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x) = x proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x) = x proof (prove)
goal (1 subgoal):
 1. LENGTH(12) < LENGTH(32) proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma shiftl_shiftr_2_word10[simp]:
  "ucast (((ucast (x:: 10 word) << 2)::word32) >> 2) = x" apply (subst shiftl_shiftr_id) apply simp apply (cut_tac ucast_less[where x=x]) apply (erule less_trans) apply simp apply simp apply (rule ucast_ucast_id) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) x << 2 >> 2) = x proof (prove)
goal (3 subgoals):
 1. 2 < LENGTH(32)
 2. UCAST(10 \<rightarrow> 32) x < 2 ^ (LENGTH(32) - 2)
 3. UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) x) = x proof (prove)
goal (2 subgoals):
 1. UCAST(10 \<rightarrow> 32) x < 2 ^ (LENGTH(32) - 2)
 2. UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) x) = x proof (prove)
goal (3 subgoals):
 1. UCAST(10 \<rightarrow> ?'a2) x < 2 ^ LENGTH(10) \<Longrightarrow> UCAST(10 \<rightarrow> 32) x < 2 ^ (LENGTH(32) - 2)
 2. LENGTH(10) < LENGTH(?'a2)
 3. UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) x) = x proof (prove)
goal (3 subgoals):
 1. 2 ^ LENGTH(10) < 2 ^ (LENGTH(32) - 2)
 2. LENGTH(10) < LENGTH(32)
 3. UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) x) = x proof (prove)
goal (2 subgoals):
 1. LENGTH(10) < LENGTH(32)
 2. UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) x) = x proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 10) (UCAST(10 \<rightarrow> 32) x) = x proof (prove)
goal (1 subgoal):
 1. LENGTH(10) < LENGTH(32) proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma shiftl_shiftr_2_word8[simp]:
  "ucast (((ucast (x:: 8 word) << 2)::word32) >> 2) = x" apply (subst shiftl_shiftr_id) apply simp apply (cut_tac ucast_less[where x=x]) apply (erule less_trans) apply simp apply simp apply (rule ucast_ucast_id) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) x << 2 >> 2) = x proof (prove)
goal (3 subgoals):
 1. 2 < LENGTH(32)
 2. UCAST(8 \<rightarrow> 32) x < 2 ^ (LENGTH(32) - 2)
 3. UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) x) = x proof (prove)
goal (2 subgoals):
 1. UCAST(8 \<rightarrow> 32) x < 2 ^ (LENGTH(32) - 2)
 2. UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) x) = x proof (prove)
goal (3 subgoals):
 1. UCAST(8 \<rightarrow> ?'a2) x < 2 ^ LENGTH(8) \<Longrightarrow> UCAST(8 \<rightarrow> 32) x < 2 ^ (LENGTH(32) - 2)
 2. LENGTH(8) < LENGTH(?'a2)
 3. UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) x) = x proof (prove)
goal (3 subgoals):
 1. 2 ^ LENGTH(8) < 2 ^ (LENGTH(32) - 2)
 2. LENGTH(8) < LENGTH(32)
 3. UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) x) = x proof (prove)
goal (2 subgoals):
 1. LENGTH(8) < LENGTH(32)
 2. UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) x) = x proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) x) = x proof (prove)
goal (1 subgoal):
 1. LENGTH(8) < LENGTH(32) proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma mult_shiftr_id[simp]:
  "length x = 10 \<Longrightarrow> of_bl x * (0x10::word32) >> 4 = of_bl x" apply (simp add: shiftl_t2n[symmetric, where n=4, simplified mult.commute, simplified] ) apply (subst shiftl_shiftr_id) apply simp apply (rule less_trans) apply (rule of_bl_length_less) apply assumption apply simp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length x = 10 \<Longrightarrow> of_bl x * 0x10 >> 4 = of_bl x proof (prove)
goal (1 subgoal):
 1. length x = 10 \<Longrightarrow> of_bl x << 4 >> 4 = of_bl x proof (prove)
goal (3 subgoals):
 1. length x = 10 \<Longrightarrow> 4 < LENGTH(32)
 2. length x = 10 \<Longrightarrow> of_bl x < 2 ^ (LENGTH(32) - 4)
 3. length x = 10 \<Longrightarrow> of_bl x = of_bl x proof (prove)
goal (2 subgoals):
 1. length x = 10 \<Longrightarrow> of_bl x < 2 ^ (LENGTH(32) - 4)
 2. length x = 10 \<Longrightarrow> of_bl x = of_bl x proof (prove)
goal (3 subgoals):
 1. length x = 10 \<Longrightarrow> of_bl x < ?y1
 2. length x = 10 \<Longrightarrow> ?y1 < 2 ^ (LENGTH(32) - 4)
 3. length x = 10 \<Longrightarrow> of_bl x = of_bl x proof (prove)
goal (4 subgoals):
 1. length x = 10 \<Longrightarrow> length x = ?k4
 2. length x = 10 \<Longrightarrow> ?k4 < LENGTH(32)
 3. length x = 10 \<Longrightarrow> 2 ^ ?k4 < 2 ^ (LENGTH(32) - 4)
 4. length x = 10 \<Longrightarrow> of_bl x = of_bl x proof (prove)
goal (3 subgoals):
 1. length x = 10 \<Longrightarrow> 10 < LENGTH(32)
 2. length x = 10 \<Longrightarrow> 2 ^ 10 < 2 ^ (LENGTH(32) - 4)
 3. length x = 10 \<Longrightarrow> of_bl x = of_bl x proof (prove)
goal (2 subgoals):
 1. length x = 10 \<Longrightarrow> 2 ^ 10 < 2 ^ (LENGTH(32) - 4)
 2. length x = 10 \<Longrightarrow> of_bl x = of_bl x proof (prove)
goal (1 subgoal):
 1. length x = 10 \<Longrightarrow> of_bl x = of_bl x proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma to_bl_ucast_of_bl[simp]:
  "length x = 10 \<Longrightarrow> to_bl ((ucast ((of_bl x)::word32))::10 word) = x" apply (subst ucast_of_bl_up) apply (simp add: word_size) apply (simp add: word_rep_drop) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length x = 10 \<Longrightarrow> to_bl (UCAST(32 \<rightarrow> 10) (of_bl x)) = x proof (prove)
goal (2 subgoals):
 1. length x = 10 \<Longrightarrow> length x \<le> size (of_bl x)
 2. length x = 10 \<Longrightarrow> to_bl (of_bl x) = x proof (prove)
goal (1 subgoal):
 1. length x = 10 \<Longrightarrow> to_bl (of_bl x) = x proof (prove)
goal:
No subgoals!
theory Example_Valid_StateH

lemma subtree_node_Some:
  "m \<turnstile> a \<rightarrow> b \<Longrightarrow> m a \<noteq> None" by (erule subtree.cases) (auto simp: parentOf_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> a \<rightarrow> b \<Longrightarrow> m a \<noteq> None
theory Example_Valid_StateH

lemma Sys1_valid_initial_state_noenabled:
  assumes domains: "1 \<le> maxDomain"
  assumes utf_det: "\<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s
                   \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})"
  assumes utf_non_empty: "\<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}"
  assumes utf_non_interrupt: "\<forall>t pl pr pxn tc ms e f g. (e,f,g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt"
  assumes det_inv_invariant: "invariant_over_ADT_if det_inv utf"
  assumes det_inv_s0: "det_inv KernelExit (cur_context s0_internal) s0_internal"
  shows "valid_initial_state_noenabled det_inv utf s0_internal Sys1PAS timer_irq s0_context" by (rule Sys1_valid_initial_state_noenabled[OF step_restrict_s0 utf_det utf_non_empty
                                                 utf_non_interrupt det_inv_invariant det_inv_s0
                                                 ],
      rule domains)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_initial_state_noenabled det_inv utf s0_internal Sys1PAS timer_irq s0_context
theory Arbitrary_Comm_Monoid

lemma idem_comm_monoid_not_canc:
  "((x :: 'a) \<noteq> e) \<Longrightarrow> idem_comm_monoid f (e :: 'a :: times) \<Longrightarrow> \<not> canc_comm_monoid f e" apply (clarsimp simp: idem_comm_monoid_def canc_comm_monoid_def canc_comm_monoid_axioms_def
                        idem_comm_monoid_axioms_def) apply (rule_tac x="x" in exI) apply (rule_tac x="x" in exI) apply (rule_tac x="e" in exI) apply (erule_tac x=x in allE, clarsimp) apply (clarsimp simp: comm_monoid_def comm_monoid_axioms_def abel_semigroup_def
                        abel_semigroup_axioms_def semigroup_def) by metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> e; idem_comm_monoid f e\<rbrakk> \<Longrightarrow> \<not> canc_comm_monoid f e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> e; comm_monoid f e; \<forall>a. f a a = a\<rbrakk> \<Longrightarrow> \<exists>a b c. f a b = f a c \<and> b \<noteq> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> e; comm_monoid f e; \<forall>a. f a a = a\<rbrakk> \<Longrightarrow> \<exists>b c. f x b = f x c \<and> b \<noteq> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> e; comm_monoid f e; \<forall>a. f a a = a\<rbrakk> \<Longrightarrow> \<exists>c. f x x = f x c \<and> x \<noteq> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> e; comm_monoid f e; \<forall>a. f a a = a\<rbrakk> \<Longrightarrow> f x x = f x e \<and> x \<noteq> e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> e; comm_monoid f e; f x x = x\<rbrakk> \<Longrightarrow> x = f x e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> e; f x x = x; \<forall>a b c. f c (f a b) = f a (f b c); \<forall>a b. f a b = f b a; \<forall>a. f a e = a\<rbrakk> \<Longrightarrow> x = f e x
theory Separation_Algebra

lemma sep_disj_commute: "x ## y = y ## x" by (blast intro: sep_disj_commuteI)

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

lemma sep_add_left_commute:
  assumes a: "a ## b" "b ## c" "a ## c"
  shows "b + (a + c) = a + (b + c)" (is "?lhs = ?rhs") proof - have "?lhs = b + a + c" using a by (simp add: sep_add_assoc[symmetric] sep_disj_commute) also have "... = a + b + c" using a by (simp add: sep_add_commute sep_disj_commute) also have "... = ?rhs" using a by (simp add: sep_add_assoc sep_disj_commute) finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b + (a + c) = a + (b + c) proof (state)
goal (1 subgoal):
 1. b + (a + c) = a + (b + c) proof (prove)
goal (1 subgoal):
 1. b + (a + c) = b + a + c proof (prove)
using this:
a ## b
b ## c
a ## c

goal (1 subgoal):
 1. b + (a + c) = b + a + c proof (state)
this:
b + (a + c) = b + a + c

goal (1 subgoal):
 1. b + (a + c) = a + (b + c) proof (state)
this:
b + (a + c) = b + a + c

goal (1 subgoal):
 1. b + (a + c) = a + (b + c) proof (prove)
goal (1 subgoal):
 1. b + a + c = a + b + c proof (prove)
using this:
a ## b
b ## c
a ## c

goal (1 subgoal):
 1. b + a + c = a + b + c proof (state)
this:
b + a + c = a + b + c

goal (1 subgoal):
 1. b + (a + c) = a + (b + c) proof (state)
this:
b + a + c = a + b + c

goal (1 subgoal):
 1. b + (a + c) = a + (b + c) proof (prove)
goal (1 subgoal):
 1. a + b + c = a + (b + c) proof (prove)
using this:
a ## b
b ## c
a ## c

goal (1 subgoal):
 1. a + b + c = a + (b + c) proof (state)
this:
a + b + c = a + (b + c)

goal (1 subgoal):
 1. b + (a + c) = a + (b + c) proof (chain)
picking this:
b + (a + c) = a + (b + c) proof (prove)
using this:
b + (a + c) = a + (b + c)

goal (1 subgoal):
 1. b + (a + c) = a + (b + c) proof (state)
this:
b + (a + c) = a + (b + c)

goal:
No subgoals!
theory Separation_Algebra

lemma disjoint_zero_sym [simp]: "0 ## x" by (simp add: sep_disj_commute)

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

lemma sep_add_zero_sym [simp]: "0 + x = x" by (simp add: sep_add_commute)

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

lemma sep_disj_addD2: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## z" by (metis sep_add_commute sep_disj_addD1 sep_disj_commuteI)

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

lemma sep_disj_addD: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## y \<and> x ## z" by (metis sep_disj_addD1 sep_disj_addD2)

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

lemma sep_add_disjD: "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## z \<and> y ## z" by (metis sep_disj_addD sep_disj_commuteI)

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

lemma sep_disj_addI2:
  "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x + z ## y" using sep_add_commute sep_disj_addI1 sep_disj_commuteI by presburger

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

goal (1 subgoal):
 1. \<lbrakk>x ## y + z; y ## z\<rbrakk> \<Longrightarrow> x + z ## y
theory Separation_Algebra

lemma sep_add_disjI1:
  "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x + z ## y" by (metis sep_add_commute sep_disj_addI1 sep_disj_commuteI sep_add_disjD)

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

lemma sep_add_disjI2:
  "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> z + y ## x" by (metis sep_add_commute sep_disj_addI1 sep_disj_commuteI sep_add_disjD)

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

lemma sep_disj_addI3:
  "x + y ## z \<Longrightarrow> x ## y \<Longrightarrow> x ## y + z" by (metis sep_add_commute sep_disj_addI1 sep_disj_commuteI sep_add_disjD)

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

lemma sep_disj_add:
  "\<lbrakk> y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## y + z = x + y ## z" by (metis sep_disj_addI1 sep_disj_addI3)

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

lemma sep_substate_disj_add:
  "x ## y \<Longrightarrow> x \<preceq> x + y" unfolding sep_substate_def by blast

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

lemma sep_substate_disj_add':
  "x ## y \<Longrightarrow> x \<preceq> y + x" by (simp add: sep_add_ac sep_substate_disj_add)

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

lemma sep_conjE:
  "\<lbrakk> (P ** Q) h; \<And>x y. \<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> X \<rbrakk> \<Longrightarrow> X" by (auto simp: sep_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P \<and>* Q) h; \<And>x y. \<lbrakk>P x; Q y; x ## y; h = x + y\<rbrakk> \<Longrightarrow> X\<rbrakk> \<Longrightarrow> X
theory Separation_Algebra

lemma sep_conjI:
  "\<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> (P ** Q) h" by (auto simp: sep_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P x; Q y; x ## y; h = x + y\<rbrakk> \<Longrightarrow> (P \<and>* Q) h