Quelle Lift_FSet.thy Sprache: Isabelle

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

section \<open>Lifting and transfer with a finite set type\<close>

theory Lift_FSet
imports Main
begin

subsection \<open>Equivalence relation and quotient type definition\<close>

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
begin

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 \<open>Lifted constant definitions\<close>

lift_definition fnil :: "'a fset" (\<open>{||}\<close>) 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 \<open>Constants with nested types (like concat) yield a more
  complicated proof obligation.\<close>

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)
  done

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)
    done
qed

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

end

syntax
  "_fset" :: "args => 'a fset"  (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
syntax_consts
  "_fset" == fcons
translations
  "{|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 \<open>We can export code:\<close>

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

subsection \<open>Using transfer with type \<open>fset\<close>\<close>

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

thm pcr_fset_def

subsection \<open>Transfer examples\<close>

text \<open>The \<open>transfer\<close> method replaces equality on \<open>fset\<close> with the \<open>list_eq\<close> relation on lists, which is
  logically equivalent.\<close>

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

text \<open>The \<open>transfer'\<close> variant can replace equality on \<open>fset\<close> with equality on \<open>list\<close>, which is logically stronger
  but sometimes more convenient.\<close>

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) = (\xs\fset xss. fset xs)"
  using set_concat [Transfer.transferred] .

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

lemma "fnil = fconcat xss \ (\xs\fset xss. xs = fnil)"
  apply transfer
  apply simp
  done

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

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] .

end

quality99%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.