theory InfoFlow_IF

lemma do_machine_op_spec_rev:
  assumes equiv_dmo:
    "spec_equiv_valid_inv (machine_state st) (equiv_machine_state (aag_can_read aag)) \<top>\<top> \<top> f"
  assumes mo_inv: "\<And>P. f \<lbrace>P\<rbrace>"
  shows "reads_spec_equiv_valid_inv st A aag P (do_machine_op f)" unfolding do_machine_op_def spec_equiv_valid_def apply (rule equiv_valid_2_guard_imp) apply (rule_tac R'="\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and>
                                equiv_irq_state rv rv'"
               and Q="\<lambda>r s. st = s \<and> r = machine_state s"
               and Q'="\<lambda>r s. r = machine_state s"
               and P="(=) st" and P'=\<top>
                in equiv_valid_2_bind) apply (rule_tac R'="\<lambda>(r, ms') (r', ms''). r = r' \<and>
                                                 equiv_machine_state (aag_can_read aag) ms' ms''"
                   and Q="\<lambda>(r,ms') s. ms' = rv \<and> rv = machine_state s \<and> st = s"
                   and Q'="\<lambda>(r,ms') s. ms' = rv' \<and> rv' = machine_state s"
                   and P="\<lambda>s. st = s \<and> rv = machine_state s" and P'="\<lambda> s. rv' = machine_state s"
                   and S="\<lambda>s. st = s \<and> rv = machine_state s" and S'="\<lambda>s. rv' = machine_state s"
                    in equiv_valid_2_bind_pre) apply (clarsimp simp: modify_def get_def put_def bind_def return_def equiv_valid_2_def) apply (clarsimp simp: select_f_def equiv_valid_2_def equiv_valid_def2 equiv_for_or
                                 split_def equiv_for_def
                          split: prod.splits) apply (insert equiv_dmo)[1] apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def) apply (drule_tac x="machine_state t" in spec) apply (clarsimp simp: equiv_for_def) apply blast apply (wp select_f_inv) apply clarsimp apply (drule state_unchanged[OF mo_inv], simp) apply (wp select_f_inv) apply clarsimp apply (drule state_unchanged[OF mo_inv], simp) apply simp+ apply (clarsimp simp: equiv_valid_2_def in_monad) apply (fastforce intro: elim: equiv_forE reads_equivE) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_spec_equiv_valid_inv st A aag P (do_machine_op f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (reads_equiv aag) A A (=) (P and (=) st) P (do ms <- gets machine_state;
(r, ms') <- select_f (f ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od) (do ms <- gets machine_state;
(r, ms') <- select_f (f ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od) proof (prove)
goal (3 subgoals):
 1. equiv_valid_2 (reads_equiv aag) A A (=) ?Q ?Q' (do ms <- gets machine_state;
(r, ms') <- select_f (f ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od) (do ms <- gets machine_state;
(r, ms') <- select_f (f ms);
modify (machine_state_update (\<lambda>_. ms'));
return r
od)
 2. \<And>s. (P and (=) st) s \<Longrightarrow> ?Q s
 3. \<And>s. P s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) A A (=) (\<lambda>s. st = s \<and> rv = machine_state s) (\<lambda>s. rv' = machine_state s) (do (r, ms') <- select_f (f rv);
modify (machine_state_update (\<lambda>_. ms'));
return r
od) (do (r, ms') <- select_f (f rv');
modify (machine_state_update (\<lambda>_. ms'));
return r
od)
 2. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 3. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 4. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 5. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 6. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (11 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; (case rva of (r, ms') \<Rightarrow> \<lambda>(r', ms''). r = r' \<and> equiv_machine_state (aag_can_read aag) ms' ms'') rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) A A (=) (case rva of (r, ms') \<Rightarrow> \<lambda>s. ms' = rv \<and> rv = machine_state s \<and> st = s) (case rv'a of (r, ms') \<Rightarrow> \<lambda>s. ms' = rv' \<and> rv' = machine_state s) (case rva of (r, ms') \<Rightarrow> do modify (machine_state_update (\<lambda>_. ms'));
return r
od) (case rv'a of (r, ms') \<Rightarrow> do modify (machine_state_update (\<lambda>_. ms'));
return r
od)
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) A A (\<lambda>(r, ms') (r', ms''). r = r' \<and> equiv_machine_state (aag_can_read aag) ms' ms'') (\<lambda>s. st = s \<and> rv = machine_state s) (\<lambda>s. rv' = machine_state s) (select_f (f rv)) (select_f (f rv'))
 3. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. st = s \<and> rv = machine_state s\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s \<and> st = s\<rbrace>
 4. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. rv' = machine_state s\<rbrace> select_f (f rv') \<lbrace>\<lambda>(r, ms') s. ms' = rv' \<and> rv' = machine_state s\<rbrace>
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 6. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 7. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 8. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 9. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 10. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) A A (\<lambda>(r, ms') (r', ms''). r = r' \<and> equiv_machine_state (aag_can_read aag) ms' ms'') (\<lambda>s. st = s \<and> rv = machine_state s) (\<lambda>s. rv' = machine_state s) (select_f (f rv)) (select_f (f rv'))
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. st = s \<and> rv = machine_state s\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s \<and> st = s\<rbrace>
 3. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. rv' = machine_state s\<rbrace> select_f (f rv') \<lbrace>\<lambda>(r, ms') s. ms' = rv' \<and> rv' = machine_state s\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 6. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 7. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 8. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 9. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 10. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (10 subgoals):
 1. \<And>t a b aa ba. \<lbrakk>\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory (machine_state t) x; \<forall>x. aag_can_read aag x \<longrightarrow> device_state (machine_state st) x = device_state (machine_state t) x; equiv_irq_state (machine_state st) (machine_state t); (a, b) \<in> fst (f (machine_state st)); (aa, ba) \<in> fst (f (machine_state t)); reads_equiv aag st t; A st t\<rbrakk> \<Longrightarrow> a = aa \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory b x = underlying_memory ba x) \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> device_state b x = device_state ba x)
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. st = s \<and> rv = machine_state s\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s \<and> st = s\<rbrace>
 3. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. rv' = machine_state s\<rbrace> select_f (f rv') \<lbrace>\<lambda>(r, ms') s. ms' = rv' \<and> rv' = machine_state s\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 6. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 7. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 8. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 9. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 10. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (10 subgoals):
 1. \<And>t a b aa ba. \<lbrakk>\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory (machine_state t) x; \<forall>x. aag_can_read aag x \<longrightarrow> device_state (machine_state st) x = device_state (machine_state t) x; equiv_irq_state (machine_state st) (machine_state t); (a, b) \<in> fst (f (machine_state st)); (aa, ba) \<in> fst (f (machine_state t)); reads_equiv aag st t; A st t; spec_equiv_valid_inv (machine_state st) (equiv_machine_state (aag_can_read aag)) (\<lambda>_ _. True) (\<lambda>_. True) f\<rbrakk> \<Longrightarrow> a = aa \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory b x = underlying_memory ba x) \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> device_state b x = device_state ba x)
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. st = s \<and> rv = machine_state s\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s \<and> st = s\<rbrace>
 3. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. rv' = machine_state s\<rbrace> select_f (f rv') \<lbrace>\<lambda>(r, ms') s. ms' = rv' \<and> rv' = machine_state s\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 6. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 7. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 8. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 9. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 10. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (10 subgoals):
 1. \<And>t a b aa ba. \<lbrakk>\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory (machine_state t) x; \<forall>x. aag_can_read aag x \<longrightarrow> device_state (machine_state st) x = device_state (machine_state t) x; equiv_irq_state (machine_state st) (machine_state t); (a, b) \<in> fst (f (machine_state st)); (aa, ba) \<in> fst (f (machine_state t)); reads_equiv aag st t; A st t; \<forall>t. equiv_machine_state (aag_can_read aag) (machine_state st) t \<longrightarrow> (\<forall>x\<in>fst (f (machine_state st)). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> equiv_machine_state (aag_can_read aag) s' t')\<rbrakk> \<Longrightarrow> a = aa \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory b x = underlying_memory ba x) \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> device_state b x = device_state ba x)
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. st = s \<and> rv = machine_state s\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s \<and> st = s\<rbrace>
 3. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. rv' = machine_state s\<rbrace> select_f (f rv') \<lbrace>\<lambda>(r, ms') s. ms' = rv' \<and> rv' = machine_state s\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 6. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 7. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 8. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 9. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 10. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (10 subgoals):
 1. \<And>t a b aa ba. \<lbrakk>\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory (machine_state t) x; \<forall>x. aag_can_read aag x \<longrightarrow> device_state (machine_state st) x = device_state (machine_state t) x; equiv_irq_state (machine_state st) (machine_state t); (a, b) \<in> fst (f (machine_state st)); (aa, ba) \<in> fst (f (machine_state t)); reads_equiv aag st t; A st t; equiv_machine_state (aag_can_read aag) (machine_state st) (machine_state t) \<longrightarrow> (\<forall>x\<in>fst (f (machine_state st)). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f (machine_state t)). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> equiv_machine_state (aag_can_read aag) s' t')\<rbrakk> \<Longrightarrow> a = aa \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory b x = underlying_memory ba x) \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> device_state b x = device_state ba x)
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. st = s \<and> rv = machine_state s\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s \<and> st = s\<rbrace>
 3. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. rv' = machine_state s\<rbrace> select_f (f rv') \<lbrace>\<lambda>(r, ms') s. ms' = rv' \<and> rv' = machine_state s\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 6. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 7. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 8. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 9. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 10. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (10 subgoals):
 1. \<And>t a b aa ba. \<lbrakk>\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory (machine_state t) x; \<forall>x. aag_can_read aag x \<longrightarrow> device_state (machine_state st) x = device_state (machine_state t) x; equiv_irq_state (machine_state st) (machine_state t); (a, b) \<in> fst (f (machine_state st)); (aa, ba) \<in> fst (f (machine_state t)); reads_equiv aag st t; A st t; \<forall>x\<in>fst (f (machine_state st)). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f (machine_state t)). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory s' x = underlying_memory t' x) \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> device_state s' x = device_state t' x)\<rbrakk> \<Longrightarrow> a = aa \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory b x = underlying_memory ba x) \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> device_state b x = device_state ba x)
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. st = s \<and> rv = machine_state s\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s \<and> st = s\<rbrace>
 3. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. rv' = machine_state s\<rbrace> select_f (f rv') \<lbrace>\<lambda>(r, ms') s. ms' = rv' \<and> rv' = machine_state s\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 6. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 7. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 8. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 9. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 10. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (9 subgoals):
 1. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. st = s \<and> rv = machine_state s\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s \<and> st = s\<rbrace>
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. rv' = machine_state s\<rbrace> select_f (f rv') \<lbrace>\<lambda>(r, ms') s. ms' = rv' \<and> rv' = machine_state s\<rbrace>
 3. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 5. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 6. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 7. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 8. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 9. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f rv). (case x of (r, ms') \<Rightarrow> \<lambda>s. ms' = rv \<and> rv = machine_state s \<and> st = s) s
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. rv' = machine_state s\<rbrace> select_f (f rv') \<lbrace>\<lambda>(r, ms') s. ms' = rv' \<and> rv' = machine_state s\<rbrace>
 3. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 5. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 6. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 7. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 8. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 9. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (9 subgoals):
 1. \<And>rv' a b. \<lbrakk>(a, b) \<in> fst (f (machine_state st)); equiv_for (aag_can_read aag) underlying_memory (machine_state st) rv'; equiv_for (aag_can_read aag) device_state (machine_state st) rv'; equiv_irq_state (machine_state st) rv'\<rbrakk> \<Longrightarrow> b = machine_state st
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. rv' = machine_state s\<rbrace> select_f (f rv') \<lbrace>\<lambda>(r, ms') s. ms' = rv' \<and> rv' = machine_state s\<rbrace>
 3. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 5. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 6. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 7. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 8. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 9. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>\<lambda>s. rv' = machine_state s\<rbrace> select_f (f rv') \<lbrace>\<lambda>(r, ms') s. ms' = rv' \<and> rv' = machine_state s\<rbrace>
 2. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 3. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 4. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 5. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 6. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 7. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 8. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f rv'). (case x of (r, ms') \<Rightarrow> \<lambda>s. ms' = rv' \<and> rv' = machine_state s) s
 2. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 3. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 4. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 5. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 6. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 7. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 8. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (8 subgoals):
 1. \<And>rv s a b. \<lbrakk>(a, b) \<in> fst (f (machine_state s)); equiv_for (aag_can_read aag) underlying_memory rv (machine_state s); equiv_for (aag_can_read aag) device_state rv (machine_state s); equiv_irq_state rv (machine_state s)\<rbrakk> \<Longrightarrow> b = machine_state s
 2. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 3. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 4. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 5. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 6. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 7. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 8. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; st = s \<and> rv = machine_state s\<rbrakk> \<Longrightarrow> (st = s \<and> rv = machine_state s) \<and> st = s \<and> rv = machine_state s
 2. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'; rv' = machine_state s\<rbrakk> \<Longrightarrow> rv' = machine_state s \<and> rv' = machine_state s
 3. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 4. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 5. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 6. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 7. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (5 subgoals):
 1. equiv_valid_2 (reads_equiv aag) A A (\<lambda>rv rv'. equiv_for (aag_can_read aag) underlying_memory rv rv' \<and> equiv_for (aag_can_read aag) device_state rv rv' \<and> equiv_irq_state rv rv') ((=) st) (\<lambda>_. True) (gets machine_state) (gets machine_state)
 2. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 3. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 4. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 5. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>reads_equiv aag st t; A st t\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag) underlying_memory (machine_state st) (machine_state t) \<and> equiv_for (aag_can_read aag) device_state (machine_state st) (machine_state t) \<and> equiv_irq_state (machine_state st) (machine_state t)
 2. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 3. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 4. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 5. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?S4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. st = s \<and> r = machine_state s\<rbrace>
 2. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. r = machine_state s\<rbrace>
 3. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
 4. \<And>s. P s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal:
No subgoals!