# HG changeset patch
# User clasohm
# Date 787926244 -3600
# Node ID 4a266c3d4cc0f4f3af74dd1cdfadd358bc617499
# Parent  bf4b7c37db2ce2f30278ff6783111dff4617e2c2
qed is a utility that makes ML files store the defined theories in Isabelle's
theorem database

diff -r bf4b7c37db2c -r 4a266c3d4cc0 src/Tools/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Makefile	Tue Dec 20 13:24:04 1994 +0100
@@ -0,0 +1,13 @@
+OPTIONS= -DDEBUG
+CC = g++ $(OPTIONS)
+OBJS = qed.o
+
+.SUFFIXES: .cc .o
+
+.cc.o:
+	$(CC) -c $<
+
+qed:	$(OBJS)
+	g++ -o qed $(OBJS)
+
+qed.o: qed.cc
diff -r bf4b7c37db2c -r 4a266c3d4cc0 src/Tools/qed.cc
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/qed.cc	Tue Dec 20 13:24:04 1994 +0100
@@ -0,0 +1,138 @@
+// Little utility to convert result() -> qed ... in Isabelle's files
+// Written in 1994 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>
+
+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()")) && (!isalpha(*(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 (!isalpha(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 ((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")) 
+		 && (!isalpha(*(rPos-1))) 
+		 && (!isalpha(*(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 (!isalpha(name[eqPos-(valPos+4)-1]))
+	        name[eqPos-(valPos+4)-1] = 0;
+#ifdef DEBUG
+	    cerr << "Found prove_goal: \"" << name << "\"\n";
+#endif
+	    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"))
+		 && (!isalpha(*(rPos-1))) 
+		 && (!isalpha(*(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 (!isalpha(name[eqPos-(valPos+4)-1]))
+	        name[eqPos-(valPos+4)-1] = 0;
+#ifdef DEBUG
+	    cerr << "Found standard: \"" << name << "\"\n";
+#endif
+	    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
+}
diff -r bf4b7c37db2c -r 4a266c3d4cc0 src/Tools/qed.doc
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/qed.doc	Tue Dec 20 13:24:04 1994 +0100
@@ -0,0 +1,97 @@
+			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.
+
diff -r bf4b7c37db2c -r 4a266c3d4cc0 src/Tools/runqed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/runqed	Tue Dec 20 13:24:04 1994 +0100
@@ -0,0 +1,5 @@
+foreach n (*ML)
+qed $n $n:r.MLL
+mv $n $n:r.bak
+mv $n:r.MLL $n
+end