Theory Transport_Dep_Fun_Rel_Examples

✐‹creator "Kevin Kappelmann"›
section ‹Example Transports for Dependent Function Relator›
theory Transport_Dep_Fun_Rel_Examples
  imports
    Transport_Prototype
    Galois_Relator_Syntax
    HOL_Alignment_Binary_Relations
    "HOL-Library.IArray"
begin

unbundle no HOL_ascii_syntax

paragraph ‹Summary›
text ‹Dependent function relator examples from \<^cite>‹"transport"›.
Refer to the paper for more details.›
context
  includes galois_rel_Galois_syntax and transport_equivalences_syntax
  notes
    transport_rel_if.partial_equivalence_rel_equivalence_if_iff_if_partial_equivalence_rel_equivalence
      [rotated, per_intro]
    transport_Dep_Fun_Rel_no_dep_fun.partial_equivalence_rel_equivalenceI
      [ML_Krattr ‹Drule.rearrange_prems [1] #> Drule.rearrange_prems [2]›, per_intro]
begin

interpretation transport L R l r for L R l r .

abbreviation "Zpos ≡ ((=⇘(≤)(0 :: int)⇙) :: int ⇒ _)"

lemma Zpos_per [per_intro]: "(Zpos ≡⇘PER⇙ (=)) nat int"
  by fastforce

lemma sub_parametric [trp_in_dom]:
  "((i _ ∷ Zpos) ⇛ (j _ ∷ Zpos | j ≤ i) ⇛ Zpos) (-) (-)"
  by fastforce

trp_term nat_sub :: "nat ⇒ nat ⇒ nat" where x = "(-) :: int ⇒ _"
  and L = "(i _ ∷ Zpos) ⇛ (j _ ∷ Zpos | j ≤ i) ⇛ Zpos"
  and R = "(n _ ∷ (=)) ⇛ (m _ ∷ (=) | m ≤ n) ⇛ (=)"
  (*fastforce discharges the remaining side-conditions*)
  by trp_prover (fastforce intro: transport_Dep_Fun_Rel.mono_cond_intros)+

thm nat_sub_app_eq
text ‹Note: as of now, @{command trp_term} does not rewrite the
Galois relator of dependent function relators.›
thm nat_sub_related'

abbreviation "LRel ≡ list_all2"
abbreviation "IARel ≡ rel_iarray"

lemma [per_intro]:
  assumes "partial_equivalence_rel R"
  shows "(LRel R ≡⇘PER⇙ IARel R) IArray.IArray IArray.list_of"
  using assms by (fastforce simp flip: transp_eq_transitive symp_eq_symmetric
    intro: list.rel_transp list.rel_symp iarray.rel_transp iarray.rel_symp
    elim: iarray.rel_cases)+

lemma [trp_in_dom]:
  "((xs _ ∷ LRel R) ⇛ (i _ ∷ (=) | i < length xs) ⇛ R) (!) (!)"
  by (fastforce simp: list_all2_lengthD list_all2_nthD2)

context
  fixes R :: "'a ⇒ 'a ⇒ bool" assumes [per_intro]: "partial_equivalence_rel R"
begin

interpretation Rper : transport_partial_equivalence_rel_id R
  by unfold_locales per_prover

declare Rper.partial_equivalence_rel_equivalence [per_intro]

trp_term iarray_index where x = "(!) :: 'a list ⇒ _"
  and L = "((xs _ ∷ LRel R) ⇛ (i _ ∷ (=) | i < length xs) ⇛ R)"
  and R = "((xs _ ∷ IARel R) ⇛ (i _ ∷ (=) | i < IArray.length xs) ⇛ R)"
  by trp_prover
  (*fastforce discharges the remaining side-conditions*)
  (fastforce simp: list_all2_lengthD elim: iarray.rel_cases
    intro: transport_Dep_Fun_Rel.mono_cond_intros)+
end
end

end