kings-crown/FVELER_Isabelle huggingface dataset:
theory InfoFlow_IF

lemma reads_equiv_work_units_completed_update':
  "reads_equiv aag s s' \<Longrightarrow>
   reads_equiv aag (s\<lparr>work_units_completed := (f (work_units_completed s))\<rparr>)
                   (s'\<lparr>work_units_completed := (f (work_units_completed s'))\<rparr>)" by (fastforce simp: reads_equiv_def2 states_equiv_for_def equiv_for_def elim!: equiv_asids_triv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv aag s s' \<Longrightarrow> reads_equiv aag (work_units_completed_update (\<lambda>_. f (work_units_completed s)) s) (work_units_completed_update (\<lambda>_. f (work_units_completed s')) s')
theory InfoFlow_IF

lemma affects_equiv_def2:
  "affects_equiv aag l s s' = states_equiv_for (aag_can_affect aag l)
                                               (aag_can_affect_irq aag l)
                                               (aag_can_affect_asid aag l)
                                               (aag_can_affect_domain aag l) s s'" by (auto simp: affects_equiv_def
           dest: equiv_forD
          elim!: states_equiv_forE
         intro!: states_equiv_forI equiv_forI equiv_asids_False)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. affects_equiv aag l s s' = states_equiv_for (aag_can_affect aag l) (aag_can_affect_irq aag l) (aag_can_affect_asid aag l) (aag_can_affect_domain aag l) s s'
theory InfoFlow_IF

lemma affects_equivE:
  assumes sef: "affects_equiv aag l s s'"
  obtains "equiv_for (aag_can_affect aag l) kheap s s'"
          "equiv_machine_state (aag_can_affect aag l) (machine_state s) (machine_state s')"
          "equiv_for ((aag_can_affect aag l) \<circ> fst) cdt s s'"
          "equiv_for ((aag_can_affect aag l) \<circ> fst) cdt_list s s'"
          "equiv_for (aag_can_affect aag l) ekheap s s'"
          "equiv_for ((aag_can_affect aag l) \<circ> fst) is_original_cap s s'"
          "equiv_for (aag_can_affect_irq aag l) interrupt_states s s'"
          "equiv_for (aag_can_affect_irq aag l) interrupt_irq_node s s'"
          "equiv_asids (aag_can_affect_asid aag l) s s'"
          "equiv_for (aag_can_affect_domain aag l) ready_queues s s'" using sef by (auto simp: affects_equiv_def2 elim: states_equiv_forE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>equiv_for (aag_can_affect aag l) kheap s s'; equiv_machine_state (aag_can_affect aag l) (machine_state s) (machine_state s'); equiv_for (aag_can_affect aag l \<circ> fst) cdt s s'; equiv_for (aag_can_affect aag l \<circ> fst) cdt_list s s'; equiv_for (aag_can_affect aag l) ekheap s s'; equiv_for (aag_can_affect aag l \<circ> fst) is_original_cap s s'; equiv_for (aag_can_affect_irq aag l) interrupt_states s s'; equiv_for (aag_can_affect_irq aag l) interrupt_irq_node s s'; equiv_asids (aag_can_affect_asid aag l) s s'; equiv_for (aag_can_affect_domain aag l) ready_queues s s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
affects_equiv aag l s s'

goal (1 subgoal):
 1. (\<lbrakk>equiv_for (aag_can_affect aag l) kheap s s'; equiv_machine_state (aag_can_affect aag l) (machine_state s) (machine_state s'); equiv_for (aag_can_affect aag l \<circ> fst) cdt s s'; equiv_for (aag_can_affect aag l \<circ> fst) cdt_list s s'; equiv_for (aag_can_affect aag l) ekheap s s'; equiv_for (aag_can_affect aag l \<circ> fst) is_original_cap s s'; equiv_for (aag_can_affect_irq aag l) interrupt_states s s'; equiv_for (aag_can_affect_irq aag l) interrupt_irq_node s s'; equiv_asids (aag_can_affect_asid aag l) s s'; equiv_for (aag_can_affect_domain aag l) ready_queues s s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory InfoFlow_IF

