29 type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, |
29 type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, |
30 asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}; |
30 asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}; |
31 |
31 |
32 fun gen_focus (do_prems, do_concl) ctxt i raw_st = |
32 fun gen_focus (do_prems, do_concl) ctxt i raw_st = |
33 let |
33 let |
34 val st = Simplifier.norm_hhf_protect ctxt raw_st; |
34 val st = raw_st |
|
35 |> Thm.transfer (Proof_Context.theory_of ctxt) |
|
36 |> Simplifier.norm_hhf_protect ctxt; |
35 val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt; |
37 val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt; |
36 val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1; |
38 val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1; |
37 |
39 |
38 val (asms, concl) = |
40 val (asms, concl) = |
39 if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal) |
41 if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal) |
40 else ([], goal); |
42 else ([], goal); |
41 val text = asms @ (if do_concl then [concl] else []); |
43 val text = asms @ (if do_concl then [concl] else []); |
42 |
44 |
43 val ((_, schematic_terms), ctxt3) = |
45 val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2; |
44 Variable.import_inst true (map Thm.term_of text) ctxt2 |
46 val (_, schematic_terms) = Thm.certify_inst ctxt3 inst; |
45 |>> Thm.certify_inst (Thm.theory_of_thm raw_st); |
|
46 |
47 |
47 val schematics = (schematic_types, schematic_terms); |
48 val schematics = (schematic_types, schematic_terms); |
48 val asms' = map (Thm.instantiate_cterm schematics) asms; |
49 val asms' = map (Thm.instantiate_cterm schematics) asms; |
49 val concl' = Thm.instantiate_cterm schematics concl; |
50 val concl' = Thm.instantiate_cterm schematics concl; |
50 val (prems, context) = Assumption.add_assumes asms' ctxt3; |
51 val (prems, context) = Assumption.add_assumes asms' ctxt3; |