# HG changeset patch # User wenzelm # Date 1273675559 -7200 # Node ID f99ae7e27150a562a84a5db88ecfd75b25854a8d # Parent b78d3c87fc889c5012b191a1c2e083272fe49f83# Parent 426d5781bb250abf895cd579d2d1f629719e01b4 merged diff -r b78d3c87fc88 -r f99ae7e27150 Admin/CHECKLIST --- a/Admin/CHECKLIST Wed May 12 15:25:23 2010 +0200 +++ b/Admin/CHECKLIST Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,7 @@ Checklist for official releases =============================== -- test mosml, polyml-5.2.1, polyml-5.2, polyml-5.1, polyml-5.0; +- test polyml-5.3.0, polyml-5.2.1, polyml-5.2, polyml-5.1, polyml-5.0; - test sparc-solaris, x86-solaris; @@ -19,6 +19,8 @@ - check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS; +- diff NEWS wrt. last official release, which is read-only; + - update https://isabelle.in.tum.de/repos/website; - maintain Docs: diff -r b78d3c87fc88 -r f99ae7e27150 Admin/Mercurial/convert --- a/Admin/Mercurial/convert Wed May 12 15:25:23 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -#!/bin/bash -# $Id$ - -THIS="$(cd "$(dirname "$0")"; pwd)" -SUPER="$(cd "$THIS/.."; pwd)" - -LOG="$THIS/log" -date >> "$LOG" - - -## cvs update - -cd "$THIS/cvs" -cvs up -dAP >> "$LOG" 2>&1 || exit 2 - - -## hg convert - -export HGRCPATH="$THIS/cvs/Admin/Mercurial/hgrc" - -cd "$THIS" -/home/isabelle/mercurial/bin/hg convert --filemap cvs/Admin/Mercurial/filemap cvs isabelle-cvs >> "$LOG" 2>&1 || exit 2 - -[ -e isabelle-cvs/.hg/hgrc ] || ln -s ../../cvs/Admin/Mercurial/hgrc isabelle-cvs/.hg/hgrc - - -## logrotate - -/usr/sbin/logrotate -s "$THIS/log.state" "$THIS/cvs/Admin/Mercurial/logrotate.conf" diff -r b78d3c87fc88 -r f99ae7e27150 Admin/Mercurial/filemap --- a/Admin/Mercurial/filemap Wed May 12 15:25:23 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ -rename Doc doc-src -exclude Distribution/bin/Isabelle -exclude Admin/page/main-content/PG-preview.mov -exclude Admin/website/media/pg_preview.mov -rename Distribution . -rename CCL src/CCL -rename CTT src/CTT -rename Cube src/Cube -rename FOL src/FOL -rename FOLP src/FOLP -rename HOL src/HOL -rename HOLCF src/HOLCF -rename LCF src/LCF -rename LK src/LK -rename Modal src/Modal -rename Provers src/Provers -rename Pure src/Pure -rename Sequents src/Sequents -rename Tools src/Tools -rename ZF src/ZF diff -r b78d3c87fc88 -r f99ae7e27150 Admin/Mercurial/hgrc --- a/Admin/Mercurial/hgrc Wed May 12 15:25:23 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -[extensions] -hgext.convert = - -[convert] -cvsps = /home/isabelle-repository/repos/cvsps-2.1-patched/cvsps -A -u --cvs-direct --norc -b HEAD - -[web] -style = isabelle -description = Snapshot of the old Isabelle CVS -allow_archive = gz -maxfiles = 50 diff -r b78d3c87fc88 -r f99ae7e27150 Admin/Mercurial/logrotate.conf --- a/Admin/Mercurial/logrotate.conf Wed May 12 15:25:23 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -# $Id$ - -/home/isabelle-repository/repos/log { - compress - nomail - daily - rotate 5 -} diff -r b78d3c87fc88 -r f99ae7e27150 Admin/README --- a/Admin/README Wed May 12 15:25:23 2010 +0200 +++ b/Admin/README Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,2 @@ - -$Id$ - This directory contains some administrative tools for the Isabelle repository at TUM. They do not appear in proper distributions. diff -r b78d3c87fc88 -r f99ae7e27150 Admin/check_ml_headers --- a/Admin/check_ml_headers Wed May 12 15:25:23 2010 +0200 +++ b/Admin/check_ml_headers Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ #!/usr/bin/env bash # -# $Id$ -# # check_ml_headers - check headers of *.ML files in Distribution for inconsistencies # # requires some GNU tools diff -r b78d3c87fc88 -r f99ae7e27150 Admin/isasync --- a/Admin/isasync Wed May 12 15:25:23 2010 +0200 +++ b/Admin/isasync Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ #!/usr/bin/env bash # -# $Id$ -# # mirror script for Isabelle distribution or website diff -r b78d3c87fc88 -r f99ae7e27150 Admin/linktest --- a/Admin/linktest Wed May 12 15:25:23 2010 +0200 +++ b/Admin/linktest Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ #!/usr/bin/env bash # -# $Id$ -# # leightweight link checker for the isabelle website diff -r b78d3c87fc88 -r f99ae7e27150 Admin/mirror-website --- a/Admin/mirror-website Wed May 12 15:25:23 2010 +0200 +++ b/Admin/mirror-website Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ #!/usr/bin/env bash # -# $Id$ -# # mirrors the Isabelle website HOST=$(hostname) diff -r b78d3c87fc88 -r f99ae7e27150 Admin/profiling_report --- a/Admin/profiling_report Wed May 12 15:25:23 2010 +0200 +++ b/Admin/profiling_report Wed May 12 16:45:59 2010 +0200 @@ -1,6 +1,5 @@ #!/usr/bin/env perl # -# $Id$ # Author: Makarius # # DESCRIPTION: Simple report generator for Poly/ML profiling output. diff -r b78d3c87fc88 -r f99ae7e27150 Admin/profiling_reports --- a/Admin/profiling_reports Wed May 12 15:25:23 2010 +0200 +++ b/Admin/profiling_reports Wed May 12 16:45:59 2010 +0200 @@ -1,6 +1,5 @@ #!/usr/bin/env bash # -# $Id$ # Author: Makarius # # DESCRIPTION: Cumulative reports for Poly/ML profiling output. diff -r b78d3c87fc88 -r f99ae7e27150 Admin/psbooklet --- a/Admin/psbooklet Wed May 12 15:25:23 2010 +0200 +++ b/Admin/psbooklet Wed May 12 16:45:59 2010 +0200 @@ -1,9 +1,6 @@ #!/usr/bin/env bash # -# $Id$ -# # psbooklet - rearrange pages of ps file to be printed as booklet (duplex) -# psbook "$@" | \ pstops '4:0L@.7(21cm,0cm)+1L@.7(21cm,14.85cm),3R@.7(0cm,14.85cm)+2R@.7(0cm,29.7cm)' diff -r b78d3c87fc88 -r f99ae7e27150 Admin/rsyncd --- a/Admin/rsyncd Wed May 12 15:25:23 2010 +0200 +++ b/Admin/rsyncd Wed May 12 16:45:59 2010 +0200 @@ -1,9 +1,6 @@ #!/usr/bin/env bash # # rsync server start script -# -# $Id$ -# /usr/bin/rsync --daemon --config=/home/proj/isabelle/rsyncd.conf diff -r b78d3c87fc88 -r f99ae7e27150 Admin/spass/README --- a/Admin/spass/README Wed May 12 15:25:23 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,33 +0,0 @@ - -This distribution of SPASS 3.0 has been compiled according to the -INSTALL instructions of the official source download from -http://www.spass-prover.org - -The following example is for x86-linux: - - $ tar xvzf spass30.tgz - $ cd SPASS-3.0 - $ ./configure --prefix="$HOME/tmp/spass" --exec-prefix="$HOME/tmp/spass/x86-linux" - $ make - $ make install - - -The x86-darwin platform works the same; use "make distclean" before -reconfiguration. - -Native x86_64 is avoided here, due to numerous compiler warnings about -int/pointer casts of different size. The x86 binaries are used -instead. - -For x86-cygwin we have removed the "__inline__" configuration to -workaround a problem with "___sgetc_r": - -diff configure-orig configure -3522c3522 -< CFLAGS="-O3 -D__inline__=" ---- -> CFLAGS="-O3" - - - Makarius - 30-Oct-2009 diff -r b78d3c87fc88 -r f99ae7e27150 README --- a/README Wed May 12 15:25:23 2010 +0200 +++ b/README Wed May 12 16:45:59 2010 +0200 @@ -12,17 +12,17 @@ Isabelle requires a regular Unix platform (e.g. GNU Linux) with the following additional software: - * A full Standard ML Compiler (works best with Poly/ML 5.3.0). + * The Poly/ML compiler and runtime system (version 5.x). * The GNU bash shell (version 3.x or 2.x). * Perl (version 5.x). - * GNU Emacs (version 22 or 23) -- for the Proof General interface. + * GNU Emacs (version 22) -- for the Proof General interface. * A complete LaTeX installation -- for document preparation. Installation Binary packages are available for Isabelle/HOL and ZF for several - platforms from the Isabelle web page. The system may be easily - built from scratch, using the tar.gz source distribution. See file + platforms from the Isabelle web page. The system may be also built + from scratch, using the tar.gz source distribution. See file INSTALL as distributed with Isabelle for more information. Further background information may be found in the Isabelle System @@ -30,13 +30,13 @@ User interface - The main Isabelle user interface is Proof General by David Aspinall - and others. It is a generic Emacs interface for proof assistants, - including Isabelle. Proof General is suitable for use by pacifists - and Emacs militants alike. Its most prominent feature is script - management, providing a metaphor of live proof script editing. - Proof General also provides some support for mathematical symbols - displayed on screen. + The classic Isabelle user interface is Proof General by David + Aspinall and others. It is a generic Emacs interface for proof + assistants, including Isabelle. Proof General is suitable for use + by pacifists and Emacs militants alike. Its most prominent feature + is script management, providing a metaphor of live proof script + editing. Proof General also provides some support for mathematical + symbols displayed on screen. Other sources of information diff -r b78d3c87fc88 -r f99ae7e27150 README_REPOSITORY --- a/README_REPOSITORY Wed May 12 15:25:23 2010 +0200 +++ b/README_REPOSITORY Wed May 12 16:45:59 2010 +0200 @@ -32,11 +32,6 @@ Initial configuration --------------------- -Always use Mercurial versions from the 1.0 or 1.1 branch, or later. -The old 0.9.x versions do not work in a multi-user environment with -shared file spaces! - - The official Isabelle repository can be cloned like this: hg clone http://isabelle.in.tum.de/repos/isabelle diff -r b78d3c87fc88 -r f99ae7e27150 src/CCL/IsaMakefile --- a/src/CCL/IsaMakefile Wed May 12 15:25:23 2010 +0200 +++ b/src/CCL/IsaMakefile Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,3 @@ -# -# $Id$ # # IsaMakefile for CCL # diff -r b78d3c87fc88 -r f99ae7e27150 src/CTT/IsaMakefile --- a/src/CTT/IsaMakefile Wed May 12 15:25:23 2010 +0200 +++ b/src/CTT/IsaMakefile Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,3 @@ -# -# $Id$ # # IsaMakefile for CTT # diff -r b78d3c87fc88 -r f99ae7e27150 src/CTT/README.html --- a/src/CTT/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/CTT/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/Cube/IsaMakefile --- a/src/Cube/IsaMakefile Wed May 12 15:25:23 2010 +0200 +++ b/src/Cube/IsaMakefile Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,3 @@ -# -# $Id$ # # IsaMakefile for Cube # diff -r b78d3c87fc88 -r f99ae7e27150 src/Cube/README.html --- a/src/Cube/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/Cube/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/FOL/FOL.thy Wed May 12 16:45:59 2010 +0200 @@ -348,11 +348,10 @@ text {* Proper handling of non-atomic rule statements. *} -constdefs - induct_forall where "induct_forall(P) == \x. P(x)" - induct_implies where "induct_implies(A, B) == A \ B" - induct_equal where "induct_equal(x, y) == x = y" - induct_conj where "induct_conj(A, B) == A \ B" +definition "induct_forall(P) == \x. P(x)" +definition "induct_implies(A, B) == A \ B" +definition "induct_equal(x, y) == x = y" +definition "induct_conj(A, B) == A \ B" lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\x. P(x)))" unfolding atomize_all induct_forall_def . diff -r b78d3c87fc88 -r f99ae7e27150 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Wed May 12 15:25:23 2010 +0200 +++ b/src/FOL/IsaMakefile Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,3 @@ -# -# $Id$ # # IsaMakefile for FOL # diff -r b78d3c87fc88 -r f99ae7e27150 src/FOL/README.html --- a/src/FOL/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/FOL/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/FOL/document/root.tex --- a/src/FOL/document/root.tex Wed May 12 15:25:23 2010 +0200 +++ b/src/FOL/document/root.tex Wed May 12 16:45:59 2010 +0200 @@ -1,6 +1,3 @@ - -% $Id$ - \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \usepackage{pdfsetup} diff -r b78d3c87fc88 -r f99ae7e27150 src/FOLP/IsaMakefile --- a/src/FOLP/IsaMakefile Wed May 12 15:25:23 2010 +0200 +++ b/src/FOLP/IsaMakefile Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,3 @@ -# -# $Id$ # # IsaMakefile for FOLP # diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Auth/KerberosIV.thy --- a/src/HOL/Auth/KerberosIV.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Auth/KerberosIV.thy Wed May 12 16:45:59 2010 +0200 @@ -21,30 +21,32 @@ Tgs_not_bad [iff]: "Tgs \ bad" --{*Tgs is secure --- we already know that Kas is secure*} -constdefs +definition (* authKeys are those contained in an authTicket *) - authKeys :: "event list => key set" - "authKeys evs == {authK. \A Peer Ta. Says Kas A + authKeys :: "event list => key set" where + "authKeys evs = {authK. \A Peer Ta. Says Kas A (Crypt (shrK A) \Key authK, Agent Peer, Number Ta, (Crypt (shrK Peer) \Agent A, Agent Peer, Key authK, Number Ta\) \) \ set evs}" +definition (* A is the true creator of X if she has sent X and X never appeared on the trace before this event. Recall that traces grow from head. *) Issues :: "[agent, agent, msg, event list] => bool" - ("_ Issues _ with _ on _") - "A Issues B with X on evs == - \Y. Says A B Y \ set evs & X \ parts {Y} & - X \ parts (spies (takeWhile (% z. z \ Says A B Y) (rev evs)))" + ("_ Issues _ with _ on _") where + "A Issues B with X on evs = + (\Y. Says A B Y \ set evs & X \ parts {Y} & + X \ parts (spies (takeWhile (% z. z \ Says A B Y) (rev evs))))" +definition (* Yields the subtrace of a given trace from its beginning to a given event *) before :: "[event, event list] => event list" ("before _ on _") - "before ev on evs == takeWhile (% z. z ~= ev) (rev evs)" + where "before ev on evs = takeWhile (% z. z ~= ev) (rev evs)" +definition (* States than an event really appears only once on a trace *) Unique :: "[event, event list] => bool" ("Unique _ on _") - "Unique ev on evs == - ev \ set (tl (dropWhile (% z. z \ ev) evs))" + where "Unique ev on evs = (ev \ set (tl (dropWhile (% z. z \ ev) evs)))" consts diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Auth/KerberosIV_Gets.thy --- a/src/HOL/Auth/KerberosIV_Gets.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Auth/KerberosIV_Gets.thy Wed May 12 16:45:59 2010 +0200 @@ -21,18 +21,18 @@ Tgs_not_bad [iff]: "Tgs \ bad" --{*Tgs is secure --- we already know that Kas is secure*} -constdefs +definition (* authKeys are those contained in an authTicket *) - authKeys :: "event list => key set" - "authKeys evs == {authK. \A Peer Ta. Says Kas A + authKeys :: "event list => key set" where + "authKeys evs = {authK. \A Peer Ta. Says Kas A (Crypt (shrK A) \Key authK, Agent Peer, Number Ta, (Crypt (shrK Peer) \Agent A, Agent Peer, Key authK, Number Ta\) \) \ set evs}" +definition (* States than an event really appears only once on a trace *) Unique :: "[event, event list] => bool" ("Unique _ on _") - "Unique ev on evs == - ev \ set (tl (dropWhile (% z. z \ ev) evs))" + where "Unique ev on evs = (ev \ set (tl (dropWhile (% z. z \ ev) evs)))" consts diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Auth/KerberosV.thy --- a/src/HOL/Auth/KerberosV.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Auth/KerberosV.thy Wed May 12 16:45:59 2010 +0200 @@ -21,21 +21,22 @@ Tgs_not_bad [iff]: "Tgs \ bad" --{*Tgs is secure --- we already know that Kas is secure*} -constdefs +definition (* authKeys are those contained in an authTicket *) - authKeys :: "event list => key set" - "authKeys evs == {authK. \A Peer Ta. + authKeys :: "event list => key set" where + "authKeys evs = {authK. \A Peer Ta. Says Kas A \Crypt (shrK A) \Key authK, Agent Peer, Ta\, Crypt (shrK Peer) \Agent A, Agent Peer, Key authK, Ta\ \ \ set evs}" +definition (* A is the true creator of X if she has sent X and X never appeared on the trace before this event. Recall that traces grow from head. *) Issues :: "[agent, agent, msg, event list] => bool" - ("_ Issues _ with _ on _") - "A Issues B with X on evs == - \Y. Says A B Y \ set evs \ X \ parts {Y} \ - X \ parts (spies (takeWhile (% z. z \ Says A B Y) (rev evs)))" + ("_ Issues _ with _ on _") where + "A Issues B with X on evs = + (\Y. Says A B Y \ set evs \ X \ parts {Y} \ + X \ parts (spies (takeWhile (% z. z \ Says A B Y) (rev evs))))" consts diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Auth/Kerberos_BAN.thy --- a/src/HOL/Auth/Kerberos_BAN.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Auth/Kerberos_BAN.thy Wed May 12 16:45:59 2010 +0200 @@ -51,24 +51,24 @@ "expiredA T evs == authlife + T < CT evs" -constdefs - +definition (* A is the true creator of X if she has sent X and X never appeared on the trace before this event. Recall that traces grow from head. *) Issues :: "[agent, agent, msg, event list] => bool" - ("_ Issues _ with _ on _") - "A Issues B with X on evs == - \Y. Says A B Y \ set evs & X \ parts {Y} & - X \ parts (spies (takeWhile (% z. z \ Says A B Y) (rev evs)))" + ("_ Issues _ with _ on _") where + "A Issues B with X on evs = + (\Y. Says A B Y \ set evs & X \ parts {Y} & + X \ parts (spies (takeWhile (% z. z \ Says A B Y) (rev evs))))" +definition (* Yields the subtrace of a given trace from its beginning to a given event *) before :: "[event, event list] => event list" ("before _ on _") - "before ev on evs == takeWhile (% z. z ~= ev) (rev evs)" + where "before ev on evs = takeWhile (% z. z ~= ev) (rev evs)" +definition (* States than an event really appears only once on a trace *) Unique :: "[event, event list] => bool" ("Unique _ on _") - "Unique ev on evs == - ev \ set (tl (dropWhile (% z. z \ ev) evs))" + where "Unique ev on evs = (ev \ set (tl (dropWhile (% z. z \ ev) evs)))" inductive_set bankerberos :: "event list set" diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Auth/Kerberos_BAN_Gets.thy --- a/src/HOL/Auth/Kerberos_BAN_Gets.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy Wed May 12 16:45:59 2010 +0200 @@ -52,15 +52,15 @@ "expiredA T evs == authlife + T < CT evs" -constdefs +definition (* Yields the subtrace of a given trace from its beginning to a given event *) before :: "[event, event list] => event list" ("before _ on _") - "before ev on evs == takeWhile (% z. z ~= ev) (rev evs)" + where "before ev on evs = takeWhile (% z. z ~= ev) (rev evs)" +definition (* States than an event really appears only once on a trace *) Unique :: "[event, event list] => bool" ("Unique _ on _") - "Unique ev on evs == - ev \ set (tl (dropWhile (% z. z \ ev) evs))" + where "Unique ev on evs = (ev \ set (tl (dropWhile (% z. z \ ev) evs)))" inductive_set bankerb_gets :: "event list set" diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Wed May 12 16:45:59 2010 +0200 @@ -14,15 +14,14 @@ Proc. Royal Soc. 426 *} -constdefs - +definition (* A is the true creator of X if she has sent X and X never appeared on the trace before this event. Recall that traces grow from head. *) Issues :: "[agent, agent, msg, event list] => bool" - ("_ Issues _ with _ on _") - "A Issues B with X on evs == - \Y. Says A B Y \ set evs & X \ parts {Y} & - X \ parts (spies (takeWhile (% z. z \ Says A B Y) (rev evs)))" + ("_ Issues _ with _ on _") where + "A Issues B with X on evs = + (\Y. Says A B Y \ set evs & X \ parts {Y} & + X \ parts (spies (takeWhile (% z. z \ Says A B Y) (rev evs))))" inductive_set ns_shared :: "event list set" diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Extraction/Greatest_Common_Divisor.thy --- a/src/HOL/Extraction/Greatest_Common_Divisor.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Extraction/Greatest_Common_Divisor.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Extraction/Greatest_Common_Divisor.thy - ID: $Id$ Author: Stefan Berghofer, TU Muenchen Helmut Schwichtenberg, LMU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Extraction/QuotRem.thy --- a/src/HOL/Extraction/QuotRem.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Extraction/QuotRem.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Extraction/QuotRem.thy - ID: $Id$ Author: Stefan Berghofer, TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Hahn_Banach/README.html --- a/src/HOL/Hahn_Banach/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Hahn_Banach/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Hoare/SchorrWaite.thy --- a/src/HOL/Hoare/SchorrWaite.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Hoare/SchorrWaite.thy Wed May 12 16:45:59 2010 +0200 @@ -11,16 +11,22 @@ section {* Machinery for the Schorr-Waite proof*} -constdefs +definition -- "Relations induced by a mapping" rel :: "('a \ 'a ref) \ ('a \ 'a) set" - "rel m == {(x,y). m x = Ref y}" + where "rel m = {(x,y). m x = Ref y}" + +definition relS :: "('a \ 'a ref) set \ ('a \ 'a) set" - "relS M == (\ m \ M. rel m)" + where "relS M = (\ m \ M. rel m)" + +definition addrs :: "'a ref set \ 'a set" - "addrs P == {a. Ref a \ P}" + where "addrs P = {a. Ref a \ P}" + +definition reachable :: "('a \ 'a) set \ 'a ref set \ 'a set" - "reachable r P == (r\<^sup>* `` addrs P)" + where "reachable r P = (r\<^sup>* `` addrs P)" lemmas rel_defs = relS_def rel_def @@ -77,10 +83,10 @@ apply (simp add:rel_defs fun_upd_apply) done -constdefs +definition -- "Restriction of a relation" restr ::"('a \ 'a) set \ ('a \ bool) \ ('a \ 'a) set" ("(_/ | _)" [50, 51] 50) - "restr r m == {(x,y). (x,y) \ r \ \ m x}" + where "restr r m = {(x,y). (x,y) \ r \ \ m x}" text {* Rewrite rules for the restriction of a relation *} @@ -109,10 +115,10 @@ apply (simp add:restr_def fun_upd_apply) done -constdefs +definition -- "A short form for the stack mapping function for List" S :: "('a \ bool) \ ('a \ 'a ref) \ ('a \ 'a ref) \ ('a \ 'a ref)" - "S c l r == (\x. if c x then r x else l x)" + where "S c l r = (\x. if c x then r x else l x)" text {* Rewrite rules for Lists using S as their mapping *} diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Hoare/document/root.tex --- a/src/HOL/Hoare/document/root.tex Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Hoare/document/root.tex Wed May 12 16:45:59 2010 +0200 @@ -1,6 +1,3 @@ - -% $Id$ - \documentclass[11pt,a4paper]{report} \usepackage{graphicx} \usepackage[english]{babel} diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/IOA/Asig.thy --- a/src/HOL/IOA/Asig.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/IOA/Asig.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/Asig.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind Copyright 1994 TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/IOA/IOA.thy --- a/src/HOL/IOA/IOA.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/IOA/IOA.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/IOA.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind Copyright 1994 TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/IOA/README.html --- a/src/HOL/IOA/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/IOA/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/IOA/Solve.thy --- a/src/HOL/IOA/Solve.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/IOA/Solve.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/IOA/Solve.thy - ID: $Id$ Author: Tobias Nipkow & Konrad Slind Copyright 1994 TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Induct/ABexp.thy --- a/src/HOL/Induct/ABexp.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Induct/ABexp.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Induct/ABexp.thy - ID: $Id$ Author: Stefan Berghofer, TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Induct/Com.thy --- a/src/HOL/Induct/Com.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Induct/Com.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ -(* Title: HOL/Induct/Com - ID: $Id$ +(* Title: HOL/Induct/Com.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Induct/Ordinals.thy --- a/src/HOL/Induct/Ordinals.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Induct/Ordinals.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Induct/Ordinals.thy - ID: $Id$ Author: Stefan Berghofer and Markus Wenzel, TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Induct/PropLog.thy --- a/src/HOL/Induct/PropLog.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Induct/PropLog.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Induct/PropLog.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1994 TU Muenchen & University of Cambridge *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Induct/README.html --- a/src/HOL/Induct/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Induct/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Induct/Sigma_Algebra.thy --- a/src/HOL/Induct/Sigma_Algebra.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Induct/Sigma_Algebra.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Induct/Sigma_Algebra.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Induct/Term.thy --- a/src/HOL/Induct/Term.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Induct/Term.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Induct/Term.thy - ID: $Id$ Author: Stefan Berghofer, TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Isar_Examples/README.html --- a/src/HOL/Isar_Examples/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Isar_Examples/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lambda/Commutation.thy --- a/src/HOL/Lambda/Commutation.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lambda/Commutation.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Lambda/Commutation.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1995 TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lambda/InductTermi.thy --- a/src/HOL/Lambda/InductTermi.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lambda/InductTermi.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Lambda/InductTermi.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1998 TU Muenchen diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lambda/Lambda.thy --- a/src/HOL/Lambda/Lambda.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lambda/Lambda.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Lambda/Lambda.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1995 TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lambda/ListApplication.thy --- a/src/HOL/Lambda/ListApplication.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lambda/ListApplication.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Lambda/ListApplication.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1998 TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lambda/ListBeta.thy --- a/src/HOL/Lambda/ListBeta.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lambda/ListBeta.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Lambda/ListBeta.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1998 TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lambda/ListOrder.thy --- a/src/HOL/Lambda/ListOrder.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lambda/ListOrder.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Lambda/ListOrder.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1998 TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lambda/ParRed.thy --- a/src/HOL/Lambda/ParRed.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lambda/ParRed.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Lambda/ParRed.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1995 TU Muenchen diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lambda/README.html --- a/src/HOL/Lambda/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lambda/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lambda/Standardization.thy --- a/src/HOL/Lambda/Standardization.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lambda/Standardization.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Lambda/Standardization.thy - ID: $Id$ Author: Stefan Berghofer Copyright 2005 TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lambda/Type.thy --- a/src/HOL/Lambda/Type.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lambda/Type.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Lambda/Type.thy - ID: $Id$ Author: Stefan Berghofer Copyright 2000 TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lambda/document/root.tex --- a/src/HOL/Lambda/document/root.tex Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lambda/document/root.tex Wed May 12 16:45:59 2010 +0200 @@ -1,6 +1,3 @@ - -% $Id$ - \documentclass[11pt,a4paper]{article} \usepackage{graphicx} \usepackage[english]{babel} diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Lattice/document/root.tex --- a/src/HOL/Lattice/document/root.tex Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Lattice/document/root.tex Wed May 12 16:45:59 2010 +0200 @@ -1,6 +1,3 @@ - -% $Id$ - \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym,pdfsetup} \usepackage[only,bigsqcap]{stmaryrd} diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Matrix/document/root.tex --- a/src/HOL/Matrix/document/root.tex Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Matrix/document/root.tex Wed May 12 16:45:59 2010 +0200 @@ -1,6 +1,3 @@ - -% $Id$ - \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/README.html --- a/src/HOL/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/SET_Protocol/Message_SET.thy --- a/src/HOL/SET_Protocol/Message_SET.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/SET_Protocol/Message_SET.thy Wed May 12 16:45:59 2010 +0200 @@ -93,10 +93,10 @@ by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split) -constdefs +definition (*Keys useful to decrypt elements of a message set*) keysFor :: "msg set => key set" - "keysFor H == invKey ` {K. \X. Crypt K X \ H}" + where "keysFor H = invKey ` {K. \X. Crypt K X \ H}" subsubsection{*Inductive definition of all "parts" of a message.*} diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/SET_Protocol/Public_SET.thy --- a/src/HOL/SET_Protocol/Public_SET.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/SET_Protocol/Public_SET.thy Wed May 12 16:45:59 2010 +0200 @@ -119,20 +119,22 @@ subsection{*Signature Primitives*} -constdefs - +definition (* Signature = Message + signed Digest *) sign :: "[key, msg]=>msg" - "sign K X == {|X, Crypt K (Hash X) |}" + where "sign K X = {|X, Crypt K (Hash X) |}" +definition (* Signature Only = signed Digest Only *) signOnly :: "[key, msg]=>msg" - "signOnly K X == Crypt K (Hash X)" + where "signOnly K X = Crypt K (Hash X)" +definition (* Signature for Certificates = Message + signed Message *) signCert :: "[key, msg]=>msg" - "signCert K X == {|X, Crypt K X |}" + where "signCert K X = {|X, Crypt K X |}" +definition (* Certification Authority's Certificate. Contains agent name, a key, a number specifying the key's target use, a key to sign the entire certificate. @@ -141,16 +143,16 @@ then Ka=pubEK i or pubSK i depending on T ?? *) cert :: "[agent, key, msg, key] => msg" - "cert A Ka T signK == signCert signK {|Agent A, Key Ka, T|}" + where "cert A Ka T signK = signCert signK {|Agent A, Key Ka, T|}" - +definition (* Cardholder's Certificate. Contains a PAN, the certified key Ka, the PANSecret PS, a number specifying the target use for Ka, the signing key signK. *) certC :: "[nat, key, nat, msg, key] => msg" - "certC PAN Ka PS T signK == - signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}" + where "certC PAN Ka PS T signK = + signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}" (*cert and certA have no repeated elements, so they could be abbreviations, but that's tricky and makes proofs slower*) @@ -164,13 +166,13 @@ definition EXcrypt :: "[key,key,msg,msg] => msg" where --{*Extra Encryption*} (*K: the symmetric key EK: the public encryption key*) - "EXcrypt K EK M m == + "EXcrypt K EK M m = {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m|}|}" definition EXHcrypt :: "[key,key,msg,msg] => msg" where --{*Extra Encryption with Hashing*} (*K: the symmetric key EK: the public encryption key*) - "EXHcrypt K EK M m == + "EXHcrypt K EK M m = {|Crypt K {|M, Hash m|}, Crypt EK {|Key K, m, Hash M|}|}" definition Enc :: "[key,key,key,msg] => msg" where @@ -178,12 +180,12 @@ (*SK: the sender's signing key K: the symmetric key EK: the public encryption key*) - "Enc SK K EK M == + "Enc SK K EK M = {|Crypt K (sign SK M), Crypt EK (Key K)|}" definition EncB :: "[key,key,key,msg,msg] => msg" where --{*Encapsulation with Baggage. Keys as above, and baggage b.*} - "EncB SK K EK M b == + "EncB SK K EK M b = {|Enc SK K EK {|M, Hash b|}, b|}" @@ -390,14 +392,14 @@ text{*A set is expanded only if a relation is applied to it*} lemma def_abbrev_simp_relation: - "A == B ==> (A \ X) = (B \ X) & + "A = B ==> (A \ X) = (B \ X) & (u = A) = (u = B) & (A = u) = (B = u)" by auto text{*A set is expanded only if one of the given functions is applied to it*} lemma def_abbrev_simp_function: - "A == B + "A = B ==> parts (insert A X) = parts (insert B X) & analz (insert A X) = analz (insert B X) & keysFor (insert A X) = keysFor (insert B X)" diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/TLA/Memory/MemClerk.thy --- a/src/HOL/TLA/Memory/MemClerk.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/TLA/Memory/MemClerk.thy Wed May 12 16:45:59 2010 +0200 @@ -17,52 +17,57 @@ mClkRcvChType = "rpcSndChType" mClkStType = "(PrIds => mClkState) stfun" -constdefs +definition (* state predicates *) MClkInit :: "mClkRcvChType => mClkStType => PrIds => stpred" - "MClkInit rcv cst p == PRED (cst!p = #clkA & ~Calling rcv p)" + where "MClkInit rcv cst p = PRED (cst!p = #clkA & ~Calling rcv p)" +definition (* actions *) MClkFwd :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" - "MClkFwd send rcv cst p == ACT + where "MClkFwd send rcv cst p = ACT $Calling send p & $(cst!p) = #clkA & Call rcv p MClkRelayArg> & (cst!p)$ = #clkB & unchanged (rtrner send!p)" +definition MClkRetry :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" - "MClkRetry send rcv cst p == ACT + where "MClkRetry send rcv cst p = ACT $(cst!p) = #clkB & res<$(rcv!p)> = #RPCFailure & Call rcv p MClkRelayArg> & unchanged (cst!p, rtrner send!p)" +definition MClkReply :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" - "MClkReply send rcv cst p == ACT + where "MClkReply send rcv cst p = ACT ~$Calling rcv p & $(cst!p) = #clkB & Return send p MClkReplyVal> & (cst!p)$ = #clkA & unchanged (caller rcv!p)" +definition MClkNext :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" - "MClkNext send rcv cst p == ACT + where "MClkNext send rcv cst p = ACT ( MClkFwd send rcv cst p | MClkRetry send rcv cst p | MClkReply send rcv cst p)" - +definition (* temporal *) MClkIPSpec :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal" - "MClkIPSpec send rcv cst p == TEMP + where "MClkIPSpec send rcv cst p = TEMP Init MClkInit rcv cst p & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p) & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p) & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)" +definition MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal" - "MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)" + where "MClkISpec send rcv cst = TEMP (ALL p. MClkIPSpec send rcv cst p)" lemmas MC_action_defs = MClkInit_def MClkFwd_def MClkRetry_def MClkReply_def MClkNext_def diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/TLA/Memory/MemClerkParameters.thy --- a/src/HOL/TLA/Memory/MemClerkParameters.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy Wed May 12 16:45:59 2010 +0200 @@ -19,12 +19,14 @@ mClkSndArgType = "memOp" mClkRcvArgType = "rpcOp" -constdefs +definition (* translate a memory call to an RPC call *) MClkRelayArg :: "memOp => rpcOp" - "MClkRelayArg marg == memcall marg" + where "MClkRelayArg marg = memcall marg" + +definition (* translate RPC failures to memory failures *) MClkReplyVal :: "Vals => Vals" - "MClkReplyVal v == if v = RPCFailure then MemFailure else v" + where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)" end diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Wed May 12 16:45:59 2010 +0200 @@ -34,82 +34,104 @@ cst :: "mClkStType" ires :: "resType" -constdefs +definition (* auxiliary predicates *) MVOKBARF :: "Vals => bool" - "MVOKBARF v == (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)" + where "MVOKBARF v <-> (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)" + +definition MVOKBA :: "Vals => bool" - "MVOKBA v == (v : MemVal) | (v = OK) | (v = BadArg)" + where "MVOKBA v <-> (v : MemVal) | (v = OK) | (v = BadArg)" + +definition MVNROKBA :: "Vals => bool" - "MVNROKBA v == (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)" + where "MVNROKBA v <-> (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)" +definition (* tuples of state functions changed by the various components *) e :: "PrIds => (bit * memOp) stfun" - "e p == PRED (caller memCh!p)" + where "e p = PRED (caller memCh!p)" + +definition c :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcOp)) stfun" - "c p == PRED (cst!p, rtrner memCh!p, caller crCh!p)" + where "c p = PRED (cst!p, rtrner memCh!p, caller crCh!p)" + +definition r :: "PrIds => (rpcState * (bit * Vals) * (bit * memOp)) stfun" - "r p == PRED (rst!p, rtrner crCh!p, caller rmCh!p)" + where "r p = PRED (rst!p, rtrner crCh!p, caller rmCh!p)" + +definition m :: "PrIds => ((bit * Vals) * Vals) stfun" - "m p == PRED (rtrner rmCh!p, ires!p)" + where "m p = PRED (rtrner rmCh!p, ires!p)" +definition (* the environment action *) ENext :: "PrIds => action" - "ENext p == ACT (? l. #l : #MemLoc & Call memCh p #(read l))" + where "ENext p = ACT (? l. #l : #MemLoc & Call memCh p #(read l))" +definition (* specification of the history variable *) HInit :: "histType => PrIds => stpred" - "HInit rmhist p == PRED rmhist!p = #histA" + where "HInit rmhist p = PRED rmhist!p = #histA" +definition HNext :: "histType => PrIds => action" - "HNext rmhist p == ACT (rmhist!p)$ = + where "HNext rmhist p = ACT (rmhist!p)$ = (if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p) then #histB else if (MClkReply memCh crCh cst p) then #histA else $(rmhist!p))" +definition HistP :: "histType => PrIds => temporal" - "HistP rmhist p == TEMP Init HInit rmhist p - & [][HNext rmhist p]_(c p,r p,m p, rmhist!p)" + where "HistP rmhist p = (TEMP Init HInit rmhist p + & [][HNext rmhist p]_(c p,r p,m p, rmhist!p))" +definition Hist :: "histType => temporal" - "Hist rmhist == TEMP (ALL p. HistP rmhist p)" + where "Hist rmhist = TEMP (ALL p. HistP rmhist p)" +definition (* the implementation *) IPImp :: "PrIds => temporal" - "IPImp p == TEMP ( Init ~Calling memCh p & [][ENext p]_(e p) + where "IPImp p = (TEMP ( Init ~Calling memCh p & [][ENext p]_(e p) & MClkIPSpec memCh crCh cst p & RPCIPSpec crCh rmCh rst p & RPSpec rmCh mm ires p - & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l))" + & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l)))" +definition ImpInit :: "PrIds => stpred" - "ImpInit p == PRED ( ~Calling memCh p + where "ImpInit p = PRED ( ~Calling memCh p & MClkInit crCh cst p & RPCInit rmCh rst p & PInit ires p)" +definition ImpNext :: "PrIds => action" - "ImpNext p == ACT [ENext p]_(e p) + where "ImpNext p = (ACT [ENext p]_(e p) & [MClkNext memCh crCh cst p]_(c p) & [RPCNext crCh rmCh rst p]_(r p) - & [RNext rmCh mm ires p]_(m p)" + & [RNext rmCh mm ires p]_(m p))" +definition ImpLive :: "PrIds => temporal" - "ImpLive p == TEMP WF(MClkFwd memCh crCh cst p)_(c p) + where "ImpLive p = (TEMP WF(MClkFwd memCh crCh cst p)_(c p) & SF(MClkReply memCh crCh cst p)_(c p) & WF(RPCNext crCh rmCh rst p)_(r p) & WF(RNext rmCh mm ires p)_(m p) - & WF(MemReturn rmCh ires p)_(m p)" + & WF(MemReturn rmCh ires p)_(m p))" +definition Implementation :: "temporal" - "Implementation == TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p)) + where "Implementation = (TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p)) & MClkISpec memCh crCh cst & RPCISpec crCh rmCh rst - & IRSpec rmCh mm ires)" + & IRSpec rmCh mm ires))" +definition (* the predicate S describes the states of the implementation. slight simplification: two "histState" parameters instead of a (one- or two-element) set. @@ -117,7 +139,7 @@ the type definitions. The last conjunct is asserted separately as the memory invariant MemInv, proved in Memory.thy. *) S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred" - "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED + where "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p = (PRED Calling memCh p = #ecalling & Calling crCh p = #ccalling & (#ccalling --> arg = MClkRelayArg>) @@ -129,29 +151,42 @@ & cst!p = #cs & rst!p = #rs & (rmhist!p = #hs1 | rmhist!p = #hs2) - & MVNROKBA" + & MVNROKBA)" +definition (* predicates S1 -- S6 define special instances of S *) S1 :: "histType => PrIds => stpred" - "S1 rmhist p == S rmhist False False False clkA rpcA histA histA p" + where "S1 rmhist p = S rmhist False False False clkA rpcA histA histA p" + +definition S2 :: "histType => PrIds => stpred" - "S2 rmhist p == S rmhist True False False clkA rpcA histA histA p" + where "S2 rmhist p = S rmhist True False False clkA rpcA histA histA p" + +definition S3 :: "histType => PrIds => stpred" - "S3 rmhist p == S rmhist True True False clkB rpcA histA histB p" + where "S3 rmhist p = S rmhist True True False clkB rpcA histA histB p" + +definition S4 :: "histType => PrIds => stpred" - "S4 rmhist p == S rmhist True True True clkB rpcB histA histB p" + where "S4 rmhist p = S rmhist True True True clkB rpcB histA histB p" + +definition S5 :: "histType => PrIds => stpred" - "S5 rmhist p == S rmhist True True False clkB rpcB histB histB p" + where "S5 rmhist p = S rmhist True True False clkB rpcB histB histB p" + +definition S6 :: "histType => PrIds => stpred" - "S6 rmhist p == S rmhist True False False clkB rpcA histB histB p" + where "S6 rmhist p = S rmhist True False False clkB rpcA histB histB p" +definition (* The invariant asserts that the system is always in one of S1 - S6, for every p *) ImpInv :: "histType => PrIds => stpred" - "ImpInv rmhist p == PRED ( S1 rmhist p | S2 rmhist p | S3 rmhist p - | S4 rmhist p | S5 rmhist p | S6 rmhist p)" + where "ImpInv rmhist p = (PRED (S1 rmhist p | S2 rmhist p | S3 rmhist p + | S4 rmhist p | S5 rmhist p | S6 rmhist p))" +definition resbar :: "histType => resType" (* refinement mapping *) - "resbar rmhist s p == + where"resbar rmhist s p = (if (S1 rmhist p s | S2 rmhist p s) then ires s p else if S3 rmhist p s @@ -167,7 +202,7 @@ then MemFailure else res (crCh s p) else NotAResult)" (* dummy value *) -axioms +axiomatization where (* the "base" variables: everything except resbar and hist (for any index) *) MI_base: "basevars (caller memCh!p, (rtrner memCh!p, caller crCh!p, cst!p), diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Tools/Qelim/ferrante_rackoff.ML --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/Qelim/ferrante_rackoff.ML - ID: $Id$ Author: Amine Chaieb, TU Muenchen Ferrante and Rackoff's algorithm for quantifier elimination in dense diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Tools/Qelim/ferrante_rackoff_data.ML --- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/Qelim/ferrante_rackoff_data.ML - ID: $Id$ Author: Amine Chaieb, TU Muenchen Context data for Ferrante and Rackoff's algorithm for quantifier diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Tools/primrec.ML Wed May 12 16:45:59 2010 +0200 @@ -326,7 +326,8 @@ || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) => Toplevel.theory (snd o (if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec) - alt_name (map P.triple_swap eqns))))); + alt_name (map P.triple_swap eqns) o + tap (fn _ => legacy_feature "Old variant of 'primrec' command -- use new syntax instead"))))); end; diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Tools/recdef.ML Wed May 12 16:45:59 2010 +0200 @@ -184,7 +184,7 @@ fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy = let - val _ = legacy_feature ("\"recdef\"; prefer \"function\" instead"); + val _ = legacy_feature "Old 'recdef' command -- use 'fun' or 'function' instead"; val _ = requires_recdef thy; val name = Sign.intern_const thy raw_name; diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Comp/Alloc.thy Wed May 12 16:45:59 2010 +0200 @@ -20,15 +20,16 @@ clientState + dummy :: 'a --{*dummy field for new variables*} -constdefs +definition --{*DUPLICATED FROM Client.thy, but with "tok" removed*} --{*Maybe want a special theory section to declare such maps*} non_dummy :: "'a clientState_d => clientState" - "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)" + where "non_dummy s = (|giv = giv s, ask = ask s, rel = rel s|)" +definition --{*Renaming map to put a Client into the standard form*} client_map :: "'a clientState_d => clientState*'a" - "client_map == funPair non_dummy dummy" + where "client_map = funPair non_dummy dummy" record allocState = @@ -46,78 +47,86 @@ dummy :: 'a --{*dummy field for new variables*} -constdefs - --{** Resource allocation system specification **} +definition --{*spec (1)*} system_safety :: "'a systemState program set" - "system_safety == + where "system_safety = Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s) \ NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}" +definition --{*spec (2)*} system_progress :: "'a systemState program set" - "system_progress == INT i : lessThan Nclients. + where "system_progress = (INT i : lessThan Nclients. INT h. {s. h \ (ask o sub i o client)s} LeadsTo - {s. h pfixLe (giv o sub i o client) s}" + {s. h pfixLe (giv o sub i o client) s})" +definition system_spec :: "'a systemState program set" - "system_spec == system_safety Int system_progress" + where "system_spec = system_safety Int system_progress" --{** Client specification (required) ***} +definition --{*spec (3)*} client_increasing :: "'a clientState_d program set" - "client_increasing == - UNIV guarantees Increasing ask Int Increasing rel" + where "client_increasing = UNIV guarantees Increasing ask Int Increasing rel" +definition --{*spec (4)*} client_bounded :: "'a clientState_d program set" - "client_bounded == - UNIV guarantees Always {s. ALL elt : set (ask s). elt \ NbT}" + where "client_bounded = UNIV guarantees Always {s. ALL elt : set (ask s). elt \ NbT}" +definition --{*spec (5)*} client_progress :: "'a clientState_d program set" - "client_progress == + where "client_progress = Increasing giv guarantees (INT h. {s. h \ giv s & h pfixGe ask s} LeadsTo {s. tokens h \ (tokens o rel) s})" +definition --{*spec: preserves part*} client_preserves :: "'a clientState_d program set" - "client_preserves == preserves giv Int preserves clientState_d.dummy" + where "client_preserves = preserves giv Int preserves clientState_d.dummy" +definition --{*environmental constraints*} client_allowed_acts :: "'a clientState_d program set" - "client_allowed_acts == + where "client_allowed_acts = {F. AllowedActs F = insert Id (UNION (preserves (funPair rel ask)) Acts)}" +definition client_spec :: "'a clientState_d program set" - "client_spec == client_increasing Int client_bounded Int client_progress + where "client_spec = client_increasing Int client_bounded Int client_progress Int client_allowed_acts Int client_preserves" --{** Allocator specification (required) **} +definition --{*spec (6)*} alloc_increasing :: "'a allocState_d program set" - "alloc_increasing == + where "alloc_increasing = UNIV guarantees (INT i : lessThan Nclients. Increasing (sub i o allocGiv))" +definition --{*spec (7)*} alloc_safety :: "'a allocState_d program set" - "alloc_safety == + where "alloc_safety = (INT i : lessThan Nclients. Increasing (sub i o allocRel)) guarantees Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s) \ NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}" +definition --{*spec (8)*} alloc_progress :: "'a allocState_d program set" - "alloc_progress == + where "alloc_progress = (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int Increasing (sub i o allocRel)) Int @@ -141,96 +150,104 @@ thus h should have been a function variable. However, only h i is ever looked at.*) +definition --{*spec: preserves part*} alloc_preserves :: "'a allocState_d program set" - "alloc_preserves == preserves allocRel Int preserves allocAsk Int + where "alloc_preserves = preserves allocRel Int preserves allocAsk Int preserves allocState_d.dummy" +definition --{*environmental constraints*} alloc_allowed_acts :: "'a allocState_d program set" - "alloc_allowed_acts == + where "alloc_allowed_acts = {F. AllowedActs F = insert Id (UNION (preserves allocGiv) Acts)}" +definition alloc_spec :: "'a allocState_d program set" - "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int + where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int alloc_allowed_acts Int alloc_preserves" --{** Network specification **} +definition --{*spec (9.1)*} network_ask :: "'a systemState program set" - "network_ask == INT i : lessThan Nclients. + where "network_ask = (INT i : lessThan Nclients. Increasing (ask o sub i o client) guarantees - ((sub i o allocAsk) Fols (ask o sub i o client))" + ((sub i o allocAsk) Fols (ask o sub i o client)))" +definition --{*spec (9.2)*} network_giv :: "'a systemState program set" - "network_giv == INT i : lessThan Nclients. + where "network_giv = (INT i : lessThan Nclients. Increasing (sub i o allocGiv) guarantees - ((giv o sub i o client) Fols (sub i o allocGiv))" + ((giv o sub i o client) Fols (sub i o allocGiv)))" +definition --{*spec (9.3)*} network_rel :: "'a systemState program set" - "network_rel == INT i : lessThan Nclients. + where "network_rel = (INT i : lessThan Nclients. Increasing (rel o sub i o client) guarantees - ((sub i o allocRel) Fols (rel o sub i o client))" + ((sub i o allocRel) Fols (rel o sub i o client)))" +definition --{*spec: preserves part*} network_preserves :: "'a systemState program set" - "network_preserves == + where "network_preserves = preserves allocGiv Int (INT i : lessThan Nclients. preserves (rel o sub i o client) Int preserves (ask o sub i o client))" +definition --{*environmental constraints*} network_allowed_acts :: "'a systemState program set" - "network_allowed_acts == + where "network_allowed_acts = {F. AllowedActs F = insert Id (UNION (preserves allocRel Int (INT i: lessThan Nclients. preserves(giv o sub i o client))) Acts)}" +definition network_spec :: "'a systemState program set" - "network_spec == network_ask Int network_giv Int + where "network_spec = network_ask Int network_giv Int network_rel Int network_allowed_acts Int network_preserves" --{** State mappings **} +definition sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState" - "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s + where "sysOfAlloc = (%s. let (cl,xtr) = allocState_d.dummy s in (| allocGiv = allocGiv s, allocAsk = allocAsk s, allocRel = allocRel s, client = cl, - dummy = xtr|)" + dummy = xtr|))" +definition sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState" - "sysOfClient == %(cl,al). (| allocGiv = allocGiv al, + where "sysOfClient = (%(cl,al). (| allocGiv = allocGiv al, allocAsk = allocAsk al, allocRel = allocRel al, client = cl, - systemState.dummy = allocState_d.dummy al|)" + systemState.dummy = allocState_d.dummy al|))" -consts - Alloc :: "'a allocState_d program" - Client :: "'a clientState_d program" - Network :: "'a systemState program" - System :: "'a systemState program" +axiomatization Alloc :: "'a allocState_d program" + where Alloc: "Alloc : alloc_spec" -axioms - Alloc: "Alloc : alloc_spec" - Client: "Client : client_spec" - Network: "Network : network_spec" +axiomatization Client :: "'a clientState_d program" + where Client: "Client : client_spec" -defs - System_def: - "System == rename sysOfAlloc Alloc Join Network Join +axiomatization Network :: "'a systemState program" + where Network: "Network : network_spec" + +definition System :: "'a systemState program" + where "System = rename sysOfAlloc Alloc Join Network Join (rename sysOfClient (plam x: lessThan Nclients. rename client_map Client))" diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Comp/AllocImpl.thy --- a/src/HOL/UNITY/Comp/AllocImpl.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy Wed May 12 16:45:59 2010 +0200 @@ -21,7 +21,7 @@ dummy :: 'a (*dummy field for new variables*) definition non_dummy :: "('a,'b) merge_d => 'b merge" where - "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)" + "non_dummy s = (|In = In s, Out = Out s, iOut = iOut s|)" record 'b distr = In :: "'b list" (*items to distribute*) @@ -49,30 +49,32 @@ dummy :: 'a (*dummy field for new variables*) -constdefs - (** Merge specification (the number of inputs is Nclients) ***) +definition (*spec (10)*) merge_increasing :: "('a,'b) merge_d program set" - "merge_increasing == + where "merge_increasing = UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)" +definition (*spec (11)*) merge_eqOut :: "('a,'b) merge_d program set" - "merge_eqOut == + where "merge_eqOut = UNIV guarantees Always {s. length (merge.Out s) = length (merge.iOut s)}" +definition (*spec (12)*) merge_bounded :: "('a,'b) merge_d program set" - "merge_bounded == + where "merge_bounded = UNIV guarantees Always {s. \elt \ set (merge.iOut s). elt < Nclients}" +definition (*spec (13)*) merge_follows :: "('a,'b) merge_d program set" - "merge_follows == + where "merge_follows = (\i \ lessThan Nclients. Increasing (sub i o merge.In)) guarantees (\i \ lessThan Nclients. @@ -80,25 +82,29 @@ {k. k < size(merge.iOut s) & merge.iOut s! k = i}) Fols (sub i o merge.In))" +definition (*spec: preserves part*) merge_preserves :: "('a,'b) merge_d program set" - "merge_preserves == preserves merge.In Int preserves merge_d.dummy" + where "merge_preserves = preserves merge.In Int preserves merge_d.dummy" +definition (*environmental constraints*) merge_allowed_acts :: "('a,'b) merge_d program set" - "merge_allowed_acts == + where "merge_allowed_acts = {F. AllowedActs F = insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}" +definition merge_spec :: "('a,'b) merge_d program set" - "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int + where "merge_spec = merge_increasing Int merge_eqOut Int merge_bounded Int merge_follows Int merge_allowed_acts Int merge_preserves" (** Distributor specification (the number of outputs is Nclients) ***) +definition (*spec (14)*) distr_follows :: "('a,'b) distr_d program set" - "distr_follows == + where "distr_follows = Increasing distr.In Int Increasing distr.iIn Int Always {s. \elt \ set (distr.iIn s). elt < Nclients} guarantees @@ -107,28 +113,33 @@ (%s. sublist (distr.In s) {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))" +definition distr_allowed_acts :: "('a,'b) distr_d program set" - "distr_allowed_acts == + where "distr_allowed_acts = {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}" +definition distr_spec :: "('a,'b) distr_d program set" - "distr_spec == distr_follows Int distr_allowed_acts" + where "distr_spec = distr_follows Int distr_allowed_acts" (** Single-client allocator specification (required) ***) +definition (*spec (18)*) alloc_increasing :: "'a allocState_d program set" - "alloc_increasing == UNIV guarantees Increasing giv" + where "alloc_increasing = UNIV guarantees Increasing giv" +definition (*spec (19)*) alloc_safety :: "'a allocState_d program set" - "alloc_safety == + where "alloc_safety = Increasing rel guarantees Always {s. tokens (giv s) \ NbT + tokens (rel s)}" +definition (*spec (20)*) alloc_progress :: "'a allocState_d program set" - "alloc_progress == + where "alloc_progress = Increasing ask Int Increasing rel Int Always {s. \elt \ set (ask s). elt \ NbT} Int @@ -137,20 +148,23 @@ {s. tokens h \ tokens (rel s)}) guarantees (\h. {s. h \ ask s} LeadsTo {s. h pfixLe giv s})" +definition (*spec: preserves part*) alloc_preserves :: "'a allocState_d program set" - "alloc_preserves == preserves rel Int + where "alloc_preserves = preserves rel Int preserves ask Int preserves allocState_d.dummy" +definition (*environmental constraints*) alloc_allowed_acts :: "'a allocState_d program set" - "alloc_allowed_acts == + where "alloc_allowed_acts = {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}" +definition alloc_spec :: "'a allocState_d program set" - "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int + where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int alloc_allowed_acts Int alloc_preserves" locale Merge = diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Comp/Client.thy --- a/src/HOL/UNITY/Comp/Client.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Comp/Client.thy Wed May 12 16:45:59 2010 +0200 @@ -5,7 +5,7 @@ header{*Distributed Resource Management System: the Client*} -theory Client imports Rename AllocBase begin +theory Client imports "../Rename" AllocBase begin types tokbag = nat --{*tokbags could be multisets...or any ordered type?*} @@ -23,12 +23,12 @@ (*Array indexing is translated to list indexing as A[n] == A!(n-1). *) -constdefs (** Release some tokens **) +definition rel_act :: "('a state_d * 'a state_d) set" - "rel_act == {(s,s'). + where "rel_act = {(s,s'). \nrel. nrel = size (rel s) & s' = s (| rel := rel s @ [giv s!nrel] |) & nrel < size (giv s) & @@ -39,15 +39,18 @@ (** Including s'=s suppresses fairness, allowing the non-trivial part of the action to be ignored **) +definition tok_act :: "('a state_d * 'a state_d) set" - "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" + where "tok_act = {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" +definition ask_act :: "('a state_d * 'a state_d) set" - "ask_act == {(s,s'). s'=s | + where "ask_act = {(s,s'). s'=s | (s' = s (|ask := ask s @ [tok s]|))}" +definition Client :: "'a state_d program" - "Client == + where "Client = mk_total_program ({s. tok s \ atMost NbT & giv s = [] & ask s = [] & rel s = []}, @@ -55,13 +58,15 @@ \G \ preserves rel Int preserves ask Int preserves tok. Acts G)" +definition (*Maybe want a special theory section to declare such maps*) non_dummy :: "'a state_d => state" - "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)" + where "non_dummy s = (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)" +definition (*Renaming map to put a Client into the standard form*) client_map :: "'a state_d => state*'a" - "client_map == funPair non_dummy dummy" + where "client_map = funPair non_dummy dummy" declare Client_def [THEN def_prg_Init, simp] diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Comp/Counter.thy --- a/src/HOL/UNITY/Comp/Counter.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Comp/Counter.thy Wed May 12 16:45:59 2010 +0200 @@ -28,10 +28,10 @@ types command = "(state*state)set" definition a :: "nat=>command" where - "a i == {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}" + "a i = {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}" definition Component :: "nat => state program" where - "Component i == + "Component i = mk_total_program({s. s C = 0 & s (c i) = 0}, {a i}, \G \ preserves (%s. s (c i)). Acts G)" diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Comp/Counterc.thy --- a/src/HOL/UNITY/Comp/Counterc.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Comp/Counterc.thy Wed May 12 16:45:59 2010 +0200 @@ -33,12 +33,12 @@ types command = "(state*state)set" definition a :: "nat=>command" where - "a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}" + "a i = {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}" definition Component :: "nat => state program" where - "Component i == mk_total_program({s. C s = 0 & (c s) i = 0}, - {a i}, - \G \ preserves (%s. (c s) i). Acts G)" + "Component i = mk_total_program({s. C s = 0 & (c s) i = 0}, + {a i}, + \G \ preserves (%s. (c s) i). Acts G)" declare Component_def [THEN def_prg_Init, simp] diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Comp/Handshake.thy --- a/src/HOL/UNITY/Comp/Handshake.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Comp/Handshake.thy Wed May 12 16:45:59 2010 +0200 @@ -15,24 +15,28 @@ NF :: nat NG :: nat -constdefs +definition (*F's program*) cmdF :: "(state*state) set" - "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}" + where "cmdF = {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}" +definition F :: "state program" - "F == mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)" + where "F = mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)" +definition (*G's program*) cmdG :: "(state*state) set" - "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}" + where "cmdG = {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}" +definition G :: "state program" - "G == mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)" + where "G = mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)" +definition (*the joint invariant*) invFG :: "state set" - "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}" + where "invFG = {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}" declare F_def [THEN def_prg_Init, simp] diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Comp/Priority.thy --- a/src/HOL/UNITY/Comp/Priority.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Comp/Priority.thy Wed May 12 16:45:59 2010 +0200 @@ -21,51 +21,51 @@ text{*Following the definitions given in section 4.4 *} -definition highest :: "[vertex, (vertex*vertex)set]=>bool" where - "highest i r == A i r = {}" +definition highest :: "[vertex, (vertex*vertex)set]=>bool" + where "highest i r <-> A i r = {}" --{* i has highest priority in r *} -definition lowest :: "[vertex, (vertex*vertex)set]=>bool" where - "lowest i r == R i r = {}" +definition lowest :: "[vertex, (vertex*vertex)set]=>bool" + where "lowest i r <-> R i r = {}" --{* i has lowest priority in r *} -definition act :: command where - "act i == {(s, s'). s'=reverse i s & highest i s}" +definition act :: command + where "act i = {(s, s'). s'=reverse i s & highest i s}" -definition Component :: "vertex=>state program" where - "Component i == mk_total_program({init}, {act i}, UNIV)" +definition Component :: "vertex=>state program" + where "Component i = mk_total_program({init}, {act i}, UNIV)" --{* All components start with the same initial state *} text{*Some Abbreviations *} -definition Highest :: "vertex=>state set" where - "Highest i == {s. highest i s}" +definition Highest :: "vertex=>state set" + where "Highest i = {s. highest i s}" -definition Lowest :: "vertex=>state set" where - "Lowest i == {s. lowest i s}" +definition Lowest :: "vertex=>state set" + where "Lowest i = {s. lowest i s}" -definition Acyclic :: "state set" where - "Acyclic == {s. acyclic s}" +definition Acyclic :: "state set" + where "Acyclic = {s. acyclic s}" -definition Maximal :: "state set" where +definition Maximal :: "state set" --{* Every ``above'' set has a maximal vertex*} - "Maximal == \i. {s. ~highest i s-->(\j \ above i s. highest j s)}" + where "Maximal = (\i. {s. ~highest i s-->(\j \ above i s. highest j s)})" -definition Maximal' :: "state set" where +definition Maximal' :: "state set" --{* Maximal vertex: equivalent definition*} - "Maximal' == \i. Highest i Un (\j. {s. j \ above i s} Int Highest j)" + where "Maximal' = (\i. Highest i Un (\j. {s. j \ above i s} Int Highest j))" -definition Safety :: "state set" where - "Safety == \i. {s. highest i s --> (\j \ neighbors i s. ~highest j s)}" +definition Safety :: "state set" + where "Safety = (\i. {s. highest i s --> (\j \ neighbors i s. ~highest j s)})" (* Composition of a finite set of component; the vertex 'UNIV' is finite by assumption *) -definition system :: "state program" where - "system == JN i. Component i" +definition system :: "state program" + where "system = (JN i. Component i)" declare highest_def [simp] lowest_def [simp] diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Comp/TimerArray.thy --- a/src/HOL/UNITY/Comp/TimerArray.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Comp/TimerArray.thy Wed May 12 16:45:59 2010 +0200 @@ -9,14 +9,14 @@ types 'a state = "nat * 'a" (*second component allows new variables*) -definition count :: "'a state => nat" where - "count s == fst s" +definition count :: "'a state => nat" + where "count s = fst s" -definition decr :: "('a state * 'a state) set" where - "decr == UN n uu. {((Suc n, uu), (n,uu))}" +definition decr :: "('a state * 'a state) set" + where "decr = (UN n uu. {((Suc n, uu), (n,uu))})" -definition Timer :: "'a state program" where - "Timer == mk_total_program (UNIV, {decr}, UNIV)" +definition Timer :: "'a state program" + where "Timer = mk_total_program (UNIV, {decr}, UNIV)" declare Timer_def [THEN def_prg_Init, simp] diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/ELT.thy --- a/src/HOL/UNITY/ELT.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/ELT.thy Wed May 12 16:45:59 2010 +0200 @@ -38,20 +38,21 @@ | Union: "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F" -constdefs - +definition (*the set of all sets determined by f alone*) givenBy :: "['a => 'b] => 'a set set" - "givenBy f == range (%B. f-` B)" + where "givenBy f = range (%B. f-` B)" +definition (*visible version of the LEADS-TO relation*) leadsETo :: "['a set, 'a set set, 'a set] => 'a program set" ("(3_/ leadsTo[_]/ _)" [80,0,80] 80) - "leadsETo A CC B == {F. (A,B) : elt CC F}" + where "leadsETo A CC B = {F. (A,B) : elt CC F}" +definition LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set" ("(3_/ LeadsTo[_]/ _)" [80,0,80] 80) - "LeadsETo A CC B == + where "LeadsETo A CC B = {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] B}" diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Extend.thy --- a/src/HOL/UNITY/Extend.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Extend.thy Wed May 12 16:45:59 2010 +0200 @@ -11,36 +11,42 @@ theory Extend imports Guar begin -constdefs - +definition (*MOVE to Relation.thy?*) Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set" - "Restrict A r == r \ (A <*> UNIV)" + where "Restrict A r = r \ (A <*> UNIV)" +definition good_map :: "['a*'b => 'c] => bool" - "good_map h == surj h & (\x y. fst (inv h (h (x,y))) = x)" + where "good_map h <-> surj h & (\x y. fst (inv h (h (x,y))) = x)" (*Using the locale constant "f", this is f (h (x,y))) = x*) +definition extend_set :: "['a*'b => 'c, 'a set] => 'c set" - "extend_set h A == h ` (A <*> UNIV)" + where "extend_set h A = h ` (A <*> UNIV)" +definition project_set :: "['a*'b => 'c, 'c set] => 'a set" - "project_set h C == {x. \y. h(x,y) \ C}" + where "project_set h C = {x. \y. h(x,y) \ C}" +definition extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set" - "extend_act h == %act. \(s,s') \ act. \y. {(h(s,y), h(s',y))}" + where "extend_act h = (%act. \(s,s') \ act. \y. {(h(s,y), h(s',y))})" +definition project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set" - "project_act h act == {(x,x'). \y y'. (h(x,y), h(x',y')) \ act}" + where "project_act h act = {(x,x'). \y y'. (h(x,y), h(x',y')) \ act}" +definition extend :: "['a*'b => 'c, 'a program] => 'c program" - "extend h F == mk_program (extend_set h (Init F), + where "extend h F = mk_program (extend_set h (Init F), extend_act h ` Acts F, project_act h -` AllowedActs F)" +definition (*Argument C allows weak safety laws to be projected*) project :: "['a*'b => 'c, 'c set, 'c program] => 'a program" - "project h C F == + where "project h C F = mk_program (project_set h (Init F), project_act h ` Restrict C ` Acts F, {act. Restrict (project_set h C) act : diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Simple/Lift.thy --- a/src/HOL/UNITY/Simple/Lift.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Simple/Lift.thy Wed May 12 16:45:59 2010 +0200 @@ -18,98 +18,116 @@ up :: "bool" --{*current direction of movement*} move :: "bool" --{*whether moving takes precedence over opening*} -consts - Min :: "int" --{*least and greatest floors*} +axiomatization + Min :: "int" and --{*least and greatest floors*} Max :: "int" --{*least and greatest floors*} - -axioms +where Min_le_Max [iff]: "Min \ Max" -constdefs --{*Abbreviations: the "always" part*} +definition above :: "state set" - "above == {s. \i. floor s < i & i \ Max & i \ req s}" + where "above = {s. \i. floor s < i & i \ Max & i \ req s}" +definition below :: "state set" - "below == {s. \i. Min \ i & i < floor s & i \ req s}" + where "below = {s. \i. Min \ i & i < floor s & i \ req s}" +definition queueing :: "state set" - "queueing == above \ below" + where "queueing = above \ below" +definition goingup :: "state set" - "goingup == above \ ({s. up s} \ -below)" + where "goingup = above \ ({s. up s} \ -below)" +definition goingdown :: "state set" - "goingdown == below \ ({s. ~ up s} \ -above)" + where "goingdown = below \ ({s. ~ up s} \ -above)" +definition ready :: "state set" - "ready == {s. stop s & ~ open s & move s}" + where "ready = {s. stop s & ~ open s & move s}" --{*Further abbreviations*} +definition moving :: "state set" - "moving == {s. ~ stop s & ~ open s}" + where "moving = {s. ~ stop s & ~ open s}" +definition stopped :: "state set" - "stopped == {s. stop s & ~ open s & ~ move s}" + where "stopped = {s. stop s & ~ open s & ~ move s}" +definition opened :: "state set" - "opened == {s. stop s & open s & move s}" + where "opened = {s. stop s & open s & move s}" +definition closed :: "state set" --{*but this is the same as ready!!*} - "closed == {s. stop s & ~ open s & move s}" + where "closed = {s. stop s & ~ open s & move s}" +definition atFloor :: "int => state set" - "atFloor n == {s. floor s = n}" + where "atFloor n = {s. floor s = n}" +definition Req :: "int => state set" - "Req n == {s. n \ req s}" + where "Req n = {s. n \ req s}" --{*The program*} +definition request_act :: "(state*state) set" - "request_act == {(s,s'). s' = s (|stop:=True, move:=False|) + where "request_act = {(s,s'). s' = s (|stop:=True, move:=False|) & ~ stop s & floor s \ req s}" +definition open_act :: "(state*state) set" - "open_act == + where "open_act = {(s,s'). s' = s (|open :=True, req := req s - {floor s}, move := True|) & stop s & ~ open s & floor s \ req s & ~(move s & s \ queueing)}" +definition close_act :: "(state*state) set" - "close_act == {(s,s'). s' = s (|open := False|) & open s}" + where "close_act = {(s,s'). s' = s (|open := False|) & open s}" +definition req_up :: "(state*state) set" - "req_up == + where "req_up = {(s,s'). s' = s (|stop :=False, floor := floor s + 1, up := True|) & s \ (ready \ goingup)}" +definition req_down :: "(state*state) set" - "req_down == + where "req_down = {(s,s'). s' = s (|stop :=False, floor := floor s - 1, up := False|) & s \ (ready \ goingdown)}" +definition move_up :: "(state*state) set" - "move_up == + where "move_up = {(s,s'). s' = s (|floor := floor s + 1|) & ~ stop s & up s & floor s \ req s}" +definition move_down :: "(state*state) set" - "move_down == + where "move_down = {(s,s'). s' = s (|floor := floor s - 1|) & ~ stop s & ~ up s & floor s \ req s}" +definition button_press :: "(state*state) set" --{*This action is omitted from prior treatments, which therefore are unrealistic: nobody asks the lift to do anything! But adding this @@ -117,14 +135,15 @@ "ensures" properties fail. Maybe it should be constrained to only allow button presses in the current direction of travel, like in a real lift.*} - "button_press == + where "button_press = {(s,s'). \n. s' = s (|req := insert n (req s)|) & Min \ n & n \ Max}" +definition Lift :: "state program" --{*for the moment, we OMIT @{text button_press}*} - "Lift == mk_total_program + where "Lift = mk_total_program ({s. floor s = Min & ~ up s & move s & stop s & ~ open s & req s = {}}, {request_act, open_act, close_act, @@ -134,34 +153,41 @@ --{*Invariants*} +definition bounded :: "state set" - "bounded == {s. Min \ floor s & floor s \ Max}" + where "bounded = {s. Min \ floor s & floor s \ Max}" +definition open_stop :: "state set" - "open_stop == {s. open s --> stop s}" + where "open_stop = {s. open s --> stop s}" +definition open_move :: "state set" - "open_move == {s. open s --> move s}" + where "open_move = {s. open s --> move s}" +definition stop_floor :: "state set" - "stop_floor == {s. stop s & ~ move s --> floor s \ req s}" + where "stop_floor = {s. stop s & ~ move s --> floor s \ req s}" +definition moving_up :: "state set" - "moving_up == {s. ~ stop s & up s --> + where "moving_up = {s. ~ stop s & up s --> (\f. floor s \ f & f \ Max & f \ req s)}" +definition moving_down :: "state set" - "moving_down == {s. ~ stop s & ~ up s --> + where "moving_down = {s. ~ stop s & ~ up s --> (\f. Min \ f & f \ floor s & f \ req s)}" +definition metric :: "[int,state] => int" - "metric == - %n s. if floor s < n then (if up s then n - floor s + where "metric = + (%n s. if floor s < n then (if up s then n - floor s else (floor s - Min) + (n-Min)) else if n < floor s then (if up s then (Max - floor s) + (Max-n) else floor s - n) - else 0" + else 0)" locale Floor = fixes n diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Simple/Mutex.thy --- a/src/HOL/UNITY/Simple/Mutex.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Simple/Mutex.thy Wed May 12 16:45:59 2010 +0200 @@ -16,44 +16,43 @@ types command = "(state*state) set" -constdefs - + (** The program for process U **) - U0 :: command - "U0 == {(s,s'). s' = s (|u:=True, m:=1|) & m s = 0}" +definition U0 :: command + where "U0 = {(s,s'). s' = s (|u:=True, m:=1|) & m s = 0}" - U1 :: command - "U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = 1}" +definition U1 :: command + where "U1 = {(s,s'). s' = s (|p:= v s, m:=2|) & m s = 1}" - U2 :: command - "U2 == {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}" +definition U2 :: command + where "U2 = {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}" - U3 :: command - "U3 == {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}" +definition U3 :: command + where "U3 = {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}" - U4 :: command - "U4 == {(s,s'). s' = s (|p:=True, m:=0|) & m s = 4}" +definition U4 :: command + where "U4 = {(s,s'). s' = s (|p:=True, m:=0|) & m s = 4}" (** The program for process V **) - V0 :: command - "V0 == {(s,s'). s' = s (|v:=True, n:=1|) & n s = 0}" +definition V0 :: command + where "V0 = {(s,s'). s' = s (|v:=True, n:=1|) & n s = 0}" - V1 :: command - "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = 1}" +definition V1 :: command + where "V1 = {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = 1}" - V2 :: command - "V2 == {(s,s'). s' = s (|n:=3|) & p s & n s = 2}" +definition V2 :: command + where "V2 = {(s,s'). s' = s (|n:=3|) & p s & n s = 2}" - V3 :: command - "V3 == {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}" +definition V3 :: command + where "V3 = {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}" - V4 :: command - "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}" +definition V4 :: command + where "V4 = {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}" - Mutex :: "state program" - "Mutex == mk_total_program +definition Mutex :: "state program" + where "Mutex = mk_total_program ({s. ~ u s & ~ v s & m s = 0 & n s = 0}, {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, UNIV)" @@ -61,16 +60,16 @@ (** The correct invariants **) - IU :: "state set" - "IU == {s. (u s = (1 \ m s & m s \ 3)) & (m s = 3 --> ~ p s)}" +definition IU :: "state set" + where "IU = {s. (u s = (1 \ m s & m s \ 3)) & (m s = 3 --> ~ p s)}" - IV :: "state set" - "IV == {s. (v s = (1 \ n s & n s \ 3)) & (n s = 3 --> p s)}" +definition IV :: "state set" + where "IV = {s. (v s = (1 \ n s & n s \ 3)) & (n s = 3 --> p s)}" (** The faulty invariant (for U alone) **) - bad_IU :: "state set" - "bad_IU == {s. (u s = (1 \ m s & m s \ 3)) & +definition bad_IU :: "state set" + where "bad_IU = {s. (u s = (1 \ m s & m s \ 3)) & (3 \ m s & m s \ 4 --> ~ p s)}" diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Simple/NSP_Bad.thy --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Wed May 12 16:45:59 2010 +0200 @@ -17,36 +17,38 @@ types state = "event list" -constdefs - (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) +definition Fake :: "(state*state) set" - "Fake == {(s,s'). + where "Fake = {(s,s'). \B X. s' = Says Spy B X # s & X \ synth (analz (spies s))}" (*The numeric suffixes on A identify the rule*) (*Alice initiates a protocol run, sending a nonce to Bob*) +definition NS1 :: "(state*state) set" - "NS1 == {(s1,s'). + where "NS1 = {(s1,s'). \A1 B NA. s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1 & Nonce NA \ used s1}" (*Bob responds to Alice's message with a further nonce*) +definition NS2 :: "(state*state) set" - "NS2 == {(s2,s'). + where "NS2 = {(s2,s'). \A' A2 B NA NB. s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2 & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) \ set s2 & Nonce NB \ used s2}" (*Alice proves her existence by sending NB back to Bob.*) +definition NS3 :: "(state*state) set" - "NS3 == {(s3,s'). + where "NS3 = {(s3,s'). \A3 B' B NA NB. s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3 & Says A3 B (Crypt (pubK B) {|Nonce NA, Agent A3|}) \ set s3 @@ -55,7 +57,7 @@ definition Nprg :: "state program" where (*Initial trace is empty*) - "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)" + "Nprg = mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)" declare spies_partsEs [elim] declare analz_into_parts [dest] diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Simple/Reach.thy --- a/src/HOL/UNITY/Simple/Reach.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Simple/Reach.thy Wed May 12 16:45:59 2010 +0200 @@ -17,20 +17,20 @@ edges :: "(vertex*vertex) set" -definition asgt :: "[vertex,vertex] => (state*state) set" where - "asgt u v == {(s,s'). s' = s(v:= s u | s v)}" +definition asgt :: "[vertex,vertex] => (state*state) set" + where "asgt u v = {(s,s'). s' = s(v:= s u | s v)}" -definition Rprg :: "state program" where - "Rprg == mk_total_program ({%v. v=init}, \(u,v)\edges. {asgt u v}, UNIV)" +definition Rprg :: "state program" + where "Rprg = mk_total_program ({%v. v=init}, \(u,v)\edges. {asgt u v}, UNIV)" -definition reach_invariant :: "state set" where - "reach_invariant == {s. (\v. s v --> (init, v) \ edges^*) & s init}" +definition reach_invariant :: "state set" + where "reach_invariant = {s. (\v. s v --> (init, v) \ edges^*) & s init}" -definition fixedpoint :: "state set" where - "fixedpoint == {s. \(u,v)\edges. s u --> s v}" +definition fixedpoint :: "state set" + where "fixedpoint = {s. \(u,v)\edges. s u --> s v}" -definition metric :: "state => nat" where - "metric s == card {v. ~ s v}" +definition metric :: "state => nat" + where "metric s = card {v. ~ s v}" text{**We assume that the set of vertices is finite*} diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/UNITY.thy --- a/src/HOL/UNITY/UNITY.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/UNITY.thy Wed May 12 16:45:59 2010 +0200 @@ -431,26 +431,26 @@ text{*They avoid expanding the full program, which is a large expression*} lemma def_prg_Init: - "F == mk_total_program (init,acts,allowed) ==> Init F = init" + "F = mk_total_program (init,acts,allowed) ==> Init F = init" by (simp add: mk_total_program_def) lemma def_prg_Acts: - "F == mk_total_program (init,acts,allowed) + "F = mk_total_program (init,acts,allowed) ==> Acts F = insert Id (totalize_act ` acts)" by (simp add: mk_total_program_def) lemma def_prg_AllowedActs: - "F == mk_total_program (init,acts,allowed) + "F = mk_total_program (init,acts,allowed) ==> AllowedActs F = insert Id allowed" by (simp add: mk_total_program_def) text{*An action is expanded if a pair of states is being tested against it*} lemma def_act_simp: - "act == {(s,s'). P s s'} ==> ((s,s') \ act) = P s s'" + "act = {(s,s'). P s s'} ==> ((s,s') \ act) = P s s'" by (simp add: mk_total_program_def) text{*A set is expanded only if an element is being tested against it*} -lemma def_set_simp: "A == B ==> (x \ A) = (x \ B)" +lemma def_set_simp: "A = B ==> (x \ A) = (x \ B)" by (simp add: mk_total_program_def) subsubsection{*Inspectors for type "program"*} diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/UNITY/Union.thy Wed May 12 16:45:59 2010 +0200 @@ -9,31 +9,35 @@ theory Union imports SubstAx FP begin -constdefs - (*FIXME: conjoin Init F \ Init G \ {} *) +definition ok :: "['a program, 'a program] => bool" (infixl "ok" 65) - "F ok G == Acts F \ AllowedActs G & + where "F ok G == Acts F \ AllowedActs G & Acts G \ AllowedActs F" (*FIXME: conjoin (\i \ I. Init (F i)) \ {} *) +definition OK :: "['a set, 'a => 'b program] => bool" - "OK I F == (\i \ I. \j \ I-{i}. Acts (F i) \ AllowedActs (F j))" + where "OK I F = (\i \ I. \j \ I-{i}. Acts (F i) \ AllowedActs (F j))" +definition JOIN :: "['a set, 'a => 'b program] => 'b program" - "JOIN I F == mk_program (\i \ I. Init (F i), \i \ I. Acts (F i), + where "JOIN I F = mk_program (\i \ I. Init (F i), \i \ I. Acts (F i), \i \ I. AllowedActs (F i))" +definition Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65) - "F Join G == mk_program (Init F \ Init G, Acts F \ Acts G, + where "F Join G = mk_program (Init F \ Init G, Acts F \ Acts G, AllowedActs F \ AllowedActs G)" +definition SKIP :: "'a program" - "SKIP == mk_program (UNIV, {}, UNIV)" + where "SKIP = mk_program (UNIV, {}, UNIV)" (*Characterizes safety properties. Used with specifying Allowed*) +definition safety_prop :: "'a program set => bool" - "safety_prop X == SKIP: X & (\G. Acts G \ UNION X Acts --> G \ X)" + where "safety_prop X <-> SKIP: X & (\G. Acts G \ UNION X Acts --> G \ X)" notation (xsymbols) SKIP ("\") and @@ -420,12 +424,12 @@ by (simp add: Allowed_def) lemma def_total_prg_Allowed: - "[| F == mk_total_program (init, acts, UNION X Acts) ; safety_prop X |] + "[| F = mk_total_program (init, acts, UNION X Acts) ; safety_prop X |] ==> Allowed F = X" by (simp add: mk_total_program_def def_prg_Allowed) lemma def_UNION_ok_iff: - "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |] + "[| F = mk_program(init,acts,UNION X Acts); safety_prop X |] ==> F ok G = (G \ X & acts \ AllowedActs G)" by (auto simp add: ok_def safety_prop_Acts_iff) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Unix/Unix.thy --- a/src/HOL/Unix/Unix.thy Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Unix/Unix.thy Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Unix/Unix.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/Word/document/root.tex --- a/src/HOL/Word/document/root.tex Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/Word/document/root.tex Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,3 @@ -% $Id$ - \documentclass[11pt,a4paper]{article} \usepackage{graphicx,isabelle,isabellesym} \usepackage{pdfsetup} diff -r b78d3c87fc88 -r f99ae7e27150 src/HOL/ZF/document/root.tex --- a/src/HOL/ZF/document/root.tex Wed May 12 15:25:23 2010 +0200 +++ b/src/HOL/ZF/document/root.tex Wed May 12 16:45:59 2010 +0200 @@ -1,6 +1,3 @@ - -% $Id$ - \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} diff -r b78d3c87fc88 -r f99ae7e27150 src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Wed May 12 15:25:23 2010 +0200 +++ b/src/HOLCF/Tools/fixrec.ML Wed May 12 16:45:59 2010 +0200 @@ -427,7 +427,7 @@ fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = let - val _ = legacy_feature "\"fixpat\"; prefer \"fixrec_simp\" method instead"; + val _ = legacy_feature "Old 'fixpat' command -- use \"fixrec_simp\" method instead"; val atts = map (prep_attrib thy) srcs; val ts = map (prep_term thy) strings; val simps = map (fix_pat thy) ts; diff -r b78d3c87fc88 -r f99ae7e27150 src/LCF/IsaMakefile --- a/src/LCF/IsaMakefile Wed May 12 15:25:23 2010 +0200 +++ b/src/LCF/IsaMakefile Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,3 @@ -# -# $Id$ # # IsaMakefile for LCF # diff -r b78d3c87fc88 -r f99ae7e27150 src/LCF/README.html --- a/src/LCF/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/LCF/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Wed May 12 15:25:23 2010 +0200 +++ b/src/Pure/Isar/constdefs.ML Wed May 12 16:45:59 2010 +0200 @@ -22,7 +22,7 @@ fun gen_constdef prep_vars prep_prop prep_att structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy = let - val _ = legacy_feature ("\"constdefs\"; prefer \"definition\" instead"); + val _ = legacy_feature "Old 'constdefs' command -- use 'definition' instead"; fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); diff -r b78d3c87fc88 -r f99ae7e27150 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed May 12 15:25:23 2010 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed May 12 16:45:59 2010 +0200 @@ -181,7 +181,10 @@ val _ = OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl - (Scan.repeat1 SpecParse.spec >> (Toplevel.theory o IsarCmd.add_axioms)); + (Scan.repeat1 SpecParse.spec >> + (Toplevel.theory o + (IsarCmd.add_axioms o + tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead")))); val opt_unchecked_overloaded = Scan.optional (P.$$$ "(" |-- P.!!! diff -r b78d3c87fc88 -r f99ae7e27150 src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Wed May 12 15:25:23 2010 +0200 +++ b/src/Pure/old_goals.ML Wed May 12 16:45:59 2010 +0200 @@ -293,7 +293,6 @@ *) fun prepare_proof atomic rths chorn = let - val _ = legacy_feature "Old goal command"; val thy = Thm.theory_of_cterm chorn; val horn = Thm.term_of chorn; val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg; @@ -514,7 +513,6 @@ (*simple version with minimal amount of checking and postprocessing*) fun simple_prove_goal_cterm G f = let - val _ = legacy_feature "Old goal command"; val As = Drule.strip_imp_prems G; val B = Drule.strip_imp_concl G; val asms = map Assumption.assume As; diff -r b78d3c87fc88 -r f99ae7e27150 src/Sequents/IsaMakefile --- a/src/Sequents/IsaMakefile Wed May 12 15:25:23 2010 +0200 +++ b/src/Sequents/IsaMakefile Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,3 @@ -# -# $Id$ # # IsaMakefile for Sequents # diff -r b78d3c87fc88 -r f99ae7e27150 src/Sequents/README.html --- a/src/Sequents/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/Sequents/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/Tools/WWW_Find/doc/design.tex --- a/src/Tools/WWW_Find/doc/design.tex Wed May 12 15:25:23 2010 +0200 +++ b/src/Tools/WWW_Find/doc/design.tex Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,3 @@ -% $Id$ -% % vim:nojs: tw=76 sw=4 sts=4 fo=awn fdm=marker % % 20090406 T. Bourke diff -r b78d3c87fc88 -r f99ae7e27150 src/Tools/WWW_Find/www/find_theorems.js --- a/src/Tools/WWW_Find/www/find_theorems.js Wed May 12 15:25:23 2010 +0200 +++ b/src/Tools/WWW_Find/www/find_theorems.js Wed May 12 16:45:59 2010 +0200 @@ -1,4 +1,4 @@ -/* $Id$ +/* * Author: Timothy Bourke, NICTA */ var utf8 = new Object(); diff -r b78d3c87fc88 -r f99ae7e27150 src/ZF/AC/README.html --- a/src/ZF/AC/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/ZF/AC/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/ZF/Coind/README.html --- a/src/ZF/Coind/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/ZF/Coind/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/ZF/Constructible/README.html --- a/src/ZF/Constructible/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/ZF/Constructible/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/ZF/IMP/README.html --- a/src/ZF/IMP/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/ZF/IMP/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Wed May 12 15:25:23 2010 +0200 +++ b/src/ZF/IsaMakefile Wed May 12 16:45:59 2010 +0200 @@ -1,5 +1,3 @@ -# -# $Id$ # # IsaMakefile for ZF # diff -r b78d3c87fc88 -r f99ae7e27150 src/ZF/README.html --- a/src/ZF/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/ZF/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/ZF/Resid/README.html --- a/src/ZF/Resid/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/ZF/Resid/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - - diff -r b78d3c87fc88 -r f99ae7e27150 src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Wed May 12 15:25:23 2010 +0200 +++ b/src/ZF/Tools/ind_cases.ML Wed May 12 16:45:59 2010 +0200 @@ -19,7 +19,7 @@ structure IndCasesData = Theory_Data ( - type T = (Proof.context -> cterm -> thm) Symtab.table; + type T = (Proof.context -> conv) Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data = Symtab.merge (K true) data; diff -r b78d3c87fc88 -r f99ae7e27150 src/ZF/ex/README.html --- a/src/ZF/ex/README.html Wed May 12 15:25:23 2010 +0200 +++ b/src/ZF/ex/README.html Wed May 12 16:45:59 2010 +0200 @@ -1,7 +1,5 @@ - -