theory SEL4GlobalsSwap

lemma globals_swap_ex_swap:
  "\<forall>x \<in> set gxs. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s'
        \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs))
            \<and> (\<forall>v gs. g' (s v gs) = g' gs)
            \<and> (\<forall>v gs. g (s' v gs) = g gs))
    \<Longrightarrow> (\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs))
            \<and> (\<forall>v gs. g (th_s v gs) = g gs)
            \<and> (\<forall>v gs. th_g (s v gs) = th_g gs)
    \<Longrightarrow> g (globals_swap th_g th_s symt gxs gs) = g gs
    \<and> globals_swap th_g th_s symt gxs (s v gs) = s v (globals_swap th_g th_s symt gxs gs)" apply (simp add: globals_swap_def) apply (rule conjI) apply (rule foldr_does_nothing_to_xf) apply (drule(1) bspec) apply (case_tac x, simp_all add: global_swap_def is_global_data_def K_def) apply (rule foldr_update_commutes[symmetric]) apply (drule(1) bspec) apply (case_tac x, simp_all add: global_swap_def is_global_data_def K_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set gxs. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs)) \<and> (\<forall>v gs. g' (s v gs) = g' gs) \<and> (\<forall>v gs. g (s' v gs) = g gs)); (\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs)) \<and> (\<forall>v gs. g (th_s v gs) = g gs) \<and> (\<forall>v gs. th_g (s v gs) = th_g gs)\<rbrakk> \<Longrightarrow> g (globals_swap th_g th_s symt gxs gs) = g gs \<and> globals_swap th_g th_s symt gxs (s v gs) = s v (globals_swap th_g th_s symt gxs gs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set gxs. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs)) \<and> (\<forall>v gs. g' (s v gs) = g' gs) \<and> (\<forall>v gs. g (s' v gs) = g gs)); (\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs)) \<and> (\<forall>v gs. g (th_s v gs) = g gs) \<and> (\<forall>v gs. th_g (s v gs) = th_g gs)\<rbrakk> \<Longrightarrow> g (foldr (global_swap th_g th_s symt) gxs gs) = g gs \<and> foldr (global_swap th_g th_s symt) gxs (s v gs) = s v (foldr (global_swap th_g th_s symt) gxs gs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set gxs. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs)) \<and> (\<forall>v gs. g' (s v gs) = g' gs) \<and> (\<forall>v gs. g (s' v gs) = g gs)); (\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs)) \<and> (\<forall>v gs. g (th_s v gs) = g gs) \<and> (\<forall>v gs. th_g (s v gs) = th_g gs)\<rbrakk> \<Longrightarrow> g (foldr (global_swap th_g th_s symt) gxs gs) = g gs
 2. \<lbrakk>\<forall>x\<in>set gxs. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs)) \<and> (\<forall>v gs. g' (s v gs) = g' gs) \<and> (\<forall>v gs. g (s' v gs) = g gs)); (\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs)) \<and> (\<forall>v gs. g (th_s v gs) = g gs) \<and> (\<forall>v gs. th_g (s v gs) = th_g gs)\<rbrakk> \<Longrightarrow> foldr (global_swap th_g th_s symt) gxs (s v gs) = s v (foldr (global_swap th_g th_s symt) gxs gs) proof (prove)
goal (2 subgoals):
 1. \<And>x sa. \<lbrakk>\<forall>x\<in>set gxs. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs)) \<and> (\<forall>v gs. g' (s v gs) = g' gs) \<and> (\<forall>v gs. g (s' v gs) = g gs)); (\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs)) \<and> (\<forall>v gs. g (th_s v gs) = g gs) \<and> (\<forall>v gs. th_g (s v gs) = th_g gs); x \<in> set gxs\<rbrakk> \<Longrightarrow> g (global_swap th_g th_s symt x sa) = g sa
 2. \<lbrakk>\<forall>x\<in>set gxs. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs)) \<and> (\<forall>v gs. g' (s v gs) = g' gs) \<and> (\<forall>v gs. g (s' v gs) = g gs)); (\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs)) \<and> (\<forall>v gs. g (th_s v gs) = g gs) \<and> (\<forall>v gs. th_g (s v gs) = th_g gs)\<rbrakk> \<Longrightarrow> foldr (global_swap th_g th_s symt) gxs (s v gs) = s v (foldr (global_swap th_g th_s symt) gxs gs) proof (prove)
goal (2 subgoals):
 1. \<And>x sa. \<lbrakk>(\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs)) \<and> (\<forall>v gs. g (th_s v gs) = g gs) \<and> (\<forall>v gs. th_g (s v gs) = th_g gs); x \<in> set gxs; is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs)) \<and> (\<forall>v gs. g' (s v gs) = g' gs) \<and> (\<forall>v gs. g (s' v gs) = g gs))\<rbrakk> \<Longrightarrow> g (global_swap th_g th_s symt x sa) = g sa
 2. \<lbrakk>\<forall>x\<in>set gxs. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs)) \<and> (\<forall>v gs. g' (s v gs) = g' gs) \<and> (\<forall>v gs. g (s' v gs) = g gs)); (\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs)) \<and> (\<forall>v gs. g (th_s v gs) = g gs) \<and> (\<forall>v gs. th_g (s v gs) = th_g gs)\<rbrakk> \<Longrightarrow> foldr (global_swap th_g th_s symt) gxs (s v gs) = s v (foldr (global_swap th_g th_s symt) gxs gs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set gxs. (case x of GlobalData x xa xb xc xd \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs)) \<and> (\<forall>v gs. g' (s v gs) = g' gs) \<and> (\<forall>v gs. g (s' v gs) = g gs)); (\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs)) \<and> (\<forall>v gs. g (th_s v gs) = g gs) \<and> (\<forall>v gs. th_g (s v gs) = th_g gs)\<rbrakk> \<Longrightarrow> foldr (global_swap th_g th_s symt) gxs (s v gs) = s v (foldr (global_swap th_g th_s symt) gxs gs) proof (prove)
goal (1 subgoal):
 1. \<And>x sa. \<lbrakk>\<forall>x\<in>set gxs. (case x of GlobalData x xa xb xc xd \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs)) \<and> (\<forall>v gs. g' (s v gs) = g' gs) \<and> (\<forall>v gs. g (s' v gs) = g gs)); (\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs)) \<and> (\<forall>v gs. g (th_s v gs) = g gs) \<and> (\<forall>v gs. th_g (s v gs) = th_g gs); x \<in> set gxs\<rbrakk> \<Longrightarrow> s v (global_swap th_g th_s symt x sa) = global_swap th_g th_s symt x (s v sa) proof (prove)
goal (1 subgoal):
 1. \<And>x sa. \<lbrakk>(\<forall>v v' gs. th_s v (s v' gs) = s v' (th_s v gs)) \<and> (\<forall>v gs. g (th_s v gs) = g gs) \<and> (\<forall>v gs. th_g (s v gs) = th_g gs); x \<in> set gxs; (case x of GlobalData x xa xb xc xd \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (s v' gs) = s v' (s' v gs)) \<and> (\<forall>v gs. g' (s v gs) = g' gs) \<and> (\<forall>v gs. g (s' v gs) = g gs))\<rbrakk> \<Longrightarrow> s v (global_swap th_g th_s symt x sa) = global_swap th_g th_s symt x (s v sa) proof (prove)
goal:
No subgoals!