src/HOL/Lex/Auto.ML
author berghofe
Tue Jul 30 17:33:26 1996 +0200 (1996-07-30)
changeset 1894 c2c8279d40f0
parent 1465 5d7a7e439cec
child 1985 84cf16192e03
permissions -rw-r--r--
Classical tactics now use default claset.
     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 (!claset addSEs [Cons_neq_Nil]) 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 by (Fast_tac 1);
    38 qed"acc_prefix_Cons";
    39 Addsimps [acc_prefix_Cons];