4832
|
1 |
(* Title: HOL/Lex/RegSet_of_nat_DA.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1998 TUM
|
|
5 |
|
|
6 |
Conversion of deterministic automata into regular sets.
|
|
7 |
|
|
8 |
To generate a regual expression, the alphabet must be finite.
|
|
9 |
regexp needs to be supplied with an 'a list for a unique order
|
|
10 |
|
|
11 |
add_Atom d i j r a = (if d a i = j then Union r (Atom a) else r)
|
|
12 |
atoms d i j as = foldl (add_Atom d i j) Empty as
|
|
13 |
|
|
14 |
regexp as d i j 0 = (if i=j then Union (Star Empty) (atoms d i j as)
|
|
15 |
else atoms d i j as
|
|
16 |
*)
|
|
17 |
|
14431
|
18 |
theory RegSet_of_nat_DA = RegSet + DA:
|
4832
|
19 |
|
|
20 |
types 'a nat_next = "'a => nat => nat"
|
|
21 |
|
14431
|
22 |
syntax deltas :: "'a nat_next => 'a list => nat => nat"
|
4832
|
23 |
translations "deltas" == "foldl2"
|
|
24 |
|
14431
|
25 |
consts trace :: "'a nat_next => nat => 'a list => nat list"
|
5184
|
26 |
primrec
|
4832
|
27 |
"trace d i [] = []"
|
|
28 |
"trace d i (x#xs) = d x i # trace d (d x i) xs"
|
|
29 |
|
|
30 |
(* conversion a la Warshall *)
|
|
31 |
|
14431
|
32 |
consts regset :: "'a nat_next => nat => nat => nat => 'a list set"
|
5184
|
33 |
primrec
|
4832
|
34 |
"regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j}
|
|
35 |
else {[a] | a. d a i = j})"
|
|
36 |
"regset d i j (Suc k) = regset d i j k Un
|
|
37 |
conc (regset d i k k)
|
|
38 |
(conc (star(regset d k k k))
|
|
39 |
(regset d k j k))"
|
|
40 |
|
|
41 |
constdefs
|
14431
|
42 |
regset_of_DA :: "('a,nat)da => nat => 'a list set"
|
4832
|
43 |
"regset_of_DA A k == UN j:{j. j<k & fin A j}. regset (next A) (start A) j k"
|
|
44 |
|
|
45 |
bounded :: "'a => nat => bool"
|
|
46 |
"bounded d k == !n. n < k --> (!x. d x n < k)"
|
|
47 |
|
14431
|
48 |
declare
|
|
49 |
in_set_butlast_appendI[simp,intro] less_SucI[simp] image_eqI[simp]
|
|
50 |
|
|
51 |
(* Lists *)
|
|
52 |
|
|
53 |
lemma butlast_empty[iff]:
|
|
54 |
"(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])"
|
|
55 |
by (case_tac "xs") simp_all
|
|
56 |
|
|
57 |
lemma in_set_butlast_concatI:
|
|
58 |
"x:set(butlast xs) ==> xs:set xss ==> x:set(butlast(concat xss))"
|
|
59 |
apply (induct "xss")
|
|
60 |
apply simp
|
|
61 |
apply (simp add: butlast_append del: ball_simps)
|
|
62 |
apply (rule conjI)
|
|
63 |
apply (clarify)
|
|
64 |
apply (erule disjE)
|
|
65 |
apply (blast)
|
|
66 |
apply (subgoal_tac "xs=[]")
|
|
67 |
apply simp
|
|
68 |
apply (blast)
|
|
69 |
apply (blast dest: in_set_butlastD)
|
|
70 |
done
|
|
71 |
|
|
72 |
(* Regular sets *)
|
|
73 |
|
|
74 |
(* The main lemma:
|
|
75 |
how to decompose a trace into a prefix, a list of loops and a suffix.
|
|
76 |
*)
|
|
77 |
lemma decompose[rule_format]:
|
|
78 |
"!i. k : set(trace d i xs) --> (EX pref mids suf.
|
|
79 |
xs = pref @ concat mids @ suf &
|
|
80 |
deltas d pref i = k & (!n:set(butlast(trace d i pref)). n ~= k) &
|
|
81 |
(!mid:set mids. (deltas d mid k = k) &
|
|
82 |
(!n:set(butlast(trace d k mid)). n ~= k)) &
|
|
83 |
(!n:set(butlast(trace d k suf)). n ~= k))"
|
|
84 |
apply (induct "xs")
|
|
85 |
apply (simp)
|
|
86 |
apply (rename_tac a as)
|
|
87 |
apply (intro strip)
|
|
88 |
apply (case_tac "d a i = k")
|
|
89 |
apply (rule_tac x = "[a]" in exI)
|
|
90 |
apply simp
|
|
91 |
apply (case_tac "k : set(trace d (d a i) as)")
|
|
92 |
apply (erule allE)
|
|
93 |
apply (erule impE)
|
|
94 |
apply (assumption)
|
|
95 |
apply (erule exE)+
|
|
96 |
apply (rule_tac x = "pref#mids" in exI)
|
|
97 |
apply (rule_tac x = "suf" in exI)
|
|
98 |
apply simp
|
|
99 |
apply (rule_tac x = "[]" in exI)
|
|
100 |
apply (rule_tac x = "as" in exI)
|
|
101 |
apply simp
|
|
102 |
apply (blast dest: in_set_butlastD)
|
|
103 |
apply simp
|
|
104 |
apply (erule allE)
|
|
105 |
apply (erule impE)
|
|
106 |
apply (assumption)
|
|
107 |
apply (erule exE)+
|
|
108 |
apply (rule_tac x = "a#pref" in exI)
|
|
109 |
apply (rule_tac x = "mids" in exI)
|
|
110 |
apply (rule_tac x = "suf" in exI)
|
|
111 |
apply simp
|
|
112 |
done
|
|
113 |
|
|
114 |
lemma length_trace[simp]: "!!i. length(trace d i xs) = length xs"
|
|
115 |
by (induct "xs") simp_all
|
|
116 |
|
|
117 |
lemma deltas_append[simp]:
|
|
118 |
"!!i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)"
|
|
119 |
by (induct "xs") simp_all
|
|
120 |
|
|
121 |
lemma trace_append[simp]:
|
|
122 |
"!!i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys"
|
|
123 |
by (induct "xs") simp_all
|
|
124 |
|
|
125 |
lemma trace_concat[simp]:
|
|
126 |
"(!xs: set xss. deltas d xs i = i) ==>
|
|
127 |
trace d i (concat xss) = concat (map (trace d i) xss)"
|
|
128 |
by (induct "xss") simp_all
|
|
129 |
|
|
130 |
lemma trace_is_Nil[simp]: "!!i. (trace d i xs = []) = (xs = [])"
|
|
131 |
by (case_tac "xs") simp_all
|
|
132 |
|
|
133 |
lemma trace_is_Cons_conv[simp]:
|
|
134 |
"(trace d i xs = n#ns) =
|
|
135 |
(case xs of [] => False | y#ys => n = d y i & ns = trace d n ys)"
|
|
136 |
apply (case_tac "xs")
|
|
137 |
apply simp_all
|
|
138 |
apply (blast)
|
|
139 |
done
|
|
140 |
|
|
141 |
lemma set_trace_conv:
|
|
142 |
"!!i. set(trace d i xs) =
|
|
143 |
(if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))"
|
|
144 |
apply (induct "xs")
|
|
145 |
apply (simp)
|
|
146 |
apply (simp add: insert_commute)
|
|
147 |
done
|
|
148 |
|
|
149 |
lemma deltas_concat[simp]:
|
|
150 |
"(!mid:set mids. deltas d mid k = k) ==> deltas d (concat mids) k = k"
|
|
151 |
by (induct mids) simp_all
|
|
152 |
|
|
153 |
lemma lem: "[| n < Suc k; n ~= k |] ==> n < k"
|
|
154 |
by arith
|
|
155 |
|
|
156 |
lemma regset_spec:
|
|
157 |
"!!i j xs. xs : regset d i j k =
|
|
158 |
((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)"
|
|
159 |
apply (induct k)
|
|
160 |
apply(simp split: list.split)
|
|
161 |
apply(fastsimp)
|
|
162 |
apply (simp add: conc_def)
|
|
163 |
apply (rule iffI)
|
|
164 |
apply (erule disjE)
|
|
165 |
apply simp
|
|
166 |
apply (erule exE conjE)+
|
|
167 |
apply simp
|
|
168 |
apply (subgoal_tac
|
|
169 |
"(!m:set(butlast(trace d n xsb)). m < Suc n) & deltas d xsb n = n")
|
|
170 |
apply (simp add: set_trace_conv butlast_append ball_Un)
|
|
171 |
apply (erule star.induct)
|
|
172 |
apply (simp)
|
|
173 |
apply (simp add: set_trace_conv butlast_append ball_Un)
|
|
174 |
apply (case_tac "n : set(butlast(trace d i xs))")
|
|
175 |
prefer 2 apply (rule disjI1)
|
|
176 |
apply (blast intro:lem)
|
|
177 |
apply (rule disjI2)
|
|
178 |
apply (drule in_set_butlastD[THEN decompose])
|
|
179 |
apply (clarify)
|
|
180 |
apply (rule_tac x = "pref" in exI)
|
|
181 |
apply simp
|
|
182 |
apply (rule conjI)
|
|
183 |
apply (rule ballI)
|
|
184 |
apply (rule lem)
|
|
185 |
prefer 2 apply simp
|
|
186 |
apply (drule bspec) prefer 2 apply assumption
|
|
187 |
apply simp
|
|
188 |
apply (rule_tac x = "concat mids" in exI)
|
|
189 |
apply (simp)
|
|
190 |
apply (rule conjI)
|
|
191 |
apply (rule concat_in_star)
|
|
192 |
apply simp
|
|
193 |
apply (rule ballI)
|
|
194 |
apply (rule ballI)
|
|
195 |
apply (rule lem)
|
|
196 |
prefer 2 apply simp
|
|
197 |
apply (drule bspec) prefer 2 apply assumption
|
|
198 |
apply (simp add: image_eqI in_set_butlast_concatI)
|
|
199 |
apply (rule ballI)
|
|
200 |
apply (rule lem)
|
|
201 |
apply auto
|
|
202 |
done
|
|
203 |
|
|
204 |
lemma trace_below:
|
|
205 |
"bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)"
|
|
206 |
apply (unfold bounded_def)
|
|
207 |
apply (induct "xs")
|
|
208 |
apply simp
|
|
209 |
apply (simp (no_asm))
|
|
210 |
apply (blast)
|
|
211 |
done
|
|
212 |
|
|
213 |
lemma regset_below:
|
|
214 |
"[| bounded d k; i < k; j < k |] ==>
|
|
215 |
regset d i j k = {xs. deltas d xs i = j}"
|
|
216 |
apply (rule set_ext)
|
|
217 |
apply (simp add: regset_spec)
|
|
218 |
apply (blast dest: trace_below in_set_butlastD)
|
|
219 |
done
|
|
220 |
|
|
221 |
lemma deltas_below:
|
|
222 |
"!!i. bounded d k ==> i < k ==> deltas d w i < k"
|
|
223 |
apply (unfold bounded_def)
|
|
224 |
apply (induct "w")
|
|
225 |
apply simp_all
|
|
226 |
done
|
|
227 |
|
|
228 |
lemma regset_DA_equiv:
|
|
229 |
"[| bounded (next A) k; start A < k; j < k |] ==> \
|
|
230 |
\ w : regset_of_DA A k = accepts A w"
|
|
231 |
apply(unfold regset_of_DA_def)
|
|
232 |
apply (simp cong: conj_cong
|
|
233 |
add: regset_below deltas_below accepts_def delta_def)
|
|
234 |
done
|
|
235 |
|
4832
|
236 |
end
|