--- 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 <>)!
}