Theory Transport_Lists_Sets_Examples

✐‹creator "Kevin Kappelmann"›
section ‹Example Transports Between Lists and Sets›
theory Transport_Lists_Sets_Examples
  imports
    Transport_Prototype
    Transport_Syntax
    "HOL-Library.FSet"
begin

paragraph ‹Summary›
text ‹Introductory examples from \<^cite>‹"transport"›.
Transports between lists and (finite) sets. Refer to the paper for more details.›

context
  includes galois_rel_syntax and transport_syntax
begin

paragraph ‹Introductory examples from paper›

text ‹Left and right relations.›

definition "LFSL xs xs' ≡ fset_of_list xs = fset_of_list xs'"
abbreviation (input) "(LFSR :: 'a fset ⇒ _) ≡ (=)"
definition "LSL xs xs' ≡ set xs = set xs'"
abbreviation (input) "(LSR :: 'a set ⇒ _) ≡ (=⇘finite :: 'a set ⇒ bool⇙)"

interpretation t : transport LSL R l r for LSL R l r .

text ‹Proofs of equivalences.›

lemma list_fset_PER [per_intro]: "(LFSL ≡⇘PER⇙ LFSR) fset_of_list sorted_list_of_fset"
  unfolding LFSL_def by fastforce

lemma list_set_PER [per_intro]: "(LSL ≡⇘PER⇙ LSR) set sorted_list_of_set"
  unfolding LSL_def by fastforce

text ‹We can rewrite the Galois relators in the following theorems to the relator of the paper.›

definition "LFS xs s ≡ fset_of_list xs = s"
definition "LS xs s ≡ set xs = s"

lemma LFSL_Galois_eq_LFS: "(⇘LFSL⇙⪅⇘LFSR sorted_list_of_fset⇙) ≡ LFS"
  unfolding LFS_def LFSL_def by (intro eq_reflection ext) (auto)
lemma LFSR_Galois_eq_inv_LFS: "(⇘LFSR⇙⪅⇘LFSL fset_of_list⇙) ≡ LFS¯"
  unfolding LFS_def LFSL_def by (intro eq_reflection ext) (auto)
lemma LSL_Galois_eq_LS: "(⇘LSL⇙⪅⇘LSR sorted_list_of_set⇙) ≡ LS"
  unfolding LS_def LSL_def by (intro eq_reflection ext) (auto)

declare LFSL_Galois_eq_LFS[trp_relator_rewrite, trp_uhint]
  LFSR_Galois_eq_inv_LFS[trp_relator_rewrite, trp_uhint]
  LSL_Galois_eq_LS[trp_relator_rewrite, trp_uhint]

definition "max_list xs ≡ foldr max xs (0 :: nat)"

text ‹Proof of parametricity for @{term max_list}.›

lemma max_max_list_removeAll_eq_maxlist:
  assumes "x ∈ set xs"
  shows "max x (max_list (removeAll x xs)) = max_list xs"
  unfolding max_list_def using assms by (induction xs)
  (simp_all, (metis max.left_idem removeAll_id max.left_commute)+)

lemma max_list_parametric [trp_in_dom]: "(LSL ⇛ (=)) max_list max_list"
proof (intro Fun_Rel_relI)
  fix xs xs' :: "nat list" assume "LSL xs xs'"
  then have "finite (set xs)" "set xs = set xs'" unfolding LSL_def by auto
  then show "max_list xs = max_list xs'"
  proof (induction "set xs"  arbitrary: xs xs' rule: finite_induct)
    case (insert x F)
    then have "F = set (removeAll x xs)" by auto
    moreover from insert have "... = set (removeAll x xs')" by auto
    ultimately have "max_list (removeAll x xs) = max_list (removeAll x xs')"
      (is "?lhs = ?rhs") using insert by blast
    then have "max x ?lhs = max x ?rhs" by simp
    then show ?case
      using insert max_max_list_removeAll_eq_maxlist insertI1 by metis
  qed auto
qed

lemma LFSL_eq_LSL: "LFSL ≡ LSL"
  unfolding LFSL_def LSL_def by (intro eq_reflection ext) (auto simp: fset_of_list_elem)

lemma max_list_parametricfin [trp_in_dom]: "(LFSL ⇛ (=)) max_list max_list"
  using max_list_parametric by (simp only: LFSL_eq_LSL)

text ‹Transport from lists to finite sets.›

trp_term max_fset :: "nat fset ⇒ nat" where x = max_list
  and L = "(LFSL ⇛ (=))"
  by trp_prover

text ‹Use @{command print_theorems} to show all theorems. Here's the correctness theorem:›
lemma "(LFS ⇛ (=)) max_list max_fset" by (trp_hints_resolve max_fset_related')

lemma [trp_in_dom]: "(LFSR ⇛ (=)) max_fset max_fset" by simp

text ‹Transport from lists to sets.›

trp_term max_set :: "nat set ⇒ nat" where x = max_list
  by trp_prover

lemma "(LS ⇛ (=)) max_list max_set" by (trp_hints_resolve max_set_related')

text ‹The registration of symmetric equivalence rules is not done by default as of now,
but that would not be a problem in principle.›

lemma list_fset_PER_sym [per_intro]:
  "(LFSR ≡⇘PER⇙ LFSL) sorted_list_of_fset fset_of_list"
  by (subst transport.partial_equivalence_rel_equivalence_right_left_iff_partial_equivalence_rel_equivalence_left_right)
  (fact list_fset_PER)

text ‹Transport from finite sets to lists.›

trp_term max_list' :: "nat list ⇒ nat" where x = max_fset
  by trp_prover

lemma "(LFS¯ ⇛ (=)) max_fset max_list'" by (trp_hints_resolve max_list'_related')

text ‹Transporting higher-order functions.›

lemma map_parametric [trp_in_dom]:
  "(((=) ⇛ (=)) ⇛ LSL ⇛ LSL) map map"
  unfolding LSL_def by (intro Fun_Rel_relI) simp

lemma [trp_uhint]: "P ≡ (=) ⟹ P ≡ (=) ⇛ (=)" by simp
lemma [trp_uhint]: "P ≡ ⊤ ⟹ (=⇘P :: 'a ⇒ bool⇙) ≡ ((=) :: 'a ⇒ _)" by simp

(*sorted_list_of_fset requires a linorder, but in theory,
we could use a different transport function to avoid that constraint*)
trp_term map_set :: "('a :: linorder ⇒ 'b) ⇒ 'a set ⇒ ('b :: linorder) set"
  where x = "map :: ('a :: linorder ⇒ 'b) ⇒ 'a list ⇒ ('b :: linorder) list"
  by trp_prover

lemma "(((=) ⇛ (=)) ⇛ LS ⇛ LS) map map_set" by (trp_hints_resolve map_set_related')


lemma filter_parametric [trp_in_dom]:
  "(((=) ⇛ (⟷)) ⇛ LSL ⇛ LSL) filter filter"
  unfolding LSL_def by (intro Fun_Rel_relI) simp

trp_term filter_set :: "('a :: linorder ⇒ bool) ⇒ 'a set ⇒ 'a set"
  where x = "filter :: ('a :: linorder ⇒ bool) ⇒ 'a list ⇒ 'a list"
  by trp_prover

lemma "(((=) ⇛ (=)) ⇛ LS ⇛ LS) filter filter_set" by (trp_hints_resolve filter_set_related')

lemma append_parametric [trp_in_dom]:
  "(LSL ⇛ LSL ⇛ LSL) append append"
  unfolding LSL_def by (intro Fun_Rel_relI) simp

trp_term append_set :: "('a :: linorder) set ⇒ 'a set ⇒ 'a set"
  where x = "append :: ('a :: linorder) list ⇒ 'a list ⇒ 'a list"
  by trp_prover

lemma "(LS ⇛ LS ⇛ LS) append append_set" by (trp_hints_resolve append_set_related')

text ‹The prototype also provides a simplified definition.›
lemma "append_set s s' ≡ set (sorted_list_of_set s) ∪ set (sorted_list_of_set s')"
  by (fact append_set_app_eq)

lemma "finite s ⟹ finite s' ⟹ append_set s s' = s ∪ s'"
  by (auto simp: append_set_app_eq)

end


end