kings-crown/FVELER_Isabelle huggingface dataset:
theory Sep_Tactic_Examples

lemma "(A \<and>* B \<and>* C \<and>* D) s  \<Longrightarrow>  (A \<and>* B \<and>* C \<and>* D) s" apply (sep_select 4) apply (sep_select_asm 3) apply (sep_select 2) apply (sep_cancel) 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> (A \<and>* B \<and>* C \<and>* D) s proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* D) s \<Longrightarrow> (D \<and>* A \<and>* B \<and>* C) s proof (prove)
goal (1 subgoal):
 1. (C \<and>* A \<and>* B \<and>* D) s \<Longrightarrow> (D \<and>* A \<and>* B \<and>* C) s proof (prove)
goal (1 subgoal):
 1. (C \<and>* A \<and>* B \<and>* D) s \<Longrightarrow> (A \<and>* D \<and>* B \<and>* C) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (C \<and>* B \<and>* D) s \<Longrightarrow> (D \<and>* B \<and>* C) s proof (prove)
goal (1 subgoal):
 1. \<And>s sa. (C \<and>* B) sa \<Longrightarrow> (B \<and>* C) sa proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma example_drule:
  "(ptr \<mapsto>o obj) s
  \<Longrightarrow> (ptr \<mapsto>S obj \<and>* ptr \<mapsto>f obj) s" by (metis sep_conj_commute sep_map_o_decomp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ptr \<mapsto>o obj) s \<Longrightarrow> (ptr \<mapsto>S obj \<and>* ptr \<mapsto>f obj) s
theory Sep_Tactic_Examples

lemma sep_drule_example:
  "(ptr \<mapsto>o obj \<and>* A \<and>* B ) s
  \<Longrightarrow> (A \<and>* B \<and>* ptr \<mapsto>f obj \<and>* ptr \<mapsto>S obj) s" apply (sep_drule  example_drule) apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ptr \<mapsto>o obj \<and>* A \<and>* B) s \<Longrightarrow> (A \<and>* B \<and>* ptr \<mapsto>f obj \<and>* ptr \<mapsto>S obj) s proof (prove)
goal (1 subgoal):
 1. ((ptr \<mapsto>S obj \<and>* ptr \<mapsto>f obj) \<and>* A \<and>* B) s \<Longrightarrow> (A \<and>* B \<and>* ptr \<mapsto>f obj \<and>* ptr \<mapsto>S obj) s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma example_rule:
  "(ptr \<mapsto>f obj \<and>* ptr \<mapsto>S obj) s
  \<Longrightarrow> (ptr \<mapsto>o obj) s" by (metis sep_map_o_decomp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ptr \<mapsto>f obj \<and>* ptr \<mapsto>S obj) s \<Longrightarrow> (ptr \<mapsto>o obj) s
theory Sep_Tactic_Examples

lemma sep_rule_example: "(ptr \<mapsto>f obj \<and>* A \<and>* B \<and>* ptr \<mapsto>S obj ) s \<Longrightarrow> (ptr \<mapsto>o obj \<and>* A \<and>* B) s" apply (sep_rule example_rule) apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ptr \<mapsto>f obj \<and>* A \<and>* B \<and>* ptr \<mapsto>S obj) s \<Longrightarrow> (ptr \<mapsto>o obj \<and>* A \<and>* B) s proof (prove)
goal (1 subgoal):
 1. (ptr \<mapsto>f obj \<and>* A \<and>* B \<and>* ptr \<mapsto>S obj) s \<Longrightarrow> ((ptr \<mapsto>f obj \<and>* ptr \<mapsto>S obj) \<and>* A \<and>* B) s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma swap_cap_wp_old:
  "\<lbrace><dest \<mapsto>c cap \<and>*  src \<mapsto>c cap' \<and>* R>\<rbrace>
    swap_cap cap' src cap dest
   \<lbrace>\<lambda>_.<dest \<mapsto>c cap' \<and>* src \<mapsto>c cap \<and>* R>\<rbrace>" apply (clarsimp simp add: swap_cap_def) apply (wp swap_parents_wp set_cap_wp) apply (rule hoare_chain) apply (rule set_cap_wp) apply (sep_solve)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c cap \<and>* src \<mapsto>c cap' \<and>* R)\<rbrace> swap_cap cap' src cap dest \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c cap \<and>* src \<mapsto>c cap' \<and>* R)\<rbrace> do y <- set_cap src cap;
