# HG changeset patch
# User wenzelm
# Date 1386262683 -3600
# Node ID d64a4ef26edbaeac0ea1d11aecd342382664f7c8
# Parent cfb21e03fe2a2686d74a6a442503ce0dba6f88e5# Parent 30666a281ae3b317dce4c0b70fb3772da863fedd
merged, resolving obvious conflicts in NEWS and src/Pure/System/isabelle_process.ML;
diff -r cfb21e03fe2a -r d64a4ef26edb .hgignore
--- a/.hgignore Thu Dec 05 17:52:12 2013 +0100
+++ b/.hgignore Thu Dec 05 17:58:03 2013 +0100
@@ -5,7 +5,9 @@
*.jar
*.orig
*.rej
+*.pyc
.DS_Store
+.swp
syntax: regexp
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/App1/README
--- a/Admin/MacOS/App1/README Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-Isabelle application bundle for MacOS
-=====================================
-
-Requirements:
-
-* CocoaDialog 2.1.1 http://cocoadialog.sourceforge.net/
-
-* Platypus 4.7 http://www.sveinbjorn.org/platypus
- Preferences: Install command line tool
-
-* final packaging:
-
- hdiutil create -srcfolder DIR DMG
-
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/App1/build
--- a/Admin/MacOS/App1/build Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-#!/usr/bin/env bash
-#
-# Make Isabelle application bundle
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-
-COCOADIALOG_APP="/Applications/CocoaDialog.app"
-
-/usr/local/bin/platypus \
- -a Isabelle -u Isabelle \
- -I "de.tum.in.isabelle" \
- -i "$THIS/../isabelle.icns" \
- -D -X thy \
- -Q "$THIS/../theory.icns" \
- -p /bin/bash \
- -R \
- -o None \
- -f "$COCOADIALOG_APP" \
- "$THIS/script" \
- "$PWD/Isabelle.app"
-
-rm -f Contents/Resources/Isabelle
-ln -s Contents/Resources/Isabelle Isabelle.app/Isabelle
\ No newline at end of file
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/App1/script
--- a/Admin/MacOS/App1/script Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Isabelle application wrapper
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-THIS_APP="$(cd "$THIS/../.."; pwd)"
-SUPER_APP="$(cd "$THIS/../../.."; pwd)"
-
-
-# global defaults
-
-ISABELLE_TOOL="$THIS/Isabelle/bin/isabelle"
-PROOFGENERAL_EMACS="$THIS/Aquamacs.app/Contents/MacOS/Aquamacs"
-
-
-# environment
-
-cd "$HOME"
-if [ -x /usr/libexec/path_helper ]; then
- eval $(/usr/libexec/path_helper -s)
-fi
-
-[ -z "$LANG" ] && export LANG=en_US.UTF-8
-
-
-# run interface with error feedback
-
-ISABELLE_INTERFACE_CHOICE="$("$ISABELLE_TOOL" getenv -b ISABELLE_INTERFACE_CHOICE)"
-if [ "$ISABELLE_INTERFACE_CHOICE" != emacs -a "$ISABELLE_INTERFACE_CHOICE" != jedit ]
-then
- declare -a CHOICE
- CHOICE=($("$THIS/CocoaDialog.app/Contents/MacOS/CocoaDialog" dropdown \
- --title Isabelle \
- --text "Which Isabelle interface?" \
- --items "Isabelle/jEdit PIDE" "Emacs / Proof General" \
- --button2 "OK, do not ask again" --button1 "OK"))
- if [ "${CHOICE[1]}" = 0 ]; then
- ISABELLE_INTERFACE_CHOICE=jedit
- else
- ISABELLE_INTERFACE_CHOICE=emacs
- fi
- if [ "${CHOICE[0]}" = 2 ]; then
- ISABELLE_HOME_USER="$("$ISABELLE_TOOL" getenv -b ISABELLE_HOME_USER)"
- mkdir -p "$ISABELLE_HOME_USER/etc"
- ( echo; echo "ISABELLE_INTERFACE_CHOICE=$ISABELLE_INTERFACE_CHOICE"; ) \
- >> "$ISABELLE_HOME_USER/etc/settings"
- "$THIS/CocoaDialog.app/Contents/MacOS/CocoaDialog" ok-msgbox \
- --title Isabelle \
- --text Note \
- --informative-text "ISABELLE_INTERFACE_CHOICE stored in $ISABELLE_HOME_USER/etc/settings" \
- --no-cancel
- fi
-fi
-
-OUTPUT="/tmp/isabelle$$.out"
-
-if [ "$ISABELLE_INTERFACE_CHOICE" = emacs ]; then
- ( "$ISABELLE_TOOL" emacs -p "$PROOFGENERAL_EMACS" "$@" ) > "$OUTPUT" 2>&1
- RC=$?
-else
- ( "$ISABELLE_TOOL" jedit -s "$@" ) > "$OUTPUT" 2>&1
- RC=$?
-fi
-
-if [ "$RC" != 0 ]; then
- echo >> "$OUTPUT"
- echo "Return code: $RC" >> "$OUTPUT"
-fi
-
-if [ $(stat -f "%z" "$OUTPUT") != 0 ]; then
- "$THIS/CocoaDialog.app/Contents/MacOS/CocoaDialog" textbox \
- --title "Isabelle" \
- --informative-text "Isabelle output" \
- --text-from-file "$OUTPUT" \
- --button1 "OK"
-fi
-
-rm -f "$OUTPUT"
-
-exit "$RC"
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/App2/Isabelle.app/Contents/Info.plist
--- a/Admin/MacOS/App2/Isabelle.app/Contents/Info.plist Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-
-
-
-
- CFBundleDevelopmentRegion
- English
- CFBundleExecutable
- Isabelle
- CFBundleGetInfoString
- Isabelle
- CFBundleIconFile
- isabelle.icns
- CFBundleIdentifier
- de.tum.in.isabelle
- CFBundleInfoDictionaryVersion
- 6.0
- CFBundleName
- Isabelle
- CFBundlePackageType
- APPL
- CFBundleShortVersionString
- ????
- CFBundleSignature
- ????
- CFBundleVersion
- ????
- Java
-
- JVMVersion
- 1.6
- VMOptions
- -Xms128m -Xmx512m -Xss2m
- ClassPath
- $JAVAROOT/isabelle-scala.jar
- MainClass
- isabelle.GUI_Setup
- Properties
-
- isabelle.home
- $APP_PACKAGE/Contents/Resources/Isabelle
- apple.laf.useScreenMenuBar
- true
- com.apple.mrj.application.apple.menu.about.name
- Isabelle
-
-
-
-
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/App2/Isabelle.app/Contents/MacOS/Isabelle
--- a/Admin/MacOS/App2/Isabelle.app/Contents/MacOS/Isabelle Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-/System/Library/Frameworks/JavaVM.framework/Resources/MacOS/JavaApplicationStub
\ No newline at end of file
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/App2/README
--- a/Admin/MacOS/App2/README Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-Isabelle/JVM application bundle for MacOS
-=========================================
-
-* http://developer.apple.com/documentation/Java/Conceptual/Java14Development/03-JavaDeployment/JavaDeployment.html
-
-* http://developer.apple.com/documentation/Java/Reference/Java_InfoplistRef/Articles/JavaDictionaryInfo.plistKeys.html#//apple_ref/doc/uid/TP40001969
-
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/App2/mk
--- a/Admin/MacOS/App2/mk Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-#!/usr/bin/env bash
-#
-# Make Isabelle/JVM application bundle
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-
-APP="$THIS/Isabelle.app"
-
-mkdir -p "$APP/Contents/Resources/Java"
-cp "$THIS/../../../lib/classes/isabelle-scala.jar" "$APP/Contents/Resources/Java"
-cp "$THIS/../isabelle.icns" "$APP/Contents/Resources"
-
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/App3/Info.plist-part1
--- a/Admin/MacOS/App3/Info.plist-part1 Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-
-
-
-
-CFBundleDevelopmentRegion
-English
-CFBundleExecutable
-JavaAppLauncher
-CFBundleIconFile
-isabelle.icns
-CFBundleIdentifier
-de.tum.in.isabelle
-CFBundleDisplayName
-{ISABELLE_NAME}
-CFBundleInfoDictionaryVersion
-6.0
-CFBundleName
-{ISABELLE_NAME}
-CFBundlePackageType
-APPL
-CFBundleShortVersionString
-1.0
-CFBundleSignature
-????
-CFBundleVersion
-1
-NSHumanReadableCopyright
-
-LSApplicationCategoryType
-public.app-category.developer-tools
-JVMRuntime
-jdk
-JVMMainClassName
-isabelle.Main
-JVMOptions
-
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/App3/Info.plist-part2
--- a/Admin/MacOS/App3/Info.plist-part2 Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
--Disabelle.home=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}
-
-JVMArguments
-
-
-
-
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/App3/README
--- a/Admin/MacOS/App3/README Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-Isabelle/JVM application bundle for Mac OS X
-============================================
-
-* http://java.net/projects/appbundler
-
- see appbundler-1.0.jar
- see com/oracle/appbundler/JavaAppLauncher
-
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/App3/Resources/en.lproj/Localizable.strings
--- a/Admin/MacOS/App3/Resources/en.lproj/Localizable.strings Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-"JRELoadError" = "Unable to load Java Runtime Environment.";
-"MainClassNameRequired" = "Main class name is required.";
-"JavaDirectoryNotFound" = "Unable to enumerate Java directory contents.";
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/Info.plist-part1
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/Info.plist-part1 Thu Dec 05 17:58:03 2013 +0100
@@ -0,0 +1,36 @@
+
+
+
+
+CFBundleDevelopmentRegion
+English
+CFBundleExecutable
+JavaAppLauncher
+CFBundleIconFile
+isabelle.icns
+CFBundleIdentifier
+de.tum.in.isabelle
+CFBundleDisplayName
+{ISABELLE_NAME}
+CFBundleInfoDictionaryVersion
+6.0
+CFBundleName
+{ISABELLE_NAME}
+CFBundlePackageType
+APPL
+CFBundleShortVersionString
+1.0
+CFBundleSignature
+????
+CFBundleVersion
+1
+NSHumanReadableCopyright
+
+LSApplicationCategoryType
+public.app-category.developer-tools
+JVMRuntime
+jdk
+JVMMainClassName
+isabelle.Main
+JVMOptions
+
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/Info.plist-part2
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/Info.plist-part2 Thu Dec 05 17:58:03 2013 +0100
@@ -0,0 +1,7 @@
+-Disabelle.home=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}
+
+JVMArguments
+
+
+
+
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/README
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/README Thu Dec 05 17:58:03 2013 +0100
@@ -0,0 +1,8 @@
+Isabelle/JVM application bundle for Mac OS X
+============================================
+
+* http://java.net/projects/appbundler
+
+ see appbundler-1.0.jar
+ see com/oracle/appbundler/JavaAppLauncher
+
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/Resources/en.lproj/Localizable.strings
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/MacOS/Resources/en.lproj/Localizable.strings Thu Dec 05 17:58:03 2013 +0100
@@ -0,0 +1,3 @@
+"JRELoadError" = "Unable to load Java Runtime Environment.";
+"MainClassNameRequired" = "Main class name is required.";
+"JavaDirectoryNotFound" = "Unable to enumerate Java directory contents.";
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/Resources/isabelle.icns
Binary file Admin/MacOS/Resources/isabelle.icns has changed
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/Resources/theory.icns
Binary file Admin/MacOS/Resources/theory.icns has changed
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/isabelle.icns
Binary file Admin/MacOS/isabelle.icns has changed
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/MacOS/theory.icns
Binary file Admin/MacOS/theory.icns has changed
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/Windows/launch4j/README
--- a/Admin/Windows/launch4j/README Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-Java application wrapper for Windows
-====================================
-
-* http://launch4j.sourceforge.net
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/Windows/launch4j/isabelle.ico
Binary file Admin/Windows/launch4j/isabelle.ico has changed
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/Windows/launch4j/isabelle.xml
--- a/Admin/Windows/launch4j/isabelle.xml Thu Dec 05 17:52:12 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-
- true
- gui
-
- Isabelle.exe
-
-
-
- normal
-
-
- false
- true
-
- isabelle.ico
-
- isabelle.Main
- %EXEDIR%\lib\classes\ext\Pure.jar
- %EXEDIR%\lib\classes\ext\scala-compiler.jar
- %EXEDIR%\lib\classes\ext\scala-library.jar
- %EXEDIR%\lib\classes\ext\scala-swing.jar
- %EXEDIR%\lib\classes\ext\scala-actors.jar
- %EXEDIR%\lib\classes\ext\scala-reflect.jar
- %EXEDIR%\src\Tools\jEdit\dist\jedit.jar
-
-
- %EXEDIR%\contrib\jdk\x86-cygwin
-
-
- jdkOnly
- -Dfile.encoding=UTF-8 -server -Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false -Disabelle.home="%EXEDIR%"
-
-
- isabelle.bmp
- false
- 10
- false
-
-
\ No newline at end of file
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/isatest/isatest-stats
--- a/Admin/isatest/isatest-stats Thu Dec 05 17:52:12 2013 +0100
+++ b/Admin/isatest/isatest-stats Thu Dec 05 17:58:03 2013 +0100
@@ -14,11 +14,9 @@
HOL-Auth
HOL-BNF
HOL-BNF-Examples
+ HOL-BNF-LFP
HOL-BNF-Nitpick_Examples
- HOL-BNF-LFP
HOL-Bali
- HOL-Boogie
- HOL-Boogie-Examples
HOL-Cardinals
HOL-Cardinals-Base
HOL-Codegenerator_Test
diff -r cfb21e03fe2a -r d64a4ef26edb Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle Thu Dec 05 17:52:12 2013 +0100
+++ b/Admin/lib/Tools/makedist_bundle Thu Dec 05 17:58:03 2013 +0100
@@ -261,7 +261,7 @@
(
cd "$TMP"
- APP_TEMPLATE="$ISABELLE_HOME/Admin/MacOS/App3"
+ APP_TEMPLATE="$ISABELLE_HOME/Admin/MacOS"
APP="${ISABELLE_NAME}.app"
for NAME in Java MacOS PlugIns Resources
@@ -289,7 +289,6 @@
done
cp -R "$APP_TEMPLATE/Resources/." "$APP/Contents/Resources/."
- cp "$APP_TEMPLATE/../isabelle.icns" "$APP/Contents/Resources/."
ln -sf "../Resources/${ISABELLE_NAME}/contrib/jdk/x86_64-darwin" \
"$APP/Contents/PlugIns/jdk"
diff -r cfb21e03fe2a -r d64a4ef26edb CONTRIBUTORS
--- a/CONTRIBUTORS Thu Dec 05 17:52:12 2013 +0100
+++ b/CONTRIBUTORS Thu Dec 05 17:58:03 2013 +0100
@@ -3,6 +3,10 @@
who is listed as an author in one of the source files of this Isabelle
distribution.
+Contributions to this Isabelle version
+--------------------------------------
+
+
Contributions to Isabelle2013-1
-------------------------------
diff -r cfb21e03fe2a -r d64a4ef26edb NEWS
--- a/NEWS Thu Dec 05 17:52:12 2013 +0100
+++ b/NEWS Thu Dec 05 17:58:03 2013 +0100
@@ -1,6 +1,98 @@
Isabelle NEWS -- history user-relevant changes
==============================================
+New in this Isabelle version
+----------------------------
+
+*** Prover IDE -- Isabelle/Scala/jEdit ***
+
+* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
+Open text buffers take precedence over copies within the file-system.
+
+
+*** HOL ***
+
+* Qualified constant names Wellfounded.acc, Wellfounded.accp.
+INCOMPATIBILITY.
+
+* Fact generalization and consolidation:
+ neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
+INCOMPATIBILITY.
+
+* Purely algebraic definition of even. Fact generalization and consolidation:
+ nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd
+ even_zero_(nat|int) ~> even_zero
+INCOMPATIBILITY.
+
+* Abolished neg_numeral.
+ * Canonical representation for minus one is "- 1".
+ * Canonical representation for other negative numbers is "- (numeral _)".
+ * When devising rule sets for number calculation, consider the
+ following canonical cases: 0, 1, numeral _, - 1, - numeral _.
+ * HOLogic.dest_number also recognizes numerals in non-canonical forms
+ like "numeral One", "- numeral One", "- 0" and even "- … - _".
+ * Syntax for negative numerals is mere input syntax.
+INCOMPATBILITY.
+
+* Elimination of fact duplicates:
+ equals_zero_I ~> minus_unique
+ diff_eq_0_iff_eq ~> right_minus_eq
+ nat_infinite ~> infinite_UNIV_nat
+ int_infinite ~> infinite_UNIV_int
+INCOMPATIBILITY.
+
+* Fact name consolidation:
+ diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
+ minus_le_self_iff ~> neg_less_eq_nonneg
+ le_minus_self_iff ~> less_eq_neg_nonpos
+ neg_less_nonneg ~> neg_less_pos
+ less_minus_self_iff ~> less_neg_neg [simp]
+INCOMPATIBILITY.
+
+* More simplification rules on unary and binary minus:
+add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,
+add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
+add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
+le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
+minus_add_cancel, uminus_add_conv_diff. These correspondingly
+have been taken away from fact collections algebra_simps and
+field_simps. INCOMPATIBILITY.
+
+To restore proofs, the following patterns are helpful:
+
+a) Arbitrary failing proof not involving "diff_def":
+Consider simplification with algebra_simps or field_simps.
+
+b) Lifting rules from addition to subtraction:
+Try with "using of [… "- _" …]" by simp".
+
+c) Simplification with "diff_def": just drop "diff_def".
+Consider simplification with algebra_simps or field_simps;
+or the brute way with
+"simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
+
+* SUP and INF generalized to conditionally_complete_lattice
+
+* Theory Lubs moved HOL image to HOL-Library. It is replaced by
+Conditionally_Complete_Lattices. INCOMPATIBILITY.
+
+* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
+instead of explicitly stating boundedness of sets.
+
+* ccpo.admissible quantifies only over non-empty chains to allow
+more syntax-directed proof rules; the case of the empty chain
+shows up as additional case in fixpoint induction proofs.
+INCOMPATIBILITY
+
+*** ML ***
+
+* Toplevel function "use" refers to raw ML bootstrap environment,
+without Isar context nor antiquotations. Potential INCOMPATIBILITY.
+Note that 'ML_file' is the canonical command to load ML files into the
+formal context.
+
+
+
New in Isabelle2013-2 (December 2013)
-------------------------------------
@@ -457,6 +549,10 @@
sets ~> set
IMCOMPATIBILITY.
+* Nitpick:
+ - Fixed soundness bug whereby mutually recursive datatypes could take
+ infinite values.
+
*** ML ***
diff -r cfb21e03fe2a -r d64a4ef26edb etc/isar-keywords.el
--- a/etc/isar-keywords.el Thu Dec 05 17:52:12 2013 +0100
+++ b/etc/isar-keywords.el Thu Dec 05 17:58:03 2013 +0100
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + HOL-Auth + HOL-BNF + HOL-BNF-LFP + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-ex + HOLCF + Pure.
+;; Generated from HOL + HOL-Auth + HOL-BNF + HOL-BNF-LFP + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
@@ -33,6 +33,7 @@
"axiomatization"
"back"
"bnf"
+ "boogie_file"
"bundle"
"by"
"cannot_undo"
@@ -343,7 +344,6 @@
"module_name"
"monos"
"morphisms"
- "no_discs_sels"
"notes"
"obtains"
"open"
@@ -352,7 +352,6 @@
"parametric"
"permissive"
"pervasive"
- "rep_compat"
"shows"
"structure"
"type_class"
@@ -487,6 +486,7 @@
"atom_decl"
"attribute_setup"
"axiomatization"
+ "boogie_file"
"bundle"
"case_of_simps"
"class"
diff -r cfb21e03fe2a -r d64a4ef26edb src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy Thu Dec 05 17:52:12 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Dec 05 17:58:03 2013 +0100
@@ -8,22 +8,9 @@
*)
theory Datatypes
-imports Setup
-keywords
- "primcorec_notyet" :: thy_decl
+imports Setup "~~/src/HOL/Library/Simps_Case_Conv"
begin
-(*<*)
-(* FIXME: Temporary setup until "primcorec" and "primcorecursive" are fully implemented. *)
-ML_command {*
-fun add_dummy_cmd _ _ lthy = lthy;
-
-val _ = Outer_Syntax.local_theory @{command_spec "primcorec_notyet"} ""
- (Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd);
-*}
-(*>*)
-
-
section {* Introduction
\label{sec:introduction} *}
@@ -54,17 +41,19 @@
text {*
\noindent
-The package also provides some convenience, notably automatically generated
-discriminators and selectors.
-
-In addition to plain inductive datatypes, the new package supports coinductive
-datatypes, or \emph{codatatypes}, which may have infinite values. For example,
-the following command introduces the type of lazy lists, which comprises both
-finite and infinite values:
+Furthermore, the package provides a lot of convenience, including automatically
+generated discriminators, selectors, and relators as well as a wealth of
+properties about them.
+
+In addition to inductive datatypes, the new package supports coinductive
+datatypes, or \emph{codatatypes}, which allow infinite values. For example, the
+following command introduces the type of lazy lists, which comprises both finite
+and infinite values:
*}
(*<*)
locale early
+ locale late
(*>*)
codatatype (*<*)(in early) (*>*)'a llist = LNil | LCons 'a "'a llist"
@@ -80,10 +69,10 @@
codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
text {*
-The first two tree types allow only finite branches, whereas the last two allow
-branches of infinite length. Orthogonally, the nodes in the first and third
-types have finite branching, whereas those of the second and fourth may have
-infinitely many direct subtrees.
+The first two tree types allow only paths of finite length, whereas the last two
+allow infinite paths. Orthogonally, the nodes in the first and third types have
+finitely many direct subtrees, whereas those of the second and fourth may have
+infinite branching.
To use the package, it is necessary to import the @{theory BNF} theory, which
can be precompiled into the \texttt{HOL-BNF} image. The following commands show
@@ -152,15 +141,15 @@
\newbox\boxA
-\setbox\boxA=\hbox{\texttt{nospam}}
-
-\newcommand\authoremaili{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
+\setbox\boxA=\hbox{\texttt{NOSPAM}}
+
+\newcommand\authoremaili{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
in.\allowbreak tum.\allowbreak de}}
-\newcommand\authoremailii{\texttt{lore{\color{white}nospam}\kern-\wd\boxA{}nz.panny@\allowbreak
+\newcommand\authoremailii{\texttt{lore{\color{white}NOSPAM}\kern-\wd\boxA{}nz.panny@\allowbreak
\allowbreak tum.\allowbreak de}}
-\newcommand\authoremailiii{\texttt{pope{\color{white}nospam}\kern-\wd\boxA{}scua@\allowbreak
+\newcommand\authoremailiii{\texttt{pope{\color{white}NOSPAM}\kern-\wd\boxA{}scua@\allowbreak
in.\allowbreak tum.\allowbreak de}}
-\newcommand\authoremailiv{\texttt{tray{\color{white}nospam}\kern-\wd\boxA{}tel@\allowbreak
+\newcommand\authoremailiv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak
in.\allowbreak tum.\allowbreak de}}
The commands @{command datatype_new} and @{command primrec_new} are expected to
@@ -171,13 +160,6 @@
Comments and bug reports concerning either the tool or this tutorial should be
directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
and \authoremailiv.
-
-\begin{framed}
-\noindent
-\textbf{Warning:}\enskip This tutorial and the package it describes are under
-construction. Please forgive their appearance. Should you have suggestions
-or comments regarding either, please let the authors know.
-\end{framed}
*}
@@ -195,7 +177,7 @@
text {*
Datatypes are illustrated through concrete examples featuring different flavors
of recursion. More examples can be found in the directory
-\verb|~~/src/HOL/BNF/Examples|.
+\verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|.
*}
subsubsection {* Nonrecursive Types
@@ -260,7 +242,8 @@
text {*
\noindent
-Lists were shown in the introduction. Terminated lists are a variant:
+Lists were shown in the introduction. Terminated lists are a variant that
+stores a value of type @{typ 'b} at the very end:
*}
datatype_new (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
@@ -310,7 +293,7 @@
Not all nestings are admissible. For example, this command will fail:
*}
- datatype_new 'a wrong = Wrong (*<*)'a
+ datatype_new 'a wrong = W1 | W2 (*<*)'a
typ (*>*)"'a wrong \ 'a"
text {*
@@ -321,7 +304,7 @@
*}
datatype_new ('a, 'b) fn = Fn "'a \ 'b"
- datatype_new 'a also_wrong = Also_Wrong (*<*)'a
+ datatype_new 'a also_wrong = W1 | W2 (*<*)'a
typ (*>*)"('a also_wrong, 'a) fn"
text {*
@@ -344,20 +327,30 @@
datatype_new} and @{command codatatype} commands.
Section~\ref{sec:registering-bounded-natural-functors} explains how to register
arbitrary type constructors as BNFs.
+
+Here is another example that fails:
*}
-
-subsubsection {* Custom Names and Syntaxes
- \label{sssec:datatype-custom-names-and-syntaxes} *}
+ datatype_new 'a pow_list = PNil 'a (*<*)'a
+ datatype_new 'a pow_list' = PNil' 'a (*>*)| PCons "('a * 'a) pow_list"
+
+text {*
+\noindent
+This one features a different flavor of nesting, where the recursive call in the
+type specification occurs around (rather than inside) another type constructor.
+*}
+
+subsubsection {* Auxiliary Constants and Properties
+ \label{sssec:datatype-auxiliary-constants-and-properties} *}
text {*
The @{command datatype_new} command introduces various constants in addition to
the constructors. With each datatype are associated set functions, a map
function, a relator, discriminators, and selectors, all of which can be given
-custom names. In the example below, the traditional names
-@{text set}, @{text map}, @{text list_all2}, @{text null}, @{text hd}, and
-@{text tl} override the default names @{text list_set}, @{text list_map}, @{text
-list_rel}, @{text is_Nil}, @{text un_Cons1}, and @{text un_Cons2}:
+custom names. In the example below, the familiar names @{text null}, @{text hd},
+@{text tl}, @{text set}, @{text map}, and @{text list_all2}, override the
+default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2},
+@{text set_list}, @{text map_list}, and @{text rel_list}:
*}
(*<*)
@@ -370,7 +363,7 @@
Cons (infixr "#" 65)
hide_type list
- hide_const Nil Cons hd tl set map list_all2 list_case list_rec
+ hide_const Nil Cons hd tl set map list_all2
context early begin
(*>*)
@@ -380,14 +373,34 @@
text {*
\noindent
-The command introduces a discriminator @{const null} and a pair of selectors
-@{const hd} and @{const tl} characterized as follows:
+
+\begin{tabular}{@ {}ll@ {}}
+Constructors: &
+ @{text "Nil \ 'a list"} \\
+&
+ @{text "Cons \ 'a \ 'a list \ 'a list"} \\
+Discriminator: &
+ @{text "null \ 'a list \ bool"} \\
+Selectors: &
+ @{text "hd \ 'a list \ 'a"} \\
+&
+ @{text "tl \ 'a list \ 'a list"} \\
+Set function: &
+ @{text "set \ 'a list \ 'a set"} \\
+Map function: &
+ @{text "map \ ('a \ 'b) \ 'a list \ 'b list"} \\
+Relator: &
+ @{text "list_all2 \ ('a \ 'b \ bool) \ 'a list \ 'b list \ bool"}
+\end{tabular}
+
+The discriminator @{const null} and the selectors @{const hd} and @{const tl}
+are characterized as follows:
%
\[@{thm list.collapse(1)[of xs, no_vars]}
\qquad @{thm list.collapse(2)[of xs, no_vars]}\]
%
-For two-constructor datatypes, a single discriminator constant suffices. The
-discriminator associated with @{const Cons} is simply
+For two-constructor datatypes, a single discriminator constant is sufficient.
+The discriminator associated with @{const Cons} is simply
@{term "\xs. \ null xs"}.
The @{text defaults} clause following the @{const Nil} constructor specifies a
@@ -447,7 +460,7 @@
@@{command datatype_new} target? @{syntax dt_options}? \\
(@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
;
- @{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'
+ @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
"}
The syntactic entity \synt{target} can be used to specify a local
@@ -464,6 +477,10 @@
should be generated.
\item
+The @{text "no_code"} option indicates that the datatype should not be
+registered for code generation.
+
+\item
The @{text "rep_compat"} option indicates that the generated names should
contain optional (and normally not displayed) ``@{text "new."}'' components to
prevent clashes with a later call to \keyw{rep\_datatype}. See
@@ -488,7 +505,7 @@
reference manual \cite{isabelle-isar-ref}.
The optional names preceding the type variables allow to override the default
-names of the set functions (@{text t_set1}, \ldots, @{text t_setM}).
+names of the set functions (@{text set1_t}, \ldots, @{text setM_t}).
Inside a mutually recursive specification, all defined datatypes must
mention exactly the same type variables in the same order.
@@ -589,6 +606,10 @@
or the function type. In principle, it should be possible to support old-style
datatypes as well, but the command does not support this yet (and there is
currently no way to register old-style datatypes as new-style datatypes).
+
+\item The recursor produced for types that recurse through functions has a
+different signature than with the old package. This makes it impossible to use
+the old \keyw{primrec} command.
\end{itemize}
An alternative to @{command datatype_new_compat} is to use the old package's
@@ -609,7 +630,7 @@
\begin{itemize}
\setlength{\itemsep}{0pt}
-\item \relax{Case combinator}: @{text t_case} (rendered using the familiar
+\item \relax{Case combinator}: @{text t.case_t} (rendered using the familiar
@{text case}--@{text of} syntax)
\item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
@@ -621,22 +642,22 @@
\phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
\item \relax{Set functions} (or \relax{natural transformations}):
-@{text t_set1}, \ldots, @{text t_setm}
-
-\item \relax{Map function} (or \relax{functorial action}): @{text t_map}
-
-\item \relax{Relator}: @{text t_rel}
-
-\item \relax{Iterator}: @{text t_fold}
-
-\item \relax{Recursor}: @{text t_rec}
+@{text set1_t}, \ldots, @{text t.setm_t}
+
+\item \relax{Map function} (or \relax{functorial action}): @{text t.map_t}
+
+\item \relax{Relator}: @{text t.rel_t}
+
+\item \relax{Iterator}: @{text t.fold_t}
+
+\item \relax{Recursor}: @{text t.rec_t}
\end{itemize}
\noindent
The case combinator, discriminators, and selectors are collectively called
\emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
-name and is normally hidden.
+names and is normally hidden.
*}
@@ -687,8 +708,9 @@
(*>*)
text {*
-The first subgroup of properties is concerned with the constructors.
-They are listed below for @{typ "'a list"}:
+The free constructor theorems are partitioned in three subgroups. The first
+subgroup of properties is concerned with the constructors. They are listed below
+for @{typ "'a list"}:
\begin{indentblock}
\begin{description}
@@ -715,7 +737,7 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{list.distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rm:] ~ \\
+\item[@{text "t."}\hthm{distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rm:] ~ \\
@{thm list.distinct(1)[THEN notE, elim!, no_vars]} \\
@{thm list.distinct(2)[THEN notE, elim!, no_vars]}
@@ -750,7 +772,7 @@
\end{indentblock}
\noindent
-The third and last subgroup revolves around discriminators and selectors:
+The third subgroup revolves around discriminators and selectors:
\begin{indentblock}
\begin{description}
@@ -793,11 +815,15 @@
\item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\
@{thm list.sel_split_asm[no_vars]}
-\item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\
-@{thm list.case_conv_if[no_vars]}
+\item[@{text "t."}\hthm{case\_eq\_if}\rm:] ~ \\
+@{thm list.case_eq_if[no_vars]}
\end{description}
\end{indentblock}
+
+\noindent
+In addition, equational versions of @{text t.disc} are registered with the @{text "[code]"}
+attribute.
*}
@@ -805,7 +831,9 @@
\label{sssec:functorial-theorems} *}
text {*
-The BNF-related theorem are as follows:
+The functorial theorems are partitioned in two subgroups. The first subgroup
+consists of properties involving the constructors and either a set function, the
+map function, or the relator:
\begin{indentblock}
\begin{description}
@@ -818,16 +846,56 @@
@{thm list.map(1)[no_vars]} \\
@{thm list.map(2)[no_vars]}
-\item[@{text "t."}\hthm{rel\_inject} @{text "[simp, code]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{rel\_inject} @{text "[simp]"}\rm:] ~ \\
@{thm list.rel_inject(1)[no_vars]} \\
@{thm list.rel_inject(2)[no_vars]}
-\item[@{text "t."}\hthm{rel\_distinct} @{text "[simp, code]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{rel\_distinct} @{text "[simp]"}\rm:] ~ \\
@{thm list.rel_distinct(1)[no_vars]} \\
@{thm list.rel_distinct(2)[no_vars]}
\end{description}
\end{indentblock}
+
+\noindent
+In addition, equational versions of @{text t.rel_inject} and @{text
+rel_distinct} are registered with the @{text "[code]"} attribute.
+
+The second subgroup consists of more abstract properties of the set functions,
+the map function, and the relator:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{map\_comp}\rm:] ~ \\
+@{thm list.map_cong0[no_vars]}
+
+\item[@{text "t."}\hthm{map\_cong} @{text "[fundef_cong]"}\rm:] ~ \\
+@{thm list.map_cong[no_vars]}
+
+\item[@{text "t."}\hthm{map\_id}\rm:] ~ \\
+@{thm list.map_id[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_compp}\rm:] ~ \\
+@{thm list.rel_compp[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_conversep}\rm:] ~ \\
+@{thm list.rel_conversep[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_eq}\rm:] ~ \\
+@{thm list.rel_eq[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_flip}\rm:] ~ \\
+@{thm list.rel_flip[no_vars]}
+
+\item[@{text "t."}\hthm{rel\_mono}\rm:] ~ \\
+@{thm list.rel_mono[no_vars]}
+
+\item[@{text "t."}\hthm{set\_map}\rm:] ~ \\
+@{thm list.set_map[no_vars]}
+
+\end{description}
+\end{indentblock}
*}
@@ -889,18 +957,22 @@
is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype}
to register new-style datatypes as old-style datatypes.
-\item \emph{The recursor @{text "t_rec"} has a different signature for nested
-recursive datatypes.} In the old package, nested recursion was internally
-reduced to mutual recursion. This reduction was visible in the type of the
-recursor, used by \keyw{primrec}. In the new package, nested recursion is
-handled in a more modular fashion. The old-style recursor can be generated on
-demand using @{command primrec_new}, as explained in
+\item \emph{The constants @{text t_case} and @{text t_rec} are now called
+@{text case_t} and @{text rec_t}.}
+
+\item \emph{The recursor @{text rec_t} has a different signature for nested
+recursive datatypes.} In the old package, nested recursion through non-functions
+was internally reduced to mutual recursion. This reduction was visible in the
+type of the recursor, used by \keyw{primrec}. Recursion through functions was
+handled specially. In the new package, nested recursion (for functions and
+non-functions) is handled in a more modular fashion. The old-style recursor can
+be generated on demand using @{command primrec_new}, as explained in
Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
new-style datatypes.
-\item \emph{Accordingly, the induction principle is different for nested
-recursive datatypes.} Again, the old-style induction principle can be generated
-on demand using @{command primrec_new}, as explained in
+\item \emph{Accordingly, the induction rule is different for nested recursive
+datatypes.} Again, the old-style induction rule can be generated on demand using
+@{command primrec_new}, as explained in
Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
new-style datatypes.
@@ -940,9 +1012,9 @@
\label{sec:defining-recursive-functions} *}
text {*
-Recursive functions over datatypes can be specified using @{command
-primrec_new}, which supports primitive recursion, or using the more general
-\keyw{fun} and \keyw{function} commands. Here, the focus is on @{command
+Recursive functions over datatypes can be specified using the @{command
+primrec_new} command, which supports primitive recursion, or using the more
+general \keyw{fun} and \keyw{function} commands. Here, the focus is on @{command
primrec_new}; the other two commands are described in a separate tutorial
\cite{isabelle-function}.
@@ -1026,9 +1098,24 @@
text {*
\noindent
-The next example is not primitive recursive, but it can be defined easily using
-\keyw{fun}. The @{command datatype_new_compat} command is needed to register
-new-style datatypes for use with \keyw{fun} and \keyw{function}
+Pattern matching is only available for the argument on which the recursion takes
+place. Fortunately, it is easy to generate pattern-maching equations using the
+\keyw{simps\_of\_case} command provided by the theory
+\verb|~~/src/HOL/Library/Simps_Case_Conv|.
+*}
+
+ simps_of_case at_simps: at.simps
+
+text {*
+This generates the lemma collection @{thm [source] at_simps}:
+%
+\[@{thm at_simps(1)[no_vars]}
+ \qquad @{thm at_simps(2)[no_vars]}\]
+%
+The next example is defined using \keyw{fun} to escape the syntactic
+restrictions imposed on primitive recursive functions. The
+@{command datatype_new_compat} command is needed to register new-style datatypes
+for use with \keyw{fun} and \keyw{function}
(Section~\ref{sssec:datatype-new-compat}):
*}
@@ -1109,13 +1196,13 @@
\noindent
The next example features recursion through the @{text option} type. Although
@{text option} is not a new-style datatype, it is registered as a BNF with the
-map function @{const option_map}:
+map function @{const map_option}:
*}
primrec_new (*<*)(in early) (*>*)sum_btree :: "('a\{zero,plus}) btree \ 'a" where
"sum_btree (BNode a lt rt) =
- a + the_default 0 (option_map sum_btree lt) +
- the_default 0 (option_map sum_btree rt)"
+ a + the_default 0 (map_option sum_btree lt) +
+ the_default 0 (map_option sum_btree rt)"
text {*
\noindent
@@ -1124,28 +1211,51 @@
(@{text \}) is simply composition (@{text "op \"}):
*}
- primrec_new (*<*)(in early) (*>*)ftree_map :: "('a \ 'a) \ 'a ftree \ 'a ftree" where
- "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
- "ftree_map f (FTNode g) = FTNode (ftree_map f \ g)"
+ primrec_new (*<*)(in early) (*>*)relabel_ft :: "('a \ 'a) \ 'a ftree \ 'a ftree" where
+ "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
+ "relabel_ft f (FTNode g) = FTNode (relabel_ft f \ g)"
text {*
\noindent
-(No such map function is defined by the package because the type
-variable @{typ 'a} is dead in @{typ "'a ftree"}.)
-
-Using \keyw{fun} or \keyw{function}, recursion through functions can be
-expressed using $\lambda$-expressions and function application rather
-than through composition. For example:
+For convenience, recursion through functions can also be expressed using
+$\lambda$-abstractions and function application rather than through composition.
+For example:
*}
- datatype_new_compat ftree
+ primrec_new relabel_ft :: "('a \ 'a) \ 'a ftree \ 'a ftree" where
+ "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
+ "relabel_ft f (FTNode g) = FTNode (\x. relabel_ft f (g x))"
text {* \blankline *}
- function ftree_map :: "('a \ 'a) \ 'a ftree \ 'a ftree" where
- "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
- "ftree_map f (FTNode g) = FTNode (\x. ftree_map f (g x))"
- by auto (metis ftree.exhaust)
+ primrec_new subtree_ft :: "'a \ 'a ftree \ 'a ftree" where
+ "subtree_ft x (FTNode g) = g x"
+
+text {*
+\noindent
+For recursion through curried $n$-ary functions, $n$ applications of
+@{term "op \"} are necessary. The examples below illustrate the case where
+$n = 2$:
+*}
+
+ datatype_new 'a ftree2 = FTLeaf2 'a | FTNode2 "'a \ 'a \ 'a ftree2"
+
+text {* \blankline *}
+
+ primrec_new (*<*)(in early) (*>*)relabel_ft2 :: "('a \ 'a) \ 'a ftree2 \ 'a ftree2" where
+ "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)" |
+ "relabel_ft2 f (FTNode2 g) = FTNode2 (op \ (op \ (relabel_ft2 f)) g)"
+
+text {* \blankline *}
+
+ primrec_new relabel_ft2 :: "('a \ 'a) \ 'a ftree2 \ 'a ftree2" where
+ "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)" |
+ "relabel_ft2 f (FTNode2 g) = FTNode2 (\x y. relabel_ft2 f (g x y))"
+
+text {* \blankline *}
+
+ primrec_new subtree_ft2 :: "'a \ 'a \ 'a ftree2 \ 'a ftree2" where
+ "subtree_ft2 x y (FTNode2 g) = g x y"
subsubsection {* Nested-as-Mutual Recursion
@@ -1177,12 +1287,12 @@
text {*
\noindent
-Appropriate induction principles are generated under the names
+Appropriate induction rules are generated as
@{thm [source] at\<^sub>f\<^sub>f.induct},
@{thm [source] ats\<^sub>f\<^sub>f.induct}, and
-@{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}.
-
-%%% TODO: Add recursors.
+@{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}. The
+induction rules and the underlying recursors are generated on a per-need basis
+and are kept in a cache to speed up subsequent definitions.
Here is a second example:
*}
@@ -1340,7 +1450,7 @@
\begin{itemize}
\setlength{\itemsep}{0pt}
-\item \emph{Theorems sometimes have different names.}
+\item \emph{Some theorems have different names.}
For $m > 1$ mutually recursive functions,
@{text "f\<^sub>1_\_f\<^sub>m.simps"} has been broken down into separate
subcollections @{text "f\<^sub>i.simps"}.
@@ -1415,7 +1525,7 @@
text {*
\noindent
Notice that the @{const cont} selector is associated with both @{const Skip}
-and @{const Choice}.
+and @{const Action}.
*}
@@ -1488,9 +1598,9 @@
\begin{itemize}
\setlength{\itemsep}{0pt}
-\item \relax{Coiterator}: @{text t_unfold}
-
-\item \relax{Corecursor}: @{text t_corec}
+\item \relax{Coiterator}: @{text unfold_t}
+
+\item \relax{Corecursor}: @{text corec_t}
\end{itemize}
*}
@@ -1606,10 +1716,10 @@
\label{sec:defining-corecursive-functions} *}
text {*
-Corecursive functions can be specified using @{command primcorec} and
-@{command primcorecursive}, which support primitive corecursion, or using the
-more general \keyw{partial\_function} command. Here, the focus is on
-the former two. More examples can be found in the directory
+Corecursive functions can be specified using the @{command primcorec} and
+\keyw{prim\-corec\-ursive} commands, which support primitive corecursion, or
+using the more general \keyw{partial\_function} command. Here, the focus is on
+the first two. More examples can be found in the directory
\verb|~~/src/HOL/BNF/Examples|.
Whereas recursive functions consume datatypes one constructor at a time,
@@ -1630,7 +1740,7 @@
This style is popular in the coalgebraic literature.
\item The \emph{constructor view} specifies $f$ by equations of the form
-\[@{text "\ \ f x\<^sub>1 \ x\<^sub>n = C \"}\]
+\[@{text "\ \ f x\<^sub>1 \ x\<^sub>n = C\<^sub>j \"}\]
This style is often more concise than the previous one.
\item The \emph{code view} specifies $f$ by a single equation of the form
@@ -1643,14 +1753,6 @@
All three styles are available as input syntax. Whichever syntax is chosen,
characteristic theorems for all three styles are generated.
-\begin{framed}
-\noindent
-\textbf{Warning:}\enskip The @{command primcorec} and @{command primcorecursive}
-commands are under development. Some of the functionality described here is
-vaporware. An alternative is to define corecursive functions directly using the
-generated @{text t_unfold} or @{text t_corec} combinators.
-\end{framed}
-
%%% TODO: partial_function? E.g. for defining tail recursive function on lazy
%%% lists (cf. terminal0 in TLList.thy)
*}
@@ -1668,11 +1770,6 @@
present the same examples expressed using the constructor and destructor views.
*}
-(*<*)
- locale code_view
- begin
-(*>*)
-
subsubsection {* Simple Corecursion
\label{sssec:primcorec-simple-corecursion} *}
@@ -1683,19 +1780,19 @@
*}
primcorec literate :: "('a \ 'a) \ 'a \ 'a llist" where
- "literate f x = LCons x (literate f (f x))"
+ "literate g x = LCons x (literate g (g x))"
text {* \blankline *}
primcorec siterate :: "('a \ 'a) \ 'a \ 'a stream" where
- "siterate f x = SCons x (siterate f (f x))"
+ "siterate g x = SCons x (siterate g (g x))"
text {*
\noindent
The constructor ensures that progress is made---i.e., the function is
\emph{productive}. The above functions compute the infinite lazy list or stream
-@{text "[x, f x, f (f x), \]"}. Productivity guarantees that prefixes
-@{text "[x, f x, f (f x), \, (f ^^ k) x]"} of arbitrary finite length
+@{text "[x, g x, g (g x), \]"}. Productivity guarantees that prefixes
+@{text "[x, g x, g (g x), \, (g ^^ k) x]"} of arbitrary finite length
@{text k} can be computed by unfolding the code equation a finite number of
times.
@@ -1714,7 +1811,7 @@
appear around constructors that guard corecursive calls:
*}
- primcorec_notyet lappend :: "'a llist \ 'a llist \ 'a llist" where
+ primcorec lappend :: "'a llist \ 'a llist \ 'a llist" where
"lappend xs ys =
(case xs of
LNil \ ys
@@ -1722,6 +1819,19 @@
text {*
\noindent
+Pattern matching is not supported by @{command primcorec}. Fortunately, it is
+easy to generate pattern-maching equations using the \keyw{simps\_of\_case}
+command provided by the theory \verb|~~/src/HOL/Library/Simps_Case_Conv|.
+*}
+
+ simps_of_case lappend_simps: lappend.code
+
+text {*
+This generates the lemma collection @{thm [source] lappend_simps}:
+%
+\[@{thm lappend_simps(1)[no_vars]}
+ \qquad @{thm lappend_simps(2)[no_vars]}\]
+%
Corecursion is useful to specify not only functions but also infinite objects:
*}
@@ -1735,7 +1845,7 @@
pseudorandom seed (@{text n}):
*}
- primcorec_notyet
+ primcorec
random_process :: "'a stream \ (int \ int) \ int \ 'a process"
where
"random_process s f n =
@@ -1780,43 +1890,71 @@
The next pair of examples generalize the @{const literate} and @{const siterate}
functions (Section~\ref{sssec:primcorec-nested-corecursion}) to possibly
infinite trees in which subnodes are organized either as a lazy list (@{text
-tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}):
+tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}). They rely on the map functions of
+the nesting type constructors to lift the corecursive calls:
*}
primcorec iterate\<^sub>i\<^sub>i :: "('a \ 'a llist) \ 'a \ 'a tree\<^sub>i\<^sub>i" where
- "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i f) (f x))"
+ "iterate\<^sub>i\<^sub>i g x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i g) (g x))"
text {* \blankline *}
primcorec iterate\<^sub>i\<^sub>s :: "('a \ 'a fset) \ 'a \ 'a tree\<^sub>i\<^sub>s" where
- "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fimage (iterate\<^sub>i\<^sub>s f) (f x))"
+ "iterate\<^sub>i\<^sub>s g x = Node\<^sub>i\<^sub>s x (fimage (iterate\<^sub>i\<^sub>s g) (g x))"
text {*
\noindent
-Deterministic finite automata (DFAs) are traditionally defined as 5-tuples
-@{text "(Q, \, \, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,
+Both examples follow the usual format for constructor arguments associated
+with nested recursive occurrences of the datatype. Consider
+@{const iterate\<^sub>i\<^sub>i}. The term @{term "g x"} constructs an @{typ "'a llist"}
+value, which is turned into an @{typ "'a tree\<^sub>i\<^sub>i llist"} value using
+@{const lmap}.
+
+This format may sometimes feel artificial. The following function constructs
+a tree with a single, infinite branch from a stream:
+*}
+
+ primcorec tree\<^sub>i\<^sub>i_of_stream :: "'a stream \ 'a tree\<^sub>i\<^sub>i" where
+ "tree\<^sub>i\<^sub>i_of_stream s =
+ Node\<^sub>i\<^sub>i (shd s) (lmap tree\<^sub>i\<^sub>i_of_stream (LCons (stl s) LNil))"
+
+text {*
+\noindent
+Fortunately, it is easy to prove the following lemma, where the corecursive call
+is moved inside the lazy list constructor, thereby eliminating the need for
+@{const lmap}:
+*}
+
+ lemma tree\<^sub>i\<^sub>i_of_stream_alt:
+ "tree\<^sub>i\<^sub>i_of_stream s = Node\<^sub>i\<^sub>i (shd s) (LCons (tree\<^sub>i\<^sub>i_of_stream (stl s)) LNil)"
+ by (subst tree\<^sub>i\<^sub>i_of_stream.code) simp
+
+text {*
+The next example illustrates corecursion through functions, which is a bit
+special. Deterministic finite automata (DFAs) are traditionally defined as
+5-tuples @{text "(Q, \, \, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,
@{text \} is a finite alphabet, @{text \} is a transition function, @{text q\<^sub>0}
is an initial state, and @{text F} is a set of final states. The following
function translates a DFA into a @{type state_machine}:
*}
- primcorec (*<*)(in early) (*>*)
- sm_of_dfa :: "('q \ 'a \ 'q) \ 'q set \ 'q \ 'a state_machine"
+ primcorec
+ (*<*)(in early) (*>*)sm_of_dfa :: "('q \ 'a \ 'q) \ 'q set \ 'q \ 'a state_machine"
where
- "sm_of_dfa \ F q = State_Machine (q \ F) (sm_of_dfa \ F o \ q)"
+ "sm_of_dfa \ F q = State_Machine (q \ F) (sm_of_dfa \ F \ \ q)"
text {*
\noindent
The map function for the function type (@{text \}) is composition
-(@{text "op \"}). For convenience, corecursion through functions can be
-expressed using $\lambda$-expressions and function application rather
+(@{text "op \"}). For convenience, corecursion through functions can
+also be expressed using $\lambda$-abstractions and function application rather
than through composition. For example:
*}
primcorec
sm_of_dfa :: "('q \ 'a \ 'q) \ 'q set \ 'q \ 'a state_machine"
where
- "sm_of_dfa \ F q = State_Machine (q \ F) (sm_of_dfa \ F o \ q)"
+ "sm_of_dfa \ F q = State_Machine (q \ F) (\a. sm_of_dfa \ F (\ q a))"
text {* \blankline *}
@@ -1833,9 +1971,32 @@
primcorec
or_sm :: "'a state_machine \ 'a state_machine \ 'a state_machine"
where
- "or_sm M N =
- State_Machine (accept M \ accept N)
- (\a. or_sm (trans M a) (trans N a))"
+ "or_sm M N = State_Machine (accept M \ accept N)
+ (\a. or_sm (trans M a) (trans N a))"
+
+text {*
+\noindent
+For recursion through curried $n$-ary functions, $n$ applications of
+@{term "op \"} are necessary. The examples below illustrate the case where
+$n = 2$:
+*}
+
+ codatatype ('a, 'b) state_machine2 =
+ State_Machine2 (accept2: bool) (trans2: "'a \ 'b \ ('a, 'b) state_machine2")
+
+text {* \blankline *}
+
+ primcorec
+ (*<*)(in early) (*>*)sm2_of_dfa :: "('q \ 'a \ 'b \ 'q) \ 'q set \ 'q \ ('a, 'b) state_machine2"
+ where
+ "sm2_of_dfa \ F q = State_Machine2 (q \ F) (op \ (op \ (sm2_of_dfa \ F)) (\ q))"
+
+text {* \blankline *}
+
+ primcorec
+ sm2_of_dfa :: "('q \ 'a \ 'b \ 'q) \ 'q set \ 'q \ ('a, 'b) state_machine2"
+ where
+ "sm2_of_dfa \ F q = State_Machine2 (q \ F) (\a b. sm2_of_dfa \ F (\ q a b))"
subsubsection {* Nested-as-Mutual Corecursion
@@ -1848,15 +2009,31 @@
pretend that nested codatatypes are mutually corecursive. For example:
*}
- primcorec_notyet
+(*<*)
+ context late
+ begin
+(*>*)
+ primcorec
iterate\<^sub>i\<^sub>i :: "('a \ 'a llist) \ 'a \ 'a tree\<^sub>i\<^sub>i" and
iterates\<^sub>i\<^sub>i :: "('a \ 'a llist) \ 'a llist \ 'a tree\<^sub>i\<^sub>i llist"
where
- "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (iterates\<^sub>i\<^sub>i f (f x))" |
- "iterates\<^sub>i\<^sub>i f xs =
+ "iterate\<^sub>i\<^sub>i g x = Node\<^sub>i\<^sub>i x (iterates\<^sub>i\<^sub>i g (g x))" |
+ "iterates\<^sub>i\<^sub>i g xs =
(case xs of
LNil \ LNil
- | LCons x xs' \ LCons (iterate\<^sub>i\<^sub>i f x) (iterates\<^sub>i\<^sub>i f xs'))"
+ | LCons x xs' \ LCons (iterate\<^sub>i\<^sub>i g x) (iterates\<^sub>i\<^sub>i g xs'))"
+
+text {*
+\noindent
+Coinduction rules are generated as
+@{thm [source] iterate\<^sub>i\<^sub>i.coinduct},
+@{thm [source] iterates\<^sub>i\<^sub>i.coinduct}, and
+@{thm [source] iterate\<^sub>i\<^sub>i_iterates\<^sub>i\<^sub>i.coinduct}
+and analogously for @{text strong_coinduct}. These rules and the
+underlying corecursors are generated on a per-need basis and are kept in a cache
+to speed up subsequent definitions.
+*}
+
(*<*)
end
(*>*)
@@ -1866,7 +2043,7 @@
\label{ssec:primrec-constructor-view} *}
(*<*)
- locale ctr_view = code_view
+ locale ctr_view
begin
(*>*)
@@ -1937,7 +2114,7 @@
\label{ssec:primrec-destructor-view} *}
(*<*)
- locale dest_view
+ locale dtr_view
begin
(*>*)
@@ -1951,13 +2128,13 @@
primcorec literate :: "('a \ 'a) \ 'a \ 'a llist" where
"\ lnull (literate _ x)" |
"lhd (literate _ x) = x" |
- "ltl (literate f x) = literate f (f x)"
+ "ltl (literate g x) = literate g (g x)"
text {* \blankline *}
primcorec siterate :: "('a \ 'a) \ 'a \ 'a stream" where
"shd (siterate _ x) = x" |
- "stl (siterate f x) = siterate f (f x)"
+ "stl (siterate g x) = siterate g (g x)"
text {* \blankline *}
@@ -1993,6 +2170,9 @@
(*<*)
end
+ locale dtr_view2
+ begin
+
primcorec lappend :: "'a llist \ 'a llist \ 'a llist" where
"lnull xs \ lnull ys \ lnull (lappend xs ys)" |
(*>*)
@@ -2000,8 +2180,6 @@
(*<*) |
"lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
"ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
-
- context dest_view begin
(*>*)
text {*
@@ -2044,8 +2222,8 @@
text {* \blankline *}
primcorec iterate\<^sub>i\<^sub>i :: "('a \ 'a llist) \ 'a \ 'a tree\<^sub>i\<^sub>i" where
- "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = x" |
- "sub\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = lmap (iterate\<^sub>i\<^sub>i f) (f x)"
+ "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i g x) = x" |
+ "sub\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i g x) = lmap (iterate\<^sub>i\<^sub>i g) (g x)"
(*<*)
end
(*>*)
@@ -2148,11 +2326,39 @@
\end{matharray}
@{rail "
- @@{command bnf} target? (name ':')? term \\
- term_list term term_list term?
+ @@{command bnf} target? (name ':')? typ \\
+ 'map:' term ('sets:' (term +))? 'bd:' term \\
+ ('wits:' (term +))? ('rel:' term)?
+"}
+*}
+
+
+subsubsection {* \keyw{bnf\_decl}
+ \label{sssec:bnf-decl} *}
+
+text {*
+%%% TODO: use command_def once the command is available
+\begin{matharray}{rcl}
+ @{text "bnf_decl"} & : & @{text "local_theory \ local_theory"}
+\end{matharray}
+
+@{rail "
+ @@{command bnf_decl} target? @{syntax dt_name}
;
- X_list: '[' (X + ',') ']'
+ @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
+ ;
+ @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')'
+ ;
+ @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
"}
+
+Declares a fresh type and fresh constants (map, set, relator, cardinal bound)
+and asserts the bnf properties for these constants as axioms. Additionally,
+type arguments may be marked as dead (by using @{syntax "-"} instead of a name for the
+set function)---this is the only difference of @{syntax dt_name} compared to
+the syntax used by the @{command datatype_new}/@{command codatatype} commands.
+
+The axioms are sound, since one there exists a bnf of any given arity.
*}
@@ -2185,8 +2391,10 @@
% old \keyw{datatype}
%
% * @{command wrap_free_constructors}
-% * @{text "no_discs_sels"}, @{text "rep_compat"}
+% * @{text "no_discs_sels"}, @{text "no_code"}, @{text "rep_compat"}
% * hack to have both co and nonco view via locale (cf. ext nats)
+% * code generator
+% * eq, refl, simps
*}
@@ -2215,11 +2423,11 @@
@{syntax_def wfc_discs_sels}: name_list (name_list_list name_term_list_list? )?
;
@{syntax_def name_term}: (name ':' term)
+ ;
+ X_list: '[' (X + ',') ']'
"}
-% options: no_discs_sels rep_compat
-
-% X_list is as for BNF
+% options: no_discs_sels no_code rep_compat
\noindent
Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
@@ -2307,8 +2515,9 @@
suggested major simplifications to the internal constructions, much of which has
yet to be implemented. Florian Haftmann and Christian Urban provided general
advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder
-found an elegant proof to eliminate one of the BNF assumptions. Christian
-Sternagel suggested many textual improvements to this tutorial.
+found an elegant proof to eliminate one of the BNF assumptions. Andreas
+Lochbihler and Christian Sternagel suggested many textual improvements to this
+tutorial.
*}
end
diff -r cfb21e03fe2a -r d64a4ef26edb src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex Thu Dec 05 17:52:12 2013 +0100
+++ b/src/Doc/Datatypes/document/root.tex Thu Dec 05 17:58:03 2013 +0100
@@ -58,10 +58,10 @@
\begin{abstract}
\noindent
-This tutorial describes how to use the new package for defining datatypes and
-codatatypes in Isabelle/HOL. The package provides five main commands:
+This tutorial describes the new package for defining datatypes and codatatypes
+in Isabelle/HOL. The package provides four main commands:
\keyw{datatype\_new}, \keyw{codatatype}, \keyw{primrec\_new},
-\keyw{primcorecursive}, and \keyw{primcorec}. The commands suffixed by
+and \keyw{primcorec}. The commands suffixed by
\keyw{\_new} are intended to subsume, and eventually replace, the corresponding
commands from the old datatype package.
\end{abstract}
diff -r cfb21e03fe2a -r d64a4ef26edb src/Doc/Functions/Functions.thy
--- a/src/Doc/Functions/Functions.thy Thu Dec 05 17:52:12 2013 +0100
+++ b/src/Doc/Functions/Functions.thy Thu Dec 05 17:58:03 2013 +0100
@@ -1003,13 +1003,13 @@
recursive calls. In general, there is one introduction rule for each
recursive call.
- The predicate @{term "accp findzero_rel"} is the accessible part of
+ The predicate @{term "Wellfounded.accp findzero_rel"} is the accessible part of
that relation. An argument belongs to the accessible part, if it can
be reached in a finite number of steps (cf.~its definition in @{text
"Wellfounded.thy"}).
Since the domain predicate is just an abbreviation, you can use
- lemmas for @{const accp} and @{const findzero_rel} directly. Some
+ lemmas for @{const Wellfounded.accp} and @{const findzero_rel} directly. Some
lemmas which are occasionally useful are @{thm [source] accpI}, @{thm [source]
accp_downward}, and of course the introduction and elimination rules
for the recursion relation @{thm [source] "findzero_rel.intros"} and @{thm
diff -r cfb21e03fe2a -r d64a4ef26edb src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy Thu Dec 05 17:52:12 2013 +0100
+++ b/src/Doc/IsarImplementation/ML.thy Thu Dec 05 17:58:03 2013 +0100
@@ -1033,7 +1033,7 @@
without any message output.
\begin{warn}
- The actual error channel is accessed via @{ML Output.error_msg}, but
+ The actual error channel is accessed via @{ML Output.error_message}, but
the old interaction protocol of Proof~General \emph{crashes} if that
function is used in regular ML code: error output and toplevel
command failure always need to coincide in classic TTY interaction.
diff -r cfb21e03fe2a -r d64a4ef26edb src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy Thu Dec 05 17:52:12 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy Thu Dec 05 17:58:03 2013 +0100
@@ -1068,12 +1068,6 @@
text {*
\begin{itemize}
- \item \textbf{Problem:} Lack of dependency management for auxiliary files
- that contribute to a theory (e.g.\ @{command ML_file}).
-
- \textbf{Workaround:} Re-load files manually within the prover, by
- editing corresponding command in the text.
-
\item \textbf{Problem:} Odd behavior of some diagnostic commands with
global side-effects, like writing a physical file.
diff -r cfb21e03fe2a -r d64a4ef26edb src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex Thu Dec 05 17:52:12 2013 +0100
+++ b/src/Doc/Nitpick/document/root.tex Thu Dec 05 17:58:03 2013 +0100
@@ -1965,6 +1965,8 @@
\texttt{.kki}, \texttt{.cnf}, \texttt{.out}, and
\texttt{.err}; you may safely remove them after Nitpick has run.
+\textbf{Warning:} This option is not thread-safe. Use at your own risks.
+
\nopagebreak
{\small See also \textit{debug} (\S\ref{output-format}).}
\end{enum}
@@ -2382,6 +2384,14 @@
\cite{kodkod-2009}. Unlike the standard version of MiniSat, the JNI version can
be used incrementally.
+\item[\labelitemi] \textbf{\textit{Riss3g}:} Riss3g is an efficient solver written in
+\cpp{}. To use Riss3g, set the environment variable \texttt{RISS3G\_HOME} to the
+directory that contains the \texttt{riss3g} executable.%
+\footref{cygwin-paths}
+The \cpp{} sources for Riss3g are available at
+\url{http://tools.computational-logic.org/content/riss3g.php}.
+Nitpick has been tested with the SAT Competition 2013 version.
+
\item[\labelitemi] \textbf{\textit{zChaff}:} zChaff is an older solver written
in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
the directory that contains the \texttt{zchaff} executable.%
@@ -2794,11 +2804,12 @@
\subsection{Registering Coinductive Datatypes}
\label{registering-coinductive-datatypes}
+Coinductive datatypes defined using the \textbf{codatatype} command that do not
+involve nested recursion through non-codatatypes are supported by Nitpick.
If you have defined a custom coinductive datatype, you can tell Nitpick about
-it, so that it can use an efficient Kodkod axiomatization similar to the one it
-uses for lazy lists. The interface for registering and unregistering coinductive
-datatypes consists of the following pair of functions defined in the
-\textit{Nitpick\_HOL} structure:
+it, so that it can use an efficient Kodkod axiomatization. The interface for
+registering and unregistering coinductive datatypes consists of the following
+pair of functions defined in the \textit{Nitpick\_HOL} structure:
\prew
$\textbf{val}\,~\textit{register\_codatatype\/} : {}$ \\
@@ -2886,6 +2897,12 @@
\item[\labelitemi] Nitpick produces spurious counterexamples when invoked after a
\textbf{guess} command in a structured proof.
+\item[\labelitemi] Datatypes defined using \textbf{datatype\_new} are not
+supported.
+
+\item[\labelitemi] Codatatypes defined using \textbf{codatatype} that
+involve nested recursion through non-codatatypes are not supported.
+
\item[\labelitemi] The \textit{nitpick\_xxx} attributes and the
\textit{Nitpick\_xxx.register\_yyy} functions can cause havoc if used
improperly.
diff -r cfb21e03fe2a -r d64a4ef26edb src/Doc/ProgProve/Basics.thy
--- a/src/Doc/ProgProve/Basics.thy Thu Dec 05 17:52:12 2013 +0100
+++ b/src/Doc/ProgProve/Basics.thy Thu Dec 05 17:58:03 2013 +0100
@@ -22,8 +22,8 @@
\item[type constructors,]
in particular @{text list}, the type of
lists, and @{text set}, the type of sets. Type constructors are written
-postfix, e.g.\ @{typ "nat list"} is the type of lists whose elements are
-natural numbers.
+postfix, i.e., after their arguments. For example,
+@{typ "nat list"} is the type of lists whose elements are natural numbers.
\item[function types,]
denoted by @{text"\"}.
\item[type variables,]
@@ -41,8 +41,8 @@
\begin{warn}
There are many predefined infix symbols like @{text "+"} and @{text"\"}.
The name of the corresponding binary function is @{term"op +"},
-not just @{text"+"}. That is, @{term"x + y"} is syntactic sugar for
-\noquotes{@{term[source]"op + x y"}}.
+not just @{text"+"}. That is, @{term"x + y"} is nice surface syntax
+(``syntactic sugar'') for \noquotes{@{term[source]"op + x y"}}.
\end{warn}
HOL also supports some basic constructs from functional programming:
diff -r cfb21e03fe2a -r d64a4ef26edb src/Doc/ProgProve/Bool_nat_list.thy
--- a/src/Doc/ProgProve/Bool_nat_list.thy Thu Dec 05 17:52:12 2013 +0100
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Thu Dec 05 17:58:03 2013 +0100
@@ -99,10 +99,10 @@
For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate
that you are talking about natural numbers. Hence Isabelle can only infer
that @{term x} is of some arbitrary type where @{text 0} and @{text"+"}
- exist. As a consequence, you will be unable to prove the
- goal. To alert you to such pitfalls, Isabelle flags numerals without a
- fixed type in its output: @{prop"x+0 = x"}. In this particular example,
- you need to include
+ exist. As a consequence, you will be unable to prove the goal.
+% To alert you to such pitfalls, Isabelle flags numerals without a
+% fixed type in its output: @ {prop"x+0 = x"}.
+ In this particular example, you need to include
an explicit type constraint, for example @{text"x+0 = (x::nat)"}. If there
is enough contextual information this may not be necessary: @{prop"Suc x =
x"} automatically implies @{text"x::nat"} because @{term Suc} is not
@@ -372,10 +372,10 @@
ys zs)"}. It appears almost mysterious because we suddenly complicate the
term by appending @{text Nil} on the left. What is really going on is this:
when proving some equality \mbox{@{prop"s = t"}}, both @{text s} and @{text t} are
-simplified to some common term @{text u}. This heuristic for equality proofs
+simplified until they ``meet in the middle''. This heuristic for equality proofs
works well for a functional programming context like ours. In the base case
-@{text s} is @{term"app (app Nil ys) zs"}, @{text t} is @{term"app Nil (app
-ys zs)"}, and @{text u} is @{term"app ys zs"}.
+both @{term"app (app Nil ys) zs"} and @{term"app Nil (app
+ys zs)"} are simplified to @{term"app ys zs"}, the term in the middle.
\subsection{Predefined Lists}
\label{sec:predeflists}
@@ -419,13 +419,19 @@
From now on lists are always the predefined lists.
-\subsection{Exercises}
+\subsection*{Exercises}
+
+\begin{exercise}
+Use the \isacom{value} command to evaluate the following expressions:
+@{term[source] "1 + (2::nat)"}, @{term[source] "1 + (2::int)"},
+@{term[source] "1 - (2::nat)"} and @{term[source] "1 - (2::int)"}.
+\end{exercise}
\begin{exercise}
Start from the definition of @{const add} given above.
-Prove it is associative (@{prop"add (add m n) p = add m (add n p)"})
-and commutative (@{prop"add m n = add n m"}). Define a recursive function
-@{text double} @{text"::"} @{typ"nat \ nat"} and prove that @{prop"double m = add m m"}.
+Prove that @{const add} is associative and commutative.
+Define a recursive function @{text double} @{text"::"} @{typ"nat \ nat"}
+and prove @{prop"double m = add m m"}.
\end{exercise}
\begin{exercise}
@@ -436,11 +442,15 @@
\begin{exercise}
Define a recursive function @{text "snoc ::"} @{typ"'a list \ 'a \ 'a list"}
-that appends an element to the end of a list. Do not use the predefined append
-operator @{text"@"}. With the help of @{text snoc} define a recursive function
-@{text "reverse ::"} @{typ"'a list \ 'a list"} that reverses a list. Do not
-use the predefined function @{const rev}.
-Prove @{prop"reverse(reverse xs) = xs"}.
+that appends an element to the end of a list. With the help of @{text snoc}
+define a recursive function @{text "reverse ::"} @{typ"'a list \ 'a list"}
+that reverses a list. Prove @{prop"reverse(reverse xs) = xs"}.
+\end{exercise}
+
+\begin{exercise}
+Define a recursive function @{text "sum ::"} @{typ"nat \ nat"} such that
+\mbox{@{text"sum n"}} @{text"="} @{text"0 + ... + n"} and prove
+@{prop" sum(n::nat) = n * (n+1) div 2"}.
\end{exercise}
*}
(*<*)
diff -r cfb21e03fe2a -r d64a4ef26edb src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy Thu Dec 05 17:52:12 2013 +0100
+++ b/src/Doc/ProgProve/Isar.thy Thu Dec 05 17:58:03 2013 +0100
@@ -590,15 +590,15 @@
the fact just proved, in this case the preceding block. In general,
\isacom{note} introduces a new name for one or more facts.
-\subsection{Exercises}
+\subsection*{Exercises}
\exercise
Give a readable, structured proof of the following lemma:
*}
-lemma assumes T: "\ x y. T x y \ T y x"
- and A: "\ x y. A x y \ A y x \ x = y"
- and TA: "\ x y. T x y \ A x y" and "A x y"
-shows "T x y"
+lemma assumes T: "\x y. T x y \ T y x"
+ and A: "\x y. A x y \ A y x \ x = y"
+ and TA: "\x y. T x y \ A x y" and "A x y"
+ shows "T x y"
(*<*)oops(*>*)
text{*
\endexercise
@@ -612,10 +612,11 @@
text{*
Hint: There are predefined functions @{const_typ take} and @{const_typ drop}
such that @{text"take k [x\<^sub>1,\] = [x\<^sub>1,\,x\<^sub>k]"} and
-@{text"drop k [x\<^sub>1,\] = [x\<^bsub>k+1\<^esub>,\]"}. Let @{text simp} and especially
-sledgehammer find and apply the relevant @{const take} and @{const drop} lemmas for you.
+@{text"drop k [x\<^sub>1,\] = [x\<^bsub>k+1\<^esub>,\]"}. Let sledgehammer find and apply
+the relevant @{const take} and @{const drop} lemmas for you.
\endexercise
+
\section{Case Analysis and Induction}
\subsection{Datatype Case Analysis}
@@ -1018,7 +1019,7 @@
\isacom{lemma} @{text[source]"I r s t \ \"}
\end{isabelle}
Applying the standard form of
-rule induction in such a situation will lead to strange and typically unproveable goals.
+rule induction in such a situation will lead to strange and typically unprovable goals.
We can easily reduce this situation to the standard one by introducing
new variables @{text x}, @{text y}, @{text z} and reformulating the goal like this:
\begin{isabelle}
@@ -1040,7 +1041,7 @@
proof(induction "Suc m" arbitrary: m rule: ev.induct)
fix n assume IH: "\m. n = Suc m \ \ ev m"
show "\ ev (Suc n)"
- proof --"contradition"
+ proof --"contradiction"
assume "ev(Suc n)"
thus False
proof cases --"rule inversion"
@@ -1075,45 +1076,38 @@
@{text induct} method.
\end{warn}
-\subsection{Exercises}
+
+\subsection*{Exercises}
+
+
+\exercise
+Give a structured proof by rule inversion:
+*}
+
+lemma assumes a: "ev(Suc(Suc n))" shows "ev n"
+(*<*)oops(*>*)
+
+text{*
+\endexercise
+
+\begin{exercise}
+Give a structured proof of @{prop "\ ev(Suc(Suc(Suc 0)))"}
+by rule inversions. If there are no cases to be proved you can close
+a proof immediateley with \isacom{qed}.
+\end{exercise}
+
+\begin{exercise}
+Recall predicate @{text star} from \autoref{sec:star} and @{text iter}
+from Exercise~\ref{exe:iter}. Prove @{prop "iter r n x y \ star r x y"}
+in a structured style, do not just sledgehammer each case of the
+required induction.
+\end{exercise}
\begin{exercise}
Define a recursive function @{text "elems ::"} @{typ"'a list \ 'a set"}
and prove @{prop "x : elems xs \ \ys zs. xs = ys @ x # zs \ x \ elems ys"}.
\end{exercise}
-
-\begin{exercise}
-A context-free grammar can be seen as an inductive definition where each
-nonterminal $A$ is an inductively defined predicate on lists of terminal
-symbols: $A(w)$ mans
-that $w$ is in the language generated by $A$. For example, the production $S
-\to a S b$ can be viewed as the implication @{prop"S w \ S (a # w @ [b])"}
-where @{text a} and @{text b} are constructors of some datatype of terminal
-symbols: \isacom{datatype} @{text"tsymbs = a | b | \"}
-
-Define the two grammars
-\[
-\begin{array}{r@ {\quad}c@ {\quad}l}
-S &\to& \varepsilon \quad\mid\quad a~S~b \quad\mid\quad S~S \\
-T &\to& \varepsilon \quad\mid\quad T~a~T~b
-\end{array}
-\]
-($\varepsilon$ is the empty word)
-as two inductive predicates and prove @{prop"S w \ T w"}.
-\end{exercise}
-
*}
-(*
-lemma "\ ev(Suc(Suc(Suc 0)))"
-proof
- assume "ev(Suc(Suc(Suc 0)))"
- then show False
- proof cases
- case evSS
- from `ev(Suc 0)` show False by cases
- qed
-qed
-*)
(*<*)
end
diff -r cfb21e03fe2a -r d64a4ef26edb src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy Thu Dec 05 17:52:12 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy Thu Dec 05 17:58:03 2013 +0100
@@ -141,6 +141,28 @@
See \cite{Nipkow-Main} for the wealth of further predefined functions in theory
@{theory Main}.
+
+\subsection*{Exercises}
+
+\exercise
+Start from the data type of binary trees defined earlier:
+*}
+
+datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"
+
+text{*
+Define a function @{text "set ::"} @{typ "'a tree \ 'a set"}
+that returns the elements in a tree and a function
+@{text "ord ::"} @{typ "int tree \ bool"}
+the tests if an @{typ "int tree"} is ordered.
+
+Define a function @{text ins} that inserts an element into an ordered @{typ "int tree"}
+while maintaining the order of the tree. If the element is already in the tree, the
+same tree should be returned. Prove correctness of @{text ins}:
+@{prop "set(ins x t) = {x} \ set t"} and @{prop "ord t \ ord(ins i t)"}.
+\endexercise
+
+
\section{Proof Automation}
So far we have only seen @{text simp} and @{text auto}: Both perform
@@ -459,12 +481,12 @@
text{* In this particular example we could have backchained with
@{thm[source] Suc_leD}, too, but because the premise is more complicated than the conclusion this can easily lead to nontermination.
-\subsection{Finding Theorems}
-
-Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
-theory. Search criteria include pattern matching on terms and on names.
-For details see the Isabelle/Isar Reference Manual~\cite{IsarRef}.
-\bigskip
+%\subsection{Finding Theorems}
+%
+%Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
+%theory. Search criteria include pattern matching on terms and on names.
+%For details see the Isabelle/Isar Reference Manual~\cite{IsarRef}.
+%\bigskip
\begin{warn}
To ease readability we will drop the question marks
@@ -708,8 +730,8 @@
apply(rename_tac u x y)
defer
(*>*)
-txt{* The induction is over @{prop"star r x y"} and we try to prove
-\mbox{@{prop"star r y z \ star r x z"}},
+txt{* The induction is over @{prop"star r x y"} (the first matching assumption)
+and we try to prove \mbox{@{prop"star r y z \ star r x z"}},
which we abbreviate by @{prop"P x y"}. These are our two subgoals:
@{subgoals[display,indent=0]}
The first one is @{prop"P x x"}, the result of case @{thm[source]refl},
@@ -764,6 +786,95 @@
conditions}. In rule inductions, these side-conditions appear as additional
assumptions. The \isacom{for} clause seen in the definition of the reflexive
transitive closure merely simplifies the form of the induction rule.
+
+
+\subsection*{Exercises}
+
+\begin{exercise}
+Formalise the following definition of palindromes
+\begin{itemize}
+\item The empty list and a singleton list are palindromes.
+\item If @{text xs} is a palindrome, so is @{term "a # xs @ [a]"}.
+\end{itemize}
+as an inductive predicate @{text "palindrome ::"} @{typ "'a list \ bool"}
+and prove that @{prop "rev xs = xs"} if @{text xs} is a palindrome.
+\end{exercise}
+
+\exercise
+We could also have defined @{const star} as follows:
+*}
+
+inductive star' :: "('a \ 'a \ bool) \ 'a \ 'a \