# HG changeset patch # User kleing # Date 1375368783 -7200 # Node ID 122416054a9ce78de45eb18151135fef67dfd981 # Parent 71fef62c4213132c420fa59645c0910a7ccd7547# Parent b7a83845bc93854f640b0bb7c8bc42b523a5a039 merged diff -r 71fef62c4213 -r 122416054a9c NEWS --- a/NEWS Thu Aug 01 16:52:28 2013 +0200 +++ b/NEWS Thu Aug 01 16:53:03 2013 +0200 @@ -43,11 +43,11 @@ *** Prover IDE -- Isabelle/Scala/jEdit *** -* Execution range of continuous document processing may be set to -"all", "none", "visible". See also dockable window "Theories" or -keyboard shortcuts "C-e BACK_SPACE" for "none", and "C-e SPACE" for -"visible". These declarative options supersede the old-style action -buttons "Cancel" and "Check". +* Improved "Theories" panel: Continuous checking of proof document +(visible and required parts) may be controlled explicitly, using check +box or shortcut "C+e ENTER". Individual theory nodes may be marked +explicitly as required and checked in full, using check box or +shortcut "C+e SPACE". * Strictly monotonic document update, without premature cancelation of running transactions that are still needed: avoid reset/restart of @@ -70,6 +70,12 @@ *** Pure *** +* Type theory is now immutable, without any special treatment of +drafts or linear updates (which could lead to "stale theory" errors in +the past). Discontinued obsolete operations like Theory.copy, +Theory.checkpoint, and the auxiliary type theory_ref. Minor +INCOMPATIBILITY. + * System option "proofs" has been discontinued. Instead the global state of Proofterm.proofs is persistently compiled into logic images as required, notably HOL-Proofs. Users no longer need to change diff -r 71fef62c4213 -r 122416054a9c doc/Contents --- a/doc/Contents Thu Aug 01 16:52:28 2013 +0200 +++ b/doc/Contents Thu Aug 01 16:53:03 2013 +0200 @@ -3,6 +3,7 @@ tutorial Tutorial on Isabelle/HOL locales Tutorial on Locales classes Tutorial on Type Classes + datatypes Tutorial on (Co)datatype Definitions functions Tutorial on Function Definitions codegen Tutorial on Code Generation nitpick User's Guide to Nitpick diff -r 71fef62c4213 -r 122416054a9c etc/options --- a/etc/options Thu Aug 01 16:52:28 2013 +0200 +++ b/etc/options Thu Aug 01 16:53:03 2013 +0200 @@ -123,11 +123,11 @@ public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" -option editor_execution_priority : int = -1 - -- "execution priority of main document structure (e.g. 0, -1, -2)" +public option editor_continuous_checking : bool = true + -- "continuous checking of proof document (visible and required parts)" -option editor_execution_range : string = "visible" - -- "execution range of continuous document processing: all, none, visible" +option editor_execution_delay : real = 0.02 + -- "delay for start of execution process after document update (seconds)" section "Miscellaneous Tools" diff -r 71fef62c4213 -r 122416054a9c etc/settings --- a/etc/settings Thu Aug 01 16:52:28 2013 +0200 +++ b/etc/settings Thu Aug 01 16:53:03 2013 +0200 @@ -8,7 +8,7 @@ # * DO NOT COPY this file into your ~/.isabelle directory! ### -### JVM components (Scala or Java) +### Isabelle/Scala ### ISABELLE_SCALA_BUILD_OPTIONS="-nowarn -target:jvm-1.5 -Xmax-classfile-name 130" @@ -41,9 +41,6 @@ ISABELLE_MAKEINDEX="makeindex" ISABELLE_EPSTOPDF="epstopdf" -# Paranoia setting for strange latex installations ... -#unset TEXMF - ### ### Misc path settings @@ -106,10 +103,6 @@ # DVI file viewer (command-line to eval) DVI_VIEWER=xdvi -#DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5" -#DVI_VIEWER="xdvi -geometry 711x1005 -expert -s 7" -#DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10" -#DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9" ### diff -r 71fef62c4213 -r 122416054a9c src/Doc/Datatypes/Datatypes.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Aug 01 16:53:03 2013 +0200 @@ -0,0 +1,610 @@ +(* Title: Doc/Datatypes/Datatypes.thy + Author: Jasmin Blanchette, TU Muenchen + +Tutorial for (co)datatype definitions with the new package. +*) + +theory Datatypes +imports Setup +begin + +section {* Introduction *} + +text {* +The 2013 edition of Isabelle introduced new definitional package for datatypes +and codatatypes. The datatype support is similar to that provided by the earlier +package due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL}; +indeed, replacing @{command datatype} by @{command datatype_new} is usually sufficient +to port existing specifications to the new package. What makes the new package +attractive is that it supports definitions with recursion through a large class +of non-datatypes, notably finite sets: +*} + + datatype_new 'a treeFS = TreeFS 'a "'a treeFS fset" + +text {* +\noindent +Another advantage of the new package is that it supports local definitions: +*} + + context linorder + begin + datatype_new flag = Less | Eq | Greater + end + +text {* +\noindent +Finally, the package also provides some convenience, notably automatically +generated destructors. + +The command @{command datatype_new} is expected to displace @{command datatype} in a future +release. Authors of new theories are encouraged to use @{command datatype_new}, and +maintainers of older theories may want to consider upgrading in the coming months. + +The package also provides codatatypes (or ``coinductive datatypes''), which may +have infinite values. The following command introduces a codatatype of infinite +streams: +*} + + codatatype 'a stream = Stream 'a "'a stream" + +text {* +\noindent +Mixed inductive--coinductive recursion is possible via nesting. +Compare the following four examples: +*} + + datatype_new 'a treeFF = TreeFF 'a "'a treeFF list" + datatype_new 'a treeFI = TreeFI 'a "'a treeFF stream" + codatatype 'a treeIF = TreeIF 'a "'a treeFF list" + codatatype 'a treeII = TreeII 'a "'a treeFF stream" + +text {* +To use the package, it is necessary to import the @{theory BNF} theory, which +can be precompiled as the \textit{HOL-BNF} image. The following commands show +how to launch jEdit/PIDE with the image loaded and how to build the image +without launching jEdit: +*} + +text {* +\noindent +\ \ \ \ \texttt{isabelle jedit -l HOL-BNF} \\ +\ \ \ \ \texttt{isabelle build -b HOL-BNF} +*} + +text {* +The package, like its predecessor, fully adheres to the LCF philosophy +\cite{mgordon79}: The characteristic theorems associated with the specified +(co)datatypes are derived rather than introduced axiomatically.% +\footnote{Nonetheless, if the \textit{quick\_and\_dirty} option is enabled, some +of the internal constructions and most of the internal proof obligations are +skipped.} +The package's metatheory is described in a pair of papers +\cite{traytel-et-al-2012,blanchette-et-al-wit}. +*} + +text {* +This tutorial is organized as follows: + +\begin{itemize} +\setlength{\itemsep}{0pt} + +\item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,'' +describes how to specify datatypes using the @{command datatype_new} command. + +\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive +Functions,'' describes how to specify recursive functions using +\keyw{primrec\_new}, @{command fun}, and @{command function}. + +\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,'' +describes how to specify codatatypes using the @{command codatatype} command. + +\item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive +Functions,'' describes how to specify corecursive functions using the +\keyw{primcorec} command. + +\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering +Bounded Natural Functors,'' explains how to set up the (co)datatype package to +allow nested recursion through custom well-behaved type constructors. + +\item Section \ref{sec:generating-free-constructor-theorems}, ``Generating Free +Constructor Theorems,'' explains how to derive convenience theorems for free +constructors, as performed internally by @{command datatype_new} and +@{command codatatype}. + +\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,'' +describes the package's programmatic interface. + +\item Section \ref{sec:interoperability}, ``Interoperability,'' +is concerned with the packages' interaction with other Isabelle packages and +tools, such as the code generator and the counterexample generators. + +\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and +Limitations,'' concludes with known open issues at the time of writing. +\end{itemize} + + +\newbox\boxA +\setbox\boxA=\hbox{\texttt{nospam}} + +\newcommand\authoremaili{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak +in.\allowbreak tum.\allowbreak de}} +\newcommand\authoremailii{\texttt{pope{\color{white}nospam}\kern-\wd\boxA{}scua@\allowbreak +in.\allowbreak tum.\allowbreak de}} +\newcommand\authoremailiii{\texttt{tray{\color{white}nospam}\kern-\wd\boxA{}tel@\allowbreak +in.\allowbreak tum.\allowbreak de}} + +\noindent +Comments and bug reports concerning either +the tool or the manual should be directed to the authors at +\authoremaili, \authoremailii, and \authoremailiii. + +\begin{framed} +\noindent +\textbf{Warning:} This document is under heavy construction. Please apologise +for its appearance and come back in a few months. +\end{framed} + +*} + +section {* Defining Datatypes% + \label{sec:defining-datatypes} *} + +text {* +This section describes how to specify datatypes using the @{command datatype_new} +command. The command is first illustrated through concrete examples featuring +different flavors of recursion. More examples can be found in the directory +\verb|~~/src/HOL/BNF/Examples|. +*} + + +subsection {* Introductory Examples *} + +subsubsection {* Nonrecursive Types *} + +text {* +enumeration type: +*} + + datatype_new trool = Truue | Faalse | Maaybe + +text {* +Haskell-style option type: +*} + + datatype_new 'a maybe = Nothing | Just 'a + +text {* +triple: +*} + + datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c + + +subsubsection {* Simple Recursion *} + +text {* +simplest recursive type: natural numbers +*} + + datatype_new nat = Zero | Suc nat + +text {* +lists were shown in the introduction + +terminated lists are a variant: +*} + + datatype_new ('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist" + +text {* +On the right-hand side of the equal sign, the usual Isabelle conventions apply: +Nonatomic types must be enclosed in double quotes. +*} + + +subsubsection {* Mutual Recursion *} + +text {* +Mutual recursion = Define several types simultaneously, referring to each other. + +Simple example: distinction between even and odd natural numbers: +*} + + datatype_new even_nat = Zero | Even_Suc odd_nat + and odd_nat = Odd_Suc even_nat + +text {* +More complex, and more realistic, example: +*} + + datatype_new ('a, 'b) expr = + Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) expr" + and ('a, 'b) trm = + Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" + and ('a, 'b) factor = + Const 'a | Var 'b | Sub_Expr "('a, 'b) expr" + + +subsubsection {* Nested Recursion *} + +text {* +Nested recursion = Have recursion through a type constructor. + +The introduction showed some examples of trees with nesting through lists. + +More complex example, which reuses our maybe and triple types: +*} + + datatype_new 'a triple_tree = + Triple_Tree "('a triple_tree maybe, bool, 'a triple_tree maybe) triple" + +text {* +Recursion may not be arbitrary; e.g. impossible to define +*} + +(* + datatype_new 'a foo = Foo (*<*) datatype_new 'a bar = Bar "'a foo \ 'a foo" +*) + + datatype_new 'a evil = Evil (*<*)'a + typ (*>*)"'a evil \ 'a evil" + +text {* +Issue: => allows recursion only on its right-hand side. +This issue is inherited by polymorphic datatypes (and codatatypes) +defined in terms of =>. +In general, type constructors "('a1, ..., 'an) k" allow recursion on a subset +of their type arguments. +*} + + +subsubsection {* Auxiliary Constants and Syntaxes *} + +text {* +The @{command datatype_new} command introduces various constants in addition to the +constructors. Given a type @{text "('a1,\,'aM) t"} with constructors +@{text t.C1}, \ldots, @{text t.C}$\!M,$ the following auxiliary constants are +introduced (among others): + +\begin{itemize} +\setlength{\itemsep}{0pt} + +\item \emph{Set functions} (\emph{natural transformations}): @{text t_set1}, +\ldots, @{text t_set}$M$ + +\item \emph{Map function} (\emph{functorial action}): @{text t_map} + +\item \emph{Relator}: @{text t_rel} + +\item \emph{Iterator}: @{text t_fold} + +\item \emph{Recursor}: @{text t_rec} + +\item \emph{Discriminators}: @{text t.is_C1}, \ldots, @{text t.is_C}$\!M$ + +\item \emph{Selectors}: +@{text t.un_C11}, \ldots, @{text t.un_C1}$k_1$, \ldots, +@{text t.un_C}$\!M$@{text 1}, \ldots, @{text t.un_C}$\!Mk_M$ +\end{itemize} + +The discriminators and selectors are collectively called \emph{destructors}. +The @{text "t."} prefix is optional. + +The set functions, map function, relator, discriminators, and selectors can be +given custom names, as in the example below: +*} + +(*<*)hide_const Nil Cons hd tl(*>*) + datatype_new (set: 'a) list (map: map rel: list_all2) = + null: Nil (defaults tl: Nil) + | Cons (hd: 'a) (tl: "'a list") + +text {* +\noindent +The command introduces a discriminator @{const null} and a pair of selectors +@{const hd} and @{const tl} characterized as follows: +% +\[@{thm list.collapse(1)[of xs, no_vars]} + \qquad @{thm list.collapse(2)[of xs, no_vars]}\] +% +For two-constructor datatypes, a single discriminator constant suffices. The +discriminator associated with @{const Cons} is simply @{text "\ null"}. + +The \keyw{defaults} keyword following the @{const Nil} constructor specifies a +default value for selectors associated with other constructors. Here, it is +used to specify that the tail of the empty list is the empty list (instead of +being unspecified). + +Because @{const Nil} is a nullary constructor, it is also possible to use @{text +"= Nil"} as a discriminator. This is specified by specifying @{text "="} instead +of the identifier @{const null} in the declaration above. Although this may look +appealing, the mixture of constructors and selectors in the resulting +characteristic theorems can lead Isabelle's automation to switch between the +constructor and the destructor view in surprising ways. +*} + +text {* +The usual mixfix syntaxes are available for both types and constructors. For example: + +%%% FIXME: remove trailing underscore and use locale trick instead once this is +%%% supported. +*} + + datatype_new ('a, 'b) prod (infixr "*" 20) = + Pair 'a 'b + + datatype_new (set_: 'a) list_ = + null: Nil ("[]") + | Cons (hd: 'a) (tl: "'a list_") (infixr "#" 65) + + +subsection {* General Syntax *} + +text {* +Datatype definitions have the following general syntax: + +@{rail " + @@{command datatype_new} ('(' (@{syntax dt_option} + ',') ')')? \\ + (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and') +"} + +Two options are supported: + +@{rail " + @{syntax_def dt_option}: @'no_dests' | @'rep_compat' +"} + +\begin{itemize} +\setlength{\itemsep}{0pt} + +\item +The \keyw{no\_dests} option indicates that no destructors (i.e., +discriminators and selectors) should be generated. + +\item +The \keyw{rep\_compat} option indicates that the names generated by the +package should contain optional (and normally not displayed) @{text "new."} +components to prevent clashes with a later call to @{command rep_datatype}. See +Section~\ref{ssec:datatype-compatibility-issues} for details. +\end{itemize} + +Left-hand sides specify the name of the type to define, its type parameters, +and more: + +@{rail " + @{syntax_def dt_name}: @{syntax type_params}? @{syntax name} \\ + @{syntax map_rel}? @{syntax mixfix}? + ; + @{syntax_def type_params}: @{syntax typefree} | '(' ((@{syntax name} ':')? @{syntax typefree} + ',') ')' + ; + @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' @{syntax name}) +) ')' +"} + +@{syntax name} specifies the type name ... + +@{syntax typefree} is type variable ('a, 'b, \ldots) +The names are for the set functions. + +Additional constraint: All mutually recursive datatypes defined together must +specify the same type variables in the same order. + +@{syntax mixfix} is the usual parenthesized mixfix notation, documented in the +Isar reference manual \cite{isabelle-isar-ref}. + +@{rail " + @{syntax_def ctor}: (@{syntax name} ':')? @{syntax name} (@{syntax ctor_arg} *) \\ + @{syntax sel_defaults}? @{syntax mixfix}? +"} + + +First, optional name: discriminator. Second, mandatory name: name of +constructor. Default names for discriminators are generated. + +@{rail " + @{syntax_def ctor_arg}: @{syntax type} | '(' (@{syntax name} ':')? @{syntax type} ')' + ; + @{syntax_def sel_defaults}: '(' @'defaults' (@{syntax name} ':' @{syntax term} *) ')' +"} +*} + + +subsection {* Characteristic Theorems *} + + +subsection {* Compatibility Issues% + \label{ssec:datatype-compatibility-issues} *} + + +section {* Defining Recursive Functions% + \label{sec:defining-recursive-functions} *} + +text {* +This describes how to specify recursive functions over datatypes +specified using @{command datatype_new}. The focus in on the \keyw{primrec\_new} +command, which supports primitive recursion. A few examples feature the +@{command fun} and @{command function} commands, described in a separate +tutorial \cite{isabelle-function}. +%%% TODO: partial_function? +*} + + +subsection {* Introductory Examples *} + +text {* +More examples in \verb|~~/src/HOL/BNF/Examples|. +*} + + +subsection {* General Syntax *} + + +subsection {* Characteristic Theorems *} + + +subsection {* Compatibility Issues *} + + +section {* Defining Codatatypes% + \label{sec:defining-codatatypes} *} + +text {* +This section describes how to specify codatatypes using the @{command codatatype} +command. +*} + + +subsection {* Introductory Examples *} + +text {* +More examples in \verb|~~/src/HOL/BNF/Examples|. +*} + + +subsection {* General Syntax *} + +text {* +\keyw{no\_dests} is not available. +*} + +subsection {* Characteristic Theorems *} + + +section {* Defining Corecursive Functions% + \label{sec:defining-corecursive-functions} *} + +text {* +This section describes how to specify corecursive functions using the +\keyw{primcorec} command. +*} + + +subsection {* Introductory Examples *} + +text {* +More examples in \verb|~~/src/HOL/BNF/Examples|. +*} + + +subsection {* General Syntax *} + + +subsection {* Characteristic Theorems *} + + +section {* Registering Bounded Natural Functors% + \label{sec:registering-bounded-natural-functors} *} + +text {* +This section explains how to set up the (co)datatype package to allow nested +recursion through custom well-behaved type constructors. The key concept is that +of a bounded natural functor (BNF). +*} + + +subsection {* Introductory Example *} + +text {* +More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and +\verb|~~/src/HOL/BNF/More_BNFs.thy|. + +Mention distinction between live and dead type arguments; +mention =>. +*} + + +subsection {* General Syntax *} + + +section {* Generating Free Constructor Theorems% + \label{sec:generating-free-constructor-theorems} *} + +text {* +This section explains how to derive convenience theorems for free constructors, +as performed internally by @{command datatype_new} and @{command codatatype}. + + * need for this is rare but may arise if you want e.g. to add destructors to + a type not introduced by ... + + * also useful for compatibility with old package, e.g. add destructors to + old @{command datatype} +*} + + +subsection {* Introductory Example *} + + +subsection {* General Syntax *} + + +section {* Standard ML Interface% + \label{sec:standard-ml-interface} *} + +text {* +This section describes the package's programmatic interface. +*} + + +section {* Interoperability% + \label{sec:interoperability} *} + +text {* +This section is concerned with the packages' interaction with other Isabelle +packages and tools, such as the code generator and the counterexample +generators. +*} + + +subsection {* Transfer and Lifting *} + + +subsection {* Code Generator *} + + +subsection {* Quickcheck *} + + +subsection {* Nitpick *} + + +subsection {* Nominal Isabelle *} + + +section {* Known Bugs and Limitations% + \label{sec:known-bugs-and-limitations} *} + +text {* +This section lists known open issues of the package. +*} + +text {* +* primrec\_new and primcorec are vaporware + +* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting) + +* issues with HOL-Proofs? + +* partial documentation + +* too much output by commands like "datatype_new" and "codatatype" + +* no direct way to define recursive functions for default values -- but show trick + based on overloading +*} + + +section {* Acknowledgments% + \label{sec:acknowledgments} *} + +text {* + * same people as usual + * Tobias Nipkow + * Makarius Wenzel + * Andreas Lochbihler + * Brian Huffman + * also: + * Stefan Milius + * Lutz Schr\"oder +*} + +end diff -r 71fef62c4213 -r 122416054a9c src/Doc/Datatypes/Setup.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Datatypes/Setup.thy Thu Aug 01 16:53:03 2013 +0200 @@ -0,0 +1,9 @@ +theory Setup +imports BNF +begin + +ML_file "../antiquote_setup.ML" + +setup Antiquote_Setup.setup + +end diff -r 71fef62c4213 -r 122416054a9c src/Doc/Datatypes/document/build --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Datatypes/document/build Thu Aug 01 16:53:03 2013 +0200 @@ -0,0 +1,14 @@ +#!/bin/bash + +set -e + +FORMAT="$1" +VARIANT="$2" + +cp "$ISABELLE_HOME/src/Doc/iman.sty" . +cp "$ISABELLE_HOME/src/Doc/extra.sty" . +cp "$ISABELLE_HOME/src/Doc/isar.sty" . +cp "$ISABELLE_HOME/src/Doc/manual.bib" . + +"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" + diff -r 71fef62c4213 -r 122416054a9c src/Doc/Datatypes/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Datatypes/document/root.tex Thu Aug 01 16:53:03 2013 +0200 @@ -0,0 +1,62 @@ +\documentclass[12pt,a4paper]{article} % fleqn +\usepackage{cite} +\usepackage{enumitem} +\usepackage{latexsym} +\usepackage{graphicx} +\usepackage{iman} +\usepackage{extra} +\usepackage{isar} +\usepackage{isabelle} +\usepackage{isabellesym} +\usepackage{style} +\usepackage{pdfsetup} +\usepackage{railsetup} +\usepackage{framed} + +\newbox\boxA +\setbox\boxA=\hbox{\ } +\parindent=4\wd\boxA + +\newcommand{\keyw}[1]{\isacommand{#1}} + +\renewcommand{\isacharprime}{\isamath{{'}\mskip-2mu}} +\renewcommand{\isacharunderscore}{\mbox{\_}} +\renewcommand{\isacharunderscorekeyword}{\mbox{\_}} +\renewcommand{\isachardoublequote}{\mbox{\upshape{``}}} +\renewcommand{\isachardoublequoteopen}{\mbox{\upshape{``}\,}} +\renewcommand{\isachardoublequoteclose}{\mbox{\,\upshape{''}}} + +\hyphenation{isa-belle} + +\isadroptag{theory} + +\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] +Defining (Co)datatypes in Isabelle/HOL} +\author{\hbox{} \\ +Jasmin Christian Blanchette \\ +Andrei Popescu \\ +Dmitriy Traytel \\ +{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\ +\hbox{}} +\begin{document} + +\maketitle + +\begin{abstract} +\noindent +This tutorial describes how to use the new package for defining datatypes and +codatatypes in Isabelle/HOL. The package provides four main user-level commands: +\keyw{datatype\_new}, \keyw{codatatype}, \keyw{primrec\_new}, and \keyw{primcorec}. +The commands suffixed by \keyw{\_new} are intended to subsume, and eventually +replace, the corresponding commands from the old datatype package. +\end{abstract} + +\tableofcontents + +\input{Datatypes.tex} + +\let\em=\sl +\bibliography{manual}{} +\bibliographystyle{abbrv} + +\end{document} diff -r 71fef62c4213 -r 122416054a9c src/Doc/Datatypes/document/style.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Datatypes/document/style.sty Thu Aug 01 16:53:03 2013 +0200 @@ -0,0 +1,58 @@ + +%% toc +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} +\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}} + +%% paragraphs +\setlength{\parindent}{1em} + +%% references +\newcommand{\secref}[1]{\S\ref{#1}} +\newcommand{\figref}[1]{figure~\ref{#1}} + +%% logical markup +\newcommand{\strong}[1]{{\bfseries {#1}}} +\newcommand{\qn}[1]{\emph{#1}} + +%% typographic conventions +\newcommand{\qt}[1]{``{#1}''} +\newcommand{\ditem}[1]{\item[\isastyletext #1]} + +%% quote environment +\isakeeptag{quote} +\renewenvironment{quote} + {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax} + {\endlist} +\renewcommand{\isatagquote}{\begin{quote}} +\renewcommand{\endisatagquote}{\end{quote}} +\newcommand{\quotebreak}{\\[1.2ex]} + +%% typewriter text +\newenvironment{typewriter}{\renewcommand{\isastyletext}{}% +\renewcommand{\isadigit}[1]{{##1}}% +\parindent0pt% +\makeatletter\isa@parindent0pt\makeatother% +\isabellestyle{tt}\isastyle% +\fontsize{9pt}{9pt}\selectfont}{} + +\isakeeptag{quotetypewriter} +\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}} +\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}} + +%% presentation +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} + +%% character detail +\renewcommand{\isadigit}[1]{\isamath{#1}} +\binperiod +\underscoreoff + +%% format +\pagestyle{headings} +\isabellestyle{it} + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "implementation" +%%% End: diff -r 71fef62c4213 -r 122416054a9c src/Doc/Functions/document/root.tex --- a/src/Doc/Functions/document/root.tex Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Doc/Functions/document/root.tex Thu Aug 01 16:53:03 2013 +0200 @@ -59,7 +59,7 @@ \maketitle \begin{abstract} - This tutorial describes the use of the new \emph{function} package, + This tutorial describes the use of the \emph{function} package, which provides general recursive function definitions for Isabelle/HOL. We start with very simple examples and then gradually move on to more advanced topics such as manual termination proofs, nested recursion, diff -r 71fef62c4213 -r 122416054a9c src/Doc/IsarImplementation/Integration.thy --- a/src/Doc/IsarImplementation/Integration.thy Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Doc/IsarImplementation/Integration.thy Thu Aug 01 16:53:03 2013 +0200 @@ -22,13 +22,7 @@ \medskip The toplevel maintains an implicit state, which is transformed by a sequence of transitions -- either interactively or - in batch-mode. In interactive mode, Isar state transitions are - encapsulated as safe transactions, such that both failure and undo - are handled conveniently without destroying the underlying draft - theory (cf.~\secref{sec:context-theory}). In batch mode, - transitions operate in a linear (destructive) fashion, such that - error conditions abort the present attempt to construct a theory or - proof altogether. + in batch-mode. The toplevel state is a disjoint sum of empty @{text toplevel}, or @{text theory}, or @{text proof}. On entering the main Isar loop we diff -r 71fef62c4213 -r 122416054a9c src/Doc/IsarImplementation/Logic.thy --- a/src/Doc/IsarImplementation/Logic.thy Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Doc/IsarImplementation/Logic.thy Thu Aug 01 16:53:03 2013 +0200 @@ -718,8 +718,8 @@ \item Type @{ML_type thm} represents proven propositions. This is an abstract datatype that guarantees that its values have been constructed by basic principles of the @{ML_struct Thm} module. - Every @{ML_type thm} value contains a sliding back-reference to the - enclosing theory, cf.\ \secref{sec:context-theory}. + Every @{ML_type thm} value refers its background theory, + cf.\ \secref{sec:context-theory}. \item @{ML Thm.transfer}~@{text "thy thm"} transfers the given theorem to a \emph{larger} theory, see also \secref{sec:context}. diff -r 71fef62c4213 -r 122416054a9c src/Doc/IsarImplementation/Prelim.thy --- a/src/Doc/IsarImplementation/Prelim.thy Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Doc/IsarImplementation/Prelim.thy Thu Aug 01 16:53:03 2013 +0200 @@ -80,24 +80,6 @@ ancestor theories. To this end, the system maintains a set of symbolic ``identification stamps'' within each theory. - In order to avoid the full-scale overhead of explicit sub-theory - identification of arbitrary intermediate stages, a theory is - switched into @{text "draft"} mode under certain circumstances. A - draft theory acts like a linear type, where updates invalidate - earlier versions. An invalidated draft is called \emph{stale}. - - The @{text "checkpoint"} operation produces a safe stepping stone - that will survive the next update without becoming stale: both the - old and the new theory remain valid and are related by the - sub-theory relation. Checkpointing essentially recovers purely - functional theory values, at the expense of some extra internal - bookkeeping. - - The @{text "copy"} operation produces an auxiliary version that has - the same data content, but is unrelated to the original: updates of - the copy do not affect the original, neither does the sub-theory - relation hold. - The @{text "merge"} operation produces the least upper bound of two theories, which actually degenerates into absorption of one theory into the other (according to the nominal sub-theory relation). @@ -110,10 +92,8 @@ \medskip The example in \figref{fig:ex-theory} below shows a theory graph derived from @{text "Pure"}, with theory @{text "Length"} importing @{text "Nat"} and @{text "List"}. The body of @{text - "Length"} consists of a sequence of updates, working mostly on - drafts internally, while transaction boundaries of Isar top-level - commands (\secref{sec:isar-toplevel}) are guaranteed to be safe - checkpoints. + "Length"} consists of a sequence of updates, resulting in locally a + linear sub-theory relation for each intermediate step. \begin{figure}[htb] \begin{center} @@ -125,56 +105,33 @@ @{text "Nat"} & & & & @{text "List"} \\ & $\searrow$ & & $\swarrow$ \\ & & @{text "Length"} \\ - & & \multicolumn{3}{l}{~~@{keyword "imports"}} \\ & & \multicolumn{3}{l}{~~@{keyword "begin"}} \\ & & $\vdots$~~ \\ - & & @{text "\"}~~ \\ - & & $\vdots$~~ \\ - & & @{text "\"}~~ \\ - & & $\vdots$~~ \\ & & \multicolumn{3}{l}{~~@{command "end"}} \\ \end{tabular} \caption{A theory definition depending on ancestors}\label{fig:ex-theory} \end{center} \end{figure} - \medskip There is a separate notion of \emph{theory reference} for - maintaining a live link to an evolving theory context: updates on - drafts are propagated automatically. Dynamic updating stops when - the next @{text "checkpoint"} is reached. - - Derived entities may store a theory reference in order to indicate - the formal context from which they are derived. This implicitly - assumes monotonic reasoning, because the referenced context may - become larger without further notice. -*} + \medskip Derived formal entities may retain a reference to the + background theory in order to indicate the formal context from which + they were produced. This provides an immutable certificate of the + background theory. *} text %mlref {* \begin{mldecls} @{index_ML_type theory} \\ @{index_ML Theory.eq_thy: "theory * theory -> bool"} \\ @{index_ML Theory.subthy: "theory * theory -> bool"} \\ - @{index_ML Theory.checkpoint: "theory -> theory"} \\ - @{index_ML Theory.copy: "theory -> theory"} \\ @{index_ML Theory.merge: "theory * theory -> theory"} \\ @{index_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\ @{index_ML Theory.parents_of: "theory -> theory list"} \\ @{index_ML Theory.ancestors_of: "theory -> theory list"} \\ \end{mldecls} - \begin{mldecls} - @{index_ML_type theory_ref} \\ - @{index_ML Theory.deref: "theory_ref -> theory"} \\ - @{index_ML Theory.check_thy: "theory -> theory_ref"} \\ - \end{mldecls} \begin{description} - \item Type @{ML_type theory} represents theory contexts. This is - essentially a linear type, with explicit runtime checking. - Primitive theory operations destroy the original version, which then - becomes ``stale''. This can be prevented by explicit checkpointing, - which the system does at least at the boundary of toplevel command - transactions \secref{sec:isar-toplevel}. + \item Type @{ML_type theory} represents theory contexts. \item @{ML "Theory.eq_thy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} check strict identity of two theories. @@ -185,18 +142,9 @@ (@{text "\"}) of the corresponding content (according to the semantics of the ML modules that implement the data). - \item @{ML "Theory.checkpoint"}~@{text "thy"} produces a safe - stepping stone in the linear development of @{text "thy"}. This - changes the old theory, but the next update will result in two - related, valid theories. - - \item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text - "thy"} with the same data. The copy is not related to the original, - but the original is unchanged. - \item @{ML "Theory.merge"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} absorbs one theory - into the other, without changing @{text "thy\<^sub>1"} or @{text "thy\<^sub>2"}. - This version of ad-hoc theory merge fails for unrelated theories! + into the other. This version of ad-hoc theory merge fails for + unrelated theories! \item @{ML "Theory.begin_theory"}~@{text "name parents"} constructs a new theory based on the given parents. This ML function is @@ -208,18 +156,6 @@ \item @{ML "Theory.ancestors_of"}~@{text "thy"} returns all ancestors of @{text thy} (not including @{text thy} itself). - \item Type @{ML_type theory_ref} represents a sliding reference to - an always valid theory; updates on the original are propagated - automatically. - - \item @{ML "Theory.deref"}~@{text "thy_ref"} turns a @{ML_type - "theory_ref"} into an @{ML_type "theory"} value. As the referenced - theory evolves monotonically over time, later invocations of @{ML - "Theory.deref"} may refer to a larger context. - - \item @{ML "Theory.check_thy"}~@{text "thy"} produces a @{ML_type - "theory_ref"} from a valid @{ML_type "theory"} value. - \end{description} *} @@ -254,13 +190,11 @@ subsection {* Proof context \label{sec:context-proof} *} -text {* A proof context is a container for pure data with a - back-reference to the theory from which it is derived. The @{text - "init"} operation creates a proof context from a given theory. - Modifications to draft theories are propagated to the proof context - as usual, but there is also an explicit @{text "transfer"} operation - to force resynchronization with more substantial updates to the - underlying theory. +text {* A proof context is a container for pure data that refers to + the theory from which it is derived. The @{text "init"} operation + creates a proof context from a given theory. There is an explicit + @{text "transfer"} operation to force resynchronization with updates + to the background theory -- this is rarely required in practice. Entities derived in a proof context need to record logical requirements explicitly, since there is no separate context @@ -293,15 +227,12 @@ \begin{description} \item Type @{ML_type Proof.context} represents proof contexts. - Elements of this type are essentially pure values, with a sliding - reference to the background theory. - \item @{ML Proof_Context.init_global}~@{text "thy"} produces a proof context - derived from @{text "thy"}, initializing all data. + \item @{ML Proof_Context.init_global}~@{text "thy"} produces a proof + context derived from @{text "thy"}, initializing all data. \item @{ML Proof_Context.theory_of}~@{text "ctxt"} selects the - background theory from @{text "ctxt"}, dereferencing its internal - @{ML_type theory_ref}. + background theory from @{text "ctxt"}. \item @{ML Proof_Context.transfer}~@{text "thy ctxt"} promotes the background theory of @{text "ctxt"} to the super theory @{text diff -r 71fef62c4213 -r 122416054a9c src/Doc/IsarImplementation/Tactic.thy --- a/src/Doc/IsarImplementation/Tactic.thy Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Doc/IsarImplementation/Tactic.thy Thu Aug 01 16:53:03 2013 +0200 @@ -509,7 +509,7 @@ regarded as an atomic formula, to solve premise @{text "i"} of @{text "thm\<^sub>2"}. Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text "\"} and @{text "\\<^sub>1 \ \ \\<^sub>n \ \"}. The unique @{text "s"} that - unifies @{text "\"} and @{text "\"} yields the theorem @{text "(\\<^sub>1 \ + unifies @{text "\"} and @{text "\\<^isub>i"} yields the theorem @{text "(\\<^sub>1 \ \ \\<^sub>i\<^sub>-\<^sub>1 \ \\<^sub>i\<^sub>+\<^sub>1 \ \ \\<^sub>n \ \)s"}. Multiple results are considered as error (exception @{ML THM}). diff -r 71fef62c4213 -r 122416054a9c src/Doc/ProgProve/document/intro-isabelle.tex --- a/src/Doc/ProgProve/document/intro-isabelle.tex Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Doc/ProgProve/document/intro-isabelle.tex Thu Aug 01 16:53:03 2013 +0200 @@ -51,7 +51,29 @@ %This introduction to Isabelle has grown out of many years of teaching %Isabelle courses. -\ifsem\else +\ifsem +\subsection*{Getting Started with Isabelle} + +If you have not done so already, download and install Isabelle +from \url{http://isabelle.in.tum.de}. You can start it by clicking +on the application icon. This will launch Isabelle's +user interface based on the text editor \concept{jedit}. Below you see +a typical example snapshot of a jedit session. At this point we merely explain +the layout of the window, not its contents. + +\begin{center} +\includegraphics[width=\textwidth]{jedit.png} +\end{center} +The upper part of the window shows the input typed by the user, i.e.\ the +gradually growing Isabelle text of definitions, theorems, proofs, etc. The +interface processes the user input automatically while it is typed, just like +modern Java IDEs. Isabelle's response to the user input is shown in the +lower part of the window. You can examine the response to any input phrase +by clicking on that phrase or by hovering over underlined text. + +This should suffice to get started with the jedit interface. +Now you need to learn what to type into it. +\else If you want to apply what you have learned about Isabelle we recommend you donwload and read the book \href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete @@ -64,6 +86,9 @@ Proving in Isabelle/HOL}. \fi +\ifsem\else \paragraph{Acknowledgements} -\ifsem We \else I \fi wish to thank the following people for their comments: -Florian Haftmann, Ren\'{e} Thiemann and Christian Sternagel. \ No newline at end of file +I wish to thank the following people for their comments +on this document: +Florian Haftmann, Ren\'{e} Thiemann and Christian Sternagel. +\fi \ No newline at end of file diff -r 71fef62c4213 -r 122416054a9c src/Doc/ROOT --- a/src/Doc/ROOT Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Doc/ROOT Thu Aug 01 16:53:03 2013 +0200 @@ -37,6 +37,21 @@ "document/root.tex" "document/style.sty" +session Datatypes (doc) in "Datatypes" = "HOL-BNF" + + options [document_variants = "datatypes"] + theories [document = false] Setup + theories Datatypes + files + "../prepare_document" + "../pdfsetup.sty" + "../iman.sty" + "../extra.sty" + "../isar.sty" + "../manual.bib" + "document/build" + "document/root.tex" + "document/style.sty" + session Functions (doc) in "Functions" = HOL + options [document_variants = "functions", skip_proofs = false] theories Functions diff -r 71fef62c4213 -r 122416054a9c src/Doc/manual.bib --- a/src/Doc/manual.bib Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Doc/manual.bib Thu Aug 01 16:53:03 2013 +0200 @@ -301,6 +301,12 @@ author = "Jasmin Christian Blanchette and Tobias Nipkow", crossref = {itp2010}} +@unpublished{blanchette-et-al-wit, + author = {J.C. Blanchette and A. Popescu and D. Traytel}, + title = {Witnessing (Co)datatypes}, + year = 2013, + note = {\url{http://www21.in.tum.de/~traytel/papers/witness/wit.pdf}}} + @inproceedings{why3, author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich}, title = {{Why3}: Shepherd Your Herd of Provers}, @@ -1662,7 +1668,16 @@ Subtyping (long version)}, year = 2011, note = {Submitted, - \url{http://isabelle.in.tum.de/doc/implementation.pdf}}}, + \url{http://isabelle.in.tum.de/doc/implementation.pdf}}} + +@inproceedings{traytel-et-al-2012, + author = "Dmitriy Traytel and Andrei Popescu and Jasmin Christian Blanchette", + title = {Foundational, Compositional (Co)datatypes for Higher-Order + Logic---{C}ategory Theory Applied to Theorem Proving}, + year = {2012}, + pages = {596--605}, + booktitle = {LICS 2012}, + publisher = {IEEE} } @Unpublished{Trybulec:1993:MizarFeatures, diff -r 71fef62c4213 -r 122416054a9c src/HOL/BNF/Examples/Misc_Data.thy --- a/src/HOL/BNF/Examples/Misc_Data.thy Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/BNF/Examples/Misc_Data.thy Thu Aug 01 16:53:03 2013 +0200 @@ -150,6 +150,8 @@ and s8 = S8 nat *) +datatype_new 'a deadbar = DeadBar "'a \ 'a" +datatype_new 'a deadbar_option = DeadBarOption "'a option \ 'a option" datatype_new ('a, 'b) bar = Bar "'b \ 'a" datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \ 'c + 'a" diff -r 71fef62c4213 -r 122416054a9c src/HOL/BNF/README.html --- a/src/HOL/BNF/README.html Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/BNF/README.html Thu Aug 01 16:53:03 2013 +0200 @@ -23,7 +23,7 @@ The package is described in the following paper: diff -r 71fef62c4213 -r 122416054a9c src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Aug 01 16:53:03 2013 +0200 @@ -42,7 +42,7 @@ (((bool * bool) * term list) * term) * (binding list * (binding list list * (binding * term) list list)) -> local_theory -> ctr_sugar * local_theory - val parse_wrap_options: (bool * bool) parser + val parse_wrap_free_constructors_options: (bool * bool) parser val parse_bound_term: (binding * string) parser end; @@ -753,7 +753,7 @@ val parse_bound_terms = parse_bracket_list parse_bound_term; val parse_bound_termss = parse_bracket_list parse_bound_terms; -val parse_wrap_options = +val parse_wrap_free_constructors_options = Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_dests"} >> K (true, false)) || (@{keyword "rep_compat"} >> K (false, true))) --| @{keyword ")"} >> (pairself (exists I) o split_list)) (false, false); @@ -761,7 +761,8 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"} "wrap an existing freely generated type's constructors" - ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- + ((parse_wrap_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --| + @{keyword "]"}) -- Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss -- Scan.optional parse_bound_termss []) ([], [])) ([], ([], []))) >> wrap_free_constructors_cmd); diff -r 71fef62c4213 -r 122416054a9c src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Aug 01 16:53:03 2013 +0200 @@ -1009,17 +1009,34 @@ fun mk_in_bd () = let + val bdT = fst (dest_relT (fastype_of bnf_bd_As)); + val bdTs = replicate live bdT; + val bd_bnfT = mk_bnf_T bdTs CA; + val surj_imp_ordLeq_inst = (if live = 0 then TrueI else + let + val ranTs = map (fn AT => mk_sumT (AT, HOLogic.unitT)) As'; + val funTs = map (fn T => bdT --> T) ranTs; + val ran_bnfT = mk_bnf_T ranTs CA; + val (revTs, Ts) = `rev (bd_bnfT :: funTs); + val cTs = map (SOME o certifyT lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts]; + val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs) + (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs, + map Bound (live - 1 downto 0)) $ Bound live)); + val cts = [NONE, SOME (certify lthy tinst)]; + in + Drule.instantiate' cTs cts @{thm surj_imp_ordLeq} + end); val bd = mk_cexp (if live = 0 then ctwo else mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo) - (mk_csum bnf_bd_As (mk_card_of (HOLogic.mk_UNIV - (mk_bnf_T (replicate live (fst (dest_relT (fastype_of bnf_bd_As)))) CA)))); + (mk_csum bnf_bd_As (mk_card_of (HOLogic.mk_UNIV bd_bnfT))); val in_bd_goal = fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd)); in Goal.prove_sorry lthy [] [] in_bd_goal - (mk_in_bd_tac live (Lazy.force map_comp') (Lazy.force map_id') (#map_cong0 axioms) + (mk_in_bd_tac live surj_imp_ordLeq_inst + (Lazy.force map_comp') (Lazy.force map_id') (#map_cong0 axioms) (map Lazy.force set_map') (#set_bd axioms) (#bd_card_order axioms) bd_Card_order bd_Cinfinite bd_Cnotzero) |> Thm.close_derivation diff -r 71fef62c4213 -r 122416054a9c src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 01 16:53:03 2013 +0200 @@ -31,8 +31,8 @@ val mk_map_transfer_tac: thm -> thm -> thm list -> thm -> thm -> {prems: thm list, context: Proof.context} -> tactic - val mk_in_bd_tac: int -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm -> thm -> - {prems: 'a, context: Proof.context} -> tactic + val mk_in_bd_tac: int -> thm -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm -> + thm -> {prems: 'a, context: Proof.context} -> tactic end; structure BNF_Def_Tactics : BNF_DEF_TACTICS = @@ -232,7 +232,7 @@ REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})]) end; -fun mk_in_bd_tac live map_comp' map_id' map_cong0 set_map's set_bds +fun mk_in_bd_tac live surj_imp_ordLeq_inst map_comp' map_id' map_cong0 set_map's set_bds bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero {context = ctxt, prems = _} = if live = 0 then rtac @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order] @@ -269,7 +269,7 @@ rtac @{thm ordLeq_refl[OF Card_order_cexp]}] 1 THEN unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN - EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac @{thm surj_imp_ordLeq}, rtac subsetI, + EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac surj_imp_ordLeq_inst, rtac subsetI, Method.insert_tac inserts, REPEAT_DETERM o dtac meta_spec, REPEAT_DETERM o eresolve_tac [exE, Tactic.make_elim conjunct1], etac CollectE, if live = 1 then K all_tac @@ -284,13 +284,14 @@ REPEAT_DETERM_N (2 * live) o atac, REPEAT_DETERM_N live o rtac (@{thm prod.cases} RS trans), rtac refl, - rtac @{thm surj_imp_ordLeq}, rtac subsetI, rtac @{thm image_eqI}, rtac sym, - rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]}, - map_comp' RS sym, map_id']), + rtac @{thm surj_imp_ordLeq}, rtac subsetI, rtac (Drule.rotate_prems 1 @{thm image_eqI}), REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, CONJ_WRAP' (fn thm => rtac (thm RS ord_eq_le_trans) THEN' etac @{thm subset_trans[OF image_mono Un_upper1]}) - set_map's] 1 + set_map's, + rtac sym, + rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]}, + map_comp' RS sym, map_id'])] 1 end; end; diff -r 71fef62c4213 -r 122416054a9c src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Aug 01 16:53:03 2013 +0200 @@ -135,7 +135,7 @@ fun register_fp_sugar key fp_sugar = Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); + (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar))); fun register_fp_sugars fp pre_bnfs nested_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars co_iterss co_inducts co_iter_thmsss lthy = @@ -995,7 +995,7 @@ Sign.add_type no_defs_lthy (type_binding_of spec, length (type_args_named_constrained_of spec), mixfix_of spec); - val fake_thy = Theory.copy #> fold add_fake_type specs; + val fake_thy = fold add_fake_type specs; val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy; fun mk_fake_T b = @@ -1464,7 +1464,7 @@ parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec); -val parse_co_datatype = parse_wrap_options -- Parse.and_list1 parse_spec; +val parse_co_datatype = parse_wrap_free_constructors_options -- Parse.and_list1 parse_spec; fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp; diff -r 71fef62c4213 -r 122416054a9c src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Aug 01 16:53:03 2013 +0200 @@ -8,7 +8,7 @@ imports Complex_Main "~~/src/HOL/Library/Abstract_Rat" Polynomial_List begin -subsection{* Datatype of polynomial expressions *} +subsection{* Datatype of polynomial expressions *} datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly @@ -36,7 +36,7 @@ | "polybound0 (Bound n) = (n>0)" | "polybound0 (Neg a) = polybound0 a" | "polybound0 (Add a b) = (polybound0 a \ polybound0 b)" -| "polybound0 (Sub a b) = (polybound0 a \ polybound0 b)" +| "polybound0 (Sub a b) = (polybound0 a \ polybound0 b)" | "polybound0 (Mul a b) = (polybound0 a \ polybound0 b)" | "polybound0 (Pw p n) = (polybound0 p)" | "polybound0 (CN c n p) = (n \ 0 \ polybound0 c \ polybound0 p)" @@ -47,13 +47,13 @@ | "polysubst0 t (Bound n) = (if n=0 then t else Bound n)" | "polysubst0 t (Neg a) = Neg (polysubst0 t a)" | "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)" -| "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" +| "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" | "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)" | "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n" | "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p)) else CN (polysubst0 t c) n (polysubst0 t p))" -fun decrpoly:: "poly \ poly" +fun decrpoly:: "poly \ poly" where "decrpoly (Bound n) = Bound (n - 1)" | "decrpoly (Neg a) = Neg (decrpoly a)" @@ -117,12 +117,12 @@ fun polyadd :: "poly \ poly \ poly" (infixl "+\<^sub>p" 60) where "polyadd (C c) (C c') = C (c+\<^sub>Nc')" -| "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'" +| "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'" | "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p" | "polyadd (CN c n p) (CN c' n' p') = (if n < n' then CN (polyadd c (CN c' n' p')) n p else if n'p then cc' else CN cc' n pp')))" | "polyadd a b = Add a b" @@ -140,13 +140,13 @@ fun polymul :: "poly \ poly \ poly" (infixl "*\<^sub>p" 60) where "polymul (C c) (C c') = C (c*\<^sub>Nc')" -| "polymul (C c) (CN c' n' p') = +| "polymul (C c) (CN c' n' p') = (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))" -| "polymul (CN c n p) (C c') = +| "polymul (CN c n p) (C c') = (if c' = 0\<^sub>N then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))" -| "polymul (CN c n p) (CN c' n' p') = +| "polymul (CN c n p) (CN c' n' p') = (if np n' (polymul (CN c n p) p')))" | "polymul a b = Mul a b" @@ -157,7 +157,7 @@ fun polypow :: "nat \ poly \ poly" where "polypow 0 = (\p. (1)\<^sub>p)" -| "polypow n = (\p. let q = polypow (n div 2) p ; d = polymul q q in +| "polypow n = (\p. let q = polypow (n div 2) p ; d = polymul q q in if even n then d else polymul p d)" abbreviation poly_pow :: "poly \ nat \ poly" (infixl "^\<^sub>p" 60) @@ -196,13 +196,15 @@ partial_function (tailrec) polydivide_aux :: "poly \ nat \ poly \ nat \ poly \ nat \ poly" where - "polydivide_aux a n p k s = + "polydivide_aux a n p k s = (if s = 0\<^sub>p then (k,s) - else (let b = head s; m = degree s in - (if m < n then (k,s) else - (let p'= funpow (m - n) shift1 p in - (if a = b then polydivide_aux a n p k (s -\<^sub>p p') - else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))" + else + (let b = head s; m = degree s in + (if m < n then (k,s) + else + (let p'= funpow (m - n) shift1 p in + (if a = b then polydivide_aux a n p k (s -\<^sub>p p') + else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))" definition polydivide :: "poly \ poly \ (nat \ poly)" where "polydivide s p \ polydivide_aux (head p) (degree p) p 0 s" @@ -234,9 +236,9 @@ Ipoly_syntax :: "poly \ 'a list \'a::{field_char_0, field_inverse_zero, power}" ("\_\\<^sub>p\<^bsup>_\<^esup>") where "\p\\<^sub>p\<^bsup>bs\<^esup> \ Ipoly bs p" -lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" +lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" by (simp add: INum_def) -lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j" +lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j" by (simp add: INum_def) lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat @@ -258,49 +260,52 @@ text{* polyadd preserves normal forms *} -lemma polyadd_normh: "\isnpolyh p n0 ; isnpolyh q n1\ +lemma polyadd_normh: "\isnpolyh p n0 ; isnpolyh q n1\ \ isnpolyh (polyadd p q) (min n0 n1)" -proof(induct p q arbitrary: n0 n1 rule: polyadd.induct) +proof (induct p q arbitrary: n0 n1 rule: polyadd.induct) case (2 ab c' n' p' n0 n1) - from 2 have th1: "isnpolyh (C ab) (Suc n')" by simp + from 2 have th1: "isnpolyh (C ab) (Suc n')" by simp from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \ n1" by simp_all with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp with 2(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')" by simp - from nplen1 have n01len1: "min n0 n1 \ n'" by simp + from nplen1 have n01len1: "min n0 n1 \ n'" by simp thus ?case using 2 th3 by simp next case (3 c' n' p' ab n1 n0) - from 3 have th1: "isnpolyh (C ab) (Suc n')" by simp + from 3 have th1: "isnpolyh (C ab) (Suc n')" by simp from 3(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \ n1" by simp_all with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')" by simp - from nplen1 have n01len1: "min n0 n1 \ n'" by simp + from nplen1 have n01len1: "min n0 n1 \ n'" by simp thus ?case using 3 th3 by simp next case (4 c n p c' n' p' n0 n1) hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all - from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all + from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all from 4 have ngen0: "n \ n0" by simp - from 4 have n'gen1: "n' \ n1" by simp + from 4 have n'gen1: "n' \ n1" by simp have "n < n' \ n' < n \ n = n'" by auto - moreover {assume eq: "n = n'" - with "4.hyps"(3)[OF nc nc'] + moreover { + assume eq: "n = n'" + with "4.hyps"(3)[OF nc nc'] have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)" using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp have minle: "min n0 n1 \ n'" using ngen0 n'gen1 eq by simp - from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)} - moreover {assume lt: "n < n'" + from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def) } + moreover { + assume lt: "n < n'" have "min n0 n1 \ n0" by simp - with 4 lt have th1:"min n0 n1 \ n" by auto + with 4 lt have th1:"min n0 n1 \ n" by auto from 4 have th21: "isnpolyh c (Suc n)" by simp from 4 have th22: "isnpolyh (CN c' n' p') n'" by simp from lt have th23: "min (Suc n) n' = Suc n" by arith from "4.hyps"(1)[OF th21 th22] have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)" using th23 by simp - with 4 lt th1 have ?case by simp } - moreover {assume gt: "n' < n" hence gt': "n' < n \ \ n < n'" by simp + with 4 lt th1 have ?case by simp } + moreover { + assume gt: "n' < n" hence gt': "n' < n \ \ n < n'" by simp have "min n0 n1 \ n1" by simp with 4 gt have th1:"min n0 n1 \ n'" by auto from 4 have th21: "isnpolyh c' (Suc n')" by simp_all @@ -308,8 +313,8 @@ from gt have th23: "min n (Suc n') = Suc n'" by arith from "4.hyps"(2)[OF th22 th21] have "isnpolyh (polyadd (CN c n p) c') (Suc n')" using th23 by simp - with 4 gt th1 have ?case by simp} - ultimately show ?case by blast + with 4 gt th1 have ?case by simp } + ultimately show ?case by blast qed auto lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q" @@ -321,8 +326,8 @@ text{* The degree of addition and other general lemmas needed for the normal form of polymul *} -lemma polyadd_different_degreen: - "\isnpolyh p n0 ; isnpolyh q n1; degreen p m \ degreen q m ; m \ min n0 n1\ \ +lemma polyadd_different_degreen: + "\isnpolyh p n0 ; isnpolyh q n1; degreen p m \ degreen q m ; m \ min n0 n1\ \ degreen (polyadd p q) m = max (degreen p m) (degreen q m)" proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct) case (4 c n p c' n' p' m n0 n1) @@ -362,11 +367,13 @@ shows "degreen (p +\<^sub>p q) m \ max (degreen p m) (degreen q m)" using np nq m proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct) - case (2 c c' n' p' n0 n1) thus ?case by (cases n') simp_all + case (2 c c' n' p' n0 n1) + thus ?case by (cases n') simp_all next - case (3 c n p c' n0 n1) thus ?case by (cases n) auto + case (3 c n p c' n0 n1) + thus ?case by (cases n) auto next - case (4 c n p c' n' p' n0 n1 m) + case (4 c n p c' n' p' n0 n1 m) have "n' = n \ n < n' \ n' < n" by arith thus ?case proof (elim disjE) @@ -376,21 +383,21 @@ qed simp_all qed auto -lemma polyadd_eq_const_degreen: "\ isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\ +lemma polyadd_eq_const_degreen: "\ isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\ \ degreen p m = degreen q m" proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct) - case (4 c n p c' n' p' m n0 n1 x) - {assume nn': "n' < n" hence ?case using 4 by simp} - moreover - {assume nn':"\ n' < n" hence "n < n' \ n = n'" by arith - moreover {assume "n < n'" with 4 have ?case by simp } - moreover {assume eq: "n = n'" hence ?case using 4 + case (4 c n p c' n' p' m n0 n1 x) + { assume nn': "n' < n" hence ?case using 4 by simp } + moreover + { assume nn':"\ n' < n" hence "n < n' \ n = n'" by arith + moreover { assume "n < n'" with 4 have ?case by simp } + moreover { assume eq: "n = n'" hence ?case using 4 apply (cases "p +\<^sub>p p' = 0\<^sub>p") apply (auto simp add: Let_def) apply blast done - } - ultimately have ?case by blast} + } + ultimately have ?case by blast } ultimately show ?case by blast qed simp_all @@ -399,37 +406,37 @@ and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \ min n0 n1" - shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" - and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \ q = 0\<^sub>p)" + shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" + and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \ q = 0\<^sub>p)" and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \ q = 0\<^sub>p) then 0 else degreen p m + degreen q m)" using np nq m proof (induct p q arbitrary: n0 n1 m rule: polymul.induct) - case (2 c c' n' p') - { case (1 n0 n1) + case (2 c c' n' p') + { case (1 n0 n1) with "2.hyps"(4-6)[of n' n' n'] and "2.hyps"(1-3)[of "Suc n'" "Suc n'" n'] show ?case by (auto simp add: min_def) next - case (2 n0 n1) thus ?case by auto + case (2 n0 n1) thus ?case by auto next - case (3 n0 n1) thus ?case using "2.hyps" by auto } + case (3 n0 n1) thus ?case using "2.hyps" by auto } next case (3 c n p c') - { case (1 n0 n1) + { case (1 n0 n1) with "3.hyps"(4-6)[of n n n] "3.hyps"(1-3)[of "Suc n" "Suc n" n] show ?case by (auto simp add: min_def) next case (2 n0 n1) thus ?case by auto next - case (3 n0 n1) thus ?case using "3.hyps" by auto } + case (3 n0 n1) thus ?case using "3.hyps" by auto } next case (4 c n p c' n' p') let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'" { case (1 n0 n1) hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'" - and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" + and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')" and nn0: "n \ n0" and nn1:"n' \ n1" by simp_all @@ -462,23 +469,24 @@ let ?d2 = "degreen ?cnp' m" let ?eq = "?d = (if ?cnp = 0\<^sub>p \ ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)" have "n' n < n' \ n' = n" by auto - moreover + moreover {assume "n' < n \ n < n'" - with "4.hyps"(3,6,18) np np' m + with "4.hyps"(3,6,18) np np' m have ?eq by auto } moreover - {assume nn': "n' = n" hence nn:"\ n' < n \ \ n < n'" by arith + { assume nn': "n' = n" + hence nn: "\ n' < n \ \ n < n'" by arith from "4.hyps"(16,18)[of n n' n] "4.hyps"(13,14)[of n "Suc n'" n] np np' nn' have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n" "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" - "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" + "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" "?cnp *\<^sub>p p' \ 0\<^sub>p" by (auto simp add: min_def) - {assume mn: "m = n" + { assume mn: "m = n" from "4.hyps"(17,18)[OF norm(1,4), of n] "4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn - have degs: "degreen (?cnp *\<^sub>p c') n = + have degs: "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)" "degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n" by (simp_all add: min_def) from degs norm @@ -487,31 +495,31 @@ by simp have nmin: "n \ min n n" by (simp add: min_def) from polyadd_different_degreen[OF norm(3,6) neq nmin] th1 - have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n = degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp + have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n = degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp from "4.hyps"(16-18)[OF norm(1,4), of n] "4.hyps"(13-15)[OF norm(1,2), of n] mn norm m nn' deg - have ?eq by simp} + have ?eq by simp } moreover - {assume mn: "m \ n" hence mn': "m < n" using m np by auto - from nn' m np have max1: "m \ max n n" by simp - hence min1: "m \ min n n" by simp + { assume mn: "m \ n" hence mn': "m < n" using m np by auto + from nn' m np have max1: "m \ max n n" by simp + hence min1: "m \ min n n" by simp hence min2: "m \ min n (Suc n)" by simp from "4.hyps"(16-18)[OF norm(1,4) min1] "4.hyps"(13-15)[OF norm(1,2) min2] degreen_polyadd[OF norm(3,6) max1] - have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m + have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m \ max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)" using mn nn' np np' by simp with "4.hyps"(16-18)[OF norm(1,4) min1] "4.hyps"(13-15)[OF norm(1,2) min2] degreen_0[OF norm(3) mn'] - have ?eq using nn' mn np np' by clarsimp} - ultimately have ?eq by blast} - ultimately show ?eq by blast} + have ?eq using nn' mn np np' by clarsimp } + ultimately have ?eq by blast } + ultimately show ?eq by blast } { case (2 n0 n1) - hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1" + hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1" and m: "m \ min n0 n1" by simp_all hence mn: "m \ n" by simp let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')" @@ -522,32 +530,32 @@ np np' C(2) mn have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n" "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" - "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" - "?cnp *\<^sub>p p' \ 0\<^sub>p" + "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" + "?cnp *\<^sub>p p' \ 0\<^sub>p" "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)" "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n" by (simp_all add: min_def) - + from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp - have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" + have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" using norm by simp from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq have "False" by simp } - thus ?case using "4.hyps" by clarsimp} + thus ?case using "4.hyps" by clarsimp } qed auto lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)" by (induct p q rule: polymul.induct) (auto simp add: field_simps) -lemma polymul_normh: +lemma polymul_normh: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\isnpolyh p n0 ; isnpolyh q n1\ \ isnpolyh (p *\<^sub>p q) (min n0 n1)" - using polymul_properties(1) by blast + using polymul_properties(1) by blast -lemma polymul_eq0_iff: +lemma polymul_eq0_iff: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\ isnpolyh p n0 ; isnpolyh q n1\ \ (p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \ q = 0\<^sub>p) " - using polymul_properties(2) by blast + using polymul_properties(2) by blast lemma polymul_degreen: (* FIXME duplicate? *) assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" @@ -555,7 +563,7 @@ degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \ q = 0\<^sub>p) then 0 else degreen p m + degreen q m)" using polymul_properties(3) by blast -lemma polymul_norm: +lemma polymul_norm: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\ isnpoly p; isnpoly q\ \ isnpoly (polymul p q)" using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp @@ -567,14 +575,14 @@ by (induct p arbitrary: n0) auto lemma monic_eqI: - assumes np: "isnpolyh p n0" + assumes np: "isnpolyh p n0" shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})" unfolding monic_def Let_def proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np]) let ?h = "headconst p" assume pz: "p \ 0\<^sub>p" - {assume hz: "INum ?h = (0::'a)" + { assume hz: "INum ?h = (0::'a)" from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast} @@ -602,18 +610,19 @@ lemma polysub[simp]: "Ipoly bs (polysub p q) = (Ipoly bs p) - (Ipoly bs q)" by (simp add: polysub_def) -lemma polysub_normh: "\ n0 n1. \ isnpolyh p n0 ; isnpolyh q n1\ \ isnpolyh (polysub p q) (min n0 n1)" +lemma polysub_normh: + "\n0 n1. \ isnpolyh p n0 ; isnpolyh q n1\ \ isnpolyh (polysub p q) (min n0 n1)" by (simp add: polysub_def polyneg_normh polyadd_normh) lemma polysub_norm: "\ isnpoly p; isnpoly q\ \ isnpoly (polysub p q)" - using polyadd_norm polyneg_norm by (simp add: polysub_def) + using polyadd_norm polyneg_norm by (simp add: polysub_def) lemma polysub_same_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpolyh p n0 \ polysub p p = 0\<^sub>p" unfolding polysub_def split_def fst_conv snd_conv by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def]) -lemma polysub_0: +lemma polysub_0: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\ isnpolyh p n0 ; isnpolyh q n1\ \ (p -\<^sub>p q = 0\<^sub>p) = (p = q)" unfolding polysub_def split_def fst_conv snd_conv @@ -631,8 +640,8 @@ let ?q = "polypow ((Suc n) div 2) p" let ?d = "polymul ?q ?q" have "odd (Suc n) \ even (Suc n)" by simp - moreover - {assume odd: "odd (Suc n)" + moreover + { assume odd: "odd (Suc n)" have th: "(Suc (Suc (Suc (0\nat)) * (Suc n div Suc (Suc (0\nat))))) = Suc n div 2 + Suc n div 2 + 1" by arith from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" by (simp add: Let_def) @@ -642,10 +651,10 @@ by (simp only: power_add power_one_right) simp also have "\ = (Ipoly bs p) ^ (Suc (Suc (Suc (0\nat)) * (Suc n div Suc (Suc (0\nat)))))" by (simp only: th) - finally have ?case + finally have ?case using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp } - moreover - {assume even: "even (Suc n)" + moreover + { assume even: "even (Suc n)" have th: "(Suc (Suc (0\nat))) * (Suc n div Suc (Suc (0\nat))) = Suc n div 2 + Suc n div 2" by arith from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def) @@ -655,7 +664,7 @@ ultimately show ?case by blast qed -lemma polypow_normh: +lemma polypow_normh: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpolyh p n \ isnpolyh (polypow k p) n" proof (induct k arbitrary: n rule: polypow.induct) @@ -666,9 +675,9 @@ from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n" by simp from dn on show ?case by (simp add: Let_def) -qed auto +qed auto -lemma polypow_norm: +lemma polypow_norm: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpoly p \ isnpoly (polypow k p)" by (simp add: polypow_normh isnpoly_def) @@ -679,7 +688,7 @@ "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})" by (induct p rule:polynate.induct) auto -lemma polynate_norm[simp]: +lemma polynate_norm[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "isnpoly (polynate p)" by (induct p rule: polynate.induct) @@ -692,7 +701,7 @@ lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)" by (simp add: shift1_def) -lemma shift1_isnpoly: +lemma shift1_isnpoly: assumes pn: "isnpoly p" and pnz: "p \ 0\<^sub>p" shows "isnpoly (shift1 p) " @@ -700,11 +709,11 @@ lemma shift1_nz[simp]:"shift1 p \ 0\<^sub>p" by (simp add: shift1_def) -lemma funpow_shift1_isnpoly: +lemma funpow_shift1_isnpoly: "\ isnpoly p ; p \ 0\<^sub>p\ \ isnpoly (funpow n shift1 p)" by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1) -lemma funpow_isnpolyh: +lemma funpow_isnpolyh: assumes f: "\ p. isnpolyh p n \ isnpolyh (f p) n" and np: "isnpolyh p n" shows "isnpolyh (funpow k f p) n" @@ -718,7 +727,7 @@ lemma shift1_isnpolyh: "isnpolyh p n0 \ p\ 0\<^sub>p \ isnpolyh (shift1 p) 0" using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def) -lemma funpow_shift1_1: +lemma funpow_shift1_1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)" by (simp add: funpow_shift1) @@ -733,8 +742,8 @@ using np proof (induct p arbitrary: n rule: behead.induct) case (1 c p n) hence pn: "isnpolyh p n" by simp - from 1(1)[OF pn] - have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . + from 1(1)[OF pn] + have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p") apply (simp_all add: th[symmetric] field_simps) @@ -778,7 +787,7 @@ assumes nb: "polybound0 a" shows "Ipoly (b#bs) a = Ipoly (b'#bs) a" using nb - by (induct a rule: poly.induct) auto + by (induct a rule: poly.induct) auto lemma polysubst0_I: "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t" by (induct t) simp_all @@ -816,15 +825,15 @@ lemma wf_bs_coefficients: "wf_bs bs p \ \ c \ set (coefficients p). wf_bs bs c" proof (induct p rule: coefficients.induct) - case (1 c p) - show ?case + case (1 c p) + show ?case proof fix x assume xc: "x \ set (coefficients (CN c 0 p))" hence "x = c \ x \ set (coefficients p)" by simp - moreover + moreover {assume "x = c" hence "wf_bs bs x" using "1.prems" unfolding wf_bs_def by simp} - moreover - {assume H: "x \ set (coefficients p)" + moreover + {assume H: "x \ set (coefficients p)" from "1.prems" have "wf_bs bs p" unfolding wf_bs_def by simp with "1.hyps" H have "wf_bs bs x" by blast } ultimately show "wf_bs bs x" by blast @@ -838,7 +847,7 @@ unfolding wf_bs_def by (induct p) (auto simp add: nth_append) lemma take_maxindex_wf: - assumes wf: "wf_bs bs p" + assumes wf: "wf_bs bs p" shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p" proof- let ?ip = "maxindex p" @@ -885,14 +894,14 @@ done lemma wf_bs_polyadd: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p +\<^sub>p q)" - unfolding wf_bs_def + unfolding wf_bs_def apply (induct p q rule: polyadd.induct) apply (auto simp add: Let_def) done lemma wf_bs_polyul: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p *\<^sub>p q)" - unfolding wf_bs_def - apply (induct p q arbitrary: bs rule: polymul.induct) + unfolding wf_bs_def + apply (induct p q arbitrary: bs rule: polymul.induct) apply (simp_all add: wf_bs_polyadd) apply clarsimp apply (rule wf_bs_polyadd[unfolded wf_bs_def, rule_format]) @@ -918,12 +927,12 @@ have cp: "isnpolyh (CN c 0 p) n0" by fact hence norm: "isnpolyh c 0" "isnpolyh p 0" "p \ 0\<^sub>p" "n0 = 0" by (auto simp add: isnpolyh_mono[where n'=0]) - from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case by simp + from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case by simp qed auto lemma coefficients_isconst: "isnpolyh p n \ \q\set (coefficients p). isconstant q" - by (induct p arbitrary: n rule: coefficients.induct) + by (induct p arbitrary: n rule: coefficients.induct) (auto simp add: isnpolyh_Suc_const) lemma polypoly_polypoly': @@ -940,17 +949,17 @@ hence "\q \ ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)" using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs] by auto - - thus ?thesis unfolding polypoly_def polypoly'_def by simp + + thus ?thesis unfolding polypoly_def polypoly'_def by simp qed lemma polypoly_poly: assumes np: "isnpolyh p n0" shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x" - using np + using np by (induct p arbitrary: n0 bs rule: coefficients.induct) (auto simp add: polypoly_def) -lemma polypoly'_poly: +lemma polypoly'_poly: assumes np: "isnpolyh p n0" shows "\p\\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x" using polypoly_poly[OF np, simplified polypoly_polypoly'[OF np]] . @@ -959,14 +968,14 @@ lemma polypoly_poly_polybound0: assumes np: "isnpolyh p n0" and nb: "polybound0 p" shows "polypoly bs p = [Ipoly bs p]" - using np nb unfolding polypoly_def + using np nb unfolding polypoly_def apply (cases p) apply auto apply (case_tac nat) apply auto done -lemma head_isnpolyh: "isnpolyh p n0 \ isnpolyh (head p) n0" +lemma head_isnpolyh: "isnpolyh p n0 \ isnpolyh (head p) n0" by (induct p rule: head.induct) auto lemma headn_nz[simp]: "isnpolyh p n0 \ (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)" @@ -978,7 +987,7 @@ lemma head_nz[simp]: "isnpolyh p n0 \ (head p = 0\<^sub>p) = (p = 0\<^sub>p)" by (simp add: head_eq_headn0) -lemma isnpolyh_zero_iff: +lemma isnpolyh_zero_iff: assumes nq: "isnpolyh p n0" and eq :"\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, field_inverse_zero, power})" shows "p = 0\<^sub>p" @@ -994,10 +1003,10 @@ let ?h = "head p" let ?hd = "decrpoly ?h" let ?ihd = "maxindex ?hd" - from head_isnpolyh[OF np] head_polybound0[OF np] have h:"isnpolyh ?h n0" "polybound0 ?h" + from head_isnpolyh[OF np] head_polybound0[OF np] have h:"isnpolyh ?h n0" "polybound0 ?h" by simp_all hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast - + from maxindex_coefficients[of p] coefficients_head[of p, symmetric] have mihn: "maxindex ?h \ maxindex p" by auto with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < maxindex p" by auto @@ -1023,21 +1032,21 @@ with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" by simp with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\?hd\\<^sub>p\<^bsup>bs\<^esup> = 0" by simp } then have hdz: "\bs. wf_bs bs ?hd \ \?hd\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast - + from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast hence "?h = 0\<^sub>p" by simp with head_nz[OF np] have "p = 0\<^sub>p" by simp} ultimately show "p = 0\<^sub>p" by blast qed -lemma isnpolyh_unique: +lemma isnpolyh_unique: assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1" shows "(\bs. \p\\<^sub>p\<^bsup>bs\<^esup> = (\q\\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0, field_inverse_zero, power})) \ p = q" proof(auto) assume H: "\bs. (\p\\<^sub>p\<^bsup>bs\<^esup> ::'a)= \q\\<^sub>p\<^bsup>bs\<^esup>" hence "\bs.\p -\<^sub>p q\\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp - hence "\bs. wf_bs bs (p -\<^sub>p q) \ \p -\<^sub>p q\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" + hence "\bs. wf_bs bs (p -\<^sub>p q) \ \p -\<^sub>p q\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" using wf_bs_polysub[where p=p and q=q] by auto with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq] show "p = q" by blast @@ -1056,28 +1065,28 @@ lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp lemma one_normh: "isnpolyh (1)\<^sub>p n" by simp -lemma polyadd_0[simp]: +lemma polyadd_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p" - using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] + using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all -lemma polymul_1[simp]: +lemma polymul_1[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" shows "p *\<^sub>p (1)\<^sub>p = p" and "(1)\<^sub>p *\<^sub>p p = p" - using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] + using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all -lemma polymul_0[simp]: +lemma polymul_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np: "isnpolyh p n0" shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" and "0\<^sub>p *\<^sub>p p = 0\<^sub>p" - using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] + using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all -lemma polymul_commute: +lemma polymul_commute: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np:"isnpolyh p n0" and nq: "isnpolyh q n1" @@ -1086,15 +1095,15 @@ by simp declare polyneg_polyneg [simp] - -lemma isnpolyh_polynate_id [simp]: + +lemma isnpolyh_polynate_id [simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and np:"isnpolyh p n0" shows "polynate p = p" using isnpolyh_unique[where ?'a= "'a::{field_char_0, field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0, field_inverse_zero}"] by simp -lemma polynate_idempotent[simp]: +lemma polynate_idempotent[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "polynate (polynate p) = polynate p" using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] . @@ -1137,34 +1146,34 @@ from degree_polyadd[OF np nq'] show ?thesis by (simp add: polysub_def degree_polyneg[OF nq]) qed -lemma degree_polysub_samehead: +lemma degree_polysub_samehead: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" + and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" and d: "degree p = degree q" shows "degree (p -\<^sub>p q) < degree p \ (p -\<^sub>p q = 0\<^sub>p)" unfolding polysub_def split_def fst_conv snd_conv using np nq h d proof (induct p q rule: polyadd.induct) case (1 c c') - thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) + thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) next - case (2 c c' n' p') + case (2 c c' n' p') from 2 have "degree (C c) = degree (CN c' n' p')" by simp hence nz:"n' > 0" by (cases n') auto hence "head (CN c' n' p') = CN c' n' p'" by (cases n') auto with 2 show ?case by simp next - case (3 c n p c') + case (3 c n p c') hence "degree (C c') = degree (CN c n p)" by simp hence nz:"n > 0" by (cases n) auto hence "head (CN c n p) = CN c n p" by (cases n) auto with 3 show ?case by simp next case (4 c n p c' n' p') - hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" + hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" "head (CN c n p) = head (CN c' n' p')" "degree (CN c n p) = degree (CN c' n' p')" by simp+ - hence degc: "degree c = 0" and degc': "degree c' = 0" by simp_all - hence degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0" + hence degc: "degree c = 0" and degc': "degree c' = 0" by simp_all + hence degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0" using H(1-2) degree_polyneg by auto from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')" by simp+ from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' have degcmc': "degree (c +\<^sub>p ~\<^sub>pc') = 0" by simp @@ -1178,10 +1187,10 @@ with nn' H(3) have cc':"c = c'" and pp': "p = p'" by (cases n, auto)+ hence ?case using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] polysub_same_0[OF c'nh, simplified polysub_def] - using nn' 4 by (simp add: Let_def)} + using nn' 4 by (simp add: Let_def) } ultimately have ?case by blast} moreover - {assume nn': "n < n'" hence n'p: "n' > 0" by simp + {assume nn': "n < n'" hence n'p: "n' > 0" by simp hence headcnp':"head (CN c' n' p') = CN c' n' p'" by (cases n') simp_all have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" using 4 nn' by (cases n', simp_all) @@ -1189,7 +1198,7 @@ hence headcnp: "head (CN c n p) = CN c n p" by (cases n) auto from H(3) headcnp headcnp' nn' have ?case by auto} moreover - {assume nn': "n > n'" hence np: "n > 0" by simp + {assume nn': "n > n'" hence np: "n > 0" by simp hence headcnp:"head (CN c n p) = CN c n p" by (cases n) simp_all from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp from np have degcnp: "degree (CN c n p) = 0" by (cases n) simp_all @@ -1198,7 +1207,7 @@ from H(3) headcnp headcnp' nn' have ?case by auto} ultimately show ?case by blast qed auto - + lemma shift1_head : "isnpolyh p n0 \ head (shift1 p) = head p" by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def) @@ -1210,7 +1219,7 @@ case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh) with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" - and "head (shift1 p) = head p" by (simp_all add: shift1_head) + and "head (shift1 p) = head p" by (simp_all add: shift1_head) thus ?case by (simp add: funpow_swap1) qed @@ -1231,7 +1240,7 @@ lemma head_head[simp]: "isnpolyh p n0 \ head (head p) = head p" by (induct p rule: head.induct) auto -lemma polyadd_eq_const_degree: +lemma polyadd_eq_const_degree: "isnpolyh p n0 \ isnpolyh q n1 \ polyadd p q = C c \ degree p = degree q" using polyadd_eq_const_degreen degree_eq_degreen0 by simp @@ -1255,15 +1264,15 @@ apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans) done -lemma polymul_head_polyeq: +lemma polymul_head_polyeq: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "\isnpolyh p n0; isnpolyh q n1 ; p \ 0\<^sub>p ; q \ 0\<^sub>p \ \ head (p *\<^sub>p q) = head p *\<^sub>p head q" proof (induct p q arbitrary: n0 n1 rule: polymul.induct) case (2 c c' n' p' n0 n1) hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum c" by (simp_all add: head_isnpolyh) thus ?case using 2 by (cases n') auto -next - case (3 c n p c' n0 n1) +next + case (3 c n p c' n0 n1) hence "isnpolyh (head (CN c n p)) n0" "isnormNum c'" by (simp_all add: head_isnpolyh) thus ?case using 3 by (cases n) auto next @@ -1272,8 +1281,8 @@ "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'" by simp_all have "n < n' \ n' < n \ n = n'" by arith - moreover - {assume nn': "n < n'" hence ?case + moreover + {assume nn': "n < n'" hence ?case using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)] apply simp apply (cases n) @@ -1283,7 +1292,7 @@ done } moreover {assume nn': "n'< n" hence ?case - using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] + using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] apply simp apply (cases n') apply simp @@ -1291,14 +1300,14 @@ apply auto done } moreover {assume nn': "n' = n" - from nn' polymul_normh[OF norm(5,4)] + from nn' polymul_normh[OF norm(5,4)] have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def) - from nn' polymul_normh[OF norm(5,3)] norm + from nn' polymul_normh[OF norm(5,3)] norm have ncnpp':"isnpolyh (CN c n p *\<^sub>p p') n" by simp from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6) - have ncnpp0':"isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp - from polyadd_normh[OF ncnpc' ncnpp0'] - have nth: "isnpolyh ((CN c n p *\<^sub>p c') +\<^sub>p (CN 0\<^sub>p n (CN c n p *\<^sub>p p'))) n" + have ncnpp0':"isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp + from polyadd_normh[OF ncnpc' ncnpp0'] + have nth: "isnpolyh ((CN c n p *\<^sub>p c') +\<^sub>p (CN 0\<^sub>p n (CN c n p *\<^sub>p p'))) n" by (simp add: min_def) {assume np: "n > 0" with nn' head_isnpolyh_Suc'[OF np nth] @@ -1314,7 +1323,7 @@ from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth have ?case using norm "4.hyps"(6)[OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] nn' nz by simp } - ultimately have ?case by (cases n) auto} + ultimately have ?case by (cases n) auto} ultimately show ?case by blast qed simp_all @@ -1359,25 +1368,29 @@ and ns: "isnpolyh s n1" and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \ 0\<^sub>p" - shows "(polydivide_aux a n p k s = (k',r) \ (k' \ k) \ (degree r = 0 \ degree r < degree p) + shows "(polydivide_aux a n p k s = (k',r) \ (k' \ k) \ (degree r = 0 \ degree r < degree p) \ (\nr. isnpolyh r nr) \ (\q n1. isnpolyh q n1 \ ((polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))" using ns proof (induct "degree s" arbitrary: s k k' r n1 rule: less_induct) case less let ?qths = "\q n1. isnpolyh q n1 \ (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" - let ?ths = "polydivide_aux a n p k s = (k', r) \ k \ k' \ (degree r = 0 \ degree r < degree p) + let ?ths = "polydivide_aux a n p k s = (k', r) \ k \ k' \ (degree r = 0 \ degree r < degree p) \ (\nr. isnpolyh r nr) \ ?qths" let ?b = "head s" let ?p' = "funpow (degree s - n) shift1 p" let ?xdn = "funpow (degree s - n) shift1 (1)\<^sub>p" let ?akk' = "a ^\<^sub>p (k' - k)" note ns = `isnpolyh s n1` - from np have np0: "isnpolyh p 0" - using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp - have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="degree s - n"] isnpoly_def by simp - have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] by simp - from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def) - from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap + from np have np0: "isnpolyh p 0" + using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp + have np': "isnpolyh ?p' 0" + using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="degree s - n"] isnpoly_def + by simp + have headp': "head ?p' = head p" + using funpow_shift1_head[OF np pnz] by simp + from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" + by (simp add: isnpoly_def) + from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap have nakk':"isnpolyh ?akk' 0" by blast { assume sz: "s = 0\<^sub>p" hence ?ths using np polydivide_aux.simps @@ -1386,67 +1399,82 @@ apply simp done } moreover - {assume sz: "s \ 0\<^sub>p" - {assume dn: "degree s < n" + { assume sz: "s \ 0\<^sub>p" + { assume dn: "degree s < n" hence "?ths" using ns ndp np polydivide_aux.simps apply auto apply (rule exI[where x="0\<^sub>p"]) apply simp done } - moreover - {assume dn': "\ degree s < n" hence dn: "degree s \ n" by arith - have degsp': "degree s = degree ?p'" + moreover + { assume dn': "\ degree s < n" hence dn: "degree s \ n" by arith + have degsp': "degree s = degree ?p'" using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] by simp - {assume ba: "?b = a" - hence headsp': "head s = head ?p'" using ap headp' by simp - have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp + { assume ba: "?b = a" + hence headsp': "head s = head ?p'" + using ap headp' by simp + have nr: "isnpolyh (s -\<^sub>p ?p') 0" + using polysub_normh[OF ns np'] by simp from degree_polysub_samehead[OF ns np' headsp' degsp'] have "degree (s -\<^sub>p ?p') < degree s \ s -\<^sub>p ?p' = 0\<^sub>p" by simp - moreover - {assume deglt:"degree (s -\<^sub>p ?p') < degree s" + moreover + { assume deglt:"degree (s -\<^sub>p ?p') < degree s" from polydivide_aux.simps sz dn' ba have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')" by (simp add: Let_def) - {assume h1: "polydivide_aux a n p k s = (k', r)" - from less(1)[OF deglt nr, of k k' r] - trans[OF eq[symmetric] h1] - have kk': "k \ k'" and nr:"\nr. isnpolyh r nr" and dr: "degree r = 0 \ degree r < degree p" - and q1:"\q nq. isnpolyh q nq \ (a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r)" by auto - from q1 obtain q n1 where nq: "isnpolyh q n1" - and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r" by blast + { assume h1: "polydivide_aux a n p k s = (k', r)" + from less(1)[OF deglt nr, of k k' r] trans[OF eq[symmetric] h1] + have kk': "k \ k'" + and nr:"\nr. isnpolyh r nr" + and dr: "degree r = 0 \ degree r < degree p" + and q1: "\q nq. isnpolyh q nq \ (a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r)" + by auto + from q1 obtain q n1 where nq: "isnpolyh q n1" + and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r" by blast from nr obtain nr where nr': "isnpolyh r nr" by blast - from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp + from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" + by simp from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq] have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp - from polyadd_normh[OF polymul_normh[OF np + from polyadd_normh[OF polymul_normh[OF np polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr'] - have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp - from asp have "\ (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = + have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" + by simp + from asp have "\ (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp - hence " \(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = - Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" + hence " \(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = + Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" by (simp add: field_simps) - hence " \(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = - Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) - + Ipoly bs p * Ipoly bs q + Ipoly bs r" - by (auto simp only: funpow_shift1_1) - hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = - Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) - + Ipoly bs q) + Ipoly bs r" by (simp add: field_simps) - hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = - Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp + hence " \(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = + Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) + + Ipoly bs p * Ipoly bs q + Ipoly bs r" + by (auto simp only: funpow_shift1_1) + hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = + Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) + + Ipoly bs q) + Ipoly bs r" + by (simp add: field_simps) + hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = + Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r)" + by simp with isnpolyh_unique[OF nakks' nqr'] - have "a ^\<^sub>p (k' - k) *\<^sub>p s = - p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast + have "a ^\<^sub>p (k' - k) *\<^sub>p s = + p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r" + by blast hence ?qths using nq' apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q" in exI) - apply (rule_tac x="0" in exI) by simp + apply (rule_tac x="0" in exI) + apply simp + done with kk' nr dr have "k \ k' \ (degree r = 0 \ degree r < degree p) \ (\nr. isnpolyh r nr) \ ?qths" - by blast } hence ?ths by blast } - moreover - {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p" + by blast + } + hence ?ths by blast + } + moreover + { assume spz:"s -\<^sub>p ?p' = 0\<^sub>p" from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0, field_inverse_zero}"] - have " \(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp + have " \(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" + by simp hence "\(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" using np nxdn apply simp @@ -1455,134 +1483,162 @@ done hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast - {assume h1: "polydivide_aux a n p k s = (k',r)" + { assume h1: "polydivide_aux a n p k s = (k',r)" from polydivide_aux.simps sz dn' ba have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')" by (simp add: Let_def) - also have "\ = (k,0\<^sub>p)" using polydivide_aux.simps spz by simp + also have "\ = (k,0\<^sub>p)" + using polydivide_aux.simps spz by simp finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]] polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?ths apply auto - apply (rule exI[where x="?xdn"]) + apply (rule exI[where x="?xdn"]) apply (auto simp add: polymul_commute[of p]) - done} } - ultimately have ?ths by blast } + done + } + } + ultimately have ?ths by blast + } moreover - {assume ba: "?b \ a" - from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] + { assume ba: "?b \ a" + from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np']] - have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def) + have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" + by (simp add: min_def) have nzths: "a *\<^sub>p s \ 0\<^sub>p" "?b *\<^sub>p ?p' \ 0\<^sub>p" - using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] + using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns] - funpow_shift1_nz[OF pnz] by simp_all + funpow_shift1_nz[OF pnz] + by simp_all from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="degree s - n"] - have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" + have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" using head_head[OF ns] funpow_shift1_head[OF np pnz] polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]] by (simp add: ap) from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] head_nz[OF np] pnz sz ap[symmetric] funpow_shift1_nz[OF pnz, where n="degree s - n"] - polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"] head_nz[OF ns] + polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"] head_nz[OF ns] ndp dn - have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') " + have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p')" by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree) - {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s" - from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']] - ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp - {assume h1:"polydivide_aux a n p k s = (k', r)" + { assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s" + from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] + polymul_normh[OF head_isnpolyh[OF ns]np']] ap + have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" + by simp + { assume h1:"polydivide_aux a n p k s = (k', r)" from h1 polydivide_aux.simps sz dn' ba have eq:"polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)" by (simp add: Let_def) with less(1)[OF dth nasbp', of "Suc k" k' r] - obtain q nq nr where kk': "Suc k \ k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" + obtain q nq nr where kk': "Suc k \ k'" + and nr: "isnpolyh r nr" + and nq: "isnpolyh q nq" and dr: "degree r = 0 \ degree r < degree p" - and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" by auto + and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" + by auto from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith - {fix bs:: "'a::{field_char_0, field_inverse_zero} list" - - from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric] - have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" - by simp - hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = - Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r" - by (simp add: field_simps) - hence "Ipoly bs a ^ (k' - k) * Ipoly bs s = - Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r" - by (simp add: kk'' funpow_shift1_1[where n="degree s - n" and p="p"]) - hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = - Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" - by (simp add: field_simps)} - hence ieq:"\(bs :: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = - Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" by auto + { + fix bs:: "'a::{field_char_0, field_inverse_zero} list" + from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric] + have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" + by simp + hence "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = + Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r" + by (simp add: field_simps) + hence "Ipoly bs a ^ (k' - k) * Ipoly bs s = + Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r" + by (simp add: kk'' funpow_shift1_1[where n="degree s - n" and p="p"]) + hence "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = + Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" + by (simp add: field_simps) + } + hence ieq:"\(bs :: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = + Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" + by auto let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)" from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap ] nxdn]] - have nqw: "isnpolyh ?q 0" by simp + have nqw: "isnpolyh ?q 0" + by simp from ieq isnpolyh_unique[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - k"] ns, simplified ap] polyadd_normh[OF polymul_normh[OF np nqw] nr]] - have asth: "(a ^\<^sub>p (k' - k) *\<^sub>p s) = p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r" by blast - from dr kk' nr h1 asth nqw have ?ths apply simp + have asth: "(a ^\<^sub>p (k' - k) *\<^sub>p s) = p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r" + by blast + from dr kk' nr h1 asth nqw have ?ths + apply simp apply (rule conjI) apply (rule exI[where x="nr"], simp) apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp) apply (rule exI[where x="0"], simp) - done} - hence ?ths by blast } - moreover - {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p" - {fix bs :: "'a::{field_char_0, field_inverse_zero} list" + done + } + hence ?ths by blast + } + moreover + { assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p" + { + fix bs :: "'a::{field_char_0, field_inverse_zero} list" from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz - have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp - hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" - by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"]) - hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp - } - hence hth: "\ (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) = + have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" + by simp + hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" + by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"]) + hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" + by simp + } + hence hth: "\ (bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" .. - from hth - have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" - using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns] + from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" + using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]], simplified ap] by simp - {assume h1: "polydivide_aux a n p k s = (k', r)" - from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps - have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def) - with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn] - polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq - have ?ths - apply (clarsimp simp add: Let_def) - apply (rule exI[where x="?b *\<^sub>p ?xdn"]) - apply simp - apply (rule exI[where x="0"], simp) - done } - hence ?ths by blast } + { assume h1: "polydivide_aux a n p k s = (k', r)" + from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps + have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def) + with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn] + polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq + have ?ths + apply (clarsimp simp add: Let_def) + apply (rule exI[where x="?b *\<^sub>p ?xdn"]) + apply simp + apply (rule exI[where x="0"], simp) + done + } + hence ?ths by blast + } ultimately have ?ths using degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth] polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] head_nz[OF np] pnz sz ap[symmetric] - by (simp add: degree_eq_degreen0[symmetric]) blast } + by (simp add: degree_eq_degreen0[symmetric]) blast + } ultimately have ?ths by blast } - ultimately have ?ths by blast } + ultimately have ?ths by blast + } ultimately show ?ths by blast qed -lemma polydivide_properties: +lemma polydivide_properties: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \ 0\<^sub>p" - shows "(\ k r. polydivide s p = (k,r) \ (\nr. isnpolyh r nr) \ (degree r = 0 \ degree r < degree p) - \ (\q n1. isnpolyh q n1 \ ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))" -proof- - have trv: "head p = head p" "degree p = degree p" by simp_all - from polydivide_def[where s="s" and p="p"] - have ex: "\ k r. polydivide s p = (k,r)" by auto - then obtain k r where kr: "polydivide s p = (k,r)" by blast + and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \ 0\<^sub>p" + shows "\k r. polydivide s p = (k,r) \ + (\nr. isnpolyh r nr) \ (degree r = 0 \ degree r < degree p) \ + (\q n1. isnpolyh q n1 \ ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r))" +proof - + have trv: "head p = head p" "degree p = degree p" + by simp_all + from polydivide_def[where s="s" and p="p"] have ex: "\ k r. polydivide s p = (k,r)" + by auto + then obtain k r where kr: "polydivide s p = (k,r)" + by blast from trans[OF meta_eq_to_obj_eq[OF polydivide_def[where s="s"and p="p"], symmetric] kr] polydivide_aux_properties[OF np ns trv pnz, where k="0" and k'="k" and r="r"] have "(degree r = 0 \ degree r < degree p) \ - (\nr. isnpolyh r nr) \ (\q n1. isnpolyh q n1 \ head p ^\<^sub>p k - 0 *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" by blast - with kr show ?thesis + (\nr. isnpolyh r nr) \ (\q n1. isnpolyh q n1 \ head p ^\<^sub>p k - 0 *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" + by blast + with kr show ?thesis apply - apply (rule exI[where x="k"]) apply (rule exI[where x="r"]) @@ -1596,23 +1652,23 @@ definition "isnonconstant p = (\ isconstant p)" lemma isnonconstant_pnormal_iff: - assumes nc: "isnonconstant p" - shows "pnormal (polypoly bs p) \ Ipoly bs (head p) \ 0" + assumes nc: "isnonconstant p" + shows "pnormal (polypoly bs p) \ Ipoly bs (head p) \ 0" proof - let ?p = "polypoly bs p" + let ?p = "polypoly bs p" assume H: "pnormal ?p" have csz: "coefficients p \ []" using nc by (cases p) auto - - from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] + + from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] pnormal_last_nonzero[OF H] show "Ipoly bs (head p) \ 0" by (simp add: polypoly_def) next assume h: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" let ?p = "polypoly bs p" have csz: "coefficients p \ []" using nc by (cases p) auto - hence pz: "?p \ []" by (simp add: polypoly_def) + hence pz: "?p \ []" by (simp add: polypoly_def) hence lg: "length ?p > 0" by simp - from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] + from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] have lz: "last ?p \ 0" by (simp add: polypoly_def) from pnormal_last_length[OF lg lz] show "pnormal ?p" . qed @@ -1638,10 +1694,10 @@ assume h: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" from isnonconstant_pnormal_iff[OF inc, of bs] h have pn: "pnormal ?p" by blast - {fix x assume H: "?p = [x]" + { fix x assume H: "?p = [x]" from H have "length (coefficients p) = 1" unfolding polypoly_def by auto - with isnonconstant_coefficients_length[OF inc] have False by arith} - thus "nonconstant ?p" using pn unfolding nonconstant_def by blast + with isnonconstant_coefficients_length[OF inc] have False by arith } + thus "nonconstant ?p" using pn unfolding nonconstant_def by blast qed lemma pnormal_length: "p\[] \ pnormal p \ length (pnormalize p) = length p" @@ -1655,29 +1711,29 @@ assumes inc: "isnonconstant p" shows "degree p = Polynomial_List.degree (polypoly bs p) \ \head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" proof - let ?p = "polypoly bs p" + let ?p = "polypoly bs p" assume H: "degree p = Polynomial_List.degree ?p" from isnonconstant_coefficients_length[OF inc] have pz: "?p \ []" unfolding polypoly_def by auto from H degree_coefficients[of p] isnonconstant_coefficients_length[OF inc] have lg:"length (pnormalize ?p) = length ?p" unfolding Polynomial_List.degree_def polypoly_def by simp - hence "pnormal ?p" using pnormal_length[OF pz] by blast - with isnonconstant_pnormal_iff[OF inc] + hence "pnormal ?p" using pnormal_length[OF pz] by blast + with isnonconstant_pnormal_iff[OF inc] show "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" by blast next - let ?p = "polypoly bs p" + let ?p = "polypoly bs p" assume H: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" with isnonconstant_pnormal_iff[OF inc] have "pnormal ?p" by blast with degree_coefficients[of p] isnonconstant_coefficients_length[OF inc] - show "degree p = Polynomial_List.degree ?p" + show "degree p = Polynomial_List.degree ?p" unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto qed -section{* Swaps ; Division by a certain variable *} +section {* Swaps ; Division by a certain variable *} -primrec swap:: "nat \ nat \ poly \ poly" where +primrec swap :: "nat \ nat \ poly \ poly" where "swap n m (C x) = C x" | "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)" | "swap n m (Neg t) = Neg (swap n m t)" @@ -1685,8 +1741,8 @@ | "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)" | "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)" | "swap n m (Pw t k) = Pw (swap n m t) k" -| "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k) - (swap n m p)" +| "swap n m (CN c k p) = + CN (swap n m c) (if k = n then m else if k=m then n else k) (swap n m p)" lemma swap: assumes nbs: "n < length bs" @@ -1694,10 +1750,10 @@ shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" proof (induct t) case (Bound k) - thus ?case using nbs mbs by simp + thus ?case using nbs mbs by simp next case (CN c k p) - thus ?case using nbs mbs by simp + thus ?case using nbs mbs by simp qed simp_all lemma swap_swap_id [simp]: "swap n m (swap m n t) = t" @@ -1723,9 +1779,9 @@ shows "isnpoly (swapnorm n m p)" unfolding swapnorm_def by simp -definition "polydivideby n s p = +definition "polydivideby n s p = (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp - in (k,swapnorm 0 n h,swapnorm 0 n r))" + in (k, swapnorm 0 n h,swapnorm 0 n r))" lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)" by (induct p) simp_all @@ -1736,10 +1792,10 @@ | "isweaknpoly (CN c n p) \ isweaknpoly c \ isweaknpoly p" | "isweaknpoly p = False" -lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \ isweaknpoly p" +lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \ isweaknpoly p" by (induct p arbitrary: n0) auto -lemma swap_isweanpoly: "isweaknpoly p \ isweaknpoly (swap n m p)" +lemma swap_isweanpoly: "isweaknpoly p \ isweaknpoly (swap n m p)" by (induct p) auto end \ No newline at end of file diff -r 71fef62c4213 -r 122416054a9c src/HOL/HOLCF/Tools/Domain/domain.ML --- a/src/HOL/HOLCF/Tools/Domain/domain.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Thu Aug 01 16:53:03 2013 +0200 @@ -68,7 +68,6 @@ (* this theory is used just for parsing and error checking *) val tmp_thy = thy - |> Theory.copy |> fold (add_arity o thy_arity) dtnvs val dbinds : binding list = diff -r 71fef62c4213 -r 122416054a9c src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Aug 01 16:53:03 2013 +0200 @@ -408,7 +408,6 @@ (* this theory is used just for parsing *) val tmp_thy = thy |> - Theory.copy |> Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) => (tbind, length tvs, mx)) doms_raw) diff -r 71fef62c4213 -r 122416054a9c src/HOL/Library/Zorn.thy --- a/src/HOL/Library/Zorn.thy Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Library/Zorn.thy Thu Aug 01 16:53:03 2013 +0200 @@ -756,8 +756,7 @@ assumes "chain\<^sub>\ R" and "\r. r \ R \ extension_on (Field r) r p" shows "extension_on (Field (\R)) (\R) p" using assms - by (simp add: chain_subset_def extension_on_def) - (metis Field_def mono_Field set_mp) + by (simp add: chain_subset_def extension_on_def) (metis mono_Field set_mp) lemma downset_on_empty [simp]: "downset_on {} p" by (auto simp: downset_on_def) diff -r 71fef62c4213 -r 122416054a9c src/HOL/Matrix_LP/Compute_Oracle/compute.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Thu Aug 01 16:53:03 2013 +0200 @@ -169,10 +169,10 @@ fun default_naming i = "v_" ^ string_of_int i datatype computer = Computer of - (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming) + (theory * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming) option Unsynchronized.ref -fun theory_of (Computer (Unsynchronized.ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy +fun theory_of (Computer (Unsynchronized.ref (SOME (thy,_,_,_,_,_,_)))) = thy fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable) fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable @@ -304,7 +304,7 @@ val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable - in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end + in (thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end fun make_with_cache machine thy cache_patterns raw_thms = Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms))) @@ -388,7 +388,7 @@ datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int | Prem of AbstractMachine.term -datatype theorem = Theorem of theory_ref * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table +datatype theorem = Theorem of theory * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table * prem list * AbstractMachine.term * term list * sort list @@ -446,13 +446,12 @@ val (encoding, concl) = remove_types encoding (Logic.strip_imp_concl prop) val _ = set_encoding computer encoding in - Theorem (Theory.check_thy (theory_of_thm th), stamp_of computer, vartab, varsubst, + Theorem (theory_of_thm th, stamp_of computer, vartab, varsubst, prems, concl, hyps, shyps) end -fun theory_of_theorem (Theorem (rthy,_,_,_,_,_,_,_)) = Theory.deref rthy -fun update_theory thy (Theorem (_,p0,p1,p2,p3,p4,p5,p6)) = - Theorem (Theory.check_thy thy,p0,p1,p2,p3,p4,p5,p6) +fun theory_of_theorem (Theorem (thy,_,_,_,_,_,_,_)) = thy +fun update_theory thy (Theorem (_,p0,p1,p2,p3,p4,p5,p6)) = Theorem (thy,p0,p1,p2,p3,p4,p5,p6) fun stamp_of_theorem (Theorem (_,s, _, _, _, _, _, _)) = s fun vartab_of_theorem (Theorem (_,_,vt,_,_,_,_,_)) = vt fun varsubst_of_theorem (Theorem (_,_,_,vs,_,_,_,_)) = vs diff -r 71fef62c4213 -r 122416054a9c src/HOL/Matrix_LP/Compute_Oracle/linker.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Thu Aug 01 16:53:03 2013 +0200 @@ -233,7 +233,7 @@ datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list datatype pcomputer = - PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref * + PComputer of theory * Compute.computer * theorem list Unsynchronized.ref * pattern list Unsynchronized.ref (*fun collect_consts (Var x) = [] @@ -410,14 +410,13 @@ val (_, (pats, ths)) = add_monos thy monocs pats ths val computer = create_computer machine thy pats ths in - PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats) + PComputer (thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats) end fun make machine thy ths cs = make_with_cache machine thy [] ths cs -fun add_instances (PComputer (thyref, computer, rths, rpats)) cs = +fun add_instances (PComputer (thy, computer, rths, rpats)) cs = let - val thy = Theory.deref thyref val (changed, (pats, ths)) = add_monos thy cs (!rpats) (!rths) in if changed then diff -r 71fef62c4213 -r 122416054a9c src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Thu Aug 01 16:53:03 2013 +0200 @@ -198,8 +198,7 @@ val new_type_names' = map (fn n => n ^ "_Rep") new_type_names; - val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy - ||> Theory.checkpoint; + val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy; val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names'); fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr (Datatype.DtRec i); @@ -256,8 +255,7 @@ Primrec.add_primrec_overloaded (map (fn (s, sT) => (s, sT, false)) (List.take (perm_names' ~~ perm_names_types, length new_type_names))) - (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1 - ||> Theory.checkpoint; + (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1; (**** prove that permutation functions introduced by unfolding are ****) (**** equivalent to already existing permutation functions ****) @@ -429,7 +427,6 @@ (s, map (inter_sort thy sort o snd) tvs, [cp_class]) (fn _ => Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy) (full_new_type_names' ~~ tyvars) thy - |> Theory.checkpoint end; val (perm_thmss,thy3) = thy2 |> @@ -454,8 +451,7 @@ ((Binding.name (space_implode "_" new_type_names ^ "_perm_append"), perm_append_thms), [Simplifier.simp_add]), ((Binding.name (space_implode "_" new_type_names ^ "_perm_eq"), - perm_eq_thms), [Simplifier.simp_add])] ||> - Theory.checkpoint; + perm_eq_thms), [Simplifier.simp_add])]; (**** Define representing sets ****) @@ -535,8 +531,7 @@ (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn)) (rep_set_names' ~~ recTs')) [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] - ||> Sign.restore_naming thy3 - ||> Theory.checkpoint; + ||> Sign.restore_naming thy3; (**** Prove that representing set is closed under permutation ****) @@ -598,8 +593,7 @@ (Const (Sign.intern_const thy ("Rep_" ^ Binding.name_of name), T --> U) $ Free ("x", T))))), [])] thy) end)) - (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names)) - ||> Theory.checkpoint; + (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names)); val perm_defs = map snd typedefs; val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs; @@ -628,7 +622,6 @@ [Rep RS perm_closed RS Abs_inverse]) 1, asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Global_Theory.get_thm thy ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy - |> Theory.checkpoint end) (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms); @@ -667,7 +660,7 @@ val thy7 = fold (fn x => fn thy => thy |> pt_instance x |> fold (cp_instance x) (atoms ~~ perm_closed_thmss)) - (atoms ~~ perm_closed_thmss) thy6 |> Theory.checkpoint; + (atoms ~~ perm_closed_thmss) thy6; (**** constructors ****) @@ -767,8 +760,7 @@ val def_name = (Long_Name.base_name cname) ^ "_def"; val ([def_thm], thy') = thy |> Sign.add_consts_i [(cname', constrT, mx)] |> - (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)] ||> - Theory.checkpoint; + (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]; in (thy', defs @ [def_thm], eqns @ [eqn]) end; fun dt_constr_defs ((((((_, (_, _, constrs)), @@ -782,7 +774,7 @@ val (thy', defs', eqns') = fold (make_constr_def tname T T') (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, []) in - (Theory.checkpoint (Sign.parent_path thy'), defs', eqns @ [eqns'], dist_lemmas @ [dist]) + (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist]) end; val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = fold dt_constr_defs @@ -1112,8 +1104,7 @@ in fold (fn Type (s, Ts) => Axclass.prove_arity (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class]) (fn _ => Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy - end) (atoms ~~ finite_supp_thms) ||> - Theory.checkpoint; + end) (atoms ~~ finite_supp_thms); (**** strong induction theorem ****) @@ -1395,8 +1386,7 @@ Sign.add_path big_name |> Global_Theory.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>> Global_Theory.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>> - Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])] ||> - Theory.checkpoint; + Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])]; (**** recursion combinator ****) @@ -1504,8 +1494,7 @@ (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||> Global_Theory.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct") - ||> Sign.restore_naming thy10 - ||> Theory.checkpoint; + ||> Sign.restore_naming thy10; (** equivariance **) @@ -2009,8 +1998,7 @@ (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", 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)) - ||> Theory.checkpoint; + (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)); (* prove characteristic equations for primrec combinators *) @@ -2051,9 +2039,7 @@ ((Binding.name "rec_unique", map Drule.export_without_context rec_unique_thms), []), ((Binding.name "recs", rec_thms), [])] ||> Sign.parent_path ||> - map_nominal_datatypes (fold Symtab.update dt_infos) ||> - Theory.checkpoint; - + map_nominal_datatypes (fold Symtab.update dt_infos); in thy13 end; diff -r 71fef62c4213 -r 122416054a9c src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Thu Aug 01 16:53:03 2013 +0200 @@ -57,7 +57,7 @@ ||> List.partition (has_role TPTP_Syntax.Role_Definition) in (map get_prop conjs, pairself (map get_prop) defs_and_nondefs, - thy |> Theory.checkpoint |> Proof_Context.init_global) + thy |> Proof_Context.init_global) end diff -r 71fef62c4213 -r 122416054a9c src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Thu Aug 01 16:53:03 2013 +0200 @@ -181,8 +181,7 @@ coind = false, no_elim = true, no_ind = false, skip_mono = true} (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] - ||> Sign.restore_naming thy1 - ||> Theory.checkpoint; + ||> Sign.restore_naming thy1; (********************************* typedef ********************************) @@ -349,7 +348,7 @@ Logic.mk_equals (Const (iso_name, T --> Univ_elT), list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos); val (def_thms, thy') = - apsnd Theory.checkpoint ((Global_Theory.add_defs false o map Thm.no_attributes) defs thy); + (Global_Theory.add_defs false o map Thm.no_attributes) defs thy; (* prove characteristic equations *) @@ -361,7 +360,7 @@ in (thy', char_thms' @ char_thms) end; val (thy5, iso_char_thms) = - apfst Theory.checkpoint (fold_rev make_iso_defs (tl descr) (Sign.add_path big_name thy4, [])); + fold_rev make_iso_defs (tl descr) (Sign.add_path big_name thy4, []); (* prove isomorphism properties *) @@ -647,9 +646,7 @@ thy6 |> Global_Theory.note_thmss "" [((Binding.qualify true big_name (Binding.name "induct"), [case_names_induct]), - [([dt_induct], [])])] - ||> Theory.checkpoint; - + [([dt_induct], [])])]; in ((constr_inject', distinct_thms', dt_induct'), thy7) end; @@ -690,7 +687,6 @@ fun prep_specs parse raw_specs thy = let val ctxt = thy - |> Theory.copy |> Sign.add_types_global (map (fn ((b, args, mx), _) => (b, length args, mx)) raw_specs) |> Proof_Context.init_global |> fold (fn ((_, args, _), _) => fold (fn (a, _) => diff -r 71fef62c4213 -r 122416054a9c src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Thu Aug 01 16:53:03 2013 +0200 @@ -97,8 +97,7 @@ fold_map (fn ((tname, atts), thms) => Global_Theory.note_thmss "" [((Binding.qualify true tname (Binding.name name), atts), [(thms, [])])] - #-> (fn [(_, res)] => pair res)) (tnames ~~ attss ~~ thmss) - ##> Theory.checkpoint; + #-> (fn [(_, res)] => pair res)) (tnames ~~ attss ~~ thmss); fun store_thmss name tnames = store_thmss_atts name tnames (replicate (length tnames) []); @@ -106,8 +105,7 @@ fold_map (fn ((tname, atts), thm) => Global_Theory.note_thmss "" [((Binding.qualify true tname (Binding.name name), atts), [([thm], [])])] - #-> (fn [(_, [res])] => pair res)) (tnames ~~ attss ~~ thms) - ##> Theory.checkpoint; + #-> (fn [(_, [res])] => pair res)) (tnames ~~ attss ~~ thms); fun store_thms name tnames = store_thms_atts name tnames (replicate (length tnames) []); diff -r 71fef62c4213 -r 122416054a9c src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Aug 01 16:53:03 2013 +0200 @@ -109,8 +109,7 @@ 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 tyco) + `(fn thy => mk_eq_eqns thy tyco) #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK [((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]), diff -r 71fef62c4213 -r 122416054a9c src/HOL/Tools/Datatype/rep_datatype.ML --- a/src/HOL/Tools/Datatype/rep_datatype.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Thu Aug 01 16:53:03 2013 +0200 @@ -149,8 +149,7 @@ (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] - ||> Sign.restore_naming thy0 - ||> Theory.checkpoint; + ||> Sign.restore_naming thy0; (* prove uniqueness and termination of primrec combinators *) @@ -238,8 +237,7 @@ (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)) - ||> Sign.parent_path - ||> Theory.checkpoint; + ||> Sign.parent_path; (* prove characteristic equations for primrec combinators *) @@ -262,7 +260,6 @@ |> Global_Theory.note_thmss "" [((Binding.name "recs", [Nitpick_Simps.add]), [(rec_thms, [])])] ||> Sign.parent_path - ||> Theory.checkpoint |-> (fn thms => pair (reccomb_names, maps #2 thms)) end; @@ -325,8 +322,7 @@ |> (Global_Theory.add_defs false o map Thm.no_attributes) [def]; in (defs @ [def_thm], thy') end) - (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names) ([], thy1) - ||> Theory.checkpoint; + (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names) ([], thy1); val case_thms = (map o map) (fn t => @@ -479,9 +475,8 @@ in -fun derive_datatype_props config dt_names descr induct inject distinct thy1 = +fun derive_datatype_props config dt_names descr induct inject distinct thy2 = let - val thy2 = thy1 |> Theory.checkpoint; val flat_descr = flat descr; val new_type_names = map Long_Name.base_name dt_names; val _ = diff -r 71fef62c4213 -r 122416054a9c src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Tools/Function/size.ML Thu Aug 01 16:53:03 2013 +0200 @@ -231,7 +231,6 @@ thy |> Sign.root_path |> Sign.add_path prefix - |> Theory.checkpoint |> prove_size_thms info new_type_names |> Sign.restore_naming thy end; diff -r 71fef62c4213 -r 122416054a9c src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 01 16:53:03 2013 +0200 @@ -941,7 +941,7 @@ val T = Sign.the_const_type (Proof_Context.theory_of ctxt) name val t = Const (name, T) val thy' = - Theory.copy (Proof_Context.theory_of ctxt) + Proof_Context.theory_of ctxt |> Predicate_Compile.preprocess preprocess_options t val ctxt' = Proof_Context.init_global thy' val _ = tracing "Generating prolog program..." @@ -1020,7 +1020,7 @@ let val t' = fold_rev absfree (Term.add_frees t []) t val options = code_options_of (Proof_Context.theory_of ctxt) - val thy = Theory.copy (Proof_Context.theory_of ctxt) + val thy = Proof_Context.theory_of ctxt val ((((full_constname, constT), vs'), intro), thy1) = Predicate_Compile_Aux.define_quickcheck_predicate t' thy val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 diff -r 71fef62c4213 -r 122416054a9c src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Aug 01 16:53:03 2013 +0200 @@ -99,7 +99,6 @@ | NONE => ([], thy) else Predicate_Compile_Fun.define_predicates (get_specs funnames) thy else ([], thy)) - (*||> Theory.checkpoint*) val _ = print_specs options thy1 fun_pred_specs val specs = (get_specs prednames) @ fun_pred_specs val (intross3, thy2) = process_specification options specs thy1 @@ -273,7 +272,7 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"} "prove equations for predicate specified by intro/elim rules" - (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd) + (opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd) val _ = Outer_Syntax.improper_command @{command_spec "values"} diff -r 71fef62c4213 -r 122416054a9c src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 01 16:53:03 2013 +0200 @@ -1118,12 +1118,12 @@ val ctxt' = Proof_Context.init_global thy' val rules as ((intro, elim), _) = create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T)) - in thy' + in + thy' |> set_function_name Pred name mode mode_cname |> add_predfun_data name mode (definition, rules) |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd - |> Theory.checkpoint end; in thy |> defined_function_of Pred name |> fold create_definition modes @@ -1366,8 +1366,7 @@ val _ = print_step options "Defining executable functions..." val thy'' = cond_timeit (Config.get ctxt Quickcheck.timing) "Defining executable functions..." - (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy' - |> Theory.checkpoint) + (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy') val ctxt'' = Proof_Context.init_global thy'' val _ = print_step options "Compiling equations..." val compiled_terms = @@ -1388,7 +1387,7 @@ fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [attrib])] thy)) - result_thms' thy'' |> Theory.checkpoint) + result_thms' thy'') in thy''' end @@ -1397,7 +1396,7 @@ let fun dest_steps (Steps s) = s val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps))) - val thy' = extend_intro_graph names thy |> Theory.checkpoint; + val thy' = extend_intro_graph names thy; fun strong_conn_of gr keys = Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr) val scc = strong_conn_of (PredData.get thy') names @@ -1414,7 +1413,7 @@ add_equations_of steps mode_analysis_options options preds thy end else thy) - scc thy'' |> Theory.checkpoint + scc thy'' in thy''' end val add_equations = gen_add_equations diff -r 71fef62c4213 -r 122416054a9c src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Aug 01 16:53:03 2013 +0200 @@ -224,7 +224,7 @@ fun compile_term compilation options ctxt t = let val t' = fold_rev absfree (Term.add_frees t []) t - val thy = Theory.copy (Proof_Context.theory_of ctxt) + val thy = Proof_Context.theory_of ctxt val ((((full_constname, constT), vs'), intro), thy1) = Predicate_Compile_Aux.define_quickcheck_predicate t' thy val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 diff -r 71fef62c4213 -r 122416054a9c src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Thu Aug 01 16:53:03 2013 +0200 @@ -298,7 +298,6 @@ (map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) vs nparms rs) rss); val thy1' = thy1 |> - Theory.copy |> Sign.add_types_global (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |> Extraction.add_typeof_eqns_i ty_eqs; diff -r 71fef62c4213 -r 122416054a9c src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/HOL/Tools/record.ML Thu Aug 01 16:53:03 2013 +0200 @@ -1555,8 +1555,7 @@ val ([ext_def], defs_thy) = timeit_msg ctxt "record extension constructor def:" (fn () => typ_thy |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd - |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])] - ||> Theory.checkpoint); + |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]); (* prepare propositions *) @@ -2009,8 +2008,7 @@ map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs ||>> (Global_Theory.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) - [make_spec, fields_spec, extend_spec, truncate_spec] - ||> Theory.checkpoint); + [make_spec, fields_spec, extend_spec, truncate_spec]); (* prepare propositions *) val _ = timing_msg ctxt "record preparing propositions"; diff -r 71fef62c4213 -r 122416054a9c src/Pure/Concurrent/event_timer.ML --- a/src/Pure/Concurrent/event_timer.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Concurrent/event_timer.ML Thu Aug 01 16:53:03 2013 +0200 @@ -14,6 +14,7 @@ val request: Time.time -> event -> request val cancel: request -> bool val shutdown: unit -> unit + val future: Time.time -> unit future end; structure Event_Timer: EVENT_TIMER = @@ -125,5 +126,16 @@ else if is_none manager then SOME ((), init_state) else NONE); + +(* future *) + +val future = uninterruptible (fn _ => fn time => + let + val req: request Single_Assignment.var = Single_Assignment.var "request"; + fun abort () = ignore (cancel (Single_Assignment.await req)); + val promise: unit future = Future.promise abort; + val _ = Single_Assignment.assign req (request time (Future.fulfill promise)); + in promise end); + end; diff -r 71fef62c4213 -r 122416054a9c src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Isar/class.ML Thu Aug 01 16:53:03 2013 +0200 @@ -566,7 +566,6 @@ | NONE => NONE); in thy - |> Theory.checkpoint |> Proof_Context.init_global |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params)) |> fold (Variable.declare_typ o TFree) vs diff -r 71fef62c4213 -r 122416054a9c src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Isar/class_declaration.ML Thu Aug 01 16:53:03 2013 +0200 @@ -314,7 +314,6 @@ |> Expression.add_locale I b (Binding.qualify true "class" b) supexpr elems |> snd |> Local_Theory.exit_global |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax - ||> Theory.checkpoint |-> (fn (param_map, params, assm_axiom) => `(fn thy => calculate thy class sups base_sort param_map assm_axiom) #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) => diff -r 71fef62c4213 -r 122416054a9c src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Isar/code.ML Thu Aug 01 16:53:03 2013 +0200 @@ -276,11 +276,11 @@ local type data = Any.T Datatab.table; -fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory_ref) option); +fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory) option); structure Code_Data = Theory_Data ( - type T = spec * (data * theory_ref) option Synchronized.var; + type T = spec * (data * theory) option Synchronized.var; val empty = (make_spec (false, (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ()); val extend : T -> T = apsnd (K (empty_dataref ())); @@ -320,7 +320,9 @@ #> map_history_concluded (K true)) |> SOME; -val _ = Context.>> (Context.map_theory (Theory.at_begin continue_history #> Theory.at_end conclude_history)); +val _ = + Context.>> (Context.map_theory + (Theory.at_begin continue_history #> Theory.at_end conclude_history)); (* access to data dependent on abstract executable code *) @@ -328,17 +330,18 @@ fun change_yield_data (kind, mk, dest) theory f = let val dataref = (snd o Code_Data.get) theory; - val (datatab, thy_ref) = case Synchronized.value dataref - of SOME (datatab, thy_ref) => if Theory.eq_thy (theory, Theory.deref thy_ref) - then (datatab, thy_ref) - else (Datatab.empty, Theory.check_thy theory) - | NONE => (Datatab.empty, Theory.check_thy theory) + val (datatab, thy) = case Synchronized.value dataref + of SOME (datatab, thy) => + if Theory.eq_thy (theory, thy) + then (datatab, thy) + else (Datatab.empty, theory) + | NONE => (Datatab.empty, theory) val data = case Datatab.lookup datatab kind of SOME data => data | NONE => invoke_init kind; val result as (_, data') = f (dest data); val _ = Synchronized.change dataref - ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref)); + ((K o SOME) (Datatab.update (kind, mk data') datatab, thy)); in result end; end; (*local*) @@ -1039,7 +1042,7 @@ let val thm = Thm.close_derivation raw_thm; val c = const_eqn thy thm; - fun update_subsume thy verbose (thm, proper) eqns = + fun update_subsume verbose (thm, proper) eqns = let val args_of = snd o take_prefix is_Var o rev o snd o strip_comb o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of; @@ -1058,13 +1061,12 @@ Display.string_of_thm_global thy thm') else (); true) else false; in (thm, proper) :: filter_out drop eqns end; - fun natural_order thy_ref eqns = - (eqns, Lazy.lazy (fn () => fold (update_subsume (Theory.deref thy_ref) false) eqns [])) - fun add_eqn' true (Default (eqns, _)) = - Default (natural_order (Theory.check_thy thy) ((thm, proper) :: eqns)) + fun natural_order eqns = + (eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns [])) + fun add_eqn' true (Default (eqns, _)) = Default (natural_order ((thm, proper) :: eqns)) (*this restores the natural order and drops syntactic redundancies*) | add_eqn' true fun_spec = fun_spec - | add_eqn' false (Eqns eqns) = Eqns (update_subsume thy true (thm, proper) eqns) + | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns) | add_eqn' false _ = Eqns [(thm, proper)]; in change_fun_spec false c (add_eqn' default) thy end; @@ -1152,7 +1154,6 @@ (K ((map o apsnd o apsnd) register_for_constructors)); in thy - |> Theory.checkpoint |> `(fn thy => case_cong thy case_const entry) |-> (fn cong => map_exec_purge (register_case cong #> register_type)) end; diff -r 71fef62c4213 -r 122416054a9c src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Isar/element.ML Thu Aug 01 16:53:03 2013 +0200 @@ -50,7 +50,6 @@ val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism val satisfy_morphism: witness list -> morphism val eq_morphism: theory -> thm list -> morphism option - val transfer_morphism: theory -> morphism val init: context_i -> Context.generic -> Context.generic val activate_i: context_i -> Proof.context -> context_i * Proof.context val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context @@ -392,13 +391,11 @@ in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end; fun instT_morphism thy env = - let val thy_ref = Theory.check_thy thy in - Morphism.morphism - {binding = [], - typ = [instT_type env], - term = [instT_term env], - fact = [map (fn th => instT_thm (Theory.deref thy_ref) env th)]} - end; + Morphism.morphism + {binding = [], + typ = [instT_type env], + term = [instT_term env], + fact = [map (instT_thm thy env)]}; (* instantiate types and terms *) @@ -437,13 +434,11 @@ end; fun inst_morphism thy (envT, env) = - let val thy_ref = Theory.check_thy thy in - Morphism.morphism - {binding = [], - typ = [instT_type envT], - term = [inst_term (envT, env)], - fact = [map (fn th => inst_thm (Theory.deref thy_ref) (envT, env) th)]} - end; + Morphism.morphism + {binding = [], + typ = [instT_type envT], + term = [inst_term (envT, env)], + fact = [map (inst_thm thy (envT, env))]}; (* satisfy hypotheses *) @@ -468,13 +463,6 @@ fact = [map (rewrite_rule thms)]}); -(* transfer to theory using closure *) - -fun transfer_morphism thy = - let val thy_ref = Theory.check_thy thy - in Morphism.thm_morphism (fn th => Thm.transfer (Theory.deref thy_ref) th) end; - - (** activate in context **) diff -r 71fef62c4213 -r 122416054a9c src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Isar/local_theory.ML Thu Aug 01 16:53:03 2013 +0200 @@ -205,15 +205,12 @@ fun raw_theory f = #2 o raw_theory_result (f #> pair ()); -val checkpoint = raw_theory Theory.checkpoint; - fun background_theory_result f lthy = lthy |> raw_theory_result (fn thy => thy |> Sign.map_naming (K (naming_of lthy)) |> f - ||> Sign.restore_naming thy - ||> Theory.checkpoint); + ||> Sign.restore_naming thy); fun background_theory f = #2 o background_theory_result (f #> pair ()); @@ -256,11 +253,11 @@ fun operation2 f x y = operation (fn ops => f ops x y); val pretty = operation #pretty; -val abbrev = apsnd checkpoint ooo operation2 #abbrev; -val define = apsnd checkpoint oo operation2 #define false; -val define_internal = apsnd checkpoint oo operation2 #define true; -val notes_kind = apsnd checkpoint ooo operation2 #notes; -val declaration = checkpoint ooo operation2 #declaration; +val abbrev = operation2 #abbrev; +val define = operation2 #define false; +val define_internal = operation2 #define true; +val notes_kind = operation2 #notes; +val declaration = operation2 #declaration; (* basic derived operations *) @@ -322,13 +319,12 @@ fun init naming operations target = target |> Data.map (fn [] => [make_lthy (naming, operations, I, false, target)] - | _ => error "Local theory already initialized") - |> checkpoint; + | _ => error "Local theory already initialized"); (* exit *) -val exit = Proof_Context.background_theory Theory.checkpoint o operation #exit; +val exit = operation #exit; val exit_global = Proof_Context.theory_of o exit; fun exit_result f (x, lthy) = diff -r 71fef62c4213 -r 122416054a9c src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Isar/locale.ML Thu Aug 01 16:53:03 2013 +0200 @@ -431,6 +431,8 @@ (** Public activation functions **) +fun transfer_morphism thy = Morphism.thm_morphism (Thm.transfer thy); + fun activate_declarations dep = Context.proof_map (fn context => let val thy = Context.theory_of context; @@ -443,14 +445,14 @@ let val thy = Context.theory_of context; val activate = - activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export; + activate_notes Element.init (transfer_morphism o Context.theory_of) context export; in roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context) |-> Idents.put end; fun init name thy = - activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of) + activate_all name thy Element.init (transfer_morphism o Context.theory_of) (empty_idents, Context.Proof (Proof_Context.init_global thy)) |-> Idents.put |> Context.proof_of; @@ -628,7 +630,7 @@ fun cons_elem (elem as Notes _) = show_facts ? cons elem | cons_elem elem = cons elem; val elems = - activate_all name thy cons_elem (K (Element.transfer_morphism thy)) (empty_idents, []) + activate_all name thy cons_elem (K (transfer_morphism thy)) (empty_idents, []) |> snd |> rev; in Pretty.block diff -r 71fef62c4213 -r 122416054a9c src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Isar/overloading.ML Thu Aug 01 16:53:03 2013 +0200 @@ -194,7 +194,6 @@ (Term.dest_Const (prep_const ctxt const), (v, checked))); in thy - |> Theory.checkpoint |> Proof_Context.init_global |> Data.put overloading |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading diff -r 71fef62c4213 -r 122416054a9c src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Isar/toplevel.ML Thu Aug 01 16:53:03 2013 +0200 @@ -269,7 +269,6 @@ val (result, err) = cont_node |> Runtime.controlled_execution f - |> map_theory Theory.checkpoint |> state_error NONE handle exn => state_error (SOME exn) cont_node; in @@ -298,8 +297,7 @@ local fun apply_tr _ (Init f) (State (NONE, _)) = - State (SOME (Theory (Context.Theory - (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE) + State (SOME (Theory (Context.Theory (Runtime.controlled_execution f ()), NONE)), NONE) | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) = exit_transaction state | apply_tr int (Keep f) state = @@ -421,7 +419,6 @@ (fn Theory (Context.Theory thy, _) => let val thy' = thy |> Sign.new_group - |> Theory.checkpoint |> f int |> Sign.reset_group; in Theory (Context.Theory thy', NONE) end @@ -529,9 +526,9 @@ fun theory_to_proof f = begin_proof (fn _ => fn gthy => - (Context.Theory o Theory.checkpoint o Sign.reset_group o Proof_Context.theory_of, + (Context.Theory o Sign.reset_group o Proof_Context.theory_of, (case gthy of - Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) + Context.Theory thy => f (Sign.new_group thy) | _ => raise UNDEF))); end; diff -r 71fef62c4213 -r 122416054a9c src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/PIDE/command.ML Thu Aug 01 16:53:03 2013 +0200 @@ -9,6 +9,7 @@ val read: (unit -> theory) -> Token.T list -> Toplevel.transition type eval val eval_eq: eval * eval -> bool + val eval_running: eval -> bool val eval_finished: eval -> bool val eval_result_state: eval -> Toplevel.state val eval: (unit -> theory) -> Token.T list -> eval -> eval @@ -46,9 +47,7 @@ | Result res => Exn.release res); fun memo_finished (Memo v) = - (case Synchronized.value v of - Expr _ => false - | Result _ => true); + (case Synchronized.value v of Expr _ => false | Result _ => true); fun memo_exec execution_id (Memo v) = Synchronized.timed_access v (K (SOME Time.zeroTime)) @@ -120,6 +119,7 @@ fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id'; +fun eval_running (Eval {exec_id, ...}) = Execution.is_running_exec exec_id; fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process; fun eval_result (Eval {eval_process, ...}) = memo_result eval_process; diff -r 71fef62c4213 -r 122416054a9c src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/PIDE/document.ML Thu Aug 01 16:53:03 2013 +0200 @@ -7,19 +7,19 @@ signature DOCUMENT = sig + val timing: bool Unsynchronized.ref type node_header = string * Thy_Header.header * string list datatype node_edit = Clear | (* FIXME unused !? *) Edits of (Document_ID.command option * Document_ID.command option) list | Deps of node_header | - Perspective of Document_ID.command list + Perspective of bool * Document_ID.command list type edit = string * node_edit type state val init_state: state val define_command: Document_ID.command -> string -> string -> state -> state val remove_versions: Document_ID.version list -> state -> state val start_execution: state -> state - val timing: bool Unsynchronized.ref val update: Document_ID.version -> Document_ID.version -> edit list -> state -> Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state val state: unit -> state @@ -29,18 +29,23 @@ structure Document: DOCUMENT = struct +val timing = Unsynchronized.ref false; +fun timeit msg e = cond_timeit (! timing) msg e; + + + (** document structure **) fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id); fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id); type node_header = string * Thy_Header.header * string list; -type perspective = Inttab.set * Document_ID.command option; +type perspective = bool * Inttab.set * Document_ID.command option; structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord); abstype node = Node of {header: node_header, (*master directory, theory header, errors*) - perspective: perspective, (*visible commands, last visible command*) + perspective: perspective, (*required node, visible commands, last visible command*) entries: Command.exec option Entries.T, (*command entries with excecutions*) result: Command.eval option} (*result of last execution*) and version = Version of node String_Graph.T (*development graph wrt. static imports*) @@ -52,11 +57,11 @@ fun map_node f (Node {header, perspective, entries, result}) = make_node (f (header, perspective, entries, result)); -fun make_perspective command_ids : perspective = - (Inttab.make_set command_ids, try List.last command_ids); +fun make_perspective (required, command_ids) : perspective = + (required, Inttab.make_set command_ids, try List.last command_ids); val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]); -val no_perspective = make_perspective []; +val no_perspective = make_perspective (false, []); val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE); val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE)); @@ -78,11 +83,12 @@ in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end; fun get_perspective (Node {perspective, ...}) = perspective; -fun set_perspective ids = - map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result)); +fun set_perspective args = + map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result)); -val visible_command = Inttab.defined o #1 o get_perspective; -val visible_last = #2 o get_perspective; +val required_node = #1 o get_perspective; +val visible_command = Inttab.defined o #2 o get_perspective; +val visible_last = #3 o get_perspective; val visible_node = is_some o visible_last fun map_entries f = @@ -122,7 +128,7 @@ Clear | Edits of (Document_ID.command option * Document_ID.command option) list | Deps of node_header | - Perspective of Document_ID.command list; + Perspective of bool * Document_ID.command list; type edit = string * node_edit; @@ -199,13 +205,16 @@ type execution = {version_id: Document_ID.version, (*static version id*) execution_id: Document_ID.execution, (*dynamic execution id*) + delay_request: unit future, (*pending event timer request*) frontier: Future.task Symtab.table}; (*node name -> running execution task*) val no_execution: execution = - {version_id = Document_ID.none, execution_id = Document_ID.none, frontier = Symtab.empty}; + {version_id = Document_ID.none, execution_id = Document_ID.none, + delay_request = Future.value (), frontier = Symtab.empty}; -fun new_execution version_id frontier : execution = - {version_id = version_id, execution_id = Execution.start (), frontier = frontier}; +fun new_execution version_id delay_request frontier : execution = + {version_id = version_id, execution_id = Execution.start (), + delay_request = delay_request, frontier = frontier}; abstype state = State of {versions: version Inttab.table, (*version id -> document content*) @@ -226,11 +235,11 @@ (* document versions *) fun define_version version_id version = - map_state (fn (versions, commands, {frontier, ...}) => + map_state (fn (versions, commands, {delay_request, frontier, ...}) => let val versions' = Inttab.update_new (version_id, version) versions handle Inttab.DUP dup => err_dup "document version" dup; - val execution' = new_execution version_id frontier; + val execution' = new_execution version_id delay_request frontier; in (versions', commands, execution') end); fun the_version (State {versions, ...}) version_id = @@ -292,17 +301,22 @@ (* document execution *) fun start_execution state = state |> map_state (fn (versions, commands, execution) => - let - val {version_id, execution_id, frontier} = execution; - val pri = Options.default_int "editor_execution_priority"; + timeit "Document.start_execution" (fn () => + let + val {version_id, execution_id, delay_request, frontier} = execution; - val new_tasks = - if Execution.is_running execution_id then + val delay = seconds (Options.default_real "editor_execution_delay"); + + val _ = Future.cancel delay_request; + val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay)); + + val new_tasks = nodes_of (the_version state version_id) |> String_Graph.schedule (fn deps => fn (name, node) => if visible_node node orelse pending_result node then let - val former_task = Symtab.lookup frontier name; + val more_deps = + Future.task_of delay_request' :: the_list (Symtab.lookup frontier name); fun body () = iterate_entries (fn (_, opt_exec) => fn () => (case opt_exec of @@ -315,14 +329,15 @@ val future = (singleton o Future.forks) {name = "theory:" ^ name, group = SOME (Future.new_group NONE), - deps = the_list former_task @ map #2 (maps #2 deps), - pri = pri, interrupts = false} body; + deps = more_deps @ map #2 (maps #2 deps), + pri = 0, interrupts = false} body; in [(name, Future.task_of future)] end - else []) - else []; - val frontier' = (fold o fold) Symtab.update new_tasks frontier; - val execution' = {version_id = version_id, execution_id = execution_id, frontier = frontier'}; - in (versions, commands, execution') end); + else []); + val frontier' = (fold o fold) Symtab.update new_tasks frontier; + val execution' = + {version_id = version_id, execution_id = execution_id, + delay_request = delay_request', frontier = frontier'}; + in (versions, commands, execution') end)); @@ -346,23 +361,22 @@ (* update *) -val timing = Unsynchronized.ref false; -fun timeit msg e = cond_timeit (! timing) msg e; - local fun make_required nodes = let - val all_visible = - String_Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] + fun all_preds P = + String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes [] |> String_Graph.all_preds nodes - |> map (rpair ()) |> Symtab.make; + |> Symtab.make_set; - val required = - Symtab.fold (fn (a, ()) => - exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ? - Symtab.update (a, ())) all_visible Symtab.empty; - in required end; + val all_visible = all_preds visible_node; + val all_required = all_preds required_node; + in + Symtab.fold (fn (a, ()) => + exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ? + Symtab.update (a, ())) all_visible all_required + end; fun init_theory deps node span = let @@ -389,7 +403,7 @@ is_some (Thy_Info.lookup_theory name) orelse can get_header node andalso (not full orelse is_some (get_result node)); -fun last_common state node0 node = +fun last_common state node_required node0 node = let fun update_flags prev (visible, initial) = let @@ -400,15 +414,17 @@ | SOME command_id => not (Keyword.is_theory_begin (the_command_name state command_id))); in (visible', initial') end; - fun get_common ((prev, command_id), opt_exec) (_, same, flags, assign_update) = - if same then + fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) = + if ok then let - val flags' = update_flags prev flags; - val same' = + val flags' as (visible', _) = update_flags prev flags; + val ok' = (case (lookup_entry node0 command_id, opt_exec) of - (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval) + (SOME (eval0, _), SOME (eval, _)) => + Command.eval_eq (eval0, eval) andalso + (visible' orelse node_required orelse Command.eval_running eval) | _ => false); - val assign_update' = assign_update |> same' ? + val assign_update' = assign_update |> ok' ? (case opt_exec of SOME (eval, prints) => let @@ -420,12 +436,12 @@ | NONE => I) end | NONE => I); - in SOME (prev, same', flags', assign_update') end + in SOME (prev, ok', flags', assign_update') end else NONE; - val (common, same, flags, assign_update') = + val (common, ok, flags, assign_update') = iterate_entries get_common node (NONE, true, (true, true), assign_update_empty); val (common', flags') = - if same then + if ok then let val last = Entries.get_after (get_entries node) common in (last, update_flags last flags) end else (common, flags); @@ -469,7 +485,7 @@ (singleton o Future.forks) {name = "Document.update", group = NONE, deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} - (fn () => + (fn () => timeit ("Document.update " ^ name) (fn () => let val imports = map (apsnd Future.join) deps; val imports_result_changed = exists (#4 o #1 o #2) imports; @@ -487,7 +503,7 @@ val (print_execs, common, (still_visible, initial)) = if imports_result_changed then (assign_update_empty, NONE, (true, true)) - else last_common state node0 node; + else last_common state node_required node0 node; val common_command_exec = the_default_entry node common; val (updated_execs, (command_id', (eval', _)), _) = @@ -522,7 +538,7 @@ val result_changed = changed_result node0 node'; in ((removed, assign_update, assigned_node, result_changed), node') end else (([], [], NONE, false), node) - end)) + end))) |> Future.joins |> map #1); val removed = maps #1 updated; diff -r 71fef62c4213 -r 122416054a9c src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/PIDE/document.scala Thu Aug 01 16:53:03 2013 +0200 @@ -66,7 +66,8 @@ case class Clear[A, B]() extends Edit[A, B] case class Edits[A, B](edits: List[A]) extends Edit[A, B] case class Deps[A, B](header: Header) extends Edit[A, B] - case class Perspective[A, B](perspective: B) extends Edit[A, B] + case class Perspective[A, B](required: Boolean, perspective: B) extends Edit[A, B] + type Perspective_Text = Perspective[Text.Edit, Text.Perspective] def command_starts(commands: Iterator[Command], offset: Text.Offset = 0) : Iterator[(Command, Text.Offset)] = @@ -86,7 +87,7 @@ final class Node private( val header: Node.Header = Node.bad_header("Bad theory header"), - val perspective: Command.Perspective = Command.Perspective.empty, + val perspective: (Boolean, Command.Perspective) = (false, Command.Perspective.empty), val commands: Linear_Set[Command] = Linear_Set.empty) { def clear: Node = new Node(header = header) @@ -94,9 +95,12 @@ def update_header(new_header: Node.Header): Node = new Node(new_header, perspective, commands) - def update_perspective(new_perspective: Command.Perspective): Node = + def update_perspective(new_perspective: (Boolean, Command.Perspective)): Node = new Node(header, new_perspective, commands) + def same_perspective(other: (Boolean, Command.Perspective)): Boolean = + perspective._1 == other._1 && (perspective._2 same other._2) + def update_commands(new_commands: Linear_Set[Command]): Node = new Node(header, perspective, new_commands) diff -r 71fef62c4213 -r 122416054a9c src/Pure/PIDE/execution.ML --- a/src/Pure/PIDE/execution.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/PIDE/execution.ML Thu Aug 01 16:53:03 2013 +0200 @@ -7,9 +7,11 @@ signature EXECUTION = sig + val reset: unit -> unit val start: unit -> Document_ID.execution val discontinue: unit -> unit val is_running: Document_ID.execution -> bool + val is_running_exec: Document_ID.exec -> bool val running: Document_ID.execution -> Document_ID.exec -> bool val cancel: Document_ID.exec -> unit val terminate: Document_ID.exec -> unit @@ -18,13 +20,18 @@ structure Execution: EXECUTION = struct -val state = - Synchronized.var "Execution.state" - (Document_ID.none, Inttab.empty: Future.group Inttab.table); +(* global state *) + +type state = Document_ID.execution * Future.group Inttab.table; + +val init_state: state = (Document_ID.none, Inttab.empty); +val state = Synchronized.var "Execution.state" init_state; (* unique running execution *) +fun reset () = Synchronized.change state (K init_state); + fun start () = let val execution_id = Document_ID.make (); @@ -39,6 +46,9 @@ (* registered execs *) +fun is_running_exec exec_id = + Inttab.defined (snd (Synchronized.value state)) exec_id; + fun running execution_id exec_id = Synchronized.guarded_access state (fn (execution_id', execs) => diff -r 71fef62c4213 -r 122416054a9c src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/PIDE/markup.ML Thu Aug 01 16:53:03 2013 +0200 @@ -142,6 +142,7 @@ val padding_command: Properties.entry val dialogN: string val dialog: serial -> string -> T val functionN: string + val flush: Properties.T val assign_update: Properties.T val removed_versions: Properties.T val protocol_handler: string -> Properties.T @@ -463,6 +464,8 @@ val functionN = "function" +val flush = [(functionN, "flush")]; + val assign_update = [(functionN, "assign_update")]; val removed_versions = [(functionN, "removed_versions")]; diff -r 71fef62c4213 -r 122416054a9c src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/PIDE/markup.scala Thu Aug 01 16:53:03 2013 +0200 @@ -315,6 +315,8 @@ val FUNCTION = "function" val Function = new Properties.String(FUNCTION) + val Flush: Properties.T = List((FUNCTION, "flush")) + val Assign_Update: Properties.T = List((FUNCTION, "assign_update")) val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions")) diff -r 71fef62c4213 -r 122416054a9c src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/PIDE/protocol.ML Thu Aug 01 16:53:03 2013 +0200 @@ -8,7 +8,19 @@ struct val _ = - Isabelle_Process.protocol_command "echo" (fn args => List.app writeln args); + Isabelle_Process.protocol_command "Isabelle_Process.echo" + (fn args => List.app writeln args); + +val _ = + Isabelle_Process.protocol_command "Isabelle_Process.options" + (fn [options_yxml] => + let val options = Options.decode (YXML.parse_body options_yxml) in + Options.set_default options; + Future.ML_statistics := true; + Multithreading.trace := Options.int options "threads_trace"; + Multithreading.max_threads := Options.int options "threads"; + Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0) + end); val _ = Isabelle_Process.protocol_command "Document.define_command" @@ -44,7 +56,7 @@ val imports' = map (rpair Position.none) imports; val header = Thy_Header.make (name, Position.none) imports' keywords; in Document.Deps (master, header, errors) end, - fn (a, []) => Document.Perspective (map int_atom a)])) + fn (a :: b, []) => Document.Perspective (bool_atom a, map int_atom b)])) end; val (removed, assign_update, state') = Document.update old_id new_id edits state; diff -r 71fef62c4213 -r 122416054a9c src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/PIDE/protocol.scala Thu Aug 01 16:53:03 2013 +0200 @@ -340,7 +340,8 @@ option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))), list(Encode.string)))))( (dir, (name.theory, (imports, (keywords, header.errors)))))) }, - { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) + { case Document.Node.Perspective(a, b) => + (bool_atom(a) :: b.commands.map(c => long_atom(c.id)), Nil) })) def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => { val (name, edit) = node_edit diff -r 71fef62c4213 -r 122416054a9c src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Proof/extraction.ML Thu Aug 01 16:53:03 2013 +0200 @@ -35,8 +35,7 @@ val typ = Simple_Syntax.read_typ; val add_syntax = - Theory.copy - #> Sign.root_path + Sign.root_path #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)] #> Sign.add_consts_i [(Binding.name "typeof", typ "'b => Type", NoSyn), diff -r 71fef62c4213 -r 122416054a9c src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Thu Aug 01 16:53:03 2013 +0200 @@ -41,7 +41,6 @@ fun add_proof_syntax thy = thy - |> Theory.copy |> Sign.root_path |> Sign.set_defsort [] |> Sign.add_types_global [(Binding.name "proof", 0, NoSyn)] diff -r 71fef62c4213 -r 122416054a9c src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/ROOT.ML Thu Aug 01 16:53:03 2013 +0200 @@ -70,8 +70,6 @@ (* concurrency within the ML runtime *) -use "Concurrent/event_timer.ML"; - if ML_System.is_polyml then use "ML/exn_properties_polyml.ML" else use "ML/exn_properties_dummy.ML"; @@ -84,8 +82,6 @@ if Multithreading.available then () else use "Concurrent/single_assignment_sequential.ML"; -if ML_System.is_polyml then use "Concurrent/time_limit.ML" else (); - if Multithreading.available then use "Concurrent/bash.ML" else use "Concurrent/bash_sequential.ML"; @@ -93,6 +89,9 @@ use "Concurrent/par_exn.ML"; use "Concurrent/task_queue.ML"; use "Concurrent/future.ML"; +use "Concurrent/event_timer.ML"; + +if ML_System.is_polyml then use "Concurrent/time_limit.ML" else (); use "Concurrent/lazy.ML"; if Multithreading.available then () @@ -315,7 +314,6 @@ toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm"; toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp"; toplevel_pp ["Context", "theory"] "Context.pretty_thy"; -toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; toplevel_pp ["Ast", "ast"] "Ast.pretty_ast"; toplevel_pp ["Path", "T"] "Path.pretty"; diff -r 71fef62c4213 -r 122416054a9c src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/System/isabelle_process.ML Thu Aug 01 16:53:03 2013 +0200 @@ -3,14 +3,6 @@ Isabelle process wrapper, based on private fifos for maximum robustness and performance, or local socket for maximum portability. - -Startup phases: - - raw Posix process startup with uncontrolled output on stdout/stderr - - stderr \002: ML running - - stdin/stdout/stderr freely available (raw ML loop) - - protocol thread initialization - - rendezvous on system channel - - message INIT: channels ready *) signature ISABELLE_PROCESS = @@ -41,7 +33,8 @@ local val commands = - Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table); + Synchronized.var "Isabelle_Process.commands" + (Symtab.empty: (string list -> unit) Symtab.table); in @@ -98,20 +91,7 @@ end); -(* message channels *) - -local - -fun chunk s = [string_of_int (size s), "\n", s]; - -fun message do_flush msg_channel name raw_props body = - let - val robust_props = map (pairself YXML.embed_controls) raw_props; - val header = YXML.string_of (XML.Elem ((name, robust_props), [])); - val msg = chunk header @ chunk body; - in Message_Channel.send msg_channel msg do_flush end; - -in +(* output channels *) fun init_channels channel = let @@ -120,10 +100,13 @@ val msg_channel = Message_Channel.make channel; + fun message name props body = + Message_Channel.send msg_channel (Message_Channel.message name props body); + fun standard_message opt_serial name body = if body = "" then () else - message false msg_channel name + message name ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I) (Position.properties_of (Position.thread_data ()))) body; in @@ -138,15 +121,13 @@ (fn s => standard_message (SOME (serial ())) Markup.warningN s); Output.Private_Hooks.error_fn := (fn (i, s) => standard_message (SOME i) Markup.errorN s); - Output.Private_Hooks.protocol_message_fn := message true msg_channel Markup.protocolN; + Output.Private_Hooks.protocol_message_fn := message Markup.protocolN; Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn; Output.Private_Hooks.prompt_fn := ignore; - message true msg_channel Markup.initN [] (Session.welcome ()); + message Markup.initN [] (Session.welcome ()); msg_channel end; -end; - (* protocol loop -- uninterruptible *) @@ -163,12 +144,14 @@ val n = (case Int.fromString len of SOME n => n - | NONE => error ("Isabelle process: malformed chunk header " ^ quote len)); + | NONE => error ("Isabelle process: malformed header " ^ quote len)); val chunk = System_Channel.inputN channel n; - val m = size chunk; + val i = size chunk; in - if m = n then chunk - else error ("Isabelle process: bad chunk (" ^ string_of_int m ^ " vs. " ^ string_of_int n ^ ")") + if i <> n then + error ("Isabelle process: bad chunk (unexpected EOF after " ^ + string_of_int i ^ " of " ^ string_of_int n ^ " bytes)") + else chunk end; fun read_command channel = @@ -190,7 +173,7 @@ | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true); in if continue then loop channel - else (Future.shutdown (); Goal.reset_futures (); ()) + else (Future.shutdown (); Goal.reset_futures (); Execution.reset ()) end; end; @@ -221,19 +204,5 @@ fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2); fun init_socket name = init (fn () => System_Channel.socket_rendezvous name); - -(* options *) - -val _ = - protocol_command "Isabelle_Process.options" - (fn [options_yxml] => - let val options = Options.decode (YXML.parse_body options_yxml) in - Options.set_default options; - Future.ML_statistics := true; - Multithreading.trace := Options.int options "threads_trace"; - Multithreading.max_threads := Options.int options "threads"; - Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0) - end); - end; diff -r 71fef62c4213 -r 122416054a9c src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/System/isabelle_process.scala Thu Aug 01 16:53:03 2013 +0200 @@ -289,10 +289,9 @@ val default_buffer = new Array[Byte](65536) var c = -1 - def read_chunk(do_decode: Boolean): XML.Body = + def read_int(): Int = + //{{{ { - //{{{ - // chunk size var n = 0 c = stream.read if (c == -1) throw new EOF @@ -300,9 +299,16 @@ n = 10 * n + (c - 48) c = stream.read } - if (c != 10) throw new Protocol_Error("bad message chunk header") + if (c != 10) + throw new Protocol_Error("malformed header: expected integer followed by newline") + else n + } + //}}} - // chunk content + def read_chunk(do_decode: Boolean): XML.Body = + //{{{ + { + val n = read_int() val buf = if (n <= default_buffer.size) default_buffer else new Array[Byte](n) @@ -312,20 +318,21 @@ do { m = stream.read(buf, i, n - i) if (m != -1) i += m - } while (m != -1 && n > i) + } + while (m != -1 && n > i) - if (i != n) throw new Protocol_Error("bad message chunk content") + if (i != n) + throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)") if (do_decode) YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n)) else List(XML.Text(UTF8.decode_chars(s => s, buf, 0, n).toString)) - //}}} } + //}}} try { do { try { - //{{{ val header = read_chunk(true) header match { case List(XML.Elem(Markup(name, props), Nil)) => @@ -336,10 +343,10 @@ read_chunk(false) throw new Protocol_Error("bad header: " + header.toString) } - //}}} } catch { case _: EOF => } - } while (c != -1) + } + while (c != -1) } catch { case e: IOException => system_output("Cannot read message:\n" + e.getMessage) diff -r 71fef62c4213 -r 122416054a9c src/Pure/System/message_channel.ML --- a/src/Pure/System/message_channel.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/System/message_channel.ML Thu Aug 01 16:53:03 2013 +0200 @@ -6,8 +6,10 @@ signature MESSAGE_CHANNEL = sig + type message + val message: string -> Properties.T -> string -> message type T - val send: T -> string list -> bool -> unit + val send: T -> message -> unit val shutdown: T -> unit val make: System_Channel.T -> T end; @@ -15,25 +17,46 @@ structure Message_Channel: MESSAGE_CHANNEL = struct -datatype T = Message_Channel of - {send: string list -> bool -> unit, - shutdown: unit -> unit}; +(* message *) + +datatype message = Message of string list; + +fun chunk s = [string_of_int (size s), "\n", s]; + +fun message name raw_props body = + let + val robust_props = map (pairself YXML.embed_controls) raw_props; + val header = YXML.string_of (XML.Elem ((name, robust_props), [])); + in Message (chunk header @ chunk body) end; + +fun output_message channel (Message ss) = + List.app (System_Channel.output channel) ss; + + +(* flush *) + +fun flush channel = ignore (try System_Channel.flush channel); + +val flush_message = message Markup.protocolN Markup.flush ""; +fun flush_output channel = (output_message channel flush_message; flush channel); + + +(* channel *) + +datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit}; fun send (Message_Channel {send, ...}) = send; fun shutdown (Message_Channel {shutdown, ...}) = shutdown (); -fun flush channel = ignore (try System_Channel.flush channel); - fun message_output mbox channel = let fun loop receive = (case receive mbox of - SOME NONE => flush channel - | SOME (SOME (msg, do_flush)) => - (List.app (fn s => System_Channel.output channel s) msg; - if do_flush then flush channel else (); + SOME NONE => flush_output channel + | SOME (SOME msg) => + (output_message channel msg; loop (Mailbox.receive_timeout (seconds 0.02))) - | NONE => (flush channel; loop (SOME o Mailbox.receive))); + | NONE => (flush_output channel; loop (SOME o Mailbox.receive))); in fn () => loop (SOME o Mailbox.receive) end; fun make channel = @@ -41,14 +64,14 @@ let val mbox = Mailbox.create (); val thread = Simple_Thread.fork false (message_output mbox channel); - fun send msg do_flush = Mailbox.send mbox (SOME (msg, do_flush)); + fun send msg = Mailbox.send mbox (SOME msg); fun shutdown () = (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread); in Message_Channel {send = send, shutdown = shutdown} end else let - fun send msg = (List.app (fn s => System_Channel.output channel s) msg; flush channel); - in Message_Channel {send = fn msg => fn _ => send msg, shutdown = fn () => ()} end; + fun send msg = (output_message channel msg; flush channel); + in Message_Channel {send = send, shutdown = fn () => ()} end; end; diff -r 71fef62c4213 -r 122416054a9c src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/System/session.scala Thu Aug 01 16:53:03 2013 +0200 @@ -119,7 +119,7 @@ /* tuning parameters */ def output_delay: Time = Time.seconds(0.1) // prover output (markup, common messages) - def message_delay: Time = Time.seconds(0.01) // incoming prover messages + def message_delay: Time = Time.seconds(0.1) // prover input/output messages def prune_delay: Time = Time.seconds(60.0) // prune history -- delete old versions def prune_size: Int = 0 // size of retained history def syslog_limit: Int = 100 @@ -260,7 +260,7 @@ { private var buffer = new mutable.ListBuffer[Isabelle_Process.Message] - def flush(): Unit = synchronized { + private def flush(): Unit = synchronized { if (!buffer.isEmpty) { val msgs = buffer.toList this_actor ! Messages(msgs) @@ -268,17 +268,20 @@ } } def invoke(msg: Isabelle_Process.Message): Unit = synchronized { - buffer += msg msg match { + case _: Isabelle_Process.Input => + buffer += msg case output: Isabelle_Process.Output => - if (output.is_syslog) - syslog >> (queue => - { - val queue1 = queue.enqueue(output.message) - if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1 - }) - if (output.is_protocol) flush() - case _ => + if (output.is_protocol && output.properties == Markup.Flush) flush() + else { + buffer += msg + if (output.is_syslog) + syslog >> (queue => + { + val queue1 = queue.enqueue(output.message) + if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1 + }) + } } } diff -r 71fef62c4213 -r 122416054a9c src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Thy/thy_load.ML Thu Aug 01 16:53:03 2013 +0200 @@ -210,8 +210,7 @@ fun begin_theory master_dir {name, imports, keywords} parents = Theory.begin_theory name parents |> put_deps master_dir imports - |> fold Thy_Header.declare_keyword keywords - |> Theory.checkpoint; + |> fold Thy_Header.declare_keyword keywords; fun excursion last_timing init elements = let diff -r 71fef62c4213 -r 122416054a9c src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Thu Aug 01 16:53:03 2013 +0200 @@ -311,17 +311,17 @@ case (name, Document.Node.Edits(text_edits)) => val commands0 = node.commands val commands1 = edit_text(text_edits, commands0) - val commands2 = recover_spans(syntax, name, node.perspective, commands1) + val commands2 = recover_spans(syntax, name, node.perspective._2, commands1) node.update_commands(commands2) case (_, Document.Node.Deps(_)) => node - case (name, Document.Node.Perspective(text_perspective)) => - val perspective = command_perspective(node, text_perspective) - if (node.perspective same perspective) node + case (name, Document.Node.Perspective(required, text_perspective)) => + val perspective = (required, command_perspective(node, text_perspective)) + if (node.same_perspective(perspective)) node else node.update_perspective(perspective).update_commands( - consolidate_spans(syntax, reparse_limit, name, perspective, node.commands)) + consolidate_spans(syntax, reparse_limit, name, perspective._2, node.commands)) } } @@ -353,8 +353,9 @@ else node val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _)) - if (!(node.perspective same node2.perspective)) - doc_edits += (name -> Document.Node.Perspective(node2.perspective)) + if (!(node.same_perspective(node2.perspective))) + doc_edits += + (name -> Document.Node.Perspective(node2.perspective._1, node2.perspective._2)) doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) diff -r 71fef62c4213 -r 122416054a9c src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/Tools/find_theorems.ML Thu Aug 01 16:53:03 2013 +0200 @@ -315,8 +315,7 @@ let val thy' = Proof_Context.theory_of ctxt - |> Context_Position.set_visible_global (Context_Position.is_visible ctxt) - |> Theory.checkpoint; + |> Context_Position.set_visible_global (Context_Position.is_visible ctxt); val ctxt' = Proof_Context.transfer thy' ctxt; val goal' = Thm.transfer thy' goal; diff -r 71fef62c4213 -r 122416054a9c src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/axclass.ML Thu Aug 01 16:53:03 2013 +0200 @@ -320,7 +320,7 @@ let val string_of_sort = Syntax.string_of_sort_global thy; val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; - val _ = Sign.primitive_classrel (c1, c2) (Theory.copy thy); + val _ = Sign.primitive_classrel (c1, c2) thy; val _ = (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of [] => () diff -r 71fef62c4213 -r 122416054a9c src/Pure/context.ML --- a/src/Pure/context.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/context.ML Thu Aug 01 16:53:03 2013 +0200 @@ -14,7 +14,6 @@ signature BASIC_CONTEXT = sig type theory - type theory_ref exception THEORY of string * theory list structure Proof: sig type context end structure Proof_Context: @@ -42,13 +41,10 @@ val str_of_thy: theory -> string val get_theory: theory -> string -> theory val this_theory: theory -> string -> theory - val deref: theory_ref -> theory - val check_thy: theory -> theory_ref val eq_thy: theory * theory -> bool val subthy: theory * theory -> bool val joinable: theory * theory -> bool val merge: theory * theory -> theory - val merge_refs: theory_ref * theory_ref -> theory_ref val finish_thy: theory -> theory val begin_thy: (theory -> pretty) -> string -> theory list -> theory (*proof context*) @@ -229,14 +225,6 @@ else get_theory thy name; -(* theory references *) (* FIXME dummy *) - -datatype theory_ref = Theory_Ref of theory; - -fun deref (Theory_Ref thy) = thy; -fun check_thy thy = Theory_Ref thy; - - (* build ids *) fun insert_id id ids = Inttab.update (id, ()) ids; @@ -285,8 +273,6 @@ else error (cat_lines ["Attempt to perform non-trivial merge of theories:", str_of_thy thy1, str_of_thy thy2]); -fun merge_refs (ref1, ref2) = check_thy (merge (deref ref1, deref ref2)); - (** build theories **) @@ -379,12 +365,12 @@ structure Proof = struct - datatype context = Context of Any.T Datatab.table * theory_ref; + datatype context = Context of Any.T Datatab.table * theory; end; -fun theory_of_proof (Proof.Context (_, thy_ref)) = deref thy_ref; +fun theory_of_proof (Proof.Context (_, thy)) = thy; fun data_of_proof (Proof.Context (data, _)) = data; -fun map_prf f (Proof.Context (data, thy_ref)) = Proof.Context (f data, thy_ref); +fun map_prf f (Proof.Context (data, thy)) = Proof.Context (f data, thy); (* proof data kinds *) @@ -406,19 +392,16 @@ in -fun raw_transfer thy' (Proof.Context (data, thy_ref)) = +fun raw_transfer thy' (Proof.Context (data, thy)) = let - val thy = deref thy_ref; val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory"; - val _ = check_thy thy; val data' = init_new_data data thy'; - val thy_ref' = check_thy thy'; - in Proof.Context (data', thy_ref') end; + in Proof.Context (data', thy') end; structure Proof_Context = struct val theory_of = theory_of_proof; - fun init_global thy = Proof.Context (init_data thy, check_thy thy); + fun init_global thy = Proof.Context (init_data thy, thy); fun get_global thy name = init_global (get_theory thy name); end; diff -r 71fef62c4213 -r 122416054a9c src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/global_theory.ML Thu Aug 01 16:53:03 2013 +0200 @@ -75,7 +75,6 @@ "_" => "Pure.asm_rl" | name => name); val res = Facts.lookup context facts name; - val _ = Theory.check_thy thy; in (case res of NONE => error ("Unknown fact " ^ quote name ^ Position.here pos) diff -r 71fef62c4213 -r 122416054a9c src/Pure/goal.ML --- a/src/Pure/goal.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/goal.ML Thu Aug 01 16:53:03 2013 +0200 @@ -293,7 +293,7 @@ Term.exists_subterm Term.is_Var t orelse Term.exists_type (Term.exists_subtype Term.is_TVar) t; -fun prove_common immediate ctxt xs asms props tac = +fun prove_common immediate pri ctxt xs asms props tac = let val thy = Proof_Context.theory_of ctxt; val string_of_term = Syntax.string_of_term ctxt; @@ -337,7 +337,7 @@ val res = if immediate orelse schematic orelse not future orelse skip then result () - else future_result ctxt' (fork ~1 result) (Thm.term_of stmt); + else future_result ctxt' (fork pri result) (Thm.term_of stmt); in Conjunction.elim_balanced (length props) res |> map (Assumption.export false ctxt' ctxt) @@ -345,11 +345,14 @@ |> map Drule.zero_var_indexes end; -val prove_multi = prove_common true; +val prove_multi = prove_common true 0; -fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac); +fun prove_future_pri pri ctxt xs asms prop tac = + hd (prove_common false pri ctxt xs asms [prop] tac); -fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac); +val prove_future = prove_future_pri ~1; + +fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac); fun prove_global_future thy xs asms prop tac = Drule.export_without_context (prove_future (Proof_Context.init_global thy) xs asms prop tac); @@ -360,7 +363,7 @@ fun prove_sorry ctxt xs asms prop tac = if Config.get ctxt quick_and_dirty then prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac) - else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac; + else (if future_enabled () then prove_future_pri ~2 else prove) ctxt xs asms prop tac; fun prove_sorry_global thy xs asms prop tac = Drule.export_without_context diff -r 71fef62c4213 -r 122416054a9c src/Pure/theory.ML --- a/src/Pure/theory.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/theory.ML Thu Aug 01 16:53:03 2013 +0200 @@ -12,13 +12,8 @@ val parents_of: theory -> theory list val ancestors_of: theory -> theory list val nodes_of: theory -> theory list - val check_thy: theory -> theory_ref - val deref: theory_ref -> theory val merge: theory * theory -> theory - val merge_refs: theory_ref * theory_ref -> theory_ref val merge_list: theory list -> theory - val checkpoint: theory -> theory - val copy: theory -> theory val requires: theory -> string -> string -> unit val get_markup: theory -> Markup.T val axiom_space: theory -> Name_Space.T @@ -55,18 +50,11 @@ val ancestors_of = Context.ancestors_of; fun nodes_of thy = thy :: ancestors_of thy; -val check_thy = Context.check_thy; -val deref = Context.deref; - val merge = Context.merge; -val merge_refs = Context.merge_refs; fun merge_list [] = raise THEORY ("Empty merge of theories", []) | merge_list (thy :: thys) = Library.foldl merge (thy, thys); -val checkpoint : theory -> theory = I; (* FIXME dummy *) -val copy : theory -> theory = I; (* FIXME dummy *) - fun requires thy name what = if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then () else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); diff -r 71fef62c4213 -r 122416054a9c src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Pure/thm.ML Thu Aug 01 16:53:03 2013 +0200 @@ -11,11 +11,7 @@ sig (*certified types*) type ctyp - val rep_ctyp: ctyp -> - {thy_ref: theory_ref, - T: typ, - maxidx: int, - sorts: sort Ord_List.T} + val rep_ctyp: ctyp -> {thy: theory, T: typ, maxidx: int, sorts: sort Ord_List.T} val theory_of_ctyp: ctyp -> theory val typ_of: ctyp -> typ val ctyp_of: theory -> typ -> ctyp @@ -23,14 +19,8 @@ (*certified terms*) type cterm exception CTERM of string * cterm list - val rep_cterm: cterm -> - {thy_ref: theory_ref, - t: term, - T: typ, - maxidx: int, - sorts: sort Ord_List.T} - val crep_cterm: cterm -> - {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T} + val rep_cterm: cterm -> {thy: theory, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T} + val crep_cterm: cterm -> {thy: theory, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T} val theory_of_cterm: cterm -> theory val term_of: cterm -> term val cterm_of: theory -> term -> cterm @@ -40,7 +30,7 @@ type thm type conv = cterm -> thm val rep_thm: thm -> - {thy_ref: theory_ref, + {thy: theory, tags: Properties.T, maxidx: int, shyps: sort Ord_List.T, @@ -48,7 +38,7 @@ tpairs: (term * term) list, prop: term} val crep_thm: thm -> - {thy_ref: theory_ref, + {thy: theory, tags: Properties.T, maxidx: int, shyps: sort Ord_List.T, @@ -158,15 +148,11 @@ (** certified types **) -abstype ctyp = Ctyp of - {thy_ref: theory_ref, - T: typ, - maxidx: int, - sorts: sort Ord_List.T} +abstype ctyp = Ctyp of {thy: theory, T: typ, maxidx: int, sorts: sort Ord_List.T} with fun rep_ctyp (Ctyp args) = args; -fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref; +fun theory_of_ctyp (Ctyp {thy, ...}) = thy; fun typ_of (Ctyp {T, ...}) = T; fun ctyp_of thy raw_T = @@ -174,10 +160,10 @@ val T = Sign.certify_typ thy raw_T; val maxidx = Term.maxidx_of_typ T; val sorts = Sorts.insert_typ T []; - in Ctyp {thy_ref = Theory.check_thy thy, T = T, maxidx = maxidx, sorts = sorts} end; + in Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts} end; -fun dest_ctyp (Ctyp {thy_ref, T = Type (_, Ts), maxidx, sorts}) = - map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts +fun dest_ctyp (Ctyp {thy, T = Type (_, Ts), maxidx, sorts}) = + map (fn T => Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts}) Ts | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); @@ -185,74 +171,69 @@ (** certified terms **) (*certified terms with checked typ, maxidx, and sorts*) -abstype cterm = Cterm of - {thy_ref: theory_ref, - t: term, - T: typ, - maxidx: int, - sorts: sort Ord_List.T} +abstype cterm = Cterm of {thy: theory, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T} with exception CTERM of string * cterm list; fun rep_cterm (Cterm args) = args; -fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) = - {thy_ref = thy_ref, t = t, maxidx = maxidx, sorts = sorts, - T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}}; +fun crep_cterm (Cterm {thy, t, T, maxidx, sorts}) = + {thy = thy, t = t, maxidx = maxidx, sorts = sorts, + T = Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts}}; -fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref; +fun theory_of_cterm (Cterm {thy, ...}) = thy; fun term_of (Cterm {t, ...}) = t; -fun ctyp_of_term (Cterm {thy_ref, T, maxidx, sorts, ...}) = - Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}; +fun ctyp_of_term (Cterm {thy, T, maxidx, sorts, ...}) = + Ctyp {thy = thy, T = T, maxidx = maxidx, sorts = sorts}; fun cterm_of thy tm = let val (t, T, maxidx) = Sign.certify_term thy tm; val sorts = Sorts.insert_term t []; - in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; + in Cterm {thy = thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; -fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) = - Theory.merge_refs (r1, r2); +fun merge_thys0 (Cterm {thy = thy1, ...}) (Cterm {thy = thy2, ...}) = + Theory.merge (thy1, thy2); (* destructors *) -fun dest_comb (Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) = +fun dest_comb (Cterm {t = c $ a, T, thy, maxidx, sorts}) = let val A = Term.argument_type_of c 0 in - (Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, - Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) + (Cterm {t = c, T = A --> T, thy = thy, maxidx = maxidx, sorts = sorts}, + Cterm {t = a, T = A, thy = thy, maxidx = maxidx, sorts = sorts}) end | dest_comb ct = raise CTERM ("dest_comb", [ct]); -fun dest_fun (Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) = +fun dest_fun (Cterm {t = c $ _, T, thy, maxidx, sorts}) = let val A = Term.argument_type_of c 0 - in Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end + in Cterm {t = c, T = A --> T, thy = thy, maxidx = maxidx, sorts = sorts} end | dest_fun ct = raise CTERM ("dest_fun", [ct]); -fun dest_arg (Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) = +fun dest_arg (Cterm {t = c $ a, T = _, thy, maxidx, sorts}) = let val A = Term.argument_type_of c 0 - in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end + in Cterm {t = a, T = A, thy = thy, maxidx = maxidx, sorts = sorts} end | dest_arg ct = raise CTERM ("dest_arg", [ct]); -fun dest_fun2 (Cterm {t = c $ _ $ _, T, thy_ref, maxidx, sorts}) = +fun dest_fun2 (Cterm {t = c $ _ $ _, T, thy, maxidx, sorts}) = let val A = Term.argument_type_of c 0; val B = Term.argument_type_of c 1; - in Cterm {t = c, T = A --> B --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end + in Cterm {t = c, T = A --> B --> T, thy = thy, maxidx = maxidx, sorts = sorts} end | dest_fun2 ct = raise CTERM ("dest_fun2", [ct]); -fun dest_arg1 (Cterm {t = c $ a $ _, T = _, thy_ref, maxidx, sorts}) = +fun dest_arg1 (Cterm {t = c $ a $ _, T = _, thy, maxidx, sorts}) = let val A = Term.argument_type_of c 0 - in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end + in Cterm {t = a, T = A, thy = thy, maxidx = maxidx, sorts = sorts} end | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); -fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) = +fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy, maxidx, sorts}) = let val (y', t') = Term.dest_abs (the_default x a, T, t) in - (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, - Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) + (Cterm {t = Free (y', T), T = T, thy = thy, maxidx = maxidx, sorts = sorts}, + Cterm {t = t', T = U, thy = thy, maxidx = maxidx, sorts = sorts}) end | dest_abs _ ct = raise CTERM ("dest_abs", [ct]); @@ -263,7 +244,7 @@ (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...}) (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) = if T = dty then - Cterm {thy_ref = merge_thys0 cf cx, + Cterm {thy = merge_thys0 cf cx, t = f $ x, T = rty, maxidx = Int.max (maxidx1, maxidx2), @@ -275,7 +256,7 @@ (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...}) (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) = let val t = Term.lambda_name (x, t1) t2 in - Cterm {thy_ref = merge_thys0 ct1 ct2, + Cterm {thy = merge_thys0 ct1 ct2, t = t, T = T1 --> T2, maxidx = Int.max (maxidx1, maxidx2), sorts = Sorts.union sorts1 sorts2} @@ -286,17 +267,17 @@ (* indexes *) -fun adjust_maxidx_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = +fun adjust_maxidx_cterm i (ct as Cterm {thy, t, T, maxidx, sorts}) = if maxidx = i then ct else if maxidx < i then - Cterm {maxidx = i, thy_ref = thy_ref, t = t, T = T, sorts = sorts} + Cterm {maxidx = i, thy = thy, t = t, T = T, sorts = sorts} else - Cterm {maxidx = Int.max (maxidx_of_term t, i), thy_ref = thy_ref, t = t, T = T, sorts = sorts}; + Cterm {maxidx = Int.max (maxidx_of_term t, i), thy = thy, t = t, T = T, sorts = sorts}; -fun incr_indexes_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = +fun incr_indexes_cterm i (ct as Cterm {thy, t, T, maxidx, sorts}) = if i < 0 then raise CTERM ("negative increment", [ct]) else if i = 0 then ct - else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t, + else Cterm {thy = thy, t = Logic.incr_indexes ([], i) t, T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts}; @@ -308,17 +289,16 @@ (ct1 as Cterm {t = t1, sorts = sorts1, ...}, ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) = let - val thy = Theory.deref (merge_thys0 ct1 ct2); + val thy = merge_thys0 ct1 ct2; val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); val sorts = Sorts.union sorts1 sorts2; fun mk_cTinst ((a, i), (S, T)) = - (Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts}, - Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}); + (Ctyp {T = TVar ((a, i), S), thy = thy, maxidx = i, sorts = sorts}, + Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts}); fun mk_ctinst ((x, i), (T, t)) = let val T = Envir.subst_type Tinsts T in - (Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy, - maxidx = i, sorts = sorts}, - Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}) + (Cterm {t = Var ((x, i), T), T = T, thy = thy, maxidx = i, sorts = sorts}, + Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts}) end; in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; @@ -335,7 +315,7 @@ abstype thm = Thm of deriv * (*derivation*) - {thy_ref: theory_ref, (*dynamic reference to theory*) + {thy: theory, (*background theory*) tags: Properties.T, (*additional annotations/comments*) maxidx: int, (*maximum index of any Var or TVar*) shyps: sort Ord_List.T, (*sort hypotheses*) @@ -354,9 +334,9 @@ fun rep_thm (Thm (_, args)) = args; -fun crep_thm (Thm (_, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = - let fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps} in - {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps, +fun crep_thm (Thm (_, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) = + let fun cterm max t = Cterm {thy = thy, t = t, T = propT, maxidx = max, sorts = shyps} in + {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps, hyps = map (cterm ~1) hyps, tpairs = map (pairself (cterm maxidx)) tpairs, prop = cterm maxidx prop} @@ -383,16 +363,16 @@ (* merge theories of cterms/thms -- trivial absorption only *) -fun merge_thys1 (Cterm {thy_ref = r1, ...}) (Thm (_, {thy_ref = r2, ...})) = - Theory.merge_refs (r1, r2); +fun merge_thys1 (Cterm {thy = thy1, ...}) (Thm (_, {thy = thy2, ...})) = + Theory.merge (thy1, thy2); -fun merge_thys2 (Thm (_, {thy_ref = r1, ...})) (Thm (_, {thy_ref = r2, ...})) = - Theory.merge_refs (r1, r2); +fun merge_thys2 (Thm (_, {thy = thy1, ...})) (Thm (_, {thy = thy2, ...})) = + Theory.merge (thy1, thy2); (* basic components *) -val theory_of_thm = Theory.deref o #thy_ref o rep_thm; +val theory_of_thm = #thy o rep_thm; val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); val hyps_of = #hyps o rep_thm; @@ -410,26 +390,23 @@ | [] => raise THM ("major_prem_of: rule with no premises", 0, [th])); (*the statement of any thm is a cterm*) -fun cprop_of (Thm (_, {thy_ref, maxidx, shyps, prop, ...})) = - Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop, sorts = shyps}; +fun cprop_of (Thm (_, {thy, maxidx, shyps, prop, ...})) = + Cterm {thy = thy, maxidx = maxidx, T = propT, t = prop, sorts = shyps}; -fun cprem_of (th as Thm (_, {thy_ref, maxidx, shyps, prop, ...})) i = - Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, sorts = shyps, +fun cprem_of (th as Thm (_, {thy, maxidx, shyps, prop, ...})) i = + Cterm {thy = thy, maxidx = maxidx, T = propT, sorts = shyps, t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])}; (*explicit transfer to a super theory*) fun transfer thy' thm = let - val Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop}) = thm; - val thy = Theory.deref thy_ref; + val Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop}) = thm; val _ = Theory.subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]); - val is_eq = Theory.eq_thy (thy, thy'); - val _ = Theory.check_thy thy; in - if is_eq then thm + if Theory.eq_thy (thy, thy') then thm else Thm (der, - {thy_ref = Theory.check_thy thy', + {thy = thy', tags = tags, maxidx = maxidx, shyps = shyps, @@ -450,7 +427,7 @@ raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, []) else Thm (der, - {thy_ref = merge_thys1 ct th, + {thy = merge_thys1 ct th, tags = tags, maxidx = maxidx, shyps = Sorts.union sorts shyps, @@ -461,11 +438,10 @@ fun weaken_sorts raw_sorts ct = let - val Cterm {thy_ref, t, T, maxidx, sorts} = ct; - val thy = Theory.deref thy_ref; + val Cterm {thy, t, T, maxidx, sorts} = ct; val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts); val sorts' = Sorts.union sorts more_sorts; - in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end; + in Cterm {thy = thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end; (*dangling sort constraints of a thm*) fun extra_shyps (th as Thm (_, {shyps, ...})) = @@ -516,8 +492,8 @@ | join_promises promises = join_promises_of (Future.joins (map snd promises)) and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms)); -fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) = - Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body +fun fulfill_body (Thm (Deriv {promises, body}, {thy, ...})) = + Proofterm.fulfill_norm_proof thy (fulfill_promises promises) body and fulfill_promises promises = map fst promises ~~ map fulfill_body (Future.joins (map snd promises)); @@ -554,10 +530,9 @@ fun future_result i orig_thy orig_shyps orig_prop thm = let fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]); - val Thm (Deriv {promises, ...}, {thy_ref, shyps, hyps, tpairs, prop, ...}) = thm; + val Thm (Deriv {promises, ...}, {thy, shyps, hyps, tpairs, prop, ...}) = thm; - val _ = Theory.eq_thy (Theory.deref thy_ref, orig_thy) orelse err "bad theory"; - val _ = Theory.check_thy orig_thy; + val _ = Theory.eq_thy (thy, orig_thy) orelse err "bad theory"; val _ = prop aconv orig_prop orelse err "bad prop"; val _ = null tpairs orelse err "bad tpairs"; val _ = null hyps orelse err "bad hyps"; @@ -568,15 +543,14 @@ fun future future_thm ct = let - val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct; - val thy = Theory.deref thy_ref; + val Cterm {thy = thy, t = prop, T, maxidx, sorts} = ct; val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); val i = serial (); val future = future_thm |> Future.map (future_result i thy sorts prop); in Thm (make_deriv [(i, future)] [] [] (Proofterm.promise_proof thy i prop), - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -595,14 +569,12 @@ fun name_derivation name (thm as Thm (der, args)) = let val Deriv {promises, body} = der; - val {thy_ref, shyps, hyps, prop, tpairs, ...} = args; + val {thy, shyps, hyps, prop, tpairs, ...} = args; val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]); val ps = map (apsnd (Future.map fulfill_body)) promises; - val thy = Theory.deref thy_ref; val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body; val der' = make_deriv [] [] [pthm] proof; - val _ = Theory.check_thy thy; in Thm (der', args) end; @@ -619,7 +591,7 @@ val maxidx = maxidx_of_term prop; val shyps = Sorts.insert_term prop []; in - Thm (der, {thy_ref = Theory.check_thy thy, tags = [], + Thm (der, {thy = thy, tags = [], maxidx = maxidx, shyps = shyps, hyps = [], tpairs = [], prop = prop}) end); in @@ -637,27 +609,23 @@ val get_tags = #tags o rep_thm; -fun map_tags f (Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = - Thm (der, {thy_ref = thy_ref, tags = f tags, maxidx = maxidx, +fun map_tags f (Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) = + Thm (der, {thy = thy, tags = f tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); (* technical adjustments *) -fun norm_proof (Thm (der, args as {thy_ref, ...})) = - let - val thy = Theory.deref thy_ref; - val der' = deriv_rule1 (Proofterm.rew_proof thy) der; - val _ = Theory.check_thy thy; - in Thm (der', args) end; +fun norm_proof (Thm (der, args as {thy, ...})) = + Thm (deriv_rule1 (Proofterm.rew_proof thy) der, args); -fun adjust_maxidx_thm i (th as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = +fun adjust_maxidx_thm i (th as Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) = if maxidx = i then th else if maxidx < i then - Thm (der, {maxidx = i, thy_ref = thy_ref, tags = tags, shyps = shyps, + Thm (der, {maxidx = i, thy = thy, tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}) else - Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), thy_ref = thy_ref, + Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), thy = thy, tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); @@ -668,13 +636,13 @@ (*The assumption rule A |- A*) fun assume raw_ct = - let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in + let val Cterm {thy, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in if T <> propT then raise THM ("assume: prop", 0, []) else if maxidx <> ~1 then raise THM ("assume: variables", maxidx, []) else Thm (deriv_rule0 (Proofterm.Hyp prop), - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = ~1, shyps = sorts, @@ -697,7 +665,7 @@ raise THM ("implies_intr: assumptions must have type prop", 0, [th]) else Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der, - {thy_ref = merge_thys1 ct th, + {thy = merge_thys1 ct th, tags = [], maxidx = Int.max (maxidxA, maxidx), shyps = Sorts.union sorts shyps, @@ -722,7 +690,7 @@ Const ("==>", _) $ A $ B => if A aconv propA then Thm (deriv_rule2 (curry Proofterm.%%) der derA, - {thy_ref = merge_thys2 thAB thA, + {thy = merge_thys2 thAB thA, tags = [], maxidx = Int.max (maxA, maxidx), shyps = Sorts.union shypsA shyps, @@ -746,7 +714,7 @@ let fun result a = Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der, - {thy_ref = merge_thys1 ct th, + {thy = merge_thys1 ct th, tags = [], maxidx = maxidx, shyps = Sorts.union sorts shyps, @@ -758,10 +726,10 @@ raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th]) else (); in - case x of + (case x of Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a) | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a) - | _ => raise THM ("forall_intr: not a variable", 0, [th]) + | _ => raise THM ("forall_intr: not a variable", 0, [th])) end; (*Forall elimination @@ -778,7 +746,7 @@ raise THM ("forall_elim: type mismatch", 0, [th]) else Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der, - {thy_ref = merge_thys1 ct th, + {thy = merge_thys1 ct th, tags = [], maxidx = Int.max (maxidx, maxt), shyps = Sorts.union sorts shyps, @@ -793,9 +761,9 @@ (*Reflexivity t == t *) -fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) = +fun reflexive (Cterm {thy, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 Proofterm.reflexive, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -808,11 +776,11 @@ ------ u == t *) -fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = +fun symmetric (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) = (case prop of (eq as Const ("==", _)) $ t $ u => Thm (deriv_rule1 Proofterm.symmetric der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = shyps, @@ -839,7 +807,7 @@ if not (u aconv u') then err "middle term" else Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2, - {thy_ref = merge_thys2 th1 th2, + {thy = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, @@ -853,7 +821,7 @@ (%x. t)(u) == t[u/x] fully beta-reduces the term if full = true *) -fun beta_conversion full (Cterm {thy_ref, t, T = _, maxidx, sorts}) = +fun beta_conversion full (Cterm {thy, t, T = _, maxidx, sorts}) = let val t' = if full then Envir.beta_norm t else @@ -861,7 +829,7 @@ | _ => raise THM ("beta_conversion: not a redex", 0, [])); in Thm (deriv_rule0 Proofterm.reflexive, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -870,9 +838,9 @@ prop = Logic.mk_equals (t, t')}) end; -fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) = +fun eta_conversion (Cterm {thy, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 Proofterm.reflexive, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -880,9 +848,9 @@ tpairs = [], prop = Logic.mk_equals (t, Envir.eta_contract t)}); -fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) = +fun eta_long_conversion (Cterm {thy, t, T = _, maxidx, sorts}) = Thm (deriv_rule0 Proofterm.reflexive, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -898,13 +866,13 @@ *) fun abstract_rule a (Cterm {t = x, T, sorts, ...}) - (th as Thm (der, {thy_ref, maxidx, hyps, shyps, tpairs, prop, ...})) = + (th as Thm (der, {thy, maxidx, hyps, shyps, tpairs, prop, ...})) = let val (t, u) = Logic.dest_equals prop handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]); val result = Thm (deriv_rule1 (Proofterm.abstract_rule x a) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = Sorts.union sorts shyps, @@ -917,10 +885,10 @@ raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th]) else (); in - case x of + (case x of Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result) | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result) - | _ => raise THM ("abstract_rule: not a variable", 0, [th]) + | _ => raise THM ("abstract_rule: not a variable", 0, [th])) end; (*The combination rule @@ -942,19 +910,19 @@ else () | _ => raise THM ("combination: not function type", 0, [th1, th2])); in - case (prop1, prop2) of + (case (prop1, prop2) of (Const ("==", Type ("fun", [fT, _])) $ f $ g, Const ("==", Type ("fun", [tT, _])) $ t $ u) => (chktypes fT tT; Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2, - {thy_ref = merge_thys2 th1 th2, + {thy = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (f $ t, g $ u)})) - | _ => raise THM ("combination: premises", 0, [th1, th2]) + | _ => raise THM ("combination: premises", 0, [th1, th2])) end; (*Equality introduction @@ -970,11 +938,11 @@ prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]); in - case (prop1, prop2) of + (case (prop1, prop2) of (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') => if A aconv A' andalso B aconv B' then Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2, - {thy_ref = merge_thys2 th1 th2, + {thy = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, @@ -982,7 +950,7 @@ tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (A, B)}) else err "not equal" - | _ => err "premises" + | _ => err "premises") end; (*The equal propositions rule @@ -998,11 +966,11 @@ tpairs = tpairs2, prop = prop2, ...}) = th2; fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]); in - case prop1 of + (case prop1 of Const ("==", _) $ A $ B => if prop2 aconv A then Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2, - {thy_ref = merge_thys2 th1 th2, + {thy = merge_thys2 th1 th2, tags = [], maxidx = Int.max (max1, max2), shyps = Sorts.union shyps1 shyps2, @@ -1010,7 +978,7 @@ tpairs = union_tpairs tpairs1 tpairs2, prop = B}) else err "not equal" - | _ => err"major premise" + | _ => err "major premise") end; @@ -1021,25 +989,23 @@ Instantiates the theorem and deletes trivial tpairs. Resulting sequence may contain multiple elements if the tpairs are not all flex-flex.*) -fun flexflex_rule (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = - let val thy = Theory.deref thy_ref in - Unify.smash_unifiers thy tpairs (Envir.empty maxidx) - |> Seq.map (fn env => - if Envir.is_empty env then th - else - let - val tpairs' = tpairs |> map (pairself (Envir.norm_term env)) - (*remove trivial tpairs, of the form t==t*) - |> filter_out (op aconv); - val der' = deriv_rule1 (Proofterm.norm_proof' env) der; - val prop' = Envir.norm_term env prop; - val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); - val shyps = Envir.insert_sorts env shyps; - in - Thm (der', {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx, - shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) - end) - end; +fun flexflex_rule (th as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) = + Unify.smash_unifiers thy tpairs (Envir.empty maxidx) + |> Seq.map (fn env => + if Envir.is_empty env then th + else + let + val tpairs' = tpairs |> map (pairself (Envir.norm_term env)) + (*remove trivial tpairs, of the form t==t*) + |> filter_out (op aconv); + val der' = deriv_rule1 (Proofterm.norm_proof' env) der; + val prop' = Envir.norm_term env prop; + val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); + val shyps = Envir.insert_sorts env shyps; + in + Thm (der', {thy = thy, tags = [], maxidx = maxidx, + shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) + end); (*Generalization of fixed variables @@ -1051,7 +1017,7 @@ fun generalize ([], []) _ th = th | generalize (tfrees, frees) idx th = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...}) = th; + val Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...}) = th; val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); val bad_type = @@ -1072,7 +1038,7 @@ val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); in Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx', shyps = shyps, @@ -1093,33 +1059,33 @@ fun pretty_typing thy t T = Pretty.block [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T]; -fun add_inst (ct, cu) (thy_ref, sorts) = +fun add_inst (ct, cu) (thy, sorts) = let val Cterm {t = t, T = T, ...} = ct; val Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; - val thy_ref' = Theory.merge_refs (thy_ref, merge_thys0 ct cu); + val thy' = Theory.merge (thy, merge_thys0 ct cu); val sorts' = Sorts.union sorts_u sorts; in (case t of Var v => - if T = U then ((v, (u, maxidx_u)), (thy_ref', sorts')) + if T = U then ((v, (u, maxidx_u)), (thy', sorts')) else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", - Pretty.fbrk, pretty_typing (Theory.deref thy_ref') t T, - Pretty.fbrk, pretty_typing (Theory.deref thy_ref') u U]), [T, U], [t, u]) + Pretty.fbrk, pretty_typing thy' t T, + Pretty.fbrk, pretty_typing thy' u U]), [T, U], [t, u]) | _ => raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: not a variable", - Pretty.fbrk, Syntax.pretty_term_global (Theory.deref thy_ref') t]), [], [t])) + Pretty.fbrk, Syntax.pretty_term_global thy' t]), [], [t])) end; -fun add_instT (cT, cU) (thy_ref, sorts) = +fun add_instT (cT, cU) (thy, sorts) = let - val Ctyp {T, thy_ref = thy_ref1, ...} = cT - and Ctyp {T = U, thy_ref = thy_ref2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; - val thy' = Theory.deref (Theory.merge_refs (thy_ref, Theory.merge_refs (thy_ref1, thy_ref2))); + val Ctyp {T, thy = thy1, ...} = cT + and Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; + val thy' = Theory.merge (thy, Theory.merge (thy1, thy2)); val sorts' = Sorts.union sorts_U sorts; in (case T of TVar (v as (_, S)) => - if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (Theory.check_thy thy', sorts')) + if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts')) else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], []) | _ => raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: not a type variable", @@ -1134,9 +1100,9 @@ fun instantiate ([], []) th = th | instantiate (instT, inst) th = let - val Thm (der, {thy_ref, hyps, shyps, tpairs, prop, ...}) = th; - val (inst', (instT', (thy_ref', shyps'))) = - (thy_ref, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT; + val Thm (der, {thy, hyps, shyps, tpairs, prop, ...}) = th; + val (inst', (instT', (thy', shyps'))) = + (thy, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT; val subst = Term_Subst.instantiate_maxidx (instT', inst'); val (prop', maxidx1) = subst prop ~1; val (tpairs', maxidx') = @@ -1144,7 +1110,7 @@ in Thm (deriv_rule1 (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, - {thy_ref = thy_ref', + {thy = thy', tags = [], maxidx = maxidx', shyps = shyps', @@ -1157,14 +1123,14 @@ fun instantiate_cterm ([], []) ct = ct | instantiate_cterm (instT, inst) ct = let - val Cterm {thy_ref, t, T, sorts, ...} = ct; - val (inst', (instT', (thy_ref', sorts'))) = - (thy_ref, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT; + val Cterm {thy, t, T, sorts, ...} = ct; + val (inst', (instT', (thy', sorts'))) = + (thy, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT; val subst = Term_Subst.instantiate_maxidx (instT', inst'); val substT = Term_Subst.instantiateT_maxidx instT'; val (t', maxidx1) = subst t ~1; val (T', maxidx') = substT T maxidx1; - in Cterm {thy_ref = thy_ref', t = t', T = T', sorts = sorts', maxidx = maxidx'} end + in Cterm {thy = thy', t = t', T = T', sorts = sorts', maxidx = maxidx'} end handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); end; @@ -1172,12 +1138,12 @@ (*The trivial implication A ==> A, justified by assume and forall rules. A can contain Vars, not so for assume!*) -fun trivial (Cterm {thy_ref, t =A, T, maxidx, sorts}) = +fun trivial (Cterm {thy, t = A, T, maxidx, sorts}) = if T <> propT then raise THM ("trivial: the term must have type prop", 0, []) else Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)), - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -1192,14 +1158,13 @@ *) fun of_class (cT, raw_c) = let - val Ctyp {thy_ref, T, ...} = cT; - val thy = Theory.deref thy_ref; + val Ctyp {thy, T, ...} = cT; val c = Sign.certify_class thy raw_c; val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c)); in if Sign.of_sort thy (T, [c]) then Thm (deriv_rule0 (Proofterm.OfClass (T, c)), - {thy_ref = Theory.check_thy thy, + {thy = thy, tags = [], maxidx = maxidx, shyps = sorts, @@ -1211,9 +1176,8 @@ (*Remove extra sorts that are witnessed by type signature information*) fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm - | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = + | strip_shyps (thm as Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) = let - val thy = Theory.deref thy_ref; val algebra = Sign.classes_of thy; val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; @@ -1225,7 +1189,7 @@ in Thm (deriv_rule_unconditional (Proofterm.strip_shyps_proof algebra present witnessed extra') der, - {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx, + {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) end; @@ -1233,7 +1197,7 @@ fun unconstrainT (thm as Thm (der, args)) = let val Deriv {promises, body} = der; - val {thy_ref, shyps, hyps, tpairs, prop, ...} = args; + val {thy, shyps, hyps, tpairs, prop, ...} = args; fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); val _ = null hyps orelse err "illegal hyps"; @@ -1242,14 +1206,12 @@ val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); val ps = map (apsnd (Future.map fulfill_body)) promises; - val thy = Theory.deref thy_ref; val (pthm as (_, (_, prop', _)), proof) = Proofterm.unconstrain_thm_proof thy shyps prop ps body; val der' = make_deriv [] [] [pthm] proof; - val _ = Theory.check_thy thy; in Thm (der', - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx_of_term prop', shyps = [[]], (*potentially redundant*) @@ -1259,7 +1221,7 @@ end; (* Replace all TFrees not fixed or in the hyps by new TVars *) -fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = +fun varifyT_global' fixed (Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) = let val tfrees = fold Term.add_tfrees hyps fixed; val prop1 = attach_tpairs tpairs prop; @@ -1267,7 +1229,7 @@ val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = Int.max (0, maxidx), shyps = shyps, @@ -1279,14 +1241,14 @@ val varifyT_global = #2 o varifyT_global' []; (* Replace all TVars by TFrees that are often new *) -fun legacy_freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) = +fun legacy_freezeT (Thm (der, {thy, shyps, hyps, tpairs, prop, ...})) = let val prop1 = attach_tpairs tpairs prop; val prop2 = Type.legacy_freeze prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx_of_term prop2, shyps = shyps, @@ -1319,7 +1281,7 @@ if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, []) else Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der, - {thy_ref = merge_thys1 goal orule, + {thy = merge_thys1 goal orule, tags = [], maxidx = maxidx + inc, shyps = Sorts.union shyps sorts, (*sic!*) @@ -1328,12 +1290,12 @@ prop = Logic.list_implies (map lift_all As, lift_all B)}) end; -fun incr_indexes i (thm as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = +fun incr_indexes i (thm as Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...})) = if i < 0 then raise THM ("negative increment", 0, [thm]) else if i = 0 then thm else Thm (deriv_rule1 (Proofterm.incr_indexes i) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx + i, shyps = shyps, @@ -1344,8 +1306,7 @@ (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) fun assumption i state = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state; - val thy = Theory.deref thy_ref; + val Thm (der, {thy, maxidx, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); fun newth n (env, tpairs) = Thm (deriv_rule1 @@ -1363,7 +1324,7 @@ Logic.list_implies (Bs, C) else (*normalize the new rule fully*) Envir.norm_term env (Logic.list_implies (Bs, C)), - thy_ref = Theory.check_thy thy}); + thy = thy}); val (close, asms, concl) = Logic.assum_problems (~1, Bi); val concl' = close concl; @@ -1380,7 +1341,7 @@ Checks if Bi's conclusion is alpha/eta-convertible to one of its assumptions*) fun eq_assumption i state = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state; + val Thm (der, {thy, maxidx, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val (_, asms, concl) = Logic.assum_problems (~1, Bi); in @@ -1388,7 +1349,7 @@ ~1 => raise THM ("eq_assumption", 0, [state]) | n => Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = shyps, @@ -1401,7 +1362,7 @@ (*For rotate_tac: fast rotation of assumptions of subgoal i*) fun rotate_rule k i state = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state; + val Thm (der, {thy, maxidx, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val params = Term.strip_all_vars Bi; val rest = Term.strip_all_body Bi; @@ -1417,7 +1378,7 @@ else raise THM ("rotate_rule", k, [state]); in Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = shyps, @@ -1432,7 +1393,7 @@ number of premises. Useful with etac and underlies defer_tac*) fun permute_prems j k rl = let - val Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...}) = rl; + val Thm (der, {thy, maxidx, shyps, hyps, tpairs, prop, ...}) = rl; val prems = Logic.strip_imp_prems prop and concl = Logic.strip_imp_concl prop; val moved_prems = List.drop (prems, j) @@ -1448,7 +1409,7 @@ else raise THM ("permute_prems: k", k, [rl]); in Thm (deriv_rule1 (Proofterm.permute_prems_proof prems j m) der, - {thy_ref = thy_ref, + {thy = thy, tags = [], maxidx = maxidx, shyps = shyps, @@ -1466,7 +1427,7 @@ preceding parameters may be renamed to make all params distinct.*) fun rename_params_rule (cs, i) state = let - val Thm (der, {thy_ref, tags, maxidx, shyps, hyps, ...}) = state; + val Thm (der, {thy, tags, maxidx, shyps, hyps, ...}) = state; val (tpairs, Bs, Bi, C) = dest_state (state, i); val iparams = map #1 (Logic.strip_params Bi); val short = length iparams - length cs; @@ -1483,7 +1444,7 @@ a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); state) | [] => Thm (der, - {thy_ref = thy_ref, + {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps, @@ -1495,11 +1456,11 @@ (*** Preservation of bound variable names ***) -fun rename_boundvars pat obj (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = +fun rename_boundvars pat obj (thm as Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) = (case Term.rename_abs pat obj prop of NONE => thm | SOME prop' => Thm (der, - {thy_ref = thy_ref, + {thy = thy, tags = tags, maxidx = maxidx, hyps = hyps, @@ -1622,7 +1583,7 @@ tpairs=rtpairs, prop=rprop,...}) = orule (*How many hyps to skip over during normalization*) and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0) - val thy = Theory.deref (merge_thys2 state orule); + val thy = merge_thys2 state orule; (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **) fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) = let val normt = Envir.norm_term env; @@ -1654,7 +1615,7 @@ hyps = union_hyps rhyps shyps, tpairs = ntpairs, prop = Logic.list_implies normp, - thy_ref = Theory.check_thy thy}) + thy = thy}) in Seq.cons th thq end handle COMPOSE => thq; val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop) handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); @@ -1749,14 +1710,14 @@ (* oracle rule *) -fun invoke_oracle thy_ref1 name oracle arg = - let val Cterm {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = oracle arg in +fun invoke_oracle thy1 name oracle arg = + let val Cterm {thy = thy2, t = prop, T, maxidx, sorts} = oracle arg in if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else let val (ora, prf) = Proofterm.oracle_proof name prop in Thm (make_deriv [] [ora] [] prf, - {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), + {thy = Theory.merge (thy1, thy2), tags = [], maxidx = maxidx, shyps = sorts, @@ -1788,7 +1749,7 @@ let val (name, tab') = Name_Space.define (Context.Theory thy) true (b, ()) (Oracles.get thy); val thy' = Oracles.put tab' thy; - in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end; + in ((name, invoke_oracle thy' name oracle), thy') end; end; diff -r 71fef62c4213 -r 122416054a9c src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Tools/Code/code_haskell.ML Thu Aug 01 16:53:03 2013 +0200 @@ -463,19 +463,21 @@ fun add_monad target' raw_c_bind thy = let val c_bind = Code.read_const thy raw_c_bind; - in if target = target' then - thy - |> Code_Target.set_printings (Code_Symbol.Constant (c_bind, [(target, - SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))])) - else error "Only Haskell target allows for monad syntax" end; + in + if target = target' then + thy + |> Code_Target.set_printings (Code_Symbol.Constant (c_bind, [(target, + SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))])) + else error "Only Haskell target allows for monad syntax" + end; (** Isar setup **) val _ = Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads" - (Parse.term_group -- Parse.name >> (fn (raw_bind, target) => - Toplevel.theory (add_monad target raw_bind))); + (Parse.term -- Parse.name >> (fn (raw_bind, target) => + Toplevel.theory (add_monad target raw_bind))); val setup = Code_Target.add_target diff -r 71fef62c4213 -r 122416054a9c src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Tools/Code/code_target.ML Thu Aug 01 16:53:03 2013 +0200 @@ -752,7 +752,7 @@ -- Parse.and_list1 (@{keyword "("} |-- (Parse.name --| @{keyword ")"} -- Scan.option parse_target))); fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module = - parse_single_symbol_pragma @{keyword "constant"} Parse.term_group parse_const + parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const >> Code_Symbol.Constant || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco >> Code_Symbol.Type_Constructor @@ -784,7 +784,7 @@ -- code_expr_argsP))) >> (fn seri_args => check_code_cmd raw_cs seri_args); -val code_exprP = Scan.repeat1 Parse.term_group +val code_exprP = Scan.repeat1 Parse.term :|-- (fn raw_cs => (code_expr_checkingP raw_cs || code_expr_inP raw_cs)); val _ = @@ -812,7 +812,7 @@ val _ = Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant" - (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax + (process_multi_syntax Parse.term Code_Printer.parse_const_syntax add_const_syntax_cmd); val _ = @@ -842,7 +842,7 @@ val _ = Outer_Syntax.command @{command_spec "code_abort"} "permit constant to be implemented as program abort" - (Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd)); + (Scan.repeat1 Parse.term >> (Toplevel.theory o fold allow_abort_cmd)); val _ = Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants" diff -r 71fef62c4213 -r 122416054a9c src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Tools/Code/code_thingol.ML Thu Aug 01 16:53:03 2013 +0200 @@ -1018,10 +1018,16 @@ fun belongs_here thy' c = forall (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy'); fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy'); - fun read_const_expr "_" = ([], consts_of thy) - | read_const_expr s = if String.isSuffix "._" s + + val ctxt = Proof_Context.init_global thy; + fun read_const_expr str = + (case Syntax.parse_token ctxt (K NONE) Markup.empty (SOME o Symbol_Pos.implode o #1) str of + SOME "_" => ([], consts_of thy) + | SOME s => + if String.isSuffix "._" s then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s))) - else ([Code.read_const thy s], []); + else ([Code.read_const thy str], []) + | NONE => ([Code.read_const thy str], [])); in pairself flat o split_list o map read_const_expr end; fun code_depgr thy consts = @@ -1061,14 +1067,14 @@ val _ = Outer_Syntax.improper_command @{command_spec "code_thms"} "print system of code equations for code" - (Scan.repeat1 Parse.term_group >> (fn cs => + (Scan.repeat1 Parse.term >> (fn cs => Toplevel.unknown_theory o Toplevel.keep (fn state => code_thms_cmd (Toplevel.theory_of state) cs))); val _ = Outer_Syntax.improper_command @{command_spec "code_deps"} "visualize dependencies of code equations for code" - (Scan.repeat1 Parse.term_group >> (fn cs => + (Scan.repeat1 Parse.term >> (fn cs => Toplevel.unknown_theory o Toplevel.keep (fn state => code_deps_cmd (Toplevel.theory_of state) cs))); diff -r 71fef62c4213 -r 122416054a9c src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Tools/jEdit/src/actions.xml Thu Aug 01 16:53:03 2013 +0200 @@ -52,14 +52,34 @@ wm.addDockableWindow("isabelle-symbols"); - + - isabelle.jedit.PIDE.execution_range_none(); + isabelle.jedit.Isabelle.set_continuous_checking(); + + + + + isabelle.jedit.Isabelle.reset_continuous_checking(); - + + + isabelle.jedit.Isabelle.toggle_continuous_checking(); + + + - isabelle.jedit.PIDE.execution_range_visible(); + isabelle.jedit.Isabelle.set_node_required(view); + + + + + isabelle.jedit.Isabelle.reset_node_required(view); + + + + + isabelle.jedit.Isabelle.toggle_node_required(view); diff -r 71fef62c4213 -r 122416054a9c src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Thu Aug 01 16:53:03 2013 +0200 @@ -79,20 +79,33 @@ /* perspective */ - def node_perspective(): Text.Perspective = + private var _node_required = false + def node_required: Boolean = _node_required + def node_required_=(b: Boolean) + { + Swing_Thread.require() + if (_node_required != b) { + _node_required = b + PIDE.options_changed() + PIDE.flush_buffers() + } + } + + def node_perspective(): Document.Node.Perspective_Text = { Swing_Thread.require() - PIDE.execution_range() match { - case PIDE.Execution_Range.ALL => Text.Perspective.full - case PIDE.Execution_Range.NONE => Text.Perspective.empty - case PIDE.Execution_Range.VISIBLE => - Text.Perspective( + val perspective = + if (Isabelle.continuous_checking) { + (node_required, Text.Perspective( for { doc_view <- PIDE.document_views(buffer) range <- doc_view.perspective().ranges - } yield range) - } + } yield range)) + } + else (false, Text.Perspective.empty) + + Document.Node.Perspective(perspective._1, perspective._2) } @@ -101,6 +114,7 @@ def init_edits(): List[Document.Edit_Text] = { Swing_Thread.require() + val header = node_header() val text = JEdit_Lib.buffer_text(buffer) val perspective = node_perspective() @@ -108,18 +122,19 @@ List(session.header_edit(name, header), name -> Document.Node.Clear(), name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), - name -> Document.Node.Perspective(perspective)) + name -> perspective) } - def node_edits(perspective: Text.Perspective, text_edits: List[Text.Edit]) + def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit]) : List[Document.Edit_Text] = { Swing_Thread.require() + val header = node_header() List(session.header_edit(name, header), name -> Document.Node.Edits(text_edits), - name -> Document.Node.Perspective(perspective)) + name -> perspective) } @@ -128,7 +143,8 @@ private object pending_edits // owned by Swing thread { private val pending = new mutable.ListBuffer[Text.Edit] - private var last_perspective: Text.Perspective = Text.Perspective.empty + private var last_perspective: Document.Node.Perspective_Text = + Document.Node.Perspective(node_required, Text.Perspective.empty) def snapshot(): List[Text.Edit] = pending.toList diff -r 71fef62c4213 -r 122416054a9c src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Thu Aug 01 16:53:03 2013 +0200 @@ -57,6 +57,45 @@ } + /* continuous checking */ + + private val CONTINUOUS_CHECKING = "editor_continuous_checking" + + def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING) + + def continuous_checking_=(b: Boolean) + { + Swing_Thread.require() + + if (continuous_checking != b) { + PIDE.options.bool(CONTINUOUS_CHECKING) = b + PIDE.options_changed() + PIDE.flush_buffers() + } + } + + def set_continuous_checking() { continuous_checking = true } + def reset_continuous_checking() { continuous_checking = false } + def toggle_continuous_checking() { continuous_checking = !continuous_checking } + + + /* required document nodes */ + + private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false) + { + Swing_Thread.require() + PIDE.document_model(view.getBuffer) match { + case Some(model) => + model.node_required = (if (toggle) !model.node_required else set) + case None => + } + } + + def set_node_required(view: View) { node_required_update(view, set = true) } + def reset_node_required(view: View) { node_required_update(view, set = false) } + def toggle_node_required(view: View) { node_required_update(view, toggle = true) } + + /* font size */ def change_font_size(view: View, change: Int => Int) diff -r 71fef62c4213 -r 122416054a9c src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Thu Aug 01 16:53:03 2013 +0200 @@ -185,10 +185,14 @@ isabelle-readme.dock-position=bottom isabelle-symbols.dock-position=bottom isabelle-theories.dock-position=right -isabelle.execution-range-none.label=Check nothing -isabelle.execution-range-none.shortcut=C+e BACK_SPACE -isabelle.execution-range-visible=Check visible parts of theories -isabelle.execution-range-visible.shortcut=C+e SPACE +isabelle.set-continuous-checking.label=Set continuous checking +isabelle.reset-continuous-checking.label=Reset continuous checking +isabelle.toggle-continuous-checking.label=Toggle continuous checking +isabelle.toggle-continuous-checking.shortcut=C+e ENTER +isabelle.set-node-required.label=Set node required +isabelle.reset-node-required.label=Reset node required +isabelle.toggle-node-required.label=Toggle node required +isabelle.toggle-node-required.shortcut=C+e SPACE isabelle.control-bold.label=Control bold isabelle.control-bold.shortcut=C+e RIGHT isabelle.control-isub.label=Control subscript diff -r 71fef62c4213 -r 122416054a9c src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Thu Aug 01 16:53:03 2013 +0200 @@ -35,6 +35,8 @@ @volatile var plugin: Plugin = null @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty)) + def options_changed() { session.global_options.event(Session.Global_Options(options.value)) } + def thy_load(): JEdit_Thy_Load = session.thy_load.asInstanceOf[JEdit_Thy_Load] @@ -116,47 +118,22 @@ } } - - /* execution range */ - - object Execution_Range extends Enumeration { - val ALL = Value("all") - val NONE = Value("none") - val VISIBLE = Value("visible") - } - - def execution_range(): Execution_Range.Value = - options.string("editor_execution_range") match { - case "all" => Execution_Range.ALL - case "none" => Execution_Range.NONE - case "visible" => Execution_Range.VISIBLE - case s => error("Bad value for option \"editor_execution_range\": " + quote(s)) - } - - def update_execution_range(range: Execution_Range.Value) + def flush_buffers() { Swing_Thread.require() - if (options.string("editor_execution_range") != range.toString) { - options.string("editor_execution_range") = range.toString - PIDE.session.global_options.event(Session.Global_Options(options.value)) - - PIDE.session.update( - (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) { - case (edits, buffer) => - JEdit_Lib.buffer_lock(buffer) { - document_model(buffer) match { - case Some(model) => model.flushed_edits() ::: edits - case None => edits - } + session.update( + (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) { + case (edits, buffer) => + JEdit_Lib.buffer_lock(buffer) { + document_model(buffer) match { + case Some(model) => model.flushed_edits() ::: edits + case None => edits } - } - ) - } + } + } + ) } - - def execution_range_none(): Unit = update_execution_range(Execution_Range.NONE) - def execution_range_visible(): Unit = update_execution_range(Execution_Range.VISIBLE) } diff -r 71fef62c4213 -r 122416054a9c src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Thu Aug 01 16:52:28 2013 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Aug 01 16:53:03 2013 +0200 @@ -10,14 +10,14 @@ import isabelle._ import scala.actors.Actor._ -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component, - BoxPanel, Orientation, RadioButton, ButtonGroup} -import scala.swing.event.{ButtonClicked, MouseClicked} +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, + ScrollPane, Component, CheckBox, BorderPanel} +import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved} import java.lang.System -import java.awt.{BorderLayout, Graphics2D, Insets, Color} +import java.awt.{BorderLayout, Graphics2D, Insets, Point, Dimension} import javax.swing.{JList, BorderFactory} -import javax.swing.border.{BevelBorder, SoftBevelBorder, LineBorder} +import javax.swing.border.{BevelBorder, SoftBevelBorder} import org.gjt.sp.jedit.{View, jEdit} @@ -28,10 +28,27 @@ private val status = new ListView(Nil: List[Document.Node.Name]) { listenTo(mouse.clicks) + listenTo(mouse.moves) reactions += { - case MouseClicked(_, point, _, clicks, _) if clicks == 2 => + case MouseClicked(_, point, _, clicks, _) => val index = peer.locationToIndex(point) - if (index >= 0) Hyperlink(listData(index).node).follow(view) + if (index >= 0) { + if (in_checkbox(peer.indexToLocation(index), point)) { + if (clicks == 1) { + for { + buffer <- JEdit_Lib.jedit_buffer(listData(index).node) + model <- PIDE.document_model(buffer) + } model.node_required = !model.node_required + } + } + else if (clicks == 2) Hyperlink(listData(index).node).follow(view) + } + case MouseMoved(_, point, _) => + val index = peer.locationToIndex(point) + if (index >= 0 && in_checkbox(peer.indexToLocation(index), point)) + tooltip = "Mark as required for continuous checking" + else + tooltip = null } } status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP) @@ -55,77 +72,99 @@ Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " } } - private val execution_range = new BoxPanel(Orientation.Horizontal) { - private def button(range: PIDE.Execution_Range.Value, tip: String): RadioButton = - new RadioButton(range.toString) { - tooltip = tip - reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) } - } - private val label = - new Label("Range:") { tooltip = "Execution range of continuous document processing" } - private val b1 = button(PIDE.Execution_Range.ALL, "Check all theories (potentially slow)") - private val b2 = button(PIDE.Execution_Range.NONE, "Check nothing") - private val b3 = button(PIDE.Execution_Range.VISIBLE, "Check visible parts of theories") - private val group = new ButtonGroup(b1, b2, b3) - contents ++= List(label, b1, b2, b3) - border = new LineBorder(Color.GRAY) - - def load() - { - PIDE.execution_range() match { - case PIDE.Execution_Range.ALL => group.select(b1) - case PIDE.Execution_Range.NONE => group.select(b2) - case PIDE.Execution_Range.VISIBLE => group.select(b3) - } - } + private val continuous_checking = new CheckBox("Continuous checking") { + tooltip = "Continuous checking of proof document (visible and required parts)" + reactions += { case ButtonClicked(_) => Isabelle.continuous_checking = selected } + def load() { selected = Isabelle.continuous_checking } load() } private val logic = Isabelle_Logic.logic_selector(true) private val controls = - new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic) + new FlowPanel(FlowPanel.Alignment.Right)(continuous_checking, session_phase, logic) add(controls.peer, BorderLayout.NORTH) /* component state -- owned by Swing thread */ private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty + private var nodes_required: Set[Document.Node.Name] = Set.empty - private object Node_Renderer_Component extends Label + private def update_nodes_required() + { + nodes_required = Set.empty + for { + buffer <- JEdit_Lib.jedit_buffers + model <- PIDE.document_model(buffer) + if model.node_required + } nodes_required += model.name + } + + private def in_checkbox(loc0: Point, p: Point): Boolean = + Node_Renderer_Component != null && + (Node_Renderer_Component.checkbox_geometry match { + case Some((loc, size)) => + loc0.x + loc.x <= p.x && p.x < loc0.x + size.width && + loc0.y + loc.y <= p.y && p.y < loc0.y + size.height + case None => false + }) + + private object Node_Renderer_Component extends BorderPanel { opaque = false - xAlignment = Alignment.Leading - border = BorderFactory.createEmptyBorder(2, 2, 2, 2) var node_name = Document.Node.Name.empty - override def paintComponent(gfx: Graphics2D) - { - nodes_status.get(node_name) match { - case Some(st) if st.total > 0 => - val colors = List( - (st.unprocessed, PIDE.options.color_value("unprocessed1_color")), - (st.running, PIDE.options.color_value("running_color")), - (st.warned, PIDE.options.color_value("warning_color")), - (st.failed, PIDE.options.color_value("error_color"))) + + var checkbox_geometry: Option[(Point, Dimension)] = None + val checkbox = new CheckBox { + opaque = false + override def paintComponent(gfx: Graphics2D) + { + super.paintComponent(gfx) + if (location != null && size != null) + checkbox_geometry = Some((location, size)) + } + } + + val label = new Label { + opaque = false + xAlignment = Alignment.Leading + + override def paintComponent(gfx: Graphics2D) + { + border = BorderFactory.createEmptyBorder(2, 2, 2, 2) + val size = peer.getSize() + val insets = border.getBorderInsets(peer) + val w = size.width - insets.left - insets.right + val h = size.height - insets.top - insets.bottom - val size = peer.getSize() - val insets = border.getBorderInsets(peer) - val w = size.width - insets.left - insets.right - val h = size.height - insets.top - insets.bottom - var end = size.width - insets.right + nodes_status.get(node_name) match { + case Some(st) if st.total > 0 => + val colors = List( + (st.unprocessed, PIDE.options.color_value("unprocessed1_color")), + (st.running, PIDE.options.color_value("running_color")), + (st.warned, PIDE.options.color_value("warning_color")), + (st.failed, PIDE.options.color_value("error_color"))) - for { (n, color) <- colors } - { - gfx.setColor(color) - val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0) - gfx.fillRect(end - v, insets.top, v, h) - end = end - v - 1 - } - case _ => + var end = size.width - insets.right + for { (n, color) <- colors } + { + gfx.setColor(color) + val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0) + gfx.fillRect(end - v, insets.top, v, h) + end = end - v - 1 + } + case _ => + gfx.setColor(PIDE.options.color_value("unprocessed1_color")) + gfx.fillRect(insets.left, insets.top, w, h) + } + super.paintComponent(gfx) } - super.paintComponent(gfx) } + + layout(checkbox) = BorderPanel.Position.West + layout(label) = BorderPanel.Position.Center } private class Node_Renderer extends ListView.Renderer[Document.Node.Name] @@ -135,7 +174,8 @@ { val component = Node_Renderer_Component component.node_name = name - component.text = name.theory + component.checkbox.selected = nodes_required.contains(name) + component.label.text = name.theory component } } @@ -175,8 +215,10 @@ case _: Session.Global_Options => Swing_Thread.later { - execution_range.load() + continuous_checking.load() logic.load () + update_nodes_required() + status.repaint() } case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))