Theory Lift_FSet

(*  Title:      HOL/Quotient_Examples/Lift_FSet.thy
    Author:     Brian Huffman, TU Munich

section ‹Lifting and transfer with a finite set type›

theory Lift_FSet
imports Main

subsection ‹Equivalence relation and quotient type definition›

definition list_eq :: "'a list  'a list  bool"
  where [simp]: "list_eq xs ys  set xs = set ys"

lemma reflp_list_eq: "reflp list_eq"
  unfolding reflp_def by simp

lemma symp_list_eq: "symp list_eq"
  unfolding symp_def by simp

lemma transp_list_eq: "transp list_eq"
  unfolding transp_def by simp

lemma equivp_list_eq: "equivp list_eq"
  by (intro equivpI reflp_list_eq symp_list_eq transp_list_eq)

context includes lifting_syntax

lemma list_eq_transfer [transfer_rule]:
  assumes [transfer_rule]: "bi_unique A"
  shows "(list_all2 A ===> list_all2 A ===> (=)) list_eq list_eq"
  unfolding list_eq_def [abs_def] by transfer_prover

quotient_type 'a fset = "'a list" / "list_eq" parametric list_eq_transfer
  by (rule equivp_list_eq)

subsection ‹Lifted constant definitions›

lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric list.ctr_transfer(1) .

lift_definition fcons :: "'a  'a fset  'a fset" is Cons parametric list.ctr_transfer(2)
  by simp

lift_definition fappend :: "'a fset  'a fset  'a fset" is append parametric append_transfer
  by simp

lift_definition fmap :: "('a  'b)  'a fset  'b fset" is map parametric list.map_transfer
  by simp

lift_definition ffilter :: "('a  bool)  'a fset  'a fset" is filter parametric filter_transfer
  by simp

lift_definition fset :: "'a fset  'a set" is set parametric list.set_transfer
  by simp

text ‹Constants with nested types (like concat) yield a more
  complicated proof obligation.›

lemma list_all2_cr_fset:
  "list_all2 cr_fset xs ys  map abs_fset xs = ys"
  unfolding cr_fset_def
  apply safe
  apply (erule list_all2_induct, simp, simp)
  apply (simp add: list_all2_map2 List.list_all2_refl)

lemma abs_fset_eq_iff: "abs_fset xs = abs_fset ys  list_eq xs ys"
  using Quotient_rel [OF Quotient_fset] by simp

lift_definition fconcat :: "'a fset fset  'a fset" is concat parametric concat_transfer
proof (simp only: fset.pcr_cr_eq)
  fix xss yss :: "'a list list"
  assume "(list_all2 cr_fset OO list_eq OO (list_all2 cr_fset)¯¯) xss yss"
  then obtain uss vss where
    "list_all2 cr_fset xss uss" and "list_eq uss vss" and
    "list_all2 cr_fset yss vss" by clarsimp
  hence "list_eq (map abs_fset xss) (map abs_fset yss)"
    unfolding list_all2_cr_fset by simp
  thus "list_eq (concat xss) (concat yss)"
    apply (simp add: set_eq_iff image_def)
    apply safe
    apply (rename_tac xs, drule_tac x="abs_fset xs" in spec)
    apply (drule iffD1, fast, clarsimp simp add: abs_fset_eq_iff, fast)
    apply (rename_tac xs, drule_tac x="abs_fset xs" in spec)
    apply (drule iffD2, fast, clarsimp simp add: abs_fset_eq_iff, fast)

lemma member_transfer:
  assumes [transfer_rule]: "bi_unique A"
  shows "(A ===> list_all2 A ===> (=)) (λx xs. x  set xs) (λx xs. x  set xs)"
by transfer_prover


  "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")

  "{|x, xs|}" == "CONST fcons x {|xs|}"
  "{|x|}"     == "CONST fcons x {||}"

lift_definition fmember :: "'a  'a fset  bool" (infix "|∈|" 50) is "λx xs. x  set xs"
   parametric member_transfer by simp

abbreviation notin_fset :: "'a  'a fset  bool" (infix "|∉|" 50) where
  "x |∉| S  ¬ (x |∈| S)"

lemma fmember_fmap[simp]: "a |∈| fmap f X = (b. b |∈| X  a = f b)"
  by transfer auto

text ‹We can export code:›

export_code fnil fcons fappend fmap ffilter fset fmember in SML file_prefix fset

subsection ‹Using transfer with type fset›

text ‹The correspondence relation cr_fset› can only relate
  list› and fset› types with the same element type.
  To relate nested types like 'a list list› and
  'a fset fset›, we define a parameterized version of the
  correspondence relation, pcr_fset›.›

thm pcr_fset_def

subsection ‹Transfer examples›

text ‹The transfer› method replaces equality on fset› with the list_eq› relation on lists, which is
  logically equivalent.›

lemma "fmap f (fmap g xs) = fmap (f  g) xs"
  apply transfer
  apply simp

text ‹The transfer'› variant can replace equality on fset› with equality on list›, which is logically stronger
  but sometimes more convenient.›

lemma "fmap f (fmap g xs) = fmap (f  g) xs"
  using map_map [Transfer.transferred] .

lemma "ffilter p (fmap f xs) = fmap f (ffilter (p  f) xs)"
  using filter_map [Transfer.transferred] .

lemma "ffilter p (ffilter q xs) = ffilter (λx. q x  p x) xs"
  using filter_filter [Transfer.transferred] .

lemma "fset (fcons x xs) = insert x (fset xs)"
  using list.set(2) [Transfer.transferred] .

lemma "fset (fappend xs ys) = fset xs  fset ys"
  using set_append [Transfer.transferred] .

lemma "fset (fconcat xss) = (xsfset xss. fset xs)"
  using set_concat [Transfer.transferred] .

lemma "xfset xs. f x = g x  fmap f xs = fmap g xs"
  apply transfer
  apply (simp cong: map_cong del: set_map)

lemma "fnil = fconcat xss  (xsfset xss. xs = fnil)"
  apply transfer
  apply simp

lemma "fconcat (fmap (λx. fcons x fnil) xs) = xs"
  apply transfer
  apply simp

lemma concat_map_concat: "concat (map concat xsss) = concat (concat xsss)"
  by (induct xsss, simp_all)

lemma "fconcat (fmap fconcat xss) = fconcat (fconcat xss)"
  using concat_map_concat [Transfer.transferred] .