Theory Axioms_Classical

section Classical instantiation of registerss

(* AXIOM INSTANTIATION (use instantiate_laws.py to generate Laws_Classical.thy)
 
   domain → type
   comp_update → map_comp
   id_update → Some

   Generic laws about registers → Generic laws about registers, instantiated classically
*)

theory Axioms_Classical
  imports Main
begin

type_synonym 'a update = 'a  'a

lemma id_update_left: "Some m a = a"
  by (auto intro!: ext simp add: map_comp_def option.case_eq_if)
lemma id_update_right: "a m Some = a"
  by auto

lemma comp_update_assoc: "(a m b) m c = a m (b m c)"
  by (auto intro!: ext simp add: map_comp_def option.case_eq_if)

type_synonym ('a,'b) preregister = 'a update  'b update
definition preregister :: ('a,'b) preregister  bool where
  preregister F  (g s. a m. F a m = (case a (g m) of None  None | Some x  s x m))

lemma id_preregister: preregister id
  unfolding preregister_def
  apply (rule exI[of _ λm. m])
  apply (rule exI[of _ λa m. Some a])
  by (simp add: option.case_eq_if)

lemma preregister_mult_right: preregister (λa. a m z)
  unfolding preregister_def 
  apply (rule exI[of _ λm. the (z m)])
  apply (rule exI[of _ λx m. case z m of None  None | _  Some x])
  by (auto simp add: option.case_eq_if)

lemma preregister_mult_left: preregister (λa. z m a)
  unfolding preregister_def 
  apply (rule exI[of _ λm. m])
  apply (rule exI[of _ λx m. z x])
  by (auto simp add: option.case_eq_if)

lemma comp_preregister: "preregister (G  F)" if "preregister F" and preregister G
proof -
  from preregister F
  obtain sF gF where F: F a m = (case a (gF m) of None  None | Some x  sF x m) for a m
    using preregister_def by blast
  from preregister G
  obtain sG gG where G: G a m = (case a (gG m) of None  None | Some x  sG x m) for a m
    using preregister_def by blast
  define s g where s a m = (case sF a (gG m) of None  None | Some x  sG x m)
    and g m = gF (gG m) for a m
  have (G  F) a m = (case a (g m) of None  None | Some x  s x m) for a m
    unfolding F G s_def g_def
    by (auto simp add: option.case_eq_if)
  then show "preregister (G  F)"
    using preregister_def by blast
qed

definition tensor_update :: 'a update  'b update  ('a×'b) update where
  tensor_update a b m = (case a (fst m) of None  None | Some x  (case b (snd m) of None  None | Some y  Some (x,y)))

lemma tensor_update_mult: tensor_update a c m tensor_update b d = tensor_update (a m b) (c m d)
  by (auto intro!: ext simp add: map_comp_def option.case_eq_if tensor_update_def)

definition update1 :: 'a  'a  'a update where
  update1 x y m = (if m=x then Some y else None)

lemma update1_extensionality:
  assumes preregister F
  assumes preregister G
  assumes FGeq: x y. F (update1 x y) = G (update1 x y)
  shows "F = G"
proof (rule ccontr)
  assume neq: F  G
  then obtain z m where neq': F z m  G z m 
    apply atomize_elim by auto
  obtain gF sF where gsF: F z m = (case z (gF m) of None  None | Some x  sF x m) for z m
    using preregister F preregister_def by blast
  obtain gG sG where gsG: G z m = (case z (gG m) of None  None | Some x  sG x m) for z m
    using preregister G preregister_def by blast
  consider (abeq) x where z (gF m) = Some x z (gG m) = Some x gF m = gG m
    | (abnone) z (gG m) = None z (gF m) = None
    | (neqF) x where gF m  gG m F z m = Some x
    | (neqG) y where gF m  gG m G z m = Some y
    | (neqNone) gF m  gG m F z m = None G z m = None
    apply atomize_elim by (metis option.exhaust_sel)
  then show False
  proof cases
    case (abeq x)
    then have F z m = sF x m and G z m = sG x m
      by (simp_all add: gsF gsG)
    moreover have F (update1 (gF m) x) m = sF x m
      by (simp add: gsF update1_def)
    moreover have G (update1 (gF m) x) m = sG x m
      by (simp add: abeq gsG update1_def)
    ultimately show False
      using FGeq neq' by force
  next
    case abnone
    then show False
      using gsF gsG neq' by force
  next
    case neqF
    moreover
    have F (update1 (gF m) (the (z (gF m)))) m = F z m
      by (metis gsF neqF(2) option.case_eq_if option.simps(3) option.simps(5) update1_def)
    moreover have G (update1 (gF m) (the (z (gF m)))) m = None
      by (metis gsG neqF(1) option.case_eq_if update1_def)
    ultimately show False
      using FGeq by force
  next
    case neqG
    moreover
    have G (update1 (gG m) (the (z (gG m)))) m = G z m
      by (metis gsG neqG(2) option.case_eq_if option.distinct(1) option.simps(5) update1_def)
    moreover have F (update1 (gG m) (the (z (gG m)))) m = None
      by (simp add: gsF neqG(1) update1_def)
    ultimately show False
      using FGeq by force
  next
    case neqNone
    with neq' show False
      by fastforce
  qed
