author | wenzelm |
Fri, 19 Jan 2001 11:53:21 +0100 | |
changeset 10939 | fe14e54594a3 |
child 10972 | af160f8d3bd7 |
permissions | -rw-r--r-- |
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 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
5 |
# |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
6 |
# convert.pl - convert legacy tactic scripts to Isabelle/Isar tactic |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
7 |
# emulation using heuristics - leaves unrecognized patterns unchanged |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
8 |
# produces from each input file (on the command line) a new file with |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
9 |
# ".thy" appended |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
10 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
11 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
12 |
sub thmlist { |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
13 |
my $s = shift; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
14 |
$s =~ s/^\[(.*)\]$/$1/sg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
15 |
$s =~ s/, +/ /g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
16 |
$s =~ s/,/ /g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
17 |
$s; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
18 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
19 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
20 |
sub process_tac { |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
21 |
my $t = shift; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
22 |
my $simpmodmod = ($t =~ m/auto_tac|force_tac|clarsimp_tac/) ? "simp " : ""; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
23 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
24 |
$_ = $t; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
25 |
s/Blast_tac *1/blast/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
26 |
s/Fast_tac *1/fast/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
27 |
s/Slow_tac *1/slow/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
28 |
s/Best_tac *1/best/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
29 |
s/Safe_tac/safe/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
30 |
s/Clarify_tac *1/clarify/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
31 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
32 |
s/blast_tac *\( *claset *\( *\) *(.*?)\) *1/blast $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
33 |
s/fast_tac *\( *claset *\( *\) *(.*?)\) *1/fast $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
34 |
s/slow_tac *\( *claset *\( *\) *(.*?)\) *1/slow $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
35 |
s/best_tac *\( *claset *\( *\) *(.*?)\) *1/best $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
36 |
s/safe_tac *\( *claset *\( *\) *(.*?)\) */safe $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
37 |
s/clarify_tac *\( *claset *\( *\) *(.*?)\) *1/clarify $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
38 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
39 |
s/Auto_tac/auto/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
40 |
s/Force_tac *1/force/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
41 |
s/Clarsimp_tac *1/clarsimp/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
42 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
43 |
s/auto_tac *\( *claset *\( *\) *(.*?), *simpset *\( *\) *(.*?)\) */auto$1$2/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
44 |
s/force_tac *\( *claset *\( *\) *(.*?), *simpset *\( *\) *(.*?)\) *1/force$1$2/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
45 |
s/clarsimp_tac *\( *claset *\( *\) *(.*?), *simpset *\( *\) *(.*?)\) *1/clarsimp$1$2/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
46 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
47 |
s/Simp_tac *1/simp (no_asm)/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
48 |
s/Asm_simp_tac *1/simp (no_asm_simp)/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
49 |
s/Full_simp_tac_tac *1/simp (no_asm_use)/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
50 |
s/Asm_full_simp_tac_tac *1/simp/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
51 |
s/ALLGOALS *Asm_full_simp_tac/simp_all/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
52 |
s/ALLGOALS *Simp_tac/simp_all (no_asm)/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
53 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
54 |
s/atac *1/assumption/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
55 |
s/hypsubst_tac *1/hypsubst/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
56 |
s/arith_tac *1/arith/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
57 |
s/strip_tac *1/intro strip/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
58 |
s/split_all_tac *1/simp (no_asm_simp) only: split_tupled_all/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
59 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
60 |
s/rotate_tac *(\d+) *1/rotate_tac $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
61 |
s/rotate_tac *(\d+) *(\d+)/rotate_tac [$2] $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
62 |
s/case_tac *(\".*\") *1/case_tac $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
63 |
s/case_tac *(\".*\") *(\d+)/case_tac [$2] $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
64 |
s/induct_tac *(\".*\") *1/induct_tac $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
65 |
s/induct_tac *(\".*\") *(\d+)/induct_tac [$2] $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
66 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
67 |
s/stac (\w+) +1/subst $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
68 |
s/rtac (\w+) +1/rule $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
69 |
s/rtac (\w+) +(\d+)/rule_tac [$2] $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
70 |
s/dtac (\w+) +1/drule $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
71 |
s/dtac (\w+) +(\d+)/drule_tac [$2] $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
72 |
s/etac (\w+) +1/erule $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
73 |
s/etac (\w+) +(\d+)/erule_tac [$2] $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
74 |
s/ftac (\w+) +1/frule $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
75 |
s/rfac (\w+) +(\d+)/frule_tac [$2] $1/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
76 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
77 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
78 |
s/THEN/,/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
79 |
s/ORELSE/|/g; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
80 |
s/fold_goals_tac *(\[[\w\s,]*\]|[\w]+)/"fold ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
81 |
s/rewrite_goals_tac *(\[[\w\s,]*\]|[\w]+)/"unfold ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
82 |
s/cut_facts_tac *(\[[\w\s,]*\]|[\w]+)/"insert ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
83 |
s/EVERY *(\[[\w\s,]*\]|[\w]+)/thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
84 |
s/addIs *(\[[\w\s,]*\]|[\w]+)/" intro: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
85 |
s/addSIs *(\[[\w\s,]*\]|[\w]+)/" intro!: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
86 |
s/addEs *(\[[\w\s,]*\]|[\w]+)/" elim: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
87 |
s/addSEs *(\[[\w\s,]*\]|[\w]+)/" elim!: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
88 |
s/addDs *(\[[\w\s,]*\]|[\w]+)/" dest: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
89 |
s/addSDs *(\[[\w\s,]*\]|[\w]+)/" dest!: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
90 |
s/delrules *(\[[\w\s,]*\]|[\w]+)/" del: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
91 |
s/addsimps *(\[[\w\s,]*\]|[\w]+)/" $simpmodmod"."add: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
92 |
s/delsimps *(\[[\w\s,]*\]|[\w]+)/" $simpmodmod"."del: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
93 |
s/addcongs *(\[[\w\s,]*\]|[\w]+)/" cong add: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
94 |
s/delcongs *(\[[\w\s,]*\]|[\w]+)/" cong del: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
95 |
s/addsplits *(\[[\w\s,]*\]|[\w]+)/" split add: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
96 |
s/delsplits *(\[[\w\s,]*\]|[\w]+)/" split del: ".thmlist($1)/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
97 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
98 |
s/^\s*(.*)\s*$/$1/s; # remove enclosing whitespace |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
99 |
s/^\(\s*([\w]+)\s*\)$/$1/; # remove enclosing parentheses around atoms |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
100 |
s/^([a-zA-Z])/ $1/; # add space if required |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
101 |
$_; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
102 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
103 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
104 |
sub thmname { "@@" . ++$thmcount . "@@"; } |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
105 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
106 |
sub backpatch_thmnames { |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
107 |
if($oldargv ne "") { |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
108 |
select(STDOUT); |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
109 |
close(ARGVOUT); |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
110 |
open(TMPW, '>'.$finalfile); |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
111 |
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
|
112 |
while(<TMPR>) { |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
113 |
s/@@(\d+)@@/$thmnames[$1]/eg; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
114 |
print TMPW $_; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
115 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
116 |
system("rm " . $oldargv . '.thy~~'); |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
117 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
118 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
119 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
120 |
sub done { |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
121 |
my $name = shift; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
122 |
my $attr = shift; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
123 |
$thmnames[$thmcount] = $name.$attr; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
124 |
"done"; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
125 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
126 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
127 |
$next = "nonempty"; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
128 |
while (<>) { # main loop |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
129 |
if ($ARGV ne $oldargv) { |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
130 |
$x=$_; backpatch_thmnames; $_=$x; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
131 |
$thmcount=0; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
132 |
$finalfile = "$ARGV" . '.thy'; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
133 |
$tmpfile = $finalfile . '~~'; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
134 |
open(ARGVOUT, '>'.$tmpfile); |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
135 |
select(ARGVOUT); |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
136 |
$oldargv = $ARGV; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
137 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
138 |
|
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
139 |
nl: |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
140 |
if(!(s/;\s*?(\n?)$/$1/s)) {# no end_of_ML_command marker |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
141 |
$next = <>; $_ = $_ . $next; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
142 |
if($next) { goto nl; } |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
143 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
144 |
s/\\(\s*\n\s*)\\/ $1 /g; # remove backslashes escaping newlines |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
145 |
nlc: |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
146 |
m/^(\s*)(.*?)(\s*)$/s; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
147 |
$head=$1; $line=$2; $tail=$3; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
148 |
print $head; $_=$2.$tail; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
149 |
if ($line =~ m/^\(\*/) { # start comment |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
150 |
while (($i = index $_,"*)") == -1) { # no end comment |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
151 |
print $_; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
152 |
$_ = <>; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
153 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
154 |
print substr $_,0,$i+2; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
155 |
$_ = substr $_,$i+2; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
156 |
goto nlc; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
157 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
158 |
$_=$line; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
159 |
s/^Goalw *(\[[\w\s,]*\]|[\w]+) *(.+)/ |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
160 |
"lemma ".thmname().": $2$head"."apply (unfold ".thmlist($1).")"/se; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
161 |
s/^Goal *(.+)/"lemma ".thmname().": $1"/se; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
162 |
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
|
163 |
s/^qed *\"(.*?)\"/done($1,"")/se; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
164 |
s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
165 |
s/^by(\s*)(.*)$/"apply$1".process_tac($2)/se; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
166 |
print "$_$tail"; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
167 |
if(!$next) { last; } # prevents reading finally from stdin (thru <>)! |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
168 |
} |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
169 |
backpatch_thmnames; |
fe14e54594a3
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff
changeset
|
170 |
select(STDOUT); |