# Theory Classical_Extra

```section ‹Derived facts about classical registers›

theory Classical_Extra
imports Laws_Classical Misc
begin

lemma register_from_getter_setter_of_getter_setter[simp]: ‹register_from_getter_setter (getter F) (setter F) = F› if ‹register F›
by (metis getter_of_register_from_getter_setter register_def setter_of_register_from_getter_setter that)

lemma valid_getter_setter_getter_setter[simp]: ‹valid_getter_setter (getter F) (setter F)› if ‹register F›
by (metis getter_of_register_from_getter_setter register_def setter_of_register_from_getter_setter that)

lemma register_register_from_getter_setter[simp]: ‹register (register_from_getter_setter g s)› if ‹valid_getter_setter g s›
using register_def that by blast

definition ‹total_fun f = (∀x. f x ≠ None)›

lemma register_total:
assumes ‹register F›
assumes ‹total_fun a›
shows ‹total_fun (F a)›
using assms
by (auto simp: register_def total_fun_def register_from_getter_setter_def option.case_eq_if)

lemma register_apply:
assumes ‹register F›
shows ‹Some o register_apply F a = F (Some o a)›
proof -
have ‹total_fun (F (Some o a))›
using assms apply (rule register_total)
by (auto simp: total_fun_def)
then show ?thesis
by (auto simp: register_apply_def dom_def total_fun_def)
qed

lemma register_empty:
assumes ‹preregister F›
shows ‹F Map.empty = Map.empty›
using assms unfolding preregister_def by auto

lemma compatible_setter:
fixes F :: ‹('a,'c) preregister› and G :: ‹('b,'c) preregister›
assumes [simp]: ‹register F› ‹register G›
shows ‹compatible F G ⟷ (∀a b. setter F a o setter G b = setter G b o setter F a)›
proof (intro allI iffI)
fix a b
assume ‹compatible F G›
then show ‹setter F a o setter G b = setter G b o setter F a›
apply (rule_tac compatible_setter)
unfolding compatible_def by auto
next
assume commute[rule_format, THEN fun_cong, unfolded o_def]: ‹∀a b. setter F a ∘ setter G b = setter G b ∘ setter F a›
have ‹valid_getter_setter (getter F) (setter F)›
by auto
then have ‹F a ∘⇩m G b = G b ∘⇩m F a› for a b
apply (subst (2) register_from_getter_setter_of_getter_setter[symmetric, of F], simp)
apply (subst (1) register_from_getter_setter_of_getter_setter[symmetric, of F], simp)
apply (subst (2) register_from_getter_setter_of_getter_setter[symmetric, of G], simp)
apply (subst (1) register_from_getter_setter_of_getter_setter[symmetric, of G], simp)
unfolding register_from_getter_setter_def valid_getter_setter_def
apply (auto intro!: ext simp: option.case_eq_if map_comp_def) (* Sledgehammer: *)
apply ((metis commute option.distinct option.simps)+)[4]
apply (smt (verit, ccfv_threshold) assms(2) commute valid_getter_setter_def valid_getter_setter_getter_setter)
apply (smt (verit, ccfv_threshold) assms(2) commute valid_getter_setter_def valid_getter_setter_getter_setter)
by (smt (verit, del_insts) assms(2) commute option.inject valid_getter_setter_def valid_getter_setter_getter_setter)
then show ‹compatible F G›
unfolding compatible_def by auto
qed

lemma register_from_getter_setter_compatibleI[intro]:
assumes [simp]: ‹valid_getter_setter g s› ‹valid_getter_setter g' s'›
assumes ‹⋀x y m. s x (s' y m) = s' y (s x m)›
shows ‹compatible (register_from_getter_setter g s) (register_from_getter_setter g' s')›
apply (subst compatible_setter)
using assms by auto

lemma separating_update1:
‹separating TYPE(_) {update1 x y | x y. True}›
by (smt (verit) mem_Collect_eq separating_def update1_extensionality)

definition "permutation_register (p::'b⇒'a) = register_from_getter_setter p (λa _. inv p a)"

lemma permutation_register_register[simp]:
fixes p :: "'b ⇒ 'a"
assumes [simp]: "bij p"
shows "register (permutation_register p)"
apply (auto intro!: register_register_from_getter_setter simp: permutation_register_def valid_getter_setter_def bij_inv_eq_iff)
by (meson assms bij_inv_eq_iff)

lemma getter_permutation_register: ‹bij p ⟹ getter (permutation_register p) = p›
by (smt (verit, ccfv_threshold) bij_inv_eq_iff getter_of_register_from_getter_setter permutation_register_def valid_getter_setter_def)

lemma setter_permutation_register: ‹bij p ⟹ setter (permutation_register p) a m = inv p a›
by (metis bij_inv_eq_iff getter_permutation_register permutation_register_register valid_getter_setter_def valid_getter_setter_getter_setter)

definition empty_var :: ‹'a::{CARD_1} update ⇒ 'b update› where
"empty_var = register_from_getter_setter (λ_. undefined) (λ_ m. m)"

lemma valid_empty_var[simp]: ‹valid_getter_setter (λ_. (undefined::_::CARD_1)) (λ_ m. m)›

lemma register_empty_var[simp]: ‹register empty_var›
using empty_var_def register_def valid_empty_var by blast

lemma getter_empty_var[simp]: ‹getter empty_var m = undefined›
by (rule everything_the_same)

lemma setter_empty_var[simp]: ‹setter empty_var a m = m›

lemma empty_var_compatible[simp]: ‹compatible empty_var X› if [simp]: ‹register X›
apply (subst compatible_setter) by auto

lemma empty_var_compatible'[simp]: ‹register X ⟹ compatible X empty_var›
using compatible_sym empty_var_compatible by blast

paragraph ‹Example›

record memory =
x :: "int*int"
y :: nat

definition "X = register_from_getter_setter x (λa b. b⦇x:=a⦈)"
definition "Y = register_from_getter_setter y (λa b. b⦇y:=a⦈)"

lemma validX[simp]: ‹valid_getter_setter x (λa b. b⦇x:=a⦈)›
unfolding valid_getter_setter_def by auto

lemma registerX[simp]: ‹register X›
using X_def register_def validX by blast

lemma validY[simp]: ‹valid_getter_setter y (λa b. b⦇y:=a⦈)›
unfolding valid_getter_setter_def by auto

lemma registerY[simp]: ‹register Y›
using Y_def register_def validY by blast

lemma compatibleXY[simp]: ‹compatible X Y›
unfolding X_def Y_def by auto

(* Avoiding namespace pollution *)
hide_const (open) x y x_update y_update X Y

end
```