# HG changeset patch # User wenzelm # Date 1126642763 -7200 # Node ID ab97ccef124abd93e44538389f46fd9a5138aab3 # Parent 6b8a7bb820bbbda9c945829a9a45fddd498b2628 tuned Isar interfaces; tuned IsarThy.theorem_i; diff -r 6b8a7bb820bb -r ab97ccef124a src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Tue Sep 13 22:19:22 2005 +0200 +++ b/src/HOL/Tools/typedef_package.ML Tue Sep 13 22:19:23 2005 +0200 @@ -21,10 +21,10 @@ {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, Rep_induct: thm, Abs_induct: thm} - val typedef_proof: (bool * string) * (bstring * string list * mixfix) * string - * (string * string) option -> bool -> theory -> ProofHistory.T - val typedef_proof_i: (bool * string) * (bstring * string list * mixfix) * term - * (string * string) option -> bool -> theory -> ProofHistory.T + val typedef: (bool * string) * (bstring * string list * mixfix) * string + * (string * string) option -> theory -> Proof.state + val typedef_i: (bool * string) * (bstring * string list * mixfix) * term + * (string * string) option -> theory -> Proof.state val setup: (theory -> theory) list end; @@ -240,6 +240,8 @@ (* add_typedef interfaces *) +local + fun gen_typedef prep_term def name typ set opt_morphs tac1 names thms tac2 thy = let val (cset, goal, _, typedef_result) = @@ -252,24 +254,34 @@ gen_typedef prep_term def (if_none opt_name (#1 typ)) typ set opt_morphs all_tac [] [] (SOME tac); +in + fun add_typedef_x name typ set names thms tac = #1 o gen_typedef read_term true name typ set NONE (Tactic.rtac exI 1) names thms tac; val add_typedef = sane_typedef read_term; val add_typedef_i = sane_typedef cert_term; +end; -(* typedef_proof interface *) + +(* Isar typedef interface *) -fun gen_typedef_proof prep_term ((def, name), typ, set, opt_morphs) int thy = +local + +fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy = let val (_, goal, goal_pat, att_result) = prepare_typedef prep_term def name typ set opt_morphs thy; val att = #1 o att_result; - in thy |> IsarThy.theorem_i Drule.internalK (("", [att]), (goal, ([goal_pat], []))) int end; + in IsarThy.theorem_i Drule.internalK ("", [att]) (goal, ([goal_pat], [])) thy end; + +in -val typedef_proof = gen_typedef_proof read_term; -val typedef_proof_i = gen_typedef_proof cert_term; +val typedef = gen_typedef read_term; +val typedef_i = gen_typedef cert_term; + +end; @@ -379,19 +391,19 @@ Toplevel.theory (add_typedecls [(t, vs, mx)]))); -val typedef_proof_decl = +val typedef_decl = Scan.optional (P.$$$ "(" |-- ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name)); -fun mk_typedef_proof ((((((def, opt_name), (vs, t)), mx), A), morphs)) = - typedef_proof ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs); +fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = + typedef ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs); val typedefP = OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal - (typedef_proof_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef_proof))); + (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef))); val _ = OuterSyntax.add_keywords ["morphisms"]; diff -r 6b8a7bb820bb -r ab97ccef124a src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue Sep 13 22:19:22 2005 +0200 +++ b/src/Pure/axclass.ML Tue Sep 13 22:19:23 2005 +0200 @@ -10,27 +10,22 @@ val quiet_mode: bool ref val print_axclasses: theory -> unit val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list} - val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list - -> theory -> theory * {intro: thm, axioms: thm list} - val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list - -> theory -> theory * {intro: thm, axioms: thm list} + val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list -> + theory -> theory * {intro: thm, axioms: thm list} + val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list -> + theory -> theory * {intro: thm, axioms: thm list} val add_classrel_thms: thm list -> theory -> theory val add_arity_thms: thm list -> theory -> theory val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory val add_inst_subclass_i: class * class -> tactic -> theory -> theory val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory - val instance_subclass_proof: xstring * xstring -> (theory -> theory) - -> bool -> theory -> ProofHistory.T - val instance_subclass_proof_i: class * class -> (theory -> theory) - -> bool -> theory -> ProofHistory.T - val instance_arity_proof: xstring * string list * string -> (theory -> theory) - -> bool -> theory -> ProofHistory.T - val instance_arity_proof_i: string * sort list * sort -> (theory -> theory) - -> bool -> theory -> ProofHistory.T + val instance_subclass: xstring * xstring -> theory -> Proof.state + val instance_subclass_i: class * class -> theory -> Proof.state + val instance_arity: xstring * string list * string -> theory -> Proof.state + val instance_arity_i: string * sort list * sort -> theory -> Proof.state val intro_classes_tac: thm list -> tactic val default_intro_classes_tac: thm list -> tactic - (*legacy interfaces*) val axclass_tac: thm list -> tactic val add_inst_subclass_x: xstring * xstring -> string list -> thm list @@ -317,20 +312,19 @@ local -fun inst_proof mk_prop add_thms inst after_qed int theory = - theory - |> IsarThy.multi_theorem_i Drule.internalK (K after_qed) ProofContext.export_standard - ("", [fn (thy, th) => (add_thms [th] thy, th)]) [] - (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int; +fun gen_instance mk_prop add_thms inst thy = thy + |> ProofContext.init + |> Proof.theorem_i Drule.internalK (K (fold add_thms)) NONE ("", []) + (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst)); in -val instance_subclass_proof = - inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms; -val instance_subclass_proof_i = - inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms; -val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms; -val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms; +val instance_subclass = + gen_instance (single oo (mk_classrel oo read_classrel)) add_classrel_thms; +val instance_subclass_i = + gen_instance (single oo (mk_classrel oo cert_classrel)) add_classrel_thms; +val instance_arity = gen_instance (mk_arities oo read_arity) add_arity_thms; +val instance_arity_i = gen_instance (mk_arities oo cert_arity) add_arity_thms; end; @@ -364,15 +358,13 @@ OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl ((P.name -- Scan.optional ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name - >> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs))); + >> (Toplevel.theory o (#1 oo uncurry add_axclass))); val instanceP = OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal - ((P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.xname) - >> (fn i => instance_subclass_proof i I) || - (P.xname -- (P.$$$ "::" |-- P.arity) >> P.triple2) - >> (fn i => instance_arity_proof i I)) - >> (Toplevel.print oo Toplevel.theory_to_proof)); + ((P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> instance_subclass || + P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> (instance_arity o P.triple2)) + >> (Toplevel.print oo Toplevel.theory_to_proof)); val _ = OuterSyntax.add_parsers [axclassP, instanceP];