kings-crown/FVELER_Isabelle huggingface dataset:
theory ExampleSystem

lemma thread_bound_ntfns_1:
  "thread_bound_ntfns s1 = Map.empty" unfolding s1_def thread_bound_ntfns_def apply (rule ext) apply (simp add: get_tcb_def) apply (simp add: kh1_def kh1_obj_def ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_bound_ntfns s1 = (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. case get_tcb p \<lparr>kheap = kh1, cdt = \<lambda>x. None, is_original_cap = undefined, cur_thread = undefined, idle_thread = undefined, machine_state = undefined, interrupt_irq_node = \<lambda>_. 0xA, interrupt_states = undefined, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = undefined, arm_next_asid = undefined, arm_asid_map = undefined, arm_global_pd = undefined, arm_global_pts = undefined, arm_kernel_vspace = undefined\<rparr>, exst = exst1\<rparr> of None \<Rightarrow> None | Some x \<Rightarrow> tcb_bound_notification x) = (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. \<And>p. (case get_tcb p \<lparr>kheap = kh1, cdt = \<lambda>x. None, is_original_cap = undefined, cur_thread = undefined, idle_thread = undefined, machine_state = undefined, interrupt_irq_node = \<lambda>_. 0xA, interrupt_states = undefined, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = undefined, arm_next_asid = undefined, arm_asid_map = undefined, arm_global_pd = undefined, arm_global_pts = undefined, arm_kernel_vspace = undefined\<rparr>, exst = exst1\<rparr> of None \<Rightarrow> None | Some x \<Rightarrow> tcb_bound_notification x) = None proof (prove)
goal (1 subgoal):
 1. \<And>p. (case case kh1 p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | Some _ \<Rightarrow> None of None \<Rightarrow> None | Some x2 \<Rightarrow> tcb_bound_notification x2) = None proof (prove)
goal:
No subgoals!
theory ExampleSystem

lemma domains_of_state_s1[simp]:
  "domains_of_state s1 = {}" apply (rule equalityI) apply (rule subsetI) apply clarsimp apply (erule domains_of_state_aux.induct) apply (simp add: s1_def exst1_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domains_of_state s1 = {} proof (prove)
goal (2 subgoals):
 1. domains_of_state s1 \<subseteq> {}
 2. {} \<subseteq> domains_of_state s1 proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> domains_of_state s1 \<Longrightarrow> x \<in> {}
 2. {} \<subseteq> domains_of_state s1 proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> domains_of_state s1 \<Longrightarrow> False
 2. {} \<subseteq> domains_of_state s1 proof (prove)
goal (2 subgoals):
 1. \<And>a b ptr etcb d. \<lbrakk>ekheap s1 ptr = Some etcb; d = tcb_domain etcb\<rbrakk> \<Longrightarrow> False
 2. {} \<subseteq> domains_of_state s1 proof (prove)
goal (1 subgoal):
 1. {} \<subseteq> domains_of_state s1 proof (prove)
goal:
No subgoals!
theory ExampleSystem

lemma "asid_high_bits_of asid2_3065 \<noteq> asid_high_bits_of asid2_3063" by (simp add: asid2_3063_def asid_high_bits_of_def asid2_3065_def asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_high_bits_of asid2_3065 \<noteq> asid_high_bits_of asid2_3063
theory ExampleSystem

lemma caps2_7_well_formed: "well_formed_cnode_n 10 caps2_7" apply (clarsimp simp: caps2_7_def well_formed_cnode_n_def) apply (clarsimp simp: the_nat_to_bl_10_def the_nat_to_bl_def nat_to_bl_def) apply (clarsimp simp: empty_cnode_def dom_def) apply (rule set_eqI, clarsimp) apply (rule iffI) apply (elim disjE, insert len_bin_to_bl, simp_all)[1] apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n 10 caps2_7 proof (prove)
goal (1 subgoal):
 1. insert (the_nat_to_bl_10 4) (insert (the_nat_to_bl_10 3) (insert (the_nat_to_bl_10 2) (insert (the_nat_to_bl_10 (Suc 0)) (dom (empty_cnode 10))))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. insert [False, False, False, False, False, False, False, True, False, False] (insert [False, False, False, False, False, False, False, False, True, True] (insert [False, False, False, False, False, False, False, False, True, False] (insert [False, False, False, False, False, False, False, False, False, True] (dom (empty_cnode 10))))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. insert [False, False, False, False, False, False, False, True, False, False] (insert [False, False, False, False, False, False, False, False, True, True] (insert [False, False, False, False, False, False, False, False, True, False] (insert [False, False, False, False, False, False, False, False, False, True] {a. length a = 10}))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. \<And>x. (x = [False, False, False, False, False, False, False, True, False, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10) = (length x = 10) proof (prove)
goal (2 subgoals):
 1. \<And>x. x = [False, False, False, False, False, False, False, True, False, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 \<Longrightarrow> length x = 10
 2. \<And>x. length x = 10 \<Longrightarrow> x = [False, False, False, False, False, False, False, True, False, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 proof (prove)
goal (1 subgoal):
 1. \<And>x. length x = 10 \<Longrightarrow> x = [False, False, False, False, False, False, False, True, False, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 proof (prove)
goal:
No subgoals!
theory ExampleSystem

lemma caps2_6_well_formed: "well_formed_cnode_n 10 caps2_6" apply (clarsimp simp: caps2_6_def well_formed_cnode_n_def) apply (clarsimp simp: the_nat_to_bl_10_def the_nat_to_bl_def nat_to_bl_def) apply (clarsimp simp: empty_cnode_def dom_def) apply (rule set_eqI, clarsimp) apply (rule iffI) apply (elim disjE, insert len_bin_to_bl, simp_all)[1] apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n 10 caps2_6 proof (prove)
goal (1 subgoal):
 1. insert (the_nat_to_bl_10 4) (insert (the_nat_to_bl_10 3) (insert (the_nat_to_bl_10 2) (insert (the_nat_to_bl_10 (Suc 0)) (dom (empty_cnode 10))))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. insert [False, False, False, False, False, False, False, True, False, False] (insert [False, False, False, False, False, False, False, False, True, True] (insert [False, False, False, False, False, False, False, False, True, False] (insert [False, False, False, False, False, False, False, False, False, True] (dom (empty_cnode 10))))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. insert [False, False, False, False, False, False, False, True, False, False] (insert [False, False, False, False, False, False, False, False, True, True] (insert [False, False, False, False, False, False, False, False, True, False] (insert [False, False, False, False, False, False, False, False, False, True] {a. length a = 10}))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. \<And>x. (x = [False, False, False, False, False, False, False, True, False, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10) = (length x = 10) proof (prove)
goal (2 subgoals):
 1. \<And>x. x = [False, False, False, False, False, False, False, True, False, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 \<Longrightarrow> length x = 10
 2. \<And>x. length x = 10 \<Longrightarrow> x = [False, False, False, False, False, False, False, True, False, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 proof (prove)
goal (1 subgoal):
 1. \<And>x. length x = 10 \<Longrightarrow> x = [False, False, False, False, False, False, False, True, False, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 proof (prove)
goal:
No subgoals!
theory ExampleSystem

lemma Sys2_wellformed: "pas_wellformed Sys2PAS" apply (clarsimp simp: Sys2PAS_def policy_wellformed_def) apply (intro conjI) apply (simp_all add: Sys2AuthGraph_def complete_AuthGraph_def
                       Sys2AuthGraph_aux_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_wellformed Sys2PAS proof (prove)
goal (1 subgoal):
 1. (\<forall>agent'. (UT2, Control, agent') \<in> Sys2AuthGraph \<longrightarrow> UT2 = agent') \<and> (\<forall>a. (UT2, a, UT2) \<in> Sys2AuthGraph) \<and> (\<forall>s r. (\<exists>ep. (s, Grant, ep) \<in> Sys2AuthGraph \<and> (r, Receive, ep) \<in> Sys2AuthGraph) \<longrightarrow> (s, Control, r) \<in> Sys2AuthGraph \<and> (r, Control, s) \<in> Sys2AuthGraph) \<and> (\<forall>ntfn. (IRQ2, Notify, ntfn) \<in> Sys2AuthGraph \<longrightarrow> (UT2, Notify, ntfn) \<in> Sys2AuthGraph) \<and> (\<forall>s ep. (s, Call, ep) \<in> Sys2AuthGraph \<longrightarrow> (s, SyncSend, ep) \<in> Sys2AuthGraph) \<and> (\<forall>s r. (\<exists>ep. (s, Call, ep) \<in> Sys2AuthGraph \<and> (r, Receive, ep) \<in> Sys2AuthGraph) \<longrightarrow> (r, Reply, s) \<in> Sys2AuthGraph) \<and> (\<forall>s r. (s, Reply, r) \<in> Sys2AuthGraph \<longrightarrow> (r, DeleteDerived, s) \<in> Sys2AuthGraph) \<and> (\<forall>l1 l2. (l1, DeleteDerived, l2) \<in> Sys2AuthGraph \<longrightarrow> (\<forall>l3. (l2, DeleteDerived, l3) \<in> Sys2AuthGraph \<longrightarrow> (l1, DeleteDerived, l3) \<in> Sys2AuthGraph)) \<and> (\<forall>s r. (\<exists>ep. (s, Call, ep) \<in> Sys2AuthGraph \<and> (r, Receive, ep) \<in> Sys2AuthGraph \<and> (r, Grant, ep) \<in> Sys2AuthGraph) \<longrightarrow> (s, Control, r) \<in> Sys2AuthGraph \<and> (r, Control, s) \<in> Sys2AuthGraph) proof (prove)
goal (9 subgoals):
 1. \<forall>agent'. (UT2, Control, agent') \<in> Sys2AuthGraph \<longrightarrow> UT2 = agent'
 2. \<forall>a. (UT2, a, UT2) \<in> Sys2AuthGraph
 3. \<forall>s r. (\<exists>ep. (s, Grant, ep) \<in> Sys2AuthGraph \<and> (r, Receive, ep) \<in> Sys2AuthGraph) \<longrightarrow> (s, Control, r) \<in> Sys2AuthGraph \<and> (r, Control, s) \<in> Sys2AuthGraph
 4. \<forall>ntfn. (IRQ2, Notify, ntfn) \<in> Sys2AuthGraph \<longrightarrow> (UT2, Notify, ntfn) \<in> Sys2AuthGraph
 5. \<forall>s ep. (s, Call, ep) \<in> Sys2AuthGraph \<longrightarrow> (s, SyncSend, ep) \<in> Sys2AuthGraph
 6. \<forall>s r. (\<exists>ep. (s, Call, ep) \<in> Sys2AuthGraph \<and> (r, Receive, ep) \<in> Sys2AuthGraph) \<longrightarrow> (r, Reply, s) \<in> Sys2AuthGraph
 7. \<forall>s r. (s, Reply, r) \<in> Sys2AuthGraph \<longrightarrow> (r, DeleteDerived, s) \<in> Sys2AuthGraph
 8. \<forall>l1 l2. (l1, DeleteDerived, l2) \<in> Sys2AuthGraph \<longrightarrow> (\<forall>l3. (l2, DeleteDerived, l3) \<in> Sys2AuthGraph \<longrightarrow> (l1, DeleteDerived, l3) \<in> Sys2AuthGraph)
 9. \<forall>s r. (\<exists>ep. (s, Call, ep) \<in> Sys2AuthGraph \<and> (r, Receive, ep) \<in> Sys2AuthGraph \<and> (r, Grant, ep) \<in> Sys2AuthGraph) \<longrightarrow> (s, Control, r) \<in> Sys2AuthGraph \<and> (r, Control, s) \<in> Sys2AuthGraph proof (prove)
goal:
No subgoals!
theory ExampleSystem

lemma Sys2AgentMap_simps:
  "Sys2AgentMap 5 = UT2"
  "Sys2AgentMap 6 = UT2"
  "Sys2AgentMap 7 = T2"
  "Sys2AgentMap 9 = T2"
  "Sys2AgentMap 3063 = UT2"
  "Sys2AgentMap 3065 = T2"
  "Sys2AgentMap 3072 = UT2"
  "Sys2AgentMap 3077 = T2"
  "Sys2AgentMap 3079 = UT2"
  "Sys2AgentMap 3080 = T2"
  "Sys2AgentMap 9001 = IRQ2" by (simp_all add: Sys2AgentMap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Sys2AgentMap 5 = UT2 &&& Sys2AgentMap 6 = UT2) &&& Sys2AgentMap 7 = T2 &&& Sys2AgentMap 9 = T2 &&& Sys2AgentMap 0xBF7 = UT2) &&& (Sys2AgentMap 0xBF9 = T2 &&& Sys2AgentMap 0xC00 = UT2 &&& Sys2AgentMap 0xC05 = T2) &&& Sys2AgentMap 0xC07 = UT2 &&& Sys2AgentMap 0xC08 = T2 &&& Sys2AgentMap 0x2329 = IRQ2
theory ExampleSystem

lemma domains_of_state_s2[simp]:
  "domains_of_state s2 = {}" apply (rule equalityI) apply (rule subsetI) apply clarsimp apply (erule domains_of_state_aux.induct) apply (simp add: s2_def exst1_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domains_of_state s2 = {} proof (prove)
goal (2 subgoals):
 1. domains_of_state s2 \<subseteq> {}
 2. {} \<subseteq> domains_of_state s2 proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> domains_of_state s2 \<Longrightarrow> x \<in> {}
 2. {} \<subseteq> domains_of_state s2 proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> domains_of_state s2 \<Longrightarrow> False
 2. {} \<subseteq> domains_of_state s2 proof (prove)
goal (2 subgoals):
 1. \<And>a b ptr etcb d. \<lbrakk>ekheap s2 ptr = Some etcb; d = tcb_domain etcb\<rbrakk> \<Longrightarrow> False
 2. {} \<subseteq> domains_of_state s2 proof (prove)
goal (1 subgoal):
 1. {} \<subseteq> domains_of_state s2 proof (prove)
goal:
No subgoals!
theory ExampleSystem

lemma thread_bound_ntfns_2[simp]:
  "thread_bound_ntfns s2 = Map.empty" unfolding s2_def thread_bound_ntfns_def apply (rule ext) apply (simp add: get_tcb_def) apply (simp add: kh2_def kh2_obj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_bound_ntfns s2 = (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. case get_tcb p \<lparr>kheap = kh2, cdt = \<lambda>x. None, is_original_cap = undefined, cur_thread = undefined, idle_thread = undefined, machine_state = undefined, interrupt_irq_node = \<lambda>_. 0x2329, interrupt_states = undefined, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = undefined, arm_next_asid = undefined, arm_asid_map = undefined, arm_global_pd = undefined, arm_global_pts = undefined, arm_kernel_vspace = undefined\<rparr>, exst = exst1\<rparr> of None \<Rightarrow> None | Some x \<Rightarrow> tcb_bound_notification x) = (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. \<And>p. (case get_tcb p \<lparr>kheap = kh2, cdt = \<lambda>x. None, is_original_cap = undefined, cur_thread = undefined, idle_thread = undefined, machine_state = undefined, interrupt_irq_node = \<lambda>_. 0x2329, interrupt_states = undefined, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = undefined, arm_next_asid = undefined, arm_asid_map = undefined, arm_global_pd = undefined, arm_global_pts = undefined, arm_kernel_vspace = undefined\<rparr>, exst = exst1\<rparr> of None \<Rightarrow> None | Some x \<Rightarrow> tcb_bound_notification x) = None proof (prove)
goal (1 subgoal):
 1. \<And>p. (case case kh2 p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | Some _ \<Rightarrow> None of None \<Rightarrow> None | Some x2 \<Rightarrow> tcb_bound_notification x2) = None proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma un_eq:
  "\<lbrakk> S = S'; T = T' \<rbrakk> \<Longrightarrow> S \<union> T = S' \<union> T'" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S = S'; T = T'\<rbrakk> \<Longrightarrow> S \<union> T = S' \<union> T'
theory Noninterference_Base

lemma Un_eq:
  "\<lbrakk> \<And>x y. \<lbrakk> x \<in> xs; y \<in> ys \<rbrakk> \<Longrightarrow> P x = Q y; \<exists>x. x \<in> xs; \<exists>y. y \<in> ys \<rbrakk>
     \<Longrightarrow> (\<Union>x \<in> xs. P x) = (\<Union>y \<in> ys. Q y)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. \<lbrakk>x \<in> xs; y \<in> ys\<rbrakk> \<Longrightarrow> P x = Q y; \<exists>x. x \<in> xs; \<exists>y. y \<in> ys\<rbrakk> \<Longrightarrow> \<Union> (P ` xs) = \<Union> (Q ` ys)
theory Noninterference_Base

lemma Int_eq:
  "\<lbrakk> \<And>x y. \<lbrakk> x \<in> xs; y \<in> ys \<rbrakk> \<Longrightarrow> P x = Q y; \<exists>x. x \<in> xs; \<exists>y. y \<in> ys \<rbrakk>
     \<Longrightarrow> (\<Inter>x \<in> xs. P x) = (\<Inter>y \<in> ys. Q y)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. \<lbrakk>x \<in> xs; y \<in> ys\<rbrakk> \<Longrightarrow> P x = Q y; \<exists>x. x \<in> xs; \<exists>y. y \<in> ys\<rbrakk> \<Longrightarrow> \<Inter> (P ` xs) = \<Inter> (Q ` ys)
theory Noninterference_Base

lemma Un_eq_Int:
  assumes ex: "\<exists>x. x \<in> xs"
  assumes ey: "\<exists>y. y \<in> ys"
  assumes a: "\<And>x y. \<lbrakk> x \<in> xs; y \<in> ys \<rbrakk> \<Longrightarrow> S x = S' y"
  shows "(\<Union>x \<in> xs. S x) = (\<Inter>x \<in> ys. S' x)" apply (rule equalityI) apply (clarsimp) apply (drule a, assumption, simp) apply clarsimp apply (insert ex ey) apply clarsimp apply (frule a, assumption) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Union> (S ` xs) = \<Inter> (S' ` ys) proof (prove)
goal (2 subgoals):
 1. \<Union> (S ` xs) \<subseteq> \<Inter> (S' ` ys)
 2. \<Inter> (S' ` ys) \<subseteq> \<Union> (S ` xs) proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>xa \<in> xs; x \<in> S xa; xb \<in> ys\<rbrakk> \<Longrightarrow> x \<in> S' xb
 2. \<Inter> (S' ` ys) \<subseteq> \<Union> (S ` xs) proof (prove)
goal (1 subgoal):
 1. \<Inter> (S' ` ys) \<subseteq> \<Union> (S ` xs) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>xa\<in>ys. x \<in> S' xa \<Longrightarrow> \<exists>xa\<in>xs. x \<in> S xa proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>xa\<in>ys. x \<in> S' xa; \<exists>x. x \<in> xs; \<exists>y. y \<in> ys\<rbrakk> \<Longrightarrow> \<exists>xa\<in>xs. x \<in> S xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa y. \<lbrakk>\<forall>xa\<in>ys. x \<in> S' xa; xa \<in> xs; y \<in> ys\<rbrakk> \<Longrightarrow> \<exists>xa\<in>xs. x \<in> S xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa y. \<lbrakk>\<forall>xa\<in>ys. x \<in> S' xa; xa \<in> xs; y \<in> ys; S xa = S' y\<rbrakk> \<Longrightarrow> \<exists>xa\<in>xs. x \<in> S xa proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Run_trans:
  "\<lbrakk> (s,t) \<in> Run Stepf as; (t,u) \<in> Run Stepf bs \<rbrakk>
     \<Longrightarrow> (s,u) \<in> Run Stepf (as @ bs)" by (induct as arbitrary: bs s t u) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, t) \<in> Run Stepf as; (t, u) \<in> Run Stepf bs\<rbrakk> \<Longrightarrow> (s, u) \<in> Run Stepf (as @ bs)
theory Noninterference_Base

lemma Run_app:
  "Run Stepf (as @ bs) = (Run Stepf as) O (Run Stepf bs)" apply (rule equalityI) apply (fastforce dest: Run_mid) apply (fastforce intro: Run_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Run Stepf (as @ bs) = Run Stepf as O Run Stepf bs proof (prove)
goal (2 subgoals):
 1. Run Stepf (as @ bs) \<subseteq> Run Stepf as O Run Stepf bs
 2. Run Stepf as O Run Stepf bs \<subseteq> Run Stepf (as @ bs) proof (prove)
goal (1 subgoal):
 1. Run Stepf as O Run Stepf bs \<subseteq> Run Stepf (as @ bs) proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma reachable_enabled:
  "reachable s \<Longrightarrow> \<exists>s'. s' \<in> execution A s js" apply (simp add: reachable_def) apply (erule enabled) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> \<exists>s'. s' \<in> execution A s js proof (prove)
goal (1 subgoal):
 1. \<exists>js. s \<in> execution A s0 js \<Longrightarrow> \<exists>s'. s' \<in> execution A s js proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma enabled_Step:
  "reachable s \<Longrightarrow> \<exists>s'. (s,s') \<in> Step a" by (simp add: Step_def, blast intro: reachable_enabled)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> \<exists>s'. (s, s') \<in> local.Step a
theory Noninterference_Base

lemma execution_Run':
  "s \<in> execution A s0 js \<Longrightarrow> execution A s as = {s'. (s,s') \<in> Run Step as}" apply (rule execution_Run) apply (fastforce simp: reachable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<in> execution A s0 js \<Longrightarrow> execution A s as = {s'. (s, s') \<in> Run local.Step as} proof (prove)
goal (1 subgoal):
 1. s \<in> execution A s0 js \<Longrightarrow> reachable s proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma reachable_Run:
  "reachable s \<Longrightarrow> \<exists>as. (s0,s) \<in> Run Step as" apply (clarsimp simp add: reachable_def) apply (cut_tac as=js in execution_Run[OF reachable_s0]) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> \<exists>as. (s0, s) \<in> Run local.Step as proof (prove)
goal (1 subgoal):
 1. \<And>js. s \<in> execution A s0 js \<Longrightarrow> \<exists>as. (s0, s) \<in> Run local.Step as proof (prove)
goal (1 subgoal):
 1. \<And>js. \<lbrakk>s \<in> execution A s0 js; execution A s0 js = {s'. (s0, s') \<in> Run local.Step js}\<rbrakk> \<Longrightarrow> \<exists>as. (s0, s) \<in> Run local.Step as proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma Run_reachable:
  "\<exists>as. (s0,s) \<in> Run Step as \<Longrightarrow> reachable s" apply (clarsimp simp add: reachable_def) apply (cut_tac as=as in execution_Run[OF reachable_s0]) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>as. (s0, s) \<in> Run local.Step as \<Longrightarrow> reachable s proof (prove)
goal (1 subgoal):
 1. \<And>as. (s0, s) \<in> Run local.Step as \<Longrightarrow> \<exists>js. s \<in> execution A s0 js proof (prove)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>(s0, s) \<in> Run local.Step as; execution A s0 as = {s'. (s0, s') \<in> Run local.Step as}\<rbrakk> \<Longrightarrow> \<exists>js. s \<in> execution A s0 js proof (prove)
goal:
No subgoals!
theory Noninterference_Base

lemma reachable_execution:
  "\<lbrakk> reachable s; s' \<in> execution A s js \<rbrakk> \<Longrightarrow> reachable s'" apply (clarsimp simp: reachable_def) apply (rule_tac x="jsa @ js" in exI) apply (frule execution_Run'[where s=s and as=js]) apply (simp add: execution_Run[where s=s0, simplified reachable_s0]) apply (fastforce simp: Run_app) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; s' \<in> execution A s js\<rbrakk> \<Longrightarrow> reachable s' proof (prove)
goal (1 subgoal):
 1. \<And>jsa. \<lbrakk>s' \<in> execution A s js; s \<in> execution A s0 jsa\<rbrakk> \<Longrightarrow> \<exists>js. s' \<in> execution A s0 js proof (prove)
goal (1 subgoal):
 1. \<And>jsa. \<lbrakk>s' \<in> execution A s js; s \<in> execution A s0 jsa\<rbrakk> \<Longrightarrow> s' \<in> execution A s0 (jsa @ js) proof (prove)
goal (1 subgoal):
 1. \<And>jsa. \<lbrakk>s' \<in> execution A s js; s \<in> execution A s0 jsa; execution A s js = {s'. (s, s') \<in> Run local.Step js}\<rbrakk> \<Longrightarrow> s' \<in> execution A s0 (jsa @ js) proof (prove)
goal (1 subgoal):
 1. \<And>jsa. \<lbrakk>(s, s') \<in> Run local.Step js; (s0, s) \<in> Run local.Step jsa; execution A s js = {s'. (s, s') \<in> Run local.Step js}\<rbrakk> \<Longrightarrow> (s0, s') \<in> Run local.Step (jsa @ js) proof (prove)
goal:
No subgoals!