lib/scripts/convert.pl
author oheimb
Mon, 05 Feb 2001 14:57:17 +0100
changeset 11068 e91f576830e9
parent 11029 a221d8a9413c
child 11081 ce9a6746cd1e
permissions -rw-r--r--
improvements concerning instantiations etc.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
     9
#   ".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
    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
11014
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    20
sub subst_RS {
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    21
  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    22
  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    23
  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    24
  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    25
  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3\]/g;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    26
  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3\]/g;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    27
  s/\(([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2\]/g;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    28
  s/([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2\]/g;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
    29
  s/THEN sym\b/symmetric$1/g;
11014
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    30
}
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    31
11027
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    32
sub subst_RS_fun {
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    33
  my $s = shift;
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    34
  $_ = $s;
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    35
  subst_RS();
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    36
  $_;
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    37
}
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
    38
11014
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    39
sub decl {
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    40
  my $s = shift;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    41
  my $a = shift;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    42
  $_ = $s;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    43
  subst_RS();
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    44
  s/, */ [$a] /g;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    45
  s/$/ [$a]/;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    46
  s/\] *\[/, /g;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    47
  "declare $_";
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    48
}
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
    49
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    50
sub process_tac {
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    51
  my $lead = shift;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    52
  my $t = shift;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    53
  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
    54
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    55
  $_ = $t;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    56
  s/\s+/ /sg;             # remove multiple whitespace
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    57
  s/\s/ /sg;              # substitute all remaining tabs and newlines by space
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    58
  s/\( /\(/g; s/ \)/\)/g; # remove leading and trailing space inside parentheses
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    59
  s/\[ /\[/g; s/ \]/\]/g; # remove leading and trailing space inside sq brackets
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    60
  s/ ?\( ?\)/\(\)/g;      # remove space before and inside empty tuples
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    61
  s/\(\)([^ ])/\(\) $1/g; # possibly add space after empty tuples
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    62
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    63
  s/Blast_tac 1/blast/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    64
  s/Fast_tac 1/fast/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    65
  s/Slow_tac 1/slow/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    66
  s/Best_tac 1/best/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    67
  s/Safe_tac/safe/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    68
  s/Clarify_tac 1/clarify/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    69
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    70
  s/blast_tac \(claset\(\) (.*?)\) 1/blast $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    71
  s/fast_tac \(claset\(\) (.*?)\) 1/fast $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    72
  s/slow_tac \(claset\(\) (.*?)\) 1/slow $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    73
  s/best_tac \(claset\(\) (.*?)\) 1/best $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    74
  s/safe_tac \(claset\(\) (.*?)\)/safe $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    75
  s/clarify_tac \(claset\(\) (.*?)\) 1/clarify $1/g;
10939
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
  s/Auto_tac/auto/g;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    78
  s/Force_tac 1/force/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    79
  s/Clarsimp_tac 1/clarsimp/g;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    80
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    81
  s/auto_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\)/auto $1 $2/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    82
  s/force_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\) 1/force $1 $2/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    83
  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
    84
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    85
  s/Asm_full_simp_tac 1/simp/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    86
  s/Full_simp_tac 1/simp (no_asm_use)/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    87
  s/Asm_simp_tac 1/simp (no_asm_simp)/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    88
  s/Simp_tac 1/simp (no_asm)/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    89
  s/ALLGOALS Asm_full_simp_tac/simp_all/g;
11029
a221d8a9413c little bugfixes; added induct_thm_tac
oheimb
parents: 11027
diff changeset
    90
  s/ALLGOALS Full_simp_tac/simp_all (no_asm_use)/g;
a221d8a9413c little bugfixes; added induct_thm_tac
oheimb
parents: 11027
diff changeset
    91
  s/ALLGOALS Asm_simp_tac/simp_all (no_asm_simp)/g;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    92
  s/ALLGOALS Simp_tac/simp_all (no_asm)/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    93
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    94
  s/asm_full_simp_tac \(simpset\(\) (.*?)\) 1/simp $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    95
  s/full_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_use) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    96
  s/asm_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_simp) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    97
  s/simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    98
  s/ALLGOALS \(asm_full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
    99
  s/ALLGOALS \(full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_use) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   100
  s/ALLGOALS \(asm_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_simp) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   101
  s/ALLGOALS \(simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm) $1/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   102
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   103
  s/a((ssume_)?)tac 1/assumption/g;
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   104
  s/a((ssume_)?)tac (\d+)/tactic \"assume_tac $1\"/g;
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   105
  s/\bmp_tac 1/erule (1) notE impE/g;
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   106
  s/\bmp_tac (\d+)/erule_tac [$1] notE impE, tactic \"assume_tac $1\"/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   107
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   108
  s/hypsubst_tac 1/hypsubst/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   109
  s/arith_tac 1/arith/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   110
  s/strip_tac 1/intro strip/g;
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   111
  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
   112
11009
9e0ad9a5f9bb added attribute declarations, etc.
oheimb
parents: 11001
diff changeset
   113
  s/rotate_tac (\d+) (\d+)/rotate_tac [$2] $1/g;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   114
  s/rotate_tac ~ *(\d+) (\d+)/rotate_tac [$2] -$1/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   115
  s/rename_tac (\".*?\") (\d+)/rename_tac [$2] $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   116
  s/case_tac (\".*?\") (\d+)/case_tac [$2] $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   117
  s/induct_tac (\".*?\") (\d+)/induct_tac [$2] $1/g;
11029
a221d8a9413c little bugfixes; added induct_thm_tac
oheimb
parents: 11027
diff changeset
   118
  s/induct_thm_tac ([\w\'\. \[,\]]+?) (\".*?\") (\d+)/induct_tac [$3] $2 rule: $1/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   119
  s/subgoal_tac (\".*?\") (\d+)/subgoal_tac [$2] $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   120
  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
   121
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   122
  s/THEN /, /g;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   123
  s/ORELSE/|/g;
11014
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   124
  subst_RS();
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   125
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   126
  s/\(\"(.*?)\" *, *(\".*?\")\) *, */$1 = $2 and /g; # instantiations
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   127
  s/\(\"(.*?)\" *, *(\".*?\")\)/$1 = $2/g;       # last instantiation
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   128
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   129
  s/rewtac ([\w\'\. \[,\]]+)/unfold $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   130
  s/stac ([\w\'\. \[,\]]+?) 1/subst $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   131
  s/rtac ([\w\'\. \[,\]]+?) 1/rule $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   132
  s/rtac ([\w\'\. \[,\]]+?) (\d+)/rule_tac [$2] $1/g;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   133
  s/res_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/rule_tac [$3] $1 in $2/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   134
  s/dtac ([\w\'\. \[,\]]+?) 1/drule $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   135
  s/dtac ([\w\'\. \[,\]]+?) (\d+)/drule_tac [$2] $1/g;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   136
  s/dres_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/drule_tac [$3] $1 in $2/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   137
  s/datac ([\w\'\. \[,\]]+?) (\d+) 1/drule ($2) $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   138
  s/etac ([\w\'\. \[,\]]+?) 1/erule $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   139
  s/etac ([\w\'\. \[,\]]+?) (\d+)/erule_tac [$2] $1/g;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   140
  s/eres_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/erule_tac [$3] $1 in $2/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   141
  s/eatac ([\w\'\. \[,\]]+?) (\d+) 1/erule ($2) $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   142
  s/forward_tac \[([\w\'\. \[,\]]+)\] 1/frule $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   143
  s/forward_tac \[([\w\'\. \[,\]]+)\] (\d+)/frule_tac [$2] $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   144
  s/ftac ([\w\'\. \[,\]]+?) 1/frule $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   145
  s/ftac ([\w\'\. \[,\]]+?) (\d+)/frule_tac [$2] $1/g;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   146
  s/forw_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/frule_tac [$3] $1 in $2/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   147
  s/fatac ([\w\'\. \[,\]]+?) (\d+) 1/frule ($2) $1/g;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   148
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   149
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   150
  s/fold_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"fold ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   151
  s/rewrite_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"unfold ".thmlist($1)/eg;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   152
  s/cut_inst_tac \[(.*?)\] ([\w\'\. \[,\]]+?) (\d+)/cut_tac [$3] $1 in $2/g;
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   153
  s/cut_facts_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+) (\d+)/"cut_tac [$2] ".thmlist($1)/eg;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   154
  s/resolve_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+) 1/"rule ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   155
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   156
  s/addIs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"intro: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   157
  s/addSIs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"intro!: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   158
  s/addEs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"elim: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   159
  s/addSEs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"elim!: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   160
  s/addDs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"dest: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   161
  s/addSDs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"dest!: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   162
  s/delrules *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"del: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   163
  s/addsimps *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"$simpmodmod"."add: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   164
  s/delsimps *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"$simpmodmod"."del: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   165
  s/addcongs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"cong add: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   166
  s/delcongs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"cong del: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   167
  s/addsplits *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"split add: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   168
  s/delsplits *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"split del: ".thmlist($1)/eg;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   169
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   170
  s/_tac \[1\]/_tac/g;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   171
  s/ +/ /g;                       # remove multiple whitespace
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   172
  s/\( /\(/; s/ \)/\)/g;  # remove leading and trailing space inside parentheses
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   173
  s/^ *(.*?) *$/$1/s;             # remove enclosing whitespace
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   174
  s/^([a-zA-Z])/ $1/ if (!($lead =~ m/[\s\(]$/)); # add space if required
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   175
  $_;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   176
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   177
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   178
sub thmname { "@@" . ++$thmcount . "@@"; }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   179
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   180
sub backpatch_thmnames {
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   181
  if($currfile ne "") {
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   182
    select(STDOUT);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   183
    close(ARGVOUT);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   184
    open(TMPW, '>'.$finalfile);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   185
    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
   186
    while(<TMPR>) {
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   187
      s/@@(\d+)@@/$thmnames[$1]/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   188
      print TMPW $_;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   189
    }
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   190
    system("mv $currfile $currfile~0~") if($currfile ne $default);
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   191
    system("rm $tmpfile");
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   192
  }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   193
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   194
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   195
sub done {
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   196
  my $name = shift;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   197
  my $attr = shift;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   198
  $thmnames[$thmcount] = $name.$attr;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   199
  "done";
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   200
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   201
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   202
$currfile = "";
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   203
$next = "nonempty";
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   204
$default = "convert_default_stdout";
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   205
while (<>) { # main loop
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   206
  if ($ARGV ne $currfile) {
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   207
    $x=$_; backpatch_thmnames; $_=$x;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   208
    $currfile = ($ARGV eq "-" ? $default : $ARGV);
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   209
    $thmcount=0;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   210
    $finalfile = "$currfile.thy";
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   211
    $tmpfile   = "$finalfile.~0~";
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   212
    open(ARGVOUT, '>'.$tmpfile);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   213
    select(ARGVOUT);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   214
  }
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
 nl:
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   217
  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
   218
    $next = <>; $_ = $_ . $next;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   219
    if($next) { goto nl; }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   220
  }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   221
  s/\\(\s*\n\s*)\\/ $1 /g; # remove backslashes escaping newlines
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   222
 nlc:
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   223
  m/^(\s*)(.*?)(\s*)$/s;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   224
  $head=$1; $line=$2; $tail=$3;
10972
af160f8d3bd7 debugging and extensions
oheimb
parents: 10939
diff changeset
   225
  $tail =~ s/\s+\n/\n/sg;  # remove trailing whitespace at end of lines
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   226
  print $head; $_=$2.$tail;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   227
  if ($line =~ m/^\(\*/) { # start comment
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   228
    while (($i = index $_,"*)") == -1) { # no end comment
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   229
      print $_;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   230
      $_ = <>;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   231
    }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   232
    print substr $_,0,$i+2;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   233
    $_ = substr $_,$i+2;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   234
    goto nlc;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   235
  }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   236
  $_=$line;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   237
  s/^Goalw *(\[[\w\'\.\s,]*\]|[\w\'\. \[,\]]+) *(.+)/
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   238
    "lemma ".thmname().": $2$head"."apply (unfold ".thmlist($1).")"/se;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   239
  s/^Goal *(.+)/"lemma ".thmname().": $1"/se;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   240
  s/\bgoal/"(*".thmname()."*)goal"/se; # ugly old-style goals
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   241
  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
   242
  s/^qed *\"(.*?)\"/done($1,"")/se;
11068
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   243
  s/^val *(\w+) *= *result *\( *\) *$/done($1,"")/se;
e91f576830e9 improvements concerning instantiations etc.
oheimb
parents: 11029
diff changeset
   244
  s/^bind_thm *\( *\"(.*?)\" *, *(result *\( *\) *?) *\) *$/done($1,"")/se;
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   245
  s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
11027
17e9f0ba15ee added translations for bind_thm and val
oheimb
parents: 11014
diff changeset
   246
  s/^bind_thm *\( *\"(.*?)\" *, *(.*?) *\) *$/"lemmas $1 = ".subst_RS_fun($2)/se;
11029
a221d8a9413c little bugfixes; added induct_thm_tac
oheimb
parents: 11027
diff changeset
   247
  s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/"apply".$1.process_tac($1,$2).$3/se;
11013
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   248
  s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
b2af88422983 further minor improvements
oheimb
parents: 11009
diff changeset
   249
                             # remove outermost parentheses if around atoms
11014
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   250
  s/^Addsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"simp")/seg;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   251
  s/^Delsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"simp del")/seg;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   252
  s/^Addsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"split")/seg;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   253
  s/^Delsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"split del")/seg;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   254
  s/^AddIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"intro")/seg;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   255
  s/^AddSIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"intro!")/seg;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   256
  s/^AddEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"elim")/seg;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   257
  s/^AddSEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"elim!")/seg;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   258
  s/^AddDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"dest")/seg;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   259
  s/^AddSDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/decl($1,"dest!")/seg;
c205ede3140d debugged declare
oheimb
parents: 11013
diff changeset
   260
  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
   261
  print "$_$tail";
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   262
  if(!$next) { last; } # prevents reading finally from stdin (thru <>)!
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   263
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   264
backpatch_thmnames;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   265
select(STDOUT);