Initial version of HOL quotient package.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri Feb 19 13:54:19 2010 +0100 (2010-02-19)
changeset 352224f1fba00f66d
parent 35221 5cb63cb4213f
child 35229 d4ec25836a78
child 35234 7508302738ea
child 35507 d1c15bf767c0
Initial version of HOL quotient package.
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Library/Quotient_Syntax.thy
src/HOL/Main.thy
src/HOL/Quotient.thy
src/HOL/Quotient_Examples/LarryDatatype.thy
src/HOL/Quotient_Examples/LarryInt.thy
src/HOL/Quotient_Examples/ROOT.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/Quotient/quotient_typ.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Feb 19 09:35:18 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Feb 19 13:54:19 2010 +0100
     1.3 @@ -52,6 +52,7 @@
     1.4    HOL-Nominal-Examples \
     1.5    HOL-Number_Theory \
     1.6    HOL-Old_Number_Theory \
     1.7 +  HOL-Quotient_Examples \
     1.8    HOL-Probability \
     1.9    HOL-Prolog \
    1.10    HOL-Proofs-Extraction \
    1.11 @@ -265,6 +266,7 @@
    1.12    Presburger.thy \
    1.13    Predicate_Compile.thy \
    1.14    Quickcheck.thy \
    1.15 +  Quotient.thy \
    1.16    Random.thy \
    1.17    Random_Sequence.thy \
    1.18    Recdef.thy \
    1.19 @@ -307,6 +309,11 @@
    1.20    Tools/Qelim/generated_cooper.ML \
    1.21    Tools/Qelim/presburger.ML \
    1.22    Tools/Qelim/qelim.ML \
    1.23 +  Tools/Quotient/quotient_def.ML \
    1.24 +  Tools/Quotient/quotient_info.ML \
    1.25 +  Tools/Quotient/quotient_tacs.ML \
    1.26 +  Tools/Quotient/quotient_term.ML \
    1.27 +  Tools/Quotient/quotient_typ.ML \
    1.28    Tools/recdef.ML \
    1.29    Tools/res_atp.ML \
    1.30    Tools/res_axioms.ML \
    1.31 @@ -407,7 +414,10 @@
    1.32    Library/Diagonalize.thy Library/RBT.thy Library/Univ_Poly.thy		\
    1.33    Library/Poly_Deriv.thy Library/Polynomial.thy Library/Preorder.thy	\
    1.34    Library/Product_plus.thy Library/Product_Vector.thy Library/Tree.thy	\
    1.35 -  Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML		\
    1.36 +  Library/Enum.thy Library/Float.thy Library/Quotient_List.thy          \
    1.37 +  Library/Quotient_Option.thy Library/Quotient_Product.thy              \
    1.38 +  Library/Quotient_Sum.thy Library/Quotient_Syntax.thy                  \
    1.39 +  $(SRC)/Tools/float.ML                                                 \
    1.40    $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML		\
    1.41    Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy	\
    1.42    Library/OptionalSugar.thy Library/SML_Quickcheck.thy
    1.43 @@ -1273,6 +1283,15 @@
    1.44  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle
    1.45  
    1.46  
    1.47 +## HOL-Quotient_Examples
    1.48 +
    1.49 +HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
    1.50 +
    1.51 +$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL	      			\
    1.52 +  Quotient_Examples/LarryInt.thy Quotient_Examples/LarryDatatype.thy
    1.53 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
    1.54 +
    1.55 +
    1.56  ## clean
    1.57  
    1.58  clean:
     2.1 --- a/src/HOL/Library/Library.thy	Fri Feb 19 09:35:18 2010 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Fri Feb 19 13:54:19 2010 +0100
     2.3 @@ -45,6 +45,11 @@
     2.4    Preorder
     2.5    Product_Vector
     2.6    Quicksort
     2.7 +  Quotient_List
     2.8 +  Quotient_Option
     2.9 +  Quotient_Product
    2.10 +  Quotient_Sum
    2.11 +  Quotient_Syntax
    2.12    Quotient_Type
    2.13    Ramsey
    2.14    Reflection
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Quotient_List.thy	Fri Feb 19 13:54:19 2010 +0100
     3.3 @@ -0,0 +1,232 @@
     3.4 +(*  Title:      Quotient_List.thy
     3.5 +    Author:     Cezary Kaliszyk and Christian Urban
     3.6 +*)
     3.7 +theory Quotient_List
     3.8 +imports Main Quotient_Syntax
     3.9 +begin
    3.10 +
    3.11 +section {* Quotient infrastructure for the list type. *}
    3.12 +
    3.13 +fun
    3.14 +  list_rel
    3.15 +where
    3.16 +  "list_rel R [] [] = True"
    3.17 +| "list_rel R (x#xs) [] = False"
    3.18 +| "list_rel R [] (x#xs) = False"
    3.19 +| "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)"
    3.20 +
    3.21 +declare [[map list = (map, list_rel)]]
    3.22 +
    3.23 +lemma split_list_all:
    3.24 +  shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
    3.25 +  apply(auto)
    3.26 +  apply(case_tac x)
    3.27 +  apply(simp_all)
    3.28 +  done
    3.29 +
    3.30 +lemma map_id[id_simps]:
    3.31 +  shows "map id = id"
    3.32 +  apply(simp add: expand_fun_eq)
    3.33 +  apply(rule allI)
    3.34 +  apply(induct_tac x)
    3.35 +  apply(simp_all)
    3.36 +  done
    3.37 +
    3.38 +
    3.39 +lemma list_rel_reflp:
    3.40 +  shows "equivp R \<Longrightarrow> list_rel R xs xs"
    3.41 +  apply(induct xs)
    3.42 +  apply(simp_all add: equivp_reflp)
    3.43 +  done
    3.44 +
    3.45 +lemma list_rel_symp:
    3.46 +  assumes a: "equivp R"
    3.47 +  shows "list_rel R xs ys \<Longrightarrow> list_rel R ys xs"
    3.48 +  apply(induct xs ys rule: list_induct2')
    3.49 +  apply(simp_all)
    3.50 +  apply(rule equivp_symp[OF a])
    3.51 +  apply(simp)
    3.52 +  done
    3.53 +
    3.54 +lemma list_rel_transp:
    3.55 +  assumes a: "equivp R"
    3.56 +  shows "list_rel R xs1 xs2 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> list_rel R xs1 xs3"
    3.57 +  apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2')
    3.58 +  apply(simp_all)
    3.59 +  apply(case_tac xs3)
    3.60 +  apply(simp_all)
    3.61 +  apply(rule equivp_transp[OF a])
    3.62 +  apply(auto)
    3.63 +  done
    3.64 +
    3.65 +lemma list_equivp[quot_equiv]:
    3.66 +  assumes a: "equivp R"
    3.67 +  shows "equivp (list_rel R)"
    3.68 +  apply(rule equivpI)
    3.69 +  unfolding reflp_def symp_def transp_def
    3.70 +  apply(subst split_list_all)
    3.71 +  apply(simp add: equivp_reflp[OF a] list_rel_reflp[OF a])
    3.72 +  apply(blast intro: list_rel_symp[OF a])
    3.73 +  apply(blast intro: list_rel_transp[OF a])
    3.74 +  done
    3.75 +
    3.76 +lemma list_rel_rel:
    3.77 +  assumes q: "Quotient R Abs Rep"
    3.78 +  shows "list_rel R r s = (list_rel R r r \<and> list_rel R s s \<and> (map Abs r = map Abs s))"
    3.79 +  apply(induct r s rule: list_induct2')
    3.80 +  apply(simp_all)
    3.81 +  using Quotient_rel[OF q]
    3.82 +  apply(metis)
    3.83 +  done
    3.84 +
    3.85 +lemma list_quotient[quot_thm]:
    3.86 +  assumes q: "Quotient R Abs Rep"
    3.87 +  shows "Quotient (list_rel R) (map Abs) (map Rep)"
    3.88 +  unfolding Quotient_def
    3.89 +  apply(subst split_list_all)
    3.90 +  apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id)
    3.91 +  apply(rule conjI)
    3.92 +  apply(rule allI)
    3.93 +  apply(induct_tac a)
    3.94 +  apply(simp)
    3.95 +  apply(simp)
    3.96 +  apply(simp add: Quotient_rep_reflp[OF q])
    3.97 +  apply(rule allI)+
    3.98 +  apply(rule list_rel_rel[OF q])
    3.99 +  done
   3.100 +
   3.101 +
   3.102 +lemma cons_prs_aux:
   3.103 +  assumes q: "Quotient R Abs Rep"
   3.104 +  shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
   3.105 +  by (induct t) (simp_all add: Quotient_abs_rep[OF q])
   3.106 +
   3.107 +lemma cons_prs[quot_preserve]:
   3.108 +  assumes q: "Quotient R Abs Rep"
   3.109 +  shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
   3.110 +  by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q])
   3.111 +     (simp)
   3.112 +
   3.113 +lemma cons_rsp[quot_respect]:
   3.114 +  assumes q: "Quotient R Abs Rep"
   3.115 +  shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)"
   3.116 +  by (auto)
   3.117 +
   3.118 +lemma nil_prs[quot_preserve]:
   3.119 +  assumes q: "Quotient R Abs Rep"
   3.120 +  shows "map Abs [] = []"
   3.121 +  by simp
   3.122 +
   3.123 +lemma nil_rsp[quot_respect]:
   3.124 +  assumes q: "Quotient R Abs Rep"
   3.125 +  shows "list_rel R [] []"
   3.126 +  by simp
   3.127 +
   3.128 +lemma map_prs_aux:
   3.129 +  assumes a: "Quotient R1 abs1 rep1"
   3.130 +  and     b: "Quotient R2 abs2 rep2"
   3.131 +  shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
   3.132 +  by (induct l)
   3.133 +     (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
   3.134 +
   3.135 +
   3.136 +lemma map_prs[quot_preserve]:
   3.137 +  assumes a: "Quotient R1 abs1 rep1"
   3.138 +  and     b: "Quotient R2 abs2 rep2"
   3.139 +  shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
   3.140 +  by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
   3.141 +     (simp)
   3.142 +
   3.143 +
   3.144 +lemma map_rsp[quot_respect]:
   3.145 +  assumes q1: "Quotient R1 Abs1 Rep1"
   3.146 +  and     q2: "Quotient R2 Abs2 Rep2"
   3.147 +  shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"
   3.148 +  apply(simp)
   3.149 +  apply(rule allI)+
   3.150 +  apply(rule impI)
   3.151 +  apply(rule allI)+
   3.152 +  apply (induct_tac xa ya rule: list_induct2')
   3.153 +  apply simp_all
   3.154 +  done
   3.155 +
   3.156 +lemma foldr_prs_aux:
   3.157 +  assumes a: "Quotient R1 abs1 rep1"
   3.158 +  and     b: "Quotient R2 abs2 rep2"
   3.159 +  shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
   3.160 +  by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
   3.161 +
   3.162 +lemma foldr_prs[quot_preserve]:
   3.163 +  assumes a: "Quotient R1 abs1 rep1"
   3.164 +  and     b: "Quotient R2 abs2 rep2"
   3.165 +  shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
   3.166 +  by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b])
   3.167 +     (simp)
   3.168 +
   3.169 +lemma foldl_prs_aux:
   3.170 +  assumes a: "Quotient R1 abs1 rep1"
   3.171 +  and     b: "Quotient R2 abs2 rep2"
   3.172 +  shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
   3.173 +  by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
   3.174 +
   3.175 +
   3.176 +lemma foldl_prs[quot_preserve]:
   3.177 +  assumes a: "Quotient R1 abs1 rep1"
   3.178 +  and     b: "Quotient R2 abs2 rep2"
   3.179 +  shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
   3.180 +  by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b])
   3.181 +     (simp)
   3.182 +
   3.183 +lemma list_rel_empty:
   3.184 +  shows "list_rel R [] b \<Longrightarrow> length b = 0"
   3.185 +  by (induct b) (simp_all)
   3.186 +
   3.187 +lemma list_rel_len:
   3.188 +  shows "list_rel R a b \<Longrightarrow> length a = length b"
   3.189 +  apply (induct a arbitrary: b)
   3.190 +  apply (simp add: list_rel_empty)
   3.191 +  apply (case_tac b)
   3.192 +  apply simp_all
   3.193 +  done
   3.194 +
   3.195 +(* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
   3.196 +lemma foldl_rsp[quot_respect]:
   3.197 +  assumes q1: "Quotient R1 Abs1 Rep1"
   3.198 +  and     q2: "Quotient R2 Abs2 Rep2"
   3.199 +  shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"
   3.200 +  apply(auto)
   3.201 +  apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
   3.202 +  apply simp
   3.203 +  apply (rule_tac x="xa" in spec)
   3.204 +  apply (rule_tac x="ya" in spec)
   3.205 +  apply (rule_tac xs="xb" and ys="yb" in list_induct2)
   3.206 +  apply (rule list_rel_len)
   3.207 +  apply (simp_all)
   3.208 +  done
   3.209 +
   3.210 +lemma foldr_rsp[quot_respect]:
   3.211 +  assumes q1: "Quotient R1 Abs1 Rep1"
   3.212 +  and     q2: "Quotient R2 Abs2 Rep2"
   3.213 +  shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr"
   3.214 +  apply auto
   3.215 +  apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)")
   3.216 +  apply simp
   3.217 +  apply (rule_tac xs="xa" and ys="ya" in list_induct2)
   3.218 +  apply (rule list_rel_len)
   3.219 +  apply (simp_all)
   3.220 +  done
   3.221 +
   3.222 +lemma list_rel_eq[id_simps]:
   3.223 +  shows "(list_rel (op =)) = (op =)"
   3.224 +  unfolding expand_fun_eq
   3.225 +  apply(rule allI)+
   3.226 +  apply(induct_tac x xa rule: list_induct2')
   3.227 +  apply(simp_all)
   3.228 +  done
   3.229 +
   3.230 +lemma list_rel_refl:
   3.231 +  assumes a: "\<And>x y. R x y = (R x = R y)"
   3.232 +  shows "list_rel R x x"
   3.233 +  by (induct x) (auto simp add: a)
   3.234 +
   3.235 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Quotient_Option.thy	Fri Feb 19 13:54:19 2010 +0100
     4.3 @@ -0,0 +1,80 @@
     4.4 +(*  Title:      Quotient_Option.thy
     4.5 +    Author:     Cezary Kaliszyk and Christian Urban
     4.6 +*)
     4.7 +theory Quotient_Option
     4.8 +imports Main Quotient_Syntax
     4.9 +begin
    4.10 +
    4.11 +section {* Quotient infrastructure for the option type. *}
    4.12 +
    4.13 +fun
    4.14 +  option_rel
    4.15 +where
    4.16 +  "option_rel R None None = True"
    4.17 +| "option_rel R (Some x) None = False"
    4.18 +| "option_rel R None (Some x) = False"
    4.19 +| "option_rel R (Some x) (Some y) = R x y"
    4.20 +
    4.21 +declare [[map option = (Option.map, option_rel)]]
    4.22 +
    4.23 +text {* should probably be in Option.thy *}
    4.24 +lemma split_option_all:
    4.25 +  shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
    4.26 +  apply(auto)
    4.27 +  apply(case_tac x)
    4.28 +  apply(simp_all)
    4.29 +  done
    4.30 +
    4.31 +lemma option_quotient[quot_thm]:
    4.32 +  assumes q: "Quotient R Abs Rep"
    4.33 +  shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
    4.34 +  unfolding Quotient_def
    4.35 +  apply(simp add: split_option_all)
    4.36 +  apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
    4.37 +  using q
    4.38 +  unfolding Quotient_def
    4.39 +  apply(blast)
    4.40 +  done
    4.41 +
    4.42 +lemma option_equivp[quot_equiv]:
    4.43 +  assumes a: "equivp R"
    4.44 +  shows "equivp (option_rel R)"
    4.45 +  apply(rule equivpI)
    4.46 +  unfolding reflp_def symp_def transp_def
    4.47 +  apply(simp_all add: split_option_all)
    4.48 +  apply(blast intro: equivp_reflp[OF a])
    4.49 +  apply(blast intro: equivp_symp[OF a])
    4.50 +  apply(blast intro: equivp_transp[OF a])
    4.51 +  done
    4.52 +
    4.53 +lemma option_None_rsp[quot_respect]:
    4.54 +  assumes q: "Quotient R Abs Rep"
    4.55 +  shows "option_rel R None None"
    4.56 +  by simp
    4.57 +
    4.58 +lemma option_Some_rsp[quot_respect]:
    4.59 +  assumes q: "Quotient R Abs Rep"
    4.60 +  shows "(R ===> option_rel R) Some Some"
    4.61 +  by simp
    4.62 +
    4.63 +lemma option_None_prs[quot_preserve]:
    4.64 +  assumes q: "Quotient R Abs Rep"
    4.65 +  shows "Option.map Abs None = None"
    4.66 +  by simp
    4.67 +
    4.68 +lemma option_Some_prs[quot_preserve]:
    4.69 +  assumes q: "Quotient R Abs Rep"
    4.70 +  shows "(Rep ---> Option.map Abs) Some = Some"
    4.71 +  apply(simp add: expand_fun_eq)
    4.72 +  apply(simp add: Quotient_abs_rep[OF q])
    4.73 +  done
    4.74 +
    4.75 +lemma option_map_id[id_simps]:
    4.76 +  shows "Option.map id = id"
    4.77 +  by (simp add: expand_fun_eq split_option_all)
    4.78 +
    4.79 +lemma option_rel_eq[id_simps]:
    4.80 +  shows "option_rel (op =) = (op =)"
    4.81 +  by (simp add: expand_fun_eq split_option_all)
    4.82 +
    4.83 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Feb 19 13:54:19 2010 +0100
     5.3 @@ -0,0 +1,104 @@
     5.4 +(*  Title:      Quotient_Product.thy
     5.5 +    Author:     Cezary Kaliszyk and Christian Urban
     5.6 +*)
     5.7 +theory Quotient_Product
     5.8 +imports Main Quotient_Syntax
     5.9 +begin
    5.10 +
    5.11 +section {* Quotient infrastructure for the product type. *}
    5.12 +
    5.13 +fun
    5.14 +  prod_rel
    5.15 +where
    5.16 +  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
    5.17 +
    5.18 +declare [[map * = (prod_fun, prod_rel)]]
    5.19 +
    5.20 +
    5.21 +lemma prod_equivp[quot_equiv]:
    5.22 +  assumes a: "equivp R1"
    5.23 +  assumes b: "equivp R2"
    5.24 +  shows "equivp (prod_rel R1 R2)"
    5.25 +  apply(rule equivpI)
    5.26 +  unfolding reflp_def symp_def transp_def
    5.27 +  apply(simp_all add: split_paired_all)
    5.28 +  apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
    5.29 +  apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
    5.30 +  apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
    5.31 +  done
    5.32 +
    5.33 +lemma prod_quotient[quot_thm]:
    5.34 +  assumes q1: "Quotient R1 Abs1 Rep1"
    5.35 +  assumes q2: "Quotient R2 Abs2 Rep2"
    5.36 +  shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
    5.37 +  unfolding Quotient_def
    5.38 +  apply(simp add: split_paired_all)
    5.39 +  apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
    5.40 +  apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
    5.41 +  using q1 q2
    5.42 +  unfolding Quotient_def
    5.43 +  apply(blast)
    5.44 +  done
    5.45 +
    5.46 +lemma Pair_rsp[quot_respect]:
    5.47 +  assumes q1: "Quotient R1 Abs1 Rep1"
    5.48 +  assumes q2: "Quotient R2 Abs2 Rep2"
    5.49 +  shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
    5.50 +  by simp
    5.51 +
    5.52 +lemma Pair_prs[quot_preserve]:
    5.53 +  assumes q1: "Quotient R1 Abs1 Rep1"
    5.54 +  assumes q2: "Quotient R2 Abs2 Rep2"
    5.55 +  shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
    5.56 +  apply(simp add: expand_fun_eq)
    5.57 +  apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    5.58 +  done
    5.59 +
    5.60 +lemma fst_rsp[quot_respect]:
    5.61 +  assumes "Quotient R1 Abs1 Rep1"
    5.62 +  assumes "Quotient R2 Abs2 Rep2"
    5.63 +  shows "(prod_rel R1 R2 ===> R1) fst fst"
    5.64 +  by simp
    5.65 +
    5.66 +lemma fst_prs[quot_preserve]:
    5.67 +  assumes q1: "Quotient R1 Abs1 Rep1"
    5.68 +  assumes q2: "Quotient R2 Abs2 Rep2"
    5.69 +  shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
    5.70 +  apply(simp add: expand_fun_eq)
    5.71 +  apply(simp add: Quotient_abs_rep[OF q1])
    5.72 +  done
    5.73 +
    5.74 +lemma snd_rsp[quot_respect]:
    5.75 +  assumes "Quotient R1 Abs1 Rep1"
    5.76 +  assumes "Quotient R2 Abs2 Rep2"
    5.77 +  shows "(prod_rel R1 R2 ===> R2) snd snd"
    5.78 +  by simp
    5.79 +
    5.80 +lemma snd_prs[quot_preserve]:
    5.81 +  assumes q1: "Quotient R1 Abs1 Rep1"
    5.82 +  assumes q2: "Quotient R2 Abs2 Rep2"
    5.83 +  shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
    5.84 +  apply(simp add: expand_fun_eq)
    5.85 +  apply(simp add: Quotient_abs_rep[OF q2])
    5.86 +  done
    5.87 +
    5.88 +lemma split_rsp[quot_respect]:
    5.89 +  shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
    5.90 +  by auto
    5.91 +
    5.92 +lemma split_prs[quot_preserve]:
    5.93 +  assumes q1: "Quotient R1 Abs1 Rep1"
    5.94 +  and     q2: "Quotient R2 Abs2 Rep2"
    5.95 +  shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
    5.96 +  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    5.97 +
    5.98 +lemma prod_fun_id[id_simps]:
    5.99 +  shows "prod_fun id id = id"
   5.100 +  by (simp add: prod_fun_def)
   5.101 +
   5.102 +lemma prod_rel_eq[id_simps]:
   5.103 +  shows "prod_rel (op =) (op =) = (op =)"
   5.104 +  by (simp add: expand_fun_eq)
   5.105 +
   5.106 +
   5.107 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Feb 19 13:54:19 2010 +0100
     6.3 @@ -0,0 +1,96 @@
     6.4 +(*  Title:      Quotient_Sum.thy
     6.5 +    Author:     Cezary Kaliszyk and Christian Urban
     6.6 +*)
     6.7 +theory Quotient_Sum
     6.8 +imports Main Quotient_Syntax
     6.9 +begin
    6.10 +
    6.11 +section {* Quotient infrastructure for the sum type. *}
    6.12 +
    6.13 +fun
    6.14 +  sum_rel
    6.15 +where
    6.16 +  "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    6.17 +| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
    6.18 +| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    6.19 +| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    6.20 +
    6.21 +fun
    6.22 +  sum_map
    6.23 +where
    6.24 +  "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    6.25 +| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    6.26 +
    6.27 +declare [[map "+" = (sum_map, sum_rel)]]
    6.28 +
    6.29 +
    6.30 +text {* should probably be in Sum_Type.thy *}
    6.31 +lemma split_sum_all:
    6.32 +  shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
    6.33 +  apply(auto)
    6.34 +  apply(case_tac x)
    6.35 +  apply(simp_all)
    6.36 +  done
    6.37 +
    6.38 +lemma sum_equivp[quot_equiv]:
    6.39 +  assumes a: "equivp R1"
    6.40 +  assumes b: "equivp R2"
    6.41 +  shows "equivp (sum_rel R1 R2)"
    6.42 +  apply(rule equivpI)
    6.43 +  unfolding reflp_def symp_def transp_def
    6.44 +  apply(simp_all add: split_sum_all)
    6.45 +  apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
    6.46 +  apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
    6.47 +  apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
    6.48 +  done
    6.49 +
    6.50 +lemma sum_quotient[quot_thm]:
    6.51 +  assumes q1: "Quotient R1 Abs1 Rep1"
    6.52 +  assumes q2: "Quotient R2 Abs2 Rep2"
    6.53 +  shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
    6.54 +  unfolding Quotient_def
    6.55 +  apply(simp add: split_sum_all)
    6.56 +  apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
    6.57 +  apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
    6.58 +  using q1 q2
    6.59 +  unfolding Quotient_def
    6.60 +  apply(blast)+
    6.61 +  done
    6.62 +
    6.63 +lemma sum_Inl_rsp[quot_respect]:
    6.64 +  assumes q1: "Quotient R1 Abs1 Rep1"
    6.65 +  assumes q2: "Quotient R2 Abs2 Rep2"
    6.66 +  shows "(R1 ===> sum_rel R1 R2) Inl Inl"
    6.67 +  by simp
    6.68 +
    6.69 +lemma sum_Inr_rsp[quot_respect]:
    6.70 +  assumes q1: "Quotient R1 Abs1 Rep1"
    6.71 +  assumes q2: "Quotient R2 Abs2 Rep2"
    6.72 +  shows "(R2 ===> sum_rel R1 R2) Inr Inr"
    6.73 +  by simp
    6.74 +
    6.75 +lemma sum_Inl_prs[quot_preserve]:
    6.76 +  assumes q1: "Quotient R1 Abs1 Rep1"
    6.77 +  assumes q2: "Quotient R2 Abs2 Rep2"
    6.78 +  shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
    6.79 +  apply(simp add: expand_fun_eq)
    6.80 +  apply(simp add: Quotient_abs_rep[OF q1])
    6.81 +  done
    6.82 +
    6.83 +lemma sum_Inr_prs[quot_preserve]:
    6.84 +  assumes q1: "Quotient R1 Abs1 Rep1"
    6.85 +  assumes q2: "Quotient R2 Abs2 Rep2"
    6.86 +  shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
    6.87 +  apply(simp add: expand_fun_eq)
    6.88 +  apply(simp add: Quotient_abs_rep[OF q2])
    6.89 +  done
    6.90 +
    6.91 +lemma sum_map_id[id_simps]:
    6.92 +  shows "sum_map id id = id"
    6.93 +  by (simp add: expand_fun_eq split_sum_all)
    6.94 +
    6.95 +lemma sum_rel_eq[id_simps]:
    6.96 +  shows "sum_rel (op =) (op =) = (op =)"
    6.97 +  by (simp add: expand_fun_eq split_sum_all)
    6.98 +
    6.99 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Library/Quotient_Syntax.thy	Fri Feb 19 13:54:19 2010 +0100
     7.3 @@ -0,0 +1,18 @@
     7.4 +(*  Title:      Quotient_Syntax.thy
     7.5 +    Author:     Cezary Kaliszyk and Christian Urban
     7.6 +*)
     7.7 +
     7.8 +header {* Pretty syntax for Quotient operations *}
     7.9 +
    7.10 +(*<*)
    7.11 +theory Quotient_Syntax
    7.12 +imports Main
    7.13 +begin
    7.14 +
    7.15 +notation
    7.16 +  rel_conj (infixr "OOO" 75) and
    7.17 +  fun_map (infixr "--->" 55) and
    7.18 +  fun_rel (infixr "===>" 55)
    7.19 +
    7.20 +end
    7.21 +(*>*)
     8.1 --- a/src/HOL/Main.thy	Fri Feb 19 09:35:18 2010 +0100
     8.2 +++ b/src/HOL/Main.thy	Fri Feb 19 13:54:19 2010 +0100
     8.3 @@ -1,7 +1,7 @@
     8.4  header {* Main HOL *}
     8.5  
     8.6  theory Main
     8.7 -imports Plain Predicate_Compile Nitpick
     8.8 +imports Plain Predicate_Compile Nitpick Quotient
     8.9  begin
    8.10  
    8.11  text {*
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Quotient.thy	Fri Feb 19 13:54:19 2010 +0100
     9.3 @@ -0,0 +1,797 @@
     9.4 +(*  Title:      Quotient.thy
     9.5 +    Author:     Cezary Kaliszyk and Christian Urban
     9.6 +*)
     9.7 +
     9.8 +theory Quotient
     9.9 +imports Plain ATP_Linkup
    9.10 +uses
    9.11 +  ("~~/src/HOL/Tools/Quotient/quotient_info.ML")
    9.12 +  ("~~/src/HOL/Tools/Quotient/quotient_typ.ML")
    9.13 +  ("~~/src/HOL/Tools/Quotient/quotient_def.ML")
    9.14 +  ("~~/src/HOL/Tools/Quotient/quotient_term.ML")
    9.15 +  ("~~/src/HOL/Tools/Quotient/quotient_tacs.ML")
    9.16 +begin
    9.17 +
    9.18 +
    9.19 +text {*
    9.20 +  Basic definition for equivalence relations
    9.21 +  that are represented by predicates.
    9.22 +*}
    9.23 +
    9.24 +definition
    9.25 +  "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
    9.26 +
    9.27 +definition
    9.28 +  "reflp E \<equiv> \<forall>x. E x x"
    9.29 +
    9.30 +definition
    9.31 +  "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
    9.32 +
    9.33 +definition
    9.34 +  "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
    9.35 +
    9.36 +lemma equivp_reflp_symp_transp:
    9.37 +  shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
    9.38 +  unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
    9.39 +  by blast
    9.40 +
    9.41 +lemma equivp_reflp:
    9.42 +  shows "equivp E \<Longrightarrow> E x x"
    9.43 +  by (simp only: equivp_reflp_symp_transp reflp_def)
    9.44 +
    9.45 +lemma equivp_symp:
    9.46 +  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
    9.47 +  by (metis equivp_reflp_symp_transp symp_def)
    9.48 +
    9.49 +lemma equivp_transp:
    9.50 +  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
    9.51 +  by (metis equivp_reflp_symp_transp transp_def)
    9.52 +
    9.53 +lemma equivpI:
    9.54 +  assumes "reflp R" "symp R" "transp R"
    9.55 +  shows "equivp R"
    9.56 +  using assms by (simp add: equivp_reflp_symp_transp)
    9.57 +
    9.58 +lemma identity_equivp:
    9.59 +  shows "equivp (op =)"
    9.60 +  unfolding equivp_def
    9.61 +  by auto
    9.62 +
    9.63 +text {* Partial equivalences: not yet used anywhere *}
    9.64 +
    9.65 +definition
    9.66 +  "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)))"
    9.67 +
    9.68 +lemma equivp_implies_part_equivp:
    9.69 +  assumes a: "equivp E"
    9.70 +  shows "part_equivp E"
    9.71 +  using a
    9.72 +  unfolding equivp_def part_equivp_def
    9.73 +  by auto
    9.74 +
    9.75 +text {* Composition of Relations *}
    9.76 +
    9.77 +abbreviation
    9.78 +  rel_conj (infixr "OOO" 75)
    9.79 +where
    9.80 +  "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
    9.81 +
    9.82 +lemma eq_comp_r:
    9.83 +  shows "((op =) OOO R) = R"
    9.84 +  by (auto simp add: expand_fun_eq)
    9.85 +
    9.86 +section {* Respects predicate *}
    9.87 +
    9.88 +definition
    9.89 +  Respects
    9.90 +where
    9.91 +  "Respects R x \<equiv> R x x"
    9.92 +
    9.93 +lemma in_respects:
    9.94 +  shows "(x \<in> Respects R) = R x x"
    9.95 +  unfolding mem_def Respects_def
    9.96 +  by simp
    9.97 +
    9.98 +section {* Function map and function relation *}
    9.99 +
   9.100 +definition
   9.101 +  fun_map (infixr "--->" 55)
   9.102 +where
   9.103 +[simp]: "fun_map f g h x = g (h (f x))"
   9.104 +
   9.105 +definition
   9.106 +  fun_rel (infixr "===>" 55)
   9.107 +where
   9.108 +[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
   9.109 +
   9.110 +
   9.111 +lemma fun_map_id:
   9.112 +  shows "(id ---> id) = id"
   9.113 +  by (simp add: expand_fun_eq id_def)
   9.114 +
   9.115 +lemma fun_rel_eq:
   9.116 +  shows "((op =) ===> (op =)) = (op =)"
   9.117 +  by (simp add: expand_fun_eq)
   9.118 +
   9.119 +lemma fun_rel_id:
   9.120 +  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   9.121 +  shows "(R1 ===> R2) f g"
   9.122 +  using a by simp
   9.123 +
   9.124 +lemma fun_rel_id_asm:
   9.125 +  assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
   9.126 +  shows "A \<longrightarrow> (R1 ===> R2) f g"
   9.127 +  using a by auto
   9.128 +
   9.129 +
   9.130 +section {* Quotient Predicate *}
   9.131 +
   9.132 +definition
   9.133 +  "Quotient E Abs Rep \<equiv>
   9.134 +     (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
   9.135 +     (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
   9.136 +
   9.137 +lemma Quotient_abs_rep:
   9.138 +  assumes a: "Quotient E Abs Rep"
   9.139 +  shows "Abs (Rep a) = a"
   9.140 +  using a
   9.141 +  unfolding Quotient_def
   9.142 +  by simp
   9.143 +
   9.144 +lemma Quotient_rep_reflp:
   9.145 +  assumes a: "Quotient E Abs Rep"
   9.146 +  shows "E (Rep a) (Rep a)"
   9.147 +  using a
   9.148 +  unfolding Quotient_def
   9.149 +  by blast
   9.150 +
   9.151 +lemma Quotient_rel:
   9.152 +  assumes a: "Quotient E Abs Rep"
   9.153 +  shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
   9.154 +  using a
   9.155 +  unfolding Quotient_def
   9.156 +  by blast
   9.157 +
   9.158 +lemma Quotient_rel_rep:
   9.159 +  assumes a: "Quotient R Abs Rep"
   9.160 +  shows "R (Rep a) (Rep b) = (a = b)"
   9.161 +  using a
   9.162 +  unfolding Quotient_def
   9.163 +  by metis
   9.164 +
   9.165 +lemma Quotient_rep_abs:
   9.166 +  assumes a: "Quotient R Abs Rep"
   9.167 +  shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
   9.168 +  using a unfolding Quotient_def
   9.169 +  by blast
   9.170 +
   9.171 +lemma Quotient_rel_abs:
   9.172 +  assumes a: "Quotient E Abs Rep"
   9.173 +  shows "E r s \<Longrightarrow> Abs r = Abs s"
   9.174 +  using a unfolding Quotient_def
   9.175 +  by blast
   9.176 +
   9.177 +lemma Quotient_symp:
   9.178 +  assumes a: "Quotient E Abs Rep"
   9.179 +  shows "symp E"
   9.180 +  using a unfolding Quotient_def symp_def
   9.181 +  by metis
   9.182 +
   9.183 +lemma Quotient_transp:
   9.184 +  assumes a: "Quotient E Abs Rep"
   9.185 +  shows "transp E"
   9.186 +  using a unfolding Quotient_def transp_def
   9.187 +  by metis
   9.188 +
   9.189 +lemma identity_quotient:
   9.190 +  shows "Quotient (op =) id id"
   9.191 +  unfolding Quotient_def id_def
   9.192 +  by blast
   9.193 +
   9.194 +lemma fun_quotient:
   9.195 +  assumes q1: "Quotient R1 abs1 rep1"
   9.196 +  and     q2: "Quotient R2 abs2 rep2"
   9.197 +  shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
   9.198 +proof -
   9.199 +  have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
   9.200 +    using q1 q2
   9.201 +    unfolding Quotient_def
   9.202 +    unfolding expand_fun_eq
   9.203 +    by simp
   9.204 +  moreover
   9.205 +  have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
   9.206 +    using q1 q2
   9.207 +    unfolding Quotient_def
   9.208 +    by (simp (no_asm)) (metis)
   9.209 +  moreover
   9.210 +  have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
   9.211 +        (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
   9.212 +    unfolding expand_fun_eq
   9.213 +    apply(auto)
   9.214 +    using q1 q2 unfolding Quotient_def
   9.215 +    apply(metis)
   9.216 +    using q1 q2 unfolding Quotient_def
   9.217 +    apply(metis)
   9.218 +    using q1 q2 unfolding Quotient_def
   9.219 +    apply(metis)
   9.220 +    using q1 q2 unfolding Quotient_def
   9.221 +    apply(metis)
   9.222 +    done
   9.223 +  ultimately
   9.224 +  show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
   9.225 +    unfolding Quotient_def by blast
   9.226 +qed
   9.227 +
   9.228 +lemma abs_o_rep:
   9.229 +  assumes a: "Quotient R Abs Rep"
   9.230 +  shows "Abs o Rep = id"
   9.231 +  unfolding expand_fun_eq
   9.232 +  by (simp add: Quotient_abs_rep[OF a])
   9.233 +
   9.234 +lemma equals_rsp:
   9.235 +  assumes q: "Quotient R Abs Rep"
   9.236 +  and     a: "R xa xb" "R ya yb"
   9.237 +  shows "R xa ya = R xb yb"
   9.238 +  using a Quotient_symp[OF q] Quotient_transp[OF q]
   9.239 +  unfolding symp_def transp_def
   9.240 +  by blast
   9.241 +
   9.242 +lemma lambda_prs:
   9.243 +  assumes q1: "Quotient R1 Abs1 Rep1"
   9.244 +  and     q2: "Quotient R2 Abs2 Rep2"
   9.245 +  shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
   9.246 +  unfolding expand_fun_eq
   9.247 +  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   9.248 +  by simp
   9.249 +
   9.250 +lemma lambda_prs1:
   9.251 +  assumes q1: "Quotient R1 Abs1 Rep1"
   9.252 +  and     q2: "Quotient R2 Abs2 Rep2"
   9.253 +  shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
   9.254 +  unfolding expand_fun_eq
   9.255 +  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   9.256 +  by simp
   9.257 +
   9.258 +lemma rep_abs_rsp:
   9.259 +  assumes q: "Quotient R Abs Rep"
   9.260 +  and     a: "R x1 x2"
   9.261 +  shows "R x1 (Rep (Abs x2))"
   9.262 +  using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
   9.263 +  by metis
   9.264 +
   9.265 +lemma rep_abs_rsp_left:
   9.266 +  assumes q: "Quotient R Abs Rep"
   9.267 +  and     a: "R x1 x2"
   9.268 +  shows "R (Rep (Abs x1)) x2"
   9.269 +  using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
   9.270 +  by metis
   9.271 +
   9.272 +text{*
   9.273 +  In the following theorem R1 can be instantiated with anything,
   9.274 +  but we know some of the types of the Rep and Abs functions;
   9.275 +  so by solving Quotient assumptions we can get a unique R1 that
   9.276 +  will be provable; which is why we need to use apply_rsp and
   9.277 +  not the primed version *}
   9.278 +
   9.279 +lemma apply_rsp:
   9.280 +  fixes f g::"'a \<Rightarrow> 'c"
   9.281 +  assumes q: "Quotient R1 Abs1 Rep1"
   9.282 +  and     a: "(R1 ===> R2) f g" "R1 x y"
   9.283 +  shows "R2 (f x) (g y)"
   9.284 +  using a by simp
   9.285 +
   9.286 +lemma apply_rsp':
   9.287 +  assumes a: "(R1 ===> R2) f g" "R1 x y"
   9.288 +  shows "R2 (f x) (g y)"
   9.289 +  using a by simp
   9.290 +
   9.291 +section {* lemmas for regularisation of ball and bex *}
   9.292 +
   9.293 +lemma ball_reg_eqv:
   9.294 +  fixes P :: "'a \<Rightarrow> bool"
   9.295 +  assumes a: "equivp R"
   9.296 +  shows "Ball (Respects R) P = (All P)"
   9.297 +  using a
   9.298 +  unfolding equivp_def
   9.299 +  by (auto simp add: in_respects)
   9.300 +
   9.301 +lemma bex_reg_eqv:
   9.302 +  fixes P :: "'a \<Rightarrow> bool"
   9.303 +  assumes a: "equivp R"
   9.304 +  shows "Bex (Respects R) P = (Ex P)"
   9.305 +  using a
   9.306 +  unfolding equivp_def
   9.307 +  by (auto simp add: in_respects)
   9.308 +
   9.309 +lemma ball_reg_right:
   9.310 +  assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
   9.311 +  shows "All P \<longrightarrow> Ball R Q"
   9.312 +  using a by (metis COMBC_def Collect_def Collect_mem_eq)
   9.313 +
   9.314 +lemma bex_reg_left:
   9.315 +  assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
   9.316 +  shows "Bex R Q \<longrightarrow> Ex P"
   9.317 +  using a by (metis COMBC_def Collect_def Collect_mem_eq)
   9.318 +
   9.319 +lemma ball_reg_left:
   9.320 +  assumes a: "equivp R"
   9.321 +  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
   9.322 +  using a by (metis equivp_reflp in_respects)
   9.323 +
   9.324 +lemma bex_reg_right:
   9.325 +  assumes a: "equivp R"
   9.326 +  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
   9.327 +  using a by (metis equivp_reflp in_respects)
   9.328 +
   9.329 +lemma ball_reg_eqv_range:
   9.330 +  fixes P::"'a \<Rightarrow> bool"
   9.331 +  and x::"'a"
   9.332 +  assumes a: "equivp R2"
   9.333 +  shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
   9.334 +  apply(rule iffI)
   9.335 +  apply(rule allI)
   9.336 +  apply(drule_tac x="\<lambda>y. f x" in bspec)
   9.337 +  apply(simp add: in_respects)
   9.338 +  apply(rule impI)
   9.339 +  using a equivp_reflp_symp_transp[of "R2"]
   9.340 +  apply(simp add: reflp_def)
   9.341 +  apply(simp)
   9.342 +  apply(simp)
   9.343 +  done
   9.344 +
   9.345 +lemma bex_reg_eqv_range:
   9.346 +  assumes a: "equivp R2"
   9.347 +  shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
   9.348 +  apply(auto)
   9.349 +  apply(rule_tac x="\<lambda>y. f x" in bexI)
   9.350 +  apply(simp)
   9.351 +  apply(simp add: Respects_def in_respects)
   9.352 +  apply(rule impI)
   9.353 +  using a equivp_reflp_symp_transp[of "R2"]
   9.354 +  apply(simp add: reflp_def)
   9.355 +  done
   9.356 +
   9.357 +(* Next four lemmas are unused *)
   9.358 +lemma all_reg:
   9.359 +  assumes a: "!x :: 'a. (P x --> Q x)"
   9.360 +  and     b: "All P"
   9.361 +  shows "All Q"
   9.362 +  using a b by (metis)
   9.363 +
   9.364 +lemma ex_reg:
   9.365 +  assumes a: "!x :: 'a. (P x --> Q x)"
   9.366 +  and     b: "Ex P"
   9.367 +  shows "Ex Q"
   9.368 +  using a b by metis
   9.369 +
   9.370 +lemma ball_reg:
   9.371 +  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
   9.372 +  and     b: "Ball R P"
   9.373 +  shows "Ball R Q"
   9.374 +  using a b by (metis COMBC_def Collect_def Collect_mem_eq)
   9.375 +
   9.376 +lemma bex_reg:
   9.377 +  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
   9.378 +  and     b: "Bex R P"
   9.379 +  shows "Bex R Q"
   9.380 +  using a b by (metis COMBC_def Collect_def Collect_mem_eq)
   9.381 +
   9.382 +
   9.383 +lemma ball_all_comm:
   9.384 +  assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
   9.385 +  shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
   9.386 +  using assms by auto
   9.387 +
   9.388 +lemma bex_ex_comm:
   9.389 +  assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)"
   9.390 +  shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
   9.391 +  using assms by auto
   9.392 +
   9.393 +section {* Bounded abstraction *}
   9.394 +
   9.395 +definition
   9.396 +  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   9.397 +where
   9.398 +  "x \<in> p \<Longrightarrow> Babs p m x = m x"
   9.399 +
   9.400 +lemma babs_rsp:
   9.401 +  assumes q: "Quotient R1 Abs1 Rep1"
   9.402 +  and     a: "(R1 ===> R2) f g"
   9.403 +  shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
   9.404 +  apply (auto simp add: Babs_def in_respects)
   9.405 +  apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   9.406 +  using a apply (simp add: Babs_def)
   9.407 +  apply (simp add: in_respects)
   9.408 +  using Quotient_rel[OF q]
   9.409 +  by metis
   9.410 +
   9.411 +lemma babs_prs:
   9.412 +  assumes q1: "Quotient R1 Abs1 Rep1"
   9.413 +  and     q2: "Quotient R2 Abs2 Rep2"
   9.414 +  shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
   9.415 +  apply (rule ext)
   9.416 +  apply (simp)
   9.417 +  apply (subgoal_tac "Rep1 x \<in> Respects R1")
   9.418 +  apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   9.419 +  apply (simp add: in_respects Quotient_rel_rep[OF q1])
   9.420 +  done
   9.421 +
   9.422 +lemma babs_simp:
   9.423 +  assumes q: "Quotient R1 Abs Rep"
   9.424 +  shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
   9.425 +  apply(rule iffI)
   9.426 +  apply(simp_all only: babs_rsp[OF q])
   9.427 +  apply(auto simp add: Babs_def)
   9.428 +  apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   9.429 +  apply(metis Babs_def)
   9.430 +  apply (simp add: in_respects)
   9.431 +  using Quotient_rel[OF q]
   9.432 +  by metis
   9.433 +
   9.434 +(* If a user proves that a particular functional relation
   9.435 +   is an equivalence this may be useful in regularising *)
   9.436 +lemma babs_reg_eqv:
   9.437 +  shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
   9.438 +  by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
   9.439 +
   9.440 +
   9.441 +(* 3 lemmas needed for proving repabs_inj *)
   9.442 +lemma ball_rsp:
   9.443 +  assumes a: "(R ===> (op =)) f g"
   9.444 +  shows "Ball (Respects R) f = Ball (Respects R) g"
   9.445 +  using a by (simp add: Ball_def in_respects)
   9.446 +
   9.447 +lemma bex_rsp:
   9.448 +  assumes a: "(R ===> (op =)) f g"
   9.449 +  shows "(Bex (Respects R) f = Bex (Respects R) g)"
   9.450 +  using a by (simp add: Bex_def in_respects)
   9.451 +
   9.452 +lemma bex1_rsp:
   9.453 +  assumes a: "(R ===> (op =)) f g"
   9.454 +  shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
   9.455 +  using a
   9.456 +  by (simp add: Ex1_def in_respects) auto
   9.457 +
   9.458 +(* 2 lemmas needed for cleaning of quantifiers *)
   9.459 +lemma all_prs:
   9.460 +  assumes a: "Quotient R absf repf"
   9.461 +  shows "Ball (Respects R) ((absf ---> id) f) = All f"
   9.462 +  using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
   9.463 +  by metis
   9.464 +
   9.465 +lemma ex_prs:
   9.466 +  assumes a: "Quotient R absf repf"
   9.467 +  shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
   9.468 +  using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
   9.469 +  by metis
   9.470 +
   9.471 +section {* Bex1_rel quantifier *}
   9.472 +
   9.473 +definition
   9.474 +  Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   9.475 +where
   9.476 +  "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)))"
   9.477 +
   9.478 +lemma bex1_rel_aux:
   9.479 +  "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
   9.480 +  unfolding Bex1_rel_def
   9.481 +  apply (erule conjE)+
   9.482 +  apply (erule bexE)
   9.483 +  apply rule
   9.484 +  apply (rule_tac x="xa" in bexI)
   9.485 +  apply metis
   9.486 +  apply metis
   9.487 +  apply rule+
   9.488 +  apply (erule_tac x="xaa" in ballE)
   9.489 +  prefer 2
   9.490 +  apply (metis)
   9.491 +  apply (erule_tac x="ya" in ballE)
   9.492 +  prefer 2
   9.493 +  apply (metis)
   9.494 +  apply (metis in_respects)
   9.495 +  done
   9.496 +
   9.497 +lemma bex1_rel_aux2:
   9.498 +  "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x"
   9.499 +  unfolding Bex1_rel_def
   9.500 +  apply (erule conjE)+
   9.501 +  apply (erule bexE)
   9.502 +  apply rule
   9.503 +  apply (rule_tac x="xa" in bexI)
   9.504 +  apply metis
   9.505 +  apply metis
   9.506 +  apply rule+
   9.507 +  apply (erule_tac x="xaa" in ballE)
   9.508 +  prefer 2
   9.509 +  apply (metis)
   9.510 +  apply (erule_tac x="ya" in ballE)
   9.511 +  prefer 2
   9.512 +  apply (metis)
   9.513 +  apply (metis in_respects)
   9.514 +  done
   9.515 +
   9.516 +lemma bex1_rel_rsp:
   9.517 +  assumes a: "Quotient R absf repf"
   9.518 +  shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
   9.519 +  apply simp
   9.520 +  apply clarify
   9.521 +  apply rule
   9.522 +  apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
   9.523 +  apply (erule bex1_rel_aux2)
   9.524 +  apply assumption
   9.525 +  done
   9.526 +
   9.527 +
   9.528 +lemma ex1_prs:
   9.529 +  assumes a: "Quotient R absf repf"
   9.530 +  shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
   9.531 +apply simp
   9.532 +apply (subst Bex1_rel_def)
   9.533 +apply (subst Bex_def)
   9.534 +apply (subst Ex1_def)
   9.535 +apply simp
   9.536 +apply rule
   9.537 + apply (erule conjE)+
   9.538 + apply (erule_tac exE)
   9.539 + apply (erule conjE)
   9.540 + apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y")
   9.541 +  apply (rule_tac x="absf x" in exI)
   9.542 +  apply (simp)
   9.543 +  apply rule+
   9.544 +  using a unfolding Quotient_def
   9.545 +  apply metis
   9.546 + apply rule+
   9.547 + apply (erule_tac x="x" in ballE)
   9.548 +  apply (erule_tac x="y" in ballE)
   9.549 +   apply simp
   9.550 +  apply (simp add: in_respects)
   9.551 + apply (simp add: in_respects)
   9.552 +apply (erule_tac exE)
   9.553 + apply rule
   9.554 + apply (rule_tac x="repf x" in exI)
   9.555 + apply (simp only: in_respects)
   9.556 +  apply rule
   9.557 + apply (metis Quotient_rel_rep[OF a])
   9.558 +using a unfolding Quotient_def apply (simp)
   9.559 +apply rule+
   9.560 +using a unfolding Quotient_def in_respects
   9.561 +apply metis
   9.562 +done
   9.563 +
   9.564 +lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
   9.565 +  apply (simp add: Ex1_def Bex1_rel_def in_respects)
   9.566 +  apply clarify
   9.567 +  apply auto
   9.568 +  apply (rule bexI)
   9.569 +  apply assumption
   9.570 +  apply (simp add: in_respects)
   9.571 +  apply (simp add: in_respects)
   9.572 +  apply auto
   9.573 +  done
   9.574 +
   9.575 +section {* Various respects and preserve lemmas *}
   9.576 +
   9.577 +lemma quot_rel_rsp:
   9.578 +  assumes a: "Quotient R Abs Rep"
   9.579 +  shows "(R ===> R ===> op =) R R"
   9.580 +  apply(rule fun_rel_id)+
   9.581 +  apply(rule equals_rsp[OF a])
   9.582 +  apply(assumption)+
   9.583 +  done
   9.584 +
   9.585 +lemma o_prs:
   9.586 +  assumes q1: "Quotient R1 Abs1 Rep1"
   9.587 +  and     q2: "Quotient R2 Abs2 Rep2"
   9.588 +  and     q3: "Quotient R3 Abs3 Rep3"
   9.589 +  shows "(Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g)) = f o g"
   9.590 +  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
   9.591 +  unfolding o_def expand_fun_eq by simp
   9.592 +
   9.593 +lemma o_rsp:
   9.594 +  assumes q1: "Quotient R1 Abs1 Rep1"
   9.595 +  and     q2: "Quotient R2 Abs2 Rep2"
   9.596 +  and     q3: "Quotient R3 Abs3 Rep3"
   9.597 +  and     a1: "(R2 ===> R3) f1 f2"
   9.598 +  and     a2: "(R1 ===> R2) g1 g2"
   9.599 +  shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
   9.600 +  using a1 a2 unfolding o_def expand_fun_eq
   9.601 +  by (auto)
   9.602 +
   9.603 +lemma cond_prs:
   9.604 +  assumes a: "Quotient R absf repf"
   9.605 +  shows "absf (if a then repf b else repf c) = (if a then b else c)"
   9.606 +  using a unfolding Quotient_def by auto
   9.607 +
   9.608 +lemma if_prs:
   9.609 +  assumes q: "Quotient R Abs Rep"
   9.610 +  shows "Abs (If a (Rep b) (Rep c)) = If a b c"
   9.611 +  using Quotient_abs_rep[OF q] by auto
   9.612 +
   9.613 +(* q not used *)
   9.614 +lemma if_rsp:
   9.615 +  assumes q: "Quotient R Abs Rep"
   9.616 +  and     a: "a1 = a2" "R b1 b2" "R c1 c2"
   9.617 +  shows "R (If a1 b1 c1) (If a2 b2 c2)"
   9.618 +  using a by auto
   9.619 +
   9.620 +lemma let_prs:
   9.621 +  assumes q1: "Quotient R1 Abs1 Rep1"
   9.622 +  and     q2: "Quotient R2 Abs2 Rep2"
   9.623 +  shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f"
   9.624 +  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
   9.625 +
   9.626 +lemma let_rsp:
   9.627 +  assumes q1: "Quotient R1 Abs1 Rep1"
   9.628 +  and     a1: "(R1 ===> R2) f g"
   9.629 +  and     a2: "R1 x y"
   9.630 +  shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
   9.631 +  using apply_rsp[OF q1 a1] a2 by auto
   9.632 +
   9.633 +locale quot_type =
   9.634 +  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   9.635 +  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
   9.636 +  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
   9.637 +  assumes equivp: "equivp R"
   9.638 +  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
   9.639 +  and     rep_inverse: "\<And>x. Abs (Rep x) = x"
   9.640 +  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
   9.641 +  and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
   9.642 +begin
   9.643 +
   9.644 +definition
   9.645 +  abs::"'a \<Rightarrow> 'b"
   9.646 +where
   9.647 +  "abs x \<equiv> Abs (R x)"
   9.648 +
   9.649 +definition
   9.650 +  rep::"'b \<Rightarrow> 'a"
   9.651 +where
   9.652 +  "rep a = Eps (Rep a)"
   9.653 +
   9.654 +lemma homeier_lem9:
   9.655 +  shows "R (Eps (R x)) = R x"
   9.656 +proof -
   9.657 +  have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
   9.658 +  then have "R x (Eps (R x))" by (rule someI)
   9.659 +  then show "R (Eps (R x)) = R x"
   9.660 +    using equivp unfolding equivp_def by simp
   9.661 +qed
   9.662 +
   9.663 +theorem homeier_thm10:
   9.664 +  shows "abs (rep a) = a"
   9.665 +  unfolding abs_def rep_def
   9.666 +proof -
   9.667 +  from rep_prop
   9.668 +  obtain x where eq: "Rep a = R x" by auto
   9.669 +  have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
   9.670 +  also have "\<dots> = Abs (R x)" using homeier_lem9 by simp
   9.671 +  also have "\<dots> = Abs (Rep a)" using eq by simp
   9.672 +  also have "\<dots> = a" using rep_inverse by simp
   9.673 +  finally
   9.674 +  show "Abs (R (Eps (Rep a))) = a" by simp
   9.675 +qed
   9.676 +
   9.677 +lemma homeier_lem7:
   9.678 +  shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
   9.679 +proof -
   9.680 +  have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
   9.681 +  also have "\<dots> = ?LHS" by (simp add: abs_inverse)
   9.682 +  finally show "?LHS = ?RHS" by simp
   9.683 +qed
   9.684 +
   9.685 +theorem homeier_thm11:
   9.686 +  shows "R r r' = (abs r = abs r')"
   9.687 +  unfolding abs_def
   9.688 +  by (simp only: equivp[simplified equivp_def] homeier_lem7)
   9.689 +
   9.690 +lemma rep_refl:
   9.691 +  shows "R (rep a) (rep a)"
   9.692 +  unfolding rep_def
   9.693 +  by (simp add: equivp[simplified equivp_def])
   9.694 +
   9.695 +
   9.696 +lemma rep_abs_rsp:
   9.697 +  shows "R f (rep (abs g)) = R f g"
   9.698 +  and   "R (rep (abs g)) f = R g f"
   9.699 +  by (simp_all add: homeier_thm10 homeier_thm11)
   9.700 +
   9.701 +lemma Quotient:
   9.702 +  shows "Quotient R abs rep"
   9.703 +  unfolding Quotient_def
   9.704 +  apply(simp add: homeier_thm10)
   9.705 +  apply(simp add: rep_refl)
   9.706 +  apply(subst homeier_thm11[symmetric])
   9.707 +  apply(simp add: equivp[simplified equivp_def])
   9.708 +  done
   9.709 +
   9.710 +end
   9.711 +
   9.712 +section {* ML setup *}
   9.713 +
   9.714 +text {* Auxiliary data for the quotient package *}
   9.715 +
   9.716 +use "~~/src/HOL/Tools/Quotient/quotient_info.ML"
   9.717 +
   9.718 +declare [[map "fun" = (fun_map, fun_rel)]]
   9.719 +
   9.720 +lemmas [quot_thm] = fun_quotient
   9.721 +lemmas [quot_respect] = quot_rel_rsp
   9.722 +lemmas [quot_equiv] = identity_equivp
   9.723 +
   9.724 +
   9.725 +text {* Lemmas about simplifying id's. *}
   9.726 +lemmas [id_simps] =
   9.727 +  id_def[symmetric]
   9.728 +  fun_map_id
   9.729 +  id_apply
   9.730 +  id_o
   9.731 +  o_id
   9.732 +  eq_comp_r
   9.733 +
   9.734 +text {* Translation functions for the lifting process. *}
   9.735 +use "~~/src/HOL/Tools/Quotient/quotient_term.ML"
   9.736 +
   9.737 +
   9.738 +text {* Definitions of the quotient types. *}
   9.739 +use "~~/src/HOL/Tools/Quotient/quotient_typ.ML"
   9.740 +
   9.741 +
   9.742 +text {* Definitions for quotient constants. *}
   9.743 +use "~~/src/HOL/Tools/Quotient/quotient_def.ML"
   9.744 +
   9.745 +
   9.746 +text {*
   9.747 +  An auxiliary constant for recording some information
   9.748 +  about the lifted theorem in a tactic.
   9.749 +*}
   9.750 +definition
   9.751 +  "Quot_True x \<equiv> True"
   9.752 +
   9.753 +lemma
   9.754 +  shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
   9.755 +  and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
   9.756 +  and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
   9.757 +  and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
   9.758 +  and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
   9.759 +  by (simp_all add: Quot_True_def ext)
   9.760 +
   9.761 +lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
   9.762 +  by (simp add: Quot_True_def)
   9.763 +
   9.764 +
   9.765 +text {* Tactics for proving the lifted theorems *}
   9.766 +use "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"
   9.767 +
   9.768 +section {* Methods / Interface *}
   9.769 +
   9.770 +method_setup lifting =
   9.771 +  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
   9.772 +  {* lifts theorems to quotient types *}
   9.773 +
   9.774 +method_setup lifting_setup =
   9.775 +  {* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
   9.776 +  {* sets up the three goals for the quotient lifting procedure *}
   9.777 +
   9.778 +method_setup regularize =
   9.779 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
   9.780 +  {* proves the regularization goals from the quotient lifting procedure *}
   9.781 +
   9.782 +method_setup injection =
   9.783 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *}
   9.784 +  {* proves the rep/abs injection goals from the quotient lifting procedure *}
   9.785 +
   9.786 +method_setup cleaning =
   9.787 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *}
   9.788 +  {* proves the cleaning goals from the quotient lifting procedure *}
   9.789 +
   9.790 +attribute_setup quot_lifted =
   9.791 +  {* Scan.succeed Quotient_Tacs.lifted_attrib *}
   9.792 +  {* lifts theorems to quotient types *}
   9.793 +
   9.794 +no_notation
   9.795 +  rel_conj (infixr "OOO" 75) and
   9.796 +  fun_map (infixr "--->" 55) and
   9.797 +  fun_rel (infixr "===>" 55)
   9.798 +
   9.799 +end
   9.800 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Quotient_Examples/LarryDatatype.thy	Fri Feb 19 13:54:19 2010 +0100
    10.3 @@ -0,0 +1,394 @@
    10.4 +theory LarryDatatype
    10.5 +imports Main Quotient_Syntax
    10.6 +begin
    10.7 +
    10.8 +subsection{*Defining the Free Algebra*}
    10.9 +
   10.10 +datatype
   10.11 +  freemsg = NONCE  nat
   10.12 +        | MPAIR  freemsg freemsg
   10.13 +        | CRYPT  nat freemsg  
   10.14 +        | DECRYPT  nat freemsg
   10.15 +
   10.16 +inductive 
   10.17 +  msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
   10.18 +where 
   10.19 +  CD:    "CRYPT K (DECRYPT K X) \<sim> X"
   10.20 +| DC:    "DECRYPT K (CRYPT K X) \<sim> X"
   10.21 +| NONCE: "NONCE N \<sim> NONCE N"
   10.22 +| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
   10.23 +| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
   10.24 +| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
   10.25 +| SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
   10.26 +| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
   10.27 +
   10.28 +lemmas msgrel.intros[intro]
   10.29 +
   10.30 +text{*Proving that it is an equivalence relation*}
   10.31 +
   10.32 +lemma msgrel_refl: "X \<sim> X"
   10.33 +by (induct X, (blast intro: msgrel.intros)+)
   10.34 +
   10.35 +theorem equiv_msgrel: "equivp msgrel"
   10.36 +proof (rule equivpI)
   10.37 +  show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
   10.38 +  show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
   10.39 +  show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
   10.40 +qed
   10.41 +
   10.42 +subsection{*Some Functions on the Free Algebra*}
   10.43 +
   10.44 +subsubsection{*The Set of Nonces*}
   10.45 +
   10.46 +fun
   10.47 +  freenonces :: "freemsg \<Rightarrow> nat set"
   10.48 +where
   10.49 +  "freenonces (NONCE N) = {N}"
   10.50 +| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
   10.51 +| "freenonces (CRYPT K X) = freenonces X"
   10.52 +| "freenonces (DECRYPT K X) = freenonces X"
   10.53 +
   10.54 +theorem msgrel_imp_eq_freenonces: 
   10.55 +  assumes a: "U \<sim> V"
   10.56 +  shows "freenonces U = freenonces V"
   10.57 +  using a by (induct) (auto) 
   10.58 +
   10.59 +subsubsection{*The Left Projection*}
   10.60 +
   10.61 +text{*A function to return the left part of the top pair in a message.  It will
   10.62 +be lifted to the initial algrebra, to serve as an example of that process.*}
   10.63 +fun
   10.64 +  freeleft :: "freemsg \<Rightarrow> freemsg"
   10.65 +where
   10.66 +  "freeleft (NONCE N) = NONCE N"
   10.67 +| "freeleft (MPAIR X Y) = X"
   10.68 +| "freeleft (CRYPT K X) = freeleft X"
   10.69 +| "freeleft (DECRYPT K X) = freeleft X"
   10.70 +
   10.71 +text{*This theorem lets us prove that the left function respects the
   10.72 +equivalence relation.  It also helps us prove that MPair
   10.73 +  (the abstract constructor) is injective*}
   10.74 +lemma msgrel_imp_eqv_freeleft_aux:
   10.75 +  shows "freeleft U \<sim> freeleft U"
   10.76 +  by (induct rule: freeleft.induct) (auto)
   10.77 +
   10.78 +theorem msgrel_imp_eqv_freeleft:
   10.79 +  assumes a: "U \<sim> V" 
   10.80 +  shows "freeleft U \<sim> freeleft V"
   10.81 +  using a
   10.82 +  by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
   10.83 +
   10.84 +subsubsection{*The Right Projection*}
   10.85 +
   10.86 +text{*A function to return the right part of the top pair in a message.*}
   10.87 +fun
   10.88 +  freeright :: "freemsg \<Rightarrow> freemsg"
   10.89 +where
   10.90 +  "freeright (NONCE N) = NONCE N"
   10.91 +| "freeright (MPAIR X Y) = Y"
   10.92 +| "freeright (CRYPT K X) = freeright X"
   10.93 +| "freeright (DECRYPT K X) = freeright X"
   10.94 +
   10.95 +text{*This theorem lets us prove that the right function respects the
   10.96 +equivalence relation.  It also helps us prove that MPair
   10.97 +  (the abstract constructor) is injective*}
   10.98 +lemma msgrel_imp_eqv_freeright_aux:
   10.99 +  shows "freeright U \<sim> freeright U"
  10.100 +  by (induct rule: freeright.induct) (auto)
  10.101 +
  10.102 +theorem msgrel_imp_eqv_freeright:
  10.103 +  assumes a: "U \<sim> V" 
  10.104 +  shows "freeright U \<sim> freeright V"
  10.105 +  using a
  10.106 +  by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
  10.107 +
  10.108 +subsubsection{*The Discriminator for Constructors*}
  10.109 +
  10.110 +text{*A function to distinguish nonces, mpairs and encryptions*}
  10.111 +fun 
  10.112 +  freediscrim :: "freemsg \<Rightarrow> int"
  10.113 +where
  10.114 +   "freediscrim (NONCE N) = 0"
  10.115 + | "freediscrim (MPAIR X Y) = 1"
  10.116 + | "freediscrim (CRYPT K X) = freediscrim X + 2"
  10.117 + | "freediscrim (DECRYPT K X) = freediscrim X - 2"
  10.118 +
  10.119 +text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
  10.120 +theorem msgrel_imp_eq_freediscrim:
  10.121 +  assumes a: "U \<sim> V"
  10.122 +  shows "freediscrim U = freediscrim V"
  10.123 +  using a by (induct) (auto)
  10.124 +
  10.125 +subsection{*The Initial Algebra: A Quotiented Message Type*}
  10.126 +
  10.127 +quotient_type msg = freemsg / msgrel
  10.128 +  by (rule equiv_msgrel)
  10.129 +
  10.130 +text{*The abstract message constructors*}
  10.131 +
  10.132 +quotient_definition
  10.133 +  "Nonce :: nat \<Rightarrow> msg"
  10.134 +is
  10.135 +  "NONCE"
  10.136 +
  10.137 +quotient_definition
  10.138 +  "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
  10.139 +is
  10.140 +  "MPAIR"
  10.141 +
  10.142 +quotient_definition
  10.143 +  "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
  10.144 +is
  10.145 +  "CRYPT"
  10.146 +
  10.147 +quotient_definition
  10.148 +  "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
  10.149 +is
  10.150 +  "DECRYPT"
  10.151 +
  10.152 +lemma [quot_respect]:
  10.153 +  shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
  10.154 +by (auto intro: CRYPT)
  10.155 +
  10.156 +lemma [quot_respect]:
  10.157 +  shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
  10.158 +by (auto intro: DECRYPT)
  10.159 +
  10.160 +text{*Establishing these two equations is the point of the whole exercise*}
  10.161 +theorem CD_eq [simp]: 
  10.162 +  shows "Crypt K (Decrypt K X) = X"
  10.163 +  by (lifting CD)
  10.164 +
  10.165 +theorem DC_eq [simp]: 
  10.166 +  shows "Decrypt K (Crypt K X) = X"
  10.167 +  by (lifting DC)
  10.168 +
  10.169 +subsection{*The Abstract Function to Return the Set of Nonces*}
  10.170 +
  10.171 +quotient_definition
  10.172 +   "nonces:: msg \<Rightarrow> nat set"
  10.173 +is
  10.174 +  "freenonces"
  10.175 +
  10.176 +text{*Now prove the four equations for @{term nonces}*}
  10.177 +
  10.178 +lemma [quot_respect]:
  10.179 +  shows "(op \<sim> ===> op =) freenonces freenonces"
  10.180 +  by (simp add: msgrel_imp_eq_freenonces)
  10.181 +
  10.182 +lemma [quot_respect]:
  10.183 +  shows "(op = ===> op \<sim>) NONCE NONCE"
  10.184 +  by (simp add: NONCE)
  10.185 +
  10.186 +lemma nonces_Nonce [simp]: 
  10.187 +  shows "nonces (Nonce N) = {N}"
  10.188 +  by (lifting freenonces.simps(1))
  10.189 + 
  10.190 +lemma [quot_respect]:
  10.191 +  shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
  10.192 +  by (simp add: MPAIR)
  10.193 +
  10.194 +lemma nonces_MPair [simp]: 
  10.195 +  shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
  10.196 +  by (lifting freenonces.simps(2))
  10.197 +
  10.198 +lemma nonces_Crypt [simp]: 
  10.199 +  shows "nonces (Crypt K X) = nonces X"
  10.200 +  by (lifting freenonces.simps(3))
  10.201 +
  10.202 +lemma nonces_Decrypt [simp]: 
  10.203 +  shows "nonces (Decrypt K X) = nonces X"
  10.204 +  by (lifting freenonces.simps(4))
  10.205 +
  10.206 +subsection{*The Abstract Function to Return the Left Part*}
  10.207 +
  10.208 +quotient_definition
  10.209 +  "left:: msg \<Rightarrow> msg"
  10.210 +is
  10.211 +  "freeleft"
  10.212 +
  10.213 +lemma [quot_respect]:
  10.214 +  shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
  10.215 +  by (simp add: msgrel_imp_eqv_freeleft)
  10.216 +
  10.217 +lemma left_Nonce [simp]: 
  10.218 +  shows "left (Nonce N) = Nonce N"
  10.219 +  by (lifting freeleft.simps(1))
  10.220 +
  10.221 +lemma left_MPair [simp]: 
  10.222 +  shows "left (MPair X Y) = X"
  10.223 +  by (lifting freeleft.simps(2))
  10.224 +
  10.225 +lemma left_Crypt [simp]: 
  10.226 +  shows "left (Crypt K X) = left X"
  10.227 +  by (lifting freeleft.simps(3))
  10.228 +
  10.229 +lemma left_Decrypt [simp]: 
  10.230 +  shows "left (Decrypt K X) = left X"
  10.231 +  by (lifting freeleft.simps(4))
  10.232 +
  10.233 +subsection{*The Abstract Function to Return the Right Part*}
  10.234 +
  10.235 +quotient_definition
  10.236 +  "right:: msg \<Rightarrow> msg"
  10.237 +is
  10.238 +  "freeright"
  10.239 +
  10.240 +text{*Now prove the four equations for @{term right}*}
  10.241 +
  10.242 +lemma [quot_respect]:
  10.243 +  shows "(op \<sim> ===> op \<sim>) freeright freeright"
  10.244 +  by (simp add: msgrel_imp_eqv_freeright)
  10.245 +
  10.246 +lemma right_Nonce [simp]: 
  10.247 +  shows "right (Nonce N) = Nonce N"
  10.248 +  by (lifting freeright.simps(1))
  10.249 +
  10.250 +lemma right_MPair [simp]: 
  10.251 +  shows "right (MPair X Y) = Y"
  10.252 +  by (lifting freeright.simps(2))
  10.253 +
  10.254 +lemma right_Crypt [simp]: 
  10.255 +  shows "right (Crypt K X) = right X"
  10.256 +  by (lifting freeright.simps(3))
  10.257 +
  10.258 +lemma right_Decrypt [simp]: 
  10.259 +  shows "right (Decrypt K X) = right X"
  10.260 +  by (lifting freeright.simps(4))
  10.261 +
  10.262 +subsection{*Injectivity Properties of Some Constructors*}
  10.263 +
  10.264 +lemma NONCE_imp_eq: 
  10.265 +  shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
  10.266 +  by (drule msgrel_imp_eq_freenonces, simp)
  10.267 +
  10.268 +text{*Can also be proved using the function @{term nonces}*}
  10.269 +lemma Nonce_Nonce_eq [iff]: 
  10.270 +  shows "(Nonce m = Nonce n) = (m = n)"
  10.271 +proof
  10.272 +  assume "Nonce m = Nonce n"
  10.273 +  then show "m = n" by (lifting NONCE_imp_eq)
  10.274 +next
  10.275 +  assume "m = n" 
  10.276 +  then show "Nonce m = Nonce n" by simp
  10.277 +qed
  10.278 +
  10.279 +lemma MPAIR_imp_eqv_left: 
  10.280 +  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
  10.281 +  by (drule msgrel_imp_eqv_freeleft) (simp)
  10.282 +
  10.283 +lemma MPair_imp_eq_left: 
  10.284 +  assumes eq: "MPair X Y = MPair X' Y'" 
  10.285 +  shows "X = X'"
  10.286 +  using eq by (lifting MPAIR_imp_eqv_left)
  10.287 +
  10.288 +lemma MPAIR_imp_eqv_right: 
  10.289 +  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
  10.290 +  by (drule msgrel_imp_eqv_freeright) (simp)
  10.291 +
  10.292 +lemma MPair_imp_eq_right: 
  10.293 +  shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
  10.294 +  by (lifting  MPAIR_imp_eqv_right)
  10.295 +
  10.296 +theorem MPair_MPair_eq [iff]: 
  10.297 +  shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" 
  10.298 +  by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
  10.299 +
  10.300 +lemma NONCE_neqv_MPAIR: 
  10.301 +  shows "\<not>(NONCE m \<sim> MPAIR X Y)"
  10.302 +  by (auto dest: msgrel_imp_eq_freediscrim)
  10.303 +
  10.304 +theorem Nonce_neq_MPair [iff]: 
  10.305 +  shows "Nonce N \<noteq> MPair X Y"
  10.306 +  by (lifting NONCE_neqv_MPAIR)
  10.307 +
  10.308 +text{*Example suggested by a referee*}
  10.309 +
  10.310 +lemma CRYPT_NONCE_neq_NONCE:
  10.311 +  shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
  10.312 +  by (auto dest: msgrel_imp_eq_freediscrim)
  10.313 +
  10.314 +theorem Crypt_Nonce_neq_Nonce: 
  10.315 +  shows "Crypt K (Nonce M) \<noteq> Nonce N"
  10.316 +  by (lifting CRYPT_NONCE_neq_NONCE)
  10.317 +
  10.318 +text{*...and many similar results*}
  10.319 +lemma CRYPT2_NONCE_neq_NONCE: 
  10.320 +  shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
  10.321 +  by (auto dest: msgrel_imp_eq_freediscrim)  
  10.322 +
  10.323 +theorem Crypt2_Nonce_neq_Nonce: 
  10.324 +  shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
  10.325 +  by (lifting CRYPT2_NONCE_neq_NONCE) 
  10.326 +
  10.327 +theorem Crypt_Crypt_eq [iff]: 
  10.328 +  shows "(Crypt K X = Crypt K X') = (X=X')" 
  10.329 +proof
  10.330 +  assume "Crypt K X = Crypt K X'"
  10.331 +  hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
  10.332 +  thus "X = X'" by simp
  10.333 +next
  10.334 +  assume "X = X'"
  10.335 +  thus "Crypt K X = Crypt K X'" by simp
  10.336 +qed
  10.337 +
  10.338 +theorem Decrypt_Decrypt_eq [iff]: 
  10.339 +  shows "(Decrypt K X = Decrypt K X') = (X=X')" 
  10.340 +proof
  10.341 +  assume "Decrypt K X = Decrypt K X'"
  10.342 +  hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
  10.343 +  thus "X = X'" by simp
  10.344 +next
  10.345 +  assume "X = X'"
  10.346 +  thus "Decrypt K X = Decrypt K X'" by simp
  10.347 +qed
  10.348 +
  10.349 +lemma msg_induct_aux:
  10.350 +  shows "\<lbrakk>\<And>N. P (Nonce N);
  10.351 +          \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
  10.352 +          \<And>K X. P X \<Longrightarrow> P (Crypt K X);
  10.353 +          \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
  10.354 +  by (lifting freemsg.induct)
  10.355 +
  10.356 +lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
  10.357 +  assumes N: "\<And>N. P (Nonce N)"
  10.358 +      and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
  10.359 +      and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
  10.360 +      and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
  10.361 +  shows "P msg"
  10.362 +  using N M C D by (rule msg_induct_aux)
  10.363 +
  10.364 +subsection{*The Abstract Discriminator*}
  10.365 +
  10.366 +text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
  10.367 +need this function in order to prove discrimination theorems.*}
  10.368 +
  10.369 +quotient_definition
  10.370 +  "discrim:: msg \<Rightarrow> int"
  10.371 +is
  10.372 +  "freediscrim"
  10.373 +
  10.374 +text{*Now prove the four equations for @{term discrim}*}
  10.375 +
  10.376 +lemma [quot_respect]:
  10.377 +  shows "(op \<sim> ===> op =) freediscrim freediscrim"
  10.378 +  by (auto simp add: msgrel_imp_eq_freediscrim)
  10.379 +
  10.380 +lemma discrim_Nonce [simp]: 
  10.381 +  shows "discrim (Nonce N) = 0"
  10.382 +  by (lifting freediscrim.simps(1))
  10.383 +
  10.384 +lemma discrim_MPair [simp]: 
  10.385 +  shows "discrim (MPair X Y) = 1"
  10.386 +  by (lifting freediscrim.simps(2))
  10.387 +
  10.388 +lemma discrim_Crypt [simp]: 
  10.389 +  shows "discrim (Crypt K X) = discrim X + 2"
  10.390 +  by (lifting freediscrim.simps(3))
  10.391 +
  10.392 +lemma discrim_Decrypt [simp]: 
  10.393 +  shows "discrim (Decrypt K X) = discrim X - 2"
  10.394 +  by (lifting freediscrim.simps(4))
  10.395 +
  10.396 +end
  10.397 +
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Quotient_Examples/LarryInt.thy	Fri Feb 19 13:54:19 2010 +0100
    11.3 @@ -0,0 +1,395 @@
    11.4 +
    11.5 +header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
    11.6 +
    11.7 +theory LarryInt
    11.8 +imports Main Quotient_Product
    11.9 +begin
   11.10 +
   11.11 +fun
   11.12 +  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 
   11.13 +where
   11.14 +  "intrel (x, y) (u, v) = (x + v = u + y)"
   11.15 +
   11.16 +quotient_type int = "nat \<times> nat" / intrel
   11.17 +  by (auto simp add: equivp_def expand_fun_eq)
   11.18 +
   11.19 +instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
   11.20 +begin
   11.21 +
   11.22 +quotient_definition
   11.23 +  Zero_int_def: "0::int" is "(0::nat, 0::nat)"
   11.24 +
   11.25 +quotient_definition
   11.26 +  One_int_def: "1::int" is "(1::nat, 0::nat)"
   11.27 +
   11.28 +definition
   11.29 +  "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
   11.30 +
   11.31 +quotient_definition
   11.32 +  "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 
   11.33 +is
   11.34 +  "add_raw"
   11.35 +
   11.36 +definition
   11.37 +  "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
   11.38 +
   11.39 +quotient_definition
   11.40 +  "uminus :: int \<Rightarrow> int" 
   11.41 +is
   11.42 +  "uminus_raw"
   11.43 +
   11.44 +fun
   11.45 +  mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
   11.46 +where
   11.47 +  "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
   11.48 +
   11.49 +quotient_definition
   11.50 +  "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 
   11.51 +is
   11.52 +  "mult_raw"
   11.53 +
   11.54 +definition
   11.55 +  "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
   11.56 +
   11.57 +quotient_definition 
   11.58 +  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 
   11.59 +is
   11.60 +  "le_raw"
   11.61 +
   11.62 +definition
   11.63 +  less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
   11.64 +
   11.65 +definition
   11.66 +  diff_int_def:  "z - (w::int) \<equiv> z + (-w)"
   11.67 +
   11.68 +instance ..
   11.69 +
   11.70 +end
   11.71 +
   11.72 +subsection{*Construction of the Integers*}
   11.73 +
   11.74 +lemma zminus_zminus_raw:
   11.75 +  "uminus_raw (uminus_raw z) = z"
   11.76 +  by (cases z) (simp add: uminus_raw_def)
   11.77 +
   11.78 +lemma [quot_respect]:
   11.79 +  shows "(intrel ===> intrel) uminus_raw uminus_raw"
   11.80 +  by (simp add: uminus_raw_def)
   11.81 +  
   11.82 +lemma zminus_zminus:
   11.83 +  fixes z::"int"
   11.84 +  shows "- (- z) = z"
   11.85 +  by(lifting zminus_zminus_raw)
   11.86 +
   11.87 +lemma zminus_0_raw:
   11.88 +  shows "uminus_raw (0, 0) = (0, 0::nat)"
   11.89 +  by (simp add: uminus_raw_def)
   11.90 +
   11.91 +lemma zminus_0: 
   11.92 +  shows "- 0 = (0::int)"
   11.93 +  by (lifting zminus_0_raw)
   11.94 +
   11.95 +subsection{*Integer Addition*}
   11.96 +
   11.97 +lemma zminus_zadd_distrib_raw:
   11.98 +  shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"
   11.99 +by (cases z, cases w)
  11.100 +   (auto simp add: add_raw_def uminus_raw_def)
  11.101 +
  11.102 +lemma [quot_respect]:
  11.103 +  shows "(intrel ===> intrel ===> intrel) add_raw add_raw"
  11.104 +by (simp add: add_raw_def)
  11.105 +
  11.106 +lemma zminus_zadd_distrib: 
  11.107 +  fixes z w::"int"
  11.108 +  shows "- (z + w) = (- z) + (- w)"
  11.109 +  by(lifting zminus_zadd_distrib_raw)
  11.110 +
  11.111 +lemma zadd_commute_raw:
  11.112 +  shows "add_raw z w = add_raw w z"
  11.113 +by (cases z, cases w)
  11.114 +   (simp add: add_raw_def)
  11.115 +
  11.116 +lemma zadd_commute:
  11.117 +  fixes z w::"int"
  11.118 +  shows "(z::int) + w = w + z"
  11.119 +  by (lifting zadd_commute_raw)
  11.120 +
  11.121 +lemma zadd_assoc_raw:
  11.122 +  shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
  11.123 +  by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
  11.124 +
  11.125 +lemma zadd_assoc: 
  11.126 +  fixes z1 z2 z3::"int"
  11.127 +  shows "(z1 + z2) + z3 = z1 + (z2 + z3)"
  11.128 +  by (lifting zadd_assoc_raw)
  11.129 +
  11.130 +lemma zadd_0_raw:
  11.131 +  shows "add_raw (0, 0) z = z"
  11.132 +  by (simp add: add_raw_def)
  11.133 +
  11.134 +
  11.135 +text {*also for the instance declaration int :: plus_ac0*}
  11.136 +lemma zadd_0: 
  11.137 +  fixes z::"int"
  11.138 +  shows "0 + z = z"
  11.139 +  by (lifting zadd_0_raw)
  11.140 +
  11.141 +lemma zadd_zminus_inverse_raw:
  11.142 +  shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
  11.143 +  by (cases z) (simp add: add_raw_def uminus_raw_def)
  11.144 +
  11.145 +lemma zadd_zminus_inverse2: 
  11.146 +  fixes z::"int"
  11.147 +  shows "(- z) + z = 0"
  11.148 +  by (lifting zadd_zminus_inverse_raw)
  11.149 +
  11.150 +subsection{*Integer Multiplication*}
  11.151 +
  11.152 +lemma zmult_zminus_raw:
  11.153 +  shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
  11.154 +apply(cases z, cases w)
  11.155 +apply(simp add: uminus_raw_def)
  11.156 +done
  11.157 +
  11.158 +lemma mult_raw_fst:
  11.159 +  assumes a: "intrel x z"
  11.160 +  shows "intrel (mult_raw x y) (mult_raw z y)"
  11.161 +using a
  11.162 +apply(cases x, cases y, cases z)
  11.163 +apply(auto simp add: mult_raw.simps intrel.simps)
  11.164 +apply(rename_tac u v w x y z)
  11.165 +apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
  11.166 +apply(simp add: mult_ac)
  11.167 +apply(simp add: add_mult_distrib [symmetric])
  11.168 +done
  11.169 +
  11.170 +lemma mult_raw_snd:
  11.171 +  assumes a: "intrel x z"
  11.172 +  shows "intrel (mult_raw y x) (mult_raw y z)"
  11.173 +using a
  11.174 +apply(cases x, cases y, cases z)
  11.175 +apply(auto simp add: mult_raw.simps intrel.simps)
  11.176 +apply(rename_tac u v w x y z)
  11.177 +apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
  11.178 +apply(simp add: mult_ac)
  11.179 +apply(simp add: add_mult_distrib [symmetric])
  11.180 +done
  11.181 +
  11.182 +lemma [quot_respect]:
  11.183 +  shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
  11.184 +apply(simp only: fun_rel_def)
  11.185 +apply(rule allI | rule impI)+
  11.186 +apply(rule equivp_transp[OF int_equivp])
  11.187 +apply(rule mult_raw_fst)
  11.188 +apply(assumption)
  11.189 +apply(rule mult_raw_snd)
  11.190 +apply(assumption)
  11.191 +done
  11.192 +
  11.193 +lemma zmult_zminus: 
  11.194 +  fixes z w::"int"
  11.195 +  shows "(- z) * w = - (z * w)"
  11.196 +  by (lifting zmult_zminus_raw)
  11.197 +
  11.198 +lemma zmult_commute_raw: 
  11.199 +  shows "mult_raw z w = mult_raw w z"
  11.200 +apply(cases z, cases w)
  11.201 +apply(simp add: add_ac mult_ac)
  11.202 +done
  11.203 +
  11.204 +lemma zmult_commute: 
  11.205 +  fixes z w::"int"
  11.206 +  shows "z * w = w * z"
  11.207 +  by (lifting zmult_commute_raw)
  11.208 +
  11.209 +lemma zmult_assoc_raw:
  11.210 +  shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
  11.211 +apply(cases z1, cases z2, cases z3)
  11.212 +apply(simp add: add_mult_distrib2 mult_ac)
  11.213 +done
  11.214 +
  11.215 +lemma zmult_assoc: 
  11.216 +  fixes z1 z2 z3::"int"
  11.217 +  shows "(z1 * z2) * z3 = z1 * (z2 * z3)"
  11.218 +  by (lifting zmult_assoc_raw)
  11.219 +
  11.220 +lemma zadd_mult_distrib_raw:
  11.221 +  shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
  11.222 +apply(cases z1, cases z2, cases w)
  11.223 +apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
  11.224 +done
  11.225 +
  11.226 +lemma zadd_zmult_distrib: 
  11.227 +  fixes z1 z2 w::"int"
  11.228 +  shows "(z1 + z2) * w = (z1 * w) + (z2 * w)"
  11.229 +  by(lifting zadd_mult_distrib_raw)
  11.230 +
  11.231 +lemma zadd_zmult_distrib2: 
  11.232 +  fixes w z1 z2::"int"
  11.233 +  shows "w * (z1 + z2) = (w * z1) + (w * z2)"
  11.234 +  by (simp add: zmult_commute [of w] zadd_zmult_distrib)
  11.235 +
  11.236 +lemma zdiff_zmult_distrib: 
  11.237 +  fixes w z1 z2::"int"
  11.238 +  shows "(z1 - z2) * w = (z1 * w) - (z2 * w)"
  11.239 +  by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
  11.240 +
  11.241 +lemma zdiff_zmult_distrib2: 
  11.242 +  fixes w z1 z2::"int"
  11.243 +  shows "w * (z1 - z2) = (w * z1) - (w * z2)"
  11.244 +  by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
  11.245 +
  11.246 +lemmas int_distrib =
  11.247 +  zadd_zmult_distrib zadd_zmult_distrib2
  11.248 +  zdiff_zmult_distrib zdiff_zmult_distrib2
  11.249 +
  11.250 +lemma zmult_1_raw:
  11.251 +  shows "mult_raw (1, 0) z = z"
  11.252 +  by (cases z) (auto)
  11.253 +
  11.254 +lemma zmult_1:
  11.255 +  fixes z::"int"
  11.256 +  shows "1 * z = z"
  11.257 +  by (lifting zmult_1_raw)
  11.258 +
  11.259 +lemma zmult_1_right: 
  11.260 +  fixes z::"int"
  11.261 +  shows "z * 1 = z"
  11.262 +  by (rule trans [OF zmult_commute zmult_1])
  11.263 +
  11.264 +lemma zero_not_one:
  11.265 +  shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
  11.266 +  by auto
  11.267 +
  11.268 +text{*The Integers Form A Ring*}
  11.269 +instance int :: comm_ring_1
  11.270 +proof
  11.271 +  fix i j k :: int
  11.272 +  show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
  11.273 +  show "i + j = j + i" by (simp add: zadd_commute)
  11.274 +  show "0 + i = i" by (rule zadd_0)
  11.275 +  show "- i + i = 0" by (rule zadd_zminus_inverse2)
  11.276 +  show "i - j = i + (-j)" by (simp add: diff_int_def)
  11.277 +  show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
  11.278 +  show "i * j = j * i" by (rule zmult_commute)
  11.279 +  show "1 * i = i" by (rule zmult_1) 
  11.280 +  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
  11.281 +  show "0 \<noteq> (1::int)" by (lifting zero_not_one)
  11.282 +qed
  11.283 +
  11.284 +
  11.285 +subsection{*The @{text "\<le>"} Ordering*}
  11.286 +
  11.287 +lemma zle_refl_raw:
  11.288 +  shows "le_raw w w"
  11.289 +  by (cases w) (simp add: le_raw_def)
  11.290 +
  11.291 +lemma [quot_respect]:
  11.292 +  shows "(intrel ===> intrel ===> op =) le_raw le_raw"
  11.293 +  by (auto) (simp_all add: le_raw_def)
  11.294 +
  11.295 +lemma zle_refl: 
  11.296 +  fixes w::"int"
  11.297 +  shows "w \<le> w"
  11.298 +  by (lifting zle_refl_raw)
  11.299 +
  11.300 +
  11.301 +lemma zle_trans_raw:
  11.302 +  shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
  11.303 +apply(cases i, cases j, cases k)
  11.304 +apply(auto simp add: le_raw_def)
  11.305 +done
  11.306 +
  11.307 +lemma zle_trans: 
  11.308 +  fixes i j k::"int"
  11.309 +  shows "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"
  11.310 +  by (lifting zle_trans_raw)
  11.311 +
  11.312 +lemma zle_anti_sym_raw:
  11.313 +  shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
  11.314 +apply(cases z, cases w)
  11.315 +apply(auto iff: le_raw_def)
  11.316 +done
  11.317 +
  11.318 +lemma zle_anti_sym: 
  11.319 +  fixes z w::"int"
  11.320 +  shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = w"
  11.321 +  by (lifting zle_anti_sym_raw)
  11.322 +
  11.323 +
  11.324 +(* Axiom 'order_less_le' of class 'order': *)
  11.325 +lemma zless_le: 
  11.326 +  fixes w z::"int"
  11.327 +  shows "(w < z) = (w \<le> z & w \<noteq> z)"
  11.328 +  by (simp add: less_int_def)
  11.329 +
  11.330 +instance int :: order
  11.331 +apply (default)
  11.332 +apply(auto simp add: zless_le zle_anti_sym)[1]
  11.333 +apply(rule zle_refl)
  11.334 +apply(erule zle_trans, assumption)
  11.335 +apply(erule zle_anti_sym, assumption)
  11.336 +done
  11.337 +
  11.338 +(* Axiom 'linorder_linear' of class 'linorder': *)
  11.339 +
  11.340 +lemma zle_linear_raw:
  11.341 +  shows "le_raw z w \<or> le_raw w z"
  11.342 +apply(cases w, cases z)
  11.343 +apply(auto iff: le_raw_def)
  11.344 +done
  11.345 +
  11.346 +lemma zle_linear: 
  11.347 +  fixes z w::"int"
  11.348 +  shows "z \<le> w \<or> w \<le> z"
  11.349 +  by (lifting zle_linear_raw)
  11.350 +
  11.351 +instance int :: linorder
  11.352 +apply(default)
  11.353 +apply(rule zle_linear)
  11.354 +done
  11.355 +
  11.356 +lemma zadd_left_mono_raw:
  11.357 +  shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
  11.358 +apply(cases k)
  11.359 +apply(auto simp add: add_raw_def le_raw_def)
  11.360 +done
  11.361 +
  11.362 +lemma zadd_left_mono: 
  11.363 +  fixes i j::"int"
  11.364 +  shows "i \<le> j \<Longrightarrow> k + i \<le> k + j"
  11.365 +  by (lifting zadd_left_mono_raw)
  11.366 +
  11.367 +
  11.368 +subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
  11.369 +
  11.370 +definition
  11.371 +  "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
  11.372 +
  11.373 +quotient_definition
  11.374 +  "nat2::int \<Rightarrow> nat"
  11.375 +is
  11.376 +  "nat_raw"
  11.377 +
  11.378 +abbreviation
  11.379 +  "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))"
  11.380 +
  11.381 +lemma nat_le_eq_zle_raw:
  11.382 +  shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
  11.383 +  apply (cases w)
  11.384 +  apply (cases z)
  11.385 +  apply (simp add: nat_raw_def le_raw_def)
  11.386 +  by auto
  11.387 +
  11.388 +lemma [quot_respect]:
  11.389 +  shows "(intrel ===> op =) nat_raw nat_raw"
  11.390 +  by (auto iff: nat_raw_def)
  11.391 +
  11.392 +lemma nat_le_eq_zle: 
  11.393 +  fixes w z::"int"
  11.394 +  shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
  11.395 +  unfolding less_int_def
  11.396 +  by (lifting nat_le_eq_zle_raw)
  11.397 +
  11.398 +end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Quotient_Examples/ROOT.ML	Fri Feb 19 13:54:19 2010 +0100
    12.3 @@ -0,0 +1,8 @@
    12.4 +(*  Title:      HOL/Quotient_Examples/ROOT.ML
    12.5 +    Author:     Cezary Kaliszyk and Christian Urban
    12.6 +
    12.7 +Testing the quotient package.
    12.8 +*)
    12.9 +
   12.10 +use_thys ["LarryInt", "LarryDatatype"];
   12.11 +
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Feb 19 13:54:19 2010 +0100
    13.3 @@ -0,0 +1,110 @@
    13.4 +(*  Title:      quotient_def.thy
    13.5 +    Author:     Cezary Kaliszyk and Christian Urban
    13.6 +
    13.7 +    Definitions for constants on quotient types.
    13.8 +
    13.9 +*)
   13.10 +
   13.11 +signature QUOTIENT_DEF =
   13.12 +sig
   13.13 +  val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->
   13.14 +    local_theory -> (term * thm) * local_theory
   13.15 +
   13.16 +  val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
   13.17 +    local_theory -> (term * thm) * local_theory
   13.18 +
   13.19 +  val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory
   13.20 +end;
   13.21 +
   13.22 +structure Quotient_Def: QUOTIENT_DEF =
   13.23 +struct
   13.24 +
   13.25 +open Quotient_Info;
   13.26 +open Quotient_Term;
   13.27 +
   13.28 +(** Interface and Syntax Setup **)
   13.29 +
   13.30 +(* The ML-interface for a quotient definition takes
   13.31 +   as argument:
   13.32 +
   13.33 +    - an optional binding and mixfix annotation
   13.34 +    - attributes
   13.35 +    - the new constant as term
   13.36 +    - the rhs of the definition as term
   13.37 +
   13.38 +   It returns the defined constant and its definition
   13.39 +   theorem; stores the data in the qconsts data slot.
   13.40 +
   13.41 +   Restriction: At the moment the right-hand side of the
   13.42 +   definition must be a constant. Similarly the left-hand 
   13.43 +   side must be a constant.
   13.44 +*)
   13.45 +fun error_msg bind str = 
   13.46 +let 
   13.47 +  val name = Binding.name_of bind
   13.48 +  val pos = Position.str_of (Binding.pos_of bind)
   13.49 +in
   13.50 +  error ("Head of quotient_definition " ^ 
   13.51 +    (quote str) ^ " differs from declaration " ^ name ^ pos)
   13.52 +end
   13.53 +
   13.54 +fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
   13.55 +let
   13.56 +  val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
   13.57 +  val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
   13.58 +  
   13.59 +  fun sanity_test NONE _ = true
   13.60 +    | sanity_test (SOME bind) str =
   13.61 +        if Name.of_binding bind = str then true
   13.62 +        else error_msg bind str
   13.63 +
   13.64 +  val _ = sanity_test optbind lhs_str
   13.65 +
   13.66 +  val qconst_bname = Binding.name lhs_str
   13.67 +  val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
   13.68 +  val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
   13.69 +  val (_, prop') = LocalDefs.cert_def lthy prop
   13.70 +  val (_, newrhs) = Primitive_Defs.abs_def prop'
   13.71 +
   13.72 +  val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
   13.73 +
   13.74 +  (* data storage *)
   13.75 +  fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
   13.76 +  fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
   13.77 +  val lthy'' = Local_Theory.declaration true
   13.78 +                 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
   13.79 +in
   13.80 +  ((trm, thm), lthy'')
   13.81 +end
   13.82 +
   13.83 +fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
   13.84 +let
   13.85 +  val lhs = Syntax.read_term lthy lhs_str
   13.86 +  val rhs = Syntax.read_term lthy rhs_str
   13.87 +  val lthy' = Variable.declare_term lhs lthy
   13.88 +  val lthy'' = Variable.declare_term rhs lthy'
   13.89 +in
   13.90 +  quotient_def (decl, (attr, (lhs, rhs))) lthy''
   13.91 +end
   13.92 +
   13.93 +fun quotient_lift_const (b, t) ctxt =
   13.94 +  quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
   13.95 +    (Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt
   13.96 +
   13.97 +local
   13.98 +  structure P = OuterParse;
   13.99 +in
  13.100 +
  13.101 +val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where"
  13.102 +
  13.103 +val quotdef_parser =
  13.104 +  Scan.optional quotdef_decl (NONE, NoSyn) -- 
  13.105 +    P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
  13.106 +end
  13.107 +
  13.108 +val _ =
  13.109 +  OuterSyntax.local_theory "quotient_definition"
  13.110 +    "definition for constants over the quotient type"
  13.111 +      OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
  13.112 +
  13.113 +end; (* structure *)
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Feb 19 13:54:19 2010 +0100
    14.3 @@ -0,0 +1,289 @@
    14.4 +(*  Title:      quotient_info.thy
    14.5 +    Author:     Cezary Kaliszyk and Christian Urban
    14.6 +
    14.7 +    Data slots for the quotient package.
    14.8 +
    14.9 +*)
   14.10 +
   14.11 +
   14.12 +signature QUOTIENT_INFO =
   14.13 +sig
   14.14 +  exception NotFound
   14.15 +
   14.16 +  type maps_info = {mapfun: string, relmap: string}
   14.17 +  val maps_defined: theory -> string -> bool
   14.18 +  val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)
   14.19 +  val maps_update_thy: string -> maps_info -> theory -> theory
   14.20 +  val maps_update: string -> maps_info -> Proof.context -> Proof.context
   14.21 +  val print_mapsinfo: Proof.context -> unit
   14.22 +
   14.23 +  type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
   14.24 +  val transform_quotdata: morphism -> quotdata_info -> quotdata_info
   14.25 +  val quotdata_lookup_raw: theory -> string -> quotdata_info option
   14.26 +  val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
   14.27 +  val quotdata_update_thy: string -> quotdata_info -> theory -> theory
   14.28 +  val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
   14.29 +  val quotdata_dest: Proof.context -> quotdata_info list
   14.30 +  val print_quotinfo: Proof.context -> unit
   14.31 +
   14.32 +  type qconsts_info = {qconst: term, rconst: term, def: thm}
   14.33 +  val transform_qconsts: morphism -> qconsts_info -> qconsts_info
   14.34 +  val qconsts_lookup: theory -> term -> qconsts_info     (* raises NotFound *)
   14.35 +  val qconsts_update_thy: string -> qconsts_info -> theory -> theory
   14.36 +  val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
   14.37 +  val qconsts_dest: Proof.context -> qconsts_info list
   14.38 +  val print_qconstinfo: Proof.context -> unit
   14.39 +
   14.40 +  val equiv_rules_get: Proof.context -> thm list
   14.41 +  val equiv_rules_add: attribute
   14.42 +  val rsp_rules_get: Proof.context -> thm list
   14.43 +  val prs_rules_get: Proof.context -> thm list
   14.44 +  val id_simps_get: Proof.context -> thm list
   14.45 +  val quotient_rules_get: Proof.context -> thm list
   14.46 +  val quotient_rules_add: attribute
   14.47 +end;
   14.48 +
   14.49 +
   14.50 +structure Quotient_Info: QUOTIENT_INFO =
   14.51 +struct
   14.52 +
   14.53 +exception NotFound
   14.54 +
   14.55 +
   14.56 +(** data containers **)
   14.57 +
   14.58 +(* info about map- and rel-functions for a type *)
   14.59 +type maps_info = {mapfun: string, relmap: string}
   14.60 +
   14.61 +structure MapsData = Theory_Data
   14.62 +  (type T = maps_info Symtab.table
   14.63 +   val empty = Symtab.empty
   14.64 +   val extend = I
   14.65 +   val merge = Symtab.merge (K true))
   14.66 +
   14.67 +fun maps_defined thy s =
   14.68 +  Symtab.defined (MapsData.get thy) s
   14.69 +
   14.70 +fun maps_lookup thy s =
   14.71 +  case (Symtab.lookup (MapsData.get thy) s) of
   14.72 +    SOME map_fun => map_fun
   14.73 +  | NONE => raise NotFound
   14.74 +
   14.75 +fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
   14.76 +fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
   14.77 +
   14.78 +fun maps_attribute_aux s minfo = Thm.declaration_attribute
   14.79 +  (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
   14.80 +
   14.81 +(* attribute to be used in declare statements *)
   14.82 +fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
   14.83 +let
   14.84 +  val thy = ProofContext.theory_of ctxt
   14.85 +  val tyname = Sign.intern_type thy tystr
   14.86 +  val mapname = Sign.intern_const thy mapstr
   14.87 +  val relname = Sign.intern_const thy relstr
   14.88 +
   14.89 +  fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
   14.90 +  val _ = List.app sanity_check [mapname, relname]
   14.91 +in
   14.92 +  maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
   14.93 +end
   14.94 +
   14.95 +val maps_attr_parser =
   14.96 +  Args.context -- Scan.lift
   14.97 +    ((Args.name --| OuterParse.$$$ "=") --
   14.98 +      (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
   14.99 +        Args.name --| OuterParse.$$$ ")"))
  14.100 +
  14.101 +val _ = Context.>> (Context.map_theory
  14.102 +  (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
  14.103 +    "declaration of map information"))
  14.104 +
  14.105 +fun print_mapsinfo ctxt =
  14.106 +let
  14.107 +  fun prt_map (ty_name, {mapfun, relmap}) =
  14.108 +    Pretty.block (Library.separate (Pretty.brk 2)
  14.109 +      (map Pretty.str
  14.110 +        ["type:", ty_name,
  14.111 +        "map:", mapfun,
  14.112 +        "relation map:", relmap]))
  14.113 +in
  14.114 +  MapsData.get (ProofContext.theory_of ctxt)
  14.115 +  |> Symtab.dest
  14.116 +  |> map (prt_map)
  14.117 +  |> Pretty.big_list "maps for type constructors:"
  14.118 +  |> Pretty.writeln
  14.119 +end
  14.120 +
  14.121 +
  14.122 +(* info about quotient types *)
  14.123 +type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
  14.124 +
  14.125 +structure QuotData = Theory_Data
  14.126 +  (type T = quotdata_info Symtab.table
  14.127 +   val empty = Symtab.empty
  14.128 +   val extend = I
  14.129 +   val merge = Symtab.merge (K true))
  14.130 +
  14.131 +fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
  14.132 +  {qtyp = Morphism.typ phi qtyp,
  14.133 +   rtyp = Morphism.typ phi rtyp,
  14.134 +   equiv_rel = Morphism.term phi equiv_rel,
  14.135 +   equiv_thm = Morphism.thm phi equiv_thm}
  14.136 +
  14.137 +fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str
  14.138 +
  14.139 +fun quotdata_lookup thy str =
  14.140 +  case Symtab.lookup (QuotData.get thy) str of
  14.141 +    SOME qinfo => qinfo
  14.142 +  | NONE => raise NotFound
  14.143 +
  14.144 +fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
  14.145 +fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
  14.146 +
  14.147 +fun quotdata_dest lthy =
  14.148 +  map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy)))
  14.149 +
  14.150 +fun print_quotinfo ctxt =
  14.151 +let
  14.152 +  fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
  14.153 +    Pretty.block (Library.separate (Pretty.brk 2)
  14.154 +     [Pretty.str "quotient type:",
  14.155 +      Syntax.pretty_typ ctxt qtyp,
  14.156 +      Pretty.str "raw type:",
  14.157 +      Syntax.pretty_typ ctxt rtyp,
  14.158 +      Pretty.str "relation:",
  14.159 +      Syntax.pretty_term ctxt equiv_rel,
  14.160 +      Pretty.str "equiv. thm:",
  14.161 +      Syntax.pretty_term ctxt (prop_of equiv_thm)])
  14.162 +in
  14.163 +  QuotData.get (ProofContext.theory_of ctxt)
  14.164 +  |> Symtab.dest
  14.165 +  |> map (prt_quot o snd)
  14.166 +  |> Pretty.big_list "quotients:"
  14.167 +  |> Pretty.writeln
  14.168 +end
  14.169 +
  14.170 +
  14.171 +(* info about quotient constants *)
  14.172 +type qconsts_info = {qconst: term, rconst: term, def: thm}
  14.173 +
  14.174 +fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y
  14.175 +
  14.176 +(* We need to be able to lookup instances of lifted constants,
  14.177 +   for example given "nat fset" we need to find "'a fset";
  14.178 +   but overloaded constants share the same name *)
  14.179 +structure QConstsData = Theory_Data
  14.180 +  (type T = (qconsts_info list) Symtab.table
  14.181 +   val empty = Symtab.empty
  14.182 +   val extend = I
  14.183 +   val merge = Symtab.merge_list qconsts_info_eq)
  14.184 +
  14.185 +fun transform_qconsts phi {qconst, rconst, def} =
  14.186 +  {qconst = Morphism.term phi qconst,
  14.187 +   rconst = Morphism.term phi rconst,
  14.188 +   def = Morphism.thm phi def}
  14.189 +
  14.190 +fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo))
  14.191 +fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I
  14.192 +
  14.193 +fun qconsts_dest lthy =
  14.194 +  flat (map snd (Symtab.dest (QConstsData.get (ProofContext.theory_of lthy))))
  14.195 +
  14.196 +fun qconsts_lookup thy t =
  14.197 +  let
  14.198 +    val (name, qty) = dest_Const t
  14.199 +    fun matches x =
  14.200 +      let
  14.201 +        val (name', qty') = dest_Const (#qconst x);
  14.202 +      in
  14.203 +        name = name' andalso Sign.typ_instance thy (qty, qty')
  14.204 +      end
  14.205 +  in
  14.206 +    case Symtab.lookup (QConstsData.get thy) name of
  14.207 +      NONE => raise NotFound
  14.208 +    | SOME l =>
  14.209 +      (case (find_first matches l) of
  14.210 +        SOME x => x
  14.211 +      | NONE => raise NotFound)
  14.212 +  end
  14.213 +
  14.214 +fun print_qconstinfo ctxt =
  14.215 +let
  14.216 +  fun prt_qconst {qconst, rconst, def} =
  14.217 +    Pretty.block (separate (Pretty.brk 1)
  14.218 +     [Syntax.pretty_term ctxt qconst,
  14.219 +      Pretty.str ":=",
  14.220 +      Syntax.pretty_term ctxt rconst,
  14.221 +      Pretty.str "as",
  14.222 +      Syntax.pretty_term ctxt (prop_of def)])
  14.223 +in
  14.224 +  QConstsData.get (ProofContext.theory_of ctxt)
  14.225 +  |> Symtab.dest
  14.226 +  |> map snd
  14.227 +  |> flat
  14.228 +  |> map prt_qconst
  14.229 +  |> Pretty.big_list "quotient constants:"
  14.230 +  |> Pretty.writeln
  14.231 +end
  14.232 +
  14.233 +(* equivalence relation theorems *)
  14.234 +structure EquivRules = Named_Thms
  14.235 +  (val name = "quot_equiv"
  14.236 +   val description = "Equivalence relation theorems.")
  14.237 +
  14.238 +val equiv_rules_get = EquivRules.get
  14.239 +val equiv_rules_add = EquivRules.add
  14.240 +
  14.241 +(* respectfulness theorems *)
  14.242 +structure RspRules = Named_Thms
  14.243 +  (val name = "quot_respect"
  14.244 +   val description = "Respectfulness theorems.")
  14.245 +
  14.246 +val rsp_rules_get = RspRules.get
  14.247 +
  14.248 +(* preservation theorems *)
  14.249 +structure PrsRules = Named_Thms
  14.250 +  (val name = "quot_preserve"
  14.251 +   val description = "Preservation theorems.")
  14.252 +
  14.253 +val prs_rules_get = PrsRules.get
  14.254 +
  14.255 +(* id simplification theorems *)
  14.256 +structure IdSimps = Named_Thms
  14.257 +  (val name = "id_simps"
  14.258 +   val description = "Identity simp rules for maps.")
  14.259 +
  14.260 +val id_simps_get = IdSimps.get
  14.261 +
  14.262 +(* quotient theorems *)
  14.263 +structure QuotientRules = Named_Thms
  14.264 +  (val name = "quot_thm"
  14.265 +   val description = "Quotient theorems.")
  14.266 +
  14.267 +val quotient_rules_get = QuotientRules.get
  14.268 +val quotient_rules_add = QuotientRules.add
  14.269 +
  14.270 +(* setup of the theorem lists *)
  14.271 +
  14.272 +val _ = Context.>> (Context.map_theory
  14.273 +  (EquivRules.setup #>
  14.274 +   RspRules.setup #>
  14.275 +   PrsRules.setup #>
  14.276 +   IdSimps.setup #>
  14.277 +   QuotientRules.setup))
  14.278 +
  14.279 +(* setup of the printing commands *)
  14.280 +
  14.281 +fun improper_command (pp_fn, cmd_name, descr_str) =
  14.282 +  OuterSyntax.improper_command cmd_name descr_str
  14.283 +    OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
  14.284 +
  14.285 +val _ = map improper_command
  14.286 +  [(print_mapsinfo, "print_maps", "prints out all map functions"),
  14.287 +   (print_quotinfo, "print_quotients", "prints out all quotients"),
  14.288 +   (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
  14.289 +
  14.290 +
  14.291 +end; (* structure *)
  14.292 +
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Feb 19 13:54:19 2010 +0100
    15.3 @@ -0,0 +1,665 @@
    15.4 +(*  Title:      quotient_tacs.thy
    15.5 +    Author:     Cezary Kaliszyk and Christian Urban
    15.6 +
    15.7 +    Tactics for solving goal arising from lifting
    15.8 +    theorems to quotient types.
    15.9 +*)
   15.10 +
   15.11 +signature QUOTIENT_TACS =
   15.12 +sig
   15.13 +  val regularize_tac: Proof.context -> int -> tactic
   15.14 +  val injection_tac: Proof.context -> int -> tactic
   15.15 +  val all_injection_tac: Proof.context -> int -> tactic
   15.16 +  val clean_tac: Proof.context -> int -> tactic
   15.17 +  val procedure_tac: Proof.context -> thm -> int -> tactic
   15.18 +  val lift_tac: Proof.context -> thm list -> int -> tactic
   15.19 +  val quotient_tac: Proof.context -> int -> tactic
   15.20 +  val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
   15.21 +  val lifted_attrib: attribute
   15.22 +end;
   15.23 +
   15.24 +structure Quotient_Tacs: QUOTIENT_TACS =
   15.25 +struct
   15.26 +
   15.27 +open Quotient_Info;
   15.28 +open Quotient_Term;
   15.29 +
   15.30 +
   15.31 +(** various helper fuctions **)
   15.32 +
   15.33 +(* Since HOL_basic_ss is too "big" for us, we *)
   15.34 +(* need to set up our own minimal simpset.    *)
   15.35 +fun mk_minimal_ss ctxt =
   15.36 +  Simplifier.context ctxt empty_ss
   15.37 +    setsubgoaler asm_simp_tac
   15.38 +    setmksimps (mksimps [])
   15.39 +
   15.40 +(* composition of two theorems, used in maps *)
   15.41 +fun OF1 thm1 thm2 = thm2 RS thm1
   15.42 +
   15.43 +(* prints a warning, if the subgoal is not solved *)
   15.44 +fun WARN (tac, msg) i st =
   15.45 + case Seq.pull (SOLVED' tac i st) of
   15.46 +     NONE    => (warning msg; Seq.single st)
   15.47 +   | seqcell => Seq.make (fn () => seqcell)
   15.48 +
   15.49 +fun RANGE_WARN tacs = RANGE (map WARN tacs)
   15.50 +
   15.51 +fun atomize_thm thm =
   15.52 +let
   15.53 +  val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
   15.54 +  val thm'' = ObjectLogic.atomize (cprop_of thm')
   15.55 +in
   15.56 +  @{thm equal_elim_rule1} OF [thm'', thm']
   15.57 +end
   15.58 +
   15.59 +
   15.60 +
   15.61 +(*** Regularize Tactic ***)
   15.62 +
   15.63 +(** solvers for equivp and quotient assumptions **)
   15.64 +
   15.65 +fun equiv_tac ctxt =
   15.66 +  REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
   15.67 +
   15.68 +fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
   15.69 +val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
   15.70 +
   15.71 +fun quotient_tac ctxt =
   15.72 +  (REPEAT_ALL_NEW (FIRST'
   15.73 +    [rtac @{thm identity_quotient},
   15.74 +     resolve_tac (quotient_rules_get ctxt)]))
   15.75 +
   15.76 +fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
   15.77 +val quotient_solver =
   15.78 +  Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
   15.79 +
   15.80 +fun solve_quotient_assm ctxt thm =
   15.81 +  case Seq.pull (quotient_tac ctxt 1 thm) of
   15.82 +    SOME (t, _) => t
   15.83 +  | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
   15.84 +
   15.85 +
   15.86 +fun prep_trm thy (x, (T, t)) =
   15.87 +  (cterm_of thy (Var (x, T)), cterm_of thy t)
   15.88 +
   15.89 +fun prep_ty thy (x, (S, ty)) =
   15.90 +  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
   15.91 +
   15.92 +fun get_match_inst thy pat trm =
   15.93 +let
   15.94 +  val univ = Unify.matchers thy [(pat, trm)]
   15.95 +  val SOME (env, _) = Seq.pull univ             (* raises BIND, if no unifier *)
   15.96 +  val tenv = Vartab.dest (Envir.term_env env)
   15.97 +  val tyenv = Vartab.dest (Envir.type_env env)
   15.98 +in
   15.99 +  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
  15.100 +end
  15.101 +
  15.102 +(* Calculates the instantiations for the lemmas:
  15.103 +
  15.104 +      ball_reg_eqv_range and bex_reg_eqv_range
  15.105 +
  15.106 +   Since the left-hand-side contains a non-pattern '?P (f ?x)'
  15.107 +   we rely on unification/instantiation to check whether the
  15.108 +   theorem applies and return NONE if it doesn't.
  15.109 +*)
  15.110 +fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
  15.111 +let
  15.112 +  val thy = ProofContext.theory_of ctxt
  15.113 +  fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
  15.114 +  val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
  15.115 +  val trm_inst = map (SOME o cterm_of thy) [R2, R1]
  15.116 +in
  15.117 +  case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
  15.118 +    NONE => NONE
  15.119 +  | SOME thm' =>
  15.120 +      (case try (get_match_inst thy (get_lhs thm')) redex of
  15.121 +        NONE => NONE
  15.122 +      | SOME inst2 => try (Drule.instantiate inst2) thm')
  15.123 +end
  15.124 +
  15.125 +fun ball_bex_range_simproc ss redex =
  15.126 +let
  15.127 +  val ctxt = Simplifier.the_context ss
  15.128 +in
  15.129 +  case redex of
  15.130 +    (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
  15.131 +      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
  15.132 +        calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
  15.133 +
  15.134 +  | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
  15.135 +      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
  15.136 +        calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
  15.137 +
  15.138 +  | _ => NONE
  15.139 +end
  15.140 +
  15.141 +(* Regularize works as follows:
  15.142 +
  15.143 +  0. preliminary simplification step according to
  15.144 +     ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
  15.145 +
  15.146 +  1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
  15.147 +
  15.148 +  2. monos
  15.149 +
  15.150 +  3. commutation rules for ball and bex (ball_all_comm bex_ex_comm)
  15.151 +
  15.152 +  4. then rel-equalities, which need to be instantiated with 'eq_imp_rel'
  15.153 +     to avoid loops
  15.154 +
  15.155 +  5. then simplification like 0
  15.156 +
  15.157 +  finally jump back to 1
  15.158 +*)
  15.159 +
  15.160 +fun regularize_tac ctxt =
  15.161 +let
  15.162 +  val thy = ProofContext.theory_of ctxt
  15.163 +  val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
  15.164 +  val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
  15.165 +  val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
  15.166 +  val simpset = (mk_minimal_ss ctxt)
  15.167 +                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
  15.168 +                       addsimprocs [simproc]
  15.169 +                       addSolver equiv_solver addSolver quotient_solver
  15.170 +  val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
  15.171 +  val eq_eqvs = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
  15.172 +in
  15.173 +  simp_tac simpset THEN'
  15.174 +  REPEAT_ALL_NEW (CHANGED o FIRST'
  15.175 +    [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
  15.176 +     resolve_tac (Inductive.get_monos ctxt),
  15.177 +     resolve_tac @{thms ball_all_comm bex_ex_comm},
  15.178 +     resolve_tac eq_eqvs,
  15.179 +     simp_tac simpset])
  15.180 +end
  15.181 +
  15.182 +
  15.183 +
  15.184 +(*** Injection Tactic ***)
  15.185 +
  15.186 +(* Looks for Quot_True assumptions, and in case its parameter
  15.187 +   is an application, it returns the function and the argument.
  15.188 +*)
  15.189 +fun find_qt_asm asms =
  15.190 +let
  15.191 +  fun find_fun trm =
  15.192 +    case trm of
  15.193 +      (Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
  15.194 +    | _ => false
  15.195 +in
  15.196 + case find_first find_fun asms of
  15.197 +   SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
  15.198 + | _ => NONE
  15.199 +end
  15.200 +
  15.201 +fun quot_true_simple_conv ctxt fnctn ctrm =
  15.202 +  case (term_of ctrm) of
  15.203 +    (Const (@{const_name Quot_True}, _) $ x) =>
  15.204 +    let
  15.205 +      val fx = fnctn x;
  15.206 +      val thy = ProofContext.theory_of ctxt;
  15.207 +      val cx = cterm_of thy x;
  15.208 +      val cfx = cterm_of thy fx;
  15.209 +      val cxt = ctyp_of thy (fastype_of x);
  15.210 +      val cfxt = ctyp_of thy (fastype_of fx);
  15.211 +      val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
  15.212 +    in
  15.213 +      Conv.rewr_conv thm ctrm
  15.214 +    end
  15.215 +
  15.216 +fun quot_true_conv ctxt fnctn ctrm =
  15.217 +  case (term_of ctrm) of
  15.218 +    (Const (@{const_name Quot_True}, _) $ _) =>
  15.219 +      quot_true_simple_conv ctxt fnctn ctrm
  15.220 +  | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
  15.221 +  | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
  15.222 +  | _ => Conv.all_conv ctrm
  15.223 +
  15.224 +fun quot_true_tac ctxt fnctn =
  15.225 +   CONVERSION
  15.226 +    ((Conv.params_conv ~1 (fn ctxt =>
  15.227 +       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
  15.228 +
  15.229 +fun dest_comb (f $ a) = (f, a)
  15.230 +fun dest_bcomb ((_ $ l) $ r) = (l, r)
  15.231 +
  15.232 +fun unlam t =
  15.233 +  case t of
  15.234 +    (Abs a) => snd (Term.dest_abs a)
  15.235 +  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
  15.236 +
  15.237 +fun dest_fun_type (Type("fun", [T, S])) = (T, S)
  15.238 +  | dest_fun_type _ = error "dest_fun_type"
  15.239 +
  15.240 +val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
  15.241 +
  15.242 +(* We apply apply_rsp only in case if the type needs lifting.
  15.243 +   This is the case if the type of the data in the Quot_True
  15.244 +   assumption is different from the corresponding type in the goal.
  15.245 +*)
  15.246 +val apply_rsp_tac =
  15.247 +  Subgoal.FOCUS (fn {concl, asms, context,...} =>
  15.248 +  let
  15.249 +    val bare_concl = HOLogic.dest_Trueprop (term_of concl)
  15.250 +    val qt_asm = find_qt_asm (map term_of asms)
  15.251 +  in
  15.252 +    case (bare_concl, qt_asm) of
  15.253 +      (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
  15.254 +         if fastype_of qt_fun = fastype_of f
  15.255 +         then no_tac
  15.256 +         else
  15.257 +           let
  15.258 +             val ty_x = fastype_of x
  15.259 +             val ty_b = fastype_of qt_arg
  15.260 +             val ty_f = range_type (fastype_of f)
  15.261 +             val thy = ProofContext.theory_of context
  15.262 +             val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
  15.263 +             val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
  15.264 +             val inst_thm = Drule.instantiate' ty_inst
  15.265 +               ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
  15.266 +           in
  15.267 +             (rtac inst_thm THEN' quotient_tac context) 1
  15.268 +           end
  15.269 +    | _ => no_tac
  15.270 +  end)
  15.271 +
  15.272 +(* Instantiates and applies 'equals_rsp'. Since the theorem is
  15.273 +   complex we rely on instantiation to tell us if it applies
  15.274 +*)
  15.275 +fun equals_rsp_tac R ctxt =
  15.276 +let
  15.277 +  val thy = ProofContext.theory_of ctxt
  15.278 +in
  15.279 +  case try (cterm_of thy) R of (* There can be loose bounds in R *)
  15.280 +    SOME ctm =>
  15.281 +      let
  15.282 +        val ty = domain_type (fastype_of R)
  15.283 +      in
  15.284 +        case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
  15.285 +          [SOME (cterm_of thy R)]) @{thm equals_rsp} of
  15.286 +          SOME thm => rtac thm THEN' quotient_tac ctxt
  15.287 +        | NONE => K no_tac
  15.288 +      end
  15.289 +  | _ => K no_tac
  15.290 +end
  15.291 +
  15.292 +fun rep_abs_rsp_tac ctxt =
  15.293 +  SUBGOAL (fn (goal, i) =>
  15.294 +    case (try bare_concl goal) of
  15.295 +      SOME (rel $ _ $ (rep $ (abs $ _))) =>
  15.296 +        let
  15.297 +          val thy = ProofContext.theory_of ctxt;
  15.298 +          val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
  15.299 +          val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
  15.300 +        in
  15.301 +          case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
  15.302 +            SOME t_inst =>
  15.303 +              (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
  15.304 +                SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
  15.305 +              | NONE => no_tac)
  15.306 +          | NONE => no_tac
  15.307 +        end
  15.308 +    | _ => no_tac)
  15.309 +
  15.310 +
  15.311 +
  15.312 +(* Injection means to prove that the regularised theorem implies
  15.313 +   the abs/rep injected one.
  15.314 +
  15.315 +   The deterministic part:
  15.316 +    - remove lambdas from both sides
  15.317 +    - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
  15.318 +    - prove Ball/Bex relations unfolding fun_rel_id
  15.319 +    - reflexivity of equality
  15.320 +    - prove equality of relations using equals_rsp
  15.321 +    - use user-supplied RSP theorems
  15.322 +    - solve 'relation of relations' goals using quot_rel_rsp
  15.323 +    - remove rep_abs from the right side
  15.324 +      (Lambdas under respects may have left us some assumptions)
  15.325 +
  15.326 +   Then in order:
  15.327 +    - split applications of lifted type (apply_rsp)
  15.328 +    - split applications of non-lifted type (cong_tac)
  15.329 +    - apply extentionality
  15.330 +    - assumption
  15.331 +    - reflexivity of the relation
  15.332 +*)
  15.333 +fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
  15.334 +(case (bare_concl goal) of
  15.335 +    (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
  15.336 +  (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
  15.337 +      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
  15.338 +
  15.339 +    (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
  15.340 +| (Const (@{const_name "op ="},_) $
  15.341 +    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
  15.342 +    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
  15.343 +      => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
  15.344 +
  15.345 +    (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
  15.346 +| (Const (@{const_name fun_rel}, _) $ _ $ _) $
  15.347 +    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
  15.348 +    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
  15.349 +      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
  15.350 +
  15.351 +    (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
  15.352 +| Const (@{const_name "op ="},_) $
  15.353 +    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
  15.354 +    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
  15.355 +      => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
  15.356 +
  15.357 +    (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
  15.358 +| (Const (@{const_name fun_rel}, _) $ _ $ _) $
  15.359 +    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
  15.360 +    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
  15.361 +      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
  15.362 +
  15.363 +| (Const (@{const_name fun_rel}, _) $ _ $ _) $
  15.364 +    (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
  15.365 +      => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
  15.366 +
  15.367 +| (_ $
  15.368 +    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
  15.369 +    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
  15.370 +      => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
  15.371 +
  15.372 +| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
  15.373 +   (rtac @{thm refl} ORELSE'
  15.374 +    (equals_rsp_tac R ctxt THEN' RANGE [
  15.375 +       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
  15.376 +
  15.377 +    (* reflexivity of operators arising from Cong_tac *)
  15.378 +| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
  15.379 +
  15.380 +   (* respectfulness of constants; in particular of a simple relation *)
  15.381 +| _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
  15.382 +    => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
  15.383 +
  15.384 +    (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
  15.385 +    (* observe fun_map *)
  15.386 +| _ $ _ $ _
  15.387 +    => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
  15.388 +       ORELSE' rep_abs_rsp_tac ctxt
  15.389 +
  15.390 +| _ => K no_tac
  15.391 +) i)
  15.392 +
  15.393 +fun injection_step_tac ctxt rel_refl =
  15.394 + FIRST' [
  15.395 +    injection_match_tac ctxt,
  15.396 +
  15.397 +    (* R (t $ ...) (t' $ ...) ----> apply_rsp   provided type of t needs lifting *)
  15.398 +    apply_rsp_tac ctxt THEN'
  15.399 +                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
  15.400 +
  15.401 +    (* (op =) (t $ ...) (t' $ ...) ----> Cong   provided type of t does not need lifting *)
  15.402 +    (* merge with previous tactic *)
  15.403 +    Cong_Tac.cong_tac @{thm cong} THEN'
  15.404 +                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
  15.405 +
  15.406 +    (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
  15.407 +    rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
  15.408 +
  15.409 +    (* resolving with R x y assumptions *)
  15.410 +    atac,
  15.411 +
  15.412 +    (* reflexivity of the basic relations *)
  15.413 +    (* R ... ... *)
  15.414 +    resolve_tac rel_refl]
  15.415 +
  15.416 +fun injection_tac ctxt =
  15.417 +let
  15.418 +  val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
  15.419 +in
  15.420 +  injection_step_tac ctxt rel_refl
  15.421 +end
  15.422 +
  15.423 +fun all_injection_tac ctxt =
  15.424 +  REPEAT_ALL_NEW (injection_tac ctxt)
  15.425 +
  15.426 +
  15.427 +
  15.428 +(*** Cleaning of the Theorem ***)
  15.429 +
  15.430 +(* expands all fun_maps, except in front of the (bound) variables listed in xs *)
  15.431 +fun fun_map_simple_conv xs ctrm =
  15.432 +  case (term_of ctrm) of
  15.433 +    ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
  15.434 +        if member (op=) xs h
  15.435 +        then Conv.all_conv ctrm
  15.436 +        else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm
  15.437 +  | _ => Conv.all_conv ctrm
  15.438 +
  15.439 +fun fun_map_conv xs ctxt ctrm =
  15.440 +  case (term_of ctrm) of
  15.441 +      _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
  15.442 +                fun_map_simple_conv xs) ctrm
  15.443 +    | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
  15.444 +    | _ => Conv.all_conv ctrm
  15.445 +
  15.446 +fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
  15.447 +
  15.448 +(* custom matching functions *)
  15.449 +fun mk_abs u i t =
  15.450 +  if incr_boundvars i u aconv t then Bound i else
  15.451 +  case t of
  15.452 +    t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
  15.453 +  | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
  15.454 +  | Bound j => if i = j then error "make_inst" else t
  15.455 +  | _ => t
  15.456 +
  15.457 +fun make_inst lhs t =
  15.458 +let
  15.459 +  val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
  15.460 +  val _ $ (Abs (_, _, (_ $ g))) = t;
  15.461 +in
  15.462 +  (f, Abs ("x", T, mk_abs u 0 g))
  15.463 +end
  15.464 +
  15.465 +fun make_inst_id lhs t =
  15.466 +let
  15.467 +  val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
  15.468 +  val _ $ (Abs (_, _, g)) = t;
  15.469 +in
  15.470 +  (f, Abs ("x", T, mk_abs u 0 g))
  15.471 +end
  15.472 +
  15.473 +(* Simplifies a redex using the 'lambda_prs' theorem.
  15.474 +   First instantiates the types and known subterms.
  15.475 +   Then solves the quotient assumptions to get Rep2 and Abs1
  15.476 +   Finally instantiates the function f using make_inst
  15.477 +   If Rep2 is an identity then the pattern is simpler and
  15.478 +   make_inst_id is used
  15.479 +*)
  15.480 +fun lambda_prs_simple_conv ctxt ctrm =
  15.481 +  case (term_of ctrm) of
  15.482 +    (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
  15.483 +      let
  15.484 +        val thy = ProofContext.theory_of ctxt
  15.485 +        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
  15.486 +        val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
  15.487 +        val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
  15.488 +        val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
  15.489 +        val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
  15.490 +        val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
  15.491 +        val thm3 = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
  15.492 +        val (insp, inst) =
  15.493 +          if ty_c = ty_d
  15.494 +          then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
  15.495 +          else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
  15.496 +        val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
  15.497 +      in
  15.498 +        Conv.rewr_conv thm4 ctrm
  15.499 +      end
  15.500 +  | _ => Conv.all_conv ctrm
  15.501 +
  15.502 +fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
  15.503 +fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
  15.504 +
  15.505 +
  15.506 +(* Cleaning consists of:
  15.507 +
  15.508 +  1. unfolding of ---> in front of everything, except
  15.509 +     bound variables (this prevents lambda_prs from
  15.510 +     becoming stuck)
  15.511 +
  15.512 +  2. simplification with lambda_prs
  15.513 +
  15.514 +  3. simplification with:
  15.515 +
  15.516 +      - Quotient_abs_rep Quotient_rel_rep
  15.517 +        babs_prs all_prs ex_prs ex1_prs
  15.518 +
  15.519 +      - id_simps and preservation lemmas and
  15.520 +
  15.521 +      - symmetric versions of the definitions
  15.522 +        (that is definitions of quotient constants
  15.523 +         are folded)
  15.524 +
  15.525 +  4. test for refl
  15.526 +*)
  15.527 +fun clean_tac lthy =
  15.528 +let
  15.529 +  val defs = map (symmetric o #def) (qconsts_dest lthy)
  15.530 +  val prs = prs_rules_get lthy
  15.531 +  val ids = id_simps_get lthy
  15.532 +  val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
  15.533 +
  15.534 +  val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
  15.535 +in
  15.536 +  EVERY' [fun_map_tac lthy,
  15.537 +          lambda_prs_tac lthy,
  15.538 +          simp_tac ss,
  15.539 +          TRY o rtac refl]
  15.540 +end
  15.541 +
  15.542 +
  15.543 +
  15.544 +(** Tactic for Generalising Free Variables in a Goal **)
  15.545 +
  15.546 +fun inst_spec ctrm =
  15.547 +   Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
  15.548 +
  15.549 +fun inst_spec_tac ctrms =
  15.550 +  EVERY' (map (dtac o inst_spec) ctrms)
  15.551 +
  15.552 +fun all_list xs trm =
  15.553 +  fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
  15.554 +
  15.555 +fun apply_under_Trueprop f =
  15.556 +  HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
  15.557 +
  15.558 +fun gen_frees_tac ctxt =
  15.559 +  SUBGOAL (fn (concl, i) =>
  15.560 +    let
  15.561 +      val thy = ProofContext.theory_of ctxt
  15.562 +      val vrs = Term.add_frees concl []
  15.563 +      val cvrs = map (cterm_of thy o Free) vrs
  15.564 +      val concl' = apply_under_Trueprop (all_list vrs) concl
  15.565 +      val goal = Logic.mk_implies (concl', concl)
  15.566 +      val rule = Goal.prove ctxt [] [] goal
  15.567 +        (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
  15.568 +    in
  15.569 +      rtac rule i
  15.570 +    end)
  15.571 +
  15.572 +
  15.573 +(** The General Shape of the Lifting Procedure **)
  15.574 +
  15.575 +(* - A is the original raw theorem
  15.576 +   - B is the regularized theorem
  15.577 +   - C is the rep/abs injected version of B
  15.578 +   - D is the lifted theorem
  15.579 +
  15.580 +   - 1st prem is the regularization step
  15.581 +   - 2nd prem is the rep/abs injection step
  15.582 +   - 3rd prem is the cleaning part
  15.583 +
  15.584 +   the Quot_True premise in 2nd records the lifted theorem
  15.585 +*)
  15.586 +val lifting_procedure_thm =
  15.587 +  @{lemma  "[|A;
  15.588 +              A --> B;
  15.589 +              Quot_True D ==> B = C;
  15.590 +              C = D|] ==> D"
  15.591 +      by (simp add: Quot_True_def)}
  15.592 +
  15.593 +fun lift_match_error ctxt msg rtrm qtrm =
  15.594 +let
  15.595 +  val rtrm_str = Syntax.string_of_term ctxt rtrm
  15.596 +  val qtrm_str = Syntax.string_of_term ctxt qtrm
  15.597 +  val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
  15.598 +    "", "does not match with original theorem", rtrm_str]
  15.599 +in
  15.600 +  error msg
  15.601 +end
  15.602 +
  15.603 +fun procedure_inst ctxt rtrm qtrm =
  15.604 +let
  15.605 +  val thy = ProofContext.theory_of ctxt
  15.606 +  val rtrm' = HOLogic.dest_Trueprop rtrm
  15.607 +  val qtrm' = HOLogic.dest_Trueprop qtrm
  15.608 +  val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
  15.609 +    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
  15.610 +  val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
  15.611 +    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
  15.612 +in
  15.613 +  Drule.instantiate' []
  15.614 +    [SOME (cterm_of thy rtrm'),
  15.615 +     SOME (cterm_of thy reg_goal),
  15.616 +     NONE,
  15.617 +     SOME (cterm_of thy inj_goal)] lifting_procedure_thm
  15.618 +end
  15.619 +
  15.620 +(* the tactic leaves three subgoals to be proved *)
  15.621 +fun procedure_tac ctxt rthm =
  15.622 +  ObjectLogic.full_atomize_tac
  15.623 +  THEN' gen_frees_tac ctxt
  15.624 +  THEN' SUBGOAL (fn (goal, i) =>
  15.625 +    let
  15.626 +      val rthm' = atomize_thm rthm
  15.627 +      val rule = procedure_inst ctxt (prop_of rthm') goal
  15.628 +    in
  15.629 +      (rtac rule THEN' rtac rthm') i
  15.630 +    end)
  15.631 +
  15.632 +
  15.633 +(* Automatic Proofs *)
  15.634 +
  15.635 +val msg1 = "The regularize proof failed."
  15.636 +val msg2 = cat_lines ["The injection proof failed.",
  15.637 +                      "This is probably due to missing respects lemmas.",
  15.638 +                      "Try invoking the injection method manually to see",
  15.639 +                      "which lemmas are missing."]
  15.640 +val msg3 = "The cleaning proof failed."
  15.641 +
  15.642 +fun lift_tac ctxt rthms =
  15.643 +let
  15.644 +  fun mk_tac rthm =
  15.645 +    procedure_tac ctxt rthm
  15.646 +    THEN' RANGE_WARN
  15.647 +      [(regularize_tac ctxt, msg1),
  15.648 +       (all_injection_tac ctxt, msg2),
  15.649 +       (clean_tac ctxt, msg3)]
  15.650 +in
  15.651 +  simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
  15.652 +  THEN' RANGE (map mk_tac rthms)
  15.653 +end
  15.654 +
  15.655 +(* An Attribute which automatically constructs the qthm *)
  15.656 +fun lifted_attrib_aux context thm =
  15.657 +let
  15.658 +  val ctxt = Context.proof_of context
  15.659 +  val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
  15.660 +  val goal = (quotient_lift_all ctxt' o prop_of) thm'
  15.661 +in
  15.662 +  Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm] 1))
  15.663 +  |> singleton (ProofContext.export ctxt' ctxt)
  15.664 +end;
  15.665 +
  15.666 +val lifted_attrib = Thm.rule_attribute lifted_attrib_aux
  15.667 +
  15.668 +end; (* structure *)
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Feb 19 13:54:19 2010 +0100
    16.3 @@ -0,0 +1,786 @@
    16.4 +(*  Title:      quotient_term.thy
    16.5 +    Author:     Cezary Kaliszyk and Christian Urban
    16.6 +
    16.7 +    Constructs terms corresponding to goals from
    16.8 +    lifting theorems to quotient types.
    16.9 +*)
   16.10 +
   16.11 +signature QUOTIENT_TERM =
   16.12 +sig
   16.13 +  exception LIFT_MATCH of string
   16.14 +
   16.15 +  datatype flag = AbsF | RepF
   16.16 +
   16.17 +  val absrep_fun: flag -> Proof.context -> typ * typ -> term
   16.18 +  val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
   16.19 +
   16.20 +  (* Allows Nitpick to represent quotient types as single elements from raw type *)
   16.21 +  val absrep_const_chk: flag -> Proof.context -> string -> term
   16.22 +
   16.23 +  val equiv_relation: Proof.context -> typ * typ -> term
   16.24 +  val equiv_relation_chk: Proof.context -> typ * typ -> term
   16.25 +
   16.26 +  val regularize_trm: Proof.context -> term * term -> term
   16.27 +  val regularize_trm_chk: Proof.context -> term * term -> term
   16.28 +
   16.29 +  val inj_repabs_trm: Proof.context -> term * term -> term
   16.30 +  val inj_repabs_trm_chk: Proof.context -> term * term -> term
   16.31 +
   16.32 +  val quotient_lift_const: string * term -> local_theory -> term
   16.33 +  val quotient_lift_all: Proof.context -> term -> term
   16.34 +end;
   16.35 +
   16.36 +structure Quotient_Term: QUOTIENT_TERM =
   16.37 +struct
   16.38 +
   16.39 +open Quotient_Info;
   16.40 +
   16.41 +exception LIFT_MATCH of string
   16.42 +
   16.43 +
   16.44 +
   16.45 +(*** Aggregate Rep/Abs Function ***)
   16.46 +
   16.47 +
   16.48 +(* The flag RepF is for types in negative position; AbsF is for types
   16.49 +   in positive position. Because of this, function types need to be
   16.50 +   treated specially, since there the polarity changes.
   16.51 +*)
   16.52 +
   16.53 +datatype flag = AbsF | RepF
   16.54 +
   16.55 +fun negF AbsF = RepF
   16.56 +  | negF RepF = AbsF
   16.57 +
   16.58 +fun is_identity (Const (@{const_name "id"}, _)) = true
   16.59 +  | is_identity _ = false
   16.60 +
   16.61 +fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
   16.62 +
   16.63 +fun mk_fun_compose flag (trm1, trm2) =
   16.64 +  case flag of
   16.65 +    AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
   16.66 +  | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
   16.67 +
   16.68 +fun get_mapfun ctxt s =
   16.69 +let
   16.70 +  val thy = ProofContext.theory_of ctxt
   16.71 +  val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
   16.72 +  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
   16.73 +in
   16.74 +  Const (mapfun, dummyT)
   16.75 +end
   16.76 +
   16.77 +(* makes a Free out of a TVar *)
   16.78 +fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
   16.79 +
   16.80 +(* produces an aggregate map function for the
   16.81 +   rty-part of a quotient definition; abstracts
   16.82 +   over all variables listed in vs (these variables
   16.83 +   correspond to the type variables in rty)
   16.84 +
   16.85 +   for example for: (?'a list * ?'b)
   16.86 +   it produces:     %a b. prod_map (map a) b
   16.87 +*)
   16.88 +fun mk_mapfun ctxt vs rty =
   16.89 +let
   16.90 +  val vs' = map (mk_Free) vs
   16.91 +
   16.92 +  fun mk_mapfun_aux rty =
   16.93 +    case rty of
   16.94 +      TVar _ => mk_Free rty
   16.95 +    | Type (_, []) => mk_identity rty
   16.96 +    | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
   16.97 +    | _ => raise LIFT_MATCH "mk_mapfun (default)"
   16.98 +in
   16.99 +  fold_rev Term.lambda vs' (mk_mapfun_aux rty)
  16.100 +end
  16.101 +
  16.102 +(* looks up the (varified) rty and qty for
  16.103 +   a quotient definition
  16.104 +*)
  16.105 +fun get_rty_qty ctxt s =
  16.106 +let
  16.107 +  val thy = ProofContext.theory_of ctxt
  16.108 +  val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
  16.109 +  val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
  16.110 +in
  16.111 +  (#rtyp qdata, #qtyp qdata)
  16.112 +end
  16.113 +
  16.114 +(* takes two type-environments and looks
  16.115 +   up in both of them the variable v, which
  16.116 +   must be listed in the environment
  16.117 +*)
  16.118 +fun double_lookup rtyenv qtyenv v =
  16.119 +let
  16.120 +  val v' = fst (dest_TVar v)
  16.121 +in
  16.122 +  (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
  16.123 +end
  16.124 +
  16.125 +(* matches a type pattern with a type *)
  16.126 +fun match ctxt err ty_pat ty =
  16.127 +let
  16.128 +  val thy = ProofContext.theory_of ctxt
  16.129 +in
  16.130 +  Sign.typ_match thy (ty_pat, ty) Vartab.empty
  16.131 +  handle MATCH_TYPE => err ctxt ty_pat ty
  16.132 +end
  16.133 +
  16.134 +(* produces the rep or abs constant for a qty *)
  16.135 +fun absrep_const flag ctxt qty_str =
  16.136 +let
  16.137 +  val thy = ProofContext.theory_of ctxt
  16.138 +  val qty_name = Long_Name.base_name qty_str
  16.139 +in
  16.140 +  case flag of
  16.141 +    AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
  16.142 +  | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
  16.143 +end
  16.144 +
  16.145 +(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
  16.146 +fun absrep_const_chk flag ctxt qty_str =
  16.147 +  Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
  16.148 +
  16.149 +fun absrep_match_err ctxt ty_pat ty =
  16.150 +let
  16.151 +  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
  16.152 +  val ty_str = Syntax.string_of_typ ctxt ty
  16.153 +in
  16.154 +  raise LIFT_MATCH (space_implode " "
  16.155 +    ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
  16.156 +end
  16.157 +
  16.158 +
  16.159 +(** generation of an aggregate absrep function **)
  16.160 +
  16.161 +(* - In case of equal types we just return the identity.
  16.162 +
  16.163 +   - In case of TFrees we also return the identity.
  16.164 +
  16.165 +   - In case of function types we recurse taking
  16.166 +     the polarity change into account.
  16.167 +
  16.168 +   - If the type constructors are equal, we recurse for the
  16.169 +     arguments and build the appropriate map function.
  16.170 +
  16.171 +   - If the type constructors are unequal, there must be an
  16.172 +     instance of quotient types:
  16.173 +
  16.174 +       - we first look up the corresponding rty_pat and qty_pat
  16.175 +         from the quotient definition; the arguments of qty_pat
  16.176 +         must be some distinct TVars
  16.177 +       - we then match the rty_pat with rty and qty_pat with qty;
  16.178 +         if matching fails the types do not correspond -> error
  16.179 +       - the matching produces two environments; we look up the
  16.180 +         assignments for the qty_pat variables and recurse on the
  16.181 +         assignments
  16.182 +       - we prefix the aggregate map function for the rty_pat,
  16.183 +         which is an abstraction over all type variables
  16.184 +       - finally we compose the result with the appropriate
  16.185 +         absrep function in case at least one argument produced
  16.186 +         a non-identity function /
  16.187 +         otherwise we just return the appropriate absrep
  16.188 +         function
  16.189 +
  16.190 +     The composition is necessary for types like
  16.191 +
  16.192 +        ('a list) list / ('a foo) foo
  16.193 +
  16.194 +     The matching is necessary for types like
  16.195 +
  16.196 +        ('a * 'a) list / 'a bar
  16.197 +
  16.198 +     The test is necessary in order to eliminate superfluous
  16.199 +     identity maps.
  16.200 +*)
  16.201 +
  16.202 +fun absrep_fun flag ctxt (rty, qty) =
  16.203 +  if rty = qty
  16.204 +  then mk_identity rty
  16.205 +  else
  16.206 +    case (rty, qty) of
  16.207 +      (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
  16.208 +        let
  16.209 +          val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
  16.210 +          val arg2 = absrep_fun flag ctxt (ty2, ty2')
  16.211 +        in
  16.212 +          list_comb (get_mapfun ctxt "fun", [arg1, arg2])
  16.213 +        end
  16.214 +    | (Type (s, tys), Type (s', tys')) =>
  16.215 +        if s = s'
  16.216 +        then
  16.217 +           let
  16.218 +             val args = map (absrep_fun flag ctxt) (tys ~~ tys')
  16.219 +           in
  16.220 +             list_comb (get_mapfun ctxt s, args)
  16.221 +           end
  16.222 +        else
  16.223 +           let
  16.224 +             val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
  16.225 +             val rtyenv = match ctxt absrep_match_err rty_pat rty
  16.226 +             val qtyenv = match ctxt absrep_match_err qty_pat qty
  16.227 +             val args_aux = map (double_lookup rtyenv qtyenv) vs
  16.228 +             val args = map (absrep_fun flag ctxt) args_aux
  16.229 +             val map_fun = mk_mapfun ctxt vs rty_pat
  16.230 +             val result = list_comb (map_fun, args)
  16.231 +           in
  16.232 +             if forall is_identity args
  16.233 +             then absrep_const flag ctxt s'
  16.234 +             else mk_fun_compose flag (absrep_const flag ctxt s', result)
  16.235 +           end
  16.236 +    | (TFree x, TFree x') =>
  16.237 +        if x = x'
  16.238 +        then mk_identity rty
  16.239 +        else raise (LIFT_MATCH "absrep_fun (frees)")
  16.240 +    | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
  16.241 +    | _ => raise (LIFT_MATCH "absrep_fun (default)")
  16.242 +
  16.243 +fun absrep_fun_chk flag ctxt (rty, qty) =
  16.244 +  absrep_fun flag ctxt (rty, qty)
  16.245 +  |> Syntax.check_term ctxt
  16.246 +
  16.247 +
  16.248 +
  16.249 +
  16.250 +(*** Aggregate Equivalence Relation ***)
  16.251 +
  16.252 +
  16.253 +(* works very similar to the absrep generation,
  16.254 +   except there is no need for polarities
  16.255 +*)
  16.256 +
  16.257 +(* instantiates TVars so that the term is of type ty *)
  16.258 +fun force_typ ctxt trm ty =
  16.259 +let
  16.260 +  val thy = ProofContext.theory_of ctxt
  16.261 +  val trm_ty = fastype_of trm
  16.262 +  val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
  16.263 +in
  16.264 +  map_types (Envir.subst_type ty_inst) trm
  16.265 +end
  16.266 +
  16.267 +fun is_eq (Const (@{const_name "op ="}, _)) = true
  16.268 +  | is_eq _ = false
  16.269 +
  16.270 +fun mk_rel_compose (trm1, trm2) =
  16.271 +  Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
  16.272 +
  16.273 +fun get_relmap ctxt s =
  16.274 +let
  16.275 +  val thy = ProofContext.theory_of ctxt
  16.276 +  val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
  16.277 +  val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
  16.278 +in
  16.279 +  Const (relmap, dummyT)
  16.280 +end
  16.281 +
  16.282 +fun mk_relmap ctxt vs rty =
  16.283 +let
  16.284 +  val vs' = map (mk_Free) vs
  16.285 +
  16.286 +  fun mk_relmap_aux rty =
  16.287 +    case rty of
  16.288 +      TVar _ => mk_Free rty
  16.289 +    | Type (_, []) => HOLogic.eq_const rty
  16.290 +    | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
  16.291 +    | _ => raise LIFT_MATCH ("mk_relmap (default)")
  16.292 +in
  16.293 +  fold_rev Term.lambda vs' (mk_relmap_aux rty)
  16.294 +end
  16.295 +
  16.296 +fun get_equiv_rel ctxt s =
  16.297 +let
  16.298 +  val thy = ProofContext.theory_of ctxt
  16.299 +  val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
  16.300 +in
  16.301 +  #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
  16.302 +end
  16.303 +
  16.304 +fun equiv_match_err ctxt ty_pat ty =
  16.305 +let
  16.306 +  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
  16.307 +  val ty_str = Syntax.string_of_typ ctxt ty
  16.308 +in
  16.309 +  raise LIFT_MATCH (space_implode " "
  16.310 +    ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
  16.311 +end
  16.312 +
  16.313 +(* builds the aggregate equivalence relation
  16.314 +   that will be the argument of Respects
  16.315 +*)
  16.316 +fun equiv_relation ctxt (rty, qty) =
  16.317 +  if rty = qty
  16.318 +  then HOLogic.eq_const rty
  16.319 +  else
  16.320 +    case (rty, qty) of
  16.321 +      (Type (s, tys), Type (s', tys')) =>
  16.322 +       if s = s'
  16.323 +       then
  16.324 +         let
  16.325 +           val args = map (equiv_relation ctxt) (tys ~~ tys')
  16.326 +         in
  16.327 +           list_comb (get_relmap ctxt s, args)
  16.328 +         end
  16.329 +       else
  16.330 +         let
  16.331 +           val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
  16.332 +           val rtyenv = match ctxt equiv_match_err rty_pat rty
  16.333 +           val qtyenv = match ctxt equiv_match_err qty_pat qty
  16.334 +           val args_aux = map (double_lookup rtyenv qtyenv) vs
  16.335 +           val args = map (equiv_relation ctxt) args_aux
  16.336 +           val rel_map = mk_relmap ctxt vs rty_pat
  16.337 +           val result = list_comb (rel_map, args)
  16.338 +           val eqv_rel = get_equiv_rel ctxt s'
  16.339 +           val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
  16.340 +         in
  16.341 +           if forall is_eq args
  16.342 +           then eqv_rel'
  16.343 +           else mk_rel_compose (result, eqv_rel')
  16.344 +         end
  16.345 +      | _ => HOLogic.eq_const rty
  16.346 +
  16.347 +fun equiv_relation_chk ctxt (rty, qty) =
  16.348 +  equiv_relation ctxt (rty, qty)
  16.349 +  |> Syntax.check_term ctxt
  16.350 +
  16.351 +
  16.352 +
  16.353 +(*** Regularization ***)
  16.354 +
  16.355 +(* Regularizing an rtrm means:
  16.356 +
  16.357 + - Quantifiers over types that need lifting are replaced
  16.358 +   by bounded quantifiers, for example:
  16.359 +
  16.360 +      All P  ----> All (Respects R) P
  16.361 +
  16.362 +   where the aggregate relation R is given by the rty and qty;
  16.363 +
  16.364 + - Abstractions over types that need lifting are replaced
  16.365 +   by bounded abstractions, for example:
  16.366 +
  16.367 +      %x. P  ----> Ball (Respects R) %x. P
  16.368 +
  16.369 + - Equalities over types that need lifting are replaced by
  16.370 +   corresponding equivalence relations, for example:
  16.371 +
  16.372 +      A = B  ----> R A B
  16.373 +
  16.374 +   or
  16.375 +
  16.376 +      A = B  ----> (R ===> R) A B
  16.377 +
  16.378 +   for more complicated types of A and B
  16.379 +
  16.380 +
  16.381 + The regularize_trm accepts raw theorems in which equalities
  16.382 + and quantifiers match exactly the ones in the lifted theorem
  16.383 + but also accepts partially regularized terms.
  16.384 +
  16.385 + This means that the raw theorems can have:
  16.386 +   Ball (Respects R),  Bex (Respects R), Bex1_rel (Respects R), Babs, R
  16.387 + in the places where:
  16.388 +   All, Ex, Ex1, %, (op =)
  16.389 + is required the lifted theorem.
  16.390 +
  16.391 +*)
  16.392 +
  16.393 +val mk_babs = Const (@{const_name Babs}, dummyT)
  16.394 +val mk_ball = Const (@{const_name Ball}, dummyT)
  16.395 +val mk_bex  = Const (@{const_name Bex}, dummyT)
  16.396 +val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
  16.397 +val mk_resp = Const (@{const_name Respects}, dummyT)
  16.398 +
  16.399 +(* - applies f to the subterm of an abstraction,
  16.400 +     otherwise to the given term,
  16.401 +   - used by regularize, therefore abstracted
  16.402 +     variables do not have to be treated specially
  16.403 +*)
  16.404 +fun apply_subt f (trm1, trm2) =
  16.405 +  case (trm1, trm2) of
  16.406 +    (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
  16.407 +  | _ => f (trm1, trm2)
  16.408 +
  16.409 +fun term_mismatch str ctxt t1 t2 =
  16.410 +let
  16.411 +  val t1_str = Syntax.string_of_term ctxt t1
  16.412 +  val t2_str = Syntax.string_of_term ctxt t2
  16.413 +  val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
  16.414 +  val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
  16.415 +in
  16.416 +  raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
  16.417 +end
  16.418 +
  16.419 +(* the major type of All and Ex quantifiers *)
  16.420 +fun qnt_typ ty = domain_type (domain_type ty)
  16.421 +
  16.422 +(* Checks that two types match, for example:
  16.423 +     rty -> rty   matches   qty -> qty *)
  16.424 +fun matches_typ thy rT qT =
  16.425 +  if rT = qT then true else
  16.426 +  case (rT, qT) of
  16.427 +    (Type (rs, rtys), Type (qs, qtys)) =>
  16.428 +      if rs = qs then
  16.429 +        if length rtys <> length qtys then false else
  16.430 +        forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
  16.431 +      else
  16.432 +        (case Quotient_Info.quotdata_lookup_raw thy qs of
  16.433 +          SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
  16.434 +        | NONE => false)
  16.435 +  | _ => false
  16.436 +
  16.437 +
  16.438 +(* produces a regularized version of rtrm
  16.439 +
  16.440 +   - the result might contain dummyTs
  16.441 +
  16.442 +   - for regularisation we do not need any
  16.443 +     special treatment of bound variables
  16.444 +*)
  16.445 +fun regularize_trm ctxt (rtrm, qtrm) =
  16.446 +  case (rtrm, qtrm) of
  16.447 +    (Abs (x, ty, t), Abs (_, ty', t')) =>
  16.448 +       let
  16.449 +         val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
  16.450 +       in
  16.451 +         if ty = ty' then subtrm
  16.452 +         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
  16.453 +       end
  16.454 +  | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
  16.455 +       let
  16.456 +         val subtrm = regularize_trm ctxt (t, t')
  16.457 +         val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
  16.458 +       in
  16.459 +         if resrel <> needres
  16.460 +         then term_mismatch "regularize (Babs)" ctxt resrel needres
  16.461 +         else mk_babs $ resrel $ subtrm
  16.462 +       end
  16.463 +
  16.464 +  | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
  16.465 +       let
  16.466 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
  16.467 +       in
  16.468 +         if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
  16.469 +         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
  16.470 +       end
  16.471 +
  16.472 +  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
  16.473 +       let
  16.474 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
  16.475 +       in
  16.476 +         if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
  16.477 +         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
  16.478 +       end
  16.479 +
  16.480 +  | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
  16.481 +      (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
  16.482 +        (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
  16.483 +     Const (@{const_name "Ex1"}, ty') $ t') =>
  16.484 +       let
  16.485 +         val t_ = incr_boundvars (~1) t
  16.486 +         val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
  16.487 +         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
  16.488 +       in
  16.489 +         if resrel <> needrel
  16.490 +         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
  16.491 +         else mk_bex1_rel $ resrel $ subtrm
  16.492 +       end
  16.493 +
  16.494 +  | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
  16.495 +       let
  16.496 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
  16.497 +       in
  16.498 +         if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
  16.499 +         else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
  16.500 +       end
  16.501 +
  16.502 +  | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
  16.503 +     Const (@{const_name "All"}, ty') $ t') =>
  16.504 +       let
  16.505 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
  16.506 +         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
  16.507 +       in
  16.508 +         if resrel <> needrel
  16.509 +         then term_mismatch "regularize (Ball)" ctxt resrel needrel
  16.510 +         else mk_ball $ (mk_resp $ resrel) $ subtrm
  16.511 +       end
  16.512 +
  16.513 +  | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
  16.514 +     Const (@{const_name "Ex"}, ty') $ t') =>
  16.515 +       let
  16.516 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
  16.517 +         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
  16.518 +       in
  16.519 +         if resrel <> needrel
  16.520 +         then term_mismatch "regularize (Bex)" ctxt resrel needrel
  16.521 +         else mk_bex $ (mk_resp $ resrel) $ subtrm
  16.522 +       end
  16.523 +
  16.524 +  | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
  16.525 +       let
  16.526 +         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
  16.527 +         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
  16.528 +       in
  16.529 +         if resrel <> needrel
  16.530 +         then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
  16.531 +         else mk_bex1_rel $ resrel $ subtrm
  16.532 +       end
  16.533 +
  16.534 +  | (* equalities need to be replaced by appropriate equivalence relations *)
  16.535 +    (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
  16.536 +         if ty = ty' then rtrm
  16.537 +         else equiv_relation ctxt (domain_type ty, domain_type ty')
  16.538 +
  16.539 +  | (* in this case we just check whether the given equivalence relation is correct *)
  16.540 +    (rel, Const (@{const_name "op ="}, ty')) =>
  16.541 +       let
  16.542 +         val rel_ty = fastype_of rel
  16.543 +         val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
  16.544 +       in
  16.545 +         if rel' aconv rel then rtrm
  16.546 +         else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
  16.547 +       end
  16.548 +
  16.549 +  | (_, Const _) =>
  16.550 +       let
  16.551 +         val thy = ProofContext.theory_of ctxt
  16.552 +         fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
  16.553 +           | same_const _ _ = false
  16.554 +       in
  16.555 +         if same_const rtrm qtrm then rtrm
  16.556 +         else
  16.557 +           let
  16.558 +             val rtrm' = #rconst (qconsts_lookup thy qtrm)
  16.559 +               handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
  16.560 +           in
  16.561 +             if Pattern.matches thy (rtrm', rtrm)
  16.562 +             then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
  16.563 +           end
  16.564 +       end
  16.565 +
  16.566 +  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
  16.567 +     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
  16.568 +       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
  16.569 +
  16.570 +  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)),
  16.571 +     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) =>
  16.572 +       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
  16.573 +
  16.574 +  | (t1 $ t2, t1' $ t2') =>
  16.575 +       regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
  16.576 +
  16.577 +  | (Bound i, Bound i') =>
  16.578 +       if i = i' then rtrm
  16.579 +       else raise (LIFT_MATCH "regularize (bounds mismatch)")
  16.580 +
  16.581 +  | _ =>
  16.582 +       let
  16.583 +         val rtrm_str = Syntax.string_of_term ctxt rtrm
  16.584 +         val qtrm_str = Syntax.string_of_term ctxt qtrm
  16.585 +       in
  16.586 +         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
  16.587 +       end
  16.588 +
  16.589 +fun regularize_trm_chk ctxt (rtrm, qtrm) =
  16.590 +  regularize_trm ctxt (rtrm, qtrm)
  16.591 +  |> Syntax.check_term ctxt
  16.592 +
  16.593 +
  16.594 +
  16.595 +(*** Rep/Abs Injection ***)
  16.596 +
  16.597 +(*
  16.598 +Injection of Rep/Abs means:
  16.599 +
  16.600 +  For abstractions:
  16.601 +
  16.602 +  * If the type of the abstraction needs lifting, then we add Rep/Abs
  16.603 +    around the abstraction; otherwise we leave it unchanged.
  16.604 +
  16.605 +  For applications:
  16.606 +
  16.607 +  * If the application involves a bounded quantifier, we recurse on
  16.608 +    the second argument. If the application is a bounded abstraction,
  16.609 +    we always put an Rep/Abs around it (since bounded abstractions
  16.610 +    are assumed to always need lifting). Otherwise we recurse on both
  16.611 +    arguments.
  16.612 +
  16.613 +  For constants:
  16.614 +
  16.615 +  * If the constant is (op =), we leave it always unchanged.
  16.616 +    Otherwise the type of the constant needs lifting, we put
  16.617 +    and Rep/Abs around it.
  16.618 +
  16.619 +  For free variables:
  16.620 +
  16.621 +  * We put a Rep/Abs around it if the type needs lifting.
  16.622 +
  16.623 +  Vars case cannot occur.
  16.624 +*)
  16.625 +
  16.626 +fun mk_repabs ctxt (T, T') trm =
  16.627 +  absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
  16.628 +
  16.629 +fun inj_repabs_err ctxt msg rtrm qtrm =
  16.630 +let
  16.631 +  val rtrm_str = Syntax.string_of_term ctxt rtrm
  16.632 +  val qtrm_str = Syntax.string_of_term ctxt qtrm
  16.633 +in
  16.634 +  raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
  16.635 +end
  16.636 +
  16.637 +
  16.638 +(* bound variables need to be treated properly,
  16.639 +   as the type of subterms needs to be calculated   *)
  16.640 +fun inj_repabs_trm ctxt (rtrm, qtrm) =
  16.641 + case (rtrm, qtrm) of
  16.642 +    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
  16.643 +       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
  16.644 +
  16.645 +  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
  16.646 +       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
  16.647 +
  16.648 +  | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
  16.649 +      let
  16.650 +        val rty = fastype_of rtrm
  16.651 +        val qty = fastype_of qtrm
  16.652 +      in
  16.653 +        mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
  16.654 +      end
  16.655 +
  16.656 +  | (Abs (x, T, t), Abs (x', T', t')) =>
  16.657 +      let
  16.658 +        val rty = fastype_of rtrm
  16.659 +        val qty = fastype_of qtrm
  16.660 +        val (y, s) = Term.dest_abs (x, T, t)
  16.661 +        val (_, s') = Term.dest_abs (x', T', t')
  16.662 +        val yvar = Free (y, T)
  16.663 +        val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
  16.664 +      in
  16.665 +        if rty = qty then result
  16.666 +        else mk_repabs ctxt (rty, qty) result
  16.667 +      end
  16.668 +
  16.669 +  | (t $ s, t' $ s') =>
  16.670 +       (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
  16.671 +
  16.672 +  | (Free (_, T), Free (_, T')) =>
  16.673 +        if T = T' then rtrm
  16.674 +        else mk_repabs ctxt (T, T') rtrm
  16.675 +
  16.676 +  | (_, Const (@{const_name "op ="}, _)) => rtrm
  16.677 +
  16.678 +  | (_, Const (_, T')) =>
  16.679 +      let
  16.680 +        val rty = fastype_of rtrm
  16.681 +      in
  16.682 +        if rty = T' then rtrm
  16.683 +        else mk_repabs ctxt (rty, T') rtrm
  16.684 +      end
  16.685 +
  16.686 +  | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
  16.687 +
  16.688 +fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
  16.689 +  inj_repabs_trm ctxt (rtrm, qtrm)
  16.690 +  |> Syntax.check_term ctxt
  16.691 +
  16.692 +
  16.693 +
  16.694 +(*** Wrapper for automatically transforming an rthm into a qthm ***)
  16.695 +
  16.696 +(* subst_tys takes a list of (rty, qty) substitution pairs
  16.697 +   and replaces all occurences of rty in the given type
  16.698 +   by appropriate qty, with substitution *)
  16.699 +fun subst_ty thy ty (rty, qty) r =
  16.700 +  if r <> NONE then r else
  16.701 +  case try (Sign.typ_match thy (rty, ty)) Vartab.empty of
  16.702 +    SOME inst => SOME (Envir.subst_type inst qty)
  16.703 +  | NONE => NONE
  16.704 +fun subst_tys thy substs ty =
  16.705 +  case fold (subst_ty thy ty) substs NONE of
  16.706 +    SOME ty => ty
  16.707 +  | NONE =>
  16.708 +      (case ty of
  16.709 +        Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
  16.710 +      | x => x)
  16.711 +
  16.712 +(* subst_trms takes a list of (rtrm, qtrm) substitution pairs
  16.713 +   and if the given term matches any of the raw terms it
  16.714 +   returns the appropriate qtrm instantiated. If none of
  16.715 +   them matched it returns NONE. *)
  16.716 +fun subst_trm thy t (rtrm, qtrm) s =
  16.717 +  if s <> NONE then s else
  16.718 +    case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of
  16.719 +      SOME inst => SOME (Envir.subst_term inst qtrm)
  16.720 +    | NONE => NONE;
  16.721 +fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
  16.722 +
  16.723 +(* prepares type and term substitution pairs to be used by above
  16.724 +   functions that let replace all raw constructs by appropriate
  16.725 +   lifted counterparts. *)
  16.726 +fun get_ty_trm_substs ctxt =
  16.727 +let
  16.728 +  val thy = ProofContext.theory_of ctxt
  16.729 +  val quot_infos  = Quotient_Info.quotdata_dest ctxt
  16.730 +  val const_infos = Quotient_Info.qconsts_dest ctxt
  16.731 +  val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
  16.732 +  val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
  16.733 +  fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
  16.734 +  val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
  16.735 +in
  16.736 +  (ty_substs, const_substs @ rel_substs)
  16.737 +end
  16.738 +
  16.739 +fun quotient_lift_const (b, t) ctxt =
  16.740 +let
  16.741 +  val thy = ProofContext.theory_of ctxt
  16.742 +  val (ty_substs, _) = get_ty_trm_substs ctxt;
  16.743 +  val (_, ty) = dest_Const t;
  16.744 +  val nty = subst_tys thy ty_substs ty;
  16.745 +in
  16.746 +  Free(b, nty)
  16.747 +end
  16.748 +
  16.749 +(*
  16.750 +Takes a term and
  16.751 +
  16.752 +* replaces raw constants by the quotient constants
  16.753 +
  16.754 +* replaces equivalence relations by equalities
  16.755 +
  16.756 +* replaces raw types by the quotient types
  16.757 +
  16.758 +*)
  16.759 +
  16.760 +fun quotient_lift_all ctxt t =
  16.761 +let
  16.762 +  val thy = ProofContext.theory_of ctxt
  16.763 +  val (ty_substs, substs) = get_ty_trm_substs ctxt
  16.764 +  fun lift_aux t =
  16.765 +    case subst_trms thy substs t of
  16.766 +      SOME x => x
  16.767 +    | NONE =>
  16.768 +      (case t of
  16.769 +        a $ b => lift_aux a $ lift_aux b
  16.770 +      | Abs(a, ty, s) =>
  16.771 +          let
  16.772 +            val (y, s') = Term.dest_abs (a, ty, s)
  16.773 +            val nty = subst_tys thy ty_substs ty
  16.774 +          in
  16.775 +            Abs(y, nty, abstract_over (Free (y, nty), lift_aux s'))
  16.776 +          end
  16.777 +      | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
  16.778 +      | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)
  16.779 +      | Bound i => Bound i
  16.780 +      | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
  16.781 +in
  16.782 +  lift_aux t
  16.783 +end
  16.784 +
  16.785 +
  16.786 +end; (* structure *)
  16.787 +
  16.788 +
  16.789 +
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Feb 19 13:54:19 2010 +0100
    17.3 @@ -0,0 +1,309 @@
    17.4 +(*  Title:      quotient_typ.thy
    17.5 +    Author:     Cezary Kaliszyk and Christian Urban
    17.6 +
    17.7 +    Definition of a quotient type.
    17.8 +
    17.9 +*)
   17.10 +
   17.11 +signature QUOTIENT_TYPE =
   17.12 +sig
   17.13 +  val quotient_type: ((string list * binding * mixfix) * (typ * term)) list
   17.14 +    -> Proof.context -> Proof.state
   17.15 +
   17.16 +  val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list
   17.17 +    -> Proof.context -> Proof.state
   17.18 +end;
   17.19 +
   17.20 +structure Quotient_Type: QUOTIENT_TYPE =
   17.21 +struct
   17.22 +
   17.23 +open Quotient_Info;
   17.24 +
   17.25 +(* wrappers for define, note, Attrib.internal and theorem_i *)
   17.26 +fun define (name, mx, rhs) lthy =
   17.27 +let
   17.28 +  val ((rhs, (_ , thm)), lthy') =
   17.29 +     Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
   17.30 +in
   17.31 +  ((rhs, thm), lthy')
   17.32 +end
   17.33 +
   17.34 +fun note (name, thm, attrs) lthy =
   17.35 +let
   17.36 +  val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy
   17.37 +in
   17.38 +  (thm', lthy')
   17.39 +end
   17.40 +
   17.41 +fun intern_attr at = Attrib.internal (K at)
   17.42 +
   17.43 +fun theorem after_qed goals ctxt =
   17.44 +let
   17.45 +  val goals' = map (rpair []) goals
   17.46 +  fun after_qed' thms = after_qed (the_single thms)
   17.47 +in
   17.48 +  Proof.theorem_i NONE after_qed' [goals'] ctxt
   17.49 +end
   17.50 +
   17.51 +
   17.52 +
   17.53 +(*** definition of quotient types ***)
   17.54 +
   17.55 +val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)}
   17.56 +val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)}
   17.57 +
   17.58 +(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
   17.59 +fun typedef_term rel rty lthy =
   17.60 +let
   17.61 +  val [x, c] =
   17.62 +    [("x", rty), ("c", HOLogic.mk_setT rty)]
   17.63 +    |> Variable.variant_frees lthy [rel]
   17.64 +    |> map Free
   17.65 +in
   17.66 +  lambda c (HOLogic.exists_const rty $
   17.67 +     lambda x (HOLogic.mk_eq (c, (rel $ x))))
   17.68 +end
   17.69 +
   17.70 +
   17.71 +(* makes the new type definitions and proves non-emptyness *)
   17.72 +fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
   17.73 +let
   17.74 +  val typedef_tac =
   17.75 +     EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
   17.76 +in
   17.77 +  Local_Theory.theory_result
   17.78 +    (Typedef.add_typedef false NONE
   17.79 +       (qty_name, vs, mx)
   17.80 +          (typedef_term rel rty lthy)
   17.81 +             NONE typedef_tac) lthy
   17.82 +end
   17.83 +
   17.84 +
   17.85 +(* tactic to prove the quot_type theorem for the new type *)
   17.86 +fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
   17.87 +let
   17.88 +  val rep_thm = #Rep typedef_info RS mem_def1
   17.89 +  val rep_inv = #Rep_inverse typedef_info
   17.90 +  val abs_inv = mem_def2 RS #Abs_inverse typedef_info
   17.91 +  val rep_inj = #Rep_inject typedef_info
   17.92 +in
   17.93 +  (rtac @{thm quot_type.intro} THEN' RANGE [
   17.94 +    rtac equiv_thm,
   17.95 +    rtac rep_thm,
   17.96 +    rtac rep_inv,
   17.97 +    EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]),
   17.98 +    rtac rep_inj]) 1
   17.99 +end
  17.100 +
  17.101 +
  17.102 +(* proves the quot_type theorem for the new type *)
  17.103 +fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
  17.104 +let
  17.105 +  val quot_type_const = Const (@{const_name "quot_type"}, dummyT)
  17.106 +  val goal =
  17.107 +    HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
  17.108 +    |> Syntax.check_term lthy
  17.109 +in
  17.110 +  Goal.prove lthy [] [] goal
  17.111 +    (K (typedef_quot_type_tac equiv_thm typedef_info))
  17.112 +end
  17.113 +
  17.114 +(* proves the quotient theorem for the new type *)
  17.115 +fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
  17.116 +let
  17.117 +  val quotient_const = Const (@{const_name "Quotient"}, dummyT)
  17.118 +  val goal =
  17.119 +    HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
  17.120 +    |> Syntax.check_term lthy
  17.121 +
  17.122 +  val typedef_quotient_thm_tac =
  17.123 +    EVERY1 [
  17.124 +      K (rewrite_goals_tac [abs_def, rep_def]),
  17.125 +      rtac @{thm quot_type.Quotient},
  17.126 +      rtac quot_type_thm]
  17.127 +in
  17.128 +  Goal.prove lthy [] [] goal
  17.129 +    (K typedef_quotient_thm_tac)
  17.130 +end
  17.131 +
  17.132 +
  17.133 +(* main function for constructing a quotient type *)
  17.134 +fun mk_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy =
  17.135 +let
  17.136 +  (* generates the typedef *)
  17.137 +  val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy
  17.138 +
  17.139 +  (* abs and rep functions from the typedef *)
  17.140 +  val Abs_ty = #abs_type typedef_info
  17.141 +  val Rep_ty = #rep_type typedef_info
  17.142 +  val Abs_name = #Abs_name typedef_info
  17.143 +  val Rep_name = #Rep_name typedef_info
  17.144 +  val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
  17.145 +  val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
  17.146 +
  17.147 +  (* more useful abs and rep definitions *)
  17.148 +  val abs_const = Const (@{const_name "quot_type.abs"}, dummyT )
  17.149 +  val rep_const = Const (@{const_name "quot_type.rep"}, dummyT )
  17.150 +  val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)
  17.151 +  val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
  17.152 +  val abs_name = Binding.prefix_name "abs_" qty_name
  17.153 +  val rep_name = Binding.prefix_name "rep_" qty_name
  17.154 +
  17.155 +  val ((abs, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
  17.156 +  val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
  17.157 +
  17.158 +  (* quot_type theorem *)
  17.159 +  val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3
  17.160 +
  17.161 +  (* quotient theorem *)
  17.162 +  val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3
  17.163 +  val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
  17.164 +
  17.165 +  (* name equivalence theorem *)
  17.166 +  val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
  17.167 +
  17.168 +  (* storing the quot-info *)
  17.169 +  fun qinfo phi = transform_quotdata phi
  17.170 +    {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
  17.171 +  val lthy4 = Local_Theory.declaration true
  17.172 +    (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3
  17.173 +in
  17.174 +  lthy4
  17.175 +  |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
  17.176 +  ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add])
  17.177 +end
  17.178 +
  17.179 +
  17.180 +(* sanity checks for the quotient type specifications *)
  17.181 +fun sanity_check ((vs, qty_name, _), (rty, rel)) =
  17.182 +let
  17.183 +  val rty_tfreesT = map fst (Term.add_tfreesT rty [])
  17.184 +  val rel_tfrees = map fst (Term.add_tfrees rel [])
  17.185 +  val rel_frees = map fst (Term.add_frees rel [])
  17.186 +  val rel_vars = Term.add_vars rel []
  17.187 +  val rel_tvars = Term.add_tvars rel []
  17.188 +  val qty_str = Binding.str_of qty_name ^ ": "
  17.189 +
  17.190 +  val illegal_rel_vars =
  17.191 +    if null rel_vars andalso null rel_tvars then []
  17.192 +    else [qty_str ^ "illegal schematic variable(s) in the relation."]
  17.193 +
  17.194 +  val dup_vs =
  17.195 +    (case duplicates (op =) vs of
  17.196 +       [] => []
  17.197 +     | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
  17.198 +
  17.199 +  val extra_rty_tfrees =
  17.200 +    (case subtract (op =) vs rty_tfreesT of
  17.201 +       [] => []
  17.202 +     | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
  17.203 +
  17.204 +  val extra_rel_tfrees =
  17.205 +    (case subtract (op =) vs rel_tfrees of
  17.206 +       [] => []
  17.207 +     | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
  17.208 +
  17.209 +  val illegal_rel_frees =
  17.210 +    (case rel_frees of
  17.211 +      [] => []
  17.212 +    | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
  17.213 +
  17.214 +  val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
  17.215 +in
  17.216 +  if null errs then () else error (cat_lines errs)
  17.217 +end
  17.218 +
  17.219 +(* check for existence of map functions *)
  17.220 +fun map_check ctxt (_, (rty, _)) =
  17.221 +let
  17.222 +  val thy = ProofContext.theory_of ctxt
  17.223 +
  17.224 +  fun map_check_aux rty warns =
  17.225 +    case rty of
  17.226 +      Type (_, []) => warns
  17.227 +    | Type (s, _) => if maps_defined thy s then warns else s::warns
  17.228 +    | _ => warns
  17.229 +
  17.230 +  val warns = map_check_aux rty []
  17.231 +in
  17.232 +  if null warns then ()
  17.233 +  else warning ("No map function defined for " ^ commas warns ^
  17.234 +    ". This will cause problems later on.")
  17.235 +end
  17.236 +
  17.237 +
  17.238 +
  17.239 +(*** interface and syntax setup ***)
  17.240 +
  17.241 +
  17.242 +(* the ML-interface takes a list of 5-tuples consisting of:
  17.243 +
  17.244 + - the name of the quotient type
  17.245 + - its free type variables (first argument)
  17.246 + - its mixfix annotation
  17.247 + - the type to be quotient
  17.248 + - the relation according to which the type is quotient
  17.249 +
  17.250 + it opens a proof-state in which one has to show that the
  17.251 + relations are equivalence relations
  17.252 +*)
  17.253 +
  17.254 +fun quotient_type quot_list lthy =
  17.255 +let
  17.256 +  (* sanity check *)
  17.257 +  val _ = List.app sanity_check quot_list
  17.258 +  val _ = List.app (map_check lthy) quot_list
  17.259 +
  17.260 +  fun mk_goal (rty, rel) =
  17.261 +  let
  17.262 +    val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
  17.263 +  in
  17.264 +    HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel)
  17.265 +  end
  17.266 +
  17.267 +  val goals = map (mk_goal o snd) quot_list
  17.268 +
  17.269 +  fun after_qed thms lthy =
  17.270 +    fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd
  17.271 +in
  17.272 +  theorem after_qed goals lthy
  17.273 +end
  17.274 +
  17.275 +fun quotient_type_cmd specs lthy =
  17.276 +let
  17.277 +  fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy =
  17.278 +  let
  17.279 +    (* new parsing with proper declaration *)
  17.280 +    val rty = Syntax.read_typ lthy rty_str
  17.281 +    val lthy1 = Variable.declare_typ rty lthy
  17.282 +    val pre_rel = Syntax.parse_term lthy1 rel_str
  17.283 +    val pre_rel' = Syntax.type_constraint (rty --> rty --> @{typ bool}) pre_rel
  17.284 +    val rel = Syntax.check_term lthy1 pre_rel'
  17.285 +    val lthy2 = Variable.declare_term rel lthy1
  17.286 +
  17.287 +    (* old parsing *)
  17.288 +    (* val rty = Syntax.read_typ lthy rty_str
  17.289 +       val rel = Syntax.read_term lthy rel_str *)
  17.290 +  in
  17.291 +    (((vs, qty_name, mx), (rty, rel)), lthy2)
  17.292 +  end
  17.293 +
  17.294 +  val (spec', lthy') = fold_map parse_spec specs lthy
  17.295 +in
  17.296 +  quotient_type spec' lthy'
  17.297 +end
  17.298 +
  17.299 +val quotspec_parser =
  17.300 +    OuterParse.and_list1
  17.301 +     ((OuterParse.type_args -- OuterParse.binding) --
  17.302 +        OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
  17.303 +         (OuterParse.$$$ "/" |-- OuterParse.term))
  17.304 +
  17.305 +val _ = OuterKeyword.keyword "/"
  17.306 +
  17.307 +val _ =
  17.308 +    OuterSyntax.local_theory_to_proof "quotient_type"
  17.309 +      "quotient type definitions (require equivalence proofs)"
  17.310 +         OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
  17.311 +
  17.312 +end; (* structure *)