theory InfoFlow_IF

lemma do_machine_op_spec_reads_respects':
  assumes equiv_dmo:
   "equiv_valid_inv (equiv_machine_state (aag_can_read aag) and equiv_irq_state)
                    (equiv_machine_state (aag_can_affect aag l)) Q f"
  assumes guard:
    "\<And>s. P s \<Longrightarrow> Q (machine_state s)"
  shows
  "spec_reads_respects st aag l 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 or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'" and Q="\<lambda> r s. st = s \<and> Q r" and Q'="\<lambda> r s. Q r" and P="(=) st" and P'="\<top>" in equiv_valid_2_bind) apply (rule gen_asm_ev2_l[simplified K_def pred_conj_def]) apply (rule gen_asm_ev2_r') apply (rule_tac R'="\<lambda> (r, ms') (r', ms'').  r = r' \<and> equiv_machine_state (aag_can_read aag)  ms' ms'' \<and> equiv_machine_state (aag_can_affect aag l) ms' ms'' \<and> equiv_irq_state ms' ms''" and Q="\<lambda> r s. st = s" and Q'="\<top>\<top>" and P="\<top>" and P'="\<top>" in equiv_valid_2_bind_pre) apply (clarsimp simp: modify_def get_def put_def bind_def return_def equiv_valid_2_def) apply (fastforce intro: reads_equiv_machine_state_update affects_equiv_machine_state_update) apply (insert equiv_dmo)[1] apply (clarsimp simp: select_f_def equiv_valid_2_def equiv_valid_def2 equiv_for_or simp: split_def split: prod.splits simp: equiv_for_def)[1] apply (drule_tac x=rv in spec, drule_tac x=rv' in spec) apply (fastforce) apply (rule select_f_inv) apply (rule wp_post_taut) apply simp+ apply (clarsimp simp: equiv_valid_2_def in_monad) apply (fastforce elim: reads_equivE affects_equivE equiv_forE intro: equiv_forI) apply (wp | simp add: guard)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_reads_respects st aag l P (do_machine_op f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (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) (affects_equiv aag l) (affects_equiv aag l) (=) ?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 or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>s. st = s \<and> Q rv) (\<lambda>s. Q rv') (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) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 4. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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 (6 subgoals):
 1. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) ((=) st) (\<lambda>s. Q rv') (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) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 4. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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 (6 subgoals):
 1. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) ((=) st) (\<lambda>_. True) (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) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 4. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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 or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; (case rva of (r, ms') \<Rightarrow> \<lambda>(r', ms''). r = r' \<and> equiv_machine_state (aag_can_read aag) ms' ms'' \<and> equiv_machine_state (aag_can_affect aag l) ms' ms'' \<and> equiv_irq_state ms' ms'') rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) ((=) st) (\<lambda>_. True) (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'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>(r, ms') (r', ms''). r = r' \<and> equiv_machine_state (aag_can_read aag) ms' ms'' \<and> equiv_machine_state (aag_can_affect aag l) ms' ms'' \<and> equiv_irq_state ms' ms'') (\<lambda>_. True) (\<lambda>_. True) (select_f (f rv)) (select_f (f rv'))
 3. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>r. (=) st\<rbrace>
 4. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'9 rv rv'\<rbrace> select_f (f rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' s
 6. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 rv rv' s
 7. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 9. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<rbrace>
 10. \<And>s. (P and (=) st) s \<Longrightarrow> st = s \<and> ?S4 s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv rv' b ba t. \<lbrakk>Q rv; Q rv'; equiv_for (\<lambda>x. aag_can_read aag x \<or> aag_can_affect aag l x) underlying_memory rv rv'; equiv_for (\<lambda>x. aag_can_read aag x \<or> aag_can_affect aag l x) device_state rv rv'; equiv_irq_state rv rv'; equiv_for (aag_can_read aag) underlying_memory b ba; equiv_for (aag_can_read aag) device_state b ba; equiv_for (aag_can_affect aag l) underlying_memory b ba; equiv_for (aag_can_affect aag l) device_state b ba; equiv_irq_state b ba; reads_equiv aag st t; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> reads_equiv aag (st\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) \<and> affects_equiv aag l (st\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>)
 2. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>(r, ms') (r', ms''). r = r' \<and> equiv_machine_state (aag_can_read aag) ms' ms'' \<and> equiv_machine_state (aag_can_affect aag l) ms' ms'' \<and> equiv_irq_state ms' ms'') (\<lambda>_. True) (\<lambda>_. True) (select_f (f rv)) (select_f (f rv'))
 3. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>r. (=) st\<rbrace>
 4. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'9 rv rv'\<rbrace> select_f (f rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' s
 6. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 rv rv' s
 7. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 9. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>(r, ms') (r', ms''). r = r' \<and> equiv_machine_state (aag_can_read aag) ms' ms'' \<and> equiv_machine_state (aag_can_affect aag l) ms' ms'' \<and> equiv_irq_state ms' ms'') (\<lambda>_. True) (\<lambda>_. True) (select_f (f rv)) (select_f (f rv'))
 2. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>r. (=) st\<rbrace>
 3. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'9 rv rv'\<rbrace> select_f (f rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' s
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 rv rv' s
 6. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 8. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; equiv_valid_inv (equiv_machine_state (aag_can_read aag) and equiv_irq_state) (equiv_machine_state (aag_can_affect aag l)) Q f\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>(r, ms') (r', ms''). r = r' \<and> equiv_machine_state (aag_can_read aag) ms' ms'' \<and> equiv_machine_state (aag_can_affect aag l) ms' ms'' \<and> equiv_irq_state ms' ms'') (\<lambda>_. True) (\<lambda>_. True) (select_f (f rv)) (select_f (f rv'))
 2. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>r. (=) st\<rbrace>
 3. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'9 rv rv'\<rbrace> select_f (f rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' s
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 rv rv' s
 6. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 8. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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>rv rv' a b aa ba s t. \<lbrakk>Q rv; Q rv'; \<forall>s t. Q s \<and> Q t \<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) \<and> equiv_irq_state s t \<and> (\<forall>x. aag_can_affect aag l x \<longrightarrow> underlying_memory s x = underlying_memory t x) \<and> (\<forall>x. aag_can_affect aag l x \<longrightarrow> device_state s x = device_state t x) \<longrightarrow> (\<forall>x\<in>fst (f s). \<forall>xa\<in>fst (f t). fst x = fst xa \<and> (\<forall>xb. aag_can_read aag xb \<longrightarrow> underlying_memory (snd x) xb = underlying_memory (snd xa) xb) \<and> (\<forall>xb. aag_can_read aag xb \<longrightarrow> device_state (snd x) xb = device_state (snd xa) xb) \<and> equiv_irq_state (snd x) (snd xa) \<and> (\<forall>xb. aag_can_affect aag l xb \<longrightarrow> underlying_memory (snd x) xb = underlying_memory (snd xa) xb) \<and> (\<forall>xb. aag_can_affect aag l xb \<longrightarrow> device_state (snd x) xb = device_state (snd xa) xb)); \<forall>x. (aag_can_read aag x \<longrightarrow> underlying_memory rv x = underlying_memory rv' x) \<and> (aag_can_affect aag l x \<longrightarrow> underlying_memory rv x = underlying_memory rv' x); \<forall>x. (aag_can_read aag x \<longrightarrow> device_state rv x = device_state rv' x) \<and> (aag_can_affect aag l x \<longrightarrow> device_state rv x = device_state rv' x); equiv_irq_state rv rv'; (a, b) \<in> fst (f rv); (aa, ba) \<in> fst (f rv'); reads_equiv aag s t; affects_equiv aag l 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) \<and> (\<forall>x. aag_can_affect aag l x \<longrightarrow> underlying_memory b x = underlying_memory ba x) \<and> (\<forall>x. aag_can_affect aag l x \<longrightarrow> device_state b x = device_state ba x) \<and> equiv_irq_state b ba
 2. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>r. (=) st\<rbrace>
 3. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'9 rv rv'\<rbrace> select_f (f rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' s
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 rv rv' s
 6. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 8. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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>rv rv' a b aa ba s t. \<lbrakk>Q rv; Q rv'; \<forall>x. (aag_can_read aag x \<longrightarrow> underlying_memory rv x = underlying_memory rv' x) \<and> (aag_can_affect aag l x \<longrightarrow> underlying_memory rv x = underlying_memory rv' x); \<forall>x. (aag_can_read aag x \<longrightarrow> device_state rv x = device_state rv' x) \<and> (aag_can_affect aag l x \<longrightarrow> device_state rv x = device_state rv' x); equiv_irq_state rv rv'; (a, b) \<in> fst (f rv); (aa, ba) \<in> fst (f rv'); reads_equiv aag s t; affects_equiv aag l s t; Q rv \<and> Q rv' \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> underlying_memory rv x = underlying_memory rv' x) \<and> (\<forall>x. aag_can_read aag x \<longrightarrow> device_state rv x = device_state rv' x) \<and> equiv_irq_state rv rv' \<and> (\<forall>x. aag_can_affect aag l x \<longrightarrow> underlying_memory rv x = underlying_memory rv' x) \<and> (\<forall>x. aag_can_affect aag l x \<longrightarrow> device_state rv x = device_state rv' x) \<longrightarrow> (\<forall>x\<in>fst (f rv). \<forall>xa\<in>fst (f rv'). fst x = fst xa \<and> (\<forall>xb. aag_can_read aag xb \<longrightarrow> underlying_memory (snd x) xb = underlying_memory (snd xa) xb) \<and> (\<forall>xb. aag_can_read aag xb \<longrightarrow> device_state (snd x) xb = device_state (snd xa) xb) \<and> equiv_irq_state (snd x) (snd xa) \<and> (\<forall>xb. aag_can_affect aag l xb \<longrightarrow> underlying_memory (snd x) xb = underlying_memory (snd xa) xb) \<and> (\<forall>xb. aag_can_affect aag l xb \<longrightarrow> device_state (snd x) xb = device_state (snd xa) xb))\<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) \<and> (\<forall>x. aag_can_affect aag l x \<longrightarrow> underlying_memory b x = underlying_memory ba x) \<and> (\<forall>x. aag_can_affect aag l x \<longrightarrow> device_state b x = device_state ba x) \<and> equiv_irq_state b ba
 2. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>r. (=) st\<rbrace>
 3. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'9 rv rv'\<rbrace> select_f (f rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' s
 5. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 rv rv' s
 6. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 8. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>r. (=) st\<rbrace>
 2. \<And>rv rv'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'9 rv rv'\<rbrace> select_f (f rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; st = s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' s
 4. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 rv rv' s
 5. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 7. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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'. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'\<rbrakk> \<Longrightarrow> \<lbrace>?S'9 rv rv'\<rbrace> select_f (f rv') \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; st = s\<rbrakk> \<Longrightarrow> True \<and> st = s
 3. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; True\<rbrakk> \<Longrightarrow> True \<and> ?S'9 rv rv' s
 4. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 6. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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 or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; st = s\<rbrakk> \<Longrightarrow> True \<and> st = s
 2. \<And>rv rv' s. \<lbrakk>equiv_machine_state (aag_can_read aag or aag_can_affect aag l) rv rv' \<and> equiv_irq_state rv rv'; Q rv; Q rv'; True\<rbrakk> \<Longrightarrow> True \<and> True
 3. equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag or aag_can_affect aag l) 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> Q r\<rbrace>
 5. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. equiv_for (\<lambda>x. aag_can_read aag x \<or> aag_can_affect aag l x) underlying_memory rv rv' \<and> equiv_for (\<lambda>x. aag_can_read aag x \<or> aag_can_affect aag l x) 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> Q r\<rbrace>
 3. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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; affects_equiv aag l st t\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. aag_can_read aag x \<or> aag_can_affect aag l x) underlying_memory (machine_state st) (machine_state t) \<and> equiv_for (\<lambda>x. aag_can_read aag x \<or> aag_can_affect aag l x) 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> Q r\<rbrace>
 3. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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> Q r\<rbrace>
 2. \<lbrace>?S'4\<rbrace> gets machine_state \<lbrace>\<lambda>r s. Q r\<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!