CTT/README

# HG changeset patch # User webertj # Date 1100392827 -3600 # Node ID f2146645033025c9e87024ace950a4d3d06cd914 # Parent 765d5d6e4468e6f6f0defffb307b4f999b8158a4 DOCTYPE declaration added diff -r 765d5d6e4468 -r f21466450330 etc/settings --- a/etc/settings Sat Nov 13 17:30:03 2004 +0100 +++ b/etc/settings Sun Nov 14 01:40:27 2004 +0100 @@ -224,8 +224,8 @@ # Einhoven model checker #EINDHOVEN_HOME=/usr/local/bin -# ZChaff, Version 2003.12.04 (SAT Solver) -#ZCHAFF_HOME=/usr/local/bin +# ZChaff, Version 2004.05.13 (SAT Solver) +ZCHAFF_HOME=/home/webertj/bin # BerkMin561 (SAT Solver) #BERKMIN_HOME=/usr/local/bin diff -r 765d5d6e4468 -r f21466450330 src/CTT/README.html --- a/src/CTT/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/CTT/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,4 @@ + CTT/README @@ -11,8 +12,8 @@ Useful references on Constructive Type Theory:

B. Nordström, K. Petersson and J. M. Smith,
- Programming in Martin-Löf's Type Theory
+
B. Nordstrm, K. Petersson and J. M. Smith,
+ Programming in Martin-Lf's Type Theory
(Oxford University Press, 1990)
Simon Thompson,
diff -r 765d5d6e4468 -r f21466450330 src/Cube/README.html --- a/src/Cube/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/Cube/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,4 @@ + Cube/README diff -r 765d5d6e4468 -r f21466450330 src/FOL/README.html --- a/src/FOL/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/FOL/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + FOL/README
FOL: First-Order Logic with Natural Deduction
diff -r 765d5d6e4468 -r f21466450330 src/HOL/Algebra/README.html --- a/src/HOL/Algebra/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Algebra/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/Algebra/README.html @@ -12,7 +14,7 @@
GroupTheory, including Sylow's Theorem
-
These proofs are mainly by Florian Kammüller. (Later, Larry +
These proofs are mainly by Florian Kammller. (Later, Larry Paulson simplified some of the proofs.) These theories were indeed the original motivation for locales. diff -r 765d5d6e4468 -r f21466450330 src/HOL/Auth/Guard/README.html --- a/src/HOL/Auth/Guard/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Auth/Guard/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/Auth/Guard/README.html diff -r 765d5d6e4468 -r f21466450330 src/HOL/Auth/README.html --- a/src/HOL/Auth/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Auth/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/Auth/README
Auth--The Inductive Approach to Verifying Security Protocols
diff -r 765d5d6e4468 -r f21466450330 src/HOL/AxClasses/README.html --- a/src/HOL/AxClasses/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/AxClasses/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + diff -r 765d5d6e4468 -r f21466450330 src/HOL/Complex/README.html --- a/src/HOL/Complex/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Complex/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/Complex/README diff -r 765d5d6e4468 -r f21466450330 src/HOL/Hoare/README.html --- a/src/HOL/Hoare/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Hoare/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/Hoare/ReadMe
Hoare Logic for a Simple WHILE Language
diff -r 765d5d6e4468 -r f21466450330 src/HOL/IMPP/README.html --- a/src/HOL/IMPP/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/IMPP/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/IMPP/README diff -r 765d5d6e4468 -r f21466450330 src/HOL/IOA/README.html --- a/src/HOL/IOA/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/IOA/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOLCF/IOA/README
IOA: A basic formalization of I/O automata in HOL
diff -r 765d5d6e4468 -r f21466450330 src/HOL/Induct/README.html --- a/src/HOL/Induct/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Induct/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/Induct/README diff -r 765d5d6e4468 -r f21466450330 src/HOL/Isar_examples/README.html --- a/src/HOL/Isar_examples/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Isar_examples/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + diff -r 765d5d6e4468 -r f21466450330 src/HOL/Lambda/README.html --- a/src/HOL/Lambda/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Lambda/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/Lambda diff -r 765d5d6e4468 -r f21466450330 src/HOL/Library/README.html --- a/src/HOL/Library/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Library/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + diff -r 765d5d6e4468 -r f21466450330 src/HOL/Modelcheck/README.html --- a/src/HOL/Modelcheck/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Modelcheck/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + diff -r 765d5d6e4468 -r f21466450330 src/HOL/Prolog/README.html --- a/src/HOL/Prolog/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Prolog/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/Prolog/README diff -r 765d5d6e4468 -r f21466450330 src/HOL/README.html --- a/src/HOL/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + diff -r 765d5d6e4468 -r f21466450330 src/HOL/Real/HahnBanach/README.html --- a/src/HOL/Real/HahnBanach/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Real/HahnBanach/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,8 +1,10 @@ + + HOL/Real/HahnBanach/README -
The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar).
+
The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)
-Author: Gertrud Bauer, Technische Universität München
+Author: Gertrud Bauer, Technische Universität München
This directory contains the proof of the Hahn-Banach theorem for real vectorspaces, following H. Heuser, Funktionalanalysis, p. 228 -232. diff -r 765d5d6e4468 -r f21466450330 src/HOL/TLA/README.html --- a/src/HOL/TLA/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/TLA/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/TLA
TLA: Lamport's Temporal Logic of Actions
@@ -56,4 +58,4 @@ Last modified: Mon Jan 25 14:06:43 MET 1999 - \ No newline at end of file + diff -r 765d5d6e4468 -r f21466450330 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/Tools/refute.ML Sun Nov 14 01:40:27 2004 +0100 @@ -1141,11 +1141,11 @@ (* unit -> (interpretation * model * arguments) option *) fun interpret_groundtype () = let - val size = (if T = Term.propT then 2 else (the o assoc) (typs, T)) (* the model MUST specify a size for ground types *) - val next = (if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 2 *) - val _ = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *) + val size = (if T = Term.propT then 2 else (the o assoc) (typs, T)) (* the model MUST specify a size for ground types *) + val next = (if size=1 then next_idx else if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 1 or 2 *) + val _ = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *) (* prop_formula list *) - val fms = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)] + val fms = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)] else (map BoolVar (next_idx upto (next_idx+size-1)))) (* interpretation *) val intr = Leaf fms @@ -1155,7 +1155,7 @@ (* prop_formula list -> prop_formula *) fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs) (* prop_formula *) - val wf = (if size=2 then True else exactly_one_true fms) + val wf = (if size=1 then True else if size=2 then True else exactly_one_true fms) in (* extend the model, increase 'next_idx', add well-formedness condition *) Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)}) @@ -1327,7 +1327,7 @@ in (* ------------------------------------------------------------------------- *) (* Providing interpretations directly is more efficient than unfolding the *) - (* logical constants. IN HOL however, logical constants can themselves be *) + (* logical constants. In HOL however, logical constants can themselves be *) (* arguments. "All" and "Ex" are then translated just like any other *) (* constant, with the relevant axiom being added by 'collect_axioms'. *) (* ------------------------------------------------------------------------- *) @@ -1509,10 +1509,10 @@ (* recursively compute the size of the datatype *) val size = size_of_dtyp typs' descr typ_assoc constrs val next_idx = #next_idx args - val next = (if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 2 *) + val next = (if size=1 then next_idx else if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 1 or size 2 *) val _ = (if next-1>(#maxvars args) andalso (#maxvars args)>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *) (* prop_formula list *) - val fms = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)] + val fms = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)] else (map BoolVar (next_idx upto (next_idx+size-1)))) (* interpretation *) val intr = Leaf fms @@ -1522,7 +1522,7 @@ (* prop_formula list -> prop_formula *) fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs) (* prop_formula *) - val wf = (if size=2 then True else exactly_one_true fms) + val wf = (if size=1 then True else if size=2 then True else exactly_one_true fms) in (* extend the model, increase 'next_idx', add well-formedness condition *) Some (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)}) diff -r 765d5d6e4468 -r f21466450330 src/HOL/UNITY/Comp/README.html --- a/src/HOL/UNITY/Comp/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/UNITY/Comp/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/UNITY/README diff -r 765d5d6e4468 -r f21466450330 src/HOL/UNITY/README.html --- a/src/HOL/UNITY/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/UNITY/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/UNITY/README diff -r 765d5d6e4468 -r f21466450330 src/HOL/UNITY/Simple/README.html --- a/src/HOL/UNITY/Simple/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/UNITY/Simple/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/UNITY/README diff -r 765d5d6e4468 -r f21466450330 src/HOL/W0/README.html --- a/src/HOL/W0/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/W0/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/W0/README diff -r 765d5d6e4468 -r f21466450330 src/HOL/ex/README.html --- a/src/HOL/ex/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOL/ex/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOL/ex/README diff -r 765d5d6e4468 -r f21466450330 src/HOLCF/FOCUS/README.html --- a/src/HOLCF/FOCUS/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOLCF/FOCUS/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOLCF/README
FOCUS: a theory of stream-processing functions Isabelle/HOLCF
diff -r 765d5d6e4468 -r f21466450330 src/HOLCF/IMP/README.html --- a/src/HOLCF/IMP/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOLCF/IMP/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,8 +1,10 @@ + + HOLCF/IMP/README -
IMP --- A WHILE-language and its Semantics
+
IMP -- A WHILE-language and its Semantics
This is the HOLCF-based denotational semantics of a simple -WHILE-language. For a full description see HOL/IMP. +WHILE-language. For a full description see HOL/IMP. diff -r 765d5d6e4468 -r f21466450330 src/HOLCF/IOA/README.html --- a/src/HOLCF/IOA/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOLCF/IOA/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOLCF/IOA/README
IOA: A formalization of I/O automata in HOLCF
diff -r 765d5d6e4468 -r f21466450330 src/HOLCF/README.html --- a/src/HOLCF/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/HOLCF/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + HOLCF/README
HOLCF: A higher-order version of LCF based on Isabelle/HOL
diff -r 765d5d6e4468 -r f21466450330 src/LCF/README.html --- a/src/LCF/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/LCF/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + LCF/README
LCF: Logic for Computable Functions
diff -r 765d5d6e4468 -r f21466450330 src/Sequents/README.html --- a/src/Sequents/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/Sequents/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + Sequents/README diff -r 765d5d6e4468 -r f21466450330 src/ZF/AC/README.html --- a/src/ZF/AC/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/ZF/AC/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + ZF/AC/README @@ -16,7 +18,9 @@
The report -Mechanizing Set Theory, by Paulson and Grabczewski, describes both this development and ZF's theories of cardinals. +Mechanizing Set Theory, +by Paulson and Grabczewski, describes both this development and ZF's theories +of cardinals. diff -r 765d5d6e4468 -r f21466450330 src/ZF/Coind/README.html --- a/src/ZF/Coind/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/ZF/Coind/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + ZF/Coind/README diff -r 765d5d6e4468 -r f21466450330 src/ZF/Constructible/README.html --- a/src/ZF/Constructible/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/ZF/Constructible/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,8 +1,10 @@ + + ZF/Constructible/README
Constructible--Relative Consistency of the Axiom of Choice
-
Gödel's proof of the relative consistency of the axiom of choice is +
Gödel's proof of the relative consistency of the axiom of choice is mechanized using Isabelle/ZF. The proof builds upon a previous mechanization of the reflection @@ -25,4 +27,4 @@ HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson, lcp@cl.cam.ac.uk - \ No newline at end of file + diff -r 765d5d6e4468 -r f21466450330 src/ZF/IMP/README.html --- a/src/ZF/IMP/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/ZF/IMP/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,12 +1,13 @@ + + ZF/IMP/README
IMP -- A while-language and two semantics
-The formalization of the denotational and operational semantics of -a simple while-language together with an equivalence proof between the two -semantics. The whole development essentially formalizes/transcribes chapters -2 and 5 of +The formalization of the denotational and operational semantics of a simple +while-language together with an equivalence proof between the two semantics. +The whole development essentially formalizes/transcribes chapters 2 and 5 of
```
 @book{Winskel,
@@ -16,9 +17,9 @@
  year = 1993}.
 
```
-There is a - -report by Lötzbeyer and Sandner. +There is a +report +by Lötzbeyer and Sandner.
A much extended version of this development is found in HOL/IMP. diff -r 765d5d6e4468 -r f21466450330 src/ZF/README.html --- a/src/ZF/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/ZF/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + ZF/README
ZF: Zermelo-Fraenkel Set Theory
@@ -23,7 +25,7 @@
Resid
subdirectory containing a proof of the Church-Rosser Theorem. It is -by Ole Rasmussen, following the Coq proof by Gérard Huet.
+by Ole Rasmussen, following the Coq proof by Gï¿½ard Huet.

