equal
deleted
inserted
replaced
425 val v = Free (x', T); |
425 val v = Free (x', T); |
426 val t' = subst_bound (v, t); |
426 val t' = subst_bound (v, t); |
427 val rec_term = regularise t' rty rel lthy2; |
427 val rec_term = regularise t' rty rel lthy2; |
428 val lam_term = Term.lambda_name (x, v) rec_term |
428 val lam_term = Term.lambda_name (x, v) rec_term |
429 in |
429 in |
430 Const(@{const_name "All"}, at) $ lam_term |
430 Const(@{const_name "Ex"}, at) $ lam_term |
431 end |
431 end |
432 | ((Const (@{const_name "Ex"}, at)) $ P) => |
432 | ((Const (@{const_name "Ex"}, at)) $ P) => |
433 let |
433 let |
434 val (_, [al, _]) = dest_Type (fastype_of P); |
434 val (_, [al, _]) = dest_Type (fastype_of P); |
435 val ([x], lthy2) = Variable.variant_fixes [""] lthy; |
435 val ([x], lthy2) = Variable.variant_fixes [""] lthy; |
1145 apply (tactic {* foo_tac' @{context} 1 *}) |
1145 apply (tactic {* foo_tac' @{context} 1 *}) |
1146 done |
1146 done |
1147 |
1147 |
1148 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *} |
1148 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *} |
1149 |
1149 |
1150 (* TODO: the following 2 lemmas should go to quotscript.thy after all are done *) |
|
1151 lemma RIGHT_RES_FORALL_REGULAR: |
|
1152 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
|
1153 shows "All P ==> Ball R Q" |
|
1154 using a |
|
1155 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
|
1156 done |
|
1157 |
|
1158 lemma LEFT_RES_FORALL_REGULAR: |
|
1159 assumes a: "!x. (R x \<and> (Q x --> P x))" |
|
1160 shows "Ball R Q ==> All P" |
|
1161 using a |
|
1162 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
|
1163 done |
|
1164 |
|
1165 prove {* |
1150 prove {* |
1166 Logic.mk_implies |
1151 Logic.mk_implies |
1167 ((prop_of li), |
1152 ((prop_of li), |
1168 (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
1153 (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
1169 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
1154 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
1174 apply (rule allI) |
1159 apply (rule allI) |
1175 apply (rule impI) |
1160 apply (rule impI) |
1176 apply (rule impI) |
1161 apply (rule impI) |
1177 apply (assumption) |
1162 apply (assumption) |
1178 done |
1163 done |
|
1164 |
|
1165 ML {* val li = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
|
1166 |
|
1167 prove card1_suc_r: {* |
|
1168 Logic.mk_implies |
|
1169 ((prop_of li), |
|
1170 (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
|
1171 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
|
1172 apply (simp only: equiv_res_exists[OF equiv_list_eq]) |
|
1173 done |
|
1174 |
|
1175 thm card1_suc |
|
1176 ML {* @{thm card1_suc_r} OF [li] *} |
1179 |
1177 |
1180 ML {* |
1178 ML {* |
1181 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1179 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1182 *} |
1180 *} |
1183 |
1181 |
1232 |
1230 |
1233 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
1231 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
1234 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
1232 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
1235 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
1233 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
1236 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
1234 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
1237 (*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} @{context}) *} |
1235 thm card1_suc_r |
1238 local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) |
1236 ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc_r} @{context}) *} |
|
1237 (*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) |
1239 |
1238 |
1240 thm m1_lift |
1239 thm m1_lift |
1241 thm leqi4_lift |
1240 thm leqi4_lift |
1242 thm leqi5_lift |
1241 thm leqi5_lift |
1243 thm m2_lift |
1242 thm m2_lift |