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. bx:=a)"
definition "Y = register_from_getter_setter y (λa b. by:=a)"

lemma validX[simp]: valid_getter_setter x (λa b. bx:=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. by:=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