lemma affects_equiv_machine_state_update:
  "\<lbrakk> affects_equiv aag l s s'; equiv_machine_state (aag_can_affect aag l) kh kh' \<rbrakk>
     \<Longrightarrow> affects_equiv aag l (s\<lparr>machine_state := kh\<rparr>) (s'\<lparr>machine_state := kh'\<rparr>)" by (fastforce simp: affects_equiv_def2 intro: states_equiv_for_machine_state_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>affects_equiv aag l s s'; equiv_machine_state (aag_can_affect aag l) kh kh'\<rbrakk> \<Longrightarrow> affects_equiv aag l (s\<lparr>machine_state := kh\<rparr>) (s'\<lparr>machine_state := kh'\<rparr>)
theory InfoFlow_IF

lemma affects_equiv_non_asid_pool_kheap_update:
  "\<lbrakk> affects_equiv aag l s s'; equiv_for (aag_can_affect aag l) id kh kh';
     non_asid_pool_kheap_update s kh; non_asid_pool_kheap_update s' kh' \<rbrakk>
     \<Longrightarrow> affects_equiv aag l (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)" by (fastforce simp: affects_equiv_def2 intro: states_equiv_for_non_asid_pool_kheap_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>affects_equiv aag l s s'; equiv_for (aag_can_affect aag l) id kh kh'; non_asid_pool_kheap_update s kh; non_asid_pool_kheap_update s' kh'\<rbrakk> \<Longrightarrow> affects_equiv aag l (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)
theory InfoFlow_IF

lemma affects_equiv_identical_kheap_updates:
  "\<lbrakk>affects_equiv aag l s s';
    identical_kheap_updates s s' kh kh'\<rbrakk> \<Longrightarrow>
   affects_equiv aag l (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)" by (fastforce simp: affects_equiv_def2 intro: states_equiv_for_identical_kheap_updates)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>affects_equiv aag l s s'; identical_kheap_updates s s' kh kh'\<rbrakk> \<Longrightarrow> affects_equiv aag l (s\<lparr>kheap := kh\<rparr>) (s'\<lparr>kheap := kh'\<rparr>)
theory InfoFlow_IF

lemma affects_equiv_cdt_list_update:
  "\<lbrakk>affects_equiv aag l s s'; equiv_for ((aag_can_affect aag l) \<circ> fst) id (kh (cdt_list s)) (kh' (cdt_list s'))\<rbrakk> \<Longrightarrow>
   affects_equiv aag l (cdt_list_update kh s) (cdt_list_update kh' s')" by (fastforce simp: affects_equiv_def2 intro: states_equiv_for_cdt_list_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>affects_equiv aag l s s'; equiv_for (aag_can_affect aag l \<circ> fst) id (kh (cdt_list s)) (kh' (cdt_list s'))\<rbrakk> \<Longrightarrow> affects_equiv aag l (cdt_list_update kh s) (cdt_list_update kh' s')
theory InfoFlow_IF

lemma affects_equiv_identical_ekheap_updates:
  "\<lbrakk>affects_equiv aag l s s'; identical_ekheap_updates s s' (kh (ekheap s)) (kh' (ekheap s'))\<rbrakk> \<Longrightarrow>
    affects_equiv aag l (ekheap_update kh s) (ekheap_update kh' s')" by (fastforce simp: affects_equiv_def2 intro: states_equiv_for_identical_ekheap_updates)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>affects_equiv aag l s s'; identical_ekheap_updates s s' (kh (ekheap s)) (kh' (ekheap s'))\<rbrakk> \<Longrightarrow> affects_equiv aag l (ekheap_update kh s) (ekheap_update kh' s')
theory InfoFlow_IF

lemma affects_equiv_ekheap_update:
  "\<lbrakk>affects_equiv aag l s s'; equiv_for (aag_can_affect aag l) id (kh (ekheap s)) (kh' (ekheap s')) \<rbrakk> \<Longrightarrow>
    affects_equiv aag l (ekheap_update kh s) (ekheap_update kh' s')" by (fastforce simp: affects_equiv_def2 intro: states_equiv_for_ekheap_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>affects_equiv aag l s s'; equiv_for (aag_can_affect aag l) id (kh (ekheap s)) (kh' (ekheap s'))\<rbrakk> \<Longrightarrow> affects_equiv aag l (ekheap_update kh s) (ekheap_update kh' s')