y <- set_cap dest cap';
swap_parents src dest
od \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap src cap \<lbrace>\<lambda>y. cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace>
 2. \<And>s. cdl.lift (dest \<mapsto>c cap \<and>* src \<mapsto>c cap' \<and>* R) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P5\<rbrace> set_cap src cap \<lbrace>?Q5\<rbrace>
 2. \<And>s. ?Q s \<Longrightarrow> ?P5 s
 3. \<And>rv s. ?Q5 rv s \<Longrightarrow> cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R) s
 4. \<And>s. cdl.lift (dest \<mapsto>c cap \<and>* src \<mapsto>c cap' \<and>* R) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>s. ?Q s \<Longrightarrow> cdl.lift (src \<mapsto>c - \<and>* ?R9) s
 2. \<And>rv s. cdl.lift (src \<mapsto>c cap \<and>* ?R9) s \<Longrightarrow> cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R) s
 3. \<And>s. cdl.lift (dest \<mapsto>c cap \<and>* src \<mapsto>c cap' \<and>* R) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma "(A \<and>* B \<and>* C \<and>* D) s  \<Longrightarrow>  (A \<and>* B \<and>* C \<and>* D) s" apply (sep_select 4 3 2 1) apply (sep_select_asm 4 3 2 1) apply (sep_select_asm 2 4) oops

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

lemma "\<lbrace>A \<and>* B \<and>* C \<and>* D\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace>" apply (sep_select_pre 4 1 2 3) apply (sep_select_post 3 4 2 1) apply (sep_select_post 3 4) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A \<and>* B \<and>* C \<and>* D\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>D \<and>* A \<and>* B \<and>* C\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>D \<and>* A \<and>* B \<and>* C\<rbrace> f \<lbrace>\<lambda>rv. C \<and>* D \<and>* B \<and>* A\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>D \<and>* A \<and>* B \<and>* C\<rbrace> f \<lbrace>\<lambda>rv. B \<and>* A \<and>* C \<and>* D\<rbrace>
theory Sep_Tactic_Examples

lemma "\<lbrace>A \<and>* B \<and>* C \<and>* D\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace>, \<lbrace>E\<rbrace>" apply (sep_select_pre 4 1 2 3) apply (sep_select_post 3 4 2 1) apply (sep_select_post 3 4) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A \<and>* B \<and>* C \<and>* D\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>D \<and>* A \<and>* B \<and>* C\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>D \<and>* A \<and>* B \<and>* C\<rbrace> f \<lbrace>\<lambda>rv. C \<and>* D \<and>* B \<and>* A\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>D \<and>* A \<and>* B \<and>* C\<rbrace> f \<lbrace>\<lambda>rv. B \<and>* A \<and>* C \<and>* D\<rbrace>, \<lbrace>E\<rbrace>
theory Sep_Tactic_Examples

lemma "\<lbrace>A \<and>* B \<and>* C \<and>* D\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace>, -" apply (sep_select_pre 4 1 2 3) apply (sep_select_post 3 4 2 1) apply (sep_select_post 3 4) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A \<and>* B \<and>* C \<and>* D\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>D \<and>* A \<and>* B \<and>* C\<rbrace> f \<lbrace>\<lambda>_. A \<and>* B \<and>* C \<and>* D\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>D \<and>* A \<and>* B \<and>* C\<rbrace> f \<lbrace>\<lambda>rv. C \<and>* D \<and>* B \<and>* A\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>D \<and>* A \<and>* B \<and>* C\<rbrace> f \<lbrace>\<lambda>rv. B \<and>* A \<and>* C \<and>* D\<rbrace>, -
theory Sep_Tactic_Examples

lemma "(P \<and>* (P \<longrightarrow>* Q)) s \<Longrightarrow> Q s" apply (sep_mp, assumption ) done

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

lemma "P s \<Longrightarrow> (Q \<longrightarrow>* (P \<and>* Q)) s" apply (erule sep_curry[rotated]) apply (assumption) done

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

lemma move_cap_wp2:
 "\<lbrace><dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R>\<rbrace>
    move_cap cap' src dest
  \<lbrace>\<lambda>_. <dest \<mapsto>c cap'  \<and>* src \<mapsto>c NullCap \<and>* R>\<rbrace>" apply (simp add: move_cap_def) apply (sep_wp set_cap_wp swap_parents_wp insert_cap_orphan_wp)+ apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> move_cap cap' src dest \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> do y <- insert_cap_orphan cap' dest;
y <- set_cap src NullCap;
swap_parents src dest
od \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (dest \<mapsto>c - \<and>* src \<mapsto>c cap \<and>* R) s \<Longrightarrow> cdl.lift (dest \<mapsto>c - \<and>* (dest \<mapsto>c cap' \<longrightarrow>* src \<mapsto>c - \<and>* (src \<mapsto>c NullCap \<longrightarrow>* ?P15 \<and>* (?P15 \<longrightarrow>* dest \<mapsto>c cap' \<and>* src \<mapsto>c NullCap \<and>* R)))) s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma swap_cap_wp2:
  "\<lbrace><dest \<mapsto>c cap \<and>*  src \<mapsto>c cap' \<and>* R>\<rbrace>
    swap_cap cap' src cap dest
   \<lbrace>\<lambda>_.<dest \<mapsto>c cap' \<and>* src \<mapsto>c cap \<and>* R>\<rbrace>" apply (clarsimp simp: swap_cap_def) apply (sep_wp swap_parents_wp set_cap_wp)+ apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c cap \<and>* src \<mapsto>c cap' \<and>* R)\<rbrace> swap_cap cap' src cap dest \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c cap \<and>* src \<mapsto>c cap' \<and>* R)\<rbrace> do y <- set_cap src cap;
