--- a/Admin/update-keywords Sun Nov 15 13:06:07 2009 +0100
+++ b/Admin/update-keywords Sun Nov 15 13:06:42 2009 +0100
@@ -1,30 +1,19 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
-# DESCRIPTION: Update standard keyword files.
+# DESCRIPTION: Update standard keyword files for Emacs Proof General
ISABELLE_HOME="$(isabelle getenv -b ISABELLE_HOME)"
LOG="$(isabelle getenv -b ISABELLE_OUTPUT)"/log
-## Emacs ProofGeneral
-
cd "$ISABELLE_HOME/etc"
-isabelle keywords -t emacs \
+isabelle keywords \
"$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \
- "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
+ "$LOG/IOA.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
-isabelle keywords -t emacs -k ZF \
+isabelle keywords -k ZF \
"$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
-
-## jEdit
-
-cd "$ISABELLE_HOME/lib/jedit"
-
-isabelle keywords -t jedit \
- "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz" \
- "$LOG/HOL-Statespace.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
--- a/etc/isar-keywords-ZF.el Sun Nov 15 13:06:07 2009 +0100
+++ b/etc/isar-keywords-ZF.el Sun Nov 15 13:06:42 2009 +0100
@@ -237,6 +237,7 @@
"open"
"output"
"overloaded"
+ "pervasive"
"recursor_eqns"
"shows"
"structure"
--- a/etc/isar-keywords.el Sun Nov 15 13:06:07 2009 +0100
+++ b/etc/isar-keywords.el Sun Nov 15 13:06:42 2009 +0100
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
+;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-Statespace.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
@@ -40,6 +40,10 @@
"axiomatization"
"axioms"
"back"
+ "boogie_end"
+ "boogie_open"
+ "boogie_status"
+ "boogie_vc"
"by"
"cannot_undo"
"case"
@@ -204,6 +208,7 @@
"refute_params"
"remove_thy"
"rep_datatype"
+ "repdef"
"sect"
"section"
"setup"
@@ -298,6 +303,7 @@
"outputs"
"overloaded"
"permissive"
+ "pervasive"
"post"
"pre"
"rename"
@@ -341,6 +347,7 @@
"atp_kill"
"atp_messages"
"atp_minimize"
+ "boogie_status"
"cd"
"class_deps"
"code_deps"
@@ -432,6 +439,8 @@
"axclass"
"axiomatization"
"axioms"
+ "boogie_end"
+ "boogie_open"
"class"
"classes"
"classrel"
@@ -518,6 +527,7 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
+ "boogie_vc"
"code_pred"
"corollary"
"cpodef"
@@ -531,6 +541,7 @@
"pcpodef"
"recdef_tc"
"rep_datatype"
+ "repdef"
"specification"
"subclass"
"sublocale"
--- a/lib/ProofGeneral/pgip.rnc Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/ProofGeneral/pgip.rnc Sun Nov 15 13:06:42 2009 +0100
@@ -4,8 +4,6 @@
# Authors: David Aspinall, LFCS, University of Edinburgh
# Christoph Lüth, University of Bremen
#
-# Version: $Id$
-#
# Status: Prototype.
#
# For additional commentary, see accompanying commentary document available at
--- a/lib/ProofGeneral/pgip_isar.xml Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/ProofGeneral/pgip_isar.xml Sun Nov 15 13:06:42 2009 +0100
@@ -1,8 +1,6 @@
-
<!-- Title: Pure/pgip_isar.xml
- ID: $Id$
Author: David Aspinall, University of Edinburgh
- Christoph Lüth, University of Bremen
+ Author: Christoph Lüth, University of Bremen
This file contains the configuration messages which configure
PGIP interfaces for Isabelle/Isar, in particular, explaining
--- a/lib/ProofGeneral/pgml.rnc Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/ProofGeneral/pgml.rnc Sun Nov 15 13:06:42 2009 +0100
@@ -3,7 +3,6 @@
#
# Authors: David Aspinall, LFCS, University of Edinburgh
# Christoph Lueth, University of Bremen
-# Version: $Id$
#
# Status: Complete, prototype.
#
--- a/lib/Tools/keywords Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/Tools/keywords Sun Nov 15 13:06:42 2009 +0100
@@ -16,9 +16,9 @@
echo
echo " Options are:"
echo " -k NAME specific name of keywords collection (default: empty)"
- echo " -t TARGET target tool (default: emacs)"
echo
echo " Generate outer syntax keyword files from (compressed) session LOGS."
+ echo " Targets Emacs Proof General."
echo
exit 1
}
@@ -29,17 +29,13 @@
# options
KEYWORDS_NAME=""
-TARGET_TOOL="emacs"
-while getopts "k:t:" OPT
+while getopts "k:" OPT
do
case "$OPT" in
k)
KEYWORDS_NAME="$OPTARG"
;;
- t)
- TARGET_TOOL="$OPTARG"
- ;;
\?)
usage
;;
@@ -49,15 +45,10 @@
shift $(($OPTIND - 1))
-# args
-
-LOGS="$@"; shift "$#"
-
-
## main
SESSIONS=""
-for LOG in $LOGS
+for LOG in "$@"
do
NAME="$(basename "$LOG" .gz)"
if [ -z "$SESSIONS" ]; then
@@ -67,7 +58,7 @@
fi
done
-for LOG in $LOGS
+for LOG in "$@"
do
if [ "${LOG%.gz}" = "$LOG" ]; then
cat "$LOG"
@@ -76,4 +67,4 @@
fi
echo
done | \
-perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$TARGET_TOOL" "$SESSIONS"
+perl -w "$ISABELLE_HOME/lib/scripts/keywords.pl" "$KEYWORDS_NAME" "$SESSIONS"
--- a/lib/browser/GraphBrowser/AWTFontMetrics.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/AWTFontMetrics.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,8 +1,6 @@
/***************************************************************************
Title: GraphBrowser/AWTFontMetrics.java
- ID: $Id$
Author: Gerwin Klein, TU Muenchen
- Copyright 2003 TU Muenchen
AbstractFontMetrics from the AWT for graphics mode.
--- a/lib/browser/GraphBrowser/AbstractFontMetrics.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/AbstractFontMetrics.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,8 +1,6 @@
/***************************************************************************
Title: GraphBrowser/AWTFontMetrics.java
- ID: $Id$
Author: Gerwin Klein, TU Muenchen
- Copyright 2003 TU Muenchen
AbstractFontMetrics avoids dependency on java.awt.FontMetrics in
batch mode.
--- a/lib/browser/GraphBrowser/Box.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/Box.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,8 +1,6 @@
/***************************************************************************
Title: GraphBrowser/Box.java
- ID: $Id$
Author: Gerwin Klein, TU Muenchen
- Copyright 2003 TU Muenchen
A box with width and height. Used instead of java.awt.Dimension for
batch mode.
--- a/lib/browser/GraphBrowser/Console.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/Console.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,6 +1,5 @@
/***************************************************************************
Title: GraphBrowser/Console.java
- ID: $Id$
Author: Gerwin Klein, TU Muenchen
This is the graph browser's main class when run as a console application.
--- a/lib/browser/GraphBrowser/DefaultFontMetrics.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/DefaultFontMetrics.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,6 +1,5 @@
/***************************************************************************
Title: GraphBrowser/DefaultFontMetrics.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Default font metrics which is used when no graphics context
--- a/lib/browser/GraphBrowser/DummyVertex.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/DummyVertex.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,8 +1,6 @@
/***************************************************************************
Title: GraphBrowser/DummyVertex.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
- Copyright 1997 TU Muenchen
This class represents a dummy vertex, which is used to simplify the
layout algorithm.
--- a/lib/browser/GraphBrowser/Graph.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/Graph.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,8 +1,6 @@
/***************************************************************************
Title: GraphBrowser/Graph.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
- Copyright 1997 TU Muenchen
This class contains the core of the layout algorithm and methods for
drawing and PostScript output.
--- a/lib/browser/GraphBrowser/GraphBrowser.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/GraphBrowser.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,6 +1,5 @@
/***************************************************************************
Title: GraphBrowser/GraphBrowser.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
This is the graph browser's main class. It contains the "main(...)"
--- a/lib/browser/GraphBrowser/GraphBrowserFrame.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/GraphBrowserFrame.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,6 +1,5 @@
/***************************************************************************
Title: GraphBrowser/GraphBrowserFrame.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
This class is the frame for the stand-alone application. It contains
--- a/lib/browser/GraphBrowser/GraphView.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/GraphView.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,6 +1,5 @@
/***************************************************************************
Title: GraphBrowser/GraphView.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
This class defines the window in which the graph is displayed. It
--- a/lib/browser/GraphBrowser/NormalVertex.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/NormalVertex.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,6 +1,5 @@
/***************************************************************************
Title: GraphBrowser/NormalVertex.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
This class represents an ordinary vertex. It contains methods for
--- a/lib/browser/GraphBrowser/Region.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/Region.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,8 +1,6 @@
/***************************************************************************
Title: GraphBrowser/Region.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
- Copyright 1997 TU Muenchen
This is an auxiliary class which is used by the layout algorithm when
calculating coordinates with the "pendulum method". A "region" is a
--- a/lib/browser/GraphBrowser/Spline.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/Spline.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,8 +1,6 @@
/***************************************************************************
Title: GraphBrowser/Spline.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
- Copyright 1997 TU Muenchen
This class is used for drawing spline curves (which are not yet
supported by the Java AWT).
--- a/lib/browser/GraphBrowser/TreeBrowser.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/TreeBrowser.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,6 +1,5 @@
/***************************************************************************
Title: GraphBrowser/TreeBrowser.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
This class defines the browser window which is used to display directory
--- a/lib/browser/GraphBrowser/TreeNode.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/TreeNode.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,6 +1,5 @@
/***************************************************************************
Title: GraphBrowser/TreeNode.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
This class contains methods for storing and manipulating directory
--- a/lib/browser/GraphBrowser/Vertex.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/GraphBrowser/Vertex.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,6 +1,5 @@
/***************************************************************************
Title: GraphBrowser/Vertex.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
This class contains attributes and methods common to all kinds of
--- a/lib/browser/Makefile Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/Makefile Sun Nov 15 13:06:42 2009 +0100
@@ -1,4 +1,3 @@
-# $Id$
DST=classes
--- a/lib/browser/awtUtilities/Border.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/awtUtilities/Border.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,8 +1,6 @@
/***************************************************************************
Title: awtUtilities/Border.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
- Copyright 1997 TU Muenchen
This class defines a nice 3D border.
***************************************************************************/
--- a/lib/browser/awtUtilities/MessageDialog.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/awtUtilities/MessageDialog.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,8 +1,6 @@
/***************************************************************************
Title: awtUtilities/MessageDialog.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
- Copyright 1997 TU Muenchen
This class defines a dialog window for displaying messages and buttons.
***************************************************************************/
--- a/lib/browser/awtUtilities/TextFrame.java Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/browser/awtUtilities/TextFrame.java Sun Nov 15 13:06:42 2009 +0100
@@ -1,8 +1,6 @@
/***************************************************************************
Title: Graph/TextFrame.java
- ID: $Id$
Author: Stefan Berghofer, TU Muenchen
- Copyright 1997 TU Muenchen
This class defines a simple text viewer.
***************************************************************************/
--- a/lib/html/library_index_header.template Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/html/library_index_header.template Sun Nov 15 13:06:42 2009 +0100
@@ -1,7 +1,6 @@
<?xml version="1.0" encoding="iso-8859-1"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<!-- $Id$ -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
--- a/lib/jedit/README Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-Isabelle support for jEdit -- http://www.jedit.org/
-===================================================
-
-This provides both a basic editing "mode" (with some degree of syntax
-highlighting), and a minimal "plugin" with some support for
-interaction with the Isabelle process.
-
-
-Mode installation
------------------
-
-1) Copy or symlink [ISABELLE_HOME]/lib/jedit/isabelle.xml to
-[JEDIT_SETTINGS]/modes/
-
-2) Add the following entry [JEDIT_SETTINGS]/modes/catalog
-
- <MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>
-
-Example catalog file:
-
- <?xml version="1.0"?>
- <!DOCTYPE MODES SYSTEM "catalog.dtd">
- <MODES>
- <MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>
- </MODES>
-
-
-Plugin installation
--------------------
-
-1) Install copies of the Isabelle jars:
-
- [ISABELLE_HOME]/lib/classes/Pure.jar -> [JEDIT_SETTINGS]/jars/isabelle-Pure.jar
- [ISABELLE_HOME]/lib/jedit/isabelle.jar -> [JEDIT_SETTINGS]/jars/isabelle.jar
-
-2) Install scala-library.jar from the regular Scala distribution,
-cf. the http://www.scala-lang.org/downloads/index.html as
-
- [JEDIT_SETTINGS]/jars/isabelle-scala-library.jar
-
-3) Enable the plugin using the manager of jEdit; invoke the "isabelle"
-editor action. The resulting window may be docked, e.g. at bottom.
-
-Note that the Errorlist plugin provides some useful options like "Show
-error icons in the gutter", for immediate feedback of Isabelle
-warnings and errors in the source text. The Errorlist window may be
-docked likewise.
-
-
-$Id$
--- a/lib/jedit/isabelle.xml Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,347 +0,0 @@
-<?xml version="1.0"?>
-<!DOCTYPE MODE SYSTEM "xmode.dtd">
-<!-- Generated from Pure + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + FOL + ZF. -->
-<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->
-<MODE>
- <PROPS>
- <PROPERTY NAME="commentStart" VALUE="(*"/>
- <PROPERTY NAME="commentEnd" VALUE="*)"/>
- <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
- <PROPERTY NAME="indentOpenBrackets" VALUE="{"/>
- <PROPERTY NAME="indentCloseBrackets" VALUE="}"/>
- <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
- <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
- <PROPERTY NAME="tabSize" VALUE="2" />
- <PROPERTY NAME="indentSize" VALUE="2" />
- </PROPS>
- <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
- <SPAN TYPE="COMMENT1" NO_ESCAPE="TRUE">
- <BEGIN>(*</BEGIN>
- <END>*)</END>
- </SPAN>
- <SPAN TYPE="COMMENT3" NO_ESCAPE="TRUE">
- <BEGIN>{*</BEGIN>
- <END>*}</END>
- </SPAN>
- <SPAN TYPE="LITERAL1">
- <BEGIN>`</BEGIN>
- <END>`</END>
- </SPAN>
- <SPAN TYPE="LITERAL3">
- <BEGIN>"</BEGIN>
- <END>"</END>
- </SPAN>
- <KEYWORDS>
- <OPERATOR>.</OPERATOR>
- <OPERATOR>..</OPERATOR>
- <INVALID>Isabelle.command</INVALID>
- <INVALID>Isar.begin_document</INVALID>
- <INVALID>Isar.define_command</INVALID>
- <INVALID>Isar.edit_document</INVALID>
- <INVALID>Isar.end_document</INVALID>
- <OPERATOR>ML</OPERATOR>
- <LABEL>ML_command</LABEL>
- <OPERATOR>ML_prf</OPERATOR>
- <LABEL>ML_val</LABEL>
- <OPERATOR>abbreviation</OPERATOR>
- <KEYWORD4>actions</KEYWORD4>
- <KEYWORD4>advanced</KEYWORD4>
- <OPERATOR>also</OPERATOR>
- <KEYWORD4>and</KEYWORD4>
- <KEYWORD1>apply</KEYWORD1>
- <KEYWORD1>apply_end</KEYWORD1>
- <OPERATOR>arities</OPERATOR>
- <KEYWORD2>assume</KEYWORD2>
- <KEYWORD4>assumes</KEYWORD4>
- <OPERATOR>atom_decl</OPERATOR>
- <LABEL>atp_info</LABEL>
- <LABEL>atp_kill</LABEL>
- <LABEL>atp_messages</LABEL>
- <LABEL>atp_minimize</LABEL>
- <KEYWORD4>attach</KEYWORD4>
- <OPERATOR>attribute_setup</OPERATOR>
- <OPERATOR>automaton</OPERATOR>
- <KEYWORD4>avoids</KEYWORD4>
- <OPERATOR>ax_specification</OPERATOR>
- <OPERATOR>axclass</OPERATOR>
- <OPERATOR>axiomatization</OPERATOR>
- <OPERATOR>axioms</OPERATOR>
- <KEYWORD1>back</KEYWORD1>
- <KEYWORD4>begin</KEYWORD4>
- <KEYWORD4>binder</KEYWORD4>
- <OPERATOR>by</OPERATOR>
- <INVALID>cannot_undo</INVALID>
- <KEYWORD2>case</KEYWORD2>
- <KEYWORD4>case_eqns</KEYWORD4>
- <LABEL>cd</LABEL>
- <OPERATOR>chapter</OPERATOR>
- <OPERATOR>class</OPERATOR>
- <LABEL>class_deps</LABEL>
- <OPERATOR>classes</OPERATOR>
- <OPERATOR>classrel</OPERATOR>
- <OPERATOR>codatatype</OPERATOR>
- <OPERATOR>code_abort</OPERATOR>
- <OPERATOR>code_class</OPERATOR>
- <OPERATOR>code_const</OPERATOR>
- <OPERATOR>code_datatype</OPERATOR>
- <LABEL>code_deps</LABEL>
- <OPERATOR>code_include</OPERATOR>
- <OPERATOR>code_instance</OPERATOR>
- <OPERATOR>code_library</OPERATOR>
- <OPERATOR>code_module</OPERATOR>
- <OPERATOR>code_modulename</OPERATOR>
- <OPERATOR>code_monad</OPERATOR>
- <OPERATOR>code_pred</OPERATOR>
- <OPERATOR>code_reserved</OPERATOR>
- <LABEL>code_thms</LABEL>
- <OPERATOR>code_type</OPERATOR>
- <OPERATOR>coinductive</OPERATOR>
- <OPERATOR>coinductive_set</OPERATOR>
- <LABEL>commit</LABEL>
- <KEYWORD4>compose</KEYWORD4>
- <KEYWORD4>con_defs</KEYWORD4>
- <KEYWORD4>congs</KEYWORD4>
- <OPERATOR>constdefs</OPERATOR>
- <KEYWORD4>constrains</KEYWORD4>
- <OPERATOR>consts</OPERATOR>
- <OPERATOR>consts_code</OPERATOR>
- <KEYWORD4>contains</KEYWORD4>
- <OPERATOR>context</OPERATOR>
- <OPERATOR>corollary</OPERATOR>
- <OPERATOR>cpodef</OPERATOR>
- <OPERATOR>datatype</OPERATOR>
- <OPERATOR>declaration</OPERATOR>
- <OPERATOR>declare</OPERATOR>
- <KEYWORD2>def</KEYWORD2>
- <OPERATOR>defaultsort</OPERATOR>
- <KEYWORD1>defer</KEYWORD1>
- <OPERATOR>defer_recdef</OPERATOR>
- <KEYWORD4>defines</KEYWORD4>
- <OPERATOR>definition</OPERATOR>
- <OPERATOR>defs</OPERATOR>
- <LABEL>disable_pr</LABEL>
- <LABEL>display_drafts</LABEL>
- <OPERATOR>domain</OPERATOR>
- <KEYWORD4>domains</KEYWORD4>
- <OPERATOR>done</OPERATOR>
- <KEYWORD4>elimination</KEYWORD4>
- <LABEL>enable_pr</LABEL>
- <KEYWORD3>end</KEYWORD3>
- <OPERATOR>equivariance</OPERATOR>
- <INVALID>exit</INVALID>
- <LABEL>export_code</LABEL>
- <OPERATOR>extract</OPERATOR>
- <OPERATOR>extract_type</OPERATOR>
- <KEYWORD4>file</KEYWORD4>
- <OPERATOR>finalconsts</OPERATOR>
- <OPERATOR>finally</OPERATOR>
- <LABEL>find_consts</LABEL>
- <LABEL>find_theorems</LABEL>
- <KEYWORD2>fix</KEYWORD2>
- <KEYWORD4>fixes</KEYWORD4>
- <OPERATOR>fixpat</OPERATOR>
- <OPERATOR>fixrec</OPERATOR>
- <KEYWORD4>for</KEYWORD4>
- <OPERATOR>from</OPERATOR>
- <LABEL>full_prf</LABEL>
- <OPERATOR>fun</OPERATOR>
- <OPERATOR>function</OPERATOR>
- <OPERATOR>global</OPERATOR>
- <KEYWORD2>guess</KEYWORD2>
- <OPERATOR>have</OPERATOR>
- <LABEL>header</LABEL>
- <LABEL>help</LABEL>
- <OPERATOR>hence</OPERATOR>
- <OPERATOR>hide</OPERATOR>
- <KEYWORD4>hide_action</KEYWORD4>
- <KEYWORD4>hints</KEYWORD4>
- <KEYWORD4>identifier</KEYWORD4>
- <KEYWORD4>if</KEYWORD4>
- <KEYWORD4>imports</KEYWORD4>
- <KEYWORD4>in</KEYWORD4>
- <KEYWORD4>induction</KEYWORD4>
- <OPERATOR>inductive</OPERATOR>
- <KEYWORD1>inductive_cases</KEYWORD1>
- <OPERATOR>inductive_set</OPERATOR>
- <KEYWORD4>infix</KEYWORD4>
- <KEYWORD4>infixl</KEYWORD4>
- <KEYWORD4>infixr</KEYWORD4>
- <INVALID>init_toplevel</INVALID>
- <KEYWORD4>initially</KEYWORD4>
- <KEYWORD4>inputs</KEYWORD4>
- <OPERATOR>instance</OPERATOR>
- <OPERATOR>instantiation</OPERATOR>
- <KEYWORD4>internals</KEYWORD4>
- <OPERATOR>interpret</OPERATOR>
- <OPERATOR>interpretation</OPERATOR>
- <KEYWORD4>intros</KEYWORD4>
- <KEYWORD4>is</KEYWORD4>
- <OPERATOR>judgment</OPERATOR>
- <INVALID>kill</INVALID>
- <LABEL>kill_thy</LABEL>
- <KEYWORD4>lazy</KEYWORD4>
- <OPERATOR>lemma</OPERATOR>
- <OPERATOR>lemmas</OPERATOR>
- <OPERATOR>let</OPERATOR>
- <INVALID>linear_undo</INVALID>
- <OPERATOR>local</OPERATOR>
- <OPERATOR>local_setup</OPERATOR>
- <OPERATOR>locale</OPERATOR>
- <OPERATOR>method_setup</OPERATOR>
- <KEYWORD4>module_name</KEYWORD4>
- <KEYWORD4>monos</KEYWORD4>
- <OPERATOR>moreover</OPERATOR>
- <KEYWORD4>morphisms</KEYWORD4>
- <OPERATOR>next</OPERATOR>
- <LABEL>nitpick</LABEL>
- <OPERATOR>nitpick_params</OPERATOR>
- <OPERATOR>no_notation</OPERATOR>
- <OPERATOR>no_syntax</OPERATOR>
- <OPERATOR>no_translations</OPERATOR>
- <OPERATOR>nominal_datatype</OPERATOR>
- <OPERATOR>nominal_inductive</OPERATOR>
- <OPERATOR>nominal_inductive2</OPERATOR>
- <OPERATOR>nominal_primrec</OPERATOR>
- <OPERATOR>nonterminals</OPERATOR>
- <LABEL>normal_form</LABEL>
- <OPERATOR>notation</OPERATOR>
- <OPERATOR>note</OPERATOR>
- <KEYWORD4>notes</KEYWORD4>
- <KEYWORD2>obtain</KEYWORD2>
- <KEYWORD4>obtains</KEYWORD4>
- <OPERATOR>oops</OPERATOR>
- <KEYWORD4>open</KEYWORD4>
- <OPERATOR>oracle</OPERATOR>
- <KEYWORD4>output</KEYWORD4>
- <KEYWORD4>outputs</KEYWORD4>
- <KEYWORD4>overloaded</KEYWORD4>
- <OPERATOR>overloading</OPERATOR>
- <OPERATOR>parse_ast_translation</OPERATOR>
- <OPERATOR>parse_translation</OPERATOR>
- <OPERATOR>pcpodef</OPERATOR>
- <KEYWORD4>permissive</KEYWORD4>
- <KEYWORD4>post</KEYWORD4>
- <LABEL>pr</LABEL>
- <KEYWORD4>pre</KEYWORD4>
- <KEYWORD1>prefer</KEYWORD1>
- <KEYWORD2>presume</KEYWORD2>
- <LABEL>pretty_setmargin</LABEL>
- <LABEL>prf</LABEL>
- <OPERATOR>primrec</OPERATOR>
- <LABEL>print_abbrevs</LABEL>
- <LABEL>print_antiquotations</LABEL>
- <OPERATOR>print_ast_translation</OPERATOR>
- <LABEL>print_atps</LABEL>
- <LABEL>print_attributes</LABEL>
- <LABEL>print_binds</LABEL>
- <LABEL>print_cases</LABEL>
- <LABEL>print_claset</LABEL>
- <LABEL>print_classes</LABEL>
- <LABEL>print_codeproc</LABEL>
- <LABEL>print_codesetup</LABEL>
- <LABEL>print_commands</LABEL>
- <LABEL>print_configs</LABEL>
- <LABEL>print_context</LABEL>
- <LABEL>print_drafts</LABEL>
- <LABEL>print_facts</LABEL>
- <LABEL>print_induct_rules</LABEL>
- <LABEL>print_interps</LABEL>
- <LABEL>print_locale</LABEL>
- <LABEL>print_locales</LABEL>
- <LABEL>print_methods</LABEL>
- <LABEL>print_orders</LABEL>
- <LABEL>print_rules</LABEL>
- <LABEL>print_simpset</LABEL>
- <LABEL>print_statement</LABEL>
- <LABEL>print_syntax</LABEL>
- <LABEL>print_tcset</LABEL>
- <LABEL>print_theorems</LABEL>
- <LABEL>print_theory</LABEL>
- <LABEL>print_trans_rules</LABEL>
- <OPERATOR>print_translation</OPERATOR>
- <OPERATOR>proof</OPERATOR>
- <LABEL>prop</LABEL>
- <LABEL>pwd</LABEL>
- <OPERATOR>qed</OPERATOR>
- <LABEL>quickcheck</LABEL>
- <OPERATOR>quickcheck_params</OPERATOR>
- <INVALID>quit</INVALID>
- <OPERATOR>realizability</OPERATOR>
- <OPERATOR>realizers</OPERATOR>
- <OPERATOR>recdef</OPERATOR>
- <OPERATOR>recdef_tc</OPERATOR>
- <OPERATOR>record</OPERATOR>
- <KEYWORD4>recursor_eqns</KEYWORD4>
- <LABEL>refute</LABEL>
- <OPERATOR>refute_params</OPERATOR>
- <LABEL>remove_thy</LABEL>
- <KEYWORD4>rename</KEYWORD4>
- <OPERATOR>rep_datatype</OPERATOR>
- <KEYWORD4>restrict</KEYWORD4>
- <OPERATOR>sect</OPERATOR>
- <OPERATOR>section</OPERATOR>
- <OPERATOR>setup</OPERATOR>
- <KEYWORD2>show</KEYWORD2>
- <KEYWORD4>shows</KEYWORD4>
- <KEYWORD4>signature</KEYWORD4>
- <OPERATOR>simproc_setup</OPERATOR>
- <LABEL>sledgehammer</LABEL>
- <OPERATOR>sorry</OPERATOR>
- <OPERATOR>specification</OPERATOR>
- <KEYWORD4>states</KEYWORD4>
- <OPERATOR>statespace</OPERATOR>
- <KEYWORD4>structure</KEYWORD4>
- <OPERATOR>subclass</OPERATOR>
- <OPERATOR>sublocale</OPERATOR>
- <OPERATOR>subsect</OPERATOR>
- <OPERATOR>subsection</OPERATOR>
- <OPERATOR>subsubsect</OPERATOR>
- <OPERATOR>subsubsection</OPERATOR>
- <OPERATOR>syntax</OPERATOR>
- <LABEL>term</LABEL>
- <OPERATOR>termination</OPERATOR>
- <OPERATOR>text</OPERATOR>
- <OPERATOR>text_raw</OPERATOR>
- <OPERATOR>then</OPERATOR>
- <OPERATOR>theorem</OPERATOR>
- <OPERATOR>theorems</OPERATOR>
- <KEYWORD3>theory</KEYWORD3>
- <LABEL>thm</LABEL>
- <LABEL>thm_deps</LABEL>
- <KEYWORD2>thus</KEYWORD2>
- <LABEL>thy_deps</LABEL>
- <KEYWORD4>to</KEYWORD4>
- <LABEL>touch_thy</LABEL>
- <KEYWORD4>transitions</KEYWORD4>
- <OPERATOR>translations</OPERATOR>
- <KEYWORD4>transrel</KEYWORD4>
- <OPERATOR>txt</OPERATOR>
- <OPERATOR>txt_raw</OPERATOR>
- <LABEL>typ</LABEL>
- <KEYWORD4>type_elims</KEYWORD4>
- <KEYWORD4>type_intros</KEYWORD4>
- <OPERATOR>typed_print_translation</OPERATOR>
- <OPERATOR>typedecl</OPERATOR>
- <OPERATOR>typedef</OPERATOR>
- <OPERATOR>types</OPERATOR>
- <OPERATOR>types_code</OPERATOR>
- <OPERATOR>ultimately</OPERATOR>
- <KEYWORD4>unchecked</KEYWORD4>
- <INVALID>undo</INVALID>
- <INVALID>undos_proof</INVALID>
- <OPERATOR>unfolding</OPERATOR>
- <LABEL>unused_thms</LABEL>
- <OPERATOR>use</OPERATOR>
- <LABEL>use_thy</LABEL>
- <KEYWORD4>uses</KEYWORD4>
- <OPERATOR>using</OPERATOR>
- <LABEL>value</LABEL>
- <LABEL>values</LABEL>
- <LABEL>welcome</LABEL>
- <KEYWORD4>where</KEYWORD4>
- <OPERATOR>with</OPERATOR>
- <OPERATOR>{</OPERATOR>
- <OPERATOR>}</OPERATOR>
- </KEYWORDS>
- </RULES>
-</MODE>
--- a/lib/jedit/plugin/Isabelle.props Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-## Isabelle plugin properties
-## $Id$
-
-#identification
-plugin.isabelle.jedit.IsabellePlugin.name = Isabelle
-plugin.isabelle.jedit.IsabellePlugin.author = Makarius
-plugin.isabelle.jedit.IsabellePlugin.version = 0.0.1
-plugin.isabelle.jedit.IsabellePlugin.description = Basic Isabelle support
-
-#system parameters
-plugin.isabelle.jedit.IsabellePlugin.activate = defer
-plugin.isabelle.jedit.IsabellePlugin.usePluginHome = false
-plugin.isabelle.jedit.IsabellePlugin.jars = isabelle-Pure.jar isabelle-scala-library.jar
-
-#dependencies
-plugin.isabelle.jedit.IsabellePlugin.depend.0 = jdk 1.5
-plugin.isabelle.jedit.IsabellePlugin.depend.1 = jedit 04.03.00.00
-plugin.isabelle.jedit.IsabellePlugin.depend.2 = plugin errorlist.ErrorListPlugin 1.7
-plugin.isabelle.jedit.IsabellePlugin.depend.3 = plugin sidekick.SideKickPlugin 0.7.4
-
-#dockable component
-isabelle.label = Isabelle
-isabelle.title = Isabelle
-isabelle.longtitle = Basic Isabelle process
-
-#menu
-plugin.isabelle.jedit.IsabellePlugin.menu-item = isabelle
-
-
-#Isabelle options
-isabelle.print-modes = no_brackets no_type_brackets xsymbols
-isabelle.logic =
--- a/lib/jedit/plugin/dockables.xml Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-<?xml version="1.0"?>
-<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
-<!-- $Id$ -->
-
-<DOCKABLES>
- <DOCKABLE NAME="isabelle" MOVABLE="TRUE">
- new isabelle.jedit.IsabelleDock(view, position);
- </DOCKABLE>
-</DOCKABLES>
-
--- a/lib/jedit/plugin/isabelle_dock.scala Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,151 +0,0 @@
-/* Title: lib/jedit/plugin/isabelle_dock.scala
- ID: $Id$
- Author: Makarius
-
-Dockable window for Isabelle process control.
-*/
-
-package isabelle.jedit
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DefaultFocusComponent
-import org.gjt.sp.jedit.gui.DockableWindowManager
-import org.gjt.sp.jedit.gui.RolloverButton
-import org.gjt.sp.jedit.gui.HistoryTextField
-import org.gjt.sp.jedit.GUIUtilities
-
-import java.awt.Color
-import java.awt.Insets
-import java.awt.BorderLayout
-import java.awt.Dimension
-import java.awt.event.ActionListener
-import java.awt.event.ActionEvent
-import javax.swing.BoxLayout
-import javax.swing.JPanel
-import javax.swing.JScrollPane
-import javax.swing.JTextPane
-import javax.swing.text.{StyledDocument, StyleConstants}
-import javax.swing.SwingUtilities
-import javax.swing.Icon
-import javax.swing.Box
-import javax.swing.JTextField
-import javax.swing.JComboBox
-import javax.swing.DefaultComboBoxModel
-
-
-class IsabelleDock(view: View, position: String)
- extends JPanel(new BorderLayout) with DefaultFocusComponent
-{
- private val text = new HistoryTextField("isabelle", false, true)
- private val logic_combo = new JComboBox
-
- {
- // output pane
- val pane = new JTextPane
- pane.setEditable(false)
- add(BorderLayout.CENTER, new JScrollPane(pane))
- if (position == DockableWindowManager.FLOATING)
- setPreferredSize(new Dimension(1000, 500))
-
- val doc = pane.getDocument.asInstanceOf[StyledDocument]
-
- def make_style(name: String, bg: Boolean, color: Color) = {
- val style = doc.addStyle(name, null)
- if (bg) StyleConstants.setBackground(style, color)
- else StyleConstants.setForeground(style, color)
- style
- }
- val raw_style = make_style("raw", false, Color.GRAY)
- val info_style = make_style("info", true, new Color(160, 255, 160))
- val warning_style = make_style("warning", true, new Color(255, 255, 160))
- val error_style = make_style("error", true, new Color(255, 160, 160))
-
- IsabellePlugin.add_permanent_consumer (result =>
- if (result != null && !result.is_system) {
- SwingUtilities.invokeLater(new Runnable {
- def run = {
- val logic = IsabellePlugin.isabelle.session
- logic_combo.setModel(new DefaultComboBoxModel(Array(logic).asInstanceOf[Array[AnyRef]]))
- logic_combo.setPrototypeDisplayValue("AAAA") // FIXME ??
-
- val doc = pane.getDocument.asInstanceOf[StyledDocument]
- val style = result.kind match {
- case IsabelleProcess.Kind.WARNING => warning_style
- case IsabelleProcess.Kind.ERROR => error_style
- case IsabelleProcess.Kind.TRACING => info_style
- case _ => if (result.is_raw) raw_style else null
- }
- doc.insertString(doc.getLength, IsabellePlugin.result_content(result), style)
- if (!result.is_raw) doc.insertString(doc.getLength, "\n", style)
- pane.setCaretPosition(doc.getLength)
- }
- })
- })
-
-
- // control box
- val box = new Box(BoxLayout.X_AXIS)
- add(BorderLayout.SOUTH, box)
-
-
- // logic combo
- logic_combo.setToolTipText("Isabelle logics")
- logic_combo.setRequestFocusEnabled(false)
- logic_combo.setModel(new DefaultComboBoxModel(Array("default").asInstanceOf[Array[AnyRef]]))
- box.add(logic_combo)
-
-
- // mode combo
- val mode_Isar = "Isar"
- val mode_ML = "ML"
- val modes = Array(mode_Isar, mode_ML)
- var mode = mode_Isar
-
- val mode_combo = new JComboBox
- mode_combo.setToolTipText("Toplevel mode")
- mode_combo.setRequestFocusEnabled(false)
- mode_combo.setModel(new DefaultComboBoxModel(modes.asInstanceOf[Array[AnyRef]]))
- mode_combo.setPrototypeDisplayValue("AAAA")
- mode_combo.addActionListener(new ActionListener {
- def actionPerformed(evt: ActionEvent): Unit = {
- mode = mode_combo.getSelectedItem.asInstanceOf[String]
- }
- })
- box.add(mode_combo)
-
-
- // input field
- text.setToolTipText("Command line")
- text.addActionListener(new ActionListener {
- def actionPerformed(evt: ActionEvent): Unit = {
- val command = IsabellePlugin.symbols.encode(text.getText)
- if (command.length > 0) {
- if (mode == mode_Isar)
- IsabellePlugin.isabelle.command(command)
- else if (mode == mode_ML)
- IsabellePlugin.isabelle.ML(command)
- text.setText("")
- }
- }
- })
- box.add(text)
-
-
- // buttons
- def icon_button(icon: String, tip: String, action: => Unit) = {
- val button = new RolloverButton(GUIUtilities.loadIcon(icon))
- button.setToolTipText(tip)
- button.setMargin(new Insets(0,0,0,0))
- button.setRequestFocusEnabled(false)
- button.addActionListener(new ActionListener {
- def actionPerformed(evt: ActionEvent): Unit = action
- })
- box.add(button)
- }
-
- icon_button("Cancel.png", "Stop", IsabellePlugin.isabelle.interrupt)
- icon_button("Clear.png", "Clear", pane.setText(""))
- }
-
- def focusOnDefaultComponent: Unit = text.requestFocus
-}
--- a/lib/jedit/plugin/isabelle_parser.scala Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-/* Title: lib/jedit/plugin/isabelle_parser.scala
- ID: $Id$
- Author: Makarius
-
-Isabelle parser setup for Sidekick plugin.
-*/
-
-package isabelle.jedit
-
-import javax.swing.text.Position
-import javax.swing.tree.DefaultMutableTreeNode
-import javax.swing.tree.DefaultTreeModel
-
-import org.gjt.sp.jedit.{Buffer, EditPane}
-import org.gjt.sp.util.Log
-
-import errorlist.DefaultErrorSource
-import sidekick.{Asset, SideKickParser, SideKickParsedData, SideKickCompletion}
-
-
-private class IsabelleAsset(name: String, content: String) extends Asset(name)
-{
- override def getShortString() = { name }
- override def getLongString() = { content }
- override def getIcon() = { null }
-}
-
-
-class IsabelleParser extends SideKickParser("isabelle") {
-
- /* parsing */
-
- private var stopped = false
-
- override def stop () { stopped = true }
-
- def parse(buffer: Buffer, e: DefaultErrorSource): SideKickParsedData = {
- stopped = false
-
- var text: String = null
- var data: SideKickParsedData = null
-
- try {
- buffer.readLock()
- text = buffer.getText(0, buffer.getLength)
- data = new SideKickParsedData(buffer.getName)
-
- val asset = new IsabelleAsset("theory", null)
- asset.setStart(buffer.createPosition(0))
- asset.setEnd(buffer.createPosition(buffer.getLength))
-
- val node = new DefaultMutableTreeNode(asset)
- data.root.insert(node, node.getChildCount)
-
- }
- finally {
- buffer.readUnlock()
- }
-
- data
- }
-
-
- /* completion */
-
- override def supportsCompletion = true
- override def canCompleteAnywhere = true
-
- override def complete(pane: EditPane, caret: Int): SideKickCompletion = null
-
-}
-
--- a/lib/jedit/plugin/isabelle_plugin.scala Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,170 +0,0 @@
-/* Title: lib/jedit/plugin/isabelle_plugin.scala
- ID: $Id$
- Author: Makarius
-
-Isabelle/jEdit plugin -- main setup.
-*/
-
-package isabelle.jedit
-
-import java.util.Properties
-import java.lang.NumberFormatException
-
-import scala.collection.mutable.ListBuffer
-import scala.io.Source
-
-import org.gjt.sp.util.Log
-import org.gjt.sp.jedit.{jEdit, EBPlugin, EBMessage}
-import org.gjt.sp.jedit.msg.DockableWindowUpdate
-
-import errorlist.DefaultErrorSource
-import errorlist.ErrorSource
-
-
-
-/** global state **/
-
-object IsabellePlugin {
-
- /* Isabelle symbols */
-
- val symbols = new Symbol.Interpretation
-
- def result_content(result: IsabelleProcess.Result) =
- XML.content(YXML.parse_failsafe(symbols.decode(result.result))).mkString("")
-
-
- /* Isabelle process */
-
- var isabelle: IsabelleProcess = null
-
-
- /* unique ids */
-
- private var id_count: BigInt = 0
-
- def id() : String = synchronized { id_count += 1; "jedit:" + id_count }
-
- def id_properties(value: String) : Properties = {
- val props = new Properties
- props.setProperty(Markup.ID, value)
- props
- }
-
- def id_properties() : Properties = { id_properties(id()) }
-
-
- /* result consumers */
-
- type Consumer = IsabelleProcess.Result => Boolean
- private var consumers = new ListBuffer[Consumer]
-
- def add_consumer(consumer: Consumer) = synchronized { consumers += consumer }
-
- def add_permanent_consumer(consumer: IsabelleProcess.Result => Unit) = {
- add_consumer(result => { consumer(result); false })
- }
-
- def del_consumer(consumer: Consumer) = synchronized { consumers -= consumer }
-
- private def consume(result: IsabelleProcess.Result) = {
- synchronized { consumers.elements.toList } foreach (consumer =>
- {
- if (result != null && result.is_control) Log.log(Log.DEBUG, result, null)
- val finished =
- try { consumer(result) }
- catch { case e: Throwable => Log.log(Log.ERROR, result, e); true }
- if (finished || result == null) del_consumer(consumer)
- })
- }
-
- class ConsumerThread extends Thread {
- override def run = {
- var finished = false
- while (!finished) {
- val result =
- try { IsabellePlugin.isabelle.get_result() }
- catch { case _: NullPointerException => null }
-
- if (result != null) {
- consume(result)
- if (result.kind == IsabelleProcess.Kind.EXIT) {
- consume(null)
- finished = true
- }
- }
- else finished = true
- }
- }
- }
-
-}
-
-
-/* Main plugin setup */
-
-class IsabellePlugin extends EBPlugin {
-
- import IsabellePlugin._
-
- val errors = new DefaultErrorSource("isabelle")
- val consumer_thread = new ConsumerThread
-
-
- override def start = {
-
- /* error source */
-
- ErrorSource.registerErrorSource(errors)
-
- add_permanent_consumer (result =>
- if (result != null &&
- (result.kind == IsabelleProcess.Kind.WARNING ||
- result.kind == IsabelleProcess.Kind.ERROR)) {
- (Position.line_of(result.props), Position.file_of(result.props)) match {
- case (Some(line), Some(file)) =>
- val typ =
- if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING
- else ErrorSource.ERROR
- val content = result_content(result)
- if (content.length > 0) {
- val lines = Source.fromString(content).getLines
- val err = new DefaultErrorSource.DefaultError(errors,
- typ, file, line - 1, 0, 0, lines.next)
- for (msg <- lines) err.addExtraMessage(msg)
- errors.addError(err)
- }
- case _ =>
- }
- })
-
-
- /* Isabelle process */
-
- val options =
- (for (mode <- jEdit.getProperty("isabelle.print-modes").split("\\s+") if mode != "")
- yield "-m" + mode)
- val args = {
- val logic = jEdit.getProperty("isabelle.logic")
- if (logic != "") List(logic) else Nil
- }
- isabelle = new IsabelleProcess((options ++ args): _*)
-
- consumer_thread.start
-
- }
-
-
- override def stop = {
- isabelle.kill
- consumer_thread.join
- ErrorSource.unregisterErrorSource(errors)
- }
-
-
- override def handleMessage(message: EBMessage) = message match {
- case _: DockableWindowUpdate => // FIXME check isabelle process
- case _ =>
- }
-
-}
--- a/lib/jedit/plugin/mk Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-#!/bin/bash
-# $Id$
-
-JEDIT_HOME="$HOME/lib/jedit/current"
-PLUGINS="$HOME/.jedit/jars"
-
-
-rm -rf build/ && mkdir -p build
-rm -f ../isabelle.jar
-
-scalac -d build \
- -cp $JEDIT_HOME/jedit.jar:$PLUGINS/SideKick.jar:$PLUGINS/ErrorList.jar:$PLUGINS/Console.jar:../../classes/Pure.jar \
- isabelle_plugin.scala \
- isabelle_dock.scala \
- isabelle_parser.scala \
-&& (
- cp *.xml *.props build/
- cd build
- jar cf ../../isabelle.jar .
-)
-
-rm -rf build/
--- a/lib/jedit/plugin/services.xml Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-<?xml version="1.0"?>
-<!DOCTYPE SERVICES SYSTEM "services.dtd">
-<!-- $Id$ -->
-
-<SERVICES>
- <SERVICE CLASS="sidekick.SideKickParser" NAME="isabelle">
- new isabelle.jedit.IsabelleParser();
- </SERVICE>
-</SERVICES>
-
--- a/lib/logo/index.html Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/logo/index.html Sun Nov 15 13:06:42 2009 +0100
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<html>
<head>
--- a/lib/scripts/keywords.pl Sun Nov 15 13:06:07 2009 +0100
+++ b/lib/scripts/keywords.pl Sun Nov 15 13:06:42 2009 +0100
@@ -6,7 +6,7 @@
## arguments
-my ($keywords_name, $target_tool, $sessions) = @ARGV;
+my ($keywords_name, $sessions) = @ARGV;
## keywords
@@ -109,106 +109,12 @@
close OUTPUT;
select;
- print STDERR "${target_tool}: ${file}\n";
-}
-
-
-## jEdit output
-
-sub jedit_output {
- my %keyword_types = (
- "minor" => "KEYWORD4",
- "control" => "INVALID",
- "diag" => "LABEL",
- "theory-begin" => "KEYWORD3",
- "theory-switch" => "KEYWORD3",
- "theory-end" => "KEYWORD3",
- "theory-heading" => "OPERATOR",
- "theory-decl" => "OPERATOR",
- "theory-script" => "KEYWORD1",
- "theory-goal" => "OPERATOR",
- "qed" => "OPERATOR",
- "qed-block" => "OPERATOR",
- "qed-global" => "OPERATOR",
- "proof-heading" => "OPERATOR",
- "proof-goal" => "OPERATOR",
- "proof-block" => "OPERATOR",
- "proof-open" => "OPERATOR",
- "proof-close" => "OPERATOR",
- "proof-chain" => "OPERATOR",
- "proof-decl" => "OPERATOR",
- "proof-asm" => "KEYWORD2",
- "proof-asm-goal" => "KEYWORD2",
- "proof-script" => "KEYWORD1"
- );
- my $file = "isabelle.xml";
- open (OUTPUT, "> ${file}") || die "$!";
- select OUTPUT;
-
- print <<'EOF';
-<?xml version="1.0"?>
-<!DOCTYPE MODE SYSTEM "xmode.dtd">
-EOF
- print "<!-- Generated from ${sessions}. -->\n";
- print "<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->\n";
- print <<'EOF';
-<MODE>
- <PROPS>
- <PROPERTY NAME="commentStart" VALUE="(*"/>
- <PROPERTY NAME="commentEnd" VALUE="*)"/>
- <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
- <PROPERTY NAME="indentOpenBrackets" VALUE="{"/>
- <PROPERTY NAME="indentCloseBrackets" VALUE="}"/>
- <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
- <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
- <PROPERTY NAME="tabSize" VALUE="2" />
- <PROPERTY NAME="indentSize" VALUE="2" />
- </PROPS>
- <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
- <SPAN TYPE="COMMENT1" NO_ESCAPE="TRUE">
- <BEGIN>(*</BEGIN>
- <END>*)</END>
- </SPAN>
- <SPAN TYPE="COMMENT3" NO_ESCAPE="TRUE">
- <BEGIN>{*</BEGIN>
- <END>*}</END>
- </SPAN>
- <SPAN TYPE="LITERAL1">
- <BEGIN>`</BEGIN>
- <END>`</END>
- </SPAN>
- <SPAN TYPE="LITERAL3">
- <BEGIN>"</BEGIN>
- <END>"</END>
- </SPAN>
- <KEYWORDS>
-EOF
-
- for my $name (sort(keys(%keywords))) {
- my $kind = $keywords{$name};
- my $type = $keyword_types{$kind};
- if ($kind ne "minor" or $name =~ m/^[A-Za-z0-9_]+$/) {
- $name =~ s/&/&/g;
- $name =~ s/</</g;
- $name =~ s/>/</g;
- print " <${type}>${name}</${type}>\n";
- }
- }
-
- print <<'EOF';
- </KEYWORDS>
- </RULES>
-</MODE>
-EOF
-
- close OUTPUT;
- select;
- print STDERR "${target_tool}: ${file}\n";
+ print STDERR "${file}\n";
}
## main
&collect_keywords();
-eval "${target_tool}_output()";
+&emacs_output();
--- a/src/HOL/Deriv.thy Sun Nov 15 13:06:07 2009 +0100
+++ b/src/HOL/Deriv.thy Sun Nov 15 13:06:42 2009 +0100
@@ -1224,27 +1224,30 @@
(* A function with positive derivative is increasing.
A simple proof using the MVT, by Jeremy Avigad. And variants.
*)
-
lemma DERIV_pos_imp_increasing:
fixes a::real and b::real and f::"real => real"
assumes "a < b" and "\<forall>x. a \<le> x & x \<le> b --> (EX y. DERIV f x :> y & y > 0)"
shows "f a < f b"
proof (rule ccontr)
assume "~ f a < f b"
- from assms have "EX l z. a < z & z < b & DERIV f z :> l
+ have "EX l z. a < z & z < b & DERIV f z :> l
& f b - f a = (b - a) * l"
- by (metis MVT DERIV_isCont differentiableI real_less_def)
+ apply (rule MVT)
+ using assms
+ apply auto
+ apply (metis DERIV_isCont)
+ apply (metis differentiableI real_less_def)
+ done
then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
and "f b - f a = (b - a) * l"
by auto
from prems have "~(l > 0)"
- by (metis assms(1) linorder_not_le mult_le_0_iff real_le_eq_diff)
+ by (metis linorder_not_le mult_le_0_iff real_le_eq_diff)
with prems show False
by (metis DERIV_unique real_less_def)
qed
-
lemma DERIV_nonneg_imp_nonincreasing:
fixes a::real and b::real and f::"real => real"
assumes "a \<le> b" and
@@ -1258,10 +1261,11 @@
assume "a ~= b"
with assms have "EX l z. a < z & z < b & DERIV f z :> l
& f b - f a = (b - a) * l"
- apply (intro MVT)
- apply auto
- apply (metis DERIV_isCont)
- apply (metis differentiableI real_less_def)
+ apply -
+ apply (rule MVT)
+ apply auto
+ apply (metis DERIV_isCont)
+ apply (metis differentiableI real_less_def)
done
then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
and "f b - f a = (b - a) * l"
@@ -1281,7 +1285,8 @@
proof -
have "(%x. -f x) a < (%x. -f x) b"
apply (rule DERIV_pos_imp_increasing [of a b "%x. -f x"])
- apply (insert prems, auto)
+ using assms
+ apply auto
apply (metis DERIV_minus neg_0_less_iff_less)
done
thus ?thesis
@@ -1296,7 +1301,8 @@
proof -
have "(%x. -f x) a \<le> (%x. -f x) b"
apply (rule DERIV_nonneg_imp_nonincreasing [of a b "%x. -f x"])
- apply (insert prems, auto)
+ using assms
+ apply auto
apply (metis DERIV_minus neg_0_le_iff_le)
done
thus ?thesis
--- a/src/HOL/Induct/LFilter.thy Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,271 +0,0 @@
-(* Title: HOL/LList.thy
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-*)
-
-header {*The "filter" functional for coinductive lists
- --defined by a combination of induction and coinduction*}
-
-theory LFilter imports LList begin
-
-inductive_set
- findRel :: "('a => bool) => ('a llist * 'a llist)set"
- for p :: "'a => bool"
- where
- found: "p x ==> (LCons x l, LCons x l) \<in> findRel p"
- | seek: "[| ~p x; (l,l') \<in> findRel p |] ==> (LCons x l, l') \<in> findRel p"
-
-declare findRel.intros [intro]
-
-definition
- find :: "['a => bool, 'a llist] => 'a llist" where
- "find p l = (SOME l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p)))"
-
-definition
- lfilter :: "['a => bool, 'a llist] => 'a llist" where
- "lfilter p l = llist_corec l (%l. case find p l of
- LNil => None
- | LCons y z => Some(y,z))"
-
-
-subsection {* @{text findRel}: basic laws *}
-
-inductive_cases
- findRel_LConsE [elim!]: "(LCons x l, l'') \<in> findRel p"
-
-
-lemma findRel_functional [rule_format]:
- "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'"
-by (erule findRel.induct, auto)
-
-lemma findRel_imp_LCons [rule_format]:
- "(l,l'): findRel p ==> \<exists>x l''. l' = LCons x l'' & p x"
-by (erule findRel.induct, auto)
-
-lemma findRel_LNil [elim!]: "(LNil,l): findRel p ==> R"
-by (blast elim: findRel.cases)
-
-
-subsection {* Properties of @{text "Domain (findRel p)"} *}
-
-lemma LCons_Domain_findRel [simp]:
- "LCons x l \<in> Domain(findRel p) = (p x | l \<in> Domain(findRel p))"
-by auto
-
-lemma Domain_findRel_iff:
- "(l \<in> Domain (findRel p)) = (\<exists>x l'. (l, LCons x l') \<in> findRel p & p x)"
-by (blast dest: findRel_imp_LCons)
-
-lemma Domain_findRel_mono:
- "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)"
-apply clarify
-apply (erule findRel.induct, blast+)
-done
-
-
-subsection {* @{text find}: basic equations *}
-
-lemma find_LNil [simp]: "find p LNil = LNil"
-by (unfold find_def, blast)
-
-lemma findRel_imp_find [simp]: "(l,l') \<in> findRel p ==> find p l = l'"
-apply (unfold find_def)
-apply (blast dest: findRel_functional)
-done
-
-lemma find_LCons_found: "p x ==> find p (LCons x l) = LCons x l"
-by (blast intro: findRel_imp_find)
-
-lemma diverge_find_LNil [simp]: "l ~: Domain(findRel p) ==> find p l = LNil"
-by (unfold find_def, blast)
-
-lemma find_LCons_seek: "~ (p x) ==> find p (LCons x l) = find p l"
-apply (case_tac "LCons x l \<in> Domain (findRel p) ")
- apply auto
-apply (blast intro: findRel_imp_find)
-done
-
-lemma find_LCons [simp]:
- "find p (LCons x l) = (if p x then LCons x l else find p l)"
-by (simp add: find_LCons_seek find_LCons_found)
-
-
-
-subsection {* @{text lfilter}: basic equations *}
-
-lemma lfilter_LNil [simp]: "lfilter p LNil = LNil"
-by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
-
-lemma diverge_lfilter_LNil [simp]:
- "l ~: Domain(findRel p) ==> lfilter p l = LNil"
-by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
-
-lemma lfilter_LCons_found:
- "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)"
-by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
-
-lemma findRel_imp_lfilter [simp]:
- "(l, LCons x l') \<in> findRel p ==> lfilter p l = LCons x (lfilter p l')"
-by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
-
-lemma lfilter_LCons_seek: "~ (p x) ==> lfilter p (LCons x l) = lfilter p l"
-apply (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
-apply (case_tac "LCons x l \<in> Domain (findRel p) ")
- apply (simp add: Domain_findRel_iff, auto)
-done
-
-lemma lfilter_LCons [simp]:
- "lfilter p (LCons x l) =
- (if p x then LCons x (lfilter p l) else lfilter p l)"
-by (simp add: lfilter_LCons_found lfilter_LCons_seek)
-
-declare llistD_Fun_LNil_I [intro!] llistD_Fun_LCons_I [intro!]
-
-
-lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)"
-apply (auto iff: Domain_findRel_iff)
-done
-
-lemma lfilter_eq_LCons [rule_format]:
- "lfilter p l = LCons x l' -->
- (\<exists>l''. l' = lfilter p l'' & (l, LCons x l'') \<in> findRel p)"
-apply (subst lfilter_def [THEN def_llist_corec])
-apply (case_tac "l \<in> Domain (findRel p) ")
- apply (auto iff: Domain_findRel_iff)
-done
-
-
-lemma lfilter_cases: "lfilter p l = LNil |
- (\<exists>y l'. lfilter p l = LCons y (lfilter p l') & p y)"
-apply (case_tac "l \<in> Domain (findRel p) ")
-apply (auto iff: Domain_findRel_iff)
-done
-
-
-subsection {* @{text lfilter}: simple facts by coinduction *}
-
-lemma lfilter_K_True: "lfilter (%x. True) l = l"
-by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
-
-lemma lfilter_idem: "lfilter p (lfilter p l) = lfilter p l"
-apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
-apply safe
-txt{*Cases: @{text "p x"} is true or false*}
-apply (rule lfilter_cases [THEN disjE])
- apply (erule ssubst, auto)
-done
-
-
-subsection {* Numerous lemmas required to prove @{text lfilter_conj} *}
-
-lemma findRel_conj_lemma [rule_format]:
- "(l,l') \<in> findRel q
- ==> l' = LCons x l'' --> p x --> (l,l') \<in> findRel (%x. p x & q x)"
-by (erule findRel.induct, auto)
-
-lemmas findRel_conj = findRel_conj_lemma [OF _ refl]
-
-lemma findRel_not_conj_Domain [rule_format]:
- "(l,l'') \<in> findRel (%x. p x & q x)
- ==> (l, LCons x l') \<in> findRel q --> ~ p x -->
- l' \<in> Domain (findRel (%x. p x & q x))"
-by (erule findRel.induct, auto)
-
-lemma findRel_conj2 [rule_format]:
- "(l,lxx) \<in> findRel q
- ==> lxx = LCons x lx --> (lx,lz) \<in> findRel(%x. p x & q x) --> ~ p x
- --> (l,lz) \<in> findRel (%x. p x & q x)"
-by (erule findRel.induct, auto)
-
-lemma findRel_lfilter_Domain_conj [rule_format]:
- "(lx,ly) \<in> findRel p
- ==> \<forall>l. lx = lfilter q l --> l \<in> Domain (findRel(%x. p x & q x))"
-apply (erule findRel.induct)
- apply (blast dest!: sym [THEN lfilter_eq_LCons] intro: findRel_conj, auto)
-apply (drule sym [THEN lfilter_eq_LCons], auto)
-apply (drule spec)
-apply (drule refl [THEN rev_mp])
-apply (blast intro: findRel_conj2)
-done
-
-
-lemma findRel_conj_lfilter [rule_format]:
- "(l,l'') \<in> findRel(%x. p x & q x)
- ==> l'' = LCons y l' -->
- (lfilter q l, LCons y (lfilter q l')) \<in> findRel p"
-by (erule findRel.induct, auto)
-
-lemma lfilter_conj_lemma:
- "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l)
- \<in> llistD_Fun (range (%u. (lfilter p (lfilter q u),
- lfilter (%x. p x & q x) u)))"
-apply (case_tac "l \<in> Domain (findRel q)")
- apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
- prefer 3 apply (blast intro: rev_subsetD [OF _ Domain_findRel_mono])
- txt{*There are no @{text qs} in @{text l}: both lists are @{text LNil}*}
- apply (simp_all add: Domain_findRel_iff, clarify)
-txt{*case @{text "q x"}*}
-apply (case_tac "p x")
- apply (simp_all add: findRel_conj [THEN findRel_imp_lfilter])
- txt{*case @{text "q x"} and @{text "~(p x)"} *}
-apply (case_tac "l' \<in> Domain (findRel (%x. p x & q x))")
- txt{*subcase: there is no @{text "p & q"} in @{text l'} and therefore none in @{text l}*}
- apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
- prefer 3 apply (blast intro: findRel_not_conj_Domain)
- apply (subgoal_tac [2] "lfilter q l' ~: Domain (findRel p) ")
- prefer 3 apply (blast intro: findRel_lfilter_Domain_conj)
- txt{* {\dots} and therefore too, no @{text p} in @{text "lfilter q l'"}.
- Both results are @{text LNil}*}
- apply (simp_all add: Domain_findRel_iff, clarify)
-txt{*subcase: there is a @{text "p & q"} in @{text l'} and therefore also one in @{text l} *}
-apply (subgoal_tac " (l, LCons xa l'a) \<in> findRel (%x. p x & q x) ")
- prefer 2 apply (blast intro: findRel_conj2)
-apply (subgoal_tac " (lfilter q l', LCons xa (lfilter q l'a)) \<in> findRel p")
- apply simp
-apply (blast intro: findRel_conj_lfilter)
-done
-
-
-lemma lfilter_conj: "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l"
-apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
-apply (blast intro: lfilter_conj_lemma rev_subsetD [OF _ llistD_Fun_mono])
-done
-
-
-subsection {* Numerous lemmas required to prove ??:
- @{text "lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)"}
- *}
-
-lemma findRel_lmap_Domain:
- "(l,l') \<in> findRel(%x. p (f x)) ==> lmap f l \<in> Domain(findRel p)"
-by (erule findRel.induct, auto)
-
-lemma lmap_eq_LCons [rule_format]: "lmap f l = LCons x l' -->
- (\<exists>y l''. x = f y & l' = lmap f l'' & l = LCons y l'')"
-apply (subst lmap_def [THEN def_llist_corec])
-apply (rule_tac l = "l" in llistE, auto)
-done
-
-
-lemma lmap_LCons_findRel_lemma [rule_format]:
- "(lx,ly) \<in> findRel p
- ==> \<forall>l. lmap f l = lx --> ly = LCons x l' -->
- (\<exists>y l''. x = f y & l' = lmap f l'' &
- (l, LCons y l'') \<in> findRel(%x. p(f x)))"
-apply (erule findRel.induct, simp_all)
-apply (blast dest!: lmap_eq_LCons)+
-done
-
-lemmas lmap_LCons_findRel = lmap_LCons_findRel_lemma [OF _ refl refl]
-
-lemma lfilter_lmap: "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)"
-apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
-apply safe
-apply (case_tac "lmap f l \<in> Domain (findRel p)")
- apply (simp add: Domain_findRel_iff, clarify)
- apply (frule lmap_LCons_findRel, force)
-apply (subgoal_tac "l ~: Domain (findRel (%x. p (f x)))", simp)
-apply (blast intro: findRel_lmap_Domain)
-done
-
-end
--- a/src/HOL/Induct/LList.thy Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,912 +0,0 @@
-(* Title: HOL/Induct/LList.thy
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
-
-Shares NIL, CONS, List_case with List.thy
-
-Still needs flatten function -- hard because it need
-bounds on the amount of lookahead required.
-
-Could try (but would it work for the gfp analogue of term?)
- LListD_Fun_def "LListD_Fun(A) == (%Z. Id_on({Numb(0)}) <++> Id_on(A) <**> Z)"
-
-A nice but complex example would be [ML for the Working Programmer, page 176]
- from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
-
-Previous definition of llistD_Fun was explicit:
- llistD_Fun_def
- "llistD_Fun(r) ==
- {(LNil,LNil)} Un
- (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))`r)"
-*)
-
-header {*Definition of type llist by a greatest fixed point*}
-
-theory LList imports SList begin
-
-coinductive_set
- llist :: "'a item set => 'a item set"
- for A :: "'a item set"
- where
- NIL_I: "NIL \<in> llist(A)"
- | CONS_I: "[| a \<in> A; M \<in> llist(A) |] ==> CONS a M \<in> llist(A)"
-
-coinductive_set
- LListD :: "('a item * 'a item)set => ('a item * 'a item)set"
- for r :: "('a item * 'a item)set"
- where
- NIL_I: "(NIL, NIL) \<in> LListD(r)"
- | CONS_I: "[| (a,b) \<in> r; (M,N) \<in> LListD(r) |]
- ==> (CONS a M, CONS b N) \<in> LListD(r)"
-
-
-typedef (LList)
- 'a llist = "llist(range Leaf) :: 'a item set"
- by (blast intro: llist.NIL_I)
-
-definition
- list_Fun :: "['a item set, 'a item set] => 'a item set" where
- --{*Now used exclusively for abbreviating the coinduction rule*}
- "list_Fun A X = {z. z = NIL | (\<exists>M a. z = CONS a M & a \<in> A & M \<in> X)}"
-
-definition
- LListD_Fun ::
- "[('a item * 'a item)set, ('a item * 'a item)set] =>
- ('a item * 'a item)set" where
- "LListD_Fun r X =
- {z. z = (NIL, NIL) |
- (\<exists>M N a b. z = (CONS a M, CONS b N) & (a, b) \<in> r & (M, N) \<in> X)}"
-
-definition
- LNil :: "'a llist" where
- --{*abstract constructor*}
- "LNil = Abs_LList NIL"
-
-definition
- LCons :: "['a, 'a llist] => 'a llist" where
- --{*abstract constructor*}
- "LCons x xs = Abs_LList(CONS (Leaf x) (Rep_LList xs))"
-
-definition
- llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b" where
- "llist_case c d l =
- List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)"
-
-definition
- LList_corec_fun :: "[nat, 'a=> ('b item * 'a) option, 'a] => 'b item" where
- "LList_corec_fun k f ==
- nat_rec (%x. {})
- (%j r x. case f x of None => NIL
- | Some(z,w) => CONS z (r w))
- k"
-
-definition
- LList_corec :: "['a, 'a => ('b item * 'a) option] => 'b item" where
- "LList_corec a f = (\<Union>k. LList_corec_fun k f a)"
-
-definition
- llist_corec :: "['a, 'a => ('b * 'a) option] => 'b llist" where
- "llist_corec a f =
- Abs_LList(LList_corec a
- (%z. case f z of None => None
- | Some(v,w) => Some(Leaf(v), w)))"
-
-definition
- llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set" where
- "llistD_Fun(r) =
- prod_fun Abs_LList Abs_LList `
- LListD_Fun (Id_on(range Leaf))
- (prod_fun Rep_LList Rep_LList ` r)"
-
-
-
-text{* The case syntax for type @{text "'a llist"} *}
-syntax (* FIXME proper case syntax!? *)
- LNil :: logic
- LCons :: logic
-translations
- "case p of LNil => a | LCons x l => b" == "CONST llist_case a (%x l. b) p"
-
-
-subsubsection{* Sample function definitions. Item-based ones start with @{text L} *}
-
-definition
- Lmap :: "('a item => 'b item) => ('a item => 'b item)" where
- "Lmap f M = LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
-
-definition
- lmap :: "('a=>'b) => ('a llist => 'b llist)" where
- "lmap f l = llist_corec l (%z. case z of LNil => None
- | LCons y z => Some(f(y), z))"
-
-definition
- iterates :: "['a => 'a, 'a] => 'a llist" where
- "iterates f a = llist_corec a (%x. Some((x, f(x))))"
-
-definition
- Lconst :: "'a item => 'a item" where
- "Lconst(M) == lfp(%N. CONS M N)"
-
-definition
- Lappend :: "['a item, 'a item] => 'a item" where
- "Lappend M N = LList_corec (M,N)
- (split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2)))))
- (%M1 M2 N. Some((M1, (M2,N))))))"
-
-definition
- lappend :: "['a llist, 'a llist] => 'a llist" where
- "lappend l n = llist_corec (l,n)
- (split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2)))))
- (%l1 l2 n. Some((l1, (l2,n))))))"
-
-
-text{*Append generates its result by applying f, where
- f((NIL,NIL)) = None
- f((NIL, CONS N1 N2)) = Some((N1, (NIL,N2))
- f((CONS M1 M2, N)) = Some((M1, (M2,N))
-*}
-
-text{*
-SHOULD @{text LListD_Fun_CONS_I}, etc., be equations (for rewriting)?
-*}
-
-lemmas UN1_I = UNIV_I [THEN UN_I, standard]
-
-subsubsection{* Simplification *}
-
-declare option.split [split]
-
-text{*This justifies using llist in other recursive type definitions*}
-lemma llist_mono:
- assumes subset: "A \<subseteq> B"
- shows "llist A \<subseteq> llist B"
-proof
- fix x
- assume "x \<in> llist A"
- then show "x \<in> llist B"
- proof coinduct
- case llist
- then show ?case using subset
- by cases blast+
- qed
-qed
-
-
-lemma llist_unfold: "llist(A) = usum {Numb(0)} (uprod A (llist A))"
- by (fast intro!: llist.intros [unfolded NIL_def CONS_def]
- elim: llist.cases [unfolded NIL_def CONS_def])
-
-
-subsection{* Type checking by coinduction *}
-
-text {*
- {\dots} using @{text list_Fun} THE COINDUCTIVE DEFINITION PACKAGE
- COULD DO THIS!
-*}
-
-lemma llist_coinduct:
- "[| M \<in> X; X \<subseteq> list_Fun A (X Un llist(A)) |] ==> M \<in> llist(A)"
-apply (simp add: list_Fun_def)
-apply (erule llist.coinduct)
-apply (blast intro: elim:);
-done
-
-lemma list_Fun_NIL_I [iff]: "NIL \<in> list_Fun A X"
-by (simp add: list_Fun_def NIL_def)
-
-lemma list_Fun_CONS_I [intro!,simp]:
- "[| M \<in> A; N \<in> X |] ==> CONS M N \<in> list_Fun A X"
-by (simp add: list_Fun_def CONS_def)
-
-
-text{*Utilise the ``strong'' part, i.e. @{text "gfp(f)"}*}
-lemma list_Fun_llist_I: "M \<in> llist(A) ==> M \<in> list_Fun A (X Un llist(A))"
-apply (unfold list_Fun_def)
-apply (erule llist.cases)
-apply auto
-done
-
-subsection{* @{text LList_corec} satisfies the desired recurion equation *}
-
-text{*A continuity result?*}
-lemma CONS_UN1: "CONS M (\<Union>x. f(x)) = (\<Union>x. CONS M (f x))"
-apply (simp add: CONS_def In1_UN1 Scons_UN1_y)
-done
-
-lemma CONS_mono: "[| M\<subseteq>M'; N\<subseteq>N' |] ==> CONS M N \<subseteq> CONS M' N'"
-apply (simp add: CONS_def In1_mono Scons_mono)
-done
-
-declare LList_corec_fun_def [THEN def_nat_rec_0, simp]
- LList_corec_fun_def [THEN def_nat_rec_Suc, simp]
-
-
-subsubsection{* The directions of the equality are proved separately *}
-
-lemma LList_corec_subset1:
- "LList_corec a f \<subseteq>
- (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))"
-apply (unfold LList_corec_def)
-apply (rule UN_least)
-apply (case_tac k)
-apply (simp_all (no_asm_simp))
-apply (rule allI impI subset_refl [THEN CONS_mono] UNIV_I [THEN UN_upper])+
-done
-
-lemma LList_corec_subset2:
- "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) \<subseteq>
- LList_corec a f"
-apply (simp add: LList_corec_def)
-apply (simp add: CONS_UN1, safe)
-apply (rule_tac a="Suc(?k)" in UN_I, simp, simp)+
-done
-
-text{*the recursion equation for @{text LList_corec} -- NOT SUITABLE FOR REWRITING!*}
-lemma LList_corec:
- "LList_corec a f =
- (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))"
-by (rule equalityI LList_corec_subset1 LList_corec_subset2)+
-
-text{*definitional version of same*}
-lemma def_LList_corec:
- "[| !!x. h(x) = LList_corec x f |]
- ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))"
-by (simp add: LList_corec)
-
-text{*A typical use of co-induction to show membership in the @{text gfp}.
- Bisimulation is @{text "range(%x. LList_corec x f)"} *}
-lemma LList_corec_type: "LList_corec a f \<in> llist UNIV"
-apply (rule_tac X = "range (%x. LList_corec x ?g)" in llist_coinduct)
-apply (rule rangeI, safe)
-apply (subst LList_corec, simp)
-done
-
-
-subsection{* @{text llist} equality as a @{text gfp}; the bisimulation principle *}
-
-text{*This theorem is actually used, unlike the many similar ones in ZF*}
-lemma LListD_unfold: "LListD r = dsum (Id_on {Numb 0}) (dprod r (LListD r))"
- by (fast intro!: LListD.intros [unfolded NIL_def CONS_def]
- elim: LListD.cases [unfolded NIL_def CONS_def])
-
-lemma LListD_implies_ntrunc_equality [rule_format]:
- "\<forall>M N. (M,N) \<in> LListD(Id_on A) --> ntrunc k M = ntrunc k N"
-apply (induct_tac "k" rule: nat_less_induct)
-apply (safe del: equalityI)
-apply (erule LListD.cases)
-apply (safe del: equalityI)
-apply (case_tac "n", simp)
-apply (rename_tac "n'")
-apply (case_tac "n'")
-apply (simp_all add: CONS_def less_Suc_eq)
-done
-
-text{*The domain of the @{text LListD} relation*}
-lemma Domain_LListD:
- "Domain (LListD(Id_on A)) \<subseteq> llist(A)"
-apply (rule subsetI)
-apply (erule llist.coinduct)
-apply (simp add: NIL_def CONS_def)
-apply (drule_tac P = "%x. xa \<in> Domain x" in LListD_unfold [THEN subst], auto)
-done
-
-text{*This inclusion justifies the use of coinduction to show @{text "M = N"}*}
-lemma LListD_subset_Id_on: "LListD(Id_on A) \<subseteq> Id_on(llist(A))"
-apply (rule subsetI)
-apply (rule_tac p = x in PairE, safe)
-apply (rule Id_on_eqI)
-apply (rule LListD_implies_ntrunc_equality [THEN ntrunc_equality], assumption)
-apply (erule DomainI [THEN Domain_LListD [THEN subsetD]])
-done
-
-
-subsubsection{* Coinduction, using @{text LListD_Fun} *}
-
-text {* THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS! *}
-
-lemma LListD_Fun_mono: "A\<subseteq>B ==> LListD_Fun r A \<subseteq> LListD_Fun r B"
-apply (simp add: LListD_Fun_def)
-apply (assumption | rule basic_monos)+
-done
-
-lemma LListD_coinduct:
- "[| M \<in> X; X \<subseteq> LListD_Fun r (X Un LListD(r)) |] ==> M \<in> LListD(r)"
-apply (cases M)
-apply (simp add: LListD_Fun_def)
-apply (erule LListD.coinduct)
-apply (auto );
-done
-
-lemma LListD_Fun_NIL_I: "(NIL,NIL) \<in> LListD_Fun r s"
-by (simp add: LListD_Fun_def NIL_def)
-
-lemma LListD_Fun_CONS_I:
- "[| x\<in>A; (M,N):s |] ==> (CONS x M, CONS x N) \<in> LListD_Fun (Id_on A) s"
-by (simp add: LListD_Fun_def CONS_def, blast)
-
-text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*}
-lemma LListD_Fun_LListD_I:
- "M \<in> LListD(r) ==> M \<in> LListD_Fun r (X Un LListD(r))"
-apply (cases M)
-apply (simp add: LListD_Fun_def)
-apply (erule LListD.cases)
-apply auto
-done
-
-
-text{*This converse inclusion helps to strengthen @{text LList_equalityI}*}
-lemma Id_on_subset_LListD: "Id_on(llist(A)) \<subseteq> LListD(Id_on A)"
-apply (rule subsetI)
-apply (erule LListD_coinduct)
-apply (rule subsetI)
-apply (erule Id_onE)
-apply (erule ssubst)
-apply (erule llist.cases)
-apply (simp_all add: Id_onI LListD_Fun_NIL_I LListD_Fun_CONS_I)
-done
-
-lemma LListD_eq_Id_on: "LListD(Id_on A) = Id_on(llist(A))"
-apply (rule equalityI LListD_subset_Id_on Id_on_subset_LListD)+
-done
-
-lemma LListD_Fun_Id_on_I: "M \<in> llist(A) ==> (M,M) \<in> LListD_Fun (Id_on A) (X Un Id_on(llist(A)))"
-apply (rule LListD_eq_Id_on [THEN subst])
-apply (rule LListD_Fun_LListD_I)
-apply (simp add: LListD_eq_Id_on Id_onI)
-done
-
-
-subsubsection{* To show two LLists are equal, exhibit a bisimulation!
- [also admits true equality]
- Replace @{text A} by some particular set, like @{text "{x. True}"}??? *}
-lemma LList_equalityI:
- "[| (M,N) \<in> r; r \<subseteq> LListD_Fun (Id_on A) (r Un Id_on(llist(A))) |]
- ==> M=N"
-apply (rule LListD_subset_Id_on [THEN subsetD, THEN Id_onE])
-apply (erule LListD_coinduct)
-apply (simp add: LListD_eq_Id_on, safe)
-done
-
-
-subsection{* Finality of @{text "llist(A)"}: Uniqueness of functions defined by corecursion *}
-
-text{*We must remove @{text Pair_eq} because it may turn an instance of reflexivity
- @{text "(h1 b, h2 b) = (h1 ?x17, h2 ?x17)"} into a conjunction!
- (or strengthen the Solver?)
-*}
-declare Pair_eq [simp del]
-
-text{*abstract proof using a bisimulation*}
-lemma LList_corec_unique:
- "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));
- !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]
- ==> h1=h2"
-apply (rule ext)
-txt{*next step avoids an unknown (and flexflex pair) in simplification*}
-apply (rule_tac A = UNIV and r = "range(%u. (h1 u, h2 u))"
- in LList_equalityI)
-apply (rule rangeI, safe)
-apply (simp add: LListD_Fun_NIL_I UNIV_I [THEN LListD_Fun_CONS_I])
-done
-
-lemma equals_LList_corec:
- "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |]
- ==> h = (%x. LList_corec x f)"
-by (simp add: LList_corec_unique LList_corec)
-
-
-subsubsection{*Obsolete proof of @{text LList_corec_unique}:
- complete induction, not coinduction *}
-
-lemma ntrunc_one_CONS [simp]: "ntrunc (Suc 0) (CONS M N) = {}"
-by (simp add: CONS_def ntrunc_one_In1)
-
-lemma ntrunc_CONS [simp]:
- "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)"
-by (simp add: CONS_def)
-
-
-lemma
- assumes prem1:
- "!!x. h1 x = (case f x of None => NIL | Some(z,w) => CONS z (h1 w))"
- and prem2:
- "!!x. h2 x = (case f x of None => NIL | Some(z,w) => CONS z (h2 w))"
- shows "h1=h2"
-apply (rule ntrunc_equality [THEN ext])
-apply (rule_tac x = x in spec)
-apply (induct_tac "k" rule: nat_less_induct)
-apply (rename_tac "n")
-apply (rule allI)
-apply (subst prem1)
-apply (subst prem2, simp)
-apply (intro strip)
-apply (case_tac "n")
-apply (rename_tac [2] "m")
-apply (case_tac [2] "m", simp_all)
-done
-
-
-subsection{*Lconst: defined directly by @{text lfp} *}
-
-text{*But it could be defined by corecursion.*}
-
-lemma Lconst_fun_mono: "mono(CONS(M))"
-apply (rule monoI subset_refl CONS_mono)+
-apply assumption
-done
-
-text{* @{text "Lconst(M) = CONS M (Lconst M)"} *}
-lemmas Lconst = Lconst_fun_mono [THEN Lconst_def [THEN def_lfp_unfold]]
-
-text{*A typical use of co-induction to show membership in the gfp.
- The containing set is simply the singleton @{text "{Lconst(M)}"}. *}
-lemma Lconst_type: "M\<in>A ==> Lconst(M): llist(A)"
-apply (rule singletonI [THEN llist_coinduct], safe)
-apply (rule_tac P = "%u. u \<in> ?A" in Lconst [THEN ssubst])
-apply (assumption | rule list_Fun_CONS_I singletonI UnI1)+
-done
-
-lemma Lconst_eq_LList_corec: "Lconst(M) = LList_corec M (%x. Some(x,x))"
-apply (rule equals_LList_corec [THEN fun_cong], simp)
-apply (rule Lconst)
-done
-
-text{*Thus we could have used gfp in the definition of Lconst*}
-lemma gfp_Lconst_eq_LList_corec: "gfp(%N. CONS M N) = LList_corec M (%x. Some(x,x))"
-apply (rule equals_LList_corec [THEN fun_cong], simp)
-apply (rule Lconst_fun_mono [THEN gfp_unfold])
-done
-
-
-subsection{* Isomorphisms *}
-
-lemma LListI: "x \<in> llist (range Leaf) ==> x \<in> LList"
-by (simp add: LList_def)
-
-lemma LListD: "x \<in> LList ==> x \<in> llist (range Leaf)"
-by (simp add: LList_def)
-
-
-subsubsection{* Distinctness of constructors *}
-
-lemma LCons_not_LNil [iff]: "~ LCons x xs = LNil"
-apply (simp add: LNil_def LCons_def)
-apply (subst Abs_LList_inject)
-apply (rule llist.intros CONS_not_NIL rangeI LListI Rep_LList [THEN LListD])+
-done
-
-lemmas LNil_not_LCons [iff] = LCons_not_LNil [THEN not_sym, standard]
-
-
-subsubsection{* llist constructors *}
-
-lemma Rep_LList_LNil: "Rep_LList LNil = NIL"
-apply (simp add: LNil_def)
-apply (rule llist.NIL_I [THEN LListI, THEN Abs_LList_inverse])
-done
-
-lemma Rep_LList_LCons: "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)"
-apply (simp add: LCons_def)
-apply (rule llist.CONS_I [THEN LListI, THEN Abs_LList_inverse]
- rangeI Rep_LList [THEN LListD])+
-done
-
-subsubsection{* Injectiveness of @{text CONS} and @{text LCons} *}
-
-lemma CONS_CONS_eq2: "(CONS M N=CONS M' N') = (M=M' & N=N')"
-apply (simp add: CONS_def)
-done
-
-lemmas CONS_inject = CONS_CONS_eq [THEN iffD1, THEN conjE, standard]
-
-
-text{*For reasoning about abstract llist constructors*}
-
-declare Rep_LList [THEN LListD, intro] LListI [intro]
-declare llist.intros [intro]
-
-lemma LCons_LCons_eq [iff]: "(LCons x xs=LCons y ys) = (x=y & xs=ys)"
-apply (simp add: LCons_def)
-apply (subst Abs_LList_inject)
-apply (auto simp add: Rep_LList_inject)
-done
-
-lemma CONS_D2: "CONS M N \<in> llist(A) ==> M \<in> A & N \<in> llist(A)"
-apply (erule llist.cases)
-apply (erule CONS_neq_NIL, fast)
-done
-
-
-subsection{* Reasoning about @{text "llist(A)"} *}
-
-text{*A special case of @{text list_equality} for functions over lazy lists*}
-lemma LList_fun_equalityI:
- "[| M \<in> llist(A); g(NIL): llist(A);
- f(NIL)=g(NIL);
- !!x l. [| x\<in>A; l \<in> llist(A) |] ==>
- (f(CONS x l),g(CONS x l)) \<in>
- LListD_Fun (Id_on A) ((%u.(f(u),g(u)))`llist(A) Un
- Id_on(llist(A)))
- |] ==> f(M) = g(M)"
-apply (rule LList_equalityI)
-apply (erule imageI)
-apply (rule image_subsetI)
-apply (erule_tac a=x in llist.cases)
-apply (erule ssubst, erule ssubst, erule LListD_Fun_Id_on_I, blast)
-done
-
-
-subsection{* The functional @{text Lmap} *}
-
-lemma Lmap_NIL [simp]: "Lmap f NIL = NIL"
-by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp)
-
-lemma Lmap_CONS [simp]: "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"
-by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp)
-
-
-
-text{*Another type-checking proof by coinduction*}
-lemma Lmap_type:
- "[| M \<in> llist(A); !!x. x\<in>A ==> f(x):B |] ==> Lmap f M \<in> llist(B)"
-apply (erule imageI [THEN llist_coinduct], safe)
-apply (erule llist.cases, simp_all)
-done
-
-text{*This type checking rule synthesises a sufficiently large set for @{text f}*}
-lemma Lmap_type2: "M \<in> llist(A) ==> Lmap f M \<in> llist(f`A)"
-apply (erule Lmap_type)
-apply (erule imageI)
-done
-
-subsubsection{* Two easy results about @{text Lmap} *}
-
-lemma Lmap_compose: "M \<in> llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)"
-apply (simp add: o_def)
-apply (drule imageI)
-apply (erule LList_equalityI, safe)
-apply (erule llist.cases, simp_all)
-apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ f])+
-apply assumption
-done
-
-lemma Lmap_ident: "M \<in> llist(A) ==> Lmap (%x. x) M = M"
-apply (drule imageI)
-apply (erule LList_equalityI, safe)
-apply (erule llist.cases, simp_all)
-apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ "%x. x"])+
-apply assumption
-done
-
-
-subsection{* @{text Lappend} -- its two arguments cause some complications! *}
-
-lemma Lappend_NIL_NIL [simp]: "Lappend NIL NIL = NIL"
-apply (simp add: Lappend_def)
-apply (rule LList_corec [THEN trans], simp)
-done
-
-lemma Lappend_NIL_CONS [simp]:
- "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"
-apply (simp add: Lappend_def)
-apply (rule LList_corec [THEN trans], simp)
-done
-
-lemma Lappend_CONS [simp]:
- "Lappend (CONS M M') N = CONS M (Lappend M' N)"
-apply (simp add: Lappend_def)
-apply (rule LList_corec [THEN trans], simp)
-done
-
-declare llist.intros [simp] LListD_Fun_CONS_I [simp]
- range_eqI [simp] image_eqI [simp]
-
-
-lemma Lappend_NIL [simp]: "M \<in> llist(A) ==> Lappend NIL M = M"
-by (erule LList_fun_equalityI, simp_all)
-
-lemma Lappend_NIL2: "M \<in> llist(A) ==> Lappend M NIL = M"
-by (erule LList_fun_equalityI, simp_all)
-
-
-subsubsection{* Alternative type-checking proofs for @{text Lappend} *}
-
-text{*weak co-induction: bisimulation and case analysis on both variables*}
-lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
-apply (rule_tac X = "\<Union>u\<in>llist (A) . \<Union>v \<in> llist (A) . {Lappend u v}" in llist_coinduct)
-apply fast
-apply safe
-apply (erule_tac a = u in llist.cases)
-apply (erule_tac a = v in llist.cases, simp_all, blast)
-done
-
-text{*strong co-induction: bisimulation and case analysis on one variable*}
-lemma Lappend_type': "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
-apply (rule_tac X = "(%u. Lappend u N) `llist (A)" in llist_coinduct)
-apply (erule imageI)
-apply (rule image_subsetI)
-apply (erule_tac a = x in llist.cases)
-apply (simp add: list_Fun_llist_I, simp)
-done
-
-subsection{* Lazy lists as the type @{text "'a llist"} -- strongly typed versions of above *}
-
-subsubsection{* @{text llist_case}: case analysis for @{text "'a llist"} *}
-
-declare LListI [THEN Abs_LList_inverse, simp]
-declare Rep_LList_inverse [simp]
-declare Rep_LList [THEN LListD, simp]
-declare rangeI [simp] inj_Leaf [simp]
-
-lemma llist_case_LNil [simp]: "llist_case c d LNil = c"
-by (simp add: llist_case_def LNil_def)
-
-lemma llist_case_LCons [simp]: "llist_case c d (LCons M N) = d M N"
-by (simp add: llist_case_def LCons_def)
-
-
-text{*Elimination is case analysis, not induction.*}
-lemma llistE: "[| l=LNil ==> P; !!x l'. l=LCons x l' ==> P |] ==> P"
-apply (rule Rep_LList [THEN LListD, THEN llist.cases])
- apply (simp add: Rep_LList_LNil [symmetric] Rep_LList_inject, blast)
-apply (erule LListI [THEN Rep_LList_cases], clarify)
-apply (simp add: Rep_LList_LCons [symmetric] Rep_LList_inject, blast)
-done
-
-subsubsection{* @{text llist_corec}: corecursion for @{text "'a llist"} *}
-
-text{*Lemma for the proof of @{text llist_corec}*}
-lemma LList_corec_type2:
- "LList_corec a
- (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w))
- \<in> llist(range Leaf)"
-apply (rule_tac X = "range (%x. LList_corec x ?g)" in llist_coinduct)
-apply (rule rangeI, safe)
-apply (subst LList_corec, force)
-done
-
-lemma llist_corec [nitpick_simp]:
- "llist_corec a f =
- (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))"
-apply (unfold llist_corec_def LNil_def LCons_def)
-apply (subst LList_corec)
-apply (case_tac "f a")
-apply (simp add: LList_corec_type2)
-apply (force simp add: LList_corec_type2)
-done
-
-text{*definitional version of same*}
-lemma def_llist_corec:
- "[| !!x. h(x) = llist_corec x f |] ==>
- h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))"
-by (simp add: llist_corec)
-
-subsection{* Proofs about type @{text "'a llist"} functions *}
-
-subsection{* Deriving @{text llist_equalityI} -- @{text llist} equality is a bisimulation *}
-
-lemma LListD_Fun_subset_Times_llist:
- "r \<subseteq> (llist A) <*> (llist A)
- ==> LListD_Fun (Id_on A) r \<subseteq> (llist A) <*> (llist A)"
-by (auto simp add: LListD_Fun_def)
-
-lemma subset_Times_llist:
- "prod_fun Rep_LList Rep_LList ` r \<subseteq>
- (llist(range Leaf)) <*> (llist(range Leaf))"
-by (blast intro: Rep_LList [THEN LListD])
-
-lemma prod_fun_lemma:
- "r \<subseteq> (llist(range Leaf)) <*> (llist(range Leaf))
- ==> prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r \<subseteq> r"
-apply safe
-apply (erule subsetD [THEN SigmaE2], assumption)
-apply (simp add: LListI [THEN Abs_LList_inverse])
-done
-
-lemma prod_fun_range_eq_Id_on:
- "prod_fun Rep_LList Rep_LList ` range(%x. (x, x)) =
- Id_on(llist(range Leaf))"
-apply (rule equalityI, blast)
-apply (fast elim: LListI [THEN Abs_LList_inverse, THEN subst])
-done
-
-text{*Used with @{text lfilter}*}
-lemma llistD_Fun_mono:
- "A\<subseteq>B ==> llistD_Fun A \<subseteq> llistD_Fun B"
-apply (simp add: llistD_Fun_def prod_fun_def, auto)
-apply (rule image_eqI)
- prefer 2 apply (blast intro: rev_subsetD [OF _ LListD_Fun_mono], force)
-done
-
-subsubsection{* To show two llists are equal, exhibit a bisimulation!
- [also admits true equality] *}
-lemma llist_equalityI:
- "[| (l1,l2) \<in> r; r \<subseteq> llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2"
-apply (simp add: llistD_Fun_def)
-apply (rule Rep_LList_inject [THEN iffD1])
-apply (rule_tac r = "prod_fun Rep_LList Rep_LList `r" and A = "range (Leaf)" in LList_equalityI)
-apply (erule prod_fun_imageI)
-apply (erule image_mono [THEN subset_trans])
-apply (rule image_compose [THEN subst])
-apply (rule prod_fun_compose [THEN subst])
-apply (subst image_Un)
-apply (subst prod_fun_range_eq_Id_on)
-apply (rule LListD_Fun_subset_Times_llist [THEN prod_fun_lemma])
-apply (rule subset_Times_llist [THEN Un_least])
-apply (rule Id_on_subset_Times)
-done
-
-subsubsection{* Rules to prove the 2nd premise of @{text llist_equalityI} *}
-lemma llistD_Fun_LNil_I [simp]: "(LNil,LNil) \<in> llistD_Fun(r)"
-apply (simp add: llistD_Fun_def LNil_def)
-apply (rule LListD_Fun_NIL_I [THEN prod_fun_imageI])
-done
-
-lemma llistD_Fun_LCons_I [simp]:
- "(l1,l2):r ==> (LCons x l1, LCons x l2) \<in> llistD_Fun(r)"
-apply (simp add: llistD_Fun_def LCons_def)
-apply (rule rangeI [THEN LListD_Fun_CONS_I, THEN prod_fun_imageI])
-apply (erule prod_fun_imageI)
-done
-
-text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*}
-lemma llistD_Fun_range_I: "(l,l) \<in> llistD_Fun(r Un range(%x.(x,x)))"
-apply (simp add: llistD_Fun_def)
-apply (rule Rep_LList_inverse [THEN subst])
-apply (rule prod_fun_imageI)
-apply (subst image_Un)
-apply (subst prod_fun_range_eq_Id_on)
-apply (rule Rep_LList [THEN LListD, THEN LListD_Fun_Id_on_I])
-done
-
-text{*A special case of @{text list_equality} for functions over lazy lists*}
-lemma llist_fun_equalityI:
- "[| f(LNil)=g(LNil);
- !!x l. (f(LCons x l),g(LCons x l))
- \<in> llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))
- |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)"
-apply (rule_tac r = "range (%u. (f (u),g (u)))" in llist_equalityI)
-apply (rule rangeI, clarify)
-apply (rule_tac l = u in llistE)
-apply (simp_all add: llistD_Fun_range_I)
-done
-
-
-subsection{* The functional @{text lmap} *}
-
-lemma lmap_LNil [simp, nitpick_simp]: "lmap f LNil = LNil"
-by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
-
-lemma lmap_LCons [simp, nitpick_simp]:
-"lmap f (LCons M N) = LCons (f M) (lmap f N)"
-by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
-
-
-subsubsection{* Two easy results about @{text lmap} *}
-
-lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
-by (rule_tac l = l in llist_fun_equalityI, simp_all)
-
-lemma lmap_ident [simp]: "lmap (%x. x) l = l"
-by (rule_tac l = l in llist_fun_equalityI, simp_all)
-
-
-subsection{* iterates -- @{text llist_fun_equalityI} cannot be used! *}
-
-lemma iterates [nitpick_simp]: "iterates f x = LCons x (iterates f (f x))"
-by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
-
-lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)"
-apply (rule_tac r = "range (%u. (lmap f (iterates f u),iterates f (f u)))" in llist_equalityI)
-apply (rule rangeI, safe)
-apply (rule_tac x1 = "f (u)" in iterates [THEN ssubst])
-apply (rule_tac x1 = u in iterates [THEN ssubst], simp)
-done
-
-lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))"
-apply (subst lmap_iterates)
-apply (rule iterates)
-done
-
-subsection{* A rather complex proof about iterates -- cf Andy Pitts *}
-
-subsubsection{* Two lemmas about @{text "natrec n x (%m. g)"}, which is essentially
- @{text "(g^n)(x)"} *}
-
-lemma fun_power_lmap: "nat_rec (LCons b l) (%m. lmap(f)) n =
- LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)"
-by (induct_tac "n", simp_all)
-
-lemma fun_power_Suc: "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)"
-by (induct_tac "n", simp_all)
-
-lemmas Pair_cong = refl [THEN cong, THEN cong, of concl: Pair]
-
-
-text{*The bisimulation consists of @{text "{(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}"}
- for all @{text u} and all @{text "n::nat"}.*}
-lemma iterates_equality:
- "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)"
-apply (rule ext)
-apply (rule_tac
- r = "\<Union>u. range (%n. (nat_rec (h u) (%m y. lmap f y) n,
- nat_rec (iterates f u) (%m y. lmap f y) n))"
- in llist_equalityI)
-apply (rule UN1_I range_eqI Pair_cong nat_rec_0 [symmetric])+
-apply clarify
-apply (subst iterates, atomize)
-apply (drule_tac x=u in spec)
-apply (erule ssubst)
-apply (subst fun_power_lmap)
-apply (subst fun_power_lmap)
-apply (rule llistD_Fun_LCons_I)
-apply (rule lmap_iterates [THEN subst])
-apply (subst fun_power_Suc)
-apply (subst fun_power_Suc, blast)
-done
-
-
-subsection{* @{text lappend} -- its two arguments cause some complications! *}
-
-lemma lappend_LNil_LNil [simp, nitpick_simp]: "lappend LNil LNil = LNil"
-apply (simp add: lappend_def)
-apply (rule llist_corec [THEN trans], simp)
-done
-
-lemma lappend_LNil_LCons [simp, nitpick_simp]:
- "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
-apply (simp add: lappend_def)
-apply (rule llist_corec [THEN trans], simp)
-done
-
-lemma lappend_LCons [simp, nitpick_simp]:
- "lappend (LCons l l') N = LCons l (lappend l' N)"
-apply (simp add: lappend_def)
-apply (rule llist_corec [THEN trans], simp)
-done
-
-lemma lappend_LNil [simp]: "lappend LNil l = l"
-by (rule_tac l = l in llist_fun_equalityI, simp_all)
-
-lemma lappend_LNil2 [simp]: "lappend l LNil = l"
-by (rule_tac l = l in llist_fun_equalityI, simp_all)
-
-
-text{*The infinite first argument blocks the second*}
-lemma lappend_iterates [simp]: "lappend (iterates f x) N = iterates f x"
-apply (rule_tac r = "range (%u. (lappend (iterates f u) N,iterates f u))"
- in llist_equalityI)
- apply (rule rangeI, safe)
-apply (subst (1 2) iterates)
-apply simp
-done
-
-subsubsection{* Two proofs that @{text lmap} distributes over lappend *}
-
-text{*Long proof requiring case analysis on both both arguments*}
-lemma lmap_lappend_distrib:
- "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
-apply (rule_tac r = "\<Union>n. range (%l. (lmap f (lappend l n),
- lappend (lmap f l) (lmap f n)))"
- in llist_equalityI)
-apply (rule UN1_I)
-apply (rule rangeI, safe)
-apply (rule_tac l = l in llistE)
-apply (rule_tac l = n in llistE, simp_all)
-apply (blast intro: llistD_Fun_LCons_I)
-done
-
-text{*Shorter proof of theorem above using @{text llist_equalityI} as strong coinduction*}
-lemma lmap_lappend_distrib':
- "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
-by (rule_tac l = l in llist_fun_equalityI, auto)
-
-text{*Without strong coinduction, three case analyses might be needed*}
-lemma lappend_assoc': "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
-by (rule_tac l = l1 in llist_fun_equalityI, auto)
-
-setup {*
- Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
- (map dest_Const [@{term LNil}, @{term LCons}])
-*}
-
-end
--- a/src/HOL/Induct/README.html Sun Nov 15 13:06:07 2009 +0100
+++ b/src/HOL/Induct/README.html Sun Nov 15 13:06:42 2009 +0100
@@ -32,9 +32,6 @@
HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz">paper
available</A>).
-<LI><KBD>LFilter</KBD> is an inductive/corecursive formalization of the
-<EM>filter</EM> functional for infinite streams.
-
<LI><KBD>Exp</KBD> demonstrates the use of iterated inductive definitions to
reason about mutually recursive relations.
</UL>
--- a/src/HOL/Induct/ROOT.ML Sun Nov 15 13:06:07 2009 +0100
+++ b/src/HOL/Induct/ROOT.ML Sun Nov 15 13:06:42 2009 +0100
@@ -2,5 +2,4 @@
use_thys ["Common_Patterns"];
use_thys ["QuoDataType", "QuoNestedDataType", "Term",
- "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
- "SList", "LFilter", "Com"];
+ "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"];
--- a/src/HOL/Induct/SList.thy Sun Nov 15 13:06:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1037 +0,0 @@
-(* Title: SList.thy
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Author: B. Wolff, University of Bremen
-
-Enriched theory of lists; mutual indirect recursive data-types.
-
-Definition of type 'a list (strict lists) by a least fixed point
-
-We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
-and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
-
-so that list can serve as a "functor" for defining other recursive types.
-
-This enables the conservative construction of mutual recursive data-types
-such as
-
-datatype 'a m = Node 'a * ('a m) list
-
-Tidied by lcp. Still needs removal of nat_rec.
-*)
-
-header {* Extended List Theory (old) *}
-
-theory SList
-imports Sexp
-begin
-
-(*Hilbert_Choice is needed for the function "inv"*)
-
-(* *********************************************************************** *)
-(* *)
-(* Building up data type *)
-(* *)
-(* *********************************************************************** *)
-
-
-(* Defining the Concrete Constructors *)
-definition
- NIL :: "'a item" where
- "NIL = In0(Numb(0))"
-
-definition
- CONS :: "['a item, 'a item] => 'a item" where
- "CONS M N = In1(Scons M N)"
-
-inductive_set
- list :: "'a item set => 'a item set"
- for A :: "'a item set"
- where
- NIL_I: "NIL: list A"
- | CONS_I: "[| a: A; M: list A |] ==> CONS a M : list A"
-
-
-typedef (List)
- 'a list = "list(range Leaf) :: 'a item set"
- by (blast intro: list.NIL_I)
-
-abbreviation "Case == Datatype.Case"
-abbreviation "Split == Datatype.Split"
-
-definition
- List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b" where
- "List_case c d = Case(%x. c)(Split(d))"
-
-definition
- List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b" where
- "List_rec M c d = wfrec (pred_sexp^+)
- (%g. List_case c (%x y. d x y (g y))) M"
-
-
-(* *********************************************************************** *)
-(* *)
-(* Abstracting data type *)
-(* *)
-(* *********************************************************************** *)
-
-(*Declaring the abstract list constructors*)
-
-no_translations
- "[x, xs]" == "x#[xs]"
- "[x]" == "x#[]"
-no_notation
- Nil ("[]") and
- Cons (infixr "#" 65)
-
-definition
- Nil :: "'a list" ("[]") where
- "Nil = Abs_List(NIL)"
-
-definition
- "Cons" :: "['a, 'a list] => 'a list" (infixr "#" 65) where
- "x#xs = Abs_List(CONS (Leaf x)(Rep_List xs))"
-
-definition
- (* list Recursion -- the trancl is Essential; see list.ML *)
- list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b" where
- "list_rec l c d =
- List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
-
-definition
- list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b" where
- "list_case a f xs = list_rec xs a (%x xs r. f x xs)"
-
-(* list Enumeration *)
-translations
- "[x, xs]" == "x#[xs]"
- "[x]" == "x#[]"
-
- "case xs of [] => a | y#ys => b" == "CONST list_case(a, %y ys. b, xs)"
-
-
-(* *********************************************************************** *)
-(* *)
-(* Generalized Map Functionals *)
-(* *)
-(* *********************************************************************** *)
-
-
-(* Generalized Map Functionals *)
-
-definition
- Rep_map :: "('b => 'a item) => ('b list => 'a item)" where
- "Rep_map f xs = list_rec xs NIL(%x l r. CONS(f x) r)"
-
-definition
- Abs_map :: "('a item => 'b) => 'a item => 'b list" where
- "Abs_map g M = List_rec M Nil (%N L r. g(N)#r)"
-
-
-(**** Function definitions ****)
-
-definition
- null :: "'a list => bool" where
- "null xs = list_rec xs True (%x xs r. False)"
-
-definition
- hd :: "'a list => 'a" where
- "hd xs = list_rec xs (@x. True) (%x xs r. x)"
-
-definition
- tl :: "'a list => 'a list" where
- "tl xs = list_rec xs (@xs. True) (%x xs r. xs)"
-
-definition
- (* a total version of tl: *)
- ttl :: "'a list => 'a list" where
- "ttl xs = list_rec xs [] (%x xs r. xs)"
-
-no_notation member (infixl "mem" 55)
-
-definition
- member :: "['a, 'a list] => bool" (infixl "mem" 55) where
- "x mem xs = list_rec xs False (%y ys r. if y=x then True else r)"
-
-definition
- list_all :: "('a => bool) => ('a list => bool)" where
- "list_all P xs = list_rec xs True(%x l r. P(x) & r)"
-
-definition
- map :: "('a=>'b) => ('a list => 'b list)" where
- "map f xs = list_rec xs [] (%x l r. f(x)#r)"
-
-no_notation append (infixr "@" 65)
-
-definition
- append :: "['a list, 'a list] => 'a list" (infixr "@" 65) where
- "xs@ys = list_rec xs ys (%x l r. x#r)"
-
-definition
- filter :: "['a => bool, 'a list] => 'a list" where
- "filter P xs = list_rec xs [] (%x xs r. if P(x)then x#r else r)"
-
-definition
- foldl :: "[['b,'a] => 'b, 'b, 'a list] => 'b" where
- "foldl f a xs = list_rec xs (%a. a)(%x xs r.%a. r(f a x))(a)"
-
-definition
- foldr :: "[['a,'b] => 'b, 'b, 'a list] => 'b" where
- "foldr f a xs = list_rec xs a (%x xs r. (f x r))"
-
-definition
- length :: "'a list => nat" where
- "length xs = list_rec xs 0 (%x xs r. Suc r)"
-
-definition
- drop :: "['a list,nat] => 'a list" where
- "drop t n = (nat_rec(%x. x)(%m r xs. r(ttl xs)))(n)(t)"
-
-definition
- copy :: "['a, nat] => 'a list" where (* make list of n copies of x *)
- "copy t = nat_rec [] (%m xs. t # xs)"
-
-definition
- flat :: "'a list list => 'a list" where
- "flat = foldr (op @) []"
-
-definition
- nth :: "[nat, 'a list] => 'a" where
- "nth = nat_rec hd (%m r xs. r(tl xs))"
-
-definition
- rev :: "'a list => 'a list" where
- "rev xs = list_rec xs [] (%x xs xsa. xsa @ [x])"
-
-(* miscellaneous definitions *)
-definition
- zipWith :: "['a * 'b => 'c, 'a list * 'b list] => 'c list" where
- "zipWith f S = (list_rec (fst S) (%T.[])
- (%x xs r. %T. if null T then []
- else f(x,hd T) # r(tl T)))(snd(S))"
-
-definition
- zip :: "'a list * 'b list => ('a*'b) list" where
- "zip = zipWith (%s. s)"
-
-definition
- unzip :: "('a*'b) list => ('a list * 'b list)" where
- "unzip = foldr(% (a,b)(c,d).(a#c,b#d))([],[])"
-
-
-consts take :: "['a list,nat] => 'a list"
-primrec
- take_0: "take xs 0 = []"
- take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"
-
-consts enum :: "[nat,nat] => nat list"
-primrec
- enum_0: "enum i 0 = []"
- enum_Suc: "enum i (Suc j) = (if i <= j then enum i j @ [j] else [])"
-
-
-no_translations
- "[x\<leftarrow>xs . P]" == "filter (%x. P) xs"
-
-syntax
- (* Special syntax for list_all and filter *)
- "@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
-
-translations
- "[x\<leftarrow>xs. P]" == "CONST filter(%x. P) xs"
- "Alls x:xs. P" == "CONST list_all(%x. P)xs"
-
-
-lemma ListI: "x : list (range Leaf) ==> x : List"
-by (simp add: List_def)
-
-lemma ListD: "x : List ==> x : list (range Leaf)"
-by (simp add: List_def)
-
-lemma list_unfold: "list(A) = usum {Numb(0)} (uprod A (list(A)))"
- by (fast intro!: list.intros [unfolded NIL_def CONS_def]
- elim: list.cases [unfolded NIL_def CONS_def])
-
-(*This justifies using list in other recursive type definitions*)
-lemma list_mono: "A<=B ==> list(A) <= list(B)"
-apply (rule subsetI)
-apply (erule list.induct)
-apply (auto intro!: list.intros)
-done
-
-(*Type checking -- list creates well-founded sets*)
-lemma list_sexp: "list(sexp) <= sexp"
-apply (rule subsetI)
-apply (erule list.induct)
-apply (unfold NIL_def CONS_def)
-apply (auto intro: sexp.intros sexp_In0I sexp_In1I)
-done
-
-(* A <= sexp ==> list(A) <= sexp *)
-lemmas list_subset_sexp = subset_trans [OF list_mono list_sexp]
-
-
-(*Induction for the type 'a list *)
-lemma list_induct:
- "[| P(Nil);
- !!x xs. P(xs) ==> P(x # xs) |] ==> P(l)"
-apply (unfold Nil_def Cons_def)
-apply (rule Rep_List_inverse [THEN subst])
-(*types force good instantiation*)
-apply (rule Rep_List [unfolded List_def, THEN list.induct], simp)
-apply (erule Abs_List_inverse [unfolded List_def, THEN subst], blast)
-done
-
-
-(*** Isomorphisms ***)
-
-lemma inj_on_Abs_list: "inj_on Abs_List (list(range Leaf))"
-apply (rule inj_on_inverseI)
-apply (erule Abs_List_inverse [unfolded List_def])
-done
-
-(** Distinctness of constructors **)
-
-lemma CONS_not_NIL [iff]: "CONS M N ~= NIL"
-by (simp add: NIL_def CONS_def)
-
-lemmas NIL_not_CONS [iff] = CONS_not_NIL [THEN not_sym]
-lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE, standard]
-lemmas NIL_neq_CONS = sym [THEN CONS_neq_NIL]
-
-lemma Cons_not_Nil [iff]: "x # xs ~= Nil"
-apply (unfold Nil_def Cons_def)
-apply (rule CONS_not_NIL [THEN inj_on_Abs_list [THEN inj_on_contraD]])
-apply (simp_all add: list.intros rangeI Rep_List [unfolded List_def])
-done
-
-lemmas Nil_not_Cons [iff] = Cons_not_Nil [THEN not_sym, standard]
-lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE, standard]
-lemmas Nil_neq_Cons = sym [THEN Cons_neq_Nil]
-
-(** Injectiveness of CONS and Cons **)
-
-lemma CONS_CONS_eq [iff]: "(CONS K M)=(CONS L N) = (K=L & M=N)"
-by (simp add: CONS_def)
-
-(*For reasoning about abstract list constructors*)
-declare Rep_List [THEN ListD, intro] ListI [intro]
-declare list.intros [intro,simp]
-declare Leaf_inject [dest!]
-
-lemma Cons_Cons_eq [iff]: "(x#xs=y#ys) = (x=y & xs=ys)"
-apply (simp add: Cons_def)
-apply (subst Abs_List_inject)
-apply (auto simp add: Rep_List_inject)
-done
-
-lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard]
-
-lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
- by (induct L == "CONS M N" set: list) auto
-
-lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
-apply (simp add: CONS_def In1_def)
-apply (fast dest!: Scons_D)
-done
-
-
-(*Reasoning about constructors and their freeness*)
-
-
-lemma not_CONS_self: "N: list(A) ==> !M. N ~= CONS M N"
-apply (erule list.induct) apply simp_all done
-
-lemma not_Cons_self2: "\<forall>x. l ~= x#l"
-by (induct l rule: list_induct) simp_all
-
-
-lemma neq_Nil_conv2: "(xs ~= []) = (\<exists>y ys. xs = y#ys)"
-by (induct xs rule: list_induct) auto
-
-(** Conversion rules for List_case: case analysis operator **)
-
-lemma List_case_NIL [simp]: "List_case c h NIL = c"
-by (simp add: List_case_def NIL_def)
-
-lemma List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
-by (simp add: List_case_def CONS_def)
-
-
-(*** List_rec -- by wf recursion on pred_sexp ***)
-
-(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
- hold if pred_sexp^+ were changed to pred_sexp. *)
-
-lemma List_rec_unfold_lemma:
- "(%M. List_rec M c d) ==
- wfrec (pred_sexp^+) (%g. List_case c (%x y. d x y (g y)))"
-by (simp add: List_rec_def)
-
-lemmas List_rec_unfold =
- def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl],
- standard]
-
-
-(** pred_sexp lemmas **)
-
-lemma pred_sexp_CONS_I1:
- "[| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+"
-by (simp add: CONS_def In1_def)
-
-lemma pred_sexp_CONS_I2:
- "[| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+"
-by (simp add: CONS_def In1_def)
-
-lemma pred_sexp_CONS_D:
- "(CONS M1 M2, N) : pred_sexp^+ ==>
- (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+"
-apply (frule pred_sexp_subset_Sigma [THEN trancl_subset_Sigma, THEN subsetD])
-apply (blast dest!: sexp_CONS_D intro: pred_sexp_CONS_I1 pred_sexp_CONS_I2
- trans_trancl [THEN transD])
-done
-
-
-(** Conversion rules for List_rec **)
-
-lemma List_rec_NIL [simp]: "List_rec NIL c h = c"
-apply (rule List_rec_unfold [THEN trans])
-apply (simp add: List_case_NIL)
-done
-
-lemma List_rec_CONS [simp]:
- "[| M: sexp; N: sexp |]
- ==> List_rec (CONS M N) c h = h M N (List_rec N c h)"
-apply (rule List_rec_unfold [THEN trans])
-apply (simp add: pred_sexp_CONS_I2)
-done
-
-
-(*** list_rec -- by List_rec ***)
-
-lemmas Rep_List_in_sexp =
- subsetD [OF range_Leaf_subset_sexp [THEN list_subset_sexp]
- Rep_List [THEN ListD]]
-
-
-lemma list_rec_Nil [simp]: "list_rec Nil c h = c"
-by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Nil_def)
-
-
-lemma list_rec_Cons [simp]: "list_rec (a#l) c h = h a l (list_rec l c h)"
-by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Cons_def
- Rep_List_inverse Rep_List [THEN ListD] inj_Leaf Rep_List_in_sexp)
-
-
-(*Type checking. Useful?*)
-lemma List_rec_type:
- "[| M: list(A);
- A<=sexp;
- c: C(NIL);
- !!x y r. [| x: A; y: list(A); r: C(y) |] ==> h x y r: C(CONS x y)
- |] ==> List_rec M c h : C(M :: 'a item)"
-apply (erule list.induct, simp)
-apply (insert list_subset_sexp)
-apply (subst List_rec_CONS, blast+)
-done
-
-
-
-(** Generalized map functionals **)
-
-lemma Rep_map_Nil [simp]: "Rep_map f Nil = NIL"
-by (simp add: Rep_map_def)
-
-lemma Rep_map_Cons [simp]:
- "Rep_map f(x#xs) = CONS(f x)(Rep_map f xs)"
-by (simp add: Rep_map_def)
-
-lemma Rep_map_type: "(!!x. f(x): A) ==> Rep_map f xs: list(A)"
-apply (simp add: Rep_map_def)
-apply (rule list_induct, auto)
-done
-
-lemma Abs_map_NIL [simp]: "Abs_map g NIL = Nil"
-by (simp add: Abs_map_def)
-
-lemma Abs_map_CONS [simp]:
- "[| M: sexp; N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N"
-by (simp add: Abs_map_def)
-
-(*Eases the use of primitive recursion.*)
-lemma def_list_rec_NilCons:
- "[| !!xs. f(xs) = list_rec xs c h |]
- ==> f [] = c & f(x#xs) = h x xs (f xs)"
-by simp
-
-
-
-lemma Abs_map_inverse:
- "[| M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z |]
- ==> Rep_map f (Abs_map g M) = M"
-apply (erule list.induct, simp_all)
-apply (insert list_subset_sexp)
-apply (subst Abs_map_CONS, blast)
-apply blast
-apply simp
-done
-
-(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
-
-(** list_case **)
-
-(* setting up rewrite sets *)
-
-text{*Better to have a single theorem with a conjunctive conclusion.*}
-declare def_list_rec_NilCons [OF list_case_def, simp]
-
-(** list_case **)
-
-lemma expand_list_case:
- "P(list_case a f xs) = ((xs=[] --> P a ) & (!y ys. xs=y#ys --> P(f y ys)))"
-by (induct xs rule: list_induct) simp_all
-
-
-(**** Function definitions ****)
-
-declare def_list_rec_NilCons [OF null_def, simp]
-declare def_list_rec_NilCons [OF hd_def, simp]
-declare def_list_rec_NilCons [OF tl_def, simp]
-declare def_list_rec_NilCons [OF ttl_def, simp]
-declare def_list_rec_NilCons [OF append_def, simp]
-declare def_list_rec_NilCons [OF member_def, simp]
-declare def_list_rec_NilCons [OF map_def, simp]
-declare def_list_rec_NilCons [OF filter_def, simp]
-declare def_list_rec_NilCons [OF list_all_def, simp]
-
-
-(** nth **)
-
-lemma def_nat_rec_0_eta:
- "[| !!n. f = nat_rec c h |] ==> f(0) = c"
-by simp
-
-lemma def_nat_rec_Suc_eta:
- "[| !!n. f = nat_rec c h |] ==> f(Suc(n)) = h n (f n)"
-by simp
-
-declare def_nat_rec_0_eta [OF nth_def, simp]
-declare def_nat_rec_Suc_eta [OF nth_def, simp]
-
-
-(** length **)
-
-lemma length_Nil [simp]: "length([]) = 0"
-by (simp add: length_def)
-
-lemma length_Cons [simp]: "length(a#xs) = Suc(length(xs))"
-by (simp add: length_def)
-
-
-(** @ - append **)
-
-lemma append_assoc [simp]: "(xs@ys)@zs = xs@(ys@zs)"
-by (induct xs rule: list_induct) simp_all
-
-lemma append_Nil2 [simp]: "xs @ [] = xs"
-by (induct xs rule: list_induct) simp_all
-
-(** mem **)
-
-lemma mem_append [simp]: "x mem (xs@ys) = (x mem xs | x mem ys)"
-by (induct xs rule: list_induct) simp_all
-
-lemma mem_filter [simp]: "x mem [x\<leftarrow>xs. P x ] = (x mem xs & P(x))"
-by (induct xs rule: list_induct) simp_all
-
-(** list_all **)
-
-lemma list_all_True [simp]: "(Alls x:xs. True) = True"
-by (induct xs rule: list_induct) simp_all
-
-lemma list_all_conj [simp]:
- "list_all p (xs@ys) = ((list_all p xs) & (list_all p ys))"
-by (induct xs rule: list_induct) simp_all
-
-lemma list_all_mem_conv: "(Alls x:xs. P(x)) = (!x. x mem xs --> P(x))"
-apply (induct xs rule: list_induct)
-apply simp_all
-apply blast
-done
-
-lemma nat_case_dist : "(! n. P n) = (P 0 & (! n. P (Suc n)))"
-apply auto
-apply (induct_tac n)
-apply auto
-done
-
-
-lemma alls_P_eq_P_nth: "(Alls u:A. P u) = (!n. n < length A --> P(nth n A))"
-apply (induct_tac A rule: list_induct)
-apply simp_all
-apply (rule trans)
-apply (rule_tac [2] nat_case_dist [symmetric], simp_all)
-done
-
-
-lemma list_all_imp:
- "[| !x. P x --> Q x; (Alls x:xs. P(x)) |] ==> (Alls x:xs. Q(x))"
-by (simp add: list_all_mem_conv)
-
-
-(** The functional "map" and the generalized functionals **)
-
-lemma Abs_Rep_map:
- "(!!x. f(x): sexp) ==>
- Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"
-apply (induct xs rule: list_induct)
-apply (simp_all add: Rep_map_type list_sexp [THEN subsetD])
-done
-
-
-(** Additional mapping lemmas **)
-
-lemma map_ident [simp]: "map(%x. x)(xs) = xs"
-by (induct xs rule: list_induct) simp_all
-
-lemma map_append [simp]: "map f (xs@ys) = map f xs @ map f ys"
-by (induct xs rule: list_induct) simp_all
-
-lemma map_compose: "map(f o g)(xs) = map f (map g xs)"
-apply (simp add: o_def)
-apply (induct xs rule: list_induct)
-apply simp_all
-done
-
-
-lemma mem_map_aux1 [rule_format]:
- "x mem (map f q) --> (\<exists>y. y mem q & x = f y)"
-by (induct q rule: list_induct) auto
-
-lemma mem_map_aux2 [rule_format]:
- "(\<exists>y. y mem q & x = f y) --> x mem (map f q)"
-by (induct q rule: list_induct) auto
-
-lemma mem_map: "x mem (map f q) = (\<exists>y. y mem q & x = f y)"
-apply (rule iffI)
-apply (erule mem_map_aux1)
-apply (erule mem_map_aux2)
-done
-
-lemma hd_append [rule_format]: "A ~= [] --> hd(A @ B) = hd(A)"
-by (induct A rule: list_induct) auto
-
-lemma tl_append [rule_format]: "A ~= [] --> tl(A @ B) = tl(A) @ B"
-by (induct A rule: list_induct) auto
-
-
-(** take **)
-
-lemma take_Suc1 [simp]: "take [] (Suc x) = []"
-by simp
-
-lemma take_Suc2 [simp]: "take(a#xs)(Suc x) = a#take xs x"
-by simp
-
-
-(** drop **)
-
-lemma drop_0 [simp]: "drop xs 0 = xs"
-by (simp add: drop_def)
-
-lemma drop_Suc1 [simp]: "drop [] (Suc x) = []"
-apply (induct x)
-apply (simp_all add: drop_def)
-done
-
-lemma drop_Suc2 [simp]: "drop(a#xs)(Suc x) = drop xs x"
-by (simp add: drop_def)
-
-
-(** copy **)
-
-lemma copy_0 [simp]: "copy x 0 = []"
-by (simp add: copy_def)
-
-lemma copy_Suc [simp]: "copy x (Suc y) = x # copy x y"
-by (simp add: copy_def)
-
-
-(** fold **)
-
-lemma foldl_Nil [simp]: "foldl f a [] = a"
-by (simp add: foldl_def)
-
-lemma foldl_Cons [simp]: "foldl f a(x#xs) = foldl f (f a x) xs"
-by (simp add: foldl_def)
-
-lemma foldr_Nil [simp]: "foldr f a [] = a"
-by (simp add: foldr_def)
-
-lemma foldr_Cons [simp]: "foldr f z(x#xs) = f x (foldr f z xs)"
-by (simp add: foldr_def)
-
-
-(** flat **)
-
-lemma flat_Nil [simp]: "flat [] = []"
-by (simp add: flat_def)
-
-lemma flat_Cons [simp]: "flat (x # xs) = x @ flat xs"
-by (simp add: flat_def)
-
-(** rev **)
-
-lemma rev_Nil [simp]: "rev [] = []"
-by (simp add: rev_def)
-
-lemma rev_Cons [simp]: "rev (x # xs) = rev xs @ [x]"
-by (simp add: rev_def)
-
-
-(** zip **)
-
-lemma zipWith_Cons_Cons [simp]:
- "zipWith f (a#as,b#bs) = f(a,b) # zipWith f (as,bs)"
-by (simp add: zipWith_def)
-
-lemma zipWith_Nil_Nil [simp]: "zipWith f ([],[]) = []"
-by (simp add: zipWith_def)
-
-
-lemma zipWith_Cons_Nil [simp]: "zipWith f (x,[]) = []"
-by (induct x rule: list_induct) (simp_all add: zipWith_def)
-
-
-lemma zipWith_Nil_Cons [simp]: "zipWith f ([],x) = []"
-by (simp add: zipWith_def)
-
-lemma unzip_Nil [simp]: "unzip [] = ([],[])"
-by (simp add: unzip_def)
-
-
-
-(** SOME LIST THEOREMS **)
-
-(* SQUIGGOL LEMMAS *)
-
-lemma map_compose_ext: "map(f o g) = ((map f) o (map g))"
-apply (simp add: o_def)
-apply (rule ext)
-apply (simp add: map_compose [symmetric] o_def)
-done
-
-lemma map_flat: "map f (flat S) = flat(map (map f) S)"
-by (induct S rule: list_induct) simp_all
-
-lemma list_all_map_eq: "(Alls u:xs. f(u) = g(u)) --> map f xs = map g xs"
-by (induct xs rule: list_induct) simp_all
-
-lemma filter_map_d: "filter p (map f xs) = map f (filter(p o f)(xs))"
-by (induct xs rule: list_induct) simp_all
-
-lemma filter_compose: "filter p (filter q xs) = filter(%x. p x & q x) xs"
-by (induct xs rule: list_induct) simp_all
-
-(* "filter(p, filter(q,xs)) = filter(q, filter(p,xs))",
- "filter(p, filter(p,xs)) = filter(p,xs)" BIRD's thms.*)
-
-lemma filter_append [rule_format, simp]:
- "\<forall>B. filter p (A @ B) = (filter p A @ filter p B)"
-by (induct A rule: list_induct) simp_all
-
-
-(* inits(xs) == map(fst,splits(xs)),
-
- splits([]) = []
- splits(a # xs) = <[],xs> @ map(%x. <a # fst(x),snd(x)>, splits(xs))
- (x @ y = z) = <x,y> mem splits(z)
- x mem xs & y mem ys = <x,y> mem diag(xs,ys) *)
-
-lemma length_append: "length(xs@ys) = length(xs)+length(ys)"
-by (induct xs rule: list_induct) simp_all
-
-lemma length_map: "length(map f xs) = length(xs)"
-by (induct xs rule: list_induct) simp_all
-
-
-lemma take_Nil [simp]: "take [] n = []"
-by (induct n) simp_all
-
-lemma take_take_eq [simp]: "\<forall>n. take (take xs n) n = take xs n"
-apply (induct xs rule: list_induct)
-apply simp_all
-apply (rule allI)
-apply (induct_tac n)
-apply auto
-done
-
-lemma take_take_Suc_eq1 [rule_format]:
- "\<forall>n. take (take xs(Suc(n+m))) n = take xs n"
-apply (induct_tac xs rule: list_induct)
-apply simp_all
-apply (rule allI)
-apply (induct_tac n)
-apply auto
-done
-
-declare take_Suc [simp del]
-
-lemma take_take_1: "take (take xs (n+m)) n = take xs n"
-apply (induct m)
-apply (simp_all add: take_take_Suc_eq1)
-done
-
-lemma take_take_Suc_eq2 [rule_format]:
- "\<forall>n. take (take xs n)(Suc(n+m)) = take xs n"
-apply (induct_tac xs rule: list_induct)
-apply simp_all
-apply (rule allI)
-apply (induct_tac n)
-apply auto
-done
-
-lemma take_take_2: "take(take xs n)(n+m) = take xs n"
-apply (induct m)
-apply (simp_all add: take_take_Suc_eq2)
-done
-
-(* length(take(xs,n)) = min(n, length(xs)) *)
-(* length(drop(xs,n)) = length(xs) - n *)
-
-lemma drop_Nil [simp]: "drop [] n = []"
-by (induct n) auto
-
-lemma drop_drop [rule_format]: "\<forall>xs. drop (drop xs m) n = drop xs(m+n)"
-apply (induct_tac m)
-apply auto
-apply (induct_tac xs rule: list_induct)
-apply auto
-done
-
-lemma take_drop [rule_format]: "\<forall>xs. (take xs n) @ (drop xs n) = xs"
-apply (induct_tac n)
-apply auto
-apply (induct_tac xs rule: list_induct)
-apply auto
-done
-
-lemma copy_copy: "copy x n @ copy x m = copy x (n+m)"
-by (induct n) auto
-
-lemma length_copy: "length(copy x n) = n"
-by (induct n) auto
-
-lemma length_take [rule_format, simp]:
- "\<forall>xs. length(take xs n) = min (length xs) n"
-apply (induct n)
- apply auto
-apply (induct_tac xs rule: list_induct)
- apply auto
-done
-
-lemma length_take_drop: "length(take A k) + length(drop A k) = length(A)"
-by (simp only: length_append [symmetric] take_drop)
-
-lemma take_append [rule_format]: "\<forall>A. length(A) = n --> take(A@B) n = A"
-apply (induct n)
-apply (rule allI)
-apply (rule_tac [2] allI)
-apply (induct_tac A rule: list_induct)
-apply (induct_tac [3] A rule: list_induct, simp_all)
-done
-
-lemma take_append2 [rule_format]:
- "\<forall>A. length(A) = n --> take(A@B) (n+k) = A @ take B k"
-apply (induct n)
-apply (rule allI)
-apply (rule_tac [2] allI)
-apply (induct_tac A rule: list_induct)
-apply (induct_tac [3] A rule: list_induct, simp_all)
-done
-
-lemma take_map [rule_format]: "\<forall>n. take (map f A) n = map f (take A n)"
-apply (induct A rule: list_induct)
-apply simp_all
-apply (rule allI)
-apply (induct_tac n)
-apply simp_all
-done
-
-lemma drop_append [rule_format]: "\<forall>A. length(A) = n --> drop(A@B)n = B"
-apply (induct n)
-apply (rule allI)
-apply (rule_tac [2] allI)
-apply (induct_tac A rule: list_induct)
-apply (induct_tac [3] A rule: list_induct)
-apply simp_all
-done
-
-lemma drop_append2 [rule_format]:
- "\<forall>A. length(A) = n --> drop(A@B)(n+k) = drop B k"
-apply (induct n)
-apply (rule allI)
-apply (rule_tac [2] allI)
-apply (induct_tac A rule: list_induct)
-apply (induct_tac [3] A rule: list_induct)
-apply simp_all
-done
-
-
-lemma drop_all [rule_format]: "\<forall>A. length(A) = n --> drop A n = []"
-apply (induct n)
-apply (rule allI)
-apply (rule_tac [2] allI)
-apply (induct_tac A rule: list_induct)
-apply (induct_tac [3] A rule: list_induct)
-apply auto
-done
-
-lemma drop_map [rule_format]: "\<forall>n. drop (map f A) n = map f (drop A n)"
-apply (induct A rule: list_induct)
-apply simp_all
-apply (rule allI)
-apply (induct_tac n)
-apply simp_all
-done
-
-lemma take_all [rule_format]: "\<forall>A. length(A) = n --> take A n = A"
-apply (induct n)
-apply (rule allI)
-apply (rule_tac [2] allI)
-apply (induct_tac A rule: list_induct)
-apply (induct_tac [3] A rule: list_induct)
-apply auto
-done
-
-lemma foldl_single: "foldl f a [b] = f a b"
-by simp_all
-
-lemma foldl_append [simp]:
- "\<And>a. foldl f a (A @ B) = foldl f (foldl f a A) B"
-by (induct A rule: list_induct) simp_all
-
-lemma foldl_map:
- "\<And>e. foldl f e (map g S) = foldl (%x y. f x (g y)) e S"
-by (induct S rule: list_induct) simp_all
-
-lemma foldl_neutr_distr [rule_format]:
- assumes r_neutr: "\<forall>a. f a e = a"
- and r_neutl: "\<forall>a. f e a = a"
- and assoc: "\<forall>a b c. f a (f b c) = f(f a b) c"
- shows "\<forall>y. f y (foldl f e A) = foldl f y A"
-apply (induct A rule: list_induct)
-apply (simp_all add: r_neutr r_neutl, clarify)
-apply (erule all_dupE)
-apply (rule trans)
-prefer 2 apply assumption
-apply (simp (no_asm_use) add: assoc [THEN spec, THEN spec, THEN spec, THEN sym])
-apply simp
-done
-
-lemma foldl_append_sym:
-"[| !a. f a e = a; !a. f e a = a;
- !a b c. f a (f b c) = f(f a b) c |]
- ==> foldl f e (A @ B) = f(foldl f e A)(foldl f e B)"
-apply (rule trans)
-apply (rule foldl_append)
-apply (rule sym)
-apply (rule foldl_neutr_distr, auto)
-done
-
-lemma foldr_append [rule_format, simp]:
- "\<forall>a. foldr f a (A @ B) = foldr f (foldr f a B) A"
-by (induct A rule: list_induct) simp_all
-
-
-lemma foldr_map: "\<And>e. foldr f e (map g S) = foldr (f o g) e S"
-by (induct S rule: list_induct) (simp_all add: o_def)
-
-lemma foldr_Un_eq_UN: "foldr op Un {} S = (UN X: {t. t mem S}.X)"
-by (induct S rule: list_induct) auto
-
-lemma foldr_neutr_distr:
- "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |]
- ==> foldr f y S = f (foldr f e S) y"
-by (induct S rule: list_induct) auto
-
-lemma foldr_append2:
- "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |]
- ==> foldr f e (A @ B) = f (foldr f e A) (foldr f e B)"
-apply auto
-apply (rule foldr_neutr_distr)
-apply auto
-done
-
-lemma foldr_flat:
- "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |] ==>
- foldr f e (flat S) = (foldr f e)(map (foldr f e) S)"
-apply (induct S rule: list_induct)
-apply (simp_all del: foldr_append add: foldr_append2)
-done
-
-
-lemma list_all_map: "(Alls x:map f xs .P(x)) = (Alls x:xs.(P o f)(x))"
-by (induct xs rule: list_induct) auto
-
-lemma list_all_and:
- "(Alls x:xs. P(x)&Q(x)) = ((Alls x:xs. P(x))&(Alls x:xs. Q(x)))"
-by (induct xs rule: list_induct) auto
-
-
-lemma nth_map [rule_format]:
- "\<forall>i. i < length(A) --> nth i (map f A) = f(nth i A)"
-apply (induct A rule: list_induct)
-apply simp_all
-apply (rule allI)
-apply (induct_tac i)
-apply auto
-done
-
-lemma nth_app_cancel_right [rule_format]:
- "\<forall>i. i < length(A) --> nth i(A@B) = nth i A"
-apply (induct A rule: list_induct)
-apply simp_all
-apply (rule allI)
-apply (induct_tac i)
-apply simp_all
-done
-
-lemma nth_app_cancel_left [rule_format]:
- "\<forall>n. n = length(A) --> nth(n+i)(A@B) = nth i B"
-by (induct A rule: list_induct) simp_all
-
-
-(** flat **)
-
-lemma flat_append [simp]: "flat(xs@ys) = flat(xs) @ flat(ys)"
-by (induct xs rule: list_induct) auto
-
-lemma filter_flat: "filter p (flat S) = flat(map (filter p) S)"
-by (induct S rule: list_induct) auto
-
-
-(** rev **)
-
-lemma rev_append [simp]: "rev(xs@ys) = rev(ys) @ rev(xs)"
-by (induct xs rule: list_induct) auto
-
-lemma rev_rev_ident [simp]: "rev(rev l) = l"
-by (induct l rule: list_induct) auto
-
-lemma rev_flat: "rev(flat ls) = flat (map rev (rev ls))"
-by (induct ls rule: list_induct) auto
-
-lemma rev_map_distrib: "rev(map f l) = map f (rev l)"
-by (induct l rule: list_induct) auto
-
-lemma foldl_rev: "foldl f b (rev l) = foldr (%x y. f y x) b l"
-by (induct l rule: list_induct) auto
-
-lemma foldr_rev: "foldr f b (rev l) = foldl (%x y. f y x) b l"
-apply (rule sym)
-apply (rule trans)
-apply (rule_tac [2] foldl_rev)
-apply simp
-done
-
-end
--- a/src/HOL/IsaMakefile Sun Nov 15 13:06:07 2009 +0100
+++ b/src/HOL/IsaMakefile Sun Nov 15 13:06:42 2009 +0100
@@ -430,12 +430,11 @@
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
-$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \
- Induct/LFilter.thy Induct/LList.thy Induct/Ordinals.thy \
- Induct/PropLog.thy Induct/QuoNestedDataType.thy \
- Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \
- Induct/Sigma_Algebra.thy Induct/SList.thy Induct/ABexp.thy \
- Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
+$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \
+ Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy \
+ Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \
+ Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/Term.thy \
+ Induct/Tree.thy Induct/document/root.tex
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
--- a/src/HOL/Tools/metis_tools.ML Sun Nov 15 13:06:07 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML Sun Nov 15 13:06:42 2009 +0100
@@ -28,10 +28,10 @@
(* ------------------------------------------------------------------------- *)
(* Useful Theorems *)
(* ------------------------------------------------------------------------- *)
-val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate @{context} [(("R", 0), "False")] notE);
-val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl); (*Rename from 0,1*)
-val subst_em = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
-val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
+val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
+val REFL_THM = incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
+val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
+val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
(* ------------------------------------------------------------------------- *)
(* Useful Functions *)
--- a/src/Pure/Thy/present.ML Sun Nov 15 13:06:07 2009 +0100
+++ b/src/Pure/Thy/present.ML Sun Nov 15 13:06:42 2009 +0100
@@ -325,16 +325,16 @@
fun isabelle_document verbose format name tags path result_path =
let
val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \
- \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^
- " 2>&1" ^ (if verbose then "" else " >/dev/null");
+ \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
val doc_path = Path.append result_path (Path.ext format (Path.basic name));
- in
- if verbose then writeln s else ();
- system s;
- File.exists doc_path orelse
- error ("No document: " ^ quote (show_path doc_path));
- doc_path
- end;
+ val _ = if verbose then writeln s else ();
+ val (out, rc) = system_out s;
+ val _ =
+ if not (File.exists doc_path) orelse rc <> 0 then
+ cat_error out ("Failed to build document " ^ quote (show_path doc_path))
+ else if verbose then writeln out
+ else ();
+ in doc_path end;
fun isabelle_browser graph =
let