more conventional file name;
authorwenzelm
Tue Nov 29 22:45:21 2011 +0100 (2011-11-29)
changeset 45680a61510361b89
parent 45679 a574a9432525
child 45681 ac1651b08da2
more conventional file name;
src/HOL/IsaMakefile
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_typ.ML
src/HOL/Tools/Quotient/quotient_type.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Nov 29 21:50:00 2011 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Nov 29 22:45:21 2011 +0100
     1.3 @@ -356,7 +356,7 @@
     1.4    Tools/Quotient/quotient_info.ML \
     1.5    Tools/Quotient/quotient_tacs.ML \
     1.6    Tools/Quotient/quotient_term.ML \
     1.7 -  Tools/Quotient/quotient_typ.ML \
     1.8 +  Tools/Quotient/quotient_type.ML \
     1.9    Tools/record.ML \
    1.10    Tools/semiring_normalizer.ML \
    1.11    Tools/Sledgehammer/async_manager.ML \
     2.1 --- a/src/HOL/Quotient.thy	Tue Nov 29 21:50:00 2011 +0100
     2.2 +++ b/src/HOL/Quotient.thy	Tue Nov 29 22:45:21 2011 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  imports Plain Hilbert_Choice Equiv_Relations
     2.5  uses
     2.6    ("Tools/Quotient/quotient_info.ML")
     2.7 -  ("Tools/Quotient/quotient_typ.ML")
     2.8 +  ("Tools/Quotient/quotient_type.ML")
     2.9    ("Tools/Quotient/quotient_def.ML")
    2.10    ("Tools/Quotient/quotient_term.ML")
    2.11    ("Tools/Quotient/quotient_tacs.ML")
    2.12 @@ -696,7 +696,7 @@
    2.13  
    2.14  
    2.15  text {* Definitions of the quotient types. *}
    2.16 -use "Tools/Quotient/quotient_typ.ML"
    2.17 +use "Tools/Quotient/quotient_type.ML"
    2.18  
    2.19  
    2.20  text {* Definitions for quotient constants. *}
     3.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Tue Nov 29 21:50:00 2011 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,292 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/Quotient/quotient_typ.ML
     3.5 -    Author:     Cezary Kaliszyk and Christian Urban
     3.6 -
     3.7 -Definition of a quotient type.
     3.8 -*)
     3.9 -
    3.10 -signature QUOTIENT_TYPE =
    3.11 -sig
    3.12 -  val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
    3.13 -    ((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
    3.14 -
    3.15 -  val quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
    3.16 -    ((binding * binding) option)) list -> Proof.context -> Proof.state
    3.17 -
    3.18 -  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
    3.19 -    (binding * binding) option) list -> Proof.context -> Proof.state
    3.20 -end;
    3.21 -
    3.22 -structure Quotient_Type: QUOTIENT_TYPE =
    3.23 -struct
    3.24 -
    3.25 -
    3.26 -(*** definition of quotient types ***)
    3.27 -
    3.28 -val mem_def1 = @{lemma "y : Collect S ==> S y" by simp}
    3.29 -val mem_def2 = @{lemma "S y ==> y : Collect S" by simp}
    3.30 -
    3.31 -(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
    3.32 -fun typedef_term rel rty lthy =
    3.33 -  let
    3.34 -    val [x, c] =
    3.35 -      [("x", rty), ("c", HOLogic.mk_setT rty)]
    3.36 -      |> Variable.variant_frees lthy [rel]
    3.37 -      |> map Free
    3.38 -  in
    3.39 -    HOLogic.Collect_const (HOLogic.mk_setT rty) $ (lambda c (HOLogic.exists_const rty $
    3.40 -        lambda x (HOLogic.mk_conj (rel $ x $ x,
    3.41 -        HOLogic.mk_eq (c, HOLogic.Collect_const rty $ (rel $ x))))))
    3.42 -  end
    3.43 -
    3.44 -
    3.45 -(* makes the new type definitions and proves non-emptyness *)
    3.46 -fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
    3.47 -  let
    3.48 -    val typedef_tac =
    3.49 -      EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
    3.50 -  in
    3.51 -  (* FIXME: purely local typedef causes at the moment
    3.52 -     problems with type variables
    3.53 -
    3.54 -    Typedef.add_typedef false NONE (qty_name, vs, mx)
    3.55 -      (typedef_term rel rty lthy) NONE typedef_tac lthy
    3.56 -  *)
    3.57 -  (* FIXME should really use local typedef here *)
    3.58 -    Local_Theory.background_theory_result
    3.59 -     (Typedef.add_typedef_global false NONE
    3.60 -       (qty_name, map (rpair dummyS) vs, mx)
    3.61 -         (typedef_term rel rty lthy)
    3.62 -           NONE typedef_tac) lthy
    3.63 -  end
    3.64 -
    3.65 -
    3.66 -(* tactic to prove the quot_type theorem for the new type *)
    3.67 -fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
    3.68 -  let
    3.69 -    val rep_thm = #Rep typedef_info RS mem_def1
    3.70 -    val rep_inv = #Rep_inverse typedef_info
    3.71 -    val abs_inv = #Abs_inverse typedef_info
    3.72 -    val rep_inj = #Rep_inject typedef_info
    3.73 -  in
    3.74 -    (rtac @{thm quot_type.intro} THEN' RANGE [
    3.75 -      rtac equiv_thm,
    3.76 -      rtac rep_thm,
    3.77 -      rtac rep_inv,
    3.78 -      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
    3.79 -      rtac rep_inj]) 1
    3.80 -  end
    3.81 -
    3.82 -(* proves the quot_type theorem for the new type *)
    3.83 -fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
    3.84 -  let
    3.85 -    val quot_type_const = Const (@{const_name "quot_type"},
    3.86 -      fastype_of rel --> fastype_of abs --> fastype_of rep --> @{typ bool})
    3.87 -    val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
    3.88 -  in
    3.89 -    Goal.prove lthy [] [] goal
    3.90 -      (K (typedef_quot_type_tac equiv_thm typedef_info))
    3.91 -  end
    3.92 -
    3.93 -(* main function for constructing a quotient type *)
    3.94 -fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), equiv_thm) lthy =
    3.95 -  let
    3.96 -    val part_equiv =
    3.97 -      if partial
    3.98 -      then equiv_thm
    3.99 -      else equiv_thm RS @{thm equivp_implies_part_equivp}
   3.100 -
   3.101 -    (* generates the typedef *)
   3.102 -    val ((qty_full_name, typedef_info), lthy1) =
   3.103 -      typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
   3.104 -
   3.105 -    (* abs and rep functions from the typedef *)
   3.106 -    val Abs_ty = #abs_type (#1 typedef_info)
   3.107 -    val Rep_ty = #rep_type (#1 typedef_info)
   3.108 -    val Abs_name = #Abs_name (#1 typedef_info)
   3.109 -    val Rep_name = #Rep_name (#1 typedef_info)
   3.110 -    val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
   3.111 -    val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
   3.112 -
   3.113 -    (* more useful abs and rep definitions *)
   3.114 -    val abs_const = Const (@{const_name quot_type.abs},
   3.115 -      (rty --> rty --> @{typ bool}) --> (Rep_ty --> Abs_ty) --> rty --> Abs_ty)
   3.116 -    val rep_const = Const (@{const_name quot_type.rep}, (Abs_ty --> Rep_ty) --> Abs_ty --> rty)
   3.117 -    val abs_trm = abs_const $ rel $ Abs_const
   3.118 -    val rep_trm = rep_const $ Rep_const
   3.119 -    val (rep_name, abs_name) =
   3.120 -      (case opt_morphs of
   3.121 -        NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name)
   3.122 -      | SOME morphs => morphs)
   3.123 -
   3.124 -    val ((abs_t, (_, abs_def)), lthy2) = lthy1
   3.125 -      |> Local_Theory.define ((abs_name, NoSyn), (Attrib.empty_binding, abs_trm))
   3.126 -    val ((rep_t, (_, rep_def)), lthy3) = lthy2
   3.127 -      |> Local_Theory.define ((rep_name, NoSyn), (Attrib.empty_binding, rep_trm))
   3.128 -
   3.129 -    (* quot_type theorem *)
   3.130 -    val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
   3.131 -
   3.132 -    (* quotient theorem *)
   3.133 -    val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
   3.134 -    val quotient_thm =
   3.135 -      (quot_thm RS @{thm quot_type.Quotient})
   3.136 -      |> fold_rule [abs_def, rep_def]
   3.137 -
   3.138 -    (* name equivalence theorem *)
   3.139 -    val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
   3.140 -
   3.141 -    (* storing the quotients *)
   3.142 -    val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
   3.143 -
   3.144 -    fun qinfo phi = Quotient_Info.transform_quotients phi quotients
   3.145 -    fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}
   3.146 -
   3.147 -    val lthy4 = lthy3
   3.148 -      |> Local_Theory.declaration {syntax = false, pervasive = true}
   3.149 -        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
   3.150 -           #> Quotient_Info.update_abs_rep qty_full_name (abs_rep phi))
   3.151 -      |> (snd oo Local_Theory.note)
   3.152 -        ((equiv_thm_name,
   3.153 -          if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
   3.154 -          [equiv_thm])
   3.155 -      |> (snd oo Local_Theory.note)
   3.156 -        ((quotient_thm_name, [Attrib.internal (K Quotient_Info.quotient_rules_add)]),
   3.157 -          [quotient_thm])
   3.158 -  in
   3.159 -    (quotients, lthy4)
   3.160 -  end
   3.161 -
   3.162 -
   3.163 -(* sanity checks for the quotient type specifications *)
   3.164 -fun sanity_check ((vs, qty_name, _), (rty, rel, _), _) =
   3.165 -  let
   3.166 -    val rty_tfreesT = map fst (Term.add_tfreesT rty [])
   3.167 -    val rel_tfrees = map fst (Term.add_tfrees rel [])
   3.168 -    val rel_frees = map fst (Term.add_frees rel [])
   3.169 -    val rel_vars = Term.add_vars rel []
   3.170 -    val rel_tvars = Term.add_tvars rel []
   3.171 -    val qty_str = Binding.print qty_name ^ ": "
   3.172 -
   3.173 -    val illegal_rel_vars =
   3.174 -      if null rel_vars andalso null rel_tvars then []
   3.175 -      else [qty_str ^ "illegal schematic variable(s) in the relation."]
   3.176 -
   3.177 -    val dup_vs =
   3.178 -      (case duplicates (op =) vs of
   3.179 -        [] => []
   3.180 -      | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
   3.181 -
   3.182 -    val extra_rty_tfrees =
   3.183 -      (case subtract (op =) vs rty_tfreesT of
   3.184 -        [] => []
   3.185 -      | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
   3.186 -
   3.187 -    val extra_rel_tfrees =
   3.188 -      (case subtract (op =) vs rel_tfrees of
   3.189 -        [] => []
   3.190 -      | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
   3.191 -
   3.192 -    val illegal_rel_frees =
   3.193 -      (case rel_frees of
   3.194 -        [] => []
   3.195 -      | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
   3.196 -
   3.197 -    val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
   3.198 -  in
   3.199 -    if null errs then () else error (cat_lines errs)
   3.200 -  end
   3.201 -
   3.202 -(* check for existence of map functions *)
   3.203 -fun map_check thy (_, (rty, _, _), _) =
   3.204 -  let
   3.205 -    fun map_check_aux rty warns =
   3.206 -      (case rty of
   3.207 -        Type (_, []) => warns
   3.208 -      | Type (s, _) =>
   3.209 -          if is_some (Quotient_Info.lookup_quotmaps_global thy s) then warns else s :: warns
   3.210 -      | _ => warns)
   3.211 -
   3.212 -    val warns = map_check_aux rty []
   3.213 -  in
   3.214 -    if null warns then ()
   3.215 -    else warning ("No map function defined for " ^ commas warns ^
   3.216 -      ". This will cause problems later on.")
   3.217 -  end
   3.218 -
   3.219 -
   3.220 -
   3.221 -(*** interface and syntax setup ***)
   3.222 -
   3.223 -
   3.224 -(* the ML-interface takes a list of 5-tuples consisting of:
   3.225 -
   3.226 - - the name of the quotient type
   3.227 - - its free type variables (first argument)
   3.228 - - its mixfix annotation
   3.229 - - the type to be quotient
   3.230 - - the partial flag (a boolean)
   3.231 - - the relation according to which the type is quotient
   3.232 -
   3.233 - it opens a proof-state in which one has to show that the
   3.234 - relations are equivalence relations
   3.235 -*)
   3.236 -
   3.237 -fun quotient_type quot_list lthy =
   3.238 -  let
   3.239 -    (* sanity check *)
   3.240 -    val _ = List.app sanity_check quot_list
   3.241 -    val _ = List.app (map_check (Proof_Context.theory_of lthy)) quot_list
   3.242 -
   3.243 -    fun mk_goal (rty, rel, partial) =
   3.244 -      let
   3.245 -        val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   3.246 -        val const =
   3.247 -          if partial then @{const_name part_equivp} else @{const_name equivp}
   3.248 -      in
   3.249 -        HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
   3.250 -      end
   3.251 -
   3.252 -    val goals = map (mk_goal o #2) quot_list
   3.253 -
   3.254 -    fun after_qed [thms] = fold (snd oo add_quotient_type) (quot_list ~~ thms)
   3.255 -  in
   3.256 -    Proof.theorem NONE after_qed [map (rpair []) goals] lthy
   3.257 -  end
   3.258 -
   3.259 -fun quotient_type_cmd specs lthy =
   3.260 -  let
   3.261 -    fun parse_spec (((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
   3.262 -      let
   3.263 -        val rty = Syntax.read_typ lthy rty_str
   3.264 -        val lthy1 = Variable.declare_typ rty lthy
   3.265 -        val rel =
   3.266 -          Syntax.parse_term lthy1 rel_str
   3.267 -          |> Type.constraint (rty --> rty --> @{typ bool})
   3.268 -          |> Syntax.check_term lthy1
   3.269 -        val lthy2 = Variable.declare_term rel lthy1
   3.270 -      in
   3.271 -        (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), lthy2)
   3.272 -      end
   3.273 -
   3.274 -    val (spec', lthy') = fold_map parse_spec specs lthy
   3.275 -  in
   3.276 -    quotient_type spec' lthy'
   3.277 -  end
   3.278 -
   3.279 -val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
   3.280 -
   3.281 -val quotspec_parser =
   3.282 -  Parse.and_list1
   3.283 -    ((Parse.type_args -- Parse.binding) --
   3.284 -      Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
   3.285 -        (Parse.$$$ "/" |-- (partial -- Parse.term))  --
   3.286 -        Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
   3.287 -
   3.288 -val _ = Keyword.keyword "/"
   3.289 -
   3.290 -val _ =
   3.291 -  Outer_Syntax.local_theory_to_proof "quotient_type"
   3.292 -    "quotient type definitions (require equivalence proofs)"
   3.293 -       Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
   3.294 -
   3.295 -end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Tue Nov 29 22:45:21 2011 +0100
     4.3 @@ -0,0 +1,292 @@
     4.4 +(*  Title:      HOL/Tools/Quotient/quotient_type.ML
     4.5 +    Author:     Cezary Kaliszyk and Christian Urban
     4.6 +
     4.7 +Definition of a quotient type.
     4.8 +*)
     4.9 +
    4.10 +signature QUOTIENT_TYPE =
    4.11 +sig
    4.12 +  val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
    4.13 +    ((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
    4.14 +
    4.15 +  val quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
    4.16 +    ((binding * binding) option)) list -> Proof.context -> Proof.state
    4.17 +
    4.18 +  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
    4.19 +    (binding * binding) option) list -> Proof.context -> Proof.state
    4.20 +end;
    4.21 +
    4.22 +structure Quotient_Type: QUOTIENT_TYPE =
    4.23 +struct
    4.24 +
    4.25 +
    4.26 +(*** definition of quotient types ***)
    4.27 +
    4.28 +val mem_def1 = @{lemma "y : Collect S ==> S y" by simp}
    4.29 +val mem_def2 = @{lemma "S y ==> y : Collect S" by simp}
    4.30 +
    4.31 +(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
    4.32 +fun typedef_term rel rty lthy =
    4.33 +  let
    4.34 +    val [x, c] =
    4.35 +      [("x", rty), ("c", HOLogic.mk_setT rty)]
    4.36 +      |> Variable.variant_frees lthy [rel]
    4.37 +      |> map Free
    4.38 +  in
    4.39 +    HOLogic.Collect_const (HOLogic.mk_setT rty) $ (lambda c (HOLogic.exists_const rty $
    4.40 +        lambda x (HOLogic.mk_conj (rel $ x $ x,
    4.41 +        HOLogic.mk_eq (c, HOLogic.Collect_const rty $ (rel $ x))))))
    4.42 +  end
    4.43 +
    4.44 +
    4.45 +(* makes the new type definitions and proves non-emptyness *)
    4.46 +fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
    4.47 +  let
    4.48 +    val typedef_tac =
    4.49 +      EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
    4.50 +  in
    4.51 +  (* FIXME: purely local typedef causes at the moment
    4.52 +     problems with type variables
    4.53 +
    4.54 +    Typedef.add_typedef false NONE (qty_name, vs, mx)
    4.55 +      (typedef_term rel rty lthy) NONE typedef_tac lthy
    4.56 +  *)
    4.57 +  (* FIXME should really use local typedef here *)
    4.58 +    Local_Theory.background_theory_result
    4.59 +     (Typedef.add_typedef_global false NONE
    4.60 +       (qty_name, map (rpair dummyS) vs, mx)
    4.61 +         (typedef_term rel rty lthy)
    4.62 +           NONE typedef_tac) lthy
    4.63 +  end
    4.64 +
    4.65 +
    4.66 +(* tactic to prove the quot_type theorem for the new type *)
    4.67 +fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
    4.68 +  let
    4.69 +    val rep_thm = #Rep typedef_info RS mem_def1
    4.70 +    val rep_inv = #Rep_inverse typedef_info
    4.71 +    val abs_inv = #Abs_inverse typedef_info
    4.72 +    val rep_inj = #Rep_inject typedef_info
    4.73 +  in
    4.74 +    (rtac @{thm quot_type.intro} THEN' RANGE [
    4.75 +      rtac equiv_thm,
    4.76 +      rtac rep_thm,
    4.77 +      rtac rep_inv,
    4.78 +      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
    4.79 +      rtac rep_inj]) 1
    4.80 +  end
    4.81 +
    4.82 +(* proves the quot_type theorem for the new type *)
    4.83 +fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
    4.84 +  let
    4.85 +    val quot_type_const = Const (@{const_name "quot_type"},
    4.86 +      fastype_of rel --> fastype_of abs --> fastype_of rep --> @{typ bool})
    4.87 +    val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
    4.88 +  in
    4.89 +    Goal.prove lthy [] [] goal
    4.90 +      (K (typedef_quot_type_tac equiv_thm typedef_info))
    4.91 +  end
    4.92 +
    4.93 +(* main function for constructing a quotient type *)
    4.94 +fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), equiv_thm) lthy =
    4.95 +  let
    4.96 +    val part_equiv =
    4.97 +      if partial
    4.98 +      then equiv_thm
    4.99 +      else equiv_thm RS @{thm equivp_implies_part_equivp}
   4.100 +
   4.101 +    (* generates the typedef *)
   4.102 +    val ((qty_full_name, typedef_info), lthy1) =
   4.103 +      typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
   4.104 +
   4.105 +    (* abs and rep functions from the typedef *)
   4.106 +    val Abs_ty = #abs_type (#1 typedef_info)
   4.107 +    val Rep_ty = #rep_type (#1 typedef_info)
   4.108 +    val Abs_name = #Abs_name (#1 typedef_info)
   4.109 +    val Rep_name = #Rep_name (#1 typedef_info)
   4.110 +    val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
   4.111 +    val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
   4.112 +
   4.113 +    (* more useful abs and rep definitions *)
   4.114 +    val abs_const = Const (@{const_name quot_type.abs},
   4.115 +      (rty --> rty --> @{typ bool}) --> (Rep_ty --> Abs_ty) --> rty --> Abs_ty)
   4.116 +    val rep_const = Const (@{const_name quot_type.rep}, (Abs_ty --> Rep_ty) --> Abs_ty --> rty)
   4.117 +    val abs_trm = abs_const $ rel $ Abs_const
   4.118 +    val rep_trm = rep_const $ Rep_const
   4.119 +    val (rep_name, abs_name) =
   4.120 +      (case opt_morphs of
   4.121 +        NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name)
   4.122 +      | SOME morphs => morphs)
   4.123 +
   4.124 +    val ((abs_t, (_, abs_def)), lthy2) = lthy1
   4.125 +      |> Local_Theory.define ((abs_name, NoSyn), (Attrib.empty_binding, abs_trm))
   4.126 +    val ((rep_t, (_, rep_def)), lthy3) = lthy2
   4.127 +      |> Local_Theory.define ((rep_name, NoSyn), (Attrib.empty_binding, rep_trm))
   4.128 +
   4.129 +    (* quot_type theorem *)
   4.130 +    val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
   4.131 +
   4.132 +    (* quotient theorem *)
   4.133 +    val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
   4.134 +    val quotient_thm =
   4.135 +      (quot_thm RS @{thm quot_type.Quotient})
   4.136 +      |> fold_rule [abs_def, rep_def]
   4.137 +
   4.138 +    (* name equivalence theorem *)
   4.139 +    val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
   4.140 +
   4.141 +    (* storing the quotients *)
   4.142 +    val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
   4.143 +
   4.144 +    fun qinfo phi = Quotient_Info.transform_quotients phi quotients
   4.145 +    fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}
   4.146 +
   4.147 +    val lthy4 = lthy3
   4.148 +      |> Local_Theory.declaration {syntax = false, pervasive = true}
   4.149 +        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
   4.150 +           #> Quotient_Info.update_abs_rep qty_full_name (abs_rep phi))
   4.151 +      |> (snd oo Local_Theory.note)
   4.152 +        ((equiv_thm_name,
   4.153 +          if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
   4.154 +          [equiv_thm])
   4.155 +      |> (snd oo Local_Theory.note)
   4.156 +        ((quotient_thm_name, [Attrib.internal (K Quotient_Info.quotient_rules_add)]),
   4.157 +          [quotient_thm])
   4.158 +  in
   4.159 +    (quotients, lthy4)
   4.160 +  end
   4.161 +
   4.162 +
   4.163 +(* sanity checks for the quotient type specifications *)
   4.164 +fun sanity_check ((vs, qty_name, _), (rty, rel, _), _) =
   4.165 +  let
   4.166 +    val rty_tfreesT = map fst (Term.add_tfreesT rty [])
   4.167 +    val rel_tfrees = map fst (Term.add_tfrees rel [])
   4.168 +    val rel_frees = map fst (Term.add_frees rel [])
   4.169 +    val rel_vars = Term.add_vars rel []
   4.170 +    val rel_tvars = Term.add_tvars rel []
   4.171 +    val qty_str = Binding.print qty_name ^ ": "
   4.172 +
   4.173 +    val illegal_rel_vars =
   4.174 +      if null rel_vars andalso null rel_tvars then []
   4.175 +      else [qty_str ^ "illegal schematic variable(s) in the relation."]
   4.176 +
   4.177 +    val dup_vs =
   4.178 +      (case duplicates (op =) vs of
   4.179 +        [] => []
   4.180 +      | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
   4.181 +
   4.182 +    val extra_rty_tfrees =
   4.183 +      (case subtract (op =) vs rty_tfreesT of
   4.184 +        [] => []
   4.185 +      | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
   4.186 +
   4.187 +    val extra_rel_tfrees =
   4.188 +      (case subtract (op =) vs rel_tfrees of
   4.189 +        [] => []
   4.190 +      | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
   4.191 +
   4.192 +    val illegal_rel_frees =
   4.193 +      (case rel_frees of
   4.194 +        [] => []
   4.195 +      | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
   4.196 +
   4.197 +    val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
   4.198 +  in
   4.199 +    if null errs then () else error (cat_lines errs)
   4.200 +  end
   4.201 +
   4.202 +(* check for existence of map functions *)
   4.203 +fun map_check thy (_, (rty, _, _), _) =
   4.204 +  let
   4.205 +    fun map_check_aux rty warns =
   4.206 +      (case rty of
   4.207 +        Type (_, []) => warns
   4.208 +      | Type (s, _) =>
   4.209 +          if is_some (Quotient_Info.lookup_quotmaps_global thy s) then warns else s :: warns
   4.210 +      | _ => warns)
   4.211 +
   4.212 +    val warns = map_check_aux rty []
   4.213 +  in
   4.214 +    if null warns then ()
   4.215 +    else warning ("No map function defined for " ^ commas warns ^
   4.216 +      ". This will cause problems later on.")
   4.217 +  end
   4.218 +
   4.219 +
   4.220 +
   4.221 +(*** interface and syntax setup ***)
   4.222 +
   4.223 +
   4.224 +(* the ML-interface takes a list of 5-tuples consisting of:
   4.225 +
   4.226 + - the name of the quotient type
   4.227 + - its free type variables (first argument)
   4.228 + - its mixfix annotation
   4.229 + - the type to be quotient
   4.230 + - the partial flag (a boolean)
   4.231 + - the relation according to which the type is quotient
   4.232 +
   4.233 + it opens a proof-state in which one has to show that the
   4.234 + relations are equivalence relations
   4.235 +*)
   4.236 +
   4.237 +fun quotient_type quot_list lthy =
   4.238 +  let
   4.239 +    (* sanity check *)
   4.240 +    val _ = List.app sanity_check quot_list
   4.241 +    val _ = List.app (map_check (Proof_Context.theory_of lthy)) quot_list
   4.242 +
   4.243 +    fun mk_goal (rty, rel, partial) =
   4.244 +      let
   4.245 +        val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   4.246 +        val const =
   4.247 +          if partial then @{const_name part_equivp} else @{const_name equivp}
   4.248 +      in
   4.249 +        HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
   4.250 +      end
   4.251 +
   4.252 +    val goals = map (mk_goal o #2) quot_list
   4.253 +
   4.254 +    fun after_qed [thms] = fold (snd oo add_quotient_type) (quot_list ~~ thms)
   4.255 +  in
   4.256 +    Proof.theorem NONE after_qed [map (rpair []) goals] lthy
   4.257 +  end
   4.258 +
   4.259 +fun quotient_type_cmd specs lthy =
   4.260 +  let
   4.261 +    fun parse_spec (((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
   4.262 +      let
   4.263 +        val rty = Syntax.read_typ lthy rty_str
   4.264 +        val lthy1 = Variable.declare_typ rty lthy
   4.265 +        val rel =
   4.266 +          Syntax.parse_term lthy1 rel_str
   4.267 +          |> Type.constraint (rty --> rty --> @{typ bool})
   4.268 +          |> Syntax.check_term lthy1
   4.269 +        val lthy2 = Variable.declare_term rel lthy1
   4.270 +      in
   4.271 +        (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), lthy2)
   4.272 +      end
   4.273 +
   4.274 +    val (spec', lthy') = fold_map parse_spec specs lthy
   4.275 +  in
   4.276 +    quotient_type spec' lthy'
   4.277 +  end
   4.278 +
   4.279 +val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
   4.280 +
   4.281 +val quotspec_parser =
   4.282 +  Parse.and_list1
   4.283 +    ((Parse.type_args -- Parse.binding) --
   4.284 +      Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
   4.285 +        (Parse.$$$ "/" |-- (partial -- Parse.term))  --
   4.286 +        Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
   4.287 +
   4.288 +val _ = Keyword.keyword "/"
   4.289 +
   4.290 +val _ =
   4.291 +  Outer_Syntax.local_theory_to_proof "quotient_type"
   4.292 +    "quotient type definitions (require equivalence proofs)"
   4.293 +       Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
   4.294 +
   4.295 +end;