theory GlobalsSwap

lemma global_swap_cancel:
  "\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
         global_data_valid g_hrs g_hrs_upd gd \<rbrakk>
  \<Longrightarrow> global_swap g_hrs g_hrs_upd symtab gd (global_swap g_hrs g_hrs_upd symtab gd gs) = gs" apply (insert heap_list_update[where
                v="case gd of GlobalData _ _ _ g _ \<Rightarrow> g gs"]) apply (clarsimp simp: global_swap_def hrs_mem_update
                        global_data_valid_def global_acc_valid_def
                 split: global_data.split) apply (simp add: hrs_mem_update_def split_def o_def) apply (simp add: heap_update_list_double_id hrs_mem_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; global_data_valid g_hrs g_hrs_upd gd\<rbrakk> \<Longrightarrow> global_swap g_hrs g_hrs_upd symtab gd (global_swap g_hrs g_hrs_upd symtab gd gs) = gs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; global_data_valid g_hrs g_hrs_upd gd; \<And>p h. length (case gd of GlobalData x xa xb g xc \<Rightarrow> g gs) \<le> addr_card \<Longrightarrow> heap_list (heap_update_list p (case gd of GlobalData x xa xb g xc \<Rightarrow> g gs) h) (length (case gd of GlobalData x xa xb g xc \<Rightarrow> g gs)) p = (case gd of GlobalData x xa xb g xc \<Rightarrow> g gs)\<rbrakk> \<Longrightarrow> global_swap g_hrs g_hrs_upd symtab gd (global_swap g_hrs g_hrs_upd symtab gd gs) = gs proof (prove)
goal (1 subgoal):
 1. \<And>x11 x12 x13 x14 x15. \<lbrakk>\<And>p h. heap_list (heap_update_list p (x14 gs) h) x12 p = x14 gs; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (f \<circ> f') s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; gd = GlobalData x11 x12 x13 x14 x15; \<forall>gs. length (x14 gs) = x12; \<forall>v v' gs. x15 v (x15 v' gs) = x15 v gs; \<forall>gs. x15 (x14 gs) gs = gs; \<forall>v. length v = x12 \<longrightarrow> (\<forall>gs. x14 (x15 v gs) = v); \<forall>v f gs. x15 v (g_hrs_upd f gs) = g_hrs_upd f (x15 v gs); \<forall>v gs. g_hrs (x15 v gs) = g_hrs gs; \<forall>f gs. x14 (g_hrs_upd f gs) = x14 gs; x12 < addr_card\<rbrakk> \<Longrightarrow> g_hrs_upd (\<lambda>_. hrs_mem_update (heap_update_list (symtab x11) (heap_list (hrs_mem (g_hrs gs)) x12 (symtab x11))) (hrs_mem_update (heap_update_list (symtab x11) (x14 gs)) (g_hrs gs))) gs = gs proof (prove)
goal (1 subgoal):
 1. \<And>x11 x12 x13 x14 x15. \<lbrakk>\<And>p h. heap_list (heap_update_list p (x14 gs) h) x12 p = x14 gs; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; gd = GlobalData x11 x12 x13 x14 x15; \<forall>gs. length (x14 gs) = x12; \<forall>v v' gs. x15 v (x15 v' gs) = x15 v gs; \<forall>gs. x15 (x14 gs) gs = gs; \<forall>v. length v = x12 \<longrightarrow> (\<forall>gs. x14 (x15 v gs) = v); \<forall>v f gs. x15 v (g_hrs_upd f gs) = g_hrs_upd f (x15 v gs); \<forall>v gs. g_hrs (x15 v gs) = g_hrs gs; \<forall>f gs. x14 (g_hrs_upd f gs) = x14 gs; x12 < addr_card\<rbrakk> \<Longrightarrow> g_hrs_upd (\<lambda>_. (heap_update_list (symtab x11) (heap_list (hrs_mem (g_hrs gs)) x12 (symtab x11)) (heap_update_list (symtab x11) (x14 gs) (fst (g_hrs gs))), snd (g_hrs gs))) gs = gs proof (prove)
goal:
No subgoals!