--- a/src/Tools/Makefile Mon Sep 29 15:11:27 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-OPTIONS= -DDEBUG
-CC = g++ $(OPTIONS)
-OBJS = qed.o
-
-.SUFFIXES: .cc .o
-
-.cc.o:
- $(CC) -c $<
-
-qed: $(OBJS)
- g++ -o qed $(OBJS)
--- a/src/Tools/qed.cc Mon Sep 29 15:11:27 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,163 +0,0 @@
-// Little utility to convert result() -> qed ... in Isabelle's files
-// Written in 1995 by Carsten Clasohm (clasohm@informatik.tu-muenchen.de)
-
-#define LIN_LEN 1000 // maximal length of lines in sourcefile
-
-#include <iostream.h>
-#include <fstream.h>
-#include <string.h>
-#include <assert.h>
-#include <stdio.h>
-#include <unistd.h>
-#include <ctype.h>
-
-// Null terminated list of theorem names that must not be included in the
-// theorem database
-char * excludeName[] = {"temp", "tmp", 0};
-
-int ExcludeThm(char *name)
-{
- for (int i = 0; excludeName[i]; i++)
- if (strcmp(name, excludeName[i]) == 0)
- return 1;
- return 0;
-}
-
-main(int argc, char *argv[])
-{
- char l[LIN_LEN];
- int lines = 0;
-
- // Open input and output files
- ifstream in(argv[1]);
- ofstream out(argv[2]);
-
- if (in.bad() || out.bad())
- {
- cerr << "qed version 1.00, Written in 1994 by Carsten Clasohm"
- "(clasohm@informatik.tu-muenchen.de)\n\n";
- cerr << "Usage: qed <infile> <outfile>\n";
- exit(1);
- }
-
-#ifdef DEBUG
- cerr << "Processing file " << argv[1] << '\n';
-#endif
-
- // Process each line separatly
- in.getline(l, LIN_LEN);
- while (!in.eof())
- {
- char *rPos;
- char *valPos;
- char *eqPos;
- char *tmp;
-
- if ((rPos = strstr(l, "result()")) && (!isalnum(*(rPos-1)))
- && (valPos = strstr(l, "val ")) && (eqPos = strstr(l, "=")))
- { // does line contain "result()" and "val"?
- char name[LIN_LEN];
-
- assert(eqPos-(valPos+4) > 0);
- strncpy(name, valPos+4, eqPos-(valPos+4));
- name[eqPos-(valPos+4)] = 0;
- if (!isalnum(name[eqPos-(valPos+4)-1]))
- name[eqPos-(valPos+4)-1] = 0;
-#ifdef DEBUG
- cerr << "Found result: \"" << name << "\"\n";
-#endif
- char prefix[LIN_LEN];
- char arg[LIN_LEN];
-
- if (ExcludeThm(name))
- out << l << '\n';
- else if ((rPos - eqPos < 5) && (rPos == strstr(l, "result();")))
- { // replace by "qed"?
- strncpy(prefix, l, valPos-l);
- prefix[valPos-l] = 0;
- out << prefix << "qed \"" << name << "\";" << '\n';
- }
- else // replace by bind_thm
- {
- int d = (*(eqPos+1) == ' ') ? 2 : 1;
- strcpy(arg, eqPos+d);
- arg[strlen(arg)-1] = 0;
- strcpy(prefix, l);
- prefix[valPos-l] = 0;
- out << prefix << "bind_thm(\"" << name << "\", "
- << arg << ");\n";
- }
- }
- else if ((rPos = strstr(l, "prove_goal"))
- && (!isalnum(*(rPos-1)))
- && (!isalnum(*(rPos+10)) || (*(rPos+10) == 'w'))
- && (valPos = strstr(l, "val "))
- && (eqPos = strstr(l, "="))
- && (rPos - eqPos < 5))
- { // replace prove_goal by qed_goal?
- char name[LIN_LEN];
-
- assert(eqPos-(valPos+4) > 0);
- strncpy(name, valPos+4, eqPos-(valPos+4));
- name[eqPos-(valPos+4)] = 0;
- if (!isalnum(name[eqPos-(valPos+4)-1]))
- name[eqPos-(valPos+4)-1] = 0;
-#ifdef DEBUG
- cerr << "Found prove_goal: \"" << name << "\"\n";
-#endif
- if (ExcludeThm(name))
- out << l << '\n';
- else
- {
- char prefix[LIN_LEN];
- char arg[LIN_LEN];
-
- strncpy(prefix, l, valPos-l);
- prefix[valPos-l] = 0;
- out << prefix << "qed_goal"
- << ((*(rPos+10) == 'w') ? "w " : " ")
- << '\"' << name << '\"' << strchr(rPos, ' ') << '\n';
- }
- }
- else if ((rPos = strstr(l, "standard"))
- && (!isalnum(*(rPos-1)))
- && (!isalnum(*(rPos+8)))
- && (valPos = strstr(l, "val "))
- && (eqPos = strstr(l, "="))
- && (rPos - eqPos < 5)
- && (l[strlen(l)-1] == ';'))
- { // insert bind_thm?
- char name[LIN_LEN];
-
- assert(eqPos-(valPos+4) > 0);
- strncpy(name, valPos+4, eqPos-(valPos+4));
- name[eqPos-(valPos+4)] = 0;
- if (!isalnum(name[eqPos-(valPos+4)-1]))
- name[eqPos-(valPos+4)-1] = 0;
-#ifdef DEBUG
- cerr << "Found standard: \"" << name << "\"\n";
-#endif
- if (ExcludeThm(name))
- out << l << '\n';
- else
- {
- char prefix[LIN_LEN];
- char arg[LIN_LEN];
-
- strncpy(prefix, l, valPos-l);
- prefix[valPos-l] = 0;
- strcpy(l+strlen(l)-1, ");"); // insert ")" before line's ';'
- out << prefix << "bind_thm (\"" << name << "\","
- << strchr(rPos, ' ') << '\n';
- }
- }
- else // output line unchanged
- out << l << '\n';
- in.getline(l, LIN_LEN);
- }
- in.close();
- out.close();
-#ifdef DEBUG
- cerr << "Done\n";
-#endif
-}
--- a/src/Tools/qed.doc Mon Sep 29 15:11:27 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
- Documentation for qed
-
-qed is a utility that's able to (almost) automatically insert calls to
-Isabelle's functions qed, qed_goal, qed_goalw and bind_thm into ML
-files. It does this by looking for certain patterns and changing the
-line so that the theorems are added to Isabelle's theorem database.
-The intent of including it into the distribution is to enable you to
-convert existing theory files.
-
-
-Compilation
------------
-
-qed was written in C++ and compiled using g++ 2.5.8. Executing "make qed"
-should create the executable.
-
-
-Usage
------
-
-To start qed type:
-
-qed <infile> <outfile>
-
-<infile> is the ML file you want to convert and <outfile> is the file
-to which the output should be sent. If you want to convert a whole
-directory of ML files and keep the original files as <name>.bak you
-can use the script 'runqed'.
-
-During its execution qed will output the names of all theorems that it has
-found.
-
-
-Recognized Theorems
--------------------
-
-Because qed knows nothing about ML's syntax it has to rely on certain
-assumptions about how typical definitions of theorems look. These
-assumptions were made based on the files contained in the distribution
-and therefore it's possible that they do not fit for the files you
-want to convert. So if qed does not do what you expect it to do have a
-look at the following list.
-
-
-- val mono_Int = result();
- -> qed "mono_Int";
-
- This kind of line is recognized if it contains "val ", "=" and the word
- "result();" and if the distance between "=" and "result()" is less
- than 5 characters.
-
-
-- val XHlemma2 = result() RS mp;
- -> bind_thm("XHlemma2", result() RS mp);
-
- If the first case cannot be applied because the "=" and "result()" are too
- far apart or "result()" is not followed by a ";" this one is
- used.
-
-
-- val sym = prove_goal HOL.thy "s=t ==> t=s"
- -> qed_goal "sym" HOL.thy "s=t ==> t=s"
-
- Lines containing the word "prove_goal" or "prove_goalw" and the strings
- "val " and "=" with a distance between "prove_goal" and "=" of less
- than 5 characters are matched by this case. Note that the ML command
- continues in the next line but is not changed further.
-
-
-- val ssubst = standard (sym RS subst);
- -> bind_thm ("ssubst", (sym RS subst));
-
- A line in which the word "standard" and the strings "val " and "=" can be
- found (with the usual distance limitation) and which ends with ";" is
- converted this way.
-
-
-At least for the standard theories these rules only match the desired
-kind of lines. It is possible though that not all places for insertion
-of the theorem database functions are found. Also qed has no way to
-recognize ML commands such as "local ... in ... end" or "let ... in
-... end". Processing files where theorems are defined inside these
-commands leads to syntax errors during compilation of the generated
-files like e.g. "end expected but bind_thm was found". One can avoid
-this by changing the affected lines to "val _ = bind_thm ..." after the
-conversion or by manually editing the original file.
-
-
-Problems?
---------
-
-If qed does not do what you want it to do you could change the
-sourcecode (qed.cc) yourself which should be fairly easy. If qed does
-not handle a case that you regard as a 'typical' way of defining a
-theorem (i.e. one that occurs very often in your files) send an email
-containg some examples to clasohm@informatik.tu-muenchen.de.
-
--- a/src/Tools/runqed Mon Sep 29 15:11:27 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-#! /bin/csh
-# $Id$
-# Run qed on all ML files in the current directory
-foreach f (*ML)
-echo Expanding shorthands in $f. \ Backup file is $f:r.bak
-qed $f $f:r.MLL
-mv $f $f:r.bak
-mv $f:r.MLL $f
-end
-echo Finished.