# HG changeset patch # User haftmann # Date 1266594750 -3600 # Node ID 5d7f22e0f95616eec826ae4ae91b48ada2e23aff # Parent 04673275441a1c33d1bdb9f77844008ef6b2701a# Parent d4ec25836a787ae332845e344b945fb792b557bc merged diff -r 04673275441a -r 5d7f22e0f956 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Feb 19 16:52:00 2010 +0100 +++ b/src/HOL/IsaMakefile Fri Feb 19 16:52:30 2010 +0100 @@ -52,6 +52,7 @@ HOL-Nominal-Examples \ HOL-Number_Theory \ HOL-Old_Number_Theory \ + HOL-Quotient_Examples \ HOL-Probability \ HOL-Prolog \ HOL-Proofs-Extraction \ @@ -265,6 +266,7 @@ Presburger.thy \ Predicate_Compile.thy \ Quickcheck.thy \ + Quotient.thy \ Random.thy \ Random_Sequence.thy \ Recdef.thy \ @@ -307,6 +309,11 @@ Tools/Qelim/generated_cooper.ML \ Tools/Qelim/presburger.ML \ Tools/Qelim/qelim.ML \ + Tools/Quotient/quotient_def.ML \ + Tools/Quotient/quotient_info.ML \ + Tools/Quotient/quotient_tacs.ML \ + Tools/Quotient/quotient_term.ML \ + Tools/Quotient/quotient_typ.ML \ Tools/recdef.ML \ Tools/res_atp.ML \ Tools/res_axioms.ML \ @@ -407,7 +414,10 @@ Library/Diagonalize.thy Library/RBT.thy Library/Univ_Poly.thy \ Library/Poly_Deriv.thy Library/Polynomial.thy Library/Preorder.thy \ Library/Product_plus.thy Library/Product_Vector.thy Library/Tree.thy \ - Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML \ + Library/Enum.thy Library/Float.thy Library/Quotient_List.thy \ + Library/Quotient_Option.thy Library/Quotient_Product.thy \ + Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \ + $(SRC)/Tools/float.ML \ $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML \ Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy \ Library/OptionalSugar.thy Library/SML_Quickcheck.thy @@ -1273,6 +1283,15 @@ @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle +## HOL-Quotient_Examples + +HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz + +$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \ + Quotient_Examples/LarryInt.thy Quotient_Examples/LarryDatatype.thy + @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples + + ## clean clean: diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Fri Feb 19 16:52:00 2010 +0100 +++ b/src/HOL/Library/Library.thy Fri Feb 19 16:52:30 2010 +0100 @@ -45,6 +45,11 @@ Preorder Product_Vector Quicksort + Quotient_List + Quotient_Option + Quotient_Product + Quotient_Sum + Quotient_Syntax Quotient_Type Ramsey Reflection diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Library/Quotient_List.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Quotient_List.thy Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,232 @@ +(* Title: Quotient_List.thy + Author: Cezary Kaliszyk and Christian Urban +*) +theory Quotient_List +imports Main Quotient_Syntax +begin + +section {* Quotient infrastructure for the list type. *} + +fun + list_rel +where + "list_rel R [] [] = True" +| "list_rel R (x#xs) [] = False" +| "list_rel R [] (x#xs) = False" +| "list_rel R (x#xs) (y#ys) = (R x y \ list_rel R xs ys)" + +declare [[map list = (map, list_rel)]] + +lemma split_list_all: + shows "(\x. P x) \ P [] \ (\x xs. P (x#xs))" + apply(auto) + apply(case_tac x) + apply(simp_all) + done + +lemma map_id[id_simps]: + shows "map id = id" + apply(simp add: expand_fun_eq) + apply(rule allI) + apply(induct_tac x) + apply(simp_all) + done + + +lemma list_rel_reflp: + shows "equivp R \ list_rel R xs xs" + apply(induct xs) + apply(simp_all add: equivp_reflp) + done + +lemma list_rel_symp: + assumes a: "equivp R" + shows "list_rel R xs ys \ list_rel R ys xs" + apply(induct xs ys rule: list_induct2') + apply(simp_all) + apply(rule equivp_symp[OF a]) + apply(simp) + done + +lemma list_rel_transp: + assumes a: "equivp R" + shows "list_rel R xs1 xs2 \ list_rel R xs2 xs3 \ list_rel R xs1 xs3" + apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2') + apply(simp_all) + apply(case_tac xs3) + apply(simp_all) + apply(rule equivp_transp[OF a]) + apply(auto) + done + +lemma list_equivp[quot_equiv]: + assumes a: "equivp R" + shows "equivp (list_rel R)" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + apply(subst split_list_all) + apply(simp add: equivp_reflp[OF a] list_rel_reflp[OF a]) + apply(blast intro: list_rel_symp[OF a]) + apply(blast intro: list_rel_transp[OF a]) + done + +lemma list_rel_rel: + assumes q: "Quotient R Abs Rep" + shows "list_rel R r s = (list_rel R r r \ list_rel R s s \ (map Abs r = map Abs s))" + apply(induct r s rule: list_induct2') + apply(simp_all) + using Quotient_rel[OF q] + apply(metis) + done + +lemma list_quotient[quot_thm]: + assumes q: "Quotient R Abs Rep" + shows "Quotient (list_rel R) (map Abs) (map Rep)" + unfolding Quotient_def + apply(subst split_list_all) + apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id) + apply(rule conjI) + apply(rule allI) + apply(induct_tac a) + apply(simp) + apply(simp) + apply(simp add: Quotient_rep_reflp[OF q]) + apply(rule allI)+ + apply(rule list_rel_rel[OF q]) + done + + +lemma cons_prs_aux: + assumes q: "Quotient R Abs Rep" + shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" + by (induct t) (simp_all add: Quotient_abs_rep[OF q]) + +lemma cons_prs[quot_preserve]: + assumes q: "Quotient R Abs Rep" + shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" + by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q]) + (simp) + +lemma cons_rsp[quot_respect]: + assumes q: "Quotient R Abs Rep" + shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)" + by (auto) + +lemma nil_prs[quot_preserve]: + assumes q: "Quotient R Abs Rep" + shows "map Abs [] = []" + by simp + +lemma nil_rsp[quot_respect]: + assumes q: "Quotient R Abs Rep" + shows "list_rel R [] []" + by simp + +lemma map_prs_aux: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient 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]) + + +lemma map_prs[quot_preserve]: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" + by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b]) + (simp) + + +lemma map_rsp[quot_respect]: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" + apply(simp) + apply(rule allI)+ + apply(rule impI) + apply(rule allI)+ + apply (induct_tac xa ya rule: list_induct2') + apply simp_all + done + +lemma foldr_prs_aux: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient 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]) + +lemma foldr_prs[quot_preserve]: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" + by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b]) + (simp) + +lemma foldl_prs_aux: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient 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]) + + +lemma foldl_prs[quot_preserve]: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" + by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b]) + (simp) + +lemma list_rel_empty: + shows "list_rel R [] b \ length b = 0" + by (induct b) (simp_all) + +lemma list_rel_len: + shows "list_rel R a b \ length a = length b" + apply (induct a arbitrary: b) + apply (simp add: list_rel_empty) + apply (case_tac b) + apply simp_all + done + +(* 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" + shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" + apply(auto) + apply (subgoal_tac "R1 xa ya \ list_rel R2 xb yb \ R1 (foldl x xa xb) (foldl y ya yb)") + apply simp + apply (rule_tac x="xa" in spec) + apply (rule_tac x="ya" in spec) + apply (rule_tac xs="xb" and ys="yb" in list_induct2) + apply (rule list_rel_len) + apply (simp_all) + done + +lemma foldr_rsp[quot_respect]: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr" + apply auto + apply(subgoal_tac "R2 xb yb \ list_rel R1 xa ya \ R2 (foldr x xa xb) (foldr y ya yb)") + apply simp + apply (rule_tac xs="xa" and ys="ya" in list_induct2) + apply (rule list_rel_len) + apply (simp_all) + done + +lemma list_rel_eq[id_simps]: + shows "(list_rel (op =)) = (op =)" + unfolding expand_fun_eq + apply(rule allI)+ + apply(induct_tac x xa rule: list_induct2') + apply(simp_all) + done + +lemma list_rel_refl: + assumes a: "\x y. R x y = (R x = R y)" + shows "list_rel R x x" + by (induct x) (auto simp add: a) + +end diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Library/Quotient_Option.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Quotient_Option.thy Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,80 @@ +(* Title: Quotient_Option.thy + Author: Cezary Kaliszyk and Christian Urban +*) +theory Quotient_Option +imports Main Quotient_Syntax +begin + +section {* Quotient infrastructure for the option type. *} + +fun + option_rel +where + "option_rel R None None = True" +| "option_rel R (Some x) None = False" +| "option_rel R None (Some x) = False" +| "option_rel R (Some x) (Some y) = R x y" + +declare [[map option = (Option.map, option_rel)]] + +text {* should probably be in Option.thy *} +lemma split_option_all: + shows "(\x. P x) \ P None \ (\a. P (Some a))" + apply(auto) + apply(case_tac x) + apply(simp_all) + done + +lemma option_quotient[quot_thm]: + assumes q: "Quotient R Abs Rep" + shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" + unfolding Quotient_def + apply(simp add: split_option_all) + apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) + using q + unfolding Quotient_def + apply(blast) + done + +lemma option_equivp[quot_equiv]: + assumes a: "equivp R" + shows "equivp (option_rel R)" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + apply(simp_all add: split_option_all) + apply(blast intro: equivp_reflp[OF a]) + apply(blast intro: equivp_symp[OF a]) + apply(blast intro: equivp_transp[OF a]) + done + +lemma option_None_rsp[quot_respect]: + assumes q: "Quotient R Abs Rep" + shows "option_rel R None None" + by simp + +lemma option_Some_rsp[quot_respect]: + assumes q: "Quotient R Abs Rep" + shows "(R ===> option_rel R) Some Some" + by simp + +lemma option_None_prs[quot_preserve]: + assumes q: "Quotient R Abs Rep" + shows "Option.map Abs None = None" + by simp + +lemma option_Some_prs[quot_preserve]: + assumes q: "Quotient R Abs Rep" + shows "(Rep ---> Option.map Abs) Some = Some" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q]) + done + +lemma option_map_id[id_simps]: + shows "Option.map id = id" + by (simp add: expand_fun_eq split_option_all) + +lemma option_rel_eq[id_simps]: + shows "option_rel (op =) = (op =)" + by (simp add: expand_fun_eq split_option_all) + +end diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Library/Quotient_Product.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Quotient_Product.thy Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,104 @@ +(* Title: Quotient_Product.thy + Author: Cezary Kaliszyk and Christian Urban +*) +theory Quotient_Product +imports Main Quotient_Syntax +begin + +section {* Quotient infrastructure for the product type. *} + +fun + prod_rel +where + "prod_rel R1 R2 = (\(a, b) (c, d). R1 a c \ R2 b d)" + +declare [[map * = (prod_fun, prod_rel)]] + + +lemma prod_equivp[quot_equiv]: + assumes a: "equivp R1" + assumes b: "equivp R2" + shows "equivp (prod_rel R1 R2)" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + apply(simp_all add: split_paired_all) + apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b]) + apply(blast intro: equivp_symp[OF a] equivp_symp[OF b]) + apply(blast intro: equivp_transp[OF a] equivp_transp[OF b]) + done + +lemma prod_quotient[quot_thm]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)" + unfolding Quotient_def + apply(simp add: split_paired_all) + apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1]) + apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) + using q1 q2 + unfolding Quotient_def + apply(blast) + done + +lemma Pair_rsp[quot_respect]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" + by simp + +lemma Pair_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + done + +lemma fst_rsp[quot_respect]: + assumes "Quotient R1 Abs1 Rep1" + assumes "Quotient R2 Abs2 Rep2" + shows "(prod_rel R1 R2 ===> R1) fst fst" + by simp + +lemma fst_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q1]) + done + +lemma snd_rsp[quot_respect]: + assumes "Quotient R1 Abs1 Rep1" + assumes "Quotient R2 Abs2 Rep2" + shows "(prod_rel R1 R2 ===> R2) snd snd" + by simp + +lemma snd_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q2]) + done + +lemma split_rsp[quot_respect]: + shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" + by auto + +lemma split_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split" + by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + +lemma prod_fun_id[id_simps]: + shows "prod_fun id id = id" + by (simp add: prod_fun_def) + +lemma prod_rel_eq[id_simps]: + shows "prod_rel (op =) (op =) = (op =)" + by (simp add: expand_fun_eq) + + +end diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Library/Quotient_Sum.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Quotient_Sum.thy Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,96 @@ +(* Title: Quotient_Sum.thy + Author: Cezary Kaliszyk and Christian Urban +*) +theory Quotient_Sum +imports Main Quotient_Syntax +begin + +section {* Quotient infrastructure for the sum type. *} + +fun + sum_rel +where + "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" +| "sum_rel R1 R2 (Inl a1) (Inr b2) = False" +| "sum_rel R1 R2 (Inr a2) (Inl b1) = False" +| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" + +fun + sum_map +where + "sum_map f1 f2 (Inl a) = Inl (f1 a)" +| "sum_map f1 f2 (Inr a) = Inr (f2 a)" + +declare [[map "+" = (sum_map, sum_rel)]] + + +text {* should probably be in Sum_Type.thy *} +lemma split_sum_all: + shows "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" + apply(auto) + apply(case_tac x) + apply(simp_all) + done + +lemma sum_equivp[quot_equiv]: + assumes a: "equivp R1" + assumes b: "equivp R2" + shows "equivp (sum_rel R1 R2)" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + apply(simp_all add: split_sum_all) + apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b]) + apply(blast intro: equivp_symp[OF a] equivp_symp[OF b]) + apply(blast intro: equivp_transp[OF a] equivp_transp[OF b]) + done + +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)" + unfolding Quotient_def + apply(simp add: split_sum_all) + apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1]) + apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) + using q1 q2 + unfolding Quotient_def + apply(blast)+ + done + +lemma sum_Inl_rsp[quot_respect]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(R1 ===> sum_rel R1 R2) Inl Inl" + by simp + +lemma sum_Inr_rsp[quot_respect]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(R2 ===> sum_rel R1 R2) Inr Inr" + by simp + +lemma sum_Inl_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q1]) + done + +lemma sum_Inr_prs[quot_preserve]: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" + apply(simp add: expand_fun_eq) + apply(simp add: Quotient_abs_rep[OF q2]) + done + +lemma sum_map_id[id_simps]: + shows "sum_map id id = id" + by (simp add: expand_fun_eq split_sum_all) + +lemma sum_rel_eq[id_simps]: + shows "sum_rel (op =) (op =) = (op =)" + by (simp add: expand_fun_eq split_sum_all) + +end diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Library/Quotient_Syntax.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Quotient_Syntax.thy Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,18 @@ +(* Title: Quotient_Syntax.thy + Author: Cezary Kaliszyk and Christian Urban +*) + +header {* Pretty syntax for Quotient operations *} + +(*<*) +theory Quotient_Syntax +imports Main +begin + +notation + rel_conj (infixr "OOO" 75) and + fun_map (infixr "--->" 55) and + fun_rel (infixr "===>" 55) + +end +(*>*) diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Main.thy --- a/src/HOL/Main.thy Fri Feb 19 16:52:00 2010 +0100 +++ b/src/HOL/Main.thy Fri Feb 19 16:52:30 2010 +0100 @@ -1,7 +1,7 @@ header {* Main HOL *} theory Main -imports Plain Predicate_Compile Nitpick +imports Plain Predicate_Compile Nitpick Quotient begin text {* diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Quotient.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient.thy Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,797 @@ +(* Title: Quotient.thy + Author: Cezary Kaliszyk and Christian Urban +*) + +theory Quotient +imports Plain ATP_Linkup +uses + ("~~/src/HOL/Tools/Quotient/quotient_info.ML") + ("~~/src/HOL/Tools/Quotient/quotient_typ.ML") + ("~~/src/HOL/Tools/Quotient/quotient_def.ML") + ("~~/src/HOL/Tools/Quotient/quotient_term.ML") + ("~~/src/HOL/Tools/Quotient/quotient_tacs.ML") +begin + + +text {* + Basic definition for equivalence relations + that are represented by predicates. +*} + +definition + "equivp E \ \x y. E x y = (E x = E y)" + +definition + "reflp E \ \x. E x x" + +definition + "symp E \ \x y. E x y \ E y x" + +definition + "transp E \ \x y z. E x y \ E y z \ E x z" + +lemma equivp_reflp_symp_transp: + shows "equivp E = (reflp E \ symp E \ transp E)" + unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq + by blast + +lemma equivp_reflp: + shows "equivp E \ E x x" + by (simp only: equivp_reflp_symp_transp reflp_def) + +lemma equivp_symp: + shows "equivp E \ E x y \ E y x" + by (metis equivp_reflp_symp_transp symp_def) + +lemma equivp_transp: + shows "equivp E \ E x y \ E y z \ E x z" + by (metis equivp_reflp_symp_transp transp_def) + +lemma equivpI: + assumes "reflp R" "symp R" "transp R" + shows "equivp R" + using assms by (simp add: equivp_reflp_symp_transp) + +lemma identity_equivp: + shows "equivp (op =)" + unfolding equivp_def + by auto + +text {* Partial equivalences: not yet used anywhere *} + +definition + "part_equivp E \ (\x. E x x) \ (\x y. E x y = (E x x \ E y y \ (E x = E y)))" + +lemma equivp_implies_part_equivp: + assumes a: "equivp E" + shows "part_equivp E" + using a + unfolding equivp_def part_equivp_def + by auto + +text {* Composition of Relations *} + +abbreviation + rel_conj (infixr "OOO" 75) +where + "r1 OOO r2 \ r1 OO r2 OO r1" + +lemma eq_comp_r: + shows "((op =) OOO R) = R" + by (auto simp add: expand_fun_eq) + +section {* Respects predicate *} + +definition + Respects +where + "Respects R x \ R x x" + +lemma in_respects: + shows "(x \ Respects R) = R x x" + unfolding mem_def Respects_def + by simp + +section {* Function map and function relation *} + +definition + fun_map (infixr "--->" 55) +where +[simp]: "fun_map f g h x = g (h (f x))" + +definition + fun_rel (infixr "===>" 55) +where +[simp]: "fun_rel E1 E2 f g = (\x y. E1 x y \ E2 (f x) (g y))" + + +lemma fun_map_id: + shows "(id ---> id) = id" + by (simp add: expand_fun_eq id_def) + +lemma fun_rel_eq: + shows "((op =) ===> (op =)) = (op =)" + by (simp add: expand_fun_eq) + +lemma fun_rel_id: + assumes a: "\x y. R1 x y \ R2 (f x) (g y)" + shows "(R1 ===> R2) f g" + using a by simp + +lemma fun_rel_id_asm: + assumes a: "\x y. R1 x y \ (A \ R2 (f x) (g y))" + shows "A \ (R1 ===> R2) f g" + using a by auto + + +section {* Quotient Predicate *} + +definition + "Quotient E Abs Rep \ + (\a. Abs (Rep a) = a) \ (\a. E (Rep a) (Rep a)) \ + (\r s. E r s = (E r r \ E s s \ (Abs r = Abs s)))" + +lemma Quotient_abs_rep: + assumes a: "Quotient E Abs Rep" + shows "Abs (Rep a) = a" + using a + unfolding Quotient_def + by simp + +lemma Quotient_rep_reflp: + assumes a: "Quotient E Abs Rep" + shows "E (Rep a) (Rep a)" + using a + unfolding Quotient_def + by blast + +lemma Quotient_rel: + assumes a: "Quotient E Abs Rep" + shows " E r s = (E r r \ E s s \ (Abs r = Abs s))" + using a + unfolding Quotient_def + by blast + +lemma Quotient_rel_rep: + assumes a: "Quotient R Abs Rep" + 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" + shows "R r r \ R (Rep (Abs r)) r" + using a unfolding Quotient_def + by blast + +lemma Quotient_rel_abs: + assumes a: "Quotient E Abs Rep" + shows "E r s \ Abs r = Abs s" + using a unfolding Quotient_def + by blast + +lemma Quotient_symp: + assumes a: "Quotient E Abs Rep" + shows "symp E" + using a unfolding Quotient_def symp_def + by metis + +lemma Quotient_transp: + assumes a: "Quotient E Abs Rep" + shows "transp E" + using a unfolding Quotient_def transp_def + by metis + +lemma identity_quotient: + shows "Quotient (op =) id id" + unfolding Quotient_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)" +proof - + have "\a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" + using q1 q2 + unfolding Quotient_def + unfolding expand_fun_eq + by simp + moreover + have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" + using q1 q2 + unfolding Quotient_def + by (simp (no_asm)) (metis) + moreover + have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ + (rep1 ---> abs2) r = (rep1 ---> abs2) s)" + unfolding expand_fun_eq + apply(auto) + 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 +qed + +lemma abs_o_rep: + assumes a: "Quotient R Abs Rep" + shows "Abs o Rep = id" + unfolding expand_fun_eq + by (simp add: Quotient_abs_rep[OF a]) + +lemma equals_rsp: + assumes q: "Quotient 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] + unfolding symp_def transp_def + by blast + +lemma lambda_prs: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "(Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) = (\x. f x)" + unfolding expand_fun_eq + using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] + by simp + +lemma lambda_prs1: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "(Rep1 ---> Abs2) (\x. (Abs1 ---> Rep2) f x) = (\x. f x)" + unfolding expand_fun_eq + using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] + by simp + +lemma rep_abs_rsp: + assumes q: "Quotient 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] + by metis + +lemma rep_abs_rsp_left: + assumes q: "Quotient 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] + by metis + +text{* + In the following theorem R1 can be instantiated with anything, + but we know some of the types of the Rep and Abs functions; + so by solving Quotient assumptions we can get a unique R1 that + will be provable; which is why we need to use apply_rsp and + not the primed version *} + +lemma apply_rsp: + fixes f g::"'a \ 'c" + assumes q: "Quotient R1 Abs1 Rep1" + and a: "(R1 ===> R2) f g" "R1 x y" + shows "R2 (f x) (g y)" + using a by simp + +lemma apply_rsp': + assumes a: "(R1 ===> R2) f g" "R1 x y" + shows "R2 (f x) (g y)" + using a by simp + +section {* lemmas for regularisation of ball and bex *} + +lemma ball_reg_eqv: + fixes P :: "'a \ bool" + assumes a: "equivp R" + shows "Ball (Respects R) P = (All P)" + using a + unfolding equivp_def + by (auto simp add: in_respects) + +lemma bex_reg_eqv: + fixes P :: "'a \ bool" + assumes a: "equivp R" + shows "Bex (Respects R) P = (Ex P)" + using a + unfolding equivp_def + by (auto simp add: in_respects) + +lemma ball_reg_right: + assumes a: "\x. R x \ P x \ Q x" + shows "All P \ Ball R Q" + using a by (metis COMBC_def Collect_def Collect_mem_eq) + +lemma bex_reg_left: + assumes a: "\x. R x \ Q x \ P x" + shows "Bex R Q \ Ex P" + using a by (metis COMBC_def Collect_def Collect_mem_eq) + +lemma ball_reg_left: + assumes a: "equivp R" + shows "(\x. (Q x \ P x)) \ Ball (Respects R) Q \ All P" + using a by (metis equivp_reflp in_respects) + +lemma bex_reg_right: + assumes a: "equivp R" + shows "(\x. (Q x \ P x)) \ Ex Q \ Bex (Respects R) P" + using a by (metis equivp_reflp in_respects) + +lemma ball_reg_eqv_range: + fixes P::"'a \ bool" + and x::"'a" + assumes a: "equivp R2" + shows "(Ball (Respects (R1 ===> R2)) (\f. P (f x)) = All (\f. P (f x)))" + apply(rule iffI) + apply(rule allI) + apply(drule_tac x="\y. f x" in bspec) + apply(simp add: in_respects) + apply(rule impI) + using a equivp_reflp_symp_transp[of "R2"] + apply(simp add: reflp_def) + apply(simp) + apply(simp) + done + +lemma bex_reg_eqv_range: + assumes a: "equivp R2" + shows "(Bex (Respects (R1 ===> R2)) (\f. P (f x)) = Ex (\f. P (f x)))" + apply(auto) + apply(rule_tac x="\y. f x" in bexI) + apply(simp) + apply(simp add: Respects_def in_respects) + apply(rule impI) + using a equivp_reflp_symp_transp[of "R2"] + apply(simp add: reflp_def) + done + +(* Next four lemmas are unused *) +lemma all_reg: + assumes a: "!x :: 'a. (P x --> Q x)" + and b: "All P" + shows "All Q" + using a b by (metis) + +lemma ex_reg: + assumes a: "!x :: 'a. (P x --> Q x)" + and b: "Ex P" + shows "Ex Q" + using a b by metis + +lemma ball_reg: + assumes a: "!x :: 'a. (R x --> P x --> Q x)" + and b: "Ball R P" + shows "Ball R Q" + using a b by (metis COMBC_def Collect_def Collect_mem_eq) + +lemma bex_reg: + assumes a: "!x :: 'a. (R x --> P x --> Q x)" + and b: "Bex R P" + shows "Bex R Q" + using a b by (metis COMBC_def Collect_def Collect_mem_eq) + + +lemma ball_all_comm: + assumes "\y. (\x\P. A x y) \ (\x. B x y)" + shows "(\x\P. \y. A x y) \ (\x. \y. B x y)" + using assms by auto + +lemma bex_ex_comm: + assumes "(\y. \x. A x y) \ (\y. \x\P. B x y)" + shows "(\x. \y. A x y) \ (\x\P. \y. B x y)" + using assms by auto + +section {* Bounded abstraction *} + +definition + Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" +where + "x \ p \ Babs p m x = m x" + +lemma babs_rsp: + assumes q: "Quotient 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) + apply (subgoal_tac "x \ Respects R1 \ y \ Respects R1") + using a apply (simp add: Babs_def) + apply (simp add: in_respects) + using Quotient_rel[OF q] + by metis + +lemma babs_prs: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" + apply (rule ext) + apply (simp) + 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]) + done + +lemma babs_simp: + assumes q: "Quotient 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]) + apply(auto simp add: Babs_def) + apply (subgoal_tac "x \ Respects R1 \ y \ Respects R1") + apply(metis Babs_def) + apply (simp add: in_respects) + using Quotient_rel[OF q] + by metis + +(* If a user proves that a particular functional relation + is an equivalence this may be useful in regularising *) +lemma babs_reg_eqv: + shows "equivp R \ Babs (Respects R) P = P" + by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) + + +(* 3 lemmas needed for proving repabs_inj *) +lemma ball_rsp: + assumes a: "(R ===> (op =)) f g" + shows "Ball (Respects R) f = Ball (Respects R) g" + using a by (simp add: Ball_def in_respects) + +lemma bex_rsp: + assumes a: "(R ===> (op =)) f g" + shows "(Bex (Respects R) f = Bex (Respects R) g)" + using a by (simp add: Bex_def in_respects) + +lemma bex1_rsp: + assumes a: "(R ===> (op =)) f g" + shows "Ex1 (\x. x \ Respects R \ f x) = Ex1 (\x. x \ Respects R \ g x)" + using a + by (simp add: Ex1_def in_respects) auto + +(* 2 lemmas needed for cleaning of quantifiers *) +lemma all_prs: + assumes a: "Quotient R absf repf" + shows "Ball (Respects R) ((absf ---> id) f) = All f" + using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply + by metis + +lemma ex_prs: + assumes a: "Quotient R absf repf" + shows "Bex (Respects R) ((absf ---> id) f) = Ex f" + using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply + by metis + +section {* Bex1_rel quantifier *} + +definition + Bex1_rel :: "('a \ 'a \ bool) \ ('a \ bool) \ bool" +where + "Bex1_rel R P \ (\x \ Respects R. P x) \ (\x \ Respects R. \y \ Respects R. ((P x \ P y) \ (R x y)))" + +lemma bex1_rel_aux: + "\\xa ya. R xa ya \ x xa = y ya; Bex1_rel R x\ \ Bex1_rel R y" + unfolding Bex1_rel_def + apply (erule conjE)+ + apply (erule bexE) + apply rule + apply (rule_tac x="xa" in bexI) + apply metis + apply metis + apply rule+ + apply (erule_tac x="xaa" in ballE) + prefer 2 + apply (metis) + apply (erule_tac x="ya" in ballE) + prefer 2 + apply (metis) + apply (metis in_respects) + done + +lemma bex1_rel_aux2: + "\\xa ya. R xa ya \ x xa = y ya; Bex1_rel R y\ \ Bex1_rel R x" + unfolding Bex1_rel_def + apply (erule conjE)+ + apply (erule bexE) + apply rule + apply (rule_tac x="xa" in bexI) + apply metis + apply metis + apply rule+ + apply (erule_tac x="xaa" in ballE) + prefer 2 + apply (metis) + apply (erule_tac x="ya" in ballE) + prefer 2 + apply (metis) + apply (metis in_respects) + done + +lemma bex1_rel_rsp: + assumes a: "Quotient R absf repf" + shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)" + apply simp + apply clarify + apply rule + apply (simp_all add: bex1_rel_aux bex1_rel_aux2) + apply (erule bex1_rel_aux2) + apply assumption + done + + +lemma ex1_prs: + assumes a: "Quotient R absf repf" + shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" +apply simp +apply (subst Bex1_rel_def) +apply (subst Bex_def) +apply (subst Ex1_def) +apply simp +apply rule + apply (erule conjE)+ + apply (erule_tac exE) + apply (erule conjE) + apply (subgoal_tac "\y. R y y \ f (absf y) \ R x y") + apply (rule_tac x="absf x" in exI) + apply (simp) + apply rule+ + using a unfolding Quotient_def + apply metis + apply rule+ + apply (erule_tac x="x" in ballE) + apply (erule_tac x="y" in ballE) + apply simp + apply (simp add: in_respects) + apply (simp add: in_respects) +apply (erule_tac exE) + apply rule + 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 rule+ +using a unfolding Quotient_def in_respects +apply metis +done + +lemma bex1_bexeq_reg: "(\!x\Respects R. P x) \ (Bex1_rel R (\x. P x))" + apply (simp add: Ex1_def Bex1_rel_def in_respects) + apply clarify + apply auto + apply (rule bexI) + apply assumption + apply (simp add: in_respects) + apply (simp add: in_respects) + apply auto + done + +section {* Various respects and preserve lemmas *} + +lemma quot_rel_rsp: + assumes a: "Quotient R Abs Rep" + shows "(R ===> R ===> op =) R R" + apply(rule fun_rel_id)+ + apply(rule equals_rsp[OF a]) + apply(assumption)+ + done + +lemma o_prs: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + and q3: "Quotient R3 Abs3 Rep3" + shows "(Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g)) = f o g" + using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3] + unfolding o_def expand_fun_eq by simp + +lemma o_rsp: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + and q3: "Quotient R3 Abs3 Rep3" + and a1: "(R2 ===> R3) f1 f2" + and a2: "(R1 ===> R2) g1 g2" + shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" + using a1 a2 unfolding o_def expand_fun_eq + by (auto) + +lemma cond_prs: + assumes a: "Quotient 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 + +lemma if_prs: + assumes q: "Quotient R Abs Rep" + shows "Abs (If a (Rep b) (Rep c)) = If a b c" + using Quotient_abs_rep[OF q] by auto + +(* q not used *) +lemma if_rsp: + assumes q: "Quotient R Abs Rep" + and a: "a1 = a2" "R b1 b2" "R c1 c2" + shows "R (If a1 b1 c1) (If a2 b2 c2)" + using a by auto + +lemma let_prs: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f" + using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto + +lemma let_rsp: + assumes q1: "Quotient R1 Abs1 Rep1" + and a1: "(R1 ===> R2) f g" + and a2: "R1 x y" + shows "R2 ((Let x f)::'c) ((Let y g)::'c)" + using apply_rsp[OF q1 a1] a2 by auto + +locale quot_type = + fixes R :: "'a \ 'a \ bool" + and Abs :: "('a \ bool) \ 'b" + and Rep :: "'b \ ('a \ bool)" + assumes equivp: "equivp R" + and rep_prop: "\y. \x. Rep y = R x" + and rep_inverse: "\x. Abs (Rep x) = x" + and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" + and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" +begin + +definition + abs::"'a \ 'b" +where + "abs x \ Abs (R x)" + +definition + rep::"'b \ 'a" +where + "rep a = Eps (Rep a)" + +lemma homeier_lem9: + shows "R (Eps (R x)) = R x" +proof - + have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def) + then have "R x (Eps (R x))" by (rule someI) + then show "R (Eps (R x)) = R x" + using equivp unfolding equivp_def by simp +qed + +theorem homeier_thm10: + shows "abs (rep a) = a" + unfolding abs_def rep_def +proof - + from rep_prop + obtain x where eq: "Rep a = R x" by auto + have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp + also have "\ = Abs (R x)" using homeier_lem9 by simp + also have "\ = Abs (Rep a)" using eq by simp + also have "\ = a" using rep_inverse by simp + finally + show "Abs (R (Eps (Rep a))) = a" by simp +qed + +lemma homeier_lem7: + shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS") +proof - + have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject) + also have "\ = ?LHS" by (simp add: abs_inverse) + finally show "?LHS = ?RHS" by simp +qed + +theorem homeier_thm11: + shows "R r r' = (abs r = abs r')" + unfolding abs_def + by (simp only: equivp[simplified equivp_def] homeier_lem7) + +lemma rep_refl: + shows "R (rep a) (rep a)" + unfolding rep_def + by (simp add: equivp[simplified equivp_def]) + + +lemma rep_abs_rsp: + shows "R f (rep (abs g)) = R f g" + and "R (rep (abs g)) f = R g f" + by (simp_all add: homeier_thm10 homeier_thm11) + +lemma Quotient: + shows "Quotient R abs rep" + unfolding Quotient_def + apply(simp add: homeier_thm10) + apply(simp add: rep_refl) + apply(subst homeier_thm11[symmetric]) + apply(simp add: equivp[simplified equivp_def]) + done + +end + +section {* ML setup *} + +text {* Auxiliary data for the quotient package *} + +use "~~/src/HOL/Tools/Quotient/quotient_info.ML" + +declare [[map "fun" = (fun_map, fun_rel)]] + +lemmas [quot_thm] = fun_quotient +lemmas [quot_respect] = quot_rel_rsp +lemmas [quot_equiv] = identity_equivp + + +text {* Lemmas about simplifying id's. *} +lemmas [id_simps] = + id_def[symmetric] + fun_map_id + id_apply + id_o + o_id + eq_comp_r + +text {* Translation functions for the lifting process. *} +use "~~/src/HOL/Tools/Quotient/quotient_term.ML" + + +text {* Definitions of the quotient types. *} +use "~~/src/HOL/Tools/Quotient/quotient_typ.ML" + + +text {* Definitions for quotient constants. *} +use "~~/src/HOL/Tools/Quotient/quotient_def.ML" + + +text {* + An auxiliary constant for recording some information + about the lifted theorem in a tactic. +*} +definition + "Quot_True x \ True" + +lemma + shows QT_all: "Quot_True (All P) \ Quot_True P" + and QT_ex: "Quot_True (Ex P) \ Quot_True P" + and QT_ex1: "Quot_True (Ex1 P) \ Quot_True P" + and QT_lam: "Quot_True (\x. P x) \ (\x. Quot_True (P x))" + and QT_ext: "(\x. Quot_True (a x) \ f x = g x) \ (Quot_True a \ f = g)" + by (simp_all add: Quot_True_def ext) + +lemma QT_imp: "Quot_True a \ Quot_True b" + by (simp add: Quot_True_def) + + +text {* Tactics for proving the lifted theorems *} +use "~~/src/HOL/Tools/Quotient/quotient_tacs.ML" + +section {* Methods / Interface *} + +method_setup lifting = + {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *} + {* lifts theorems to quotient types *} + +method_setup lifting_setup = + {* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *} + {* sets up the three goals for the quotient lifting procedure *} + +method_setup regularize = + {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *} + {* proves the regularization goals from the quotient lifting procedure *} + +method_setup injection = + {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *} + {* proves the rep/abs injection goals from the quotient lifting procedure *} + +method_setup cleaning = + {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *} + {* proves the cleaning goals from the quotient lifting procedure *} + +attribute_setup quot_lifted = + {* Scan.succeed Quotient_Tacs.lifted_attrib *} + {* lifts theorems to quotient types *} + +no_notation + rel_conj (infixr "OOO" 75) and + fun_map (infixr "--->" 55) and + fun_rel (infixr "===>" 55) + +end + diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Quotient_Examples/LarryDatatype.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient_Examples/LarryDatatype.thy Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,394 @@ +theory LarryDatatype +imports Main Quotient_Syntax +begin + +subsection{*Defining the Free Algebra*} + +datatype + freemsg = NONCE nat + | MPAIR freemsg freemsg + | CRYPT nat freemsg + | DECRYPT nat freemsg + +inductive + msgrel::"freemsg \ freemsg \ bool" (infixl "\" 50) +where + CD: "CRYPT K (DECRYPT K X) \ X" +| DC: "DECRYPT K (CRYPT K X) \ X" +| NONCE: "NONCE N \ NONCE N" +| MPAIR: "\X \ X'; Y \ Y'\ \ MPAIR X Y \ MPAIR X' Y'" +| CRYPT: "X \ X' \ CRYPT K X \ CRYPT K X'" +| DECRYPT: "X \ X' \ DECRYPT K X \ DECRYPT K X'" +| SYM: "X \ Y \ Y \ X" +| TRANS: "\X \ Y; Y \ Z\ \ X \ Z" + +lemmas msgrel.intros[intro] + +text{*Proving that it is an equivalence relation*} + +lemma msgrel_refl: "X \ X" +by (induct X, (blast intro: msgrel.intros)+) + +theorem equiv_msgrel: "equivp msgrel" +proof (rule equivpI) + show "reflp msgrel" by (simp add: reflp_def msgrel_refl) + show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM) + show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS) +qed + +subsection{*Some Functions on the Free Algebra*} + +subsubsection{*The Set of Nonces*} + +fun + freenonces :: "freemsg \ nat set" +where + "freenonces (NONCE N) = {N}" +| "freenonces (MPAIR X Y) = freenonces X \ freenonces Y" +| "freenonces (CRYPT K X) = freenonces X" +| "freenonces (DECRYPT K X) = freenonces X" + +theorem msgrel_imp_eq_freenonces: + assumes a: "U \ V" + shows "freenonces U = freenonces V" + using a by (induct) (auto) + +subsubsection{*The Left Projection*} + +text{*A function to return the left part of the top pair in a message. It will +be lifted to the initial algrebra, to serve as an example of that process.*} +fun + freeleft :: "freemsg \ freemsg" +where + "freeleft (NONCE N) = NONCE N" +| "freeleft (MPAIR X Y) = X" +| "freeleft (CRYPT K X) = freeleft X" +| "freeleft (DECRYPT K X) = freeleft X" + +text{*This theorem lets us prove that the left function respects the +equivalence relation. It also helps us prove that MPair + (the abstract constructor) is injective*} +lemma msgrel_imp_eqv_freeleft_aux: + shows "freeleft U \ freeleft U" + by (induct rule: freeleft.induct) (auto) + +theorem msgrel_imp_eqv_freeleft: + assumes a: "U \ V" + shows "freeleft U \ freeleft V" + using a + by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux) + +subsubsection{*The Right Projection*} + +text{*A function to return the right part of the top pair in a message.*} +fun + freeright :: "freemsg \ freemsg" +where + "freeright (NONCE N) = NONCE N" +| "freeright (MPAIR X Y) = Y" +| "freeright (CRYPT K X) = freeright X" +| "freeright (DECRYPT K X) = freeright X" + +text{*This theorem lets us prove that the right function respects the +equivalence relation. It also helps us prove that MPair + (the abstract constructor) is injective*} +lemma msgrel_imp_eqv_freeright_aux: + shows "freeright U \ freeright U" + by (induct rule: freeright.induct) (auto) + +theorem msgrel_imp_eqv_freeright: + assumes a: "U \ V" + shows "freeright U \ freeright V" + using a + by (induct) (auto intro: msgrel_imp_eqv_freeright_aux) + +subsubsection{*The Discriminator for Constructors*} + +text{*A function to distinguish nonces, mpairs and encryptions*} +fun + freediscrim :: "freemsg \ int" +where + "freediscrim (NONCE N) = 0" + | "freediscrim (MPAIR X Y) = 1" + | "freediscrim (CRYPT K X) = freediscrim X + 2" + | "freediscrim (DECRYPT K X) = freediscrim X - 2" + +text{*This theorem helps us prove @{term "Nonce N \ MPair X Y"}*} +theorem msgrel_imp_eq_freediscrim: + assumes a: "U \ V" + shows "freediscrim U = freediscrim V" + using a by (induct) (auto) + +subsection{*The Initial Algebra: A Quotiented Message Type*} + +quotient_type msg = freemsg / msgrel + by (rule equiv_msgrel) + +text{*The abstract message constructors*} + +quotient_definition + "Nonce :: nat \ msg" +is + "NONCE" + +quotient_definition + "MPair :: msg \ msg \ msg" +is + "MPAIR" + +quotient_definition + "Crypt :: nat \ msg \ msg" +is + "CRYPT" + +quotient_definition + "Decrypt :: nat \ msg \ msg" +is + "DECRYPT" + +lemma [quot_respect]: + shows "(op = ===> op \ ===> op \) CRYPT CRYPT" +by (auto intro: CRYPT) + +lemma [quot_respect]: + shows "(op = ===> op \ ===> op \) DECRYPT DECRYPT" +by (auto intro: DECRYPT) + +text{*Establishing these two equations is the point of the whole exercise*} +theorem CD_eq [simp]: + shows "Crypt K (Decrypt K X) = X" + by (lifting CD) + +theorem DC_eq [simp]: + shows "Decrypt K (Crypt K X) = X" + by (lifting DC) + +subsection{*The Abstract Function to Return the Set of Nonces*} + +quotient_definition + "nonces:: msg \ nat set" +is + "freenonces" + +text{*Now prove the four equations for @{term nonces}*} + +lemma [quot_respect]: + shows "(op \ ===> op =) freenonces freenonces" + by (simp add: msgrel_imp_eq_freenonces) + +lemma [quot_respect]: + shows "(op = ===> op \) NONCE NONCE" + by (simp add: NONCE) + +lemma nonces_Nonce [simp]: + shows "nonces (Nonce N) = {N}" + by (lifting freenonces.simps(1)) + +lemma [quot_respect]: + shows " (op \ ===> op \ ===> op \) MPAIR MPAIR" + by (simp add: MPAIR) + +lemma nonces_MPair [simp]: + shows "nonces (MPair X Y) = nonces X \ nonces Y" + by (lifting freenonces.simps(2)) + +lemma nonces_Crypt [simp]: + shows "nonces (Crypt K X) = nonces X" + by (lifting freenonces.simps(3)) + +lemma nonces_Decrypt [simp]: + shows "nonces (Decrypt K X) = nonces X" + by (lifting freenonces.simps(4)) + +subsection{*The Abstract Function to Return the Left Part*} + +quotient_definition + "left:: msg \ msg" +is + "freeleft" + +lemma [quot_respect]: + shows "(op \ ===> op \) freeleft freeleft" + by (simp add: msgrel_imp_eqv_freeleft) + +lemma left_Nonce [simp]: + shows "left (Nonce N) = Nonce N" + by (lifting freeleft.simps(1)) + +lemma left_MPair [simp]: + shows "left (MPair X Y) = X" + by (lifting freeleft.simps(2)) + +lemma left_Crypt [simp]: + shows "left (Crypt K X) = left X" + by (lifting freeleft.simps(3)) + +lemma left_Decrypt [simp]: + shows "left (Decrypt K X) = left X" + by (lifting freeleft.simps(4)) + +subsection{*The Abstract Function to Return the Right Part*} + +quotient_definition + "right:: msg \ msg" +is + "freeright" + +text{*Now prove the four equations for @{term right}*} + +lemma [quot_respect]: + shows "(op \ ===> op \) freeright freeright" + by (simp add: msgrel_imp_eqv_freeright) + +lemma right_Nonce [simp]: + shows "right (Nonce N) = Nonce N" + by (lifting freeright.simps(1)) + +lemma right_MPair [simp]: + shows "right (MPair X Y) = Y" + by (lifting freeright.simps(2)) + +lemma right_Crypt [simp]: + shows "right (Crypt K X) = right X" + by (lifting freeright.simps(3)) + +lemma right_Decrypt [simp]: + shows "right (Decrypt K X) = right X" + by (lifting freeright.simps(4)) + +subsection{*Injectivity Properties of Some Constructors*} + +lemma NONCE_imp_eq: + shows "NONCE m \ NONCE n \ m = n" + by (drule msgrel_imp_eq_freenonces, simp) + +text{*Can also be proved using the function @{term nonces}*} +lemma Nonce_Nonce_eq [iff]: + shows "(Nonce m = Nonce n) = (m = n)" +proof + assume "Nonce m = Nonce n" + then show "m = n" by (lifting NONCE_imp_eq) +next + assume "m = n" + then show "Nonce m = Nonce n" by simp +qed + +lemma MPAIR_imp_eqv_left: + shows "MPAIR X Y \ MPAIR X' Y' \ X \ X'" + by (drule msgrel_imp_eqv_freeleft) (simp) + +lemma MPair_imp_eq_left: + assumes eq: "MPair X Y = MPair X' Y'" + shows "X = X'" + using eq by (lifting MPAIR_imp_eqv_left) + +lemma MPAIR_imp_eqv_right: + shows "MPAIR X Y \ MPAIR X' Y' \ Y \ Y'" + by (drule msgrel_imp_eqv_freeright) (simp) + +lemma MPair_imp_eq_right: + shows "MPair X Y = MPair X' Y' \ Y = Y'" + by (lifting MPAIR_imp_eqv_right) + +theorem MPair_MPair_eq [iff]: + shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" + by (blast dest: MPair_imp_eq_left MPair_imp_eq_right) + +lemma NONCE_neqv_MPAIR: + shows "\(NONCE m \ MPAIR X Y)" + by (auto dest: msgrel_imp_eq_freediscrim) + +theorem Nonce_neq_MPair [iff]: + shows "Nonce N \ MPair X Y" + by (lifting NONCE_neqv_MPAIR) + +text{*Example suggested by a referee*} + +lemma CRYPT_NONCE_neq_NONCE: + shows "\(CRYPT K (NONCE M) \ NONCE N)" + by (auto dest: msgrel_imp_eq_freediscrim) + +theorem Crypt_Nonce_neq_Nonce: + shows "Crypt K (Nonce M) \ Nonce N" + by (lifting CRYPT_NONCE_neq_NONCE) + +text{*...and many similar results*} +lemma CRYPT2_NONCE_neq_NONCE: + shows "\(CRYPT K (CRYPT K' (NONCE M)) \ NONCE N)" + by (auto dest: msgrel_imp_eq_freediscrim) + +theorem Crypt2_Nonce_neq_Nonce: + shows "Crypt K (Crypt K' (Nonce M)) \ Nonce N" + by (lifting CRYPT2_NONCE_neq_NONCE) + +theorem Crypt_Crypt_eq [iff]: + shows "(Crypt K X = Crypt K X') = (X=X')" +proof + assume "Crypt K X = Crypt K X'" + hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp + thus "X = X'" by simp +next + assume "X = X'" + thus "Crypt K X = Crypt K X'" by simp +qed + +theorem Decrypt_Decrypt_eq [iff]: + shows "(Decrypt K X = Decrypt K X') = (X=X')" +proof + assume "Decrypt K X = Decrypt K X'" + hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp + thus "X = X'" by simp +next + assume "X = X'" + thus "Decrypt K X = Decrypt K X'" by simp +qed + +lemma msg_induct_aux: + shows "\\N. P (Nonce N); + \X Y. \P X; P Y\ \ P (MPair X Y); + \K X. P X \ P (Crypt K X); + \K X. P X \ P (Decrypt K X)\ \ P msg" + by (lifting freemsg.induct) + +lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]: + assumes N: "\N. P (Nonce N)" + and M: "\X Y. \P X; P Y\ \ P (MPair X Y)" + and C: "\K X. P X \ P (Crypt K X)" + and D: "\K X. P X \ P (Decrypt K X)" + shows "P msg" + using N M C D by (rule msg_induct_aux) + +subsection{*The Abstract Discriminator*} + +text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't +need this function in order to prove discrimination theorems.*} + +quotient_definition + "discrim:: msg \ int" +is + "freediscrim" + +text{*Now prove the four equations for @{term discrim}*} + +lemma [quot_respect]: + shows "(op \ ===> op =) freediscrim freediscrim" + by (auto simp add: msgrel_imp_eq_freediscrim) + +lemma discrim_Nonce [simp]: + shows "discrim (Nonce N) = 0" + by (lifting freediscrim.simps(1)) + +lemma discrim_MPair [simp]: + shows "discrim (MPair X Y) = 1" + by (lifting freediscrim.simps(2)) + +lemma discrim_Crypt [simp]: + shows "discrim (Crypt K X) = discrim X + 2" + by (lifting freediscrim.simps(3)) + +lemma discrim_Decrypt [simp]: + shows "discrim (Decrypt K X) = discrim X - 2" + by (lifting freediscrim.simps(4)) + +end + diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Quotient_Examples/LarryInt.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient_Examples/LarryInt.thy Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,395 @@ + +header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} + +theory LarryInt +imports Main Quotient_Product +begin + +fun + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" +where + "intrel (x, y) (u, v) = (x + v = u + y)" + +quotient_type int = "nat \ nat" / intrel + by (auto simp add: equivp_def expand_fun_eq) + +instantiation int :: "{zero, one, plus, uminus, minus, times, ord}" +begin + +quotient_definition + Zero_int_def: "0::int" is "(0::nat, 0::nat)" + +quotient_definition + One_int_def: "1::int" is "(1::nat, 0::nat)" + +definition + "add_raw \ \(x, y) (u, v). (x + (u::nat), y + (v::nat))" + +quotient_definition + "(op +) :: int \ int \ int" +is + "add_raw" + +definition + "uminus_raw \ \(x::nat, y::nat). (y, x)" + +quotient_definition + "uminus :: int \ int" +is + "uminus_raw" + +fun + mult_raw::"nat \ nat \ nat \ nat \ nat \ nat" +where + "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" + +quotient_definition + "(op *) :: int \ int \ int" +is + "mult_raw" + +definition + "le_raw \ \(x, y) (u, v). (x+v \ u+(y::nat))" + +quotient_definition + le_int_def: "(op \) :: int \ int \ bool" +is + "le_raw" + +definition + less_int_def: "z < (w::int) \ (z \ w & z \ w)" + +definition + diff_int_def: "z - (w::int) \ z + (-w)" + +instance .. + +end + +subsection{*Construction of the Integers*} + +lemma zminus_zminus_raw: + "uminus_raw (uminus_raw z) = z" + by (cases z) (simp add: uminus_raw_def) + +lemma [quot_respect]: + shows "(intrel ===> intrel) uminus_raw uminus_raw" + by (simp add: uminus_raw_def) + +lemma zminus_zminus: + fixes z::"int" + shows "- (- z) = z" + by(lifting zminus_zminus_raw) + +lemma zminus_0_raw: + shows "uminus_raw (0, 0) = (0, 0::nat)" + by (simp add: uminus_raw_def) + +lemma zminus_0: + shows "- 0 = (0::int)" + by (lifting zminus_0_raw) + +subsection{*Integer Addition*} + +lemma zminus_zadd_distrib_raw: + shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)" +by (cases z, cases w) + (auto simp add: add_raw_def uminus_raw_def) + +lemma [quot_respect]: + shows "(intrel ===> intrel ===> intrel) add_raw add_raw" +by (simp add: add_raw_def) + +lemma zminus_zadd_distrib: + fixes z w::"int" + shows "- (z + w) = (- z) + (- w)" + by(lifting zminus_zadd_distrib_raw) + +lemma zadd_commute_raw: + shows "add_raw z w = add_raw w z" +by (cases z, cases w) + (simp add: add_raw_def) + +lemma zadd_commute: + fixes z w::"int" + shows "(z::int) + w = w + z" + by (lifting zadd_commute_raw) + +lemma zadd_assoc_raw: + shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)" + by (cases z1, cases z2, cases z3) (simp add: add_raw_def) + +lemma zadd_assoc: + fixes z1 z2 z3::"int" + shows "(z1 + z2) + z3 = z1 + (z2 + z3)" + by (lifting zadd_assoc_raw) + +lemma zadd_0_raw: + shows "add_raw (0, 0) z = z" + by (simp add: add_raw_def) + + +text {*also for the instance declaration int :: plus_ac0*} +lemma zadd_0: + fixes z::"int" + shows "0 + z = z" + by (lifting zadd_0_raw) + +lemma zadd_zminus_inverse_raw: + shows "intrel (add_raw (uminus_raw z) z) (0, 0)" + by (cases z) (simp add: add_raw_def uminus_raw_def) + +lemma zadd_zminus_inverse2: + fixes z::"int" + shows "(- z) + z = 0" + by (lifting zadd_zminus_inverse_raw) + +subsection{*Integer Multiplication*} + +lemma zmult_zminus_raw: + shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)" +apply(cases z, cases w) +apply(simp add: uminus_raw_def) +done + +lemma mult_raw_fst: + assumes a: "intrel x z" + shows "intrel (mult_raw x y) (mult_raw z y)" +using a +apply(cases x, cases y, cases z) +apply(auto simp add: mult_raw.simps intrel.simps) +apply(rename_tac u v w x y z) +apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") +apply(simp add: mult_ac) +apply(simp add: add_mult_distrib [symmetric]) +done + +lemma mult_raw_snd: + assumes a: "intrel x z" + shows "intrel (mult_raw y x) (mult_raw y z)" +using a +apply(cases x, cases y, cases z) +apply(auto simp add: mult_raw.simps intrel.simps) +apply(rename_tac u v w x y z) +apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") +apply(simp add: mult_ac) +apply(simp add: add_mult_distrib [symmetric]) +done + +lemma [quot_respect]: + shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw" +apply(simp only: fun_rel_def) +apply(rule allI | rule impI)+ +apply(rule equivp_transp[OF int_equivp]) +apply(rule mult_raw_fst) +apply(assumption) +apply(rule mult_raw_snd) +apply(assumption) +done + +lemma zmult_zminus: + fixes z w::"int" + shows "(- z) * w = - (z * w)" + by (lifting zmult_zminus_raw) + +lemma zmult_commute_raw: + shows "mult_raw z w = mult_raw w z" +apply(cases z, cases w) +apply(simp add: add_ac mult_ac) +done + +lemma zmult_commute: + fixes z w::"int" + shows "z * w = w * z" + by (lifting zmult_commute_raw) + +lemma zmult_assoc_raw: + shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)" +apply(cases z1, cases z2, cases z3) +apply(simp add: add_mult_distrib2 mult_ac) +done + +lemma zmult_assoc: + fixes z1 z2 z3::"int" + shows "(z1 * z2) * z3 = z1 * (z2 * z3)" + by (lifting zmult_assoc_raw) + +lemma zadd_mult_distrib_raw: + shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)" +apply(cases z1, cases z2, cases w) +apply(simp add: add_mult_distrib2 mult_ac add_raw_def) +done + +lemma zadd_zmult_distrib: + fixes z1 z2 w::"int" + shows "(z1 + z2) * w = (z1 * w) + (z2 * w)" + by(lifting zadd_mult_distrib_raw) + +lemma zadd_zmult_distrib2: + fixes w z1 z2::"int" + shows "w * (z1 + z2) = (w * z1) + (w * z2)" + by (simp add: zmult_commute [of w] zadd_zmult_distrib) + +lemma zdiff_zmult_distrib: + fixes w z1 z2::"int" + shows "(z1 - z2) * w = (z1 * w) - (z2 * w)" + by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus) + +lemma zdiff_zmult_distrib2: + fixes w z1 z2::"int" + shows "w * (z1 - z2) = (w * z1) - (w * z2)" + by (simp add: zmult_commute [of w] zdiff_zmult_distrib) + +lemmas int_distrib = + zadd_zmult_distrib zadd_zmult_distrib2 + zdiff_zmult_distrib zdiff_zmult_distrib2 + +lemma zmult_1_raw: + shows "mult_raw (1, 0) z = z" + by (cases z) (auto) + +lemma zmult_1: + fixes z::"int" + shows "1 * z = z" + by (lifting zmult_1_raw) + +lemma zmult_1_right: + fixes z::"int" + shows "z * 1 = z" + by (rule trans [OF zmult_commute zmult_1]) + +lemma zero_not_one: + shows "\(intrel (0, 0) (1::nat, 0::nat))" + by auto + +text{*The Integers Form A Ring*} +instance int :: comm_ring_1 +proof + fix i j k :: int + show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc) + show "i + j = j + i" by (simp add: zadd_commute) + show "0 + i = i" by (rule zadd_0) + show "- i + i = 0" by (rule zadd_zminus_inverse2) + show "i - j = i + (-j)" by (simp add: diff_int_def) + show "(i * j) * k = i * (j * k)" by (rule zmult_assoc) + show "i * j = j * i" by (rule zmult_commute) + show "1 * i = i" by (rule zmult_1) + show "(i + j) * k = i * k + j * k" by (simp add: int_distrib) + show "0 \ (1::int)" by (lifting zero_not_one) +qed + + +subsection{*The @{text "\"} Ordering*} + +lemma zle_refl_raw: + shows "le_raw w w" + by (cases w) (simp add: le_raw_def) + +lemma [quot_respect]: + shows "(intrel ===> intrel ===> op =) le_raw le_raw" + by (auto) (simp_all add: le_raw_def) + +lemma zle_refl: + fixes w::"int" + shows "w \ w" + by (lifting zle_refl_raw) + + +lemma zle_trans_raw: + shows "\le_raw i j; le_raw j k\ \ le_raw i k" +apply(cases i, cases j, cases k) +apply(auto simp add: le_raw_def) +done + +lemma zle_trans: + fixes i j k::"int" + shows "\i \ j; j \ k\ \ i \ k" + by (lifting zle_trans_raw) + +lemma zle_anti_sym_raw: + shows "\le_raw z w; le_raw w z\ \ intrel z w" +apply(cases z, cases w) +apply(auto iff: le_raw_def) +done + +lemma zle_anti_sym: + fixes z w::"int" + shows "\z \ w; w \ z\ \ z = w" + by (lifting zle_anti_sym_raw) + + +(* Axiom 'order_less_le' of class 'order': *) +lemma zless_le: + fixes w z::"int" + shows "(w < z) = (w \ z & w \ z)" + by (simp add: less_int_def) + +instance int :: order +apply (default) +apply(auto simp add: zless_le zle_anti_sym)[1] +apply(rule zle_refl) +apply(erule zle_trans, assumption) +apply(erule zle_anti_sym, assumption) +done + +(* Axiom 'linorder_linear' of class 'linorder': *) + +lemma zle_linear_raw: + shows "le_raw z w \ le_raw w z" +apply(cases w, cases z) +apply(auto iff: le_raw_def) +done + +lemma zle_linear: + fixes z w::"int" + shows "z \ w \ w \ z" + by (lifting zle_linear_raw) + +instance int :: linorder +apply(default) +apply(rule zle_linear) +done + +lemma zadd_left_mono_raw: + shows "le_raw i j \ le_raw (add_raw k i) (add_raw k j)" +apply(cases k) +apply(auto simp add: add_raw_def le_raw_def) +done + +lemma zadd_left_mono: + fixes i j::"int" + shows "i \ j \ k + i \ k + j" + by (lifting zadd_left_mono_raw) + + +subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*} + +definition + "nat_raw \ \(x, y).x - (y::nat)" + +quotient_definition + "nat2::int \ nat" +is + "nat_raw" + +abbreviation + "less_raw x y \ (le_raw x y \ \(intrel x y))" + +lemma nat_le_eq_zle_raw: + shows "less_raw (0, 0) w \ le_raw (0, 0) z \ (nat_raw w \ nat_raw z) = (le_raw w z)" + apply (cases w) + apply (cases z) + apply (simp add: nat_raw_def le_raw_def) + by auto + +lemma [quot_respect]: + shows "(intrel ===> op =) nat_raw nat_raw" + by (auto iff: nat_raw_def) + +lemma nat_le_eq_zle: + fixes w z::"int" + shows "0 < w \ 0 \ z \ (nat2 w \ nat2 z) = (w\z)" + unfolding less_int_def + by (lifting nat_le_eq_zle_raw) + +end diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Quotient_Examples/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,8 @@ +(* Title: HOL/Quotient_Examples/ROOT.ML + Author: Cezary Kaliszyk and Christian Urban + +Testing the quotient package. +*) + +use_thys ["LarryInt", "LarryDatatype"]; + diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Tools/Quotient/quotient_def.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,110 @@ +(* Title: quotient_def.thy + Author: Cezary Kaliszyk and Christian Urban + + Definitions for constants on quotient types. + +*) + +signature QUOTIENT_DEF = +sig + val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) -> + local_theory -> (term * thm) * local_theory + + val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) -> + local_theory -> (term * thm) * local_theory + + val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory +end; + +structure Quotient_Def: QUOTIENT_DEF = +struct + +open Quotient_Info; +open Quotient_Term; + +(** Interface and Syntax Setup **) + +(* The ML-interface for a quotient definition takes + as argument: + + - an optional binding and mixfix annotation + - attributes + - the new constant as term + - the rhs of the definition as term + + It returns the defined constant and its definition + theorem; stores the data in the qconsts data slot. + + Restriction: At the moment the right-hand side of the + definition must be a constant. Similarly the left-hand + side must be a constant. +*) +fun error_msg bind str = +let + val name = Binding.name_of bind + val pos = Position.str_of (Binding.pos_of bind) +in + error ("Head of quotient_definition " ^ + (quote str) ^ " differs from declaration " ^ name ^ pos) +end + +fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy = +let + val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." + val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" + + fun sanity_test NONE _ = true + | sanity_test (SOME bind) str = + if Name.of_binding bind = str then true + else error_msg bind str + + val _ = sanity_test optbind lhs_str + + val qconst_bname = Binding.name lhs_str + val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs + val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) + val (_, prop') = LocalDefs.cert_def lthy prop + val (_, newrhs) = Primitive_Defs.abs_def prop' + + val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy + + (* data storage *) + fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} + fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) + val lthy'' = Local_Theory.declaration true + (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' +in + ((trm, thm), lthy'') +end + +fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy = +let + val lhs = Syntax.read_term lthy lhs_str + val rhs = Syntax.read_term lthy rhs_str + val lthy' = Variable.declare_term lhs lthy + val lthy'' = Variable.declare_term rhs lthy' +in + quotient_def (decl, (attr, (lhs, rhs))) lthy'' +end + +fun quotient_lift_const (b, t) ctxt = + quotient_def ((NONE, NoSyn), (Attrib.empty_binding, + (Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt + +local + structure P = OuterParse; +in + +val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where" + +val quotdef_parser = + Scan.optional quotdef_decl (NONE, NoSyn) -- + P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term)) +end + +val _ = + OuterSyntax.local_theory "quotient_definition" + "definition for constants over the quotient type" + OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd)) + +end; (* structure *) diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Tools/Quotient/quotient_info.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,289 @@ +(* Title: quotient_info.thy + Author: Cezary Kaliszyk and Christian Urban + + Data slots for the quotient package. + +*) + + +signature QUOTIENT_INFO = +sig + exception NotFound + + type maps_info = {mapfun: string, relmap: string} + val maps_defined: theory -> string -> bool + val maps_lookup: theory -> string -> maps_info (* raises NotFound *) + val maps_update_thy: string -> maps_info -> theory -> theory + val maps_update: string -> maps_info -> Proof.context -> Proof.context + val print_mapsinfo: Proof.context -> unit + + type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} + val transform_quotdata: morphism -> quotdata_info -> quotdata_info + val quotdata_lookup_raw: theory -> string -> quotdata_info option + val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) + val quotdata_update_thy: string -> quotdata_info -> theory -> theory + val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic + val quotdata_dest: Proof.context -> quotdata_info list + val print_quotinfo: Proof.context -> unit + + type qconsts_info = {qconst: term, rconst: term, def: thm} + val transform_qconsts: morphism -> qconsts_info -> qconsts_info + val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) + val qconsts_update_thy: string -> qconsts_info -> theory -> theory + val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic + val qconsts_dest: Proof.context -> qconsts_info list + val print_qconstinfo: Proof.context -> unit + + val equiv_rules_get: Proof.context -> thm list + val equiv_rules_add: attribute + val rsp_rules_get: Proof.context -> thm list + val prs_rules_get: Proof.context -> thm list + val id_simps_get: Proof.context -> thm list + val quotient_rules_get: Proof.context -> thm list + val quotient_rules_add: attribute +end; + + +structure Quotient_Info: QUOTIENT_INFO = +struct + +exception NotFound + + +(** data containers **) + +(* info about map- and rel-functions for a type *) +type maps_info = {mapfun: string, relmap: string} + +structure MapsData = Theory_Data + (type T = maps_info Symtab.table + val empty = Symtab.empty + val extend = I + val merge = Symtab.merge (K true)) + +fun maps_defined thy s = + Symtab.defined (MapsData.get thy) s + +fun maps_lookup thy s = + case (Symtab.lookup (MapsData.get thy) s) of + SOME map_fun => map_fun + | NONE => raise NotFound + +fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) +fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) + +fun maps_attribute_aux s minfo = Thm.declaration_attribute + (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) + +(* attribute to be used in declare statements *) +fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = +let + val thy = ProofContext.theory_of ctxt + val tyname = Sign.intern_type thy tystr + val mapname = Sign.intern_const thy mapstr + val relname = Sign.intern_const thy relstr + + fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ()) + val _ = List.app sanity_check [mapname, relname] +in + maps_attribute_aux tyname {mapfun = mapname, relmap = relname} +end + +val maps_attr_parser = + Args.context -- Scan.lift + ((Args.name --| OuterParse.$$$ "=") -- + (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- + Args.name --| OuterParse.$$$ ")")) + +val _ = Context.>> (Context.map_theory + (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) + "declaration of map information")) + +fun print_mapsinfo ctxt = +let + fun prt_map (ty_name, {mapfun, relmap}) = + Pretty.block (Library.separate (Pretty.brk 2) + (map Pretty.str + ["type:", ty_name, + "map:", mapfun, + "relation map:", relmap])) +in + MapsData.get (ProofContext.theory_of ctxt) + |> Symtab.dest + |> map (prt_map) + |> Pretty.big_list "maps for type constructors:" + |> Pretty.writeln +end + + +(* info about quotient types *) +type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} + +structure QuotData = Theory_Data + (type T = quotdata_info Symtab.table + val empty = Symtab.empty + val extend = I + val merge = Symtab.merge (K true)) + +fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = + {qtyp = Morphism.typ phi qtyp, + rtyp = Morphism.typ phi rtyp, + equiv_rel = Morphism.term phi equiv_rel, + equiv_thm = Morphism.thm phi equiv_thm} + +fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str + +fun quotdata_lookup thy str = + case Symtab.lookup (QuotData.get thy) str of + SOME qinfo => qinfo + | NONE => raise NotFound + +fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) +fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I + +fun quotdata_dest lthy = + map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy))) + +fun print_quotinfo ctxt = +let + fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = + Pretty.block (Library.separate (Pretty.brk 2) + [Pretty.str "quotient type:", + Syntax.pretty_typ ctxt qtyp, + Pretty.str "raw type:", + Syntax.pretty_typ ctxt rtyp, + Pretty.str "relation:", + Syntax.pretty_term ctxt equiv_rel, + Pretty.str "equiv. thm:", + Syntax.pretty_term ctxt (prop_of equiv_thm)]) +in + QuotData.get (ProofContext.theory_of ctxt) + |> Symtab.dest + |> map (prt_quot o snd) + |> Pretty.big_list "quotients:" + |> Pretty.writeln +end + + +(* info about quotient constants *) +type qconsts_info = {qconst: term, rconst: term, def: thm} + +fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y + +(* We need to be able to lookup instances of lifted constants, + for example given "nat fset" we need to find "'a fset"; + but overloaded constants share the same name *) +structure QConstsData = Theory_Data + (type T = (qconsts_info list) Symtab.table + val empty = Symtab.empty + val extend = I + val merge = Symtab.merge_list qconsts_info_eq) + +fun transform_qconsts phi {qconst, rconst, def} = + {qconst = Morphism.term phi qconst, + rconst = Morphism.term phi rconst, + def = Morphism.thm phi def} + +fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo)) +fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I + +fun qconsts_dest lthy = + flat (map snd (Symtab.dest (QConstsData.get (ProofContext.theory_of lthy)))) + +fun qconsts_lookup thy t = + let + val (name, qty) = dest_Const t + fun matches x = + let + val (name', qty') = dest_Const (#qconst x); + in + name = name' andalso Sign.typ_instance thy (qty, qty') + end + in + case Symtab.lookup (QConstsData.get thy) name of + NONE => raise NotFound + | SOME l => + (case (find_first matches l) of + SOME x => x + | NONE => raise NotFound) + end + +fun print_qconstinfo ctxt = +let + fun prt_qconst {qconst, rconst, def} = + Pretty.block (separate (Pretty.brk 1) + [Syntax.pretty_term ctxt qconst, + Pretty.str ":=", + Syntax.pretty_term ctxt rconst, + Pretty.str "as", + Syntax.pretty_term ctxt (prop_of def)]) +in + QConstsData.get (ProofContext.theory_of ctxt) + |> Symtab.dest + |> map snd + |> flat + |> map prt_qconst + |> Pretty.big_list "quotient constants:" + |> Pretty.writeln +end + +(* equivalence relation theorems *) +structure EquivRules = Named_Thms + (val name = "quot_equiv" + val description = "Equivalence relation theorems.") + +val equiv_rules_get = EquivRules.get +val equiv_rules_add = EquivRules.add + +(* respectfulness theorems *) +structure RspRules = Named_Thms + (val name = "quot_respect" + val description = "Respectfulness theorems.") + +val rsp_rules_get = RspRules.get + +(* preservation theorems *) +structure PrsRules = Named_Thms + (val name = "quot_preserve" + val description = "Preservation theorems.") + +val prs_rules_get = PrsRules.get + +(* id simplification theorems *) +structure IdSimps = Named_Thms + (val name = "id_simps" + val description = "Identity simp rules for maps.") + +val id_simps_get = IdSimps.get + +(* quotient theorems *) +structure QuotientRules = Named_Thms + (val name = "quot_thm" + val description = "Quotient theorems.") + +val quotient_rules_get = QuotientRules.get +val quotient_rules_add = QuotientRules.add + +(* setup of the theorem lists *) + +val _ = Context.>> (Context.map_theory + (EquivRules.setup #> + RspRules.setup #> + PrsRules.setup #> + IdSimps.setup #> + QuotientRules.setup)) + +(* setup of the printing commands *) + +fun improper_command (pp_fn, cmd_name, descr_str) = + OuterSyntax.improper_command cmd_name descr_str + OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of))) + +val _ = map improper_command + [(print_mapsinfo, "print_maps", "prints out all map functions"), + (print_quotinfo, "print_quotients", "prints out all quotients"), + (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")] + + +end; (* structure *) + diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Tools/Quotient/quotient_tacs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,665 @@ +(* Title: quotient_tacs.thy + Author: Cezary Kaliszyk and Christian Urban + + Tactics for solving goal arising from lifting + theorems to quotient types. +*) + +signature QUOTIENT_TACS = +sig + val regularize_tac: Proof.context -> int -> tactic + val injection_tac: Proof.context -> int -> tactic + val all_injection_tac: Proof.context -> int -> tactic + val clean_tac: Proof.context -> int -> tactic + val procedure_tac: Proof.context -> thm -> int -> tactic + val lift_tac: Proof.context -> thm list -> int -> tactic + val quotient_tac: Proof.context -> int -> tactic + val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic + val lifted_attrib: attribute +end; + +structure Quotient_Tacs: QUOTIENT_TACS = +struct + +open Quotient_Info; +open Quotient_Term; + + +(** various helper fuctions **) + +(* Since HOL_basic_ss is too "big" for us, we *) +(* need to set up our own minimal simpset. *) +fun mk_minimal_ss ctxt = + Simplifier.context ctxt empty_ss + setsubgoaler asm_simp_tac + setmksimps (mksimps []) + +(* composition of two theorems, used in maps *) +fun OF1 thm1 thm2 = thm2 RS thm1 + +(* prints a warning, if the subgoal is not solved *) +fun WARN (tac, msg) i st = + case Seq.pull (SOLVED' tac i st) of + NONE => (warning msg; Seq.single st) + | seqcell => Seq.make (fn () => seqcell) + +fun RANGE_WARN tacs = RANGE (map WARN tacs) + +fun atomize_thm thm = +let + val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *) + val thm'' = ObjectLogic.atomize (cprop_of thm') +in + @{thm equal_elim_rule1} OF [thm'', thm'] +end + + + +(*** Regularize Tactic ***) + +(** solvers for equivp and quotient assumptions **) + +fun equiv_tac ctxt = + REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) + +fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) +val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac + +fun quotient_tac ctxt = + (REPEAT_ALL_NEW (FIRST' + [rtac @{thm identity_quotient}, + resolve_tac (quotient_rules_get ctxt)])) + +fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) +val quotient_solver = + Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac + +fun solve_quotient_assm ctxt thm = + case Seq.pull (quotient_tac ctxt 1 thm) of + SOME (t, _) => t + | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing." + + +fun prep_trm thy (x, (T, t)) = + (cterm_of thy (Var (x, T)), cterm_of thy t) + +fun prep_ty thy (x, (S, ty)) = + (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) + +fun get_match_inst thy pat trm = +let + val univ = Unify.matchers thy [(pat, trm)] + val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) + val tenv = Vartab.dest (Envir.term_env env) + val tyenv = Vartab.dest (Envir.type_env env) +in + (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) +end + +(* Calculates the instantiations for the lemmas: + + ball_reg_eqv_range and bex_reg_eqv_range + + Since the left-hand-side contains a non-pattern '?P (f ?x)' + we rely on unification/instantiation to check whether the + theorem applies and return NONE if it doesn't. +*) +fun calculate_inst ctxt ball_bex_thm redex R1 R2 = +let + val thy = ProofContext.theory_of ctxt + fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) + val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] + val trm_inst = map (SOME o cterm_of thy) [R2, R1] +in + case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of + NONE => NONE + | SOME thm' => + (case try (get_match_inst thy (get_lhs thm')) redex of + NONE => NONE + | SOME inst2 => try (Drule.instantiate inst2) thm') +end + +fun ball_bex_range_simproc ss redex = +let + val ctxt = Simplifier.the_context ss +in + case redex of + (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => + calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2 + + | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => + calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 + + | _ => NONE +end + +(* Regularize works as follows: + + 0. preliminary simplification step according to + ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range + + 1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left) + + 2. monos + + 3. commutation rules for ball and bex (ball_all_comm bex_ex_comm) + + 4. then rel-equalities, which need to be instantiated with 'eq_imp_rel' + to avoid loops + + 5. then simplification like 0 + + finally jump back to 1 +*) + +fun regularize_tac ctxt = +let + val thy = ProofContext.theory_of ctxt + val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} + val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} + val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) + val simpset = (mk_minimal_ss ctxt) + addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} + addsimprocs [simproc] + addSolver equiv_solver addSolver quotient_solver + val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)} + val eq_eqvs = map (OF1 eq_imp_rel) (equiv_rules_get ctxt) +in + simp_tac simpset THEN' + REPEAT_ALL_NEW (CHANGED o FIRST' + [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg}, + resolve_tac (Inductive.get_monos ctxt), + resolve_tac @{thms ball_all_comm bex_ex_comm}, + resolve_tac eq_eqvs, + simp_tac simpset]) +end + + + +(*** Injection Tactic ***) + +(* Looks for Quot_True assumptions, and in case its parameter + is an application, it returns the function and the argument. +*) +fun find_qt_asm asms = +let + fun find_fun trm = + case trm of + (Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true + | _ => false +in + case find_first find_fun asms of + SOME (_ $ (_ $ (f $ a))) => SOME (f, a) + | _ => NONE +end + +fun quot_true_simple_conv ctxt fnctn ctrm = + case (term_of ctrm) of + (Const (@{const_name Quot_True}, _) $ x) => + let + val fx = fnctn x; + val thy = ProofContext.theory_of ctxt; + val cx = cterm_of thy x; + val cfx = cterm_of thy fx; + val cxt = ctyp_of thy (fastype_of x); + val cfxt = ctyp_of thy (fastype_of fx); + val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp} + in + Conv.rewr_conv thm ctrm + end + +fun quot_true_conv ctxt fnctn ctrm = + case (term_of ctrm) of + (Const (@{const_name Quot_True}, _) $ _) => + quot_true_simple_conv ctxt fnctn ctrm + | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm + | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm + | _ => Conv.all_conv ctrm + +fun quot_true_tac ctxt fnctn = + CONVERSION + ((Conv.params_conv ~1 (fn ctxt => + (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) + +fun dest_comb (f $ a) = (f, a) +fun dest_bcomb ((_ $ l) $ r) = (l, r) + +fun unlam t = + case t of + (Abs a) => snd (Term.dest_abs a) + | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) + +fun dest_fun_type (Type("fun", [T, S])) = (T, S) + | dest_fun_type _ = error "dest_fun_type" + +val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl + +(* We apply apply_rsp only in case if the type needs lifting. + This is the case if the type of the data in the Quot_True + assumption is different from the corresponding type in the goal. +*) +val apply_rsp_tac = + Subgoal.FOCUS (fn {concl, asms, context,...} => + let + val bare_concl = HOLogic.dest_Trueprop (term_of concl) + val qt_asm = find_qt_asm (map term_of asms) + in + case (bare_concl, qt_asm) of + (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => + if fastype_of qt_fun = fastype_of f + then no_tac + else + let + val ty_x = fastype_of x + val ty_b = fastype_of qt_arg + val ty_f = range_type (fastype_of f) + val thy = ProofContext.theory_of context + 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} + in + (rtac inst_thm THEN' quotient_tac context) 1 + end + | _ => no_tac + end) + +(* Instantiates and applies 'equals_rsp'. Since the theorem is + complex we rely on instantiation to tell us if it applies +*) +fun equals_rsp_tac R ctxt = +let + val thy = ProofContext.theory_of ctxt +in + case try (cterm_of thy) R of (* There can be loose bounds in R *) + SOME ctm => + let + val ty = domain_type (fastype_of R) + in + case try (Drule.instantiate' [SOME (ctyp_of thy ty)] + [SOME (cterm_of thy R)]) @{thm equals_rsp} of + SOME thm => rtac thm THEN' quotient_tac ctxt + | NONE => K no_tac + end + | _ => K no_tac +end + +fun rep_abs_rsp_tac ctxt = + SUBGOAL (fn (goal, i) => + case (try bare_concl goal) of + SOME (rel $ _ $ (rep $ (abs $ _))) => + let + val thy = ProofContext.theory_of ctxt; + val (ty_a, ty_b) = dest_fun_type (fastype_of abs); + val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; + in + case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of + SOME t_inst => + (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of + SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i + | NONE => no_tac) + | NONE => no_tac + end + | _ => no_tac) + + + +(* Injection means to prove that the regularised theorem implies + the abs/rep injected one. + + The deterministic part: + - remove lambdas from both sides + - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp + - prove Ball/Bex relations unfolding fun_rel_id + - reflexivity of equality + - prove equality of relations using equals_rsp + - use user-supplied RSP theorems + - solve 'relation of relations' goals using quot_rel_rsp + - remove rep_abs from the right side + (Lambdas under respects may have left us some assumptions) + + Then in order: + - split applications of lifted type (apply_rsp) + - split applications of non-lifted type (cong_tac) + - apply extentionality + - assumption + - reflexivity of the relation +*) +fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) => +(case (bare_concl goal) of + (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) + (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + + (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *) +| (Const (@{const_name "op ="},_) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) + => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} + + (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *) +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + + (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *) +| Const (@{const_name "op ="},_) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} + + (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *) +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _) + => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt + +| (_ $ + (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) + => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] + +| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => + (rtac @{thm refl} ORELSE' + (equals_rsp_tac R ctxt THEN' RANGE [ + quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) + + (* reflexivity of operators arising from Cong_tac *) +| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl} + + (* respectfulness of constants; in particular of a simple relation *) +| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) + => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt + + (* R (...) (Rep (Abs ...)) ----> R (...) (...) *) + (* observe fun_map *) +| _ $ _ $ _ + => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) + ORELSE' rep_abs_rsp_tac ctxt + +| _ => K no_tac +) i) + +fun injection_step_tac ctxt rel_refl = + FIRST' [ + injection_match_tac ctxt, + + (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) + apply_rsp_tac ctxt THEN' + RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], + + (* (op =) (t $ ...) (t' $ ...) ----> Cong provided type of t does not need lifting *) + (* merge with previous tactic *) + Cong_Tac.cong_tac @{thm cong} THEN' + RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], + + (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *) + rtac @{thm ext} THEN' quot_true_tac ctxt unlam, + + (* resolving with R x y assumptions *) + atac, + + (* reflexivity of the basic relations *) + (* R ... ... *) + resolve_tac rel_refl] + +fun injection_tac ctxt = +let + val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) +in + injection_step_tac ctxt rel_refl +end + +fun all_injection_tac ctxt = + REPEAT_ALL_NEW (injection_tac ctxt) + + + +(*** Cleaning of the Theorem ***) + +(* expands all fun_maps, except in front of the (bound) variables listed in xs *) +fun fun_map_simple_conv xs ctrm = + case (term_of ctrm) of + ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => + if member (op=) xs h + then Conv.all_conv ctrm + else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm + | _ => Conv.all_conv ctrm + +fun fun_map_conv xs ctxt ctrm = + case (term_of ctrm) of + _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv + fun_map_simple_conv xs) ctrm + | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm + | _ => Conv.all_conv ctrm + +fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) + +(* custom matching functions *) +fun mk_abs u i t = + if incr_boundvars i u aconv t then Bound i else + case t of + t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2 + | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') + | Bound j => if i = j then error "make_inst" else t + | _ => t + +fun make_inst lhs t = +let + val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; + val _ $ (Abs (_, _, (_ $ g))) = t; +in + (f, Abs ("x", T, mk_abs u 0 g)) +end + +fun make_inst_id lhs t = +let + val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; + val _ $ (Abs (_, _, g)) = t; +in + (f, Abs ("x", T, mk_abs u 0 g)) +end + +(* Simplifies a redex using the 'lambda_prs' theorem. + First instantiates the types and known subterms. + Then solves the quotient assumptions to get Rep2 and Abs1 + Finally instantiates the function f using make_inst + If Rep2 is an identity then the pattern is simpler and + make_inst_id is used +*) +fun lambda_prs_simple_conv ctxt ctrm = + case (term_of ctrm) of + (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => + let + val thy = ProofContext.theory_of ctxt + val (ty_b, ty_a) = dest_fun_type (fastype_of r1) + val (ty_c, ty_d) = dest_fun_type (fastype_of a2) + val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] + val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] + val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} + val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1) + val thm3 = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2 + val (insp, inst) = + if ty_c = ty_d + then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm) + else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm) + val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3 + in + Conv.rewr_conv thm4 ctrm + end + | _ => Conv.all_conv ctrm + +fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt +fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) + + +(* Cleaning consists of: + + 1. unfolding of ---> in front of everything, except + bound variables (this prevents lambda_prs from + becoming stuck) + + 2. simplification with lambda_prs + + 3. simplification with: + + - Quotient_abs_rep Quotient_rel_rep + babs_prs all_prs ex_prs ex1_prs + + - id_simps and preservation lemmas and + + - symmetric versions of the definitions + (that is definitions of quotient constants + are folded) + + 4. test for refl +*) +fun clean_tac lthy = +let + val defs = map (symmetric o #def) (qconsts_dest lthy) + val prs = prs_rules_get lthy + val ids = id_simps_get lthy + val thms = @{thms Quotient_abs_rep Quotient_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 + EVERY' [fun_map_tac lthy, + lambda_prs_tac lthy, + simp_tac ss, + TRY o rtac refl] +end + + + +(** Tactic for Generalising Free Variables in a Goal **) + +fun inst_spec ctrm = + Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} + +fun inst_spec_tac ctrms = + EVERY' (map (dtac o inst_spec) ctrms) + +fun all_list xs trm = + fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm + +fun apply_under_Trueprop f = + HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop + +fun gen_frees_tac ctxt = + SUBGOAL (fn (concl, i) => + let + val thy = ProofContext.theory_of ctxt + val vrs = Term.add_frees concl [] + val cvrs = map (cterm_of thy o Free) vrs + val concl' = apply_under_Trueprop (all_list vrs) concl + val goal = Logic.mk_implies (concl', concl) + val rule = Goal.prove ctxt [] [] goal + (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) + in + rtac rule i + end) + + +(** The General Shape of the Lifting Procedure **) + +(* - A is the original raw theorem + - B is the regularized theorem + - C is the rep/abs injected version of B + - D is the lifted theorem + + - 1st prem is the regularization step + - 2nd prem is the rep/abs injection step + - 3rd prem is the cleaning part + + the Quot_True premise in 2nd records the lifted theorem +*) +val lifting_procedure_thm = + @{lemma "[|A; + A --> B; + Quot_True D ==> B = C; + C = D|] ==> D" + by (simp add: Quot_True_def)} + +fun lift_match_error ctxt msg rtrm qtrm = +let + val rtrm_str = Syntax.string_of_term ctxt rtrm + val qtrm_str = Syntax.string_of_term ctxt qtrm + val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str, + "", "does not match with original theorem", rtrm_str] +in + error msg +end + +fun procedure_inst ctxt rtrm qtrm = +let + val thy = ProofContext.theory_of ctxt + val rtrm' = HOLogic.dest_Trueprop rtrm + val qtrm' = HOLogic.dest_Trueprop qtrm + val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm') + handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm + val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') + handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm +in + Drule.instantiate' [] + [SOME (cterm_of thy rtrm'), + SOME (cterm_of thy reg_goal), + NONE, + SOME (cterm_of thy inj_goal)] lifting_procedure_thm +end + +(* the tactic leaves three subgoals to be proved *) +fun procedure_tac ctxt rthm = + ObjectLogic.full_atomize_tac + THEN' gen_frees_tac ctxt + THEN' SUBGOAL (fn (goal, i) => + let + val rthm' = atomize_thm rthm + val rule = procedure_inst ctxt (prop_of rthm') goal + in + (rtac rule THEN' rtac rthm') i + end) + + +(* Automatic Proofs *) + +val msg1 = "The regularize proof failed." +val msg2 = cat_lines ["The injection proof failed.", + "This is probably due to missing respects lemmas.", + "Try invoking the injection method manually to see", + "which lemmas are missing."] +val msg3 = "The cleaning proof failed." + +fun lift_tac ctxt rthms = +let + fun mk_tac rthm = + procedure_tac ctxt rthm + THEN' RANGE_WARN + [(regularize_tac ctxt, msg1), + (all_injection_tac ctxt, msg2), + (clean_tac ctxt, msg3)] +in + simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) + THEN' RANGE (map mk_tac rthms) +end + +(* An Attribute which automatically constructs the qthm *) +fun lifted_attrib_aux context thm = +let + val ctxt = Context.proof_of context + val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt + val goal = (quotient_lift_all ctxt' o prop_of) thm' +in + Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm] 1)) + |> singleton (ProofContext.export ctxt' ctxt) +end; + +val lifted_attrib = Thm.rule_attribute lifted_attrib_aux + +end; (* structure *) diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Tools/Quotient/quotient_term.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,786 @@ +(* Title: quotient_term.thy + Author: Cezary Kaliszyk and Christian Urban + + Constructs terms corresponding to goals from + lifting theorems to quotient types. +*) + +signature QUOTIENT_TERM = +sig + exception LIFT_MATCH of string + + datatype flag = AbsF | RepF + + val absrep_fun: flag -> Proof.context -> typ * typ -> term + val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term + + (* Allows Nitpick to represent quotient types as single elements from raw type *) + val absrep_const_chk: flag -> Proof.context -> string -> term + + val equiv_relation: Proof.context -> typ * typ -> term + val equiv_relation_chk: Proof.context -> typ * typ -> term + + val regularize_trm: Proof.context -> term * term -> term + val regularize_trm_chk: Proof.context -> term * term -> term + + val inj_repabs_trm: Proof.context -> term * term -> term + val inj_repabs_trm_chk: Proof.context -> term * term -> term + + val quotient_lift_const: string * term -> local_theory -> term + val quotient_lift_all: Proof.context -> term -> term +end; + +structure Quotient_Term: QUOTIENT_TERM = +struct + +open Quotient_Info; + +exception LIFT_MATCH of string + + + +(*** Aggregate Rep/Abs Function ***) + + +(* The flag RepF is for types in negative position; AbsF is for types + in positive position. Because of this, function types need to be + treated specially, since there the polarity changes. +*) + +datatype flag = AbsF | RepF + +fun negF AbsF = RepF + | negF RepF = AbsF + +fun is_identity (Const (@{const_name "id"}, _)) = true + | is_identity _ = false + +fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) + +fun mk_fun_compose flag (trm1, trm2) = + case flag of + AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 + | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 + +fun get_mapfun ctxt s = +let + val thy = ProofContext.theory_of ctxt + val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") + val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn +in + Const (mapfun, dummyT) +end + +(* makes a Free out of a TVar *) +fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) + +(* produces an aggregate map function for the + rty-part of a quotient definition; abstracts + over all variables listed in vs (these variables + correspond to the type variables in rty) + + for example for: (?'a list * ?'b) + it produces: %a b. prod_map (map a) b +*) +fun mk_mapfun ctxt vs rty = +let + val vs' = map (mk_Free) vs + + fun mk_mapfun_aux rty = + case rty of + TVar _ => mk_Free rty + | Type (_, []) => mk_identity rty + | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) + | _ => raise LIFT_MATCH "mk_mapfun (default)" +in + fold_rev Term.lambda vs' (mk_mapfun_aux rty) +end + +(* looks up the (varified) rty and qty for + a quotient definition +*) +fun get_rty_qty ctxt s = +let + val thy = ProofContext.theory_of ctxt + val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") + val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn +in + (#rtyp qdata, #qtyp qdata) +end + +(* takes two type-environments and looks + up in both of them the variable v, which + must be listed in the environment +*) +fun double_lookup rtyenv qtyenv v = +let + val v' = fst (dest_TVar v) +in + (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) +end + +(* matches a type pattern with a type *) +fun match ctxt err ty_pat ty = +let + val thy = ProofContext.theory_of ctxt +in + Sign.typ_match thy (ty_pat, ty) Vartab.empty + handle MATCH_TYPE => err ctxt ty_pat ty +end + +(* produces the rep or abs constant for a qty *) +fun absrep_const flag ctxt qty_str = +let + val thy = ProofContext.theory_of ctxt + val qty_name = Long_Name.base_name qty_str +in + case flag of + AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) + | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) +end + +(* Lets Nitpick represent elements of quotient types as elements of the raw type *) +fun absrep_const_chk flag ctxt qty_str = + Syntax.check_term ctxt (absrep_const flag ctxt qty_str) + +fun absrep_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 " " + ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) +end + + +(** generation of an aggregate absrep function **) + +(* - In case of equal types we just return the identity. + + - In case of TFrees we also return the identity. + + - In case of function types we recurse taking + the polarity change into account. + + - If the type constructors are equal, we recurse for the + arguments and build the appropriate map function. + + - If the type constructors are unequal, there must be an + instance of quotient types: + + - we first look up the corresponding rty_pat and qty_pat + from the quotient definition; the arguments of qty_pat + must be some distinct TVars + - we then match the rty_pat with rty and qty_pat with qty; + if matching fails the types do not correspond -> error + - the matching produces two environments; we look up the + assignments for the qty_pat variables and recurse on the + assignments + - we prefix the aggregate map function for the rty_pat, + which is an abstraction over all type variables + - finally we compose the result with the appropriate + absrep function in case at least one argument produced + a non-identity function / + otherwise we just return the appropriate absrep + function + + The composition is necessary for types like + + ('a list) list / ('a foo) foo + + The matching is necessary for types like + + ('a * 'a) list / 'a bar + + The test is necessary in order to eliminate superfluous + identity maps. +*) + +fun absrep_fun flag ctxt (rty, qty) = + if rty = qty + then mk_identity rty + else + case (rty, qty) of + (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => + let + val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') + val arg2 = absrep_fun flag ctxt (ty2, ty2') + in + list_comb (get_mapfun ctxt "fun", [arg1, arg2]) + end + | (Type (s, tys), Type (s', tys')) => + if s = s' + then + let + val args = map (absrep_fun flag ctxt) (tys ~~ tys') + in + list_comb (get_mapfun ctxt s, args) + end + else + let + val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' + val rtyenv = match ctxt absrep_match_err rty_pat rty + val qtyenv = match ctxt absrep_match_err qty_pat qty + val args_aux = map (double_lookup rtyenv qtyenv) vs + val args = map (absrep_fun flag ctxt) args_aux + val map_fun = mk_mapfun ctxt vs rty_pat + val result = list_comb (map_fun, args) + in + if forall is_identity args + then absrep_const flag ctxt s' + else mk_fun_compose flag (absrep_const flag ctxt s', result) + end + | (TFree x, TFree x') => + if x = x' + then mk_identity rty + else raise (LIFT_MATCH "absrep_fun (frees)") + | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") + | _ => raise (LIFT_MATCH "absrep_fun (default)") + +fun absrep_fun_chk flag ctxt (rty, qty) = + absrep_fun flag ctxt (rty, qty) + |> Syntax.check_term ctxt + + + + +(*** Aggregate Equivalence Relation ***) + + +(* works very similar to the absrep generation, + except there is no need for polarities +*) + +(* instantiates TVars so that the term is of type ty *) +fun force_typ ctxt trm ty = +let + val thy = ProofContext.theory_of ctxt + val trm_ty = fastype_of trm + val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty +in + map_types (Envir.subst_type ty_inst) trm +end + +fun is_eq (Const (@{const_name "op ="}, _)) = true + | is_eq _ = false + +fun mk_rel_compose (trm1, trm2) = + Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2 + +fun get_relmap ctxt s = +let + val thy = ProofContext.theory_of ctxt + val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") + val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn +in + Const (relmap, dummyT) +end + +fun mk_relmap ctxt vs rty = +let + val vs' = map (mk_Free) vs + + fun mk_relmap_aux rty = + case rty of + TVar _ => mk_Free rty + | Type (_, []) => HOLogic.eq_const rty + | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys) + | _ => raise LIFT_MATCH ("mk_relmap (default)") +in + fold_rev Term.lambda vs' (mk_relmap_aux rty) +end + +fun get_equiv_rel ctxt s = +let + val thy = ProofContext.theory_of ctxt + val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") +in + #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn +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 + +(* builds the aggregate equivalence relation + that will be the argument of Respects +*) +fun equiv_relation ctxt (rty, qty) = + if rty = qty + then HOLogic.eq_const rty + else + case (rty, qty) of + (Type (s, tys), Type (s', tys')) => + if s = s' + then + let + val args = map (equiv_relation ctxt) (tys ~~ tys') + in + list_comb (get_relmap ctxt s, args) + end + else + let + val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' + val rtyenv = match ctxt equiv_match_err rty_pat rty + val qtyenv = match ctxt equiv_match_err qty_pat qty + val args_aux = map (double_lookup rtyenv qtyenv) vs + val args = map (equiv_relation ctxt) args_aux + val rel_map = mk_relmap ctxt vs rty_pat + val result = list_comb (rel_map, args) + val eqv_rel = get_equiv_rel ctxt s' + val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) + in + if forall is_eq args + then eqv_rel' + else mk_rel_compose (result, eqv_rel') + end + | _ => HOLogic.eq_const rty + +fun equiv_relation_chk ctxt (rty, qty) = + equiv_relation ctxt (rty, qty) + |> Syntax.check_term ctxt + + + +(*** Regularization ***) + +(* Regularizing an rtrm means: + + - Quantifiers over types that need lifting are replaced + by bounded quantifiers, for example: + + All P ----> All (Respects R) P + + where the aggregate relation R is given by the rty and qty; + + - Abstractions over types that need lifting are replaced + by bounded abstractions, for example: + + %x. P ----> Ball (Respects R) %x. P + + - Equalities over types that need lifting are replaced by + corresponding equivalence relations, for example: + + A = B ----> R A B + + or + + A = B ----> (R ===> R) A B + + for more complicated types of A and B + + + The regularize_trm accepts raw theorems in which equalities + and quantifiers match exactly the ones in the lifted theorem + but also accepts partially regularized terms. + + This means that the raw theorems can have: + Ball (Respects R), Bex (Respects R), Bex1_rel (Respects R), Babs, R + in the places where: + All, Ex, Ex1, %, (op =) + is required the lifted theorem. + +*) + +val mk_babs = Const (@{const_name Babs}, dummyT) +val mk_ball = Const (@{const_name Ball}, dummyT) +val mk_bex = Const (@{const_name Bex}, dummyT) +val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT) +val mk_resp = Const (@{const_name Respects}, dummyT) + +(* - applies f to the subterm of an abstraction, + otherwise to the given term, + - used by regularize, therefore abstracted + variables do not have to be treated specially +*) +fun apply_subt f (trm1, trm2) = + case (trm1, trm2) of + (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) + | _ => f (trm1, trm2) + +fun term_mismatch str ctxt t1 t2 = +let + val t1_str = Syntax.string_of_term ctxt t1 + val t2_str = Syntax.string_of_term ctxt t2 + val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1) + val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2) +in + raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) +end + +(* the major type of All and Ex quantifiers *) +fun qnt_typ ty = domain_type (domain_type ty) + +(* Checks that two types match, for example: + rty -> rty matches qty -> qty *) +fun matches_typ thy rT qT = + if rT = qT then true else + case (rT, qT) of + (Type (rs, rtys), Type (qs, qtys)) => + if rs = qs then + if length rtys <> length qtys then false else + forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys) + else + (case Quotient_Info.quotdata_lookup_raw thy qs of + SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) + | NONE => false) + | _ => false + + +(* produces a regularized version of rtrm + + - the result might contain dummyTs + + - for regularisation we do not need any + special treatment of bound variables +*) +fun regularize_trm ctxt (rtrm, qtrm) = + case (rtrm, qtrm) of + (Abs (x, ty, t), Abs (_, ty', t')) => + let + val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) + in + if ty = ty' then subtrm + else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm + end + | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => + let + val subtrm = regularize_trm ctxt (t, t') + val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') + in + if resrel <> needres + then term_mismatch "regularize (Babs)" ctxt resrel needres + else mk_babs $ resrel $ subtrm + end + + | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + in + if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm + else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm + end + + | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + in + if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm + else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm + end + + | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _, + (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $ + (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))), + Const (@{const_name "Ex1"}, ty') $ t') => + let + val t_ = incr_boundvars (~1) t + val subtrm = apply_subt (regularize_trm ctxt) (t_, t') + val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') + in + if resrel <> needrel + then term_mismatch "regularize (Bex1)" ctxt resrel needrel + else mk_bex1_rel $ resrel $ subtrm + end + + | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + in + if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm + else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm + end + + | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, + Const (@{const_name "All"}, ty') $ t') => + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') + in + if resrel <> needrel + then term_mismatch "regularize (Ball)" ctxt resrel needrel + else mk_ball $ (mk_resp $ resrel) $ subtrm + end + + | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, + Const (@{const_name "Ex"}, ty') $ t') => + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') + in + if resrel <> needrel + then term_mismatch "regularize (Bex)" ctxt resrel needrel + else mk_bex $ (mk_resp $ resrel) $ subtrm + end + + | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => + let + val subtrm = apply_subt (regularize_trm ctxt) (t, t') + val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') + in + if resrel <> needrel + then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel + else mk_bex1_rel $ resrel $ subtrm + end + + | (* equalities need to be replaced by appropriate equivalence relations *) + (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => + if ty = ty' then rtrm + else equiv_relation ctxt (domain_type ty, domain_type ty') + + | (* in this case we just check whether the given equivalence relation is correct *) + (rel, Const (@{const_name "op ="}, ty')) => + let + val rel_ty = fastype_of rel + val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') + in + if rel' aconv rel then rtrm + else term_mismatch "regularise (relation mismatch)" ctxt rel rel' + end + + | (_, Const _) => + let + val thy = ProofContext.theory_of ctxt + fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T' + | same_const _ _ = false + in + if same_const rtrm qtrm then rtrm + else + let + val rtrm' = #rconst (qconsts_lookup thy qtrm) + handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm + in + if Pattern.matches thy (rtrm', rtrm) + then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm + end + end + + | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), + ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => + regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) + + | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)), + ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) => + regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) + + | (t1 $ t2, t1' $ t2') => + regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') + + | (Bound i, Bound i') => + if i = i' then rtrm + else raise (LIFT_MATCH "regularize (bounds mismatch)") + + | _ => + let + val rtrm_str = Syntax.string_of_term ctxt rtrm + val qtrm_str = Syntax.string_of_term ctxt qtrm + in + raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) + end + +fun regularize_trm_chk ctxt (rtrm, qtrm) = + regularize_trm ctxt (rtrm, qtrm) + |> Syntax.check_term ctxt + + + +(*** Rep/Abs Injection ***) + +(* +Injection of Rep/Abs means: + + For abstractions: + + * If the type of the abstraction needs lifting, then we add Rep/Abs + around the abstraction; otherwise we leave it unchanged. + + For applications: + + * If the application involves a bounded quantifier, we recurse on + the second argument. If the application is a bounded abstraction, + we always put an Rep/Abs around it (since bounded abstractions + are assumed to always need lifting). Otherwise we recurse on both + arguments. + + For constants: + + * If the constant is (op =), we leave it always unchanged. + Otherwise the type of the constant needs lifting, we put + and Rep/Abs around it. + + For free variables: + + * We put a Rep/Abs around it if the type needs lifting. + + Vars case cannot occur. +*) + +fun mk_repabs ctxt (T, T') trm = + absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm) + +fun inj_repabs_err ctxt msg rtrm qtrm = +let + val rtrm_str = Syntax.string_of_term ctxt rtrm + val qtrm_str = Syntax.string_of_term ctxt qtrm +in + raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) +end + + +(* bound variables need to be treated properly, + as the type of subterms needs to be calculated *) +fun inj_repabs_trm ctxt (rtrm, qtrm) = + case (rtrm, qtrm) of + (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => + Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) + + | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => + Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t')) + + | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => + let + val rty = fastype_of rtrm + val qty = fastype_of qtrm + in + mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))) + end + + | (Abs (x, T, t), Abs (x', T', t')) => + let + val rty = fastype_of rtrm + val qty = fastype_of qtrm + val (y, s) = Term.dest_abs (x, T, t) + val (_, s') = Term.dest_abs (x', T', t') + val yvar = Free (y, T) + val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s')) + in + if rty = qty then result + else mk_repabs ctxt (rty, qty) result + end + + | (t $ s, t' $ s') => + (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s')) + + | (Free (_, T), Free (_, T')) => + if T = T' then rtrm + else mk_repabs ctxt (T, T') rtrm + + | (_, Const (@{const_name "op ="}, _)) => rtrm + + | (_, Const (_, T')) => + let + val rty = fastype_of rtrm + in + if rty = T' then rtrm + else mk_repabs ctxt (rty, T') rtrm + end + + | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm + +fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = + inj_repabs_trm ctxt (rtrm, qtrm) + |> Syntax.check_term ctxt + + + +(*** Wrapper for automatically transforming an rthm into a qthm ***) + +(* subst_tys takes a list of (rty, qty) substitution pairs + and replaces all occurences of rty in the given type + by appropriate qty, with substitution *) +fun subst_ty thy ty (rty, qty) r = + if r <> NONE then r else + case try (Sign.typ_match thy (rty, ty)) Vartab.empty of + SOME inst => SOME (Envir.subst_type inst qty) + | NONE => NONE +fun subst_tys thy substs ty = + case fold (subst_ty thy ty) substs NONE of + SOME ty => ty + | NONE => + (case ty of + Type (s, tys) => Type (s, map (subst_tys thy substs) tys) + | x => x) + +(* subst_trms takes a list of (rtrm, qtrm) substitution pairs + and if the given term matches any of the raw terms it + returns the appropriate qtrm instantiated. If none of + them matched it returns NONE. *) +fun subst_trm thy t (rtrm, qtrm) s = + if s <> NONE then s else + case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of + SOME inst => SOME (Envir.subst_term inst qtrm) + | NONE => NONE; +fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE + +(* prepares type and term substitution pairs to be used by above + functions that let replace all raw constructs by appropriate + lifted counterparts. *) +fun get_ty_trm_substs ctxt = +let + val thy = ProofContext.theory_of ctxt + val quot_infos = Quotient_Info.quotdata_dest ctxt + val const_infos = Quotient_Info.qconsts_dest ctxt + val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos + val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos + fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) + val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos +in + (ty_substs, const_substs @ rel_substs) +end + +fun quotient_lift_const (b, t) ctxt = +let + val thy = ProofContext.theory_of ctxt + val (ty_substs, _) = get_ty_trm_substs ctxt; + val (_, ty) = dest_Const t; + val nty = subst_tys thy ty_substs ty; +in + Free(b, nty) +end + +(* +Takes a term and + +* replaces raw constants by the quotient constants + +* replaces equivalence relations by equalities + +* replaces raw types by the quotient types + +*) + +fun quotient_lift_all ctxt t = +let + val thy = ProofContext.theory_of ctxt + val (ty_substs, substs) = get_ty_trm_substs ctxt + fun lift_aux t = + case subst_trms thy substs t of + SOME x => x + | NONE => + (case t of + a $ b => lift_aux a $ lift_aux b + | Abs(a, ty, s) => + let + val (y, s') = Term.dest_abs (a, ty, s) + val nty = subst_tys thy ty_substs ty + in + Abs(y, nty, abstract_over (Free (y, nty), lift_aux s')) + end + | Free(n, ty) => Free(n, subst_tys thy ty_substs ty) + | Var(n, ty) => Var(n, subst_tys thy ty_substs ty) + | Bound i => Bound i + | Const(s, ty) => Const(s, subst_tys thy ty_substs ty)) +in + lift_aux t +end + + +end; (* structure *) + + + diff -r 04673275441a -r 5d7f22e0f956 src/HOL/Tools/Quotient/quotient_typ.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Feb 19 16:52:30 2010 +0100 @@ -0,0 +1,309 @@ +(* Title: quotient_typ.thy + Author: Cezary Kaliszyk and Christian Urban + + Definition of a quotient type. + +*) + +signature QUOTIENT_TYPE = +sig + val quotient_type: ((string list * binding * mixfix) * (typ * term)) list + -> Proof.context -> Proof.state + + val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list + -> Proof.context -> Proof.state +end; + +structure Quotient_Type: QUOTIENT_TYPE = +struct + +open Quotient_Info; + +(* wrappers for define, note, Attrib.internal and theorem_i *) +fun define (name, mx, rhs) lthy = +let + val ((rhs, (_ , thm)), lthy') = + Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy +in + ((rhs, thm), lthy') +end + +fun note (name, thm, attrs) lthy = +let + val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy +in + (thm', lthy') +end + +fun intern_attr at = Attrib.internal (K at) + +fun theorem after_qed goals ctxt = +let + val goals' = map (rpair []) goals + fun after_qed' thms = after_qed (the_single thms) +in + Proof.theorem_i NONE after_qed' [goals'] ctxt +end + + + +(*** definition of quotient types ***) + +val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)} +val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)} + +(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) +fun typedef_term rel rty lthy = +let + val [x, c] = + [("x", rty), ("c", HOLogic.mk_setT rty)] + |> Variable.variant_frees lthy [rel] + |> map Free +in + lambda c (HOLogic.exists_const rty $ + lambda x (HOLogic.mk_eq (c, (rel $ x)))) +end + + +(* makes the new type definitions and proves non-emptyness *) +fun typedef_make (vs, qty_name, mx, rel, rty) lthy = +let + val typedef_tac = + EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) +in + Local_Theory.theory_result + (Typedef.add_typedef false NONE + (qty_name, vs, mx) + (typedef_term rel rty lthy) + NONE typedef_tac) lthy +end + + +(* tactic to prove the quot_type theorem for the new type *) +fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = +let + val rep_thm = #Rep typedef_info RS mem_def1 + val rep_inv = #Rep_inverse typedef_info + val abs_inv = mem_def2 RS #Abs_inverse typedef_info + val rep_inj = #Rep_inject typedef_info +in + (rtac @{thm quot_type.intro} THEN' RANGE [ + rtac equiv_thm, + rtac rep_thm, + rtac rep_inv, + EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), + rtac rep_inj]) 1 +end + + +(* proves the quot_type theorem for the new type *) +fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = +let + val quot_type_const = Const (@{const_name "quot_type"}, dummyT) + val goal = + HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) + |> Syntax.check_term lthy +in + Goal.prove lthy [] [] goal + (K (typedef_quot_type_tac equiv_thm typedef_info)) +end + +(* proves the quotient theorem for the new type *) +fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = +let + val quotient_const = Const (@{const_name "Quotient"}, dummyT) + val goal = + HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) + |> Syntax.check_term lthy + + val typedef_quotient_thm_tac = + EVERY1 [ + K (rewrite_goals_tac [abs_def, rep_def]), + rtac @{thm quot_type.Quotient}, + rtac quot_type_thm] +in + Goal.prove lthy [] [] goal + (K typedef_quotient_thm_tac) +end + + +(* main function for constructing a quotient type *) +fun mk_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = +let + (* generates the typedef *) + val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy + + (* abs and rep functions from the typedef *) + val Abs_ty = #abs_type typedef_info + val Rep_ty = #rep_type typedef_info + val Abs_name = #Abs_name typedef_info + val Rep_name = #Rep_name typedef_info + val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty) + val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty) + + (* more useful abs and rep definitions *) + val abs_const = Const (@{const_name "quot_type.abs"}, dummyT ) + val rep_const = Const (@{const_name "quot_type.rep"}, dummyT ) + val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const) + val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const) + val abs_name = Binding.prefix_name "abs_" qty_name + val rep_name = Binding.prefix_name "rep_" qty_name + + val ((abs, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1 + val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2 + + (* quot_type theorem *) + val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3 + + (* quotient theorem *) + val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3 + val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name + + (* name equivalence theorem *) + val equiv_thm_name = Binding.suffix_name "_equivp" qty_name + + (* storing the quot-info *) + fun qinfo phi = transform_quotdata phi + {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} + val lthy4 = Local_Theory.declaration true + (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 +in + lthy4 + |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) + ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) +end + + +(* sanity checks for the quotient type specifications *) +fun sanity_check ((vs, qty_name, _), (rty, rel)) = +let + val rty_tfreesT = map fst (Term.add_tfreesT rty []) + val rel_tfrees = map fst (Term.add_tfrees rel []) + val rel_frees = map fst (Term.add_frees rel []) + val rel_vars = Term.add_vars rel [] + val rel_tvars = Term.add_tvars rel [] + val qty_str = Binding.str_of qty_name ^ ": " + + val illegal_rel_vars = + if null rel_vars andalso null rel_tvars then [] + else [qty_str ^ "illegal schematic variable(s) in the relation."] + + val dup_vs = + (case duplicates (op =) vs of + [] => [] + | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups]) + + val extra_rty_tfrees = + (case subtract (op =) vs rty_tfreesT of + [] => [] + | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras]) + + val extra_rel_tfrees = + (case subtract (op =) vs rel_tfrees of + [] => [] + | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras]) + + val illegal_rel_frees = + (case rel_frees of + [] => [] + | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs]) + + val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees +in + if null errs then () else error (cat_lines errs) +end + +(* check for existence of map functions *) +fun map_check ctxt (_, (rty, _)) = +let + val thy = ProofContext.theory_of ctxt + + fun map_check_aux rty warns = + case rty of + Type (_, []) => warns + | Type (s, _) => if maps_defined thy s then warns else s::warns + | _ => warns + + val warns = map_check_aux rty [] +in + if null warns then () + else warning ("No map function defined for " ^ commas warns ^ + ". This will cause problems later on.") +end + + + +(*** interface and syntax setup ***) + + +(* the ML-interface takes a list of 5-tuples consisting of: + + - the name of the quotient type + - its free type variables (first argument) + - its mixfix annotation + - the type to be quotient + - the relation according to which the type is quotient + + it opens a proof-state in which one has to show that the + relations are equivalence relations +*) + +fun quotient_type quot_list lthy = +let + (* sanity check *) + val _ = List.app sanity_check quot_list + val _ = List.app (map_check lthy) quot_list + + fun mk_goal (rty, rel) = + let + val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} + in + HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel) + end + + val goals = map (mk_goal o snd) quot_list + + fun after_qed thms lthy = + fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd +in + theorem after_qed goals lthy +end + +fun quotient_type_cmd specs lthy = +let + fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy = + let + (* new parsing with proper declaration *) + val rty = Syntax.read_typ lthy rty_str + val lthy1 = Variable.declare_typ rty lthy + val pre_rel = Syntax.parse_term lthy1 rel_str + val pre_rel' = Syntax.type_constraint (rty --> rty --> @{typ bool}) pre_rel + val rel = Syntax.check_term lthy1 pre_rel' + val lthy2 = Variable.declare_term rel lthy1 + + (* old parsing *) + (* val rty = Syntax.read_typ lthy rty_str + val rel = Syntax.read_term lthy rel_str *) + in + (((vs, qty_name, mx), (rty, rel)), lthy2) + end + + val (spec', lthy') = fold_map parse_spec specs lthy +in + quotient_type spec' lthy' +end + +val quotspec_parser = + OuterParse.and_list1 + ((OuterParse.type_args -- OuterParse.binding) -- + OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- + (OuterParse.$$$ "/" |-- OuterParse.term)) + +val _ = OuterKeyword.keyword "/" + +val _ = + OuterSyntax.local_theory_to_proof "quotient_type" + "quotient type definitions (require equivalence proofs)" + OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) + +end; (* structure *)