# HG changeset patch
# User oheimb
# Date 981043399 -3600
# Node ID b2af88422983d30c96603c0a8ebffe1671e5e78b
# Parent  8eb472444705e4e30d019760de52ec29664794a3
further minor improvements

diff -r 8eb472444705 -r b2af88422983 lib/scripts/convert.pl
--- a/lib/scripts/convert.pl	Wed Jan 31 22:16:22 2001 +0100
+++ b/lib/scripts/convert.pl	Thu Feb 01 17:03:19 2001 +0100
@@ -71,6 +71,10 @@
   s/ALLGOALS \(simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm) $1/g;
 
   s/atac 1/assumption/g;
+  s/atac (\d+)/tactic \"assume_tac $1\"/g;
+  s/^mp_tac 1/erule (1) notE impE/g;
+  s/^mp_tac (\d+)/erule_tac [$1] notE impE, tactic \"assume_tac $1\"/g;
+
   s/hypsubst_tac 1/hypsubst/g;
   s/arith_tac 1/arith/g;
   s/strip_tac 1/intro strip/g;
@@ -80,65 +84,71 @@
   s/rotate_tac (\d+) (\d+)/rotate_tac [$2] $1/g;
   s/rotate_tac (~\d+) 1/rotate_tac -$1/g;
   s/rotate_tac (~\d+) (\d+)/rotate_tac [$2] -$1/g;
