author | berghofe |
Mon, 30 Sep 2002 16:14:02 +0200 | |
changeset 13601 | fd3e3d6b37b2 |
parent 13187 | e5434b822a96 |
child 14401 | 477380c74c1d |
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 |
||
8741
61bc5ed22b62
removal of less_SucI, le_SucI from default simpset
paulson
parents:
8442
diff
changeset
|
7 |
Addsimps [in_set_butlast_appendI, less_SucI]; |
5458
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=[])"; |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
14 |
by (case_tac "xs" 1); |
4832 | 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 (Asm_full_simp_tac 1); |
|
30 |
by (Blast_tac 1); |
|
31 |
by (blast_tac (claset() addDs [in_set_butlastD]) 1); |
|
32 |
qed_spec_mp "in_set_butlast_concatI"; |
|
33 |
||
34 |
(* Regular sets *) |
|
35 |
||
36 |
(* The main lemma: |
|
37 |
how to decompose a trace into a prefix, a list of loops and a suffix. |
|
38 |
*) |
|
5069 | 39 |
Goal "!i. k : set(trace d i xs) --> (? pref mids suf. \ |
4832 | 40 |
\ xs = pref @ concat mids @ suf & \ |
41 |
\ deltas d pref i = k & (!n:set(butlast(trace d i pref)). n ~= k) & \ |
|
42 |
\ (!mid:set mids. (deltas d mid k = k) & \ |
|
43 |
\ (!n:set(butlast(trace d k mid)). n ~= k)) & \ |
|
44 |
\ (!n:set(butlast(trace d k suf)). n ~= k))"; |
|
45 |
by (induct_tac "xs" 1); |
|
46 |
by (Simp_tac 1); |
|
47 |
by (rename_tac "a as" 1); |
|
48 |
by (rtac allI 1); |
|
49 |
by (case_tac "d a i = k" 1); |
|
50 |
by (strip_tac 1); |
|
51 |
by (res_inst_tac[("x","[a]")]exI 1); |
|
52 |
by (Asm_full_simp_tac 1); |
|
53 |
by (case_tac "k : set(trace d (d a i) as)" 1); |
|
54 |
by (etac allE 1); |
|
55 |
by (etac impE 1); |
|
56 |
by (assume_tac 1); |
|
57 |
by (REPEAT(etac exE 1)); |
|
58 |
by (res_inst_tac[("x","pref#mids")]exI 1); |
|
59 |
by (res_inst_tac[("x","suf")]exI 1); |
|
60 |
by (Asm_full_simp_tac 1); |
|
61 |
by (res_inst_tac[("x","[]")]exI 1); |
|
62 |
by (res_inst_tac[("x","as")]exI 1); |
|
63 |
by (Asm_full_simp_tac 1); |
|
64 |
by (blast_tac (claset() addDs [in_set_butlastD]) 1); |
|
65 |
by (Asm_simp_tac 1); |
|
66 |
by (strip_tac 1); |
|
67 |
by (etac allE 1); |
|
68 |
by (etac impE 1); |
|
69 |
by (assume_tac 1); |
|
70 |
by (REPEAT(etac exE 1)); |
|
71 |
by (res_inst_tac[("x","a#pref")]exI 1); |
|
72 |
by (res_inst_tac[("x","mids")]exI 1); |
|
73 |
by (res_inst_tac[("x","suf")]exI 1); |
|
74 |
by (Asm_simp_tac 1); |
|
75 |
qed_spec_mp "decompose"; |
|
76 |
||
5069 | 77 |
Goal "!i. length(trace d i xs) = length xs"; |
4832 | 78 |
by (induct_tac "xs" 1); |
79 |
by (ALLGOALS Asm_simp_tac); |
|
80 |
qed "length_trace"; |
|
81 |
Addsimps [length_trace]; |
|
82 |
||
5069 | 83 |
Goal "!i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)"; |
4832 | 84 |
by (induct_tac "xs" 1); |
85 |
by (ALLGOALS Asm_simp_tac); |
|
86 |
qed "deltas_append"; |
|
87 |
Addsimps [deltas_append]; |
|
88 |
||
5069 | 89 |
Goal "!i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys"; |
4832 | 90 |
by (induct_tac "xs" 1); |
91 |
by (ALLGOALS Asm_simp_tac); |
|
92 |
qed "trace_append"; |
|
93 |
Addsimps [trace_append]; |
|
94 |
||
5069 | 95 |
Goal "(!xs: set xss. deltas d xs i = i) --> \ |
4832 | 96 |
\ trace d i (concat xss) = concat (map (trace d i) xss)"; |
97 |
by (induct_tac "xss" 1); |
|
98 |
by (ALLGOALS Asm_simp_tac); |
|
99 |
qed_spec_mp "trace_concat"; |
|
100 |
Addsimps [trace_concat]; |
|
101 |
||
5069 | 102 |
Goal "!i. (trace d i xs = []) = (xs = [])"; |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
103 |
by (case_tac "xs" 1); |
4832 | 104 |
by (ALLGOALS Asm_simp_tac); |
105 |
qed "trace_is_Nil"; |
|
106 |
Addsimps [trace_is_Nil]; |
|
107 |
||
5069 | 108 |
Goal "(trace d i xs = n#ns) = \ |
4832 | 109 |
\ (case xs of [] => False | y#ys => n = d y i & ns = trace d n ys)"; |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
110 |
by (case_tac "xs" 1); |
4832 | 111 |
by (ALLGOALS Asm_simp_tac); |
112 |
by (Blast_tac 1); |
|
113 |
qed_spec_mp "trace_is_Cons_conv"; |
|
114 |
Addsimps [trace_is_Cons_conv]; |
|
115 |
||
5069 | 116 |
Goal "!i. set(trace d i xs) = \ |
4832 | 117 |
\ (if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))"; |
118 |
by (induct_tac "xs" 1); |
|
119 |
by (Simp_tac 1); |
|
120 |
by (asm_simp_tac (simpset() addsimps [insert_commute]) 1); |
|
121 |
qed "set_trace_conv"; |
|
122 |
||
5069 | 123 |
Goal |
4832 | 124 |
"(!mid:set mids. deltas d mid k = k) --> deltas d (concat mids) k = k"; |
125 |
by (induct_tac "mids" 1); |
|
126 |
by (ALLGOALS Asm_simp_tac); |
|
127 |
qed_spec_mp "deltas_concat"; |
|
128 |
Addsimps [deltas_concat]; |
|
129 |
||
8777 | 130 |
Goal "[| n < Suc k; n ~= k |] ==> n < k"; |
131 |
by (arith_tac 1); |
|
4832 | 132 |
val lemma = result(); |
133 |
||
5069 | 134 |
Goal |
4832 | 135 |
"!i j xs. xs : regset d i j k = \ |
136 |
\ ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)"; |
|
137 |
by (induct_tac "k" 1); |
|
5184 | 138 |
by (simp_tac (simpset() addcongs [conj_cong] addsplits [list.split]) 1); |
4832 | 139 |
by (strip_tac 1); |
140 |
by (asm_simp_tac (simpset() addsimps [conc_def]) 1); |
|
141 |
by (rtac iffI 1); |
|
142 |
by (etac disjE 1); |
|
143 |
by (Asm_simp_tac 1); |
|
144 |
by (REPEAT(eresolve_tac[exE,conjE] 1)); |
|
145 |
by (Asm_full_simp_tac 1); |
|
146 |
by (subgoal_tac |
|
5184 | 147 |
"(!m:set(butlast(trace d n xsb)). m < Suc n) & deltas d xsb n = n" 1); |
4832 | 148 |
by (asm_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1); |
149 |
by (etac star.induct 1); |
|
150 |
by (Simp_tac 1); |
|
151 |
by (asm_full_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1); |
|
5184 | 152 |
by (case_tac "n : set(butlast(trace d i xs))" 1); |
4832 | 153 |
by (rtac disjI1 2); |
154 |
by (blast_tac (claset() addIs [lemma]) 2); |
|
155 |
by (rtac disjI2 1); |
|
156 |
by (dtac (in_set_butlastD RS decompose) 1); |
|
157 |
by (Clarify_tac 1); |
|
158 |
by (res_inst_tac [("x","pref")] exI 1); |
|
159 |
by (Asm_full_simp_tac 1); |
|
160 |
by (rtac conjI 1); |
|
161 |
by (rtac ballI 1); |
|
162 |
by (rtac lemma 1); |
|
163 |
by (Asm_simp_tac 2); |
|
164 |
by (EVERY[dtac bspec 1, atac 2]); |
|
165 |
by (Asm_simp_tac 1); |
|
166 |
by (res_inst_tac [("x","concat mids")] exI 1); |
|
167 |
by (Simp_tac 1); |
|
168 |
by (rtac conjI 1); |
|
169 |
by (rtac concat_in_star 1); |
|
170 |
by (Asm_simp_tac 1); |
|
171 |
by (rtac ballI 1); |
|
172 |
by (rtac ballI 1); |
|
173 |
by (rtac lemma 1); |
|
174 |
by (Asm_simp_tac 2); |
|
175 |
by (EVERY[dtac bspec 1, atac 2]); |
|
176 |
by (asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1); |
|
177 |
by (rtac ballI 1); |
|
178 |
by (rtac lemma 1); |
|
5521 | 179 |
by (Auto_tac); |
4832 | 180 |
qed_spec_mp "regset_spec"; |
181 |
||
5069 | 182 |
Goalw [bounded_def] |
5118 | 183 |
"bounded d k ==> !i. i < k --> (!n:set(trace d i xs). n < k)"; |
4832 | 184 |
by (induct_tac "xs" 1); |
185 |
by (ALLGOALS Simp_tac); |
|
186 |
by (Blast_tac 1); |
|
187 |
qed_spec_mp "trace_below"; |
|
188 |
||
5118 | 189 |
Goal "[| bounded d k; i < k; j < k |] ==> \ |
190 |
\ regset d i j k = {xs. deltas d xs i = j}"; |
|
4832 | 191 |
by (rtac set_ext 1); |
192 |
by (simp_tac (simpset() addsimps [regset_spec]) 1); |
|
193 |
by (blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1); |
|
194 |
qed "regset_below"; |
|
195 |
||
5069 | 196 |
Goalw [bounded_def] |
5118 | 197 |
"bounded d k ==> !i. i < k --> deltas d w i < k"; |
4832 | 198 |
by (induct_tac "w" 1); |
199 |
by (ALLGOALS Simp_tac); |
|
200 |
by (Blast_tac 1); |
|
201 |
qed_spec_mp "deltas_below"; |
|
202 |
||
5069 | 203 |
Goalw [regset_of_DA_def] |
5118 | 204 |
"[| bounded (next A) k; start A < k; j < k |] ==> \ |
205 |
\ w : regset_of_DA A k = accepts A w"; |
|
5132 | 206 |
by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps |
4832 | 207 |
[regset_below,deltas_below,accepts_def,delta_def]) 1); |
208 |
qed "regset_DA_equiv"; |