theory InfoFlow_IF

lemma do_machine_op_spec_reads_respects:
  assumes equiv_dmo:
   "equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) \<top> f"
  assumes irq_state_inv:
    "\<And>P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace>"
  shows
    "spec_reads_respects st aag l \<top> (do_machine_op f)" apply (rule do_machine_op_spec_reads_respects'[where Q=\<top>, simplified]) apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def) apply (subgoal_tac "equiv_irq_state b ba", simp) apply (insert equiv_dmo, fastforce simp: equiv_valid_def2 equiv_valid_2_def) apply (insert irq_state_inv) apply (drule_tac x="\<lambda>ms. ms = irq_state s" in meta_spec) apply (clarsimp simp: valid_def) apply (frule_tac x=s in spec) apply (erule (1) impE) apply (drule bspec, assumption, simp) apply (drule_tac x=t in spec, simp) apply (drule bspec, assumption) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_reads_respects st aag l (\<lambda>_. True) (do_machine_op f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (equiv_machine_state (aag_can_read aag) and equiv_irq_state) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) f proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t\<rbrakk> \<Longrightarrow> a = aa \<and> equiv_for (aag_can_read aag) underlying_memory b ba \<and> equiv_for (aag_can_read aag) device_state b ba \<and> equiv_irq_state b ba \<and> equiv_machine_state (aag_can_affect aag l) b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t; equiv_irq_state b ba\<rbrakk> \<Longrightarrow> a = aa \<and> equiv_for (aag_can_read aag) underlying_memory b ba \<and> equiv_for (aag_can_read aag) device_state b ba \<and> equiv_machine_state (aag_can_affect aag l) b ba
 2. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t\<rbrakk> \<Longrightarrow> equiv_irq_state b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t; equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) f\<rbrakk> \<Longrightarrow> equiv_irq_state b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t; equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) f; \<And>P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> f \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace>\<rbrakk> \<Longrightarrow> equiv_irq_state b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t; equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) f; \<lbrace>\<lambda>ms. equiv_irq_state ms s\<rbrace> f \<lbrace>\<lambda>_ ms. equiv_irq_state ms s\<rbrace>\<rbrakk> \<Longrightarrow> equiv_irq_state b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t; equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) f; \<forall>s. equiv_irq_state s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> equiv_irq_state s' t)\<rbrakk> \<Longrightarrow> equiv_irq_state b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t; equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) f; \<forall>s. equiv_irq_state s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> equiv_irq_state s' t); equiv_irq_state s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> equiv_irq_state s' t)\<rbrakk> \<Longrightarrow> equiv_irq_state b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t; equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) f; \<forall>s. equiv_irq_state s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> equiv_irq_state s' t); \<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> equiv_irq_state s' t\<rbrakk> \<Longrightarrow> equiv_irq_state b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t; equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) f; \<forall>s. equiv_irq_state s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> equiv_irq_state s' t); equiv_irq_state b t\<rbrakk> \<Longrightarrow> equiv_irq_state t ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t; equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) f; equiv_irq_state b t; \<forall>(r, s')\<in>fst (f t). equiv_irq_state s' t\<rbrakk> \<Longrightarrow> equiv_irq_state t ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); equiv_for (aag_can_read aag) underlying_memory s t; equiv_for (aag_can_read aag) device_state s t; equiv_irq_state s t; equiv_for (aag_can_affect aag l) underlying_memory s t; equiv_for (aag_can_affect aag l) device_state s t; equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) f; equiv_irq_state b t; case (aa, ba) of (r, s') \<Rightarrow> equiv_irq_state s' t\<rbrakk> \<Longrightarrow> equiv_irq_state t ba proof (prove)
goal:
No subgoals!