Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
#! /bin/sh
#
#expandshort - shell script to expand shorthand goal commands
# ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
# rewrite_goals_tac on 1-element lists
#
# Usage:
# expandshort FILE1 ... FILEn
#
# leaves previous versions as XXX~~
#
for f in $*
do
echo Expanding shorthands in $f. \ Backup file is $f~~
mv $f $f~~; sed -e '
s/^ba \([0-9]*\); *$/by (assume_tac \1);/
s/^br \(.*\) \([0-9]*\); *$/by (rtac \1 \2);/
s/^brs \(.*\) \([0-9]*\); *$/by (resolve_tac \1 \2);/
s/^bd \(.*\) \([0-9]*\); *$/by (dtac \1 \2);/
s/^bds \(.*\) \([0-9]*\); *$/by (dresolve_tac \1 \2);/
s/^be \(.*\) \([0-9]*\); *$/by (etac \1 \2);/
s/^bes \(.*\) \([0-9]*\); *$/by (eresolve_tac \1 \2);/
s/^bw \(.*\); *$/by (rewtac \1);/
s/^bws \(.*\); *$/by (rewrite_goals_tac \1);/
s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
' $f~~ > $f
done
echo Finished.