# HG changeset patch # User paulson # Date 1428765554 -3600 # Node ID 05d4dce039c64fe701d7d49f58b5aa65e648a31e # Parent b785d6d064305efd9bbc5af955897cc7bc96b81d# Parent 5fe58ca9cf40e0dd4f98864281e9cd813b77dbbf Merge diff -r b785d6d06430 -r 05d4dce039c6 Admin/Release/build_library --- a/Admin/Release/build_library Sat Apr 11 11:56:40 2015 +0100 +++ b/Admin/Release/build_library Sat Apr 11 16:19:14 2015 +0100 @@ -75,7 +75,6 @@ cd * ISABELLE_NAME="$(basename "$PWD")" -echo "Z3_NON_COMMERCIAL=yes" >> etc/settings echo "ISABELLE_FULL_TEST=true" >> etc/settings echo -n > src/Doc/ROOT diff -r b785d6d06430 -r 05d4dce039c6 Admin/components/bundled-windows --- a/Admin/components/bundled-windows Sat Apr 11 11:56:40 2015 +0100 +++ b/Admin/components/bundled-windows Sat Apr 11 16:19:14 2015 +0100 @@ -1,3 +1,3 @@ #additional components to be bundled for release -cygwin-20140813 +cygwin-20150410 windows_app-20131201 diff -r b785d6d06430 -r 05d4dce039c6 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Sat Apr 11 11:56:40 2015 +0100 +++ b/Admin/components/components.sha1 Sat Apr 11 16:19:14 2015 +0100 @@ -14,6 +14,7 @@ 8e562dfe57a2f894f9461f4addedb88afa108152 cygwin-20140725.tar.gz 238d8e30e8e22495b7ea3f5ec36e852e97fe8bbf cygwin-20140813.tar.gz 629b8fbe35952d1551cd2a7ff08db697f6dff870 cygwin-20141024.tar.gz +ce93d0b3b2743c4f4e5bba30c2889b3b7bc22f2c cygwin-20150410.tar.gz 0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz 2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz diff -r b785d6d06430 -r 05d4dce039c6 Admin/isatest/settings/mac-poly-M2-alternative --- a/Admin/isatest/settings/mac-poly-M2-alternative Sat Apr 11 11:56:40 2015 +0100 +++ b/Admin/isatest/settings/mac-poly-M2-alternative Sat Apr 11 16:19:14 2015 +0100 @@ -30,6 +30,3 @@ ISABELLE_FULL_TEST=true ISABELLE_GHC=ghc - -Z3_NON_COMMERCIAL="yes" - diff -r b785d6d06430 -r 05d4dce039c6 Admin/isatest/settings/mac-poly-M4 --- a/Admin/isatest/settings/mac-poly-M4 Sat Apr 11 11:56:40 2015 +0100 +++ b/Admin/isatest/settings/mac-poly-M4 Sat Apr 11 16:19:14 2015 +0100 @@ -35,6 +35,3 @@ ISABELLE_POLYML="$ML_HOME/poly" #ISABELLE_SCALA="$SCALA_HOME/bin" ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml" - -Z3_NON_COMMERCIAL="yes" - diff -r b785d6d06430 -r 05d4dce039c6 Admin/isatest/settings/mac-poly-M8 --- a/Admin/isatest/settings/mac-poly-M8 Sat Apr 11 11:56:40 2015 +0100 +++ b/Admin/isatest/settings/mac-poly-M8 Sat Apr 11 16:19:14 2015 +0100 @@ -35,6 +35,3 @@ ISABELLE_POLYML="$ML_HOME/poly" #ISABELLE_SCALA="$SCALA_HOME/bin" ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml" - -Z3_NON_COMMERCIAL="yes" - diff -r b785d6d06430 -r 05d4dce039c6 Admin/isatest/settings/mac-poly-M8-quick_and_dirty --- a/Admin/isatest/settings/mac-poly-M8-quick_and_dirty Sat Apr 11 11:56:40 2015 +0100 +++ b/Admin/isatest/settings/mac-poly-M8-quick_and_dirty Sat Apr 11 16:19:14 2015 +0100 @@ -27,6 +27,3 @@ ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" ISABELLE_BUILD_OPTIONS="threads=8 quick_and_dirty" - -Z3_NON_COMMERCIAL="yes" - diff -r b785d6d06430 -r 05d4dce039c6 Admin/isatest/settings/mac-poly-M8-skip_proofs --- a/Admin/isatest/settings/mac-poly-M8-skip_proofs Sat Apr 11 11:56:40 2015 +0100 +++ b/Admin/isatest/settings/mac-poly-M8-skip_proofs Sat Apr 11 16:19:14 2015 +0100 @@ -27,6 +27,3 @@ ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" ISABELLE_BUILD_OPTIONS="threads=8 skip_proofs" - -Z3_NON_COMMERCIAL="yes" - diff -r b785d6d06430 -r 05d4dce039c6 Admin/lib/Tools/makedist_cygwin --- a/Admin/lib/Tools/makedist_cygwin Sat Apr 11 11:56:40 2015 +0100 +++ b/Admin/lib/Tools/makedist_cygwin Sat Apr 11 16:19:14 2015 +0100 @@ -4,7 +4,7 @@ ## global parameters -CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2014" +CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2015" ## diagnostics @@ -55,7 +55,7 @@ --site "$CYGWIN_MIRROR" --no-verify \ --local-package-dir 'C:\temp' \ --root "$(cygpath -w "$TARGET")" \ - --packages libgmp3,perl,perl_vendor,rlwrap,unzip,vim \ + --packages perl,perl-libwww-perl,rlwrap,unzip,vim \ --no-shortcuts --no-startmenu --no-desktop --quiet-mode [ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2 @@ -65,7 +65,7 @@ for NAME in hosts protocols services networks passwd group do - rm "$TARGET/etc/$NAME" + rm -f "$TARGET/etc/$NAME" done ln -s cygperl5_14.dll "$TARGET/bin/cygperl5_14_2.dll" @@ -77,4 +77,3 @@ DATE=$(date +%Y%m%d) tar -C "$TARGET/.." -cz -f "cygwin-${DATE}.tar.gz" cygwin - diff -r b785d6d06430 -r 05d4dce039c6 Admin/mira.py --- a/Admin/mira.py Sat Apr 11 11:56:40 2015 +0100 +++ b/Admin/mira.py Sat Apr 11 16:19:14 2015 +0100 @@ -24,7 +24,6 @@ # patch settings extra_settings = ''' -Z3_NON_COMMERCIAL="yes" init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/main" init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional" diff -r b785d6d06430 -r 05d4dce039c6 NEWS --- a/NEWS Sat Apr 11 11:56:40 2015 +0100 +++ b/NEWS Sat Apr 11 16:19:14 2015 +0100 @@ -1,8 +1,11 @@ Isabelle NEWS -- history of user-relevant changes ================================================= -New in this Isabelle version ----------------------------- +(Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.) + + +New in Isabelle2015 (May 2015) +------------------------------ *** General *** @@ -54,9 +57,6 @@ *** Prover IDE -- Isabelle/Scala/jEdit *** -* Old graph browser (Java/AWT 1.1) is superseded by improved graphview -panel, which also produces PDF output without external tools. - * Improved folding mode "isabelle" based on Isar syntax. Alternatively, the "sidekick" mode may be used for document structure. @@ -74,12 +74,12 @@ * Less waste of vertical space via negative line spacing (see Global Options / Text Area). +* Old graph browser (Java/AWT 1.1) is superseded by improved graphview +panel, which also produces PDF output without external tools. + *** Document preparation *** -* Discontinued obsolete option "document_graph": session_graph.pdf is -produced unconditionally for HTML browser_info and PDF-LaTeX document. - * Document markup commands 'chapter', 'section', 'subsection', 'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any context, even before the initial 'theory' command. Obsolete proof @@ -89,6 +89,17 @@ should be replaced by 'chapter', 'section' etc. (using "isabelle update_header"). Minor INCOMPATIBILITY. +* Official support for "tt" style variants, via \isatt{...} or +\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or +verbatim environment of LaTeX is no longer used. This allows @{ML} etc. +as argument to other macros (such as footnotes). + +* Document antiquotation @{verbatim} prints ASCII text literally in "tt" +style. + +* Discontinued obsolete option "document_graph": session_graph.pdf is +produced unconditionally for HTML browser_info and PDF-LaTeX document. + * Diagnostic commands and document markup commands within a proof do not affect the command tag for output. Thus commands like 'thm' are subject to proof document structure, and no longer "stick out" accidentally. @@ -103,21 +114,9 @@ antiquotations need to observe the margin explicitly according to Thy_Output.string_of_margin. Minor INCOMPATIBILITY. -* Official support for "tt" style variants, via \isatt{...} or -\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or -verbatim environment of LaTeX is no longer used. This allows @{ML} etc. -as argument to other macros (such as footnotes). - -* Document antiquotation @{verbatim} prints ASCII text literally in "tt" -style. - *** Pure *** -* Explicit instantiation via attributes "where", "of", and proof methods -"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns -("_") that stand for anonymous local variables. - * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac" etc.) allow an optional context of local variables ('for' declaration): these variables become schematic in the instantiated theorem; this @@ -127,18 +126,22 @@ declare rule_insts_schematic = true temporarily and update to use local variable declarations or dummy patterns instead. +* Explicit instantiation via attributes "where", "of", and proof methods +"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns +("_") that stand for anonymous local variables. + * Generated schematic variables in standard format of exported facts are incremented to avoid material in the proof context. Rare INCOMPATIBILITY, explicit instantiation sometimes needs to refer to different index. -* Command "class_deps" takes optional sort arguments constraining -the search space. - -* Lexical separation of signed and unsigend numerals: categories "num" -and "float" are unsigend. INCOMPATIBILITY: subtle change in precedence -of numeral signs, particulary in expressions involving infix syntax like -"(- 1) ^ n". +* Command "class_deps" takes optional sort arguments to constrain then +resulting class hierarchy. + +* Lexical separation of signed and unsigned numerals: categories "num" +and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence +of numeral signs, particularly in expressions involving infix syntax +like "(- 1) ^ n". * Old inner token category "xnum" has been discontinued. Potential INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" @@ -147,88 +150,6 @@ *** HOL *** -* Given up separate type class no_zero_divisors in favour of fully -algebraic semiring_no_zero_divisors. INCOMPATIBILITY. - -* Class linordered_semidom really requires no zero divisors. -INCOMPATIBILITY. - -* Classes division_ring, field and linordered_field always demand -"inverse 0 = 0". Given up separate classes division_ring_inverse_zero, -field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY. - -* Type classes cancel_ab_semigroup_add / cancel_monoid_add specify -explicit additive inverse operation. INCOMPATIBILITY. - -* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for -single-step rewriting with subterm selection based on patterns. - -* The functions "sin" and "cos" are now defined for any -"'{real_normed_algebra_1,banach}" type, so in particular on "real" and -"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be -needed. - -* New library of properties of the complex transcendental functions sin, -cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light. - -* The factorial function, "fact", now has type "nat => 'a" (of a sort -that admits numeric types including nat, int, real and complex. -INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type -constraint, and the combination "real (fact k)" is likely to be -unsatisfactory. If a type conversion is still necessary, then use -"of_nat (fact k)" or "real_of_nat (fact k)". - -* Removed functions "natfloor" and "natceiling", use "nat o floor" and -"nat o ceiling" instead. A few of the lemmas have been retained and -adapted: in their names "natfloor"/"natceiling" has been replaced by -"nat_floor"/"nat_ceiling". - -* Qualified some duplicated fact names required for boostrapping the -type class hierarchy: - ab_add_uminus_conv_diff ~> diff_conv_add_uminus - field_inverse_zero ~> inverse_zero - field_divide_inverse ~> divide_inverse - field_inverse ~> left_inverse -Minor INCOMPATIBILITY. - -* Eliminated fact duplicates: - mult_less_imp_less_right ~> mult_right_less_imp_less - mult_less_imp_less_left ~> mult_left_less_imp_less -Minor INCOMPATIBILITY. - -* Fact consolidation: even_less_0_iff is subsumed by -double_add_less_zero_iff_single_add_less_zero (simp by default anyway). - -* Add NO_MATCH-simproc, allows to check for syntactic non-equality. - -* Generalized and consolidated some theorems concerning divsibility: - dvd_reduce ~> dvd_add_triv_right_iff - dvd_plus_eq_right ~> dvd_add_right_iff - dvd_plus_eq_left ~> dvd_add_left_iff -Minor INCOMPATIBILITY. - -* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _" -and part of theory Main. - even_def ~> even_iff_mod_2_eq_zero -INCOMPATIBILITY. - -* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor -INCOMPATIBILITY. - -* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid -non-termination in case of distributing a division. With this change -field_simps is in some cases slightly less powerful, if it fails try to -add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY. - -* Bootstrap of listsum as special case of abstract product over lists. -Fact rename: - listsum_def ~> listsum.eq_foldr -INCOMPATIBILITY. - -* Command and antiquotation "value" provide different evaluation slots -(again), where the previous strategy (NBE after ML) serves as default. -Minor INCOMPATIBILITY. - * New (co)datatype package: - The 'datatype_new' command has been renamed 'datatype'. The old command of that name is now called 'old_datatype' and is provided @@ -285,10 +206,8 @@ ~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy INCOMPATIBILITY. -* Product over lists via constant "listprod". - * Nitpick: - - Fixed soundness bug related to the strict and nonstrict subset + - Fixed soundness bug related to the strict and non-strict subset operations. * Sledgehammer: @@ -297,7 +216,7 @@ - Z3 is now always enabled by default, now that it is fully open source. The "z3_non_commercial" option is discontinued. - Minimization is now always enabled by default. - Removed subcommand: + Removed sub-command: min - Proof reconstruction, both one-liners and Isar, has been dramatically improved. @@ -318,18 +237,95 @@ - New option 'smt_statistics' to display statistics of the new 'smt' method, especially runtime statistics of Z3 proof reconstruction. -* List: renamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc. +* Command and antiquotation "value" provide different evaluation slots +(again), where the previous strategy (NBE after ML) serves as default. +Minor INCOMPATIBILITY. + +* Add NO_MATCH-simproc, allows to check for syntactic non-equality. + +* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid +non-termination in case of distributing a division. With this change +field_simps is in some cases slightly less powerful, if it fails try to +add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY. + +* Separate class no_zero_divisors has been given up in favour of fully +algebraic semiring_no_zero_divisors. INCOMPATIBILITY. + +* Class linordered_semidom really requires no zero divisors. +INCOMPATIBILITY. + +* Classes division_ring, field and linordered_field always demand +"inverse 0 = 0". Given up separate classes division_ring_inverse_zero, +field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY. + +* Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit +additive inverse operation. INCOMPATIBILITY. + +* The functions "sin" and "cos" are now defined for any type of sort +"{real_normed_algebra_1,banach}" type, so in particular on "real" and +"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be +needed. + +* New library of properties of the complex transcendental functions sin, +cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light. + +* The factorial function, "fact", now has type "nat => 'a" (of a sort +that admits numeric types including nat, int, real and complex. +INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type +constraint, and the combination "real (fact k)" is likely to be +unsatisfactory. If a type conversion is still necessary, then use +"of_nat (fact k)" or "real_of_nat (fact k)". + +* Removed functions "natfloor" and "natceiling", use "nat o floor" and +"nat o ceiling" instead. A few of the lemmas have been retained and +adapted: in their names "natfloor"/"natceiling" has been replaced by +"nat_floor"/"nat_ceiling". + +* Qualified some duplicated fact names required for boostrapping the +type class hierarchy: + ab_add_uminus_conv_diff ~> diff_conv_add_uminus + field_inverse_zero ~> inverse_zero + field_divide_inverse ~> divide_inverse + field_inverse ~> left_inverse +Minor INCOMPATIBILITY. + +* Eliminated fact duplicates: + mult_less_imp_less_right ~> mult_right_less_imp_less + mult_less_imp_less_left ~> mult_left_less_imp_less +Minor INCOMPATIBILITY. + +* Fact consolidation: even_less_0_iff is subsumed by +double_add_less_zero_iff_single_add_less_zero (simp by default anyway). + +* Generalized and consolidated some theorems concerning divsibility: + dvd_reduce ~> dvd_add_triv_right_iff + dvd_plus_eq_right ~> dvd_add_right_iff + dvd_plus_eq_left ~> dvd_add_left_iff +Minor INCOMPATIBILITY. + +* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _" +and part of theory Main. + even_def ~> even_iff_mod_2_eq_zero +INCOMPATIBILITY. + +* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor +INCOMPATIBILITY. + +* Bootstrap of listsum as special case of abstract product over lists. +Fact rename: + listsum_def ~> listsum.eq_foldr +INCOMPATIBILITY. + +* Product over lists via constant "listprod". + +* Theory List: renamed drop_Suc_conv_tl and nth_drop' to +Cons_nth_drop_Suc. * New infrastructure for compiling, running, evaluating and testing generated code in target languages in HOL/Library/Code_Test. See HOL/Codegenerator_Test/Code_Test* for examples. -* Library/Sum_of_Squares: simplified and improved "sos" method. Always -use local CSDP executable, which is much faster than the NEOS server. -The "sos_cert" functionality is invoked as "sos" with additional -argument. Minor INCOMPATIBILITY. - -* Theory "Library/Multiset": +* Library/Multiset: - Introduced "replicate_mset" operation. - Introduced alternative characterizations of the multiset ordering in "Library/Multiset_Order". @@ -345,6 +341,8 @@ INCOMPATIBILITY. - Renamed in_multiset_of ~> in_multiset_in_set + Multiset.fold ~> fold_mset + Multiset.filter ~> filter_mset INCOMPATIBILITY. - Removed mcard, is equal to size. - Added attributes: @@ -358,26 +356,37 @@ in_Union_mset_iff [iff] INCOMPATIBILITY. -* HOL-Decision_Procs: - - New counterexample generator quickcheck[approximation] for - inequalities of transcendental functions. - Uses hardware floating point arithmetic to randomly discover - potential counterexamples. Counterexamples are certified with the - 'approximation' method. - See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for - examples. +* Library/Sum_of_Squares: simplified and improved "sos" method. Always +use local CSDP executable, which is much faster than the NEOS server. +The "sos_cert" functionality is invoked as "sos" with additional +argument. Minor INCOMPATIBILITY. + +* HOL-Decision_Procs: New counterexample generator quickcheck +[approximation] for inequalities of transcendental functions. Uses +hardware floating point arithmetic to randomly discover potential +counterexamples. Counterexamples are certified with the "approximation" +method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for +examples. * HOL-Probability: Reworked measurability prover - - applies destructor rules repeatetly + - applies destructor rules repeatedly - removed application splitting (replaced by destructor rule) - added congruence rules to rewrite measure spaces under the sets projection +* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for +single-step rewriting with subterm selection based on patterns. + *** ML *** -* Cartouches within ML sources are turned into values of type -Input.source (with formal position information). +* Subtle change of name space policy: undeclared entries are now +considered inaccessible, instead of accessible via the fully-qualified +internal name. This mainly affects Name_Space.intern (and derivatives), +which may produce an unexpected Long_Name.hidden prefix. Note that +contemporary applications use the strict Name_Space.check (and +derivatives) instead, which is not affected by the change. Potential +INCOMPATIBILITY in rare applications of Name_Space.intern. * Basic combinators map, fold, fold_map, split_list, apply are available as parameterized antiquotations, e.g. @{map 4} for lists of quadruples. @@ -392,8 +401,8 @@ INCOMPATIBILITY: synchronized access needs to be atomic and cannot be nested. -* Synchronized.value (ML) is actually synchronized (as in Scala): -subtle change of semantics with minimal potential for INCOMPATIBILITY. +* Synchronized.value (ML) is actually synchronized (as in Scala): subtle +change of semantics with minimal potential for INCOMPATIBILITY. * The main operations to certify logical entities are Thm.ctyp_of and Thm.cterm_of with a local context; old-style global theory variants are @@ -404,14 +413,6 @@ INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of, Thm.term_of etc. -* Subtle change of name space policy: undeclared entries are now -considered inaccessible, instead of accessible via the fully-qualified -internal name. This mainly affects Name_Space.intern (and derivatives), -which may produce an unexpected Long_Name.hidden prefix. Note that -contempory applications use the strict Name_Space.check (and -derivatives) instead, which is not affected by the change. Potential -INCOMPATIBILITY in rare applications of Name_Space.intern. - * Proper context for various elementary tactics: assume_tac, resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac, compose_tac, Splitter.split_tac etc. INCOMPATIBILITY. @@ -426,6 +427,9 @@ @{command_keyword COMMAND} (usually without quotes and with PIDE markup). Minor INCOMPATIBILITY. +* Cartouches within ML sources are turned into values of type +Input.source (with formal position information). + *** System *** @@ -452,7 +456,7 @@ semicolons from theory sources. * Support for Proof General and Isar TTY loop has been discontinued. -Minor INCOMPATIBILITY. +Minor INCOMPATIBILITY, use standard PIDE infrastructure instead. diff -r b785d6d06430 -r 05d4dce039c6 src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Sat Apr 11 11:56:40 2015 +0100 +++ b/src/Doc/Isar_Ref/Proof.thy Sat Apr 11 16:19:14 2015 +0100 @@ -565,7 +565,7 @@ that method @{text m\<^sub>1} is applied with restriction to the first subgoal, then @{text m\<^sub>2} is applied consecutively with restriction to each subgoal that has newly emerged due to @{text m\<^sub>1}. This is analogous to the tactic - combinator @{ML THEN_ALL_NEW} in Isabelle/ML, see also @{cite + combinator @{ML_op THEN_ALL_NEW} in Isabelle/ML, see also @{cite "isabelle-implementation"}. For example, @{text "(rule r; blast)"} applies rule @{text "r"} and then solves all new subgoals by @{text blast}. diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Library/DAList_Multiset.thy --- a/src/HOL/Library/DAList_Multiset.thy Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Library/DAList_Multiset.thy Sat Apr 11 16:19:14 2015 +0100 @@ -24,7 +24,7 @@ lemma [code, code del]: "image_mset = image_mset" .. -lemma [code, code del]: "Multiset.filter = Multiset.filter" .. +lemma [code, code del]: "filter_mset = filter_mset" .. lemma [code, code del]: "count = count" .. @@ -199,7 +199,7 @@ (simp add: count_of_subtract_entries_raw alist.Alist_inverse distinct_subtract_entries_raw subtract_entries_def) -lemma filter_Bag [code]: "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \ fst) xs)" +lemma filter_Bag [code]: "filter_mset P (Bag xs) = Bag (DAList.filter (P \ fst) xs)" by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq) @@ -285,7 +285,7 @@ lemma DAList_Multiset_fold: assumes fn: "\a n x. fn a n x = (f a ^^ n) x" - shows "Multiset.fold f e (Bag al) = DAList_Multiset.fold fn e al" + shows "fold_mset f e (Bag al) = DAList_Multiset.fold fn e al" unfolding DAList_Multiset.fold_def proof (induct al) fix ys @@ -294,12 +294,12 @@ have count[simp]: "\x. count (Abs_multiset (count_of x)) = count_of x" by (rule Abs_multiset_inverse[OF count_of_multiset]) assume ys: "ys \ ?inv" - then show "Multiset.fold f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))" + then show "fold_mset f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))" unfolding Bag_def unfolding Alist_inverse[OF ys] proof (induct ys arbitrary: e rule: list.induct) case Nil show ?case - by (rule trans[OF arg_cong[of _ "{#}" "Multiset.fold f e", OF multiset_eqI]]) + by (rule trans[OF arg_cong[of _ "{#}" "fold_mset f e", OF multiset_eqI]]) (auto, simp add: cs) next case (Cons pair ys e) @@ -388,7 +388,7 @@ apply (auto simp: ac_simps) done -lemma size_fold: "size A = Multiset.fold (\_. Suc) 0 A" (is "_ = Multiset.fold ?f _ _") +lemma size_fold: "size A = fold_mset (\_. Suc) 0 A" (is "_ = fold_mset ?f _ _") proof - interpret comp_fun_commute ?f by default auto show ?thesis by (induct A) auto @@ -403,7 +403,7 @@ qed -lemma set_of_fold: "set_of A = Multiset.fold insert {} A" (is "_ = Multiset.fold ?f _ _") +lemma set_of_fold: "set_of A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _") proof - interpret comp_fun_commute ?f by default auto show ?thesis by (induct A) auto diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Library/Multiset.thy Sat Apr 11 16:19:14 2015 +0100 @@ -527,40 +527,39 @@ text {* Multiset comprehension *} -lift_definition filter :: "('a \ bool) \ 'a multiset \ 'a multiset" is "\P M. \x. if P x then M x else 0" +lift_definition filter_mset :: "('a \ bool) \ 'a multiset \ 'a multiset" +is "\P M. \x. if P x then M x else 0" by (rule filter_preserves_multiset) -hide_const (open) filter - -lemma count_filter [simp]: - "count (Multiset.filter P M) a = (if P a then count M a else 0)" - by (simp add: filter.rep_eq) - -lemma filter_empty [simp]: - "Multiset.filter P {#} = {#}" +lemma count_filter_mset [simp]: + "count (filter_mset P M) a = (if P a then count M a else 0)" + by (simp add: filter_mset.rep_eq) + +lemma filter_empty_mset [simp]: + "filter_mset P {#} = {#}" + by (rule multiset_eqI) simp + +lemma filter_single_mset [simp]: + "filter_mset P {#x#} = (if P x then {#x#} else {#})" by (rule multiset_eqI) simp -lemma filter_single [simp]: - "Multiset.filter P {#x#} = (if P x then {#x#} else {#})" +lemma filter_union_mset [simp]: + "filter_mset P (M + N) = filter_mset P M + filter_mset P N" by (rule multiset_eqI) simp -lemma filter_union [simp]: - "Multiset.filter P (M + N) = Multiset.filter P M + Multiset.filter P N" +lemma filter_diff_mset [simp]: + "filter_mset P (M - N) = filter_mset P M - filter_mset P N" by (rule multiset_eqI) simp -lemma filter_diff [simp]: - "Multiset.filter P (M - N) = Multiset.filter P M - Multiset.filter P N" +lemma filter_inter_mset [simp]: + "filter_mset P (M #\ N) = filter_mset P M #\ filter_mset P N" by (rule multiset_eqI) simp -lemma filter_inter [simp]: - "Multiset.filter P (M #\ N) = Multiset.filter P M #\ Multiset.filter P N" - by (rule multiset_eqI) simp - -lemma multiset_filter_subset[simp]: "Multiset.filter f M \ M" +lemma multiset_filter_subset[simp]: "filter_mset f M \ M" unfolding less_eq_multiset.rep_eq by auto lemma multiset_filter_mono: assumes "A \ B" - shows "Multiset.filter f A \ Multiset.filter f B" + shows "filter_mset f A \ filter_mset f B" proof - from assms[unfolded mset_le_exists_conv] obtain C where B: "B = A + C" by auto @@ -572,7 +571,7 @@ syntax (xsymbol) "_MCollect" :: "pttrn \ 'a multiset \ bool \ 'a multiset" ("(1{# _ \# _./ _#})") translations - "{#x \# M. P#}" == "CONST Multiset.filter (\x. P) M" + "{#x \# M. P#}" == "CONST filter_mset (\x. P) M" subsubsection {* Set of elements *} @@ -694,7 +693,7 @@ show ?thesis unfolding B by (induct C, auto) qed -lemma size_filter_mset_lesseq[simp]: "size (Multiset.filter f M) \ size M" +lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \ size M" by (rule size_mset_mono[OF multiset_filter_subset]) lemma size_Diff_submset: @@ -798,19 +797,19 @@ subsection {* The fold combinator *} -definition fold :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b" +definition fold_mset :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b" where - "fold f s M = Finite_Set.fold (\x. f x ^^ count M x) s (set_of M)" + "fold_mset f s M = Finite_Set.fold (\x. f x ^^ count M x) s (set_of M)" lemma fold_mset_empty [simp]: - "fold f s {#} = s" - by (simp add: fold_def) + "fold_mset f s {#} = s" + by (simp add: fold_mset_def) context comp_fun_commute begin lemma fold_mset_insert: - "fold f s (M + {#x#}) = f x (fold f s M)" + "fold_mset f s (M + {#x#}) = f x (fold_mset f s M)" proof - interpret mset: comp_fun_commute "\y. f y ^^ count M y" by (fact comp_fun_commute_funpow) @@ -824,7 +823,7 @@ Finite_Set.fold (\y. f y ^^ count M y) s (set_of M)" by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) with False * show ?thesis - by (simp add: fold_def del: count_union) + by (simp add: fold_mset_def del: count_union) next case True def N \ "set_of M - {x}" @@ -832,23 +831,23 @@ then have "Finite_Set.fold (\y. f y ^^ count (M + {#x#}) y) s N = Finite_Set.fold (\y. f y ^^ count M y) s N" by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) - with * show ?thesis by (simp add: fold_def del: count_union) simp + with * show ?thesis by (simp add: fold_mset_def del: count_union) simp qed qed corollary fold_mset_single [simp]: - "fold f s {#x#} = f x s" + "fold_mset f s {#x#} = f x s" proof - - have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp + have "fold_mset f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp then show ?thesis by simp qed lemma fold_mset_fun_left_comm: - "f x (fold f s M) = fold f (f x s) M" + "f x (fold_mset f s M) = fold_mset f (f x s) M" by (induct M) (simp_all add: fold_mset_insert fun_left_comm) lemma fold_mset_union [simp]: - "fold f s (M + N) = fold f (fold f s M) N" + "fold_mset f s (M + N) = fold_mset f (fold_mset f s M) N" proof (induct M) case empty then show ?case by simp next @@ -860,7 +859,7 @@ lemma fold_mset_fusion: assumes "comp_fun_commute g" - shows "(\x y. h (g x y) = f x (h y)) \ h (fold g w A) = fold f (h w) A" (is "PROP ?P") + shows "(\x y. h (g x y) = f x (h y)) \ h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P") proof - interpret comp_fun_commute g by (fact assms) show "PROP ?P" by (induct A) auto @@ -870,10 +869,10 @@ text {* A note on code generation: When defining some function containing a - subterm @{term "fold F"}, code generation is not automatic. When + subterm @{term "fold_mset F"}, code generation is not automatic. When interpreting locale @{text left_commutative} with @{text F}, the - would be code thms for @{const fold} become thms like - @{term "fold F z {#} = z"} where @{text F} is not a pattern but + would be code thms for @{const fold_mset} become thms like + @{term "fold_mset F z {#} = z"} where @{text F} is not a pattern but contains defined symbols, i.e.\ is not a code thm. Hence a separate constant with its own code thms needs to be introduced for @{text F}. See the image operator below. @@ -883,7 +882,7 @@ subsection {* Image *} definition image_mset :: "('a \ 'b) \ 'a multiset \ 'b multiset" where - "image_mset f = fold (plus o single o f) {#}" + "image_mset f = fold_mset (plus o single o f) {#}" lemma comp_fun_commute_mset_image: "comp_fun_commute (plus o single o f)" @@ -1164,7 +1163,7 @@ definition sorted_list_of_multiset :: "'a multiset \ 'a list" where - "sorted_list_of_multiset M = fold insort [] M" + "sorted_list_of_multiset M = fold_mset insort [] M" lemma sorted_list_of_multiset_empty [simp]: "sorted_list_of_multiset {#} = []" @@ -1223,7 +1222,7 @@ definition F :: "'a multiset \ 'a" where - eq_fold: "F M = Multiset.fold f 1 M" + eq_fold: "F M = fold_mset f 1 M" lemma empty [simp]: "F {#} = 1" @@ -1252,7 +1251,7 @@ declare comp_fun_commute.fold_mset_insert[OF comp_fun_commute_plus_mset, simp] -lemma in_mset_fold_plus_iff[iff]: "x \# Multiset.fold (op +) M NN \ x \# M \ (\N. N \# NN \ x \# N)" +lemma in_mset_fold_plus_iff[iff]: "x \# fold_mset (op +) M NN \ x \# M \ (\N. N \# NN \ x \# N)" by (induct NN) auto notation times (infixl "*" 70) @@ -1353,7 +1352,7 @@ lemma msetprod_multiplicity: "msetprod M = setprod (\x. x ^ count M x) (set_of M)" - by (simp add: Multiset.fold_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def) + by (simp add: fold_mset_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def) end @@ -2101,8 +2100,6 @@ multiset_postproc *} -hide_const (open) fold - subsection {* Naive implementation using lists *} @@ -2125,7 +2122,7 @@ by (simp add: multiset_of_map) lemma [code]: - "Multiset.filter f (multiset_of xs) = multiset_of (filter f xs)" + "filter_mset f (multiset_of xs) = multiset_of (filter f xs)" by (simp add: multiset_of_filter) lemma [code]: @@ -2438,8 +2435,7 @@ unfolding rel_mset_def[abs_def] BNF_Def.Grp_def OO_def apply (rule ext)+ apply auto - apply (rule_tac x = "multiset_of (zip xs ys)" in exI) - apply auto[1] + apply (rule_tac x = "multiset_of (zip xs ys)" in exI; auto) apply (metis list_all2_lengthD map_fst_zip multiset_of_map) apply (auto simp: list_all2_iff)[1] apply (metis list_all2_lengthD map_snd_zip multiset_of_map) @@ -2451,7 +2447,8 @@ apply (rule_tac x = "map fst xys" in exI) apply (auto simp: multiset_of_map) apply (rule_tac x = "map snd xys" in exI) - by (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd) + apply (auto simp: multiset_of_map list_all2I subset_eq zip_map_fst_snd) + done next show "\z. z \ set_of {#} \ False" by auto diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Library/Sublist.thy --- a/src/HOL/Library/Sublist.thy Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Library/Sublist.thy Sat Apr 11 16:19:14 2015 +0100 @@ -144,7 +144,7 @@ lemma take_prefix: "prefix xs ys \ prefix (take n xs) ys" apply (induct n arbitrary: xs ys) - apply (case_tac ys, simp_all)[1] + apply (case_tac ys; simp) apply (metis prefix_order.less_trans prefixI take_is_prefixeq) done diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Sat Apr 11 16:19:14 2015 +0100 @@ -190,7 +190,7 @@ val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c) in thy' |> - BNF_LFP_Compat.add_primrec_global + BNF_LFP_Compat.primrec_global [(Binding.name swap_name, SOME swapT, NoSyn)] [(Attrib.empty_binding, def1)] ||> Sign.parent_path ||>> @@ -224,7 +224,7 @@ Const (swap_name, swapT) $ x $ (prm $ xs $ a))); in thy' |> - BNF_LFP_Compat.add_primrec_global + BNF_LFP_Compat.primrec_global [(Binding.name prm_name, SOME prmT, NoSyn)] [(Attrib.empty_binding, def1), (Attrib.empty_binding, def2)] ||> Sign.parent_path diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat Apr 11 16:19:14 2015 +0100 @@ -162,7 +162,7 @@ fun fresh_star_const T U = Const (@{const_name Nominal.fresh_star}, HOLogic.mk_setT T --> U --> HOLogic.boolT); -fun gen_nominal_datatype prep_specs config dts thy = +fun gen_nominal_datatype prep_specs (config: Old_Datatype_Aux.config) dts thy = let val new_type_names = map (fn ((tname, _, _), _) => Binding.name_of tname) dts; @@ -256,7 +256,7 @@ end) descr; val (perm_simps, thy2) = - BNF_LFP_Compat.add_primrec_overloaded + BNF_LFP_Compat.primrec_overloaded (map (fn (s, sT) => (s, sT, false)) (List.take (perm_names' ~~ perm_names_types, length new_type_names))) (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1; diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Sat Apr 11 16:19:14 2015 +0100 @@ -8,11 +8,11 @@ signature NOMINAL_PRIMREC = sig - val add_primrec: term list option -> term option -> + val primrec: term list option -> term option -> (binding * typ option * mixfix) list -> (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> local_theory -> Proof.state - val add_primrec_cmd: string list option -> string option -> + val primrec_cmd: string list option -> string option -> (binding * string option * mixfix) list -> (binding * string option * mixfix) list -> (Attrib.binding * string) list -> local_theory -> Proof.state @@ -382,8 +382,8 @@ in -val add_primrec = gen_primrec Specification.check_spec (K I); -val add_primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term; +val primrec = gen_primrec Specification.check_spec (K I); +val primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term; end; @@ -407,7 +407,7 @@ "define primitive recursive functions on nominal datatypes" (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs >> (fn ((((invs, fctxt), fixes), params), specs) => - add_primrec_cmd invs fctxt fixes params specs)); + primrec_cmd invs fctxt fixes params specs)); end; diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Num.thy --- a/src/HOL/Num.thy Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Num.thy Sat Apr 11 16:19:14 2015 +0100 @@ -1195,10 +1195,10 @@ declaration {* let - fun number_of thy T n = - if not (Sign.of_sort thy (T, @{sort numeral})) + fun number_of ctxt T n = + if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral})) then raise CTERM ("number_of", []) - else Numeral.mk_cnumber (Thm.global_ctyp_of thy T) n; + else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n; in K ( Lin_Arith.add_simps (@{thms arith_simps} @ @{thms more_arith_simps} diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Probability/measurable.ML --- a/src/HOL/Probability/measurable.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Probability/measurable.ML Sat Apr 11 16:19:14 2015 +0100 @@ -51,14 +51,14 @@ dest_thms : thm Item_Net.T, cong_thms : thm Item_Net.T, preprocessors : (string * preprocessor) list } - val empty = { + val empty: T = { measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst), dest_thms = Thm.full_rules, cong_thms = Thm.full_rules, preprocessors = [] }; val extend = I; fun merge ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1 }, - {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) = { + {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) : T = { measurable_thms = Item_Net.merge (t1, t2), dest_thms = Item_Net.merge (dt1, dt2), cong_thms = Item_Net.merge (ct1, ct2), @@ -81,7 +81,7 @@ fun map_cong_thms f = map_data I I f I fun map_preprocessors f = map_data I I I f -fun generic_add_del map = +fun generic_add_del map : attribute context_parser = Scan.lift (Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >> (fn f => Thm.declaration_attribute (Data.map o map o f)) diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/ROOT --- a/src/HOL/ROOT Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/ROOT Sat Apr 11 16:19:14 2015 +0100 @@ -229,7 +229,7 @@ document_files "root.bib" "root.tex" session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + - options [document = false, browser_info = false] + options [condition = ML_SYSTEM_POLYML, document = false, browser_info = false] theories Generate Generate_Binary_Nat @@ -673,7 +673,7 @@ TPTP-related extensions. *} - options [document = false] + options [condition = ML_SYSTEM_POLYML, document = false] theories ATP_Theory_Export MaSh_Eval @@ -806,7 +806,7 @@ theories Mirabelle_Test session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + - options [document = false, timeout = 60] + options [condition = ML_SYSTEM_POLYML, document = false, timeout = 60] theories Ex session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" + diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Sat Apr 11 16:19:14 2015 +0100 @@ -8,7 +8,7 @@ signature BNF_COMP = sig - val inline_threshold: int Config.T + val typedef_threshold: int Config.T val ID_bnf: BNF_Def.bnf val DEADID_bnf: BNF_Def.bnf @@ -76,7 +76,7 @@ open BNF_Tactics open BNF_Comp_Tactics -val inline_threshold = Attrib.setup_config_int @{binding bnf_inline_threshold} (K 5); +val typedef_threshold = Attrib.setup_config_int @{binding bnf_typedef_threshold} (K 6); val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID"); val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID"); @@ -755,10 +755,10 @@ fun maybe_typedef ctxt force_out_of_line (b, As, mx) set opt_morphs tac = let - val threshold = Config.get ctxt inline_threshold; + val threshold = Config.get ctxt typedef_threshold; val repT = HOLogic.dest_setT (fastype_of set); val out_of_line = force_out_of_line orelse - (threshold >= 0 andalso Term.size_of_typ repT > threshold); + (threshold >= 0 andalso Term.size_of_typ repT >= threshold); in if out_of_line then typedef (b, As, mx) set opt_morphs tac diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Apr 11 16:19:14 2015 +0100 @@ -49,7 +49,7 @@ val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list -> term -> 'a -> 'a val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) -> - typ list -> term -> term + (typ list -> term -> unit) -> typ list -> term -> term val massage_nested_corec_call: Proof.context -> (term -> bool) -> (typ list -> typ -> typ -> term -> term) -> (typ list -> typ -> typ -> term -> term) -> typ list -> typ -> typ -> term -> term @@ -70,10 +70,10 @@ val gfp_rec_sugar_interpretation: string -> (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory - val add_primcorecursive_cmd: corec_option list -> + val primcorecursive_cmd: corec_option list -> (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list -> Proof.context -> Proof.state - val add_primcorec_cmd: corec_option list -> + val primcorec_cmd: corec_option list -> (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list -> local_theory -> local_theory end; @@ -243,11 +243,11 @@ SOME {casex = Const (s', _), split_sels = _ :: _, ...} => SOME s' | _ => NONE); -fun massage_let_if_case ctxt has_call massage_leaf bound_Ts t0 = +fun massage_let_if_case ctxt has_call massage_leaf unexpected_call bound_Ts t0 = let val thy = Proof_Context.theory_of ctxt; - fun check_no_call t = if has_call t then unexpected_corec_call ctxt [t0] t else (); + fun check_no_call bound_Ts t = if has_call t then unexpected_call bound_Ts t else (); fun massage_abs bound_Ts 0 t = massage_rec bound_Ts t | massage_abs bound_Ts m (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) (m - 1) t) @@ -264,7 +264,8 @@ (dummy_branch' :: _, []) => dummy_branch' | (_, [branch']) => branch' | (_, branches') => - Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')) + Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj, + branches')) | (c as Const (@{const_name case_prod}, _), arg :: args) => massage_rec bound_Ts (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args))) @@ -287,7 +288,7 @@ val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T'); in Term.list_comb (casex', - branches' @ tap (List.app check_no_call) obj_leftovers) + branches' @ tap (List.app (check_no_call bound_Ts)) obj_leftovers) end else massage_leaf bound_Ts t @@ -304,6 +305,9 @@ if Term.is_dummy_pattern t then Const (@{const_name undefined}, fastype_of t) else t) end; +fun massage_let_if_case_corec ctxt has_call massage_leaf bound_Ts t0 = + massage_let_if_case ctxt has_call massage_leaf (K (unexpected_corec_call ctxt [t0])) bound_Ts t0; + fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T; fun massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts U T t0 = @@ -348,7 +352,7 @@ (betapply (t, var)))) end) and massage_any_call bound_Ts U T = - massage_let_if_case ctxt has_call (fn bound_Ts => fn t => + massage_let_if_case_corec ctxt has_call (fn bound_Ts => fn t => if has_call t then (case U of Type (s, Us) => @@ -384,8 +388,6 @@ | _ => ill_formed_corec_call ctxt t) else massage_noncall bound_Ts U T t) bound_Ts; - - val T = fastype_of1 (bound_Ts, t0); in (if has_call t0 then massage_any_call else massage_noncall) bound_Ts U T t0 end; @@ -399,12 +401,12 @@ fun expand_corec_code_rhs ctxt has_call bound_Ts t = (case fastype_of1 (bound_Ts, t) of Type (s, Ts) => - massage_let_if_case ctxt has_call (fn _ => fn t => + massage_let_if_case_corec ctxt has_call (fn _ => fn t => if can (dest_ctr ctxt s) t then t else expand_to_ctr_term ctxt s Ts t) bound_Ts t | _ => raise Fail "expand_corec_code_rhs"); fun massage_corec_code_rhs ctxt massage_ctr = - massage_let_if_case ctxt (K false) + massage_let_if_case_corec ctxt (K false) (fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb); fun fold_rev_corec_code_rhs ctxt f = @@ -883,7 +885,7 @@ fun rewrite_end _ t = if has_call t then undef_const else t; fun rewrite_cont bound_Ts t = if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const; - fun massage f _ = massage_let_if_case ctxt has_call f bound_Ts rhs_term + fun massage f _ = massage_let_if_case_corec ctxt has_call f bound_Ts rhs_term |> abs_tuple_balanced fun_args; in (massage rewrite_stop, massage rewrite_end, massage rewrite_cont) @@ -1039,7 +1041,7 @@ fun is_trivial_implies thm = uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm)); -fun add_primcorec_ursive auto opts fixes specs of_specs_opt lthy = +fun primcorec_ursive auto opts fixes specs of_specs_opt lthy = let val thy = Proof_Context.theory_of lthy; @@ -1525,7 +1527,7 @@ (goalss, after_qed, lthy') end; -fun add_primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy = +fun primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy = let val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes); val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups)); @@ -1534,18 +1536,18 @@ split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy)); val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy); in - add_primcorec_ursive auto opts fixes specs of_specs_opt lthy + primcorec_ursive auto opts fixes specs of_specs_opt lthy end; -val add_primcorecursive_cmd = (fn (goalss, after_qed, lthy) => +val primcorecursive_cmd = (fn (goalss, after_qed, lthy) => lthy |> Proof.theorem NONE after_qed goalss |> Proof.refine (Method.primitive_text (K I)) - |> Seq.hd) ooo add_primcorec_ursive_cmd false; + |> Seq.hd) ooo primcorec_ursive_cmd false; -val add_primcorec_cmd = (fn (goalss, after_qed, lthy) => +val primcorec_cmd = (fn (goalss, after_qed, lthy) => lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo - add_primcorec_ursive_cmd true; + primcorec_ursive_cmd true; val corec_option_parser = Parse.group (K "option") (Plugin_Name.parse_filter >> Plugins_Option @@ -1560,13 +1562,13 @@ "define primitive corecursive functions" ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) -- - (Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorecursive_cmd); + (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorecursive_cmd); val _ = Outer_Syntax.local_theory @{command_keyword primcorec} "define primitive corecursive functions" ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) -- - (Parse.fixes -- where_alt_props_of_parser) >> uncurry add_primcorec_cmd); + (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorec_cmd); val _ = Theory.setup (gfp_rec_sugar_interpretation Transfer_BNF.transfer_plugin gfp_rec_sugar_transfer_interpretation); diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Sat Apr 11 16:19:14 2015 +0100 @@ -26,14 +26,14 @@ val datatype_compat_global: string list -> theory -> theory val datatype_compat_cmd: string list -> local_theory -> local_theory val add_datatype: preference list -> Old_Datatype_Aux.spec list -> theory -> string list * theory - val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> + val primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> local_theory -> (term list * thm list) * local_theory - val add_primrec_global: (binding * typ option * mixfix) list -> + val primrec_global: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory -> (term list * thm list) * theory - val add_primrec_overloaded: (string * (string * typ) * bool) list -> + val primrec_overloaded: (string * (string * typ) * bool) list -> (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory -> (term list * thm list) * theory - val add_primrec_simple: ((binding * typ) * mixfix) list -> term list -> + val primrec_simple: ((binding * typ) * mixfix) list -> term list -> local_theory -> (string list * (term list * thm list)) * local_theory end; @@ -532,11 +532,12 @@ |> not (member (op =) prefs Keep_Nesting) ? perhaps (try (datatype_compat_global fpT_names))) end; -val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec; -val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global; -val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded; -val add_primrec_simple = apfst (apsnd (apsnd (flat o snd))) ooo - BNF_LFP_Rec_Sugar.add_primrec_simple; +fun old_of_new f (ts, _, simpss) = (ts, f simpss); + +val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec; +val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global; +val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded; +val primrec_simple = apfst (apsnd (old_of_new (flat o snd))) ooo BNF_LFP_Rec_Sugar.primrec_simple; val _ = Outer_Syntax.local_theory @{command_keyword datatype_compat} diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sat Apr 11 16:19:14 2015 +0100 @@ -61,17 +61,18 @@ val lfp_rec_sugar_interpretation: string -> (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory - val add_primrec: (binding * typ option * mixfix) list -> - (Attrib.binding * term) list -> local_theory -> (term list * thm list list) * local_theory - val add_primrec_cmd: rec_option list -> (binding * string option * mixfix) list -> - (Attrib.binding * string) list -> local_theory -> (term list * thm list list) * local_theory - val add_primrec_global: (binding * typ option * mixfix) list -> - (Attrib.binding * term) list -> theory -> (term list * thm list list) * theory - val add_primrec_overloaded: (string * (string * typ) * bool) list -> + val primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> + local_theory -> (term list * thm list * thm list list) * local_theory + val primrec_cmd: rec_option list -> (binding * string option * mixfix) list -> + (Attrib.binding * string) list -> local_theory -> + (term list * thm list * thm list list) * local_theory + val primrec_global: (binding * typ option * mixfix) list -> + (Attrib.binding * term) list -> theory -> (term list * thm list * thm list list) * theory + val primrec_overloaded: (string * (string * typ) * bool) list -> (binding * typ option * mixfix) list -> - (Attrib.binding * term) list -> theory -> (term list * thm list list) * theory - val add_primrec_simple: ((binding * typ) * mixfix) list -> term list -> - local_theory -> (string list * (term list * (int list list * thm list list))) * local_theory + (Attrib.binding * term) list -> theory -> (term list * thm list * thm list list) * theory + val primrec_simple: ((binding * typ) * mixfix) list -> term list -> local_theory -> + (string list * (term list * thm list * (int list list * thm list list))) * local_theory end; structure BNF_LFP_Rec_Sugar : BNF_LFP_REC_SUGAR = @@ -546,7 +547,7 @@ find_indices (op = o apply2 (fn {fun_name, ctr, ...} => (fun_name, ctr))) fun_data eqns_data; - val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs + val simps = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs |> fst |> map_filter (try (fn (x, [y]) => (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y))) @@ -556,7 +557,7 @@ |> K |> Goal.prove_sorry lthy' [] [] user_eqn |> Thm.close_derivation); in - ((js, simp_thms), lthy') + ((js, simps), lthy') end; val notes = @@ -591,7 +592,7 @@ lthy |> Local_Theory.notes (notes @ common_notes) |> snd) end; -fun add_primrec_simple0 plugins nonexhaustive transfer fixes ts lthy = +fun primrec_simple0 plugins nonexhaustive transfer fixes ts lthy = let val actual_nn = length fixes; @@ -604,20 +605,19 @@ lthy' |> fold_map Local_Theory.define defs |-> (fn defs => fn lthy => - let val (thms, lthy) = prove lthy defs; - in ((names, (map fst defs, thms)), lthy) end) + let val ((jss, simpss), lthy) = prove lthy defs; + in ((names, (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy) end) end; -fun add_primrec_simple fixes ts lthy = - add_primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy +fun primrec_simple fixes ts lthy = + primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy handle OLD_PRIMREC () => - Old_Primrec.add_primrec_simple fixes ts lthy - |>> apsnd (apsnd (pair [] o single)) o apfst single; + Old_Primrec.primrec_simple fixes ts lthy + |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single; -fun gen_primrec old_primrec prep_spec opts - (raw_fixes : (binding * 'a option * mixfix) list) raw_specs lthy = +fun gen_primrec old_primrec prep_spec opts raw_fixes raw_specs lthy = let - val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes); + val dups = duplicates (op =) (map (fn (x, _, _) => Binding.name_of x) raw_fixes); val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups)); val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) @@ -643,25 +643,27 @@ end); in lthy - |> add_primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs) - |-> (fn (names, (ts, (jss, simpss))) => + |> primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs) + |-> (fn (names, (ts, defs, (jss, simpss))) => Spec_Rules.add Spec_Rules.Equational (ts, flat simpss) #> Local_Theory.notes (mk_notes jss names simpss) - #>> pair ts o map snd) + #>> (fn notes => (ts, defs, map snd notes))) end - handle OLD_PRIMREC () => old_primrec raw_fixes raw_specs lthy |>> apsnd single; + handle OLD_PRIMREC () => + old_primrec raw_fixes raw_specs lthy + |>> (fn (ts, thms) => (ts, [], [thms])); -val add_primrec = gen_primrec Old_Primrec.add_primrec Specification.check_spec []; -val add_primrec_cmd = gen_primrec Old_Primrec.add_primrec_cmd Specification.read_spec; +val primrec = gen_primrec Old_Primrec.primrec Specification.check_spec []; +val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_spec; -fun add_primrec_global fixes specs = +fun primrec_global fixes specs = Named_Target.theory_init - #> add_primrec fixes specs + #> primrec fixes specs ##> Local_Theory.exit_global; -fun add_primrec_overloaded ops fixes specs = +fun primrec_overloaded ops fixes specs = Overloading.overloading ops - #> add_primrec fixes specs + #> primrec fixes specs ##> Local_Theory.exit_global; val rec_option_parser = Parse.group (K "option") @@ -674,6 +676,6 @@ ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser) --| @{keyword ")"}) []) -- (Parse.fixes -- Parse_Spec.where_alt_specs) - >> (fn (opts, (fixes, specs)) => snd o add_primrec_cmd opts fixes specs)); + >> (fn (opts, (fixes, specs)) => snd o primrec_cmd opts fixes specs)); end; diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Sat Apr 11 16:19:14 2015 +0100 @@ -6,7 +6,13 @@ More recursor sugar. *) -structure BNF_LFP_Rec_Sugar_More : sig end = +signature BNF_LFP_REC_SUGAR_MORE = +sig + val massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> + (typ * typ -> term) -> typ list -> term -> term -> term -> term +end; + +structure BNF_LFP_Rec_Sugar_More : BNF_LFP_REC_SUGAR_MORE = struct open BNF_Util @@ -68,20 +74,20 @@ error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t)); fun invalid_map ctxt t = error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t)); -fun unexpected_rec_call ctxt t = - error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t)); +fun unexpected_rec_call ctxt eqns t = + error_at ctxt eqns ("Unexpected recursive call in " ^ quote (Syntax.string_of_term ctxt t)); -fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' = +fun massage_nested_rec_call ctxt has_call massage_fun massage_nonfun bound_Ts y y' t0 = let - fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else (); + fun check_no_call t = if has_call t then unexpected_rec_call ctxt [t0] t else (); val typof = curry fastype_of1 bound_Ts; - val build_map_fst = build_map ctxt [] (fst_const o fst); + val massage_no_call = build_map ctxt [] massage_nonfun; val yT = typof y; val yU = typof y'; - fun y_of_y' () = build_map_fst (yU, yT) $ y'; + fun y_of_y' () = massage_no_call (yU, yT) $ y'; val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t); fun massage_mutual_fun U T t = @@ -89,12 +95,7 @@ Const (@{const_name comp}, _) $ t1 $ t2 => mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2) | _ => - if has_call t then - (case try HOLogic.dest_prodT U of - SOME (U1, U2) => if U1 = T then raw_massage_fun T U2 t else invalid_map ctxt t - | NONE => invalid_map ctxt t) - else - mk_comp bound_Ts (t, build_map_fst (U, T))); + if has_call t then massage_fun U T t else mk_comp bound_Ts (t, massage_no_call (U, T))); fun massage_map (Type (_, Us)) (Type (s, Ts)) t = (case try (dest_map ctxt s) t of @@ -115,7 +116,7 @@ massage_map U T t handle NO_MAP _ => massage_mutual_fun U T t; - fun massage_call (t as t1 $ t2) = + fun massage_outer_call (t as t1 $ t2) = if has_call t then if t2 = y then massage_map yU yT (elim_y t1) $ y' @@ -123,25 +124,28 @@ else let val (g, xs) = Term.strip_comb t2 in if g = y then - if exists has_call xs then unexpected_rec_call ctxt t2 - else Term.list_comb (massage_call (mk_compN (length xs) bound_Ts (t1, y)), xs) + if exists has_call xs then unexpected_rec_call ctxt [t0] t2 + else Term.list_comb (massage_outer_call (mk_compN (length xs) bound_Ts (t1, y)), xs) else ill_formed_rec_call ctxt t end else elim_y t - | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t; + | massage_outer_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t; in - massage_call + massage_outer_call t0 end; -fun rewrite_map_arg ctxt get_ctr_pos rec_type res_type = +fun rewrite_map_fun ctxt get_ctr_pos U T t = let - val pT = HOLogic.mk_prodT (rec_type, res_type); + val _ = + (case try HOLogic.dest_prodT U of + SOME (U1, _) => U1 = T orelse invalid_map ctxt t + | NONE => invalid_map ctxt t); - fun subst d (t as Bound d') = t |> d = SOME d' ? curry (op $) (fst_const pT) + fun subst d (t as Bound d') = t |> d = SOME d' ? curry (op $) (fst_const U) | subst d (Abs (v, T, b)) = - Abs (v, if d = SOME ~1 then pT else T, subst (Option.map (Integer.add 1) d) b) + Abs (v, if d = SOME ~1 then U else T, subst (Option.map (Integer.add 1) d) b) | subst d t = let val (u, vs) = strip_comb t; @@ -149,22 +153,22 @@ in if ctr_pos >= 0 then if d = SOME ~1 andalso length vs = ctr_pos then - Term.list_comb (permute_args ctr_pos (snd_const pT), vs) + Term.list_comb (permute_args ctr_pos (snd_const U), vs) else if length vs > ctr_pos andalso is_some d andalso d = try (fn Bound n => n) (nth vs ctr_pos) then - Term.list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs)) + Term.list_comb (snd_const U $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs)) else error ("Recursive call not directly applied to constructor argument in " ^ quote (Syntax.string_of_term ctxt t)) else - Term.list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs) - end + Term.list_comb (u, map (subst (if d = SOME ~1 then NONE else d)) vs) + end; in - subst (SOME ~1) + subst (SOME ~1) t end; fun rewrite_nested_rec_call ctxt has_call get_ctr_pos = - massage_nested_rec_call ctxt has_call (rewrite_map_arg ctxt get_ctr_pos); + massage_nested_rec_call ctxt has_call (rewrite_map_fun ctxt get_ctr_pos) (fst_const o fst); val _ = Theory.setup (register_lfp_rec_extension {nested_simps = nested_simps, is_new_datatype = is_new_datatype, diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Tools/Old_Datatype/old_primrec.ML --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Sat Apr 11 16:19:14 2015 +0100 @@ -8,16 +8,16 @@ signature OLD_PRIMREC = sig - val add_primrec: (binding * typ option * mixfix) list -> + val primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> local_theory -> (term list * thm list) * local_theory - val add_primrec_cmd: (binding * string option * mixfix) list -> + val primrec_cmd: (binding * string option * mixfix) list -> (Attrib.binding * string) list -> local_theory -> (term list * thm list) * local_theory - val add_primrec_global: (binding * typ option * mixfix) list -> + val primrec_global: (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory -> (term list * thm list) * theory - val add_primrec_overloaded: (string * (string * typ) * bool) list -> + val primrec_overloaded: (string * (string * typ) * bool) list -> (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory -> (term list * thm list) * theory - val add_primrec_simple: ((binding * typ) * mixfix) list -> term list -> + val primrec_simple: ((binding * typ) * mixfix) list -> term list -> local_theory -> (string * (term list * thm list)) * local_theory end; @@ -260,7 +260,7 @@ (* primrec definition *) -fun add_primrec_simple fixes ts lthy = +fun primrec_simple fixes ts lthy = let val ((prefix, (_, defs)), prove) = distill lthy fixes ts; in @@ -280,7 +280,7 @@ (Binding.qualify true prefix (Binding.name "simps"), @{attributes [simp, nitpick_simp]}); in lthy - |> add_primrec_simple fixes (map snd spec) + |> primrec_simple fixes (map snd spec) |-> (fn (prefix, (ts, simps)) => Spec_Rules.add Spec_Rules.Equational (ts, simps) #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps) @@ -290,22 +290,22 @@ in -val add_primrec = gen_primrec Specification.check_spec; -val add_primrec_cmd = gen_primrec Specification.read_spec; +val primrec = gen_primrec Specification.check_spec; +val primrec_cmd = gen_primrec Specification.read_spec; end; -fun add_primrec_global fixes specs thy = +fun primrec_global fixes specs thy = let val lthy = Named_Target.theory_init thy; - val ((ts, simps), lthy') = add_primrec fixes specs lthy; + val ((ts, simps), lthy') = primrec fixes specs lthy; val simps' = Proof_Context.export lthy' lthy simps; in ((ts, simps'), Local_Theory.exit_global lthy') end; -fun add_primrec_overloaded ops fixes specs thy = +fun primrec_overloaded ops fixes specs thy = let val lthy = Overloading.overloading ops thy; - val ((ts, simps), lthy') = add_primrec fixes specs lthy; + val ((ts, simps), lthy') = primrec fixes specs lthy; val simps' = Proof_Context.export lthy' lthy simps; in ((ts, simps'), Local_Theory.exit_global lthy') end; diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sat Apr 11 16:19:14 2015 +0100 @@ -96,7 +96,7 @@ subst_v (@{const Code_Numeral.Suc} $ t_k) eq]; val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0; val ((_, (_, eqs2)), lthy') = lthy - |> BNF_LFP_Compat.add_primrec_simple + |> BNF_LFP_Compat.primrec_simple [((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1; val cT_random_aux = inst pt_random_aux; val cT_rhs = inst pt_rhs; diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Tools/int_arith.ML Sat Apr 11 16:19:14 2015 +0100 @@ -79,10 +79,10 @@ make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", proc = sproc, identifier = []} -fun number_of thy T n = - if not (Sign.of_sort thy (T, @{sort numeral})) +fun number_of ctxt T n = + if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral})) then raise CTERM ("number_of", []) - else Numeral.mk_cnumber (Thm.global_ctyp_of thy T) n; + else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n; val setup = Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2] diff -r b785d6d06430 -r 05d4dce039c6 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/HOL/Tools/lin_arith.ML Sat Apr 11 16:19:14 2015 +0100 @@ -16,7 +16,7 @@ val add_simprocs: simproc list -> Context.generic -> Context.generic val add_inj_const: string * typ -> Context.generic -> Context.generic val add_discrete_type: string -> Context.generic -> Context.generic - val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic + val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic val setup: Context.generic -> Context.generic val global_setup: theory -> theory val split_limit: int Config.T diff -r b785d6d06430 -r 05d4dce039c6 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Sat Apr 11 16:19:14 2015 +0100 @@ -91,16 +91,16 @@ val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, lessD: thm list, neqE: thm list, simpset: simpset, - number_of: (theory -> typ -> int -> cterm) option} -> + number_of: (Proof.context -> typ -> int -> cterm) option} -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, lessD: thm list, neqE: thm list, simpset: simpset, - number_of: (theory -> typ -> int -> cterm) option}) -> + number_of: (Proof.context -> typ -> int -> cterm) option}) -> Context.generic -> Context.generic val add_inj_thms: thm list -> Context.generic -> Context.generic val add_lessD: thm -> Context.generic -> Context.generic val add_simps: thm list -> Context.generic -> Context.generic val add_simprocs: simproc list -> Context.generic -> Context.generic - val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic + val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic end; functor Fast_Lin_Arith @@ -119,7 +119,7 @@ lessD: thm list, neqE: thm list, simpset: simpset, - number_of: (theory -> typ -> int -> cterm) option}; + number_of: (Proof.context -> typ -> int -> cterm) option}; val empty : T = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], @@ -169,7 +169,7 @@ fun number_of ctxt = (case Data.get (Context.Proof ctxt) of - {number_of = SOME f, ...} => f (Proof_Context.theory_of ctxt) + {number_of = SOME f, ...} => f ctxt | _ => fn _ => fn _ => raise CTERM ("number_of", [])); diff -r b785d6d06430 -r 05d4dce039c6 src/Pure/drule.ML --- a/src/Pure/drule.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/Pure/drule.ML Sat Apr 11 16:19:14 2015 +0100 @@ -204,10 +204,12 @@ val ps = outer_params (Thm.term_of goal) |> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T)); val Ts = map Term.fastype_of ps; - val inst = Thm.fold_terms Term.add_vars th [] |> map (fn (xi, T) => - (Thm.global_cterm_of thy (Var (xi, T)), Thm.global_cterm_of thy (Term.list_comb (Var (xi, Ts ---> T), ps)))); + val inst = + Thm.fold_terms Term.add_vars th [] + |> map (fn (xi, T) => ((xi, T), Term.list_comb (Var (xi, Ts ---> T), ps))); in - th |> Thm.instantiate ([], inst) + th + |> Thm.instantiate (Thm.certify_inst thy ([], inst)) |> fold_rev (Thm.forall_intr o Thm.global_cterm_of thy) ps end; @@ -228,12 +230,10 @@ | zero_var_indexes_list ths = let val thy = Theory.merge_list (map Thm.theory_of_thm ths); - val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths); - val cinstT = - map (fn (v, T) => (Thm.global_ctyp_of thy (TVar v), Thm.global_ctyp_of thy T)) instT; - val cinst = - map (fn (v, t) => (Thm.global_cterm_of thy (Var v), Thm.global_cterm_of thy t)) inst; - in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end; + val inst = + Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths) + |> Thm.certify_inst thy; + in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate inst) ths end; val zero_var_indexes = singleton zero_var_indexes_list; @@ -629,9 +629,9 @@ let val thy = Thm.theory_of_cterm ct; val T = Thm.typ_of_cterm ct; - val a = Thm.global_ctyp_of thy (TVar (("'a", 0), [])); + val instT = apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), []), T); val x = Thm.global_cterm_of thy (Var (("x", 0), T)); - in Thm.instantiate ([(a, Thm.global_ctyp_of thy T)], [(x, ct)]) termI end; + in Thm.instantiate ([instT], [(x, ct)]) termI end; fun dest_term th = let val cprop = strip_imp_concl (Thm.cprop_of th) in diff -r b785d6d06430 -r 05d4dce039c6 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Sat Apr 11 11:56:40 2015 +0100 +++ b/src/ZF/Tools/primrec_package.ML Sat Apr 11 16:19:14 2015 +0100 @@ -8,8 +8,8 @@ signature PRIMREC_PACKAGE = sig - val add_primrec: ((binding * string) * Token.src list) list -> theory -> theory * thm list - val add_primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list + val primrec: ((binding * string) * Token.src list) list -> theory -> theory * thm list + val primrec_i: ((binding * term) * attribute list) list -> theory -> theory * thm list end; structure PrimrecPackage : PRIMREC_PACKAGE = @@ -161,7 +161,7 @@ (* prepare functions needed for definitions *) -fun add_primrec_i args thy = +fun primrec_i args thy = let val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args); val SOME (fname, ftype, ls, rs, con_info, eqns) = @@ -188,8 +188,8 @@ ||> Sign.parent_path; in (thy3, eqn_thms') end; -fun add_primrec args thy = - add_primrec_i (map (fn ((name, s), srcs) => +fun primrec args thy = + primrec_i (map (fn ((name, s), srcs) => ((name, Syntax.read_prop_global thy s), map (Attrib.attribute_cmd_global thy) srcs)) args) thy; @@ -199,7 +199,7 @@ val _ = Outer_Syntax.command @{command_keyword primrec} "define primitive recursive functions on datatypes" (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop) - >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap)))); + >> (Toplevel.theory o (#1 oo (primrec o map Parse.triple_swap)))); end;