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