# HG changeset patch # User huffman # Date 1335085504 -7200 # Node ID 7a5c681c0265bae7e3abcf7195150b0e6ff65f7f # Parent e3c4d1b0b3514481528746457464b3863ab78b9f new example theory for quotient/transfer diff -r e3c4d1b0b351 -r 7a5c681c0265 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Apr 21 21:38:08 2012 +0200 +++ b/src/HOL/IsaMakefile Sun Apr 22 11:05:04 2012 +0200 @@ -1509,6 +1509,7 @@ Quotient_Examples/DList.thy \ Quotient_Examples/FSet.thy \ Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \ + Quotient_Examples/Lift_FSet.thy \ Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \ Quotient_Examples/Lift_Fun.thy Quotient_Examples/Lift_DList.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples diff -r e3c4d1b0b351 -r 7a5c681c0265 src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Sat Apr 21 21:38:08 2012 +0200 +++ b/src/HOL/Library/Quotient_List.thy Sun Apr 22 11:05:04 2012 +0200 @@ -22,6 +22,21 @@ by (induct xs ys rule: list_induct2') simp_all qed +lemma list_all2_OO: "list_all2 (A OO B) = list_all2 A OO list_all2 B" +proof (intro ext iffI) + fix xs ys + assume "list_all2 (A OO B) xs ys" + thus "(list_all2 A OO list_all2 B) xs ys" + unfolding OO_def + by (induct, simp, simp add: list_all2_Cons1 list_all2_Cons2, fast) +next + fix xs ys + assume "(list_all2 A OO list_all2 B) xs ys" + then obtain zs where "list_all2 A xs zs" and "list_all2 B zs ys" .. + thus "list_all2 (A OO B) xs ys" + by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast) +qed + lemma list_reflp: assumes "reflp R" shows "reflp (list_all2 R)" diff -r e3c4d1b0b351 -r 7a5c681c0265 src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Sat Apr 21 21:38:08 2012 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Sun Apr 22 11:05:04 2012 +0200 @@ -91,6 +91,10 @@ "((A ===> B) ===> set_rel A ===> set_rel B) image image" unfolding fun_rel_def set_rel_def by simp fast +lemma UNION_transfer [transfer_rule]: + "(set_rel A ===> (A ===> set_rel B) ===> set_rel B) UNION UNION" + unfolding SUP_def [abs_def] by transfer_prover + lemma Ball_transfer [transfer_rule]: "(set_rel A ===> (A ===> op =) ===> op =) Ball Ball" unfolding set_rel_def fun_rel_def by fast diff -r e3c4d1b0b351 -r 7a5c681c0265 src/HOL/Quotient_Examples/Lift_FSet.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Sun Apr 22 11:05:04 2012 +0200 @@ -0,0 +1,285 @@ +(* Title: HOL/Quotient_Examples/Lift_FSet.thy + Author: Brian Huffman, TU Munich +*) + +header {* Lifting and transfer with a finite set type *} + +theory Lift_FSet +imports "~~/src/HOL/Library/Quotient_List" +begin + +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) + +quotient_type 'a fset = "'a list" / "list_eq" + by (rule equivp_list_eq) + +subsection {* Lifted constant definitions *} + +lift_definition fnil :: "'a fset" is "[]" + by simp + +lift_definition fcons :: "'a \ 'a fset \ 'a fset" is Cons + by simp + +lift_definition fappend :: "'a fset \ 'a fset \ 'a fset" is append + by simp + +lift_definition fmap :: "('a \ 'b) \ 'a fset \ 'b fset" is map + by simp + +lift_definition ffilter :: "('a \ bool) \ 'a fset \ 'a fset" is filter + by simp + +lift_definition fset :: "'a fset \ 'a set" is set + 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) + 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 +proof - + 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 + +text {* Note that the generated transfer rule contains a composition + of relations. The transfer rule is not yet very useful in this form. *} + +lemma "(list_all2 cr_fset OO cr_fset ===> cr_fset) concat fconcat" + by (fact fconcat.transfer) + + +subsection {* Using transfer with type @{text "fset"} *} + +text {* The correspondence relation @{text "cr_fset"} can only relate + @{text "list"} and @{text "fset"} types with the same element type. + To relate nested types like @{text "'a list list"} and + @{text "'a fset fset"}, we define a parameterized version of the + correspondence relation, @{text "cr_fset'"}. *} + +definition cr_fset' :: "('a \ 'b \ bool) \ 'a list \ 'b fset \ bool" + where "cr_fset' R = list_all2 R OO cr_fset" + +lemma right_unique_cr_fset' [transfer_rule]: + "right_unique A \ right_unique (cr_fset' A)" + unfolding cr_fset'_def + by (intro right_unique_OO right_unique_list_all2 fset.right_unique) + +lemma right_total_cr_fset' [transfer_rule]: + "right_total A \ right_total (cr_fset' A)" + unfolding cr_fset'_def + by (intro right_total_OO right_total_list_all2 fset.right_total) + +lemma bi_total_cr_fset' [transfer_rule]: + "bi_total A \ bi_total (cr_fset' A)" + unfolding cr_fset'_def + by (intro bi_total_OO bi_total_list_all2 fset.bi_total) + +text {* Transfer rules for @{text "cr_fset'"} can be derived from the + existing transfer rules for @{text "cr_fset"} together with the + transfer rules for the polymorphic raw constants. *} + +text {* Note that the proofs below all have a similar structure and + could potentially be automated. *} + +lemma fnil_transfer [transfer_rule]: + "(cr_fset' A) [] fnil" + unfolding cr_fset'_def + apply (rule relcomppI) + apply (rule Nil_transfer) + apply (rule fnil.transfer) + done + +lemma fcons_transfer [transfer_rule]: + "(A ===> cr_fset' A ===> cr_fset' A) Cons fcons" + unfolding cr_fset'_def + apply (intro fun_relI) + apply (elim relcomppE) + apply (rule relcomppI) + apply (erule (1) Cons_transfer [THEN fun_relD, THEN fun_relD]) + apply (erule fcons.transfer [THEN fun_relD, THEN fun_relD, OF refl]) + done + +lemma fappend_transfer [transfer_rule]: + "(cr_fset' A ===> cr_fset' A ===> cr_fset' A) append fappend" + unfolding cr_fset'_def + apply (intro fun_relI) + apply (elim relcomppE) + apply (rule relcomppI) + apply (erule (1) append_transfer [THEN fun_relD, THEN fun_relD]) + apply (erule (1) fappend.transfer [THEN fun_relD, THEN fun_relD]) + done + +lemma fmap_transfer [transfer_rule]: + "((A ===> B) ===> cr_fset' A ===> cr_fset' B) map fmap" + unfolding cr_fset'_def + apply (intro fun_relI) + apply (elim relcomppE) + apply (rule relcomppI) + apply (erule (1) map_transfer [THEN fun_relD, THEN fun_relD]) + apply (erule fmap.transfer [THEN fun_relD, THEN fun_relD, OF refl]) + done + +lemma ffilter_transfer [transfer_rule]: + "((A ===> op =) ===> cr_fset' A ===> cr_fset' A) filter ffilter" + unfolding cr_fset'_def + apply (intro fun_relI) + apply (elim relcomppE) + apply (rule relcomppI) + apply (erule (1) filter_transfer [THEN fun_relD, THEN fun_relD]) + apply (erule ffilter.transfer [THEN fun_relD, THEN fun_relD, OF refl]) + done + +lemma fset_transfer [transfer_rule]: + "(cr_fset' A ===> set_rel A) set fset" + unfolding cr_fset'_def + apply (intro fun_relI) + apply (elim relcomppE) + apply (drule fset.transfer [THEN fun_relD]) + apply (erule subst) + apply (erule set_transfer [THEN fun_relD]) + done + +lemma fconcat_transfer [transfer_rule]: + "(cr_fset' (cr_fset' A) ===> cr_fset' A) concat fconcat" + unfolding cr_fset'_def + unfolding list_all2_OO + apply (intro fun_relI) + apply (elim relcomppE) + apply (rule relcomppI) + apply (erule concat_transfer [THEN fun_relD]) + apply (rule fconcat.transfer [THEN fun_relD]) + apply (erule (1) relcomppI) + done + +lemma list_eq_transfer [transfer_rule]: + assumes [transfer_rule]: "bi_unique A" + shows "(list_all2 A ===> list_all2 A ===> op =) list_eq list_eq" + unfolding list_eq_def [abs_def] by transfer_prover + +lemma fset_eq_transfer [transfer_rule]: + assumes "bi_unique A" + shows "(cr_fset' A ===> cr_fset' A ===> op =) list_eq (op =)" + unfolding cr_fset'_def + apply (intro fun_relI) + apply (elim relcomppE) + apply (rule trans) + apply (erule (1) list_eq_transfer [THEN fun_relD, THEN fun_relD, OF assms]) + apply (erule (1) fset.rel_eq_transfer [THEN fun_relD, THEN fun_relD]) + done + +text {* We don't need the original transfer rules any more: *} + +lemmas [transfer_rule del] = + fset.bi_total fset.right_total fset.right_unique + fnil.transfer fcons.transfer fappend.transfer fmap.transfer + ffilter.transfer fset.transfer fconcat.transfer fset.rel_eq_transfer + +subsection {* Transfer examples *} + +text {* The @{text "transfer"} method replaces equality on @{text + "fset"} with the @{text "list_eq"} relation on lists, which is + logically equivalent. *} + +lemma "fmap f (fmap g xs) = fmap (f \ g) xs" + apply transfer + apply simp + done + +text {* The @{text "transfer'"} variant can replace equality on @{text + "fset"} with equality on @{text "list"}, which is logically stronger + but sometimes more convenient. *} + +lemma "fmap f (fmap g xs) = fmap (f \ g) xs" + apply transfer' + apply (rule map_map) + done + +lemma "ffilter p (fmap f xs) = fmap f (ffilter (p \ f) xs)" + apply transfer' + apply (rule filter_map) + done + +lemma "ffilter p (ffilter q xs) = ffilter (\x. q x \ p x) xs" + apply transfer' + apply (rule filter_filter) + done + +lemma "fset (fcons x xs) = insert x (fset xs)" + apply transfer + apply (rule set.simps) + done + +lemma "fset (fappend xs ys) = fset xs \ fset ys" + apply transfer + apply (rule set_append) + done + +lemma "fset (fconcat xss) = (\xs\fset xss. fset xs)" + apply transfer + apply (rule set_concat) + done + +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)" + apply transfer' + apply (rule concat_map_concat) + done + +end diff -r e3c4d1b0b351 -r 7a5c681c0265 src/HOL/Quotient_Examples/ROOT.ML --- a/src/HOL/Quotient_Examples/ROOT.ML Sat Apr 21 21:38:08 2012 +0200 +++ b/src/HOL/Quotient_Examples/ROOT.ML Sun Apr 22 11:05:04 2012 +0200 @@ -4,6 +4,6 @@ Testing the quotient package. *) -use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", +use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Lift_FSet", "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat", "Lift_DList"]; diff -r e3c4d1b0b351 -r 7a5c681c0265 src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Sat Apr 21 21:38:08 2012 +0200 +++ b/src/HOL/Transfer.thy Sun Apr 22 11:05:04 2012 +0200 @@ -153,6 +153,25 @@ "bi_unique R \ (R ===> R ===> op =) (op =) (op =)" unfolding bi_unique_def fun_rel_def by auto +text {* Properties are preserved by relation composition. *} + +lemma OO_def: "R OO S = (\x z. \y. R x y \ S y z)" + by auto + +lemma bi_total_OO: "\bi_total A; bi_total B\ \ bi_total (A OO B)" + unfolding bi_total_def OO_def by metis + +lemma bi_unique_OO: "\bi_unique A; bi_unique B\ \ bi_unique (A OO B)" + unfolding bi_unique_def OO_def by metis + +lemma right_total_OO: + "\right_total A; right_total B\ \ right_total (A OO B)" + unfolding right_total_def OO_def by metis + +lemma right_unique_OO: + "\right_unique A; right_unique B\ \ right_unique (A OO B)" + unfolding right_unique_def OO_def by metis + subsection {* Properties of relators *}