HOL.thy:
"@" is no longer introduced as a "binder" but has its own explicit
translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further
translation rules for abstractions with patterns take care of the rest. This
is very modular and avoids problems with "binders" such as "!" mentioned
below.
let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u)
Set.thy:
UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@"
above, except that "@" was a "binder" originally.
Prod.thy:
Added new syntax for pttrn which allows arbitrarily nested tuples. Two
translation rules take care of %pttrn. Unfortunately they cannot be
reversed. Hence a little ML-code is used as well.
Note that now "! (x,y). ..." is syntactically valid but leads to a
translation error. This is because "!" is introduced as a "binder" which
means that its translation into lambda-terms is not done by a rewrite rule
(aka macro) but by some fixed ML-code which comes after the rewriting stage
and does not know how to handle patterns. This looks like a minor blemish
since patterns in unbounded quantifiers are not that useful (well, except
maybe in unique existence ...). Ideally, there should be two syntactic
categories:
idts, as we know and love it, which does not admit patterns.
patterns, which is what idts has become now.
There is one more point where patterns are now allowed but don't make sense:
{e | idts . P}
where idts is the list of local variables.
Univ.thy: converted the defs for <++> and <**> into pattern form. It worked
perfectly.
#! /bin/sh
#
#make-all: make all systems afresh
# Creates gzipped log files called makeNNNN.log.gz on each subdirectory and
# displays the last few lines of these files -- this indicates whether
# the "make" failed (whether it terminated due to an error)
# switches are
# -noforce don't delete old databases/images first
# -clean delete databases/images after use (leaving Pure)
# -notest make databases/images w/o running the examples
# -noexec don't execute, just check settings and Makefiles
#Environment variables required:
# ISABELLEBIN: the directory to hold Poly/ML databases or New Jersey ML images
# ISABELLECOMP: the ML compiler
# A typical shell script for /bin/sh is...
# ML_DBASE=/usr/groups/theory/poly2.04/`arch`/ML_dbase
# ISABELLEBIN=/homes/`whoami`/bin
# ISABELLECOMP="poly -noDisplay"
# export ML_DBASE ISABELLEBIN ISABELLECOMP
# nohup make-all $*
set -e #fail immediately upon errors
# process command line switches
CLEAN="off";
FORCE="on";
TEST="test";
EXEC="on";
NO="";
for A in $*
do
case $A in
-clean) CLEAN="on" ;;
-noforce) FORCE="off" ;;
-notest) TEST="" ;;
-noexec) EXEC="off"
NO="-n" ;;
*) echo "Bad flag for make-all: $A"
echo "Usage: make-all [-noforce] [-clean] [-notest] [-noexec]"
exit ;;
esac
done
echo Started at `date`
echo Source=`pwd`
echo Destination=${ISABELLEBIN?'No destination directory specified'}
echo force=$FORCE ' ' clean=$CLEAN ' '
echo Compiler=${ISABELLECOMP?'No compiler specified'}
echo Running on `hostname`
echo Log files will be called make$$.log.gz
case $FORCE.$EXEC in
on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL HOLCF Cube FOLP)
esac
set +e #no longer fail upon errors -- e.g. if a "make" fails
echo
echo
echo '*****Pure Isabelle*****'
(cd Pure; make $NO > make$$.log)
tail Pure/make$$.log
gzip Pure/make$$.log
echo
echo
echo '*****First-Order Logic (FOL)*****'
(cd FOL; make $NO $TEST > make$$.log)
tail FOL/make$$.log
gzip FOL/make$$.log
#cannot delete FOL yet... it is needed for ZF, CCL and LCF!
echo
echo
echo '*****Set theory (ZF)*****'
(cd ZF; make $NO $TEST > make$$.log)
tail ZF/make$$.log
gzip ZF/make$$.log
case $CLEAN.$EXEC in
on.on) rm $ISABELLEBIN/ZF
esac
echo
echo
echo '*****Classical Computational Logic (CCL)*****'
(cd CCL; make $NO $TEST > make$$.log)
tail CCL/make$$.log
gzip CCL/make$$.log
case $CLEAN.$EXEC in
on.on) rm $ISABELLEBIN/CCL
esac
echo
echo
echo '*****Domain Theory (LCF)*****'
(cd LCF; make $NO $TEST > make$$.log)
tail LCF/make$$.log
gzip LCF/make$$.log
case $CLEAN.$EXEC in
on.on) rm $ISABELLEBIN/FOL $ISABELLEBIN/LCF
esac
echo
echo
echo '*****Constructive Type Theory (CTT)*****'
(cd CTT; make $NO $TEST > make$$.log)
tail CTT/make$$.log
gzip CTT/make$$.log
case $CLEAN.$EXEC in
on.on) rm $ISABELLEBIN/CTT
esac
echo
echo
echo '*****Classical Sequent Calculus (LK)*****'
(cd LK; make $NO $TEST > make$$.log)
tail LK/make$$.log
gzip LK/make$$.log
#cannot delete LK yet... it is needed for Modal!
echo
echo
echo '*****Modal logic (Modal)*****'
(cd Modal; make $NO $TEST > make$$.log)
tail Modal/make$$.log
gzip Modal/make$$.log
case $CLEAN.$EXEC in
on.on) rm $ISABELLEBIN/LK $ISABELLEBIN/Modal
esac
echo
echo
echo '*****Higher-Order Logic (HOL)*****'
(cd HOL; make $NO $TEST > make$$.log)
tail HOL/make$$.log
gzip HOL/make$$.log
#cannot delete HOL yet... it is needed for HOLCF!
echo
echo
echo '*****LCF in HOL (HOLCF)*****'
(cd HOLCF; make $NO $TEST > make$$.log)
tail HOLCF/make$$.log
gzip HOLCF/make$$.log
case $CLEAN.$EXEC in
on.on) rm $ISABELLEBIN/HOL $ISABELLEBIN/HOLCF
esac
echo
echo
echo '*****The Lambda-Cube (Cube)*****'
(cd Cube; make $NO $TEST > make$$.log)
case $CLEAN.$EXEC in
on.on) rm $ISABELLEBIN/Cube
esac
tail Cube/make$$.log
gzip Cube/make$$.log
echo
echo
echo '*****First-Order Logic with Proof Terms (FOLP)*****'
(cd FOLP; make $NO $TEST > make$$.log)
case $CLEAN.$EXEC in
on.on) rm $ISABELLEBIN/FOLP
esac
tail FOLP/make$$.log
gzip FOLP/make$$.log
case $TEST.$EXEC in
test.on) echo
echo '***** Now check the dates on the "test" files *****'
ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\
LK/test Modal/test HOL/test HOLCF/test Cube/test\
FOLP/test
esac
echo Finished at `date`