# HG changeset patch # User schirmer # Date 1258286802 -3600 # Node ID f06fe9c2152ddd7256e2f185d82b9ed74bc2f0aa # Parent 9d76c8080aea772f2ccab6f952387d600431b5a0# Parent 889d06128608945fc225c5b48902c7d611f669c6 merged diff -r 9d76c8080aea -r f06fe9c2152d Admin/update-keywords --- 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" diff -r 9d76c8080aea -r f06fe9c2152d etc/isar-keywords-ZF.el --- 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" diff -r 9d76c8080aea -r f06fe9c2152d etc/isar-keywords.el --- 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" diff -r 9d76c8080aea -r f06fe9c2152d lib/ProofGeneral/pgip.rnc --- 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 diff -r 9d76c8080aea -r f06fe9c2152d lib/ProofGeneral/pgip_isar.xml --- 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 @@ - diff -r 9d76c8080aea -r f06fe9c2152d lib/jedit/README --- 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 - - - -Example catalog file: - - - - - - - - -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$ diff -r 9d76c8080aea -r f06fe9c2152d lib/jedit/isabelle.xml --- 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 @@ - - - - - - - - - - - - - - - - - - - (* - *) - - - {* - *} - - - ` - ` - - - " - " - - - . - .. - Isabelle.command - Isar.begin_document - Isar.define_command - Isar.edit_document - Isar.end_document - ML - - ML_prf - - abbreviation - actions - advanced - also - and - apply - apply_end - arities - assume - assumes - atom_decl - - - - - attach - attribute_setup - automaton - avoids - ax_specification - axclass - axiomatization - axioms - back - begin - binder - by - cannot_undo - case - case_eqns - - chapter - class - - classes - classrel - codatatype - code_abort - code_class - code_const - code_datatype - - code_include - code_instance - code_library - code_module - code_modulename - code_monad - code_pred - code_reserved - - code_type - coinductive - coinductive_set - - compose - con_defs - congs - constdefs - constrains - consts - consts_code - contains - context - corollary - cpodef - datatype - declaration - declare - def - defaultsort - defer - defer_recdef - defines - definition - defs - - - domain - domains - done - elimination - - end - equivariance - exit - - extract - extract_type - file - finalconsts - finally - - - fix - fixes - fixpat - fixrec - for - from - - fun - function - global - guess - have - - - hence - hide - hide_action - hints - identifier - if - imports - in - induction - inductive - inductive_cases - inductive_set - infix - infixl - infixr - init_toplevel - initially - inputs - instance - instantiation - internals - interpret - interpretation - intros - is - judgment - kill - - lazy - lemma - lemmas - let - linear_undo - local - local_setup - locale - method_setup - module_name - monos - moreover - morphisms - next - - nitpick_params - no_notation - no_syntax - no_translations - nominal_datatype - nominal_inductive - nominal_inductive2 - nominal_primrec - nonterminals - - notation - note - notes - obtain - obtains - oops - open - oracle - output - outputs - overloaded - overloading - parse_ast_translation - parse_translation - pcpodef - permissive - post - - pre - prefer - presume - - - primrec - - - print_ast_translation - - - - - - - - - - - - - - - - - - - - - - - - - - - - print_translation - proof - - - qed - - quickcheck_params - quit - realizability - realizers - recdef - recdef_tc - record - recursor_eqns - - refute_params - - rename - rep_datatype - restrict - sect - section - setup - show - shows - signature - simproc_setup - - sorry - specification - states - statespace - structure - subclass - sublocale - subsect - subsection - subsubsect - subsubsection - syntax - - termination - text - text_raw - then - theorem - theorems - theory - - - thus - - to - - transitions - translations - transrel - txt - txt_raw - - type_elims - type_intros - typed_print_translation - typedecl - typedef - types - types_code - ultimately - unchecked - undo - undos_proof - unfolding - - use - - uses - using - - - - where - with - { - } - - - diff -r 9d76c8080aea -r f06fe9c2152d lib/jedit/plugin/Isabelle.props --- 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 = diff -r 9d76c8080aea -r f06fe9c2152d lib/jedit/plugin/dockables.xml --- 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 @@ - - - - - - - new isabelle.jedit.IsabelleDock(view, position); - - - diff -r 9d76c8080aea -r f06fe9c2152d lib/jedit/plugin/isabelle_dock.scala --- 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 -} diff -r 9d76c8080aea -r f06fe9c2152d lib/jedit/plugin/isabelle_parser.scala --- 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 - -} - diff -r 9d76c8080aea -r f06fe9c2152d lib/jedit/plugin/isabelle_plugin.scala --- 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 _ => - } - -} diff -r 9d76c8080aea -r f06fe9c2152d lib/jedit/plugin/mk --- 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/ diff -r 9d76c8080aea -r f06fe9c2152d lib/jedit/plugin/services.xml --- 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 @@ - - - - - - - new isabelle.jedit.IsabelleParser(); - - - diff -r 9d76c8080aea -r f06fe9c2152d lib/logo/index.html --- 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 @@ - - diff -r 9d76c8080aea -r f06fe9c2152d lib/scripts/keywords.pl --- 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'; - - -EOF - print "\n"; - print "\n"; - print <<'EOF'; - - - - - - - - - - - - - - - (* - *) - - - {* - *} - - - ` - ` - - - " - " - - -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; - print " <${type}>${name}\n"; - } - } - - print <<'EOF'; - - - -EOF - - close OUTPUT; - select; - print STDERR "${target_tool}: ${file}\n"; + print STDERR "${file}\n"; } ## main &collect_keywords(); -eval "${target_tool}_output()"; +&emacs_output(); diff -r 9d76c8080aea -r f06fe9c2152d src/HOL/Deriv.thy --- 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 "\x. a \ x & x \ 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 \ 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 \ (%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 diff -r 9d76c8080aea -r f06fe9c2152d src/HOL/Induct/LFilter.thy --- 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) \ findRel p" - | seek: "[| ~p x; (l,l') \ findRel p |] ==> (LCons x l, l') \ 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'') \ 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 ==> \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 \ Domain(findRel p) = (p x | l \ Domain(findRel p))" -by auto - -lemma Domain_findRel_iff: - "(l \ Domain (findRel p)) = (\x l'. (l, LCons x l') \ 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') \ 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 \ 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') \ 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 \ 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' --> - (\l''. l' = lfilter p l'' & (l, LCons x l'') \ findRel p)" -apply (subst lfilter_def [THEN def_llist_corec]) -apply (case_tac "l \ Domain (findRel p) ") - apply (auto iff: Domain_findRel_iff) -done - - -lemma lfilter_cases: "lfilter p l = LNil | - (\y l'. lfilter p l = LCons y (lfilter p l') & p y)" -apply (case_tac "l \ 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') \ findRel q - ==> l' = LCons x l'' --> p x --> (l,l') \ 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'') \ findRel (%x. p x & q x) - ==> (l, LCons x l') \ findRel q --> ~ p x --> - l' \ Domain (findRel (%x. p x & q x))" -by (erule findRel.induct, auto) - -lemma findRel_conj2 [rule_format]: - "(l,lxx) \ findRel q - ==> lxx = LCons x lx --> (lx,lz) \ findRel(%x. p x & q x) --> ~ p x - --> (l,lz) \ findRel (%x. p x & q x)" -by (erule findRel.induct, auto) - -lemma findRel_lfilter_Domain_conj [rule_format]: - "(lx,ly) \ findRel p - ==> \l. lx = lfilter q l --> l \ 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'') \ findRel(%x. p x & q x) - ==> l'' = LCons y l' --> - (lfilter q l, LCons y (lfilter q l')) \ findRel p" -by (erule findRel.induct, auto) - -lemma lfilter_conj_lemma: - "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l) - \ llistD_Fun (range (%u. (lfilter p (lfilter q u), - lfilter (%x. p x & q x) u)))" -apply (case_tac "l \ 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' \ 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) \ 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)) \ 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') \ findRel(%x. p (f x)) ==> lmap f l \ Domain(findRel p)" -by (erule findRel.induct, auto) - -lemma lmap_eq_LCons [rule_format]: "lmap f l = LCons x l' --> - (\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) \ findRel p - ==> \l. lmap f l = lx --> ly = LCons x l' --> - (\y l''. x = f y & l' = lmap f l'' & - (l, LCons y l'') \ 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 \ 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 diff -r 9d76c8080aea -r f06fe9c2152d src/HOL/Induct/LList.thy --- 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 \ llist(A)" - | CONS_I: "[| a \ A; M \ llist(A) |] ==> CONS a M \ 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) \ LListD(r)" - | CONS_I: "[| (a,b) \ r; (M,N) \ LListD(r) |] - ==> (CONS a M, CONS b N) \ 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 | (\M a. z = CONS a M & a \ A & M \ 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) | - (\M N a b. z = (CONS a M, CONS b N) & (a, b) \ r & (M, N) \ 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 = (\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 \ B" - shows "llist A \ llist B" -proof - fix x - assume "x \ llist A" - then show "x \ 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 \ X; X \ list_Fun A (X Un llist(A)) |] ==> M \ llist(A)" -apply (simp add: list_Fun_def) -apply (erule llist.coinduct) -apply (blast intro: elim:); -done - -lemma list_Fun_NIL_I [iff]: "NIL \ list_Fun A X" -by (simp add: list_Fun_def NIL_def) - -lemma list_Fun_CONS_I [intro!,simp]: - "[| M \ A; N \ X |] ==> CONS M N \ 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 \ llist(A) ==> M \ 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 (\x. f(x)) = (\x. CONS M (f x))" -apply (simp add: CONS_def In1_UN1 Scons_UN1_y) -done - -lemma CONS_mono: "[| M\M'; N\N' |] ==> CONS M N \ 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 \ - (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)) \ - 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 \ 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]: - "\M N. (M,N) \ 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)) \ llist(A)" -apply (rule subsetI) -apply (erule llist.coinduct) -apply (simp add: NIL_def CONS_def) -apply (drule_tac P = "%x. xa \ 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) \ 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\B ==> LListD_Fun r A \ LListD_Fun r B" -apply (simp add: LListD_Fun_def) -apply (assumption | rule basic_monos)+ -done - -lemma LListD_coinduct: - "[| M \ X; X \ LListD_Fun r (X Un LListD(r)) |] ==> M \ 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) \ LListD_Fun r s" -by (simp add: LListD_Fun_def NIL_def) - -lemma LListD_Fun_CONS_I: - "[| x\A; (M,N):s |] ==> (CONS x M, CONS x N) \ 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 \ LListD(r) ==> M \ 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)) \ 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 \ llist(A) ==> (M,M) \ 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) \ r; r \ 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\A ==> Lconst(M): llist(A)" -apply (rule singletonI [THEN llist_coinduct], safe) -apply (rule_tac P = "%u. u \ ?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 \ llist (range Leaf) ==> x \ LList" -by (simp add: LList_def) - -lemma LListD: "x \ LList ==> x \ 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 \ llist(A) ==> M \ A & N \ 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 \ llist(A); g(NIL): llist(A); - f(NIL)=g(NIL); - !!x l. [| x\A; l \ llist(A) |] ==> - (f(CONS x l),g(CONS x l)) \ - 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 \ llist(A); !!x. x\A ==> f(x):B |] ==> Lmap f M \ 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 \ llist(A) ==> Lmap f M \ llist(f`A)" -apply (erule Lmap_type) -apply (erule imageI) -done - -subsubsection{* Two easy results about @{text Lmap} *} - -lemma Lmap_compose: "M \ 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 \ 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 \ llist(A) ==> Lappend NIL M = M" -by (erule LList_fun_equalityI, simp_all) - -lemma Lappend_NIL2: "M \ 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 \ llist(A); N \ llist(A) |] ==> Lappend M N \ llist(A)" -apply (rule_tac X = "\u\llist (A) . \v \ 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 \ llist(A); N \ llist(A) |] ==> Lappend M N \ 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)) - \ 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 \ (llist A) <*> (llist A) - ==> LListD_Fun (Id_on A) r \ (llist A) <*> (llist A)" -by (auto simp add: LListD_Fun_def) - -lemma subset_Times_llist: - "prod_fun Rep_LList Rep_LList ` r \ - (llist(range Leaf)) <*> (llist(range Leaf))" -by (blast intro: Rep_LList [THEN LListD]) - -lemma prod_fun_lemma: - "r \ (llist(range Leaf)) <*> (llist(range Leaf)) - ==> prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r \ 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\B ==> llistD_Fun A \ 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) \ r; r \ 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) \ 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) \ 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) \ 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)) - \ 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 = "\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 = "\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 diff -r 9d76c8080aea -r f06fe9c2152d src/HOL/Induct/README.html --- 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). -
  • LFilter is an inductive/corecursive formalization of the -filter functional for infinite streams. -
  • Exp demonstrates the use of iterated inductive definitions to reason about mutually recursive relations. diff -r 9d76c8080aea -r f06fe9c2152d src/HOL/Induct/ROOT.ML --- 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"]; diff -r 9d76c8080aea -r f06fe9c2152d src/HOL/Induct/SList.thy --- 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\xs . P]" == "filter (%x. P) xs" - -syntax - (* Special syntax for list_all and filter *) - "@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10) - -translations - "[x\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: "\x. l ~= x#l" -by (induct l rule: list_induct) simp_all - - -lemma neq_Nil_conv2: "(xs ~= []) = (\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\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) --> (\y. y mem q & x = f y)" -by (induct q rule: list_induct) auto - -lemma mem_map_aux2 [rule_format]: - "(\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) = (\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]: - "\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. , splits(xs)) - (x @ y = z) = mem splits(z) - x mem xs & y mem ys = 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]: "\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]: - "\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]: - "\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]: "\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]: "\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]: - "\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]: "\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]: - "\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]: "\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]: "\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]: - "\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]: "\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]: "\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]: "\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]: - "\a. foldl f a (A @ B) = foldl f (foldl f a A) B" -by (induct A rule: list_induct) simp_all - -lemma foldl_map: - "\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: "\a. f a e = a" - and r_neutl: "\a. f e a = a" - and assoc: "\a b c. f a (f b c) = f(f a b) c" - shows "\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]: - "\a. foldr f a (A @ B) = foldr f (foldr f a B) A" -by (induct A rule: list_induct) simp_all - - -lemma foldr_map: "\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]: - "\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]: - "\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]: - "\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 diff -r 9d76c8080aea -r f06fe9c2152d src/HOL/IsaMakefile --- 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 diff -r 9d76c8080aea -r f06fe9c2152d src/HOL/Tools/metis_tools.ML --- 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 *) diff -r 9d76c8080aea -r f06fe9c2152d src/Pure/Thy/present.ML --- 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