qed

lemma tensor_extensionality:
  assumes preregister F
  assumes preregister G
  assumes FGeq: a b. F (tensor_update a b) = G (tensor_update a b)
  shows "F = G"
proof -
  have F (update1 x y) = G (update1 x y) for x y
    using FGeq[of update1 (fst x) (fst y) update1 (snd x) (snd y)]
    apply (auto intro!:ext simp: tensor_update_def[abs_def] update1_def[abs_def])
    by (smt (z3) assms(1) assms(2) option.case(2) option.case_eq_if preregister_def prod.collapse)
  with assms(1,2) show "F = G"
    by (rule update1_extensionality)
qed

definition "valid_getter_setter g s  
  (b. b = s (g b) b)  (a b. g (s a b) = a)  (a a' b. s a (s a' b) = s a b)"

definition register_from_getter_setter g s a m = (case a (g m) of None  None | Some x  Some (s x m))
definition register_apply F a = the o F (Some o a)
definition setter F a m = register_apply F (λ_. a) m for F :: 'a update  'b update
definition getter F m = (THE x. setter F x m = m) for F :: 'a update  'b update

lemma
  assumes valid_getter_setter g s
  shows getter_of_register_from_getter_setter[simp]: getter (register_from_getter_setter g s) = g
    and setter_of_register_from_getter_setter[simp]: setter (register_from_getter_setter g s) = s
