theory global_asm_stmt_gref

lemma phantom_machine_state_'_update_globals_swap[simp]:
  "phantom_machine_state_' (gswap gs) = phantom_machine_state_' gs
    \<and> gswap (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (gswap gs)" apply (rule globals_swap_ex_swap) apply (simp only: globals_list_def global_data_defs list.simps ball_simps
                     is_global_data_simps simp_thms) apply (simp_all add: global_data_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. phantom_machine_state_' (gswap gs) = phantom_machine_state_' gs \<and> gswap (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (gswap gs) proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set global_data_list. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (s' v gs)) \<and> (\<forall>v gs. g' (phantom_machine_state_'_update f gs) = g' gs) \<and> (\<forall>v gs. phantom_machine_state_' (s' v gs) = phantom_machine_state_' gs))
 2. (\<forall>v v' gs. t_hrs_'_update v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (t_hrs_'_update v gs)) \<and> (\<forall>v gs. phantom_machine_state_' (t_hrs_'_update v gs) = phantom_machine_state_' gs) \<and> (\<forall>v gs. t_hrs_' (phantom_machine_state_'_update f gs) = t_hrs_' gs) proof (prove)
goal (2 subgoals):
 1. (case global_data ''a_mod_global'' a_mod_global_' a_mod_global_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (phantom_machine_state_'_update f gs) = g' gs) \<and> (\<forall>v gs. phantom_machine_state_' (s' v gs) = phantom_machine_state_' gs)) \<and> (case global_data ''b_mod_global'' b_mod_global_' b_mod_global_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (phantom_machine_state_'_update f gs) = g' gs) \<and> (\<forall>v gs. phantom_machine_state_' (s' v gs) = phantom_machine_state_' gs)) \<and> (case global_data ''c_mod_global'' c_mod_global_' c_mod_global_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (phantom_machine_state_'_update f gs) = g' gs) \<and> (\<forall>v gs. phantom_machine_state_' (s' v gs) = phantom_machine_state_' gs)) \<and> (case global_data ''d_mod_global'' d_mod_global_' d_mod_global_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (phantom_machine_state_'_update f gs) = g' gs) \<and> (\<forall>v gs. phantom_machine_state_' (s' v gs) = phantom_machine_state_' gs))
 2. (\<forall>v v' gs. t_hrs_'_update v (phantom_machine_state_'_update f gs) = phantom_machine_state_'_update f (t_hrs_'_update v gs)) \<and> (\<forall>v gs. phantom_machine_state_' (t_hrs_'_update v gs) = phantom_machine_state_' gs) \<and> (\<forall>v gs. t_hrs_' (phantom_machine_state_'_update f gs) = t_hrs_' gs) proof (prove)
goal:
No subgoals!