author  wenzelm 
Mon, 20 Nov 2006 23:47:10 +0100  
changeset 21426  87ac12bed1ab 
parent 14981  e73f8140af78 
permissions  rwrr 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

1 
# 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

2 
# $Id$ 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

3 
# Author: David von Oheimb, TU Muenchen 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

4 
# 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

5 
# convert.pl  convert legacy tactic scripts to Isabelle/Isar tactic 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

6 
# emulation using heuristics  leaves unrecognized patterns unchanged 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

7 
# produces from each input file (on the command line) a new file with 
10972  8 
# ".thy" appended and renames the original input file by appending "~0~" 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

9 

fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

10 
sub thmlist { 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

11 
my $s = shift; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

12 
$s =~ s/^\[(.*)\]$/$1/sg; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

13 
$s =~ s/, +/ /g; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

14 
$s =~ s/,/ /g; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

15 
$s; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

16 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

17 

11014  18 
sub subst_RS { 
11131  19 
s/ RS ([\w\'\.]+)/ [THEN $1]/g; 
20 
s/ RS \((.+?)\)/ [THEN $1]/g; 

11271  21 
s/\(([\w\'\.]+ \[THEN [\w\'\.]+\])\)/$1/g; 
11274  22 
s/\] \[THEN /, THEN /g; 
11131  23 
s/THEN sym\b/symmetric/g; 
11014  24 
} 
25 

11131  26 
sub subst_RS_standard { 
11027  27 
my $s = shift; 
28 
$_ = $s; 

11131  29 
s/\s+/ /sg; # remove multiple whitespace 
30 
s/\s/ /sg; # substitute all remaining tabs and newlines by space 

11027  31 
subst_RS(); 
11131  32 
s/\]\s*$/, standard]/g; 
11027  33 
$_; 
34 
} 

35 

11014  36 
sub decl { 
37 
my $s = shift; 

38 
my $a = shift; 

39 
$_ = $s; 

40 
subst_RS(); 

41 
s/, */ [$a] /g; 

42 
s/$/ [$a]/; 

43 
s/\] *\[/, /g; 

44 
"declare $_"; 

45 
} 

46 

10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

47 
sub process_tac { 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

48 
$prefer = ""; 
10972  49 
my $lead = shift; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

50 
my $t = shift; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

51 
my $simpmodmod = ($t =~ m/auto_tacforce_tacclarsimp_tac/) ? "simp " : ""; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

52 

fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

53 
$_ = $t; 
10972  54 
s/\s+/ /sg; # remove multiple whitespace 
55 
s/\s/ /sg; # substitute all remaining tabs and newlines by space 

56 
s/\( /\(/g; s/ \)/\)/g; # remove leading and trailing space inside parentheses 

57 
s/\[ /\[/g; s/ \]/\]/g; # remove leading and trailing space inside sq brackets 

58 
s/ ?\( ?\)/\(\)/g; # remove space before and inside empty tuples 

11329
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

59 
s/([^ ])\(/$1 \(/g; # possibly add space before opening parentheses 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

60 
s/\)([^ ])/\) $1/g; # possibly add space after closing parentheses 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

61 

11273
673783831234
improve support for EVERY', added support for EVERY
oheimb
parents:
11272
diff
changeset

62 
s/EVERY *\[(.*?)\]/$1/; 
11283  63 
if(s/EVERY\' ?\[(.*?)\] *(\d+)/$1 $2/) { 
11271  64 
$goal = $2; 
65 
s/,/ $goal,/g; 

66 
} 

10972  67 
s/Blast_tac 1/blast/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

68 
s/^Blast_tac (\d+)/{$prefer="prefer $1 "; "blast"}/e; 
10972  69 
s/Fast_tac 1/fast/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

70 
s/^Fast_tac (\d+)/{$prefer="prefer $1 "; "fast"}/e; 
10972  71 
s/Slow_tac 1/slow/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

72 
s/^Slow_tac (\d+)/{$prefer="prefer $1 "; "slow"}/e; 
10972  73 
s/Best_tac 1/best/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

74 
s/^Best_tac (\d+)/{$prefer="prefer $1 "; "best"}/e; 
10972  75 
s/Safe_tac/safe/g; 
76 
s/Clarify_tac 1/clarify/g; 

77 

13076
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

78 
s/ALLGOALS \(blast_tac \(claset \(\) (.*?)\) \)$/(blast $1)+/g; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

79 
s/blast_tac \(claset \(\) (.*?)\) 1/blast $1/g; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

80 
s/^blast_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "blast $1"}/e; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

81 
s/ALLGOALS \(fast_tac \(claset \(\) (.*?)\) \)$/(fast $1)+/g; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

82 
s/fast_tac \(claset \(\) (.*?)\) 1/fast $1/g; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

83 
s/^fast_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "fast $1"}/e; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

84 
s/slow_tac \(claset \(\) (.*?)\) 1/slow $1/g; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

85 
s/^slow_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "slow $1"}/e; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

86 
s/ALLGOALS \(best_tac \(claset \(\) (.*?)\) \)$/(best $1)+/g; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

87 
s/best_tac \(claset \(\) (.*?)\) 1/best $1/g; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

88 
s/^best_tac \(claset \(\) (.*?)\) (\d+)/{$prefer="prefer $2 "; "best $1"}/e; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

89 
s/safe_tac \(claset \(\) (.*?)\)/safe $1/g; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

90 
s/clarify_tac \(claset \(\) (.*?)\) 1/clarify $1/g; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

91 

fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

92 
s/Auto_tac/auto/g; 
13076
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

93 
s/ALLGOALS Force_tac/force+/g; 
10972  94 
s/Force_tac 1/force/g; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

95 
s/^Force_tac (\d+)/{$prefer="prefer $1 "; "force"}/e; 
10972  96 
s/Clarsimp_tac 1/clarsimp/g; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

97 

11329
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

98 
s/auto_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\)/auto $1 $2/g; 
13076
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

99 
s/ALLGOALS \(force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) \)$/(force $1 $2)+/g; 
11329
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

