src/Pure/Isar/obtain.ML
author wenzelm
Thu Nov 10 20:57:21 2005 +0100 (2005-11-10)
changeset 18151 32538cf750ca
parent 18124 a310c78298f9
child 18185 9d51fad6bb1f
permissions -rw-r--r--
guess: Seq.hd;
Term.find_free;
     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 list * 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 list * typ option) list ->
    43     ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
    44     -> bool -> Proof.state -> Proof.state
    45   val guess: (string list * string option) list -> bool -> Proof.state -> Proof.state
    46   val guess_i: (string list * typ option) list -> bool -> Proof.state -> Proof.state
    47 end;
    48 
    49 structure Obtain: OBTAIN =
    50 struct
    51 
    52 (** export_obtained **)
    53 
    54 fun export_obtained state parms rule cprops thm =
    55   let
    56     val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
    57     val cparms = map (Thm.cterm_of thy) parms;
    58 
    59     val thm' = thm
    60       |> Drule.implies_intr_protected cprops
    61       |> Drule.forall_intr_list cparms
    62       |> Drule.forall_elim_vars (maxidx + 1);
    63     val elim_tacs = replicate (length cprops) (Tactic.etac Drule.protectI);
    64 
    65     val concl = Logic.strip_assums_concl prop;
    66     val bads = parms inter (Term.term_frees concl);
    67   in
    68     if not (null bads) then
    69       raise Proof.STATE ("Conclusion contains obtained parameters: " ^
    70         space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
    71     else if not (ObjectLogic.is_judgment thy concl) then
    72       raise Proof.STATE ("Conclusion in obtained context must be object-logic judgments", state)
    73     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    74   end;
    75 
    76 
    77 
    78 (** obtain **)
    79 
    80 fun bind_judgment ctxt name =
    81   let val (t as _ $ Free v) =
    82     ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name
    83     |> ProofContext.bind_skolem ctxt [name]
    84   in (v, t) end;
    85 
    86 local
    87 
    88 val thatN = "that";
    89 
    90 fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms int state =
    91   let
    92     val _ = Proof.assert_forward_or_chain state;
    93     val ctxt = Proof.context_of state;
    94     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    95 
    96     (*obtain vars*)
    97     val (vars, vars_ctxt) = fold_map prep_vars raw_vars ctxt;
    98     val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;
    99     val xs = List.concat (map fst vars);
   100 
   101     (*obtain asms*)
   102     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
   103     val asm_props = List.concat (map (map fst) proppss);
   104     val asms = map fst (Attrib.map_specs (prep_att (Proof.theory_of state)) raw_asms) ~~ proppss;
   105 
   106     val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
   107 
   108     (*obtain statements*)
   109     val thesisN = Term.variant xs AutoBind.thesisN;
   110     val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
   111 
   112     fun occs_var x = Library.get_first (fn t =>
   113       Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
   114     val raw_parms = map occs_var xs;
   115     val parms = List.mapPartial I raw_parms;
   116     val parm_names =
   117       List.mapPartial (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
   118 
   119     val that_prop =
   120       Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, thesis))
   121       |> Library.curry Logic.list_rename_params (map #2 parm_names);
   122     val obtain_prop =
   123       Logic.list_rename_params ([AutoBind.thesisN],
   124         Term.list_all_free ([thesis_var], Logic.mk_implies (that_prop, thesis)));
   125 
   126     fun after_qed _ =
   127       Proof.local_qed (NONE, false)
   128       #> Seq.map (`Proof.the_fact #-> (fn rule =>
   129         Proof.fix_i vars
   130         #> Proof.assm_i (K (export_obtained state parms rule)) asms));
   131   in
   132     state
   133     |> Proof.enter_forward
   134     |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
   135     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
   136     |> Proof.fix_i [([thesisN], NONE)]
   137     |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
   138     |> `Proof.the_facts
   139     ||> Proof.chain_facts chain_facts
   140     ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
   141     |-> (Proof.refine o Method.Basic o K o Method.insert) |> Seq.hd
   142   end;
   143 
   144 in
   145 
   146 val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp;
   147 val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
   148 
   149 end;
   150 
   151 
   152 
   153 (** guess **)
   154 
   155 local
   156 
   157 fun match_params state vars rule =
   158   let
   159     val ctxt = Proof.context_of state;
   160     val thy = Proof.theory_of state;
   161     val string_of_typ = ProofContext.string_of_typ ctxt;
   162     val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
   163 
   164     fun err msg th = raise Proof.STATE (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th, state);
   165 
   166     val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
   167     val m = length vars;
   168     val n = length params;
   169     val _ = conditional (m > n)
   170       (fn () => err "More variables than parameters in obtained rule" rule);
   171 
   172     fun match ((x, SOME T), (y, U)) tyenv =
   173         ((x, T), Sign.typ_match thy (U, T) tyenv handle Type.TYPE_MATCH =>
   174           err ("Failed to match variable " ^
   175             string_of_term (Free (x, T)) ^ " against parameter " ^
   176             string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule)
   177       | match ((x, NONE), (_, U)) tyenv = ((x, U), tyenv);
   178     val (xs, tyenv) = fold_map match (vars ~~ Library.take (m, params)) Vartab.empty;
   179     val ys = Library.drop (m, params);
   180     val norm_type = Envir.norm_type tyenv;
   181 
   182     val xs' = xs |> map (apsnd norm_type);
   183     val ys' =
   184       map Syntax.internal (Term.variantlist (map fst ys, map fst xs)) ~~
   185       map (norm_type o snd) ys;
   186     val instT =
   187       fold (Term.add_tvarsT o #2) params []
   188       |> map (TVar #> (fn T => (Thm.ctyp_of thy T, Thm.ctyp_of thy (norm_type T))));
   189     val rule' = rule |> Thm.instantiate (instT, []);
   190 
   191     val tvars = Drule.tvars_of rule';
   192     val vars = fold (remove op =) (Term.add_vars (Thm.concl_of rule') []) (Drule.vars_of rule');
   193     val _ =
   194       if null tvars andalso null vars then ()
   195       else err ("Illegal schematic variable(s) " ^
   196         commas (map (string_of_typ o TVar) tvars @ map (string_of_term o Var) vars) ^ " in") rule';
   197   in (xs' @ ys', rule') end;
   198 
   199 fun gen_guess prep_vars raw_vars int state =
   200   let
   201     val _ = Proof.assert_forward_or_chain state;
   202     val thy = Proof.theory_of state;
   203     val ctxt = Proof.context_of state;
   204     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
   205 
   206     val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
   207     val varss = #1 (fold_map prep_vars raw_vars ctxt);
   208     val vars = List.concat (map (fn (xs, T) => map (rpair T) xs) varss);
   209 
   210     fun check_result th =
   211       (case Thm.prems_of th of
   212         [prem] =>
   213           if Thm.concl_of th aconv thesis andalso
   214             Logic.strip_assums_concl prem aconv thesis then ()
   215           else raise Proof.STATE ("Guessed a different clause:\n" ^
   216             ProofContext.string_of_thm ctxt th, state)
   217       | [] => raise Proof.STATE ("Goal solved -- nothing guessed.", state)
   218       | _ => raise Proof.STATE ("Guess split into several cases:\n" ^
   219         ProofContext.string_of_thm ctxt th, state));
   220 
   221     fun guess_context raw_rule =
   222       let
   223         val (parms, rule) = match_params state vars raw_rule;
   224         val ts = map (ProofContext.bind_skolem ctxt (map #1 parms) o Free) parms;
   225         val ps = map dest_Free ts;
   226         val asms =
   227           Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
   228           |> map (fn asm => (Library.foldl Term.betapply (Term.list_abs (ps, asm), ts), ([], [])));
   229         val _ = conditional (null asms) (fn () =>
   230           raise Proof.STATE ("Trivial result -- nothing guessed", state));
   231       in
   232         Proof.fix_i (map (fn (x, T) => ([x], SOME T)) parms)
   233         #> Proof.assm_i (K (export_obtained state ts rule)) [(("", []), asms)]
   234         #> Proof.add_binds_i AutoBind.no_facts
   235       end;
   236 
   237     val before_qed = SOME (Method.primitive_text (Goal.conclude #> Goal.protect));
   238     fun after_qed [[res]] =
   239       (check_result res; Proof.end_block #> Seq.map (`Proof.the_fact #-> guess_context));
   240   in
   241     state
   242     |> Proof.enter_forward
   243     |> Proof.begin_block
   244     |> Proof.fix_i [([AutoBind.thesisN], NONE)]
   245     |> Proof.chain_facts chain_facts
   246     |> Proof.local_goal (ProofDisplay.print_results int) (K I) (apsnd (rpair I))
   247       "guess" before_qed after_qed [(("", []), [Var (("guess", 0), propT)])]
   248     |> Proof.refine (Method.primitive_text (K (Goal.init (Thm.cterm_of thy thesis)))) |> Seq.hd
   249   end;
   250 
   251 in
   252 
   253 val guess = gen_guess ProofContext.read_vars;
   254 val guess_i = gen_guess ProofContext.cert_vars;
   255 
   256 end;
   257 
   258 end;