new example theory for quotient/transfer
authorhuffman
Sun Apr 22 11:05:04 2012 +0200 (2012-04-22)
changeset 476607a5c681c0265
parent 47659 e3c4d1b0b351
child 47661 012a887997f3
child 47667 b4f71d8aecd6
new example theory for quotient/transfer
src/HOL/IsaMakefile
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Set.thy
src/HOL/Quotient_Examples/Lift_FSet.thy
src/HOL/Quotient_Examples/ROOT.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/IsaMakefile	Sat Apr 21 21:38:08 2012 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Sun Apr 22 11:05:04 2012 +0200
     1.3 @@ -1509,6 +1509,7 @@
     1.4    Quotient_Examples/DList.thy \
     1.5    Quotient_Examples/FSet.thy \
     1.6    Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
     1.7 +  Quotient_Examples/Lift_FSet.thy \
     1.8    Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \
     1.9    Quotient_Examples/Lift_Fun.thy Quotient_Examples/Lift_DList.thy
    1.10  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
     2.1 --- a/src/HOL/Library/Quotient_List.thy	Sat Apr 21 21:38:08 2012 +0200
     2.2 +++ b/src/HOL/Library/Quotient_List.thy	Sun Apr 22 11:05:04 2012 +0200
     2.3 @@ -22,6 +22,21 @@
     2.4      by (induct xs ys rule: list_induct2') simp_all
     2.5  qed
     2.6  
     2.7 +lemma list_all2_OO: "list_all2 (A OO B) = list_all2 A OO list_all2 B"
     2.8 +proof (intro ext iffI)
     2.9 +  fix xs ys
    2.10 +  assume "list_all2 (A OO B) xs ys"
    2.11 +  thus "(list_all2 A OO list_all2 B) xs ys"
    2.12 +    unfolding OO_def
    2.13 +    by (induct, simp, simp add: list_all2_Cons1 list_all2_Cons2, fast)
    2.14 +next
    2.15 +  fix xs ys
    2.16 +  assume "(list_all2 A OO list_all2 B) xs ys"
    2.17 +  then obtain zs where "list_all2 A xs zs" and "list_all2 B zs ys" ..
    2.18 +  thus "list_all2 (A OO B) xs ys"
    2.19 +    by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
    2.20 +qed
    2.21 +
    2.22  lemma list_reflp:
    2.23    assumes "reflp R"
    2.24    shows "reflp (list_all2 R)"
     3.1 --- a/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 21:38:08 2012 +0200
     3.2 +++ b/src/HOL/Library/Quotient_Set.thy	Sun Apr 22 11:05:04 2012 +0200
     3.3 @@ -91,6 +91,10 @@
     3.4    "((A ===> B) ===> set_rel A ===> set_rel B) image image"
     3.5    unfolding fun_rel_def set_rel_def by simp fast
     3.6  
     3.7 +lemma UNION_transfer [transfer_rule]:
     3.8 +  "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) UNION UNION"
     3.9 +  unfolding SUP_def [abs_def] by transfer_prover
    3.10 +
    3.11  lemma Ball_transfer [transfer_rule]:
    3.12    "(set_rel A ===> (A ===> op =) ===> op =) Ball Ball"
    3.13    unfolding set_rel_def fun_rel_def by fast
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Apr 22 11:05:04 2012 +0200
     4.3 @@ -0,0 +1,285 @@
     4.4 +(*  Title:      HOL/Quotient_Examples/Lift_FSet.thy
     4.5 +    Author:     Brian Huffman, TU Munich
     4.6 +*)
     4.7 +
     4.8 +header {* Lifting and transfer with a finite set type *}
     4.9 +
    4.10 +theory Lift_FSet
    4.11 +imports "~~/src/HOL/Library/Quotient_List"
    4.12 +begin
    4.13 +
    4.14 +subsection {* Equivalence relation and quotient type definition *}
    4.15 +
    4.16 +definition list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    4.17 +  where [simp]: "list_eq xs ys \<longleftrightarrow> set xs = set ys"
    4.18 +
    4.19 +lemma reflp_list_eq: "reflp list_eq"
    4.20 +  unfolding reflp_def by simp
    4.21 +
    4.22 +lemma symp_list_eq: "symp list_eq"
    4.23 +  unfolding symp_def by simp
    4.24 +
    4.25 +lemma transp_list_eq: "transp list_eq"
    4.26 +  unfolding transp_def by simp
    4.27 +
    4.28 +lemma equivp_list_eq: "equivp list_eq"
    4.29 +  by (intro equivpI reflp_list_eq symp_list_eq transp_list_eq)
    4.30 +
    4.31 +quotient_type 'a fset = "'a list" / "list_eq"
    4.32 +  by (rule equivp_list_eq)
    4.33 +
    4.34 +subsection {* Lifted constant definitions *}
    4.35 +
    4.36 +lift_definition fnil :: "'a fset" is "[]"
    4.37 +  by simp
    4.38 +
    4.39 +lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons
    4.40 +  by simp
    4.41 +
    4.42 +lift_definition fappend :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is append
    4.43 +  by simp
    4.44 +
    4.45 +lift_definition fmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is map
    4.46 +  by simp
    4.47 +
    4.48 +lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is filter
    4.49 +  by simp
    4.50 +
    4.51 +lift_definition fset :: "'a fset \<Rightarrow> 'a set" is set
    4.52 +  by simp
    4.53 +
    4.54 +text {* Constants with nested types (like concat) yield a more
    4.55 +  complicated proof obligation. *}
    4.56 +
    4.57 +lemma list_all2_cr_fset:
    4.58 +  "list_all2 cr_fset xs ys \<longleftrightarrow> map abs_fset xs = ys"
    4.59 +  unfolding cr_fset_def
    4.60 +  apply safe
    4.61 +  apply (erule list_all2_induct, simp, simp)
    4.62 +  apply (simp add: list_all2_map2 List.list_all2_refl)
    4.63 +  done
    4.64 +
    4.65 +lemma abs_fset_eq_iff: "abs_fset xs = abs_fset ys \<longleftrightarrow> list_eq xs ys"
    4.66 +  using Quotient_rel [OF Quotient_fset] by simp
    4.67 +
    4.68 +lift_definition fconcat :: "'a fset fset \<Rightarrow> 'a fset" is concat
    4.69 +proof -
    4.70 +  fix xss yss :: "'a list list"
    4.71 +  assume "(list_all2 cr_fset OO list_eq OO (list_all2 cr_fset)\<inverse>\<inverse>) xss yss"
    4.72 +  then obtain uss vss where
    4.73 +    "list_all2 cr_fset xss uss" and "list_eq uss vss" and
    4.74 +    "list_all2 cr_fset yss vss" by clarsimp
    4.75 +  hence "list_eq (map abs_fset xss) (map abs_fset yss)"
    4.76 +    unfolding list_all2_cr_fset by simp
    4.77 +  thus "list_eq (concat xss) (concat yss)"
    4.78 +    apply (simp add: set_eq_iff image_def)
    4.79 +    apply safe
    4.80 +    apply (rename_tac xs, drule_tac x="abs_fset xs" in spec)
    4.81 +    apply (drule iffD1, fast, clarsimp simp add: abs_fset_eq_iff, fast)
    4.82 +    apply (rename_tac xs, drule_tac x="abs_fset xs" in spec)
    4.83 +    apply (drule iffD2, fast, clarsimp simp add: abs_fset_eq_iff, fast)
    4.84 +    done
    4.85 +qed
    4.86 +
    4.87 +text {* Note that the generated transfer rule contains a composition
    4.88 +  of relations. The transfer rule is not yet very useful in this form. *}
    4.89 +
    4.90 +lemma "(list_all2 cr_fset OO cr_fset ===> cr_fset) concat fconcat"
    4.91 +  by (fact fconcat.transfer)
    4.92 +
    4.93 +
    4.94 +subsection {* Using transfer with type @{text "fset"} *}
    4.95 +
    4.96 +text {* The correspondence relation @{text "cr_fset"} can only relate
    4.97 +  @{text "list"} and @{text "fset"} types with the same element type.
    4.98 +  To relate nested types like @{text "'a list list"} and
    4.99 +  @{text "'a fset fset"}, we define a parameterized version of the
   4.100 +  correspondence relation, @{text "cr_fset'"}. *}
   4.101 +
   4.102 +definition cr_fset' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b fset \<Rightarrow> bool"
   4.103 +  where "cr_fset' R = list_all2 R OO cr_fset"
   4.104 +
   4.105 +lemma right_unique_cr_fset' [transfer_rule]:
   4.106 +  "right_unique A \<Longrightarrow> right_unique (cr_fset' A)"
   4.107 +  unfolding cr_fset'_def
   4.108 +  by (intro right_unique_OO right_unique_list_all2 fset.right_unique)
   4.109 +
   4.110 +lemma right_total_cr_fset' [transfer_rule]:
   4.111 +  "right_total A \<Longrightarrow> right_total (cr_fset' A)"
   4.112 +  unfolding cr_fset'_def
   4.113 +  by (intro right_total_OO right_total_list_all2 fset.right_total)
   4.114 +
   4.115 +lemma bi_total_cr_fset' [transfer_rule]:
   4.116 +  "bi_total A \<Longrightarrow> bi_total (cr_fset' A)"
   4.117 +  unfolding cr_fset'_def
   4.118 +  by (intro bi_total_OO bi_total_list_all2 fset.bi_total)
   4.119 +
   4.120 +text {* Transfer rules for @{text "cr_fset'"} can be derived from the
   4.121 +  existing transfer rules for @{text "cr_fset"} together with the
   4.122 +  transfer rules for the polymorphic raw constants. *}
   4.123 +
   4.124 +text {* Note that the proofs below all have a similar structure and
   4.125 +  could potentially be automated. *}
   4.126 +
   4.127 +lemma fnil_transfer [transfer_rule]:
   4.128 +  "(cr_fset' A) [] fnil"
   4.129 +  unfolding cr_fset'_def
   4.130 +  apply (rule relcomppI)
   4.131 +  apply (rule Nil_transfer)
   4.132 +  apply (rule fnil.transfer)
   4.133 +  done
   4.134 +
   4.135 +lemma fcons_transfer [transfer_rule]:
   4.136 +  "(A ===> cr_fset' A ===> cr_fset' A) Cons fcons"
   4.137 +  unfolding cr_fset'_def
   4.138 +  apply (intro fun_relI)
   4.139 +  apply (elim relcomppE)
   4.140 +  apply (rule relcomppI)
   4.141 +  apply (erule (1) Cons_transfer [THEN fun_relD, THEN fun_relD])
   4.142 +  apply (erule fcons.transfer [THEN fun_relD, THEN fun_relD, OF refl])
   4.143 +  done
   4.144 +
   4.145 +lemma fappend_transfer [transfer_rule]:
   4.146 +  "(cr_fset' A ===> cr_fset' A ===> cr_fset' A) append fappend"
   4.147 +  unfolding cr_fset'_def
   4.148 +  apply (intro fun_relI)
   4.149 +  apply (elim relcomppE)
   4.150 +  apply (rule relcomppI)
   4.151 +  apply (erule (1) append_transfer [THEN fun_relD, THEN fun_relD])
   4.152 +  apply (erule (1) fappend.transfer [THEN fun_relD, THEN fun_relD])
   4.153 +  done
   4.154 +
   4.155 +lemma fmap_transfer [transfer_rule]:
   4.156 +  "((A ===> B) ===> cr_fset' A ===> cr_fset' B) map fmap"
   4.157 +  unfolding cr_fset'_def
   4.158 +  apply (intro fun_relI)
   4.159 +  apply (elim relcomppE)
   4.160 +  apply (rule relcomppI)
   4.161 +  apply (erule (1) map_transfer [THEN fun_relD, THEN fun_relD])
   4.162 +  apply (erule fmap.transfer [THEN fun_relD, THEN fun_relD, OF refl])
   4.163 +  done
   4.164 +
   4.165 +lemma ffilter_transfer [transfer_rule]:
   4.166 +  "((A ===> op =) ===> cr_fset' A ===> cr_fset' A) filter ffilter"
   4.167 +  unfolding cr_fset'_def
   4.168 +  apply (intro fun_relI)
   4.169 +  apply (elim relcomppE)
   4.170 +  apply (rule relcomppI)
   4.171 +  apply (erule (1) filter_transfer [THEN fun_relD, THEN fun_relD])
   4.172 +  apply (erule ffilter.transfer [THEN fun_relD, THEN fun_relD, OF refl])
   4.173 +  done
   4.174 +
   4.175 +lemma fset_transfer [transfer_rule]:
   4.176 +  "(cr_fset' A ===> set_rel A) set fset"
   4.177 +  unfolding cr_fset'_def
   4.178 +  apply (intro fun_relI)
   4.179 +  apply (elim relcomppE)
   4.180 +  apply (drule fset.transfer [THEN fun_relD])
   4.181 +  apply (erule subst)
   4.182 +  apply (erule set_transfer [THEN fun_relD])
   4.183 +  done
   4.184 +
   4.185 +lemma fconcat_transfer [transfer_rule]:
   4.186 +  "(cr_fset' (cr_fset' A) ===> cr_fset' A) concat fconcat"
   4.187 +  unfolding cr_fset'_def
   4.188 +  unfolding list_all2_OO
   4.189 +  apply (intro fun_relI)
   4.190 +  apply (elim relcomppE)
   4.191 +  apply (rule relcomppI)
   4.192 +  apply (erule concat_transfer [THEN fun_relD])
   4.193 +  apply (rule fconcat.transfer [THEN fun_relD])
   4.194 +  apply (erule (1) relcomppI)
   4.195 +  done
   4.196 +
   4.197 +lemma list_eq_transfer [transfer_rule]:
   4.198 +  assumes [transfer_rule]: "bi_unique A"
   4.199 +  shows "(list_all2 A ===> list_all2 A ===> op =) list_eq list_eq"
   4.200 +  unfolding list_eq_def [abs_def] by transfer_prover
   4.201 +
   4.202 +lemma fset_eq_transfer [transfer_rule]:
   4.203 +  assumes "bi_unique A"
   4.204 +  shows "(cr_fset' A ===> cr_fset' A ===> op =) list_eq (op =)"
   4.205 +  unfolding cr_fset'_def
   4.206 +  apply (intro fun_relI)
   4.207 +  apply (elim relcomppE)
   4.208 +  apply (rule trans)
   4.209 +  apply (erule (1) list_eq_transfer [THEN fun_relD, THEN fun_relD, OF assms])
   4.210 +  apply (erule (1) fset.rel_eq_transfer [THEN fun_relD, THEN fun_relD])
   4.211 +  done
   4.212 +
   4.213 +text {* We don't need the original transfer rules any more: *}
   4.214 +
   4.215 +lemmas [transfer_rule del] =
   4.216 +  fset.bi_total fset.right_total fset.right_unique
   4.217 +  fnil.transfer fcons.transfer fappend.transfer fmap.transfer
   4.218 +  ffilter.transfer fset.transfer fconcat.transfer fset.rel_eq_transfer
   4.219 +
   4.220 +subsection {* Transfer examples *}
   4.221 +
   4.222 +text {* The @{text "transfer"} method replaces equality on @{text
   4.223 +  "fset"} with the @{text "list_eq"} relation on lists, which is
   4.224 +  logically equivalent. *}
   4.225 +
   4.226 +lemma "fmap f (fmap g xs) = fmap (f \<circ> g) xs"
   4.227 +  apply transfer
   4.228 +  apply simp
   4.229 +  done
   4.230 +
   4.231 +text {* The @{text "transfer'"} variant can replace equality on @{text
   4.232 +  "fset"} with equality on @{text "list"}, which is logically stronger
   4.233 +  but sometimes more convenient. *}
   4.234 +
   4.235 +lemma "fmap f (fmap g xs) = fmap (f \<circ> g) xs"
   4.236 +  apply transfer'
   4.237 +  apply (rule map_map)
   4.238 +  done
   4.239 +
   4.240 +lemma "ffilter p (fmap f xs) = fmap f (ffilter (p \<circ> f) xs)"
   4.241 +  apply transfer'
   4.242 +  apply (rule filter_map)
   4.243 +  done
   4.244 +
   4.245 +lemma "ffilter p (ffilter q xs) = ffilter (\<lambda>x. q x \<and> p x) xs"
   4.246 +  apply transfer'
   4.247 +  apply (rule filter_filter)
   4.248 +  done
   4.249 +
   4.250 +lemma "fset (fcons x xs) = insert x (fset xs)"
   4.251 +  apply transfer
   4.252 +  apply (rule set.simps)
   4.253 +  done
   4.254 +
   4.255 +lemma "fset (fappend xs ys) = fset xs \<union> fset ys"
   4.256 +  apply transfer
   4.257 +  apply (rule set_append)
   4.258 +  done
   4.259 +
   4.260 +lemma "fset (fconcat xss) = (\<Union>xs\<in>fset xss. fset xs)"
   4.261 +  apply transfer
   4.262 +  apply (rule set_concat)
   4.263 +  done
   4.264 +
   4.265 +lemma "\<forall>x\<in>fset xs. f x = g x \<Longrightarrow> fmap f xs = fmap g xs"
   4.266 +  apply transfer
   4.267 +  apply (simp cong: map_cong del: set_map)
   4.268 +  done
   4.269 +
   4.270 +lemma "fnil = fconcat xss \<longleftrightarrow> (\<forall>xs\<in>fset xss. xs = fnil)"
   4.271 +  apply transfer
   4.272 +  apply simp
   4.273 +  done
   4.274 +
   4.275 +lemma "fconcat (fmap (\<lambda>x. fcons x fnil) xs) = xs"
   4.276 +  apply transfer'
   4.277 +  apply simp
   4.278 +  done
   4.279 +
   4.280 +lemma concat_map_concat: "concat (map concat xsss) = concat (concat xsss)"
   4.281 +  by (induct xsss, simp_all)
   4.282 +
   4.283 +lemma "fconcat (fmap fconcat xss) = fconcat (fconcat xss)"
   4.284 +  apply transfer'
   4.285 +  apply (rule concat_map_concat)
   4.286 +  done
   4.287 +
   4.288 +end
     5.1 --- a/src/HOL/Quotient_Examples/ROOT.ML	Sat Apr 21 21:38:08 2012 +0200
     5.2 +++ b/src/HOL/Quotient_Examples/ROOT.ML	Sun Apr 22 11:05:04 2012 +0200
     5.3 @@ -4,6 +4,6 @@
     5.4  Testing the quotient package.
     5.5  *)
     5.6  
     5.7 -use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message",
     5.8 +use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Lift_FSet",
     5.9    "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat", "Lift_DList"];
    5.10  
     6.1 --- a/src/HOL/Transfer.thy	Sat Apr 21 21:38:08 2012 +0200
     6.2 +++ b/src/HOL/Transfer.thy	Sun Apr 22 11:05:04 2012 +0200
     6.3 @@ -153,6 +153,25 @@
     6.4    "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
     6.5    unfolding bi_unique_def fun_rel_def by auto
     6.6  
     6.7 +text {* Properties are preserved by relation composition. *}
     6.8 +
     6.9 +lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"
    6.10 +  by auto
    6.11 +
    6.12 +lemma bi_total_OO: "\<lbrakk>bi_total A; bi_total B\<rbrakk> \<Longrightarrow> bi_total (A OO B)"
    6.13 +  unfolding bi_total_def OO_def by metis
    6.14 +
    6.15 +lemma bi_unique_OO: "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A OO B)"
    6.16 +  unfolding bi_unique_def OO_def by metis
    6.17 +
    6.18 +lemma right_total_OO:
    6.19 +  "\<lbrakk>right_total A; right_total B\<rbrakk> \<Longrightarrow> right_total (A OO B)"
    6.20 +  unfolding right_total_def OO_def by metis
    6.21 +
    6.22 +lemma right_unique_OO:
    6.23 +  "\<lbrakk>right_unique A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A OO B)"
    6.24 +  unfolding right_unique_def OO_def by metis
    6.25 +
    6.26  
    6.27  subsection {* Properties of relators *}
    6.28