|
4832
|
1 |
(* Title: HOL/Lex/RegSet.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1998 TUM
|
|
|
5 |
|
|
|
6 |
Regular sets
|
|
|
7 |
*)
|
|
|
8 |
|
|
14431
|
9 |
theory RegSet = Main:
|
|
4832
|
10 |
|
|
|
11 |
constdefs
|
|
14431
|
12 |
conc :: "'a list set => 'a list set => 'a list set"
|
|
4832
|
13 |
"conc A B == {xs@ys | xs ys. xs:A & ys:B}"
|
|
|
14 |
|
|
14431
|
15 |
consts star :: "'a list set => 'a list set"
|
|
4832
|
16 |
inductive "star A"
|
|
14431
|
17 |
intros
|
|
|
18 |
NilI[iff]: "[] : star A"
|
|
|
19 |
ConsI[intro,simp]: "[| a:A; as : star A |] ==> a@as : star A"
|
|
|
20 |
|
|
|
21 |
lemma concat_in_star: "!xs: set xss. xs:S ==> concat xss : star S"
|
|
|
22 |
by (induct "xss") simp_all
|
|
|
23 |
|
|
|
24 |
lemma in_star:
|
|
|
25 |
"w : star U = (? us. (!u : set(us). u : U) & (w = concat us))"
|
|
|
26 |
apply (rule iffI)
|
|
|
27 |
apply (erule star.induct)
|
|
|
28 |
apply (rule_tac x = "[]" in exI)
|
|
|
29 |
apply simp
|
|
|
30 |
apply clarify
|
|
|
31 |
apply (rule_tac x = "a#us" in exI)
|
|
|
32 |
apply simp
|
|
|
33 |
apply clarify
|
|
|
34 |
apply (simp add: concat_in_star)
|
|
|
35 |
done
|
|
4832
|
36 |
|
|
|
37 |
end
|