--- 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.
--- 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 =
--- 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: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
by simp
--- 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
*}
--- 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 \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
@@ -358,13 +358,15 @@
where [code del]:
"(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> 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:
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
--- 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)
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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'
--- 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"
);
--- 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 |>
--- 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
--- 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 ())
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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";
--- 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
--- 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 =
--- 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;
--- 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
--- 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
--- 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*)
--- 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";
);
--- 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) *}
--- 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,