theory InfoFlow_IF

lemma affects_equiv_is_original_cap_update:
  "\<lbrakk>affects_equiv aag l s s'; equiv_for ((aag_can_affect aag l) \<circ> fst) id kh kh'\<rbrakk> \<Longrightarrow>
   affects_equiv aag l (s\<lparr>is_original_cap := kh\<rparr>) (s'\<lparr>is_original_cap := kh'\<rparr>)" by (fastforce simp: affects_equiv_def2 intro: states_equiv_for_is_original_cap_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>affects_equiv aag l s s'; equiv_for (aag_can_affect aag l \<circ> fst) id kh kh'\<rbrakk> \<Longrightarrow> affects_equiv aag l (s\<lparr>is_original_cap := kh\<rparr>) (s'\<lparr>is_original_cap := kh'\<rparr>)
theory InfoFlow_IF

lemma affects_equiv_interrupt_states_update:
  "\<lbrakk>affects_equiv aag l s s'; equiv_for (aag_can_affect_irq aag l) id kh kh'\<rbrakk> \<Longrightarrow>
   affects_equiv aag l (s\<lparr>interrupt_states := kh\<rparr>) (s'\<lparr>interrupt_states := kh'\<rparr>)" by (fastforce simp: affects_equiv_def2 intro: states_equiv_for_interrupt_states_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>affects_equiv aag l s s'; equiv_for (aag_can_affect_irq aag l) id kh kh'\<rbrakk> \<Longrightarrow> affects_equiv aag l (s\<lparr>interrupt_states := kh\<rparr>) (s'\<lparr>interrupt_states := kh'\<rparr>)
theory InfoFlow_IF

lemma affects_equiv_interrupt_irq_node_update:
  "\<lbrakk>affects_equiv aag l s s'; equiv_for (aag_can_affect_irq aag l) id kh kh'\<rbrakk> \<Longrightarrow>
   affects_equiv aag l (s\<lparr>interrupt_irq_node := kh\<rparr>) (s'\<lparr>interrupt_irq_node := kh'\<rparr>)" by (fastforce simp: affects_equiv_def2 intro: states_equiv_for_interrupt_irq_node_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>affects_equiv aag l s s'; equiv_for (aag_can_affect_irq aag l) id kh kh'\<rbrakk> \<Longrightarrow> affects_equiv aag l (s\<lparr>interrupt_irq_node := kh\<rparr>) (s'\<lparr>interrupt_irq_node := kh'\<rparr>)
theory InfoFlow_IF

lemma affects_equiv_ready_queues_update:
  "\<lbrakk>affects_equiv aag l s s'; equiv_for (aag_can_affect_domain aag l) id kh kh'\<rbrakk> \<Longrightarrow>
   affects_equiv aag l (s\<lparr>ready_queues := kh\<rparr>) (s'\<lparr>ready_queues := kh'\<rparr>)" by (fastforce simp: affects_equiv_def2 intro: states_equiv_for_ready_queues_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>affects_equiv aag l s s'; equiv_for (aag_can_affect_domain aag l) id kh kh'\<rbrakk> \<Longrightarrow> affects_equiv aag l (ready_queues_update (\<lambda>_. kh) s) (ready_queues_update (\<lambda>_. kh') s')
theory InfoFlow_IF

