author | wenzelm |
Tue, 16 Dec 1997 17:58:03 +0100 | |
changeset 4423 | a129b817b58a |
parent 4137 | 2ce2e659c2b1 |
child 4686 | 74a12e86b20b |
permissions | -rw-r--r-- |
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
1 |
Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
2 |
AddIs [in_set_butlast_appendI1,in_set_butlast_appendI2]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
3 |
Addsimps [image_eqI]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
4 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
5 |
AddIffs [star.NilI]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
6 |
Addsimps [star.ConsI]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
7 |
AddIs [star.ConsI]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
8 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
9 |
(* Lists *) |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
10 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
11 |
(* |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
12 |
(* could go into List. Needs WF_Rel as ancestor. *) |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
13 |
(* Induction over the length of a list: *) |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
14 |
val prems = goal thy |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
15 |
"(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs"; |
4423 | 16 |
by (res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")] |
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
17 |
wf_induct 1); |
4423 | 18 |
by (Simp_tac 1); |
19 |
by (asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1); |
|
20 |
by (eresolve_tac prems 1); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
21 |
qed "list_length_induct"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
22 |
*) |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
23 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
24 |
goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])"; |
4423 | 25 |
by (exhaust_tac "xs" 1); |
26 |
by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]))); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
27 |
qed "butlast_empty"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
28 |
AddIffs [butlast_empty]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
29 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
30 |
goal thy "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))"; |
4423 | 31 |
by (induct_tac "xss" 1); |
32 |
by (Simp_tac 1); |
|
33 |
by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
34 |
addsplits [expand_if]) 1); |
4423 | 35 |
by (rtac conjI 1); |
36 |
by (Clarify_tac 1); |
|
37 |
by (rtac 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); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
45 |
qed_spec_mp "in_set_butlast_concatI"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
46 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
47 |
(* Regular sets *) |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
48 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
49 |
goal thy "(!xs: set xss. xs:A) --> concat xss : star A"; |
4423 | 50 |
by (induct_tac "xss" 1); |
51 |
by (ALLGOALS Asm_full_simp_tac); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
52 |
qed_spec_mp "concat_in_star"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
53 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
54 |
(* The main lemma: |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
55 |
how to decompose a trace into a prefix, a list of loops and a suffix. |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
56 |
*) |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
57 |
goal thy "!i. k : set(trace A i xs) --> (? pref mids suf. \ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
58 |
\ xs = pref @ concat mids @ suf & \ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
59 |
\ deltas A pref i = k & (!n:set(butlast(trace A i pref)). n ~= k) & \ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
60 |
\ (!mid:set mids. (deltas A mid k = k) & \ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
61 |
\ (!n:set(butlast(trace A k mid)). n ~= k)) & \ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
62 |
\ (!n:set(butlast(trace A k suf)). n ~= k))"; |
4423 | 63 |
by (induct_tac "xs" 1); |
64 |
by (Simp_tac 1); |
|
65 |
by (rename_tac "a as" 1); |
|
66 |
by (rtac 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 |
by (etac allE 1); |
|
73 |
by (etac impE 1); |
|
74 |
by (assume_tac 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 |
by (rtac conjI 1); |
|
85 |
by (Blast_tac 1); |
|
86 |
by (strip_tac 1); |
|
87 |
by (etac allE 1); |
|
88 |
by (etac impE 1); |
|
89 |
by (assume_tac 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); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
95 |
qed_spec_mp "decompose"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
96 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
97 |
goal thy "!i. length(trace A i xs) = length xs"; |
4423 | 98 |
by (induct_tac "xs" 1); |
99 |
by (ALLGOALS Asm_simp_tac); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
100 |
qed "length_trace"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
101 |
Addsimps [length_trace]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
102 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
103 |
goal thy "!i. deltas A (xs@ys) i = deltas A ys (deltas A xs i)"; |
4423 | 104 |
by (induct_tac "xs" 1); |
105 |
by (ALLGOALS Asm_simp_tac); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
106 |
qed "deltas_append"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
107 |
Addsimps [deltas_append]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
108 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
109 |
goal thy "!i. trace A i (xs@ys) = trace A i xs @ trace A (deltas A xs i) ys"; |
4423 | 110 |
by (induct_tac "xs" 1); |
111 |
by (ALLGOALS Asm_simp_tac); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
112 |
qed "trace_append"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
113 |
Addsimps [trace_append]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
114 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
115 |
goal thy "(!xs: set xss. deltas A xs i = i) --> \ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
116 |
\ trace A i (concat xss) = concat (map (trace A i) xss)"; |
4423 | 117 |
by (induct_tac "xss" 1); |
118 |
by (ALLGOALS Asm_simp_tac); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
119 |
qed_spec_mp "trace_concat"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
120 |
Addsimps [trace_concat]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
121 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
122 |
goal thy "!i. (trace A i xs = []) = (xs = [])"; |
4423 | 123 |
by (exhaust_tac "xs" 1); |
124 |
by (ALLGOALS Asm_simp_tac); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
125 |
qed "trace_is_Nil"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
126 |
Addsimps [trace_is_Nil]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
127 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
128 |
goal thy "(trace A i xs = n#ns) = \ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
129 |
\ (case xs of [] => False | y#ys => n = A y i & ns = trace A n ys)"; |
4423 | 130 |
by (exhaust_tac "xs" 1); |
131 |
by (ALLGOALS Asm_simp_tac); |
|
132 |
by (Blast_tac 1); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
133 |
qed_spec_mp "trace_is_Cons_conv"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
134 |
Addsimps [trace_is_Cons_conv]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
135 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
136 |
goal thy "!i. set(trace A i xs) = \ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
137 |
\ (if xs=[] then {} else insert(deltas A xs i)(set(butlast(trace A i xs))))"; |
4423 | 138 |
by (induct_tac "xs" 1); |
139 |
by (Simp_tac 1); |
|
140 |
by (asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
141 |
qed "set_trace_conv"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
142 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
143 |
goal thy |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
144 |
"(!mid:set mids. deltas A mid k = k) --> deltas A (concat mids) k = k"; |
4423 | 145 |
by (induct_tac "mids" 1); |
146 |
by (ALLGOALS Asm_simp_tac); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
147 |
qed_spec_mp "deltas_concat"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
148 |
Addsimps [deltas_concat]; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
149 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
150 |
goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k"; |
4423 | 151 |
by (etac nat_neqE 1); |
152 |
by (ALLGOALS trans_tac); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
153 |
val lemma = result(); |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
154 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
155 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
156 |
goal thy |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
157 |
"!i j xs. xs : regset_of A i j k = \ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
158 |
\ ((!n:set(butlast(trace A i xs)). n < k) & deltas A xs i = j)"; |
4423 | 159 |
by (induct_tac "k" 1); |
160 |
by (simp_tac (simpset() addcongs [conj_cong] |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
161 |
addsplits [expand_if,split_list_case]) 1); |
4423 | 162 |
by (strip_tac 1); |
163 |
by (asm_simp_tac (simpset() addsimps [conc_def]) 1); |
|
164 |
by (rtac iffI 1); |
|
165 |
by (etac 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 |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
170 |
"(!n:set(butlast(trace A k xsb)). n < Suc k) & deltas A xsb k = k" 1); |
4423 | 171 |
by (asm_simp_tac (simpset() addsplits [expand_if] |
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
172 |
addsimps [set_trace_conv,butlast_append,ball_Un]) 1); |
4423 | 173 |
by (etac star.induct 1); |
174 |
by (Simp_tac 1); |
|
175 |
by (asm_full_simp_tac (simpset() addsplits [expand_if] |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
176 |
addsimps [set_trace_conv,butlast_append,ball_Un]) 1); |
4423 | 177 |
by (case_tac "k : set(butlast(trace A i xs))" 1); |
178 |
by (rtac disjI1 2); |
|
179 |
by (blast_tac (claset() addIs [lemma]) 2); |
|
180 |
by (rtac disjI2 1); |
|
181 |
by (dtac (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 |
by (rtac conjI 1); |
|
186 |
by (rtac ballI 1); |
|
187 |
by (rtac 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 |
by (rtac conjI 1); |
|
194 |
by (rtac concat_in_star 1); |
|
195 |
by (Asm_simp_tac 1); |
|
196 |
by (rtac ballI 1); |
|
197 |
by (rtac ballI 1); |
|
198 |
by (rtac 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 |
by (rtac ballI 1); |
|
203 |
by (rtac lemma 1); |
|
204 |
by (Asm_simp_tac 2); |
|
205 |
by (EVERY[dtac bspec 1, atac 2]); |
|
206 |
by (Asm_simp_tac 1); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
207 |
qed_spec_mp "regset_of_spec"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
208 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
209 |
goal thy "!!A. !n. n < k --> (!x. A x n < k) ==> \ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
210 |
\ !i. i < k --> (!n:set(trace A i xs). n < k)"; |
4423 | 211 |
by (induct_tac "xs" 1); |
212 |
by (ALLGOALS Simp_tac); |
|
213 |
by (Blast_tac 1); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
214 |
qed_spec_mp "trace_below"; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
215 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
216 |
goal thy "!!A. [| !n. n < k --> (!x. A x n < k); i < k; j < k |] ==> \ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
217 |
\ regset_of A i j k = {xs. deltas A xs i = j}"; |
4423 | 218 |
by (rtac 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); |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
221 |
qed "regset_of_below"; |