y <- set_cap dest cap';
swap_parents src dest
od \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap' \<and>* src \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (dest \<mapsto>c cap \<and>* src \<mapsto>c cap' \<and>* R) s \<Longrightarrow> cdl.lift (src \<mapsto>c - \<and>* (src \<mapsto>c cap \<longrightarrow>* dest \<mapsto>c - \<and>* (dest \<mapsto>c cap' \<longrightarrow>* ?P15 \<and>* (?P15 \<longrightarrow>* dest \<mapsto>c cap' \<and>* src \<mapsto>c cap \<and>* R)))) s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma invoke_cnode_rotate2_wp:
  "(dest) \<noteq> (rnd) \<Longrightarrow>
  \<lbrace><dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>*
    rnd \<mapsto>c - \<and>* R>\<rbrace>
     invoke_cnode (RotateCall cap1 cap2 dest src rnd)
  \<lbrace>\<lambda>_. <dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>*
    rnd \<mapsto>c cap2 \<and>* R>\<rbrace>" apply (clarsimp simp: invoke_cnode_def) apply (sep_wp move_cap_wp)+ apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dest \<noteq> rnd \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R)\<rbrace> invoke_cnode (RotateCall cap1 cap2 dest src rnd) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. dest \<noteq> rnd \<Longrightarrow> \<lbrace>cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R)\<rbrace> liftE (do y <- move_cap cap2 src rnd;
