# HG changeset patch # User huffman # Date 1333479392 -7200 # Node ID dac11ab962771c578848170e7812dbad7e6e03e9 # Parent 432b29a96f610fdf94c7c469111b0dccbefd0190# Parent 15428dd82b54d9d5fcff92f92e96803477cb0ca6 merged diff -r 432b29a96f61 -r dac11ab96277 Admin/isatest/isatest-settings --- a/Admin/isatest/isatest-settings Tue Apr 03 15:15:00 2012 +0200 +++ b/Admin/isatest/isatest-settings Tue Apr 03 20:56:32 2012 +0200 @@ -25,7 +25,8 @@ hoelzl@in.tum.de \ krauss@in.tum.de \ noschinl@in.tum.de \ -kuncar@in.tum.de" +kuncar@in.tum.de \ +ns441@cam.ac.uk" LOGPREFIX=$HOME/log MASTERLOG=$LOGPREFIX/isatest.log diff -r 432b29a96f61 -r dac11ab96277 etc/isar-keywords.el --- a/etc/isar-keywords.el Tue Apr 03 15:15:00 2012 +0200 +++ b/etc/isar-keywords.el Tue Apr 03 20:56:32 2012 +0200 @@ -190,7 +190,9 @@ "print_orders" "print_quotconsts" "print_quotients" + "print_quotientsQ3" "print_quotmaps" + "print_quotmapsQ3" "print_rules" "print_simpset" "print_statement" @@ -403,7 +405,9 @@ "print_orders" "print_quotconsts" "print_quotients" + "print_quotientsQ3" "print_quotmaps" + "print_quotmapsQ3" "print_rules" "print_simpset" "print_statement" diff -r 432b29a96f61 -r dac11ab96277 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/IsaMakefile Tue Apr 03 20:56:32 2012 +0200 @@ -281,6 +281,7 @@ Hilbert_Choice.thy \ Int.thy \ Lazy_Sequence.thy \ + Lifting.thy \ List.thy \ Main.thy \ Map.thy \ @@ -315,6 +316,10 @@ Tools/code_evaluation.ML \ Tools/groebner.ML \ Tools/int_arith.ML \ + Tools/Lifting/lifting_def.ML \ + Tools/Lifting/lifting_info.ML \ + Tools/Lifting/lifting_term.ML \ + Tools/Lifting/lifting_setup.ML \ Tools/list_code.ML \ Tools/list_to_set_comprehension.ML \ Tools/nat_numeral_simprocs.ML \ @@ -1036,7 +1041,8 @@ $(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy \ Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy \ Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy \ - Isar_Examples/Group.thy Isar_Examples/Hoare.thy \ + Isar_Examples/Group.thy Isar_Examples/Group_Context.thy \ + Isar_Examples/Group_Notepad.thy Isar_Examples/Hoare.thy \ Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy \ Isar_Examples/Mutilated_Checkerboard.thy \ Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy \ @@ -1495,7 +1501,7 @@ Quotient_Examples/FSet.thy \ Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \ Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \ - Quotient_Examples/Lift_Fun.thy + Quotient_Examples/Lift_Fun.thy Quotient_Examples/Lift_DList.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Isar_Examples/Group_Context.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_Examples/Group_Context.thy Tue Apr 03 20:56:32 2012 +0200 @@ -0,0 +1,94 @@ +(* Title: HOL/Isar_Examples/Group_Context.thy + Author: Makarius +*) + +header {* Some algebraic identities derived from group axioms -- theory context version *} + +theory Group_Context +imports Main +begin + +text {* hypothetical group axiomatization *} + +context + fixes prod :: "'a \ 'a \ 'a" (infixl "**" 70) + and one :: "'a" + and inverse :: "'a => 'a" + assumes assoc: "\x y z. (x ** y) ** z = x ** (y ** z)" + and left_one: "\x. one ** x = x" + and left_inverse: "\x. inverse x ** x = one" +begin + +text {* some consequences *} + +lemma right_inverse: "x ** inverse x = one" +proof - + have "x ** inverse x = one ** (x ** inverse x)" + by (simp only: left_one) + also have "\ = one ** x ** inverse x" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** inverse x ** x ** inverse x" + by (simp only: left_inverse) + also have "\ = inverse (inverse x) ** (inverse x ** x) ** inverse x" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** one ** inverse x" + by (simp only: left_inverse) + also have "\ = inverse (inverse x) ** (one ** inverse x)" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** inverse x" + by (simp only: left_one) + also have "\ = one" + by (simp only: left_inverse) + finally show "x ** inverse x = one" . +qed + +lemma right_one: "x ** one = x" +proof - + have "x ** one = x ** (inverse x ** x)" + by (simp only: left_inverse) + also have "\ = x ** inverse x ** x" + by (simp only: assoc) + also have "\ = one ** x" + by (simp only: right_inverse) + also have "\ = x" + by (simp only: left_one) + finally show "x ** one = x" . +qed + +lemma one_equality: "e ** x = x \ one = e" +proof - + fix e x + assume eq: "e ** x = x" + have "one = x ** inverse x" + by (simp only: right_inverse) + also have "\ = (e ** x) ** inverse x" + by (simp only: eq) + also have "\ = e ** (x ** inverse x)" + by (simp only: assoc) + also have "\ = e ** one" + by (simp only: right_inverse) + also have "\ = e" + by (simp only: right_one) + finally show "one = e" . +qed + +lemma inverse_equality: "x' ** x = one \ inverse x = x'" +proof - + fix x x' + assume eq: "x' ** x = one" + have "inverse x = one ** inverse x" + by (simp only: left_one) + also have "\ = (x' ** x) ** inverse x" + by (simp only: eq) + also have "\ = x' ** (x ** inverse x)" + by (simp only: assoc) + also have "\ = x' ** one" + by (simp only: right_inverse) + also have "\ = x'" + by (simp only: right_one) + finally show "inverse x = x'" . +qed + +end + +end diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Isar_Examples/Group_Notepad.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_Examples/Group_Notepad.thy Tue Apr 03 20:56:32 2012 +0200 @@ -0,0 +1,96 @@ +(* Title: HOL/Isar_Examples/Group_Notepad.thy + Author: Makarius +*) + +header {* Some algebraic identities derived from group axioms -- proof notepad version *} + +theory Group_Notepad +imports Main +begin + +notepad +begin + txt {* hypothetical group axiomatization *} + + fix prod :: "'a \ 'a \ 'a" (infixl "**" 70) + and one :: "'a" + and inverse :: "'a => 'a" + assume assoc: "\x y z. (x ** y) ** z = x ** (y ** z)" + and left_one: "\x. one ** x = x" + and left_inverse: "\x. inverse x ** x = one" + + txt {* some consequences *} + + have right_inverse: "\x. x ** inverse x = one" + proof - + fix x + have "x ** inverse x = one ** (x ** inverse x)" + by (simp only: left_one) + also have "\ = one ** x ** inverse x" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** inverse x ** x ** inverse x" + by (simp only: left_inverse) + also have "\ = inverse (inverse x) ** (inverse x ** x) ** inverse x" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** one ** inverse x" + by (simp only: left_inverse) + also have "\ = inverse (inverse x) ** (one ** inverse x)" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** inverse x" + by (simp only: left_one) + also have "\ = one" + by (simp only: left_inverse) + finally show "x ** inverse x = one" . + qed + + have right_one: "\x. x ** one = x" + proof - + fix x + have "x ** one = x ** (inverse x ** x)" + by (simp only: left_inverse) + also have "\ = x ** inverse x ** x" + by (simp only: assoc) + also have "\ = one ** x" + by (simp only: right_inverse) + also have "\ = x" + by (simp only: left_one) + finally show "x ** one = x" . + qed + + have one_equality: "\e x. e ** x = x \ one = e" + proof - + fix e x + assume eq: "e ** x = x" + have "one = x ** inverse x" + by (simp only: right_inverse) + also have "\ = (e ** x) ** inverse x" + by (simp only: eq) + also have "\ = e ** (x ** inverse x)" + by (simp only: assoc) + also have "\ = e ** one" + by (simp only: right_inverse) + also have "\ = e" + by (simp only: right_one) + finally show "one = e" . + qed + + have inverse_equality: "\x x'. x' ** x = one \ inverse x = x'" + proof - + fix x x' + assume eq: "x' ** x = one" + have "inverse x = one ** inverse x" + by (simp only: left_one) + also have "\ = (x' ** x) ** inverse x" + by (simp only: eq) + also have "\ = x' ** (x ** inverse x)" + by (simp only: assoc) + also have "\ = x' ** one" + by (simp only: right_inverse) + also have "\ = x'" + by (simp only: right_one) + finally show "inverse x = x'" . + qed + +end + +end diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Library/DAList.thy --- a/src/HOL/Library/DAList.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Library/DAList.thy Tue Apr 03 20:56:32 2012 +0200 @@ -39,33 +39,29 @@ subsection {* Primitive operations *} -(* FIXME: improve quotient_definition so that type annotations on the right hand sides can be removed *) - -quotient_definition lookup :: "('key, 'value) alist \ 'key \ 'value option" -where "lookup" is "map_of :: ('key * 'value) list \ 'key \ 'value option" .. +lift_definition lookup :: "('key, 'value) alist \ 'key \ 'value option" is map_of .. -quotient_definition empty :: "('key, 'value) alist" -where "empty" is "[] :: ('key * 'value) list" by simp +lift_definition empty :: "('key, 'value) alist" is "[]" by simp -quotient_definition update :: "'key \ 'value \ ('key, 'value) alist \ ('key, 'value) alist" -where "update" is "AList.update :: 'key \ 'value \ ('key * 'value) list \ ('key * 'value) list" +lift_definition update :: "'key \ 'value \ ('key, 'value) alist \ ('key, 'value) alist" + is AList.update by (simp add: distinct_update) (* FIXME: we use an unoptimised delete operation. *) -quotient_definition delete :: "'key \ ('key, 'value) alist \ ('key, 'value) alist" -where "delete" is "AList.delete :: 'key \ ('key * 'value) list \ ('key * 'value) list" +lift_definition delete :: "'key \ ('key, 'value) alist \ ('key, 'value) alist" + is AList.delete by (simp add: distinct_delete) -quotient_definition map_entry :: "'key \ ('value \ 'value) \ ('key, 'value) alist \ ('key, 'value) alist" -where "map_entry" is "AList.map_entry :: 'key \ ('value \ 'value) \ ('key * 'value) list \ ('key * 'value) list" +lift_definition map_entry :: "'key \ ('value \ 'value) \ ('key, 'value) alist \ ('key, 'value) alist" + is AList.map_entry by (simp add: distinct_map_entry) -quotient_definition filter :: "('key \ 'value \ bool) \ ('key, 'value) alist \ ('key, 'value) alist" -where "filter" is "List.filter :: ('key \ 'value \ bool) \ ('key * 'value) list \ ('key * 'value) list" +lift_definition filter :: "('key \ 'value \ bool) \ ('key, 'value) alist \ ('key, 'value) alist" + is List.filter by (simp add: distinct_map_fst_filter) -quotient_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist" -where "map_default" is "AList.map_default :: 'key => 'value => ('value => 'value) => ('key * 'value) list => ('key * 'value) list" +lift_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist" + is AList.map_default by (simp add: distinct_map_default) subsection {* Abstract operation properties *} diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Library/Multiset.thy Tue Apr 03 20:56:32 2012 +0200 @@ -1111,14 +1111,12 @@ text {* Operations on alists with distinct keys *} -quotient_definition join :: "('a \ 'b \ 'b \ 'b) \ ('a, 'b) alist \ ('a, 'b) alist \ ('a, 'b) alist" -where - "join" is "join_raw :: ('a \ 'b \ 'b \ 'b) \ ('a \ 'b) list \ ('a \ 'b) list \ ('a \ 'b) list" +lift_definition join :: "('a \ 'b \ 'b \ 'b) \ ('a, 'b) alist \ ('a, 'b) alist \ ('a, 'b) alist" +is join_raw by (simp add: distinct_join_raw) -quotient_definition subtract_entries :: "('a, ('b :: minus)) alist \ ('a, 'b) alist \ ('a, 'b) alist" -where - "subtract_entries" is "subtract_entries_raw :: ('a \ 'b) list \ ('a \ 'b) list \ ('a \ 'b) list" +lift_definition subtract_entries :: "('a, ('b :: minus)) alist \ ('a, 'b) alist \ ('a, 'b) alist" +is subtract_entries_raw by (simp add: distinct_subtract_entries_raw) text {* Implementing multisets by means of association lists *} diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Library/Quotient_List.thy Tue Apr 03 20:56:32 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Library/Quotient_List.thy +(* Title: HOL/Library/Quotient3_List.thy Author: Cezary Kaliszyk and Christian Urban *) @@ -56,63 +56,63 @@ "equivp R \ equivp (list_all2 R)" by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE) -lemma list_quotient [quot_thm]: - assumes "Quotient R Abs Rep" - shows "Quotient (list_all2 R) (map Abs) (map Rep)" -proof (rule QuotientI) - from assms have "\x. Abs (Rep x) = x" by (rule Quotient_abs_rep) +lemma list_quotient3 [quot_thm]: + assumes "Quotient3 R Abs Rep" + shows "Quotient3 (list_all2 R) (map Abs) (map Rep)" +proof (rule Quotient3I) + from assms have "\x. Abs (Rep x) = x" by (rule Quotient3_abs_rep) then show "\xs. map Abs (map Rep xs) = xs" by (simp add: comp_def) next - from assms have "\x y. R (Rep x) (Rep y) \ x = y" by (rule Quotient_rel_rep) + from assms have "\x y. R (Rep x) (Rep y) \ x = y" by (rule Quotient3_rel_rep) then show "\xs. list_all2 R (map Rep xs) (map Rep xs)" by (simp add: list_all2_map1 list_all2_map2 list_all2_eq) next fix xs ys - from assms have "\x y. R x x \ R y y \ Abs x = Abs y \ R x y" by (rule Quotient_rel) + from assms have "\x y. R x x \ R y y \ Abs x = Abs y \ R x y" by (rule Quotient3_rel) then show "list_all2 R xs ys \ list_all2 R xs xs \ list_all2 R ys ys \ map Abs xs = map Abs ys" by (induct xs ys rule: list_induct2') auto qed -declare [[map list = (list_all2, list_quotient)]] +declare [[mapQ3 list = (list_all2, list_quotient3)]] lemma cons_prs [quot_preserve]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" - by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q]) + by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q]) lemma cons_rsp [quot_respect]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)" by auto lemma nil_prs [quot_preserve]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "map Abs [] = []" by simp lemma nil_rsp [quot_respect]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "list_all2 R [] []" by simp lemma map_prs_aux: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" by (induct l) - (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) lemma map_prs [quot_preserve]: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" and "((abs1 ---> id) ---> map rep1 ---> id) map = map" by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def) - (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) lemma map_rsp [quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map" and "((R1 ===> op =) ===> (list_all2 R1) ===> op =) map map" apply (simp_all add: fun_rel_def) @@ -124,35 +124,35 @@ done lemma foldr_prs_aux: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" - by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + by (induct l) (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) lemma foldr_prs [quot_preserve]: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" apply (simp add: fun_eq_iff) by (simp only: fun_eq_iff foldr_prs_aux[OF a b]) (simp) lemma foldl_prs_aux: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" - by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + by (induct l arbitrary:e) (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b]) lemma foldl_prs [quot_preserve]: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" + assumes a: "Quotient3 R1 abs1 rep1" + and b: "Quotient3 R2 abs2 rep2" shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" by (simp add: fun_eq_iff foldl_prs_aux [OF a b]) (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) lemma foldl_rsp[quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_all2 R2 ===> R1) foldl foldl" apply(auto simp add: fun_rel_def) apply (erule_tac P="R1 xa ya" in rev_mp) @@ -162,8 +162,8 @@ done lemma foldr_rsp[quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "((R1 ===> R2 ===> R2) ===> list_all2 R1 ===> R2 ===> R2) foldr foldr" apply (auto simp add: fun_rel_def) apply (erule list_all2_induct, simp_all) @@ -183,18 +183,18 @@ by (simp add: list_all2_rsp fun_rel_def) lemma [quot_preserve]: - assumes a: "Quotient R abs1 rep1" + assumes a: "Quotient3 R abs1 rep1" shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2" apply (simp add: fun_eq_iff) apply clarify apply (induct_tac xa xb rule: list_induct2') - apply (simp_all add: Quotient_abs_rep[OF a]) + apply (simp_all add: Quotient3_abs_rep[OF a]) done lemma [quot_preserve]: - assumes a: "Quotient R abs1 rep1" + assumes a: "Quotient3 R abs1 rep1" shows "(list_all2 ((rep1 ---> rep1 ---> id) R) l m) = (l = m)" - by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a]) + by (induct l m rule: list_induct2') (simp_all add: Quotient3_rel_rep[OF a]) lemma list_all2_find_element: assumes a: "x \ set a" @@ -207,4 +207,48 @@ shows "list_all2 R x x" by (induct x) (auto simp add: a) +lemma list_quotient: + assumes "Quotient R Abs Rep T" + shows "Quotient (list_all2 R) (List.map Abs) (List.map Rep) (list_all2 T)" +proof (rule QuotientI) + from assms have "\x. Abs (Rep x) = x" by (rule Quotient_abs_rep) + then show "\xs. List.map Abs (List.map Rep xs) = xs" by (simp add: comp_def) +next + from assms have "\x y. R (Rep x) (Rep y) \ x = y" by (rule Quotient_rel_rep) + then show "\xs. list_all2 R (List.map Rep xs) (List.map Rep xs)" + by (simp add: list_all2_map1 list_all2_map2 list_all2_eq) +next + fix xs ys + from assms have "\x y. R x x \ R y y \ Abs x = Abs y \ R x y" by (rule Quotient_rel) + then show "list_all2 R xs ys \ list_all2 R xs xs \ list_all2 R ys ys \ List.map Abs xs = List.map Abs ys" + by (induct xs ys rule: list_induct2') auto +next + { + fix l1 l2 + have "List.length l1 = List.length l2 \ + (\(x, y)\set (zip l1 l1). R x y) = (\(x, y)\set (zip l1 l2). R x x)" + by (induction rule: list_induct2) auto + } note x = this + { + fix f g + have "list_all2 (\x y. f x y \ g x y) = (\ x y. list_all2 f x y \ list_all2 g x y)" + by (intro ext) (auto simp add: list_all2_def) + } note list_all2_conj = this + from assms have t: "T = (\x y. R x x \ Abs x = y)" by (rule Quotient_cr_rel) + show "list_all2 T = (\x y. list_all2 R x x \ List.map Abs x = y)" + apply (simp add: t list_all2_conj[symmetric]) + apply (rule sym) + apply (simp add: list_all2_conj) + apply(intro ext) + apply (intro rev_conj_cong) + unfolding list_all2_def apply (metis List.list_all2_eq list_all2_def list_all2_map1) + apply (drule conjunct1) + apply (intro conj_cong) + apply simp + apply(simp add: x) + done +qed + +declare [[map list = (list_all2, list_quotient)]] + end diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Library/Quotient_Option.thy Tue Apr 03 20:56:32 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Library/Quotient_Option.thy +(* Title: HOL/Library/Quotient3_Option.thy Author: Cezary Kaliszyk and Christian Urban *) @@ -55,36 +55,36 @@ by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE) lemma option_quotient [quot_thm]: - assumes "Quotient R Abs Rep" - shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" - apply (rule QuotientI) - apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms]) - using Quotient_rel [OF assms] + assumes "Quotient3 R Abs Rep" + shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)" + apply (rule Quotient3I) + apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms]) + using Quotient3_rel [OF assms] apply (simp add: option_rel_unfold split: option.split) done -declare [[map option = (option_rel, option_quotient)]] +declare [[mapQ3 option = (option_rel, option_quotient)]] lemma option_None_rsp [quot_respect]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "option_rel R None None" by simp lemma option_Some_rsp [quot_respect]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(R ===> option_rel R) Some Some" by auto lemma option_None_prs [quot_preserve]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "Option.map Abs None = None" by simp lemma option_Some_prs [quot_preserve]: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(Rep ---> Option.map Abs) Some = Some" apply(simp add: fun_eq_iff) - apply(simp add: Quotient_abs_rep[OF q]) + apply(simp add: Quotient3_abs_rep[OF q]) done end diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Library/Quotient_Product.thy Tue Apr 03 20:56:32 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Library/Quotient_Product.thy +(* Title: HOL/Library/Quotient3_Product.thy Author: Cezary Kaliszyk and Christian Urban *) @@ -32,56 +32,56 @@ using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE) lemma prod_quotient [quot_thm]: - assumes "Quotient R1 Abs1 Rep1" - assumes "Quotient R2 Abs2 Rep2" - shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)" - apply (rule QuotientI) + assumes "Quotient3 R1 Abs1 Rep1" + assumes "Quotient3 R2 Abs2 Rep2" + shows "Quotient3 (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)" + apply (rule Quotient3I) apply (simp add: map_pair.compositionality comp_def map_pair.identity - Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)]) - apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)]) - using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)] + Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)]) + apply (simp add: split_paired_all Quotient3_rel_rep [OF assms(1)] Quotient3_rel_rep [OF assms(2)]) + using Quotient3_rel [OF assms(1)] Quotient3_rel [OF assms(2)] apply (auto simp add: split_paired_all) done -declare [[map prod = (prod_rel, prod_quotient)]] +declare [[mapQ3 prod = (prod_rel, prod_quotient)]] lemma Pair_rsp [quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" by (auto simp add: prod_rel_def) lemma Pair_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair" apply(simp add: fun_eq_iff) - apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + apply(simp add: Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) done lemma fst_rsp [quot_respect]: - assumes "Quotient R1 Abs1 Rep1" - assumes "Quotient R2 Abs2 Rep2" + assumes "Quotient3 R1 Abs1 Rep1" + assumes "Quotient3 R2 Abs2 Rep2" shows "(prod_rel R1 R2 ===> R1) fst fst" by auto lemma fst_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst" - by (simp add: fun_eq_iff Quotient_abs_rep[OF q1]) + by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1]) lemma snd_rsp [quot_respect]: - assumes "Quotient R1 Abs1 Rep1" - assumes "Quotient R2 Abs2 Rep2" + assumes "Quotient3 R1 Abs1 Rep1" + assumes "Quotient3 R2 Abs2 Rep2" shows "(prod_rel R1 R2 ===> R2) snd snd" by auto lemma snd_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd" - by (simp add: fun_eq_iff Quotient_abs_rep[OF q2]) + by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2]) lemma split_rsp [quot_respect]: shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" @@ -89,10 +89,10 @@ by auto lemma split_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split" - by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) lemma [quot_respect]: shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> @@ -100,11 +100,11 @@ by (auto simp add: fun_rel_def) lemma [quot_preserve]: - assumes q1: "Quotient R1 abs1 rep1" - and q2: "Quotient R2 abs2 rep2" + assumes q1: "Quotient3 R1 abs1 rep1" + and q2: "Quotient3 R2 abs2 rep2" shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) ---> map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel" - by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) lemma [quot_preserve]: shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2) diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Tue Apr 03 20:56:32 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Library/Quotient_Set.thy +(* Title: HOL/Library/Quotient3_Set.thy Author: Cezary Kaliszyk and Christian Urban *) @@ -9,77 +9,77 @@ begin lemma set_quotient [quot_thm]: - assumes "Quotient R Abs Rep" - shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)" -proof (rule QuotientI) - from assms have "\x. Abs (Rep x) = x" by (rule Quotient_abs_rep) + assumes "Quotient3 R Abs Rep" + shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)" +proof (rule Quotient3I) + from assms have "\x. Abs (Rep x) = x" by (rule Quotient3_abs_rep) then show "\xs. Rep -` (Abs -` xs) = xs" unfolding vimage_def by auto next show "\xs. set_rel R (Abs -` xs) (Abs -` xs)" unfolding set_rel_def vimage_def - by auto (metis Quotient_rel_abs[OF assms])+ + by auto (metis Quotient3_rel_abs[OF assms])+ next fix r s show "set_rel R r s = (set_rel R r r \ set_rel R s s \ Rep -` r = Rep -` s)" unfolding set_rel_def vimage_def set_eq_iff - by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+ + by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+ qed -declare [[map set = (set_rel, set_quotient)]] +declare [[mapQ3 set = (set_rel, set_quotient)]] lemma empty_set_rsp[quot_respect]: "set_rel R {} {}" unfolding set_rel_def by simp lemma collect_rsp[quot_respect]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "((R ===> op =) ===> set_rel R) Collect Collect" by (intro fun_relI) (simp add: fun_rel_def set_rel_def) lemma collect_prs[quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "((Abs ---> id) ---> op -` Rep) Collect = Collect" unfolding fun_eq_iff - by (simp add: Quotient_abs_rep[OF assms]) + by (simp add: Quotient3_abs_rep[OF assms]) lemma union_rsp[quot_respect]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(set_rel R ===> set_rel R ===> set_rel R) op \ op \" by (intro fun_relI) (simp add: set_rel_def) lemma union_prs[quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \ = op \" unfolding fun_eq_iff - by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]]) + by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]]) lemma diff_rsp[quot_respect]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -" by (intro fun_relI) (simp add: set_rel_def) lemma diff_prs[quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -" unfolding fun_eq_iff - by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff) + by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff) lemma inter_rsp[quot_respect]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(set_rel R ===> set_rel R ===> set_rel R) op \ op \" by (intro fun_relI) (auto simp add: set_rel_def) lemma inter_prs[quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \ = op \" unfolding fun_eq_iff - by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]]) + by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]]) lemma mem_prs[quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(Rep ---> op -` Abs ---> id) op \ = op \" - by (simp add: fun_eq_iff Quotient_abs_rep[OF assms]) + by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms]) lemma mem_rsp[quot_respect]: shows "(R ===> set_rel R ===> op =) op \ op \" diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Library/Quotient_Sum.thy Tue Apr 03 20:56:32 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Library/Quotient_Sum.thy +(* Title: HOL/Library/Quotient3_Sum.thy Author: Cezary Kaliszyk and Christian Urban *) @@ -55,44 +55,44 @@ by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE) lemma sum_quotient [quot_thm]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" - apply (rule QuotientI) + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" + shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" + apply (rule Quotient3I) apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2 - Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2]) - using Quotient_rel [OF q1] Quotient_rel [OF q2] + Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2]) + using Quotient3_rel [OF q1] Quotient3_rel [OF q2] apply (simp add: sum_rel_unfold comp_def split: sum.split) done -declare [[map sum = (sum_rel, sum_quotient)]] +declare [[mapQ3 sum = (sum_rel, sum_quotient)]] lemma sum_Inl_rsp [quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(R1 ===> sum_rel R1 R2) Inl Inl" by auto lemma sum_Inr_rsp [quot_respect]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(R2 ===> sum_rel R1 R2) Inr Inr" by auto lemma sum_Inl_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" apply(simp add: fun_eq_iff) - apply(simp add: Quotient_abs_rep[OF q1]) + apply(simp add: Quotient3_abs_rep[OF q1]) done lemma sum_Inr_prs [quot_preserve]: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + assumes q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" apply(simp add: fun_eq_iff) - apply(simp add: Quotient_abs_rep[OF q2]) + apply(simp add: Quotient3_abs_rep[OF q2]) done end diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Lifting.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Lifting.thy Tue Apr 03 20:56:32 2012 +0200 @@ -0,0 +1,316 @@ +(* Title: HOL/Lifting.thy + Author: Brian Huffman and Ondrej Kuncar + Author: Cezary Kaliszyk and Christian Urban +*) + +header {* Lifting package *} + +theory Lifting +imports Plain Equiv_Relations +keywords + "print_quotmaps" "print_quotients" :: diag and + "lift_definition" :: thy_goal and + "setup_lifting" :: thy_decl +uses + ("Tools/Lifting/lifting_info.ML") + ("Tools/Lifting/lifting_term.ML") + ("Tools/Lifting/lifting_def.ML") + ("Tools/Lifting/lifting_setup.ML") +begin + +subsection {* Function map and function relation *} + +notation map_fun (infixr "--->" 55) + +lemma map_fun_id: + "(id ---> id) = id" + by (simp add: fun_eq_iff) + +definition + fun_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" (infixr "===>" 55) +where + "fun_rel R1 R2 = (\f g. \x y. R1 x y \ R2 (f x) (g y))" + +lemma fun_relI [intro]: + assumes "\x y. R1 x y \ R2 (f x) (g y)" + shows "(R1 ===> R2) f g" + using assms by (simp add: fun_rel_def) + +lemma fun_relE: + assumes "(R1 ===> R2) f g" and "R1 x y" + obtains "R2 (f x) (g y)" + using assms by (simp add: fun_rel_def) + +lemma fun_rel_eq: + 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 {* Quotient Predicate *} + +definition + "Quotient R Abs Rep T \ + (\a. Abs (Rep a) = a) \ + (\a. R (Rep a) (Rep a)) \ + (\r s. R r s \ R r r \ R s s \ Abs r = Abs s) \ + T = (\x y. R x x \ Abs x = y)" + +lemma QuotientI: + assumes "\a. Abs (Rep a) = a" + and "\a. R (Rep a) (Rep a)" + and "\r s. R r s \ R r r \ R s s \ Abs r = Abs s" + and "T = (\x y. R x x \ Abs x = y)" + shows "Quotient R Abs Rep T" + using assms unfolding Quotient_def by blast + +lemma Quotient_abs_rep: + assumes a: "Quotient R Abs Rep T" + shows "Abs (Rep a) = a" + using a + unfolding Quotient_def + by simp + +lemma Quotient_rep_reflp: + assumes a: "Quotient R Abs Rep T" + shows "R (Rep a) (Rep a)" + using a + unfolding Quotient_def + by blast + +lemma Quotient_rel: + assumes a: "Quotient R Abs Rep T" + shows "R r r \ R s s \ Abs r = Abs s \ R r s" -- {* orientation does not loop on rewriting *} + using a + unfolding Quotient_def + by blast + +lemma Quotient_cr_rel: + assumes a: "Quotient R Abs Rep T" + shows "T = (\x y. R x x \ Abs x = y)" + using a + unfolding Quotient_def + by blast + +lemma Quotient_refl1: + assumes a: "Quotient R Abs Rep T" + shows "R r s \ R r r" + using a unfolding Quotient_def + by fast + +lemma Quotient_refl2: + assumes a: "Quotient R Abs Rep T" + shows "R r s \ R s s" + using a unfolding Quotient_def + by fast + +lemma Quotient_rel_rep: + assumes a: "Quotient R Abs Rep T" + shows "R (Rep a) (Rep b) \ a = b" + using a + unfolding Quotient_def + by metis + +lemma Quotient_rep_abs: + assumes a: "Quotient R Abs Rep T" + shows "R r r \ R (Rep (Abs r)) r" + using a unfolding Quotient_def + by blast + +lemma Quotient_rel_abs: + assumes a: "Quotient R Abs Rep T" + shows "R r s \ Abs r = Abs s" + using a unfolding Quotient_def + by blast + +lemma Quotient_symp: + assumes a: "Quotient R Abs Rep T" + shows "symp R" + using a unfolding Quotient_def using sympI by (metis (full_types)) + +lemma Quotient_transp: + assumes a: "Quotient R Abs Rep T" + shows "transp R" + using a unfolding Quotient_def using transpI by (metis (full_types)) + +lemma Quotient_part_equivp: + assumes a: "Quotient R Abs Rep T" + shows "part_equivp R" +by (metis Quotient_rep_reflp Quotient_symp Quotient_transp a part_equivpI) + +lemma identity_quotient: "Quotient (op =) id id (op =)" +unfolding Quotient_def by simp + +lemma Quotient_alt_def: + "Quotient R Abs Rep T \ + (\a b. T a b \ Abs a = b) \ + (\b. T (Rep b) b) \ + (\x y. R x y \ T x (Abs x) \ T y (Abs y) \ Abs x = Abs y)" +apply safe +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (simp (no_asm_use) only: Quotient_def, fast) +apply (rule QuotientI) +apply simp +apply metis +apply simp +apply (rule ext, rule ext, metis) +done + +lemma Quotient_alt_def2: + "Quotient R Abs Rep T \ + (\a b. T a b \ Abs a = b) \ + (\b. T (Rep b) b) \ + (\x y. R x y \ T x (Abs y) \ T y (Abs x))" + unfolding Quotient_alt_def by (safe, metis+) + +lemma fun_quotient: + assumes 1: "Quotient R1 abs1 rep1 T1" + assumes 2: "Quotient R2 abs2 rep2 T2" + shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)" + using assms unfolding Quotient_alt_def2 + unfolding fun_rel_def fun_eq_iff map_fun_apply + by (safe, metis+) + +lemma apply_rsp: + fixes f g::"'a \ 'c" + assumes q: "Quotient R1 Abs1 Rep1 T1" + and a: "(R1 ===> R2) f g" "R1 x y" + shows "R2 (f x) (g y)" + using a by (auto elim: fun_relE) + +lemma apply_rsp': + assumes a: "(R1 ===> R2) f g" "R1 x y" + shows "R2 (f x) (g y)" + using a by (auto elim: fun_relE) + +lemma apply_rsp'': + assumes "Quotient R Abs Rep T" + 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 {* Quotient composition *} + +lemma Quotient_compose: + assumes 1: "Quotient R1 Abs1 Rep1 T1" + assumes 2: "Quotient R2 Abs2 Rep2 T2" + shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \ Abs1) (Rep1 \ Rep2) (T1 OO T2)" +proof - + from 1 have Abs1: "\a b. T1 a b \ Abs1 a = b" + unfolding Quotient_alt_def by simp + from 1 have Rep1: "\b. T1 (Rep1 b) b" + unfolding Quotient_alt_def by simp + from 2 have Abs2: "\a b. T2 a b \ Abs2 a = b" + unfolding Quotient_alt_def by simp + from 2 have Rep2: "\b. T2 (Rep2 b) b" + unfolding Quotient_alt_def by simp + from 2 have R2: + "\x y. R2 x y \ T2 x (Abs2 x) \ T2 y (Abs2 y) \ Abs2 x = Abs2 y" + unfolding Quotient_alt_def by simp + show ?thesis + unfolding Quotient_alt_def + apply simp + apply safe + apply (drule Abs1, simp) + apply (erule Abs2) + apply (rule pred_compI) + apply (rule Rep1) + apply (rule Rep2) + apply (rule pred_compI, assumption) + apply (drule Abs1, simp) + apply (clarsimp simp add: R2) + apply (rule pred_compI, assumption) + apply (drule Abs1, simp)+ + apply (clarsimp simp add: R2) + apply (drule Abs1, simp)+ + apply (clarsimp simp add: R2) + apply (rule pred_compI, assumption) + apply (rule pred_compI [rotated]) + apply (erule conversepI) + apply (drule Abs1, simp)+ + apply (simp add: R2) + done +qed + +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" + and T_def: "T \ (\x y. Abs x = y)" + shows "Quotient (op =) Abs Rep T" +proof - + interpret type_definition Rep Abs UNIV by fact + from Abs_inject Rep_inverse T_def 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}" + and T_def: "T \ (\x y. (invariant P) x x \ Abs x = y)" + shows "Quotient (invariant P) Abs Rep T" +proof - + interpret type_definition Rep Abs "{x. P x}" by fact + from Rep Abs_inject Rep_inverse T_def 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 lifting package *} + +use "Tools/Lifting/lifting_info.ML" +setup Lifting_Info.setup + +declare [[map "fun" = (fun_rel, fun_quotient)]] + +use "Tools/Lifting/lifting_term.ML" + +use "Tools/Lifting/lifting_def.ML" + +use "Tools/Lifting/lifting_setup.ML" + +hide_const (open) invariant + +end diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Metis_Examples/Clausification.thy --- a/src/HOL/Metis_Examples/Clausification.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Metis_Examples/Clausification.thy Tue Apr 03 20:56:32 2012 +0200 @@ -131,7 +131,7 @@ by (metis bounded_def subset_eq) lemma - assumes a: "Quotient R Abs Rep" + assumes a: "Quotient R Abs Rep T" shows "symp R" using a unfolding Quotient_def using sympI by (metis (full_types)) diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Quotient.thy Tue Apr 03 20:56:32 2012 +0200 @@ -5,11 +5,10 @@ header {* Definition of Quotient Types *} theory Quotient -imports Plain Hilbert_Choice Equiv_Relations +imports Plain Hilbert_Choice Equiv_Relations Lifting keywords - "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and + "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and "quotient_type" :: thy_goal and "/" and - "setup_lifting" :: thy_decl and "quotient_definition" :: thy_goal uses ("Tools/Quotient/quotient_info.ML") @@ -53,37 +52,6 @@ shows "x \ Respects R \ R x x" unfolding Respects_def by simp -subsection {* Function map and function relation *} - -notation map_fun (infixr "--->" 55) - -lemma map_fun_id: - "(id ---> id) = id" - by (simp add: fun_eq_iff) - -definition - fun_rel :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" (infixr "===>" 55) -where - "fun_rel R1 R2 = (\f g. \x y. R1 x y \ R2 (f x) (g y))" - -lemma fun_relI [intro]: - assumes "\x y. R1 x y \ R2 (f x) (g y)" - shows "(R1 ===> R2) f g" - using assms by (simp add: fun_rel_def) - -lemma fun_relE: - assumes "(R1 ===> R2) f g" and "R1 x y" - obtains "R2 (f x) (g y)" - using assms by (simp add: fun_rel_def) - -lemma fun_rel_eq: - 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" @@ -106,155 +74,169 @@ subsection {* Quotient Predicate *} definition - "Quotient R Abs Rep \ + "Quotient3 R Abs Rep \ (\a. Abs (Rep a) = a) \ (\a. R (Rep a) (Rep a)) \ (\r s. R r s \ R r r \ R s s \ Abs r = Abs s)" -lemma QuotientI: +lemma Quotient3I: assumes "\a. Abs (Rep a) = a" and "\a. R (Rep a) (Rep a)" and "\r s. R r s \ R r r \ R s s \ Abs r = Abs s" - shows "Quotient R Abs Rep" - using assms unfolding Quotient_def by blast + shows "Quotient3 R Abs Rep" + using assms unfolding Quotient3_def by blast -lemma Quotient_abs_rep: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_abs_rep: + assumes a: "Quotient3 R Abs Rep" shows "Abs (Rep a) = a" using a - unfolding Quotient_def + unfolding Quotient3_def by simp -lemma Quotient_rep_reflp: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_rep_reflp: + assumes a: "Quotient3 R Abs Rep" shows "R (Rep a) (Rep a)" using a - unfolding Quotient_def + unfolding Quotient3_def by blast -lemma Quotient_rel: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_rel: + assumes a: "Quotient3 R Abs Rep" shows "R r r \ R s s \ Abs r = Abs s \ R r s" -- {* orientation does not loop on rewriting *} using a - unfolding Quotient_def + unfolding Quotient3_def by blast -lemma Quotient_refl1: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_refl1: + assumes a: "Quotient3 R Abs Rep" shows "R r s \ R r r" - using a unfolding Quotient_def + using a unfolding Quotient3_def by fast -lemma Quotient_refl2: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_refl2: + assumes a: "Quotient3 R Abs Rep" shows "R r s \ R s s" - using a unfolding Quotient_def + using a unfolding Quotient3_def by fast -lemma Quotient_rel_rep: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_rel_rep: + assumes a: "Quotient3 R Abs Rep" shows "R (Rep a) (Rep b) \ a = b" using a - unfolding Quotient_def + unfolding Quotient3_def by metis -lemma Quotient_rep_abs: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_rep_abs: + assumes a: "Quotient3 R Abs Rep" shows "R r r \ R (Rep (Abs r)) r" - using a unfolding Quotient_def + using a unfolding Quotient3_def + by blast + +lemma Quotient3_rel_abs: + assumes a: "Quotient3 R Abs Rep" + shows "R r s \ Abs r = Abs s" + using a unfolding Quotient3_def by blast -lemma Quotient_rel_abs: - assumes a: "Quotient R Abs Rep" - shows "R r s \ Abs r = Abs s" - using a unfolding Quotient_def - by blast - -lemma Quotient_symp: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_symp: + assumes a: "Quotient3 R Abs Rep" shows "symp R" - using a unfolding Quotient_def using sympI by metis + using a unfolding Quotient3_def using sympI by metis -lemma Quotient_transp: - assumes a: "Quotient R Abs Rep" +lemma Quotient3_transp: + assumes a: "Quotient3 R Abs Rep" shows "transp R" - using a unfolding Quotient_def using transpI by metis + using a unfolding Quotient3_def using transpI by (metis (full_types)) -lemma identity_quotient: - shows "Quotient (op =) id id" - unfolding Quotient_def id_def +lemma Quotient3_part_equivp: + assumes a: "Quotient3 R Abs Rep" + shows "part_equivp R" +by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI) + +lemma identity_quotient3: + shows "Quotient3 (op =) id id" + unfolding Quotient3_def id_def by blast -lemma fun_quotient: - assumes q1: "Quotient R1 abs1 rep1" - and q2: "Quotient R2 abs2 rep2" - shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" +lemma fun_quotient3: + assumes q1: "Quotient3 R1 abs1 rep1" + and q2: "Quotient3 R2 abs2 rep2" + shows "Quotient3 (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" proof - - have "\a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" - using q1 q2 by (simp add: Quotient_def fun_eq_iff) + have "\a.(rep1 ---> abs2) ((abs1 ---> rep2) a) = a" + using q1 q2 by (simp add: Quotient3_def fun_eq_iff) moreover - have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" + have "\a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" by (rule fun_relI) - (insert q1 q2 Quotient_rel_abs [of R1 abs1 rep1] Quotient_rel_rep [of R2 abs2 rep2], - simp (no_asm) add: Quotient_def, simp) + (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2], + simp (no_asm) add: Quotient3_def, simp) + moreover - have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ + { + fix r s + have "(R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s)" - apply(auto simp add: fun_rel_def fun_eq_iff) - using q1 q2 unfolding Quotient_def - apply(metis) - using q1 q2 unfolding Quotient_def - apply(metis) - using q1 q2 unfolding Quotient_def - apply(metis) - using q1 q2 unfolding Quotient_def - apply(metis) - done - ultimately - show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" - unfolding Quotient_def by blast + proof - + + have "(R1 ===> R2) r s \ (R1 ===> R2) r r" unfolding fun_rel_def + using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] + by (metis (full_types) part_equivp_def) + moreover have "(R1 ===> R2) r s \ (R1 ===> R2) s s" unfolding fun_rel_def + using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] + by (metis (full_types) part_equivp_def) + moreover have "(R1 ===> R2) r s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s" + apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis + moreover have "((R1 ===> R2) r r \ (R1 ===> R2) s s \ + (rep1 ---> abs2) r = (rep1 ---> abs2) s) \ (R1 ===> R2) r s" + apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def + by (metis map_fun_apply) + + ultimately show ?thesis by blast + qed + } + ultimately show ?thesis by (intro Quotient3I) (assumption+) qed lemma abs_o_rep: - assumes a: "Quotient R Abs Rep" + assumes a: "Quotient3 R Abs Rep" shows "Abs o Rep = id" unfolding fun_eq_iff - by (simp add: Quotient_abs_rep[OF a]) + by (simp add: Quotient3_abs_rep[OF a]) lemma equals_rsp: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" and a: "R xa xb" "R ya yb" shows "R xa ya = R xb yb" - using a Quotient_symp[OF q] Quotient_transp[OF q] + using a Quotient3_symp[OF q] Quotient3_transp[OF q] by (blast elim: sympE transpE) lemma lambda_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) = (\x. f x)" unfolding fun_eq_iff - using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] + using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by simp lemma lambda_prs1: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. (Abs1 ---> Rep2) f x) = (\x. f x)" unfolding fun_eq_iff - using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] + using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by simp lemma rep_abs_rsp: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" and a: "R x1 x2" shows "R x1 (Rep (Abs x2))" - using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] + using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q] by metis lemma rep_abs_rsp_left: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" and a: "R x1 x2" shows "R (Rep (Abs x1)) x2" - using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] + using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q] by metis text{* @@ -264,24 +246,19 @@ will be provable; which is why we need to use @{text apply_rsp} and not the primed version *} -lemma apply_rsp: +lemma apply_rspQ3: fixes f g::"'a \ 'c" - assumes q: "Quotient R1 Abs1 Rep1" + assumes q: "Quotient3 R1 Abs1 Rep1" and a: "(R1 ===> R2) f g" "R1 x y" shows "R2 (f x) (g y)" using a by (auto elim: fun_relE) -lemma apply_rsp': - assumes a: "(R1 ===> R2) f g" "R1 x y" - shows "R2 (f x) (g y)" - using a by (auto elim: fun_relE) - -lemma apply_rsp'': - assumes "Quotient R Abs Rep" +lemma apply_rspQ3'': + assumes "Quotient3 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) + from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient3_rep_reflp) then show ?thesis using assms(2) by (auto intro: apply_rsp') qed @@ -393,29 +370,29 @@ "x \ p \ Babs p m x = m x" lemma babs_rsp: - assumes q: "Quotient R1 Abs1 Rep1" + assumes q: "Quotient3 R1 Abs1 Rep1" and a: "(R1 ===> R2) f g" shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" apply (auto simp add: Babs_def in_respects fun_rel_def) apply (subgoal_tac "x \ Respects R1 \ y \ Respects R1") using a apply (simp add: Babs_def fun_rel_def) apply (simp add: in_respects fun_rel_def) - using Quotient_rel[OF q] + using Quotient3_rel[OF q] by metis lemma babs_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" apply (rule ext) apply (simp add:) apply (subgoal_tac "Rep1 x \ Respects R1") - apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) - apply (simp add: in_respects Quotient_rel_rep[OF q1]) + apply (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) + apply (simp add: in_respects Quotient3_rel_rep[OF q1]) done lemma babs_simp: - assumes q: "Quotient R1 Abs Rep" + assumes q: "Quotient3 R1 Abs Rep" shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)" apply(rule iffI) apply(simp_all only: babs_rsp[OF q]) @@ -423,7 +400,7 @@ apply (subgoal_tac "x \ Respects R1 \ y \ Respects R1") apply(metis Babs_def) apply (simp add: in_respects) - using Quotient_rel[OF q] + using Quotient3_rel[OF q] by metis (* If a user proves that a particular functional relation @@ -451,15 +428,15 @@ (* 2 lemmas needed for cleaning of quantifiers *) lemma all_prs: - assumes a: "Quotient R absf repf" + assumes a: "Quotient3 R absf repf" shows "Ball (Respects R) ((absf ---> id) f) = All f" - using a unfolding Quotient_def Ball_def in_respects id_apply comp_def map_fun_def + using a unfolding Quotient3_def Ball_def in_respects id_apply comp_def map_fun_def by metis lemma ex_prs: - assumes a: "Quotient R absf repf" + assumes a: "Quotient3 R absf repf" shows "Bex (Respects R) ((absf ---> id) f) = Ex f" - using a unfolding Quotient_def Bex_def in_respects id_apply comp_def map_fun_def + using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def by metis subsection {* @{text Bex1_rel} quantifier *} @@ -508,7 +485,7 @@ done lemma bex1_rel_rsp: - assumes a: "Quotient R absf repf" + assumes a: "Quotient3 R absf repf" shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)" apply (simp add: fun_rel_def) apply clarify @@ -520,7 +497,7 @@ lemma ex1_prs: - assumes a: "Quotient R absf repf" + assumes a: "Quotient3 R absf repf" shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" apply (simp add:) apply (subst Bex1_rel_def) @@ -535,7 +512,7 @@ apply (rule_tac x="absf x" in exI) apply (simp) apply rule+ - using a unfolding Quotient_def + using a unfolding Quotient3_def apply metis apply rule+ apply (erule_tac x="x" in ballE) @@ -548,10 +525,10 @@ apply (rule_tac x="repf x" in exI) apply (simp only: in_respects) apply rule - apply (metis Quotient_rel_rep[OF a]) -using a unfolding Quotient_def apply (simp) + apply (metis Quotient3_rel_rep[OF a]) +using a unfolding Quotient3_def apply (simp) apply rule+ -using a unfolding Quotient_def in_respects +using a unfolding Quotient3_def in_respects apply metis done @@ -587,7 +564,7 @@ subsection {* Various respects and preserve lemmas *} lemma quot_rel_rsp: - assumes a: "Quotient R Abs Rep" + assumes a: "Quotient3 R Abs Rep" shows "(R ===> R ===> op =) R R" apply(rule fun_relI)+ apply(rule equals_rsp[OF a]) @@ -595,12 +572,12 @@ done lemma o_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - and q3: "Quotient R3 Abs3 Rep3" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" + and q3: "Quotient3 R3 Abs3 Rep3" shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \ = op \" and "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \ = op \" - using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3] + using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3] by (simp_all add: fun_eq_iff) lemma o_rsp: @@ -609,26 +586,26 @@ by (force elim: fun_relE)+ lemma cond_prs: - assumes a: "Quotient R absf repf" + assumes a: "Quotient3 R absf repf" shows "absf (if a then repf b else repf c) = (if a then b else c)" - using a unfolding Quotient_def by auto + using a unfolding Quotient3_def by auto lemma if_prs: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(id ---> Rep ---> Rep ---> Abs) If = If" - using Quotient_abs_rep[OF q] + using Quotient3_abs_rep[OF q] by (auto simp add: fun_eq_iff) lemma if_rsp: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" shows "(op = ===> R ===> R ===> R) If If" by force lemma let_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" + assumes q1: "Quotient3 R1 Abs1 Rep1" + and q2: "Quotient3 R2 Abs2 Rep2" shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let" - using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] + using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by (auto simp add: fun_eq_iff) lemma let_rsp: @@ -640,9 +617,9 @@ by auto lemma id_prs: - assumes a: "Quotient R Abs Rep" + assumes a: "Quotient3 R Abs Rep" shows "(Rep ---> Abs) id = id" - by (simp add: fun_eq_iff Quotient_abs_rep [OF a]) + by (simp add: fun_eq_iff Quotient3_abs_rep [OF a]) locale quot_type = @@ -673,8 +650,8 @@ by (metis assms exE_some equivp[simplified part_equivp_def]) lemma Quotient: - shows "Quotient R abs rep" - unfolding Quotient_def abs_def rep_def + shows "Quotient3 R abs rep" + unfolding Quotient3_def abs_def rep_def proof (intro conjI allI) fix a r s show x: "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" proof - @@ -703,149 +680,114 @@ subsection {* Quotient composition *} -lemma OOO_quotient: +lemma OOO_quotient3: 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 R1: "Quotient3 R1 Abs1 Rep1" + assumes R2: "Quotient3 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]) + shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \ Abs1) (Rep1 \ Rep2)" +apply (rule Quotient3I) + apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_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 Quotient3_rep_reflp [OF R1]) apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated]) - apply (rule Quotient_rep_reflp [OF R1]) + apply (rule Quotient3_rep_reflp [OF R1]) apply (rule Rep1) - apply (rule Quotient_rep_reflp [OF R2]) + apply (rule Quotient3_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 (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_refl1 [OF R1]) + apply (drule Quotient3_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 (erule Quotient3_symp [OF R1, THEN sympD]) + apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) + apply (rule conjI, erule Quotient3_refl1 [OF R1]) + apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) + apply (subst Quotient3_abs_rep [OF R1]) + apply (erule Quotient3_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 (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_refl1 [OF R1]) + apply (drule Quotient3_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 (erule Quotient3_symp [OF R1, THEN sympD]) + apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) + apply (rule conjI, erule Quotient3_refl2 [OF R1]) + apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) + apply (subst Quotient3_abs_rep [OF R1]) + apply (erule Quotient3_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 (rule Quotient3_rel_abs [OF R2]) + apply (rule Quotient3_rel_abs [OF R1, THEN ssubst], assumption) + apply (rule Quotient3_rel_abs [OF R1, THEN subst], assumption) apply (erule Abs1) - apply (erule Quotient_refl2 [OF R1]) - apply (erule Quotient_refl1 [OF R1]) + apply (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_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 Quotient3_rel[symmetric, OF R1, THEN iffD2]) + apply (rule conjI, erule Quotient3_refl1 [OF R1]) + apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_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 Quotient3_rel[symmetric, OF R1, THEN iffD2]) + apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1]) + apply (erule Quotient3_refl2 [OF R1]) apply (rule Rep1) apply (drule Abs1) - apply (erule Quotient_refl2 [OF R1]) - apply (erule Quotient_refl1 [OF R1]) + apply (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_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 (erule Quotient3_refl2 [OF R1]) + apply (erule Quotient3_refl1 [OF R1]) + apply (drule Quotient3_rel_abs [OF R1]) + apply (drule Quotient3_rel_abs [OF R1]) + apply (drule Quotient3_rel_abs [OF R1]) + apply (drule Quotient3_rel_abs [OF R1]) apply simp - apply (rule Quotient_rel[symmetric, OF R2, THEN iffD2]) + apply (rule Quotient3_rel[symmetric, OF R2, THEN iffD2]) apply simp done -lemma OOO_eq_quotient: +lemma OOO_eq_quotient3: 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)" + assumes R1: "Quotient3 R1 Abs1 Rep1" + assumes R2: "Quotient3 op= Abs2 Rep2" + shows "Quotient3 (R1 OOO op=) (Abs2 \ Abs1) (Rep1 \ Rep2)" using assms -by (rule OOO_quotient) auto +by (rule OOO_quotient3) 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: +lemma copy_type_to_Quotient3: assumes "type_definition Rep Abs UNIV" - shows "Quotient (op =) Abs Rep" + shows "Quotient3 (op =) Abs Rep" proof - interpret type_definition Rep Abs UNIV by fact - from Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI) + from Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I) 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: +lemma invariant_type_to_Quotient3: assumes "type_definition Rep Abs {x. P x}" - shows "Quotient (invariant P) Abs Rep" + shows "Quotient3 (Lifting.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) + from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I simp: invariant_def) qed subsection {* ML setup *} @@ -855,9 +797,9 @@ use "Tools/Quotient/quotient_info.ML" setup Quotient_Info.setup -declare [[map "fun" = (fun_rel, fun_quotient)]] +declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]] -lemmas [quot_thm] = fun_quotient +lemmas [quot_thm] = fun_quotient3 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp lemmas [quot_preserve] = if_prs o_prs let_prs id_prs lemmas [quot_equiv] = identity_equivp @@ -960,6 +902,4 @@ map_fun (infixr "--->" 55) and fun_rel (infixr "===>" 55) -hide_const (open) invariant - end diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Quotient_Examples/DList.thy --- a/src/HOL/Quotient_Examples/DList.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Quotient_Examples/DList.thy Tue Apr 03 20:56:32 2012 +0200 @@ -227,7 +227,7 @@ lemma list_of_dlist_dlist [simp]: "list_of_dlist (dlist xs) = remdups xs" unfolding list_of_dlist_def map_fun_apply id_def - by (metis Quotient_rep_abs[OF Quotient_dlist] dlist_eq_def) + by (metis Quotient3_rep_abs[OF Quotient3_dlist] dlist_eq_def) lemma remdups_list_of_dlist [simp]: "remdups (list_of_dlist dxs) = list_of_dlist dxs" @@ -236,7 +236,7 @@ lemma dlist_list_of_dlist [simp, code abstype]: "dlist (list_of_dlist dxs) = dxs" by (simp add: list_of_dlist_def) - (metis Quotient_def Quotient_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist) + (metis Quotient3_def Quotient3_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist) lemma dlist_filter_simps: "filter P empty = empty" diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Quotient_Examples/FSet.thy Tue Apr 03 20:56:32 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Quotient_Examples/FSet.thy +(* Title: HOL/Quotient3_Examples/FSet.thy Author: Cezary Kaliszyk, TU Munich Author: Christian Urban, TU Munich @@ -117,15 +117,15 @@ by (simp only: list_eq_def set_map) lemma quotient_compose_list_g: - assumes q: "Quotient R Abs Rep" + assumes q: "Quotient3 R Abs Rep" and e: "equivp R" - shows "Quotient ((list_all2 R) OOO (op \)) + shows "Quotient3 ((list_all2 R) OOO (op \)) (abs_fset \ (map Abs)) ((map Rep) \ rep_fset)" - unfolding Quotient_def comp_def + unfolding Quotient3_def comp_def proof (intro conjI allI) fix a r s show "abs_fset (map Abs (map Rep (rep_fset a))) = a" - by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] List.map.id) + by (simp add: abs_o_rep[OF q] Quotient3_abs_rep[OF Quotient3_fset] List.map.id) have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))" by (rule list_all2_refl'[OF e]) have c: "(op \ OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))" @@ -146,37 +146,37 @@ assume d: "b \ ba" assume e: "list_all2 R ba s" have f: "map Abs r = map Abs b" - using Quotient_rel[OF list_quotient[OF q]] c by blast + using Quotient3_rel[OF list_quotient3[OF q]] c by blast have "map Abs ba = map Abs s" - using Quotient_rel[OF list_quotient[OF q]] e by blast + using Quotient3_rel[OF list_quotient3[OF q]] e by blast then have g: "map Abs s = map Abs ba" by simp then show "map Abs r \ map Abs s" using d f map_list_eq_cong by simp qed then show "abs_fset (map Abs r) = abs_fset (map Abs s)" - using Quotient_rel[OF Quotient_fset] by blast + using Quotient3_rel[OF Quotient3_fset] by blast next assume a: "(list_all2 R OOO op \) r r \ (list_all2 R OOO op \) s s \ abs_fset (map Abs r) = abs_fset (map Abs s)" then have s: "(list_all2 R OOO op \) s s" by simp have d: "map Abs r \ map Abs s" - by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a) + by (subst Quotient3_rel [OF Quotient3_fset, symmetric]) (simp add: a) have b: "map Rep (map Abs r) \ map Rep (map Abs s)" by (rule map_list_eq_cong[OF d]) have y: "list_all2 R (map Rep (map Abs s)) s" - by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]]) + by (fact rep_abs_rsp_left[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of s]]) have c: "(op \ OO list_all2 R) (map Rep (map Abs r)) s" by (rule pred_compI) (rule b, rule y) have z: "list_all2 R r (map Rep (map Abs r))" - by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]]) + by (fact rep_abs_rsp[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of r]]) then show "(list_all2 R OOO op \) r s" using a c pred_compI by simp qed qed lemma quotient_compose_list[quot_thm]: - shows "Quotient ((list_all2 op \) OOO (op \)) + shows "Quotient3 ((list_all2 op \) OOO (op \)) (abs_fset \ (map abs_fset)) ((map rep_fset) \ rep_fset)" - by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp) + by (rule quotient_compose_list_g, rule Quotient3_fset, rule list_eq_equivp) section {* Quotient definitions for fsets *} @@ -404,19 +404,19 @@ done lemma Nil_prs2 [quot_preserve]: - assumes "Quotient R Abs Rep" + assumes "Quotient3 R Abs Rep" shows "(Abs \ map f) [] = Abs []" by simp lemma Cons_prs2 [quot_preserve]: - assumes q: "Quotient R1 Abs1 Rep1" - and r: "Quotient R2 Abs2 Rep2" + assumes q: "Quotient3 R1 Abs1 Rep1" + and r: "Quotient3 R2 Abs2 Rep2" shows "(Rep1 ---> (map Rep1 \ Rep2) ---> (Abs2 \ map Abs1)) (op #) = (id ---> Rep2 ---> Abs2) (op #)" - by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q]) + by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q]) lemma append_prs2 [quot_preserve]: - assumes q: "Quotient R1 Abs1 Rep1" - and r: "Quotient R2 Abs2 Rep2" + assumes q: "Quotient3 R1 Abs1 Rep1" + and r: "Quotient3 R2 Abs2 Rep2" shows "((map Rep1 \ Rep2) ---> (map Rep1 \ Rep2) ---> (Abs2 \ map Abs1)) op @ = (Rep2 ---> Rep2 ---> Abs2) op @" by (simp add: fun_eq_iff abs_o_rep[OF q] List.map.id) @@ -485,7 +485,7 @@ lemma map_prs2 [quot_preserve]: shows "((abs_fset ---> rep_fset) ---> (map rep_fset \ rep_fset) ---> abs_fset \ map abs_fset) map = (id ---> rep_fset ---> abs_fset) map" by (auto simp add: fun_eq_iff) - (simp only: map_map[symmetric] map_prs_aux[OF Quotient_fset Quotient_fset]) + (simp only: map_map[symmetric] map_prs_aux[OF Quotient3_fset Quotient3_fset]) section {* Lifted theorems *} diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Quotient_Examples/Lift_DList.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient_Examples/Lift_DList.thy Tue Apr 03 20:56:32 2012 +0200 @@ -0,0 +1,86 @@ +(* Title: HOL/Quotient_Examples/Lift_DList.thy + Author: Ondrej Kuncar +*) + +theory Lift_DList +imports Main "~~/src/HOL/Library/Quotient_List" +begin + +subsection {* The type of distinct lists *} + +typedef (open) 'a dlist = "{xs::'a list. distinct xs}" + morphisms list_of_dlist Abs_dlist +proof + show "[] \ {xs. distinct xs}" by simp +qed + +setup_lifting type_definition_dlist + +text {* Fundamental operations: *} + +lift_definition empty :: "'a dlist" is "[]" +by simp + +lift_definition insert :: "'a \ 'a dlist \ 'a dlist" is List.insert +by simp + +lift_definition remove :: "'a \ 'a dlist \ 'a dlist" is List.remove1 +by simp + +lift_definition map :: "('a \ 'b) \ 'a dlist \ 'b dlist" is "\f. remdups o List.map f" +by simp + +lift_definition filter :: "('a \ bool) \ 'a dlist \ 'a dlist" is List.filter +by simp + +text {* Derived operations: *} + +lift_definition null :: "'a dlist \ bool" is List.null +by simp + +lift_definition member :: "'a dlist \ 'a \ bool" is List.member +by simp + +lift_definition length :: "'a dlist \ nat" is List.length +by simp + +lift_definition fold :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" is List.fold +by simp + +lift_definition foldr :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" is List.foldr +by simp + +lift_definition concat :: "'a dlist dlist \ 'a dlist" is "remdups o List.concat" +proof - + { + fix x y + have "list_all2 cr_dlist x y \ + List.map Abs_dlist x = y \ list_all2 (Lifting.invariant distinct) x x" + unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto + } + note cr = this + + fix x :: "'a list list" and y :: "'a list list" + assume a: "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\\) x y" + from a have l_x: "list_all2 (Lifting.invariant distinct) x x" by (auto simp add: cr) + from a have l_y: "list_all2 (Lifting.invariant distinct) y y" by (auto simp add: cr) + from a have m: "(Lifting.invariant distinct) (List.map Abs_dlist x) (List.map Abs_dlist y)" + by (auto simp add: cr) + + have "x = y" + proof - + have m':"List.map Abs_dlist x = List.map Abs_dlist y" using m unfolding Lifting.invariant_def by simp + have dist: "\l. list_all2 (Lifting.invariant distinct) l l \ !x. x \ (set l) \ distinct x" + unfolding list_all2_def Lifting.invariant_def by (auto simp add: zip_same) + from dist[OF l_x] dist[OF l_y] have "inj_on Abs_dlist (set x \ set y)" by (intro inj_onI) + (metis CollectI UnE Abs_dlist_inverse) + with m' show ?thesis by (rule map_inj_on) + qed + then show "?thesis x y" unfolding Lifting.invariant_def by auto +qed + +text {* We can export code: *} + +export_code empty insert remove map filter null member length fold foldr concat in SML + +end diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Quotient_Examples/Lift_Fun.thy --- a/src/HOL/Quotient_Examples/Lift_Fun.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy Tue Apr 03 20:56:32 2012 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Quotient_Examples/Lift_Fun.thy +(* Title: HOL/Quotient3_Examples/Lift_Fun.thy Author: Ondrej Kuncar *) @@ -53,12 +53,12 @@ enriched_type map_endofun : map_endofun proof - - have "\ x. abs_endofun (rep_endofun x) = x" using Quotient_endofun by (auto simp: Quotient_def) + have "\ x. abs_endofun (rep_endofun x) = x" using Quotient3_endofun by (auto simp: Quotient3_def) then show "map_endofun id id = id" by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) - have a:"\ x. rep_endofun (abs_endofun x) = x" using Quotient_endofun - Quotient_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast + have a:"\ x. rep_endofun (abs_endofun x) = x" using Quotient3_endofun + Quotient3_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast show "\f g h i. map_endofun f g \ map_endofun h i = map_endofun (f \ h) (i \ g)" by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) qed @@ -74,34 +74,34 @@ 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) +assumes a: "Quotient3 R Abs Rep" +shows "Quotient3 (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)" +proof (intro Quotient3I) 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] + using fun_quotient3[OF a a, THEN Quotient3_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) + by (metis (mono_tags) Quotient3_endofun rep_abs_rsp) next have abs_to_eq: "\ x y. abs_endofun x = abs_endofun y \ x = y" - by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient_rep_abs[OF Quotient_endofun]) + by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient3_rep_abs[OF Quotient3_endofun]) fix r s show "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] + using fun_quotient3[OF a a,THEN Quotient3_refl1] apply metis - using fun_quotient[OF a a,THEN Quotient_refl2] + using fun_quotient3[OF a a,THEN Quotient3_refl2] apply metis - using fun_quotient[OF a a, THEN Quotient_rel] + using fun_quotient3[OF a a, THEN Quotient3_rel] apply metis - by (auto intro: fun_quotient[OF a a, THEN Quotient_rel, THEN iffD1] simp add: abs_to_eq) + by (auto intro: fun_quotient3[OF a a, THEN Quotient3_rel, THEN iffD1] simp add: abs_to_eq) qed -declare [[map endofun = (endofun_rel, endofun_quotient)]] +declare [[mapQ3 endofun = (endofun_rel, endofun_quotient)]] quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \ 'a) \ ('a \ 'a)" done diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Quotient_Examples/Lift_RBT.thy --- a/src/HOL/Quotient_Examples/Lift_RBT.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Tue Apr 03 20:56:32 2012 +0200 @@ -1,4 +1,6 @@ -(* Author: Lukas Bulwahn, TU Muenchen *) +(* Title: HOL/Quotient_Examples/Lift_RBT.thy + Author: Lukas Bulwahn and Ondrej Kuncar +*) header {* Lifting operations of RBT trees *} @@ -35,53 +37,35 @@ setup_lifting type_definition_rbt -quotient_definition lookup where "lookup :: ('a\linorder, 'b) rbt \ 'a \ 'b" is "RBT_Impl.lookup" +lift_definition lookup :: "('a\linorder, 'b) rbt \ 'a \ 'b" is "RBT_Impl.lookup" +by simp + +lift_definition empty :: "('a\linorder, 'b) rbt" is RBT_Impl.Empty +by (simp add: empty_def) + +lift_definition insert :: "'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" is "RBT_Impl.insert" +by simp + +lift_definition delete :: "'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" is "RBT_Impl.delete" +by simp + +lift_definition entries :: "('a\linorder, 'b) rbt \ ('a \ 'b) list" is RBT_Impl.entries 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. -But, it should be possible to infer the necessary sort constraints, making the explicit -sort constraints unnecessary. - -Hence this unannotated quotient_definition fails: - -quotient_definition empty where "empty :: ('a\linorder, 'b) rbt" -is "RBT_Impl.Empty" - -Similar issue for quotient_definition for entries, keys, map, and fold. -*) - -quotient_definition empty where "empty :: ('a\linorder, 'b) rbt" -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" by simp +lift_definition keys :: "('a\linorder, 'b) rbt \ 'a list" is RBT_Impl.keys +by simp -quotient_definition delete where "delete :: 'a\linorder \ ('a, 'b) rbt \ ('a, 'b) rbt" -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" 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" by simp - -quotient_definition "bulkload :: ('a\linorder \ 'b) list \ ('a, 'b) rbt" -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" 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" +lift_definition bulkload :: "('a\linorder \ 'b) list \ ('a, 'b) rbt" is "RBT_Impl.bulkload" 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" by simp +lift_definition map_entry :: "'a \ ('b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is RBT_Impl.map_entry +by simp + +lift_definition map :: "('a \ 'b \ 'b) \ ('a\linorder, 'b) rbt \ ('a, 'b) rbt" is RBT_Impl.map +by simp + +lift_definition fold :: "('a \ 'b \ 'c \ 'c) \ ('a\linorder, 'b) rbt \ 'c \ 'c" is RBT_Impl.fold +by simp export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Quotient_Examples/Lift_Set.thy --- a/src/HOL/Quotient_Examples/Lift_Set.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy Tue Apr 03 20:56:32 2012 +0200 @@ -2,7 +2,7 @@ Author: Lukas Bulwahn and Ondrej Kuncar *) -header {* Example of lifting definitions with the quotient infrastructure *} +header {* Example of lifting definitions with the lifting infrastructure *} theory Lift_Set imports Main @@ -16,19 +16,14 @@ setup_lifting type_definition_set[unfolded set_def] -text {* Now, we can employ quotient_definition to lift definitions. *} +text {* Now, we can employ lift_definition to lift definitions. *} -quotient_definition empty where "empty :: 'a set" -is "bot :: 'a \ bool" done +lift_definition empty :: "'a set" is "bot :: 'a \ bool" done term "Lift_Set.empty" thm Lift_Set.empty_def -definition insertp :: "'a \ ('a \ bool) \ 'a \ bool" where - "insertp x P y \ y = x \ P y" - -quotient_definition insert where "insert :: 'a => 'a set => 'a set" -is insertp done +lift_definition insert :: "'a => 'a set => 'a set" is "\ x P y. y = x \ P y" done term "Lift_Set.insert" thm Lift_Set.insert_def diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Quotient_Examples/Quotient_Int.thy --- a/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Apr 03 20:56:32 2012 +0200 @@ -145,9 +145,9 @@ (abs_int (x + u, y + v))" apply(simp add: plus_int_def id_simps) apply(fold plus_int_raw.simps) - apply(rule Quotient_rel_abs[OF Quotient_int]) + apply(rule Quotient3_rel_abs[OF Quotient3_int]) apply(rule plus_int_raw_rsp_aux) - apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) + apply(simp_all add: rep_abs_rsp_left[OF Quotient3_int]) done definition int_of_nat_raw: diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Quotient_Examples/ROOT.ML --- a/src/HOL/Quotient_Examples/ROOT.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Quotient_Examples/ROOT.ML Tue Apr 03 20:56:32 2012 +0200 @@ -5,5 +5,5 @@ *) use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", - "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"]; + "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat", "Lift_DList"]; diff -r 432b29a96f61 -r dac11ab96277 src/HOL/TPTP/TPTP_Parser/make_tptp_parser --- a/src/HOL/TPTP/TPTP_Parser/make_tptp_parser Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/make_tptp_parser Tue Apr 03 20:56:32 2012 +0200 @@ -30,7 +30,9 @@ for FILE in $INTERMEDIATE_FILES do - perl -p -e 's/\bref\b/Unsynchronized.ref/g;' -e 's/Unsafe\.(.*)/\1/g;' $FILE + perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \ + -e 's/Unsafe\.(.*)/\1/g;' \ + -e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE done ) > tptp_lexyacc.ML diff -r 432b29a96f61 -r dac11ab96277 src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Tue Apr 03 20:56:32 2012 +0200 @@ -1342,9 +1342,9 @@ yybl := size (!yyb); scan (s,AcceptingLeaves,l-i0,0)) end - else let val NewChar = Char.ord(CharVector.sub(!yyb,l)) + else let val NewChar = Char.ord(String.sub(!yyb,l)) val NewChar = if NewChar<128 then NewChar else 128 - val NewState = Char.ord(CharVector.sub(trans,NewChar)) + val NewState = Char.ord(String.sub(trans,NewChar)) in if NewState=0 then action(l,NewAcceptingLeaves) else scan(NewState,NewAcceptingLeaves,l+1,i0) end diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Tools/Lifting/lifting_def.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Apr 03 20:56:32 2012 +0200 @@ -0,0 +1,291 @@ +(* Title: HOL/Tools/Lifting/lifting_def.ML + Author: Ondrej Kuncar + +Definitions for constants on quotient types. +*) + +signature LIFTING_DEF = +sig + val add_lift_def: + (binding * mixfix) -> typ -> term -> thm -> local_theory -> local_theory + + val lift_def_cmd: + (binding * string option * mixfix) * string -> local_theory -> Proof.state + + val can_generate_code_cert: thm -> bool +end; + +structure Lifting_Def: LIFTING_DEF = +struct + +(** 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 force_rty_type ctxt rty rhs = + let + val thy = Proof_Context.theory_of ctxt + val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs + val rty_schematic = fastype_of rhs_schematic + val match = Sign.typ_match thy (rty_schematic, rty) Vartab.empty + in + Envir.subst_term_types match rhs_schematic + end + +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 = Lifting_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 can_generate_code_cert quot_thm = + case Lifting_Term.quot_thm_rel quot_thm of + Const (@{const_name HOL.eq}, _) => true + | Const (@{const_name invariant}, _) $ _ => true + | _ => false + +fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) = + let + val thy = Proof_Context.theory_of ctxt + val quot_thm = Lifting_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 = (cterm_of thy o Lifting_Term.quot_thm_rep) 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 code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = + let + val quot_thm = Lifting_Term.prove_quot_theorem lthy (get_body_types (rty, qty)) + in + if 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) ((code_eqn_thm_name, [add_abs_eqn_attrib]), [code_cert]) + end + else + lthy + end + +fun define_code_eq code_eqn_thm_name 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) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq]) + end + +fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = + if body_type rty = body_type qty then + define_code_eq code_eqn_thm_name def_thm lthy + else + define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy + + +fun add_lift_def var qty rhs rsp_thm lthy = + let + val rty = fastype_of rhs + val absrep_trm = Lifting_Term.absrep_fun lthy (rty, qty) + val rty_forced = (domain_type o fastype_of) absrep_trm + val forced_rhs = force_rty_type lthy rty_forced rhs + val lhs = Free (Binding.print (#1 var), qty) + val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs) + val (_, prop') = Local_Defs.cert_def lthy prop + val (_, newrhs) = Local_Defs.abs_def prop' + + val ((_, (_ , def_thm)), lthy') = + Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy + + fun qualify defname suffix = Binding.name suffix + |> Binding.qualify true defname + + val lhs_name = Binding.name_of (#1 var) + val rsp_thm_name = qualify lhs_name "rsp" + val code_eqn_thm_name = qualify lhs_name "rep_eq" + in + lthy' + |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm]) + |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty) + 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 lift_def_cmd (raw_var, rhs_raw) lthy = + let + val ((binding, SOME qty, mx), ctxt) = yield_singleton Proof_Context.read_vars raw_var lthy + val rhs = (Syntax.check_term ctxt o Syntax.parse_term ctxt) rhs_raw + + 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) + | _ => NONE + end + + val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty) + val rty_forced = (domain_type o fastype_of) rsp_rel; + val forced_rhs = force_rty_type lthy rty_forced rhs; + val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_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 + add_lift_def (binding, mx) qty rhs internal_rsp_thm lthy + end + + in + case maybe_proven_rsp_thm of + SOME _ => Proof.theorem NONE after_qed [] lthy + | NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy + end + +(* parser and command *) +val liftdef_parser = + ((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2) + --| @{keyword "is"} -- Parse.term + +val _ = + Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"} + "definition for constants over the quotient type" + (liftdef_parser >> lift_def_cmd) + + +end; (* structure *) diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Tools/Lifting/lifting_info.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Tue Apr 03 20:56:32 2012 +0200 @@ -0,0 +1,125 @@ +(* Title: HOL/Tools/Lifting/lifting_info.ML + Author: Ondrej Kuncar + +Context data for the lifting package. +*) + +signature LIFTING_INFO = +sig + 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 + + type quotients = {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 + val update_quotients: string -> quotients -> Context.generic -> Context.generic + val dest_quotients: Proof.context -> quotients list + val print_quotients: Proof.context -> unit + + val setup: theory -> theory +end; + +structure Lifting_Info: LIFTING_INFO = +struct + +(** data containers **) + +(* FIXME just one data slot (record) per program unit *) + +(* info about map- and rel-functions for a type *) +type quotmaps = {relmap: string, quot_thm: thm} + +structure Quotmaps = Generic_Data +( + type T = quotmaps Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data = Symtab.merge (K true) data +) + +val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof +val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory + +(* FIXME export proper internal update operation!? *) + +val quotmaps_attribute_setup = + Attrib.setup @{binding map} + ((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, quot_thm}) = + Pretty.block (separate (Pretty.brk 2) + [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:" + |> Pretty.writeln + end + +(* info about quotient types *) +type quotients = {quot_thm: thm} + +structure Quotients = Generic_Data +( + type T = quotients Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data = Symtab.merge (K true) data +) + +fun transform_quotients phi {quot_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 + +fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo)) + +fun dest_quotients ctxt = (* FIXME slightly expensive way to retrieve data *) + map snd (Symtab.dest (Quotients.get (Context.Proof ctxt))) + +fun print_quotients ctxt = + let + fun prt_quot (qty_name, {quot_thm}) = + Pretty.block (separate (Pretty.brk 2) + [Pretty.str "type:", + Pretty.str qty_name, + Pretty.str "quot. thm:", + Syntax.pretty_term ctxt (prop_of quot_thm)]) + in + map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt))) + |> Pretty.big_list "quotients:" + |> Pretty.writeln + end + +(* theory setup *) + +val setup = + quotmaps_attribute_setup + +(* outer syntax commands *) + +val _ = + Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions" + (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of))) + +val _ = + Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients" + (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of))) + +end; \ No newline at end of file diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Tools/Lifting/lifting_setup.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Apr 03 20:56:32 2012 +0200 @@ -0,0 +1,113 @@ +(* Title: HOL/Tools/Lifting/lifting_setup.ML + Author: Ondrej Kuncar + +Setting the lifting infranstructure up. +*) + +signature LIFTING_SETUP = +sig + exception SETUP_LIFTING_INFR of string + + val setup_lifting_infr: thm -> thm -> local_theory -> local_theory + + val setup_by_typedef_thm: thm -> local_theory -> local_theory +end; + +structure Lifting_Seup: LIFTING_SETUP = +struct + +infix 0 MRSL + +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm + +exception SETUP_LIFTING_INFR of string + +fun define_cr_rel equiv_thm abs_fun lthy = + let + fun force_type_of_rel rel forced_ty = + let + val thy = Proof_Context.theory_of lthy + val rel_ty = (domain_type o fastype_of) rel + val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty + in + Envir.subst_term_types ty_inst rel + end + + val (rty, qty) = (dest_funT o fastype_of) abs_fun + val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0) + val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of + Const (@{const_name equivp}, _) $ _ => abs_fun_graph + | Const (@{const_name part_equivp}, _) $ rel => + HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph) + | _ => raise SETUP_LIFTING_INFR "unsopported equivalence theorem" + ) + val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body)); + val qty_name = (fst o dest_Type) qty + val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name) + val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy + val ((_, (_ , def_thm)), lthy'') = + Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy' + in + (def_thm, lthy'') + end + +fun define_abs_type quot_thm lthy = + if Lifting_Def.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 setup_lifting_infr quot_thm equiv_thm lthy = + let + val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm + val qty_full_name = (fst o dest_Type) qtyp + val quotients = { quot_thm = quot_thm } + fun quot_info phi = Lifting_Info.transform_quotients phi quotients + in + lthy + |> Local_Theory.declaration {syntax = false, pervasive = true} + (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) + |> define_abs_type quot_thm + end + +fun setup_by_typedef_thm typedef_thm lthy = + let + fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy = + let + val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm + val equiv_thm = typedef_thm RS to_equiv_thm + val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy + val quot_thm = [typedef_thm, T_def] MRSL to_quot_thm + in + (quot_thm, equiv_thm, lthy') + end + + val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm + val (quot_thm, equiv_thm, lthy') = (case typedef_set of + Const ("Orderings.top_class.top", _) => + derive_quot_and_equiv_thm @{thm copy_type_to_Quotient} @{thm copy_type_to_equivp} + typedef_thm lthy + | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => + derive_quot_and_equiv_thm @{thm invariant_type_to_Quotient} @{thm invariant_type_to_part_equivp} + typedef_thm lthy + | _ => raise SETUP_LIFTING_INFR "unsupported typedef theorem") + in + setup_lifting_infr quot_thm equiv_thm lthy' + end + +fun setup_by_typedef_thm_aux xthm lthy = setup_by_typedef_thm (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_by_typedef_thm_aux xthm)) + +end; diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Tools/Lifting/lifting_term.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Tue Apr 03 20:56:32 2012 +0200 @@ -0,0 +1,173 @@ +(* Title: HOL/Tools/Lifting/lifting_term.ML + Author: Ondrej Kuncar + +Proves Quotient theorem. +*) + +signature LIFTING_TERM = +sig + val prove_quot_theorem: Proof.context -> typ * typ -> thm + + val absrep_fun: Proof.context -> typ * typ -> term + + (* Allows Nitpick to represent quotient types as single elements from raw type *) + (* val absrep_const_chk: Proof.context -> flag -> string -> term *) + + val equiv_relation: Proof.context -> typ * typ -> term + + val quot_thm_rel: thm -> term + val quot_thm_abs: thm -> term + val quot_thm_rep: thm -> term + val quot_thm_rty_qty: thm -> typ * typ +end + +structure Lifting_Term: LIFTING_TERM = +struct + +exception LIFT_MATCH of string + +(* matches a type pattern with a type *) +fun match ctxt err ty_pat ty = + let + val thy = Proof_Context.theory_of ctxt + in + Sign.typ_match thy (ty_pat, ty) Vartab.empty + handle Type.TYPE_MATCH => err ctxt ty_pat ty + end + +fun equiv_match_err ctxt ty_pat ty = + let + val ty_pat_str = Syntax.string_of_typ ctxt ty_pat + val ty_str = Syntax.string_of_typ ctxt ty + in + raise LIFT_MATCH (space_implode " " + ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) + end + +(* generation of the Quotient theorem *) + +exception QUOT_THM of string + +fun get_quot_thm ctxt s = + let + val thy = Proof_Context.theory_of ctxt + in + (case Lifting_Info.lookup_quotients ctxt s of + SOME qdata => Thm.transfer thy (#quot_thm qdata) + | NONE => raise QUOT_THM ("No quotient type " ^ quote s ^ " found.")) + end + +fun get_rel_quot_thm ctxt s = + let + val thy = Proof_Context.theory_of ctxt + in + (case Lifting_Info.lookup_quotmaps ctxt s of + SOME map_data => Thm.transfer thy (#quot_thm map_data) + | NONE => raise QUOT_THM ("get_relmap (no relation map function found for type " ^ s ^ ")")) + end + +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 quot_thm_rel quot_thm = + let + val (Const (@{const_name Quotient}, _) $ rel $ _ $ _ $ _) = + (HOLogic.dest_Trueprop o prop_of) quot_thm + in + rel + end + +fun quot_thm_abs quot_thm = + let + val (Const (@{const_name Quotient}, _) $ _ $ abs $ _ $ _) = + (HOLogic.dest_Trueprop o prop_of) quot_thm + in + abs + end + +fun quot_thm_rep quot_thm = + let + val (Const (@{const_name Quotient}, _) $ _ $ _ $ rep $ _) = + (HOLogic.dest_Trueprop o prop_of) quot_thm + in + rep + end + +fun quot_thm_rty_qty quot_thm = + let + val abs = quot_thm_abs quot_thm + val abs_type = fastype_of abs + in + (domain_type abs_type, range_type abs_type) + end + +fun prove_quot_theorem ctxt (rty, qty) = + 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 + if forall is_id_quot args + then + @{thm identity_quotient} + else + args MRSL (get_rel_quot_thm ctxt s) + end + else + let + val quot_thm = get_quot_thm ctxt s' + val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm + 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') + 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 + [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose} + end + end + | _ => @{thm identity_quotient} + +fun force_qty_type thy qty quot_thm = + let + val abs_schematic = quot_thm_abs quot_thm + val qty_schematic = (range_type o fastype_of) abs_schematic + val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty + fun prep_ty thy (x, (S, ty)) = + (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) + val ty_inst = Vartab.fold (cons o (prep_ty thy)) match_env [] + in + Thm.instantiate (ty_inst, []) quot_thm + end + +fun absrep_fun ctxt (rty, qty) = + let + val thy = Proof_Context.theory_of ctxt + val quot_thm = prove_quot_theorem ctxt (rty, qty) + val forced_quot_thm = force_qty_type thy qty quot_thm + in + quot_thm_abs forced_quot_thm + end + +fun equiv_relation ctxt (rty, qty) = + let + val thy = Proof_Context.theory_of ctxt + val quot_thm = prove_quot_theorem ctxt (rty, qty) + val forced_quot_thm = force_qty_type thy qty quot_thm + in + quot_thm_rel forced_quot_thm + end + +end; diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Apr 03 20:56:32 2012 +0200 @@ -86,7 +86,7 @@ let val quot_thm = Quotient_Term.prove_quot_theorem ctxt args_ty in - [quot_thm, thm] MRSL @{thm apply_rsp''} + [quot_thm, thm] MRSL @{thm apply_rspQ3''} end in fold disch_arg ty_args rsp_thm @@ -101,11 +101,11 @@ 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_thm = [quot_thm, fun_rel] MRSL @{thm Quotient3_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} + | Const (@{const_name Lifting.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 diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Tools/Quotient/quotient_info.ML --- a/src/HOL/Tools/Quotient/quotient_info.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Tue Apr 03 20:56:32 2012 +0200 @@ -70,7 +70,7 @@ (* FIXME export proper internal update operation!? *) val quotmaps_attribute_setup = - Attrib.setup @{binding map} + Attrib.setup @{binding mapQ3} ((Args.type_name true --| Scan.lift @{keyword "="}) -- (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} -- Attrib.thm --| Scan.lift @{keyword ")"}) >> @@ -298,11 +298,11 @@ (* outer syntax commands *) val _ = - Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions" + Outer_Syntax.improper_command @{command_spec "print_quotmapsQ3"} "print quotient map functions" (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of))) val _ = - Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients" + Outer_Syntax.improper_command @{command_spec "print_quotientsQ3"} "print quotients" (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of))) val _ = diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Apr 03 20:56:32 2012 +0200 @@ -62,7 +62,7 @@ fun quotient_tac ctxt = (REPEAT_ALL_NEW (FIRST' - [rtac @{thm identity_quotient}, + [rtac @{thm identity_quotient3}, resolve_tac (Quotient_Info.quotient_rules ctxt)])) fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) @@ -259,7 +259,7 @@ val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; val inst_thm = Drule.instantiate' ty_inst - ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} + ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3} in (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1 end @@ -529,7 +529,7 @@ val prs = Quotient_Info.prs_rules lthy val ids = Quotient_Info.id_simps lthy val thms = - @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs + @{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver in diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Tue Apr 03 20:56:32 2012 +0200 @@ -356,7 +356,7 @@ | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")")) end -fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient}) +fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient3}) infix 0 MRSL @@ -375,13 +375,13 @@ 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} + if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient3} else raise NOT_IMPL "nested quotients: not implemented yet" end fun prove_quot_theorem ctxt (rty, qty) = if rty = qty - then @{thm identity_quotient} + then @{thm identity_quotient3} else case (rty, qty) of (Type (s, tys), Type (s', tys')) => @@ -410,7 +410,7 @@ mk_quot_thm_compose (rel_quot_thm, quot_thm) end end - | _ => @{thm identity_quotient} + | _ => @{thm identity_quotient3} diff -r 432b29a96f61 -r dac11ab96277 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Tue Apr 03 20:56:32 2012 +0200 @@ -82,13 +82,13 @@ 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 + | Const (@{const_name Lifting.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 abs_type_thm = quot_thm RS @{thm Quotient3_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); @@ -157,7 +157,7 @@ val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3 (* quotient theorem *) - val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name + val quotient_thm_name = Binding.prefix_name "Quotient3_" qty_name val quotient_thm = (quot_thm RS @{thm quot_type.Quotient}) |> fold_rule [abs_def, rep_def] @@ -313,30 +313,5 @@ "quotient type definitions (require equivalence proofs)" (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 432b29a96f61 -r dac11ab96277 src/HOL/ex/Executable_Relation.thy --- a/src/HOL/ex/Executable_Relation.thy Tue Apr 03 15:15:00 2012 +0200 +++ b/src/HOL/ex/Executable_Relation.thy Tue Apr 03 20:56:32 2012 +0200 @@ -67,11 +67,11 @@ lemma [simp]: "rel_of_set (set_of_rel S) = S" -by (rule Quotient_abs_rep[OF Quotient_rel]) +by (rule Quotient3_abs_rep[OF Quotient3_rel]) lemma [simp]: "set_of_rel (rel_of_set R) = R" -by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl) +by (rule Quotient3_rep_abs[OF Quotient3_rel]) (rule refl) lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"] diff -r 432b29a96f61 -r dac11ab96277 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/Pure/Isar/class.ML Tue Apr 03 20:56:32 2012 +0200 @@ -486,13 +486,12 @@ ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v)) ##> Local_Theory.map_contexts (K synchronize_inst_syntax); -fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = +fun foundation (((b, U), mx), (b_def, rhs)) params lthy = (case instantiation_param lthy b of SOME c => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs) - | NONE => lthy |> - Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)); + | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params); fun pretty lthy = let @@ -553,10 +552,8 @@ |> Local_Theory.init naming {define = Generic_Target.define foundation, notes = Generic_Target.notes Generic_Target.theory_notes, - abbrev = Generic_Target.abbrev - (fn prmode => fn (b, mx) => fn (t, _) => fn _ => - Generic_Target.theory_abbrev prmode ((b, mx), t)), - declaration = K Generic_Target.standard_declaration, + abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev, + declaration = K Generic_Target.theory_declaration, pretty = pretty, exit = Local_Theory.target_of o conclude} end; diff -r 432b29a96f61 -r dac11ab96277 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/Pure/Isar/expression.ML Tue Apr 03 20:56:32 2012 +0200 @@ -43,12 +43,9 @@ (Attrib.binding * term) list -> theory -> Proof.state val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression -> (Attrib.binding * string) list -> theory -> Proof.state - val interpretation: expression_i -> (Attrib.binding * term) list -> - theory -> Proof.state - val interpretation_cmd: expression -> (Attrib.binding * string) list -> - theory -> Proof.state - val interpret: expression_i -> (Attrib.binding * term) list -> - bool -> Proof.state -> Proof.state + val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state + val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state + val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state val interpret_cmd: expression -> (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state diff -r 432b29a96f61 -r dac11ab96277 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/Pure/Isar/generic_target.ML Tue Apr 03 20:56:32 2012 +0200 @@ -24,15 +24,23 @@ term list -> local_theory -> local_theory) -> string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val background_declaration: declaration -> local_theory -> local_theory - val standard_declaration: declaration -> local_theory -> local_theory val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory + val standard_declaration: (int -> bool) -> declaration -> local_theory -> local_theory + val generic_const: bool -> Syntax.mode -> (binding * mixfix) * term -> + Context.generic -> Context.generic + val const_declaration: (int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> + local_theory -> local_theory + val background_foundation: ((binding * typ) * mixfix) * (binding * term) -> + term list * term list -> local_theory -> (term * thm) * local_theory val theory_foundation: ((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory - val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory + val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term * term -> term list -> + local_theory -> local_theory + val theory_declaration: declaration -> local_theory -> local_theory end structure Generic_Target: GENERIC_TARGET = @@ -52,6 +60,11 @@ else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))); NoSyn); +fun check_mixfix_global (b, no_params) mx = + if no_params orelse mx = NoSyn then mx + else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ + Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn); + (* define *) @@ -61,21 +74,17 @@ val thy_ctxt = Proof_Context.init_global thy; (*term and type parameters*) - val crhs = Thm.cterm_of thy rhs; - val ((defs, _), rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of; + val ((defs, _), rhs') = Thm.cterm_of thy rhs + |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of; - val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' []; + val xs = Variable.add_fixed lthy rhs' []; val T = Term.fastype_of rhs; val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []); val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs [])); val mx' = check_mixfix lthy (b, extra_tfrees) mx; val type_params = map (Logic.mk_type o TFree) extra_tfrees; - val target_ctxt = Local_Theory.target_of lthy; - val term_params = - filter (Variable.is_fixed target_ctxt o #1) xs - |> sort (Variable.fixed_ord target_ctxt o pairself #1) - |> map Free; + val term_params = map Free (sort (Variable.fixed_ord lthy o pairself #1) xs); val params = type_params @ term_params; val U = map Term.fastype_of params ---> T; @@ -184,18 +193,15 @@ fun abbrev target_abbrev prmode ((b, mx), t) lthy = let val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); - val target_ctxt = Local_Theory.target_of lthy; - val t' = Assumption.export_term lthy target_ctxt t; - val xs = map Free (rev (Variable.add_fixed target_ctxt t' [])); + val t' = Assumption.export_term lthy (Local_Theory.target_of lthy) t; + val xs = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy t' [])); val u = fold_rev lambda xs t'; + val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; val extra_tfrees = subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []); val mx' = check_mixfix lthy (b, extra_tfrees) mx; - - val global_rhs = - singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u; in lthy |> target_abbrev prmode (b, mx') (global_rhs, t') xs @@ -213,31 +219,83 @@ (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl; in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end; -fun standard_declaration decl = - background_declaration decl #> - (fn lthy => Local_Theory.map_contexts (fn _ => fn ctxt => - Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy); - fun locale_declaration locale syntax decl lthy = lthy |> Local_Theory.target (fn ctxt => ctxt |> Locale.add_declaration locale syntax (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl)); +fun standard_declaration pred decl lthy = + Local_Theory.map_contexts (fn level => fn ctxt => + if pred level then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt + else ctxt) lthy; + + +(* const declaration *) + +fun generic_const same_shape prmode ((b, mx), t) context = + let + val const_alias = + if same_shape then + (case t of + Const (c, T) => + let + val thy = Context.theory_of context; + val ctxt = Context.proof_of context; + in + (case Type_Infer_Context.const_type ctxt c of + SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE + | NONE => NONE) + end + | _ => NONE) + else NONE; + in + (case const_alias of + SOME c => + context + |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c) + |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)]) + | NONE => + context + |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, Term.close_schematic_term t) + |-> (fn (const as Const (c, _), _) => same_shape ? + (Proof_Context.generic_revert_abbrev (#1 prmode) c #> + Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) + end; + +fun const_declaration pred prmode ((b, mx), rhs) = + standard_declaration pred (fn phi => + let + val b' = Morphism.binding phi b; + val rhs' = Morphism.term phi rhs; + val same_shape = Term.aconv_untyped (rhs, rhs'); + in generic_const same_shape prmode ((b', mx), rhs') end); + (** primitive theory operations **) -fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = +fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = let + val params = type_params @ term_params; + val mx' = check_mixfix_global (b, null params) mx; + val (const, lthy2) = lthy - |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx)); - val lhs = list_comb (const, type_params @ term_params); + |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx')); + val lhs = Term.list_comb (const, params); + val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result (Thm.add_def lthy2 false false (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))); in ((lhs, def), lthy3) end; +fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) = + background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) + #-> (fn (lhs, def) => fn lthy' => lthy' |> + const_declaration (fn level => level <> Local_Theory.level lthy') + Syntax.mode_default ((b, mx), lhs) + |> pair (lhs, def)); + fun theory_notes kind global_facts local_facts = Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #> (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt => @@ -246,9 +304,16 @@ ctxt |> Attrib.local_notes kind (Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd)); -fun theory_abbrev prmode ((b, mx), t) = - Local_Theory.background_theory +fun theory_abbrev prmode (b, mx) (t, _) xs = + Local_Theory.background_theory_result (Sign.add_abbrev (#1 prmode) (b, t) #-> - (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)])); + (fn (lhs, _) => (* FIXME type_params!? *) + Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs)) + #-> (fn lhs => fn lthy' => lthy' |> + const_declaration (fn level => level <> Local_Theory.level lthy') prmode + ((b, if null xs then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, xs))); + +fun theory_declaration decl = + background_declaration decl #> standard_declaration (K true) decl; end; diff -r 432b29a96f61 -r dac11ab96277 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/Pure/Isar/local_defs.ML Tue Apr 03 20:56:32 2012 +0200 @@ -135,22 +135,22 @@ let val exp = Assumption.export false inner outer; val exp_term = Assumption.export_term inner outer; - val prems = Assumption.local_prems_of inner outer; + val asms = Assumption.local_assms_of inner outer; in fn th => let val th' = exp th; - val defs_asms = prems |> map (fn prem => - (case try (head_of_def o Thm.prop_of) prem of - NONE => (prem, false) + val defs_asms = asms |> map (Thm.assume #> (fn asm => + (case try (head_of_def o Thm.prop_of) asm of + NONE => (asm, false) | SOME x => let val t = Free x in (case try exp_term t of - NONE => (prem, false) + NONE => (asm, false) | SOME u => - if t aconv u then (prem, false) - else (Drule.abs_def prem, true)) - end)); + if t aconv u then (asm, false) + else (Drule.abs_def (Drule.gen_all asm), true)) + end))); in (pairself (map #1) (List.partition #2 defs_asms), th') end end; diff -r 432b29a96f61 -r dac11ab96277 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/Pure/Isar/local_theory.ML Tue Apr 03 20:56:32 2012 +0200 @@ -11,6 +11,7 @@ sig type operations val assert: local_theory -> local_theory + val restore: local_theory -> local_theory val level: Proof.context -> int val assert_bottom: bool -> local_theory -> local_theory val open_target: Name_Space.naming -> operations -> local_theory -> local_theory @@ -54,7 +55,6 @@ val type_alias: binding -> string -> local_theory -> local_theory val const_alias: binding -> string -> local_theory -> local_theory val init: Name_Space.naming -> operations -> Proof.context -> local_theory - val restore: local_theory -> local_theory val exit: local_theory -> Proof.context val exit_global: local_theory -> theory val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context @@ -107,6 +107,8 @@ Data.map (fn {naming, operations, target} :: parents => make_lthy (f (naming, operations, target)) :: parents); +fun restore lthy = #target (get_first_lthy lthy) |> Data.put (Data.get lthy); + (* nested structure *) @@ -126,7 +128,7 @@ |> Data.map (cons (make_lthy (naming, operations, target))); fun close_target lthy = - assert_bottom false lthy |> Data.map tl; + assert_bottom false lthy |> Data.map tl |> restore; fun map_contexts f lthy = let val n = level lthy in @@ -281,10 +283,6 @@ | _ => error "Local theory already initialized") |> checkpoint; -fun restore lthy = - let val {naming, operations, target} = get_first_lthy lthy - in init naming operations target end; - (* exit *) diff -r 432b29a96f61 -r dac11ab96277 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/Pure/Isar/named_target.ML Tue Apr 03 20:56:32 2012 +0200 @@ -46,12 +46,11 @@ (* consts in locale *) -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) = +fun locale_const (Target {target, is_class, ...}) prmode ((b, mx), rhs) = Generic_Target.locale_declaration target true (fn phi => let val b' = Morphism.binding phi b; val rhs' = Morphism.term phi rhs; - val arg = (b', Term.close_schematic_term rhs'); val same_shape = Term.aconv_untyped (rhs, rhs'); (* FIXME workaround based on educated guess *) @@ -62,31 +61,24 @@ andalso List.last prefix' = (Class.class_prefix target, false) orelse same_shape); in - not is_canonical_class ? - (Context.mapping_result - (Sign.add_abbrev Print_Mode.internal arg) - (Proof_Context.add_abbrev Print_Mode.internal arg) - #-> (fn (lhs' as Const (d, _), _) => - same_shape ? - (Context.mapping - (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #> - Morphism.form (Proof_Context.generic_notation true prmode [(lhs', mx)])))) - end); + not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs') + end) #> + (fn lthy => lthy |> Generic_Target.const_declaration + (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs)); (* define *) -fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) = - Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) +fun locale_foundation ta (((b, U), mx), (b_def, rhs)) params = + Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs) - #> pair (lhs, def)) + #> pair (lhs, def)); -fun class_foundation (ta as Target {target, ...}) - (((b, U), mx), (b_def, rhs)) (type_params, term_params) = - Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) +fun class_foundation (ta as Target {target, ...}) (((b, U), mx), (b_def, rhs)) params = + Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs) - #> Class.const target ((b, mx), (type_params, lhs)) - #> pair (lhs, def)) + #> Class.const target ((b, mx), (#1 params, lhs)) + #> pair (lhs, def)); fun target_foundation (ta as Target {is_locale, is_class, ...}) = if is_class then class_foundation ta @@ -106,31 +98,26 @@ fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t)) #-> - (fn (lhs, _) => locale_const ta prmode - ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); + (fn (lhs, _) => + locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); -fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) - prmode (b, mx) (global_rhs, t') xs lthy = +fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (t, t') xs lthy = if is_locale then lthy - |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs + |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), t) xs |> is_class ? Class.abbrev target prmode ((b, mx), t') - else - lthy - |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs); + else lthy |> Generic_Target.theory_abbrev prmode (b, mx) (t, t') xs; (* declaration *) fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy = - if target = "" then Generic_Target.standard_declaration decl lthy + if target = "" then Generic_Target.theory_declaration decl lthy else lthy |> pervasive ? Generic_Target.background_declaration decl |> Generic_Target.locale_declaration target syntax decl - |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt => - if level = 0 then ctxt - else Context.proof_map (Local_Theory.standard_form lthy' ctxt decl) ctxt)); + |> (fn lthy' => lthy' |> Generic_Target.standard_declaration (fn level => level <> 0) decl); (* pretty *) @@ -192,7 +179,7 @@ Local_Theory.assert_bottom true #> Data.get #> the #> (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target); -fun context_cmd ("-", _) thy = init I "" thy +fun context_cmd ("-", _) thy = theory_init thy | context_cmd target thy = init I (Locale.check thy target) thy; end; diff -r 432b29a96f61 -r dac11ab96277 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/Pure/Isar/overloading.ML Tue Apr 03 20:56:32 2012 +0200 @@ -158,14 +158,13 @@ ##> Local_Theory.map_contexts (K synchronize_syntax) #-> (fn (_, def) => pair (Const (c, U), def)); -fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = +fun foundation (((b, U), mx), (b_def, rhs)) params lthy = (case operation lthy b of SOME (c, (v, checked)) => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs) - | NONE => lthy - |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)); + | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params); fun pretty lthy = let @@ -204,10 +203,8 @@ |> Local_Theory.init naming {define = Generic_Target.define foundation, notes = Generic_Target.notes Generic_Target.theory_notes, - abbrev = Generic_Target.abbrev - (fn prmode => fn (b, mx) => fn (t, _) => fn _ => - Generic_Target.theory_abbrev prmode ((b, mx), t)), - declaration = K Generic_Target.standard_declaration, + abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev, + declaration = K Generic_Target.theory_declaration, pretty = pretty, exit = Local_Theory.target_of o conclude} end; diff -r 432b29a96f61 -r dac11ab96277 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Apr 03 20:56:32 2012 +0200 @@ -146,6 +146,9 @@ val add_const_constraint: string * typ option -> Proof.context -> Proof.context val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context val revert_abbrev: string -> string -> Proof.context -> Proof.context + val generic_add_abbrev: string -> binding * term -> Context.generic -> + (term * term) * Context.generic + val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic val print_syntax: Proof.context -> unit val print_abbrevs: Proof.context -> unit val print_binds: Proof.context -> unit @@ -1021,6 +1024,12 @@ fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c); +fun generic_add_abbrev mode arg = + Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg); + +fun generic_revert_abbrev mode arg = + Context.mapping (Sign.revert_abbrev mode arg) (revert_abbrev mode arg); + (* fixes *) diff -r 432b29a96f61 -r dac11ab96277 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/Pure/Isar/toplevel.ML Tue Apr 03 20:56:32 2012 +0200 @@ -109,13 +109,12 @@ val loc_init = Named_Target.context_cmd; val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global; -fun loc_begin loc (Context.Theory thy) = loc_init (the_default ("-", Position.none) loc) thy - | loc_begin NONE (Context.Proof lthy) = lthy - | loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy; - -fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit - | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore - | loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o Named_Target.reinit lthy; +fun loc_begin loc (Context.Theory thy) = + (Context.Theory o loc_exit, loc_init (the_default ("-", Position.none) loc) thy) + | loc_begin NONE (Context.Proof lthy) = + (Context.Proof o Local_Theory.restore, lthy) + | loc_begin (SOME loc) (Context.Proof lthy) = + (Context.Proof o Named_Target.reinit lthy, loc_init loc (loc_exit lthy)); (* datatype node *) @@ -477,8 +476,8 @@ fun local_theory_presentation loc f = present_transaction (fn int => (fn Theory (gthy, _) => let - val finish = loc_finish loc gthy; - val lthy' = loc_begin loc gthy + val (finish, lthy) = loc_begin loc gthy; + val lthy' = lthy |> local_theory_group |> f int |> Local_Theory.reset_group; @@ -511,34 +510,37 @@ local -fun begin_proof init finish = transaction (fn int => +fun begin_proof init = transaction (fn int => (fn Theory (gthy, _) => let - val prf = init int gthy; + val (finish, prf) = init int gthy; val skip = ! skip_proofs; val (is_goal, no_skip) = (true, Proof.schematic_goal prf) handle ERROR _ => (false, true); + val _ = + if is_goal andalso skip andalso no_skip then + warning "Cannot skip proof of schematic goal statement" + else (); in - if is_goal andalso skip andalso no_skip then - warning "Cannot skip proof of schematic goal statement" - else (); if skip andalso not no_skip then - SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy)) - else Proof (Proof_Node.init prf, (finish gthy, gthy)) + SkipProof (0, (finish (Proof.global_skip_proof int prf), gthy)) + else Proof (Proof_Node.init prf, (finish, gthy)) end | _ => raise UNDEF)); in fun local_theory_to_proof' loc f = begin_proof - (fn int => fn gthy => f int (local_theory_group (loc_begin loc gthy))) - (fn gthy => loc_finish loc gthy o Local_Theory.reset_group); + (fn int => fn gthy => + let val (finish, lthy) = loc_begin loc gthy + in (finish o Local_Theory.reset_group, f int (local_theory_group lthy)) end); fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); fun theory_to_proof f = begin_proof - (K (fn Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF)) - (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of)); + (fn _ => fn gthy => + (Context.Theory o Sign.reset_group o Proof_Context.theory_of, + (case gthy of Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF))); end; diff -r 432b29a96f61 -r dac11ab96277 src/Pure/type_infer_context.ML --- a/src/Pure/type_infer_context.ML Tue Apr 03 15:15:00 2012 +0200 +++ b/src/Pure/type_infer_context.ML Tue Apr 03 20:56:32 2012 +0200 @@ -7,6 +7,7 @@ signature TYPE_INFER_CONTEXT = sig val const_sorts: bool Config.T + val const_type: Proof.context -> string -> typ option val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list val prepare: Proof.context -> term list -> int * term list val infer_types: Proof.context -> term list -> term list