kings-crown/FVELER_Isabelle huggingface dataset:
theory EquivValid

lemma assertE_ev[wp]:
  "equiv_valid_inv I A \<top> (assertE b)" unfolding assertE_def apply wp by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>_. True) (assertE b) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>_. True) (if b then returnOk () else fail) proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (b \<longrightarrow> True) \<and> (\<not> b \<longrightarrow> True)
theory EquivValid

lemma rel_sum_comb_equals:
  "((=) \<oplus> (=)) = (=)" apply(rule ext) apply(rule ext) apply(rename_tac a b) apply(case_tac a, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (=) \<oplus> (=) = (=) proof (prove)
goal (1 subgoal):
 1. \<And>x. ((=) \<oplus> (=)) x = (=) x proof (prove)
goal (1 subgoal):
 1. \<And>x xa. ((=) \<oplus> (=)) x xa = (x = xa) proof (prove)
goal (1 subgoal):
 1. \<And>a b. ((=) \<oplus> (=)) a b = (a = b) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma spec_equiv_valid_def2:
  "spec_equiv_valid s I A A P f =
   spec_equiv_valid_2_inv s I A (=) P P f f" apply(simp add: spec_equiv_valid_def spec_equiv_valid_2_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_inv s I A P f = spec_equiv_valid_2_inv s I A (=) P P f f proof (prove)
goal:
No subgoals!
theory EquivValid

lemma drop_spec_ev2_inv:
  "equiv_valid_2 I A A R P P' f f' \<Longrightarrow>
   spec_equiv_valid_2_inv s I A R P P' f f'" apply(simp add: spec_equiv_valid_2_inv_def) apply(erule equiv_valid_2_guard_imp, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A A R P P' f f' \<Longrightarrow> spec_equiv_valid_2_inv s I A R P P' f f' proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A A R P P' f f' \<Longrightarrow> equiv_valid_2 I A A R (P and (=) s) P' f f' proof (prove)
goal:
No subgoals!
theory EquivValid

lemma spec_equiv_valid_2_inv_guard_imp:
  "\<lbrakk>spec_equiv_valid_2_inv s I A R Q Q' f f'; \<And> s. P s \<Longrightarrow> Q s; \<And> s. P' s \<Longrightarrow> Q' s\<rbrakk> \<Longrightarrow>
    spec_equiv_valid_2_inv s I A R P P' f f'" by(auto simp: spec_equiv_valid_2_inv_def equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec_equiv_valid_2_inv s I A R Q Q' f f'; \<And>s. P s \<Longrightarrow> Q s; \<And>s. P' s \<Longrightarrow> Q' s\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s I A R P P' f f'
theory EquivValid

lemma equiv_valid_rv_gets_compD:
  "equiv_valid_rv_inv I A R P (gets (f \<circ> g)) \<Longrightarrow>
   equiv_valid_rv_inv I A (\<lambda> rv rv'. R (f rv) (f rv')) P (gets g)" apply(clarsimp simp: equiv_valid_2_def gets_def bind_def return_def get_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A R P (gets (f \<circ> g)) \<Longrightarrow> equiv_valid_rv_inv I A (\<lambda>rv rv'. R (f rv) (f rv')) P (gets g) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma liftE_ev2:
  "equiv_valid_2 I A B R P P' f f' \<Longrightarrow>
   equiv_valid_2 I A B (E \<oplus> R) P P' (liftE f) (liftE f')" apply(clarsimp simp: liftE_def equiv_valid_2_def bind_def return_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A B R P P' f f' \<Longrightarrow> equiv_valid_2 I A B (E \<oplus> R) P P' (liftE f) (liftE f') proof (prove)
