theory Example2

lemma execute_op6_safe:
  "step op6 s6 \<subseteq> ({s6, s7})" apply (clarsimp, rule ext) apply (auto simp: s6_def s7_def s4_def op7_def step_def revokeOperation_def
          split: if_split_asm) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step op6 s6 \<subseteq> {s6, s7} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> step op6 s6; x \<noteq> s6\<rbrakk> \<Longrightarrow> x xa = s7 xa proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>x \<noteq> [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]; legal op6 [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]; x \<in> step' op6 [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]\<rbrakk> \<Longrightarrow> x 0 = Some (Entity (insert (full_cap 1) e0_caps))
 2. \<And>x. \<lbrakk>x \<noteq> [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]; legal op6 [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]; x \<in> step' op6 [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]\<rbrakk> \<Longrightarrow> x 1 = Some (Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2})
 3. \<And>x. \<lbrakk>x \<noteq> [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]; legal op6 [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]; x \<in> step' op6 [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]\<rbrakk> \<Longrightarrow> x 2 = Some null_entity
 4. \<And>x xa. \<lbrakk>x \<noteq> [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]; legal op6 [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]; x \<in> step' op6 [0 \<mapsto> Entity (insert (full_cap 1) (insert (write_cap 2) e0_caps)), 1 \<mapsto> Entity {create_cap 2, \<lparr>target = 1, rights = {Write, Store}\<rparr>, full_cap 2, read_cap 2}, 2 \<mapsto> null_entity]; xa \<noteq> 0; xa \<noteq> 1; xa \<noteq> 2\<rbrakk> \<Longrightarrow> x xa = None