Initial version of HOL quotient package.
--- a/src/HOL/IsaMakefile Fri Feb 19 09:35:18 2010 +0100
+++ b/src/HOL/IsaMakefile Fri Feb 19 13:54:19 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:
--- a/src/HOL/Library/Library.thy Fri Feb 19 09:35:18 2010 +0100
+++ b/src/HOL/Library/Library.thy Fri Feb 19 13:54:19 2010 +0100
@@ -45,6 +45,11 @@
Preorder
Product_Vector
Quicksort
+ Quotient_List
+ Quotient_Option
+ Quotient_Product
+ Quotient_Sum
+ Quotient_Syntax
Quotient_Type
Ramsey
Reflection
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quotient_List.thy Fri Feb 19 13:54:19 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 \<and> list_rel R xs ys)"
+
+declare [[map list = (map, list_rel)]]
+
+lemma split_list_all:
+ shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> 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 \<and> list_rel R s s \<and> (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 \<Longrightarrow> length b = 0"
+ by (induct b) (simp_all)
+
+lemma list_rel_len:
+ shows "list_rel R a b \<Longrightarrow> 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 \<longrightarrow> list_rel R2 xb yb \<longrightarrow> 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 \<longrightarrow> list_rel R1 xa ya \<longrightarrow> 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: "\<And>x y. R x y = (R x = R y)"
+ shows "list_rel R x x"
+ by (induct x) (auto simp add: a)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quotient_Option.thy Fri Feb 19 13:54:19 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 "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quotient_Product.thy Fri Feb 19 13:54:19 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 = (\<lambda>(a, b) (c, d). R1 a c \<and> 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quotient_Sum.thy Fri Feb 19 13:54:19 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 "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quotient_Syntax.thy Fri Feb 19 13:54:19 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
+(*>*)
--- a/src/HOL/Main.thy Fri Feb 19 09:35:18 2010 +0100
+++ b/src/HOL/Main.thy Fri Feb 19 13:54:19 2010 +0100
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Plain Predicate_Compile Nitpick
+imports Plain Predicate_Compile Nitpick Quotient
begin
text {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient.thy Fri Feb 19 13:54:19 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 \<equiv> \<forall>x y. E x y = (E x = E y)"
+
+definition
+ "reflp E \<equiv> \<forall>x. E x x"
+
+definition
+ "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
+
+definition
+ "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
+
+lemma equivp_reflp_symp_transp:
+ shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
+ unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
+ by blast
+
+lemma equivp_reflp:
+ shows "equivp E \<Longrightarrow> E x x"
+ by (simp only: equivp_reflp_symp_transp reflp_def)
+
+lemma equivp_symp:
+ shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
+ by (metis equivp_reflp_symp_transp symp_def)
+
+lemma equivp_transp:
+ shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> 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 \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (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 \<equiv> 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 \<equiv> R x x"
+
+lemma in_respects:
+ shows "(x \<in> 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 = (\<forall>x y. E1 x y \<longrightarrow> 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: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+ shows "(R1 ===> R2) f g"
+ using a by simp
+
+lemma fun_rel_id_asm:
+ assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
+ shows "A \<longrightarrow> (R1 ===> R2) f g"
+ using a by auto
+
+
+section {* Quotient Predicate *}
+
+definition
+ "Quotient E Abs Rep \<equiv>
+ (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
+ (\<forall>r s. E r s = (E r r \<and> E s s \<and> (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 \<and> E s s \<and> (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 \<Longrightarrow> 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 \<Longrightarrow> 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 "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
+ using q1 q2
+ unfolding Quotient_def
+ unfolding expand_fun_eq
+ by simp
+ moreover
+ have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
+ using q1 q2
+ unfolding Quotient_def
+ by (simp (no_asm)) (metis)
+ moreover
+ have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
+ (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) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>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) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>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 \<Rightarrow> '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 \<Rightarrow> 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 \<Rightarrow> 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: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
+ shows "All P \<longrightarrow> Ball R Q"
+ using a by (metis COMBC_def Collect_def Collect_mem_eq)
+
+lemma bex_reg_left:
+ assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
+ shows "Bex R Q \<longrightarrow> Ex P"
+ using a by (metis COMBC_def Collect_def Collect_mem_eq)
+
+lemma ball_reg_left:
+ assumes a: "equivp R"
+ shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
+ using a by (metis equivp_reflp in_respects)
+
+lemma bex_reg_right:
+ assumes a: "equivp R"
+ shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
+ using a by (metis equivp_reflp in_respects)
+
+lemma ball_reg_eqv_range:
+ fixes P::"'a \<Rightarrow> bool"
+ and x::"'a"
+ assumes a: "equivp R2"
+ shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
+ apply(rule iffI)
+ apply(rule allI)
+ apply(drule_tac x="\<lambda>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)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
+ apply(auto)
+ apply(rule_tac x="\<lambda>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 "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
+ shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
+ using assms by auto
+
+lemma bex_ex_comm:
+ assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)"
+ shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
+ using assms by auto
+
+section {* Bounded abstraction *}
+
+definition
+ Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+ "x \<in> p \<Longrightarrow> 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 \<in> Respects R1 \<and> y \<in> 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 \<in> 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 \<in> Respects R1 \<and> y \<in> 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 \<Longrightarrow> 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 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> 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 \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+where
+ "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
+
+lemma bex1_rel_aux:
+ "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> 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:
+ "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> 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 "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> 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: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>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 \<Rightarrow> 'a \<Rightarrow> bool"
+ and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+ and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+ assumes equivp: "equivp R"
+ and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+ and rep_inverse: "\<And>x. Abs (Rep x) = x"
+ and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+ and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
+begin
+
+definition
+ abs::"'a \<Rightarrow> 'b"
+where
+ "abs x \<equiv> Abs (R x)"
+
+definition
+ rep::"'b \<Rightarrow> '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 "\<dots> = Abs (R x)" using homeier_lem9 by simp
+ also have "\<dots> = Abs (Rep a)" using eq by simp
+ also have "\<dots> = 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 "\<dots> = ?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 \<equiv> True"
+
+lemma
+ shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
+ and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
+ and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
+ and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
+ and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
+ by (simp_all add: Quot_True_def ext)
+
+lemma QT_imp: "Quot_True a \<equiv> 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
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/LarryDatatype.thy Fri Feb 19 13:54:19 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 \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
+where
+ CD: "CRYPT K (DECRYPT K X) \<sim> X"
+| DC: "DECRYPT K (CRYPT K X) \<sim> X"
+| NONCE: "NONCE N \<sim> NONCE N"
+| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
+| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
+| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
+| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
+| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
+
+lemmas msgrel.intros[intro]
+
+text{*Proving that it is an equivalence relation*}
+
+lemma msgrel_refl: "X \<sim> 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 \<Rightarrow> nat set"
+where
+ "freenonces (NONCE N) = {N}"
+| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
+| "freenonces (CRYPT K X) = freenonces X"
+| "freenonces (DECRYPT K X) = freenonces X"
+
+theorem msgrel_imp_eq_freenonces:
+ assumes a: "U \<sim> 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 \<Rightarrow> 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 \<sim> freeleft U"
+ by (induct rule: freeleft.induct) (auto)
+
+theorem msgrel_imp_eqv_freeleft:
+ assumes a: "U \<sim> V"
+ shows "freeleft U \<sim> 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 \<Rightarrow> 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 \<sim> freeright U"
+ by (induct rule: freeright.induct) (auto)
+
+theorem msgrel_imp_eqv_freeright:
+ assumes a: "U \<sim> V"
+ shows "freeright U \<sim> 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 \<Rightarrow> 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 \<noteq> MPair X Y"}*}
+theorem msgrel_imp_eq_freediscrim:
+ assumes a: "U \<sim> 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 \<Rightarrow> msg"
+is
+ "NONCE"
+
+quotient_definition
+ "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "MPAIR"
+
+quotient_definition
+ "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "CRYPT"
+
+quotient_definition
+ "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "DECRYPT"
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
+by (auto intro: CRYPT)
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim> ===> op \<sim>) 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 \<Rightarrow> nat set"
+is
+ "freenonces"
+
+text{*Now prove the four equations for @{term nonces}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op =) freenonces freenonces"
+ by (simp add: msgrel_imp_eq_freenonces)
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim>) 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 \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
+ by (simp add: MPAIR)
+
+lemma nonces_MPair [simp]:
+ shows "nonces (MPair X Y) = nonces X \<union> 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 \<Rightarrow> msg"
+is
+ "freeleft"
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op \<sim>) 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 \<Rightarrow> msg"
+is
+ "freeright"
+
+text{*Now prove the four equations for @{term right}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> op \<sim>) 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 \<sim> NONCE n \<Longrightarrow> 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 \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> 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 \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
+ by (drule msgrel_imp_eqv_freeright) (simp)
+
+lemma MPair_imp_eq_right:
+ shows "MPair X Y = MPair X' Y' \<Longrightarrow> 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 "\<not>(NONCE m \<sim> MPAIR X Y)"
+ by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Nonce_neq_MPair [iff]:
+ shows "Nonce N \<noteq> MPair X Y"
+ by (lifting NONCE_neqv_MPAIR)
+
+text{*Example suggested by a referee*}
+
+lemma CRYPT_NONCE_neq_NONCE:
+ shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
+ by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Crypt_Nonce_neq_Nonce:
+ shows "Crypt K (Nonce M) \<noteq> Nonce N"
+ by (lifting CRYPT_NONCE_neq_NONCE)
+
+text{*...and many similar results*}
+lemma CRYPT2_NONCE_neq_NONCE:
+ shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
+ by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Crypt2_Nonce_neq_Nonce:
+ shows "Crypt K (Crypt K' (Nonce M)) \<noteq> 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 "\<lbrakk>\<And>N. P (Nonce N);
+ \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
+ \<And>K X. P X \<Longrightarrow> P (Crypt K X);
+ \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
+ by (lifting freemsg.induct)
+
+lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
+ assumes N: "\<And>N. P (Nonce N)"
+ and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
+ and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
+ and D: "\<And>K X. P X \<Longrightarrow> 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 \<Rightarrow> int"
+is
+ "freediscrim"
+
+text{*Now prove the four equations for @{term discrim}*}
+
+lemma [quot_respect]:
+ shows "(op \<sim> ===> 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
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/LarryInt.thy Fri Feb 19 13:54:19 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 \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+ "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient_type int = "nat \<times> 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 \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
+
+quotient_definition
+ "(op +) :: int \<Rightarrow> int \<Rightarrow> int"
+is
+ "add_raw"
+
+definition
+ "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
+
+quotient_definition
+ "uminus :: int \<Rightarrow> int"
+is
+ "uminus_raw"
+
+fun
+ mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
+where
+ "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+quotient_definition
+ "(op *) :: int \<Rightarrow> int \<Rightarrow> int"
+is
+ "mult_raw"
+
+definition
+ "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
+
+quotient_definition
+ le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
+is
+ "le_raw"
+
+definition
+ less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
+
+definition
+ diff_int_def: "z - (w::int) \<equiv> 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 "\<not>(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 \<noteq> (1::int)" by (lifting zero_not_one)
+qed
+
+
+subsection{*The @{text "\<le>"} 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 \<le> w"
+ by (lifting zle_refl_raw)
+
+
+lemma zle_trans_raw:
+ shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> 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 "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"
+ by (lifting zle_trans_raw)
+
+lemma zle_anti_sym_raw:
+ shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
+apply(cases z, cases w)
+apply(auto iff: le_raw_def)
+done
+
+lemma zle_anti_sym:
+ fixes z w::"int"
+ shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> 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 \<le> z & w \<noteq> 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 \<or> 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 \<le> w \<or> w \<le> 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 \<Longrightarrow> 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 \<le> j \<Longrightarrow> k + i \<le> k + j"
+ by (lifting zadd_left_mono_raw)
+
+
+subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
+
+definition
+ "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
+
+quotient_definition
+ "nat2::int \<Rightarrow> nat"
+is
+ "nat_raw"
+
+abbreviation
+ "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))"
+
+lemma nat_le_eq_zle_raw:
+ shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> 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 \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
+ unfolding less_int_def
+ by (lifting nat_le_eq_zle_raw)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/ROOT.ML Fri Feb 19 13:54:19 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"];
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Feb 19 13:54:19 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 *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Feb 19 13:54:19 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 *)
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Feb 19 13:54:19 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 *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Feb 19 13:54:19 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 *)
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Feb 19 13:54:19 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 *)