goal (1 subgoal):
 1. \<And>s t a b ab bb. \<lbrakk>\<forall>s t. P s \<and> P' t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f' t). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> I s' t' \<and> B s' t'); (a, b) \<in> fst (f s); (ab, bb) \<in> fst (f' t); P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> R a ab \<and> I b bb \<and> B b bb proof (prove)
goal:
No subgoals!
theory EquivValid

lemma whenE_spec_ev2_inv:
  assumes a: "b \<Longrightarrow> spec_equiv_valid_2_inv s I A R P P' m m'"
  assumes r: "\<And> x. R x x"
  shows "spec_equiv_valid_2_inv s I A R P P' (whenE b m) (whenE b m')" unfolding whenE_def apply (auto intro: a simp: returnOk_def intro!: drop_spec_ev2_inv[OF return_ev2] intro: r) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_2_inv s I A R P P' (whenE b m) (whenE b m') proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_2_inv s I A R P P' (if b then m else returnOk ()) (if b then m' else returnOk ()) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma whenE_spec_ev:
  assumes a: "b \<Longrightarrow> spec_equiv_valid_inv s I A P m"
  shows "spec_equiv_valid_inv s I A P  (whenE b m) " unfolding whenE_def apply (auto intro: a simp: returnOk_def intro!: drop_spec_ev[OF return_ev_pre]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_inv s I A P (whenE b m) proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_inv s I A P (if b then m else returnOk ()) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma spec_equiv_valid_2_inv_by_spec_equiv_valid:
  "\<lbrakk>spec_equiv_valid s I A A P f; P' = P; f' = f;
    (\<And> a. R a a)\<rbrakk> \<Longrightarrow>
       spec_equiv_valid_2_inv s I A R P P' f f'" apply(clarsimp simp: spec_equiv_valid_def spec_equiv_valid_2_inv_def) apply(fastforce simp: equiv_valid_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec_equiv_valid_inv s I A P f; P' = P; f' = f; \<And>a. R a a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s I A R P P' f f' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_valid_2 I A A (=) (P and (=) s) P f f; P' = P; f' = f; \<And>a. R a a\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A R (P and (=) s) P f f proof (prove)
goal:
No subgoals!
theory EquivValid

lemma mapM_ev'':
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (P x) (m x)"
  assumes inv: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> \<lambda>s. \<forall>x\<in>set lst. P x s \<rbrace> m x \<lbrace> \<lambda>_ s. \<forall>x\<in>set lst. P x s \<rbrace>"
  shows "equiv_valid_inv D A (\<lambda> s. \<forall>x\<in>set lst. P x s) (mapM m lst)" apply(rule mapM_ev) apply(rule equiv_valid_guard_imp[OF reads_res]; simp) apply(wpsimp wp: inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A (\<lambda>s. \<forall>x\<in>set lst. P x s) (mapM m lst) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (\<lambda>s. \<forall>x\<in>set lst. P x s) (m x)
 2. \<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set lst. P x s\<rbrace> m x \<lbrace>\<lambda>_ s. \<forall>x\<in>set lst. P x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set lst. P x s\<rbrace> m x \<lbrace>\<lambda>_ s. \<forall>x\<in>set lst. P x s\<rbrace> proof (prove)
goal:
No subgoals!
theory EquivValid

lemma mapM_x_ev'':
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (P x) (m x)"
  assumes inv: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> \<lambda>s. \<forall>x\<in>set lst. P x s \<rbrace> m x \<lbrace> \<lambda>_ s. \<forall>x\<in>set lst. P x s \<rbrace>"
  shows "equiv_valid_inv D A (\<lambda> s. \<forall>x\<in>set lst. P x s) (mapM_x m lst)" apply(rule mapM_x_ev) apply(rule equiv_valid_guard_imp[OF reads_res]; simp) apply(wpsimp wp: inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A (\<lambda>s. \<forall>x\<in>set lst. P x s) (mapM_x m lst) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (\<lambda>s. \<forall>x\<in>set lst. P x s) (m x)
 2. \<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set lst. P x s\<rbrace> m x \<lbrace>\<lambda>_ s. \<forall>x\<in>set lst. P x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>set lst. P x s\<rbrace> m x \<lbrace>\<lambda>_ s. \<forall>x\<in>set lst. P x s\<rbrace> proof (prove)
goal:
No subgoals!
theory EquivValid

lemma catch_ev[wp]:
  assumes ok:
    "equiv_valid I A A P f"
  assumes err:
    "\<And> e. equiv_valid I A A (E e) (handler e)"
  assumes hoare:
    "\<lbrace> Q \<rbrace> f -, \<lbrace> E \<rbrace>"
  shows
    "equiv_valid I A A (P and Q) (f <catch> handler)" apply (simp add: catch_def) apply (wp err ok | wpc | simp)+ apply (insert hoare[simplified validE_E_def validE_def])[1] apply (simp split: sum.splits) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (P and Q) (f <catch> handler) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (P and Q) (do x <- f;
case x of Inl e \<Rightarrow> handler e | Inr b \<Rightarrow> return b
od) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. rv = Inl x \<longrightarrow> E x s\<rbrace>
 2. \<And>s. (P and Q) s \<Longrightarrow> P s \<and> ?P'' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True\<rbrace> \<Longrightarrow> \<lbrace>?P''\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. rv = Inl x \<longrightarrow> E x s\<rbrace>
 2. \<And>s. (P and Q) s \<Longrightarrow> P s \<and> ?P'' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P and Q) s \<Longrightarrow> P s \<and> Q s
theory EquivValid

lemma equiv_valid_rv_trivial:
  assumes inv: "\<And> P. \<lbrace> P \<rbrace> f \<lbrace> \<lambda>_. P \<rbrace>"
  shows "equiv_valid_rv_inv I A \<top>\<top> \<top> f" by(auto simp: equiv_valid_2_def dest: state_unchanged[OF inv])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A (\<lambda>_ _. True) (\<lambda>_. True) f
theory EquivValid

lemma equiv_valid_2_trivial:
  assumes inv: "\<And> P. \<lbrace> P \<rbrace> f \<lbrace> \<lambda>_. P \<rbrace>"
  assumes inv': "\<And> P. \<lbrace> P \<rbrace> f' \<lbrace> \<lambda>_. P \<rbrace>"
  shows "equiv_valid_2 I A A \<top>\<top> \<top> \<top> f f'" by(auto simp: equiv_valid_2_def dest: state_unchanged[OF inv] state_unchanged[OF inv'])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A A (\<lambda>_ _. True) (\<lambda>_. True) (\<lambda>_. True) f f'
theory EquivValid

lemma gen_asm_ev2_r:
  "\<lbrakk>P' \<Longrightarrow> equiv_valid_2 I A B R P Q f f'\<rbrakk> \<Longrightarrow>
   equiv_valid_2 I A B R P  (Q and (K P')) f f'" apply(fastforce simp: equiv_valid_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P' \<Longrightarrow> equiv_valid_2 I A B R P Q f f') \<Longrightarrow> equiv_valid_2 I A B R P (Q and K P') f f' proof (prove)
goal:
No subgoals!
theory EquivValid

lemma gen_asm_ev2_l:
  "\<lbrakk>P \<Longrightarrow> equiv_valid_2 I A B R Q P' f f'\<rbrakk> \<Longrightarrow>
   equiv_valid_2 I A B R (Q and (K P)) P' f f'" apply(fastforce simp: equiv_valid_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> equiv_valid_2 I A B R Q P' f f') \<Longrightarrow> equiv_valid_2 I A B R (Q and K P) P' f f' proof (prove)
goal:
No subgoals!
theory EquivValid

lemma gen_asm_ev2_r':
  "\<lbrakk>P' \<Longrightarrow> equiv_valid_2 I A B R P \<top> f f'\<rbrakk> \<Longrightarrow>
   equiv_valid_2 I A B R P (\<lambda>s. P') f f'" apply(fastforce simp: equiv_valid_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P' \<Longrightarrow> equiv_valid_2 I A B R P (\<lambda>_. True) f f') \<Longrightarrow> equiv_valid_2 I A B R P (\<lambda>s. P') f f' proof (prove)
goal:
No subgoals!
theory EquivValid

lemma gen_asm_ev2_l':
  "\<lbrakk>P \<Longrightarrow> equiv_valid_2 I A B R \<top> P' f f'\<rbrakk> \<Longrightarrow>
   equiv_valid_2 I A B R (\<lambda>s. P) P' f f'" apply(fastforce simp: equiv_valid_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> equiv_valid_2 I A B R (\<lambda>_. True) P' f f') \<Longrightarrow> equiv_valid_2 I A B R (\<lambda>s. P) P' f f' proof (prove)
goal:
No subgoals!
theory EquivValid

lemma if_evrv:
  assumes "b \<Longrightarrow> equiv_valid_rv_inv I A R P f"
  assumes "\<not> b \<Longrightarrow> equiv_valid_rv_inv I A R Q g"
  shows "equiv_valid_rv_inv I A R (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s)) (if b then f else g)" apply (clarsimp split: if_split) using assms by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A R (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not> b \<longrightarrow> Q s)) (if b then f else g) proof (prove)
goal (1 subgoal):
 1. (b \<longrightarrow> equiv_valid_rv_inv I A R P f) \<and> (\<not> b \<longrightarrow> equiv_valid_rv_inv I A R Q g) proof (prove)
using this:
b \<Longrightarrow> equiv_valid_rv_inv I A R P f
\<not> b \<Longrightarrow> equiv_valid_rv_inv I A R Q g

goal (1 subgoal):
 1. (b \<longrightarrow> equiv_valid_rv_inv I A R P f) \<and> (\<not> b \<longrightarrow> equiv_valid_rv_inv I A R Q g)
theory InfoFlow_IF

lemma pas_domains_distinct_inj:
  "\<lbrakk> pas_domains_distinct aag; l1 \<in> pasDomainAbs aag d; l2 \<in> pasDomainAbs aag d \<rbrakk>
     \<Longrightarrow> l1 = l2" apply (clarsimp simp: pas_domains_distinct_def) apply (drule_tac x=d in spec) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_domains_distinct aag; l1 \<in> pasDomainAbs aag d; l2 \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> l1 = l2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>d. \<exists>l. pasDomainAbs aag d = {l}; l1 \<in> pasDomainAbs aag d; l2 \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> l1 = l2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l1 \<in> pasDomainAbs aag d; l2 \<in> pasDomainAbs aag d; \<exists>l. pasDomainAbs aag d = {l}\<rbrakk> \<Longrightarrow> l1 = l2 proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma domain_has_unique_label:
  "pas_domains_distinct aag \<Longrightarrow> \<exists>l. pasDomainAbs aag d = {l}" by (simp add: pas_domains_distinct_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_domains_distinct aag \<Longrightarrow> \<exists>l. pasDomainAbs aag d = {l}
theory InfoFlow_IF

lemma aag_can_read_self:
  "is_subject aag x \<Longrightarrow> aag_can_read aag x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_subject aag x \<Longrightarrow> aag_can_read aag x
theory InfoFlow_IF

lemma aag_can_read_read:
  "aag_has_auth_to aag Read x \<Longrightarrow> aag_can_read aag x" by (rule reads_read)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pasSubject aag, Read, pasObjectAbs aag x) \<in> pasPolicy aag \<Longrightarrow> aag_can_read aag x
theory InfoFlow_IF

lemma aag_can_read_irq_self:
  "is_subject_irq aag x \<Longrightarrow> aag_can_read_irq aag x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_subject_irq aag x \<Longrightarrow> aag_can_read_irq aag x
theory InfoFlow_IF

lemma equiv_forE:
  assumes e: "equiv_for P f c c'"
  obtains "\<And>x. P x \<Longrightarrow> f c x = f c' x" apply (erule meta_mp) apply(erule e[simplified equiv_for_def, rule_format]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<And>x. P x \<Longrightarrow> f c x = f c' x) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<And>x. P x \<Longrightarrow> f c x = f c' x proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma equiv_forI:
  "(\<And>x. P x \<Longrightarrow> f c x = f c' x) \<Longrightarrow> equiv_for P f c c'" by(simp add: equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. P x \<Longrightarrow> f c x = f c' x) \<Longrightarrow> equiv_for P f c c'
theory InfoFlow_IF

lemma equiv_forD:
  "\<lbrakk> equiv_for P f c c'; P x \<rbrakk> \<Longrightarrow> f c x = f c' x" by (blast elim: equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_for P f c c'; P x\<rbrakk> \<Longrightarrow> f c x = f c' x
theory InfoFlow_IF

lemma equiv_for_comp:
  "equiv_for P (f \<circ> g) s s' = equiv_for P f (g s) (g s')" by (simp add: equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_for P (f \<circ> g) s s' = equiv_for P f (g s) (g s')
theory InfoFlow_IF

lemma equiv_for_or:
  "equiv_for (A or B) f c c' = (equiv_for A f c c' \<and> equiv_for B f c c')" by (fastforce simp: equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_for (A or B) f c c' = (equiv_for A f c c' \<and> equiv_for B f c c')
theory InfoFlow_IF

lemma equiv_for_id_update:
  "equiv_for P id c c' \<Longrightarrow>
   equiv_for P id (c(x := v)) (c'(x := v))" by (simp add: equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_for P id c c' \<Longrightarrow> equiv_for P id (c(x := v)) (c'(x := v))
theory InfoFlow_IF

lemma states_equiv_forI:
  "\<lbrakk> equiv_for P kheap s s';
     equiv_machine_state P (machine_state s) (machine_state s');
     equiv_for (P \<circ> fst) cdt s s';
     equiv_for P ekheap s s';
     equiv_for (P \<circ> fst) cdt_list s s';
     equiv_for (P \<circ> fst) is_original_cap s s';
     equiv_for Q interrupt_states s s';
     equiv_for Q interrupt_irq_node s s';
     equiv_asids R s s';
     equiv_for S ready_queues s s' \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S s s'" by (auto simp: states_equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_for P kheap s s'; equiv_machine_state P (machine_state s) (machine_state s'); equiv_for (P \<circ> fst) cdt s s'; equiv_for P ekheap s s'; equiv_for (P \<circ> fst) cdt_list s s'; equiv_for (P \<circ> fst) is_original_cap s s'; equiv_for Q interrupt_states s s'; equiv_for Q interrupt_irq_node s s'; equiv_asids R s s'; equiv_for S ready_queues s s'\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S s s'
theory InfoFlow_IF

lemma states_equiv_for_machine_state_update:
  "\<lbrakk> states_equiv_for P Q R S s s'; equiv_machine_state P kh kh' \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>machine_state := kh\<rparr>) (s'\<lparr>machine_state := kh'\<rparr>)" by (fastforce elim: equiv_forE elim!: equiv_asids_triv
               intro: equiv_forI simp: states_equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s s'; equiv_machine_state P kh kh'\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>machine_state := kh\<rparr>) (s'\<lparr>machine_state := kh'\<rparr>)
theory InfoFlow_IF

lemma states_equiv_for_cdt_update:
  "\<lbrakk> states_equiv_for P Q R S s s'; equiv_for (P \<circ> fst) id kh kh' \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>cdt := kh\<rparr>) (s'\<lparr>cdt := kh'\<rparr>)" by (fastforce elim: equiv_forE elim!: equiv_asids_triv
               intro: equiv_forI simp: states_equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s s'; equiv_for (P \<circ> fst) id kh kh'\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>cdt := kh\<rparr>) (s'\<lparr>cdt := kh'\<rparr>)
theory InfoFlow_IF

lemma states_equiv_for_cdt_list_update:
  "\<lbrakk> states_equiv_for P Q R S s s'; equiv_for (P \<circ> fst) id (kh (cdt_list s)) (kh' (cdt_list s')) \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S (cdt_list_update kh s) (cdt_list_update kh' s')" by (fastforce elim: equiv_forE elim!: equiv_asids_triv
               intro: equiv_forI simp: states_equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s s'; equiv_for (P \<circ> fst) id (kh (cdt_list s)) (kh' (cdt_list s'))\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (cdt_list_update kh s) (cdt_list_update kh' s')
theory InfoFlow_IF

lemma states_equiv_for_is_original_cap_update:
  "\<lbrakk> states_equiv_for P Q R S s s'; equiv_for (P \<circ> fst) id kh kh' \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>is_original_cap := kh\<rparr>) (s'\<lparr>is_original_cap := kh'\<rparr>)" by (fastforce elim: equiv_forE elim!: equiv_asids_triv
               intro: equiv_forI simp: states_equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s s'; equiv_for (P \<circ> fst) id kh kh'\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>is_original_cap := kh\<rparr>) (s'\<lparr>is_original_cap := kh'\<rparr>)
theory InfoFlow_IF

lemma states_equiv_for_interrupt_states_update:
  "\<lbrakk> states_equiv_for P Q R S s s'; equiv_for Q id kh kh' \<rbrakk>
    \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>interrupt_states := kh\<rparr>) (s'\<lparr>interrupt_states := kh'\<rparr>)" by (fastforce elim: equiv_forE elim!: equiv_asids_triv
               intro: equiv_forI simp: states_equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s s'; equiv_for Q id kh kh'\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>interrupt_states := kh\<rparr>) (s'\<lparr>interrupt_states := kh'\<rparr>)
theory InfoFlow_IF

lemma states_equiv_for_interrupt_irq_node_update:
  "\<lbrakk> states_equiv_for P Q R S s s'; equiv_for Q id kh kh' \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>interrupt_irq_node := kh\<rparr>) (s'\<lparr>interrupt_irq_node := kh'\<rparr>)" by (fastforce elim: equiv_forE elim!: equiv_asids_triv
               intro: equiv_forI simp: states_equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s s'; equiv_for Q id kh kh'\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>interrupt_irq_node := kh\<rparr>) (s'\<lparr>interrupt_irq_node := kh'\<rparr>)
theory InfoFlow_IF

lemma states_equiv_for_ready_queues_update:
  "\<lbrakk> states_equiv_for P Q R S s s'; equiv_for S id kh kh' \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S (s\<lparr>ready_queues := kh\<rparr>) (s'\<lparr>ready_queues := kh'\<rparr>)" by (fastforce elim: equiv_forE elim!: equiv_asids_triv
               intro: equiv_forI simp: states_equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s s'; equiv_for S id kh kh'\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (ready_queues_update (\<lambda>_. kh) s) (ready_queues_update (\<lambda>_. kh') s')
theory InfoFlow_IF

lemma states_equiv_for_ekheap_update:
  "\<lbrakk> states_equiv_for P Q R S s s'; equiv_for P id (kh (ekheap s)) (kh' (ekheap s')) \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S (ekheap_update kh s) (ekheap_update kh' s')" by (fastforce elim: equiv_forE elim!: equiv_asids_triv
               intro: equiv_forI simp: states_equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s s'; equiv_for P id (kh (ekheap s)) (kh' (ekheap s'))\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (ekheap_update kh s) (ekheap_update kh' s')
theory InfoFlow_IF

lemma states_equiv_for_identical_ekheap_updates:
  "\<lbrakk> states_equiv_for P Q R S s s'; identical_ekheap_updates s s' (kh (ekheap s)) (kh' (ekheap s')) \<rbrakk>
     \<Longrightarrow> states_equiv_for P Q R S (ekheap_update kh s) (ekheap_update kh' s')" by (fastforce simp: identical_ekheap_updates_def equiv_for_def states_equiv_for_def equiv_asids_triv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>states_equiv_for P Q R S s s'; identical_ekheap_updates s s' (kh (ekheap s)) (kh' (ekheap s'))\<rbrakk> \<Longrightarrow> states_equiv_for P Q R S (ekheap_update kh s) (ekheap_update kh' s')