# HG changeset patch # User wenzelm # Date 1291395553 -3600 # Node ID 2c150063cd4d7cd73471fc66aec29a4640421228 # Parent e258f6817add851fc3dc7d1fa5e43594e9997aec setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option; diff -r e258f6817add -r 2c150063cd4d NEWS --- a/NEWS Thu Dec 02 21:48:36 2010 +0100 +++ b/NEWS Fri Dec 03 17:59:13 2010 +0100 @@ -101,29 +101,32 @@ *** HOL *** -* Quickcheck now by default uses exhaustive testing instead of random testing. -Random testing can be invoked by quickcheck[random], +* Quickcheck now by default uses exhaustive testing instead of random +testing. Random testing can be invoked by quickcheck[random], exhaustive testing by quickcheck[exhaustive]. -* Quickcheck instantiates polymorphic types with small finite datatypes -by default. This enables a simple execution mechanism to handle -quantifiers and function equality over the finite datatypes. - -* Functions can be declared as coercions and type inference will add them -as necessary upon input of a term. In Complex_Main, real :: nat => real -and real :: int => real are declared as coercions. A new coercion function -f is declared like this: - -declare [[coercion f]] +* Quickcheck instantiates polymorphic types with small finite +datatypes by default. This enables a simple execution mechanism to +handle quantifiers and function equality over the finite datatypes. + +* Functions can be declared as coercions and type inference will add +them as necessary upon input of a term. In theory Complex_Main, +real :: nat => real and real :: int => real are declared as +coercions. A new coercion function f is declared like this: + + declare [[coercion f]] To lift coercions through type constructors (eg from nat => real to nat list => real list), map functions can be declared, e.g. -declare [[coercion_map map]] - -Currently coercion inference is activated only in theories including real -numbers, i.e. descendants of Complex_Main. In other theories it needs to be -loaded explicitly: uses "~~/src/Tools/subtyping.ML" + declare [[coercion_map map]] + +Currently coercion inference is activated only in theories including +real numbers, i.e. descendants of Complex_Main. This is controlled by +the configuration option "infer_coercions", e.g. it can be enabled in +other theories like this: + + declare [[coercion_enabled]] * Abandoned locales equiv, congruent and congruent2 for equivalence relations. INCOMPATIBILITY: use equivI rather than equiv_intro (same for congruent(2)). diff -r e258f6817add -r 2c150063cd4d src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Dec 02 21:48:36 2010 +0100 +++ b/src/HOL/HOL.thy Fri Dec 03 17:59:13 2010 +0100 @@ -33,9 +33,11 @@ "Tools/try.ML" ("Tools/cnf_funcs.ML") ("Tools/type_mapper.ML") + "~~/src/Tools/subtyping.ML" begin setup {* Intuitionistic.method_setup @{binding iprover} *} +setup Subtyping.setup subsection {* Primitive logic *} diff -r e258f6817add -r 2c150063cd4d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Dec 02 21:48:36 2010 +0100 +++ b/src/HOL/IsaMakefile Fri Dec 03 17:59:13 2010 +0100 @@ -156,6 +156,14 @@ @$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \ + $(SRC)/Provers/Arith/cancel_div_mod.ML \ + $(SRC)/Provers/Arith/cancel_sums.ML \ + $(SRC)/Provers/Arith/fast_lin_arith.ML \ + $(SRC)/Provers/order.ML \ + $(SRC)/Provers/trancl.ML \ + $(SRC)/Tools/Metis/metis.ML \ + $(SRC)/Tools/rat.ML \ + $(SRC)/Tools/subtyping.ML \ Complete_Lattice.thy \ Complete_Partial_Order.thy \ Datatype.thy \ @@ -182,10 +190,7 @@ SAT.thy \ Set.thy \ Sum_Type.thy \ - Tools/abel_cancel.ML \ - Tools/arith_data.ML \ - Tools/async_manager.ML \ - Tools/cnf_funcs.ML \ + Tools/Datatype/datatype.ML \ Tools/Datatype/datatype_abs_proofs.ML \ Tools/Datatype/datatype_aux.ML \ Tools/Datatype/datatype_case.ML \ @@ -193,14 +198,12 @@ Tools/Datatype/datatype_data.ML \ Tools/Datatype/datatype_prop.ML \ Tools/Datatype/datatype_realizer.ML \ - Tools/Datatype/datatype.ML \ - Tools/dseq.ML \ Tools/Function/context_tree.ML \ + Tools/Function/fun.ML \ + Tools/Function/function.ML \ Tools/Function/function_common.ML \ Tools/Function/function_core.ML \ Tools/Function/function_lib.ML \ - Tools/Function/function.ML \ - Tools/Function/fun.ML \ Tools/Function/induction_schema.ML \ Tools/Function/lexicographic_order.ML \ Tools/Function/measure_functions.ML \ @@ -214,17 +217,22 @@ Tools/Function/size.ML \ Tools/Function/sum_tree.ML \ Tools/Function/termination.ML \ - Tools/inductive_codegen.ML \ - Tools/inductive.ML \ - Tools/inductive_realizer.ML \ - Tools/inductive_set.ML \ - Tools/lin_arith.ML \ Tools/Meson/meson.ML \ Tools/Meson/meson_clausify.ML \ Tools/Meson/meson_tactic.ML \ Tools/Metis/metis_reconstruct.ML \ + Tools/Metis/metis_tactics.ML \ Tools/Metis/metis_translate.ML \ - Tools/Metis/metis_tactics.ML \ + Tools/abel_cancel.ML \ + Tools/arith_data.ML \ + Tools/async_manager.ML \ + Tools/cnf_funcs.ML \ + Tools/dseq.ML \ + Tools/inductive.ML \ + Tools/inductive_codegen.ML \ + Tools/inductive_realizer.ML \ + Tools/inductive_set.ML \ + Tools/lin_arith.ML \ Tools/nat_arith.ML \ Tools/primrec.ML \ Tools/prop_logic.ML \ @@ -237,14 +245,7 @@ Tools/typedef.ML \ Transitive_Closure.thy \ Typedef.thy \ - Wellfounded.thy \ - $(SRC)/Provers/Arith/cancel_div_mod.ML \ - $(SRC)/Provers/Arith/cancel_sums.ML \ - $(SRC)/Provers/Arith/fast_lin_arith.ML \ - $(SRC)/Provers/order.ML \ - $(SRC)/Provers/trancl.ML \ - $(SRC)/Tools/Metis/metis.ML \ - $(SRC)/Tools/rat.ML + Wellfounded.thy $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES) @$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain @@ -385,7 +386,6 @@ @$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \ - $(SRC)/Tools/subtyping.ML \ Archimedean_Field.thy \ Complex.thy \ Complex_Main.thy \ diff -r e258f6817add -r 2c150063cd4d src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Thu Dec 02 21:48:36 2010 +0100 +++ b/src/HOL/RealDef.thy Fri Dec 03 17:59:13 2010 +0100 @@ -9,7 +9,6 @@ theory RealDef imports Rat -uses "~~/src/Tools/subtyping.ML" begin text {* @@ -1110,8 +1109,7 @@ real_of_nat_def [code_unfold]: "real == real_of_nat" real_of_int_def [code_unfold]: "real == real_of_int" -setup Subtyping.setup - +declare [[coercion_enabled]] declare [[coercion "real::nat\real"]] declare [[coercion "real::int\real"]] diff -r e258f6817add -r 2c150063cd4d src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Thu Dec 02 21:48:36 2010 +0100 +++ b/src/Tools/subtyping.ML Fri Dec 03 17:59:13 2010 +0100 @@ -7,6 +7,7 @@ signature SUBTYPING = sig datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT + val coercion_enabled: bool Config.T val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) -> term list -> term list val add_type_map: term -> Context.generic -> Context.generic @@ -716,11 +717,15 @@ (try (Consts.the_constraint (ProofContext.consts_of ctxt))) (ProofContext.def_type ctxt); +val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false); + val add_term_check = Syntax.add_term_check ~100 "coercions" (fn xs => fn ctxt => - let val xs' = coercion_infer_types ctxt xs - in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end); + if Config.get ctxt coercion_enabled then + let val xs' = coercion_infer_types ctxt xs + in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end + else NONE); (* declarations *) @@ -821,6 +826,7 @@ (* theory setup *) val setup = + coercion_enabled_setup #> Context.theory_map add_term_check #> Attrib.setup @{binding coercion} (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))