1.1 --- a/lib/scripts/convert.pl Wed Jan 31 22:16:22 2001 +0100
1.2 +++ b/lib/scripts/convert.pl Thu Feb 01 17:03:19 2001 +0100
1.3 @@ -71,6 +71,10 @@
1.4 s/ALLGOALS \(simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm) $1/g;
1.5
1.6 s/atac 1/assumption/g;
1.7 + s/atac (\d+)/tactic \"assume_tac $1\"/g;
1.8 + s/^mp_tac 1/erule (1) notE impE/g;
1.9 + s/^mp_tac (\d+)/erule_tac [$1] notE impE, tactic \"assume_tac $1\"/g;
1.10 +
1.11 s/hypsubst_tac 1/hypsubst/g;
1.12 s/arith_tac 1/arith/g;
1.13 s/strip_tac 1/intro strip/g;
1.14 @@ -80,65 +84,71 @@
1.15 s/rotate_tac (\d+) (\d+)/rotate_tac [$2] $1/g;
1.16 s/rotate_tac (~\d+) 1/rotate_tac -$1/g;
1.17 s/rotate_tac (~\d+) (\d+)/rotate_tac [$2] -$1/g;
1.18 - s/rename_tac *(\".*?\") *1/rename_tac $1/g;
1.19 - s/rename_tac *(\".*?\") *(\d+)/rename_tac [$2] $1/g;
1.20 - s/case_tac *(\".*?\") *1/case_tac $1/g;
1.21 - s/case_tac *(\".*?\") *(\d+)/case_tac [$2] $1/g;
1.22 - s/induct_tac *(\".*?\") *1/induct_tac $1/g;
1.23 - s/induct_tac *(\".*?\") *(\d+)/induct_tac [$2] $1/g;
1.24 - s/subgoal_tac *(\".*?\") *1/subgoal_tac $1/g;
1.25 - s/subgoal_tac *(\".*?\") *(\d+)/subgoal_tac [$2] $1/g;
1.26 - s/thin_tac *(\".*?\") *1/erule_tac V = $1 in thin_rl/g;
1.27 - s/thin_tac *(\".*?\") *(\d+)/erule_tac [$2] V = $1 in thin_rl/g;
1.28 -
1.29 - s/rewtac ([\w\'\.]+) 1/unfold $1/g;
1.30 - s/stac ([\w\'\.]+) 1/subst $1/g;
1.31 - s/rtac ([\w\'\.]+) 1/rule $1/g;
1.32 - s/rtac ([\w\'\.]+) (\d+)/rule_tac [$2] $1/g;
1.33 - s/res_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\.]+) 1/rule_tac $1 = $2 in $3/g;
1.34 - s/dtac ([\w\'\.]+) 1/drule $1/g;
1.35 - s/dtac ([\w\'\.]+) (\d+)/drule_tac [$2] $1/g;
1.36 - s/dres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\.]+) 1/drule_tac $1 = $2 in $3/g;
1.37 - s/datac ([\w\'\.]+) (\d+) 1/drule ($2) $1/g;
1.38 - s/etac ([\w\'\.]+) 1/erule $1/g;
1.39 - s/etac ([\w\'\.]+) (\d+)/erule_tac [$2] $1/g;
1.40 - s/eres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\.]+) 1/erule_tac $1 = $2 in $3/g;
1.41 - s/eatac ([\w\'\.]+) (\d+) 1/erule ($2) $1/g;
1.42 - s/forward_tac \[([\w\'\.]+)\] 1/frule $1/g;
1.43 - s/ftac ([\w\'\.]+) 1/frule $1/g;
1.44 - s/ftac ([\w\'\.]+) (\d+)/frule_tac [$2] $1/g;
1.45 - s/forw_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\.]+) 1/frule_tac $1 = $2 in $3/g;
1.46 - s/fatac ([\w\'\.]+) (\d+) 1/frule ($2) $1/g;
1.47 -
1.48 + s/rename_tac (\".*?\") 1/rename_tac $1/g;
1.49 + s/rename_tac (\".*?\") (\d+)/rename_tac [$2] $1/g;
1.50 + s/case_tac (\".*?\") 1/case_tac $1/g;
1.51 + s/case_tac (\".*?\") (\d+)/case_tac [$2] $1/g;
1.52 + s/induct_tac (\".*?\") 1/induct_tac $1/g;
1.53 + s/induct_tac (\".*?\") (\d+)/induct_tac [$2] $1/g;
1.54 + s/subgoal_tac (\".*?\") 1/subgoal_tac $1/g;
1.55 + s/subgoal_tac (\".*?\") (\d+)/subgoal_tac [$2] $1/g;
1.56 + s/thin_tac (\".*?\") *1/erule_tac V = $1 in thin_rl/g;
1.57 + s/thin_tac (\".*?\") *(\d+)/erule_tac [$2] V = $1 in thin_rl/g;
1.58
1.59 s/THEN /, /g;
1.60 s/ORELSE/|/g;
1.61 - s/fold_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"fold ".thmlist($1)/eg;
1.62 - s/rewrite_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"unfold ".thmlist($1)/eg;
1.63 - s/cut_facts_tac *(\[[\w\'\. ,]*\]|[\w\'\.]+) 1/"cut_tac ".thmlist($1)/eg;
1.64 - s/resolve_tac *(\[[\w\'\. ,]*\]|[\w\'\.]+) 1/"rule ".thmlist($1)/eg;
1.65 - s/EVERY *(\[[\w\'\. ,]*\]|[\w\'\.]+)/thmlist($1)/eg;
1.66 -
1.67 - s/addIs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"intro: ".thmlist($1)/eg;
1.68 - s/addSIs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"intro!: ".thmlist($1)/eg;
1.69 - s/addEs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"elim: ".thmlist($1)/eg;
1.70 - s/addSEs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"elim!: ".thmlist($1)/eg;
1.71 - s/addDs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"dest: ".thmlist($1)/eg;
1.72 - s/addSDs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"dest!: ".thmlist($1)/eg;
1.73 - s/delrules *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"del: ".thmlist($1)/eg;
1.74 - s/addsimps *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"$simpmodmod"."add: ".thmlist($1)/eg;
1.75 - s/delsimps *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"$simpmodmod"."del: ".thmlist($1)/eg;
1.76 - s/addcongs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"cong add: ".thmlist($1)/eg;
1.77 - s/delcongs *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"cong del: ".thmlist($1)/eg;
1.78 - s/addsplits *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"split add: ".thmlist($1)/eg;
1.79 - s/delsplits *(\[[\w\'\. ,]*\]|[\w\'\.]+)/"split del: ".thmlist($1)/eg;
1.80 -
1.81 + s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
1.82 + s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
1.83 + s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
1.84 + s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
1.85 + s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3\]/g;
1.86 + s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3\]/g;
1.87 + s/\(([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2\]/g;
1.88 s/([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2\]/g;
1.89
1.90 - s/ +/ /g; # remove multiple whitespace
1.91 + s/rewtac ([\w\'\. \[,\]]+)/unfold $1/g;
1.92 + s/stac ([\w\'\. \[,\]]+?) 1/subst $1/g;
1.93 + s/rtac ([\w\'\. \[,\]]+?) 1/rule $1/g;
1.94 + s/rtac ([\w\'\. \[,\]]+?) (\d+)/rule_tac [$2] $1/g;
1.95 + s/res_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/rule_tac $1 = $2 in $3/g;
1.96 + s/dtac ([\w\'\. \[,\]]+?) 1/drule $1/g;
1.97 + s/dtac ([\w\'\. \[,\]]+?) (\d+)/drule_tac [$2] $1/g;
1.98 + s/dres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/drule_tac $1 = $2 in $3/g;
1.99 + s/datac ([\w\'\. \[,\]]+?) (\d+) 1/drule ($2) $1/g;
1.100 + s/etac ([\w\'\. \[,\]]+?) 1/erule $1/g;
1.101 + s/etac ([\w\'\. \[,\]]+?) (\d+)/erule_tac [$2] $1/g;
1.102 + s/eres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/erule_tac $1 = $2 in $3/g;
1.103 + s/eatac ([\w\'\. \[,\]]+?) (\d+) 1/erule ($2) $1/g;
1.104 + s/forward_tac \[([\w\'\. \[,\]]+)\] 1/frule $1/g;
1.105 + s/forward_tac \[([\w\'\. \[,\]]+)\] (\d+)/frule_tac [$2] $1/g;
1.106 + s/ftac ([\w\'\. \[,\]]+?) 1/frule $1/g;
1.107 + s/ftac ([\w\'\. \[,\]]+?) (\d+)/frule_tac [$2] $1/g;
1.108 + s/forw_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/frule_tac $1 = $2 in $3/g;
1.109 + s/fatac ([\w\'\. \[,\]]+?) (\d+) 1/frule ($2) $1/g;
1.110 +
1.111 +
1.112 + s/fold_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"fold ".thmlist($1)/eg;
1.113 + s/rewrite_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"unfold ".thmlist($1)/eg;
1.114 + s/cut_facts_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+) 1/"cut_tac ".thmlist($1)/eg;
1.115 + s/resolve_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+) 1/"rule ".thmlist($1)/eg;
1.116 +
1.117 + s/addIs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"intro: ".thmlist($1)/eg;
1.118 + s/addSIs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"intro!: ".thmlist($1)/eg;
1.119 + s/addEs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"elim: ".thmlist($1)/eg;
1.120 + s/addSEs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"elim!: ".thmlist($1)/eg;
1.121 + s/addDs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"dest: ".thmlist($1)/eg;
1.122 + s/addSDs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"dest!: ".thmlist($1)/eg;
1.123 + s/delrules *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"del: ".thmlist($1)/eg;
1.124 + s/addsimps *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"$simpmodmod"."add: ".thmlist($1)/eg;
1.125 + s/delsimps *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"$simpmodmod"."del: ".thmlist($1)/eg;
1.126 + s/addcongs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"cong add: ".thmlist($1)/eg;
1.127 + s/delcongs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"cong del: ".thmlist($1)/eg;
1.128 + s/addsplits *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"split add: ".thmlist($1)/eg;
1.129 + s/delsplits *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"split del: ".thmlist($1)/eg;
1.130 +
1.131 + s/ +/ /g; # remove multiple whitespace
1.132 s/\( /\(/; s/ \)/\)/g; # remove leading and trailing space inside parentheses
1.133 - s/^ *(.*?) *$/$1/s; # remove enclosing whitespace
1.134 - s/^\( *([\w\'\.]+) *\)$/$1/; # remove outermost parentheses if around atoms
1.135 + s/^ *(.*?) *$/$1/s; # remove enclosing whitespace
1.136 s/^([a-zA-Z])/ $1/ if (!($lead =~ m/[\s\(]$/)); # add space if required
1.137 $_;
1.138 }
1.139 @@ -167,6 +177,7 @@
1.140 "done";
1.141 }
1.142
1.143 +$currfile = "";
1.144 $next = "nonempty";
1.145 while (<>) { # main loop
1.146 if ($ARGV ne $currfile) {
1.147 @@ -200,25 +211,27 @@
1.148 goto nlc;
1.149 }
1.150 $_=$line;
1.151 - s/^Goalw *(\[[\w\'\.\s,]*\]|[\w\'\.]+) *(.+)/
1.152 + s/^Goalw *(\[[\w\'\.\s,]*\]|[\w\'\. \[,\]]+) *(.+)/
1.153 "lemma ".thmname().": $2$head"."apply (unfold ".thmlist($1).")"/se;
1.154 s/^Goal *(.+)/"lemma ".thmname().": $1"/se;
1.155 s/ goal/"(*".thmname()."*) goal"/se; # ugly old-style goals
1.156 s/^qed_spec_mp *\"(.*?)\"/done($1," [rule_format (no_asm)]")/se;
1.157 s/^qed *\"(.*?)\"/done($1,"")/se;
1.158 s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
1.159 - s/^by(\s*\(?\s*)(.*?)$/"apply$1".process_tac($1,$2)/se;
1.160 - s/^Addsimps\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [simp]"/seg;
1.161 - s/^Delsimps\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [simp del]"/seg;
1.162 - s/^Addsplits\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [split]"/seg;
1.163 - s/^Delsplits\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [split del]"/seg;
1.164 - s/^AddIs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [intro]"/seg;
1.165 - s/^AddSIs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [intro!]"/seg;
1.166 - s/^AddEs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [elim]"/seg;
1.167 - s/^AddSEs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [elim!]"/seg;
1.168 - s/^AddDs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [dest]"/seg;
1.169 - s/^AddSDs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [dest!]"/seg;
1.170 - s/^AddIffs\s*\[\s*([\w\'\. ,]*)\s*\]/"declare ".thmlist($1)." [iff]"/seg;
1.171 + s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/"apply$1".process_tac($1,$2).$3/se;
1.172 + s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
1.173 + # remove outermost parentheses if around atoms
1.174 + s/^Addsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [simp]"/seg;
1.175 + s/^Delsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [simp del]"/seg;
1.176 + s/^Addsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [split]"/seg;
1.177 + s/^Delsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [split del]"/seg;
1.178 + s/^AddIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [intro]"/seg;
1.179 + s/^AddSIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [intro!]"/seg;
1.180 + s/^AddEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [elim]"/seg;
1.181 + s/^AddSEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [elim!]"/seg;
1.182 + s/^AddDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [dest]"/seg;
1.183 + s/^AddSDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [dest!]"/seg;
1.184 + s/^AddIffs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [iff]"/seg;
1.185 print "$_$tail";
1.186 if(!$next) { last; } # prevents reading finally from stdin (thru <>)!
1.187 }