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)›
  by (simp add: valid_getter_setter_def)

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›
  by (simp add: empty_var_def setter_of_register_from_getter_setter)

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