356 val t' = subst_bound (v, t); |
356 val t' = subst_bound (v, t); |
357 val rec_term = regularise t' rty rel lthy2; |
357 val rec_term = regularise t' rty rel lthy2; |
358 in |
358 in |
359 Term.lambda_name (x, v) rec_term |
359 Term.lambda_name (x, v) rec_term |
360 end |
360 end |
361 | ((Const (@{const_name "All"}, _)) $ (Abs (x, T, t))) => |
361 | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) => |
362 if T = rty then let |
362 if T = rty then let |
363 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
363 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
364 val v = Free (x', rty); |
364 val v = Free (x', rty); |
365 val t' = subst_bound (v, t); |
365 val t' = subst_bound (v, t); |
366 val rec_term = regularise t' rty rel lthy2; |
366 val rec_term = regularise t' rty rel lthy2; |
376 end else let |
376 end else let |
377 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
377 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
378 val v = Free (x', rty); |
378 val v = Free (x', rty); |
379 val t' = subst_bound (v, t); |
379 val t' = subst_bound (v, t); |
380 val rec_term = regularise t' rty rel lthy2; |
380 val rec_term = regularise t' rty rel lthy2; |
|
381 val lam_term = Term.lambda_name (x, v) rec_term |
381 in |
382 in |
382 Term.lambda_name (x, v) rec_term |
383 Const(@{const_name "All"}, at) $ lam_term |
383 end |
384 end |
384 | ((Const (@{const_name "Ex"}, _)) $ (Abs (x, T, t))) => |
385 | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) => |
385 if T = rty then let |
386 if T = rty then let |
386 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
387 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
387 val v = Free (x', rty); |
388 val v = Free (x', rty); |
388 val t' = subst_bound (v, t); |
389 val t' = subst_bound (v, t); |
389 val rec_term = regularise t' rty rel lthy2; |
390 val rec_term = regularise t' rty rel lthy2; |
399 end else let |
400 end else let |
400 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
401 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
401 val v = Free (x', rty); |
402 val v = Free (x', rty); |
402 val t' = subst_bound (v, t); |
403 val t' = subst_bound (v, t); |
403 val rec_term = regularise t' rty rel lthy2; |
404 val rec_term = regularise t' rty rel lthy2; |
|
405 val lam_term = Term.lambda_name (x, v) rec_term |
404 in |
406 in |
405 Term.lambda_name (x, v) rec_term |
407 Const(@{const_name "All"}, at) $ lam_term |
406 end |
408 end |
|
409 | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy) |
407 | _ => trm |
410 | _ => trm |
408 |
411 |
409 *} |
412 *} |
410 |
413 |
411 ML {* |
414 ML {* |
1114 apply (tactic {* foo_tac' @{context} 1 *}) |
1117 apply (tactic {* foo_tac' @{context} 1 *}) |
1115 done |
1118 done |
1116 |
1119 |
1117 thm list.induct |
1120 thm list.induct |
1118 |
1121 |
1119 ML {* val li = atomize_thm (meta_quantify @{thm list.induct}) *} |
1122 ML {* val li = Thm.freezeT (atomize_thm (meta_quantify @{thm list.induct})) *} |
1120 |
1123 |
1121 ML {* (* Doesn't recognize that 'a list = '?a list *) |
1124 ML {* |
1122 cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}) |
1125 Syntax.string_of_term @{context} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}) |
|
1126 |> writeln |
|
1127 *} |
|
1128 |
|
1129 ML {* |
|
1130 Toplevel.program (fn () => |
|
1131 cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}) |
|
1132 ) |
1123 *} |
1133 *} |
1124 |
1134 |
1125 |
1135 |
1126 |
1136 |
1127 ML {* |
1137 ML {* |