src/HOL/Quotient_Examples/Lift_FSet.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 63167 0909deb8059b
child 67399 eab6ce8368fa
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title:      HOL/Quotient_Examples/Lift_FSet.thy
     2     Author:     Brian Huffman, TU Munich
     3 *)
     4 
     5 section \<open>Lifting and transfer with a finite set type\<close>
     6 
     7 theory Lift_FSet
     8 imports Main
     9 begin
    10 
    11 subsection \<open>Equivalence relation and quotient type definition\<close>
    12 
    13 definition list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    14   where [simp]: "list_eq xs ys \<longleftrightarrow> set xs = set ys"
    15 
    16 lemma reflp_list_eq: "reflp list_eq"
    17   unfolding reflp_def by simp
    18 
    19 lemma symp_list_eq: "symp list_eq"
    20   unfolding symp_def by simp
    21 
    22 lemma transp_list_eq: "transp list_eq"
    23   unfolding transp_def by simp
    24 
    25 lemma equivp_list_eq: "equivp list_eq"
    26   by (intro equivpI reflp_list_eq symp_list_eq transp_list_eq)
    27 
    28 context includes lifting_syntax
    29 begin
    30 
    31 lemma list_eq_transfer [transfer_rule]:
    32   assumes [transfer_rule]: "bi_unique A"
    33   shows "(list_all2 A ===> list_all2 A ===> op =) list_eq list_eq"
    34   unfolding list_eq_def [abs_def] by transfer_prover
    35 
    36 quotient_type 'a fset = "'a list" / "list_eq" parametric list_eq_transfer
    37   by (rule equivp_list_eq)
    38 
    39 subsection \<open>Lifted constant definitions\<close>
    40 
    41 lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric list.ctr_transfer(1) .
    42 
    43 lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons parametric list.ctr_transfer(2)
    44   by simp
    45 
    46 lift_definition fappend :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is append parametric append_transfer
    47   by simp
    48 
    49 lift_definition fmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is map parametric list.map_transfer
    50   by simp
    51 
    52 lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is filter parametric filter_transfer
    53   by simp
    54 
    55 lift_definition fset :: "'a fset \<Rightarrow> 'a set" is set parametric list.set_transfer
    56   by simp
    57 
    58 text \<open>Constants with nested types (like concat) yield a more
    59   complicated proof obligation.\<close>
    60 
    61 lemma list_all2_cr_fset:
    62   "list_all2 cr_fset xs ys \<longleftrightarrow> map abs_fset xs = ys"
    63   unfolding cr_fset_def
    64   apply safe
    65   apply (erule list_all2_induct, simp, simp)
    66   apply (simp add: list_all2_map2 List.list_all2_refl)
    67   done
    68 
    69 lemma abs_fset_eq_iff: "abs_fset xs = abs_fset ys \<longleftrightarrow> list_eq xs ys"
    70   using Quotient_rel [OF Quotient_fset] by simp
    71 
    72 lift_definition fconcat :: "'a fset fset \<Rightarrow> 'a fset" is concat parametric concat_transfer
    73 proof (simp only: fset.pcr_cr_eq)
    74   fix xss yss :: "'a list list"
    75   assume "(list_all2 cr_fset OO list_eq OO (list_all2 cr_fset)\<inverse>\<inverse>) xss yss"
    76   then obtain uss vss where
    77     "list_all2 cr_fset xss uss" and "list_eq uss vss" and
    78     "list_all2 cr_fset yss vss" by clarsimp
    79   hence "list_eq (map abs_fset xss) (map abs_fset yss)"
    80     unfolding list_all2_cr_fset by simp
    81   thus "list_eq (concat xss) (concat yss)"
    82     apply (simp add: set_eq_iff image_def)
    83     apply safe
    84     apply (rename_tac xs, drule_tac x="abs_fset xs" in spec)
    85     apply (drule iffD1, fast, clarsimp simp add: abs_fset_eq_iff, fast)
    86     apply (rename_tac xs, drule_tac x="abs_fset xs" in spec)
    87     apply (drule iffD2, fast, clarsimp simp add: abs_fset_eq_iff, fast)
    88     done
    89 qed
    90 
    91 lemma member_transfer:
    92   assumes [transfer_rule]: "bi_unique A"
    93   shows "(A ===> list_all2 A ===> op=) (\<lambda>x xs. x \<in> set xs) (\<lambda>x xs. x \<in> set xs)"
    94 by transfer_prover
    95 
    96 end
    97 
    98 syntax
    99   "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
   100 
   101 translations
   102   "{|x, xs|}" == "CONST fcons x {|xs|}"
   103   "{|x|}"     == "CONST fcons x {||}"
   104 
   105 lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is "\<lambda>x xs. x \<in> set xs"
   106    parametric member_transfer by simp
   107 
   108 abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
   109   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
   110 
   111 lemma fmember_fmap[simp]: "a |\<in>| fmap f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
   112   by transfer auto
   113 
   114 text \<open>We can export code:\<close>
   115 
   116 export_code fnil fcons fappend fmap ffilter fset fmember in SML
   117 
   118 subsection \<open>Using transfer with type \<open>fset\<close>\<close>
   119 
   120 text \<open>The correspondence relation \<open>cr_fset\<close> can only relate
   121   \<open>list\<close> and \<open>fset\<close> types with the same element type.
   122   To relate nested types like \<open>'a list list\<close> and
   123   \<open>'a fset fset\<close>, we define a parameterized version of the
   124   correspondence relation, \<open>pcr_fset\<close>.\<close>
   125 
   126 thm pcr_fset_def
   127 
   128 subsection \<open>Transfer examples\<close>
   129 
   130 text \<open>The \<open>transfer\<close> method replaces equality on \<open>fset\<close> with the \<open>list_eq\<close> relation on lists, which is
   131   logically equivalent.\<close>
   132 
   133 lemma "fmap f (fmap g xs) = fmap (f \<circ> g) xs"
   134   apply transfer
   135   apply simp
   136   done
   137 
   138 text \<open>The \<open>transfer'\<close> variant can replace equality on \<open>fset\<close> with equality on \<open>list\<close>, which is logically stronger
   139   but sometimes more convenient.\<close>
   140 
   141 lemma "fmap f (fmap g xs) = fmap (f \<circ> g) xs"
   142   using map_map [Transfer.transferred] .
   143 
   144 lemma "ffilter p (fmap f xs) = fmap f (ffilter (p \<circ> f) xs)"
   145   using filter_map [Transfer.transferred] .
   146 
   147 lemma "ffilter p (ffilter q xs) = ffilter (\<lambda>x. q x \<and> p x) xs"
   148   using filter_filter [Transfer.transferred] .
   149 
   150 lemma "fset (fcons x xs) = insert x (fset xs)"
   151   using list.set(2) [Transfer.transferred] .
   152 
   153 lemma "fset (fappend xs ys) = fset xs \<union> fset ys"
   154   using set_append [Transfer.transferred] .
   155 
   156 lemma "fset (fconcat xss) = (\<Union>xs\<in>fset xss. fset xs)"
   157   using set_concat [Transfer.transferred] .
   158 
   159 lemma "\<forall>x\<in>fset xs. f x = g x \<Longrightarrow> fmap f xs = fmap g xs"
   160   apply transfer
   161   apply (simp cong: map_cong del: set_map)
   162   done
   163 
   164 lemma "fnil = fconcat xss \<longleftrightarrow> (\<forall>xs\<in>fset xss. xs = fnil)"
   165   apply transfer
   166   apply simp
   167   done
   168 
   169 lemma "fconcat (fmap (\<lambda>x. fcons x fnil) xs) = xs"
   170   apply transfer
   171   apply simp
   172   done
   173 
   174 lemma concat_map_concat: "concat (map concat xsss) = concat (concat xsss)"
   175   by (induct xsss, simp_all)
   176 
   177 lemma "fconcat (fmap fconcat xss) = fconcat (fconcat xss)"
   178   using concat_map_concat [Transfer.transferred] .
   179 
   180 end