1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Jun 24 11:08:21 2010 +0200
1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Jun 24 12:33:51 2010 +0100
1.3 @@ -7,13 +7,13 @@
1.4 signature QUOTIENT_DEF =
1.5 sig
1.6 val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->
1.7 - local_theory -> (term * thm) * local_theory
1.8 + local_theory -> Quotient_Info.qconsts_info * local_theory
1.9
1.10 val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
1.11 - local_theory -> (term * thm) * local_theory
1.12 + local_theory -> Quotient_Info.qconsts_info * local_theory
1.13
1.14 val quotient_lift_const: typ list -> string * term -> local_theory ->
1.15 - (term * thm) * local_theory
1.16 + Quotient_Info.qconsts_info * local_theory
1.17 end;
1.18
1.19 structure Quotient_Def: QUOTIENT_DEF =
1.20 @@ -45,7 +45,7 @@
1.21 val pos = Position.str_of (Binding.pos_of bind)
1.22 in
1.23 error ("Head of quotient_definition " ^
1.24 - (quote str) ^ " differs from declaration " ^ name ^ pos)
1.25 + quote str ^ " differs from declaration " ^ name ^ pos)
1.26 end
1.27
1.28 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
1.29 @@ -69,12 +69,14 @@
1.30 val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
1.31
1.32 (* data storage *)
1.33 - fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
1.34 + val qconst_data = {qconst = trm, rconst = rhs, def = thm}
1.35 +
1.36 + fun qcinfo phi = transform_qconsts phi qconst_data
1.37 fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
1.38 val lthy'' = Local_Theory.declaration true
1.39 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
1.40 in
1.41 - ((trm, thm), lthy'')
1.42 + (qconst_data, lthy'')
1.43 end
1.44
1.45 fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
2.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Jun 24 11:08:21 2010 +0200
2.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Jun 24 12:33:51 2010 +0100
2.3 @@ -84,7 +84,7 @@
2.4 *)
2.5 fun mk_mapfun ctxt vs rty =
2.6 let
2.7 - val vs' = map (mk_Free) vs
2.8 + val vs' = map mk_Free vs
2.9
2.10 fun mk_mapfun_aux rty =
2.11 case rty of
2.12 @@ -103,7 +103,7 @@
2.13 let
2.14 val thy = ProofContext.theory_of ctxt
2.15 val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
2.16 - val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
2.17 + val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => raise exn
2.18 in
2.19 (#rtyp qdata, #qtyp qdata)
2.20 end
3.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML Thu Jun 24 11:08:21 2010 +0200
3.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Thu Jun 24 12:33:51 2010 +0100
3.3 @@ -8,7 +8,7 @@
3.4 signature QUOTIENT_TYPE =
3.5 sig
3.6 val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm
3.7 - -> Proof.context -> (thm * thm) * local_theory
3.8 + -> Proof.context -> Quotient_Info.quotdata_info * local_theory
3.9
3.10 val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list
3.11 -> Proof.context -> Proof.state
3.12 @@ -32,11 +32,8 @@
3.13 end
3.14
3.15 fun note (name, thm, attrs) lthy =
3.16 -let
3.17 - val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy
3.18 -in
3.19 - (thm', lthy')
3.20 -end
3.21 + Local_Theory.note ((name, attrs), [thm]) lthy |> snd
3.22 +
3.23
3.24 fun intern_attr at = Attrib.internal (K at)
3.25
3.26 @@ -64,7 +61,7 @@
3.27 |> map Free
3.28 in
3.29 lambda c (HOLogic.exists_const rty $
3.30 - lambda x (HOLogic.mk_conj ((rel $ x $ x), (HOLogic.mk_eq (c, (rel $ x))))))
3.31 + lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
3.32 end
3.33
3.34
3.35 @@ -139,7 +136,10 @@
3.36 (* main function for constructing a quotient type *)
3.37 fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy =
3.38 let
3.39 - val part_equiv = if partial then equiv_thm else equiv_thm RS @{thm equivp_implies_part_equivp}
3.40 + val part_equiv =
3.41 + if partial
3.42 + then equiv_thm
3.43 + else equiv_thm RS @{thm equivp_implies_part_equivp}
3.44
3.45 (* generates the typedef *)
3.46 val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
3.47 @@ -173,15 +173,17 @@
3.48 (* name equivalence theorem *)
3.49 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
3.50
3.51 - (* storing the quot-info *)
3.52 - fun qinfo phi = transform_quotdata phi
3.53 - {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
3.54 - val lthy4 = Local_Theory.declaration true
3.55 - (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3
3.56 + (* storing the quotdata *)
3.57 + val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
3.58 +
3.59 + fun qinfo phi = transform_quotdata phi quotdata
3.60 +
3.61 + val lthy4 = lthy3
3.62 + |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
3.63 + |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
3.64 + |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
3.65 in
3.66 - lthy4
3.67 - |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
3.68 - ||>> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
3.69 + (quotdata, lthy4)
3.70 end
3.71
3.72
3.73 @@ -253,6 +255,7 @@
3.74 - its free type variables (first argument)
3.75 - its mixfix annotation
3.76 - the type to be quotient
3.77 + - the partial flag (a boolean)
3.78 - the relation according to which the type is quotient
3.79
3.80 it opens a proof-state in which one has to show that the
3.81 @@ -268,7 +271,8 @@
3.82 fun mk_goal (rty, rel, partial) =
3.83 let
3.84 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
3.85 - val const = if partial then @{const_name part_equivp} else @{const_name equivp}
3.86 + val const =
3.87 + if partial then @{const_name part_equivp} else @{const_name equivp}
3.88 in
3.89 HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
3.90 end