1040 |
1040 |
1041 section {* Genralisation of free variables in a goal *} |
1041 section {* Genralisation of free variables in a goal *} |
1042 |
1042 |
1043 ML {* |
1043 ML {* |
1044 fun inst_spec ctrm = |
1044 fun inst_spec ctrm = |
1045 let |
1045 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
1046 val cty = ctyp_of_term ctrm |
|
1047 in |
|
1048 Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec} |
|
1049 end |
|
1050 |
1046 |
1051 fun inst_spec_tac ctrms = |
1047 fun inst_spec_tac ctrms = |
1052 EVERY' (map (dtac o inst_spec) ctrms) |
1048 EVERY' (map (dtac o inst_spec) ctrms) |
1053 |
1049 |
1054 fun abs_list (xs, t) = |
1050 fun abs_list xs trm = |
1055 fold (fn (x, T) => fn t' => HOLogic.all_const T $ (lambda (Free (x, T)) t')) xs t |
1051 fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm |
|
1052 |
|
1053 fun apply_under_Trueprop f = |
|
1054 HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop |
1056 |
1055 |
1057 fun gen_frees_tac ctxt = |
1056 fun gen_frees_tac ctxt = |
1058 SUBGOAL (fn (concl, i) => |
1057 SUBGOAL (fn (concl, i) => |
1059 let |
1058 let |
1060 val thy = ProofContext.theory_of ctxt |
1059 val thy = ProofContext.theory_of ctxt |
1061 val concl' = HOLogic.dest_Trueprop concl |
1060 val vrs = Term.add_frees concl [] |
1062 val vrs = Term.add_frees concl' [] |
|
1063 val cvrs = map (cterm_of thy o Free) vrs |
1061 val cvrs = map (cterm_of thy o Free) vrs |
1064 val concl'' = HOLogic.mk_Trueprop (abs_list (vrs, concl')) |
1062 val concl' = apply_under_Trueprop (abs_list vrs) concl |
1065 val goal = Logic.mk_implies (concl'', concl) |
1063 val goal = Logic.mk_implies (concl', concl) |
1066 val rule = Goal.prove ctxt [] [] goal |
1064 val rule = Goal.prove ctxt [] [] goal |
1067 (K ((inst_spec_tac (rev cvrs) THEN' atac) 1)) |
1065 (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) |
1068 in |
1066 in |
1069 rtac rule i |
1067 rtac rule i |
1070 end) |
1068 end) |
1071 *} |
1069 *} |
1072 |
1070 |