tuned Isar interfaces;
authorwenzelm
Tue Sep 13 22:19:23 2005 +0200 (2005-09-13)
changeset 17339ab97ccef124a
parent 17338 6b8a7bb820bb
child 17340 11f959f0fe6c
tuned Isar interfaces;
tuned IsarThy.theorem_i;
src/HOL/Tools/typedef_package.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Sep 13 22:19:22 2005 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Sep 13 22:19:23 2005 +0200
     1.3 @@ -21,10 +21,10 @@
     1.4      {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
     1.5        Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
     1.6        Rep_induct: thm, Abs_induct: thm}
     1.7 -  val typedef_proof: (bool * string) * (bstring * string list * mixfix) * string
     1.8 -    * (string * string) option -> bool -> theory -> ProofHistory.T
     1.9 -  val typedef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
    1.10 -    * (string * string) option -> bool -> theory -> ProofHistory.T
    1.11 +  val typedef: (bool * string) * (bstring * string list * mixfix) * string
    1.12 +    * (string * string) option -> theory -> Proof.state
    1.13 +  val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
    1.14 +    * (string * string) option -> theory -> Proof.state
    1.15    val setup: (theory -> theory) list
    1.16  end;
    1.17  
    1.18 @@ -240,6 +240,8 @@
    1.19  
    1.20  (* add_typedef interfaces *)
    1.21  
    1.22 +local
    1.23 +
    1.24  fun gen_typedef prep_term def name typ set opt_morphs tac1 names thms tac2 thy =
    1.25    let
    1.26      val (cset, goal, _, typedef_result) =
    1.27 @@ -252,24 +254,34 @@
    1.28    gen_typedef prep_term def
    1.29      (if_none opt_name (#1 typ)) typ set opt_morphs all_tac [] [] (SOME tac);
    1.30  
    1.31 +in
    1.32 +
    1.33  fun add_typedef_x name typ set names thms tac =
    1.34    #1 o gen_typedef read_term true name typ set NONE (Tactic.rtac exI 1) names thms tac;
    1.35  
    1.36  val add_typedef = sane_typedef read_term;
    1.37  val add_typedef_i = sane_typedef cert_term;
    1.38  
    1.39 +end;
    1.40  
    1.41 -(* typedef_proof interface *)
    1.42 +
    1.43 +(* Isar typedef interface *)
    1.44  
    1.45 -fun gen_typedef_proof prep_term ((def, name), typ, set, opt_morphs) int thy =
    1.46 +local
    1.47 +
    1.48 +fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy =
    1.49    let
    1.50      val (_, goal, goal_pat, att_result) =
    1.51        prepare_typedef prep_term def name typ set opt_morphs thy;
    1.52      val att = #1 o att_result;
    1.53 -  in thy |> IsarThy.theorem_i Drule.internalK (("", [att]), (goal, ([goal_pat], []))) int end;
    1.54 +  in IsarThy.theorem_i Drule.internalK ("", [att]) (goal, ([goal_pat], [])) thy end;
    1.55 +
    1.56 +in
    1.57  
    1.58 -val typedef_proof = gen_typedef_proof read_term;
    1.59 -val typedef_proof_i = gen_typedef_proof cert_term;
    1.60 +val typedef = gen_typedef read_term;
    1.61 +val typedef_i = gen_typedef cert_term;
    1.62 +
    1.63 +end;
    1.64  
    1.65  
    1.66  
    1.67 @@ -379,19 +391,19 @@
    1.68        Toplevel.theory (add_typedecls [(t, vs, mx)])));
    1.69  
    1.70  
    1.71 -val typedef_proof_decl =
    1.72 +val typedef_decl =
    1.73    Scan.optional (P.$$$ "(" |--
    1.74        ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
    1.75          --| P.$$$ ")") (true, NONE) --
    1.76      (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
    1.77      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
    1.78  
    1.79 -fun mk_typedef_proof ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
    1.80 -  typedef_proof ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs);
    1.81 +fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
    1.82 +  typedef ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs);
    1.83  
    1.84  val typedefP =
    1.85    OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
    1.86 -    (typedef_proof_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef_proof)));
    1.87 +    (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
    1.88  
    1.89  
    1.90  val _ = OuterSyntax.add_keywords ["morphisms"];
     2.1 --- a/src/Pure/axclass.ML	Tue Sep 13 22:19:22 2005 +0200
     2.2 +++ b/src/Pure/axclass.ML	Tue Sep 13 22:19:23 2005 +0200
     2.3 @@ -10,27 +10,22 @@
     2.4    val quiet_mode: bool ref
     2.5    val print_axclasses: theory -> unit
     2.6    val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list}
     2.7 -  val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list
     2.8 -    -> theory -> theory * {intro: thm, axioms: thm list}
     2.9 -  val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list
    2.10 -    -> theory -> theory * {intro: thm, axioms: thm list}
    2.11 +  val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list ->
    2.12 +    theory -> theory * {intro: thm, axioms: thm list}
    2.13 +  val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list ->
    2.14 +    theory -> theory * {intro: thm, axioms: thm list}
    2.15    val add_classrel_thms: thm list -> theory -> theory
    2.16    val add_arity_thms: thm list -> theory -> theory
    2.17    val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory
    2.18    val add_inst_subclass_i: class * class -> tactic -> theory -> theory
    2.19    val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
    2.20    val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
    2.21 -  val instance_subclass_proof: xstring * xstring -> (theory -> theory)
    2.22 -    -> bool -> theory -> ProofHistory.T
    2.23 -  val instance_subclass_proof_i: class * class -> (theory -> theory)
    2.24 -    -> bool -> theory -> ProofHistory.T
    2.25 -  val instance_arity_proof: xstring * string list * string -> (theory -> theory)
    2.26 -    -> bool -> theory -> ProofHistory.T
    2.27 -  val instance_arity_proof_i: string * sort list * sort -> (theory -> theory)
    2.28 -    -> bool -> theory -> ProofHistory.T
    2.29 +  val instance_subclass: xstring * xstring -> theory -> Proof.state
    2.30 +  val instance_subclass_i: class * class -> theory -> Proof.state
    2.31 +  val instance_arity: xstring * string list * string -> theory -> Proof.state
    2.32 +  val instance_arity_i: string * sort list * sort -> theory -> Proof.state
    2.33    val intro_classes_tac: thm list -> tactic
    2.34    val default_intro_classes_tac: thm list -> tactic
    2.35 -
    2.36    (*legacy interfaces*)
    2.37    val axclass_tac: thm list -> tactic
    2.38    val add_inst_subclass_x: xstring * xstring -> string list -> thm list
    2.39 @@ -317,20 +312,19 @@
    2.40  
    2.41  local
    2.42  
    2.43 -fun inst_proof mk_prop add_thms inst after_qed int theory =
    2.44 -  theory
    2.45 -  |> IsarThy.multi_theorem_i Drule.internalK (K after_qed) ProofContext.export_standard
    2.46 -    ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
    2.47 -    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int;
    2.48 +fun gen_instance mk_prop add_thms inst thy = thy
    2.49 +  |> ProofContext.init
    2.50 +  |> Proof.theorem_i Drule.internalK (K (fold add_thms)) NONE ("", [])
    2.51 +    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
    2.52  
    2.53  in
    2.54  
    2.55 -val instance_subclass_proof =
    2.56 -  inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms;
    2.57 -val instance_subclass_proof_i =
    2.58 -  inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
    2.59 -val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms;
    2.60 -val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
    2.61 +val instance_subclass =
    2.62 +  gen_instance (single oo (mk_classrel oo read_classrel)) add_classrel_thms;
    2.63 +val instance_subclass_i =
    2.64 +  gen_instance (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
    2.65 +val instance_arity = gen_instance (mk_arities oo read_arity) add_arity_thms;
    2.66 +val instance_arity_i = gen_instance (mk_arities oo cert_arity) add_arity_thms;
    2.67  
    2.68  end;
    2.69  
    2.70 @@ -364,15 +358,13 @@
    2.71    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
    2.72      ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    2.73          P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name
    2.74 -      >> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs)));
    2.75 +      >> (Toplevel.theory o (#1 oo uncurry add_axclass)));
    2.76  
    2.77  val instanceP =
    2.78    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
    2.79 -   ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname)
    2.80 -      >> (fn i => instance_subclass_proof i I) ||
    2.81 -    (P.xname -- (P.$$$ "::" |-- P.arity) >> P.triple2)
    2.82 -      >> (fn i => instance_arity_proof i I))
    2.83 -   >> (Toplevel.print oo Toplevel.theory_to_proof));
    2.84 +   ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> instance_subclass ||
    2.85 +      P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> (instance_arity o P.triple2))
    2.86 +    >> (Toplevel.print oo Toplevel.theory_to_proof));
    2.87  
    2.88  val _ = OuterSyntax.add_parsers [axclassP, instanceP];
    2.89