theory GlobalsSwap

lemma global_data_valid:
  "global_data_valid g_hrs g_hrs_upd (global_data p (g :: 'g \<Rightarrow> ('a :: packed_type)) s)
    = (
        (\<forall>v v' gs. s (\<lambda>_. v) (s (\<lambda>_. v') gs) = s (\<lambda>_. v) gs)
            \<and> (\<forall>gs. s (\<lambda>_. g gs) gs = gs)
            \<and> (\<forall>v f gs. s (\<lambda>_. v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>_. v) gs))
            \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs)
            \<and> (\<forall>v gs. g_hrs (s (\<lambda>_. v) gs) = g_hrs gs)
            \<and> (\<forall>v gs. g (s (\<lambda>_. v) gs) = v))" proof - have all_to_xs: "\<And>P. (\<forall>(v :: 'a). P v) = (\<forall>xs. P (from_bytes xs))" apply (safe, simp_all) apply (drule_tac x="to_bytes_p v" in spec) apply (simp add: to_bytes_p_from_bytes) done show ?thesis apply (simp add: global_data_valid_def global_data_def) apply (simp add: all_to_xs order_less_imp_le[OF max_size]
                     inj_eq[OF to_bytes_p_inj] conj_comms K_def) apply (safe, simp_all add: to_bytes_p_from_bytes) apply (drule_tac x="to_bytes_p (from_bytes xs :: 'a)" in spec, drule mp) apply simp apply (simp add: inj_eq[OF to_bytes_p_inj]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_data_valid g_hrs g_hrs_upd (global_data p g s) = ((\<forall>v v' gs. s (\<lambda>_. v) (s (\<lambda>_. v') gs) = s (\<lambda>_. v) gs) \<and> (\<forall>gs. s (\<lambda>_. g gs) gs = gs) \<and> (\<forall>v f gs. s (\<lambda>_. v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>_. v) gs)) \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs) \<and> (\<forall>v gs. g_hrs (s (\<lambda>_. v) gs) = g_hrs gs) \<and> (\<forall>v gs. g (s (\<lambda>_. v) gs) = v)) proof (state)
goal (1 subgoal):
 1. global_data_valid g_hrs g_hrs_upd (global_data p g s) = ((\<forall>v v' gs. s (\<lambda>_. v) (s (\<lambda>_. v') gs) = s (\<lambda>_. v) gs) \<and> (\<forall>gs. s (\<lambda>_. g gs) gs = gs) \<and> (\<forall>v f gs. s (\<lambda>_. v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>_. v) gs)) \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs) \<and> (\<forall>v gs. g_hrs (s (\<lambda>_. v) gs) = g_hrs gs) \<and> (\<forall>v gs. g (s (\<lambda>_. v) gs) = v)) proof (prove)
goal (1 subgoal):
 1. \<And>P. (\<forall>v. P v) = (\<forall>xs. P (from_bytes xs)) proof (prove)
goal (1 subgoal):
 1. \<And>P v. \<forall>xs. P (from_bytes xs) \<Longrightarrow> P v proof (prove)
goal (1 subgoal):
 1. \<And>P v. P (from_bytes (to_bytes_p v)) \<Longrightarrow> P v proof (prove)
goal:
No subgoals! proof (state)
this:
(\<forall>v. ?P v) = (\<forall>xs. ?P (from_bytes xs))

goal (1 subgoal):
 1. global_data_valid g_hrs g_hrs_upd (global_data p g s) = ((\<forall>v v' gs. s (\<lambda>_. v) (s (\<lambda>_. v') gs) = s (\<lambda>_. v) gs) \<and> (\<forall>gs. s (\<lambda>_. g gs) gs = gs) \<and> (\<forall>v f gs. s (\<lambda>_. v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>_. v) gs)) \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs) \<and> (\<forall>v gs. g_hrs (s (\<lambda>_. v) gs) = g_hrs gs) \<and> (\<forall>v gs. g (s (\<lambda>_. v) gs) = v)) proof (prove)
