src/Pure/Isar/obtain.ML
author wenzelm
Sat Oct 15 00:08:07 2005 +0200 (2005-10-15)
changeset 17858 bc4db8cfd92f
parent 17357 ee2bdca144c7
child 17891 7a6c4d60a913
permissions -rw-r--r--
added 'guess', which derives the obtained context from the course of reasoning;
     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 ==> thesis" (no goal marker!) *}
    29       <proof body>
    30       apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> 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 Seq.seq
    46   val guess_i: (string list * typ option) list -> bool -> Proof.state -> Proof.state Seq.seq
    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_goals cprops
    61       |> Drule.forall_intr_list cparms
    62       |> Drule.forall_elim_vars (maxidx + 1);
    63     val elim_tacs = replicate (length cprops) (Tactic.etac Drule.triv_goal);
    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       ProofContext.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 (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_term = setmp show_types true (ProofContext.string_of_term ctxt);
   162     val string_of_thm = ProofContext.string_of_thm ctxt;
   163 
   164     val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
   165     val m = length vars;
   166     val n = length params;
   167     val _ = conditional (m > n) (fn () =>
   168       raise Proof.STATE ("More variables than parameters in obtained rule:\n" ^
   169         string_of_thm rule, state));
   170 
   171     fun match ((x, SOME T), (y, U)) tyenv =
   172         ((x, T), Sign.typ_match thy (U, T) tyenv handle Type.TYPE_MATCH =>
   173           raise Proof.STATE ("Failed to match variable " ^
   174             string_of_term (Free (x, T)) ^ " against parameter " ^
   175             string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in:\n" ^
   176             string_of_thm rule, state))
   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   in (xs' @ ys', rule') end;
   191 
   192 fun gen_guess prep_vars raw_vars int state =
   193   let
   194     val _ = Proof.assert_forward_or_chain state;
   195     val thy = Proof.theory_of state;
   196     val ctxt = Proof.context_of state;
   197     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
   198 
   199     val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
   200     val thesis_goal = Drule.instantiate' [] [SOME (Thm.cterm_of thy thesis)] Drule.asm_rl;
   201     val varss = #1 (fold_map prep_vars raw_vars ctxt);
   202     val vars = List.concat (map (fn (xs, T) => map (rpair T) xs) varss);
   203 
   204     fun unary_rule rule =
   205       (case Thm.nprems_of rule of 1 => rule
   206       | 0 => raise Proof.STATE ("Goal solved -- nothing guessed.", state)
   207       | _ => raise Proof.STATE ("Guess split into several cases:\n" ^
   208         ProofContext.string_of_thm ctxt rule, state));
   209     fun guess_context raw_rule =
   210       let
   211         val (parms, rule) = match_params state vars raw_rule;
   212         val ts = map (ProofContext.bind_skolem ctxt (map #1 parms) o Free) parms;
   213         val ps = map dest_Free ts;
   214         val asms =
   215           Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
   216           |> map (fn asm => (Library.foldl Term.betapply (Term.list_abs (ps, asm), ts), ([], [])));
   217       in
   218         Proof.fix_i (map (fn (x, T) => ([x], SOME T)) parms)
   219         #> Proof.assm_i (K (export_obtained state ts rule)) [(("", []), asms)]
   220         #> Proof.map_context (ProofContext.add_binds_i AutoBind.no_facts)
   221       end;
   222 
   223     val before_qed = SOME (Method.primitive_text (fn th =>
   224       th COMP Drule.incr_indexes_wrt [] [] [] [th] Drule.triv_goal));
   225     fun after_qed _ _ =
   226       Proof.end_block
   227       #> Seq.map (`(unary_rule o Proof.the_fact) #-> guess_context);
   228   in
   229     state
   230     |> Proof.enter_forward
   231     |> Proof.begin_block
   232     |> Proof.fix_i [([AutoBind.thesisN], NONE)]
   233     |> Proof.chain_facts chain_facts
   234     |> Proof.local_goal (ProofDisplay.print_results int) (K I) (apsnd (rpair I))
   235       "guess" before_qed after_qed [(("", []), [Var (("guess", 0), propT)])]
   236     |> Proof.refine (Method.primitive_text (K thesis_goal))
   237   end;
   238 
   239 in
   240 
   241 val guess = gen_guess ProofContext.read_vars;
   242 val guess_i = gen_guess ProofContext.cert_vars;
   243 
   244 end;
   245 
   246 end;