src/HOL/Lex/NA.ML
changeset 5323 028e00595280
child 6301 08245f5a436d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Lex/NA.ML	Mon Aug 17 11:00:57 1998 +0200
     1.3 @@ -0,0 +1,29 @@
     1.4 +(*  Title:      HOL/Lex/NA.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   1998 TUM
     1.8 +*)
     1.9 +
    1.10 +Goal
    1.11 + "steps A (v@w) = steps A w  O  steps A v";
    1.12 +by (induct_tac "v" 1);
    1.13 +by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
    1.14 +qed "steps_append";
    1.15 +Addsimps [steps_append];
    1.16 +
    1.17 +Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
    1.18 +by(rtac (steps_append RS equalityE) 1);
    1.19 +by(Blast_tac 1);
    1.20 +qed "in_steps_append";
    1.21 +AddIffs [in_steps_append];
    1.22 +
    1.23 +Goal
    1.24 + "!p. delta A w p = {q. (p,q) : steps A w}";
    1.25 +by(induct_tac "w" 1);
    1.26 +by(auto_tac (claset(), simpset() addsimps [step_def]));
    1.27 +qed_spec_mp "delta_conv_steps";
    1.28 +
    1.29 +Goalw [accepts_def]
    1.30 + "accepts A w = (? q. (start A,q) : steps A w & fin A q)";
    1.31 +by(simp_tac (simpset() addsimps [delta_conv_steps]) 1);
    1.32 +qed "accepts_conv_steps";