src/Pure/subgoal.ML
changeset 32284 d8ee8a956f19
parent 32283 3bebc195c124
child 32329 1527ff8c2dfb
     1.1 --- a/src/Pure/subgoal.ML	Thu Jul 30 12:20:43 2009 +0200
     1.2 +++ b/src/Pure/subgoal.ML	Thu Jul 30 17:54:57 2009 +0200
     1.3 @@ -65,8 +65,9 @@
     1.4    ----------------
     1.5    B ['b, y params]
     1.6  *)
     1.7 -fun lift_import params th ctxt =
     1.8 +fun lift_import idx params th ctxt =
     1.9    let
    1.10 +    val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
    1.11      val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
    1.12  
    1.13      val Ts = map (#T o Thm.rep_cterm) params;
    1.14 @@ -76,11 +77,19 @@
    1.15      val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
    1.16      val vars = rev (Term.add_vars prop []);
    1.17      val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
    1.18 -    fun var_inst (v as (_, T)) y =
    1.19 -      if member (op =) concl_vars v then (v, Free (y, T))
    1.20 -      else (v, list_comb (Free (y, Ts ---> T), ts));
    1.21 -    val th'' = Thm.certify_instantiate ([], map2 var_inst vars ys) th';
    1.22 -  in (th'', ctxt'') end;
    1.23 +
    1.24 +    fun var_inst v y =
    1.25 +      let
    1.26 +        val ((x, i), T) = v;
    1.27 +        val (U, args) =
    1.28 +          if member (op =) concl_vars v then (T, [])
    1.29 +          else (Ts ---> T, ts);
    1.30 +        val u = Free (y, U);
    1.31 +        in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
    1.32 +    val (inst1, inst2) = split_list (map (pairself (pairself cert)) (map2 var_inst vars ys));
    1.33 +
    1.34 +    val th'' = Thm.instantiate ([], inst1) th';
    1.35 +  in ((inst2, th''), ctxt'') end;
    1.36  
    1.37  (*
    1.38         [x, A x]
    1.39 @@ -103,17 +112,19 @@
    1.40  
    1.41  fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
    1.42    let
    1.43 +    val idx = Thm.maxidx_of st0 + 1;
    1.44      val ps = map #2 params;
    1.45 -    val (st2, ctxt2) = lift_import ps st1 ctxt1;
    1.46 +    val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
    1.47      val (subgoals, st3) = lift_subgoals params asms st2;
    1.48      val result = st3
    1.49        |> Goal.conclude
    1.50        |> Drule.implies_intr_list asms
    1.51        |> Drule.forall_intr_list ps
    1.52        |> Drule.implies_intr_list subgoals
    1.53 -      |> singleton (Variable.export ctxt2 ctxt0)
    1.54 -      |> Drule.zero_var_indexes
    1.55 -      |> Drule.incr_indexes st0;
    1.56 +      |> fold_rev (Thm.forall_intr o #1) subgoal_inst
    1.57 +      |> fold (Thm.forall_elim o #2) subgoal_inst
    1.58 +      |> Thm.adjust_maxidx_thm idx
    1.59 +      |> singleton (Variable.export ctxt2 ctxt0);
    1.60    in Thm.compose_no_flatten false (result, Thm.nprems_of st1) i st0 end;
    1.61  
    1.62