--- 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:
--- 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"
--- 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
--- 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
--- 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
-}
--- 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.
--- 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
--- 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
--- 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
--- 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)
--- 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.
--- 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.
--- 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)'
--- 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
--- 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
--- 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
--- 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
--- 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
#
--- 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
#
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- 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
#
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- 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) == \<forall>x. P(x)"
- induct_implies where "induct_implies(A, B) == A \<longrightarrow> B"
- induct_equal where "induct_equal(x, y) == x = y"
- induct_conj where "induct_conj(A, B) == A \<and> B"
+definition "induct_forall(P) == \<forall>x. P(x)"
+definition "induct_implies(A, B) == A \<longrightarrow> B"
+definition "induct_equal(x, y) == x = y"
+definition "induct_conj(A, B) == A \<and> B"
lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))"
unfolding atomize_all induct_forall_def .
--- 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
#
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<html>
<head>
--- 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}
--- 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
#
--- 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 \<notin> 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. \<exists>A Peer Ta. Says Kas A
+ authKeys :: "event list => key set" where
+ "authKeys evs = {authK. \<exists>A Peer Ta. Says Kas A
(Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Number Ta,
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Number Ta\<rbrace>)
\<rbrace>) \<in> 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 ==
- \<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
- X \<notin> parts (spies (takeWhile (% z. z \<noteq> Says A B Y) (rev evs)))"
+ ("_ Issues _ with _ on _") where
+ "A Issues B with X on evs =
+ (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
+ X \<notin> parts (spies (takeWhile (% z. z \<noteq> 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 \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
+ where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
consts
--- 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 \<notin> 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. \<exists>A Peer Ta. Says Kas A
+ authKeys :: "event list => key set" where
+ "authKeys evs = {authK. \<exists>A Peer Ta. Says Kas A
(Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Number Ta,
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Number Ta\<rbrace>)
\<rbrace>) \<in> 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 \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
+ where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
consts
--- 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 \<notin> 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. \<exists>A Peer Ta.
+ authKeys :: "event list => key set" where
+ "authKeys evs = {authK. \<exists>A Peer Ta.
Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authK, Agent Peer, Ta\<rbrace>,
Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key authK, Ta\<rbrace>
\<rbrace> \<in> 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 ==
- \<exists>Y. Says A B Y \<in> set evs \<and> X \<in> parts {Y} \<and>
- X \<notin> parts (spies (takeWhile (% z. z \<noteq> Says A B Y) (rev evs)))"
+ ("_ Issues _ with _ on _") where
+ "A Issues B with X on evs =
+ (\<exists>Y. Says A B Y \<in> set evs \<and> X \<in> parts {Y} \<and>
+ X \<notin> parts (spies (takeWhile (% z. z \<noteq> Says A B Y) (rev evs))))"
consts
--- 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 ==
- \<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
- X \<notin> parts (spies (takeWhile (% z. z \<noteq> Says A B Y) (rev evs)))"
+ ("_ Issues _ with _ on _") where
+ "A Issues B with X on evs =
+ (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
+ X \<notin> parts (spies (takeWhile (% z. z \<noteq> 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 \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
+ where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
inductive_set bankerberos :: "event list set"
--- 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 \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
+ where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
inductive_set bankerb_gets :: "event list set"
--- 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 ==
- \<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
- X \<notin> parts (spies (takeWhile (% z. z \<noteq> Says A B Y) (rev evs)))"
+ ("_ Issues _ with _ on _") where
+ "A Issues B with X on evs =
+ (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
+ X \<notin> parts (spies (takeWhile (% z. z \<noteq> Says A B Y) (rev evs))))"
inductive_set ns_shared :: "event list set"
--- 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
*)
--- 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
*)
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- 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 \<Rightarrow> 'a ref) \<Rightarrow> ('a \<times> 'a) set"
- "rel m == {(x,y). m x = Ref y}"
+ where "rel m = {(x,y). m x = Ref y}"
+
+definition
relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set"
- "relS M == (\<Union> m \<in> M. rel m)"
+ where "relS M = (\<Union> m \<in> M. rel m)"
+
+definition
addrs :: "'a ref set \<Rightarrow> 'a set"
- "addrs P == {a. Ref a \<in> P}"
+ where "addrs P = {a. Ref a \<in> P}"
+
+definition
reachable :: "('a \<times> 'a) set \<Rightarrow> 'a ref set \<Rightarrow> '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 \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set" ("(_/ | _)" [50, 51] 50)
- "restr r m == {(x,y). (x,y) \<in> r \<and> \<not> m x}"
+ where "restr r m = {(x,y). (x,y) \<in> r \<and> \<not> 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 \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref)"
- "S c l r == (\<lambda>x. if c x then r x else l x)"
+ where "S c l r = (\<lambda>x. if c x then r x else l x)"
text {* Rewrite rules for Lists using S as their mapping *}
--- 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}
--- 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
*)
--- 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
*)
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id -->
-
<html>
<head>
--- 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
*)
--- 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
*)
--- 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
--- 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
*)
--- 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
*)
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- 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
*)
--- 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
*)
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<html>
<head>
--- 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
*)
--- 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
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
*)
--- 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
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- 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
*)
--- 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
*)
--- 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}
--- 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}
--- 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}
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<html>
<head>
--- 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. \<exists>X. Crypt K X \<in> H}"
+ where "keysFor H = invKey ` {K. \<exists>X. Crypt K X \<in> H}"
subsubsection{*Inductive definition of all "parts" of a message.*}
--- 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 \<in> X) = (B \<in> X) &
+ "A = B ==> (A \<in> X) = (B \<in> 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)"
--- 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<arg<send!p>>
& (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<arg<send!p>>
& 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<res<rcv!p>>
& (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
--- 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
--- 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<crCh!p> = MClkRelayArg<arg<memCh!p>>)
@@ -129,29 +151,42 @@
& cst!p = #cs
& rst!p = #rs
& (rmhist!p = #hs1 | rmhist!p = #hs2)
- & MVNROKBA<ires!p>"
+ & MVNROKBA<ires!p>)"
+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),
--- 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
--- 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
--- 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;
--- 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;
--- 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)
\<le> 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 \<le> (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 \<le> NbT}"
+ where "client_bounded = UNIV guarantees Always {s. ALL elt : set (ask s). elt \<le> NbT}"
+definition
--{*spec (5)*}
client_progress :: "'a clientState_d program set"
- "client_progress ==
+ where "client_progress =
Increasing giv guarantees
(INT h. {s. h \<le> giv s & h pfixGe ask s}
LeadsTo {s. tokens h \<le> (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)
\<le> 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))"
--- 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. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
+definition
(*spec (13)*)
merge_follows :: "('a,'b) merge_d program set"
- "merge_follows ==
+ where "merge_follows =
(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
guarantees
(\<Inter>i \<in> 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. \<forall>elt \<in> 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) \<le> 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. \<forall>elt \<in> set (ask s). elt \<le> NbT}
Int
@@ -137,20 +148,23 @@
{s. tokens h \<le> tokens (rel s)})
guarantees (\<Inter>h. {s. h \<le> 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 =
--- 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').
\<exists>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 \<in> atMost NbT &
giv s = [] & ask s = [] & rel s = []},
@@ -55,13 +58,15 @@
\<Union>G \<in> 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]
--- 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},
\<Union>G \<in> preserves (%s. s (c i)). Acts G)"
--- 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},
- \<Union>G \<in> preserves (%s. (c s) i). Acts G)"
+ "Component i = mk_total_program({s. C s = 0 & (c s) i = 0},
+ {a i},
+ \<Union>G \<in> preserves (%s. (c s) i). Acts G)"
declare Component_def [THEN def_prg_Init, simp]
--- 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]
--- 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 == \<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i s. highest j s)}"
+ where "Maximal = (\<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i s. highest j s)})"
-definition Maximal' :: "state set" where
+definition Maximal' :: "state set"
--{* Maximal vertex: equivalent definition*}
- "Maximal' == \<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j)"
+ where "Maximal' = (\<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j))"
-definition Safety :: "state set" where
- "Safety == \<Inter>i. {s. highest i s --> (\<forall>j \<in> neighbors i s. ~highest j s)}"
+definition Safety :: "state set"
+ where "Safety = (\<Inter>i. {s. highest i s --> (\<forall>j \<in> 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]
--- 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]
--- 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}"
--- 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 \<inter> (A <*> UNIV)"
+ where "Restrict A r = r \<inter> (A <*> UNIV)"
+definition
good_map :: "['a*'b => 'c] => bool"
- "good_map h == surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
+ where "good_map h <-> surj h & (\<forall>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. \<exists>y. h(x,y) \<in> C}"
+ where "project_set h C = {x. \<exists>y. h(x,y) \<in> C}"
+definition
extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
- "extend_act h == %act. \<Union>(s,s') \<in> act. \<Union>y. {(h(s,y), h(s',y))}"
+ where "extend_act h = (%act. \<Union>(s,s') \<in> act. \<Union>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'). \<exists>y y'. (h(x,y), h(x',y')) \<in> act}"
+ where "project_act h act = {(x,x'). \<exists>y y'. (h(x,y), h(x',y')) \<in> 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 :
--- 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 \<le> Max"
-constdefs
--{*Abbreviations: the "always" part*}
+definition
above :: "state set"
- "above == {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}"
+ where "above = {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}"
+definition
below :: "state set"
- "below == {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}"
+ where "below = {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}"
+definition
queueing :: "state set"
- "queueing == above \<union> below"
+ where "queueing = above \<union> below"
+definition
goingup :: "state set"
- "goingup == above \<inter> ({s. up s} \<union> -below)"
+ where "goingup = above \<inter> ({s. up s} \<union> -below)"
+definition
goingdown :: "state set"
- "goingdown == below \<inter> ({s. ~ up s} \<union> -above)"
+ where "goingdown = below \<inter> ({s. ~ up s} \<union> -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 \<in> req s}"
+ where "Req n = {s. n \<in> 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 \<in> 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 \<in> req s
& ~(move s & s \<in> 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 \<in> (ready \<inter> 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 \<in> (ready \<inter> 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 \<notin> 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 \<notin> 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'). \<exists>n. s' = s (|req := insert n (req s)|)
& Min \<le> n & n \<le> 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 \<le> floor s & floor s \<le> Max}"
+ where "bounded = {s. Min \<le> floor s & floor s \<le> 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 \<in> req s}"
+ where "stop_floor = {s. stop s & ~ move s --> floor s \<in> req s}"
+definition
moving_up :: "state set"
- "moving_up == {s. ~ stop s & up s -->
+ where "moving_up = {s. ~ stop s & up s -->
(\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}"
+definition
moving_down :: "state set"
- "moving_down == {s. ~ stop s & ~ up s -->
+ where "moving_down = {s. ~ stop s & ~ up s -->
(\<exists>f. Min \<le> f & f \<le> floor s & f \<in> 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
--- 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 \<le> m s & m s \<le> 3)) & (m s = 3 --> ~ p s)}"
+definition IU :: "state set"
+ where "IU = {s. (u s = (1 \<le> m s & m s \<le> 3)) & (m s = 3 --> ~ p s)}"
- IV :: "state set"
- "IV == {s. (v s = (1 \<le> n s & n s \<le> 3)) & (n s = 3 --> p s)}"
+definition IV :: "state set"
+ where "IV = {s. (v s = (1 \<le> n s & n s \<le> 3)) & (n s = 3 --> p s)}"
(** The faulty invariant (for U alone) **)
- bad_IU :: "state set"
- "bad_IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) &
+definition bad_IU :: "state set"
+ where "bad_IU = {s. (u s = (1 \<le> m s & m s \<le> 3)) &
(3 \<le> m s & m s \<le> 4 --> ~ p s)}"
--- 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').
\<exists>B X. s' = Says Spy B X # s
& X \<in> 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').
\<exists>A1 B NA.
s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
& Nonce NA \<notin> used s1}"
(*Bob responds to Alice's message with a further nonce*)
+definition
NS2 :: "(state*state) set"
- "NS2 == {(s2,s').
+ where "NS2 = {(s2,s').
\<exists>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|}) \<in> set s2
& Nonce NB \<notin> used s2}"
(*Alice proves her existence by sending NB back to Bob.*)
+definition
NS3 :: "(state*state) set"
- "NS3 == {(s3,s').
+ where "NS3 = {(s3,s').
\<exists>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|}) \<in> 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]
--- 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}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
+definition Rprg :: "state program"
+ where "Rprg = mk_total_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
-definition reach_invariant :: "state set" where
- "reach_invariant == {s. (\<forall>v. s v --> (init, v) \<in> edges^*) & s init}"
+definition reach_invariant :: "state set"
+ where "reach_invariant = {s. (\<forall>v. s v --> (init, v) \<in> edges^*) & s init}"
-definition fixedpoint :: "state set" where
- "fixedpoint == {s. \<forall>(u,v)\<in>edges. s u --> s v}"
+definition fixedpoint :: "state set"
+ where "fixedpoint = {s. \<forall>(u,v)\<in>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*}
--- 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') \<in> act) = P s s'"
+ "act = {(s,s'). P s s'} ==> ((s,s') \<in> 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 \<in> A) = (x \<in> B)"
+lemma def_set_simp: "A = B ==> (x \<in> A) = (x \<in> B)"
by (simp add: mk_total_program_def)
subsubsection{*Inspectors for type "program"*}
--- 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 \<inter> Init G \<noteq> {} *)
+definition
ok :: "['a program, 'a program] => bool" (infixl "ok" 65)
- "F ok G == Acts F \<subseteq> AllowedActs G &
+ where "F ok G == Acts F \<subseteq> AllowedActs G &
Acts G \<subseteq> AllowedActs F"
(*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *)
+definition
OK :: "['a set, 'a => 'b program] => bool"
- "OK I F == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))"
+ where "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))"
+definition
JOIN :: "['a set, 'a => 'b program] => 'b program"
- "JOIN I F == mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i),
+ where "JOIN I F = mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i),
\<Inter>i \<in> I. AllowedActs (F i))"
+definition
Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65)
- "F Join G == mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
+ where "F Join G = mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
AllowedActs F \<inter> 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 & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
+ where "safety_prop X <-> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
notation (xsymbols)
SKIP ("\<bottom>") 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 \<in> X & acts \<subseteq> AllowedActs G)"
by (auto simp add: ok_def safety_prop_Acts_iff)
--- 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
*)
--- 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}
--- 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}
--- 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;
--- 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
#
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- 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));
--- 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.!!!
--- 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;
--- 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
#
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- 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
--- 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();
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<html>
<head>
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- 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
#
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<html>
<head>
--- 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;
--- 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 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<html>
<head>