src/Pure/subgoal.ML
changeset 32200 2bd8ab91a426
parent 31794 71af1fd6a5e4
child 32210 a5e9d9f3e5e1
     1.1 --- a/src/Pure/subgoal.ML	Sun Jul 26 13:12:54 2009 +0200
     1.2 +++ b/src/Pure/subgoal.ML	Sun Jul 26 13:12:54 2009 +0200
     1.3 @@ -1,30 +1,28 @@
     1.4  (*  Title:      Pure/subgoal.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -Tactical operations depending on local subgoal structure.
     1.8 +Tactical operations with explicit subgoal focus, based on
     1.9 +canonical proof decomposition (similar to fix/assume/show).
    1.10  *)
    1.11  
    1.12 -signature BASIC_SUBGOAL =
    1.13 -sig
    1.14 -  val SUBPROOF:
    1.15 -    ({context: Proof.context, schematics: ctyp list * cterm list,
    1.16 -      params: cterm list, asms: cterm list, concl: cterm,
    1.17 -      prems: thm list} -> tactic) -> Proof.context -> int -> tactic
    1.18 -end
    1.19 -
    1.20  signature SUBGOAL =
    1.21  sig
    1.22 -  include BASIC_SUBGOAL
    1.23 -  val focus: Proof.context -> int -> thm ->
    1.24 -   {context: Proof.context, schematics: ctyp list * cterm list,
    1.25 -    params: cterm list, asms: cterm list, concl: cterm, prems: thm list} * thm
    1.26 -
    1.27 +  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
    1.28 +    asms: cterm list, concl: cterm, schematics: ctyp list * cterm list}
    1.29 +  val focus: Proof.context -> int -> thm -> focus * thm
    1.30 +  val retrofit: Proof.context -> (string * cterm) list -> cterm list ->
    1.31 +    int -> thm -> thm -> thm Seq.seq
    1.32 +  val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
    1.33 +  val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
    1.34  end;
    1.35  
    1.36  structure Subgoal: SUBGOAL =
    1.37  struct
    1.38  
    1.39 -(* canonical proof decomposition -- similar to fix/assume/show *)
    1.40 +(* focus *)
    1.41 +
    1.42 +type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
    1.43 +  asms: cterm list, concl: cterm, schematics: ctyp list * cterm list};
    1.44  
    1.45  fun focus ctxt i st =
    1.46    let
    1.47 @@ -35,24 +33,78 @@
    1.48      val concl = Drule.strip_imp_concl goal;
    1.49      val (prems, context) = Assumption.add_assumes asms ctxt'';
    1.50    in
    1.51 -    ({context = context, schematics = schematics, params = params,
    1.52 -      asms = asms, concl = concl, prems = prems}, Goal.init concl)
    1.53 +    ({context = context, params = params, prems = prems,
    1.54 +      asms = asms, concl = concl, schematics = schematics}, Goal.init concl)
    1.55    end;
    1.56  
    1.57 -fun SUBPROOF tac ctxt i st =
    1.58 +
    1.59 +(* lift and retrofit *)
    1.60 +
    1.61 +(*
    1.62 +     B [?'b, ?y]
    1.63 +  ----------------
    1.64 +  B ['b, y params]
    1.65 +*)
    1.66 +fun lift_import params th ctxt =
    1.67 +  let
    1.68 +    val cert = Thm.cterm_of (Thm.theory_of_thm th);
    1.69 +    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
    1.70 +
    1.71 +    val Ts = map (#T o Thm.rep_cterm) params;
    1.72 +    val ts = map Thm.term_of params;
    1.73 +
    1.74 +    val vars = rev (Term.add_vars (Thm.full_prop_of th') []);
    1.75 +    val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
    1.76 +    fun var_inst (v as (_, T)) y =
    1.77 +      (cert (Var v), cert (list_comb (Free (y, Ts ---> T), ts)));
    1.78 +    val th'' = Thm.instantiate ([], map2 var_inst vars ys) th';
    1.79 +  in (th'', ctxt'') end;
    1.80 +
    1.81 +(*
    1.82 +        [A x]
    1.83 +          :
    1.84 +      B x ==> C
    1.85 +  ------------------
    1.86 +  [!!x. A x ==> B x]
    1.87 +         :
    1.88 +         C
    1.89 +*)
    1.90 +fun lift_subgoals params asms th =
    1.91 +  let
    1.92 +    val lift = fold_rev Thm.all_name params o curry Drule.list_implies asms;
    1.93 +    val unlift =
    1.94 +      fold (Thm.elim_implies o Thm.assume) asms o
    1.95 +      Drule.forall_elim_list (map #2 params) o Thm.assume;
    1.96 +    val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
    1.97 +    val th' = fold (Thm.elim_implies o unlift) subgoals th;
    1.98 +  in (subgoals, th') end;
    1.99 +
   1.100 +fun retrofit ctxt params asms i th =
   1.101 +  let
   1.102 +    val ps = map #2 params;
   1.103 +    val res0 = Goal.conclude th;
   1.104 +    val (res1, ctxt1) = lift_import ps res0 ctxt;
   1.105 +    val (subgoals, res2) = lift_subgoals params asms res1;
   1.106 +    val result = res2
   1.107 +      |> Drule.implies_intr_list asms
   1.108 +      |> Drule.forall_intr_list ps
   1.109 +      |> Drule.implies_intr_list subgoals
   1.110 +      |> singleton (Variable.export ctxt1 ctxt);
   1.111 +  in Thm.compose_no_flatten false (result, Thm.nprems_of res0) i end;
   1.112 +
   1.113 +
   1.114 +(* tacticals *)
   1.115 +
   1.116 +fun FOCUS tac ctxt i st =
   1.117    if Thm.nprems_of st < i then Seq.empty
   1.118    else
   1.119 -    let
   1.120 -      val (args as {context, params, ...}, st') = focus ctxt i st;
   1.121 -      fun export_closed th =
   1.122 -        let
   1.123 -          val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
   1.124 -          val vs = map (Thm.dest_arg o Drule.strip_imp_concl o Thm.cprop_of) params';
   1.125 -        in Drule.forall_intr_list vs th' end;
   1.126 -      fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
   1.127 -    in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end
   1.128 +    let val (args as {context, params, asms, ...}, st') = focus ctxt i st;
   1.129 +    in Seq.lifts (retrofit context params asms i) (tac args st') st end;
   1.130 +
   1.131 +fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
   1.132  
   1.133  end;
   1.134  
   1.135 -structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
   1.136 -open BasicSubgoal;
   1.137 +val FOCUS = Subgoal.FOCUS;
   1.138 +val SUBPROOF = Subgoal.SUBPROOF;
   1.139 +