drop the feature that more than one quotient type can be defined by quotient_type -> it causes problems
authorkuncar
Thu May 24 14:20:25 2012 +0200 (2012-05-24)
changeset 47983a5e699834f2d
parent 47982 7aa35601ff65
child 47984 a1a5bf806d8b
drop the feature that more than one quotient type can be defined by quotient_type -> it causes problems
src/HOL/Tools/Quotient/quotient_type.ML
     1.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Thu May 24 14:20:23 2012 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Thu May 24 14:20:25 2012 +0200
     1.3 @@ -9,11 +9,11 @@
     1.4    val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
     1.5      ((binding * binding) option * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
     1.6  
     1.7 -  val quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
     1.8 -    ((binding * binding) option * bool)) list -> Proof.context -> Proof.state
     1.9 +  val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * 
    1.10 +    ((binding * binding) option * bool) -> Proof.context -> Proof.state
    1.11  
    1.12 -  val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
    1.13 -    (binding * binding) option) list -> Proof.context -> Proof.state
    1.14 +  val quotient_type_cmd: (((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
    1.15 +    (binding * binding) option -> Proof.context -> Proof.state
    1.16  end;
    1.17  
    1.18  structure Quotient_Type: QUOTIENT_TYPE =
    1.19 @@ -290,11 +290,11 @@
    1.20   relations are equivalence relations
    1.21  *)
    1.22  
    1.23 -fun quotient_type quot_list lthy =
    1.24 +fun quotient_type quot lthy =
    1.25    let
    1.26      (* sanity check *)
    1.27 -    val _ = List.app sanity_check quot_list
    1.28 -    val _ = List.app (map_check lthy) quot_list
    1.29 +    val _ = sanity_check quot
    1.30 +    val _ = map_check lthy quot
    1.31  
    1.32      fun mk_goal (rty, rel, partial) =
    1.33        let
    1.34 @@ -305,14 +305,14 @@
    1.35          HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
    1.36        end
    1.37  
    1.38 -    val goals = map (mk_goal o #2) quot_list
    1.39 +    val goal = (mk_goal o #2) quot
    1.40  
    1.41 -    fun after_qed [thms] = fold (snd oo add_quotient_type) (quot_list ~~ thms)
    1.42 +    fun after_qed [[thm]] = (snd oo add_quotient_type) (quot, thm)
    1.43    in
    1.44 -    Proof.theorem NONE after_qed [map (rpair []) goals] lthy
    1.45 +    Proof.theorem NONE after_qed [[(goal, [])]] lthy
    1.46    end
    1.47  
    1.48 -fun quotient_type_cmd specs lthy =
    1.49 +fun quotient_type_cmd spec lthy =
    1.50    let
    1.51      fun parse_spec ((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
    1.52        let
    1.53 @@ -327,7 +327,7 @@
    1.54          (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), tmp_lthy2)
    1.55        end
    1.56  
    1.57 -    val (spec', _) = fold_map parse_spec specs lthy
    1.58 +    val (spec', _) = parse_spec spec lthy
    1.59    in
    1.60      quotient_type spec' lthy
    1.61    end
    1.62 @@ -338,12 +338,11 @@
    1.63  val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
    1.64  
    1.65  val quotspec_parser =
    1.66 -  Parse.and_list1
    1.67 -    ((opt_gen_code -- Parse.type_args -- Parse.binding) --
    1.68 +     (opt_gen_code -- Parse.type_args -- Parse.binding) --
    1.69        (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
    1.70        Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
    1.71          (@{keyword "/"} |-- (partial -- Parse.term))  --
    1.72 -        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
    1.73 +        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
    1.74  
    1.75  val _ =
    1.76    Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}