-  s/rename_tac *(\".*?\") *1/rename_tac $1/g;
-  s/rename_tac *(\".*?\") *(\d+)/rename_tac [$2] $1/g;
-  s/case_tac *(\".*?\") *1/case_tac $1/g;
-  s/case_tac *(\".*?\") *(\d+)/case_tac [$2] $1/g;
-  s/induct_tac *(\".*?\") *1/induct_tac $1/g;
-  s/induct_tac *(\".*?\") *(\d+)/induct_tac [$2] $1/g;
-  s/subgoal_tac *(\".*?\") *1/subgoal_tac $1/g;
-  s/subgoal_tac *(\".*?\") *(\d+)/subgoal_tac [$2] $1/g;
-  s/thin_tac *(\".*?\") *1/erule_tac V = $1 in thin_rl/g;
-  s/thin_tac *(\".*?\") *(\d+)/erule_tac [$2] V = $1 in thin_rl/g;
-
-  s/rewtac ([\w\'\.]+) 1/unfold $1/g;
-  s/stac ([\w\'\.]+) 1/subst $1/g;
-  s/rtac ([\w\'\.]+) 1/rule $1/g;
-  s/rtac ([\w\'\.]+) (\d+)/rule_tac [$2] $1/g;
-  s/res_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\.]+) 1/rule_tac $1 = $2 in $3/g;
-  s/dtac ([\w\'\.]+) 1/drule $1/g;
-  s/dtac ([\w\'\.]+) (\d+)/drule_tac [$2] $1/g;
-  s/dres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\.]+) 1/drule_tac $1 = $2 in $3/g;
-  s/datac ([\w\'\.]+) (\d+) 1/drule ($2) $1/g;
-  s/etac ([\w\'\.]+) 1/erule $1/g;
-  s/etac ([\w\'\.]+) (\d+)/erule_tac [$2] $1/g;
-  s/eres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\.]+) 1/erule_tac $1 = $2 in $3/g;
-  s/eatac ([\w\'\.]+) (\d+) 1/erule ($2) $1/g;
-  s/forward_tac \[([\w\'\.]+)\] 1/frule $1/g;
-  s/ftac ([\w\'\.]+) 1/frule $1/g;
-  s/ftac ([\w\'\.]+) (\d+)/frule_tac [$2] $1/g;
-  s/forw_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\.]+) 1/frule_tac $1 = $2 in $3/g;
-  s/fatac ([\w\'\.]+) (\d+) 1/frule ($2) $1/g;
-
+  s/rename_tac (\".*?\") 1/rename_tac $1/g;
+  s/rename_tac (\".*?\") (\d+)/rename_tac [$2] $1/g;
+  s/case_tac (\".*?\") 1/case_tac $1/g;
+  s/case_tac (\".*?\") (\d+)/case_tac [$2] $1/g;
+  s/induct_tac (\".*?\") 1/induct_tac $1/g;
+  s/induct_tac (\".*?\") (\d+)/induct_tac [$2] $1/g;
+  s/subgoal_tac (\".*?\") 1/subgoal_tac $1/g;
+  s/subgoal_tac (\".*?\") (\d+)/subgoal_tac [$2] $1/g;
+  s/thin_tac (\".*?\") *1/erule_tac V = $1 in thin_rl/g;
+  s/thin_tac (\".*?\") *(\d+)/erule_tac [$2] V = $1 in thin_rl/g;
 
   s/THEN /, /g;
   s/ORELSE/|/g;
-  s/fold_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"fold ".thmlist($1)/eg;
-  s/rewrite_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"unfold ".thmlist($1)/eg;
-  s/cut_facts_tac *(\[[\w\'\. ,]*\]|[\w\'\.]+) 1/"cut_tac ".thmlist($1)/eg;
-  s/resolve_tac *(\[[\w\'\. ,]*\]|[\w\'\.]+) 1/"rule ".thmlist($1)/eg;
-  s/EVERY *(\[[\w\'\. ,]*\]|[\w\'\.]+)/thmlist($1)/eg;
-
-  s/addIs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"intro: ".thmlist($1)/eg;
-  s/addSIs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"intro!: ".thmlist($1)/eg;
-  s/addEs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"elim: ".thmlist($1)/eg;
-  s/addSEs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"elim!: ".thmlist($1)/eg;
-  s/addDs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"dest: ".thmlist($1)/eg;
-  s/addSDs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"dest!: ".thmlist($1)/eg;
-  s/delrules *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"del: ".thmlist($1)/eg;
-  s/addsimps *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"$simpmodmod"."add: ".thmlist($1)/eg;
-  s/delsimps *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"$simpmodmod"."del: ".thmlist($1)/eg;
-  s/addcongs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"cong add: ".thmlist($1)/eg;
-  s/delcongs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"cong del: ".thmlist($1)/eg;
-  s/addsplits *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"split add: ".thmlist($1)/eg;
-  s/delsplits *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"split del: ".thmlist($1)/eg;
-
+  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
+  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
+  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
+  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
+  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3\]/g;
+  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3\]/g;
+  s/\(([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2\]/g;
   s/([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2\]/g;
 
-  s/ +/ /g;                  # remove multiple whitespace
+  s/rewtac ([\w\'\. \[,\]]+)/unfold $1/g;
+  s/stac ([\w\'\. \[,\]]+?) 1/subst $1/g;
+  s/rtac ([\w\'\. \[,\]]+?) 1/rule $1/g;
+  s/rtac ([\w\'\. \[,\]]+?) (\d+)/rule_tac [$2] $1/g;
+  s/res_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/rule_tac $1 = $2 in $3/g;
+  s/dtac ([\w\'\. \[,\]]+?) 1/drule $1/g;
+  s/dtac ([\w\'\. \[,\]]+?) (\d+)/drule_tac [$2] $1/g;
+  s/dres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/drule_tac $1 = $2 in $3/g;
+  s/datac ([\w\'\. \[,\]]+?) (\d+) 1/drule ($2) $1/g;
+  s/etac ([\w\'\. \[,\]]+?) 1/erule $1/g;
+  s/etac ([\w\'\. \[,\]]+?) (\d+)/erule_tac [$2] $1/g;
+  s/eres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/erule_tac $1 = $2 in $3/g;
+  s/eatac ([\w\'\. \[,\]]+?) (\d+) 1/erule ($2) $1/g;
+  s/forward_tac \[([\w\'\. \[,\]]+)\] 1/frule $1/g;
+  s/forward_tac \[([\w\'\. \[,\]]+)\] (\d+)/frule_tac [$2] $1/g;
+  s/ftac ([\w\'\. \[,\]]+?) 1/frule $1/g;
+  s/ftac ([\w\'\. \[,\]]+?) (\d+)/frule_tac [$2] $1/g;
+  s/forw_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/frule_tac $1 = $2 in $3/g;
+  s/fatac ([\w\'\. \[,\]]+?) (\d+) 1/frule ($2) $1/g;
+
+
+  s/fold_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"fold ".thmlist($1)/eg;
+  s/rewrite_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"unfold ".thmlist($1)/eg;
+  s/cut_facts_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+) 1/"cut_tac ".thmlist($1)/eg;
+  s/resolve_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+) 1/"rule ".thmlist($1)/eg;
+
+  s/addIs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"intro: ".thmlist($1)/eg;
+  s/addSIs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"intro!: ".thmlist($1)/eg;
+  s/addEs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"elim: ".thmlist($1)/eg;
+  s/addSEs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"elim!: ".thmlist($1)/eg;
+  s/addDs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"dest: ".thmlist($1)/eg;
+  s/addSDs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"dest!: ".thmlist($1)/eg;
+  s/delrules *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"del: ".thmlist($1)/eg;
+  s/addsimps *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"$simpmodmod"."add: ".thmlist($1)/eg;
+  s/delsimps *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"$simpmodmod"."del: ".thmlist($1)/eg;
+  s/addcongs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"cong add: ".thmlist($1)/eg;
+  s/delcongs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"cong del: ".thmlist($1)/eg;
+  s/addsplits *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"split add: ".thmlist($1)/eg;
+  s/delsplits *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"split del: ".thmlist($1)/eg;
+
+  s/ +/ /g;                       # remove multiple whitespace
   s/\( /\(/; s/ \)/\)/g;  # remove leading and trailing space inside parentheses
-  s/^ *(.*?) *$/$1/s;        # remove enclosing whitespace
-  s/^\( *([\w\'\.]+) *\)$/$1/; # remove outermost parentheses if around atoms
+  s/^ *(.*?) *$/$1/s;             # remove enclosing whitespace
   s/^([a-zA-Z])/ $1/ if (!($lead =~ m/[\s\(]$/)); # add space if required
   $_;
 }
@@ -167,6 +177,7 @@
   "done";
 }
 
+$currfile = "";
 $next = "nonempty";
 while (<>) { # main loop
   if ($ARGV ne $currfile) {
@@ -200,25 +211,27 @@
     goto nlc;
   }
   $_=$line;
-  s/^Goalw *(\[[\w\'\.\s,]*\]|[\w\'\.]+) *(.+)/
+  s/^Goalw *(\[[\w\'\.\s,]*\]|[\w\'\. \[,\]]+) *(.+)/
     "lemma ".thmname().": $2$head"."apply (unfold ".thmlist($1).")"/se;
   s/^Goal *(.+)/"lemma ".thmname().": $1"/se;
   s/ goal/"(*".thmname()."*) goal"/se; # ugly old-style goals
   s/^qed_spec_mp *\"(.*?)\"/done($1," [rule_format (no_asm)]")/se;
   s/^qed *\"(.*?)\"/done($1,"")/se;
   s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
-  s/^by(\s*\(?\s*)(.*?)$/"apply$1".process_tac($1,$2)/se;
-  s/^Addsimps\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [simp]"/seg;
-  s/^Delsimps\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [simp del]"/seg;
-  s/^Addsplits\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [split]"/seg;
-  s/^Delsplits\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [split del]"/seg;
-  s/^AddIs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [intro]"/seg;
-  s/^AddSIs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [intro!]"/seg;
-  s/^AddEs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [elim]"/seg;
-  s/^AddSEs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [elim!]"/seg;
-  s/^AddDs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [dest]"/seg;
-  s/^AddSDs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [dest!]"/seg;
-  s/^AddIffs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [iff]"/seg;
+  s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/"apply$1".process_tac($1,$2).$3/se;
+  s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
+                             # remove outermost parentheses if around atoms
+  s/^Addsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [simp]"/seg;
+  s/^Delsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [simp del]"/seg;
+  s/^Addsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [split]"/seg;
+  s/^Delsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [split del]"/seg;
+  s/^AddIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [intro]"/seg;
+  s/^AddSIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [intro!]"/seg;
+  s/^AddEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [elim]"/seg;
+  s/^AddSEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [elim!]"/seg;
+  s/^AddDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [dest]"/seg;
+  s/^AddSDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [dest!]"/seg;
+  s/^AddIffs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [iff]"/seg;
   print "$_$tail";
   if(!$next) { last; } # prevents reading finally from stdin (thru <>)!
 }