move_cap cap1 dest src
od) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>dest \<noteq> rnd; cdl.lift (dest \<mapsto>c cap1 \<and>* src \<mapsto>c cap2 \<and>* rnd \<mapsto>c - \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((rnd \<mapsto>c cap2 \<longrightarrow>* dest \<mapsto>c ?cap31 \<and>* (src \<mapsto>c cap1 \<and>* dest \<mapsto>c NullCap \<longrightarrow>* dest \<mapsto>c NullCap \<and>* src \<mapsto>c cap1 \<and>* rnd \<mapsto>c cap2 \<and>* R)) \<and>* rnd \<mapsto>c - \<and>* src \<mapsto>c ?cap7) s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma sep_rule_example2:
 "\<lbrakk>(ptr \<mapsto>o obj) s; finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow>
   (ptr \<mapsto>E obj \<and>* ptr \<mapsto>f obj \<and>* (\<And>* slot\<in>dom (object_slots obj). (ptr, slot) \<mapsto>s obj)) s" apply (subst (asm) sep_map_o_decomp) apply (subst (asm) sep_map_S_decomp, simp+) apply sep_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ptr \<mapsto>o obj) s; finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow> (ptr \<mapsto>E obj \<and>* ptr \<mapsto>f obj \<and>* (SETSEPCONJ slot:dom (object_slots obj). (ptr, slot) \<mapsto>s obj)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ptr \<mapsto>f obj \<and>* ptr \<mapsto>S obj) s; finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow> (ptr \<mapsto>E obj \<and>* ptr \<mapsto>f obj \<and>* (SETSEPCONJ slot:dom (object_slots obj). (ptr, slot) \<mapsto>s obj)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ptr \<mapsto>f obj \<and>* (SETSEPCONJ slot:dom (object_slots obj). (ptr, slot) \<mapsto>s obj) \<and>* ptr \<mapsto>E obj) s; finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow> (ptr \<mapsto>E obj \<and>* ptr \<mapsto>f obj \<and>* (SETSEPCONJ slot:dom (object_slots obj). (ptr, slot) \<mapsto>s obj)) s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma sep_drule_example2:
 "\<lbrakk>(ptr \<mapsto>f obj \<and>* (\<And>* slot\<in>dom (object_slots obj). (ptr, slot) \<mapsto>s obj) \<and>* ptr \<mapsto>E obj) s;
   finite (dom (object_slots obj))\<rbrakk>
    \<Longrightarrow>
  (ptr \<mapsto>o obj) s" by (metis sep_map_S_decomp sep_map_o_decomp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ptr \<mapsto>f obj \<and>* (SETSEPCONJ slot:dom (object_slots obj). (ptr, slot) \<mapsto>s obj) \<and>* ptr \<mapsto>E obj) s; finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow> (ptr \<mapsto>o obj) s
theory Sep_Tactic_Examples

lemma sep_drule_example_lemma:
  "\<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>f obj \<and>* A \<and>* B \<and>*
    (\<And>* slot\<in>dom (object_slots obj). (ptr, slot) \<mapsto>s obj) \<and>* D \<and>* G \<and>* E \<and>* F \<and>* ptr \<mapsto>E obj ) s;
    finite (dom (object_slots obj))\<rbrakk>
  \<Longrightarrow>
   (D \<and>* G \<and>* E \<and>* F  \<and>* ptr \<mapsto>o obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B) s" apply (sep_drule sep_drule_example2) apply assumption apply sep_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>f obj \<and>* A \<and>* B \<and>* (SETSEPCONJ slot:dom (object_slots obj). (ptr, slot) \<mapsto>s obj) \<and>* D \<and>* G \<and>* E \<and>* F \<and>* ptr \<mapsto>E obj) s; finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow> (D \<and>* G \<and>* E \<and>* F \<and>* ptr \<mapsto>o obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B) s proof (prove)
