src/HOL/Lex/AutoChopper.ML
author nipkow
Wed Feb 12 18:54:39 1997 +0100 (1997-02-12)
changeset 2609 4370e5f0fa3f
parent 2056 93c093620c28
child 3842 b55686a7b22c
permissions -rw-r--r--
New class "order" and accompanying changes.
clasohm@1465
     1
(*  Title:      HOL/Lex/AutoChopper.ML
nipkow@1344
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Richard Mayr & Tobias Nipkow
nipkow@1344
     4
    Copyright   1995 TUM
nipkow@1344
     5
nipkow@1344
     6
Main result: auto_chopper satisfies the is_auto_chopper specification.
nipkow@1344
     7
*)
nipkow@1344
     8
paulson@1950
     9
Delsimps (ex_simps @ all_simps);
paulson@1950
    10
nipkow@1344
    11
open AutoChopper;
nipkow@1344
    12
nipkow@1344
    13
infix repeat_RS;
nipkow@1344
    14
fun th1 repeat_RS th2 = ((th1 RS th2) repeat_RS th2) handle _ => th1;
nipkow@1344
    15
nipkow@1344
    16
Addsimps [Let_def];
nipkow@1344
    17
nipkow@1344
    18
goal AutoChopper.thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
nipkow@1344
    19
by (list.induct_tac "xs" 1);
nipkow@1344
    20
by (Simp_tac 1);
nipkow@1344
    21
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1344
    22
val accept_not_Nil = result() repeat_RS spec;
nipkow@1344
    23
Addsimps [accept_not_Nil];
nipkow@1344
    24
nipkow@1344
    25
goal AutoChopper.thy
nipkow@1344
    26
"!st us. acc xs st [] us ([],ys) A = ([], zs) --> \
nipkow@1344
    27
\        zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (nexts A st ys))";
nipkow@1344
    28
by (list.induct_tac "xs" 1);
nipkow@1344
    29
by (simp_tac (!simpset addcongs [conj_cong]) 1);
nipkow@1344
    30
by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
nipkow@1344
    31
by (strip_tac 1);
clasohm@1465
    32
by (rtac conjI 1);
berghofe@1894
    33
by (Fast_tac 1);
paulson@2056
    34
by (simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1);
nipkow@1344
    35
by (strip_tac 1);
paulson@2056
    36
by (REPEAT(eresolve_tac [conjE,exE] 1));
paulson@2056
    37
by (hyp_subst_tac 1);
nipkow@1344
    38
by (Simp_tac 1);
nipkow@1344
    39
by (case_tac "zsa = []" 1);
nipkow@1344
    40
by (Asm_simp_tac 1);
berghofe@1894
    41
by (Fast_tac 1);
nipkow@1344
    42
bind_thm("no_acc", result() RS spec RS spec RS mp);
nipkow@1344
    43
nipkow@1344
    44
nipkow@1344
    45
val [prem] = goal HOL.thy "? x.P(f(x)) ==> ? y.P(y)";
nipkow@1344
    46
by (cut_facts_tac [prem] 1);
berghofe@1894
    47
by (Fast_tac 1);
nipkow@1344
    48
val ex_special = result();
nipkow@1344
    49
nipkow@1344
    50
nipkow@1344
    51
goal AutoChopper.thy
nipkow@1344
    52
"! r erk l rst st ys yss zs::'a list. \
nipkow@1344
    53
\    acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
nipkow@2609
    54
\    ys@concat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@concat(l)@rst)";
nipkow@1344
    55
by (list.induct_tac "xs" 1);
nipkow@1344
    56
 by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
nipkow@1344
    57
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
paulson@2056
    58
by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
paulson@2056
    59
by (rename_tac "vss lrst" 1);  
nipkow@1344
    60
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1344
    61
by (res_inst_tac[("xs","vss")] list_eq_cases 1);
paulson@2056
    62
 by (hyp_subst_tac 1);
paulson@2056
    63
 by (Simp_tac 1);
berghofe@1894
    64
 by (fast_tac (!claset addSDs [no_acc]) 1);
paulson@2056
    65
by (hyp_subst_tac 1);
nipkow@1344
    66
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1344
    67
val step2_a = (result() repeat_RS spec) RS mp;
nipkow@1344
    68
nipkow@1344
    69
nipkow@1344
    70
goal AutoChopper.thy
nipkow@1344
    71
 "! st erk r l rest ys yss zs.\
nipkow@1344
    72
\   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
nipkow@1344
    73
