|
4832
|
1 |
(* Title: HOL/Lex/RegSet.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1998 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
AddIffs [star.NilI];
|
|
|
8 |
Addsimps [star.ConsI];
|
|
|
9 |
AddIs [star.ConsI];
|
|
|
10 |
|
|
5069
|
11 |
Goal "(!xs: set xss. xs:S) --> concat xss : star S";
|
|
4832
|
12 |
by (induct_tac "xss" 1);
|
|
|
13 |
by (ALLGOALS Asm_full_simp_tac);
|
|
|
14 |
qed_spec_mp "concat_in_star";
|
|
|
15 |
|
|
5069
|
16 |
Goal
|
|
4832
|
17 |
"w : star U = (? us. (!u : set(us). u : U) & (w = concat us))";
|
|
5132
|
18 |
by (rtac iffI 1);
|
|
6162
|
19 |
by (etac star.induct 1);
|
|
4832
|
20 |
by (res_inst_tac [("x","[]")] exI 1);
|
|
|
21 |
by (Simp_tac 1);
|
|
|
22 |
by (Clarify_tac 1);
|
|
|
23 |
by (res_inst_tac [("x","a#us")] exI 1);
|
|
|
24 |
by (Asm_simp_tac 1);
|
|
|
25 |
by (Clarify_tac 1);
|
|
|
26 |
by (asm_simp_tac (simpset() addsimps [concat_in_star]) 1);
|
|
|
27 |
qed "in_star";
|