src/HOL/Quotient_Examples/Lift_FSet.thy
 author haftmann Sun Oct 08 22:28:22 2017 +0200 (23 months ago) changeset 66816 212a3334e7da parent 63343 fb5d8a50c641 child 67399 eab6ce8368fa permissions -rw-r--r--
more fundamental definition of div and mod on int
```     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
```