src/HOL/Lex/Auto.ML
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1985 84cf16192e03
child 4089 96fba19bcbe2
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
     1 (*  Title:      HOL/Lex/Auto.ML
     2     ID:         $Id$
     3     Author:     Richard Mayr & Tobias Nipkow
     4     Copyright   1995 TUM
     5 *)
     6 
     7 open Auto;
     8 
     9 goalw Auto.thy [nexts_def] "nexts A st [] = st";
    10 by(Simp_tac 1);
    11 qed"nexts_Nil";
    12 
    13 goalw Auto.thy [nexts_def] "nexts A st (x#xs) = nexts A (next A st x) xs";
    14 by(Simp_tac 1);
    15 qed"nexts_Cons";
    16 
    17 Addsimps [nexts_Nil,nexts_Cons];
    18 
    19 goalw Auto.thy [acc_prefix_def] "~acc_prefix A st []";
    20 by(Simp_tac 1);
    21 qed"acc_prefix_Nil";
    22 Addsimps [acc_prefix_Nil];
    23 
    24 goalw Auto.thy [acc_prefix_def]
    25  "acc_prefix A s (x#xs) = (fin A (next A s x) | acc_prefix A (next A s x) xs)";
    26 by(simp_tac (!simpset addsimps [prefix_Cons]) 1);
    27 by(safe_tac (!claset));
    28   by(Asm_full_simp_tac 1);
    29   by (case_tac "zs=[]" 1);
    30    by(hyp_subst_tac 1);
    31    by(Asm_full_simp_tac 1);
    32   by(Fast_tac 1);
    33  by(res_inst_tac [("x","[x]")] exI 1);
    34  by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    35 by(res_inst_tac [("x","x#us")] exI 1);
    36 by(Asm_simp_tac 1);
    37 qed"acc_prefix_Cons";
    38 Addsimps [acc_prefix_Cons];