src/HOL/Lex/RegExp2NA.ML
changeset 11379 0c90ffd3f3e2
parent 8442 96023903c2df
child 12487 bbd564190c9b
     1.1 --- a/src/HOL/Lex/RegExp2NA.ML	Mon Jun 25 15:36:55 2001 +0200
     1.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Tue Jun 26 15:28:49 2001 +0200
     1.3 @@ -346,31 +346,6 @@
     1.4  Goal
     1.5   "!r. (start A,r) : steps (plus A) w --> \
     1.6  \     (? us v. w = concat us @ v & \
     1.7 -\              (!u:set us. u ~= [] & accepts A u) & \
     1.8 -\              (start A,r) : steps A v)";
     1.9 -by (rev_induct_tac "w" 1);
    1.10 - by (Simp_tac 1);
    1.11 - by (res_inst_tac [("x","[]")] exI 1);
    1.12 - by (Simp_tac 1);
    1.13 -by (Simp_tac 1);
    1.14 -by (Clarify_tac 1);
    1.15 -by (etac allE 1 THEN mp_tac 1);
    1.16 -by (Clarify_tac 1);
    1.17 -by (etac disjE 1);
    1.18 - by (res_inst_tac [("x","us")] exI 1);
    1.19 - by (Asm_simp_tac 1);
    1.20 - by (Blast_tac 1);
    1.21 -by (case_tac "v" 1);
    1.22 - by (res_inst_tac [("x","us")] exI 1);
    1.23 - by (Asm_full_simp_tac 1);
    1.24 -by (res_inst_tac [("x","us@[v]")] exI 1);
    1.25 -by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
    1.26 -by (Blast_tac 1);
    1.27 -qed_spec_mp "start_steps_plusD";
    1.28 -
    1.29 -Goal
    1.30 - "!r. (start A,r) : steps (plus A) w --> \
    1.31 -\     (? us v. w = concat us @ v & \
    1.32  \              (!u:set us. accepts A u) & \
    1.33  \              (start A,r) : steps A v)";
    1.34  by (rev_induct_tac "w" 1);