goal (2 subgoals):
 1. \<And>s. finite (dom (object_slots obj)) \<Longrightarrow> finite (dom (object_slots obj))
 2. \<lbrakk>finite (dom (object_slots obj)); (ptr \<mapsto>o obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F) s\<rbrakk> \<Longrightarrow> (D \<and>* G \<and>* E \<and>* F \<and>* ptr \<mapsto>o obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite (dom (object_slots obj)); (ptr \<mapsto>o obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F) s\<rbrakk> \<Longrightarrow> (D \<and>* G \<and>* E \<and>* F \<and>* ptr \<mapsto>o obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B) s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma sep_rule_example_lemma:
 "\<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>o obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F ) s;
  finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow>
  (D \<and>* G \<and>* E \<and>* F  \<and>* ptr \<mapsto>f obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>E obj \<and>*
   A \<and>* B \<and>* (\<And>* slot\<in>dom (object_slots obj). (ptr, slot) \<mapsto>s obj)) s" apply (sep_rule sep_rule_example2) apply sep_solve apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>o obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F) s; finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow> (D \<and>* G \<and>* E \<and>* F \<and>* ptr \<mapsto>f obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>E obj \<and>* A \<and>* B \<and>* (SETSEPCONJ slot:dom (object_slots obj). (ptr, slot) \<mapsto>s obj)) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>o obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F) s; finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow> (D \<and>* G \<and>* E \<and>* F \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>* ptr \<mapsto>o obj) s
 2. \<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>o obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F) s; finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow> finite (dom (object_slots obj)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* ptr \<mapsto>o obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F) s; finite (dom (object_slots obj))\<rbrakk> \<Longrightarrow> finite (dom (object_slots obj)) proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma sep_rule_double_conjunct_example:
  "\<lbrakk>((obj_id, slot) \<mapsto>c cap \<and>* obj_id \<mapsto>f obj) s;
    object_slots obj slot = Some cap\<rbrakk>
  \<Longrightarrow> ((obj_id, slot) \<mapsto>s obj \<and>* obj_id \<mapsto>f obj) s" apply (sep_drule sep_map_s_sep_map_c) apply assumption apply (sep_cancel)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((obj_id, slot) \<mapsto>c cap \<and>* obj_id \<mapsto>f obj) s; object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow> ((obj_id, slot) \<mapsto>s obj \<and>* obj_id \<mapsto>f obj) s proof (prove)
goal (2 subgoals):
 1. \<And>s. object_slots obj slot = Some cap \<Longrightarrow> object_slots (?obj7 s) slot = Some cap
 2. \<lbrakk>object_slots obj slot = Some cap; ((\<lambda>s. ((obj_id, slot) \<mapsto>s ?obj7 s) s) \<and>* obj_id \<mapsto>f obj) s\<rbrakk> \<Longrightarrow> ((obj_id, slot) \<mapsto>s obj \<and>* obj_id \<mapsto>f obj) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_slots obj slot = Some cap; ((obj_id, slot) \<mapsto>s obj \<and>* obj_id \<mapsto>f obj) s\<rbrakk> \<Longrightarrow> ((obj_id, slot) \<mapsto>s obj \<and>* obj_id \<mapsto>f obj) s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma sep_rule_double_conjunct_lemma:
  "\<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* obj_id \<mapsto>f obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>c cap ) s;
    object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow>
   (D \<and>* G \<and>* E \<and>* F  \<and>*(obj_id, slot) \<mapsto>s obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>*  obj_id \<mapsto>f obj) s" apply (sep_rule sep_rule_double_conjunct_example) apply sep_solve apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* obj_id \<mapsto>f obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>c cap) s; object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow> (D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>s obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>* obj_id \<mapsto>f obj) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* obj_id \<mapsto>f obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>c cap) s; object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow> (D \<and>* G \<and>* E \<and>* F \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>* (obj_id, slot) \<mapsto>c ?cap17 \<and>* obj_id \<mapsto>f obj) s
 2. \<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* obj_id \<mapsto>f obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>c cap) s; object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow> object_slots obj slot = Some ?cap17 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* obj_id \<mapsto>f obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>c cap) s; object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow> object_slots obj slot = Some cap proof (prove)
goal:
No subgoals!