src/Pure/axclass.ML
changeset 17339 ab97ccef124a
parent 17281 3b9ff0131ed1
child 17412 e26cb20ef0cc
     1.1 --- a/src/Pure/axclass.ML	Tue Sep 13 22:19:22 2005 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Sep 13 22:19:23 2005 +0200
     1.3 @@ -10,27 +10,22 @@
     1.4    val quiet_mode: bool ref
     1.5    val print_axclasses: theory -> unit
     1.6    val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list}
     1.7 -  val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list
     1.8 -    -> theory -> theory * {intro: thm, axioms: thm list}
     1.9 -  val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list
    1.10 -    -> theory -> theory * {intro: thm, axioms: thm list}
    1.11 +  val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list ->
    1.12 +    theory -> theory * {intro: thm, axioms: thm list}
    1.13 +  val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list ->
    1.14 +    theory -> theory * {intro: thm, axioms: thm list}
    1.15    val add_classrel_thms: thm list -> theory -> theory
    1.16    val add_arity_thms: thm list -> theory -> theory
    1.17    val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory
    1.18    val add_inst_subclass_i: class * class -> tactic -> theory -> theory
    1.19    val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
    1.20    val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
    1.21 -  val instance_subclass_proof: xstring * xstring -> (theory -> theory)
    1.22 -    -> bool -> theory -> ProofHistory.T
    1.23 -  val instance_subclass_proof_i: class * class -> (theory -> theory)
    1.24 -    -> bool -> theory -> ProofHistory.T
    1.25 -  val instance_arity_proof: xstring * string list * string -> (theory -> theory)
    1.26 -    -> bool -> theory -> ProofHistory.T
    1.27 -  val instance_arity_proof_i: string * sort list * sort -> (theory -> theory)
    1.28 -    -> bool -> theory -> ProofHistory.T
    1.29 +  val instance_subclass: xstring * xstring -> theory -> Proof.state
    1.30 +  val instance_subclass_i: class * class -> theory -> Proof.state
    1.31 +  val instance_arity: xstring * string list * string -> theory -> Proof.state
    1.32 +  val instance_arity_i: string * sort list * sort -> theory -> Proof.state
    1.33    val intro_classes_tac: thm list -> tactic
    1.34    val default_intro_classes_tac: thm list -> tactic
    1.35 -
    1.36    (*legacy interfaces*)
    1.37    val axclass_tac: thm list -> tactic
    1.38    val add_inst_subclass_x: xstring * xstring -> string list -> thm list
    1.39 @@ -317,20 +312,19 @@
    1.40  
    1.41  local
    1.42  
    1.43 -fun inst_proof mk_prop add_thms inst after_qed int theory =
    1.44 -  theory
    1.45 -  |> IsarThy.multi_theorem_i Drule.internalK (K after_qed) ProofContext.export_standard
    1.46 -    ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
    1.47 -    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int;
    1.48 +fun gen_instance mk_prop add_thms inst thy = thy
    1.49 +  |> ProofContext.init
    1.50 +  |> Proof.theorem_i Drule.internalK (K (fold add_thms)) NONE ("", [])
    1.51 +    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
    1.52  
    1.53  in
    1.54  
    1.55 -val instance_subclass_proof =
    1.56 -  inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms;
    1.57 -val instance_subclass_proof_i =
    1.58 -  inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
    1.59 -val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms;
    1.60 -val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
    1.61 +val instance_subclass =
    1.62 +  gen_instance (single oo (mk_classrel oo read_classrel)) add_classrel_thms;
    1.63 +val instance_subclass_i =
    1.64 +  gen_instance (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
    1.65 +val instance_arity = gen_instance (mk_arities oo read_arity) add_arity_thms;
    1.66 +val instance_arity_i = gen_instance (mk_arities oo cert_arity) add_arity_thms;
    1.67  
    1.68  end;
    1.69  
    1.70 @@ -364,15 +358,13 @@
    1.71    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
    1.72      ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    1.73          P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name
    1.74 -      >> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs)));
    1.75 +      >> (Toplevel.theory o (#1 oo uncurry add_axclass)));
    1.76  
    1.77  val instanceP =
    1.78    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    1.79 -   ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname)
    1.80 -      >> (fn i => instance_subclass_proof i I) ||
    1.81 -    (P.xname -- (P.$$$ "::" |-- P.arity) >> P.triple2)
    1.82 -      >> (fn i => instance_arity_proof i I))
    1.83 -   >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.84 +   ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> instance_subclass ||
    1.85 +      P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> (instance_arity o P.triple2))
    1.86 +    >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.87  
    1.88  val _ = OuterSyntax.add_parsers [axclassP, instanceP];
    1.89