src/HOL/Lex/Auto.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2056 93c093620c28
child 4089 96fba19bcbe2
permissions -rw-r--r--
Dep. on Provers/nat_transitive
clasohm@1465
     1
(*  Title:      HOL/Lex/Auto.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
nipkow@1344
     7
open Auto;
nipkow@1344
     8
nipkow@1344
     9
goalw Auto.thy [nexts_def] "nexts A st [] = st";
nipkow@1344
    10
by(Simp_tac 1);
nipkow@1344
    11
qed"nexts_Nil";
nipkow@1344
    12
nipkow@1344
    13
goalw Auto.thy [nexts_def] "nexts A st (x#xs) = nexts A (next A st x) xs";
nipkow@1344
    14
by(Simp_tac 1);
nipkow@1344
    15
qed"nexts_Cons";
nipkow@1344
    16
nipkow@1344
    17
Addsimps [nexts_Nil,nexts_Cons];
nipkow@1344
    18
nipkow@1344
    19
goalw Auto.thy [acc_prefix_def] "~acc_prefix A st []";
nipkow@1344
    20
by(Simp_tac 1);
nipkow@1344
    21
qed"acc_prefix_Nil";
nipkow@1344
    22
Addsimps [acc_prefix_Nil];
nipkow@1344
    23
nipkow@1344
    24
goalw Auto.thy [acc_prefix_def]
nipkow@1344
    25
 "acc_prefix A s (x#xs) = (fin A (next A s x) | acc_prefix A (next A s x) xs)";
nipkow@1344
    26
by(simp_tac (!simpset addsimps [prefix_Cons]) 1);
berghofe@1894
    27
by(safe_tac (!claset));
nipkow@1344
    28
  by(Asm_full_simp_tac 1);
nipkow@1344
    29
  by (case_tac "zs=[]" 1);
nipkow@1344
    30
   by(hyp_subst_tac 1);
nipkow@1344
    31
   by(Asm_full_simp_tac 1);
paulson@1985
    32
  by(Fast_tac 1);
nipkow@1344
    33
 by(res_inst_tac [("x","[x]")] exI 1);
nipkow@1344
    34
 by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
nipkow@1344
    35
by(res_inst_tac [("x","x#us")] exI 1);
nipkow@1344
    36
by(Asm_simp_tac 1);
nipkow@1344
    37
qed"acc_prefix_Cons";
nipkow@1344
    38
Addsimps [acc_prefix_Cons];