100 
s/force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) 1/force $1 $2/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

101 
s/^force_tac \(claset \(\) (.*?), *simpset \(\) (.*?)\) (\d+)/{$prefer="prefer $3 "; "force $1 $2"}/e; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

102 
s/clarsimp_tac \(claset \(*\) (.*?), *simpset \(\) (.*?)\) 1/clarsimp $1 $2/g; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

103 

10972  104 
s/Asm_full_simp_tac 1/simp/g; 
105 
s/Full_simp_tac 1/simp (no_asm_use)/g; 

106 
s/Asm_simp_tac 1/simp (no_asm_simp)/g; 

107 
s/Simp_tac 1/simp (no_asm)/g; 

108 
s/ALLGOALS Asm_full_simp_tac/simp_all/g; 

11029  109 
s/ALLGOALS Full_simp_tac/simp_all (no_asm_use)/g; 
110 
s/ALLGOALS Asm_simp_tac/simp_all (no_asm_simp)/g; 

10972  111 
s/ALLGOALS Simp_tac/simp_all (no_asm)/g; 
112 

11329
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

113 
s/asm_full_simp_tac \(simpset \(\) (.*?)\) 1/simp $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

114 
s/full_simp_tac \(simpset \(\) (.*?)\) 1/simp (no_asm_use) $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

115 
s/asm_simp_tac \(simpset \(\) (.*?)\) 1/simp (no_asm_simp) $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

116 
s/simp_tac \(simpset \(\) (.*?)\) 1/simp (no_asm) $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

117 
s/ALLGOALS \(asm_full_simp_tac \(simpset \(\) (.*?)\) \)/simp_all $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

118 
s/ALLGOALS \(full_simp_tac \(simpset \(\) (.*?)\) \)/simp_all (no_asm_use) $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

119 
s/ALLGOALS \(asm_simp_tac \(simpset \(\) (.*?)\) \)/simp_all (no_asm_simp) $1/g; 
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

120 
s/ALLGOALS \(simp_tac \(simpset \(\) (.*?)\) \)/simp_all (no_asm) $1/g; 
10972  121 

11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

122 
s/a(ssume_)?tac 1/assumption/g; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

