1.1 --- a/src/Pure/Isar/obtain.ML	Sat Oct 15 00:08:06 2005 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Sat Oct 15 00:08:07 2005 +0200
     1.3 @@ -2,8 +2,10 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -The 'obtain' language element -- generalized existence at the level of
     1.8 -proof texts.
     1.9 +The 'obtain' and 'guess' language elements -- generalized existence at
    1.10 +the level of proof texts: 'obtain' involves a proof that certain
    1.11 +fixes/assumes may be introduced into the present context; 'guess' is
    1.12 +similar, but derives these elements from the course of reasoning!
    1.13  
    1.14    <chain_facts>
    1.15    obtain x where "P x" <proof> ==
    1.16 @@ -15,6 +17,21 @@
    1.17      <chain_facts> show thesis <proof (insert that)>
    1.18    qed
    1.19    fix x assm (obtained) "P x"
    1.20 +
    1.21 +
    1.22 +  <chain_facts>
    1.23 +  guess x <proof body> <proof end> ==
    1.24 +
    1.25 +  {
    1.26 +    fix thesis
    1.27 +    <chain_facts> have "PROP ?guess"
    1.28 +      apply magic  -- {* turns goal into "thesis ==> thesis" (no goal marker!) *}
    1.29 +      <proof body>
    1.30 +      apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> thesis" into
    1.31 +        "GOAL ((!!x. P x ==> thesis) ==> thesis)" which is a finished goal state *}
    1.32 +      <proof end>
    1.33 +  }
    1.34 +  fix x assm (obtained) "P x"
    1.35  *)
    1.36  
    1.37  signature OBTAIN =
    1.38 @@ -25,15 +42,16 @@
    1.39    val obtain_i: (string list * typ option) list ->
    1.40      ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
    1.41      -> bool -> Proof.state -> Proof.state
    1.42 +  val guess: (string list * string option) list -> bool -> Proof.state -> Proof.state Seq.seq
    1.43 +  val guess_i: (string list * typ option) list -> bool -> Proof.state -> Proof.state Seq.seq
    1.44  end;
    1.45  
    1.46  structure Obtain: OBTAIN =
    1.47  struct
    1.48  
    1.49 +(** export_obtained **)
    1.50  
    1.51 -(** export_obtain **)
    1.52 -
    1.53 -fun export_obtain state parms rule _ cprops thm =
    1.54 +fun export_obtained state parms rule cprops thm =
    1.55    let
    1.56      val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
    1.57      val cparms = map (Thm.cterm_of thy) parms;
    1.58 @@ -50,44 +68,46 @@
    1.59      if not (null bads) then
    1.60        raise Proof.STATE ("Conclusion contains obtained parameters: " ^
    1.61          space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
    1.62 -    else if not (ObjectLogic.is_judgment thy (Logic.strip_assums_concl prop)) then
    1.63 -      raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
    1.64 +    else if not (ObjectLogic.is_judgment thy concl) then
    1.65 +      raise Proof.STATE ("Conclusion in obtained context must be object-logic judgments", state)
    1.66      else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    1.67    end;
    1.68  
    1.69  
    1.70  
    1.71 -(** obtain(_i) **)
    1.72 +(** obtain **)
    1.73 +
    1.74 +fun bind_judgment ctxt name =
    1.75 +  let val (t as _ $ Free v) =
    1.76 +    ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name
    1.77 +    |> ProofContext.bind_skolem ctxt [name]
    1.78 +  in (v, t) end;
    1.79 +
    1.80 +local
    1.81  
    1.82  val thatN = "that";
    1.83  
    1.84  fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms int state =
    1.85    let
    1.86      val _ = Proof.assert_forward_or_chain state;
    1.87 +    val ctxt = Proof.context_of state;
    1.88      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    1.89 -    val thy = Proof.theory_of state;
    1.90  
    1.91      (*obtain vars*)
    1.92 -    val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, raw_vars);
    1.93 +    val (vars, vars_ctxt) = fold_map prep_vars raw_vars ctxt;
    1.94 +    val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;
    1.95      val xs = List.concat (map fst vars);
    1.96 -    val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;
    1.97  
    1.98      (*obtain asms*)
    1.99      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
   1.100      val asm_props = List.concat (map (map fst) proppss);
   1.101 -    val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
   1.102 +    val asms = map fst (Attrib.map_specs (prep_att (Proof.theory_of state)) raw_asms) ~~ proppss;
   1.103  
   1.104      val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
   1.105  
   1.106      (*obtain statements*)
   1.107      val thesisN = Term.variant xs AutoBind.thesisN;
   1.108 -    val bind_thesis = ProofContext.bind_skolem fix_ctxt [thesisN];
   1.109 -    val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment thy thesisN);
   1.110 -    val bound_thesis_raw as (bound_thesis_name, _) =
   1.111 -      Term.dest_Free (bind_thesis (Free (thesisN, propT)));
   1.112 -    val bound_thesis_var =
   1.113 -      fold_aterms (fn Free (x, T) => (fn v => if x = bound_thesis_name then (x, T) else v)
   1.114 -        | _ => I) bound_thesis bound_thesis_raw;
   1.115 +    val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
   1.116  
   1.117      fun occs_var x = Library.get_first (fn t =>
   1.118        ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
   1.119 @@ -97,31 +117,130 @@
   1.120        List.mapPartial (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
   1.121  
   1.122      val that_prop =
   1.123 -      Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
   1.124 +      Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, thesis))
   1.125        |> Library.curry Logic.list_rename_params (map #2 parm_names);
   1.126      val obtain_prop =
   1.127        Logic.list_rename_params ([AutoBind.thesisN],
   1.128 -        Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
   1.129 +        Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
   1.130  
   1.131      fun after_qed _ _ =
   1.132        Proof.local_qed (NONE, false)
   1.133 -      #> Seq.map (`Proof.the_fact #-> (fn this =>
   1.134 +      #> Seq.map (`Proof.the_fact #-> (fn rule =>
   1.135          Proof.fix_i vars
   1.136 -        #> Proof.assm_i (export_obtain state parms this) asms));
   1.137 +        #> Proof.assm_i (K (export_obtained state parms rule)) asms));
   1.138    in
   1.139      state
   1.140      |> Proof.enter_forward
   1.141 -    |> Proof.have_i (K (K Seq.single)) [(("", []), [(obtain_prop, ([], []))])] int
   1.142 -    |> Proof.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
   1.143 +    |> Proof.have_i NONE (K (K Seq.single)) [(("", []), [(obtain_prop, ([], []))])] int
   1.144 +    |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
   1.145      |> Proof.fix_i [([thesisN], NONE)]
   1.146      |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
   1.147      |> `Proof.the_facts
   1.148      ||> Proof.chain_facts chain_facts
   1.149 -    ||> Proof.show_i after_qed [(("", []), [(bound_thesis, ([], []))])] false
   1.150 +    ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
   1.151      |-> (Proof.refine o Method.Basic o K o Method.insert) |> Seq.hd
   1.152    end;
   1.153  
   1.154 +in
   1.155 +
   1.156  val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp;
   1.157  val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
   1.158  
   1.159  end;
   1.160 +
   1.161 +
   1.162 +
   1.163 +(** guess **)
   1.164 +
   1.165 +local
   1.166 +
   1.167 +fun match_params state vars rule =
   1.168 +  let
   1.169 +    val ctxt = Proof.context_of state;
   1.170 +    val thy = Proof.theory_of state;
   1.171 +    val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
   1.172 +    val string_of_thm = ProofContext.string_of_thm ctxt;
   1.173 +
   1.174 +    val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
   1.175 +    val m = length vars;
   1.176 +    val n = length params;
   1.177 +    val _ = conditional (m > n) (fn () =>
   1.178 +      raise Proof.STATE ("More variables than parameters in obtained rule:\n" ^
   1.179 +        string_of_thm rule, state));
   1.180 +
   1.181 +    fun match ((x, SOME T), (y, U)) tyenv =
   1.182 +        ((x, T), Sign.typ_match thy (U, T) tyenv handle Type.TYPE_MATCH =>
   1.183 +          raise Proof.STATE ("Failed to match variable " ^
   1.184 +            string_of_term (Free (x, T)) ^ " against parameter " ^
   1.185 +            string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in:\n" ^
   1.186 +            string_of_thm rule, state))
   1.187 +      | match ((x, NONE), (_, U)) tyenv = ((x, U), tyenv);
   1.188 +    val (xs, tyenv) = fold_map match (vars ~~ Library.take (m, params)) Vartab.empty;
   1.189 +    val ys = Library.drop (m, params);
   1.190 +    val norm_type = Envir.norm_type tyenv;
   1.191 +
   1.192 +    val xs' = xs |> map (apsnd norm_type);
   1.193 +    val ys' =
   1.194 +      map Syntax.internal (Term.variantlist (map fst ys, map fst xs)) ~~
   1.195 +      map (norm_type o snd) ys;
   1.196 +    val instT =
   1.197 +      fold (Term.add_tvarsT o #2) params []
   1.198 +      |> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T))));
   1.199 +    val rule' = rule |> Thm.instantiate (instT, []);
   1.200 +  in (xs' @ ys', rule') end;
   1.201 +
   1.202 +fun gen_guess prep_vars raw_vars int state =
   1.203 +  let
   1.204 +    val _ = Proof.assert_forward_or_chain state;
   1.205 +    val thy = Proof.theory_of state;
   1.206 +    val ctxt = Proof.context_of state;
   1.207 +    val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
   1.208 +
   1.209 +    val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
   1.210 +    val thesis_goal = Drule.instantiate' [] [SOME (Thm.cterm_of thy thesis)] Drule.asm_rl;
   1.211 +    val varss = #1 (fold_map prep_vars raw_vars ctxt);
   1.212 +    val vars = List.concat (map (fn (xs, T) => map (rpair T) xs) varss);
   1.213 +
   1.214 +    fun unary_rule rule =
   1.215 +      (case Thm.nprems_of rule of 1 => rule
   1.216 +      | 0 => raise Proof.STATE ("Goal solved -- nothing guessed.", state)
   1.217 +      | _ => raise Proof.STATE ("Guess split into several cases:\n" ^
   1.218 +        ProofContext.string_of_thm ctxt rule, state));
   1.219 +    fun guess_context raw_rule =
   1.220 +      let
   1.221 +        val (parms, rule) = match_params state vars raw_rule;
   1.222 +        val ts = map (ProofContext.bind_skolem ctxt (map #1 parms) o Free) parms;
   1.223 +        val ps = map dest_Free ts;
   1.224 +        val asms =
   1.225 +          Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
   1.226 +          |> map (fn asm => (Library.foldl Term.betapply (Term.list_abs (ps, asm), ts), ([], [])));
   1.227 +      in
   1.228 +        Proof.fix_i (map (fn (x, T) => ([x], SOME T)) parms)
   1.229 +        #> Proof.assm_i (K (export_obtained state ts rule)) [(("", []), asms)]
   1.230 +        #> Proof.map_context (ProofContext.add_binds_i AutoBind.no_facts)
   1.231 +      end;
   1.232 +
   1.233 +    val before_qed = SOME (Method.primitive_text (fn th =>
   1.234 +      th COMP Drule.incr_indexes_wrt [] [] [] [th] Drule.triv_goal));
   1.235 +    fun after_qed _ _ =
   1.236 +      Proof.end_block
   1.237 +      #> Seq.map (`(unary_rule o Proof.the_fact) #-> guess_context);
   1.238 +  in
   1.239 +    state
   1.240 +    |> Proof.enter_forward
   1.241 +    |> Proof.begin_block
   1.242 +    |> Proof.fix_i [([AutoBind.thesisN], NONE)]
   1.243 +    |> Proof.chain_facts chain_facts
   1.244 +    |> Proof.local_goal (ProofDisplay.print_results int) (K I) (apsnd (rpair I))
   1.245 +      "guess" before_qed after_qed [(("", []), [Var (("guess", 0), propT)])]
   1.246 +    |> Proof.refine (Method.primitive_text (K thesis_goal))
   1.247 +  end;
   1.248 +
   1.249 +in
   1.250 +
   1.251 +val guess = gen_guess ProofContext.read_vars;
   1.252 +val guess_i = gen_guess ProofContext.cert_vars;
   1.253 +
   1.254 +end;
   1.255 +
   1.256 +end;