Theory Axioms_Classical
section ‹Classical instantiation of registers›
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 aux1: ‹(case (if a then b else c) of Some x ⇒ f x | None ⇒ g) =
(if a then (case b of Some x ⇒ f x | None ⇒ g) else (case c of Some x ⇒ f x | None ⇒ g))› for a b c f g
by simp
have aux2: ‹F (λm. if m = x then Some y else None) z = G (λm. if m = x then Some y else None) z›
if ‹F (λm. if fst m = fst x then if snd m = snd x then Some y else None else None) =
G (λm. if fst m = fst x then if snd m = snd x then Some y else None else None)› for x y z
using assms that
by (smt (z3) preregister_def prod.collapse)
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)›]
by (auto intro!:ext simp: tensor_update_def[abs_def] update1_def[abs_def] aux1 aux2
cong: if_cong)
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)›
by (auto simp: register_def intro!: exI[of _ fst] exI[of _ ‹λx' (x,y). (x',y)›]
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)›
by (auto simp: register_def intro!: exI[of _ snd] exI[of _ ‹λy' (x,y). (x,y')›]
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›
proof -
have *: ‹F (λxa. Some x) (the (G (λx. Some y) xa)) = G (λx. Some y) (the (F (λxa. Some x) xa))›
if ‹⋀a b. (λk. case G b k of None ⇒ None | Some v ⇒ F a v) =
(λk. case F a k of None ⇒ None | Some v ⇒ G b v)› for xa
using that assms by (smt (verit, best) option.case_eq_if option.distinct(1) register_def register_from_getter_setter_def)
then show ?thesis
using compat by (auto intro!: ext simp: setter_def register_apply_def o_def map_comp_def)
qed
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