src/Pure/Isar/obtain.ML
changeset 19779 5c77dfb74c7b
parent 19585 70a1ce3b23ae
child 19844 2c1fdc397ded
     1.1 --- a/src/Pure/Isar/obtain.ML	Mon Jun 05 21:54:24 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Mon Jun 05 21:54:25 2006 +0200
     1.3 @@ -173,7 +173,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun match_params ctxt vars rule =
     1.8 +fun unify_params ctxt vars raw_rule =
     1.9    let
    1.10      val thy = ProofContext.theory_of ctxt;
    1.11      val string_of_typ = ProofContext.string_of_typ ctxt;
    1.12 @@ -181,26 +181,27 @@
    1.13  
    1.14      fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
    1.15  
    1.16 +    val maxidx = fold (Term.maxidx_typ o snd) vars ~1;
    1.17 +    val rule = Thm.incr_indexes (maxidx + 1) raw_rule;
    1.18 +
    1.19      val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
    1.20      val m = length vars;
    1.21      val n = length params;
    1.22 -    val _ = conditional (m > n)
    1.23 -      (fn () => err "More variables than parameters in obtained rule" rule);
    1.24 +    val _ = m <= n orelse err "More variables than parameters in obtained rule" rule;
    1.25  
    1.26 -    fun match ((x, SOME T), (y, U)) tyenv =
    1.27 -        ((x, T), Sign.typ_match thy (U, T) tyenv handle Type.TYPE_MATCH =>
    1.28 -          err ("Failed to match variable " ^
    1.29 -            string_of_term (Free (x, T)) ^ " against parameter " ^
    1.30 -            string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule)
    1.31 -      | match ((x, NONE), (_, U)) tyenv = ((x, U), tyenv);
    1.32 -    val (xs, tyenv) = fold_map match (vars ~~ Library.take (m, params)) Vartab.empty;
    1.33 -    val ys = Library.drop (m, params);
    1.34 +    fun unify ((x, T), (y, U)) (tyenv, max) = Sign.typ_unify thy (T, U) (tyenv, max)
    1.35 +      handle Type.TUNIFY =>
    1.36 +        err ("Failed to unify variable " ^
    1.37 +          string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^
    1.38 +          string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
    1.39 +    val (tyenv, _) = fold unify (vars ~~ Library.take (m, params))
    1.40 +      (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
    1.41      val norm_type = Envir.norm_type tyenv;
    1.42  
    1.43 -    val xs' = xs |> map (apsnd norm_type);
    1.44 -    val ys' =
    1.45 -      map Syntax.internal (Term.variantlist (map fst ys, map fst xs)) ~~
    1.46 -      map (norm_type o snd) ys;
    1.47 +    val xs = map (apsnd norm_type) vars;
    1.48 +    val ys = map (apsnd norm_type) (Library.drop (m, params));
    1.49 +    val ys' = map Syntax.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys;
    1.50 +
    1.51      val instT =
    1.52        fold (Term.add_tvarsT o #2) params []
    1.53        |> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T))));
    1.54 @@ -212,11 +213,15 @@
    1.55        if null tvars andalso null vars then ()
    1.56        else err ("Illegal schematic variable(s) " ^
    1.57          commas (map (string_of_typ o TVar) tvars @ map (string_of_term o Var) vars) ^ " in") rule';
    1.58 -  in (xs' @ ys', rule') end;
    1.59 +  in (xs @ ys', rule') end;
    1.60  
    1.61  fun inferred_type (x, _, mx) ctxt =
    1.62    let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt
    1.63 -  in ((x, SOME T, mx), ctxt') end;
    1.64 +  in ((x, T, mx), ctxt') end;
    1.65 +
    1.66 +fun polymorphic (vars, ctxt) =
    1.67 +  let val Ts = map Logic.dest_type (ProofContext.polymorphic ctxt (map (Logic.mk_type o #2) vars))
    1.68 +  in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end;
    1.69  
    1.70  fun gen_guess prep_vars raw_vars int state =
    1.71    let
    1.72 @@ -226,7 +231,8 @@
    1.73      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    1.74  
    1.75      val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
    1.76 -    val (vars, _) = ctxt |> prep_vars (map Syntax.no_syn raw_vars) |-> fold_map inferred_type;
    1.77 +    val vars = ctxt |> prep_vars (map Syntax.no_syn raw_vars)
    1.78 +      |-> fold_map inferred_type |> polymorphic;
    1.79  
    1.80      fun check_result th =
    1.81        (case Thm.prems_of th of
    1.82 @@ -237,33 +243,37 @@
    1.83        | [] => error "Goal solved -- nothing guessed."
    1.84        | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
    1.85  
    1.86 -    fun guess_context raw_rule =
    1.87 +    fun guess_context [_, raw_rule] =
    1.88        let
    1.89 -        val (parms, rule) = match_params ctxt (map (fn (x, T, _) => (x, T)) vars) raw_rule;
    1.90 +        val (parms, rule) = unify_params ctxt (map #1 vars) raw_rule;
    1.91          val (bind, _) = ProofContext.bind_fixes (map #1 parms) ctxt;
    1.92          val ts = map (bind o Free) parms;
    1.93          val ps = map dest_Free ts;
    1.94          val asms =
    1.95            Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
    1.96            |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
    1.97 -        val _ = conditional (null asms) (fn () => error "Trivial result -- nothing guessed");
    1.98 +        val _ = not (null asms) orelse error "Trivial result -- nothing guessed";
    1.99        in
   1.100          Proof.fix_i (map (apsnd SOME) parms)
   1.101          #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)]
   1.102          #> Proof.add_binds_i AutoBind.no_facts
   1.103        end;
   1.104  
   1.105 -    val before_qed = SOME (Method.primitive_text (Goal.conclude #> Goal.protect));
   1.106 -    fun after_qed [[res]] =
   1.107 -      (check_result res; Proof.end_block #> Seq.map (`Proof.the_fact #-> guess_context));
   1.108 +    val goal = Var (("guess", 0), propT);
   1.109 +    fun print_result ctxt' (k, [(s, [_, th])]) =
   1.110 +      ProofDisplay.print_results int ctxt' (k, [(s, [th])]);
   1.111 +    val before_qed = SOME (Method.primitive_text (Goal.conclude #> (fn th =>
   1.112 +      Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
   1.113 +    fun after_qed [[_, res]] =
   1.114 +      (check_result res; Proof.end_block #> Seq.map (`Proof.the_facts #-> guess_context));
   1.115    in
   1.116      state
   1.117      |> Proof.enter_forward
   1.118      |> Proof.begin_block
   1.119      |> Proof.fix_i [(AutoBind.thesisN, NONE)]
   1.120      |> Proof.chain_facts chain_facts
   1.121 -    |> Proof.local_goal (ProofDisplay.print_results int) (K I) (apsnd (rpair I))
   1.122 -      "guess" before_qed after_qed [(("", []), [Var (("guess", 0), propT)])]
   1.123 +    |> Proof.local_goal print_result (K I) (apsnd (rpair I))
   1.124 +      "guess" before_qed after_qed [(("", []), [Logic.mk_term goal, goal])]
   1.125      |> Proof.refine (Method.primitive_text (K (Goal.init (Thm.cterm_of thy thesis)))) |> Seq.hd
   1.126    end;
   1.127