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 |
396 end |
396 end |
|
397 | ((Const (@{const_name "All"}, at)) $ P) => |
|
398 let |
|
399 val (_, [al, _]) = dest_Type (fastype_of P); |
|
400 val ([x], lthy2) = Variable.variant_fixes [""] lthy; |
|
401 val v = (Free (x, al)); |
|
402 val abs = Term.lambda_name (x, v) (P $ v); |
|
403 in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end |
397 | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) => |
404 | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) => |
398 if (needs_lift rty T) then let |
405 if (needs_lift rty T) then let |
399 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
406 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
400 val v = Free (x', T); |
407 val v = Free (x', T); |
401 val t' = subst_bound (v, t); |
408 val t' = subst_bound (v, t); |
416 val rec_term = regularise t' rty rel lthy2; |
423 val rec_term = regularise t' rty rel lthy2; |
417 val lam_term = Term.lambda_name (x, v) rec_term |
424 val lam_term = Term.lambda_name (x, v) rec_term |
418 in |
425 in |
419 Const(@{const_name "All"}, at) $ lam_term |
426 Const(@{const_name "All"}, at) $ lam_term |
420 end |
427 end |
|
428 | ((Const (@{const_name "Ex"}, at)) $ P) => |
|
429 let |
|
430 val (_, [al, _]) = dest_Type (fastype_of P); |
|
431 val ([x], lthy2) = Variable.variant_fixes [""] lthy; |
|
432 val v = (Free (x, al)); |
|
433 val abs = Term.lambda_name (x, v) (P $ v); |
|
434 in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end |
421 | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy) |
435 | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy) |
422 | _ => trm |
436 | _ => trm |
423 |
437 |
424 *} |
438 *} |
425 |
439 |
426 ML {* |
440 ML {* |
427 cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context}); |
441 cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context}); |
428 cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context}); |
442 cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context}); |
429 cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); |
443 cterm_of @{theory} (regularise @{term "\<forall>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}) |
444 cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context}); |
|
445 cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context}); |
431 *} |
446 *} |
432 |
447 |
433 |
448 |
434 |
449 |
435 |
450 |
1125 apply (atomize(full)) |
1140 apply (atomize(full)) |
1126 apply (tactic {* foo_tac' @{context} 1 *}) |
1141 apply (tactic {* foo_tac' @{context} 1 *}) |
1127 done |
1142 done |
1128 |
1143 |
1129 thm list.induct |
1144 thm list.induct |
1130 |
1145 lemma list_induct2: |
1131 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *} |
1146 shows "(P []) \<Longrightarrow> (\<forall> a list. ((P list) \<longrightarrow> (P (a # list)))) \<Longrightarrow> \<forall>l :: 'a list. (P l)" |
|
1147 apply (rule allI) |
|
1148 apply (rule list.induct) |
|
1149 apply (assumption) |
|
1150 apply (auto) |
|
1151 done |
|
1152 |
|
1153 ML {* ObjectLogic.atomize (cprop_of @{thm list_induct2}) *} |
|
1154 ML {* (atomize_thm @{thm list_induct2}) *} |
|
1155 |
|
1156 ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct2}) *} |
1132 |
1157 |
1133 (* TODO: the following 2 lemmas should go to quotscript.thy after all are done *) |
1158 (* TODO: the following 2 lemmas should go to quotscript.thy after all are done *) |
1134 lemma RIGHT_RES_FORALL_REGULAR: |
1159 lemma RIGHT_RES_FORALL_REGULAR: |
1135 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
1160 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
1136 shows "All P ==> Ball R Q" |
1161 shows "All P ==> Ball R Q" |
1145 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
1170 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
1146 done |
1171 done |
1147 |
1172 |
1148 prove {* |
1173 prove {* |
1149 Logic.mk_implies |
1174 Logic.mk_implies |
1150 ((regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}), |
1175 ((prop_of li), |
1151 (prop_of li)) *} |
1176 (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
1152 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
1177 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
1153 thm LEFT_RES_FORALL_REGULAR |
1178 thm RIGHT_RES_FORALL_REGULAR |
1154 apply (rule LEFT_RES_FORALL_REGULAR) |
1179 apply (rule RIGHT_RES_FORALL_REGULAR) |
1155 prefer 2 |
1180 prefer 2 |
1156 apply (assumption) |
1181 apply (assumption) |
1157 apply (erule thin_rl) |
|
1158 apply (rule allI) |
1182 apply (rule allI) |
1159 apply (rule conjI) |
|
1160 prefer 2 |
|
1161 apply (rule impI) |
1183 apply (rule impI) |
1162 |
1184 apply (rule impI) |
1163 apply (auto) |
1185 apply (assumption) |
1164 |
1186 done |
1165 apply (simp) |
|
1166 apply (thin_tac 1) |
|
1167 . |
|
1168 apply (simp) |
|
1169 |
|
1170 apply (unfold Ball_def) |
|
1171 apply (simp only: IN_RESPECTS) |
|
1172 apply (simp add: expand_fun_eq) |
|
1173 |
|
1174 |
|
1175 apply (tactic {* foo_tac' @{context} 1 *}) |
|
1176 apply (atomize(full)) |
|
1177 apply (simp) |
|
1178 prefer 2 |
|
1179 apply (simp only: IN_RESPECTS) |
|
1180 apply (simp add:list_eq_refl) |
|
1181 apply (tactic {* foo_tac' @{context} 1 *}) |
|
1182 prefer 2 |
|
1183 apply (auto) |
|
1184 sorry |
|
1185 |
1187 |
1186 ML {* |
1188 ML {* |
1187 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1189 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1188 *} |
1190 *} |
1189 |
1191 |