kings-crown/FVELER_Isabelle huggingface dataset:
theory Example2

lemma execute_op3:
  "step op3 s3 = ({s3, s4})" apply rule apply (rule execute_op3_safe) apply (rule execute_op3_live) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op3 s3 = {s3, s4} proof (prove)
goal (2 subgoals):
 1. step op3 s3 \<subseteq> {s3, s4}
 2. {s3, s4} \<subseteq> step op3 s3 proof (prove)
goal (1 subgoal):
 1. {s3, s4} \<subseteq> step op3 s3 proof (prove)
goal:
No subgoals!
theory Example2

lemma op4_legal:
  "legal op4 s4" by  (clarsimp simp: op4_def all_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. legal op4 s4
theory Example2

lemma execute_op4_safe:
  "step op4 s4 \<subseteq> ({s4, s5})" apply (clarsimp, rule ext) apply (auto simp: s4_def s5_def op4_def step_def takeOperation_def
                    diminish_def all_rights_def write_cap_def
             split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op4 s4 \<subseteq> {s4, s5} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> step op4 s4; x \<noteq> s4\<rbrakk> \<Longrightarrow> x xa = s5 xa proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op4:
  "step op4 s4 = ({s4, s5})" apply rule apply (rule execute_op4_safe) apply (rule execute_op4_live) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op4 s4 = {s4, s5} proof (prove)
goal (2 subgoals):
 1. step op4 s4 \<subseteq> {s4, s5}
 2. {s4, s5} \<subseteq> step op4 s4 proof (prove)
goal (1 subgoal):
 1. {s4, s5} \<subseteq> step op4 s4 proof (prove)
goal:
No subgoals!
theory Example2

lemma op5_legal:
  "legal op5 s5" by  (clarsimp simp: op5_def all_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. legal op5 s5
theory Example2

lemma execute_op5_safe:
  "step op5 s5 \<subseteq> ({s5, s6})" apply (clarsimp, rule ext) apply (auto simp: s5_def s6_def op5_def step_def copyOperation_def diminish_def all_rights_def read_cap_def
             split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op5 s5 \<subseteq> {s5, s6} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> step op5 s5; x \<noteq> s5\<rbrakk> \<Longrightarrow> x xa = s6 xa proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op5_live:
  "step op5 s5 \<supseteq> ({s5, s6})" apply clarsimp apply (simp add: step_def op5_legal) apply (rule disjI2) apply (simp add: op5_def) apply (rule ext) apply (fastforce simp: s5_def s6_def copyOperation_def diminish_def all_rights_def read_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s5, s6} \<subseteq> step op5 s5 proof (prove)
goal (1 subgoal):
 1. s5 \<in> step op5 s5 \<and> s6 \<in> step op5 s5 proof (prove)
goal (1 subgoal):
 1. s6 = s5 \<or> s6 \<in> step' op5 s5 proof (prove)
goal (1 subgoal):
 1. s6 \<in> step' op5 s5 proof (prove)
goal (1 subgoal):
 1. s6 = copyOperation 1 \<lparr>target = 1, rights = {Write, Store}\<rparr> (full_cap 2) {Read} s5 proof (prove)
goal (1 subgoal):
 1. \<And>x. s6 x = copyOperation 1 \<lparr>target = 1, rights = {Write, Store}\<rparr> (full_cap 2) {Read} s5 x proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op5:
  "step op5 s5 = ({s5, s6})" apply rule apply (rule execute_op5_safe) apply (rule execute_op5_live) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op5 s5 = {s5, s6} proof (prove)
goal (2 subgoals):
 1. step op5 s5 \<subseteq> {s5, s6}
 2. {s5, s6} \<subseteq> step op5 s5 proof (prove)
goal (1 subgoal):
 1. {s5, s6} \<subseteq> step op5 s5 proof (prove)
goal:
No subgoals!
theory Example2

lemma op6_legal:
  "legal op6 s6" by  (clarsimp simp: op6_def all_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. legal op6 s6
theory Example2

lemma execute_op6_live:
  "step op6 s6 \<supseteq> ({s6, s7})" apply (insert op6_legal) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s6, s7} \<subseteq> step op6 s6 proof (prove)
goal (1 subgoal):
 1. legal op6 s6 \<Longrightarrow> {s6, s7} \<subseteq> step op6 s6
theory Example2

lemma execute_op6_live:
  "s7 \<in> step op6 s6" oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s7 \<in> step op6 s6
theory Example2

lemma execute_op6:
  "step op6 s6 = ({s6, s7})" oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op6 s6 = {s6, s7}
theory Example2

lemma op7_legal:
  "legal op7 s7" by  (clarsimp simp: s7_def op7_def all_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. legal op7 s7
theory Example2

lemma execute_op7_safe:
  "step op7 s7 \<subseteq> ({s7, s8})" apply (clarsimp, rule ext) apply (auto simp: s7_def s8_def s4_def op7_def step_def createOperation_def
             split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op7 s7 \<subseteq> {s7, s8} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> step op7 s7; x \<noteq> s7\<rbrakk> \<Longrightarrow> x xa = s8 xa proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op7_live:
  "step op7 s7 \<supseteq> ({s7, s8})" apply clarsimp apply (simp add: step_def op7_legal) apply (rule disjI2) apply (simp add: op7_def) apply (rule ext) apply (fastforce simp: s7_def s8_def s4_def createOperation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s7, s8} \<subseteq> step op7 s7 proof (prove)
goal (1 subgoal):
 1. s7 \<in> step op7 s7 \<and> s8 \<in> step op7 s7 proof (prove)
goal (1 subgoal):
 1. s8 = s7 \<or> s8 \<in> step' op7 s7 proof (prove)
goal (1 subgoal):
 1. s8 \<in> step' op7 s7 proof (prove)
goal (1 subgoal):
 1. s8 = createOperation 0 (full_cap 0) (create_cap 3) s7 proof (prove)
goal (1 subgoal):
 1. \<And>x. s8 x = createOperation 0 (full_cap 0) (create_cap 3) s7 x proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op7:
  "step op7 s7 = ({s7, s8})" apply rule apply (rule execute_op7_safe) apply (rule execute_op7_live) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op7 s7 = {s7, s8} proof (prove)
goal (2 subgoals):
 1. step op7 s7 \<subseteq> {s7, s8}
 2. {s7, s8} \<subseteq> step op7 s7 proof (prove)
goal (1 subgoal):
 1. {s7, s8} \<subseteq> step op7 s7 proof (prove)
goal:
No subgoals!
theory Example2

lemma op8_legal:
  "legal op8 s8" by  (clarsimp simp: op8_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. legal op8 s8
theory Example2

lemma execute_op8_safe:
  "step op8 s8 \<subseteq> ({s8, s9})" apply clarsimp apply (rule ext) apply (insert op8_legal) apply (fastforce simp: step_def op8_def s8_def s9_def removeOperation_def
                        full_cap_def create_cap_def all_rights_def e0_caps_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op8 s8 \<subseteq> {s8, s9} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> step op8 s8; x \<noteq> s8\<rbrakk> \<Longrightarrow> x = s9 proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> step op8 s8; x \<noteq> s8\<rbrakk> \<Longrightarrow> x xa = s9 xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> step op8 s8; x \<noteq> s8; legal op8 s8\<rbrakk> \<Longrightarrow> x xa = s9 xa proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op8_live:
  "step op8 s8 \<supseteq> ({s8, s9})" apply (simp add: step_def op8_legal op8_def) apply (rule disjI2) apply (rule ext) apply (clarsimp simp: removeOperation_def) apply (fastforce simp: s8_def s9_def full_cap_def create_cap_def all_rights_def e0_caps_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s8, s9} \<subseteq> step op8 s8 proof (prove)
goal (1 subgoal):
 1. s9 = s8 \<or> s9 = removeOperation 0 (full_cap 0) (full_cap 3) s8 proof (prove)
goal (1 subgoal):
 1. s9 = removeOperation 0 (full_cap 0) (full_cap 3) s8 proof (prove)
goal (1 subgoal):
 1. \<And>x. s9 x = removeOperation 0 (full_cap 0) (full_cap 3) s8 x proof (prove)
goal (1 subgoal):
 1. \<And>x. (x = 0 \<longrightarrow> s9 0 = Some (Entity (insert (full_cap 1) (insert (full_cap 3) e0_caps) - {full_cap 3}))) \<and> (x \<noteq> 0 \<longrightarrow> s9 x = s8 x) proof (prove)
goal:
No subgoals!
theory Example2

lemma op9_legal:
  "legal op9 s9" apply (simp add: op9_def) apply (fastforce simp: s9_def e0_caps_def null_entity_def split:if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. legal op9 s9 proof (prove)
goal (1 subgoal):
 1. 3 \<notin> target ` (all_caps_of s9 - {create_cap 3}) proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op9_safe:
  "step op9 s9 \<subseteq> ({s9, s10})" apply (clarsimp, rule ext) apply (auto simp: s9_def s10_def s4_def op9_def step_def destroyOperation_def
             split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op9 s9 \<subseteq> {s9, s10} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> step op9 s9; x \<noteq> s9\<rbrakk> \<Longrightarrow> x xa = s10 xa proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op9_live:
  "step op9 s9 \<supseteq> ({s9, s10})" apply (simp add: step_def op9_legal) apply (rule disjI2) apply (simp add: op9_def) apply (rule ext) apply (clarsimp simp: destroyOperation_def step_def op9_def s9_def s10_def s4_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s9, s10} \<subseteq> step op9 s9 proof (prove)
goal (1 subgoal):
 1. s10 = s9 \<or> s10 \<in> step' op9 s9 proof (prove)
goal (1 subgoal):
 1. s10 \<in> step' op9 s9 proof (prove)
goal (1 subgoal):
 1. s10 = destroyOperation 0 (create_cap 3) s9 proof (prove)
goal (1 subgoal):
 1. \<And>x. s10 x = destroyOperation 0 (create_cap 3) s9 x proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op9:
  "step op9 s9 = ({s9, s10})" apply rule apply (rule execute_op9_safe) apply (rule execute_op9_live) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op9 s9 = {s9, s10} proof (prove)
goal (2 subgoals):
 1. step op9 s9 \<subseteq> {s9, s10}
 2. {s9, s10} \<subseteq> step op9 s9 proof (prove)
goal (1 subgoal):
 1. {s9, s10} \<subseteq> step op9 s9 proof (prove)
goal:
No subgoals!
theory Example2

lemma op10_legal:
  "legal op10 s10" by  (clarsimp simp: s10_def op10_def all_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. legal op10 s10
theory Example2

lemma e0_caps_diminished [simp]:
  "e0_caps - {full_cap 1, create_cap 1, create_cap 2} = e0_caps - {create_cap 1, create_cap 2}" by (fastforce simp: e0_caps_def create_cap_def full_cap_def all_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. e0_caps - {full_cap 1, create_cap 1, create_cap 2} = e0_caps - {create_cap 1, create_cap 2}
theory Example2

lemma execute_op10_safe:
  "step op10 s10 \<subseteq> ({s10, s})" apply (clarsimp, rule ext) apply (auto simp: s10_def op10_def step_def removeSetOperation_def s4_def s_def
              split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op10 s10 \<subseteq> {s10, s} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> step op10 s10; x \<noteq> s10\<rbrakk> \<Longrightarrow> x xa = s xa proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op10_live:
  "step op10 s10 \<supseteq> ({s10, s})" apply clarsimp apply (rule conjI) apply (simp add: step_def) apply (simp add: step_def op10_legal) apply (rule disjI2) apply (clarsimp simp: s10_def op10_def removeSetOperation_def) apply (rule ext) apply (fastforce simp: s4_def s_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s10, s} \<subseteq> step op10 s10 proof (prove)
goal (1 subgoal):
 1. s10 \<in> step op10 s10 \<and> s \<in> step op10 s10 proof (prove)
goal (2 subgoals):
 1. s10 \<in> step op10 s10
 2. s \<in> step op10 s10 proof (prove)
goal (1 subgoal):
 1. s \<in> step op10 s10 proof (prove)
goal (1 subgoal):
 1. s = s10 \<or> s \<in> step' op10 s10 proof (prove)
goal (1 subgoal):
 1. s \<in> step' op10 s10 proof (prove)
goal (1 subgoal):
 1. s = s4(0 \<mapsto> Entity (e0_caps - {create_cap 1, create_cap 2})) proof (prove)
goal (1 subgoal):
 1. \<And>x. s x = (s4(0 \<mapsto> Entity (e0_caps - {create_cap 1, create_cap 2}))) x proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op10:
  "step op10 s10 = ({s10, s})" apply rule apply (rule execute_op10_safe) apply (rule execute_op10_live) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op10 s10 = {s10, s} proof (prove)
goal (2 subgoals):
 1. step op10 s10 \<subseteq> {s10, s}
 2. {s10, s} \<subseteq> step op10 s10 proof (prove)
goal (1 subgoal):
 1. {s10, s} \<subseteq> step op10 s10 proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_ops:
  "s \<in> execute ops s0" apply (clarsimp simp: ops_def) apply (insert execute_op0_live execute_op1_live execute_op2_live execute_op3_live
                execute_op4_live execute_op5_live                  execute_op7_live
                execute_op8_live execute_op9_live execute_op10_live) apply (simp add: s7_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<in> execute ops s0 proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>step op0 s0. \<exists>x\<in>step op1 x. \<exists>x\<in>step op2 x. \<exists>x\<in>step op3 x. \<exists>x\<in>step op7 x. \<exists>x\<in>step op8 x. \<exists>x\<in>step op9 x. s \<in> step op10 x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{s0, s1} \<subseteq> step op0 s0; {s1, s2} \<subseteq> step op1 s1; {s2, s3} \<subseteq> step op2 s2; {s3, s4} \<subseteq> step op3 s3; {s4, s5} \<subseteq> step op4 s4; {s5, s6} \<subseteq> step op5 s5; {s7, s8} \<subseteq> step op7 s7; {s8, s9} \<subseteq> step op8 s8; {s9, s10} \<subseteq> step op9 s9; {s10, s} \<subseteq> step op10 s10\<rbrakk> \<Longrightarrow> \<exists>x\<in>step op0 s0. \<exists>x\<in>step op1 x. \<exists>x\<in>step op2 x. \<exists>x\<in>step op3 x. \<exists>x\<in>step op7 x. \<exists>x\<in>step op8 x. \<exists>x\<in>step op9 x. s \<in> step op10 x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s0 \<in> step op0 s0 \<and> s1 \<in> step op0 s0; s1 \<in> step op1 s1 \<and> s2 \<in> step op1 s1; s2 \<in> step op2 s2 \<and> s3 \<in> step op2 s2; s3 \<in> step op3 s3 \<and> s4 \<in> step op3 s3; s4 \<in> step op4 s4 \<and> s5 \<in> step op4 s4; s5 \<in> step op5 s5 \<and> s6 \<in> step op5 s5; s4 \<in> step op7 s4 \<and> s8 \<in> step op7 s4; s8 \<in> step op8 s8 \<and> s9 \<in> step op8 s8; s9 \<in> step op9 s9 \<and> s10 \<in> step op9 s9; s10 \<in> step op10 s10 \<and> s \<in> step op10 s10\<rbrakk> \<Longrightarrow> \<exists>x\<in>step op0 s0. \<exists>x\<in>step op1 x. \<exists>x\<in>step op2 x. \<exists>x\<in>step op3 x. \<exists>x\<in>step op7 x. \<exists>x\<in>step op8 x. \<exists>x\<in>step op9 x. s \<in> step op10 x proof (prove)
goal:
No subgoals!
theory Example2

lemma store_not_in_create_cap [simp]:
  "Store \<notin> rights (create_cap i)" by (simp add: create_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Store \<notin> rights (create_cap i)
theory Example2

lemma store_not_in_create_cap2 [simp]:
  "Store \<in> rights c \<Longrightarrow> c \<noteq> create_cap i" by (clarsimp simp: create_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Store \<in> rights c \<Longrightarrow> c \<noteq> create_cap i
theory Example2

lemma store_connected_direct_s_helper1:
  "{c'.(c' = \<lparr>target = 0, rights = UNIV\<rparr> \<or> c' \<in> range create_cap) \<and>
        c' \<noteq> \<lparr>target = 1, rights = {Create}\<rparr> \<and> c' \<noteq> \<lparr>target = 2, rights = {Create}\<rparr> \<and>
        Store \<in> rights c'} = {full_cap 0}" by (auto simp: create_cap_def full_cap_def all_rights_def e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {c'. (c' = \<lparr>target = 0, rights = UNIV\<rparr> \<or> c' \<in> range create_cap) \<and> c' \<noteq> \<lparr>target = 1, rights = {Create}\<rparr> \<and> c' \<noteq> \<lparr>target = 2, rights = {Create}\<rparr> \<and> Store \<in> rights c'} = {full_cap 0}
theory Example2

lemma store_connected_direct_s_helper2:
  "{c'. (c' = \<lparr>target = 2, rights = {Create}\<rparr> \<or> c' = \<lparr>target = 1, rights = {Write, Store}\<rparr> \<or>
         c' = \<lparr>target = 2, rights = UNIV\<rparr>)    \<and>  Store \<in> rights c'}
   = {\<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2}" by (auto simp: create_cap_def full_cap_def all_rights_def e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {c'. (c' = \<lparr>target = 2, rights = {Create}\<rparr> \<or> c' = \<lparr>target = 1, rights = {Write, Store}\<rparr> \<or> c' = \<lparr>target = 2, rights = UNIV\<rparr>) \<and> Store \<in> rights c'} = {\<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2}
theory Example2

lemma store_connected_direct_s:
  "store_connected_direct s = {(0,0), (1,1), (1,2)}" by (fastforce simp: store_connected_direct_def s_def e0_caps_def
                      full_cap_def all_rights_def create_cap_def null_entity_def
                      store_connected_direct_s_helper1 store_connected_direct_s_helper2
               split: if_split_asm)

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

lemma into_rtrancl [rule_format]:
  "(a,b) \<in> r^* \<Longrightarrow> (\<forall>x. (x,b) \<in> r \<longrightarrow> x = b) \<longrightarrow> a = b" apply (erule converse_rtrancl_induct) apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> r\<^sup>* \<Longrightarrow> (\<forall>x. (x, b) \<in> r \<longrightarrow> x = b) \<longrightarrow> a = b proof (prove)
goal (2 subgoals):
 1. (\<forall>x. (x, b) \<in> r \<longrightarrow> x = b) \<longrightarrow> b = b
 2. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; (\<forall>x. (x, b) \<in> r \<longrightarrow> x = b) \<longrightarrow> z = b\<rbrakk> \<Longrightarrow> (\<forall>x. (x, b) \<in> r \<longrightarrow> x = b) \<longrightarrow> y = b proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; (\<forall>x. (x, b) \<in> r \<longrightarrow> x = b) \<longrightarrow> z = b\<rbrakk> \<Longrightarrow> (\<forall>x. (x, b) \<in> r \<longrightarrow> x = b) \<longrightarrow> y = b proof (prove)
goal:
No subgoals!
theory Example2

lemma into_rtrancl2 [rule_format]:
  " \<And> B. \<lbrakk>(a,b) \<in> r^*; b \<in> B\<rbrakk> \<Longrightarrow> (\<forall>x.(x,b) \<in> r \<longrightarrow> x \<in> B) \<longrightarrow> a \<in> B" thm rtrancl_induct converse_rtrancl_induct apply (erule converse_rtrancl_induct) apply clarsimp apply clarsimp oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>B. \<lbrakk>(a, b) \<in> r\<^sup>*; b \<in> B\<rbrakk> \<Longrightarrow> (\<forall>x. (x, b) \<in> r \<longrightarrow> x \<in> B) \<longrightarrow> a \<in> B proof (prove)
goal (1 subgoal):
 1. \<And>B. \<lbrakk>(a, b) \<in> r\<^sup>*; b \<in> B\<rbrakk> \<Longrightarrow> (\<forall>x. (x, b) \<in> r \<longrightarrow> x \<in> B) \<longrightarrow> a \<in> B proof (prove)
goal (2 subgoals):
 1. \<And>B. b \<in> B \<Longrightarrow> (\<forall>x. (x, b) \<in> r \<longrightarrow> x \<in> B) \<longrightarrow> b \<in> B
 2. \<And>B y z. \<lbrakk>b \<in> B; (y, z) \<in> r; (z, b) \<in> r\<^sup>*; (\<forall>x. (x, b) \<in> r \<longrightarrow> x \<in> B) \<longrightarrow> z \<in> B\<rbrakk> \<Longrightarrow> (\<forall>x. (x, b) \<in> r \<longrightarrow> x \<in> B) \<longrightarrow> y \<in> B proof (prove)
goal (1 subgoal):
 1. \<And>B y z. \<lbrakk>b \<in> B; (y, z) \<in> r; (z, b) \<in> r\<^sup>*; (\<forall>x. (x, b) \<in> r \<longrightarrow> x \<in> B) \<longrightarrow> z \<in> B\<rbrakk> \<Longrightarrow> (\<forall>x. (x, b) \<in> r \<longrightarrow> x \<in> B) \<longrightarrow> y \<in> B proof (prove)
goal (1 subgoal):
 1. \<And>B y z. \<lbrakk>b \<in> B; (y, z) \<in> r; (z, b) \<in> r\<^sup>*; \<forall>x. (x, b) \<in> r \<longrightarrow> x \<in> B; z \<in> B\<rbrakk> \<Longrightarrow> y \<in> B
theory Example2

lemma store_connected_id:
 "{(0::word32, 0), (1, 1), (1, 2)}\<^sup>* = {(1, 2)}\<^sup>* " apply rule apply clarsimp apply (erule rtranclE) apply simp apply (fastforce dest: into_rtrancl) apply clarsimp apply (erule rtranclE) apply simp apply (fastforce dest: into_rtrancl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {(0, 0), (1, 1), (1, 2)}\<^sup>* = {(1, 2)}\<^sup>* proof (prove)
goal (2 subgoals):
 1. {(0, 0), (1, 1), (1, 2)}\<^sup>* \<subseteq> {(1, 2)}\<^sup>*
 2. {(1, 2)}\<^sup>* \<subseteq> {(0, 0), (1, 1), (1, 2)}\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>* \<Longrightarrow> (a, b) \<in> {(1, 2)}\<^sup>*
 2. {(1, 2)}\<^sup>* \<subseteq> {(0, 0), (1, 1), (1, 2)}\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a b. a = b \<Longrightarrow> (a, b) \<in> {(1, 2)}\<^sup>*
 2. \<And>a b y. \<lbrakk>(a, y) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>*; (y, b) \<in> {(0, 0), (1, 1), (1, 2)}\<rbrakk> \<Longrightarrow> (a, b) \<in> {(1, 2)}\<^sup>*
 3. {(1, 2)}\<^sup>* \<subseteq> {(0, 0), (1, 1), (1, 2)}\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>(a, y) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>*; (y, b) \<in> {(0, 0), (1, 1), (1, 2)}\<rbrakk> \<Longrightarrow> (a, b) \<in> {(1, 2)}\<^sup>*
 2. {(1, 2)}\<^sup>* \<subseteq> {(0, 0), (1, 1), (1, 2)}\<^sup>* proof (prove)
goal (1 subgoal):
 1. {(1, 2)}\<^sup>* \<subseteq> {(0, 0), (1, 1), (1, 2)}\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> {(1, 2)}\<^sup>* \<Longrightarrow> (a, b) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b. a = b \<Longrightarrow> (a, b) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>*
 2. \<And>a b y. \<lbrakk>(a, y) \<in> {(1, 2)}\<^sup>*; (y, b) \<in> {(1, 2)}\<rbrakk> \<Longrightarrow> (a, b) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>(a, y) \<in> {(1, 2)}\<^sup>*; (y, b) \<in> {(1, 2)}\<rbrakk> \<Longrightarrow> (a, b) \<in> {(0, 0), (1, 1), (1, 2)}\<^sup>* proof (prove)
goal:
No subgoals!
theory Example2

lemma caps_of_s_e0_caps: "caps_of s 0 = e0_caps - {create_cap 1, create_cap 2}" apply (clarsimp simp: caps_of_def store_connected_s Collect_disj_eq) apply (simp add: s_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of s 0 = e0_caps - {create_cap 1, create_cap 2} proof (prove)
goal (1 subgoal):
 1. direct_caps_of s 0 = e0_caps - {create_cap 1, create_cap 2} proof (prove)
goal:
No subgoals!
theory Example2

lemma caps_of_s_e0_caps_2: "caps_of s 0 = {full_cap 0} \<union> ( range create_cap - {create_cap 1, create_cap 2})" by (fastforce simp: caps_of_s_e0_caps e0_caps_def full_cap_def create_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of s 0 = {full_cap 0} \<union> (range create_cap - {create_cap 1, create_cap 2})
theory Example2

lemma caps_of_s_e1: "caps_of s 1 = {create_cap 2, \<lparr> target = 1, rights = {Write, Store}\<rparr>, full_cap 2}" apply (clarsimp simp: caps_of_def store_connected_s Collect_disj_eq) apply (simp add: s_def null_entity_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of s 1 = {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2} proof (prove)
goal (1 subgoal):
 1. direct_caps_of s 1 \<union> direct_caps_of s 2 = {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2} proof (prove)
goal:
No subgoals!
theory Example2

lemma caps_of_s_e2: "caps_of s 2 = {}" apply (simp add: caps_of_def store_connected_s) apply (simp add: s_def null_entity_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of s 2 = {} proof (prove)
goal (1 subgoal):
 1. direct_caps_of s 2 = {} proof (prove)
goal:
No subgoals!
theory Example2

lemma caps_of_s_e3: "\<lbrakk>e \<noteq> 0; e \<noteq> 1\<rbrakk> \<Longrightarrow> caps_of s e = {}" apply (simp add: caps_of_def store_connected_s) apply (simp add: s_def null_entity_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e \<noteq> 0; e \<noteq> 1\<rbrakk> \<Longrightarrow> caps_of s e = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e \<noteq> 0; e \<noteq> 1\<rbrakk> \<Longrightarrow> direct_caps_of s e = {} proof (prove)
goal:
No subgoals!