\     (if acc_prefix A st xs \
nipkow@1344
    74
\      then ys ~= [] \
nipkow@1344
    75
\      else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
nipkow@1344
    76
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1344
    77
by (list.induct_tac "xs" 1);
nipkow@1344
    78
 by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
berghofe@1894
    79
 by (Fast_tac 1);
nipkow@1344
    80
by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
paulson@2056
    81
by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
paulson@2056
    82
by (rename_tac "vss lrst" 1);  
paulson@2056
    83
by (Asm_simp_tac 1);
nipkow@1344
    84
by (strip_tac 1);
nipkow@1344
    85
by (case_tac "acc_prefix A (next A st a) list" 1);
paulson@2056
    86
 by (Asm_simp_tac 1);
nipkow@1344
    87
by (subgoal_tac "r @ [a] ~= []" 1);
berghofe@1894
    88
 by (Fast_tac 1);
nipkow@1344
    89
by (Simp_tac 1);
nipkow@1344
    90
val step2_b = (result() repeat_RS spec) RS mp;
nipkow@1344
    91
nipkow@1344
    92
nipkow@1344
    93
goal AutoChopper.thy  
nipkow@1344
    94
 "! st erk r l rest ys yss zs. \
nipkow@1344
    95
\   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
nipkow@1344
    96
\     (if acc_prefix A st xs                   \
nipkow@1344
    97
\      then ? g. ys=r@g & fin A (nexts A st g)  \
nipkow@1344
    98
\      else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
nipkow@1344
    99
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1344
   100
by (list.induct_tac "xs" 1);
nipkow@1344
   101
 by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
berghofe@1894
   102
 by (Fast_tac 1);
nipkow@1344
   103
by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
nipkow@1344
   104
by (strip_tac 1);
clasohm@1465
   105
by (rtac conjI 1);
paulson@2056
   106
 by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
paulson@2056
   107
 by (rename_tac "vss lrst" 1);  
paulson@2056
   108
 by (Asm_simp_tac 1);
nipkow@1344
   109
 by (case_tac "acc_prefix A (next A st a) list" 1);
nipkow@1344
   110
  by (strip_tac 1);
nipkow@1344
   111
  by (res_inst_tac [("f","%k.a#k")] ex_special 1);
nipkow@1344
   112
  by (Simp_tac 1);
nipkow@1344
   113
  by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
nipkow@1344
   114
   by (Simp_tac 1);
berghofe@1894
   115
  by (Fast_tac 1);
nipkow@1344
   116
 by (strip_tac 1);
nipkow@1344
   117
 by (res_inst_tac [("x","[a]")] exI 1);
nipkow@1344
   118
 by (Asm_simp_tac 1);
nipkow@1344
   119
 by (subgoal_tac "r @ [a] ~= []" 1);
paulson@2056
   120
  by (rtac sym 1);
berghofe@1894
   121
  by (Fast_tac 1);
nipkow@1344
   122
 by (Simp_tac 1);
nipkow@1344
   123
by (strip_tac 1);
nipkow@1344
   124
by (res_inst_tac [("f","%k.a#k")] ex_special 1);
nipkow@1344
   125
by (Simp_tac 1);
nipkow@1344
   126
by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
nipkow@1344
   127
 by (Simp_tac 1);
berghofe@1894
   128
by (Fast_tac 1);
nipkow@1344
   129
val step2_c = (result() repeat_RS spec) RS mp;
nipkow@1344
   130
nipkow@1344
   131
nipkow@1344
   132
goal AutoChopper.thy
nipkow@1344
   133
 "! st erk r l rest ys yss zs. \
nipkow@1344
   134
\   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
nipkow@1344
   135
\     (if acc_prefix A st xs       \
nipkow@2609
   136
\      then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
nipkow@1344
   137
\      else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
nipkow@1344
   138
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1344
   139
by (list.induct_tac "xs" 1);
nipkow@1344
   140
 by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
berghofe@1894
   141
 by (Fast_tac 1);
nipkow@1344
   142
by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
paulson@2056
   143
by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
paulson@2056
   144
by (rename_tac "vss lrst" 1);  
paulson@2056
   145
by (Asm_simp_tac 1);
nipkow@1344
   146
by (strip_tac 1);
nipkow@1344
   147
by (case_tac "acc_prefix A (next A st a) list" 1);
nipkow@1344
   148
 by (Asm_simp_tac 1);
nipkow@1344
   149
by (subgoal_tac "acc list (start A) [] [] ([],list) A = (yss,zs)" 1);
nipkow@1344
   150
 by (Asm_simp_tac 2);
nipkow@1344
   151
 by (subgoal_tac "r@[a] ~= []" 2);
berghofe@1894
   152
  by (Fast_tac 2);
nipkow@1344
   153
 by (Simp_tac 2);
nipkow@2609
   154
by (subgoal_tac "concat(yss) @ zs = list" 1);
paulson@2056
   155
 by (hyp_subst_tac 1);
paulson@2056
   156
 by (atac 1);
nipkow@1344
   157
by (case_tac "yss = []" 1);
nipkow@1344
   158
 by (Asm_simp_tac 1);
nipkow@1344
   159
 by (hyp_subst_tac 1);
berghofe@1894
   160
 by (fast_tac (!claset addSDs [no_acc]) 1);
clasohm@1465
   161
by (etac ((neq_Nil_conv RS iffD1) RS exE) 1);
clasohm@1465
   162
by (etac exE 1);
nipkow@1344
   163
by (hyp_subst_tac 1);
nipkow@1344
   164
by (Simp_tac 1);
clasohm@1465
   165
by (rtac trans 1);
paulson@2056
   166
 by (etac step2_a 1);
nipkow@1344
   167
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1344
   168
val step2_d = (result() repeat_RS spec) RS mp;
nipkow@1344
   169
nipkow@1344
   170
Delsimps [split_paired_All];
nipkow@1344
   171
goal AutoChopper.thy 
nipkow@1344
   172
"! st erk r p ys yss zs. \
nipkow@1344
   173
\  acc xs st erk r p A = (ys#yss, zs) --> \
nipkow@1344
   174
\  (if acc_prefix A st xs  \
nipkow@1344
   175
\   then ? g.ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
nipkow@1344
   176
\   else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
nipkow@1344
   177
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1344
   178
by (list.induct_tac "xs" 1);
nipkow@1344
   179
 by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
berghofe@1894
   180
 by (Fast_tac 1);
nipkow@1344
   181
by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
nipkow@1344
   182
by (strip_tac 1);
nipkow@1344
   183
by (case_tac "acc_prefix A (next A st a) list" 1);
paulson@2056
   184
 by (rtac conjI 1);
nipkow@1344
   185
  by (strip_tac 1);
nipkow@1344
   186
  by (res_inst_tac [("f","%k.a#k")] ex_special 1);
nipkow@1344
   187
  by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
nipkow@1344
   188
   by (Simp_tac 1);
nipkow@1344
   189
  by (res_inst_tac [("P","%k.ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
nipkow@1344
   190
   by (asm_simp_tac HOL_ss 1);
nipkow@1344
   191
  by (res_inst_tac [("x","x")] exI 1);
nipkow@1344
   192
  by (Asm_simp_tac 1);
paulson@2056
   193
  by (rtac list_cases 1);
nipkow@1344
   194
   by (Simp_tac 1);
nipkow@1344
   195
  by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
nipkow@1344
   196
 by (strip_tac 1);
nipkow@1344
   197
 by (res_inst_tac [("f","%k.a#k")] ex_special 1);
nipkow@1344
   198
 by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
nipkow@1344
   199
  by (Simp_tac 1);
nipkow@1344
   200
 by (res_inst_tac [("P","%k.ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
nipkow@1344
   201
  by (asm_simp_tac HOL_ss 1);
nipkow@1344
   202
 by (res_inst_tac [("x","x")] exI 1);
nipkow@1344
   203
 by (Asm_simp_tac 1);
paulson@2056
   204
 by (rtac list_cases 1);
nipkow@1344
   205
  by (Simp_tac 1);
nipkow@1344
   206
 by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
nipkow@1344
   207
by (Asm_simp_tac 1);
nipkow@1344
   208
by (strip_tac 1);
nipkow@1344
   209
by (res_inst_tac [("x","[a]")] exI 1);
clasohm@1465
   210
by (rtac conjI 1);
nipkow@1344
   211
 by (subgoal_tac "r @ [a] ~= []" 1);
berghofe@1894
   212
  by (Fast_tac 1);
nipkow@1344
   213
 by (Simp_tac 1);
clasohm@1465
   214
by (rtac list_cases 1);
nipkow@1344
   215
 by (Simp_tac 1);
nipkow@1344
   216
by (asm_full_simp_tac (!simpset addsimps [acc_prefix_def] addcongs[conj_cong]) 1);
clasohm@1465
   217
by (etac thin_rl 1); (* speed up *)
berghofe@1894
   218
by (Fast_tac 1);
nipkow@1344
   219
val step2_e = (result() repeat_RS spec) RS mp;
nipkow@1344
   220
Addsimps[split_paired_All];
nipkow@1344
   221
nipkow@1344
   222
goalw AutoChopper.thy [accepts_def, is_auto_chopper_def, auto_chopper_def,
nipkow@1344
   223
                       Chopper.is_longest_prefix_chopper_def]
nipkow@1344
   224
 "is_auto_chopper(auto_chopper)";
nipkow@1344
   225
by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
paulson@2056
   226
 by (rtac mp 1);
paulson@2056
   227
  by (etac step2_b 2);
nipkow@1344
   228
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
clasohm@1465
   229
by (rtac conjI 1);
paulson@2056
   230
 by (rtac mp 1);
paulson@2056
   231
  by (etac step2_c 2);
nipkow@1344
   232
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
clasohm@1465
   233
by (rtac conjI 1);
nipkow@1344
   234
 by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
clasohm@1465
   235
by (rtac conjI 1);
paulson@2056
   236
 by (rtac mp 1);
paulson@2056
   237
  by (etac step2_d 2);
nipkow@1344
   238
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
clasohm@1465
   239
by (rtac mp 1);
paulson@2056
   240
 by (etac step2_e 2);
nipkow@1344
   241
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
nipkow@1344
   242
qed"auto_chopper_is_auto_chopper";