further minor improvements
authoroheimb
Thu Feb 01 17:03:19 2001 +0100 (2001-02-01)
changeset 11013b2af88422983
parent 11012 8eb472444705
child 11014 c205ede3140d
further minor improvements
lib/scripts/convert.pl
     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  }