Theory Transport_Prototype
section ‹Transport via Equivalences on PERs (Prototype)›
theory Transport_Prototype
imports
Transport_Rel_If
ML_Unification.ML_Unification_HOL_Setup
ML_Unification.Unify_Resolve_Tactics
keywords "trp_term" :: thy_goal_defn
begin
paragraph ‹Summary›
text ‹We implement a simple Transport prototype. The prototype is restricted
to work with equivalences on partial equivalence relations.
It is also not forming the compositions of equivalences so far.
The support for dependent function relators is restricted to the form
described in
@{thm transport_Dep_Fun_Rel_no_dep_fun.partial_equivalence_rel_equivalenceI}:
The relations can be dependent, but the functions must be simple.
This is not production ready, but a proof of concept.
The package provides a command @{command trp_term}, which sets up the
required goals to prove a given term. See the examples in this directory for
some use cases and refer to \<^cite>‹"transport"› for more details.›
paragraph ‹Theorem Setups›
context transport
begin
lemma left_Galois_left_if_left_rel_if_partial_equivalence_rel_equivalence:
assumes "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
and "x ≤⇘L⇙ x'"
shows "x ⇘L⇙⪅ l x"
using assms by (intro left_Galois_left_if_left_rel_if_inflationary_on_in_fieldI)
(blast elim: preorder_equivalence_order_equivalenceE)+
definition "transport_per x y ≡ ((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r ∧ x ⇘L⇙⪅ y"
text ‹The choice of @{term "x'"} is arbitrary. All we need is @{term "in_dom (≤⇘L⇙) x"}.›
lemma transport_per_start:
assumes "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
and "x ≤⇘L⇙ x'"
shows "transport_per x (l x)"
using assms unfolding transport_per_def
by (blast intro: left_Galois_left_if_left_rel_if_partial_equivalence_rel_equivalence)
lemma left_Galois_if_transport_per:
assumes "transport_per x y"
shows "x ⇘L⇙⪅ y"
using assms unfolding transport_per_def by blast
end
context transport_Fun_Rel
begin
text ‹Simplification of Galois relator for simple function relator.›
corollary left_Galois_eq_Fun_Rel_left_Galois:
assumes "((≤⇘L1⇙) ≡⇘PER⇙ (≤⇘R1⇙)) l1 r1"
and "((≤⇘L2⇙) ≡⇘PER⇙ (≤⇘R2⇙)) l2 r2"
shows "(⇘L⇙⪅) = ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))"
proof (intro ext)
fix f g
show "f ⇘L⇙⪅ g ⟷ ((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅)) f g"
proof
assume "f ⇘L⇙⪅ g"
moreover have "g ≤⇘R⇙ g"
proof -
from assms have per: "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
by (intro partial_equivalence_rel_equivalenceI) auto
with ‹f ⇘L⇙⪅ g› show ?thesis by blast
qed
ultimately show "((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅)) f g" using assms
by (intro Fun_Rel_left_Galois_if_left_GaloisI)
(auto elim!: tdfrs.t1.partial_equivalence_rel_equivalenceE
tdfrs.t1.preorder_equivalence_galois_equivalenceE
tdfrs.t1.galois_equivalenceE
intro: reflexive_on_if_le_pred_if_reflexive_on in_field_if_in_dom)
next
assume "((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅)) f g"
with assms have "((⇘L1⇙⪅) ⇛ (⇘L2⇙⪅))↾⇘in_dom (≤⇘L⇙)⇙↿⇘in_codom (≤⇘R⇙)⇙ f g"
by (subst Fun_Rel_left_Galois_restrict_left_right_eq_Fun_Rel_left_GaloisI) blast+
with assms show "f ⇘L⇙⪅ g"
by (intro left_Galois_if_Fun_Rel_left_GaloisI) blast+
qed
qed
end
lemmas related_Fun_Rel_combI = Fun_Rel_relD[rotated]
lemma related_Fun_Rel_lambdaI:
assumes "⋀x y. R x y ⟹ S (f x) (g y)"
and "T = (R ⇛ S)"
shows "T f g"
using assms by blast
paragraph ‹General ML setups›
ML_file‹transport_util.ML›
paragraph ‹Unification Setup›
ML‹
@{functor_instance struct_name = Transport_Unification_Combine
and functor_name = Unification_Combine
and id = Transport_Util.transport_id}
›
local_setup ‹Transport_Unification_Combine.setup_attribute NONE›
ML‹
@{functor_instance struct_name = Transport_Mixed_Unification
and functor_name = Mixed_Unification
and id = Transport_Util.transport_id
and more_args = ‹structure UC = Transport_Unification_Combine›}
›
ML‹
structure A = Standard_Mixed_Unification
›
ML‹
@{functor_instance struct_name = Transport_Unification_Hints
and functor_name = Term_Index_Unification_Hints
and id = Transport_Util.transport_id
and more_args = ‹
structure TI = Discrimination_Tree
val init_args = {
concl_unifier = SOME (Higher_Order_Pattern_Unification.unify
|> Type_Unification.e_unify Unification_Util.unify_types),
prems_unifier = SOME (Transport_Mixed_Unification.first_higherp_decomp_comb_higher_unify
|> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif),
normalisers = SOME Transport_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify,
retrieval = SOME (Term_Index_Unification_Hints_Args.mk_sym_retrieval
TI.norm_term TI.unifiables),
hint_preprocessor = SOME (K I)
}›}
›
local_setup ‹Transport_Unification_Hints.setup_attribute NONE›
declare [[trp_uhint where hint_preprocessor = ‹Unification_Hints_Base.obj_logic_hint_preprocessor
@{thm atomize_eq[symmetric]} (Conv.rewr_conv @{thm eq_eq_True})›]]
declare [[trp_ucombine add = ‹Transport_Unification_Combine.eunif_data
(Transport_Unification_Hints.try_hints
|> Unification_Combinator.norm_unifier
(Unification_Util.inst_norm_term'
Transport_Mixed_Unification.norms_first_higherp_decomp_comb_higher_unify)
|> K)
(Transport_Unification_Combine.default_metadata Transport_Unification_Hints.binding)›]]
paragraph ‹Prototype›
ML_file‹transport.ML›
declare
transport_Dep_Fun_Rel.transport_defs[trp_def]
transport_Fun_Rel.transport_defs[trp_def]
declare
transport_Fun_Rel.partial_equivalence_rel_equivalenceI[rotated, per_intro]
transport_eq_id.partial_equivalence_rel_equivalenceI[per_intro]
transport_eq_restrict_id.partial_equivalence_rel_equivalence[per_intro]
declare
transport_id.left_Galois_eq_left[trp_relator_rewrite]
transport_Fun_Rel.left_Galois_eq_Fun_Rel_left_Galois[trp_relator_rewrite]
end