src/Pure/Isar/obtain.ML
changeset 17891 7a6c4d60a913
parent 17858 bc4db8cfd92f
child 17974 5b54db4a44ee
     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Oct 18 17:59:23 2005 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Oct 18 17:59:24 2005 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    {
     1.5      fix thesis
     1.6      <chain_facts> have "PROP ?guess"
     1.7 -      apply magic  -- {* turns goal into "thesis ==> thesis" (no goal marker!) *}
     1.8 +      apply magic      -- {* turns goal into "thesis ==> thesis" (no goal marker!) *}
     1.9        <proof body>
    1.10        apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> thesis" into
    1.11          "GOAL ((!!x. P x ==> thesis) ==> thesis)" which is a finished goal state *}
    1.12 @@ -158,22 +158,22 @@
    1.13    let
    1.14      val ctxt = Proof.context_of state;
    1.15      val thy = Proof.theory_of state;
    1.16 +    val string_of_typ = ProofContext.string_of_typ ctxt;
    1.17      val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
    1.18 -    val string_of_thm = ProofContext.string_of_thm ctxt;
    1.19 +
    1.20 +    fun err msg th = raise Proof.STATE (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th, state);
    1.21  
    1.22      val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
    1.23      val m = length vars;
    1.24      val n = length params;
    1.25 -    val _ = conditional (m > n) (fn () =>
    1.26 -      raise Proof.STATE ("More variables than parameters in obtained rule:\n" ^
    1.27 -        string_of_thm rule, state));
    1.28 +    val _ = conditional (m > n)
    1.29 +      (fn () => err "More variables than parameters in obtained rule" rule);
    1.30  
    1.31      fun match ((x, SOME T), (y, U)) tyenv =
    1.32          ((x, T), Sign.typ_match thy (U, T) tyenv handle Type.TYPE_MATCH =>
    1.33 -          raise Proof.STATE ("Failed to match variable " ^
    1.34 +          err ("Failed to match variable " ^
    1.35              string_of_term (Free (x, T)) ^ " against parameter " ^
    1.36 -            string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in:\n" ^
    1.37 -            string_of_thm rule, state))
    1.38 +            string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule)
    1.39        | match ((x, NONE), (_, U)) tyenv = ((x, U), tyenv);
    1.40      val (xs, tyenv) = fold_map match (vars ~~ Library.take (m, params)) Vartab.empty;
    1.41      val ys = Library.drop (m, params);
    1.42 @@ -187,6 +187,13 @@
    1.43        fold (Term.add_tvarsT o #2) params []
    1.44        |> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T))));
    1.45      val rule' = rule |> Thm.instantiate (instT, []);
    1.46 +
    1.47 +    val tvars = Drule.tvars_of rule';
    1.48 +    val vars = fold (remove op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule');
    1.49 +    val _ =
    1.50 +      if null tvars andalso null vars then ()
    1.51 +      else err ("Illegal schematic variable(s) " ^
    1.52 +        commas (map (string_of_typ o TVar) tvars @ map (string_of_term o Var) vars) ^ " in") rule';
    1.53    in (xs' @ ys', rule') end;
    1.54  
    1.55  fun gen_guess prep_vars raw_vars int state =
    1.56 @@ -206,6 +213,7 @@
    1.57        | 0 => raise Proof.STATE ("Goal solved -- nothing guessed.", state)
    1.58        | _ => raise Proof.STATE ("Guess split into several cases:\n" ^
    1.59          ProofContext.string_of_thm ctxt rule, state));
    1.60 +
    1.61      fun guess_context raw_rule =
    1.62        let
    1.63          val (parms, rule) = match_params state vars raw_rule;
    1.64 @@ -221,10 +229,13 @@
    1.65        end;
    1.66  
    1.67      val before_qed = SOME (Method.primitive_text (fn th =>
    1.68 -      th COMP Drule.incr_indexes_wrt [] [] [] [th] Drule.triv_goal));
    1.69 +      if Thm.concl_of th aconv thesis then
    1.70 +        th COMP Drule.incr_indexes_wrt [] [] [] [th] Drule.triv_goal
    1.71 +      else raise Proof.STATE ("Guessed a different clause:\n" ^
    1.72 +          ProofContext.string_of_thm ctxt th, state)));
    1.73      fun after_qed _ _ =
    1.74        Proof.end_block
    1.75 -      #> Seq.map (`(unary_rule o Proof.the_fact) #-> guess_context);
    1.76 +      #> Seq.map (`(Proof.the_fact #> unary_rule) #-> guess_context);
    1.77    in
    1.78      state
    1.79      |> Proof.enter_forward