|
1 Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2]; |
|
2 AddIs [in_set_butlast_appendI1,in_set_butlast_appendI2]; |
|
3 Addsimps [image_eqI]; |
|
4 |
|
5 AddIffs [star.NilI]; |
|
6 Addsimps [star.ConsI]; |
|
7 AddIs [star.ConsI]; |
|
8 |
|
9 (* Lists *) |
|
10 |
|
11 (* |
|
12 (* could go into List. Needs WF_Rel as ancestor. *) |
|
13 (* Induction over the length of a list: *) |
|
14 val prems = goal thy |
|
15 "(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs"; |
|
16 by(res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")] |
|
17 wf_induct 1); |
|
18 by(Simp_tac 1); |
|
19 by(asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1); |
|
20 bes prems 1; |
|
21 qed "list_length_induct"; |
|
22 *) |
|
23 |
|
24 goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])"; |
|
25 by(exhaust_tac "xs" 1); |
|
26 by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
|
27 qed "butlast_empty"; |
|
28 AddIffs [butlast_empty]; |
|
29 |
|
30 goal thy "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))"; |
|
31 by(induct_tac "xss" 1); |
|
32 by(Simp_tac 1); |
|
33 by(asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps |
|
34 addsplits [expand_if]) 1); |
|
35 br conjI 1; |
|
36 by(Clarify_tac 1); |
|
37 br conjI 1; |
|
38 by(Blast_tac 1); |
|
39 by(Clarify_tac 1); |
|
40 by(subgoal_tac "xs=[]" 1); |
|
41 by(rotate_tac ~1 1); |
|
42 by(Asm_full_simp_tac 1); |
|
43 by(Blast_tac 1); |
|
44 by(blast_tac (claset() addDs [in_set_butlastD]) 1); |
|
45 qed_spec_mp "in_set_butlast_concatI"; |
|
46 |
|
47 (* Regular sets *) |
|
48 |
|
49 goal thy "(!xs: set xss. xs:A) --> concat xss : star A"; |
|
50 by(induct_tac "xss" 1); |
|
51 by(ALLGOALS Asm_full_simp_tac); |
|
52 qed_spec_mp "concat_in_star"; |
|
53 |
|
54 (* The main lemma: |
|
55 how to decompose a trace into a prefix, a list of loops and a suffix. |
|
56 *) |
|
57 goal thy "!i. k : set(trace A i xs) --> (? pref mids suf. \ |
|
58 \ xs = pref @ concat mids @ suf & \ |
|
59 \ deltas A pref i = k & (!n:set(butlast(trace A i pref)). n ~= k) & \ |
|
60 \ (!mid:set mids. (deltas A mid k = k) & \ |
|
61 \ (!n:set(butlast(trace A k mid)). n ~= k)) & \ |
|
62 \ (!n:set(butlast(trace A k suf)). n ~= k))"; |
|
63 by(induct_tac "xs" 1); |
|
64 by(Simp_tac 1); |
|
65 by(rename_tac "a as" 1); |
|
66 br allI 1; |
|
67 by(case_tac "A a i = k" 1); |
|
68 by(strip_tac 1); |
|
69 by(res_inst_tac[("x","[a]")]exI 1); |
|
70 by(Asm_full_simp_tac 1); |
|
71 by(case_tac "k : set(trace A (A a i) as)" 1); |
|
72 be allE 1; |
|
73 be impE 1; |
|
74 ba 1; |
|
75 by(REPEAT(etac exE 1)); |
|
76 by(res_inst_tac[("x","pref#mids")]exI 1); |
|
77 by(res_inst_tac[("x","suf")]exI 1); |
|
78 by(Asm_full_simp_tac 1); |
|
79 by(res_inst_tac[("x","[]")]exI 1); |
|
80 by(res_inst_tac[("x","as")]exI 1); |
|
81 by(Asm_full_simp_tac 1); |
|
82 by(blast_tac (claset() addDs [in_set_butlastD]) 1); |
|
83 by(Asm_simp_tac 1); |
|
84 br conjI 1; |
|
85 by(Blast_tac 1); |
|
86 by(strip_tac 1); |
|
87 be allE 1; |
|
88 be impE 1; |
|
89 ba 1; |
|
90 by(REPEAT(etac exE 1)); |
|
91 by(res_inst_tac[("x","a#pref")]exI 1); |
|
92 by(res_inst_tac[("x","mids")]exI 1); |
|
93 by(res_inst_tac[("x","suf")]exI 1); |
|
94 by(asm_simp_tac (simpset() addsplits [expand_if]) 1); |
|
95 qed_spec_mp "decompose"; |
|
96 |
|
97 goal thy "!i. length(trace A i xs) = length xs"; |
|
98 by(induct_tac "xs" 1); |
|
99 by(ALLGOALS Asm_simp_tac); |
|
100 qed "length_trace"; |
|
101 Addsimps [length_trace]; |
|
102 |
|
103 goal thy "!i. deltas A (xs@ys) i = deltas A ys (deltas A xs i)"; |
|
104 by(induct_tac "xs" 1); |
|
105 by(ALLGOALS Asm_simp_tac); |
|
106 qed "deltas_append"; |
|
107 Addsimps [deltas_append]; |
|
108 |
|
109 goal thy "!i. trace A i (xs@ys) = trace A i xs @ trace A (deltas A xs i) ys"; |
|
110 by(induct_tac "xs" 1); |
|
111 by(ALLGOALS Asm_simp_tac); |
|
112 qed "trace_append"; |
|
113 Addsimps [trace_append]; |
|
114 |
|
115 goal thy "(!xs: set xss. deltas A xs i = i) --> \ |
|
116 \ trace A i (concat xss) = concat (map (trace A i) xss)"; |
|
117 by(induct_tac "xss" 1); |
|
118 by(ALLGOALS Asm_simp_tac); |
|
119 qed_spec_mp "trace_concat"; |
|
120 Addsimps [trace_concat]; |
|
121 |
|
122 goal thy "!i. (trace A i xs = []) = (xs = [])"; |
|
123 by(exhaust_tac "xs" 1); |
|
124 by(ALLGOALS Asm_simp_tac); |
|
125 qed "trace_is_Nil"; |
|
126 Addsimps [trace_is_Nil]; |
|
127 |
|
128 goal thy "(trace A i xs = n#ns) = \ |
|
129 \ (case xs of [] => False | y#ys => n = A y i & ns = trace A n ys)"; |
|
130 by(exhaust_tac "xs" 1); |
|
131 by(ALLGOALS Asm_simp_tac); |
|
132 by(Blast_tac 1); |
|
133 qed_spec_mp "trace_is_Cons_conv"; |
|
134 Addsimps [trace_is_Cons_conv]; |
|
135 |
|
136 goal thy "!i. set(trace A i xs) = \ |
|
137 \ (if xs=[] then {} else insert(deltas A xs i)(set(butlast(trace A i xs))))"; |
|
138 by(induct_tac "xs" 1); |
|
139 by(Simp_tac 1); |
|
140 by(asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1); |
|
141 qed "set_trace_conv"; |
|
142 |
|
143 goal thy |
|
144 "(!mid:set mids. deltas A mid k = k) --> deltas A (concat mids) k = k"; |
|
145 by(induct_tac "mids" 1); |
|
146 by(ALLGOALS Asm_simp_tac); |
|
147 qed_spec_mp "deltas_concat"; |
|
148 Addsimps [deltas_concat]; |
|
149 |
|
150 goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k"; |
|
151 be nat_neqE 1; |
|
152 by(ALLGOALS trans_tac); |
|
153 val lemma = result(); |
|
154 |
|
155 |
|
156 goal thy |
|
157 "!i j xs. xs : regset_of A i j k = \ |
|
158 \ ((!n:set(butlast(trace A i xs)). n < k) & deltas A xs i = j)"; |
|
159 by(induct_tac "k" 1); |
|
160 by(simp_tac (simpset() addcongs [conj_cong] |
|
161 addsplits [expand_if,split_list_case]) 1); |
|
162 by(strip_tac 1); |
|
163 by(asm_simp_tac (simpset() addsimps [conc_def]) 1); |
|
164 br iffI 1; |
|
165 be disjE 1; |
|
166 by(Asm_simp_tac 1); |
|
167 by(REPEAT(eresolve_tac[exE,conjE] 1)); |
|
168 by(Asm_full_simp_tac 1); |
|
169 by(subgoal_tac |
|
170 "(!n:set(butlast(trace A k xsb)). n < Suc k) & deltas A xsb k = k" 1); |
|
171 by(asm_simp_tac (simpset() addsplits [expand_if] |
|
172 addsimps [set_trace_conv,butlast_append,ball_Un]) 1); |
|
173 be star.induct 1; |
|
174 by(Simp_tac 1); |
|
175 by(asm_full_simp_tac (simpset() addsplits [expand_if] |
|
176 addsimps [set_trace_conv,butlast_append,ball_Un]) 1); |
|
177 by(case_tac "k : set(butlast(trace A i xs))" 1); |
|
178 br disjI1 2; |
|
179 by(blast_tac (claset() addIs [lemma]) 2); |
|
180 br disjI2 1; |
|
181 bd (in_set_butlastD RS decompose) 1; |
|
182 by(Clarify_tac 1); |
|
183 by(res_inst_tac [("x","pref")] exI 1); |
|
184 by(Asm_full_simp_tac 1); |
|
185 br conjI 1; |
|
186 br ballI 1; |
|
187 br lemma 1; |
|
188 by(Asm_simp_tac 2); |
|
189 by(EVERY[dtac bspec 1, atac 2]); |
|
190 by(Asm_simp_tac 1); |
|
191 by(res_inst_tac [("x","concat mids")] exI 1); |
|
192 by(Simp_tac 1); |
|
193 br conjI 1; |
|
194 br concat_in_star 1; |
|
195 by(Asm_simp_tac 1); |
|
196 br ballI 1; |
|
197 br ballI 1; |
|
198 br lemma 1; |
|
199 by(Asm_simp_tac 2); |
|
200 by(EVERY[dtac bspec 1, atac 2]); |
|
201 by(asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1); |
|
202 br ballI 1; |
|
203 br lemma 1; |
|
204 by(Asm_simp_tac 2); |
|
205 by(EVERY[dtac bspec 1, atac 2]); |
|
206 by(Asm_simp_tac 1); |
|
207 qed_spec_mp "regset_of_spec"; |
|
208 |
|
209 goal thy "!!A. !n. n < k --> (!x. A x n < k) ==> \ |
|
210 \ !i. i < k --> (!n:set(trace A i xs). n < k)"; |
|
211 by(induct_tac "xs" 1); |
|
212 by(ALLGOALS Simp_tac); |
|
213 by(Blast_tac 1); |
|
214 qed_spec_mp "trace_below"; |
|
215 |
|
216 goal thy "!!A. [| !n. n < k --> (!x. A x n < k); i < k; j < k |] ==> \ |
|
217 \ regset_of A i j k = {xs. deltas A xs i = j}"; |
|
218 br set_ext 1; |
|
219 by(simp_tac (simpset() addsimps [regset_of_spec]) 1); |
|
220 by(blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1); |
|
221 qed "regset_of_below"; |