equal
deleted
inserted
replaced
362 val rabs_term = (rabs $ res_term) $ lam_term; |
362 val rabs_term = (rabs $ res_term) $ lam_term; |
363 in |
363 in |
364 rabs_term |
364 rabs_term |
365 end else let |
365 end else let |
366 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
366 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
367 val v = Free (x', fastype_of t); |
367 val v = Free (x', T); |
368 val t' = subst_bound (v, t); |
368 val t' = subst_bound (v, t); |
369 val rec_term = regularise t' rty rel lthy2; |
369 val rec_term = regularise t' rty rel lthy2; |
370 in |
370 in |
371 Term.lambda_name (x, v) rec_term |
371 Term.lambda_name (x, v) rec_term |
372 end |
372 end |
385 val rall_term = (rall $ res_term) $ lam_term; |
385 val rall_term = (rall $ res_term) $ lam_term; |
386 in |
386 in |
387 rall_term |
387 rall_term |
388 end else let |
388 end else let |
389 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
389 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
390 val v = Free (x', fastype_of t); |
390 val v = Free (x', T); |
391 val t' = subst_bound (v, t); |
391 val t' = subst_bound (v, t); |
392 val rec_term = regularise t' rty rel lthy2; |
392 val rec_term = regularise t' rty rel lthy2; |
393 val lam_term = Term.lambda_name (x, v) rec_term |
393 val lam_term = Term.lambda_name (x, v) rec_term |
394 in |
394 in |
395 Const(@{const_name "All"}, at) $ lam_term |
395 Const(@{const_name "All"}, at) $ lam_term |
409 val rall_term = (rall $ res_term) $ lam_term; |
409 val rall_term = (rall $ res_term) $ lam_term; |
410 in |
410 in |
411 rall_term |
411 rall_term |
412 end else let |
412 end else let |
413 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
413 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
414 val v = Free (x', fastype_of t); |
414 val v = Free (x', T); |
415 val t' = subst_bound (v, t); |
415 val t' = subst_bound (v, t); |
416 val rec_term = regularise t' rty rel lthy2; |
416 val rec_term = regularise t' rty rel lthy2; |
417 val lam_term = Term.lambda_name (x, v) rec_term |
417 val lam_term = Term.lambda_name (x, v) rec_term |
418 in |
418 in |
419 Const(@{const_name "All"}, at) $ lam_term |
419 Const(@{const_name "All"}, at) $ lam_term |
422 | _ => trm |
422 | _ => trm |
423 |
423 |
424 *} |
424 *} |
425 |
425 |
426 ML {* |
426 ML {* |
|
427 cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context}); |
427 cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context}); |
428 cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context}); |
428 cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); |
429 cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); |
429 cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}) |
430 cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}) |
430 *} |
431 *} |
|
432 |
|
433 |
431 |
434 |
432 |
435 |
433 ML {* |
436 ML {* |
434 fun atomize_thm thm = |
437 fun atomize_thm thm = |
435 let |
438 let |
1125 |
1128 |
1126 thm list.induct |
1129 thm list.induct |
1127 |
1130 |
1128 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *} |
1131 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *} |
1129 |
1132 |
1130 ML {* |
1133 prove {* |
1131 Syntax.string_of_term @{context} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}) |
1134 Logic.mk_equals |
1132 |> writeln |
1135 ((regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}), |
1133 *} |
1136 (prop_of li)) *} |
1134 |
1137 apply (atomize(full)) |
1135 ML {* |
1138 apply (unfold Ball_def) |
1136 Toplevel.program (fn () => |
1139 apply (tactic {* foo_tac' @{context} 1 *}) |
1137 cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}) |
1140 apply (simp only: IN_RESPECTS) |
1138 ) |
1141 apply (simp_all add: expand_fun_eq) |
1139 *} |
1142 prefer 2 |
1140 |
1143 apply (simp only: IN_RESPECTS) |
1141 |
1144 apply (simp add:list_eq_refl) |
|
1145 apply (tactic {* foo_tac' @{context} 1 *}) |
|
1146 prefer 2 |
|
1147 apply (auto) |
|
1148 sorry |
1142 |
1149 |
1143 ML {* |
1150 ML {* |
1144 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1151 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1145 *} |
1152 *} |
1146 |
1153 |
1302 apply (simp only:list_eq_refl) |
1309 apply (simp only:list_eq_refl) |
1303 apply (unfold id_def) |
1310 apply (unfold id_def) |
1304 (*apply (simp only: FUN_MAP_I)*) |
1311 (*apply (simp only: FUN_MAP_I)*) |
1305 apply (simp) |
1312 apply (simp) |
1306 apply (simp only: QUOT_TYPE_I_fset.thm10) |
1313 apply (simp only: QUOT_TYPE_I_fset.thm10) |
1307 apply (tactic {* foo_tac' @{context} 1 *}) |
|
1308 |
|
1309 .. |
1314 .. |
1310 apply (simp add:IN_RESPECTS) |
1315 apply (simp add:IN_RESPECTS) |
1311 |
1316 |
1312 |
1317 |
1313 |
1318 |