author | nipkow |
Fri, 27 Nov 1998 17:00:30 +0100 | |
changeset 5983 | 79e301a6a51b |
parent 5625 | 77e9ab9cd7b1 |
child 8423 | 3c19160b6432 |
permissions | -rw-r--r-- |
4832 | 1 |
(* Title: HOL/Lex/RegSet_of_nat_DA.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1998 TUM |
|
5 |
*) |
|
6 |
||
5458
0e26af5975ba
in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
paulson
parents:
5184
diff
changeset
|
7 |
Addsimps [in_set_butlast_appendI]; |
0e26af5975ba
in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
paulson
parents:
5184
diff
changeset
|
8 |
AddIs [in_set_butlast_appendI]; |
4832 | 9 |
Addsimps [image_eqI]; |
10 |
||
11 |
(* Lists *) |
|
12 |
||
5069 | 13 |
Goal "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])"; |
4832 | 14 |
by (exhaust_tac "xs" 1); |
15 |
by (ALLGOALS Asm_simp_tac); |
|
16 |
qed "butlast_empty"; |
|
17 |
AddIffs [butlast_empty]; |
|
18 |
||
5069 | 19 |
Goal "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))"; |
4832 | 20 |
by (induct_tac "xss" 1); |
21 |
by (Simp_tac 1); |
|
22 |
by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps) 1); |
|
23 |
by (rtac conjI 1); |
|
24 |
by (Clarify_tac 1); |
|
25 |
by (rtac conjI 1); |
|
26 |
by (Blast_tac 1); |
|
27 |
by (Clarify_tac 1); |
|
28 |
by (subgoal_tac "xs=[]" 1); |
|
29 |
by (rotate_tac ~1 1); |
|
30 |
by (Asm_full_simp_tac 1); |
|
31 |
by (Blast_tac 1); |
|
32 |
by (blast_tac (claset() addDs [in_set_butlastD]) 1); |
|
33 |
qed_spec_mp "in_set_butlast_concatI"; |
|
34 |
||
35 |
(* Regular sets *) |
|
36 |
||
37 |
(* The main lemma: |
|
38 |
how to decompose a trace into a prefix, a list of loops and a suffix. |
|
39 |
*) |
|
5069 | 40 |
Goal "!i. k : set(trace d i xs) --> (? pref mids suf. \ |
4832 | 41 |
\ xs = pref @ concat mids @ suf & \ |
42 |
\ deltas d pref i = k & (!n:set(butlast(trace d i pref)). n ~= k) & \ |
|
43 |
\ (!mid:set mids. (deltas d mid k = k) & \ |
|
44 |
\ (!n:set(butlast(trace d k mid)). n ~= k)) & \ |
|
45 |
\ (!n:set(butlast(trace d k suf)). n ~= k))"; |
|
46 |
by (induct_tac "xs" 1); |
|
47 |
by (Simp_tac 1); |
|
48 |
by (rename_tac "a as" 1); |
|
49 |
by (rtac allI 1); |
|
50 |
by (case_tac "d a i = k" 1); |
|
51 |
by (strip_tac 1); |
|
52 |
by (res_inst_tac[("x","[a]")]exI 1); |
|
53 |
by (Asm_full_simp_tac 1); |
|
54 |
by (case_tac "k : set(trace d (d a i) as)" 1); |
|
55 |
by (etac allE 1); |
|
56 |
by (etac impE 1); |
|
57 |
by (assume_tac 1); |
|
58 |
by (REPEAT(etac exE 1)); |
|
59 |
by (res_inst_tac[("x","pref#mids")]exI 1); |
|
60 |
by (res_inst_tac[("x","suf")]exI 1); |
|
61 |
by (Asm_full_simp_tac 1); |
|
62 |
by (res_inst_tac[("x","[]")]exI 1); |
|
63 |
by (res_inst_tac[("x","as")]exI 1); |
|
64 |
by (Asm_full_simp_tac 1); |
|
65 |
by (blast_tac (claset() addDs [in_set_butlastD]) 1); |
|
66 |
by (Asm_simp_tac 1); |
|
67 |
by (rtac conjI 1); |
|
68 |
by (Blast_tac 1); |
|
69 |
by (strip_tac 1); |
|
70 |
by (etac allE 1); |
|
71 |
by (etac impE 1); |
|
72 |
by (assume_tac 1); |
|
73 |
by (REPEAT(etac exE 1)); |
|
74 |
by (res_inst_tac[("x","a#pref")]exI 1); |
|
75 |
by (res_inst_tac[("x","mids")]exI 1); |
|
76 |
by (res_inst_tac[("x","suf")]exI 1); |
|
77 |
by (Asm_simp_tac 1); |
|
78 |
qed_spec_mp "decompose"; |
|
79 |
||
5069 | 80 |
Goal "!i. length(trace d i xs) = length xs"; |
4832 | 81 |
by (induct_tac "xs" 1); |
82 |
by (ALLGOALS Asm_simp_tac); |
|
83 |
qed "length_trace"; |
|
84 |
Addsimps [length_trace]; |
|
85 |
||
5069 | 86 |
Goal "!i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)"; |
4832 | 87 |
by (induct_tac "xs" 1); |
88 |
by (ALLGOALS Asm_simp_tac); |
|
89 |
qed "deltas_append"; |
|
90 |
Addsimps [deltas_append]; |
|
91 |
||
5069 | 92 |
Goal "!i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys"; |
4832 | 93 |
by (induct_tac "xs" 1); |
94 |
by (ALLGOALS Asm_simp_tac); |
|
95 |
qed "trace_append"; |
|
96 |
Addsimps [trace_append]; |
|
97 |
||
5069 | 98 |
Goal "(!xs: set xss. deltas d xs i = i) --> \ |
4832 | 99 |
\ trace d i (concat xss) = concat (map (trace d i) xss)"; |
100 |
by (induct_tac "xss" 1); |
|
101 |
by (ALLGOALS Asm_simp_tac); |
|
102 |
qed_spec_mp "trace_concat"; |
|
103 |
Addsimps [trace_concat]; |
|
104 |
||
5069 | 105 |
Goal "!i. (trace d i xs = []) = (xs = [])"; |
4832 | 106 |
by (exhaust_tac "xs" 1); |
107 |
by (ALLGOALS Asm_simp_tac); |
|
108 |
qed "trace_is_Nil"; |
|
109 |
Addsimps [trace_is_Nil]; |
|
110 |
||
5069 | 111 |
Goal "(trace d i xs = n#ns) = \ |
4832 | 112 |
\ (case xs of [] => False | y#ys => n = d y i & ns = trace d n ys)"; |
113 |
by (exhaust_tac "xs" 1); |
|
114 |
by (ALLGOALS Asm_simp_tac); |
|
115 |
by (Blast_tac 1); |
|
116 |
qed_spec_mp "trace_is_Cons_conv"; |
|
117 |
Addsimps [trace_is_Cons_conv]; |
|
118 |
||
5069 | 119 |
Goal "!i. set(trace d i xs) = \ |
4832 | 120 |
\ (if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))"; |
121 |
by (induct_tac "xs" 1); |
|
122 |
by (Simp_tac 1); |
|
123 |
by (asm_simp_tac (simpset() addsimps [insert_commute]) 1); |
|
124 |
qed "set_trace_conv"; |
|
125 |
||
5069 | 126 |
Goal |
4832 | 127 |
"(!mid:set mids. deltas d mid k = k) --> deltas d (concat mids) k = k"; |
128 |
by (induct_tac "mids" 1); |
|
129 |
by (ALLGOALS Asm_simp_tac); |
|
130 |
qed_spec_mp "deltas_concat"; |
|
131 |
Addsimps [deltas_concat]; |
|
132 |
||
5983 | 133 |
goal Arith.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k"; |
5625 | 134 |
by (etac linorder_neqE 1); |
5983 | 135 |
by (ALLGOALS Simp_tac); |
4832 | 136 |
val lemma = result(); |
137 |
||
5069 | 138 |
Goal |
4832 | 139 |
"!i j xs. xs : regset d i j k = \ |
140 |
\ ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)"; |
|
141 |
by (induct_tac "k" 1); |
|
5184 | 142 |
by (simp_tac (simpset() addcongs [conj_cong] addsplits [list.split]) 1); |
4832 | 143 |
by (strip_tac 1); |
144 |
by (asm_simp_tac (simpset() addsimps [conc_def]) 1); |
|
145 |
by (rtac iffI 1); |
|
146 |
by (etac disjE 1); |
|
147 |
by (Asm_simp_tac 1); |
|
148 |
by (REPEAT(eresolve_tac[exE,conjE] 1)); |
|
149 |
by (Asm_full_simp_tac 1); |
|
150 |
by (subgoal_tac |
|
5184 | 151 |
"(!m:set(butlast(trace d n xsb)). m < Suc n) & deltas d xsb n = n" 1); |
4832 | 152 |
by (asm_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1); |
153 |
by (etac star.induct 1); |
|
154 |
by (Simp_tac 1); |
|
155 |
by (asm_full_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1); |
|
5184 | 156 |
by (case_tac "n : set(butlast(trace d i xs))" 1); |
4832 | 157 |
by (rtac disjI1 2); |
158 |
by (blast_tac (claset() addIs [lemma]) 2); |
|
159 |
by (rtac disjI2 1); |
|
160 |
by (dtac (in_set_butlastD RS decompose) 1); |
|
161 |
by (Clarify_tac 1); |
|
162 |
by (res_inst_tac [("x","pref")] exI 1); |
|
163 |
by (Asm_full_simp_tac 1); |
|
164 |
by (rtac conjI 1); |
|
165 |
by (rtac ballI 1); |
|
166 |
by (rtac lemma 1); |
|
167 |
by (Asm_simp_tac 2); |
|
168 |
by (EVERY[dtac bspec 1, atac 2]); |
|
169 |
by (Asm_simp_tac 1); |
|
170 |
by (res_inst_tac [("x","concat mids")] exI 1); |
|
171 |
by (Simp_tac 1); |
|
172 |
by (rtac conjI 1); |
|
173 |
by (rtac concat_in_star 1); |
|
174 |
by (Asm_simp_tac 1); |
|
175 |
by (rtac ballI 1); |
|
176 |
by (rtac ballI 1); |
|
177 |
by (rtac lemma 1); |
|
178 |
by (Asm_simp_tac 2); |
|
179 |
by (EVERY[dtac bspec 1, atac 2]); |
|
180 |
by (asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1); |
|
181 |
by (rtac ballI 1); |
|
182 |
by (rtac lemma 1); |
|
5521 | 183 |
by (Auto_tac); |
4832 | 184 |
qed_spec_mp "regset_spec"; |
185 |
||
5069 | 186 |
Goalw [bounded_def] |
5118 | 187 |
"bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)"; |
4832 | 188 |
by (induct_tac "xs" 1); |
189 |
by (ALLGOALS Simp_tac); |
|
190 |
by (Blast_tac 1); |
|
191 |
qed_spec_mp "trace_below"; |
|
192 |
||
5118 | 193 |
Goal "[| bounded d k; i < k; j < k |] ==> \ |
194 |
\ regset d i j k = {xs. deltas d xs i = j}"; |
|
4832 | 195 |
by (rtac set_ext 1); |
196 |
by (simp_tac (simpset() addsimps [regset_spec]) 1); |
|
197 |
by (blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1); |
|
198 |
qed "regset_below"; |
|
199 |
||
5069 | 200 |
Goalw [bounded_def] |
5118 | 201 |
"bounded d k ==> !i. i < k --> deltas d w i < k"; |
4832 | 202 |
by (induct_tac "w" 1); |
203 |
by (ALLGOALS Simp_tac); |
|
204 |
by (Blast_tac 1); |
|
205 |
qed_spec_mp "deltas_below"; |
|
206 |
||
5069 | 207 |
Goalw [regset_of_DA_def] |
5118 | 208 |
"[| bounded (next A) k; start A < k; j < k |] ==> \ |
209 |
\ w : regset_of_DA A k = accepts A w"; |
|
5132 | 210 |
by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps |
4832 | 211 |
[regset_below,deltas_below,accepts_def,delta_def]) 1); |
212 |
qed "regset_DA_equiv"; |