123 
s/^a(ssume_)?tac (\d+)/{$prefer="prefer $2 "; "assumption"}/e; 
11068  124 
s/\bmp_tac 1/erule (1) notE impE/g; 
125 
s/\bmp_tac (\d+)/erule_tac [$1] notE impE, tactic \"assume_tac $1\"/g; 

11013  126 

10972  127 
s/hypsubst_tac 1/hypsubst/g; 
128 
s/arith_tac 1/arith/g; 

129 
s/strip_tac 1/intro strip/g; 

130 
s/split_all_tac 1/simp (no_asm_simp) only: split_tupled_all/g; 

10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

131 

11263
e502756bcb11
added parentheses for 'b y' syntax, added primitive smp_tac support
oheimb
parents:
11198
diff
changeset

132 
s/smp_tac (\d+) (\d+)/tactic "smp_tac $1 $2"/g; 
11009  133 
s/rotate_tac (\d+) (\d+)/rotate_tac [$2] $1/g; 
11068  134 
s/rotate_tac ~ *(\d+) (\d+)/rotate_tac [$2] $1/g; 
11013  135 
s/rename_tac (\".*?\") (\d+)/rename_tac [$2] $1/g; 
136 
s/case_tac (\".*?\") (\d+)/case_tac [$2] $1/g; 

137 
s/induct_tac (\".*?\") (\d+)/induct_tac [$2] $1/g; 

11029  138 
s/induct_thm_tac ([\w\'\. \[,\]]+?) (\".*?\") (\d+)/induct_tac [$3] $2 rule: $1/g; 
11013  139 
s/subgoal_tac (\".*?\") (\d+)/subgoal_tac [$2] $1/g; 
140 
s/thin_tac (\".*?\") *(\d+)/erule_tac [$2] V = $1 in thin_rl/g; 

10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

141 

10972  142 
s/THEN /, /g; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

143 
s/ORELSE//g; 
11014  144 
subst_RS(); 
10972  145 

11329
ad8061b2da6c
improved handling of space before/after parentheses
oheimb
parents:
11286
diff
changeset

146 
s/\(\"(.*?)\" *, *(\".*?\")\) , */$1 = $2 and /g; # instantiations 
11068  147 
s/\(\"(.*?)\" *, *(\".*?\")\)/$1 = $2/g; # last instantiation 
148 

11013  149 
s/rewtac ([\w\'\. \[,\]]+)/unfold $1/g; 
150 
s/stac ([\w\'\. \[,\]]+?) 1/subst $1/g; 

151 
s/rtac ([\w\'\. \[,\]]+?) 1/rule $1/g; 

152 
s/rtac ([\w\'\. \[,\]]+?) (\d+)/rule_tac [$2] $1/g; 

11068  153 
s/res_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/rule_tac [$3] $1 in $2/g; 
11013  154 
s/dtac ([\w\'\. \[,\]]+?) 1/drule $1/g; 
155 
s/dtac ([\w\'\. \[,\]]+?) (\d+)/drule_tac [$2] $1/g; 

11068  156 
s/dres_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/drule_tac [$3] $1 in $2/g; 
11013  157 
s/datac ([\w\'\. \[,\]]+?) (\d+) 1/drule ($2) $1/g; 
158 
s/etac ([\w\'\. \[,\]]+?) 1/erule $1/g; 

159 
s/etac ([\w\'\. \[,\]]+?) (\d+)/erule_tac [$2] $1/g; 

11068  160 
s/eres_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/erule_tac [$3] $1 in $2/g; 
11013  161 
s/eatac ([\w\'\. \[,\]]+?) (\d+) 1/erule ($2) $1/g; 
162 
s/forward_tac \[([\w\'\. \[,\]]+)\] 1/frule $1/g; 

163 
s/forward_tac \[([\w\'\. \[,\]]+)\] (\d+)/frule_tac [$2] $1/g; 

164 
s/ftac ([\w\'\. \[,\]]+?) 1/frule $1/g; 

165 
s/ftac ([\w\'\. \[,\]]+?) (\d+)/frule_tac [$2] $1/g; 

11068  166 
s/forw_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/frule_tac [$3] $1 in $2/g; 
11013  167 
s/fatac ([\w\'\. \[,\]]+?) (\d+) 1/frule ($2) $1/g; 
168 

169 

170 
s/fold_goals_tac *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"fold ".thmlist($1)/eg; 

171 
s/rewrite_goals_tac *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"unfold ".thmlist($1)/eg; 

11068  172 
s/cut_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/cut_tac [$3] $1 in $2/g; 
173 
s/cut_facts_tac *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+) (\d+)/"cut_tac [$2] ".thmlist($1)/eg; 

11013  174 
s/resolve_tac *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+) 1/"rule ".thmlist($1)/eg; 
175 

176 
s/addIs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"intro: ".thmlist($1)/eg; 

177 
s/addSIs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"intro!: ".thmlist($1)/eg; 

178 
s/addEs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"elim: ".thmlist($1)/eg; 

179 
s/addSEs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"elim!: ".thmlist($1)/eg; 

180 
s/addDs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"dest: ".thmlist($1)/eg; 

181 
s/addSDs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"dest!: ".thmlist($1)/eg; 

182 
s/delrules *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"del: ".thmlist($1)/eg; 

183 
s/addsimps *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"$simpmodmod"."add: ".thmlist($1)/eg; 

184 
s/delsimps *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"$simpmodmod"."del: ".thmlist($1)/eg; 

185 
s/addcongs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"cong add: ".thmlist($1)/eg; 

186 
s/delcongs *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"cong del: ".thmlist($1)/eg; 

187 
s/addsplits *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"split add: ".thmlist($1)/eg; 

188 
s/delsplits *(\[[\w\'\. ,]*\][\w\'\. \[,\]]+)/"split del: ".thmlist($1)/eg; 

189 

11068  190 
s/_tac \[1\]/_tac/g; 
11013  191 
s/ +/ /g; # remove multiple whitespace 
10972  192 
s/\( /\(/; s/ \)/\)/g; # remove leading and trailing space inside parentheses 
11013  193 
s/^ *(.*?) *$/$1/s; # remove enclosing whitespace 
10972  194 
s/^([azAZ])/ $1/ if (!($lead =~ m/[\s\(]$/)); # add space if required 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

195 
$prefer."apply".$lead.$_; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

196 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

197 

11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

198 
sub lemmaname { 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

199 
$lemmanames[++$lemmacount] = "??unknown??"; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

200 
"@@" . $lemmacount . "@@"; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

201 
} 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

202 

11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

203 
sub backpatch_lemmanames { 
10972  204 
if($currfile ne "") { 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

205 
select(STDOUT); 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

206 
close(ARGVOUT); 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

207 
open(TMPW, '>'.$finalfile); 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

208 
open TMPR,$tmpfile or die "Can't find tmp file $tmp: $!\n"; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

209 
while(<TMPR>) { 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

210 
s/@@(\d+)@@/$lemmanames[$1]/eg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

211 
print TMPW; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

212 
} 
11068  213 
system("mv $currfile $currfile~0~") if($currfile ne $default); 
10972  214 
system("rm $tmpfile"); 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

215 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

216 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

217 

fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

218 
sub done { 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

219 
my $name = shift; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

220 
my $attr = shift; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

221 
$lemmanames[$lemmacount] = $name.$attr; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

222 
"done"; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

223 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

224 

11013  225 
$currfile = ""; 
11068  226 
$default = "convert_default_stdout"; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

227 
while (<>) { # main loop 
10972  228 
if ($ARGV ne $currfile) { 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

229 
$x=$_; backpatch_lemmanames; $_=$x; 
11068  230 
$currfile = ($ARGV eq "" ? $default : $ARGV); 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

231 
$lemmacount=0; 
10972  232 
$finalfile = "$currfile.thy"; 
233 
$tmpfile = "$finalfile.~0~"; 

10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

234 
open(ARGVOUT, '>'.$tmpfile); 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

235 
select(ARGVOUT); 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

236 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

237 
nl: 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

238 
if(!s/;(\s*?(\n?$\(\*))/$1/s && !eof()) {# no end_of_ML_command marker 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

239 
$_ = $_ . <>; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

240 
goto nl; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

241 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

242 
s/\\(\s*\n\s*)\\/ $1 /g; # remove backslashes escaping newlines 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

243 
nlc: 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

244 
m/^(\s*)(.*?)(\s*)$/s; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

245 
$head=$1; $line=$2; $tail=$3; 
10972  246 
$tail =~ s/\s+\n/\n/sg; # remove trailing whitespace at end of lines 
14362  247 
$line =~ s/\\\\<(\^?)(\w+)>/\\<$1$2>/g; # convert \\<...> to \<...> and \\<^...> to \<^...> 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

248 
print $head; $_=$line.$tail; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

249 
if ($line =~ m/^\(\*/) { # start comment 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

250 
while (($i = index $_,"*)") == 1 && !eof()) { # no end comment 
14362  251 
s/\\\\<(\^?)(\w+)>/\\<$1$2>/g; # convert \\<...> to \<...> and \\<^...> to \<^...> 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

252 
print; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

253 
$_ = <>; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

254 
} 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

255 
if ($i == 1) { print; last; } 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

256 
print substr $_,0,$i+2; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

257 
$_ = substr $_,$i+2; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

258 
goto nlc; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

259 
} 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

260 
$_=$line; 
11272  261 
if(!($head =~ m/^\n/)) { $head = "\n$head"; } 
11013  262 
s/^Goalw *(\[[\w\'\.\s,]*\][\w\'\. \[,\]]+) *(.+)/ 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

263 
"lemma ".lemmaname().": $2$head"."apply (unfold ".thmlist($1).")"/se; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

264 
s/^Goal *(.+)/"lemma ".lemmaname().": $1"/se; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

265 
s/\bgoal/"(*".lemmaname()."*)goal"/se; # ugly oldstyle goals 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

266 
s/^qed_spec_mp *\"(.*?)\"/done($1," [rule_format (no_asm)]")/se; 
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

267 
s/^qed *\"(.*?)\"/done($1,"")/se; 
11068  268 
s/^val *(\w+) *= *result *\( *\) *$/done($1,"")/se; 
269 
s/^bind_thm *\( *\"(.*?)\" *, *(result *\( *\) *?) *\) *$/done($1,"")/se; 

10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

270 
s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se; 
11131  271 
s/^bind_thm *\( *\"(.*?)\" *, *(.*?) *\) *$/"lemmas $1 = ".subst_RS_standard($2)/se; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

272 
s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/process_tac($1,$2).$3/se; 
11263
e502756bcb11
added parentheses for 'b y' syntax, added primitive smp_tac support
oheimb
parents:
11198
diff
changeset

273 
s/^b\s+y(\s*)(.*?)(\s*)$/process_tac($1,"(".$2.")").$3/se; 
11013  274 
s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/; 
13076
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

275 
# remove outermost parentheses if around atoms 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

276 
s/^(apply +)\(\((.*?)\)([+*]?)\)\s*$/$1($2)$3/; 
70704dd48bd5
bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
oheimb
parents:
11329
diff
changeset

277 
# remove outermost parentheses if around parentheses 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

278 
s/^Addsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

279 
s/^Delsimps\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"simp del")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

280 
s/^Addsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

281 
s/^Delsplits\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"split del")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

282 
s/^AddIs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"intro")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

283 
s/^AddSIs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"intro!")/seg; 
11114  284 
s/^AddXIs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"intro?")/seg; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

285 
s/^AddEs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"elim")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

286 
s/^AddSEs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"elim!")/seg; 
11114  287 
s/^AddXEs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"elim?")/seg; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

288 
s/^AddDs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"dest")/seg; 
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

289 
s/^AddSDs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"dest!")/seg; 
11114  290 
s/^AddXDs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"dest?")/seg; 
11286  291 
s/^AddIffs\s*\[?\s*([\w\'\. ,]*)\s*\]?/decl($1,"iff")/seg; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

292 
print "$_$tail"; 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

293 
if(eof()) { last; } # prevents reading finally from stdin (thru <>)! 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

294 
} 
11081
ce9a6746cd1e
solved noninitialization problems; improvements using prefer
oheimb
parents:
11068
diff
changeset

295 
backpatch_lemmanames; 
10939
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset

296 
select(STDOUT); 