wenzelm@20210: (*  Title:      Pure/subgoal.ML
wenzelm@20210:     Author:     Makarius
wenzelm@20210: 
wenzelm@32281: Tactical operations with explicit subgoal focus, based on canonical
wenzelm@32281: proof decomposition.  The "visible" part of the text within the
wenzelm@32281: context is fixed, the remaining goal may be schematic.
wenzelm@20210: *)
wenzelm@20210: 
wenzelm@20210: signature SUBGOAL =
wenzelm@20210: sig
wenzelm@32200:   type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
wenzelm@32281:     asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
wenzelm@32281:   val focus_params: Proof.context -> int -> thm -> focus * thm
wenzelm@32281:   val focus_prems: Proof.context -> int -> thm -> focus * thm
wenzelm@32200:   val focus: Proof.context -> int -> thm -> focus * thm
wenzelm@32210:   val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
wenzelm@32200:     int -> thm -> thm -> thm Seq.seq
wenzelm@32281:   val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
wenzelm@32281:   val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
wenzelm@32200:   val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
wenzelm@32200:   val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
wenzelm@20210: end;
wenzelm@20210: 
wenzelm@20210: structure Subgoal: SUBGOAL =
wenzelm@20210: struct
wenzelm@20210: 
wenzelm@32200: (* focus *)
wenzelm@32200: 
wenzelm@32200: type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
wenzelm@32281:   asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
wenzelm@20210: 
wenzelm@32281: fun gen_focus (do_prems, do_concl) ctxt i raw_st =
wenzelm@20210:   let
wenzelm@32281:     val st = Simplifier.norm_hhf_protect raw_st;
wenzelm@32281:     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
wenzelm@42495:     val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
wenzelm@32281: 
wenzelm@32213:     val (asms, concl) =
wenzelm@32281:       if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
wenzelm@32281:       else ([], goal);
wenzelm@32281:     val text = asms @ (if do_concl then [concl] else []);
wenzelm@32281: 
wenzelm@32281:     val ((_, schematic_terms), ctxt3) =
wenzelm@32281:       Variable.import_inst true (map Thm.term_of text) ctxt2
wenzelm@32281:       |>> Thm.certify_inst (Thm.theory_of_thm raw_st);
wenzelm@32281: 
wenzelm@32281:     val schematics = (schematic_types, schematic_terms);
wenzelm@32281:     val asms' = map (Thm.instantiate_cterm schematics) asms;
wenzelm@32281:     val concl' = Thm.instantiate_cterm schematics concl;
wenzelm@32281:     val (prems, context) = Assumption.add_assumes asms' ctxt3;
wenzelm@20210:   in
wenzelm@32200:     ({context = context, params = params, prems = prems,
wenzelm@32281:       asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
wenzelm@20210:   end;
wenzelm@20210: 
wenzelm@32281: val focus_params = gen_focus (false, false);
wenzelm@32281: val focus_prems = gen_focus (true, false);
wenzelm@32281: val focus = gen_focus (true, true);
wenzelm@32213: 
wenzelm@32200: 
wenzelm@32200: (* lift and retrofit *)
wenzelm@32200: 
wenzelm@32200: (*
wenzelm@32200:      B [?'b, ?y]
wenzelm@32200:   ----------------
wenzelm@32200:   B ['b, y params]
wenzelm@32200: *)
wenzelm@32284: fun lift_import idx params th ctxt =
wenzelm@32200:   let
wenzelm@42360:     val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
wenzelm@32200:     val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
wenzelm@32200: 
wenzelm@32200:     val Ts = map (#T o Thm.rep_cterm) params;
wenzelm@32200:     val ts = map Thm.term_of params;
wenzelm@32200: 
wenzelm@32281:     val prop = Thm.full_prop_of th';
wenzelm@32281:     val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
wenzelm@32281:     val vars = rev (Term.add_vars prop []);
wenzelm@32200:     val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
wenzelm@32284: 
wenzelm@32284:     fun var_inst v y =
wenzelm@32284:       let
wenzelm@32284:         val ((x, i), T) = v;
wenzelm@32284:         val (U, args) =
wenzelm@32284:           if member (op =) concl_vars v then (T, [])
wenzelm@32284:           else (Ts ---> T, ts);
wenzelm@32284:         val u = Free (y, U);
wenzelm@32284:         in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
wenzelm@32284:     val (inst1, inst2) = split_list (map (pairself (pairself cert)) (map2 var_inst vars ys));
wenzelm@32284: 
wenzelm@32284:     val th'' = Thm.instantiate ([], inst1) th';
wenzelm@32284:   in ((inst2, th''), ctxt'') end;
wenzelm@32200: 
wenzelm@32200: (*
wenzelm@32281:        [x, A x]
wenzelm@32200:           :
wenzelm@32281:        B x ==> C
wenzelm@32200:   ------------------
wenzelm@32200:   [!!x. A x ==> B x]
wenzelm@32281:           :
wenzelm@32281:           C
wenzelm@32200: *)
wenzelm@32200: fun lift_subgoals params asms th =
wenzelm@32200:   let
wenzelm@32329:     fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
wenzelm@32200:     val unlift =
wenzelm@32200:       fold (Thm.elim_implies o Thm.assume) asms o
wenzelm@32200:       Drule.forall_elim_list (map #2 params) o Thm.assume;
wenzelm@32200:     val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
wenzelm@32200:     val th' = fold (Thm.elim_implies o unlift) subgoals th;
wenzelm@32200:   in (subgoals, th') end;
wenzelm@32200: 
wenzelm@32213: fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
wenzelm@32200:   let
wenzelm@32284:     val idx = Thm.maxidx_of st0 + 1;
wenzelm@32200:     val ps = map #2 params;
wenzelm@32284:     val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
wenzelm@32213:     val (subgoals, st3) = lift_subgoals params asms st2;
wenzelm@32213:     val result = st3
wenzelm@32213:       |> Goal.conclude
wenzelm@32200:       |> Drule.implies_intr_list asms
wenzelm@32200:       |> Drule.forall_intr_list ps
wenzelm@32200:       |> Drule.implies_intr_list subgoals
wenzelm@32284:       |> fold_rev (Thm.forall_intr o #1) subgoal_inst
wenzelm@32284:       |> fold (Thm.forall_elim o #2) subgoal_inst
wenzelm@32284:       |> Thm.adjust_maxidx_thm idx
wenzelm@32284:       |> singleton (Variable.export ctxt2 ctxt0);
wenzelm@34075:   in Thm.bicompose false (false, result, Thm.nprems_of st1) i st0 end;
wenzelm@32200: 
wenzelm@32200: 
wenzelm@32200: (* tacticals *)
wenzelm@32200: 
wenzelm@32281: fun GEN_FOCUS flags tac ctxt i st =
wenzelm@20210:   if Thm.nprems_of st < i then Seq.empty
wenzelm@20210:   else
wenzelm@32329:     let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
wenzelm@32329:     in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
wenzelm@32200: 
wenzelm@32281: val FOCUS_PARAMS = GEN_FOCUS (false, false);
wenzelm@32281: val FOCUS_PREMS = GEN_FOCUS (true, false);
wenzelm@32281: val FOCUS = GEN_FOCUS (true, true);
wenzelm@32213: 
wenzelm@49845: fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
wenzelm@20210: 
wenzelm@20210: end;
wenzelm@20210: 
wenzelm@32200: val SUBPROOF = Subgoal.SUBPROOF;
wenzelm@32200: