Theory Transport_Typedef

✐‹creator "Kevin Kappelmann"›
theory Transport_Typedef
  imports
    "HOL-Library.FSet"
    Transport_Typedef_Base
    Transport_Prototype
    Transport_Syntax
    HOL_Alignment_Functions
begin

context
  includes galois_rel_syntax transport_syntax
begin

typedef pint = "{i :: int. 0 ≤ i}" by auto

interpretation typedef_pint : type_definition Rep_pint Abs_pint "{i :: int. 0 ≤ i}"
  by (fact type_definition_pint)

lemma [trp_relator_rewrite, trp_uhint]:
  "(⇘(=⇘Collect ((≤) (0 :: int))⇙)⇙⪅⇘(=) Rep_pint⇙) ≡ typedef_pint.AR"
  using typedef_pint.left_Galois_eq_AR by (intro eq_reflection) simp

typedef 'a fset = "{s :: 'a set. finite s}" by auto

interpretation typedef_fset :
  type_definition Rep_fset Abs_fset "{s :: 'a set. finite s}"
  by (fact type_definition_fset)

lemma [trp_relator_rewrite, trp_uhint]:
  "(⇘(=⇘{s :: 'a set. finite s}⇙) :: 'a set ⇒ _⇙⪅⇘(=) Rep_fset⇙) ≡ typedef_fset.AR"
  using typedef_fset.left_Galois_eq_AR by (intro eq_reflection) simp

lemma eq_restrict_set_eq_eq_uhint [trp_uhint]:
  "(⋀x. P x ≡ x ∈ A) ⟹ ((=⇘A :: 'a set⇙) :: 'a ⇒ _) ≡ (=⇘P⇙)"
  by (intro eq_reflection) (auto simp: fun_eq_iff)

(*could also automatically be tagged for every instance of type_definition*)
declare
  typedef_pint.partial_equivalence_rel_equivalence[per_intro]
  typedef_fset.partial_equivalence_rel_equivalence[per_intro]


lemma one_parametric [trp_in_dom]: "typedef_pint.L 1 1" by auto

trp_term pint_one :: "pint" where x = "1 :: int"
  by trp_prover

lemma add_parametric [trp_in_dom]:
  "(typedef_pint.L ⇛ typedef_pint.L ⇛ typedef_pint.L) (+) (+)"
  by (intro Fun_Rel_relI) fastforce

trp_term pint_add :: "pint ⇒ pint ⇒ pint"
  where x = "(+) :: int ⇒ _"
  by trp_prover

lemma empty_parametric [trp_in_dom]: "typedef_fset.L {} {}"
  by auto

trp_term fempty :: "'a fset" where x = "{} :: 'a set"
  by trp_prover


lemma insert_parametric [trp_in_dom]:
  "((=) ⇛ typedef_fset.L ⇛ typedef_fset.L) insert insert"
  by auto

trp_term finsert :: "'a ⇒ 'a fset ⇒ 'a fset" where x = insert
  and L = "((=) ⇛ typedef_fset.L ⇛ typedef_fset.L)"
  and R = "((=) ⇛ typedef_fset.R ⇛ typedef_fset.R)"
  by trp_prover


(*experiments with white-box transports*)

context
  notes refl[trp_related_intro]
begin

trp_term insert_add_int_fset_whitebox :: "int fset"
  where x = "insert (1 + (1 :: int)) {}" !
  by trp_whitebox_prover

lemma empty_parametric' [trp_related_intro]: "(rel_set R) {} {}"
  by (intro Dep_Fun_Rel_relI rel_setI) (auto dest: rel_setD1 rel_setD2)

lemma insert_parametric' [trp_related_intro]:
  "(R ⇛ rel_set R ⇛ rel_set R) insert insert"
  by (intro Fun_Rel_relI rel_setI) (auto dest: rel_setD1 rel_setD2)

context
  assumes [trp_uhint]:
  (*proven for all natural functors*)
  "L ≡ rel_set (L1 :: int ⇒ int ⇒ bool) ⟹ R ≡ rel_set (R1 :: pint ⇒ pint ⇒ bool)
  ⟹ r ≡ image r1 ⟹ S ≡ (⇘L1⇙⪅⇘R1 r1⇙) ⟹ (⇘L⇙⪅⇘R r⇙) ≡ rel_set S"
begin

trp_term insert_add_pint_set_whitebox :: "pint set"
  where x = "insert (1 + (1 :: int)) {}" !
  by trp_whitebox_prover

print_statement insert_add_int_fset_whitebox_def insert_add_pint_set_whitebox_def

end
end

lemma image_parametric [trp_in_dom]:
  "(((=) ⇛ (=)) ⇛ typedef_fset.L ⇛ typedef_fset.L) image image"
  by (intro Fun_Rel_relI) auto

trp_term fimage :: "('a ⇒ 'b) ⇒ 'a fset ⇒ 'b fset" where x = image
  by trp_prover

(*experiments with compositions*)

lemma image_parametric' [trp_related_intro]:
  "((R ⇛ S) ⇛ rel_set R ⇛ rel_set S) image image"
  using transfer_raw[simplified HOL_fun_alignment Transfer.Rel_def]
  by simp

lemma Galois_id_hint [trp_uhint]:
  "(L :: 'a ⇒ 'a ⇒ bool) ≡ R ⟹ r ≡ id ⟹ E ≡ L ⟹ (⇘L⇙⪅⇘R r⇙) ≡ E"
  by (simp only: eq_reflection[OF transport_id.left_Galois_eq_left])

lemma Freq [trp_uhint]: "L ≡ (=) ⇛ (=) ⟹ L ≡ (=)"
  by auto

context
  fixes L1 R1 l1 r1 L R l r
  assumes per1: "(L1 ≡⇘PER⇙ R1) l1 r1"
  defines "L ≡ rel_set L1" and "R ≡ rel_set R1"
  and "l ≡ image l1" and "r ≡ image r1"
begin

interpretation transport L R l r .

context
  (*proven for all natural functors*)
  assumes transport_per_set: "((≤⇘L⇙) ≡⇘PER⇙ (≤⇘R⇙)) l r"
  and compat: "transport_comp.middle_compatible_codom R typedef_fset.L"
begin

trp_term fempty_param :: "'b fset"
  where x = "{} :: 'a set"
  and L = "transport_comp.L ?L1 ?R1 (?l1 :: 'a set ⇒ 'b set) ?r1 typedef_fset.L"
  and R = "transport_comp.L typedef_fset.R typedef_fset.L ?r2 ?l2 ?R1"
  apply (rule transport_comp.partial_equivalence_rel_equivalenceI)
    apply (rule transport_per_set)
    apply per_prover
    apply (fact compat)
  apply (rule transport_comp.left_relI[where ?y="{}" and ?y'="{}"])
  apply (unfold L_def R_def l_def r_def)
  apply (auto intro!: galois_rel.left_GaloisI in_codomI empty_transfer)
  done

definition "set_succ ≡ image ((+) (1 :: int))"

lemma set_succ_parametric [trp_in_dom]:
  "(typedef_fset.L ⇛ typedef_fset.L) set_succ set_succ"
  unfolding set_succ_def by auto

trp_term fset_succ :: "int fset ⇒ int fset"
  where x = set_succ
  and L = "typedef_fset.L ⇛ typedef_fset.L"
  and R = "typedef_fset.R ⇛ typedef_fset.R"
  by trp_prover

trp_term fset_succ' :: "int fset ⇒ int fset"
  where x = set_succ
  and L = "typedef_fset.L ⇛ typedef_fset.L"
  and R = "typedef_fset.R ⇛ typedef_fset.R"
  unfold set_succ_def !
  (*current prototype gets lost in this example*)
  using refl[trp_related_intro]
  apply (tactic ‹Transport.instantiate_skeleton_tac @{context} 1›)
  apply (tactic ‹Transport.transport_related_step_tac @{context} 1›)
  apply (tactic ‹Transport.transport_related_step_tac @{context} 1›)
  apply (tactic ‹Transport.transport_related_step_tac @{context} 1›)
  apply (tactic ‹Transport.transport_related_step_tac @{context} 1›)
  apply (tactic ‹Transport.transport_related_step_tac @{context} 1›)
  apply (tactic ‹Transport.transport_related_step_tac @{context} 1›)
  apply assumption
  apply assumption
  prefer 3
  apply (tactic ‹Transport.transport_related_step_tac @{context} 1›)
  apply (tactic ‹Transport.transport_related_step_tac @{context} 1›)
  apply (fold trp_def)
  apply (trp_relator_rewrite)+
  apply (unfold trp_def)
  apply (trp_hints_resolve refl)
  done

lemma pint_middle_compat:
  "transport_comp.middle_compatible_codom (rel_set ((=) :: pint ⇒ _))
  (=⇘Collect (finite :: pint set ⇒ _)⇙)"
  by (intro transport_comp.middle_compatible_codom_if_right1_le_eqI)
  (auto simp: rel_set_eq intro!: transitiveI)

trp_term pint_fset_succ :: "pint fset ⇒ pint fset"
  where x = "set_succ :: int set ⇒ int set"
  (*automation for composition not supported as of now*)
  oops

end
end
end

end