goal (1 subgoal):
 1. global_data_valid g_hrs g_hrs_upd (global_data p g s) = ((\<forall>v v' gs. s (\<lambda>_. v) (s (\<lambda>_. v') gs) = s (\<lambda>_. v) gs) \<and> (\<forall>gs. s (\<lambda>_. g gs) gs = gs) \<and> (\<forall>v f gs. s (\<lambda>_. v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>_. v) gs)) \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs) \<and> (\<forall>v gs. g_hrs (s (\<lambda>_. v) gs) = g_hrs gs) \<and> (\<forall>v gs. g (s (\<lambda>_. v) gs) = v)) proof (prove)
goal (1 subgoal):
 1. ((\<forall>v v' gs. s (\<lambda>y. from_bytes v) (s (\<lambda>y. from_bytes v') gs) = s (\<lambda>y. from_bytes v) gs) \<and> (\<forall>gs. s (\<lambda>y. g gs) gs = gs) \<and> (\<forall>v. length v = size_of TYPE('a) \<longrightarrow> (\<forall>gs. to_bytes_p (g (s (\<lambda>y. from_bytes v) gs)) = v)) \<and> (\<forall>v f gs. s (\<lambda>y. from_bytes v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>y. from_bytes v) gs)) \<and> (\<forall>v gs. g_hrs (s (\<lambda>y. from_bytes v) gs) = g_hrs gs) \<and> (\<forall>f gs. to_bytes_p (g (g_hrs_upd f gs)) = to_bytes_p (g gs))) = ((\<forall>v v' gs. s (\<lambda>_. v) (s (\<lambda>_. v') gs) = s (\<lambda>_. v) gs) \<and> (\<forall>gs. s (\<lambda>_. g gs) gs = gs) \<and> (\<forall>v f gs. s (\<lambda>_. v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>_. v) gs)) \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs) \<and> (\<forall>v gs. g_hrs (s (\<lambda>_. v) gs) = g_hrs gs) \<and> (\<forall>v gs. g (s (\<lambda>_. v) gs) = v)) proof (prove)
goal (1 subgoal):
 1. ((\<forall>gs. s (\<lambda>y. g gs) gs = gs) \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs) \<and> (\<forall>v gs. g_hrs (s (\<lambda>y. from_bytes v) gs) = g_hrs gs) \<and> (\<forall>v. length v = size_of TYPE('a) \<longrightarrow> (\<forall>gs. to_bytes_p (g (s (\<lambda>y. from_bytes v) gs)) = v)) \<and> (\<forall>v f gs. s (\<lambda>y. from_bytes v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>y. from_bytes v) gs)) \<and> (\<forall>v v' gs. s (\<lambda>y. from_bytes v) (s (\<lambda>y. from_bytes v') gs) = s (\<lambda>y. from_bytes v) gs)) = ((\<forall>gs. s (\<lambda>_. g gs) gs = gs) \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs) \<and> (\<forall>xs gs. g (s (\<lambda>_. from_bytes xs) gs) = from_bytes xs) \<and> (\<forall>xs gs. g_hrs (s (\<lambda>_. from_bytes xs) gs) = g_hrs gs) \<and> (\<forall>xs f gs. s (\<lambda>_. from_bytes xs) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>_. from_bytes xs) gs)) \<and> (\<forall>xs xsa gs. s (\<lambda>_. from_bytes xs) (s (\<lambda>_. from_bytes xsa) gs) = s (\<lambda>_. from_bytes xs) gs)) proof (prove)
goal (1 subgoal):
 1. \<And>xs gs. \<lbrakk>\<forall>gs. s (\<lambda>y. g gs) gs = gs; \<forall>f gs. g (g_hrs_upd f gs) = g gs; \<forall>v gs. g_hrs (s (\<lambda>y. from_bytes v) gs) = g_hrs gs; \<forall>v. length v = size_of TYPE('a) \<longrightarrow> (\<forall>gs. to_bytes_p (g (s (\<lambda>y. from_bytes v) gs)) = v); \<forall>v f gs. s (\<lambda>y. from_bytes v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>y. from_bytes v) gs); \<forall>v v' gs. s (\<lambda>y. from_bytes v) (s (\<lambda>y. from_bytes v') gs) = s (\<lambda>y. from_bytes v) gs\<rbrakk> \<Longrightarrow> g (s (\<lambda>_. from_bytes xs) gs) = from_bytes xs proof (prove)
goal (2 subgoals):
 1. \<And>xs gs. \<lbrakk>\<forall>gs. s (\<lambda>y. g gs) gs = gs; \<forall>f gs. g (g_hrs_upd f gs) = g gs; \<forall>v gs. g_hrs (s (\<lambda>y. from_bytes v) gs) = g_hrs gs; \<forall>v f gs. s (\<lambda>y. from_bytes v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>y. from_bytes v) gs); \<forall>v v' gs. s (\<lambda>y. from_bytes v) (s (\<lambda>y. from_bytes v') gs) = s (\<lambda>y. from_bytes v) gs\<rbrakk> \<Longrightarrow> length (to_bytes_p (from_bytes xs)) = size_of TYPE('a)
 2. \<And>xs gs. \<lbrakk>\<forall>gs. s (\<lambda>y. g gs) gs = gs; \<forall>f gs. g (g_hrs_upd f gs) = g gs; \<forall>v gs. g_hrs (s (\<lambda>y. from_bytes v) gs) = g_hrs gs; \<forall>v f gs. s (\<lambda>y. from_bytes v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>y. from_bytes v) gs); \<forall>v v' gs. s (\<lambda>y. from_bytes v) (s (\<lambda>y. from_bytes v') gs) = s (\<lambda>y. from_bytes v) gs; \<forall>gs. to_bytes_p (g (s (\<lambda>y. from_bytes (to_bytes_p (from_bytes xs))) gs)) = to_bytes_p (from_bytes xs)\<rbrakk> \<Longrightarrow> g (s (\<lambda>_. from_bytes xs) gs) = from_bytes xs proof (prove)
goal (1 subgoal):
 1. \<And>xs gs. \<lbrakk>\<forall>gs. s (\<lambda>y. g gs) gs = gs; \<forall>f gs. g (g_hrs_upd f gs) = g gs; \<forall>v gs. g_hrs (s (\<lambda>y. from_bytes v) gs) = g_hrs gs; \<forall>v f gs. s (\<lambda>y. from_bytes v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>y. from_bytes v) gs); \<forall>v v' gs. s (\<lambda>y. from_bytes v) (s (\<lambda>y. from_bytes v') gs) = s (\<lambda>y. from_bytes v) gs; \<forall>gs. to_bytes_p (g (s (\<lambda>y. from_bytes (to_bytes_p (from_bytes xs))) gs)) = to_bytes_p (from_bytes xs)\<rbrakk> \<Longrightarrow> g (s (\<lambda>_. from_bytes xs) gs) = from_bytes xs proof (prove)
goal:
No subgoals! proof (state)
this:
global_data_valid g_hrs g_hrs_upd (global_data p g s) = ((\<forall>v v' gs. s (\<lambda>_. v) (s (\<lambda>_. v') gs) = s (\<lambda>_. v) gs) \<and> (\<forall>gs. s (\<lambda>_. g gs) gs = gs) \<and> (\<forall>v f gs. s (\<lambda>_. v) (g_hrs_upd f gs) = g_hrs_upd f (s (\<lambda>_. v) gs)) \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs) \<and> (\<forall>v gs. g_hrs (s (\<lambda>_. v) gs) = g_hrs gs) \<and> (\<forall>v gs. g (s (\<lambda>_. v) gs) = v))

goal:
No subgoals!