lemma affects_equiv_scheduler_action_update:
  "affects_equiv aag l s s' \<Longrightarrow>
   affects_equiv aag l (s\<lparr>scheduler_action := kh\<rparr>) (s'\<lparr>scheduler_action := kh\<rparr>)" by (fastforce simp: affects_equiv_def2 states_equiv_for_def equiv_for_def elim!: equiv_asids_triv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. affects_equiv aag l s s' \<Longrightarrow> affects_equiv aag l (scheduler_action_update (\<lambda>_. kh) s) (scheduler_action_update (\<lambda>_. kh) s')
theory InfoFlow_IF

lemma affects_equiv_work_units_completed_update:
  "affects_equiv aag l s s' \<Longrightarrow>
   affects_equiv aag l (s\<lparr>work_units_completed := kh\<rparr>) (s'\<lparr>work_units_completed := kh\<rparr>)" by (fastforce simp: affects_equiv_def2 states_equiv_for_def equiv_for_def elim!: equiv_asids_triv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. affects_equiv aag l s s' \<Longrightarrow> affects_equiv aag l (work_units_completed_update (\<lambda>_. kh) s) (work_units_completed_update (\<lambda>_. kh) s')
theory InfoFlow_IF

lemma affects_equiv_work_units_completed_update':
  "affects_equiv aag l s s' \<Longrightarrow>
   affects_equiv aag l (s\<lparr>work_units_completed := (f (work_units_completed s))\<rparr>)
                       (s'\<lparr>work_units_completed := (f (work_units_completed s'))\<rparr>)" by (fastforce simp: affects_equiv_def2 states_equiv_for_def equiv_for_def elim!: equiv_asids_triv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. affects_equiv aag l s s' \<Longrightarrow> affects_equiv aag l (work_units_completed_update (\<lambda>_. f (work_units_completed s)) s) (work_units_completed_update (\<lambda>_. f (work_units_completed s')) s')
theory InfoFlow_IF

lemma reads_equiv_refl:
  "reads_equiv aag s s" by (auto simp: reads_equiv_def2 intro: states_equiv_for_refl equiv_asids_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv aag s s
theory InfoFlow_IF

lemma reads_equiv_sym:
  "reads_equiv aag s t \<Longrightarrow> reads_equiv aag t s" by (auto simp: reads_equiv_def2 intro: states_equiv_for_sym equiv_asids_sym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv aag s t \<Longrightarrow> reads_equiv aag t s
theory InfoFlow_IF

lemma reads_equiv_trans:
  "\<lbrakk> reads_equiv aag s t; reads_equiv aag t u \<rbrakk> \<Longrightarrow> reads_equiv aag s u" by (auto simp: reads_equiv_def2 intro: states_equiv_for_trans equiv_asids_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s t; reads_equiv aag t u\<rbrakk> \<Longrightarrow> reads_equiv aag s u
theory InfoFlow_IF

lemma affects_equiv_refl:
  "affects_equiv aag l s s" by (auto simp: affects_equiv_def intro: states_equiv_for_refl equiv_asids_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. affects_equiv aag l s s
theory InfoFlow_IF

lemma affects_equiv_sym:
  "affects_equiv aag l s t \<Longrightarrow> affects_equiv aag l t s" by (auto simp: affects_equiv_def2 intro: states_equiv_for_sym equiv_asids_sym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. affects_equiv aag l s t \<Longrightarrow> affects_equiv aag l t s
theory InfoFlow_IF

lemma affects_equiv_trans:
  "\<lbrakk> affects_equiv aag l s t; affects_equiv aag l t u \<rbrakk>
     \<Longrightarrow> affects_equiv aag l s u" by (auto simp: affects_equiv_def2 intro: states_equiv_for_trans equiv_asids_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>affects_equiv aag l s t; affects_equiv aag l t u\<rbrakk> \<Longrightarrow> affects_equiv aag l s u
theory InfoFlow_IF

lemma globals_equivI:
  "\<lbrakk> doesnt_touch_globals P f; P s; (rv, s') \<in> fst (f s) \<rbrakk>
     \<Longrightarrow> globals_equiv s s'" by(fastforce simp: doesnt_touch_globals_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>doesnt_touch_globals P f; P s; (rv, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> globals_equiv s s'
theory InfoFlow_IF

lemma reads_equiv_gI:
  "\<lbrakk> reads_equiv aag s s'; globals_equiv s s' \<rbrakk> \<Longrightarrow> reads_equiv_g aag s s'" by (simp add: reads_equiv_g_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; globals_equiv s s'\<rbrakk> \<Longrightarrow> reads_equiv_g aag s s'
theory InfoFlow_IF

lemma equiv_for_guard_imp:
  "\<lbrakk> equiv_for P f s s'; \<And>x. Q x \<Longrightarrow> P x \<rbrakk> \<Longrightarrow> equiv_for Q f s s'" by(auto simp: equiv_for_def)

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

lemma globals_equiv_invD:
  "\<lbrace>globals_equiv st and P\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
   \<Longrightarrow> \<lbrace>P and (=) st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" by (fastforce simp: valid_def intro: globals_equiv_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and P\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace> \<Longrightarrow> \<lbrace>P and (=) st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory InfoFlow_IF

lemma doesnt_touch_globalsI:
  assumes globals_equiv_inv: "\<And>st. \<lbrace>globals_equiv st and P\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
  shows "doesnt_touch_globals P f" apply (clarsimp simp: doesnt_touch_globals_def) apply (cut_tac st=s in globals_equiv_inv) by (fastforce dest: globals_equiv_invD simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doesnt_touch_globals P f proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> globals_equiv s b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); \<lbrace>globals_equiv s and P\<rbrace> f \<lbrace>\<lambda>_. globals_equiv s\<rbrace>\<rbrakk> \<Longrightarrow> globals_equiv s b
theory InfoFlow_IF

lemma reads_respects_g_from_inv:
  "\<lbrakk> reads_respects aag l P f; \<And>st. f \<lbrace>globals_equiv st\<rbrace> \<rbrakk>
     \<Longrightarrow> reads_respects_g aag l P f" apply (rule equiv_valid_guard_imp) apply (erule reads_respects_g[where Q="\<lambda>s. True"]) apply (rule doesnt_touch_globalsI) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_respects aag l P f; \<And>st. \<lbrace>globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_g aag l P f proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_respects aag l P f; \<And>st. \<lbrace>globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_g aag l ?Q f
 2. \<And>s. \<lbrakk>reads_respects aag l P f; \<And>st. \<lbrace>globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>; P s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. (\<And>st. \<lbrace>globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<Longrightarrow> doesnt_touch_globals (\<lambda>s. True) f
 2. \<And>s. \<lbrakk>reads_respects aag l P f; \<And>st. \<lbrace>globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>; P s\<rbrakk> \<Longrightarrow> (P and (\<lambda>s. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>st. (\<And>st. \<lbrace>globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<Longrightarrow> \<lbrace>globals_equiv st and (\<lambda>s. True)\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. \<lbrakk>reads_respects aag l P f; \<And>st. \<lbrace>globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>; P s\<rbrakk> \<Longrightarrow> (P and (\<lambda>s. True)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma reads_respects_g':
  assumes rev: "reads_respects aag l P f"
  assumes gev: "\<And>st. \<lbrace>\<lambda> s. R (globals_equiv st s) s\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
  assumes and_imp: "\<And>st s. Q st s \<Longrightarrow> P s \<and> R (globals_equiv st s) s"
  assumes gev_imp: "\<And>st s. R (globals_equiv st s) s \<Longrightarrow> globals_equiv st s"
  shows "reads_respects_g aag l (Q st) f" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_g[OF rev, where Q="\<lambda>s. R (globals_equiv st s) s"]) apply (rule doesnt_touch_globalsI) apply (rule hoare_pre) apply (rule gev) apply clarsimp apply (frule gev_imp) apply (simp add: and_imp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_g aag l (Q st) f proof (prove)
goal (2 subgoals):
 1. reads_respects_g aag l ?Q f
 2. \<And>s. Q st s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals (\<lambda>s. R (globals_equiv st s) s) f
 2. \<And>s. Q st s \<Longrightarrow> (P and (\<lambda>s. R (globals_equiv st s) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>sta. \<lbrace>globals_equiv sta and (\<lambda>s. R (globals_equiv st s) s)\<rbrace> f \<lbrace>\<lambda>_. globals_equiv sta\<rbrace>
 2. \<And>s. Q st s \<Longrightarrow> (P and (\<lambda>s. R (globals_equiv st s) s)) s proof (prove)
goal (3 subgoals):
 1. \<And>st. \<lbrace>?Q6 st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>sta s. (globals_equiv sta and (\<lambda>s. R (globals_equiv st s) s)) s \<Longrightarrow> ?Q6 sta s
 3. \<And>s. Q st s \<Longrightarrow> (P and (\<lambda>s. R (globals_equiv st s) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>sta s. (globals_equiv sta and (\<lambda>s. R (globals_equiv st s) s)) s \<Longrightarrow> R (globals_equiv sta s) s
 2. \<And>s. Q st s \<Longrightarrow> (P and (\<lambda>s. R (globals_equiv st s) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>sta s. \<lbrakk>globals_equiv sta s; R (globals_equiv st s) s\<rbrakk> \<Longrightarrow> R True s
 2. \<And>s. Q st s \<Longrightarrow> (P and (\<lambda>s. R (globals_equiv st s) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>sta s. \<lbrakk>globals_equiv sta s; R (globals_equiv st s) s; globals_equiv st s\<rbrakk> \<Longrightarrow> R True s
 2. \<And>s. Q st s \<Longrightarrow> (P and (\<lambda>s. R (globals_equiv st s) s)) s proof (prove)
goal:
No subgoals!
theory InfoFlow_IF

lemma states_equiv_for_guard_imp:
  assumes "states_equiv_for P Q R S s s'"
  and "\<And>x. P' x \<Longrightarrow> P x"
  and "\<And>x. Q' x \<Longrightarrow> Q x"
  and "\<And>x. R' x \<Longrightarrow> R x"
  and "\<And>x. S' x \<Longrightarrow> S x"
  shows "states_equiv_for P' Q' R' S' s s'" using assms by (auto simp: states_equiv_for_def intro: equiv_for_guard_imp equiv_asids_guard_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. states_equiv_for P' Q' R' S' s s' proof (prove)
using this:
states_equiv_for P Q R S s s'
P' ?x \<Longrightarrow> P ?x
Q' ?x \<Longrightarrow> Q ?x
R' ?x \<Longrightarrow> R ?x
S' ?x \<Longrightarrow> S ?x

goal (1 subgoal):
 1. states_equiv_for P' Q' R' S' s s'
theory InfoFlow_IF

lemma reads_equiv_self_reads_respects:
  "pasSubject aag = l \<Longrightarrow> reads_equiv_valid_inv \<top>\<top> aag P f = reads_respects aag l P f" unfolding equiv_valid_def2 equiv_valid_2_def by (fastforce intro: cur_subject_reads_equiv_affects_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasSubject aag = l \<Longrightarrow> reads_equiv_valid_inv (\<lambda>_ _. True) aag P f = reads_respects aag l P f proof (prove)
goal (1 subgoal):
 1. pasSubject aag = l \<Longrightarrow> (\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (f t). rva = rvb \<and> reads_equiv aag s' t' \<and> True)) = (\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>(rva, s')\<in>fst (f s). \<forall>(rvb, t')\<in>fst (f t). rva = rvb \<and> reads_equiv aag s' t' \<and> affects_equiv aag l s' t'))
theory InfoFlow_IF

lemma requiv_get_tcb_eq[intro]:
  "\<lbrakk> reads_equiv aag s t; is_subject aag thread \<rbrakk>
     \<Longrightarrow> get_tcb thread s = get_tcb thread t" by (auto simp: reads_equiv_def2 get_tcb_def elim: states_equiv_forE_kheap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s t; is_subject aag thread\<rbrakk> \<Longrightarrow> get_tcb thread s = get_tcb thread t
theory InfoFlow_IF

lemma requiv_cur_thread_eq[intro]:
  "reads_equiv aag s t \<Longrightarrow> cur_thread s = cur_thread t" by (simp add: reads_equiv_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv aag s t \<Longrightarrow> cur_thread s = cur_thread t
theory InfoFlow_IF

lemma requiv_cur_domain_eq[intro]:
  "reads_equiv aag s t \<Longrightarrow> cur_domain s = cur_domain t" by (simp add: reads_equiv_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv aag s t \<Longrightarrow> cur_domain s = cur_domain t
theory InfoFlow_IF

lemma requiv_sched_act_eq[intro]:
  "reads_equiv aag s t \<Longrightarrow> scheduler_action s = scheduler_action t" by (simp add: reads_equiv_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv aag s t \<Longrightarrow> scheduler_action s = scheduler_action t
theory InfoFlow_IF

lemma requiv_wuc_eq[intro]:
  "reads_equiv aag s t \<Longrightarrow> work_units_completed s = work_units_completed t" by (simp add: reads_equiv_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv aag s t \<Longrightarrow> work_units_completed s = work_units_completed t
theory InfoFlow_IF

lemma update_object_noop:
  "kheap s ptr = Some obj \<Longrightarrow> s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr> = s" by (clarsimp simp: map_upd_triv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s ptr = Some obj \<Longrightarrow> s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr> = s