author | krauss |
Tue, 22 May 2007 17:25:26 +0200 | |
changeset 23074 | a53cb8ddb052 |
parent 22997 | d4f3b015b50b |
child 23416 | b73a6b72f706 |
permissions | -rw-r--r-- |
22375 | 1 |
(* Title: HOL/Library/sct.ML |
2 |
ID: $Id$ |
|
3 |
Author: Alexander Krauss, TU Muenchen |
|
4 |
||
5 |
Tactics for size change termination. |
|
6 |
*) |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
7 |
signature SCT = |
22375 | 8 |
sig |
9 |
val abs_rel_tac : tactic |
|
10 |
val mk_call_graph : tactic |
|
11 |
end |
|
12 |
||
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
13 |
structure Sct : SCT = |
22375 | 14 |
struct |
15 |
||
16 |
fun matrix [] ys = [] |
|
17 |
| matrix (x::xs) ys = map (pair x) ys :: matrix xs ys |
|
18 |
||
19 |
fun map_matrix f xss = map (map f) xss |
|
20 |
||
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
21 |
val scgT = @{typ scg} |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
22 |
val acgT = @{typ acg} |
22375 | 23 |
|
24 |
fun edgeT nT eT = HOLogic.mk_prodT (nT, HOLogic.mk_prodT (eT, nT)) |
|
25 |
fun graphT nT eT = Type ("Graphs.graph", [nT, eT]) |
|
26 |
||
27 |
fun graph_const nT eT = Const ("Graphs.graph.Graph", HOLogic.mk_setT (edgeT nT eT) --> graphT nT eT) |
|
28 |
||
29 |
val stepP_const = "SCT_Interpretation.stepP" |
|
30 |
val stepP_def = thm "SCT_Interpretation.stepP.simps" |
|
31 |
||
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
32 |
fun mk_stepP RD1 RD2 M1 M2 Rel = |
22375 | 33 |
let val RDT = fastype_of RD1 |
34 |
val MT = fastype_of M1 |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
35 |
in |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
36 |
Const (stepP_const, RDT --> RDT --> MT --> MT --> (fastype_of Rel) --> HOLogic.boolT) |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
37 |
$ RD1 $ RD2 $ M1 $ M2 $ Rel |
22375 | 38 |
end |
39 |
||
40 |
val no_stepI = thm "SCT_Interpretation.no_stepI" |
|
41 |
||
42 |
val approx_const = "SCT_Interpretation.approx" |
|
43 |
val approx_empty = thm "SCT_Interpretation.approx_empty" |
|
44 |
val approx_less = thm "SCT_Interpretation.approx_less" |
|
45 |
val approx_leq = thm "SCT_Interpretation.approx_leq" |
|
46 |
||
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
47 |
fun mk_approx G RD1 RD2 Ms1 Ms2 = |
22375 | 48 |
let val RDT = fastype_of RD1 |
49 |
val MsT = fastype_of Ms1 |
|
50 |
in Const (approx_const, scgT --> RDT --> RDT --> MsT --> MsT --> HOLogic.boolT) $ G $ RD1 $ RD2 $ Ms1 $ Ms2 end |
|
51 |
||
52 |
val sound_int_const = "SCT_Interpretation.sound_int" |
|
53 |
val sound_int_def = thm "SCT_Interpretation.sound_int_def" |
|
54 |
fun mk_sound_int A RDs M = |
|
55 |
let val RDsT = fastype_of RDs |
|
56 |
val MT = fastype_of M |
|
57 |
in Const (sound_int_const, acgT --> RDsT --> MT --> HOLogic.boolT) $ A $ RDs $ M end |
|
58 |
||
59 |
||
60 |
val nth_const = "List.nth" |
|
61 |
fun mk_nth xs = |
|
62 |
let val lT as Type (_, [T]) = fastype_of xs |
|
63 |
in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end |
|
64 |
||
65 |
||
22997 | 66 |
val less_nat_const = Const (@{const_name Orderings.less}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT) |
67 |
val lesseq_nat_const = Const (@{const_name Orderings.less_eq}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT) |
|
22375 | 68 |
|
69 |
val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"] |
|
70 |
||
71 |
val all_less_zero = thm "SCT_Interpretation.all_less_zero" |
|
72 |
val all_less_Suc = thm "SCT_Interpretation.all_less_Suc" |
|
73 |
||
74 |
(* --> Library? *) |
|
75 |
fun del_index n [] = [] |
|
76 |
| del_index n (x :: xs) = |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
77 |
if n>0 then x :: del_index (n - 1) xs else xs |
22375 | 78 |
|
79 |
(* Lists as finite multisets *) |
|
80 |
||
81 |
fun remove1 eq x [] = [] |
|
82 |
| remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys |
|
83 |
||
84 |
fun multi_union eq [] ys = ys |
|
85 |
| multi_union eq (x::xs) ys = x :: multi_union eq xs (remove1 eq x ys) |
|
86 |
||
87 |
fun dest_ex (Const ("Ex", _) $ Abs (a as (_,T,_))) = |
|
88 |
let |
|
89 |
val (n, body) = Term.dest_abs a |
|
90 |
in |
|
91 |
(Free (n, T), body) |
|
92 |
end |
|
93 |
| dest_ex _ = raise Match |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
94 |
|
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
95 |
fun dest_all_ex (t as (Const ("Ex",_) $ _)) = |
22375 | 96 |
let |
97 |
val (v,b) = dest_ex t |
|
98 |
val (vs, b') = dest_all_ex b |
|
99 |
in |
|
100 |
(v :: vs, b') |
|
101 |
end |
|
102 |
| dest_all_ex t = ([],t) |
|
103 |
||
22567
1565d476a9e2
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
wenzelm
parents:
22375
diff
changeset
|
104 |
fun dist_vars [] vs = (null vs orelse error "dist_vars"; []) |
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
105 |
| dist_vars (T::Ts) vs = |
22375 | 106 |
case find_index (fn v => fastype_of v = T) vs of |
107 |
~1 => Free ("", T) :: dist_vars Ts vs |
|
108 |
| i => (nth vs i) :: dist_vars Ts (del_index i vs) |
|
109 |
||
110 |
fun dest_case rebind t = |
|
111 |
let |
|
112 |
val (_ $ _ $ rhs :: _ $ _ $ match :: guards) = HOLogic.dest_conj t |
|
113 |
val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
114 |
in |
22375 | 115 |
foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match] |
116 |
end |
|
117 |
||
118 |
fun bind_many [] = I |
|
119 |
| bind_many vs = FundefLib.tupled_lambda (foldr1 HOLogic.mk_prod vs) |
|
120 |
||
121 |
(* Builds relation descriptions from a relation definition *) |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
122 |
fun mk_reldescs (Abs a) = |
22375 | 123 |
let |
124 |
val (_, Abs a') = Term.dest_abs a |
|
125 |
val (_, b) = Term.dest_abs a' |
|
126 |
val cases = HOLogic.dest_disj b |
|
127 |
val (vss, bs) = split_list (map dest_all_ex cases) |
|
128 |
val unionTs = fold (multi_union (op =)) (map (map fastype_of) vss) [] |
|
129 |
val rebind = map (bind_many o dist_vars unionTs) vss |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
130 |
|
22375 | 131 |
val RDs = map2 dest_case rebind bs |
132 |
in |
|
133 |
HOLogic.mk_list (fastype_of (hd RDs)) RDs |
|
134 |
end |
|
135 |
||
136 |
fun abs_rel_tac (st : thm) = |
|
137 |
let |
|
138 |
val thy = theory_of_thm st |
|
139 |
val (def, rd) = HOLogic.dest_eq (HOLogic.dest_Trueprop (hd (prems_of st))) |
|
140 |
val RDs = cterm_of thy (mk_reldescs def) |
|
141 |
val rdvar = Var (the_single (Term.add_vars rd [])) |> cterm_of thy |
|
142 |
in |
|
143 |
Seq.single (cterm_instantiate [(rdvar, RDs)] st) |
|
144 |
end |
|
145 |
||
146 |
||
147 |
||
148 |
||
149 |
||
150 |
||
151 |
(* very primitive *) |
|
23074 | 152 |
fun measures_of thy RD = |
22375 | 153 |
let |
154 |
val domT = range_type (fastype_of (fst (HOLogic.dest_prod (snd (HOLogic.dest_prod RD))))) |
|
23074 | 155 |
val measures = LexicographicOrder.mk_base_funs thy domT |
22375 | 156 |
in |
157 |
measures |
|
158 |
end |
|
159 |
||
160 |
val mk_number = HOLogic.mk_nat o IntInf.fromInt |
|
161 |
val dest_number = IntInf.toInt o HOLogic.dest_nat |
|
162 |
||
163 |
fun nums_to i = map mk_number (0 upto (i - 1)) |
|
164 |
||
165 |
val nth_simps = [thm "List.nth_Cons_0", thm "List.nth_Cons_Suc"] |
|
166 |
val nth_ss = (HOL_basic_ss addsimps nth_simps) |
|
167 |
val simp_nth_tac = simp_tac nth_ss |
|
168 |
||
169 |
||
170 |
fun tabulate_tlist thy l = |
|
171 |
let |
|
172 |
val n = length (HOLogic.dest_list l) |
|
173 |
val table = Inttab.make (map (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) (0 upto n - 1)) |
|
174 |
in |
|
175 |
the o Inttab.lookup table |
|
176 |
end |
|
177 |
||
178 |
val get_elem = snd o Logic.dest_equals o prop_of |
|
179 |
||
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
180 |
fun inst_nums thy i j (t:thm) = |
22375 | 181 |
instantiate' [] [NONE, NONE, NONE, SOME (cterm_of thy (mk_number i)), NONE, SOME (cterm_of thy (mk_number j))] t |
182 |
||
183 |
datatype call_fact = |
|
184 |
NoStep of thm |
|
185 |
| Graph of (term * thm) |
|
186 |
||
187 |
fun rand (_ $ t) = t |
|
188 |
||
189 |
fun setup_probe_goal thy domT Dtab Mtab (i, j) = |
|
190 |
let |
|
191 |
val RD1 = get_elem (Dtab i) |
|
192 |
val RD2 = get_elem (Dtab j) |
|
193 |
val Ms1 = get_elem (Mtab i) |
|
194 |
val Ms2 = get_elem (Mtab j) |
|
195 |
||
196 |
val Mst1 = HOLogic.dest_list (rand Ms1) |
|
197 |
val Mst2 = HOLogic.dest_list (rand Ms2) |
|
198 |
||
199 |
val mvar1 = Free ("sctmfv1", domT --> HOLogic.natT) |
|
200 |
val mvar2 = Free ("sctmfv2", domT --> HOLogic.natT) |
|
201 |
val relvar = Free ("sctmfrel", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT) |
|
202 |
val N = length Mst1 and M = length Mst2 |
|
203 |
val saved_state = HOLogic.mk_Trueprop (mk_stepP RD1 RD2 mvar1 mvar2 relvar) |
|
204 |
|> cterm_of thy |
|
205 |
|> Goal.init |
|
206 |
|> CLASIMPSET auto_tac |> Seq.hd |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
207 |
|
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
208 |
val no_step = saved_state |
22375 | 209 |
|> forall_intr (cterm_of thy relvar) |
210 |
|> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const)))) |
|
211 |
|> CLASIMPSET auto_tac |> Seq.hd |
|
212 |
||
213 |
in |
|
214 |
if Thm.no_prems no_step |
|
215 |
then NoStep (Goal.finish no_step RS no_stepI) |
|
216 |
else |
|
217 |
let |
|
218 |
fun set_m1 i = |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
219 |
let |
22375 | 220 |
val M1 = nth Mst1 i |
221 |
val with_m1 = saved_state |
|
222 |
|> forall_intr (cterm_of thy mvar1) |
|
223 |
|> forall_elim (cterm_of thy M1) |
|
224 |
|> CLASIMPSET auto_tac |> Seq.hd |
|
225 |
||
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
226 |
fun set_m2 j = |
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
227 |
let |
22375 | 228 |
val M2 = nth Mst2 j |
229 |
val with_m2 = with_m1 |
|
230 |
|> forall_intr (cterm_of thy mvar2) |
|
231 |
|> forall_elim (cterm_of thy M2) |
|
232 |
|> CLASIMPSET auto_tac |> Seq.hd |
|
233 |
||
234 |
val decr = forall_intr (cterm_of thy relvar) |
|
235 |
#> forall_elim (cterm_of thy less_nat_const) |
|
236 |
#> CLASIMPSET auto_tac #> Seq.hd |
|
237 |
||
238 |
val decreq = forall_intr (cterm_of thy relvar) |
|
239 |
#> forall_elim (cterm_of thy lesseq_nat_const) |
|
240 |
#> CLASIMPSET auto_tac #> Seq.hd |
|
241 |
||
242 |
val thm1 = decr with_m2 |
|
243 |
in |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
244 |
if Thm.no_prems thm1 |
22375 | 245 |
then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm1) 1)) |
246 |
else let val thm2 = decreq with_m2 in |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
247 |
if Thm.no_prems thm2 |
22375 | 248 |
then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm2) 1)) |
249 |
else all_tac end |
|
250 |
end |
|
251 |
in set_m2 end |
|
252 |
||
253 |
val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2) |
|
254 |
||
255 |
val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1))) |
|
256 |
THEN (rtac approx_empty 1) |
|
257 |
||
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
258 |
val approx_thm = goal |
22375 | 259 |
|> cterm_of thy |
260 |
|> Goal.init |
|
261 |
|> tac |> Seq.hd |
|
262 |
|> Goal.finish |
|
263 |
||
264 |
val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm |
|
265 |
in |
|
266 |
Graph (G, approx_thm) |
|
267 |
end |
|
268 |
end |
|
269 |
||
270 |
fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n)) |
|
271 |
||
272 |
fun mk_set T [] = Const ("{}", HOLogic.mk_setT T) |
|
273 |
| mk_set T (x :: xs) = Const ("insert", |
|
274 |
T --> HOLogic.mk_setT T --> HOLogic.mk_setT T) $ x $ mk_set T xs |
|
275 |
||
276 |
fun dest_set (Const ("{}", _)) = [] |
|
277 |
| dest_set (Const ("insert", _) $ x $ xs) = x :: dest_set xs |
|
278 |
||
279 |
val pr_graph = Sign.string_of_term |
|
280 |
fun pr_matrix thy = map_matrix (fn Graph (G, _) => pr_graph thy G | _ => "X") |
|
281 |
||
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
282 |
val in_graph_tac = |
22375 | 283 |
simp_tac (HOL_basic_ss addsimps has_edge_simps) 1 |
284 |
THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *) |
|
285 |
||
286 |
fun approx_tac (NoStep thm) = rtac disjI1 1 THEN rtac thm 1 |
|
287 |
| approx_tac (Graph (G, thm)) = |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
288 |
rtac disjI2 1 |
22375 | 289 |
THEN rtac exI 1 |
290 |
THEN rtac conjI 1 |
|
291 |
THEN rtac thm 2 |
|
292 |
THEN in_graph_tac |
|
293 |
||
294 |
fun all_less_tac [] = rtac all_less_zero 1 |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
295 |
| all_less_tac (t :: ts) = rtac all_less_Suc 1 |
22375 | 296 |
THEN simp_nth_tac 1 |
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
297 |
THEN t |
22375 | 298 |
THEN all_less_tac ts |
299 |
||
300 |
||
22997 | 301 |
fun mk_length l = HOLogic.size_const (fastype_of l) $ l; |
22375 | 302 |
val length_simps = thms "SCT_Interpretation.length_simps" |
303 |
||
304 |
||
305 |
||
306 |
fun mk_call_graph (st : thm) = |
|
307 |
let |
|
308 |
val thy = theory_of_thm st |
|
309 |
val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st)) |
|
310 |
||
311 |
val RDs = HOLogic.dest_list RDlist |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
312 |
val n = length RDs |
22375 | 313 |
|
23074 | 314 |
val Mss = map (measures_of thy) RDs |
22375 | 315 |
|
316 |
val domT = domain_type (fastype_of (hd (hd Mss))) |
|
317 |
||
318 |
val mfuns = map (fn Ms => mk_nth (HOLogic.mk_list (fastype_of (hd Ms)) Ms)) Mss |
|
319 |
|> (fn l => HOLogic.mk_list (fastype_of (hd l)) l) |
|
320 |
||
321 |
val Dtab = tabulate_tlist thy RDlist |
|
322 |
val Mtab = tabulate_tlist thy mfuns |
|
323 |
||
324 |
val len_simp = Simplifier.rewrite (HOL_basic_ss addsimps length_simps) (cterm_of thy (mk_length RDlist)) |
|
325 |
||
326 |
val mlens = map length Mss |
|
327 |
||
328 |
val indices = (n - 1 downto 0) |
|
329 |
val pairs = matrix indices indices |
|
330 |
val parts = map_matrix (fn (n,m) => |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
331 |
(timeap_msg (string_of_int n ^ "," ^ string_of_int m) |
22375 | 332 |
(setup_probe_goal thy domT Dtab Mtab) (n,m))) pairs |
333 |
||
334 |
||
335 |
val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^ |
|
336 |
pr_graph thy G ^ ",\n") |
|
337 |
| _ => I) cs) parts "" |
|
338 |
val _ = Output.warning s |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
339 |
|
22375 | 340 |
|
341 |
val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs) |
|
342 |
|> mk_set (edgeT HOLogic.natT scgT) |
|
343 |
|> curry op $ (graph_const HOLogic.natT scgT) |
|
344 |
||
345 |
||
346 |
val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns) |
|
347 |
||
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
348 |
val tac = |
22375 | 349 |
(SIMPSET (unfold_tac [sound_int_def, len_simp])) |
350 |
THEN all_less_tac (map (all_less_tac o map approx_tac) parts) |
|
351 |
in |
|
352 |
tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st) |
|
353 |
end |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
354 |
|
22375 | 355 |
|
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
356 |
end |
22375 | 357 |
|
358 |
||
359 |
||
360 |
||
361 |
||
362 |
||
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22567
diff
changeset
|
363 |