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