theory InfoFlow_IF

lemma do_machine_op_rev:
  assumes equiv_dmo: "equiv_valid_inv (equiv_machine_state (aag_can_read aag)) \<top>\<top> \<top> f"
  assumes mo_inv: "\<And>P. f \<lbrace>P\<rbrace>"
  shows "reads_equiv_valid_inv A aag \<top> (do_machine_op f)" unfolding do_machine_op_def equiv_valid_def2 apply (rule_tac W="\<lambda> rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv'"
             and Q="\<lambda> rv s. rv = machine_state s " in equiv_valid_rv_bind) apply (blast intro: equiv_valid_rv_guard_imp[OF gets_machine_state_revrv'[simplified pred_conj_def]]) 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 Q'="\<lambda> (r',ms'') s. ms'' = rv' \<and> rv' = machine_state s"
              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 (clarsimp simp: select_f_def equiv_valid_2_def) apply (insert equiv_dmo, clarsimp simp: equiv_valid_def2 equiv_valid_2_def)[1] apply blast apply (wp select_f_inv)+ apply (fastforce simp: select_f_def dest: state_unchanged[OF mo_inv])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>_. True) (do_machine_op f) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv A aag (=) (\<lambda>_. True) (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. reads_equiv_valid_rv_inv A aag (\<lambda>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv') (\<lambda>_. True) (gets machine_state)
 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>s. 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)
 3. \<lbrace>\<lambda>_. True\<rbrace> gets machine_state \<lbrace>\<lambda>rv s. rv = machine_state s\<rbrace> proof (prove)
goal (2 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. 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. \<lbrace>\<lambda>_. True\<rbrace> gets machine_state \<lbrace>\<lambda>rv s. rv = machine_state s\<rbrace> proof (prove)
goal (7 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) (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>_. True) (\<lambda>_. True) (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>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s\<rbrace>
 4. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>?S'9 rv rv'\<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'; rv = machine_state s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' 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> True \<and> ?S'9 rv rv' s
 7. \<lbrace>\<lambda>_. True\<rbrace> gets machine_state \<lbrace>\<lambda>rv s. rv = machine_state s\<rbrace> 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>(r, ms') (r', ms''). r = r' \<and> equiv_machine_state (aag_can_read aag) ms' ms'') (\<lambda>_. True) (\<lambda>_. True) (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>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s\<rbrace>
 3. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>?S'9 rv rv'\<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'; rv = machine_state s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' 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> True \<and> ?S'9 rv rv' s
 6. \<lbrace>\<lambda>_. True\<rbrace> gets machine_state \<lbrace>\<lambda>rv s. rv = machine_state s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' a b aa ba s t. \<lbrakk>equiv_for (aag_can_read aag) underlying_memory rv rv'; equiv_for (aag_can_read aag) device_state rv rv'; equiv_irq_state rv rv'; (a, b) \<in> fst (f rv); (aa, ba) \<in> fst (f rv'); reads_equiv aag s t; A s t\<rbrakk> \<Longrightarrow> a = aa \<and> equiv_machine_state (aag_can_read aag) b ba
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s\<rbrace>
 3. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>?S'9 rv rv'\<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'; rv = machine_state s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' 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> True \<and> ?S'9 rv rv' s
 6. \<lbrace>\<lambda>_. True\<rbrace> gets machine_state \<lbrace>\<lambda>rv s. rv = machine_state s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' a b aa ba s t. \<lbrakk>equiv_for (aag_can_read aag) underlying_memory rv rv'; equiv_for (aag_can_read aag) device_state rv rv'; equiv_irq_state rv rv'; (a, b) \<in> fst (f rv); (aa, ba) \<in> fst (f rv'); reads_equiv aag s t; A s t; \<forall>s t. equiv_machine_state (aag_can_read aag) s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> equiv_machine_state (aag_can_read aag) s' t')\<rbrakk> \<Longrightarrow> a = aa \<and> equiv_machine_state (aag_can_read aag) b ba
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s\<rbrace>
 3. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>?S'9 rv rv'\<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'; rv = machine_state s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' 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> True \<and> ?S'9 rv rv' s
 6. \<lbrace>\<lambda>_. True\<rbrace> gets machine_state \<lbrace>\<lambda>rv s. rv = machine_state s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>?S9 rv rv'\<rbrace> select_f (f rv) \<lbrace>\<lambda>(r, ms') s. ms' = rv \<and> rv = machine_state s\<rbrace>
 2. \<And>rv rv'. equiv_machine_state (aag_can_read aag) rv rv' \<and> equiv_irq_state rv rv' \<Longrightarrow> \<lbrace>?S'9 rv rv'\<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'; rv = machine_state s\<rbrakk> \<Longrightarrow> True \<and> ?S9 rv rv' 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> True \<and> ?S'9 rv rv' s
 5. \<lbrace>\<lambda>_. True\<rbrace> gets machine_state \<lbrace>\<lambda>rv s. rv = machine_state s\<rbrace> proof (prove)
goal (3 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> True \<and> (\<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'; rv' = machine_state s\<rbrakk> \<Longrightarrow> True \<and> (\<forall>x\<in>fst (f rv'). (case x of (r', ms'') \<Rightarrow> \<lambda>s. ms'' = rv' \<and> rv' = machine_state s) s)
 3. \<lbrace>\<lambda>_. True\<rbrace> gets machine_state \<lbrace>\<lambda>rv s. rv = machine_state s\<rbrace> proof (prove)
goal:
No subgoals!