# HG changeset patch # User kuncar # Date 1332508649 -3600 # Node ID fa3538d6004ba8b8952eec01fe1a2796f6a87ab1 # Parent d5cd13aca90ba3cc9acfb7c6f83f99aa105749f5 fix Quotient_Examples diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Mar 23 14:03:58 2012 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Mar 23 14:17:29 2012 +0100 @@ -115,6 +115,7 @@ "add_raw \ \(x, y) (u, v). (x + (u\nat), y + (v\nat))" quotient_definition "add\my_int \ my_int \ my_int" is add_raw +unfolding add_raw_def by auto lemma "add x y = add x x" nitpick [show_datatypes, expect = genuine] diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/DList.thy --- a/src/HOL/Quotient_Examples/DList.thy Fri Mar 23 14:03:58 2012 +0100 +++ b/src/HOL/Quotient_Examples/DList.thy Fri Mar 23 14:17:29 2012 +0100 @@ -88,45 +88,32 @@ definition [simp]: "card_remdups = length \ remdups" definition [simp]: "foldr_remdups f xs e = foldr f (remdups xs) e" -lemma [quot_respect]: - "(dlist_eq) Nil Nil" - "(dlist_eq ===> op =) List.member List.member" - "(op = ===> dlist_eq ===> dlist_eq) Cons Cons" - "(op = ===> dlist_eq ===> dlist_eq) removeAll removeAll" - "(dlist_eq ===> op =) card_remdups card_remdups" - "(dlist_eq ===> op =) remdups remdups" - "(op = ===> dlist_eq ===> op =) foldr_remdups foldr_remdups" - "(op = ===> dlist_eq ===> dlist_eq) map map" - "(op = ===> dlist_eq ===> dlist_eq) filter filter" - by (auto intro!: fun_relI simp add: remdups_filter) - (metis (full_types) set_remdups remdups_eq_map_eq remdups_eq_member_eq)+ - quotient_definition empty where "empty :: 'a dlist" - is "Nil" + is "Nil" done quotient_definition insert where "insert :: 'a \ 'a dlist \ 'a dlist" - is "Cons" + is "Cons" by (metis (mono_tags) List.insert_def dlist_eq_def remdups.simps(2) set_remdups) quotient_definition "member :: 'a dlist \ 'a \ bool" - is "List.member" + is "List.member" by (metis dlist_eq_def remdups_eq_member_eq) quotient_definition foldr where "foldr :: ('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" - is "foldr_remdups" + is "foldr_remdups" by auto quotient_definition "remove :: 'a \ 'a dlist \ 'a dlist" - is "removeAll" + is "removeAll" by force quotient_definition card where "card :: 'a dlist \ nat" - is "card_remdups" + is "card_remdups" by fastforce quotient_definition map where "map :: ('a \ 'b) \ 'a dlist \ 'b dlist" - is "List.map :: ('a \ 'b) \ 'a list \ 'b list" + is "List.map :: ('a \ 'b) \ 'a list \ 'b list" by (metis dlist_eq_def remdups_eq_map_eq) quotient_definition filter where "filter :: ('a \ bool) \ 'a dlist \ 'a dlist" - is "List.filter" + is "List.filter" by (metis dlist_eq_def remdups_filter) quotient_definition "list_of_dlist :: 'a dlist \ 'a list" - is "remdups" + is "remdups" by simp text {* lifted theorems *} diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Fri Mar 23 14:03:58 2012 +0100 +++ b/src/HOL/Quotient_Examples/FSet.thy Fri Mar 23 14:17:29 2012 +0100 @@ -179,140 +179,6 @@ by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp) - -subsection {* Respectfulness lemmas for list operations *} - -lemma list_equiv_rsp [quot_respect]: - shows "(op \ ===> op \ ===> op =) op \ op \" - by (auto intro!: fun_relI) - -lemma append_rsp [quot_respect]: - shows "(op \ ===> op \ ===> op \) append append" - by (auto intro!: fun_relI) - -lemma sub_list_rsp [quot_respect]: - shows "(op \ ===> op \ ===> op =) sub_list sub_list" - by (auto intro!: fun_relI) - -lemma member_rsp [quot_respect]: - shows "(op \ ===> op =) List.member List.member" -proof - fix x y assume "x \ y" - then show "List.member x = List.member y" - unfolding fun_eq_iff by simp -qed - -lemma nil_rsp [quot_respect]: - shows "(op \) Nil Nil" - by simp - -lemma cons_rsp [quot_respect]: - shows "(op = ===> op \ ===> op \) Cons Cons" - by (auto intro!: fun_relI) - -lemma map_rsp [quot_respect]: - shows "(op = ===> op \ ===> op \) map map" - by (auto intro!: fun_relI) - -lemma set_rsp [quot_respect]: - "(op \ ===> op =) set set" - by (auto intro!: fun_relI) - -lemma inter_list_rsp [quot_respect]: - shows "(op \ ===> op \ ===> op \) inter_list inter_list" - by (auto intro!: fun_relI) - -lemma removeAll_rsp [quot_respect]: - shows "(op = ===> op \ ===> op \) removeAll removeAll" - by (auto intro!: fun_relI) - -lemma diff_list_rsp [quot_respect]: - shows "(op \ ===> op \ ===> op \) diff_list diff_list" - by (auto intro!: fun_relI) - -lemma card_list_rsp [quot_respect]: - shows "(op \ ===> op =) card_list card_list" - by (auto intro!: fun_relI) - -lemma filter_rsp [quot_respect]: - shows "(op = ===> op \ ===> op \) filter filter" - by (auto intro!: fun_relI) - -lemma remdups_removeAll: (*FIXME move*) - "remdups (removeAll x xs) = remove1 x (remdups xs)" - by (induct xs) auto - -lemma member_commute_fold_once: - assumes "rsp_fold f" - and "x \ set xs" - shows "fold_once f xs = fold_once f (removeAll x xs) \ f x" -proof - - from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \ f x" - by (auto intro!: fold_remove1_split elim: rsp_foldE) - then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll) -qed - -lemma fold_once_set_equiv: - assumes "xs \ ys" - shows "fold_once f xs = fold_once f ys" -proof (cases "rsp_fold f") - case False then show ?thesis by simp -next - case True - then have "\x y. x \ set (remdups xs) \ y \ set (remdups xs) \ f x \ f y = f y \ f x" - by (rule rsp_foldE) - moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)" - by (simp add: set_eq_iff_multiset_of_remdups_eq) - ultimately have "fold f (remdups xs) = fold f (remdups ys)" - by (rule fold_multiset_equiv) - with True show ?thesis by (simp add: fold_once_fold_remdups) -qed - -lemma fold_once_rsp [quot_respect]: - shows "(op = ===> op \ ===> op =) fold_once fold_once" - unfolding fun_rel_def by (auto intro: fold_once_set_equiv) - -lemma concat_rsp_pre: - assumes a: "list_all2 op \ x x'" - and b: "x' \ y'" - and c: "list_all2 op \ y' y" - and d: "\x\set x. xa \ set x" - shows "\x\set y. xa \ set x" -proof - - obtain xb where e: "xb \ set x" and f: "xa \ set xb" using d by auto - have "\y. y \ set x' \ xb \ y" by (rule list_all2_find_element[OF e a]) - then obtain ya where h: "ya \ set x'" and i: "xb \ ya" by auto - have "ya \ set y'" using b h by simp - then have "\yb. yb \ set y \ ya \ yb" using c by (rule list_all2_find_element) - then show ?thesis using f i by auto -qed - -lemma concat_rsp [quot_respect]: - shows "(list_all2 op \ OOO op \ ===> op \) concat concat" -proof (rule fun_relI, elim pred_compE) - fix a b ba bb - assume a: "list_all2 op \ a ba" - with list_symp [OF list_eq_symp] have a': "list_all2 op \ ba a" by (rule sympE) - assume b: "ba \ bb" - with list_eq_symp have b': "bb \ ba" by (rule sympE) - assume c: "list_all2 op \ bb b" - with list_symp [OF list_eq_symp] have c': "list_all2 op \ b bb" by (rule sympE) - have "\x. (\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" - proof - fix x - show "(\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" - proof - assume d: "\xa\set a. x \ set xa" - show "\xa\set b. x \ set xa" by (rule concat_rsp_pre[OF a b c d]) - next - assume e: "\xa\set b. x \ set xa" - show "\xa\set a. x \ set xa" by (rule concat_rsp_pre[OF c' b' a' e]) - qed - qed - then show "concat a \ concat b" by auto -qed - - section {* Quotient definitions for fsets *} @@ -323,7 +189,7 @@ quotient_definition "bot :: 'a fset" - is "Nil :: 'a list" + is "Nil :: 'a list" done abbreviation empty_fset ("{||}") @@ -332,7 +198,7 @@ quotient_definition "less_eq_fset :: ('a fset \ 'a fset \ bool)" - is "sub_list :: ('a list \ 'a list \ bool)" + is "sub_list :: ('a list \ 'a list \ bool)" by simp abbreviation subset_fset :: "'a fset \ 'a fset \ bool" (infix "|\|" 50) @@ -351,7 +217,7 @@ quotient_definition "sup :: 'a fset \ 'a fset \ 'a fset" - is "append :: 'a list \ 'a list \ 'a list" + is "append :: 'a list \ 'a list \ 'a list" by simp abbreviation union_fset (infixl "|\|" 65) @@ -360,7 +226,7 @@ quotient_definition "inf :: 'a fset \ 'a fset \ 'a fset" - is "inter_list :: 'a list \ 'a list \ 'a list" + is "inter_list :: 'a list \ 'a list \ 'a list" by simp abbreviation inter_fset (infixl "|\|" 65) @@ -369,7 +235,7 @@ quotient_definition "minus :: 'a fset \ 'a fset \ 'a fset" - is "diff_list :: 'a list \ 'a list \ 'a list" + is "diff_list :: 'a list \ 'a list \ 'a list" by fastforce instance proof @@ -413,7 +279,7 @@ quotient_definition "insert_fset :: 'a \ 'a fset \ 'a fset" - is "Cons" + is "Cons" by auto syntax "_insert_fset" :: "args => 'a fset" ("{|(_)|}") @@ -425,7 +291,7 @@ quotient_definition fset_member where - "fset_member :: 'a fset \ 'a \ bool" is "List.member" + "fset_member :: 'a fset \ 'a \ bool" is "List.member" by fastforce abbreviation in_fset :: "'a \ 'a fset \ bool" (infix "|\|" 50) @@ -442,31 +308,84 @@ quotient_definition "card_fset :: 'a fset \ nat" - is card_list + is card_list by simp quotient_definition "map_fset :: ('a \ 'b) \ 'a fset \ 'b fset" - is map + is map by simp quotient_definition "remove_fset :: 'a \ 'a fset \ 'a fset" - is removeAll + is removeAll by simp quotient_definition "fset :: 'a fset \ 'a set" - is "set" + is "set" by simp + +lemma fold_once_set_equiv: + assumes "xs \ ys" + shows "fold_once f xs = fold_once f ys" +proof (cases "rsp_fold f") + case False then show ?thesis by simp +next + case True + then have "\x y. x \ set (remdups xs) \ y \ set (remdups xs) \ f x \ f y = f y \ f x" + by (rule rsp_foldE) + moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)" + by (simp add: set_eq_iff_multiset_of_remdups_eq) + ultimately have "fold f (remdups xs) = fold f (remdups ys)" + by (rule fold_multiset_equiv) + with True show ?thesis by (simp add: fold_once_fold_remdups) +qed quotient_definition "fold_fset :: ('a \ 'b \ 'b) \ 'a fset \ 'b \ 'b" - is fold_once + is fold_once by (rule fold_once_set_equiv) + +lemma concat_rsp_pre: + assumes a: "list_all2 op \ x x'" + and b: "x' \ y'" + and c: "list_all2 op \ y' y" + and d: "\x\set x. xa \ set x" + shows "\x\set y. xa \ set x" +proof - + obtain xb where e: "xb \ set x" and f: "xa \ set xb" using d by auto + have "\y. y \ set x' \ xb \ y" by (rule list_all2_find_element[OF e a]) + then obtain ya where h: "ya \ set x'" and i: "xb \ ya" by auto + have "ya \ set y'" using b h by simp + then have "\yb. yb \ set y \ ya \ yb" using c by (rule list_all2_find_element) + then show ?thesis using f i by auto +qed quotient_definition "concat_fset :: ('a fset) fset \ 'a fset" - is concat + is concat +proof (elim pred_compE) +fix a b ba bb + assume a: "list_all2 op \ a ba" + with list_symp [OF list_eq_symp] have a': "list_all2 op \ ba a" by (rule sympE) + assume b: "ba \ bb" + with list_eq_symp have b': "bb \ ba" by (rule sympE) + assume c: "list_all2 op \ bb b" + with list_symp [OF list_eq_symp] have c': "list_all2 op \ b bb" by (rule sympE) + have "\x. (\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" + proof + fix x + show "(\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" + proof + assume d: "\xa\set a. x \ set xa" + show "\xa\set b. x \ set xa" by (rule concat_rsp_pre[OF a b c d]) + next + assume e: "\xa\set b. x \ set xa" + show "\xa\set a. x \ set xa" by (rule concat_rsp_pre[OF c' b' a' e]) + qed + qed + then show "concat a \ concat b" by auto +qed quotient_definition "filter_fset :: ('a \ bool) \ 'a fset \ 'a fset" - is filter + is filter by force subsection {* Compositional respectfulness and preservation lemmas *} @@ -538,7 +457,7 @@ lemma append_rsp2 [quot_respect]: "(list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \) append append" - by (intro compositional_rsp3 append_rsp) + by (intro compositional_rsp3) (auto intro!: fun_relI simp add: append_rsp2_pre) lemma map_rsp2 [quot_respect]: @@ -967,6 +886,20 @@ (if rsp_fold f then if a |\| A then fold_fset f A else fold_fset f A \ f a else id)" by descending (simp add: fold_once_fold_remdups) +lemma remdups_removeAll: + "remdups (removeAll x xs) = remove1 x (remdups xs)" + by (induct xs) auto + +lemma member_commute_fold_once: + assumes "rsp_fold f" + and "x \ set xs" + shows "fold_once f xs = fold_once f (removeAll x xs) \ f x" +proof - + from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \ f x" + by (auto intro!: fold_remove1_split elim: rsp_foldE) + then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll) +qed + lemma in_commute_fold_fset: "rsp_fold f \ h |\| b \ fold_fset f b = fold_fset f (remove_fset h b) \ f h" by descending (simp add: member_commute_fold_once) @@ -1170,7 +1103,7 @@ then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b by auto have f: "card_list (removeAll a l) = m" using e d by (simp) - have g: "removeAll a l \ removeAll a r" using removeAll_rsp b by simp + have g: "removeAll a l \ removeAll a r" using remove_fset_rsp b by simp have "(removeAll a l) \2 (removeAll a r)" by (rule Suc.hyps[OF f g]) then have h: "(a # removeAll a l) \2 (a # removeAll a r)" by (rule list_eq2.intros(5)) have i: "l \2 (a # removeAll a l)" diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Lift_Fun.thy --- a/src/HOL/Quotient_Examples/Lift_Fun.thy Fri Mar 23 14:03:58 2012 +0100 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy Fri Mar 23 14:17:29 2012 +0100 @@ -23,17 +23,17 @@ by (simp add: identity_equivp) quotient_definition "comp' :: ('b \ 'c) \ ('a \ 'b) \ 'a \ 'c" is - "comp :: ('b \ 'c) \ ('a \ 'b) \ 'a \ 'c" + "comp :: ('b \ 'c) \ ('a \ 'b) \ 'a \ 'c" done quotient_definition "fcomp' :: ('a \ 'b) \ ('b \ 'c) \ 'a \ 'c" is - fcomp + fcomp done quotient_definition "map_fun' :: ('c \ 'a) \ ('b \ 'd) \ ('a \ 'b) \ 'c \ 'd" - is "map_fun::('c \ 'a) \ ('b \ 'd) \ ('a \ 'b) \ 'c \ 'd" + is "map_fun::('c \ 'a) \ ('b \ 'd) \ ('a \ 'b) \ 'c \ 'd" done -quotient_definition "inj_on' :: ('a \ 'b) \ 'a set \ bool" is inj_on +quotient_definition "inj_on' :: ('a \ 'b) \ 'a set \ bool" is inj_on done -quotient_definition "bij_betw' :: ('a \ 'b) \ 'a set \ 'b set \ bool" is bij_betw +quotient_definition "bij_betw' :: ('a \ 'b) \ 'a set \ 'b set \ bool" is bij_betw done subsection {* Co/Contravariant type variables *} @@ -47,7 +47,7 @@ where "map_endofun' f g e = map_fun g f e" quotient_definition "map_endofun :: ('a \ 'b) \ ('b \ 'a) \ 'a endofun \ 'b endofun" is - map_endofun' + map_endofun' done text {* Registration of the map function for 'a endofun. *} @@ -63,7 +63,7 @@ by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) qed -quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \ 'a) \ ('a \ 'a)" +quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \ 'a) \ ('a \ 'a)" done term endofun_id_id thm endofun_id_id_def @@ -73,7 +73,7 @@ text {* We have to map "'a endofun" to "('a endofun') endofun", i.e., mapping (lifting) over a type variable which is a covariant and contravariant type variable. *} -quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id +quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id done term endofun'_id_id thm endofun'_id_id_def diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Lift_RBT.thy --- a/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Mar 23 14:03:58 2012 +0100 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Mar 23 14:17:29 2012 +0100 @@ -18,7 +18,7 @@ local_setup {* fn lthy => let val quotients = {qtyp = @{typ "('a, 'b) rbt"}, rtyp = @{typ "('a, 'b) RBT_Impl.rbt"}, - equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}} + equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}} val qty_full_name = @{type_name "rbt"} fun qinfo phi = Quotient_Info.transform_quotients phi quotients @@ -50,6 +50,7 @@ subsection {* Primitive operations *} quotient_definition lookup where "lookup :: ('a\linorder, 'b) rbt \ 'a \ 'b" is "RBT_Impl.lookup" +done declare lookup_def[unfolded map_fun_def comp_def id_def, code] @@ -67,21 +68,21 @@ *) quotient_definition empty where "empty :: ('a\linorder, 'b) rbt" -is "(RBT_Impl.Empty :: ('a\linorder, 'b) RBT_Impl.rbt)" +is "(RBT_Impl.Empty :: ('a\linorder, 'b) RBT_Impl.rbt)" done lemma impl_of_empty [code abstract]: "impl_of empty = RBT_Impl.Empty" by (simp add: empty_def RBT_inverse) quotient_definition insert where "insert :: 'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" -is "RBT_Impl.insert" +is "RBT_Impl.insert" done lemma impl_of_insert [code abstract]: "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)" by (simp add: insert_def RBT_inverse) quotient_definition delete where "delete :: 'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" -is "RBT_Impl.delete" +is "RBT_Impl.delete" done lemma impl_of_delete [code abstract]: "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)" @@ -89,24 +90,24 @@ (* FIXME: unnecessary type annotations *) quotient_definition "entries :: ('a\linorder, 'b) rbt \ ('a \ 'b) list" -is "RBT_Impl.entries :: ('a\linorder, 'b) RBT_Impl.rbt \ ('a \ 'b) list" +is "RBT_Impl.entries :: ('a\linorder, 'b) RBT_Impl.rbt \ ('a \ 'b) list" done lemma [code]: "entries t = RBT_Impl.entries (impl_of t)" unfolding entries_def map_fun_def comp_def id_def .. (* FIXME: unnecessary type annotations *) quotient_definition "keys :: ('a\linorder, 'b) rbt \ 'a list" -is "RBT_Impl.keys :: ('a\linorder, 'b) RBT_Impl.rbt \ 'a list" +is "RBT_Impl.keys :: ('a\linorder, 'b) RBT_Impl.rbt \ 'a list" done quotient_definition "bulkload :: ('a\linorder \ 'b) list \ ('a, 'b) rbt" -is "RBT_Impl.bulkload" +is "RBT_Impl.bulkload" done lemma impl_of_bulkload [code abstract]: "impl_of (bulkload xs) = RBT_Impl.bulkload xs" by (simp add: bulkload_def RBT_inverse) quotient_definition "map_entry :: 'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" -is "RBT_Impl.map_entry" +is "RBT_Impl.map_entry" done lemma impl_of_map_entry [code abstract]: "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)" @@ -115,13 +116,15 @@ (* FIXME: unnecesary type annotations *) quotient_definition map where "map :: ('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is "RBT_Impl.map :: ('a \ 'b \ 'b) \ ('a\linorder, 'b) RBT_Impl.rbt \ ('a, 'b) RBT_Impl.rbt" +done lemma impl_of_map [code abstract]: "impl_of (map f t) = RBT_Impl.map f (impl_of t)" by (simp add: map_def RBT_inverse) (* FIXME: unnecessary type annotations *) -quotient_definition fold where "fold :: ('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" is "RBT_Impl.fold :: ('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) RBT_Impl.rbt \ 'c \ 'c" +quotient_definition fold where "fold :: ('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" +is "RBT_Impl.fold :: ('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) RBT_Impl.rbt \ 'c \ 'c" done lemma [code]: "fold f t = RBT_Impl.fold f (impl_of t)" unfolding fold_def map_fun_def comp_def id_def .. diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Lift_Set.thy --- a/src/HOL/Quotient_Examples/Lift_Set.thy Fri Mar 23 14:03:58 2012 +0100 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy Fri Mar 23 14:17:29 2012 +0100 @@ -20,7 +20,7 @@ let val quotients = {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"}, - equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}} + equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}} val qty_full_name = @{type_name "set"} fun qinfo phi = Quotient_Info.transform_quotients phi quotients @@ -37,7 +37,7 @@ text {* Now, we can employ quotient_definition to lift definitions. *} quotient_definition empty where "empty :: 'a set" -is "bot :: 'a \ bool" +is "bot :: 'a \ bool" done term "Lift_Set.empty" thm Lift_Set.empty_def @@ -46,7 +46,7 @@ "insertp x P y \ y = x \ P y" quotient_definition insert where "insert :: 'a => 'a set => 'a set" -is insertp +is insertp done term "Lift_Set.insert" thm Lift_Set.insert_def diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Quotient_Cset.thy --- a/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 23 14:03:58 2012 +0100 +++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 23 14:17:29 2012 +0100 @@ -21,75 +21,50 @@ subsection {* Operations *} -lemma [quot_respect]: - "(op = ===> set_eq ===> op =) (op \) (op \)" - "(op = ===> set_eq) Collect Collect" - "(set_eq ===> op =) Set.is_empty Set.is_empty" - "(op = ===> set_eq ===> set_eq) Set.insert Set.insert" - "(op = ===> set_eq ===> set_eq) Set.remove Set.remove" - "(op = ===> set_eq ===> set_eq) image image" - "(op = ===> set_eq ===> set_eq) Set.project Set.project" - "(set_eq ===> op =) Ball Ball" - "(set_eq ===> op =) Bex Bex" - "(set_eq ===> op =) Finite_Set.card Finite_Set.card" - "(set_eq ===> set_eq ===> op =) (op \) (op \)" - "(set_eq ===> set_eq ===> op =) (op \) (op \)" - "(set_eq ===> set_eq ===> set_eq) (op \) (op \)" - "(set_eq ===> set_eq ===> set_eq) (op \) (op \)" - "set_eq {} {}" - "set_eq UNIV UNIV" - "(set_eq ===> set_eq) uminus uminus" - "(set_eq ===> set_eq ===> set_eq) minus minus" - "(set_eq ===> op =) Inf Inf" - "(set_eq ===> op =) Sup Sup" - "(op = ===> set_eq) List.set List.set" - "(set_eq ===> (op = ===> set_eq) ===> set_eq) UNION UNION" -by (auto simp: fun_rel_eq) - quotient_definition "member :: 'a => 'a Quotient_Cset.set => bool" -is "op \" +is "op \" by simp quotient_definition "Set :: ('a => bool) => 'a Quotient_Cset.set" -is Collect +is Collect done quotient_definition is_empty where "is_empty :: 'a Quotient_Cset.set \ bool" -is Set.is_empty +is Set.is_empty by simp quotient_definition insert where "insert :: 'a \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is Set.insert +is Set.insert by simp quotient_definition remove where "remove :: 'a \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is Set.remove +is Set.remove by simp quotient_definition map where "map :: ('a \ 'b) \ 'a Quotient_Cset.set \ 'b Quotient_Cset.set" -is image +is image by simp quotient_definition filter where "filter :: ('a \ bool) \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is Set.project +is Set.project by simp quotient_definition "forall :: 'a Quotient_Cset.set \ ('a \ bool) \ bool" -is Ball +is Ball by simp quotient_definition "exists :: 'a Quotient_Cset.set \ ('a \ bool) \ bool" -is Bex +is Bex by simp quotient_definition card where "card :: 'a Quotient_Cset.set \ nat" -is Finite_Set.card +is Finite_Set.card by simp quotient_definition set where "set :: 'a list => 'a Quotient_Cset.set" -is List.set +is List.set done quotient_definition subset where "subset :: 'a Quotient_Cset.set \ 'a Quotient_Cset.set \ bool" -is "op \ :: 'a set \ 'a set \ bool" +is "op \ :: 'a set \ 'a set \ bool" by simp quotient_definition psubset where "psubset :: 'a Quotient_Cset.set \ 'a Quotient_Cset.set \ bool" -is "op \ :: 'a set \ 'a set \ bool" +is "op \ :: 'a set \ 'a set \ bool" by simp quotient_definition inter where "inter :: 'a Quotient_Cset.set \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is "op \ :: 'a set \ 'a set \ 'a set" +is "op \ :: 'a set \ 'a set \ 'a set" by simp quotient_definition union where "union :: 'a Quotient_Cset.set \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is "op \ :: 'a set \ 'a set \ 'a set" +is "op \ :: 'a set \ 'a set \ 'a set" by simp quotient_definition empty where "empty :: 'a Quotient_Cset.set" -is "{} :: 'a set" +is "{} :: 'a set" done quotient_definition UNIV where "UNIV :: 'a Quotient_Cset.set" -is "Set.UNIV :: 'a set" +is "Set.UNIV :: 'a set" done quotient_definition uminus where "uminus :: 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is "uminus_class.uminus :: 'a set \ 'a set" +is "uminus_class.uminus :: 'a set \ 'a set" by simp quotient_definition minus where "minus :: 'a Quotient_Cset.set \ 'a Quotient_Cset.set \ 'a Quotient_Cset.set" -is "(op -) :: 'a set \ 'a set \ 'a set" +is "(op -) :: 'a set \ 'a set \ 'a set" by simp quotient_definition Inf where "Inf :: ('a :: Inf) Quotient_Cset.set \ 'a" -is "Inf_class.Inf :: ('a :: Inf) set \ 'a" +is "Inf_class.Inf :: ('a :: Inf) set \ 'a" by simp quotient_definition Sup where "Sup :: ('a :: Sup) Quotient_Cset.set \ 'a" -is "Sup_class.Sup :: ('a :: Sup) set \ 'a" +is "Sup_class.Sup :: ('a :: Sup) set \ 'a" by simp quotient_definition UNION where "UNION :: 'a Quotient_Cset.set \ ('a \ 'b Quotient_Cset.set) \ 'b Quotient_Cset.set" -is "Complete_Lattices.UNION :: 'a set \ ('a \ 'b set) \ 'b set" +is "Complete_Lattices.UNION :: 'a set \ ('a \ 'b set) \ 'b set" by simp hide_const (open) is_empty insert remove map filter forall exists card set subset psubset inter union empty UNIV uminus minus Inf Sup UNION diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Quotient_Int.thy --- a/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Mar 23 14:03:58 2012 +0100 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Mar 23 14:17:29 2012 +0100 @@ -22,10 +22,10 @@ begin quotient_definition - "0 \ int" is "(0\nat, 0\nat)" + "0 \ int" is "(0\nat, 0\nat)" done quotient_definition - "1 \ int" is "(1\nat, 0\nat)" + "1 \ int" is "(1\nat, 0\nat)" done fun plus_int_raw :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" @@ -33,7 +33,7 @@ "plus_int_raw (x, y) (u, v) = (x + u, y + v)" quotient_definition - "(op +) \ (int \ int \ int)" is "plus_int_raw" + "(op +) \ (int \ int \ int)" is "plus_int_raw" by auto fun uminus_int_raw :: "(nat \ nat) \ (nat \ nat)" @@ -41,7 +41,7 @@ "uminus_int_raw (x, y) = (y, x)" quotient_definition - "(uminus \ (int \ int))" is "uminus_int_raw" + "(uminus \ (int \ int))" is "uminus_int_raw" by auto definition minus_int_def: "z - w = z + (-w\int)" @@ -51,8 +51,38 @@ where "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" +lemma times_int_raw_fst: + assumes a: "x \ z" + shows "times_int_raw x y \ times_int_raw z y" + using a + apply(cases x, cases y, cases z) + apply(auto simp add: times_int_raw.simps intrel.simps) + apply(rename_tac u v w x y z) + apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") + apply(simp add: mult_ac) + apply(simp add: add_mult_distrib [symmetric]) +done + +lemma times_int_raw_snd: + assumes a: "x \ z" + shows "times_int_raw y x \ times_int_raw y z" + using a + apply(cases x, cases y, cases z) + apply(auto simp add: times_int_raw.simps intrel.simps) + apply(rename_tac u v w x y z) + apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") + apply(simp add: mult_ac) + apply(simp add: add_mult_distrib [symmetric]) +done + quotient_definition "(op *) :: (int \ int \ int)" is "times_int_raw" + apply(rule equivp_transp[OF int_equivp]) + apply(rule times_int_raw_fst) + apply(assumption) + apply(rule times_int_raw_snd) + apply(assumption) +done fun le_int_raw :: "(nat \ nat) \ (nat \ nat) \ bool" @@ -60,7 +90,7 @@ "le_int_raw (x, y) (u, v) = (x+v \ u+y)" quotient_definition - le_int_def: "(op \) :: int \ int \ bool" is "le_int_raw" + le_int_def: "(op \) :: int \ int \ bool" is "le_int_raw" by auto definition less_int_def: "(z\int) < w = (z \ w \ z \ w)" @@ -75,47 +105,6 @@ end -lemma [quot_respect]: - shows "(op \ ===> op \ ===> op \) plus_int_raw plus_int_raw" - and "(op \ ===> op \) uminus_int_raw uminus_int_raw" - and "(op \ ===> op \ ===> op =) le_int_raw le_int_raw" - by (auto intro!: fun_relI) - -lemma times_int_raw_fst: - assumes a: "x \ z" - shows "times_int_raw x y \ times_int_raw z y" - using a - apply(cases x, cases y, cases z) - apply(auto simp add: times_int_raw.simps intrel.simps) - apply(rename_tac u v w x y z) - apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") - apply(simp add: mult_ac) - apply(simp add: add_mult_distrib [symmetric]) - done - -lemma times_int_raw_snd: - assumes a: "x \ z" - shows "times_int_raw y x \ times_int_raw y z" - using a - apply(cases x, cases y, cases z) - apply(auto simp add: times_int_raw.simps intrel.simps) - apply(rename_tac u v w x y z) - apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") - apply(simp add: mult_ac) - apply(simp add: add_mult_distrib [symmetric]) - done - -lemma [quot_respect]: - shows "(op \ ===> op \ ===> op \) times_int_raw times_int_raw" - apply(simp only: fun_rel_def) - apply(rule allI | rule impI)+ - apply(rule equivp_transp[OF int_equivp]) - apply(rule times_int_raw_fst) - apply(assumption) - apply(rule times_int_raw_snd) - apply(assumption) - done - text{* The integers form a @{text comm_ring_1}*} @@ -165,11 +154,7 @@ "int_of_nat_raw m = (m :: nat, 0 :: nat)" quotient_definition - "int_of_nat :: nat \ int" is "int_of_nat_raw" - -lemma[quot_respect]: - shows "(op = ===> op \) int_of_nat_raw int_of_nat_raw" - by (auto simp add: equivp_reflp [OF int_equivp]) + "int_of_nat :: nat \ int" is "int_of_nat_raw" done lemma int_of_nat: shows "of_nat m = int_of_nat m" @@ -304,11 +289,7 @@ quotient_definition "int_to_nat::int \ nat" is - "int_to_nat_raw" - -lemma [quot_respect]: - shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw" - by (auto iff: int_to_nat_raw_def) + "int_to_nat_raw" unfolding int_to_nat_raw_def by force lemma nat_le_eq_zle: fixes w z::"int" diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Quotient_Message.thy --- a/src/HOL/Quotient_Examples/Quotient_Message.thy Fri Mar 23 14:03:58 2012 +0100 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Fri Mar 23 14:17:29 2012 +0100 @@ -136,29 +136,25 @@ "Nonce :: nat \ msg" is "NONCE" +done quotient_definition "MPair :: msg \ msg \ msg" is "MPAIR" +by (rule MPAIR) quotient_definition "Crypt :: nat \ msg \ msg" is "CRYPT" +by (rule CRYPT) quotient_definition "Decrypt :: nat \ msg \ msg" is "DECRYPT" - -lemma [quot_respect]: - shows "(op = ===> op \ ===> op \) CRYPT CRYPT" -by (auto intro: CRYPT) - -lemma [quot_respect]: - shows "(op = ===> op \ ===> op \) DECRYPT DECRYPT" -by (auto intro: DECRYPT) +by (rule DECRYPT) text{*Establishing these two equations is the point of the whole exercise*} theorem CD_eq [simp]: @@ -175,25 +171,14 @@ "nonces:: msg \ nat set" is "freenonces" +by (rule msgrel_imp_eq_freenonces) text{*Now prove the four equations for @{term nonces}*} -lemma [quot_respect]: - shows "(op \ ===> op =) freenonces freenonces" - by (auto simp add: msgrel_imp_eq_freenonces) - -lemma [quot_respect]: - shows "(op = ===> op \) NONCE NONCE" - by (auto simp add: NONCE) - lemma nonces_Nonce [simp]: shows "nonces (Nonce N) = {N}" by (lifting freenonces.simps(1)) -lemma [quot_respect]: - shows " (op \ ===> op \ ===> op \) MPAIR MPAIR" - by (auto simp add: MPAIR) - lemma nonces_MPair [simp]: shows "nonces (MPair X Y) = nonces X \ nonces Y" by (lifting freenonces.simps(2)) @@ -212,10 +197,7 @@ "left:: msg \ msg" is "freeleft" - -lemma [quot_respect]: - shows "(op \ ===> op \) freeleft freeleft" - by (auto simp add: msgrel_imp_eqv_freeleft) +by (rule msgrel_imp_eqv_freeleft) lemma left_Nonce [simp]: shows "left (Nonce N) = Nonce N" @@ -239,13 +221,10 @@ "right:: msg \ msg" is "freeright" +by (rule msgrel_imp_eqv_freeright) text{*Now prove the four equations for @{term right}*} -lemma [quot_respect]: - shows "(op \ ===> op \) freeright freeright" - by (auto simp add: msgrel_imp_eqv_freeright) - lemma right_Nonce [simp]: shows "right (Nonce N) = Nonce N" by (lifting freeright.simps(1)) @@ -352,13 +331,10 @@ "discrim:: msg \ int" is "freediscrim" +by (rule msgrel_imp_eq_freediscrim) text{*Now prove the four equations for @{term discrim}*} -lemma [quot_respect]: - shows "(op \ ===> op =) freediscrim freediscrim" - by (auto simp add: msgrel_imp_eq_freediscrim) - lemma discrim_Nonce [simp]: shows "discrim (Nonce N) = 0" by (lifting freediscrim.simps(1)) diff -r d5cd13aca90b -r fa3538d6004b src/HOL/Quotient_Examples/Quotient_Rat.thy --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy Fri Mar 23 14:03:58 2012 +0100 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Fri Mar 23 14:17:29 2012 +0100 @@ -32,28 +32,29 @@ begin quotient_definition - "0 \ rat" is "(0\int, 1\int)" + "0 \ rat" is "(0\int, 1\int)" by simp quotient_definition - "1 \ rat" is "(1\int, 1\int)" + "1 \ rat" is "(1\int, 1\int)" by simp fun times_rat_raw where "times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)" quotient_definition - "(op *) :: (rat \ rat \ rat)" is times_rat_raw + "(op *) :: (rat \ rat \ rat)" is times_rat_raw by (auto simp add: mult_assoc mult_left_commute) fun plus_rat_raw where "plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)" quotient_definition - "(op +) :: (rat \ rat \ rat)" is plus_rat_raw + "(op +) :: (rat \ rat \ rat)" is plus_rat_raw + by (auto simp add: mult_commute mult_left_commute int_distrib(2)) fun uminus_rat_raw where "uminus_rat_raw (a :: int, b :: int) = (-a, b)" quotient_definition - "(uminus \ (rat \ rat))" is "uminus_rat_raw" + "(uminus \ (rat \ rat))" is "uminus_rat_raw" by fastforce definition minus_rat_def: "a - b = a + (-b\rat)" @@ -63,6 +64,32 @@ quotient_definition "(op \) :: rat \ rat \ bool" is "le_rat_raw" +proof - + { + fix a b c d e f g h :: int + assume "a * f * (b * f) \ e * b * (b * f)" + then have le: "a * f * b * f \ e * b * b * f" by simp + assume nz: "b \ 0" "d \ 0" "f \ 0" "h \ 0" + then have b2: "b * b > 0" + by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero) + have f2: "f * f > 0" using nz(3) + by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero) + assume eq: "a * d = c * b" "e * h = g * f" + have "a * f * b * f * d * d \ e * b * b * f * d * d" using le nz(2) + by (metis linorder_le_cases mult_right_mono mult_right_mono_neg) + then have "c * f * f * d * (b * b) \ e * f * d * d * (b * b)" using eq + by (metis (no_types) mult_assoc mult_commute) + then have "c * f * f * d \ e * f * d * d" using b2 + by (metis leD linorder_le_less_linear mult_strict_right_mono) + then have "c * f * f * d * h * h \ e * f * d * d * h * h" using nz(4) + by (metis linorder_le_cases mult_right_mono mult_right_mono_neg) + then have "c * h * (d * h) * (f * f) \ g * d * (d * h) * (f * f)" using eq + by (metis (no_types) mult_assoc mult_commute) + then have "c * h * (d * h) \ g * d * (d * h)" using f2 + by (metis leD linorder_le_less_linear mult_strict_right_mono) + } + then show "\x y xa ya. x \ y \ xa \ ya \ le_rat_raw x xa = le_rat_raw y ya" by auto +qed definition less_rat_def: "(z\rat) < w = (z \ w \ z \ w)" @@ -83,14 +110,7 @@ where [simp]: "Fract_raw a b = (if b = 0 then (0, 1) else (a, b))" quotient_definition "Fract :: int \ int \ rat" is - Fract_raw - -lemma [quot_respect]: - "(op \ ===> op \ ===> op \) times_rat_raw times_rat_raw" - "(op \ ===> op \ ===> op \) plus_rat_raw plus_rat_raw" - "(op \ ===> op \) uminus_rat_raw uminus_rat_raw" - "(op = ===> op = ===> op \) Fract_raw Fract_raw" - by (auto intro!: fun_relI simp add: mult_assoc mult_commute mult_left_commute int_distrib(2)) + Fract_raw by simp lemmas [simp] = Respects_def @@ -156,15 +176,11 @@ "rat_inverse_raw (a :: int, b :: int) = (if a = 0 then (0, 1) else (b, a))" quotient_definition - "inverse :: rat \ rat" is rat_inverse_raw + "inverse :: rat \ rat" is rat_inverse_raw by (force simp add: mult_commute) definition divide_rat_def: "q / r = q * inverse (r::rat)" -lemma [quot_respect]: - "(op \ ===> op \) rat_inverse_raw rat_inverse_raw" - by (auto intro!: fun_relI simp add: mult_commute) - instance proof fix q :: rat assume "q \ 0" @@ -179,34 +195,6 @@ end -lemma [quot_respect]: "(op \ ===> op \ ===> op =) le_rat_raw le_rat_raw" -proof - - { - fix a b c d e f g h :: int - assume "a * f * (b * f) \ e * b * (b * f)" - then have le: "a * f * b * f \ e * b * b * f" by simp - assume nz: "b \ 0" "d \ 0" "f \ 0" "h \ 0" - then have b2: "b * b > 0" - by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero) - have f2: "f * f > 0" using nz(3) - by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero) - assume eq: "a * d = c * b" "e * h = g * f" - have "a * f * b * f * d * d \ e * b * b * f * d * d" using le nz(2) - by (metis linorder_le_cases mult_right_mono mult_right_mono_neg) - then have "c * f * f * d * (b * b) \ e * f * d * d * (b * b)" using eq - by (metis (no_types) mult_assoc mult_commute) - then have "c * f * f * d \ e * f * d * d" using b2 - by (metis leD linorder_le_less_linear mult_strict_right_mono) - then have "c * f * f * d * h * h \ e * f * d * d * h * h" using nz(4) - by (metis linorder_le_cases mult_right_mono mult_right_mono_neg) - then have "c * h * (d * h) * (f * f) \ g * d * (d * h) * (f * f)" using eq - by (metis (no_types) mult_assoc mult_commute) - then have "c * h * (d * h) \ g * d * (d * h)" using f2 - by (metis leD linorder_le_less_linear mult_strict_right_mono) - } - then show ?thesis by (auto intro!: fun_relI) -qed - instantiation rat :: linorder begin