kings-crown/FVELER_Isabelle huggingface dataset:
theory Isolation_S

lemma flow_trans_refl [simp]:
  "s \<turnstile> x \<leadsto>* x" by (metis flow_trans_def rtrancl.rtrancl_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> x \<leadsto>* x
theory Isolation_S

lemma flow_connected [rule_format]:
  "\<forall>s'.  s' \<in> execute cmds s \<longrightarrow>
    s' \<turnstile> x \<leadsto>* y \<longrightarrow>
    s \<turnstile> x \<leadsto>* y" apply (induct_tac cmds, simp) apply clarsimp apply (drule (1) flow_connected_step) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s'. s' \<in> execute cmds s \<longrightarrow> s' \<turnstile> x \<leadsto>* y \<longrightarrow> s \<turnstile> x \<leadsto>* y proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<forall>s'. s' \<in> execute list s \<longrightarrow> s' \<turnstile> x \<leadsto>* y \<longrightarrow> s \<turnstile> x \<leadsto>* y \<Longrightarrow> \<forall>s'. s' \<in> execute (a # list) s \<longrightarrow> s' \<turnstile> x \<leadsto>* y \<longrightarrow> s \<turnstile> x \<leadsto>* y proof (prove)
goal (1 subgoal):
 1. \<And>a list s' xa. \<lbrakk>\<forall>s'. s' \<in> execute list s \<longrightarrow> s' \<turnstile> x \<leadsto>* y \<longrightarrow> s \<turnstile> x \<leadsto>* y; xa \<in> execute list s; s' \<in> step a xa; s' \<turnstile> x \<leadsto>* y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leadsto>* y proof (prove)
goal (1 subgoal):
 1. \<And>a list s' xa. \<lbrakk>\<forall>s'. s' \<in> execute list s \<longrightarrow> s' \<turnstile> x \<leadsto>* y \<longrightarrow> s \<turnstile> x \<leadsto>* y; xa \<in> execute list s; s' \<in> step a xa; xa \<turnstile> x \<leadsto>* y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leadsto>* y proof (prove)
goal:
No subgoals!
theory Isolation_S

lemma information_flow:
  "\<lbrakk>s' \<in> execute cmds s;
  \<not> s \<turnstile> x \<leadsto>* y\<rbrakk> \<Longrightarrow>
  \<not> s' \<turnstile> x \<leadsto>* y" by (auto simp: flow_connected)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> execute cmds s; \<not> s \<turnstile> x \<leadsto>* y\<rbrakk> \<Longrightarrow> \<not> s' \<turnstile> x \<leadsto>* y
theory Example

lemma de0:
  "direct_caps_of example_state id0 =
   {\<lparr> target = id1, rights = {Store}\<rparr>}" by (simp add: direct_caps_of_def example_state_def
                id_defs entity_defs
         split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of example_state id0 = {\<lparr>target = id1, rights = {Store}\<rparr>}
theory Example

lemma de1:
  "direct_caps_of example_state id1 =
   {\<lparr> target = id2, rights = {Grant}\<rparr>}" by (simp add: direct_caps_of_def example_state_def
                id_defs entity_defs
         split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of example_state id1 = {\<lparr>target = id2, rights = {Grant}\<rparr>}
theory Example

lemma de2: "direct_caps_of example_state id2 = {}" by (simp add: direct_caps_of_def example_state_def
                id_defs entity_defs
         split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of example_state id2 = {}
theory Example

lemma scd:
  "store_connected_direct example_state = {(id0,id1)}" by (auto simp: store_connected_direct_def direct_caps_of_def
                 example_state_def id_defs entity_defs
          split: if_split_asm option.splits
           cong: conj_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. store_connected_direct example_state = {(id0, id1)}
theory Example

lemma sc': "store_connected example_state = Id \<union> {(0,1)}" by (clarsimp simp: sc id_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. store_connected example_state = Id \<union> {(0, 1)}
theory Example

lemma ce0:
  "caps_of example_state id0 =
   {\<lparr>target = id1, rights = {Store}\<rparr>,
    \<lparr>target = id2, rights = {Grant}\<rparr>}" by (fastforce simp: caps_of_def sc Collect_disj_eq de0 de1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of example_state id0 = {\<lparr>target = id1, rights = {Store}\<rparr>, \<lparr>target = id2, rights = {Grant}\<rparr>}
theory Example

lemma ce1:
  "caps_of example_state id1 =
   {\<lparr> target = id2, rights = {Grant}\<rparr>}" apply (clarsimp simp: caps_of_def sc Collect_disj_eq de0 de1) apply (simp add: id0_def id1_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of example_state id1 = {\<lparr>target = id2, rights = {Grant}\<rparr>} proof (prove)
goal (1 subgoal):
 1. id1 = id0 \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Example

lemma ce2: "caps_of example_state id2 = {}" apply (simp add: caps_of_def sc) apply (rule allI) apply (rule conjI) apply (simp add: id0_def id2_def) apply (simp add: de2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of example_state id2 = {} proof (prove)
goal (1 subgoal):
 1. \<forall>x. (id2 = id0 \<and> x = id1 \<longrightarrow> direct_caps_of example_state id1 = {}) \<and> (id2 = x \<longrightarrow> direct_caps_of example_state id2 = {}) proof (prove)
goal (1 subgoal):
 1. \<And>x. (id2 = id0 \<and> x = id1 \<longrightarrow> direct_caps_of example_state id1 = {}) \<and> (id2 = x \<longrightarrow> direct_caps_of example_state id2 = {}) proof (prove)
goal (2 subgoals):
 1. \<And>x. id2 = id0 \<and> x = id1 \<longrightarrow> direct_caps_of example_state id1 = {}
 2. \<And>x. id2 = x \<longrightarrow> direct_caps_of example_state id2 = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. id2 = x \<longrightarrow> direct_caps_of example_state id2 = {} proof (prove)
goal:
No subgoals!
theory Example2

lemma direct_caps_of_empty [simp]:
  "direct_caps_of Map.empty = ( \<lambda> x. {})" by (simp add: direct_caps_of_def fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of (\<lambda>x. None) = (\<lambda>x. {})
theory Example2

lemma is_entity_s0_e0 [simp]:
  "is_entity s0 0" by (simp add: is_entity_def s0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity s0 0
theory Example2

lemma is_entity_s1_e0 [simp]:
  "is_entity s1 0" by (simp add: is_entity_def s1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity s1 0
theory Example2

lemma is_entity_s2_e0 [simp]:
  "is_entity s2 0" by (simp add: is_entity_def s2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity s2 0
theory Example2

lemma is_entity_s3_e0 [simp]:
  "is_entity s3 0" by (simp add: is_entity_def s3_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity s3 0
theory Example2

lemma is_entity_s4_e0 [simp]:
  "is_entity s4 0" by (simp add: is_entity_def s4_def)

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

lemma is_entity_s5_e0 [simp]:
  "is_entity s5 0" by (simp add: is_entity_def s5_def)

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

lemma is_entity_s8_e0 [simp]:
  "is_entity s8 0" by (simp add: is_entity_def s8_def)

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

lemma is_entity_s9_e0 [simp]:
  "is_entity s9 0" by (simp add: is_entity_def s9_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity s9 0
theory Example2

lemma is_entity_s_e0 [simp]:
  "is_entity s 0" by (simp add: is_entity_def s_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity s 0
theory Example2

lemma is_entity_s0_e1 [simp]:
  "\<not> is_entity s0 1" by (simp add: is_entity_def s0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_entity s0 1
theory Example2

lemma is_entity_s1_e1 [simp]:
  "is_entity s1 1" by (simp add: is_entity_def s1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity s1 1
theory Example2

lemma is_entity_s2_e1 [simp]:
  "is_entity s2 1" by (simp add: is_entity_def s2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity s2 1
theory Example2

lemma is_entity_s3_e1 [simp]:
  "is_entity s3 1" by (simp add: is_entity_def s3_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_entity s3 1
theory Example2

lemma is_entity_s4_e1 [simp]:
  "is_entity s4 1" by (simp add: is_entity_def s4_def)

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

lemma is_entity_s5_e1 [simp]:
  "is_entity s5 1" by (simp add: is_entity_def s5_def)

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

lemma is_entity_s3_e2 [simp]:
  "\<not> is_entity s3 2" by (simp add: is_entity_def s3_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_entity s3 2
theory Example2

lemma is_entity_s4_e3 [simp]:
  "\<not> is_entity s4 3" by (simp add: is_entity_def s4_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_entity s4 3
theory Example2

lemma direct_caps_of_s0_e0_caps [simp]:
  "direct_caps_of s0 0 = e0_caps" by (simp add: direct_caps_of_def s0_def e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of s0 0 = e0_caps
theory Example2

lemma direct_caps_of_s1_e0_caps [simp]:
  "direct_caps_of s1 0 = e0_caps \<union> {full_cap 1}" by (simp add: direct_caps_of_def s1_def e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of s1 0 = e0_caps \<union> {full_cap 1}
theory Example2

lemma direct_caps_of_s2_e0_caps [simp]:
  "direct_caps_of s2 0 = e0_caps \<union> {full_cap 1}" by (simp add: direct_caps_of_def s2_def e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of s2 0 = e0_caps \<union> {full_cap 1}
theory Example2

lemma direct_caps_of_s4_e0_caps [simp]:
  "direct_caps_of s4 0 = e0_caps \<union> {full_cap 1}" by (simp add: direct_caps_of_def s4_def e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of s4 0 = e0_caps \<union> {full_cap 1}
theory Example2

lemma direct_caps_of_s5_e0_caps [simp]:
  "direct_caps_of s5 0 = e0_caps \<union> {full_cap 1, write_cap 2}" by (simp add: direct_caps_of_def s5_def e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of s5 0 = e0_caps \<union> {full_cap 1, write_cap 2}
theory Example2

lemma direct_caps_of_s6_e0_caps [simp]:
  "direct_caps_of s6 0 = e0_caps \<union> {full_cap 1, write_cap 2}" by (simp add: direct_caps_of_def s6_def e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of s6 0 = e0_caps \<union> {full_cap 1, write_cap 2}
theory Example2

lemma direct_caps_of_s8_e0_caps [simp]:
  "direct_caps_of s8 0 = e0_caps \<union> {full_cap 1, full_cap 3}" by (simp add: direct_caps_of_def s8_def e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of s8 0 = e0_caps \<union> {full_cap 1, full_cap 3}
theory Example2

lemma direct_caps_of_s9_e0_caps [simp]:
  "direct_caps_of s9 0 = e0_caps \<union> {full_cap 1}" by (simp add: direct_caps_of_def s9_def e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of s9 0 = e0_caps \<union> {full_cap 1}
theory Example2

lemma direct_caps_of_s2_e1 [simp]:
  "direct_caps_of s2 1 = {create_cap 2}" by (simp add: direct_caps_of_def s2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of s2 1 = {create_cap 2}
theory Example2

lemma direct_caps_of_s3_e1 [simp]:
  "direct_caps_of s3 1 = {create_cap 2, \<lparr> target = 1, rights = {Write, Store}\<rparr>}" by (simp add: direct_caps_of_def s3_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. direct_caps_of s3 1 = {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>}
theory Example2

lemma direct_caps_of_s4_e1 [simp]:
  "direct_caps_of s4 1 = {create_cap 2, \<lparr> target = 1, rights = {Write, Store}\<rparr>, full_cap 2}" by (simp add: direct_caps_of_def s4_def)

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

lemma direct_caps_of_s6_e1 [simp]:
  "direct_caps_of s5 1 = {create_cap 2, \<lparr> target = 1, rights = {Write, Store}\<rparr>, full_cap 2}" by (simp add: direct_caps_of_def s5_def)

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

lemma direct_caps_of_s9_e1 [simp]:
  "direct_caps_of s9 1 = {create_cap 2, \<lparr> target = 1, rights = {Write, Store}\<rparr>, full_cap 2}" by (simp add: direct_caps_of_def s9_def)

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

lemma full_cap_e0_caps_in_caps_of_s0_e0_caps [simp]:
  "full_cap 0 \<in> caps_of s0 0" by (rule direct_cap_in_cap, simp add: e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. full_cap 0 \<in> caps_of s0 0
theory Example2

lemma full_cap_e1_in_caps_of_s1_e0_caps [simp]:
  "full_cap 1 \<in> caps_of s1 0" by (rule direct_cap_in_cap, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. full_cap 1 \<in> caps_of s1 0
theory Example2

lemma full_cap_e1_in_caps_of_s2_e0_caps [simp]:
  "full_cap 1 \<in> caps_of s2 0" by (rule direct_cap_in_cap, simp add: e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. full_cap 1 \<in> caps_of s2 0
theory Example2

lemma full_cap_e0_caps_in_caps_of_s4_e0_caps [simp]:
  "full_cap 0 \<in> caps_of s4 0" by (rule direct_cap_in_cap, simp add: e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. full_cap 0 \<in> caps_of s4 0
theory Example2

lemma full_cap_e1_in_caps_of_s4_e0_caps [simp]:
  "full_cap 1 \<in> caps_of s4 0" by (rule direct_cap_in_cap, simp add: e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. full_cap 1 \<in> caps_of s4 0
theory Example2

lemma full_cap_e1_in_caps_of_s5_e0_caps [simp]:
  "full_cap 1 \<in> caps_of s5 0" by (rule direct_cap_in_cap, simp add: e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. full_cap 1 \<in> caps_of s5 0
theory Example2

lemma full_cap_e2_in_caps_of_s5_e0_caps [simp]:
  "full_cap 2 \<in> caps_of s5 1" by (rule direct_cap_in_cap, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. full_cap 2 \<in> caps_of s5 1
theory Example2

lemma full_cap_e0_caps_in_caps_of_s8_e0_caps [simp]:
  "full_cap 0 \<in> caps_of s8 0" by (rule direct_cap_in_cap, simp add: e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. full_cap 0 \<in> caps_of s8 0
theory Example2

lemma create_cap_in_caps_of_s0_e0_caps [simp]:
  "create_cap i \<in> caps_of s0 0" by (rule direct_cap_in_cap, simp add: e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. create_cap i \<in> caps_of s0 0
theory Example2

lemma create_cap_in_caps_of_s1_e0_caps [simp]:
  "create_cap i \<in> caps_of s1 0" by (rule direct_cap_in_cap, simp add: e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. create_cap i \<in> caps_of s1 0
theory Example2

lemma create_cap_in_caps_of_s2_e1 [simp]:
  "create_cap 2 \<in> caps_of s2 1" by (rule direct_cap_in_cap, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. create_cap 2 \<in> caps_of s2 1
theory Example2

lemma create_cap_in_caps_of_s3_e1 [simp]:
  "create_cap 2 \<in> caps_of s3 1" by (rule direct_cap_in_cap, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. create_cap 2 \<in> caps_of s3 1
theory Example2

lemma create_cap_in_caps_of_s4_e3 [simp]:
  "create_cap 3 \<in> caps_of s4 0" by (rule direct_cap_in_cap, simp add: e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. create_cap 3 \<in> caps_of s4 0
theory Example2

lemma create_cap_in_caps_of_s9_e3 [simp]:
  "create_cap 3 \<in> caps_of s9 0" by (rule direct_cap_in_cap, simp add: e0_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. create_cap 3 \<in> caps_of s9 0
theory Example2

lemma write_store_e1_in_caps_of_s3_e1 [simp]:
  "\<lparr>target = 1, rights = {Write, Store}\<rparr>  \<in> caps_of s3 1" by (rule direct_cap_in_cap, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lparr>target = 1, rights = {Write, Store}\<rparr> \<in> caps_of s3 1
theory Example2

lemma write_store_e1_in_caps_of_s5_e1 [simp]:
  "\<lparr>target = 1, rights = {Write, Store}\<rparr> \<in> caps_of s5 1" by (rule direct_cap_in_cap, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lparr>target = 1, rights = {Write, Store}\<rparr> \<in> caps_of s5 1
theory Example2

lemma write_cap_e2_in_caps_of_s6_e0_caps [simp]:
  "write_cap 2 \<in> caps_of s6 0" by (rule direct_cap_in_cap, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. write_cap 2 \<in> caps_of s6 0
theory Example2

lemma op0_legal:
  "legal op0 s0" by  (clarsimp simp: op0_def all_rights_def)

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

lemma execute_op0_safe:
  "step op0 s0 \<subseteq> ({s0, s1})" by (fastforce simp: op0_def step_def createOperation_def s0_def s1_def
                 split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op0 s0 \<subseteq> {s0, s1}
theory Example2

lemma execute_op0_live:
  "step op0 s0 \<supseteq> ({s0, s1})" apply clarsimp apply (rule conjI) apply (simp add: step_def) apply (simp add: step_def op0_legal) apply (rule disjI2) apply (clarsimp simp: op0_def createOperation_def) apply (rule ext) apply (clarsimp simp: s0_def s1_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s0, s1} \<subseteq> step op0 s0 proof (prove)
goal (1 subgoal):
 1. s0 \<in> step op0 s0 \<and> s1 \<in> step op0 s0 proof (prove)
goal (2 subgoals):
 1. s0 \<in> step op0 s0
 2. s1 \<in> step op0 s0 proof (prove)
goal (1 subgoal):
 1. s1 \<in> step op0 s0 proof (prove)
goal (1 subgoal):
 1. s1 = s0 \<or> s1 \<in> step' op0 s0 proof (prove)
goal (1 subgoal):
 1. s1 \<in> step' op0 s0 proof (prove)
goal (1 subgoal):
 1. s1 = s0(0 \<mapsto> Entity (insert (full_cap 1) e0_caps), 1 \<mapsto> null_entity) proof (prove)
goal (1 subgoal):
 1. \<And>x. s1 x = (s0(0 \<mapsto> Entity (insert (full_cap 1) e0_caps), 1 \<mapsto> null_entity)) x proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op0:
  "step op0 s0 = ({s0, s1})" apply rule apply (rule execute_op0_safe) apply (rule execute_op0_live) done

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

lemma op1_legal:
  "legal op1 s1" by  (clarsimp simp: op1_def all_rights_def)

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

lemma execute_op1_safe:
  "step op1 s1 \<subseteq> ({s1, s2})" by (clarsimp simp: op1_def step_def grantOperation_def diminish_def
                     s1_def s2_def create_cap_def null_entity_def
              split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op1 s1 \<subseteq> {s1, s2}
theory Example2

lemma execute_op1_live:
  "step op1 s1 \<supseteq> ({s1, s2})" apply clarsimp apply (rule conjI) apply (simp add: step_def) apply (simp add: step_def op1_legal) apply (rule disjI2) apply (clarsimp simp: op1_def grantOperation_def) apply (rule ext) apply (clarsimp simp: s1_def s2_def null_entity_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s1, s2} \<subseteq> step op1 s1 proof (prove)
goal (1 subgoal):
 1. s1 \<in> step op1 s1 \<and> s2 \<in> step op1 s1 proof (prove)
goal (2 subgoals):
 1. s1 \<in> step op1 s1
 2. s2 \<in> step op1 s1 proof (prove)
goal (1 subgoal):
 1. s2 \<in> step op1 s1 proof (prove)
goal (1 subgoal):
 1. s2 = s1 \<or> s2 \<in> step' op1 s1 proof (prove)
goal (1 subgoal):
 1. s2 \<in> step' op1 s1 proof (prove)
goal (1 subgoal):
 1. s2 = s1(1 \<mapsto> Entity (insert (diminish UNIV (create_cap 2)) (direct_caps_of s1 1))) proof (prove)
goal (1 subgoal):
 1. \<And>x. s2 x = (s1(1 \<mapsto> Entity (insert (diminish UNIV (create_cap 2)) (direct_caps_of s1 1)))) x proof (prove)
goal:
No subgoals!
theory Example2

lemma op2_legal:
  "legal op2 s2" by  (clarsimp simp: op2_def all_rights_def)

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

lemma execute_op2_safe:
  "step op2 s2 \<subseteq> ({s2, s3})" apply clarsimp apply (rule ext) apply (auto simp: op2_def step_def grantOperation_def diminish_def s2_def s3_def full_cap_def all_rights_def
             split: if_split_asm) done

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

lemma execute_op2_live:
  "step op2 s2 \<supseteq> ({s2, s3})" apply clarsimp apply (simp add: step_def op2_legal) apply (rule disjI2) apply (simp add: op2_def) apply (rule ext) apply (fastforce simp: s2_def s3_def grantOperation_def diminish_def all_rights_def full_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s2, s3} \<subseteq> step op2 s2 proof (prove)
goal (1 subgoal):
 1. s2 \<in> step op2 s2 \<and> s3 \<in> step op2 s2 proof (prove)
goal (1 subgoal):
 1. s3 = s2 \<or> s3 \<in> step' op2 s2 proof (prove)
goal (1 subgoal):
 1. s3 \<in> step' op2 s2 proof (prove)
goal (1 subgoal):
 1. s3 = grantOperation 0 (full_cap 1) (full_cap 1) {Write, Store} s2 proof (prove)
goal (1 subgoal):
 1. \<And>x. s3 x = grantOperation 0 (full_cap 1) (full_cap 1) {Write, Store} s2 x proof (prove)
goal:
No subgoals!
theory Example2

lemma execute_op2:
  "step op2 s2 = ({s2, s3})" apply rule apply (rule execute_op2_safe) apply (rule execute_op2_live) done

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

lemma op3_legal:
  "legal op3 s3" by  (clarsimp simp: op3_def all_rights_def)

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

lemma execute_op3_safe:
  "step op3 s3 \<subseteq> ({s3, s4})" apply (clarsimp, rule ext) apply (auto simp: op3_def step_def createOperation_def s3_def s4_def
             split: if_split_asm) done

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

lemma execute_op3_live:
  "step op3 s3 \<supseteq> ({s3, s4})" apply clarsimp apply (simp add: step_def op3_legal) apply (rule disjI2) apply (clarsimp simp: op3_def createOperation_def) apply (rule ext) apply (fastforce simp: s3_def s4_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s3, s4} \<subseteq> step op3 s3 proof (prove)
goal (1 subgoal):
 1. s3 \<in> step op3 s3 \<and> s4 \<in> step op3 s3 proof (prove)
goal (1 subgoal):
 1. s4 = s3 \<or> s4 \<in> step' op3 s3 proof (prove)
goal (1 subgoal):
 1. s4 \<in> step' op3 s3 proof (prove)
goal (1 subgoal):
 1. s4 = s3(1 \<mapsto> Entity {full_cap 2, create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>}, 2 \<mapsto> null_entity) proof (prove)
goal (1 subgoal):
 1. \<And>x. s4 x = (s3(1 \<mapsto> Entity {full_cap 2, create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>}, 2 \<mapsto> null_entity)) x proof (prove)
goal:
No subgoals!