ex
subdirectory containing various examples. diff -r 765d5d6e4468 -r f21466450330 src/ZF/Resid/README.html --- a/src/ZF/Resid/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/ZF/Resid/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + ZF/Resid/README diff -r 765d5d6e4468 -r f21466450330 src/ZF/ex/README.html --- a/src/ZF/ex/README.html Sat Nov 13 17:30:03 2004 +0100 +++ b/src/ZF/ex/README.html Sun Nov 14 01:40:27 2004 +0100 @@ -1,3 +1,5 @@ + + ZF/ex/README

FOL: First-Order Logic with Natural Deduction

GroupTheory, including Sylow's Theorem

Auth--The Inductive Approach to Verifying Security Protocols

Hoare Logic for a Simple WHILE Language

IOA: A basic formalization of I/O automata in HOL

The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar).

The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)

TLA: Lamport's Temporal Logic of Actions

FOCUS: a theory of stream-processing functions Isabelle/HOLCF

IMP --- A `WHILE`-language and its Semantics

IMP -- A `WHILE`-language and its Semantics

IOA: A formalization of I/O automata in HOLCF

HOLCF: A higher-order version of LCF based on Isabelle/HOL

LCF: Logic for Computable Functions

Constructible--Relative Consistency of the Axiom of Choice

IMP -- A `while`-language and two semantics

ZF: Zermelo-Fraenkel Set Theory