src/HOL/Lex/Auto.ML
author clasohm
Tue Jan 30 15:24:36 1996 +0100 (1996-01-30)
changeset 1465 5d7a7e439cec
parent 1344 f172a7f14e49
child 1894 c2c8279d40f0
permissions -rw-r--r--
expanded tabs
     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 HOL_cs);
    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 (HOL_cs 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 HOL_cs 1);
    38 qed"acc_prefix_Cons";
    39 Addsimps [acc_prefix_Cons];