src/Pure/Isar/obtain.ML
author wenzelm
Sat Jan 21 23:02:14 2006 +0100 (2006-01-21)
changeset 18728 6790126ab5f6
parent 18693 8ae076ee5e19
child 18769 e90eb0bc0ddd
permissions -rw-r--r--
simplified type attribute;
     1 (*  Title:      Pure/Isar/obtain.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 The 'obtain' and 'guess' language elements -- generalized existence at
     6 the level of proof texts: 'obtain' involves a proof that certain
     7 fixes/assumes may be introduced into the present context; 'guess' is
     8 similar, but derives these elements from the course of reasoning!
     9 
    10   <chain_facts>
    11   obtain x where "P x" <proof> ==
    12 
    13   have "!!thesis. (!!x. P x ==> thesis) ==> thesis"
    14   proof succeed
    15     fix thesis
    16     assume that [intro?]: "!!x. P x ==> thesis"
    17     <chain_facts> show thesis <proof (insert that)>
    18   qed
    19   fix x assm (obtained) "P x"
    20 
    21 
    22   <chain_facts>
    23   guess x <proof body> <proof end> ==
    24 
    25   {
    26     fix thesis
    27     <chain_facts> have "PROP ?guess"
    28       apply magic      -- {* turns goal into "thesis ==> Goal thesis" *}
    29       <proof body>
    30       apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> Goal thesis" into
    31         "Goal ((!!x. P x ==> thesis) ==> thesis)" which is a finished goal state *}
    32       <proof end>
    33   }
    34   fix x assm (obtained) "P x"
    35 *)
    36 
    37 signature OBTAIN =
    38 sig
    39   val obtain: (string * string option) list ->
    40     ((string * Attrib.src list) * (string * (string list * string list)) list) list
    41     -> bool -> Proof.state -> Proof.state
    42   val obtain_i: (string * typ option) list ->
    43     ((string * attribute list) * (term * (term list * term list)) list) list
    44     -> bool -> Proof.state -> Proof.state
    45   val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
    46   val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
    47 end;
    48 
    49 structure Obtain: OBTAIN =
    50 struct
    51 
    52 
    53 (** obtain_export **)
    54 
    55 fun obtain_export ctxt parms rule cprops thm =
    56   let
    57     val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
    58     val cparms = map (Thm.cterm_of thy) parms;
    59 
    60     val thm' = thm
    61       |> Drule.implies_intr_protected cprops
    62       |> Drule.forall_intr_list cparms
    63       |> Drule.forall_elim_vars (maxidx + 1);
    64     val elim_tacs = replicate (length cprops) (Tactic.etac Drule.protectI);
    65 
    66     val concl = Logic.strip_assums_concl prop;
    67     val bads = parms inter (Term.term_frees concl);
    68   in
    69     if not (null bads) then
    70       error ("Conclusion contains obtained parameters: " ^
    71         space_implode " " (map (ProofContext.string_of_term ctxt) bads))
    72     else if not (ObjectLogic.is_judgment thy concl) then
    73       error "Conclusion in obtained context must be object-logic judgments"
    74     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    75   end;
    76 
    77 
    78 
    79 (** obtain **)
    80 
    81 fun bind_judgment ctxt name =
    82   let
    83     val (bind, _) = ProofContext.bind_fixes [name] ctxt;
    84     val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name);
    85   in (v, t) end;
    86 
    87 local
    88 
    89 val thatN = "that";
    90 
    91 fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms int state =
    92   let
    93     val _ = Proof.assert_forward_or_chain state;
    94     val ctxt = Proof.context_of state;
    95     val thy = Proof.theory_of state;
    96     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    97 
    98     (*obtain vars*)
    99     val (vars, vars_ctxt) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
   100     val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
   101     val xs = map #1 vars;
   102 
   103     (*obtain asms*)
   104     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
   105     val asm_props = List.concat (map (map fst) proppss);
   106     val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
   107 
   108     val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
   109 
   110     (*obtain statements*)
   111     val thesisN = Term.variant xs AutoBind.thesisN;
   112     val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
   113 
   114     fun occs_var x = Library.get_first (fn t =>
   115       Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
   116     val raw_parms = map occs_var xs;
   117     val parms = List.mapPartial I raw_parms;
   118     val parm_names =
   119       List.mapPartial (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
   120 
   121     val that_prop =
   122       Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, thesis))
   123       |> Library.curry Logic.list_rename_params (map #2 parm_names);
   124     val obtain_prop =
   125       Logic.list_rename_params ([AutoBind.thesisN],
   126         Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
   127 
   128     fun after_qed _ =
   129       Proof.local_qed (NONE, false)
   130       #> Seq.map (`Proof.the_fact #-> (fn rule =>
   131         Proof.fix_i (xs ~~ map #2 vars)
   132         #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms));
   133   in
   134     state
   135     |> Proof.enter_forward
   136     |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
   137     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
   138     |> Proof.fix_i [(thesisN, NONE)]
   139     |> Proof.assume_i
   140       [((thatN, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
   141     |> `Proof.the_facts
   142     ||> Proof.chain_facts chain_facts
   143     ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
   144     |-> (Proof.refine o Method.Basic o K o Method.insert) |> Seq.hd
   145   end;
   146 
   147 in
   148 
   149 val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
   150 val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
   151 
   152 end;
   153 
   154 
   155 
   156 (** guess **)
   157 
   158 local
   159 
   160 fun match_params ctxt vars rule =
   161   let
   162     val thy = ProofContext.theory_of ctxt;
   163     val string_of_typ = ProofContext.string_of_typ ctxt;
   164     val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
   165 
   166     fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
   167 
   168     val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
   169     val m = length vars;
   170     val n = length params;
   171     val _ = conditional (m > n)
   172       (fn () => err "More variables than parameters in obtained rule" rule);
   173 
   174     fun match ((x, SOME T), (y, U)) tyenv =
   175         ((x, T), Sign.typ_match thy (U, T) tyenv handle Type.TYPE_MATCH =>
   176           err ("Failed to match variable " ^
   177             string_of_term (Free (x, T)) ^ " against parameter " ^
   178             string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule)
   179       | match ((x, NONE), (_, U)) tyenv = ((x, U), tyenv);
   180     val (xs, tyenv) = fold_map match (vars ~~ Library.take (m, params)) Vartab.empty;
   181     val ys = Library.drop (m, params);
   182     val norm_type = Envir.norm_type tyenv;
   183 
   184     val xs' = xs |> map (apsnd norm_type);
   185     val ys' =
   186       map Syntax.internal (Term.variantlist (map fst ys, map fst xs)) ~~
   187       map (norm_type o snd) ys;
   188     val instT =
   189       fold (Term.add_tvarsT o #2) params []
   190       |> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T))));
   191     val rule' = rule |> Thm.instantiate (instT, []);
   192 
   193     val tvars = Drule.tvars_of rule';
   194     val vars = fold (remove op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule');
   195     val _ =
   196       if null tvars andalso null vars then ()
   197       else err ("Illegal schematic variable(s) " ^
   198         commas (map (string_of_typ o TVar) tvars @ map (string_of_term o Var) vars) ^ " in") rule';
   199   in (xs' @ ys', rule') end;
   200 
   201 fun inferred_type (x, _, mx) ctxt =
   202   let val ((_, T), ctxt') = ProofContext.inferred_type x ctxt
   203   in ((x, SOME T, mx), ctxt') end;
   204 
   205 fun gen_guess prep_vars raw_vars int state =
   206   let
   207     val _ = Proof.assert_forward_or_chain state;
   208     val thy = Proof.theory_of state;
   209     val ctxt = Proof.context_of state;
   210     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
   211 
   212     val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
   213     val (vars, _) = ctxt |> prep_vars (map Syntax.no_syn raw_vars) |-> fold_map inferred_type;
   214 
   215     fun check_result th =
   216       (case Thm.prems_of th of
   217         [prem] =>
   218           if Thm.concl_of th aconv thesis andalso
   219             Logic.strip_assums_concl prem aconv thesis then ()
   220           else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th)
   221       | [] => error "Goal solved -- nothing guessed."
   222       | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
   223 
   224     fun guess_context raw_rule =
   225       let
   226         val (parms, rule) = match_params ctxt (map (fn (x, T, _) => (x, T)) vars) raw_rule;
   227         val (bind, _) = ProofContext.bind_fixes (map #1 parms) ctxt;
   228         val ts = map (bind o Free) parms;
   229         val ps = map dest_Free ts;
   230         val asms =
   231           Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
   232           |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
   233         val _ = conditional (null asms) (fn () => error "Trivial result -- nothing guessed");
   234       in
   235         Proof.fix_i (map (apsnd SOME) parms)
   236         #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)]
   237         #> Proof.add_binds_i AutoBind.no_facts
   238       end;
   239 
   240     val before_qed = SOME (Method.primitive_text (Goal.conclude #> Goal.protect));
   241     fun after_qed [[res]] =
   242       (check_result res; Proof.end_block #> Seq.map (`Proof.the_fact #-> guess_context));
   243   in
   244     state
   245     |> Proof.enter_forward
   246     |> Proof.begin_block
   247     |> Proof.fix_i [(AutoBind.thesisN, NONE)]
   248     |> Proof.chain_facts chain_facts
   249     |> Proof.local_goal (ProofDisplay.print_results int) (K I) (apsnd (rpair I))
   250       "guess" before_qed after_qed [(("", []), [Var (("guess", 0), propT)])]
   251     |> Proof.refine (Method.primitive_text (K (Goal.init (Thm.cterm_of thy thesis)))) |> Seq.hd
   252   end;
   253 
   254 in
   255 
   256 val guess = gen_guess ProofContext.read_vars;
   257 val guess_i = gen_guess ProofContext.cert_vars;
   258 
   259 end;
   260 
   261 end;