--- a/Admin/isatest/isatest-stats Fri Aug 20 14:15:29 2010 +0200
+++ b/Admin/isatest/isatest-stats Fri Aug 20 14:18:55 2010 +0200
@@ -6,7 +6,7 @@
THIS=$(cd "$(dirname "$0")"; pwd -P)
-PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
+PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
ISABELLE_SESSIONS="\
HOL-Plain \
--- a/Admin/isatest/settings/at-mac-poly-5.1-para Fri Aug 20 14:15:29 2010 +0200
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Fri Aug 20 14:18:55 2010 +0200
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.2.1"
- ML_SYSTEM="polyml-5.2.1"
+ POLYML_HOME="/home/polyml/polyml-svn"
+ ML_SYSTEM="polyml-5.4.0"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--mutable 800 --immutable 2000"
--- a/Admin/isatest/settings/at-poly-5.1-para-e Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
- POLYML_HOME="/home/polyml/polyml-5.2.1"
- ML_SYSTEM="polyml-5.2.1"
- ML_PLATFORM="x86-linux"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 500"
-
-ISABELLE_HOME_USER=~/isabelle-at-poly-para-e
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 10"
-
-unset KODKODI
-
--- a/Admin/isatest/settings/at-poly-dev-e Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
- POLYML_HOME="/home/polyml/polyml-5.2"
- ML_SYSTEM="polyml-5.2"
- ML_PLATFORM="x86-linux"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 500"
-
-ISABELLE_HOME_USER=~/isabelle-at-poly-dev-e
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
-
-unset KODKODI
-
--- a/Admin/polyml/README Fri Aug 20 14:15:29 2010 +0200
+++ b/Admin/polyml/README Fri Aug 20 14:18:55 2010 +0200
@@ -1,27 +1,15 @@
-
-This distribution of Poly/ML 5.3 is based on the original
-polyml.5.3.tar.gz from http://www.polyml.org with some minimal changes:
+Poly/ML for Isabelle
+====================
-diff polyml.5.3/libpolyml/processes.cpp-orig polyml.5.3/libpolyml/processes.cpp
-995,996c995,996
-< // we set this to 100ms so that we're not waiting too long.
-< if (maxMillisecs > 100) maxMillisecs = 100;
----
-> // we set this to 10ms so that we're not waiting too long.
-> if (maxMillisecs > 10) maxMillisecs = 10;
+This distribution of Poly/ML 5.4 has been compiled from the original
+sources using the included build script. For example:
-
-Then it is compiled as follows:
+ ./build polyml.5.4 x86-linux --with-gmp
- cd polyml.5.3
- ./configure --prefix="$HOME/tmp/polyml"
- make
- make install
-
-
-Now $HOME/tmp/polyml/bin/* and $HOME/tmp/polyml/lib/* are moved to the
-platform-specific target directory (e.g. polyml-5.3.0/x86-linux).
+The resulting executables and shared libraries are moved to
+x86-linux/. This directory layout accomodates the standard ML_HOME
+settings for Isabelle.
Makarius
- 26-May-2010
+ 17-Aug-2010
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/polyml/build Fri Aug 20 14:18:55 2010 +0200
@@ -0,0 +1,85 @@
+#!/usr/bin/env bash
+#
+# Multi-platform build script for Poly/ML
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+PRG="$(basename "$0")"
+
+
+# diagnostics
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG SOURCE TARGET [OPTIONS]"
+ echo
+ echo " Build Poly/ML in SOURCE directory for given platform in TARGET,"
+ echo " using the usual Isabelle platform identifiers."
+ echo
+ echo " Additional options for ./configure may be given, e.g. --with-gmp"
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+# command line args
+
+[ "$#" -eq 0 ] && usage
+SOURCE="$1"; shift
+
+[ "$#" -eq 0 ] && usage
+TARGET="$1"; shift
+
+USER_OPTIONS=("$@")
+
+
+# main
+
+[ -d "$SOURCE" ] || fail "Bad source directory: \"$SOURCE\""
+
+case "$TARGET" in
+ x86-linux)
+ OPTIONS=()
+ ;;
+ x86_64-linux)
+ OPTIONS=()
+ ;;
+ x86-darwin)
+ OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3'
+ CXXFLAGS='-arch i686 -O3' CCASFLAGS='-arch i686 -O3')
+ ;;
+ x86_64-darwin)
+ OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3'
+ CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64')
+ ;;
+ x86-cygwin)
+ OPTIONS=()
+ ;;
+ ppc-darwin | sparc-solaris | x86-solaris | x86-bsd)
+ OPTIONS=()
+ ;;
+ *)
+ fail "Bad platform identifier: \"$TARGET\""
+ ;;
+esac
+
+(
+ cd "$SOURCE"
+ make distclean
+
+ { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \
+ make compiler && \
+ make install; } || fail "Build failed"
+)
+
+mkdir -p "$TARGET"
+mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
+mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
+rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
+rm -rf "$SOURCE/$TARGET/share"
--- a/NEWS Fri Aug 20 14:15:29 2010 +0200
+++ b/NEWS Fri Aug 20 14:18:55 2010 +0200
@@ -35,6 +35,18 @@
*** HOL ***
+* Records: logical foundation type for records do not carry a '_type' suffix
+any longer. INCOMPATIBILITY.
+
+* Code generation for records: more idiomatic representation of record types.
+Warning: records are not covered by ancient SML code generation any longer.
+INCOMPATIBILITY. In cases of need, a suitable rep_datatype declaration
+helps to succeed then:
+
+ record 'a foo = ...
+ ...
+ rep_datatype foo_ext ...
+
* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
INCOMPATIBILITY.
@@ -74,9 +86,20 @@
* Some previously unqualified names have been qualified:
types
+ bool ~> HOL.bool
nat ~> Nat.nat
constants
+ Trueprop ~> HOL.Trueprop
+ True ~> HOL.True
+ False ~> HOL.False
+ Not ~> HOL.Not
+ The ~> HOL.The
+ All ~> HOL.All
+ Ex ~> HOL.Ex
+ Ex1 ~> HOL.Ex1
+ Let ~> HOL.Let
+ If ~> HOL.If
Ball ~> Set.Ball
Bex ~> Set.Bex
Suc ~> Nat.Suc
@@ -90,7 +113,7 @@
INCOMPATIBILITY.
* Removed simplifier congruence rule of "prod_case", as has for long
-been the case with "split".
+been the case with "split". INCOMPATIBILITY.
* Datatype package: theorems generated for executable equality
(class eq) carry proper names and are treated as default code
@@ -99,8 +122,8 @@
* List.thy: use various operations from the Haskell prelude when
generating Haskell code.
-* code_simp.ML: simplification with rules determined by
-code generator.
+* code_simp.ML and method code_simp: simplification with rules determined
+by code generator.
* code generator: do not print function definitions for case
combinators any longer.
@@ -131,6 +154,16 @@
similar to inductive_cases.
+*** FOL ***
+
+* All constant names are now qualified. INCOMPATIBILITY.
+
+
+*** ZF ***
+
+* All constant names are now qualified. INCOMPATIBILITY.
+
+
*** ML ***
* ML antiquotations @{theory} and @{theory_ref} refer to named
@@ -139,6 +172,11 @@
change in semantics.
+*** System ***
+
+* Discontinued support for Poly/ML 5.0 and 5.1 versions.
+
+
New in Isabelle2009-2 (June 2010)
---------------------------------
--- a/README Fri Aug 20 14:15:29 2010 +0200
+++ b/README Fri Aug 20 14:18:55 2010 +0200
@@ -13,7 +13,7 @@
Windows with Cygwin, Mac OS) and depends on the following main
add-on tools:
- * The Poly/ML compiler and runtime system (version 5.x).
+ * The Poly/ML compiler and runtime system (version 5.2.1 or later).
* The GNU bash shell (version 3.x or 2.x).
* Perl (version 5.x).
* GNU Emacs (version 22) -- for the Proof General interface.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Fri Aug 20 14:18:55 2010 +0200
@@ -0,0 +1,251 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Evaluation}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Evaluation\isanewline
+\isakeyword{imports}\ Setup\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsection{Evaluation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Introduction%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Evaluation techniques%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+simplifier%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+nbe%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+eval target: SML standalone vs. Isabelle/SML, example, soundness%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Dynamic evaluation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+value (three variants)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+methods (three variants)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+corresponding ML interfaces%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Static evaluation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+code_simp, nbe (tbd), Eval (tbd, in simple fashion)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+hand-written: code antiquotation%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Hybrid techniques%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+code reflect runtime%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+code reflect external%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME here the old sections follow%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Evaluation oracle%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Code generation may also be used to \emph{evaluate} expressions
+ (using \isa{SML} as target language of course).
+ For instance, the \indexdef{}{command}{value}\hypertarget{command.value}{\hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}}} reduces an expression to a
+ normal form with respect to the underlying code equations:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{value}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent will display \isa{{\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}}.
+
+ The \hyperlink{method.eval}{\mbox{\isa{eval}}} method tries to reduce a goal by code generation to \isa{True}
+ and solves it in that case, but fails otherwise:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}\ {\isacharequal}\ {\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ eval%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The soundness of the \hyperlink{method.eval}{\mbox{\isa{eval}}} method depends crucially
+ on the correctness of the code generator; this is one of the reasons
+ why you should not use adaptation (see \secref{sec:adaptation}) frivolously.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Code antiquotation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In scenarios involving techniques like reflection it is quite common
+ that code generated from a theory forms the basis for implementing
+ a proof procedure in \isa{SML}. To facilitate interfacing of generated code
+ with system code, the code generator provides a \isa{code} antiquotation:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{datatype}\isamarkupfalse%
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isadelimquotett
+\ %
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ fun\ eval{\isacharunderscore}form\ %
+\isaantiq
+code\ T%
+\endisaantiq
+\ {\isacharequal}\ true\isanewline
+\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ %
+\isaantiq
+code\ F%
+\endisaantiq
+\ {\isacharequal}\ false\isanewline
+\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}%
+\isaantiq
+code\ And%
+\endisaantiq
+\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ andalso\ eval{\isacharunderscore}form\ q\isanewline
+\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}%
+\isaantiq
+code\ Or%
+\endisaantiq
+\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagquotett
+{\isafoldquotett}%
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\begin{isamarkuptext}%
+\noindent \isa{code} takes as argument the name of a constant; after the
+ whole \isa{SML} is read, the necessary code is generated transparently
+ and the corresponding constant names are inserted. This technique also
+ allows to use pattern matching on constructors stemming from compiled
+ \isa{datatypes}.
+
+ For a less simplistic example, theory \hyperlink{theory.Ferrack}{\mbox{\isa{Ferrack}}} is
+ a good reference.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy Fri Aug 20 14:18:55 2010 +0200
@@ -97,7 +97,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML_type local_theory: Proof.context} \\
- @{index_ML Named_Target.init: "string option -> theory -> local_theory"} \\[1ex]
+ @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
@{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory"} \\
@{index_ML Local_Theory.note: "Attrib.binding * thm list ->
@@ -114,13 +114,13 @@
with operations on expecting a regular @{text "ctxt:"}~@{ML_type
Proof.context}.
- \item @{ML Named_Target.init}~@{text "NONE thy"} initializes a
- trivial local theory from the given background theory.
- Alternatively, @{text "SOME name"} may be given to initialize a
- @{command locale} or @{command class} context (a fully-qualified
- internal name is expected here). This is useful for experimentation
- --- normally the Isar toplevel already takes care to initialize the
- local theory context.
+ \item @{ML Named_Target.init}~@{text "name thy"} initializes a local
+ theory derived from the given background theory. An empty name
+ refers to a \emph{global theory} context, and a non-empty name
+ refers to a @{command locale} or @{command class} context (a
+ fully-qualified internal name is expected here). This is useful for
+ experimentation --- normally the Isar toplevel already takes care to
+ initialize the local theory context.
\item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
lthy"} defines a local entity according to the specification that is
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Fri Aug 20 14:15:29 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Fri Aug 20 14:18:55 2010 +0200
@@ -123,7 +123,7 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
- \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string option -> theory -> local_theory| \\[1ex]
+ \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string -> theory -> local_theory| \\[1ex]
\indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline%
\verb| local_theory -> (term * (string * thm)) * local_theory| \\
\indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline%
@@ -139,13 +139,13 @@
any value \isa{lthy{\isacharcolon}}~\verb|local_theory| can be also used
with operations on expecting a regular \isa{ctxt{\isacharcolon}}~\verb|Proof.context|.
- \item \verb|Named_Target.init|~\isa{NONE\ thy} initializes a
- trivial local theory from the given background theory.
- Alternatively, \isa{SOME\ name} may be given to initialize a
- \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a fully-qualified
- internal name is expected here). This is useful for experimentation
- --- normally the Isar toplevel already takes care to initialize the
- local theory context.
+ \item \verb|Named_Target.init|~\isa{name\ thy} initializes a local
+ theory derived from the given background theory. An empty name
+ refers to a \emph{global theory} context, and a non-empty name
+ refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a
+ fully-qualified internal name is expected here). This is useful for
+ experimentation --- normally the Isar toplevel already takes care to
+ initialize the local theory context.
\item \verb|Local_Theory.define|~\isa{{\isacharparenleft}{\isacharparenleft}b{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}a{\isacharcomma}\ rhs{\isacharparenright}{\isacharparenright}\ lthy} defines a local entity according to the specification that is
given relatively to the current \isa{lthy} context. In
--- a/etc/isar-keywords-ZF.el Fri Aug 20 14:15:29 2010 +0200
+++ b/etc/isar-keywords-ZF.el Fri Aug 20 14:18:55 2010 +0200
@@ -8,8 +8,6 @@
'("\\."
"\\.\\."
"Isabelle\\.command"
- "Isar\\.define_command"
- "Isar\\.edit_document"
"ML"
"ML_command"
"ML_prf"
@@ -256,8 +254,6 @@
(defconst isar-keywords-control
'("Isabelle\\.command"
- "Isar\\.define_command"
- "Isar\\.edit_document"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
"ProofGeneral\\.kill_proof"
--- a/etc/isar-keywords.el Fri Aug 20 14:15:29 2010 +0200
+++ b/etc/isar-keywords.el Fri Aug 20 14:18:55 2010 +0200
@@ -8,8 +8,6 @@
'("\\."
"\\.\\."
"Isabelle\\.command"
- "Isar\\.define_command"
- "Isar\\.edit_document"
"ML"
"ML_command"
"ML_prf"
@@ -320,8 +318,6 @@
(defconst isar-keywords-control
'("Isabelle\\.command"
- "Isar\\.define_command"
- "Isar\\.edit_document"
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
"ProofGeneral\\.kill_proof"
--- a/lib/scripts/run-polyml-5.0 Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Poly/ML 5.0 startup script.
-
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail_out()
-{
- echo "Unable to create output heap file: \"$OUTFILE\"" >&2
- exit 2
-}
-
-function check_file()
-{
- if [ ! -f "$1" ]; then
- echo "Unable to locate $1" >&2
- echo "Please check your ML system settings!" >&2
- exit 2
- fi
-}
-
-
-## compiler executables and libraries
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-if [ "$(basename "$ML_HOME")" = bin ]; then
- POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
-else
- POLYLIB="$ML_HOME"
-fi
-
-export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH"
-export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH"
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
- PRG="$POLY"
- EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
-else
- check_file "$INFILE"
- PRG="$INFILE"
- EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
- COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
-else
- COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
- [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
- rm -f "${OUTFILE}.o" || fail_out
-fi
-
-
-## run it!
-
-MLTEXT="$EXIT $COMMIT $MLTEXT"
-MLEXIT="commit();"
-
-if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS=""
-else
- FEEDER_OPTS="-q"
-fi
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
- { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-RC="$?"
-
-if [ -n "$OUTFILE" ]; then
- if [ -e "${OUTFILE}.o" ]; then
- cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml $POLY_LINK_OPTIONS || fail_out
- rm -f "${OUTFILE}.o"
- [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
- fi
- [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-fi
-
-exit "$RC"
--- a/src/FOL/IFOL.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/FOL/IFOL.thy Fri Aug 20 14:18:55 2010 +0200
@@ -28,8 +28,6 @@
setup PureThy.old_appl_syntax_setup
-global
-
classes "term"
default_sort "term"
@@ -87,8 +85,6 @@
Ex (binder "\<exists>" 10) and
Ex1 (binder "\<exists>!" 10)
-local
-
finalconsts
False All Ex
"op ="
--- a/src/FOLP/IFOLP.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/FOLP/IFOLP.thy Fri Aug 20 14:18:55 2010 +0200
@@ -12,8 +12,6 @@
setup PureThy.old_appl_syntax_setup
-global
-
classes "term"
default_sort "term"
@@ -63,8 +61,6 @@
nrm :: p
NRM :: p
-local
-
syntax "_Proof" :: "[p,o]=>prop" ("(_ /: _)" [51, 10] 5)
ML {*
--- a/src/HOL/Bali/DeclConcepts.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy Fri Aug 20 14:18:55 2010 +0200
@@ -98,7 +98,7 @@
lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
by (simp add: acc_modi_accmodi_def)
-instantiation decl_ext_type:: (type) has_accmodi
+instantiation decl_ext :: (type) has_accmodi
begin
definition
@@ -150,7 +150,7 @@
class has_declclass =
fixes declclass:: "'a \<Rightarrow> qtname"
-instantiation qtname_ext_type :: (type) has_declclass
+instantiation qtname_ext :: (type) has_declclass
begin
definition
@@ -162,7 +162,7 @@
lemma qtname_declclass_def:
"declclass q \<equiv> (q::qtname)"
- by (induct q) (simp add: declclass_qtname_ext_type_def)
+ by (induct q) (simp add: declclass_qtname_ext_def)
lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
by (simp add: qtname_declclass_def)
@@ -186,14 +186,14 @@
class has_static =
fixes is_static :: "'a \<Rightarrow> bool"
-instantiation decl_ext_type :: (has_static) has_static
+instantiation decl_ext :: (has_static) has_static
begin
instance ..
end
-instantiation member_ext_type :: (type) has_static
+instantiation member_ext :: (type) has_static
begin
instance ..
@@ -457,21 +457,21 @@
class has_resTy =
fixes resTy:: "'a \<Rightarrow> ty"
-instantiation decl_ext_type :: (has_resTy) has_resTy
+instantiation decl_ext :: (has_resTy) has_resTy
begin
instance ..
end
-instantiation member_ext_type :: (has_resTy) has_resTy
+instantiation member_ext :: (has_resTy) has_resTy
begin
instance ..
end
-instantiation mhead_ext_type :: (type) has_resTy
+instantiation mhead_ext :: (type) has_resTy
begin
instance ..
@@ -487,7 +487,7 @@
lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
by (simp add: mhead_def mhead_resTy_simp)
-instantiation prod :: ("type","has_resTy") has_resTy
+instantiation prod :: (type, has_resTy) has_resTy
begin
definition
--- a/src/HOL/Bali/Name.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Bali/Name.thy Fri Aug 20 14:18:55 2010 +0200
@@ -75,7 +75,7 @@
end
definition
- qtname_qtname_def: "qtname (q::'a qtname_ext_type) = q"
+ qtname_qtname_def: "qtname (q::'a qtname_scheme) = q"
translations
(type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
--- a/src/HOL/Bali/TypeRel.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Bali/TypeRel.thy Fri Aug 20 14:18:55 2010 +0200
@@ -512,12 +512,13 @@
apply (ind_cases "G\<turnstile>S\<preceq>NT")
by auto
-lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object"
-apply (case_tac T)
-apply (auto)
-apply (subgoal_tac "G\<turnstile>qtname_ext_type\<preceq>\<^sub>C Object")
-apply (auto intro: subcls_ObjectI)
-done
+lemma widen_Object:
+ assumes "isrtype G T" and "ws_prog G"
+ shows "G\<turnstile>RefT T \<preceq> Class Object"
+proof (cases T)
+ case (ClassT C) with assms have "G\<turnstile>C\<preceq>\<^sub>C Object" by (auto intro: subcls_ObjectI)
+ with ClassT show ?thesis by auto
+qed simp_all
lemma widen_trans_lemma [rule_format (no_asm)]:
"\<lbrakk>G\<turnstile>S\<preceq>U; \<forall>C. is_class G C \<longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object\<rbrakk> \<Longrightarrow> \<forall>T. G\<turnstile>U\<preceq>T \<longrightarrow> G\<turnstile>S\<preceq>T"
--- a/src/HOL/Decision_Procs/Approximation.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Aug 20 14:18:55 2010 +0200
@@ -3301,11 +3301,11 @@
ML {*
fun reorder_bounds_tac prems i =
let
- fun variable_of_bound (Const ("Trueprop", _) $
+ fun variable_of_bound (Const (@{const_name Trueprop}, _) $
(Const (@{const_name Set.member}, _) $
Free (name, _) $ _)) = name
- | variable_of_bound (Const ("Trueprop", _) $
- (Const ("op =", _) $
+ | variable_of_bound (Const (@{const_name Trueprop}, _) $
+ (Const (@{const_name "op ="}, _) $
Free (name, _) $ _)) = name
| variable_of_bound t = raise TERM ("variable_of_bound", [t])
--- a/src/HOL/Decision_Procs/Cooper.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Aug 20 14:18:55 2010 +0200
@@ -1960,12 +1960,12 @@
@{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term ps vs t')
- | fm_of_term ps vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
+ | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
let
val (xn', p') = variant_abs (xn, xT, p);
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
in @{code E} (fm_of_term ps vs' p) end
- | fm_of_term ps vs (Const ("All", _) $ Abs (xn, xT, p)) =
+ | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
let
val (xn', p') = variant_abs (xn, xT, p);
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri Aug 20 14:18:55 2010 +0200
@@ -519,9 +519,9 @@
val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
fun h x t =
case term_of t of
- Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
+ Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
else Ferrante_Rackoff_Data.Nox
- | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
+ | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
| b$y$z => if Term.could_unify (b, lt) then
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
@@ -771,7 +771,7 @@
in rth end
| _ => Thm.reflexive ct)
-| Const("op =",_)$_$Const(@{const_name Groups.zero},_) =>
+| Const(@{const_name "op ="},_)$_$Const(@{const_name Groups.zero},_) =>
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
@@ -835,7 +835,7 @@
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| Const("op =",_)$a$b =>
+| Const(@{const_name "op ="},_)$a$b =>
let val (ca,cb) = Thm.dest_binop ct
val T = ctyp_of_term ca
val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
@@ -844,7 +844,7 @@
(Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
-| @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
+| @{term "Not"} $(Const(@{const_name "op ="},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
| _ => Thm.reflexive ct
end;
@@ -852,9 +852,9 @@
let
fun h x t =
case term_of t of
- Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
+ Const(@{const_name "op ="}, _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
else Ferrante_Rackoff_Data.Nox
- | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
+ | @{term "Not"}$(Const(@{const_name "op ="}, _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
else Ferrante_Rackoff_Data.Nox
| Const(@{const_name Orderings.less},_)$y$z =>
if term_of x aconv y then Ferrante_Rackoff_Data.Lt
--- a/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 20 14:18:55 2010 +0200
@@ -2000,9 +2000,9 @@
| fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
- | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
@{code E} (fm_of_term (("", dummyT) :: vs) p)
- | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
@{code A} (fm_of_term (("", dummyT) :: vs) p)
| fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
--- a/src/HOL/Decision_Procs/MIR.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Aug 20 14:18:55 2010 +0200
@@ -5845,9 +5845,9 @@
@{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term vs t')
- | fm_of_term vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
@{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
- | fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
@{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
| fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Aug 20 14:18:55 2010 +0200
@@ -2960,7 +2960,7 @@
val ifft = @{term "op = :: bool => _"}
fun llt rT = Const(@{const_name Orderings.less},rrT rT);
fun lle rT = Const(@{const_name Orderings.less},rrT rT);
-fun eqt rT = Const("op =",rrT rT);
+fun eqt rT = Const(@{const_name "op ="},rrT rT);
fun rz rT = Const(@{const_name Groups.zero},rT);
fun dest_nat t = case t of
@@ -3015,26 +3015,26 @@
fun fm_of_term m m' fm =
case fm of
- Const("True",_) => @{code T}
- | Const("False",_) => @{code F}
- | Const("Not",_)$p => @{code NOT} (fm_of_term m m' p)
- | Const("op &",_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
- | Const("op |",_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
- | Const("op -->",_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
- | Const("op =",ty)$p$q =>
+ Const(@{const_name True},_) => @{code T}
+ | Const(@{const_name False},_) => @{code F}
+ | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
+ | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
+ | Const(@{const_name "op ="},ty)$p$q =>
if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
| Const(@{const_name Orderings.less},_)$p$q =>
@{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
| Const(@{const_name Orderings.less_eq},_)$p$q =>
@{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
- | Const("Ex",_)$Abs(xn,xT,p) =>
+ | Const(@{const_name Ex},_)$Abs(xn,xT,p) =>
let val (xn', p') = variant_abs (xn,xT,p)
val x = Free(xn',xT)
fun incr i = i + 1
val m0 = (x,0):: (map (apsnd incr) m)
in @{code E} (fm_of_term m0 m' p') end
- | Const("All",_)$Abs(xn,xT,p) =>
+ | Const(@{const_name All},_)$Abs(xn,xT,p) =>
let val (xn', p') = variant_abs (xn,xT,p)
val x = Free(xn',xT)
fun incr i = i + 1
@@ -3045,8 +3045,8 @@
fun term_of_fm T m m' t =
case t of
- @{code T} => Const("True",bT)
- | @{code F} => Const("False",bT)
+ @{code T} => Const(@{const_name True},bT)
+ | @{code F} => Const(@{const_name False},bT)
| @{code NOT} p => nott $ (term_of_fm T m m' p)
| @{code And} (p,q) => conjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
| @{code Or} (p,q) => disjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
--- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Aug 20 14:18:55 2010 +0200
@@ -110,7 +110,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
- Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
+ Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
in
((pth RS iffD2) RS pre_thm,
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Fri Aug 20 14:18:55 2010 +0200
@@ -91,7 +91,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case prop_of pre_thm of
- Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
+ Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
in
(trace_msg ("calling procedure with term:\n" ^
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Aug 20 14:18:55 2010 +0200
@@ -33,12 +33,12 @@
{isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
let
fun uset (vars as (x::vs)) p = case term_of p of
- Const("op &", _)$ _ $ _ =>
+ Const(@{const_name "op &"}, _)$ _ $ _ =>
let
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
val (lS,lth) = uset vars l val (rS, rth) = uset vars r
in (lS@rS, Drule.binop_cong_rule b lth rth) end
- | Const("op |", _)$ _ $ _ =>
+ | Const(@{const_name "op |"}, _)$ _ $ _ =>
let
val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
val (lS,lth) = uset vars l val (rS, rth) = uset vars r
@@ -77,7 +77,7 @@
fun main vs p =
let
val ((xn,ce),(x,fm)) = (case term_of p of
- Const("Ex",_)$Abs(xn,xT,_) =>
+ Const(@{const_name Ex},_)$Abs(xn,xT,_) =>
Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
| _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
val cT = ctyp_of_term x
@@ -122,12 +122,12 @@
fun decomp_mpinf fm =
case term_of fm of
- Const("op &",_)$_$_ =>
+ Const(@{const_name "op &"},_)$_$_ =>
let val (p,q) = Thm.dest_binop fm
in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
(Thm.cabs x p) (Thm.cabs x q))
end
- | Const("op |",_)$_$_ =>
+ | Const(@{const_name "op |"},_)$_$_ =>
let val (p,q) = Thm.dest_binop fm
in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
(Thm.cabs x p) (Thm.cabs x q))
@@ -175,19 +175,19 @@
let
fun h bounds tm =
(case term_of tm of
- Const ("op =", T) $ _ $ _ =>
+ Const (@{const_name "op ="}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else Thm.dest_fun2 tm
- | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
- | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("op &", _) $ _ $ _ => find_args bounds tm
- | Const ("op |", _) $ _ $ _ => find_args bounds tm
- | Const ("op -->", _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
| Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
and find_args bounds tm =
(h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
--- a/src/HOL/Decision_Procs/langford.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Fri Aug 20 14:18:55 2010 +0200
@@ -30,7 +30,7 @@
fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
case term_of ep of
- Const("Ex",_)$_ =>
+ Const(@{const_name Ex},_)$_ =>
let
val p = Thm.dest_arg ep
val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid)
@@ -116,13 +116,13 @@
fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
fun is_eqx x eq = case term_of eq of
- Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x
+ Const(@{const_name "op ="},_)$l$r => l aconv term_of x orelse r aconv term_of x
| _ => false ;
local
fun proc ct =
case term_of ct of
- Const("Ex",_)$Abs (xn,_,_) =>
+ Const(@{const_name Ex},_)$Abs (xn,_,_) =>
let
val e = Thm.dest_fun ct
val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
@@ -176,19 +176,19 @@
let
fun h bounds tm =
(case term_of tm of
- Const ("op =", T) $ _ $ _ =>
+ Const (@{const_name "op ="}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else Thm.dest_fun2 tm
- | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
- | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("op &", _) $ _ $ _ => find_args bounds tm
- | Const ("op |", _) $ _ $ _ => find_args bounds tm
- | Const ("op -->", _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
- | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
and find_args bounds tm =
(h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Aug 20 14:18:55 2010 +0200
@@ -132,7 +132,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
- Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
+ Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let val pth =
(* If quick_and_dirty then run without proof generation as oracle*)
if !quick_and_dirty
--- a/src/HOL/HOL.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/HOL.thy Fri Aug 20 14:18:55 2010 +0200
@@ -47,33 +47,28 @@
"fun" :: (type, type) type
itself :: (type) type
-global
-
typedecl bool
judgment
Trueprop :: "bool => prop" ("(_)" 5)
consts
- Not :: "bool => bool" ("~ _" [40] 40)
True :: bool
False :: bool
+ Not :: "bool => bool" ("~ _" [40] 40)
+global consts
+ "op &" :: "[bool, bool] => bool" (infixr "&" 35)
+ "op |" :: "[bool, bool] => bool" (infixr "|" 30)
+ "op -->" :: "[bool, bool] => bool" (infixr "-->" 25)
+
+ "op =" :: "['a, 'a] => bool" (infixl "=" 50)
+
+local consts
The :: "('a => bool) => 'a"
All :: "('a => bool) => bool" (binder "ALL " 10)
Ex :: "('a => bool) => bool" (binder "EX " 10)
Ex1 :: "('a => bool) => bool" (binder "EX! " 10)
- Let :: "['a, 'a => 'b] => 'b"
-
- "op =" :: "['a, 'a] => bool" (infixl "=" 50)
- "op &" :: "[bool, bool] => bool" (infixr "&" 35)
- "op |" :: "[bool, bool] => bool" (infixr "|" 30)
- "op -->" :: "[bool, bool] => bool" (infixr "-->" 25)
-
-local
-
-consts
- If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
subsubsection {* Additional concrete syntax *}
@@ -127,8 +122,6 @@
translations
"THE x. P" == "CONST The (%x. P)"
- "_Let (_binds b bs) e" == "_Let b (_Let bs e)"
- "let x = a in e" == "CONST Let a (%x. e)"
print_translation {*
[(@{const_syntax The}, fn [Abs abs] =>
@@ -185,15 +178,21 @@
iff: "(P-->Q) --> (Q-->P) --> (P=Q)"
True_or_False: "(P=True) | (P=False)"
-defs
- Let_def [code]: "Let s f == f(s)"
- if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
-
finalconsts
"op ="
"op -->"
The
+definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
+ "If P x y \<equiv> (THE z::'a. (P=True --> z=x) & (P=False --> z=y))"
+
+definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" where
+ "Let s f \<equiv> f s"
+
+translations
+ "_Let (_binds b bs) e" == "_Let b (_Let bs e)"
+ "let x = a in e" == "CONST Let a (%x. e)"
+
axiomatization
undefined :: 'a
@@ -1084,16 +1083,16 @@
text {* \medskip if-then-else rules *}
lemma if_True [code]: "(if True then x else y) = x"
- by (unfold if_def) blast
+ by (unfold If_def) blast
lemma if_False [code]: "(if False then x else y) = y"
- by (unfold if_def) blast
+ by (unfold If_def) blast
lemma if_P: "P ==> (if P then x else y) = x"
- by (unfold if_def) blast
+ by (unfold If_def) blast
lemma if_not_P: "~P ==> (if P then x else y) = y"
- by (unfold if_def) blast
+ by (unfold If_def) blast
lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
apply (rule case_split [of Q])
@@ -1365,7 +1364,7 @@
and "c \<Longrightarrow> x = u"
and "\<not> c \<Longrightarrow> y = v"
shows "(if b then x else y) = (if c then u else v)"
- unfolding if_def using assms by simp
+ using assms by simp
text {* Prevents simplification of x and y:
faster and allows the execution of functional programs. *}
@@ -1390,13 +1389,6 @@
"f (if c then x else y) = (if c then f x else f y)"
by simp
-text {* This lemma restricts the effect of the rewrite rule u=v to the left-hand
- side of an equality. Used in @{text "{Integ,Real}/simproc.ML"} *}
-lemma restrict_to_left:
- assumes "x = y"
- shows "(x = z) = (y = z)"
- using assms by simp
-
subsubsection {* Generic cases and induction *}
@@ -1582,7 +1574,7 @@
val atomize_conjL = @{thm atomize_conjL}
val atomize_disjL = @{thm atomize_disjL}
val operator_names =
- [@{const_name "op |"}, @{const_name "op &"}, @{const_name "Ex"}]
+ [@{const_name "op |"}, @{const_name "op &"}, @{const_name Ex}]
);
*}
--- a/src/HOL/Import/HOL/bool.imp Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Import/HOL/bool.imp Fri Aug 20 14:18:55 2010 +0200
@@ -12,11 +12,11 @@
"ARB" > "ARB_def"
const_maps
- "~" > "Not"
+ "~" > "HOL.Not"
"bool_case" > "Datatype.bool.bool_case"
"\\/" > "op |"
"TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
- "T" > "True"
+ "T" > "HOL.True"
"RES_SELECT" > "HOL4Base.bool.RES_SELECT"
"RES_FORALL" > "HOL4Base.bool.RES_FORALL"
"RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE"
@@ -25,13 +25,13 @@
"ONE_ONE" > "HOL4Setup.ONE_ONE"
"LET" > "HOL4Compat.LET"
"IN" > "HOL4Base.bool.IN"
- "F" > "False"
+ "F" > "HOL.False"
"COND" > "HOL.If"
"ARB" > "HOL4Base.bool.ARB"
- "?!" > "Ex1"
- "?" > "Ex"
+ "?!" > "HOL.Ex1"
+ "?" > "HOL.Ex"
"/\\" > "op &"
- "!" > "All"
+ "!" > "HOL.All"
thm_maps
"bool_case_thm" > "HOL4Base.bool.bool_case_thm"
--- a/src/HOL/Import/HOLLight/hollight.imp Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Fri Aug 20 14:18:55 2010 +0200
@@ -18,13 +18,13 @@
"finite_sum" > "HOLLight.hollight.finite_sum"
"finite_image" > "HOLLight.hollight.finite_image"
"cart" > "HOLLight.hollight.cart"
- "bool" > "bool"
+ "bool" > "HOL.bool"
"N_3" > "HOLLight.hollight.N_3"
"N_2" > "HOLLight.hollight.N_2"
"N_1" > "Product_Type.unit"
const_maps
- "~" > "Not"
+ "~" > "HOL.Not"
"two_2" > "HOLLight.hollight.two_2"
"two_1" > "HOLLight.hollight.two_1"
"treal_of_num" > "HOLLight.hollight.treal_of_num"
@@ -229,8 +229,8 @@
"ALL2" > "HOLLight.hollight.ALL2"
"ABS_prod" > "Abs_Prod"
"@" > "Hilbert_Choice.Eps"
- "?!" > "Ex1"
- "?" > "Ex"
+ "?!" > "HOL.Ex1"
+ "?" > "HOL.Ex"
">=" > "HOLLight.hollight.>="
">" > "HOLLight.hollight.>"
"==>" > "op -->"
@@ -243,7 +243,7 @@
"+" > "Groups.plus" :: "nat => nat => nat"
"*" > "Groups.times" :: "nat => nat => nat"
"$" > "HOLLight.hollight.$"
- "!" > "All"
+ "!" > "HOL.All"
const_renames
"ALL" > "ALL_list"
--- a/src/HOL/Import/hol4rews.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML Fri Aug 20 14:18:55 2010 +0200
@@ -616,7 +616,7 @@
fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x
| handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
| handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
- | handle_meta [x] = Appl[Constant "Trueprop",x]
+ | handle_meta [x] = Appl[Constant @{const_syntax Trueprop}, x]
| handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
in
val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]
@@ -624,12 +624,12 @@
local
fun initial_maps thy =
- thy |> add_hol4_type_mapping "min" "bool" false "bool"
+ thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
|> add_hol4_type_mapping "min" "fun" false "fun"
- |> add_hol4_type_mapping "min" "ind" false "Nat.ind"
- |> add_hol4_const_mapping "min" "=" false "op ="
- |> add_hol4_const_mapping "min" "==>" false "op -->"
- |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
+ |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
+ |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
+ |> add_hol4_const_mapping "min" "==>" false @{const_name "op -->"}
+ |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
in
val hol4_setup =
initial_maps #>
--- a/src/HOL/Import/proof_kernel.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Aug 20 14:18:55 2010 +0200
@@ -388,7 +388,6 @@
val type_of = Term.type_of
-val boolT = Type("bool",[])
val propT = Type("prop",[])
fun mk_defeq name rhs thy =
@@ -1007,7 +1006,7 @@
local
val th = thm "not_def"
val thy = theory_of_thm th
- val pp = Thm.reflexive (cterm_of thy (Const("Trueprop",boolT-->propT)))
+ val pp = Thm.reflexive (cterm_of thy (Const(@{const_name Trueprop},HOLogic.boolT-->propT)))
in
val not_elim_thm = Thm.combination pp th
end
@@ -1053,9 +1052,9 @@
val c = prop_of th3
val vname = fst(dest_Free v)
val (cold,cnew) = case c of
- tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) =>
+ tpc $ (Const(@{const_name All},allT) $ Abs(oldname,ty,body)) =>
(Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
- | tpc $ (Const("All",allT) $ rest) => (tpc,tpc)
+ | tpc $ (Const(@{const_name All},allT) $ rest) => (tpc,tpc)
| _ => raise ERR "mk_GEN" "Unknown conclusion"
val th4 = Thm.rename_boundvars cold cnew th3
val res = implies_intr_hyps th4
@@ -1205,7 +1204,8 @@
fun non_trivial_term_consts t = fold_aterms
(fn Const (c, _) =>
- if c = "Trueprop" orelse c = "All" orelse c = "op -->" orelse c = "op &" orelse c = "op ="
+ if c = @{const_name Trueprop} orelse c = @{const_name All}
+ orelse c = @{const_name "op -->"} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
then I else insert (op =) c
| _ => I) t [];
@@ -1213,12 +1213,12 @@
let
fun add_consts (Const (c, _), cs) =
(case c of
- "op =" => insert (op =) "==" cs
- | "op -->" => insert (op =) "==>" cs
- | "All" => cs
+ @{const_name "op ="} => insert (op =) "==" cs
+ | @{const_name "op -->"} => insert (op =) "==>" cs
+ | @{const_name All} => cs
| "all" => cs
- | "op &" => cs
- | "Trueprop" => cs
+ | @{const_name "op &"} => cs
+ | @{const_name Trueprop} => cs
| _ => insert (op =) c cs)
| add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
| add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
@@ -1476,10 +1476,10 @@
fun mk_COMB th1 th2 thy =
let
val (f,g) = case concl_of th1 of
- _ $ (Const("op =",_) $ f $ g) => (f,g)
+ _ $ (Const(@{const_name "op ="},_) $ f $ g) => (f,g)
| _ => raise ERR "mk_COMB" "First theorem not an equality"
val (x,y) = case concl_of th2 of
- _ $ (Const("op =",_) $ x $ y) => (x,y)
+ _ $ (Const(@{const_name "op ="},_) $ x $ y) => (x,y)
| _ => raise ERR "mk_COMB" "Second theorem not an equality"
val fty = type_of f
val (fd,fr) = dom_rng fty
@@ -1521,7 +1521,7 @@
val th1 = norm_hyps th1
val th2 = norm_hyps th2
val (l,r) = case concl_of th of
- _ $ (Const("op |",_) $ l $ r) => (l,r)
+ _ $ (Const(@{const_name "op |"},_) $ l $ r) => (l,r)
| _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
@@ -1654,7 +1654,7 @@
val cwit = cterm_of thy wit'
val cty = ctyp_of_term cwit
val a = case ex' of
- (Const("Ex",_) $ a) => a
+ (Const(@{const_name Ex},_) $ a) => a
| _ => raise ERR "EXISTS" "Argument not existential"
val ca = cterm_of thy a
val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
@@ -1687,7 +1687,7 @@
val c = HOLogic.dest_Trueprop (concl_of th2)
val cc = cterm_of thy c
val a = case concl_of th1 of
- _ $ (Const("Ex",_) $ a) => a
+ _ $ (Const(@{const_name Ex},_) $ a) => a
| _ => raise ERR "CHOOSE" "Conclusion not existential"
val ca = cterm_of (theory_of_thm th1) a
val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
@@ -1773,7 +1773,7 @@
val (info',tm') = disamb_term_from info tm
val th = norm_hyps th
val ct = cterm_of thy tm'
- val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th
+ val th1 = rearrange thy (HOLogic.mk_Trueprop (Const(@{const_name Not},HOLogic.boolT-->HOLogic.boolT) $ tm')) th
val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
val res = HOLThm(rens_of info',res1)
@@ -1788,7 +1788,7 @@
val cv = cterm_of thy v
val th1 = implies_elim_all (beta_eta_thm th)
val (f,g) = case concl_of th1 of
- _ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
+ _ $ (Const(@{const_name "op ="},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
| _ => raise ERR "mk_ABS" "Bad conclusion"
val (fd,fr) = dom_rng (type_of f)
val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
@@ -1860,7 +1860,7 @@
val _ = if_debug pth hth
val th1 = implies_elim_all (beta_eta_thm th)
val a = case concl_of th1 of
- _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
+ _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name False},_)) => a
| _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
val ca = cterm_of thy a
val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
@@ -1877,7 +1877,7 @@
val _ = if_debug pth hth
val th1 = implies_elim_all (beta_eta_thm th)
val a = case concl_of th1 of
- _ $ (Const("Not",_) $ a) => a
+ _ $ (Const(@{const_name Not},_) $ a) => a
| _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
val ca = cterm_of thy a
val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
@@ -1996,7 +1996,7 @@
("x",dT,body $ Bound 0)
end
handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
- fun dest_exists (Const("Ex",_) $ abody) =
+ fun dest_exists (Const(@{const_name Ex},_) $ abody) =
dest_eta_abs abody
| dest_exists tm =
raise ERR "new_specification" "Bad existential formula"
@@ -2082,7 +2082,7 @@
val (HOLThm(rens,td_th)) = norm_hthm thy hth
val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
val c = case concl_of th2 of
- _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
+ _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
| _ => raise ERR "new_type_definition" "Bad type definition theorem"
val tfrees = OldTerm.term_tfrees c
val tnames = map fst tfrees
@@ -2108,7 +2108,7 @@
val rew = rewrite_hol4_term (concl_of td_th) thy4
val th = Thm.equal_elim rew (Thm.transfer thy4 td_th)
val c = case HOLogic.dest_Trueprop (prop_of th) of
- Const("Ex",exT) $ P =>
+ Const(@{const_name Ex},exT) $ P =>
let
val PT = domain_type exT
in
@@ -2157,7 +2157,7 @@
SOME (cterm_of thy t)] light_nonempty
val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
val c = case concl_of th2 of
- _ $ (Const("Ex",_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
+ _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
| _ => raise ERR "type_introduction" "Bad type definition theorem"
val tfrees = OldTerm.term_tfrees c
val tnames = sort_strings (map fst tfrees)
--- a/src/HOL/Import/shuffler.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Fri Aug 20 14:18:55 2010 +0200
@@ -60,14 +60,14 @@
fun mk_meta_eq th =
(case concl_of th of
- Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
+ Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
| Const("==",_) $ _ $ _ => th
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make meta equality",0,[th]) (* FIXME avoid handle _ *)
fun mk_obj_eq th =
(case concl_of th of
- Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
+ Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
| Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make object equality",0,[th]) (* FIXME avoid handle _ *)
--- a/src/HOL/IsaMakefile Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/IsaMakefile Fri Aug 20 14:18:55 2010 +0200
@@ -213,7 +213,6 @@
Tools/sat_funcs.ML \
Tools/sat_solver.ML \
Tools/split_rule.ML \
- Tools/typedef_codegen.ML \
Tools/typedef.ML \
Transitive_Closure.thy \
Typedef.thy \
@@ -303,7 +302,6 @@
Tools/Predicate_Compile/predicate_compile_specialisation.ML \
Tools/Predicate_Compile/predicate_compile_pred.ML \
Tools/quickcheck_generators.ML \
- Tools/quickcheck_record.ML \
Tools/Qelim/cooper.ML \
Tools/Qelim/cooper_procedure.ML \
Tools/Qelim/qelim.ML \
@@ -343,7 +341,6 @@
Tools/string_code.ML \
Tools/string_syntax.ML \
Tools/transfer.ML \
- Tools/typecopy.ML \
Tools/TFL/casesplit.ML \
Tools/TFL/dcterm.ML \
Tools/TFL/post.ML \
--- a/src/HOL/Library/Eval_Witness.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Fri Aug 20 14:18:55 2010 +0200
@@ -63,7 +63,7 @@
else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
fun dest_exs 0 t = t
- | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) =
+ | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) =
Abs (v, check_type T, dest_exs (n - 1) b)
| dest_exs _ _ = sys_error "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
--- a/src/HOL/Library/positivstellensatz.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Fri Aug 20 14:18:55 2010 +0200
@@ -498,7 +498,7 @@
val strip_exists =
let fun h (acc, t) =
case (term_of t) of
- Const("Ex",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+ Const(@{const_name Ex},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
@@ -515,7 +515,7 @@
fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
fun choose v th th' = case concl_of th of
- @{term Trueprop} $ (Const("Ex",_)$_) =>
+ @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
let
val p = (funpow 2 Thm.dest_arg o cprop_of) th
val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
@@ -533,7 +533,7 @@
val strip_forall =
let fun h (acc, t) =
case (term_of t) of
- Const("All",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+ Const(@{const_name All},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
--- a/src/HOL/Library/reflection.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Library/reflection.ML Fri Aug 20 14:18:55 2010 +0200
@@ -82,7 +82,7 @@
fun rearrange congs =
let
fun P (_, th) =
- let val @{term "Trueprop"}$(Const ("op =",_) $l$_) = concl_of th
+ let val @{term "Trueprop"}$(Const (@{const_name "op ="},_) $l$_) = concl_of th
in can dest_Var l end
val (yes,no) = List.partition P congs
in no @ yes end
--- a/src/HOL/Matrix/Matrix.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Matrix/Matrix.thy Fri Aug 20 14:18:55 2010 +0200
@@ -528,12 +528,12 @@
show "f (s 0) (foldseq f (\<lambda>k. if k < m then s (Suc k) else foldseq f (\<lambda>k. s (Suc (k + m))) (na - m)) m) =
foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m"
apply (simp add: subd)
- apply (case_tac "m=0")
+ apply (cases "m = 0")
apply (simp)
apply (drule sube)
apply (auto)
apply (rule a)
- by (simp add: subc if_def)
+ by (simp add: subc cong del: if_cong)
qed
then show ?thesis using assms by simp
qed
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Aug 20 14:18:55 2010 +0200
@@ -174,9 +174,9 @@
Xcoord :: int
Ycoord :: int
-lemma "make_point_ext_type (dest_point_ext_type a) = a"
+lemma "Abs_point_ext (Rep_point_ext a) = a"
nitpick [expect = none]
-by (rule dest_point_ext_type_inverse)
+by (fact Rep_point_ext_inverse)
lemma "Fract a b = of_int a / of_int b"
nitpick [card = 1, expect = none]
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Aug 20 14:18:55 2010 +0200
@@ -183,7 +183,7 @@
end;
fun mk_not_sym ths = maps (fn th => case prop_of th of
- _ $ (Const ("Not", _) $ (Const ("op =", _) $ _ $ _)) => [th, th RS not_sym]
+ _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
| _ => [th]) ths;
fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
@@ -1372,7 +1372,7 @@
SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
_ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
simp_tac ind_ss1' i
- | _ $ (Const ("Not", _) $ _) =>
+ | _ $ (Const (@{const_name Not}, _) $ _) =>
resolve_tac freshs2' i
| _ => asm_simp_tac (HOL_basic_ss addsimps
pt2_atoms addsimprocs [perm_simproc]) i)) 1])
@@ -1671,7 +1671,7 @@
val rec_unique_frees' =
Datatype_Prop.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
val rec_unique_concls = map (fn ((x, U), R) =>
- Const ("Ex1", (U --> HOLogic.boolT) --> HOLogic.boolT) $
+ Const (@{const_name Ex1}, (U --> HOLogic.boolT) --> HOLogic.boolT) $
Abs ("y", U, R $ Free x $ Bound 0))
(rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
@@ -1777,7 +1777,7 @@
| _ => false) prems';
val fresh_prems = filter (fn th => case prop_of th of
_ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
- | _ $ (Const ("Not", _) $ _) => true
+ | _ $ (Const (@{const_name Not}, _) $ _) => true
| _ => false) prems';
val Ts = map fastype_of boundsl;
@@ -1879,7 +1879,7 @@
end) rec_prems2;
val ihs = filter (fn th => case prop_of th of
- _ $ (Const ("All", _) $ _) => true | _ => false) prems';
+ _ $ (Const (@{const_name All}, _) $ _) => true | _ => false) prems';
(** pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs **)
val _ = warning "step 7: pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs";
@@ -2022,7 +2022,7 @@
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
(Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
- Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
+ Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
--- a/src/HOL/Nominal/nominal_inductive.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Aug 20 14:18:55 2010 +0200
@@ -71,14 +71,14 @@
| add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
| add_binders thy i _ bs = bs;
-fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (f p q) else NONE
| _ => NONE)
| split_conj _ _ _ _ = NONE;
fun strip_all [] t = t
- | strip_all (_ :: xs) (Const ("All", _) $ Abs (s, T, t)) = strip_all xs t;
+ | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
(*********************************************************************)
(* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *)
@@ -89,7 +89,7 @@
(* where "id" protects the subformula from simplification *)
(*********************************************************************)
-fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
(case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (HOLogic.mk_conj (p,
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Aug 20 14:18:55 2010 +0200
@@ -75,14 +75,14 @@
| add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
| add_binders thy i _ bs = bs;
-fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
+fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (f p q) else NONE
| _ => NONE)
| split_conj _ _ _ _ = NONE;
fun strip_all [] t = t
- | strip_all (_ :: xs) (Const ("All", _) $ Abs (s, T, t)) = strip_all xs t;
+ | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
(*********************************************************************)
(* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *)
@@ -93,7 +93,7 @@
(* where "id" protects the subformula from simplification *)
(*********************************************************************)
-fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ =
+fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
(case head_of p of
Const (name, _) =>
if member (op =) names name then SOME (HOLogic.mk_conj (p,
--- a/src/HOL/Nominal/nominal_thmdecls.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Fri Aug 20 14:18:55 2010 +0200
@@ -135,7 +135,7 @@
val thy = Context.theory_of context
val thms_to_be_added = (case (prop_of orig_thm) of
(* case: eqvt-lemma is of the implicational form *)
- (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
+ (Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
let
val (pi,typi) = get_pi concl thy
in
@@ -147,7 +147,7 @@
else raise EQVT_FORM "Type Implication"
end
(* case: eqvt-lemma is of the equational form *)
- | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
+ | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $
(Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
(if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]
--- a/src/HOL/Prolog/prolog.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML Fri Aug 20 14:18:55 2010 +0200
@@ -10,17 +10,17 @@
exception not_HOHH;
fun isD t = case t of
- Const("Trueprop",_)$t => isD t
- | Const("op &" ,_)$l$r => isD l andalso isD r
- | Const("op -->",_)$l$r => isG l andalso isD r
+ Const(@{const_name Trueprop},_)$t => isD t
+ | Const(@{const_name "op &"} ,_)$l$r => isD l andalso isD r
+ | Const(@{const_name "op -->"},_)$l$r => isG l andalso isD r
| Const( "==>",_)$l$r => isG l andalso isD r
- | Const("All",_)$Abs(s,_,t) => isD t
+ | Const(@{const_name All},_)$Abs(s,_,t) => isD t
| Const("all",_)$Abs(s,_,t) => isD t
- | Const("op |",_)$_$_ => false
- | Const("Ex" ,_)$_ => false
- | Const("not",_)$_ => false
- | Const("True",_) => false
- | Const("False",_) => false
+ | Const(@{const_name "op |"},_)$_$_ => false
+ | Const(@{const_name Ex} ,_)$_ => false
+ | Const(@{const_name Not},_)$_ => false
+ | Const(@{const_name True},_) => false
+ | Const(@{const_name False},_) => false
| l $ r => isD l
| Const _ (* rigid atom *) => true
| Bound _ (* rigid atom *) => true
@@ -29,17 +29,17 @@
anything else *) => false
and
isG t = case t of
- Const("Trueprop",_)$t => isG t
- | Const("op &" ,_)$l$r => isG l andalso isG r
- | Const("op |" ,_)$l$r => isG l andalso isG r
- | Const("op -->",_)$l$r => isD l andalso isG r
+ Const(@{const_name Trueprop},_)$t => isG t
+ | Const(@{const_name "op &"} ,_)$l$r => isG l andalso isG r
+ | Const(@{const_name "op |"} ,_)$l$r => isG l andalso isG r
+ | Const(@{const_name "op -->"},_)$l$r => isD l andalso isG r
| Const( "==>",_)$l$r => isD l andalso isG r
- | Const("All",_)$Abs(_,_,t) => isG t
+ | Const(@{const_name All},_)$Abs(_,_,t) => isG t
| Const("all",_)$Abs(_,_,t) => isG t
- | Const("Ex" ,_)$Abs(_,_,t) => isG t
- | Const("True",_) => true
- | Const("not",_)$_ => false
- | Const("False",_) => false
+ | Const(@{const_name Ex} ,_)$Abs(_,_,t) => isG t
+ | Const(@{const_name True},_) => true
+ | Const(@{const_name Not},_)$_ => false
+ | Const(@{const_name False},_) => false
| _ (* atom *) => true;
val check_HOHH_tac1 = PRIMITIVE (fn thm =>
@@ -51,10 +51,10 @@
fun atomizeD ctxt thm = let
fun at thm = case concl_of thm of
- _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS
+ _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
(read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
- | _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
- | _$(Const("op -->",_)$_$_) => at(thm RS mp)
+ | _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ | _$(Const(@{const_name "op -->"},_)$_$_) => at(thm RS mp)
| _ => [thm]
in map zero_var_indexes (at thm) end;
@@ -71,15 +71,15 @@
resolve_tac (maps atomizeD prems) 1);
-- is nice, but cannot instantiate unknowns in the assumptions *)
fun hyp_resolve_tac i st = let
- fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
- | ap (Const("op -->",_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
+ fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
+ | ap (Const(@{const_name "op -->"},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
| ap t = (0,false,t);
(*
fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
| rep_goal (Const ("==>",_)$s$t) =
(case rep_goal t of (l,t) => (s::l,t))
| rep_goal t = ([] ,t);
- val (prems, Const("Trueprop", _)$concl) = rep_goal
+ val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
(#3(dest_state (st,i)));
*)
val subgoal = #3(Thm.dest_state (st,i));
--- a/src/HOL/Recdef.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Recdef.thy Fri Aug 20 14:18:55 2010 +0200
@@ -5,7 +5,7 @@
header {* TFL: recursive function definitions *}
theory Recdef
-imports FunDef Plain
+imports Plain Hilbert_Choice
uses
("Tools/TFL/casesplit.ML")
("Tools/TFL/utils.ML")
--- a/src/HOL/Record.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Record.thy Fri Aug 20 14:18:55 2010 +0200
@@ -10,7 +10,7 @@
theory Record
imports Plain Quickcheck
-uses ("Tools/typecopy.ML") ("Tools/record.ML") ("Tools/quickcheck_record.ML")
+uses ("Tools/record.ML")
begin
subsection {* Introduction *}
@@ -452,9 +452,7 @@
subsection {* Record package *}
-use "Tools/typecopy.ML" setup Typecopy.setup
use "Tools/record.ML" setup Record.setup
-use "Tools/quickcheck_record.ML" setup Quickcheck_Record.setup
hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
--- a/src/HOL/Statespace/distinct_tree_prover.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Fri Aug 20 14:18:55 2010 +0200
@@ -343,7 +343,7 @@
end handle Option => NONE)
fun distinctTree_tac names ctxt
- (Const ("Trueprop",_) $ (Const ("Not", _) $ (Const ("op =", _) $ x $ y)), i) =
+ (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
(case get_fst_success (neq_x_y ctxt x y) names of
SOME neq => rtac neq i
| NONE => no_tac)
@@ -356,7 +356,7 @@
fun distinct_simproc names =
Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
- (fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
+ (fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
case try Simplifier.the_context ss of
SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq])
(get_fst_success (neq_x_y ctxt x y) names)
--- a/src/HOL/Statespace/state_fun.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Fri Aug 20 14:18:55 2010 +0200
@@ -43,9 +43,9 @@
val conj_True = thm "conj_True";
val conj_cong = thm "conj_cong";
-fun isFalse (Const ("False",_)) = true
+fun isFalse (Const (@{const_name False},_)) = true
| isFalse _ = false;
-fun isTrue (Const ("True",_)) = true
+fun isTrue (Const (@{const_name True},_)) = true
| isTrue _ = false;
in
@@ -53,7 +53,7 @@
val lazy_conj_simproc =
Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"]
(fn thy => fn ss => fn t =>
- (case t of (Const ("op &",_)$P$Q) =>
+ (case t of (Const (@{const_name "op &"},_)$P$Q) =>
let
val P_P' = Simplifier.rewrite ss (cterm_of thy P);
val P' = P_P' |> prop_of |> Logic.dest_equals |> #2
@@ -285,7 +285,7 @@
then Bound 2
else raise TERM ("",[n]);
val sel' = lo $ d $ n' $ s;
- in (Const ("op =",Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
+ in (Const (@{const_name "op ="},Teq)$sel'$x',hd (binder_types Teq),nT,swap) end;
fun dest_state (s as Bound 0) = s
| dest_state (s as (Const (sel,sT)$Bound 0)) =
@@ -295,20 +295,20 @@
| dest_state s =
raise TERM ("StateFun.ex_lookup_eq_simproc: not a record slector",[s]);
- fun dest_sel_eq (Const ("op =",Teq)$
+ fun dest_sel_eq (Const (@{const_name "op ="},Teq)$
((lo as (Const ("StateFun.lookup",lT)))$d$n$s)$X) =
(false,Teq,lT,lo,d,n,X,dest_state s)
- | dest_sel_eq (Const ("op =",Teq)$X$
+ | dest_sel_eq (Const (@{const_name "op ="},Teq)$X$
((lo as (Const ("StateFun.lookup",lT)))$d$n$s)) =
(true,Teq,lT,lo,d,n,X,dest_state s)
| dest_sel_eq _ = raise TERM ("",[]);
in
(case t of
- (Const ("Ex",Tex)$Abs(s,T,t)) =>
+ (Const (@{const_name Ex},Tex)$Abs(s,T,t)) =>
(let val (eq,eT,nT,swap) = mkeq (dest_sel_eq t) 0;
val prop = list_all ([("n",nT),("x",eT)],
- Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq),
+ Logic.mk_equals (Const (@{const_name Ex},Tex)$Abs(s,T,eq),
HOLogic.true_const));
val thm = Drule.export_without_context (prove prop);
val thm' = if swap then swap_ex_eq OF [thm] else thm
@@ -367,7 +367,7 @@
val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
val (lookup_ss', ex_lookup_ss') =
(case (concl_of thm) of
- (_$((Const ("Ex",_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
+ (_$((Const (@{const_name Ex},_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
| _ => (lookup_ss addsimps [thm], ex_lookup_ss))
fun activate_simprocs ctxt =
if simprocs_active then ctxt
--- a/src/HOL/Statespace/state_space.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Fri Aug 20 14:18:55 2010 +0200
@@ -222,8 +222,8 @@
end handle Option => NONE)
fun distinctTree_tac ctxt
- (Const ("Trueprop",_) $
- (Const ("Not", _) $ (Const ("op =", _) $ (x as Free _)$ (y as Free _))), i) =
+ (Const (@{const_name Trueprop},_) $
+ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
(case (neq_x_y ctxt x y) of
SOME neq => rtac neq i
| NONE => no_tac)
@@ -236,7 +236,7 @@
val distinct_simproc =
Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
- (fn thy => fn ss => (fn (Const ("op =",_)$(x as Free _)$(y as Free _)) =>
+ (fn thy => fn ss => (fn (Const (@{const_name "op ="},_)$(x as Free _)$(y as Free _)) =>
(case try Simplifier.the_context ss of
SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
(neq_x_y ctxt x y)
--- a/src/HOL/TLA/Intensional.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/TLA/Intensional.thy Fri Aug 20 14:18:55 2010 +0200
@@ -279,7 +279,7 @@
fun hflatten t =
case (concl_of t) of
- Const _ $ (Const ("op -->", _) $ _ $ _) => hflatten (t RS mp)
+ Const _ $ (Const (@{const_name "op -->"}, _) $ _ $ _) => hflatten (t RS mp)
| _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
in
hflatten t
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Aug 20 14:18:55 2010 +0200
@@ -16,9 +16,9 @@
(* liberal addition of code data for datatypes *)
-fun mk_constr_consts thy vs dtco cos =
+fun mk_constr_consts thy vs tyco cos =
let
- val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
+ val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
in if is_some (try (Code.constrset_of_consts thy) cs')
then SOME cs
@@ -62,12 +62,12 @@
(* equality *)
-fun mk_eq_eqns thy dtco =
+fun mk_eq_eqns thy tyco =
let
- val (vs, cos) = Datatype_Data.the_spec thy dtco;
+ val (vs, cos) = Datatype_Data.the_spec thy tyco;
val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
- Datatype_Data.the_info thy dtco;
- val ty = Type (dtco, map TFree vs);
+ Datatype_Data.the_info thy tyco;
+ val ty = Type (tyco, map TFree vs);
fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
$ t1 $ t2;
fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
@@ -88,11 +88,11 @@
|> Simpdata.mk_eq;
in (map prove (triv_injects @ injects @ distincts), prove refl) end;
-fun add_equality vs dtcos thy =
+fun add_equality vs tycos thy =
let
- fun add_def dtco lthy =
+ fun add_def tyco lthy =
let
- val ty = Type (dtco, map TFree vs);
+ val ty = Type (tyco, map TFree vs);
fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
$ Free ("x", ty) $ Free ("y", ty);
val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -105,35 +105,37 @@
in (thm', lthy') end;
fun tac thms = Class.intro_classes_tac []
THEN ALLGOALS (ProofContext.fact_tac thms);
- fun prefix dtco = Binding.qualify true (Long_Name.base_name dtco) o Binding.qualify true "eq" o Binding.name;
- fun add_eq_thms dtco =
+ fun prefix tyco = Binding.qualify true (Long_Name.base_name tyco) o Binding.qualify true "eq" o Binding.name;
+ fun add_eq_thms tyco =
Theory.checkpoint
- #> `(fn thy => mk_eq_eqns thy dtco)
+ #> `(fn thy => mk_eq_eqns thy tyco)
#-> (fn (thms, thm) => PureThy.note_thmss Thm.lemmaK
- [((prefix dtco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
- ((prefix dtco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
+ [((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
+ ((prefix tyco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
#> snd
in
thy
- |> Class.instantiation (dtcos, vs, [HOLogic.class_eq])
- |> fold_map add_def dtcos
+ |> Class.instantiation (tycos, vs, [HOLogic.class_eq])
+ |> fold_map add_def tycos
|-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
(fn _ => fn def_thms => tac def_thms) def_thms)
|-> (fn def_thms => fold Code.del_eqn def_thms)
- |> fold add_eq_thms dtcos
+ |> fold add_eq_thms tycos
end;
(* register a datatype etc. *)
-fun add_all_code config dtcos thy =
+fun add_all_code config tycos thy =
let
- val (vs :: _, coss) = (split_list o map (Datatype_Data.the_spec thy)) dtcos;
- val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
+ val (vs :: _, coss) = (split_list o map (Datatype_Data.the_spec thy)) tycos;
+ val any_css = map2 (mk_constr_consts thy vs) tycos coss;
val css = if exists is_none any_css then []
else map_filter I any_css;
- val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) dtcos;
- val certs = map (mk_case_cert thy) dtcos;
+ val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) tycos;
+ val certs = map (mk_case_cert thy) tycos;
+ val tycos_eq = filter_out
+ (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_eq]) tycos;
in
if null css then thy
else thy
@@ -141,7 +143,7 @@
|> fold Code.add_datatype css
|> fold_rev Code.add_default_eqn case_rewrites
|> fold Code.add_case certs
- |> add_equality vs dtcos
+ |> not (null tycos_eq) ? add_equality vs tycos_eq
end;
--- a/src/HOL/Tools/Function/function_core.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Fri Aug 20 14:18:55 2010 +0200
@@ -392,7 +392,7 @@
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
val ihyp = Term.all domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
- HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
+ HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
|> cterm_of thy
--- a/src/HOL/Tools/Function/termination.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML Fri Aug 20 14:18:55 2010 +0200
@@ -148,8 +148,8 @@
val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
- val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
- = Term.strip_qnt_body "Ex" c
+ val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
+ = Term.strip_qnt_body @{const_name Ex} c
in cons r o cons l end
in
mk_skel (fold collect_pats cs [])
@@ -182,11 +182,11 @@
fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
val (sk, _, _, _, _) = D
- val vs = Term.strip_qnt_vars "Ex" c
+ val vs = Term.strip_qnt_vars @{const_name Ex} c
(* FIXME: throw error "dest_call" for malformed terms *)
- val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
- = Term.strip_qnt_body "Ex" c
+ val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
+ = Term.strip_qnt_body @{const_name Ex} c
val (p, l') = dest_inj sk l
val (q, r') = dest_inj sk r
in
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Aug 20 14:18:55 2010 +0200
@@ -147,7 +147,7 @@
fun Trueprop_conv cv ct =
case Thm.term_of ct of
- Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct
+ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
| _ => raise Fail "Trueprop_conv"
fun preprocess_intro thy rule =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Aug 20 14:18:55 2010 +0200
@@ -405,13 +405,13 @@
(* general syntactic functions *)
(*Like dest_conj, but flattens conjunctions however nested*)
-fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+fun conjuncts_aux (Const (@{const_name "op &"}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
| conjuncts_aux t conjs = t::conjs;
fun conjuncts t = conjuncts_aux t [];
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
- | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
+ | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
| is_equationlike_term _ = false
val is_equationlike = is_equationlike_term o prop_of
@@ -429,10 +429,7 @@
fun is_intro constname t = is_intro_term constname (prop_of t)
-fun is_pred thy constname =
- let
- val T = (Sign.the_const_type thy constname)
- in body_type T = @{typ "bool"} end;
+fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT);
fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = @{typ bool})
| is_predT _ = false
@@ -482,7 +479,7 @@
fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
-fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
+fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
let
val (xTs, t') = strip_ex t
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Aug 20 14:18:55 2010 +0200
@@ -524,7 +524,7 @@
fun dest_conjunct_prem th =
case HOLogic.dest_Trueprop (prop_of th) of
- (Const ("op &", _) $ t $ t') =>
+ (Const (@{const_name "op &"}, _) $ t $ t') =>
dest_conjunct_prem (th RS @{thm conjunct1})
@ dest_conjunct_prem (th RS @{thm conjunct2})
| _ => [th]
@@ -576,7 +576,7 @@
fun Trueprop_conv cv ct =
case Thm.term_of ct of
- Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct
+ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
| _ => raise Fail "Trueprop_conv"
fun preprocess_intro thy rule =
@@ -587,7 +587,7 @@
fun preprocess_elim ctxt elimrule =
let
- fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
+ fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
| replace_eqs t = t
val thy = ProofContext.theory_of ctxt
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Aug 20 14:18:55 2010 +0200
@@ -111,7 +111,7 @@
fun mk_meta_equation th =
case prop_of th of
- Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
| _ => th
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
@@ -215,12 +215,12 @@
val logic_operator_names =
[@{const_name "=="},
@{const_name "==>"},
- @{const_name "Trueprop"},
- @{const_name "Not"},
+ @{const_name Trueprop},
+ @{const_name Not},
@{const_name "op ="},
@{const_name "op -->"},
- @{const_name "All"},
- @{const_name "Ex"},
+ @{const_name All},
+ @{const_name Ex},
@{const_name "op &"},
@{const_name "op |"}]
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Aug 20 14:18:55 2010 +0200
@@ -52,7 +52,7 @@
fun transform_ho_typ (T as Type ("fun", _)) =
let
val (Ts, T') = strip_type T
- in if T' = @{typ "bool"} then T else (Ts @ [T']) ---> HOLogic.boolT end
+ in if T' = HOLogic.boolT then T else (Ts @ [T']) ---> HOLogic.boolT end
| transform_ho_typ t = t
fun transform_ho_arg arg =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Aug 20 14:18:55 2010 +0200
@@ -86,11 +86,11 @@
map instantiate rew_ths
end
-fun is_compound ((Const ("Not", _)) $ t) =
+fun is_compound ((Const (@{const_name Not}, _)) $ t) =
error "is_compound: Negation should not occur; preprocessing is defect"
- | is_compound ((Const ("Ex", _)) $ _) = true
+ | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
| is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
- | is_compound ((Const ("op &", _)) $ _ $ _) =
+ | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
error "is_compound: Conjunction should not occur; preprocessing is defect"
| is_compound _ = false
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Aug 20 14:18:55 2010 +0200
@@ -168,10 +168,10 @@
mk_split_lambda' xs t
end;
-fun strip_imp_prems (Const("op -->", _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
| strip_imp_prems _ = [];
-fun strip_imp_concl (Const("op -->", _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
| strip_imp_concl A = A : term;
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Aug 20 14:18:55 2010 +0200
@@ -120,10 +120,10 @@
fun whatis x ct =
( case (term_of ct) of
- Const("op &",_)$_$_ => And (Thm.dest_binop ct)
-| Const ("op |",_)$_$_ => Or (Thm.dest_binop ct)
-| Const ("op =",_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
-| Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
+ Const(@{const_name "op &"},_)$_$_ => And (Thm.dest_binop ct)
+| Const (@{const_name "op |"},_)$_$_ => Or (Thm.dest_binop ct)
+| Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
+| Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
| Const (@{const_name Orderings.less}, _) $ y$ z =>
if term_of x aconv y then Lt (Thm.dest_arg ct)
@@ -274,7 +274,7 @@
| lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
| lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
- | lin (vs as x::_) ((b as Const("op =",_))$s$t) =
+ | lin (vs as x::_) ((b as Const(@{const_name "op ="},_))$s$t) =
(case lint vs (subC$t$s) of
(t as a$(m$c$y)$r) =>
if x <> y then b$zero$t
@@ -353,8 +353,8 @@
then (ins (dest_number c) acc, dacc) else (acc,dacc)
| Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
- | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
- | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+ | Const(@{const_name "op &"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
+ | Const(@{const_name "op |"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
| Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
| _ => (acc, dacc)
val (cs,ds) = h ([],[]) p
@@ -382,8 +382,8 @@
end
fun unit_conv t =
case (term_of t) of
- Const("op &",_)$_$_ => Conv.binop_conv unit_conv t
- | Const("op |",_)$_$_ => Conv.binop_conv unit_conv t
+ Const(@{const_name "op &"},_)$_$_ => Conv.binop_conv unit_conv t
+ | Const(@{const_name "op |"},_)$_$_ => Conv.binop_conv unit_conv t
| Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
| Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
@@ -612,19 +612,19 @@
fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
| fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
- | fm_of_term ps vs (Const ("op &", _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name "op &"}, _) $ t1 $ t2) =
Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (Const ("op |", _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
- | fm_of_term ps vs (Const ("op -->", _) $ t1 $ t2) =
+ | fm_of_term ps vs (Const (@{const_name "op -->"}, _) $ t1 $ t2) =
Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (Const (@{const_name Not}, _) $ t') =
Proc.Not (fm_of_term ps vs t')
- | fm_of_term ps vs (Const ("Ex", _) $ Abs abs) =
+ | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs abs) =
Proc.E (uncurry (fm_of_term ps) (descend vs abs))
- | fm_of_term ps vs (Const ("All", _) $ Abs abs) =
+ | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs abs) =
Proc.A (uncurry (fm_of_term ps) (descend vs abs))
| fm_of_term ps vs (@{term "op = :: int => _"} $ t1 $ t2) =
Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
@@ -687,14 +687,14 @@
fun strip_objimp ct =
(case Thm.term_of ct of
- Const ("op -->", _) $ _ $ _ =>
+ Const (@{const_name "op -->"}, _) $ _ $ _ =>
let val (A, B) = Thm.dest_binop ct
in A :: strip_objimp B end
| _ => [ct]);
fun strip_objall ct =
case term_of ct of
- Const ("All", _) $ Abs (xn,xT,p) =>
+ Const (@{const_name All}, _) $ Abs (xn,xT,p) =>
let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
in apfst (cons (a,v)) (strip_objall t')
end
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Aug 20 14:18:55 2010 +0200
@@ -490,16 +490,16 @@
else mk_bex1_rel $ resrel $ subtrm
end
- | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+ | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
in
- if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
+ if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
| (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
- Const (@{const_name "All"}, ty') $ t') =>
+ Const (@{const_name All}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
@@ -510,7 +510,7 @@
end
| (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
- Const (@{const_name "Ex"}, ty') $ t') =>
+ Const (@{const_name Ex}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
@@ -520,7 +520,7 @@
else mk_bex $ (mk_resp $ resrel) $ subtrm
end
- | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+ | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
@@ -638,10 +638,10 @@
as the type of subterms needs to be calculated *)
fun inj_repabs_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
- (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
+ (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
- | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+ | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
| (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Aug 20 14:18:55 2010 +0200
@@ -313,7 +313,7 @@
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
- Const ("op =", HOLogic.typeT)
+ Const (@{const_name "op ="}, HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
(case strip_prefix_and_undo_ascii const_prefix x of
SOME c => Const (smart_invert_const c, dummyT)
--- a/src/HOL/Tools/TFL/dcterm.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML Fri Aug 20 14:18:55 2010 +0200
@@ -24,18 +24,15 @@
val dest_exists: cterm -> cterm * cterm
val dest_forall: cterm -> cterm * cterm
val dest_imp: cterm -> cterm * cterm
- val dest_let: cterm -> cterm * cterm
val dest_neg: cterm -> cterm
val dest_pair: cterm -> cterm * cterm
val dest_var: cterm -> {Name:string, Ty:typ}
val is_conj: cterm -> bool
- val is_cons: cterm -> bool
val is_disj: cterm -> bool
val is_eq: cterm -> bool
val is_exists: cterm -> bool
val is_forall: cterm -> bool
val is_imp: cterm -> bool
- val is_let: cterm -> bool
val is_neg: cterm -> bool
val is_pair: cterm -> bool
val list_mk_disj: cterm list -> cterm
@@ -78,15 +75,15 @@
fun mk_exists (r as (Bvar, Body)) =
let val ty = #T(rep_cterm Bvar)
- val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
+ val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
in capply c (uncurry cabs r) end;
-local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name "op &"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
end;
-local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name "op |"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
end;
@@ -128,17 +125,15 @@
handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
-val dest_neg = dest_monop "not"
-val dest_pair = dest_binop @{const_name Pair};
-val dest_eq = dest_binop "op ="
-val dest_imp = dest_binop "op -->"
-val dest_conj = dest_binop "op &"
-val dest_disj = dest_binop "op |"
-val dest_cons = dest_binop "Cons"
-val dest_let = Library.swap o dest_binop "Let";
-val dest_select = dest_binder "Hilbert_Choice.Eps"
-val dest_exists = dest_binder "Ex"
-val dest_forall = dest_binder "All"
+val dest_neg = dest_monop @{const_name Not}
+val dest_pair = dest_binop @{const_name Pair}
+val dest_eq = dest_binop @{const_name "op ="}
+val dest_imp = dest_binop @{const_name "op -->"}
+val dest_conj = dest_binop @{const_name "op &"}
+val dest_disj = dest_binop @{const_name "op |"}
+val dest_select = dest_binder @{const_name Eps}
+val dest_exists = dest_binder @{const_name Ex}
+val dest_forall = dest_binder @{const_name All}
(* Query routines *)
@@ -151,8 +146,6 @@
val is_conj = can dest_conj
val is_disj = can dest_disj
val is_pair = can dest_pair
-val is_let = can dest_let
-val is_cons = can dest_cons
(*---------------------------------------------------------------------------
@@ -197,7 +190,7 @@
handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
| TERM (msg, _) => raise ERR "mk_prop" msg;
-fun drop_prop ctm = dest_monop "Trueprop" ctm handle U.ERR _ => ctm;
+fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle U.ERR _ => ctm;
end;
--- a/src/HOL/Tools/TFL/post.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/TFL/post.ML Fri Aug 20 14:18:55 2010 +0200
@@ -67,7 +67,7 @@
val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
fun mk_meta_eq r = case concl_of r of
Const("==",_)$_$_ => r
- | _ $(Const("op =",_)$_$_) => r RS eq_reflection
+ | _ $(Const(@{const_name "op ="},_)$_$_) => r RS eq_reflection
| _ => r RS P_imp_P_eq_True
(*Is this the best way to invoke the simplifier??*)
--- a/src/HOL/Tools/TFL/rules.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Fri Aug 20 14:18:55 2010 +0200
@@ -453,14 +453,14 @@
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
fun is_cong thm =
case (Thm.prop_of thm)
- of (Const("==>",_)$(Const("Trueprop",_)$ _) $
+ of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
(Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
| _ => true;
fun dest_equal(Const ("==",_) $
- (Const ("Trueprop",_) $ lhs)
- $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
+ (Const (@{const_name Trueprop},_) $ lhs)
+ $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
| dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
| dest_equal tm = S.dest_eq tm;
@@ -759,7 +759,7 @@
val cntxt = rev(Simplifier.prems_of_ss ss)
val dummy = print_thms "cntxt:" cntxt
val thy = Thm.theory_of_thm thm
- val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
+ val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
fun genl tm = let val vlist = subtract (op aconv) globals
(OldTerm.add_term_frees(tm,[]))
in fold_rev Forall vlist tm
--- a/src/HOL/Tools/TFL/tfl.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Fri Aug 20 14:18:55 2010 +0200
@@ -483,7 +483,7 @@
val (case_rewrites,context_congs) = extraction_thms thy
val tych = Thry.typecheck thy
val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
- val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
+ val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
Rtype)
val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
--- a/src/HOL/Tools/TFL/usyntax.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Fri Aug 20 14:18:55 2010 +0200
@@ -159,36 +159,36 @@
fun mk_imp{ant,conseq} =
- let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name "op -->"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[ant,conseq])
end;
fun mk_select (r as {Bvar,Body}) =
let val ty = type_of Bvar
- val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty)
+ val c = Const(@{const_name Eps},(ty --> HOLogic.boolT) --> ty)
in list_comb(c,[mk_abs r])
end;
fun mk_forall (r as {Bvar,Body}) =
let val ty = type_of Bvar
- val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT)
+ val c = Const(@{const_name All},(ty --> HOLogic.boolT) --> HOLogic.boolT)
in list_comb(c,[mk_abs r])
end;
fun mk_exists (r as {Bvar,Body}) =
let val ty = type_of Bvar
- val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT)
+ val c = Const(@{const_name Ex},(ty --> HOLogic.boolT) --> HOLogic.boolT)
in list_comb(c,[mk_abs r])
end;
fun mk_conj{conj1,conj2} =
- let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name "op &"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[conj1,conj2])
end;
fun mk_disj{disj1,disj2} =
- let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+ let val c = Const(@{const_name "op |"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[disj1,disj2])
end;
@@ -244,25 +244,25 @@
end
| dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction";
-fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
+fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
| dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
-fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
+fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
| dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
-fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a)
+fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
| dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
-fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a)
+fun dest_exists(Const(@{const_name Ex},_) $ (a as Abs _)) = fst (dest_abs [] a)
| dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
-fun dest_neg(Const("not",_) $ M) = M
+fun dest_neg(Const(@{const_name Not},_) $ M) = M
| dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
-fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
+fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
| dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
-fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
+fun dest_disj(Const(@{const_name "op |"},_) $ M $ N) = {disj1=M, disj2=N}
| dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
fun mk_pair{fst,snd} =
@@ -402,6 +402,6 @@
| is_WFR _ = false;
fun ARB ty = mk_select{Bvar=Free("v",ty),
- Body=Const("True",HOLogic.boolT)};
+ Body=Const(@{const_name True},HOLogic.boolT)};
end;
--- a/src/HOL/Tools/choice_specification.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Fri Aug 20 14:18:55 2010 +0200
@@ -24,7 +24,7 @@
fun mk_definitional [] arg = arg
| mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
case HOLogic.dest_Trueprop (concl_of thm) of
- Const("Ex",_) $ P =>
+ Const(@{const_name Ex},_) $ P =>
let
val ctype = domain_type (type_of P)
val cname_full = Sign.intern_const thy cname
@@ -51,7 +51,7 @@
end
| process ((thname,cname,covld)::cos) (thy,tm) =
case tm of
- Const("Ex",_) $ P =>
+ Const(@{const_name Ex},_) $ P =>
let
val ctype = domain_type (type_of P)
val cname_full = Sign.intern_const thy cname
--- a/src/HOL/Tools/cnf_funcs.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Fri Aug 20 14:18:55 2010 +0200
@@ -93,19 +93,19 @@
val cnftac_eq_imp = @{lemma "[| P = Q; P |] ==> Q" by auto};
-fun is_atom (Const ("False", _)) = false
- | is_atom (Const ("True", _)) = false
- | is_atom (Const ("op &", _) $ _ $ _) = false
- | is_atom (Const ("op |", _) $ _ $ _) = false
- | is_atom (Const ("op -->", _) $ _ $ _) = false
- | is_atom (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
- | is_atom (Const ("Not", _) $ _) = false
+fun is_atom (Const (@{const_name False}, _)) = false
+ | is_atom (Const (@{const_name True}, _)) = false
+ | is_atom (Const (@{const_name "op &"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name "op |"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
+ | is_atom (Const (@{const_name Not}, _) $ _) = false
| is_atom _ = true;
-fun is_literal (Const ("Not", _) $ x) = is_atom x
+fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
| is_literal x = is_atom x;
-fun is_clause (Const ("op |", _) $ x $ y) = is_clause x andalso is_clause y
+fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
| is_clause x = is_literal x;
(* ------------------------------------------------------------------------- *)
@@ -118,7 +118,7 @@
fun clause_is_trivial c =
let
(* Term.term -> Term.term *)
- fun dual (Const ("Not", _) $ x) = x
+ fun dual (Const (@{const_name Not}, _) $ x) = x
| dual x = HOLogic.Not $ x
(* Term.term list -> bool *)
fun has_duals [] = false
@@ -184,28 +184,28 @@
(* Theory.theory -> Term.term -> Thm.thm *)
-fun make_nnf_thm thy (Const ("op &", _) $ x $ y) =
+fun make_nnf_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy y
in
conj_cong OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("op |", _) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy y
in
disj_cong OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("op -->", _) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name "op -->"}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy y
in
make_nnf_imp OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -214,32 +214,32 @@
in
make_nnf_iff OF [thm1, thm2, thm3, thm4]
end
- | make_nnf_thm thy (Const ("Not", _) $ Const ("False", _)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
make_nnf_not_false
- | make_nnf_thm thy (Const ("Not", _) $ Const ("True", _)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
make_nnf_not_true
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op &", _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_conj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op |", _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_disj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op -->", _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_imp OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -248,7 +248,7 @@
in
make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("Not", _) $ x)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) =
let
val thm1 = make_nnf_thm thy x
in
@@ -276,7 +276,7 @@
(* Theory.theory -> Term.term -> Thm.thm *)
-fun simp_True_False_thm thy (Const ("op &", _) $ x $ y) =
+fun simp_True_False_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
let
val thm1 = simp_True_False_thm thy x
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -298,7 +298,7 @@
conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *)
end
end
- | simp_True_False_thm thy (Const ("op |", _) $ x $ y) =
+ | simp_True_False_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
let
val thm1 = simp_True_False_thm thy x
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -334,24 +334,24 @@
fun make_cnf_thm thy t =
let
(* Term.term -> Thm.thm *)
- fun make_cnf_thm_from_nnf (Const ("op &", _) $ x $ y) =
+ fun make_cnf_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) =
let
val thm1 = make_cnf_thm_from_nnf x
val thm2 = make_cnf_thm_from_nnf y
in
conj_cong OF [thm1, thm2]
end
- | make_cnf_thm_from_nnf (Const ("op |", _) $ x $ y) =
+ | make_cnf_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
let
(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
- fun make_cnf_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
+ fun make_cnf_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
let
val thm1 = make_cnf_disj_thm x1 y'
val thm2 = make_cnf_disj_thm x2 y'
in
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
end
- | make_cnf_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
+ | make_cnf_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
let
val thm1 = make_cnf_disj_thm x' y1
val thm2 = make_cnf_disj_thm x' y2
@@ -403,34 +403,34 @@
val var_id = Unsynchronized.ref 0 (* properly initialized below *)
fun new_free () =
Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
- fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) : thm =
+ fun make_cnfx_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) : thm =
let
val thm1 = make_cnfx_thm_from_nnf x
val thm2 = make_cnfx_thm_from_nnf y
in
conj_cong OF [thm1, thm2]
end
- | make_cnfx_thm_from_nnf (Const ("op |", _) $ x $ y) =
+ | make_cnfx_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
if is_clause x andalso is_clause y then
inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
else if is_literal y orelse is_literal x then let
(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
(* almost in CNF, and x' or y' is a literal *)
- fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
+ fun make_cnfx_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
let
val thm1 = make_cnfx_disj_thm x1 y'
val thm2 = make_cnfx_disj_thm x2 y'
in
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
end
- | make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
+ | make_cnfx_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
let
val thm1 = make_cnfx_disj_thm x' y1
val thm2 = make_cnfx_disj_thm x' y2
in
make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
end
- | make_cnfx_disj_thm (Const ("Ex", _) $ x') y' =
+ | make_cnfx_disj_thm (Const (@{const_name Ex}, _) $ x') y' =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *)
val var = new_free ()
@@ -441,7 +441,7 @@
in
iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
end
- | make_cnfx_disj_thm x' (Const ("Ex", _) $ y') =
+ | make_cnfx_disj_thm x' (Const (@{const_name Ex}, _) $ y') =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *)
val var = new_free ()
--- a/src/HOL/Tools/groebner.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/groebner.ML Fri Aug 20 14:18:55 2010 +0200
@@ -395,7 +395,7 @@
fun refute_disj rfn tm =
case term_of tm of
- Const("op |",_)$l$r =>
+ Const(@{const_name "op |"},_)$l$r =>
compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
| _ => rfn tm ;
@@ -405,11 +405,11 @@
val mk_comb = capply;
fun is_neg t =
case term_of t of
- (Const("Not",_)$p) => true
+ (Const(@{const_name Not},_)$p) => true
| _ => false;
fun is_eq t =
case term_of t of
- (Const("op =",_)$_$_) => true
+ (Const(@{const_name "op ="},_)$_$_) => true
| _ => false;
fun end_itlist f l =
@@ -430,14 +430,14 @@
val strip_exists =
let fun h (acc, t) =
case (term_of t) of
- Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
+ Const(@{const_name Ex},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end;
fun is_forall t =
case term_of t of
- (Const("All",_)$Abs(_,_,_)) => true
+ (Const(@{const_name All},_)$Abs(_,_,_)) => true
| _ => false;
val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
@@ -522,7 +522,7 @@
fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
fun choose v th th' = case concl_of th of
- @{term Trueprop} $ (Const("Ex",_)$_) =>
+ @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
let
val p = (funpow 2 Thm.dest_arg o cprop_of) th
val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
@@ -923,15 +923,15 @@
fun find_term bounds tm =
(case term_of tm of
- Const ("op =", T) $ _ $ _ =>
+ Const (@{const_name "op ="}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else dest_arg tm
- | Const ("Not", _) $ _ => find_term bounds (dest_arg tm)
- | Const ("All", _) $ _ => find_body bounds (dest_arg tm)
- | Const ("Ex", _) $ _ => find_body bounds (dest_arg tm)
- | Const ("op &", _) $ _ $ _ => find_args bounds tm
- | Const ("op |", _) $ _ $ _ => find_args bounds tm
- | Const ("op -->", _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
+ | Const (@{const_name All}, _) $ _ => find_body bounds (dest_arg tm)
+ | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
+ | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
| @{term "op ==>"} $_$_ => find_args bounds tm
| Const("op ==",_)$_$_ => find_args bounds tm
| @{term Trueprop}$_ => find_term bounds (dest_arg tm)
@@ -985,7 +985,7 @@
local
fun lhs t = case term_of t of
- Const("op =",_)$_$_ => Thm.dest_arg1 t
+ Const(@{const_name "op ="},_)$_$_ => Thm.dest_arg1 t
| _=> raise CTERM ("ideal_tac - lhs",[t])
fun exitac NONE = no_tac
| exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
--- a/src/HOL/Tools/hologic.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Fri Aug 20 14:18:55 2010 +0200
@@ -143,15 +143,15 @@
(* bool and set *)
-val boolN = "bool";
+val boolN = "HOL.bool";
val boolT = Type (boolN, []);
-val true_const = Const ("True", boolT);
-val false_const = Const ("False", boolT);
+val true_const = Const ("HOL.True", boolT);
+val false_const = Const ("HOL.False", boolT);
fun mk_setT T = T --> boolT;
-fun dest_setT (Type ("fun", [T, Type ("bool", [])])) = T
+fun dest_setT (Type ("fun", [T, Type ("HOL.bool", [])])) = T
| dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
fun mk_set T ts =
@@ -181,11 +181,11 @@
(* logic *)
-val Trueprop = Const ("Trueprop", boolT --> propT);
+val Trueprop = Const ("HOL.Trueprop", boolT --> propT);
fun mk_Trueprop P = Trueprop $ P;
-fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
+fun dest_Trueprop (Const ("HOL.Trueprop", _) $ P) = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
fun conj_intr thP thQ =
@@ -230,23 +230,23 @@
fun disjuncts t = disjuncts_aux t [];
-fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
+fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
| dest_imp t = raise TERM ("dest_imp", [t]);
-fun dest_not (Const ("Not", _) $ t) = t
+fun dest_not (Const ("HOL.Not", _) $ t) = t
| dest_not t = raise TERM ("dest_not", [t]);
-fun eq_const T = Const ("op =", [T, T] ---> boolT);
+fun eq_const T = Const ("op =", T --> T --> boolT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
| dest_eq t = raise TERM ("dest_eq", [t])
-fun all_const T = Const ("All", [T --> boolT] ---> boolT);
+fun all_const T = Const ("HOL.All", [T --> boolT] ---> boolT);
fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
-fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
+fun exists_const T = Const ("HOL.Ex", [T --> boolT] ---> boolT);
fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
@@ -657,7 +657,9 @@
$ t $ t', U)
in fold_rev mk_clause clauses (t, U) |> fst end;
-val code_numeralT = Type ("Code_Numeral.code_numeral", []);
+
+(* random seeds *)
+
val random_seedT = mk_prodT (code_numeralT, code_numeralT);
fun mk_random T t = Const ("Quickcheck.random_class.random", code_numeralT
--- a/src/HOL/Tools/lin_arith.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Aug 20 14:18:55 2010 +0200
@@ -46,12 +46,12 @@
val mk_Trueprop = HOLogic.mk_Trueprop;
fun atomize thm = case Thm.prop_of thm of
- Const ("Trueprop", _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
| _ => [thm];
-fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
- | neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
+fun neg_prop ((TP as Const(@{const_name Trueprop}, _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
+ | neg_prop ((TP as Const(@{const_name Trueprop}, _)) $ t) = TP $ (HOLogic.Not $t)
| neg_prop t = raise TERM ("neg_prop", [t]);
fun is_False thm =
@@ -258,10 +258,10 @@
| negate NONE = NONE;
fun decomp_negation data
- ((Const ("Trueprop", _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
+ ((Const (@{const_name Trueprop}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
decomp_typecheck data (T, (rel, lhs, rhs))
- | decomp_negation data ((Const ("Trueprop", _)) $
- (Const ("Not", _) $ (Const (rel, T) $ lhs $ rhs))) =
+ | decomp_negation data ((Const (@{const_name Trueprop}, _)) $
+ (Const (@{const_name Not}, _) $ (Const (rel, T) $ lhs $ rhs))) =
negate (decomp_typecheck data (T, (rel, lhs, rhs)))
| decomp_negation data _ =
NONE;
@@ -273,7 +273,7 @@
in decomp_negation (thy, discrete, inj_consts) end;
fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T
- | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
+ | domain_is_nat (_ $ (Const (@{const_name Not}, _) $ (Const (_, T) $ _ $ _))) = nT T
| domain_is_nat _ = false;
@@ -428,7 +428,7 @@
val t2' = incr_boundvars 1 t2
val t1_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
- val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_plus_d = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus},
split_type --> split_type --> split_type) $ t2' $ d)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -448,7 +448,7 @@
(map (incr_boundvars 1) rev_terms)
val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms
val t1' = incr_boundvars 1 t1
- val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
+ val t1_eq_nat_n = Const (@{const_name "op ="}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
(Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
val t1_lt_zero = Const (@{const_name Orderings.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
@@ -472,13 +472,13 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const ("op =",
+ val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -504,13 +504,13 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const ("op =",
+ val t2_neq_zero = HOLogic.mk_not (Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
val j_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -542,7 +542,7 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -556,7 +556,7 @@
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -596,7 +596,7 @@
(map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =",
+ val t2_eq_zero = Const (@{const_name "op ="},
split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
val zero_lt_t2 = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
@@ -610,7 +610,7 @@
split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t2_lt_j = Const (@{const_name Orderings.less},
split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ val t1_eq_t2_times_i_plus_j = Const (@{const_name "op ="}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
@@ -659,7 +659,7 @@
fun negated_term_occurs_positively (terms : term list) : bool =
List.exists
- (fn (Trueprop $ (Const ("Not", _) $ t)) =>
+ (fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
member Pattern.aeconv terms (Trueprop $ t)
| _ => false)
terms;
--- a/src/HOL/Tools/meson.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Aug 20 14:18:55 2010 +0200
@@ -149,21 +149,21 @@
(*Are any of the logical connectives in "bs" present in the term?*)
fun has_conns bs =
let fun has (Const(a,_)) = false
- | has (Const("Trueprop",_) $ p) = has p
- | has (Const("Not",_) $ p) = has p
- | has (Const("op |",_) $ p $ q) = member (op =) bs "op |" orelse has p orelse has q
- | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q
- | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p
- | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p
+ | has (Const(@{const_name Trueprop},_) $ p) = has p
+ | has (Const(@{const_name Not},_) $ p) = has p
+ | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs @{const_name "op |"} orelse has p orelse has q
+ | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs @{const_name "op &"} orelse has p orelse has q
+ | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
+ | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
| has _ = false
in has end;
(**** Clause handling ****)
-fun literals (Const("Trueprop",_) $ P) = literals P
- | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
- | literals (Const("Not",_) $ P) = [(false,P)]
+fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
+ | literals (Const(@{const_name "op |"},_) $ P $ Q) = literals P @ literals Q
+ | literals (Const(@{const_name Not},_) $ P) = [(false,P)]
| literals P = [(true,P)];
(*number of literals in a term*)
@@ -172,16 +172,16 @@
(*** Tautology Checking ***)
-fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) =
+fun signed_lits_aux (Const (@{const_name "op |"}, _) $ P $ Q) (poslits, neglits) =
signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
- | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits)
+ | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
| signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
(*Literals like X=X are tautologous*)
-fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u
- | taut_poslit (Const("True",_)) = true
+fun taut_poslit (Const(@{const_name "op ="},_) $ t $ u) = t aconv u
+ | taut_poslit (Const(@{const_name True},_)) = true
| taut_poslit _ = false;
fun is_taut th =
@@ -208,18 +208,18 @@
fun refl_clause_aux 0 th = th
| refl_clause_aux n th =
case HOLogic.dest_Trueprop (concl_of th) of
- (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) =>
+ (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
- | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) =>
+ | (Const (@{const_name "op |"}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
if eliminable(t,u)
then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
- | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
+ | (Const (@{const_name "op |"}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
| _ => (*not a disjunction*) th;
-fun notequal_lits_count (Const ("op |", _) $ P $ Q) =
+fun notequal_lits_count (Const (@{const_name "op |"}, _) $ P $ Q) =
notequal_lits_count P + notequal_lits_count Q
- | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1
+ | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
| notequal_lits_count _ = 0;
(*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -266,26 +266,26 @@
fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
(*Estimate the number of clauses in order to detect infeasible theorems*)
- fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
- | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
- | signed_nclauses b (Const("op &",_) $ t $ u) =
+ fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
+ | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t
+ | signed_nclauses b (Const(@{const_name "op &"},_) $ t $ u) =
if b then sum (signed_nclauses b t) (signed_nclauses b u)
else prod (signed_nclauses b t) (signed_nclauses b u)
- | signed_nclauses b (Const("op |",_) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
if b then prod (signed_nclauses b t) (signed_nclauses b u)
else sum (signed_nclauses b t) (signed_nclauses b u)
- | signed_nclauses b (Const("op -->",_) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name "op -->"},_) $ t $ u) =
if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
else sum (signed_nclauses (not b) t) (signed_nclauses b u)
- | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
+ | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
(prod (signed_nclauses (not b) u) (signed_nclauses b t))
else sum (prod (signed_nclauses b t) (signed_nclauses b u))
(prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
else 1
- | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
- | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
+ | signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t
+ | signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t
| signed_nclauses _ _ = 1; (* literal *)
in
signed_nclauses true t >= max_cl
@@ -296,7 +296,7 @@
local
val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
val spec_varT = #T (Thm.rep_cterm spec_var);
- fun name_of (Const ("All", _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
+ fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
in
fun freeze_spec th ctxt =
let
@@ -314,8 +314,7 @@
(*Any need to extend this list with
"HOL.type_class","HOL.eq_class","Pure.term"?*)
-val has_meta_conn =
- exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
+val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
fun apply_skolem_theorem (th, rls) =
let
@@ -331,18 +330,18 @@
let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
- else if not (has_conns ["All","Ex","op &"] (prop_of th))
+ else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name "op &"}] (prop_of th))
then nodups ctxt th :: ths (*no work to do, terminate*)
else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
- Const ("op &", _) => (*conjunction*)
+ Const (@{const_name "op &"}, _) => (*conjunction*)
cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
- | Const ("All", _) => (*universal quantifier*)
+ | Const (@{const_name All}, _) => (*universal quantifier*)
let val (th',ctxt') = freeze_spec th (!ctxtr)
in ctxtr := ctxt'; cnf_aux (th', ths) end
- | Const ("Ex", _) =>
+ | Const (@{const_name Ex}, _) =>
(*existential quantifier: Insert Skolem functions*)
cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
- | Const ("op |", _) =>
+ | Const (@{const_name "op |"}, _) =>
(*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
all combinations of converting P, Q to CNF.*)
let val tac =
@@ -365,8 +364,8 @@
(**** Generation of contrapositives ****)
-fun is_left (Const ("Trueprop", _) $
- (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
+fun is_left (Const (@{const_name Trueprop}, _) $
+ (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
| is_left _ = false;
(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -401,8 +400,9 @@
(*Is the string the name of a connective? Really only | and Not can remain,
since this code expects to be called on a clause form.*)
val is_conn = member (op =)
- ["Trueprop", "op &", "op |", "op -->", "Not",
- "All", "Ex", @{const_name Ball}, @{const_name Bex}];
+ [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
+ @{const_name "op -->"}, @{const_name Not},
+ @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
(*True if the term contains a function--not a logical connective--where the type
of any argument contains bool.*)
@@ -420,7 +420,7 @@
(*Returns false if any Vars in the theorem mention type bool.
Also rejects functions whose arguments are Booleans or other functions.*)
fun is_fol_term thy t =
- Term.is_first_order ["all","All","Ex"] t andalso
+ Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso
not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
| _ => false) t orelse
has_bool_arg_const t orelse
@@ -429,8 +429,8 @@
fun rigid t = not (is_Var (head_of t));
-fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
- | ok4horn (Const ("Trueprop",_) $ t) = rigid t
+fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
+ | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
| ok4horn _ = false;
(*Create a meta-level Horn clause*)
@@ -464,7 +464,7 @@
(***** MESON PROOF PROCEDURE *****)
-fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi,
+fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
As) = rhyps(phi, A::As)
| rhyps (_, As) = As;
@@ -509,8 +509,8 @@
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
not_impD, not_iffD, not_allD, not_exD, not_notD];
-fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
- | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
+fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t
+ | ok4nnf (Const (@{const_name Trueprop},_) $ t) = rigid t
| ok4nnf _ = false;
fun make_nnf1 ctxt th =
@@ -545,7 +545,7 @@
(*Pull existential quantifiers to front. This accomplishes Skolemization for
clauses that arise from a subgoal.*)
fun skolemize1 ctxt th =
- if not (has_conns ["Ex"] (prop_of th)) then th
+ if not (has_conns [@{const_name Ex}] (prop_of th)) then th
else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2,
disj_exD, disj_exD1, disj_exD2])))
handle THM ("tryres", _, _) =>
--- a/src/HOL/Tools/numeral_simprocs.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Fri Aug 20 14:18:55 2010 +0200
@@ -676,7 +676,7 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
in SOME (mk_meta_eq th) end
- | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ | Const(@{const_name "op ="},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
@@ -697,7 +697,7 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name "op ="},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]
--- a/src/HOL/Tools/prop_logic.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML Fri Aug 20 14:18:55 2010 +0200
@@ -391,20 +391,20 @@
next_idx_is_valid := true;
Unsynchronized.inc next_idx
)
- fun aux (Const ("True", _)) table =
+ fun aux (Const (@{const_name True}, _)) table =
(True, table)
- | aux (Const ("False", _)) table =
+ | aux (Const (@{const_name False}, _)) table =
(False, table)
- | aux (Const ("Not", _) $ x) table =
+ | aux (Const (@{const_name Not}, _) $ x) table =
apfst Not (aux x table)
- | aux (Const ("op |", _) $ x $ y) table =
+ | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1
in
(Or (fm1, fm2), table2)
end
- | aux (Const ("op &", _) $ x $ y) table =
+ | aux (Const (@{const_name "op &"}, _) $ x $ y) table =
let
val (fm1, table1) = aux x table
val (fm2, table2) = aux y table1
--- a/src/HOL/Tools/quickcheck_generators.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Fri Aug 20 14:18:55 2010 +0200
@@ -10,10 +10,8 @@
val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
-> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
-> seed -> (('a -> 'b) * (unit -> term)) * seed
- val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
- val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
- -> string list -> string list * string list -> typ list * typ list
- -> term list * (term * term) list
+ val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
+ -> (string * sort -> string * sort) option
val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
val compile_generator_expr:
theory -> bool -> term -> int -> term list option * (bool list * bool)
@@ -219,11 +217,11 @@
val is_rec = exists is_some ks;
val k = fold (fn NONE => I | SOME k => Integer.max k) ks 0;
val vs = Name.names Name.context "x" (map snd simple_tTs);
- val vs' = (map o apsnd) termifyT vs;
val tc = HOLogic.mk_return T @{typ Random.seed}
(HOLogic.mk_valtermify_app c vs simpleT);
- val t = HOLogic.mk_ST (map (fn (t, _) => (t, @{typ Random.seed})) tTs ~~ map SOME vs')
- tc @{typ Random.seed} (SOME T, @{typ Random.seed});
+ val t = HOLogic.mk_ST
+ (map2 (fn (t, _) => fn (v, T') => ((t, @{typ Random.seed}), SOME ((v, termifyT T')))) tTs vs)
+ tc @{typ Random.seed} (SOME T, @{typ Random.seed});
val tk = if is_rec
then if k = 0 then size
else @{term "Quickcheck.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
@@ -245,7 +243,7 @@
val auxs_rhss = map mk_select gen_exprss;
in (random_auxs, auxs_lhss ~~ auxs_rhss) end;
-fun mk_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
+fun instantiate_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
val _ = Datatype_Aux.message config "Creating quickcheck generators ...";
val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
@@ -272,11 +270,11 @@
fun perhaps_constrain thy insts raw_vs =
let
- fun meet_random (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
+ fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
(Logic.varifyT_global T, sort);
val vtab = Vartab.empty
|> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
- |> fold meet_random insts;
+ |> fold meet insts;
in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
end handle Sorts.CLASS_ERROR _ => NONE;
@@ -297,7 +295,7 @@
can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
in if has_inst then thy
else case perhaps_constrain thy (random_insts @ term_of_insts) typerep_vs
- of SOME constrain => mk_random_datatype config descr
+ of SOME constrain => instantiate_random_datatype config descr
(map constrain typerep_vs) tycos prfx (names, auxnames)
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
| NONE => thy
@@ -344,7 +342,7 @@
val bound_max = length Ts - 1;
val bounds = map_index (fn (i, ty) =>
(2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
- fun strip_imp (Const("op -->",_) $ A $ B) = apfst (cons A) (strip_imp B)
+ fun strip_imp (Const(@{const_name "op -->"},_) $ A $ B) = apfst (cons A) (strip_imp B)
| strip_imp A = ([], A)
val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
@@ -353,11 +351,11 @@
@{term "Pair :: term list option * (bool list * bool) => Random.seed => (term list option * (bool list * bool)) * Random.seed"};
fun mk_assms_report i =
HOLogic.mk_prod (@{term "None :: term list option"},
- HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"}
- (replicate i @{term "True"} @ replicate (length assms - i) @{term "False"}),
- @{term "False"}))
+ HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT
+ (replicate i @{term True} @ replicate (length assms - i) @{term False}),
+ @{term False}))
fun mk_concl_report b =
- HOLogic.mk_prod (HOLogic.mk_list @{typ "bool"} (replicate (length assms) @{term "True"}),
+ HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT (replicate (length assms) @{term True}),
if b then @{term True} else @{term False})
val If =
@{term "If :: bool => term list option * (bool list * bool) => term list option * (bool list * bool) => term list option * (bool list * bool)"}
@@ -385,22 +383,19 @@
fun compile_generator_expr thy report t =
let
val Ts = (map snd o fst o strip_abs) t;
- in
- if report then
- let
- val t' = mk_reporting_generator_expr thy t Ts;
- val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
- (fn proc => fn g => fn s => g s #>> ((apfst o Option.map o map) proc)) thy t' [];
- in
- compile #> Random_Engine.run
- end
- else
- let
- val t' = mk_generator_expr thy t Ts;
- val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
- (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
- val dummy_report = ([], false)
- in fn s => ((compile #> Random_Engine.run) s, dummy_report) end
+ in if report then
+ let
+ val t' = mk_reporting_generator_expr thy t Ts;
+ val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
+ (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) thy t' [];
+ in compile #> Random_Engine.run end
+ else
+ let
+ val t' = mk_generator_expr thy t Ts;
+ val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
+ (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+ val dummy_report = ([], false)
+ in compile #> Random_Engine.run #> rpair dummy_report end
end;
--- a/src/HOL/Tools/quickcheck_record.ML Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: HOL/Tools/quickcheck_record.ML
- Author: Florian Haftmann, TU Muenchen
-
-Quickcheck generators for records.
-*)
-
-signature QUICKCHECK_RECORD =
-sig
- val ensure_random_typecopy: string -> theory -> theory
- val setup: theory -> theory
-end;
-
-structure Quickcheck_Record : QUICKCHECK_RECORD =
-struct
-
-fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
-val size = @{term "i::code_numeral"};
-
-fun mk_random_typecopy tyco vs constr T' thy =
- let
- val mk_const = curry (Sign.mk_const thy);
- val Ts = map TFree vs;
- val T = Type (tyco, Ts);
- val Tm = termifyT T;
- val Tm' = termifyT T';
- val v = "x";
- val t_v = Free (v, Tm');
- val t_constr = Const (constr, T' --> T);
- val lhs = HOLogic.mk_random T size;
- val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))]
- (HOLogic.mk_return Tm @{typ Random.seed}
- (mk_const "Code_Evaluation.valapp" [T', T]
- $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
- @{typ Random.seed} (SOME Tm, @{typ Random.seed});
- val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
- in
- thy
- |> Class.instantiation ([tyco], vs, @{sort random})
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
- |> snd
- |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end;
-
-fun ensure_random_typecopy tyco thy =
- let
- val SOME { vs = raw_vs, constr, typ = raw_T, ... } =
- Typecopy.get_info thy tyco;
- val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
- val T = map_atyps (fn TFree (v, sort) =>
- TFree (v, constrain sort @{sort random})) raw_T;
- val vs' = Term.add_tfreesT T [];
- val vs = map (fn (v, sort) =>
- (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
- val can_inst = Sign.of_sort thy (T, @{sort random});
- in if can_inst then mk_random_typecopy tyco vs constr T thy else thy end;
-
-val setup = Typecopy.interpretation ensure_random_typecopy;
-
-end;
--- a/src/HOL/Tools/record.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/record.ML Fri Aug 20 14:18:55 2010 +0200
@@ -93,21 +93,29 @@
fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *)
);
-fun do_typedef b repT alphas thy =
+fun get_typedef_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
+ { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
let
- val (b_constr, b_proj) = (Binding.prefix_name "make_" b, Binding.prefix_name "dest_" b);
- fun get_thms thy tyco =
- let
- val SOME { vs, constr, typ = repT, proj_inject, proj_constr, ... } =
- Typecopy.get_info thy tyco;
- val absT = Type (tyco, map TFree vs);
- in
- ((proj_inject, proj_constr), Const (constr, repT --> absT), absT)
- end;
+ val exists_thm =
+ UNIV_I
+ |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
+ val proj_constr = Abs_inverse OF [exists_thm];
+ val absT = Type (tyco, map TFree vs);
in
thy
- |> Typecopy.typecopy (b, alphas) repT b_constr b_proj
- |-> (fn (tyco, _) => `(fn thy => get_thms thy tyco))
+ |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
+ end
+
+fun do_typedef raw_tyco repT raw_vs thy =
+ let
+ val ctxt = ProofContext.init_global thy |> Variable.declare_typ repT;
+ val vs = map (ProofContext.check_tfree ctxt) raw_vs;
+ val tac = Tactic.rtac UNIV_witness 1;
+ in
+ thy
+ |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
+ (HOLogic.mk_UNIV repT) NONE tac
+ |-> (fn (tyco, info) => get_typedef_info tyco vs info)
end;
fun mk_cons_tuple (left, right) =
@@ -127,7 +135,7 @@
let
val repT = HOLogic.mk_prodT (leftT, rightT);
- val (((rep_inject, abs_inverse), absC, absT), typ_thy) =
+ val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
thy
|> do_typedef b repT alphas
||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
@@ -155,7 +163,6 @@
cdef_thy
|> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
|> Sign.restore_naming thy
- |> Code.add_default_eqn isom_def;
in
((isom, cons $ isom), thm_thy)
end;
@@ -230,8 +237,8 @@
val wN = "w";
val moreN = "more";
val schemeN = "_scheme";
-val ext_typeN = "_ext_type";
-val inner_typeN = "_inner_type";
+val ext_typeN = "_ext";
+val inner_typeN = "_inner";
val extN ="_ext";
val updateN = "_update";
val makeN = "make";
@@ -1614,7 +1621,8 @@
val ext_binding = Binding.name (suffix extN base_name);
val ext_name = suffix extN name;
- val extT = Type (suffix ext_typeN name, map TFree alphas_zeta);
+ val ext_tyco = suffix ext_typeN name
+ val extT = Type (ext_tyco, map TFree alphas_zeta);
val ext_type = fields_moreTs ---> extT;
@@ -1768,10 +1776,9 @@
[("ext_induct", induct),
("ext_inject", inject),
("ext_surjective", surject),
- ("ext_split", split_meta)])
- ||> Code.add_default_eqn ext_def;
-
- in ((extT, induct', inject', surjective', split_meta', ext_def), thm_thy) end;
+ ("ext_split", split_meta)]);
+
+ in (((ext_name, ext_type), (ext_tyco, alphas_zeta), extT, induct', inject', surjective', split_meta', ext_def), thm_thy) end;
fun chunks [] [] = []
| chunks [] xs = [xs]
@@ -1815,6 +1822,73 @@
in Thm.implies_elim thm' thm end;
+(* code generation *)
+
+fun instantiate_random_record tyco vs extN Ts thy =
+ let
+ val size = @{term "i::code_numeral"};
+ fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
+ val T = Type (tyco, map TFree vs);
+ val Tm = termifyT T;
+ val params = Name.names Name.context "x" Ts;
+ val lhs = HOLogic.mk_random T size;
+ val tc = HOLogic.mk_return Tm @{typ Random.seed}
+ (HOLogic.mk_valtermify_app extN params T);
+ val rhs = HOLogic.mk_ST
+ (map (fn (v, T') => ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
+ tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
+ val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+ in
+ thy
+ |> Class.instantiation ([tyco], vs, @{sort random})
+ |> `(fn lthy => Syntax.check_term lthy eq)
+ |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
+ |> snd
+ |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+ end;
+
+fun ensure_random_record ext_tyco vs extN Ts thy =
+ let
+ val algebra = Sign.classes_of thy;
+ val has_inst = can (Sorts.mg_domain algebra ext_tyco) @{sort random};
+ in if has_inst then thy
+ else case Quickcheck_Generators.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs
+ of SOME constrain => instantiate_random_record ext_tyco (map constrain vs) extN
+ ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
+ | NONE => thy
+ end;
+
+fun add_code ext_tyco vs extT ext simps inject thy =
+ let
+ val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
+ (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT),
+ Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
+ fun tac eq_def = Class.intro_classes_tac []
+ THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
+ THEN ALLGOALS (rtac @{thm refl});
+ fun mk_eq thy eq_def = Simplifier.rewrite_rule
+ [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
+ fun mk_eq_refl thy = @{thm HOL.eq_refl}
+ |> Thm.instantiate
+ ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], [])
+ |> AxClass.unoverload thy;
+ in
+ thy
+ |> Code.add_datatype [ext]
+ |> fold Code.add_default_eqn simps
+ |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_eq])
+ |> `(fn lthy => Syntax.check_term lthy eq)
+ |-> (fn eq => Specification.definition
+ (NONE, (Attrib.empty_binding, eq)))
+ |-> (fn (_, (_, eq_def)) =>
+ Class.prove_instantiation_exit_result Morphism.thm
+ (fn _ => fn eq_def => tac eq_def) eq_def)
+ |-> (fn eq_def => fn thy => thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
+ |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
+ |> ensure_random_record ext_tyco vs (fst ext) ((fst o strip_type o snd) ext)
+ end;
+
+
(* definition *)
fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
@@ -1870,7 +1944,7 @@
val extension_name = full binding;
- val ((extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
+ val ((ext, (ext_tyco, vs), extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
thy
|> Sign.qualified_path false binding
|> extension_definition extension_name fields alphas_ext zeta moreT more vars;
@@ -2042,12 +2116,6 @@
upd_specs
||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
[make_spec, fields_spec, extend_spec, truncate_spec]
- |->
- (fn defs as ((sel_defs, upd_defs), derived_defs) =>
- fold Code.add_default_eqn sel_defs
- #> fold Code.add_default_eqn upd_defs
- #> fold Code.add_default_eqn derived_defs
- #> pair defs)
||> Theory.checkpoint
val (((sel_defs, upd_defs), derived_defs), defs_thy) =
timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
@@ -2330,6 +2398,7 @@
|> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
|> add_extfields extension_name (fields @ [(full_moreN, moreT)])
|> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
+ |> add_code ext_tyco vs extT ext simps' ext_inject
|> Sign.restore_naming thy;
in final_thy end;
--- a/src/HOL/Tools/refute.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/refute.ML Fri Aug 20 14:18:55 2010 +0200
@@ -658,7 +658,7 @@
| Const (@{const_name Finite_Set.card}, _) => t
| Const (@{const_name Finite_Set.finite}, _) => t
| Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
- Type ("fun", [@{typ nat}, Type ("bool", [])])])) => t
+ Type ("fun", [@{typ nat}, @{typ bool}])])) => t
| Const (@{const_name Groups.plus}, Type ("fun", [@{typ nat},
Type ("fun", [@{typ nat}, @{typ nat}])])) => t
| Const (@{const_name Groups.minus}, Type ("fun", [@{typ nat},
@@ -835,7 +835,7 @@
| Const (@{const_name Finite_Set.finite}, T) =>
collect_type_axioms T axs
| Const (@{const_name Orderings.less}, T as Type ("fun", [@{typ nat},
- Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
+ Type ("fun", [@{typ nat}, @{typ bool}])])) =>
collect_type_axioms T axs
| Const (@{const_name Groups.plus}, T as Type ("fun", [@{typ nat},
Type ("fun", [@{typ nat}, @{typ nat}])])) =>
@@ -2653,7 +2653,7 @@
fun Finite_Set_card_interpreter thy model args t =
case t of
Const (@{const_name Finite_Set.card},
- Type ("fun", [Type ("fun", [T, Type ("bool", [])]),
+ Type ("fun", [Type ("fun", [T, @{typ bool}]),
@{typ nat}])) =>
let
(* interpretation -> int *)
@@ -2685,7 +2685,7 @@
Leaf (replicate size_of_nat False)
end
val set_constants =
- make_constants thy model (Type ("fun", [T, Type ("bool", [])]))
+ make_constants thy model (Type ("fun", [T, HOLogic.boolT]))
in
SOME (Node (map card set_constants), model, args)
end
@@ -2702,17 +2702,17 @@
fun Finite_Set_finite_interpreter thy model args t =
case t of
Const (@{const_name Finite_Set.finite},
- Type ("fun", [Type ("fun", [T, Type ("bool", [])]),
- Type ("bool", [])])) $ _ =>
+ Type ("fun", [Type ("fun", [T, @{typ bool}]),
+ @{typ bool}])) $ _ =>
(* we only consider finite models anyway, hence EVERY set is *)
(* "finite" *)
SOME (TT, model, args)
| Const (@{const_name Finite_Set.finite},
- Type ("fun", [Type ("fun", [T, Type ("bool", [])]),
- Type ("bool", [])])) =>
+ Type ("fun", [Type ("fun", [T, @{typ bool}]),
+ @{typ bool}])) =>
let
val size_of_set =
- size_of_type thy model (Type ("fun", [T, Type ("bool", [])]))
+ size_of_type thy model (Type ("fun", [T, HOLogic.boolT]))
in
(* we only consider finite models anyway, hence EVERY set is *)
(* "finite" *)
@@ -2731,7 +2731,7 @@
fun Nat_less_interpreter thy model args t =
case t of
Const (@{const_name Orderings.less}, Type ("fun", [@{typ nat},
- Type ("fun", [@{typ nat}, Type ("bool", [])])])) =>
+ Type ("fun", [@{typ nat}, @{typ bool}])])) =>
let
val size_of_nat = size_of_type thy model (@{typ nat})
(* the 'n'-th nat is not less than the first 'n' nats, while it *)
@@ -2940,20 +2940,20 @@
fun lfp_interpreter thy model args t =
case t of
Const (@{const_name lfp}, Type ("fun", [Type ("fun",
- [Type ("fun", [T, Type ("bool", [])]),
- Type ("fun", [_, Type ("bool", [])])]),
- Type ("fun", [_, Type ("bool", [])])])) =>
+ [Type ("fun", [T, @{typ bool}]),
+ Type ("fun", [_, @{typ bool}])]),
+ Type ("fun", [_, @{typ bool}])])) =>
let
val size_elem = size_of_type thy model T
(* the universe (i.e. the set that contains every element) *)
val i_univ = Node (replicate size_elem TT)
(* all sets with elements from type 'T' *)
val i_sets =
- make_constants thy model (Type ("fun", [T, Type ("bool", [])]))
+ make_constants thy model (Type ("fun", [T, HOLogic.boolT]))
(* all functions that map sets to sets *)
val i_funs = make_constants thy model (Type ("fun",
- [Type ("fun", [T, Type ("bool", [])]),
- Type ("fun", [T, Type ("bool", [])])]))
+ [Type ("fun", [T, @{typ bool}]),
+ Type ("fun", [T, @{typ bool}])]))
(* "lfp(f) == Inter({u. f(u) <= u})" *)
(* interpretation * interpretation -> bool *)
fun is_subset (Node subs, Node sups) =
@@ -2995,20 +2995,20 @@
fun gfp_interpreter thy model args t =
case t of
Const (@{const_name gfp}, Type ("fun", [Type ("fun",
- [Type ("fun", [T, Type ("bool", [])]),
- Type ("fun", [_, Type ("bool", [])])]),
- Type ("fun", [_, Type ("bool", [])])])) =>
+ [Type ("fun", [T, @{typ bool}]),
+ Type ("fun", [_, @{typ bool}])]),
+ Type ("fun", [_, @{typ bool}])])) =>
let
val size_elem = size_of_type thy model T
(* the universe (i.e. the set that contains every element) *)
val i_univ = Node (replicate size_elem TT)
(* all sets with elements from type 'T' *)
val i_sets =
- make_constants thy model (Type ("fun", [T, Type ("bool", [])]))
+ make_constants thy model (Type ("fun", [T, HOLogic.boolT]))
(* all functions that map sets to sets *)
val i_funs = make_constants thy model (Type ("fun",
- [Type ("fun", [T, Type ("bool", [])]),
- Type ("fun", [T, Type ("bool", [])])]))
+ [Type ("fun", [T, HOLogic.boolT]),
+ Type ("fun", [T, HOLogic.boolT])]))
(* "gfp(f) == Union({u. u <= f(u)})" *)
(* interpretation * interpretation -> bool *)
fun is_subset (Node subs, Node sups) =
--- a/src/HOL/Tools/sat_funcs.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Fri Aug 20 14:18:55 2010 +0200
@@ -217,7 +217,7 @@
(* Thm.cterm -> int option *)
fun index_of_literal chyp = (
case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
- (Const ("Not", _) $ atom) =>
+ (Const (@{const_name Not}, _) $ atom) =>
SOME (~ (the (Termtab.lookup atom_table atom)))
| atom =>
SOME (the (Termtab.lookup atom_table atom))
--- a/src/HOL/Tools/simpdata.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML Fri Aug 20 14:18:55 2010 +0200
@@ -45,7 +45,7 @@
(*expects Trueprop if not == *)
of Const (@{const_name "=="},_) $ _ $ _ => th
| _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
- | _ $ (Const (@{const_name "Not"}, _) $ _) => th RS @{thm Eq_FalseI}
+ | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
| _ => th RS @{thm Eq_TrueI}
fun mk_eq_True (_: simpset) r =
--- a/src/HOL/Tools/typecopy.ML Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-(* Title: HOL/Tools/typecopy.ML
- Author: Florian Haftmann, TU Muenchen
-
-Introducing copies of types using trivial typedefs; datatype-like abstraction.
-*)
-
-signature TYPECOPY =
-sig
- type info = { vs: (string * sort) list, typ: typ, constr: string, proj: string,
- constr_inject: thm, proj_inject: thm, constr_proj: thm, proj_constr: thm }
- val typecopy: binding * (string * sort) list -> typ -> binding -> binding
- -> theory -> (string * info) * theory
- val get_info: theory -> string -> info option
- val interpretation: (string -> theory -> theory) -> theory -> theory
- val add_default_code: string -> theory -> theory
- val setup: theory -> theory
-end;
-
-structure Typecopy: TYPECOPY =
-struct
-
-(* theory data *)
-
-type info = {
- vs: (string * sort) list,
- typ: typ,
- constr: string,
- proj: string,
- constr_inject: thm,
- proj_inject: thm,
- constr_proj: thm,
- proj_constr: thm
-};
-
-structure Typecopy_Data = Theory_Data
-(
- type T = info Symtab.table;
- val empty = Symtab.empty;
- val extend = I;
- fun merge data = Symtab.merge (K true) data;
-);
-
-val get_info = Symtab.lookup o Typecopy_Data.get;
-
-
-(* interpretation of type copies *)
-
-structure Typecopy_Interpretation = Interpretation(type T = string val eq = op =);
-val interpretation = Typecopy_Interpretation.interpretation;
-
-
-(* introducing typecopies *)
-
-fun add_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
- { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
- let
- val exists_thm =
- UNIV_I
- |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
- val constr_inject = Abs_inject OF [exists_thm, exists_thm];
- val proj_constr = Abs_inverse OF [exists_thm];
- val info = {
- vs = vs,
- typ = rep_type,
- constr = Abs_name,
- proj = Rep_name,
- constr_inject = constr_inject,
- proj_inject = Rep_inject,
- constr_proj = Rep_inverse,
- proj_constr = proj_constr
- };
- in
- thy
- |> (Typecopy_Data.map o Symtab.update_new) (tyco, info)
- |> Typecopy_Interpretation.data tyco
- |> pair (tyco, info)
- end
-
-fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy =
- let
- val ty = Sign.certify_typ thy raw_ty;
- val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
- val vs = map (ProofContext.check_tfree ctxt) raw_vs;
- val tac = Tactic.rtac UNIV_witness 1;
- in
- thy
- |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
- (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac
- |-> (fn (tyco, info) => add_info tyco vs info)
- end;
-
-
-(* default code setup *)
-
-fun add_default_code tyco thy =
- let
- val SOME { vs, typ = ty_rep, constr = c, proj, proj_constr, proj_inject, ... } =
- get_info thy tyco;
- val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
- val ty = Type (tyco, map TFree vs);
- val proj = Const (proj, ty --> ty_rep);
- val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
- val eq_lhs = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
- $ t_x $ t_y;
- val eq_rhs = HOLogic.mk_eq (proj $ t_x, proj $ t_y);
- val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (eq_lhs, eq_rhs);
- fun tac eq_thm = Class.intro_classes_tac []
- THEN (Simplifier.rewrite_goals_tac
- (map Simpdata.mk_eq [eq_thm, @{thm eq}, proj_inject]))
- THEN ALLGOALS (rtac @{thm refl});
- fun mk_eq_refl thy = @{thm HOL.eq_refl}
- |> Thm.instantiate
- ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global ty)], [])
- |> AxClass.unoverload thy;
- in
- thy
- |> Code.add_datatype [constr]
- |> Code.add_eqn proj_constr
- |> Class.instantiation ([tyco], vs, [HOLogic.class_eq])
- |> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition
- (NONE, (Attrib.empty_binding, eq)))
- |-> (fn (_, (_, eq_thm)) =>
- Class.prove_instantiation_exit_result Morphism.thm
- (fn _ => fn eq_thm => tac eq_thm) eq_thm)
- |-> (fn eq_thm => Code.add_eqn eq_thm)
- |> (fn thy => Code.add_nbe_eqn (mk_eq_refl thy) thy)
- end;
-
-val setup =
- Typecopy_Interpretation.init
- #> interpretation add_default_code
-
-end;
--- a/src/HOL/Tools/typedef_codegen.ML Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-(* Title: HOL/Tools/typedef_codegen.ML
- Author: Stefan Berghofer, TU Muenchen
-
-Code generators for trivial typedefs.
-*)
-
-signature TYPEDEF_CODEGEN =
-sig
- val setup: theory -> theory
-end;
-
-structure TypedefCodegen: TYPEDEF_CODEGEN =
-struct
-
-fun typedef_codegen thy defs dep module brack t gr =
- let
- fun get_name (Type (tname, _)) = tname
- | get_name _ = "";
- fun mk_fun s T ts =
- let
- val (_, gr') = Codegen.invoke_tycodegen thy defs dep module false T gr;
- val (ps, gr'') =
- fold_map (Codegen.invoke_codegen thy defs dep module true) ts gr';
- val id = Codegen.mk_qual_id module (Codegen.get_const_id gr'' s)
- in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end;
- fun lookup f T =
- (* FIXME handle multiple typedef interpretations (!??) *)
- (case Typedef.get_info_global thy (get_name T) of
- [info] => f info
- | _ => "");
- in
- (case strip_comb t of
- (Const (s, Type ("fun", [T, U])), ts) =>
- if lookup (#Rep_name o #1) T = s andalso
- is_none (Codegen.get_assoc_type thy (get_name T))
- then mk_fun s T ts
- else if lookup (#Abs_name o #1) U = s andalso
- is_none (Codegen.get_assoc_type thy (get_name U))
- then mk_fun s U ts
- else NONE
- | _ => NONE)
- end;
-
-fun mk_tyexpr [] s = Codegen.str s
- | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)]
- | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
-
-fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
- (case Typedef.get_info_global thy s of
- (* FIXME handle multiple typedef interpretations (!??) *)
- [({abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}, _)] =>
- if is_some (Codegen.get_assoc_type thy tname) then NONE
- else
- let
- val module' = Codegen.if_library
- (Codegen.thyname_of_type thy tname) module;
- val node_id = tname ^ " (type)";
- val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
- (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
- Ts ||>>
- Codegen.mk_const_id module' Abs_name ||>>
- Codegen.mk_const_id module' Rep_name ||>>
- Codegen.mk_type_id module' s;
- val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
- in
- SOME (tyexpr, case try (Codegen.get_node gr') node_id of
- NONE =>
- let
- val (p :: ps, gr'') = fold_map
- (Codegen.invoke_tycodegen thy defs node_id module' false)
- (oldT :: Us) (Codegen.add_edge (node_id, dep)
- (Codegen.new_node (node_id, (NONE, "", "")) gr'));
- val s =
- Codegen.string_of (Pretty.block [Codegen.str "datatype ",
- mk_tyexpr ps (snd ty_id),
- Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
- Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
- Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
- Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
- Codegen.str "x) = x;"]) ^ "\n\n" ^
- (if member (op =) (!Codegen.mode) "term_of" then
- Codegen.string_of (Pretty.block [Codegen.str "fun ",
- Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
- Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
- Codegen.str "x) =", Pretty.brk 1,
- Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
- Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
- Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
- Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
- Codegen.str "x;"]) ^ "\n\n"
- else "") ^
- (if member (op =) (!Codegen.mode) "test" then
- Codegen.string_of (Pretty.block [Codegen.str "fun ",
- Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
- Codegen.str "i =", Pretty.brk 1,
- Pretty.block [Codegen.str (Abs_id ^ " ("),
- Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
- Codegen.str "i);"]]) ^ "\n\n"
- else "")
- in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
- | SOME _ => Codegen.add_edge (node_id, dep) gr')
- end
- | _ => NONE)
- | typedef_tycodegen thy defs dep module brack _ gr = NONE;
-
-val setup =
- Codegen.add_codegen "typedef" typedef_codegen
- #> Codegen.add_tycodegen "typedef" typedef_tycodegen
-
-end;
--- a/src/HOL/Typedef.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Typedef.thy Fri Aug 20 14:18:55 2010 +0200
@@ -6,9 +6,7 @@
theory Typedef
imports Set
-uses
- ("Tools/typedef.ML")
- ("Tools/typedef_codegen.ML")
+uses ("Tools/typedef.ML")
begin
ML {*
@@ -115,6 +113,5 @@
end
use "Tools/typedef.ML" setup Typedef.setup
-use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
end
--- a/src/HOL/Word/Word.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/Word/Word.thy Fri Aug 20 14:18:55 2010 +0200
@@ -4034,6 +4034,11 @@
"length (rotater n xs) = length xs"
by (simp add : rotater_rev)
+lemma restrict_to_left:
+ assumes "x = y"
+ shows "(x = z) = (y = z)"
+ using assms by simp
+
lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
simplified rotate_gal [symmetric] rotate_gal' [symmetric], standard]
lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
--- a/src/HOL/ex/SVC_Oracle.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Fri Aug 20 14:18:55 2010 +0200
@@ -88,18 +88,18 @@
else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
else replace (c $ x $ y) (*non-numeric comparison*)
(*abstraction of a formula*)
- and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
- | fm ((c as Const("True", _))) = c
- | fm ((c as Const("False", _))) = c
- | fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
+ | fm ((c as Const(@{const_name True}, _))) = c
+ | fm ((c as Const(@{const_name False}, _))) = c
+ | fm (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
(*entry point, and abstraction of a meta-formula*)
- fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
+ fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
| mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
| mt t = fm t (*it might be a formula*)
in (list_all (params, mt body), !pairs) end;
--- a/src/HOL/ex/svc_funcs.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML Fri Aug 20 14:18:55 2010 +0200
@@ -89,13 +89,13 @@
let fun tag t =
let val (c,ts) = strip_comb t
in case c of
- Const("op &", _) => apply c (map tag ts)
- | Const("op |", _) => apply c (map tag ts)
- | Const("op -->", _) => apply c (map tag ts)
- | Const("Not", _) => apply c (map tag ts)
- | Const("True", _) => (c, false)
- | Const("False", _) => (c, false)
- | Const("op =", Type ("fun", [T,_])) =>
+ Const(@{const_name "op &"}, _) => apply c (map tag ts)
+ | Const(@{const_name "op |"}, _) => apply c (map tag ts)
+ | Const(@{const_name "op -->"}, _) => apply c (map tag ts)
+ | Const(@{const_name Not}, _) => apply c (map tag ts)
+ | Const(@{const_name True}, _) => (c, false)
+ | Const(@{const_name False}, _) => (c, false)
+ | Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
if T = HOLogic.boolT then
(*biconditional: with int/nat comparisons below?*)
let val [t1,t2] = ts
@@ -183,16 +183,16 @@
| tm t = Int (lit t)
handle Match => var (t,[])
(*translation of a formula*)
- and fm pos (Const("op &", _) $ p $ q) =
+ and fm pos (Const(@{const_name "op &"}, _) $ p $ q) =
Buildin("AND", [fm pos p, fm pos q])
- | fm pos (Const("op |", _) $ p $ q) =
+ | fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
Buildin("OR", [fm pos p, fm pos q])
- | fm pos (Const("op -->", _) $ p $ q) =
+ | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
Buildin("=>", [fm (not pos) p, fm pos q])
- | fm pos (Const("Not", _) $ p) =
+ | fm pos (Const(@{const_name Not}, _) $ p) =
Buildin("NOT", [fm (not pos) p])
- | fm pos (Const("True", _)) = TrueExpr
- | fm pos (Const("False", _)) = FalseExpr
+ | fm pos (Const(@{const_name True}, _)) = TrueExpr
+ | fm pos (Const(@{const_name False}, _)) = FalseExpr
| fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
(*polarity doesn't matter*)
Buildin("=", [fm pos p, fm pos q])
@@ -200,7 +200,7 @@
Buildin("AND", (*unfolding uses both polarities*)
[Buildin("=>", [fm (not pos) p, fm pos q]),
Buildin("=>", [fm (not pos) q, fm pos p])])
- | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ x $ y) =
let val tx = tm x and ty = tm y
in if pos orelse T = HOLogic.realT then
Buildin("=", [tx, ty])
@@ -225,7 +225,7 @@
else fail t
| fm pos t = var(t,[]);
(*entry point, and translation of a meta-formula*)
- fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)
+ fun mt pos ((c as Const(@{const_name Trueprop}, _)) $ p) = fm pos (iff_tag p)
| mt pos ((c as Const("==>", _)) $ p $ q) =
Buildin("=>", [mt (not pos) p, mt pos q])
| mt pos t = fm pos (iff_tag t) (*it might be a formula*)
--- a/src/HOLCF/Tools/Domain/domain_library.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Fri Aug 20 14:18:55 2010 +0200
@@ -121,8 +121,8 @@
val r_inst = read_instantiate ctxt;
fun at thm =
case concl_of thm of
- _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
- | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
+ _$(Const(@{const_name "op &"},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
+ | _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
| _ => [thm];
in map zero_var_indexes (at thm) end;
@@ -185,7 +185,7 @@
fun mk_lam (x,T) = Abs(x,dummyT,T);
fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
fun mk_ex (x,P) = mk_exists (x,dummyT,P);
-fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
+fun mk_constrainall (x,typ,P) = %%: @{const_name All} $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
end
fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
--- a/src/Pure/General/markup.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/General/markup.ML Fri Aug 20 14:18:55 2010 +0200
@@ -9,8 +9,8 @@
val parse_int: string -> int
val print_int: int -> string
type T = string * Properties.T
- val none: T
- val is_none: T -> bool
+ val empty: T
+ val is_empty: T -> bool
val properties: Properties.T -> T -> T
val nameN: string
val name: string -> T -> T
@@ -142,10 +142,10 @@
type T = string * Properties.T;
-val none = ("", []);
+val empty = ("", []);
-fun is_none ("", _) = true
- | is_none _ = false;
+fun is_empty ("", _) = true
+ | is_empty _ = false;
fun properties more_props ((elem, props): T) =
@@ -356,7 +356,7 @@
the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
end;
-fun output m = if is_none m then no_output else #output (get_mode ()) m;
+fun output m = if is_empty m then no_output else #output (get_mode ()) m;
val enclose = output #-> Library.enclose;
--- a/src/Pure/General/markup.scala Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/General/markup.scala Fri Aug 20 14:18:55 2010 +0200
@@ -48,6 +48,11 @@
}
+ /* empty */
+
+ val Empty = Markup("", Nil)
+
+
/* name */
val NAME = "name"
--- a/src/Pure/General/position.scala Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/General/position.scala Fri Aug 20 14:18:55 2010 +0200
@@ -20,13 +20,13 @@
def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
- def get_range(pos: T): Option[(Int, Int)] =
+ def get_range(pos: T): Option[Text.Range] =
(get_offset(pos), get_end_offset(pos)) match {
- case (Some(begin), Some(end)) => Some(begin, end)
- case (Some(begin), None) => Some(begin, begin + 1)
+ case (Some(start), Some(stop)) => Some(Text.Range(start, stop))
+ case (Some(start), None) => Some(Text.Range(start, start + 1))
case (None, _) => None
}
object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
- object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
+ object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
}
--- a/src/Pure/General/pretty.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/General/pretty.ML Fri Aug 20 14:18:55 2010 +0200
@@ -132,7 +132,7 @@
fun markup_block m arg = block_markup (Markup.output m) arg;
-val blk = markup_block Markup.none;
+val blk = markup_block Markup.empty;
fun block prts = blk (2, prts);
val strs = block o breaks o map str;
@@ -142,7 +142,7 @@
fun command name = mark Markup.command (str name);
fun markup_chunks m prts = markup m (fbreaks prts);
-val chunks = markup_chunks Markup.none;
+val chunks = markup_chunks Markup.empty;
fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sha1.scala Fri Aug 20 14:18:55 2010 +0200
@@ -0,0 +1,28 @@
+/* Title: Pure/General/sha1.scala
+ Author: Makarius
+
+Digesting strings according to SHA-1 (see RFC 3174).
+*/
+
+package isabelle
+
+
+import java.security.MessageDigest
+
+
+object SHA1
+{
+ def digest_bytes(bytes: Array[Byte]): String =
+ {
+ val result = new StringBuilder
+ for (b <- MessageDigest.getInstance("SHA").digest(bytes)) {
+ val i = b.asInstanceOf[Int] & 0xFF
+ if (i < 16) result += '0'
+ result ++= Integer.toHexString(i)
+ }
+ result.toString
+ }
+
+ def digest(s: String): String = digest_bytes(Standard_System.string_bytes(s))
+}
+
--- a/src/Pure/General/symbol.scala Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/General/symbol.scala Fri Aug 20 14:18:55 2010 +0200
@@ -106,8 +106,9 @@
}
buf.toArray
}
- def decode(sym: Int): Int =
+ def decode(sym1: Int): Int =
{
+ val sym = sym1 - 1
val end = index.length
def bisect(a: Int, b: Int): Int =
{
@@ -123,6 +124,7 @@
if (i < 0) sym
else index(i).chr + sym - index(i).sym
}
+ def decode(range: Text.Range): Text.Range = range.map(decode(_))
}
--- a/src/Pure/General/xml.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/General/xml.ML Fri Aug 20 14:18:55 2010 +0200
@@ -79,7 +79,7 @@
end;
fun output_markup (markup as (name, atts)) =
- if Markup.is_none markup then Markup.no_output
+ if Markup.is_empty markup then Markup.no_output
else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
--- a/src/Pure/General/xml.scala Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/General/xml.scala Fri Aug 20 14:18:55 2010 +0200
@@ -67,30 +67,15 @@
def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
- /* iterate over content */
-
- private type State = Option[(String, List[Tree])]
+ /* text content */
- private def get_next(tree: Tree): State = tree match {
- case Elem(_, body) => get_nexts(body)
- case Text(content) => Some(content, Nil)
- }
- private def get_nexts(trees: List[Tree]): State = trees match {
- case Nil => None
- case t :: ts => get_next(t) match {
- case None => get_nexts(ts)
- case Some((s, r)) => Some((s, r ++ ts))
+ def content_stream(tree: Tree): Stream[String] =
+ tree match {
+ case Elem(_, body) => body.toStream.flatten(content_stream(_))
+ case Text(content) => Stream(content)
}
- }
- def content(tree: Tree) = new Iterator[String] {
- private var state = get_next(tree)
- def hasNext() = state.isDefined
- def next() = state match {
- case Some((s, rest)) => { state = get_nexts(rest); s }
- case None => throw new NoSuchElementException("next on empty iterator")
- }
- }
+ def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
/* pipe-lined cache for partial sharing */
--- a/src/Pure/General/yxml.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/General/yxml.ML Fri Aug 20 14:18:55 2010 +0200
@@ -52,7 +52,7 @@
(* output *)
fun output_markup (markup as (name, atts)) =
- if Markup.is_none markup then Markup.no_output
+ if Markup.is_empty markup then Markup.no_output
else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
fun element name atts body =
--- a/src/Pure/General/yxml.scala Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/General/yxml.scala Fri Aug 20 14:18:55 2010 +0200
@@ -85,7 +85,7 @@
/* stack operations */
def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
- var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup("", Nil), buffer()))
+ var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
def add(x: XML.Tree)
{
@@ -101,7 +101,7 @@
def pop()
{
(stack: @unchecked) match {
- case ((Markup("", _), _) :: _) => err_unbalanced("")
+ case ((Markup.Empty, _) :: _) => err_unbalanced("")
case ((markup, body) :: pending) =>
stack = pending
add(XML.Elem(markup, body.toList))
@@ -122,7 +122,7 @@
}
}
stack match {
- case List((Markup("", _), body)) => body.toList
+ case List((Markup.Empty, body)) => body.toList
case (Markup(name, _), _) :: _ => err_unbalanced(name)
}
}
--- a/src/Pure/IsaMakefile Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/IsaMakefile Fri Aug 20 14:18:55 2010 +0200
@@ -21,7 +21,6 @@
BOOTSTRAP_FILES = \
ML-Systems/bash.ML \
- ML-Systems/compiler_polyml-5.0.ML \
ML-Systems/compiler_polyml-5.2.ML \
ML-Systems/compiler_polyml-5.3.ML \
ML-Systems/ml_name_space.ML \
@@ -29,8 +28,6 @@
ML-Systems/multithreading.ML \
ML-Systems/multithreading_polyml.ML \
ML-Systems/overloading_smlnj.ML \
- ML-Systems/polyml-5.0.ML \
- ML-Systems/polyml-5.1.ML \
ML-Systems/polyml-5.2.1.ML \
ML-Systems/polyml-5.2.ML \
ML-Systems/polyml.ML \
@@ -160,6 +157,7 @@
ML/ml_syntax.ML \
ML/ml_thms.ML \
PIDE/document.ML \
+ PIDE/isar_document.ML \
Proof/extraction.ML \
Proof/proof_rewrite_rules.ML \
Proof/proof_syntax.ML \
@@ -191,7 +189,6 @@
Syntax/type_ext.ML \
System/isabelle_process.ML \
System/isar.ML \
- System/isar_document.ML \
System/session.ML \
Thy/html.ML \
Thy/latex.ML \
--- a/src/Pure/Isar/outer_syntax.scala Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Fri Aug 20 14:18:55 2010 +0200
@@ -16,6 +16,8 @@
protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
lazy val completion: Completion = new Completion + symbols // FIXME !?
+ def keyword_kind(name: String): Option[String] = keywords.get(name)
+
def + (name: String, kind: String): Outer_Syntax =
{
val new_keywords = keywords + (name -> kind)
--- a/src/Pure/Isar/toplevel.scala Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/Isar/toplevel.scala Fri Aug 20 14:18:55 2010 +0200
@@ -15,16 +15,18 @@
case object Finished extends Status
case object Failed extends Status
- def command_status(markup: List[Markup]): Status =
+ def command_status(markup: XML.Body): Status =
{
val forks = (0 /: markup) {
- case (i, Markup(Markup.FORKED, _)) => i + 1
- case (i, Markup(Markup.JOINED, _)) => i - 1
+ case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
+ case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
case (i, _) => i
}
if (forks != 0) Forked(forks)
- else if (markup.exists(_.name == Markup.FAILED)) Failed
- else if (markup.exists(_.name == Markup.FINISHED)) Finished
+ else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
+ Failed
+ else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
+ Finished
else Unprocessed
}
}
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: Pure/ML-Systems/compiler_polyml-5.0.ML
-
-Runtime compilation for Poly/ML 5.0 and 5.1.
-*)
-
-fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
- let
- val in_buffer = Unsynchronized.ref (explode (tune_source txt));
- val out_buffer = Unsynchronized.ref ([]: string list);
- fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
-
- val current_line = Unsynchronized.ref line;
- fun get () =
- (case ! in_buffer of
- [] => ""
- | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
- fun put s = out_buffer := s :: ! out_buffer;
-
- fun exec () =
- (case ! in_buffer of
- [] => ()
- | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
- in
- exec () handle exn => (error (output ()); reraise exn);
- if verbose then print (output ()) else ()
- end;
-
-fun use_file context verbose name =
- let
- val instream = TextIO.openIn name;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Fri Aug 20 14:18:55 2010 +0200
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/compiler_polyml-5.3.ML
-Runtime compilation for Poly/ML 5.3.0.
+Runtime compilation for Poly/ML 5.3 and 5.4.
*)
local
--- a/src/Pure/ML-Systems/polyml-5.0.ML Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-5.0.ML
-
-Compatibility wrapper for Poly/ML 5.0.
-*)
-
-fun reraise exn = raise exn;
-
-use "ML-Systems/unsynchronized.ML";
-use "ML-Systems/universal.ML";
-use "ML-Systems/thread_dummy.ML";
-use "ML-Systems/ml_name_space.ML";
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/compiler_polyml-5.0.ML";
-use "ML-Systems/pp_polyml.ML";
-
-val pointer_eq = PolyML.pointerEq;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
--- a/src/Pure/ML-Systems/polyml-5.1.ML Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-5.1.ML
-
-Compatibility wrapper for Poly/ML 5.1.
-*)
-
-fun reraise exn = raise exn;
-
-use "ML-Systems/unsynchronized.ML";
-use "ML-Systems/thread_dummy.ML";
-use "ML-Systems/ml_name_space.ML";
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/compiler_polyml-5.0.ML";
-use "ML-Systems/pp_polyml.ML";
-
-val pointer_eq = PolyML.pointerEq;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
--- a/src/Pure/ML-Systems/polyml.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Fri Aug 20 14:18:55 2010 +0200
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/polyml.ML
-Compatibility wrapper for Poly/ML 5.3.0.
+Compatibility wrapper for Poly/ML 5.3 and 5.4.
*)
use "ML-Systems/unsynchronized.ML";
--- a/src/Pure/ML/ml_lex.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML Fri Aug 20 14:18:55 2010 +0200
@@ -100,10 +100,10 @@
| Real => Markup.ML_numeral
| Char => Markup.ML_char
| String => Markup.ML_string
- | Space => Markup.none
+ | Space => Markup.empty
| Comment => Markup.ML_comment
| Error _ => Markup.ML_malformed
- | EOF => Markup.none;
+ | EOF => Markup.empty;
fun token_markup kind x =
if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
--- a/src/Pure/PIDE/command.scala Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/PIDE/command.scala Fri Aug 20 14:18:55 2010 +0200
@@ -27,9 +27,9 @@
case class State(
val command: Command,
- val status: List[Markup],
+ val status: List[XML.Tree],
val reverse_results: List[XML.Tree],
- val markup: Markup_Text)
+ val markup: Markup_Tree)
{
/* content */
@@ -37,23 +37,27 @@
def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
- def add_markup(node: Markup_Tree): State = copy(markup = markup + node)
+ def add_markup(node: Markup_Tree.Node): State = copy(markup = markup + node)
+
+ def markup_root_node: Markup_Tree.Node =
+ new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
+ def markup_root: Markup_Tree = markup + markup_root_node
/* markup */
- lazy val highlight: Markup_Text =
+ lazy val highlight: List[Markup_Tree.Node] =
{
markup.filter(_.info match {
case Command.HighlightInfo(_, _) => true
case _ => false
- })
+ }).flatten(markup_root_node)
}
- private lazy val types: List[Markup_Node] =
+ private lazy val types: List[Markup_Tree.Node] =
markup.filter(_.info match {
case Command.TypeInfo(_) => true
- case _ => false }).flatten
+ case _ => false }).flatten(markup_root_node)
def type_at(pos: Text.Offset): Option[String] =
{
@@ -67,12 +71,12 @@
}
}
- private lazy val refs: List[Markup_Node] =
+ private lazy val refs: List[Markup_Tree.Node] =
markup.filter(_.info match {
case Command.RefInfo(_, _, _, _) => true
- case _ => false }).flatten
+ case _ => false }).flatten(markup_root_node)
- def ref_at(pos: Text.Offset): Option[Markup_Node] =
+ def ref_at(pos: Text.Offset): Option[Markup_Tree.Node] =
refs.find(_.range.contains(pos))
@@ -80,26 +84,23 @@
def accumulate(message: XML.Tree): Command.State =
message match {
- case XML.Elem(Markup(Markup.STATUS, _), elems) =>
- copy(status = (for (XML.Elem(markup, _) <- elems) yield markup) ::: status)
+ case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status)
case XML.Elem(Markup(Markup.REPORT, _), elems) =>
(this /: elems)((state, elem) =>
elem match {
case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
atts match {
- case Position.Range(begin, end) =>
+ case Position.Range(range) =>
if (kind == Markup.ML_TYPING) {
val info = Pretty.string_of(body, margin = 40)
- state.add_markup(
- command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
+ state.add_markup(command.decode_range(range, Command.TypeInfo(info)))
}
else if (kind == Markup.ML_REF) {
body match {
case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
state.add_markup(
- command.markup_node(
- begin - 1, end - 1,
+ command.decode_range(range,
Command.RefInfo(
Position.get_file(props),
Position.get_line(props),
@@ -110,7 +111,7 @@
}
else {
state.add_markup(
- command.markup_node(begin - 1, end - 1,
+ command.decode_range(range,
Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
}
case _ => state
@@ -151,21 +152,18 @@
val source: String = span.map(_.source).mkString
def source(range: Text.Range): String = source.substring(range.start, range.stop)
def length: Int = source.length
+ val range: Text.Range = Text.Range(0, length)
lazy val symbol_index = new Symbol.Index(source)
/* markup */
- def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
- {
- val start = symbol_index.decode(begin)
- val stop = symbol_index.decode(end)
- new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
- }
+ def decode_range(range: Text.Range, info: Any): Markup_Tree.Node =
+ new Markup_Tree.Node(symbol_index.decode(range), info)
/* accumulated results */
- val empty_state: Command.State = Command.State(this, Nil, Nil, new Markup_Text(Nil, source))
+ val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/isar_document.ML Fri Aug 20 14:18:55 2010 +0200
@@ -0,0 +1,42 @@
+(* Title: Pure/PIDE/isar_document.ML
+ Author: Makarius
+
+Protocol commands for interactive Isar documents.
+*)
+
+structure Isar_Document: sig end =
+struct
+
+val global_state = Synchronized.var "Isar_Document" Document.init_state;
+val change_state = Synchronized.change global_state;
+
+val _ =
+ Isabelle_Process.add_command "Isar_Document.define_command"
+ (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
+
+val _ =
+ Isabelle_Process.add_command "Isar_Document.edit_version"
+ (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
+ let
+ val old_id = Document.parse_id old_id_string;
+ val new_id = Document.parse_id new_id_string;
+ val edits =
+ XML_Data.dest_list
+ (XML_Data.dest_pair
+ XML_Data.dest_string
+ (XML_Data.dest_option
+ (XML_Data.dest_list
+ (XML_Data.dest_pair
+ (XML_Data.dest_option XML_Data.dest_int)
+ (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
+
+ val (updates, state') = Document.edit old_id new_id edits state;
+ val _ =
+ implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
+ |> Markup.markup (Markup.assign new_id)
+ |> Output.status;
+ val state'' = Document.execute new_id state';
+ in state'' end));
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/isar_document.scala Fri Aug 20 14:18:55 2010 +0200
@@ -0,0 +1,65 @@
+/* Title: Pure/PIDE/isar_document.scala
+ Author: Makarius
+
+Protocol commands for interactive Isar documents.
+*/
+
+package isabelle
+
+
+object Isar_Document
+{
+ /* protocol messages */
+
+ object Assign {
+ def unapply(msg: XML.Tree)
+ : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
+ msg match {
+ case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
+ val id_edits = edits.map(Edit.unapply)
+ if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
+ else None
+ case _ => None
+ }
+ }
+
+ object Edit {
+ def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
+ msg match {
+ case XML.Elem(
+ Markup(Markup.EDIT,
+ List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
+ case _ => None
+ }
+ }
+}
+
+
+trait Isar_Document extends Isabelle_Process
+{
+ import Isar_Document._
+
+
+ /* commands */
+
+ def define_command(id: Document.Command_ID, text: String): Unit =
+ input("Isar_Document.define_command", Document.ID(id), text)
+
+
+ /* document versions */
+
+ def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
+ edits: List[Document.Edit[Document.Command_ID]])
+ {
+ val arg =
+ XML_Data.make_list(
+ XML_Data.make_pair(XML_Data.make_string)(
+ XML_Data.make_option(XML_Data.make_list(
+ XML_Data.make_pair(
+ XML_Data.make_option(XML_Data.make_long))(
+ XML_Data.make_option(XML_Data.make_long))))))(edits)
+
+ input("Isar_Document.edit_version",
+ Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
+ }
+}
--- a/src/Pure/PIDE/markup_node.scala Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-/* Title: Pure/PIDE/markup_node.scala
- Author: Fabian Immler, TU Munich
- Author: Makarius
-
-Text markup nodes.
-*/
-
-package isabelle
-
-
-import javax.swing.tree.DefaultMutableTreeNode
-
-
-
-case class Markup_Node(val range: Text.Range, val info: Any)
-{
- def fits_into(that: Markup_Node): Boolean =
- that.range.start <= this.range.start && this.range.stop <= that.range.stop
-}
-
-
-case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
-{
- private def add(branch: Markup_Tree) = // FIXME avoid sort
- copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start))
-
- private def remove(bs: List[Markup_Tree]) =
- copy(branches = branches.filterNot(bs.contains(_)))
-
- def + (new_tree: Markup_Tree): Markup_Tree =
- {
- val new_node = new_tree.node
- if (new_node fits_into node) {
- var inserted = false
- val new_branches =
- branches.map(branch =>
- if ((new_node fits_into branch.node) && !inserted) {
- inserted = true
- branch + new_tree
- }
- else branch)
- if (!inserted) {
- // new_tree did not fit into children of this
- // -> insert between this and its branches
- val fitting = branches filter(_.node fits_into new_node)
- (this remove fitting) add ((new_tree /: fitting)(_ + _))
- }
- else copy(branches = new_branches)
- }
- else {
- System.err.println("Ignored nonfitting markup: " + new_node)
- this
- }
- }
-
- def flatten: List[Markup_Node] =
- {
- var next_x = node.range.start
- if (branches.isEmpty) List(this.node)
- else {
- val filled_gaps =
- for {
- child <- branches
- markups =
- if (next_x < child.node.range.start)
- new Markup_Node(Text.Range(next_x, child.node.range.start), node.info) :: child.flatten
- else child.flatten
- update = (next_x = child.node.range.stop)
- markup <- markups
- } yield markup
- if (next_x < node.range.stop)
- filled_gaps ::: List(new Markup_Node(Text.Range(next_x, node.range.stop), node.info))
- else filled_gaps
- }
- }
-}
-
-
-case class Markup_Text(val markup: List[Markup_Tree], val content: String)
-{
- private val root = new Markup_Tree(new Markup_Node(Text.Range(0, content.length), None), markup) // FIXME !?
-
- def + (new_tree: Markup_Tree): Markup_Text =
- new Markup_Text((root + new_tree).branches, content)
-
- def filter(pred: Markup_Node => Boolean): Markup_Text =
- {
- def filt(tree: Markup_Tree): List[Markup_Tree] =
- {
- val branches = tree.branches.flatMap(filt(_))
- if (pred(tree.node)) List(tree.copy(branches = branches))
- else branches
- }
- new Markup_Text(markup.flatMap(filt(_)), content)
- }
-
- def flatten: List[Markup_Node] = markup.flatten(_.flatten)
-
- def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
- {
- def swing(tree: Markup_Tree): DefaultMutableTreeNode =
- {
- val node = swing_node(tree.node)
- tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
- node
- }
- swing(root)
- }
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/markup_tree.scala Fri Aug 20 14:18:55 2010 +0200
@@ -0,0 +1,144 @@
+/* Title: Pure/PIDE/markup_tree.scala
+ Author: Fabian Immler, TU Munich
+ Author: Makarius
+
+Markup trees over nested / non-overlapping text ranges.
+*/
+
+package isabelle
+
+
+import javax.swing.tree.DefaultMutableTreeNode
+
+import scala.collection.immutable.SortedMap
+import scala.collection.mutable
+import scala.annotation.tailrec
+
+
+object Markup_Tree
+{
+ case class Node(val range: Text.Range, val info: Any)
+ {
+ def contains(that: Node): Boolean = this.range contains that.range
+ def intersect(r: Text.Range): Node = Node(range.intersect(r), info)
+ }
+
+
+ /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */
+
+ object Branches
+ {
+ type Entry = (Node, Markup_Tree)
+ type T = SortedMap[Node, Entry]
+
+ val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node]
+ {
+ def compare(x: Node, y: Node): Int = x.range compare y.range
+ })
+ def update(branches: T, entries: Entry*): T =
+ branches ++ entries.map(e => (e._1 -> e))
+ }
+
+ val empty = new Markup_Tree(Branches.empty)
+}
+
+
+case class Markup_Tree(val branches: Markup_Tree.Branches.T)
+{
+ import Markup_Tree._
+
+ def + (new_node: Node): Markup_Tree =
+ {
+ branches.get(new_node) match {
+ case None =>
+ new Markup_Tree(Branches.update(branches, new_node -> empty))
+ case Some((node, subtree)) =>
+ if (node.range != new_node.range && node.contains(new_node))
+ new Markup_Tree(Branches.update(branches, node -> (subtree + new_node)))
+ else if (new_node.contains(branches.head._1) && new_node.contains(branches.last._1))
+ new Markup_Tree(Branches.update(Branches.empty, (new_node -> this)))
+ else {
+ var overlapping = Branches.empty
+ var rest = branches
+ while (rest.isDefinedAt(new_node)) {
+ overlapping = Branches.update(overlapping, rest(new_node))
+ rest -= new_node
+ }
+ if (overlapping.forall(e => new_node.contains(e._1)))
+ new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(overlapping)))
+ else { // FIXME split markup!?
+ System.err.println("Ignored overlapping markup: " + new_node)
+ this
+ }
+ }
+ }
+ }
+
+ // FIXME depth-first with result markup stack
+ // FIXME projection to given range
+ def flatten(parent: Node): List[Node] =
+ {
+ val result = new mutable.ListBuffer[Node]
+ var offset = parent.range.start
+ for ((_, (node, subtree)) <- branches.iterator) {
+ if (offset < node.range.start)
+ result += new Node(Text.Range(offset, node.range.start), parent.info)
+ result ++= subtree.flatten(node)
+ offset = node.range.stop
+ }
+ if (offset < parent.range.stop)
+ result += new Node(Text.Range(offset, parent.range.stop), parent.info)
+ result.toList
+ }
+
+ def filter(pred: Node => Boolean): Markup_Tree =
+ {
+ val bs = branches.toList.flatMap(entry => {
+ val (_, (node, subtree)) = entry
+ if (pred(node)) List((node, (node, subtree.filter(pred))))
+ else subtree.filter(pred).branches.toList
+ })
+ new Markup_Tree(Branches.empty ++ bs)
+ }
+
+ def select[A](range: Text.Range)(sel: PartialFunction[Node, A]): Stream[Node] =
+ {
+ def stream(parent: Node, bs: Branches.T): Stream[Node] =
+ {
+ val start = Node(parent.range.start_range, Nil)
+ val stop = Node(parent.range.stop_range, Nil)
+ val substream =
+ (for ((_, (node, subtree)) <- bs.range(start, stop).toStream) yield {
+ if (sel.isDefinedAt(node))
+ stream(node.intersect(parent.range), subtree.branches)
+ else stream(parent, subtree.branches)
+ }).flatten
+
+ def padding(last: Text.Offset, s: Stream[Node]): Stream[Node] =
+ s match {
+ case node #:: rest =>
+ if (last < node.range.start)
+ parent.intersect(Text.Range(last, node.range.start)) #::
+ node #:: padding(node.range.stop, rest)
+ else node #:: padding(node.range.stop, rest)
+ case Stream.Empty => // FIXME
+ if (last < parent.range.stop)
+ Stream(parent.intersect(Text.Range(last, parent.range.stop)))
+ else Stream.Empty
+ }
+ padding(parent.range.start, substream)
+ }
+ // FIXME handle disjoint range!?
+ stream(Node(range, Nil), branches)
+ }
+
+ def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode)
+ {
+ for ((_, (node, subtree)) <- branches) {
+ val current = swing_node(node)
+ subtree.swing_tree(current)(swing_node)
+ parent.add(current)
+ }
+ }
+}
+
--- a/src/Pure/PIDE/text.scala Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/PIDE/text.scala Fri Aug 20 14:18:55 2010 +0200
@@ -10,15 +10,42 @@
object Text
{
- /* offset and range */
+ /* offset */
type Offset = Int
+
+ /* range: interval with total quasi-ordering */
+
+ object Range
+ {
+ object Ordering extends scala.math.Ordering[Range]
+ {
+ override def compare(r1: Range, r2: Range): Int = r1 compare r2
+ }
+ }
+
sealed case class Range(val start: Offset, val stop: Offset)
{
- def contains(i: Offset): Boolean = start <= i && i < stop
+ require(start <= stop)
+
def map(f: Offset => Offset): Range = Range(f(start), f(stop))
def +(i: Offset): Range = map(_ + i)
+ def contains(i: Offset): Boolean = start <= i && i < stop
+ def contains(that: Range): Boolean =
+ this == that || this.contains(that.start) && that.stop <= this.stop
+ def overlaps(that: Range): Boolean =
+ this == that || this.contains(that.start) || that.contains(this.start)
+ def compare(that: Range): Int =
+ if (overlaps(that)) 0
+ else if (this.start < that.start) -1
+ else 1
+
+ def start_range: Range = Range(start, start)
+ def stop_range: Range = Range(stop, stop)
+
+ def intersect(that: Range): Range =
+ Range(this.start max that.start, this.stop min that.stop)
}
--- a/src/Pure/ROOT.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/ROOT.ML Fri Aug 20 14:18:55 2010 +0200
@@ -179,9 +179,9 @@
use "ML/ml_syntax.ML";
use "ML/ml_env.ML";
use "Isar/runtime.ML";
-if ml_system = "polyml-5.3.0"
-then use "ML/ml_compiler_polyml-5.3.ML"
-else use "ML/ml_compiler.ML";
+if member (op =) ["polyml-5.2", "polyml-5.2.1", "smlnj-110"] ml_system
+then use "ML/ml_compiler.ML"
+else use "ML/ml_compiler_polyml-5.3.ML";
use "ML/ml_context.ML";
(*theory sources*)
@@ -257,7 +257,7 @@
use "System/session.ML";
use "System/isabelle_process.ML";
-use "System/isar_document.ML";
+use "PIDE/isar_document.ML";
use "System/isar.ML";
--- a/src/Pure/Syntax/lexicon.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML Fri Aug 20 14:18:55 2010 +0200
@@ -181,9 +181,9 @@
| FloatSy => Markup.numeral
| XNumSy => Markup.numeral
| StrSy => Markup.inner_string
- | Space => Markup.none
+ | Space => Markup.empty
| Comment => Markup.inner_comment
- | EOF => Markup.none;
+ | EOF => Markup.empty;
fun report_token ctxt (Token (kind, _, (pos, _))) =
Context_Position.report ctxt (token_kind_markup kind) pos;
--- a/src/Pure/System/isar_document.ML Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(* Title: Pure/System/isar_document.ML
- Author: Makarius
-
-Protocol commands for interactive Isar documents.
-*)
-
-structure Isar_Document: sig end =
-struct
-
-val global_state = Synchronized.var "Isar_Document" Document.init_state;
-val change_state = Synchronized.change global_state;
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.define_command"
- (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
-
-val _ =
- Isabelle_Process.add_command "Isar_Document.edit_version"
- (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
- let
- val old_id = Document.parse_id old_id_string;
- val new_id = Document.parse_id new_id_string;
- val edits =
- XML_Data.dest_list
- (XML_Data.dest_pair
- XML_Data.dest_string
- (XML_Data.dest_option
- (XML_Data.dest_list
- (XML_Data.dest_pair
- (XML_Data.dest_option XML_Data.dest_int)
- (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
-
- val (updates, state') = Document.edit old_id new_id edits state;
- val _ =
- implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
- |> Markup.markup (Markup.assign new_id)
- |> Output.status;
- val state'' = Document.execute new_id state';
- in state'' end));
-
-end;
-
--- a/src/Pure/System/isar_document.scala Fri Aug 20 14:15:29 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-/* Title: Pure/System/isar_document.scala
- Author: Makarius
-
-Protocol commands for interactive Isar documents.
-*/
-
-package isabelle
-
-
-object Isar_Document
-{
- /* protocol messages */
-
- object Assign {
- def unapply(msg: XML.Tree)
- : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
- msg match {
- case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
- val id_edits = edits.map(Edit.unapply)
- if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
- else None
- case _ => None
- }
- }
-
- object Edit {
- def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
- msg match {
- case XML.Elem(
- Markup(Markup.EDIT,
- List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
- case _ => None
- }
- }
-}
-
-
-trait Isar_Document extends Isabelle_Process
-{
- import Isar_Document._
-
-
- /* commands */
-
- def define_command(id: Document.Command_ID, text: String): Unit =
- input("Isar_Document.define_command", Document.ID(id), text)
-
-
- /* document versions */
-
- def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
- edits: List[Document.Edit[Document.Command_ID]])
- {
- val arg =
- XML_Data.make_list(
- XML_Data.make_pair(XML_Data.make_string)(
- XML_Data.make_option(XML_Data.make_list(
- XML_Data.make_pair(
- XML_Data.make_option(XML_Data.make_long))(
- XML_Data.make_option(XML_Data.make_long))))))(edits)
-
- input("Isar_Document.edit_version",
- Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
- }
-}
--- a/src/Pure/Thy/thy_syntax.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Fri Aug 20 14:18:55 2010 +0200
@@ -59,9 +59,9 @@
| Token.String => Markup.string
| Token.AltString => Markup.altstring
| Token.Verbatim => Markup.verbatim
- | Token.Space => Markup.none
+ | Token.Space => Markup.empty
| Token.Comment => Markup.comment
- | Token.InternalValue => Markup.none
+ | Token.InternalValue => Markup.empty
| Token.Malformed => Markup.malformed
| Token.Error _ => Markup.malformed
| Token.Sync => Markup.control
@@ -73,10 +73,8 @@
let
val kind = Token.kind_of tok;
val props =
- if kind = Token.Command then
- (case Keyword.command_keyword (Token.content_of tok) of
- SOME k => Markup.properties [(Markup.kindN, Keyword.kind_of k)]
- | NONE => I)
+ if kind = Token.Command
+ then Markup.properties [(Markup.nameN, Token.content_of tok)]
else I;
in props (token_kind_markup kind) end;
--- a/src/Pure/build-jars Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/build-jars Fri Aug 20 14:18:55 2010 +0200
@@ -29,6 +29,7 @@
General/position.scala
General/pretty.scala
General/scan.scala
+ General/sha1.scala
General/symbol.scala
General/xml.scala
General/xml_data.scala
@@ -40,7 +41,8 @@
Isar/token.scala
PIDE/command.scala
PIDE/document.scala
- PIDE/markup_node.scala
+ PIDE/isar_document.scala
+ PIDE/markup_tree.scala
PIDE/text.scala
System/cygwin.scala
System/download.scala
@@ -49,7 +51,6 @@
System/isabelle_process.scala
System/isabelle_syntax.scala
System/isabelle_system.scala
- System/isar_document.scala
System/platform.scala
System/session.scala
System/session_manager.scala
--- a/src/Pure/context_position.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/context_position.ML Fri Aug 20 14:18:55 2010 +0200
@@ -9,6 +9,7 @@
val is_visible: Proof.context -> bool
val set_visible: bool -> Proof.context -> Proof.context
val restore_visible: Proof.context -> Proof.context -> Proof.context
+ val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
val report: Proof.context -> Markup.T -> Position.T -> unit
end;
@@ -25,7 +26,9 @@
val set_visible = Data.put;
val restore_visible = set_visible o is_visible;
-fun report ctxt markup pos =
- if is_visible ctxt then Position.report markup pos else ();
+fun report_text ctxt markup pos txt =
+ if is_visible ctxt then Position.report_text markup pos txt else ();
+
+fun report ctxt markup pos = report_text ctxt markup pos "";
end;
--- a/src/Pure/pure_setup.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Pure/pure_setup.ML Fri Aug 20 14:18:55 2010 +0200
@@ -18,8 +18,9 @@
(* ML toplevel pretty printing *)
-if String.isPrefix "smlnj" ml_system then ()
-else toplevel_pp ["String", "string"] "ML_Syntax.pretty_string";
+if String.isPrefix "polyml" ml_system
+then toplevel_pp ["String", "string"] "ML_Syntax.pretty_string"
+else ();
toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
@@ -39,15 +40,10 @@
toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
-if ml_system = "polyml-5.3.0"
-then use "ML/install_pp_polyml-5.3.ML"
-else if String.isPrefix "polyml" ml_system
+if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1"
then use "ML/install_pp_polyml.ML"
-else ();
-
-if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
- Secure.use_text ML_Parse.global_context (0, "") false
- "PolyML.Compiler.maxInlineSize := 20"
+else if String.isPrefix "polyml" ml_system
+then use "ML/install_pp_polyml-5.3.ML"
else ();
--- a/src/Tools/jEdit/src/jedit/document_model.scala Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Fri Aug 20 14:18:55 2010 +0200
@@ -279,7 +279,7 @@
for {
(command, command_start) <-
snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
- markup <- snapshot.state(command).highlight.flatten
+ markup <- snapshot.state(command).highlight
val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
if (abs_stop > start)
if (abs_start < stop)
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Fri Aug 20 14:15:29 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Fri Aug 20 14:18:55 2010 +0200
@@ -79,7 +79,7 @@
case Some((word, cs)) =>
val ds =
(if (Isabelle_Encoding.is_active(buffer))
- cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
+ cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
else cs).filter(_ != word)
if (ds.isEmpty) null
else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
@@ -129,7 +129,7 @@
val root = data.root
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??)
for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
- root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) =>
+ snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node) =>
{
val content = command.source(node.range).replace('\n', ' ')
val id = command.id
@@ -146,7 +146,7 @@
override def getEnd: Position = command_start + node.range.stop
override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
})
- }))
+ })
}
}
}
--- a/src/ZF/Datatype_ZF.thy Fri Aug 20 14:15:29 2010 +0200
+++ b/src/ZF/Datatype_ZF.thy Fri Aug 20 14:18:55 2010 +0200
@@ -61,7 +61,7 @@
struct
val trace = Unsynchronized.ref false;
- fun mk_new ([],[]) = Const("True",FOLogic.oT)
+ fun mk_new ([],[]) = Const(@{const_name True},FOLogic.oT)
| mk_new (largs,rargs) =
Balanced_Tree.make FOLogic.mk_conj
(map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
@@ -85,7 +85,7 @@
if #big_rec_name lcon_info = #big_rec_name rcon_info
andalso not (null (#free_iffs lcon_info)) then
if lname = rname then mk_new (largs, rargs)
- else Const("False",FOLogic.oT)
+ else Const(@{const_name False},FOLogic.oT)
else raise Match
val _ =
if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)
--- a/src/ZF/Tools/induct_tacs.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Fri Aug 20 14:18:55 2010 +0200
@@ -118,7 +118,7 @@
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
let
(*analyze the LHS of a case equation to get a constructor*)
- fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
+ fun const_of (Const(@{const_name "op ="}, _) $ (_ $ c) $ _) = c
| const_of eqn = error ("Ill-formed case equation: " ^
Syntax.string_of_term_global thy eqn);
--- a/src/ZF/Tools/inductive_package.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Fri Aug 20 14:18:55 2010 +0200
@@ -102,7 +102,7 @@
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
- fun dest_tprop (Const("Trueprop",_) $ P) = P
+ fun dest_tprop (Const(@{const_name Trueprop},_) $ P) = P
| dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
Syntax.string_of_term ctxt Q);
--- a/src/ZF/Tools/typechk.ML Fri Aug 20 14:15:29 2010 +0200
+++ b/src/ZF/Tools/typechk.ML Fri Aug 20 14:18:55 2010 +0200
@@ -75,7 +75,7 @@
if length rls <= maxr then resolve_tac rls i else no_tac
end);
-fun is_rigid_elem (Const("Trueprop",_) $ (Const(@{const_name mem},_) $ a $ _)) =
+fun is_rigid_elem (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) =
not (is_Var (head_of a))
| is_rigid_elem _ = false;