--- 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
--- 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
--- 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
--- 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"
-
--- 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"
-
--- 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"
-
--- 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"
-
--- 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"
-
--- 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
-
--- 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"
--- 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.
--- 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}.
--- 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 \<circ> fst) xs)"
+lemma filter_Bag [code]: "filter_mset P (Bag xs) = Bag (DAList.filter (P \<circ> 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: "\<And>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]: "\<And>x. count (Abs_multiset (count_of x)) = count_of x"
by (rule Abs_multiset_inverse[OF count_of_multiset])
assume ys: "ys \<in> ?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 (\<lambda>_. Suc) 0 A" (is "_ = Multiset.fold ?f _ _")
+lemma size_fold: "size A = fold_mset (\<lambda>_. 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
--- 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 \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
+lift_definition filter_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"
+is "\<lambda>P M. \<lambda>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 #\<inter> N) = filter_mset P M #\<inter> filter_mset P N"
by (rule multiset_eqI) simp
-lemma filter_inter [simp]:
- "Multiset.filter P (M #\<inter> N) = Multiset.filter P M #\<inter> Multiset.filter P N"
- by (rule multiset_eqI) simp
-
-lemma multiset_filter_subset[simp]: "Multiset.filter f M \<le> M"
+lemma multiset_filter_subset[simp]: "filter_mset f M \<le> M"
unfolding less_eq_multiset.rep_eq by auto
lemma multiset_filter_mono: assumes "A \<le> B"
- shows "Multiset.filter f A \<le> Multiset.filter f B"
+ shows "filter_mset f A \<le> 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 \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ \<in># _./ _#})")
translations
- "{#x \<in># M. P#}" == "CONST Multiset.filter (\<lambda>x. P) M"
+ "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>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) \<le> size M"
+lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \<le> 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 \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
+definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
where
- "fold f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
+ "fold_mset f s M = Finite_Set.fold (\<lambda>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 "\<lambda>y. f y ^^ count M y"
by (fact comp_fun_commute_funpow)
@@ -824,7 +823,7 @@
Finite_Set.fold (\<lambda>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 \<equiv> "set_of M - {x}"
@@ -832,23 +831,23 @@
then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
Finite_Set.fold (\<lambda>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 "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold g w A) = fold f (h w) A" (is "PROP ?P")
+ shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> 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 \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> '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 \<in># Multiset.fold (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
+lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
by (induct NN) auto
notation times (infixl "*" 70)
@@ -1353,7 +1352,7 @@
lemma msetprod_multiplicity:
"msetprod M = setprod (\<lambda>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 "\<And>z. z \<in> set_of {#} \<Longrightarrow> False"
by auto
--- 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 \<Longrightarrow> 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
--- 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
--- 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;
--- 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;
--- 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}
--- 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))
--- 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" +
--- 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
--- 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);
--- 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}
--- 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;
--- 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,
--- 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;
--- 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;
--- 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]
--- 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
--- 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", []));
--- 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
--- 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;