proof -
  define g' s' where g' = getter (register_from_getter_setter g s)
    and s' = setter (register_from_getter_setter g s)
  show s' = s
    by (auto intro!:ext simp: s'_def setter_def register_apply_def register_from_getter_setter_def)
  moreover show g' = g
  proof (rule ext, rename_tac m)
    fix m
    have g' m = (THE x. s x m = m)
      by (auto intro!:ext simp: g'_def s'_def[symmetric] s'=s getter_def register_apply_def register_from_getter_setter_def)
    moreover have s (g m) m = m
      by (metis assms valid_getter_setter_def)
    moreover have x = x' if s x m = m s x' m = m for x x'
      by (metis assms that(1) that(2) valid_getter_setter_def)
    ultimately show g' m = g m
      by (simp add: Uniq_def the1_equality')
  qed
qed

definition register :: ('a,'b) preregister  bool where
  register F  (g s. F = register_from_getter_setter g s  valid_getter_setter g s)

lemma register_of_id: register F  F Some = Some
  by (auto simp add: register_def valid_getter_setter_def register_from_getter_setter_def)

lemma register_id: register id
  unfolding register_def
  apply (rule exI[of _ id], rule exI[of _ λa m. a])
  by (auto intro!: ext simp: option.case_eq_if register_from_getter_setter_def valid_getter_setter_def)

lemma register_tensor_left: register (λa. tensor_update a Some)
  apply (auto simp: register_def)
  apply (rule exI[of _ fst])
  apply (rule exI[of _ λx' (x,y). (x',y)])
  by (auto intro!: ext simp add: tensor_update_def valid_getter_setter_def register_from_getter_setter_def option.case_eq_if)

lemma register_tensor_right: register (λa. tensor_update Some a)
  apply (auto simp: register_def)
  apply (rule exI[of _ snd])
  apply (rule exI[of _ λy' (x,y). (x,y')])
  by (auto intro!: ext simp add: tensor_update_def valid_getter_setter_def register_from_getter_setter_def option.case_eq_if)

lemma register_preregister: "preregister F" if register F
proof -
  from register F
  obtain s g where F: F a m = (case a (g m) of None  None | Some x  Some (s x m)) for a m
    unfolding register_from_getter_setter_def register_def by blast
  show ?thesis
    unfolding preregister_def
    apply (rule exI[of _ g])
    apply (rule exI[of _ λx m. Some (s x m)])
    using F by simp
qed

lemma register_comp: "register (G  F)" if register F and register G
  for F :: "('a,'b) preregister" and G :: "('b,'c) preregister"
proof -
  from register F
  obtain sF gF where F: F a m = (case a (gF m) of None  None | Some x  Some (sF x m))
    and validF: valid_getter_setter gF sF for a m
    unfolding register_def register_from_getter_setter_def by blast
  from register G
  obtain sG gG where G: G a m = (case a (gG m) of None  None | Some x  Some (sG x m))
    and validG: valid_getter_setter gG sG for a m
    unfolding register_def register_from_getter_setter_def by blast
  define s g where s a m = sG (sF a (gG m)) m and g m = gF (gG m) for a m
  have (G  F) a m = (case a (g m) of None  None | Some x  Some (s x m)) for a m
    by (auto simp add: option.case_eq_if F G s_def g_def)
  moreover have valid_getter_setter g s
    using validF validG by (auto simp: valid_getter_setter_def s_def g_def)
  ultimately show "register (G  F)"
    unfolding register_def register_from_getter_setter_def by blast
qed

lemma register_mult: "register F  F a m F b = F (a m b)"
  by (auto intro!: ext simp: register_def register_from_getter_setter_def[abs_def] valid_getter_setter_def map_comp_def option.case_eq_if)

definition register_pair ::
  ('a update  'c update)  ('b update  'c update)  (('a×'b) update  'c update) where
  register_pair F G =
    register_from_getter_setter (λm. (getter F m, getter G m)) (λ(a,b) m. setter F a (setter G b m))

lemma compatible_setter:
  assumes [simp]: register F register G
  assumes compat: a b. F a m G b = G b m F a
  shows setter F x o setter G y = setter G y o setter F x
  using compat apply (auto intro!: ext simp: setter_def register_apply_def o_def map_comp_def)
  by (smt (verit, best) assms(1) assms(2) option.case_eq_if option.distinct(1) register_def register_from_getter_setter_def)

lemma register_pair_apply:
  assumes [simp]: register F register G
  assumes a b. F a m G b = G b m F a
  shows (register_pair F G) (tensor_update a b) = F a m G b
proof -
  have validF: valid_getter_setter (getter F) (setter F) and validG: valid_getter_setter (getter G) (setter G)
    by (metis assms getter_of_register_from_getter_setter register_def setter_of_register_from_getter_setter)+
  then have F: F = register_from_getter_setter (getter F) (setter F) and G: G = register_from_getter_setter (getter G) (setter G)
    by (metis assms getter_of_register_from_getter_setter register_def setter_of_register_from_getter_setter)+
  have gFsG: getter F (setter G y m) = getter F m for y m
  proof -
    have getter F (setter G y m) = getter F (setter G y (setter F (getter F m) m))
      using validF by (metis valid_getter_setter_def)
    also have  = getter F (setter F (getter F m) (setter G y m))
      by (metis (mono_tags, lifting) assms(1) assms(2) assms(3) comp_eq_dest_lhs compatible_setter)
    also have  = getter F m
      by (metis validF valid_getter_setter_def)
    finally show ?thesis by -
  qed

  show ?thesis
    apply (subst (2) F, subst (2) G)
    by (auto intro!:ext simp: register_pair_def tensor_update_def map_comp_def option.case_eq_if
              register_from_getter_setter_def gFsG)
qed

lemma register_pair_is_register:
  fixes F :: 'a update  'c update and G
  assumes [simp]: register F and [simp]: register G
  assumes compat: a b. F a m G b = G b m F a
  shows register (register_pair F G)
proof -
  have validF: valid_getter_setter (getter F) (setter F) and validG: valid_getter_setter (getter G) (setter G)
    by (metis assms getter_of_register_from_getter_setter register_def setter_of_register_from_getter_setter)+
  then have valid_getter_setter (λm. (getter F m, getter G m)) (λ(a, b) m. setter F a (setter G b m))
    apply (simp add: valid_getter_setter_def)
    by (metis (mono_tags, lifting) assms comp_eq_dest_lhs compat compatible_setter)
  then show ?thesis
    by (auto simp: register_pair_def register_def)
qed

end