# HG changeset patch # User wenzelm # Date 1246565882 -7200 # Node ID 342a0bad5adf30b07a6c508ab2891648cf4198a0 # Parent f3227bb306a45071675b55d8fb3b729439fc6839# Parent 4263be178c8f057ae1a5a1d33489e711966ff31a merged diff -r f3227bb306a4 -r 342a0bad5adf NEWS --- a/NEWS Thu Jul 02 21:24:32 2009 +0200 +++ b/NEWS Thu Jul 02 22:18:02 2009 +0200 @@ -37,11 +37,13 @@ * New method "linarith" invokes existing linear arithmetic decision procedure only. -* Implementation of quickcheck using generic code generator; default generators -are provided for all suitable HOL types, records and datatypes. - -* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions -Set.Pow_def and Set.image_def. INCOMPATIBILITY. +* Implementation of quickcheck using generic code generator; default +generators are provided for all suitable HOL types, records and +datatypes. + +* Constants Set.Pow and Set.image now with authentic syntax; +object-logic definitions Set.Pow_def and Set.image_def. +INCOMPATIBILITY. * Renamed theorems: Suc_eq_add_numeral_1 -> Suc_eq_plus1 @@ -49,10 +51,12 @@ Suc_plus1 -> Suc_eq_plus1 * New sledgehammer option "Full Types" in Proof General settings menu. -Causes full type information to be output to the ATPs. This slows ATPs down -considerably but eliminates a source of unsound "proofs" that fail later. - -* Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.: +Causes full type information to be output to the ATPs. This slows +ATPs down considerably but eliminates a source of unsound "proofs" +that fail later. + +* Discontinued ancient tradition to suffix certain ML module names +with "_package", e.g.: DatatypePackage ~> Datatype InductivePackage ~> Inductive @@ -61,31 +65,35 @@ INCOMPATIBILITY. -* NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory. -If possible, use NewNumberTheory, not NumberTheory. +* NewNumberTheory: Jeremy Avigad's new version of part of +NumberTheory. If possible, use NewNumberTheory, not NumberTheory. * Simplified interfaces of datatype module. INCOMPATIBILITY. -* Abbreviation "arbitrary" of "undefined" has disappeared; use "undefined" directly. -INCOMPATIBILITY. - -* New evaluator "approximate" approximates an real valued term using the same method as the -approximation method. - -* "approximate" supports now arithmetic expressions as boundaries of intervals and implements -interval splitting and taylor series expansion. - -* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in DERIV_intros -assumes composition with an additional function and matches a variable to the -derivative, which has to be solved by the simplifier. Hence -(auto intro!: DERIV_intros) computes the derivative of most elementary terms. - -* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are replaced by: -(auto intro!: DERIV_intros) -INCOMPATIBILITY. +* Abbreviation "arbitrary" of "undefined" has disappeared; use +"undefined" directly. INCOMPATIBILITY. + +* New evaluator "approximate" approximates an real valued term using +the same method as the approximation method. + +* Method "approximate" supports now arithmetic expressions as +boundaries of intervals and implements interval splitting and Taylor +series expansion. + +* Changed DERIV_intros to a dynamic fact (via Named_Thms). Each of +the theorems in DERIV_intros assumes composition with an additional +function and matches a variable to the derivative, which has to be +solved by the simplifier. Hence (auto intro!: DERIV_intros) computes +the derivative of most elementary terms. + +* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are +replaced by: (auto intro!: DERIV_intros). INCOMPATIBILITY. + *** ML *** +* Renamed NamedThmsFun to Named_Thms. INCOMPATIBILITY. + * Eliminated old Attrib.add_attributes, Method.add_methods and related cominators for "args". INCOMPATIBILITY, need to use simplified Attrib/Method.setup introduced in Isabelle2009. diff -r f3227bb306a4 -r 342a0bad5adf src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Thu Jul 02 21:24:32 2009 +0200 +++ b/src/CCL/Wfd.thy Thu Jul 02 22:18:02 2009 +0200 @@ -495,7 +495,7 @@ ML {* local - structure Data = NamedThmsFun(val name = "eval" val description = "evaluation rules"); + structure Data = Named_Thms(val name = "eval" val description = "evaluation rules"); in fun eval_tac ctxt ths = diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Deriv.thy Thu Jul 02 22:18:02 2009 +0200 @@ -315,14 +315,14 @@ text {* @{text "DERIV_intros"} *} ML {* -structure DerivIntros = NamedThmsFun +structure Deriv_Intros = Named_Thms ( val name = "DERIV_intros" val description = "DERIV introduction rules" ) *} -setup DerivIntros.setup +setup Deriv_Intros.setup lemma DERIV_cong: "\ DERIV f x :> X ; X = Y \ \ DERIV f x :> Y" by simp diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/HOL.thy Thu Jul 02 22:18:02 2009 +0200 @@ -923,9 +923,11 @@ ML_Antiquote.value "claset" (Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())"); -structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules"); +structure ResAtpset = Named_Thms + (val name = "atp" val description = "ATP rules"); -structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "theorems blacklisted for ATP"); +structure ResBlacklist = Named_Thms + (val name = "noatp" val description = "theorems blacklisted for ATP"); *} text {*ResBlacklist holds theorems blacklisted to sledgehammer. @@ -1982,19 +1984,18 @@ Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k))))) *} "solve goal by normalization" + subsubsection {* Quickcheck *} ML {* -structure Quickcheck_RecFun_Simp_Thms = NamedThmsFun +structure Quickcheck_RecFun_Simps = Named_Thms ( val name = "quickcheck_recfun_simp" val description = "simplification rules of recursive functions as needed by Quickcheck" ) *} -setup {* - Quickcheck_RecFun_Simp_Thms.setup -*} +setup Quickcheck_RecFun_Simps.setup setup {* Quickcheck.add_generator ("SML", Codegen.test_term) @@ -2008,22 +2009,22 @@ text {* This will be relocated once Nitpick is moved to HOL. *} ML {* -structure Nitpick_Const_Def_Thms = NamedThmsFun +structure Nitpick_Const_Defs = Named_Thms ( val name = "nitpick_const_def" val description = "alternative definitions of constants as needed by Nitpick" ) -structure Nitpick_Const_Simp_Thms = NamedThmsFun +structure Nitpick_Const_Simps = Named_Thms ( val name = "nitpick_const_simp" val description = "equational specification of constants as needed by Nitpick" ) -structure Nitpick_Const_Psimp_Thms = NamedThmsFun +structure Nitpick_Const_Psimps = Named_Thms ( val name = "nitpick_const_psimp" val description = "partial equational specification of constants as needed by Nitpick" ) -structure Nitpick_Ind_Intro_Thms = NamedThmsFun +structure Nitpick_Ind_Intros = Named_Thms ( val name = "nitpick_ind_intro" val description = "introduction rules for (co)inductive predicates as needed by Nitpick" @@ -2031,10 +2032,10 @@ *} setup {* - Nitpick_Const_Def_Thms.setup - #> Nitpick_Const_Simp_Thms.setup - #> Nitpick_Const_Psimp_Thms.setup - #> Nitpick_Ind_Intro_Thms.setup + Nitpick_Const_Defs.setup + #> Nitpick_Const_Simps.setup + #> Nitpick_Const_Psimps.setup + #> Nitpick_Ind_Intros.setup *} diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Limits.thy --- a/src/HOL/Limits.thy Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Limits.thy Thu Jul 02 22:18:02 2009 +0200 @@ -350,7 +350,7 @@ lemmas Zfun_mult_left = mult.Zfun_left -subsection{* Limits *} +subsection {* Limits *} definition tendsto :: "('a \ 'b::topological_space) \ 'b \ 'a net \ bool" @@ -358,13 +358,15 @@ where [code del]: "(f ---> l) net \ (\S. open S \ l \ S \ eventually (\x. f x \ S) net)" -ML{* -structure TendstoIntros = - NamedThmsFun(val name = "tendsto_intros" - val description = "introduction rules for tendsto"); +ML {* +structure Tendsto_Intros = Named_Thms +( + val name = "tendsto_intros" + val description = "introduction rules for tendsto" +) *} -setup TendstoIntros.setup +setup Tendsto_Intros.setup lemma topological_tendstoI: "(\S. open S \ l \ S \ eventually (\x. f x \ S) net) diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Thu Jul 02 22:18:02 2009 +0200 @@ -373,7 +373,7 @@ lthy'' |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"), map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]), + [Simplifier.simp_add, Nitpick_Const_Simps.add]), maps snd simps') |> snd end) diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/OrderedGroup.thy Thu Jul 02 22:18:02 2009 +0200 @@ -22,13 +22,15 @@ \end{itemize} *} -ML{* -structure AlgebraSimps = - NamedThmsFun(val name = "algebra_simps" - val description = "algebra simplification rules"); +ML {* +structure Algebra_Simps = Named_Thms +( + val name = "algebra_simps" + val description = "algebra simplification rules" +) *} -setup AlgebraSimps.setup +setup Algebra_Simps.setup text{* The rewrites accumulated in @{text algebra_simps} deal with the classical algebraic structures of groups, rings and family. They simplify diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jul 02 22:18:02 2009 +0200 @@ -264,7 +264,7 @@ thy2 |> Sign.add_path (space_implode "_" new_type_names) |> PureThy.add_thmss [((Binding.name "recs", rec_thms), - [Nitpick_Const_Simp_Thms.add])] + [Nitpick_Const_Simps.add])] ||> Sign.parent_path ||> Theory.checkpoint |-> (fn thms => pair (reccomb_names, Library.flat thms)) @@ -337,7 +337,7 @@ (DatatypeProp.make_cases new_type_names descr sorts thy2) in thy2 - |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms + |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms o Context.Theory |> parent_path (#flat_names config) |> store_thmss "cases" new_type_names case_thms diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/Function/fundef.ML --- a/src/HOL/Tools/Function/fundef.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/Function/fundef.ML Thu Jul 02 22:18:02 2009 +0200 @@ -37,12 +37,12 @@ val simp_attribs = map (Attrib.internal o K) [Simplifier.simp_add, Code.add_default_eqn_attribute, - Nitpick_Const_Simp_Thms.add, - Quickcheck_RecFun_Simp_Thms.add] + Nitpick_Const_Simps.add, + Quickcheck_RecFun_Simps.add] val psimp_attribs = map (Attrib.internal o K) [Simplifier.simp_add, - Nitpick_Const_Psimp_Thms.add] + Nitpick_Const_Psimps.add] fun note_theorem ((name, atts), ths) = LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths) @@ -202,7 +202,7 @@ "declaration of congruence rule for function definitions" #> setup_case_cong #> FundefRelation.setup - #> FundefCommon.TerminationSimps.setup + #> FundefCommon.Termination_Simps.setup val get_congs = FundefCtxTree.get_fundef_congs diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/Function/fundef_common.ML --- a/src/HOL/Tools/Function/fundef_common.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_common.ML Thu Jul 02 22:18:02 2009 +0200 @@ -144,7 +144,7 @@ (* Simp rules for termination proofs *) -structure TerminationSimps = NamedThmsFun +structure Termination_Simps = Named_Thms ( val name = "termination_simp" val description = "Simplification rule for termination proofs" diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 02 22:18:02 2009 +0200 @@ -216,7 +216,8 @@ fun lexicographic_order_tac ctxt = TRY (FundefCommon.apply_termination_rule ctxt 1) - THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt)) + THEN lex_order_tac ctxt + (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt)) val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/Function/measure_functions.ML --- a/src/HOL/Tools/Function/measure_functions.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/Function/measure_functions.ML Thu Jul 02 22:18:02 2009 +0200 @@ -1,7 +1,7 @@ (* Title: HOL/Tools/Function/measure_functions.ML Author: Alexander Krauss, TU Muenchen -Measure functions, generated heuristically +Measure functions, generated heuristically. *) signature MEASURE_FUNCTIONS = @@ -16,7 +16,8 @@ struct (** User-declared size functions **) -structure MeasureHeuristicRules = NamedThmsFun( +structure Measure_Heuristic_Rules = Named_Thms +( val name = "measure_function" val description = "Rules that guide the heuristic generation of measure functions" ); @@ -24,7 +25,7 @@ fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t fun find_measures ctxt T = - DEPTH_SOLVE (resolve_tac (MeasureHeuristicRules.get ctxt) 1) + DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT))) |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init) |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) @@ -41,7 +42,7 @@ @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT) | mk_funorder_funs T = [ constant_1 T ] -fun mk_ext_base_funs ctxt (Type("+", [fT, sT])) = +fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) = map_product (SumTree.mk_sumcase fT sT HOLogic.natT) (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT) | mk_ext_base_funs ctxt T = find_measures ctxt T @@ -52,7 +53,7 @@ val get_measure_functions = mk_all_measure_funs -val setup = MeasureHeuristicRules.setup +val setup = Measure_Heuristic_Rules.setup end diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/Function/scnp_reconstruct.ML --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 02 22:18:02 2009 +0200 @@ -405,7 +405,7 @@ fun decomp_scnp orders ctxt = let - val extra_simps = FundefCommon.TerminationSimps.get ctxt + val extra_simps = FundefCommon.Termination_Simps.get ctxt val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps) in SIMPLE_METHOD diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/Function/size.ML Thu Jul 02 22:18:02 2009 +0200 @@ -209,7 +209,7 @@ val ([size_thms], thy'') = PureThy.add_thmss [((Binding.name "size", size_eqns), - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, + [Simplifier.simp_add, Nitpick_Const_Simps.add, Thm.declaration_attribute (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy' diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/arith_data.ML Thu Jul 02 22:18:02 2009 +0200 @@ -28,7 +28,8 @@ (* slots for plugging in arithmetic facts and tactics *) -structure Arith_Facts = NamedThmsFun( +structure Arith_Facts = Named_Thms +( val name = "arith" val description = "arith facts - only ground formulas" ); diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/inductive.ML Thu Jul 02 22:18:02 2009 +0200 @@ -694,7 +694,7 @@ LocalTheory.notes kind (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th], [Attrib.internal (K (ContextRules.intro_query NONE)), - Attrib.internal (K Nitpick_Ind_Intro_Thms.add)])]) intrs) |>> + Attrib.internal (K Nitpick_Ind_Intros.add)])]) intrs) |>> map (hd o snd); val (((_, elims'), (_, [induct'])), ctxt2) = ctxt1 |> diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/old_primrec.ML Thu Jul 02 22:18:02 2009 +0200 @@ -283,8 +283,8 @@ val simps'' = maps snd simps'; in thy'' - |> note (("simps", [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, - Code.add_default_eqn_attribute]), simps'') + |> note (("simps", + [Simplifier.simp_add, Nitpick_Const_Simps.add, Code.add_default_eqn_attribute]), simps'') |> snd |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns]) |> snd diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/primrec.ML Thu Jul 02 22:18:02 2009 +0200 @@ -272,7 +272,7 @@ (Binding.qualify false prefix b, Code.add_default_eqn_attrib :: attrs)) spec; fun simp_attr_binding prefix = (Binding.qualify true prefix (Binding.name "simps"), map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]); + [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]); in lthy |> set_group ? LocalTheory.set_group (serial_string ()) diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Thu Jul 02 22:18:02 2009 +0200 @@ -244,7 +244,7 @@ |-> (fn proto_simps => prove_simps proto_simps) |-> (fn simps => LocalTheory.note Thm.generatedK ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K) - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add]), + [Simplifier.simp_add, Nitpick_Const_Simps.add, Quickcheck_RecFun_Simps.add]), simps)) |> snd end diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/recdef.ML Thu Jul 02 22:18:02 2009 +0200 @@ -207,8 +207,8 @@ tfl_fn not_permissive thy cs (ss delcongs [imp_cong]) congs wfs name R eqs; val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx); - val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, - Code.add_default_eqn_attribute, Quickcheck_RecFun_Simp_Thms.add] else []; + val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simps.add, + Code.add_default_eqn_attribute, Quickcheck_RecFun_Simps.add] else []; val ((simps' :: rules', [induct']), thy) = thy diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/Tools/record.ML Thu Jul 02 22:18:02 2009 +0200 @@ -2192,7 +2192,7 @@ thms_thy |> (snd oo PureThy.add_thmss) [((Binding.name "simps", sel_upd_simps), - [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]), + [Simplifier.simp_add, Nitpick_Const_Simps.add]), ((Binding.name "iffs", iffs), [iff_add])] |> put_record name (make_record_info args parent fields extension induct_scheme') |> put_sel_upd (names @ [full_moreN]) sel_upd_simps diff -r f3227bb306a4 -r 342a0bad5adf src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOL/ex/Numeral.thy Thu Jul 02 22:18:02 2009 +0200 @@ -93,11 +93,14 @@ subsection {* Numeral operations *} ML {* -structure DigSimps = - NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals") +structure Dig_Simps = Named_Thms +( + val name = "numeral" + val description = "Simplification rules for numerals" +) *} -setup DigSimps.setup +setup Dig_Simps.setup instantiation num :: "{plus,times,ord}" begin diff -r f3227bb306a4 -r 342a0bad5adf src/HOLCF/Cont.thy --- a/src/HOLCF/Cont.thy Thu Jul 02 21:24:32 2009 +0200 +++ b/src/HOLCF/Cont.thy Thu Jul 02 22:18:02 2009 +0200 @@ -140,8 +140,11 @@ subsection {* Continuity simproc *} ML {* -structure Cont2ContData = NamedThmsFun - ( val name = "cont2cont" val description = "continuity intro rule" ) +structure Cont2ContData = Named_Thms +( + val name = "cont2cont" + val description = "continuity intro rule" +) *} setup Cont2ContData.setup diff -r f3227bb306a4 -r 342a0bad5adf src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/Pure/Isar/class.ML Thu Jul 02 22:18:02 2009 +0200 @@ -90,7 +90,7 @@ val sup_of_classes = map (snd o rules thy) sups; val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class); val axclass_intro = #intro (AxClass.get_info thy class); - val base_sort_trivs = Drule.sort_triv thy (aT, base_sort); + val base_sort_trivs = Thm.sort_triv thy (aT, base_sort); val tac = REPEAT (SOMEGOAL (Tactic.match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs) diff -r f3227bb306a4 -r 342a0bad5adf src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Thu Jul 02 22:18:02 2009 +0200 @@ -54,6 +54,7 @@ (Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn), (Binding.name "Hyp", propT --> proofT, NoSyn), (Binding.name "Oracle", propT --> proofT, NoSyn), + (Binding.name "Inclass", (Term.a_itselfT --> propT) --> proofT, NoSyn), (Binding.name "MinProof", proofT, Delimfix "?")] |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"] |> Sign.add_syntax_i @@ -112,6 +113,12 @@ | NONE => error ("Unknown theorem " ^ quote name)) end | _ => error ("Illegal proof constant name: " ^ quote s)) + | prf_of Ts (Const ("Inclass", _) $ Const (c_class, _)) = + (case try Logic.class_of_const c_class of + SOME c => + change_type (if ty then SOME Ts else NONE) + (Inclass (TVar ((Name.aT, 0), []), c)) + | NONE => error ("Bad class constant: " ^ quote c_class)) | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) = @@ -141,6 +148,7 @@ val AppPt = Const ("AppP", [proofT, proofT] ---> proofT); val Hypt = Const ("Hyp", propT --> proofT); val Oraclet = Const ("Oracle", propT --> proofT); +val Inclasst = Const ("Inclass", (Term.itselfT dummyT --> propT) --> proofT); val MinProoft = Const ("MinProof", proofT); val mk_tyapp = fold (fn T => fn prf => Const ("Appt", @@ -153,6 +161,8 @@ | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT) | term_of _ (PAxm (name, _, SOME Ts)) = mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT)) + | term_of _ (Inclass (T, c)) = + mk_tyapp [T] (Inclasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT)) | term_of _ (PBound i) = Bound i | term_of Ts (Abst (s, opT, prf)) = let val T = the_default dummyT opT diff -r f3227bb306a4 -r 342a0bad5adf src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/Pure/Proof/reconstruct.ML Thu Jul 02 22:18:02 2009 +0200 @@ -140,7 +140,8 @@ let val tvars = OldTerm.term_tvars prop; val tfrees = OldTerm.term_tfrees prop; - val (env', Ts) = (case opTs of + val (env', Ts) = + (case opTs of NONE => Library.foldl_map mk_tvar (env, map snd tvars @ map snd tfrees) | SOME Ts => (env, Ts)); val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) @@ -222,6 +223,8 @@ mk_cnstrts_atom env vTs prop opTs prf | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) = mk_cnstrts_atom env vTs prop opTs prf + | mk_cnstrts env _ _ vTs (prf as Inclass (T, c)) = + mk_cnstrts_atom env vTs (Logic.mk_inclass (T, c)) NONE prf | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) = mk_cnstrts_atom env vTs prop opTs prf | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs) @@ -318,6 +321,7 @@ | prop_of0 Hs (Hyp t) = t | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts | prop_of0 Hs (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts + | prop_of0 Hs (Inclass (T, c)) = Logic.mk_inclass (T, c) | prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts | prop_of0 _ _ = error "prop_of: partial proof object"; diff -r f3227bb306a4 -r 342a0bad5adf src/Pure/Tools/named_thms.ML --- a/src/Pure/Tools/named_thms.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/Pure/Tools/named_thms.ML Thu Jul 02 22:18:02 2009 +0200 @@ -14,7 +14,7 @@ val setup: theory -> theory end; -functor NamedThmsFun(val name: string val description: string): NAMED_THMS = +functor Named_Thms(val name: string val description: string): NAMED_THMS = struct structure Data = GenericDataFun diff -r f3227bb306a4 -r 342a0bad5adf src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/Pure/axclass.ML Thu Jul 02 22:18:02 2009 +0200 @@ -580,7 +580,7 @@ | T as TVar (_, S) => insert (eq_fst op =) (T, S) | _ => I) typ []; val hyps = vars - |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S)); + |> map (fn (T, S) => (T, Thm.sort_triv thy (T, S) ~~ S)); val ths = (typ, sort) |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy) {class_relation = diff -r f3227bb306a4 -r 342a0bad5adf src/Pure/drule.ML --- a/src/Pure/drule.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/Pure/drule.ML Thu Jul 02 22:18:02 2009 +0200 @@ -108,7 +108,6 @@ val dummy_thm: thm val sort_constraintI: thm val sort_constraint_eq: thm - val sort_triv: theory -> typ * sort -> thm list val unconstrainTs: thm -> thm val with_subgoal: int -> (thm -> thm) -> thm -> thm val comp_no_flatten: thm * int -> int -> thm -> thm @@ -209,15 +208,6 @@ (* type classes and sorts *) -fun sort_triv thy (T, S) = - let - val certT = Thm.ctyp_of thy; - val cT = certT T; - fun class_triv c = - Thm.class_triv thy c - |> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []); - in map class_triv S end; - fun unconstrainTs th = fold (Thm.unconstrainT o Thm.ctyp_of (Thm.theory_of_thm th) o TVar) (Thm.fold_terms Term.add_tvars th []) th; diff -r f3227bb306a4 -r 342a0bad5adf src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/Pure/more_thm.ML Thu Jul 02 22:18:02 2009 +0200 @@ -26,6 +26,7 @@ val eq_thm_thy: thm * thm -> bool val eq_thm_prop: thm * thm -> bool val equiv_thm: thm * thm -> bool + val sort_triv: theory -> typ * sort -> thm list val check_shyps: sort list -> thm -> thm val is_dummy: thm -> bool val plain_prop_of: thm -> term @@ -168,7 +169,16 @@ Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths); -(* sort hypotheses *) +(* type classes and sorts *) + +fun sort_triv thy (T, S) = + let + val certT = Thm.ctyp_of thy; + val cT = certT T; + fun class_triv c = + Thm.class_triv thy c + |> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []); + in map class_triv S end; fun check_shyps sorts raw_th = let diff -r f3227bb306a4 -r 342a0bad5adf src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/Pure/proofterm.ML Thu Jul 02 22:18:02 2009 +0200 @@ -19,6 +19,7 @@ | op %% of proof * proof | Hyp of term | PAxm of string * term * typ list option + | Inclass of typ * class | Oracle of string * term * typ list option | Promise of serial * term * typ list | PThm of serial * ((string * term * typ list option) * proof_body future) @@ -140,6 +141,7 @@ | op %% of proof * proof | Hyp of term | PAxm of string * term * typ list option + | Inclass of typ * class | Oracle of string * term * typ list option | Promise of serial * term * typ list | PThm of serial * ((string * term * typ list option) * proof_body future) @@ -290,6 +292,7 @@ | mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2 handle SAME => prf1 %% mapp prf2) | mapp (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (map_typs Ts)) + | mapp (Inclass (T, c)) = Inclass (apsome g (SOME T) |> the, c) | mapp (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (map_typs Ts)) | mapp (Promise (i, prop, Ts)) = Promise (i, prop, map_typs Ts) | mapp (PThm (i, ((a, prop, SOME Ts), body))) = @@ -317,6 +320,7 @@ | fold_proof_terms f g (prf1 %% prf2) = fold_proof_terms f g prf1 #> fold_proof_terms f g prf2 | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts + | fold_proof_terms _ g (Inclass (T, _)) = g T | fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts | fold_proof_terms _ g (Promise (_, _, Ts)) = fold g Ts | fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts @@ -331,6 +335,7 @@ | size_of_proof _ = 1; fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs) + | change_type (SOME [T]) (Inclass (_, c)) = Inclass (T, c) | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs) | change_type opTs (Promise _) = error "change_type: unexpected promise" | change_type opTs (PThm (i, ((name, prop, _), body))) = PThm (i, ((name, prop, opTs), body)) @@ -468,6 +473,7 @@ | norm (prf1 %% prf2) = (norm prf1 %% normh prf2 handle SAME => prf1 %% norm prf2) | norm (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome' (htypeTs norm_types_same) Ts) + | norm (Inclass (T, c)) = Inclass (htypeT norm_type_same T, c) | norm (Oracle (s, prop, Ts)) = Oracle (s, prop, apsome' (htypeTs norm_types_same) Ts) | norm (Promise (i, prop, Ts)) = Promise (i, prop, htypeTs norm_types_same Ts) | norm (PThm (i, ((s, t, Ts), body))) = @@ -713,6 +719,8 @@ handle SAME => prf1 %% lift' Us Ts prf2) | lift' _ _ (PAxm (s, prop, Ts)) = PAxm (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts) + | lift' _ _ (Inclass (T, c)) = + Inclass (same (op =) (Logic.incr_tvar inc) T, c) | lift' _ _ (Oracle (s, prop, Ts)) = Oracle (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts) | lift' _ _ (Promise (i, prop, Ts)) = @@ -967,8 +975,9 @@ orelse has_duplicates (op =) (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts)) orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf) - | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp t) - | shrink' ls lev ts prfs MinProof = ([], false, map (pair false) ts, MinProof) + | shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf) + | shrink' ls lev ts prfs (prf as MinProof) = ([], false, map (pair false) ts, prf) + | shrink' ls lev ts prfs (prf as Inclass _) = ([], false, map (pair false) ts, prf) | shrink' ls lev ts prfs prf = let val prop = @@ -1060,6 +1069,9 @@ | mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) = if s1 = s2 then optmatch matchTs inst (opTs, opUs) else raise PMatch + | mtch Ts i j inst (Inclass (T1, c1), Inclass (T2, c2)) = + if c1 = c2 then matchT inst (T1, T2) + else raise PMatch | mtch Ts i j inst (PThm (_, ((name1, prop1, opTs), _)), PThm (_, ((name2, prop2, opUs), _))) = if name1 = name2 andalso prop1 = prop2 then optmatch matchTs inst (opTs, opUs) @@ -1091,6 +1103,7 @@ NONE => prf | SOME prf' => incr_pboundvars plev tlev prf') | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Option.map (map substT) Ts) + | subst _ _ (Inclass (T, c)) = Inclass (substT T, c) | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Option.map (map substT) Ts) | subst _ _ (Promise (i, prop, Ts)) = Promise (i, prop, (map substT) Ts) | subst _ _ (PThm (i, ((id, prop, Ts), body))) = @@ -1117,6 +1130,7 @@ (_, Hyp (Var _)) => true | (Hyp (Var _), _) => true | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2 + | (Inclass (_, c), Inclass (_, d)) => c = d andalso matchrands prf1 prf2 | (PThm (_, ((a, propa, _), _)), PThm (_, ((b, propb, _), _))) => a = b andalso propa = propb andalso matchrands prf1 prf2 | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2 diff -r f3227bb306a4 -r 342a0bad5adf src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/Pure/thm.ML Thu Jul 02 22:18:02 2009 +0200 @@ -487,7 +487,8 @@ val extra' = Sorts.subtract (map #2 (Sign.witness_sorts thy present extra)) extra |> Sorts.minimal_sorts (Sign.classes_of thy); - val shyps' = Sorts.union present extra'; + val shyps' = Sorts.union present extra' + |> Sorts.remove_sort []; in Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx, shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) @@ -1110,15 +1111,21 @@ prop = Logic.mk_implies (A, A)}); (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) -fun class_triv thy c = +fun class_triv thy raw_c = let - val Cterm {t, maxidx, sorts, ...} = - cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c)) - handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); - val der = deriv_rule0 (Pt.PAxm ("Pure.class_triv:" ^ c, t, SOME [])); + val c = Sign.certify_class thy raw_c; + val T = TVar ((Name.aT, 0), [c]); + val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_inclass (T, c)) + handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); in - Thm (der, {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx, - shyps = sorts, hyps = [], tpairs = [], prop = t}) + Thm (deriv_rule0 (Pt.Inclass (T, c)), + {thy_ref = Theory.check_thy thy, + tags = [], + maxidx = maxidx, + shyps = sorts, + hyps = [], + tpairs = [], + prop = prop}) end; (*Internalize sort constraints of type variable*) diff -r f3227bb306a4 -r 342a0bad5adf src/Tools/atomize_elim.ML --- a/src/Tools/atomize_elim.ML Thu Jul 02 21:24:32 2009 +0200 +++ b/src/Tools/atomize_elim.ML Thu Jul 02 22:18:02 2009 +0200 @@ -20,7 +20,9 @@ struct (* theory data *) -structure AtomizeElimData = NamedThmsFun( + +structure AtomizeElimData = Named_Thms +( val name = "atomize_elim"; val description = "atomize_elim rewrite rule"; ); diff -r f3227bb306a4 -r 342a0bad5adf src/ZF/UNITY/Constrains.thy --- a/src/ZF/UNITY/Constrains.thy Thu Jul 02 21:24:32 2009 +0200 +++ b/src/ZF/UNITY/Constrains.thy Thu Jul 02 22:18:02 2009 +0200 @@ -462,7 +462,11 @@ val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I}); (*To allow expansion of the program's definition when appropriate*) -structure ProgramDefs = NamedThmsFun(val name = "program" val description = "program definitions"); +structure Program_Defs = Named_Thms +( + val name = "program" + val description = "program definitions" +); (*proves "co" properties when the program is specified*) @@ -478,7 +482,7 @@ (* Three subgoals *) rewrite_goal_tac [@{thm st_set_def}] 3, REPEAT (force_tac css 2), - full_simp_tac (ss addsimps (ProgramDefs.get ctxt)) 1, + full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1, ALLGOALS (clarify_tac cs), REPEAT (FIRSTGOAL (etac disjE)), ALLGOALS (clarify_tac cs), @@ -493,7 +497,7 @@ rtac @{thm AlwaysI} i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i; *} -setup ProgramDefs.setup +setup Program_Defs.setup method_setup safety = {* Scan.succeed (SIMPLE_METHOD' o constrains_tac) *} diff -r f3227bb306a4 -r 342a0bad5adf src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Thu Jul 02 21:24:32 2009 +0200 +++ b/src/ZF/UNITY/SubstAx.thy Thu Jul 02 22:18:02 2009 +0200 @@ -359,7 +359,7 @@ REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, @{thm EnsuresI}, @{thm ensuresI}] 1), (*now there are two subgoals: co & transient*) - simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2, + simp_tac (ss addsimps (Program_Defs.get ctxt)) 2, res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2, (*simplify the command's domain*) simp_tac (ss addsimps [@{thm domain_def}]) 3,