# HG changeset patch # User paulson # Date 1332519395 0 # Node ID b846c299f412dce687e17f73f59ca5041c2beb3c # Parent f8f788c8b7f31d4e655c3c036af7dcb16cd78e54# Parent ded5cc757bc9cb322bc8e7db4a63127f62c941fb merged diff -r ded5cc757bc9 -r b846c299f412 etc/isar-keywords.el --- a/etc/isar-keywords.el Fri Mar 23 16:16:15 2012 +0000 +++ b/etc/isar-keywords.el Fri Mar 23 16:16:35 2012 +0000 @@ -221,6 +221,7 @@ "sect" "section" "setup" + "setup_lifting" "show" "simproc_setup" "sledgehammer" @@ -518,13 +519,13 @@ "print_translation" "quickcheck_generator" "quickcheck_params" - "quotient_definition" "realizability" "realizers" "recdef" "record" "refute_params" "setup" + "setup_lifting" "simproc_setup" "sledgehammer_params" "spark_end" @@ -563,6 +564,7 @@ "nominal_inductive2" "nominal_primrec" "pcpodef" + "quotient_definition" "quotient_type" "recdef_tc" "rep_datatype" diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Library/Quotient_List.thy Fri Mar 23 16:16:35 2012 +0000 @@ -8,8 +8,6 @@ imports Main Quotient_Syntax begin -declare [[map list = list_all2]] - lemma map_id [id_simps]: "map id = id" by (fact List.map.id) @@ -75,6 +73,8 @@ by (induct xs ys rule: list_induct2') auto qed +declare [[map list = (list_all2, list_quotient)]] + lemma cons_prs [quot_preserve]: assumes q: "Quotient R Abs Rep" shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Library/Quotient_Option.thy Fri Mar 23 16:16:35 2012 +0000 @@ -16,8 +16,6 @@ | "option_rel R None (Some x) = False" | "option_rel R (Some x) (Some y) = R x y" -declare [[map option = option_rel]] - lemma option_rel_unfold: "option_rel R x y = (case (x, y) of (None, None) \ True | (Some x, Some y) \ R x y @@ -65,6 +63,8 @@ apply (simp add: option_rel_unfold split: option.split) done +declare [[map option = (option_rel, option_quotient)]] + lemma option_None_rsp [quot_respect]: assumes q: "Quotient R Abs Rep" shows "option_rel R None None" diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Library/Quotient_Product.thy Fri Mar 23 16:16:35 2012 +0000 @@ -13,8 +13,6 @@ where "prod_rel R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)" -declare [[map prod = prod_rel]] - lemma prod_rel_apply [simp]: "prod_rel R1 R2 (a, b) (c, d) \ R1 a c \ R2 b d" by (simp add: prod_rel_def) @@ -45,6 +43,8 @@ apply (auto simp add: split_paired_all) done +declare [[map prod = (prod_rel, prod_quotient)]] + lemma Pair_rsp [quot_respect]: assumes q1: "Quotient R1 Abs1 Rep1" assumes q2: "Quotient R2 Abs2 Rep2" diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Library/Quotient_Set.thy Fri Mar 23 16:16:35 2012 +0000 @@ -26,6 +26,8 @@ by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+ qed +declare [[map set = (set_rel, set_quotient)]] + lemma empty_set_rsp[quot_respect]: "set_rel R {} {}" unfolding set_rel_def by simp diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Library/Quotient_Sum.thy Fri Mar 23 16:16:35 2012 +0000 @@ -16,8 +16,6 @@ | "sum_rel R1 R2 (Inr a2) (Inl b1) = False" | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" -declare [[map sum = sum_rel]] - lemma sum_rel_unfold: "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \ R1 x y | (Inr x, Inr y) \ R2 x y @@ -67,6 +65,8 @@ apply (simp add: sum_rel_unfold comp_def split: sum.split) done +declare [[map sum = (sum_rel, sum_quotient)]] + lemma sum_Inl_rsp [quot_respect]: assumes q1: "Quotient R1 Abs1 Rep1" assumes q2: "Quotient R2 Abs2 Rep2" diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Mar 23 16:16:35 2012 +0000 @@ -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 ded5cc757bc9 -r b846c299f412 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Quotient.thy Fri Mar 23 16:16:35 2012 +0000 @@ -9,7 +9,8 @@ keywords "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and "quotient_type" :: thy_goal and "/" and - "quotient_definition" :: thy_decl + "setup_lifting" :: thy_decl and + "quotient_definition" :: thy_goal uses ("Tools/Quotient/quotient_info.ML") ("Tools/Quotient/quotient_type.ML") @@ -79,6 +80,10 @@ shows "((op =) ===> (op =)) = (op =)" by (auto simp add: fun_eq_iff elim: fun_relE) +lemma fun_rel_eq_rel: + shows "((op =) ===> R) = (\f g. \x. R (f x) (g x))" + by (simp add: fun_rel_def) + subsection {* set map (vimage) and set relation *} definition "set_rel R xs ys \ \x y. R x y \ x \ xs \ y \ ys" @@ -133,6 +138,18 @@ unfolding Quotient_def by blast +lemma Quotient_refl1: + assumes a: "Quotient R Abs Rep" + shows "R r s \ R r r" + using a unfolding Quotient_def + by fast + +lemma Quotient_refl2: + assumes a: "Quotient R Abs Rep" + shows "R r s \ R s s" + using a unfolding Quotient_def + by fast + lemma Quotient_rel_rep: assumes a: "Quotient R Abs Rep" shows "R (Rep a) (Rep b) \ a = b" @@ -259,6 +276,15 @@ shows "R2 (f x) (g y)" using a by (auto elim: fun_relE) +lemma apply_rsp'': + assumes "Quotient R Abs Rep" + and "(R ===> S) f f" + shows "S (f (Rep x)) (f (Rep x))" +proof - + from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp) + then show ?thesis using assms(2) by (auto intro: apply_rsp') +qed + subsection {* lemmas for regularisation of ball and bex *} lemma ball_reg_eqv: @@ -675,6 +701,153 @@ end +subsection {* Quotient composition *} + +lemma OOO_quotient: + fixes R1 :: "'a \ 'a \ bool" + fixes Abs1 :: "'a \ 'b" and Rep1 :: "'b \ 'a" + fixes Abs2 :: "'b \ 'c" and Rep2 :: "'c \ 'b" + fixes R2' :: "'a \ 'a \ bool" + fixes R2 :: "'b \ 'b \ bool" + assumes R1: "Quotient R1 Abs1 Rep1" + assumes R2: "Quotient R2 Abs2 Rep2" + assumes Abs1: "\x y. R2' x y \ R1 x x \ R1 y y \ R2 (Abs1 x) (Abs1 y)" + assumes Rep1: "\x y. R2 x y \ R2' (Rep1 x) (Rep1 y)" + shows "Quotient (R1 OO R2' OO R1) (Abs2 \ Abs1) (Rep1 \ Rep2)" +apply (rule QuotientI) + apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1]) + apply simp + apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI) + apply (rule Quotient_rep_reflp [OF R1]) + apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated]) + apply (rule Quotient_rep_reflp [OF R1]) + apply (rule Rep1) + apply (rule Quotient_rep_reflp [OF R2]) + apply safe + apply (rename_tac x y) + apply (drule Abs1) + apply (erule Quotient_refl2 [OF R1]) + apply (erule Quotient_refl1 [OF R1]) + apply (drule Quotient_refl1 [OF R2], drule Rep1) + apply (subgoal_tac "R1 r (Rep1 (Abs1 x))") + apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption) + apply (erule pred_compI) + apply (erule Quotient_symp [OF R1, THEN sympD]) + apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) + apply (rule conjI, erule Quotient_refl1 [OF R1]) + apply (rule conjI, rule Quotient_rep_reflp [OF R1]) + apply (subst Quotient_abs_rep [OF R1]) + apply (erule Quotient_rel_abs [OF R1]) + apply (rename_tac x y) + apply (drule Abs1) + apply (erule Quotient_refl2 [OF R1]) + apply (erule Quotient_refl1 [OF R1]) + apply (drule Quotient_refl2 [OF R2], drule Rep1) + apply (subgoal_tac "R1 s (Rep1 (Abs1 y))") + apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption) + apply (erule pred_compI) + apply (erule Quotient_symp [OF R1, THEN sympD]) + apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) + apply (rule conjI, erule Quotient_refl2 [OF R1]) + apply (rule conjI, rule Quotient_rep_reflp [OF R1]) + apply (subst Quotient_abs_rep [OF R1]) + apply (erule Quotient_rel_abs [OF R1, THEN sym]) + apply simp + apply (rule Quotient_rel_abs [OF R2]) + apply (rule Quotient_rel_abs [OF R1, THEN ssubst], assumption) + apply (rule Quotient_rel_abs [OF R1, THEN subst], assumption) + apply (erule Abs1) + apply (erule Quotient_refl2 [OF R1]) + apply (erule Quotient_refl1 [OF R1]) + apply (rename_tac a b c d) + apply simp + apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI) + apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) + apply (rule conjI, erule Quotient_refl1 [OF R1]) + apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1]) + apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated]) + apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2]) + apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1]) + apply (erule Quotient_refl2 [OF R1]) + apply (rule Rep1) + apply (drule Abs1) + apply (erule Quotient_refl2 [OF R1]) + apply (erule Quotient_refl1 [OF R1]) + apply (drule Abs1) + apply (erule Quotient_refl2 [OF R1]) + apply (erule Quotient_refl1 [OF R1]) + apply (drule Quotient_rel_abs [OF R1]) + apply (drule Quotient_rel_abs [OF R1]) + apply (drule Quotient_rel_abs [OF R1]) + apply (drule Quotient_rel_abs [OF R1]) + apply simp + apply (rule Quotient_rel[symmetric, OF R2, THEN iffD2]) + apply simp +done + +lemma OOO_eq_quotient: + fixes R1 :: "'a \ 'a \ bool" + fixes Abs1 :: "'a \ 'b" and Rep1 :: "'b \ 'a" + fixes Abs2 :: "'b \ 'c" and Rep2 :: "'c \ 'b" + assumes R1: "Quotient R1 Abs1 Rep1" + assumes R2: "Quotient op= Abs2 Rep2" + shows "Quotient (R1 OOO op=) (Abs2 \ Abs1) (Rep1 \ Rep2)" +using assms +by (rule OOO_quotient) auto + +subsection {* Invariant *} + +definition invariant :: "('a \ bool) \ 'a \ 'a \ bool" + where "invariant R = (\x y. R x \ x = y)" + +lemma invariant_to_eq: + assumes "invariant P x y" + shows "x = y" +using assms by (simp add: invariant_def) + +lemma fun_rel_eq_invariant: + shows "((invariant R) ===> S) = (\f g. \x. R x \ S (f x) (g x))" +by (auto simp add: invariant_def fun_rel_def) + +lemma invariant_same_args: + shows "invariant P x x \ P x" +using assms by (auto simp add: invariant_def) + +lemma copy_type_to_Quotient: + assumes "type_definition Rep Abs UNIV" + shows "Quotient (op =) Abs Rep" +proof - + interpret type_definition Rep Abs UNIV by fact + from Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI) +qed + +lemma copy_type_to_equivp: + fixes Abs :: "'a \ 'b" + and Rep :: "'b \ 'a" + assumes "type_definition Rep Abs (UNIV::'a set)" + shows "equivp (op=::'a\'a\bool)" +by (rule identity_equivp) + +lemma invariant_type_to_Quotient: + assumes "type_definition Rep Abs {x. P x}" + shows "Quotient (invariant P) Abs Rep" +proof - + interpret type_definition Rep Abs "{x. P x}" by fact + from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI simp: invariant_def) +qed + +lemma invariant_type_to_part_equivp: + assumes "type_definition Rep Abs {x. P x}" + shows "part_equivp (invariant P)" +proof (intro part_equivpI) + interpret type_definition Rep Abs "{x. P x}" by fact + show "\x. invariant P x x" using Rep by (auto simp: invariant_def) +next + show "symp (invariant P)" by (auto intro: sympI simp: invariant_def) +next + show "transp (invariant P)" by (auto intro: transpI simp: invariant_def) +qed + subsection {* ML setup *} text {* Auxiliary data for the quotient package *} @@ -682,8 +855,7 @@ use "Tools/Quotient/quotient_info.ML" setup Quotient_Info.setup -declare [[map "fun" = fun_rel]] -declare [[map set = set_rel]] +declare [[map "fun" = (fun_rel, fun_quotient)]] lemmas [quot_thm] = fun_quotient lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Quotient_Examples/DList.thy --- a/src/HOL/Quotient_Examples/DList.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Quotient_Examples/DList.thy Fri Mar 23 16:16:35 2012 +0000 @@ -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 ded5cc757bc9 -r b846c299f412 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Quotient_Examples/FSet.thy Fri Mar 23 16:16:35 2012 +0000 @@ -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 ded5cc757bc9 -r b846c299f412 src/HOL/Quotient_Examples/Lift_Fun.thy --- a/src/HOL/Quotient_Examples/Lift_Fun.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy Fri Mar 23 16:16:35 2012 +0000 @@ -6,7 +6,7 @@ theory Lift_Fun -imports Main +imports Main "~~/src/HOL/Library/Quotient_Syntax" begin text {* This file is meant as a test case for features introduced in the changeset 2d8949268303. @@ -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,45 @@ 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)" +text {* Relator for 'a endofun. *} + +definition + endofun_rel' :: "('a \ 'b \ bool) \ ('a \ 'a) \ ('b \ 'b) \ bool" +where + "endofun_rel' R = (\f g. (R ===> R) f g)" + +quotient_definition "endofun_rel :: ('a \ 'b \ bool) \ 'a endofun \ 'b endofun \ bool" is + endofun_rel' done + +lemma endofun_quotient: +assumes a: "Quotient R Abs Rep" +shows "Quotient (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)" +proof (intro QuotientI) + show "\a. map_endofun Abs Rep (map_endofun Rep Abs a) = a" + by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs) +next + show "\a. endofun_rel R (map_endofun Rep Abs a) (map_endofun Rep Abs a)" + using fun_quotient[OF a a, THEN Quotient_rep_reflp] + unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def + by (metis (mono_tags) Quotient_endofun rep_abs_rsp) +next + show "\r s. endofun_rel R r s = + (endofun_rel R r r \ + endofun_rel R s s \ map_endofun Abs Rep r = map_endofun Abs Rep s)" + apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def) + using fun_quotient[OF a a,THEN Quotient_refl1] + apply metis + using fun_quotient[OF a a,THEN Quotient_refl2] + apply metis + using fun_quotient[OF a a, THEN Quotient_rel] + apply metis + using fun_quotient[OF a a, THEN Quotient_rel] + by (smt Quotient_endofun rep_abs_rsp) +qed + +declare [[map endofun = (endofun_rel, endofun_quotient)]] + +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 +111,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 ded5cc757bc9 -r b846c299f412 src/HOL/Quotient_Examples/Lift_RBT.thy --- a/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Mar 23 16:16:35 2012 +0000 @@ -15,21 +15,6 @@ then show ?thesis .. qed -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}} - val qty_full_name = @{type_name "rbt"} - - fun qinfo phi = Quotient_Info.transform_quotients phi quotients - in lthy - |> Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi) - #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi - {abs = @{term "RBT"}, rep = @{term "impl_of"}})) - end -*} - lemma rbt_eq_iff: "t1 = t2 \ impl_of t1 = impl_of t2" by (simp add: impl_of_inject) @@ -46,12 +31,12 @@ "RBT (impl_of t) = t" by (simp add: impl_of_inverse) - subsection {* Primitive operations *} -quotient_definition lookup where "lookup :: ('a\linorder, 'b) rbt \ 'a \ 'b" is "RBT_Impl.lookup" +setup_lifting type_definition_rbt -declare lookup_def[unfolded map_fun_def comp_def id_def, code] +quotient_definition lookup where "lookup :: ('a\linorder, 'b) rbt \ 'a \ 'b" is "RBT_Impl.lookup" +by simp (* FIXME: quotient_definition at the moment requires that types variables match exactly, i.e., sort constraints must be annotated to the constant being lifted. @@ -67,65 +52,38 @@ *) quotient_definition empty where "empty :: ('a\linorder, 'b) rbt" -is "(RBT_Impl.Empty :: ('a\linorder, 'b) RBT_Impl.rbt)" - -lemma impl_of_empty [code abstract]: - "impl_of empty = RBT_Impl.Empty" - by (simp add: empty_def RBT_inverse) +is "(RBT_Impl.Empty :: ('a\linorder, 'b) RBT_Impl.rbt)" by (simp add: empty_def) quotient_definition insert where "insert :: 'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" -is "RBT_Impl.insert" - -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) +is "RBT_Impl.insert" by simp quotient_definition delete where "delete :: 'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" -is "RBT_Impl.delete" - -lemma impl_of_delete [code abstract]: - "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)" - by (simp add: delete_def RBT_inverse) +is "RBT_Impl.delete" by simp (* 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" - -lemma [code]: "entries t = RBT_Impl.entries (impl_of t)" -unfolding entries_def map_fun_def comp_def id_def .. +is "RBT_Impl.entries :: ('a\linorder, 'b) RBT_Impl.rbt \ ('a \ 'b) list" by simp (* 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" by simp quotient_definition "bulkload :: ('a\linorder \ 'b) list \ ('a, 'b) rbt" -is "RBT_Impl.bulkload" - -lemma impl_of_bulkload [code abstract]: - "impl_of (bulkload xs) = RBT_Impl.bulkload xs" - by (simp add: bulkload_def RBT_inverse) +is "RBT_Impl.bulkload" by simp quotient_definition "map_entry :: 'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" -is "RBT_Impl.map_entry" - -lemma impl_of_map_entry [code abstract]: - "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)" - by (simp add: map_entry_def RBT_inverse) +is "RBT_Impl.map_entry" by simp (* 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" - -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) +by simp (* 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" by simp -lemma [code]: "fold f t = RBT_Impl.fold f (impl_of t)" -unfolding fold_def map_fun_def comp_def id_def .. - +export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML subsection {* Derived operations *} @@ -189,6 +147,10 @@ "fold f t = List.fold (prod_case f) (entries t)" by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of) +lemma impl_of_empty: + "impl_of empty = RBT_Impl.Empty" + by (simp add: empty_def RBT_inverse) + lemma is_empty_empty [simp]: "is_empty t \ t = empty" by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split) @@ -210,5 +172,4 @@ by (simp add: keys_def RBT_Impl.keys_def distinct_entries) - end \ No newline at end of file diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Quotient_Examples/Lift_Set.thy --- a/src/HOL/Quotient_Examples/Lift_Set.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy Fri Mar 23 16:16:35 2012 +0000 @@ -14,30 +14,12 @@ morphisms member Set unfolding set_def by auto -text {* Here is some ML setup that should eventually be incorporated in the typedef command. *} - -local_setup {* fn lthy => - let - val quotients = - {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"}, - equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}} - val qty_full_name = @{type_name "set"} - - fun qinfo phi = Quotient_Info.transform_quotients phi quotients - in - lthy - |> Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => - Quotient_Info.update_quotients qty_full_name (qinfo phi) #> - Quotient_Info.update_abs_rep qty_full_name - (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}})) - end -*} +setup_lifting type_definition_set[unfolded set_def] 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,10 +28,12 @@ "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 +export_code empty insert in SML + end diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Quotient_Examples/Quotient_Cset.thy --- a/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 23 16:16:35 2012 +0000 @@ -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 ded5cc757bc9 -r b846c299f412 src/HOL/Quotient_Examples/Quotient_Int.thy --- a/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Mar 23 16:16:35 2012 +0000 @@ -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 ded5cc757bc9 -r b846c299f412 src/HOL/Quotient_Examples/Quotient_Message.thy --- a/src/HOL/Quotient_Examples/Quotient_Message.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Fri Mar 23 16:16:35 2012 +0000 @@ -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 ded5cc757bc9 -r b846c299f412 src/HOL/Quotient_Examples/Quotient_Rat.thy --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Fri Mar 23 16:16:35 2012 +0000 @@ -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 diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 23 16:16:35 2012 +0000 @@ -6,13 +6,17 @@ signature QUOTIENT_DEF = sig + val add_quotient_def: + ((binding * mixfix) * Attrib.binding) * (term * term) -> thm -> + local_theory -> Quotient_Info.quotconsts * local_theory + val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) -> - local_theory -> Quotient_Info.quotconsts * local_theory + local_theory -> Proof.state val quotient_def_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) -> - local_theory -> Quotient_Info.quotconsts * local_theory + local_theory -> Proof.state val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory -> Quotient_Info.quotconsts * local_theory @@ -23,6 +27,130 @@ (** Interface and Syntax Setup **) +(* Generation of the code certificate from the rsp theorem *) + +infix 0 MRSL + +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm + +fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V) + | get_body_types (U, V) = (U, V) + +fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W) + | get_binder_types _ = [] + +fun unabs_def ctxt def = + let + val (_, rhs) = Thm.dest_equals (cprop_of def) + fun dest_abs (Abs (var_name, T, _)) = (var_name, T) + | dest_abs tm = raise TERM("get_abs_var",[tm]) + val (var_name, T) = dest_abs (term_of rhs) + val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt + val thy = Proof_Context.theory_of ctxt' + val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T))) + in + Thm.combination def refl_thm |> + singleton (Proof_Context.export ctxt' ctxt) + end + +fun unabs_all_def ctxt def = + let + val (_, rhs) = Thm.dest_equals (cprop_of def) + val xs = strip_abs_vars (term_of rhs) + in + fold (K (unabs_def ctxt)) xs def + end + +val map_fun_unfolded = + @{thm map_fun_def[abs_def]} |> + unabs_def @{context} |> + unabs_def @{context} |> + Local_Defs.unfold @{context} [@{thm comp_def}] + +fun unfold_fun_maps ctm = + let + fun unfold_conv ctm = + case (Thm.term_of ctm) of + Const (@{const_name "map_fun"}, _) $ _ $ _ => + (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm + | _ => Conv.all_conv ctm + val try_beta_conv = Conv.try_conv (Thm.beta_conversion false) + in + (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm + end + +fun prove_rel ctxt rsp_thm (rty, qty) = + let + val ty_args = get_binder_types (rty, qty) + fun disch_arg args_ty thm = + let + val quot_thm = Quotient_Term.prove_quot_theorem ctxt args_ty + in + [quot_thm, thm] MRSL @{thm apply_rsp''} + end + in + fold disch_arg ty_args rsp_thm + end + +exception CODE_CERT_GEN of string + +fun simplify_code_eq ctxt def_thm = + Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm + +fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) = + let + val quot_thm = Quotient_Term.prove_quot_theorem ctxt (get_body_types (rty, qty)) + val fun_rel = prove_rel ctxt rsp_thm (rty, qty) + val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs} + val abs_rep_eq = + case (HOLogic.dest_Trueprop o prop_of) fun_rel of + Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm + | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq} + | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant" + val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm + val unabs_def = unabs_all_def ctxt unfolded_def + val rep = (snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) quot_thm + val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq} + val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong} + val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans} + in + simplify_code_eq ctxt code_cert + end + +fun define_code_cert def_thm rsp_thm (rty, qty) lthy = + let + val quot_thm = Quotient_Term.prove_quot_theorem lthy (get_body_types (rty, qty)) + in + if Quotient_Type.can_generate_code_cert quot_thm then + let + val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty) + val add_abs_eqn_attribute = + Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I) + val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute); + in + lthy + |> (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert]) + end + else + lthy + end + +fun define_code_eq def_thm lthy = + let + val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm + val code_eq = unabs_all_def lthy unfolded_def + val simp_code_eq = simplify_code_eq lthy code_eq + in + lthy + |> (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [simp_code_eq]) + end + +fun define_code def_thm rsp_thm (rty, qty) lthy = + if body_type rty = body_type qty then + define_code_eq def_thm lthy + else + define_code_cert def_thm rsp_thm (rty, qty) lthy + (* The ML-interface for a quotient definition takes as argument: @@ -30,6 +158,7 @@ - attributes - the new constant as term - the rhs of the definition as term + - respectfulness theorem for the rhs It stores the qconst_info in the quotconsts data slot. @@ -45,7 +174,84 @@ quote str ^ " differs from declaration " ^ name ^ pos) end -fun gen_quotient_def prep_vars prep_term (raw_var, ((name, atts), (lhs_raw, rhs_raw))) lthy = +fun add_quotient_def ((var, (name, atts)), (lhs, rhs)) rsp_thm lthy = + let + val rty = fastype_of rhs + val qty = fastype_of lhs + val absrep_trm = + Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs + val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm)) + val (_, prop') = Local_Defs.cert_def lthy prop + val (_, newrhs) = Local_Defs.abs_def prop' + + val ((trm, (_ , def_thm)), lthy') = + Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy + + (* data storage *) + val qconst_data = {qconst = trm, rconst = rhs, def = def_thm} + fun get_rsp_thm_name (lhs_name, _) = Binding.suffix_name "_rsp" lhs_name + + val lthy'' = lthy' + |> Local_Theory.declaration {syntax = false, pervasive = true} + (fn phi => + (case Quotient_Info.transform_quotconsts phi qconst_data of + qcinfo as {qconst = Const (c, _), ...} => + Quotient_Info.update_quotconsts c qcinfo + | _ => I)) + |> (snd oo Local_Theory.note) + ((get_rsp_thm_name var, [Attrib.internal (K Quotient_Info.rsp_rules_add)]), + [rsp_thm]) + |> define_code def_thm rsp_thm (rty, qty) + + in + (qconst_data, lthy'') + end + +fun mk_readable_rsp_thm_eq tm lthy = + let + val ctm = cterm_of (Proof_Context.theory_of lthy) tm + + fun norm_fun_eq ctm = + let + fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy + fun erase_quants ctm' = + case (Thm.term_of ctm') of + Const ("HOL.eq", _) $ _ $ _ => Conv.all_conv ctm' + | _ => (Conv.binder_conv (K erase_quants) lthy then_conv + Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm' + in + (abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm + end + + fun simp_arrows_conv ctm = + let + val unfold_conv = Conv.rewrs_conv + [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]}, + @{thm fun_rel_def[THEN eq_reflection]}] + val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq + fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 + in + case (Thm.term_of ctm) of + Const (@{const_name "fun_rel"}, _) $ _ $ _ => + (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm + | _ => Conv.all_conv ctm + end + + val unfold_ret_val_invs = Conv.bottom_conv + (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy + val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv) + val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} + val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy + val beta_conv = Thm.beta_conversion true + val eq_thm = + (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm + in + Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2) + end + + + +fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy = let val (vars, ctxt) = prep_vars (the_list raw_var) lthy val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE) @@ -63,27 +269,50 @@ if Variable.check_name binding = lhs_str then (binding, mx) else error_msg binding lhs_str | _ => raise Match) - - val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs - val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm)) - val (_, prop') = Local_Defs.cert_def lthy prop - val (_, newrhs) = Local_Defs.abs_def prop' - - val ((trm, (_ , thm)), lthy') = - Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy + + fun try_to_prove_refl thm = + let + val lhs_eq = + thm + |> prop_of + |> Logic.dest_implies + |> fst + |> strip_all_body + |> try HOLogic.dest_Trueprop + in + case lhs_eq of + SOME (Const ("HOL.eq", _) $ _ $ _) => SOME (@{thm refl} RS thm) + | SOME _ => (case body_type (fastype_of lhs) of + Type (typ_name, _) => ( SOME + (#equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) + RS @{thm Equiv_Relations.equivp_reflp} RS thm) + handle _ => NONE) + | _ => NONE + ) + | _ => NONE + end - (* data storage *) - val qconst_data = {qconst = trm, rconst = rhs, def = thm} + val rsp_rel = Quotient_Term.equiv_relation lthy (fastype_of rhs, lhs_ty) + val internal_rsp_tm = HOLogic.mk_Trueprop (Syntax.check_term lthy (rsp_rel $ rhs $ rhs)) + val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy + val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq + val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq) + + fun after_qed thm_list lthy = + let + val internal_rsp_thm = + case thm_list of + [] => the maybe_proven_rsp_thm + | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm + (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1) + in + snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy) + end - val lthy'' = lthy' - |> Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => - (case Quotient_Info.transform_quotconsts phi qconst_data of - qcinfo as {qconst = Const (c, _), ...} => - Quotient_Info.update_quotconsts c qcinfo - | _ => I)); in - (qconst_data, lthy'') + case maybe_proven_rsp_thm of + SOME _ => Proof.theorem NONE after_qed [] lthy + | NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy end fun check_term' cnstr ctxt = @@ -103,16 +332,19 @@ val qty = Quotient_Term.derive_qtyp ctxt qtys rty val lhs = Free (qconst_name, qty) in - quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt + (*quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt*) + ({qconst = lhs, rconst = lhs, def = @{thm refl}}, ctxt) end -(* command *) +(* parser and command *) +val quotdef_parser = + Scan.option Parse_Spec.constdecl -- + Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term)) val _ = - Outer_Syntax.local_theory @{command_spec "quotient_definition"} + Outer_Syntax.local_theory_to_proof @{command_spec "quotient_definition"} "definition for constants over the quotient type" - (Scan.option Parse_Spec.constdecl -- - Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term)) - >> (snd oo quotient_def_cmd)) + (quotdef_parser >> quotient_def_cmd) + end; (* structure *) diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Tools/Quotient/quotient_info.ML --- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 23 16:16:35 2012 +0000 @@ -6,7 +6,7 @@ signature QUOTIENT_INFO = sig - type quotmaps = {relmap: string} + type quotmaps = {relmap: string, quot_thm: thm} val lookup_quotmaps: Proof.context -> string -> quotmaps option val lookup_quotmaps_global: theory -> string -> quotmaps option val print_quotmaps: Proof.context -> unit @@ -18,7 +18,7 @@ val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic val print_abs_rep: Proof.context -> unit - type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} + type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm} val transform_quotients: morphism -> quotients -> quotients val lookup_quotients: Proof.context -> string -> quotients option val lookup_quotients_global: theory -> string -> quotients option @@ -54,7 +54,7 @@ (* FIXME just one data slot (record) per program unit *) (* info about map- and rel-functions for a type *) -type quotmaps = {relmap: string} +type quotmaps = {relmap: string, quot_thm: thm} structure Quotmaps = Generic_Data ( @@ -71,19 +71,24 @@ val quotmaps_attribute_setup = Attrib.setup @{binding map} - ((Args.type_name true --| Scan.lift (@{keyword "="})) -- Args.const_proper true >> - (fn (tyname, relname) => - let val minfo = {relmap = relname} + ((Args.type_name true --| Scan.lift (@{keyword "="})) -- + (Scan.lift (@{keyword "("}) |-- Args.const_proper true --| Scan.lift (@{keyword ","}) -- + Attrib.thm --| Scan.lift (@{keyword ")"})) >> + (fn (tyname, (relname, qthm)) => + let val minfo = {relmap = relname, quot_thm = qthm} in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end)) "declaration of map information" fun print_quotmaps ctxt = let - fun prt_map (ty_name, {relmap}) = + fun prt_map (ty_name, {relmap, quot_thm}) = Pretty.block (separate (Pretty.brk 2) - (map Pretty.str - ["type:", ty_name, - "relation map:", relmap])) + [Pretty.str "type:", + Pretty.str ty_name, + Pretty.str "relation map:", + Pretty.str relmap, + Pretty.str "quot. theorem:", + Syntax.pretty_term ctxt (prop_of quot_thm)]) in map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt))) |> Pretty.big_list "maps for type constructors:" @@ -125,7 +130,7 @@ end (* info about quotient types *) -type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} +type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm} structure Quotients = Generic_Data ( @@ -135,11 +140,12 @@ fun merge data = Symtab.merge (K true) data ) -fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm} = +fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} = {qtyp = Morphism.typ phi qtyp, rtyp = Morphism.typ phi rtyp, equiv_rel = Morphism.term phi equiv_rel, - equiv_thm = Morphism.thm phi equiv_thm} + equiv_thm = Morphism.thm phi equiv_thm, + quot_thm = Morphism.thm phi quot_thm} val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory @@ -151,7 +157,7 @@ fun print_quotients ctxt = let - fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = + fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} = Pretty.block (separate (Pretty.brk 2) [Pretty.str "quotient type:", Syntax.pretty_typ ctxt qtyp, @@ -160,7 +166,9 @@ Pretty.str "relation:", Syntax.pretty_term ctxt equiv_rel, Pretty.str "equiv. thm:", - Syntax.pretty_term ctxt (prop_of equiv_thm)]) + Syntax.pretty_term ctxt (prop_of equiv_thm), + Pretty.str "quot. thm:", + Syntax.pretty_term ctxt (prop_of quot_thm)]) in map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt))) |> Pretty.big_list "quotients:" diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Mar 23 16:16:35 2012 +0000 @@ -20,6 +20,9 @@ val equiv_relation: Proof.context -> typ * typ -> term val equiv_relation_chk: Proof.context -> typ * typ -> term + val get_rel_from_quot_thm: thm -> term + val prove_quot_theorem: Proof.context -> typ * typ -> thm + val regularize_trm: Proof.context -> term * term -> term val regularize_trm_chk: Proof.context -> term * term -> term @@ -72,9 +75,6 @@ fun defined_mapfun_data ctxt s = Symtab.defined (Enriched_Type.entries ctxt) s - -(* makes a Free out of a TVar *) -fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) (* looks up the (varified) rty and qty for a quotient definition @@ -279,35 +279,10 @@ SOME map_data => Const (#relmap map_data, dummyT) | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")) -(* takes two type-environments and looks - up in both of them the variable v, which - must be listed in the environment -*) -fun double_lookup rtyenv qtyenv v = - let - val v' = fst (dest_TVar v) - in - (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) - end - -fun mk_relmap ctxt vs rty = - let - val vs' = map (mk_Free) vs - - fun mk_relmap_aux rty = - case rty of - TVar _ => mk_Free rty - | Type (_, []) => HOLogic.eq_const rty - | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys) - | _ => raise LIFT_MATCH ("mk_relmap (default)") - in - fold_rev Term.lambda vs' (mk_relmap_aux rty) - end - fun get_equiv_rel thy s = (case Quotient_Info.lookup_quotients thy s of SOME qdata => #equiv_rel qdata - | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")) + | NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")")) fun equiv_match_err ctxt ty_pat ty = let @@ -336,11 +311,10 @@ end else let - val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' - val rtyenv = match ctxt equiv_match_err rty_pat rty + val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s' val qtyenv = match ctxt equiv_match_err qty_pat qty - val args_aux = map (double_lookup rtyenv qtyenv) vs - val args = map (equiv_relation ctxt) args_aux + val rtys' = map (Envir.subst_type qtyenv) rtys + val args = map (equiv_relation ctxt) (tys ~~ rtys') val eqv_rel = get_equiv_rel ctxt s' val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) in @@ -348,8 +322,7 @@ then eqv_rel' else let - val rel_map = mk_relmap ctxt vs rty_pat - val result = list_comb (rel_map, args) + val result = list_comb (get_relmap ctxt s, args) in mk_rel_compose (result, eqv_rel') end @@ -361,6 +334,78 @@ equiv_relation ctxt (rty, qty) |> Syntax.check_term ctxt +(* generation of the Quotient theorem *) + +fun get_quot_thm ctxt s = + let + val thy = Proof_Context.theory_of ctxt + in + (case Quotient_Info.lookup_quotients_global thy s of + SOME qdata => #quot_thm qdata + | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")) + end + +fun get_rel_quot_thm thy s = + (case Quotient_Info.lookup_quotmaps thy s of + SOME map_data => #quot_thm map_data + | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")); + +fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient}) + +infix 0 MRSL + +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm + +exception NOT_IMPL of string + +fun get_rel_from_quot_thm quot_thm = + let + val (_ $ rel $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) quot_thm + in + rel + end + +fun mk_quot_thm_compose (rel_quot_thm, quot_thm) = + let + val quot_thm_rel = get_rel_from_quot_thm quot_thm + in + if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient} + else raise NOT_IMPL "nested quotients: not implemented yet" + end + +fun prove_quot_theorem ctxt (rty, qty) = + if rty = qty + then @{thm identity_quotient} + else + case (rty, qty) of + (Type (s, tys), Type (s', tys')) => + if s = s' + then + let + val args = map (prove_quot_theorem ctxt) (tys ~~ tys') + in + args MRSL (get_rel_quot_thm ctxt s) + end + else + let + val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s' + val qtyenv = match ctxt equiv_match_err qty_pat qty + val rtys' = map (Envir.subst_type qtyenv) rtys + val args = map (prove_quot_theorem ctxt) (tys ~~ rtys') + val quot_thm = get_quot_thm ctxt s' + in + if forall is_id_quot args + then + quot_thm + else + let + val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s) + in + mk_quot_thm_compose (rel_quot_thm, quot_thm) + end + end + | _ => @{thm identity_quotient} + (*** Regularization ***) diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 23 16:16:35 2012 +0000 @@ -6,6 +6,8 @@ signature QUOTIENT_TYPE = sig + val can_generate_code_cert: thm -> bool + val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * ((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory @@ -25,7 +27,7 @@ val mem_def1 = @{lemma "y : Collect S ==> S y" by simp} val mem_def2 = @{lemma "S y ==> y : Collect S" by simp} -(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) +(* constructs the term {c. EX (x::rty). rel x x \ c = Collect (rel x)} *) fun typedef_term rel rty lthy = let val [x, c] = @@ -76,6 +78,44 @@ Goal.prove lthy [] [] goal (K (typedef_quot_type_tac equiv_thm typedef_info)) end + +fun can_generate_code_cert quot_thm = + case Quotient_Term.get_rel_from_quot_thm quot_thm of + Const (@{const_name HOL.eq}, _) => true + | Const (@{const_name invariant}, _) $ _ => true + | _ => false + +fun define_abs_type quot_thm lthy = + if can_generate_code_cert quot_thm then + let + val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep} + val add_abstype_attribute = + Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I) + val add_abstype_attrib = Attrib.internal (K add_abstype_attribute); + in + lthy + |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm]) + end + else + lthy + +fun init_quotient_infr quot_thm equiv_thm lthy = + let + val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm + val (qtyp, rtyp) = (dest_funT o fastype_of) rep + val qty_full_name = (fst o dest_Type) qtyp + val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm, + quot_thm = quot_thm } + fun quot_info phi = Quotient_Info.transform_quotients phi quotients + val abs_rep = {abs = abs, rep = rep} + fun abs_rep_info phi = Quotient_Info.transform_abs_rep phi abs_rep + in + lthy + |> Local_Theory.declaration {syntax = false, pervasive = true} + (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi) + #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi)) + |> define_abs_type quot_thm + end (* main function for constructing a quotient type *) fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), equiv_thm) lthy = @@ -86,7 +126,7 @@ else equiv_thm RS @{thm equivp_implies_part_equivp} (* generates the typedef *) - val ((qty_full_name, typedef_info), lthy1) = + val ((_, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy (* abs and rep functions from the typedef *) @@ -108,9 +148,9 @@ NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name) | SOME morphs => morphs) - val ((abs_t, (_, abs_def)), lthy2) = lthy1 + val ((_, (_, abs_def)), lthy2) = lthy1 |> Local_Theory.define ((abs_name, NoSyn), ((Thm.def_binding abs_name, []), abs_trm)) - val ((rep_t, (_, rep_def)), lthy3) = lthy2 + val ((_, (_, rep_def)), lthy3) = lthy2 |> Local_Theory.define ((rep_name, NoSyn), ((Thm.def_binding rep_name, []), rep_trm)) (* quot_type theorem *) @@ -126,15 +166,11 @@ val equiv_thm_name = Binding.suffix_name "_equivp" qty_name (* storing the quotients *) - val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} - - fun qinfo phi = Quotient_Info.transform_quotients phi quotients - fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t} + val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm, + quot_thm = quotient_thm} val lthy4 = lthy3 - |> Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi) - #> Quotient_Info.update_abs_rep qty_full_name (abs_rep phi)) + |> init_quotient_infr quotient_thm equiv_thm |> (snd oo Local_Theory.note) ((equiv_thm_name, if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]), @@ -264,15 +300,43 @@ val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false +val quotspec_parser = + Parse.and_list1 + ((Parse.type_args -- Parse.binding) -- + (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) + Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- + (@{keyword "/"} |-- (partial -- Parse.term)) -- + Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))) + val _ = Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"} "quotient type definitions (require equivalence proofs)" - (Parse.and_list1 - ((Parse.type_args -- Parse.binding) -- - (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) - Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- - (@{keyword "/"} |-- (partial -- Parse.term)) -- - Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))) - >> quotient_type_cmd) + (quotspec_parser >> quotient_type_cmd) + +(* Setup lifting using type_def_thm *) + +exception SETUP_LIFT_TYPE of string + +fun setup_lift_type typedef_thm = + let + val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm + val (quot_thm, equivp_thm) = (case typedef_set of + Const ("Orderings.top_class.top", _) => + (typedef_thm RS @{thm copy_type_to_Quotient}, + typedef_thm RS @{thm copy_type_to_equivp}) + | Const (@{const_name "Collect"}, _) $ Abs (_, _, _ $ Bound 0) => + (typedef_thm RS @{thm invariant_type_to_Quotient}, + typedef_thm RS @{thm invariant_type_to_part_equivp}) + | _ => raise SETUP_LIFT_TYPE "unsupported typedef theorem") + in + init_quotient_infr quot_thm equivp_thm + end + +fun setup_lift_type_aux xthm lthy = setup_lift_type (singleton (Attrib.eval_thms lthy) xthm) lthy + +val _ = + Outer_Syntax.local_theory @{command_spec "setup_lifting"} + "Setup lifting infrastracture" + (Parse_Spec.xthm >> (fn xthm => setup_lift_type_aux xthm)) end; diff -r ded5cc757bc9 -r b846c299f412 src/HOL/Unix/Unix.thy --- a/src/HOL/Unix/Unix.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/Unix/Unix.thy Fri Mar 23 16:16:35 2012 +0000 @@ -843,7 +843,9 @@ neither owned nor writable by @{term user\<^isub>1}. *} -definition + + +definition invariant where "invariant root path = (\att dir. access root path user\<^isub>1 {} = Some (Env att dir) \ dir \ empty \ diff -r ded5cc757bc9 -r b846c299f412 src/HOL/ex/Executable_Relation.thy --- a/src/HOL/ex/Executable_Relation.thy Fri Mar 23 16:16:15 2012 +0000 +++ b/src/HOL/ex/Executable_Relation.thy Fri Mar 23 16:16:35 2012 +0000 @@ -12,6 +12,7 @@ "(x, y) : (rel_raw X R) = ((x = y \ x : X) \ (x, y) : R)" unfolding rel_raw_def by auto + lemma Id_raw: "Id = rel_raw UNIV {}" unfolding rel_raw_def by auto @@ -74,36 +75,34 @@ lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"] -definition rel :: "'a set => ('a * 'a) set => 'a rel" -where - "rel X R = rel_of_set (rel_raw X R)" +quotient_definition rel where "rel :: 'a set => ('a * 'a) set => 'a rel" is rel_raw done subsubsection {* Constant definitions on relations *} hide_const (open) converse rel_comp rtrancl Image quotient_definition member :: "'a * 'a => 'a rel => bool" where - "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" + "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done quotient_definition converse :: "'a rel => 'a rel" where - "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set" + "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set" done quotient_definition union :: "'a rel => 'a rel => 'a rel" where - "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" + "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel" where - "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" + "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done quotient_definition rtrancl :: "'a rel => 'a rel" where - "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" + "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" done quotient_definition Image :: "'a rel => 'a set => 'a set" where - "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set" + "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set" done subsubsection {* Code generation *} @@ -111,33 +110,27 @@ lemma [code]: "member (x, y) (rel X R) = ((x = y \ x : X) \ (x, y) : R)" -unfolding rel_def member_def -by (simp add: member_raw) +by (lifting member_raw) lemma [code]: "converse (rel X R) = rel X (R^-1)" -unfolding rel_def converse_def -by (simp add: converse_raw) +by (lifting converse_raw) lemma [code]: "union (rel X R) (rel Y S) = rel (X Un Y) (R Un S)" -unfolding rel_def union_def -by (simp add: union_raw) +by (lifting union_raw) lemma [code]: "rel_comp (rel X R) (rel Y S) = rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))" -unfolding rel_def rel_comp_def -by (simp add: rel_comp_raw) +by (lifting rel_comp_raw) lemma [code]: "rtrancl (rel X R) = rel UNIV (R^+)" -unfolding rel_def rtrancl_def -by (simp add: rtrancl_raw) +by (lifting rtrancl_raw) lemma [code]: "Image (rel X R) S = (X Int S) Un (R `` S)" -unfolding rel_def Image_def -by (simp add: Image_raw) +by (lifting Image_raw) quickcheck_generator rel constructors: rel