src/Pure/Isar/obtain.ML
author skalberg
Sun Feb 13 17:15:14 2005 +0100 (2005-02-13)
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15570 8d8c70b41bab
permissions -rw-r--r--
Deleted Library.option type.
     1 (*  Title:      Pure/Isar/obtain.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 The 'obtain' language element -- generalized existence at the level of
     6 proof texts.
     7 
     8   <chain_facts>
     9   obtain x where "P x" <proof> ==
    10 
    11   have "!!thesis. (!!x. P x ==> thesis) ==> thesis"
    12   proof succeed
    13     fix thesis
    14     assume that [intro?]: "!!x. P x ==> thesis"
    15     <chain_facts> show thesis <proof (insert that)>
    16   qed
    17   fix x assm (obtained) "P x"
    18 *)
    19 
    20 signature OBTAIN =
    21 sig
    22   val obtain: (string list * string option) list ->
    23     ((string * Proof.context attribute list) * (string * (string list * string list)) list) list
    24     -> (Proof.context -> string * (string * thm list) list -> unit) *
    25       (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    26   val obtain_i: (string list * typ option) list ->
    27     ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
    28     -> (Proof.context -> string * (string * thm list) list -> unit) *
    29       (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
    30 end;
    31 
    32 structure Obtain: OBTAIN =
    33 struct
    34 
    35 
    36 (** export_obtain **)
    37 
    38 fun export_obtain state parms rule _ cprops thm =
    39   let
    40     val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
    41     val cparms = map (Thm.cterm_of sign) parms;
    42 
    43     val thm' = thm
    44       |> Drule.implies_intr_goals cprops
    45       |> Drule.forall_intr_list cparms
    46       |> Drule.forall_elim_vars (maxidx + 1);
    47     val elim_tacs = replicate (length cprops) (Tactic.etac Drule.triv_goal);
    48 
    49     val concl = Logic.strip_assums_concl prop;
    50     val bads = parms inter (Term.term_frees concl);
    51   in
    52     if not (null bads) then
    53       raise Proof.STATE ("Conclusion contains obtained parameters: " ^
    54         space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
    55     else if not (ObjectLogic.is_judgment sign (Logic.strip_assums_concl prop)) then
    56       raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
    57     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    58   end;
    59 
    60 
    61 
    62 (** obtain(_i) **)
    63 
    64 val thatN = "that";
    65 
    66 fun gen_obtain prep_vars prep_propp raw_vars raw_asms print state =
    67   let
    68     val _ = Proof.assert_forward_or_chain state;
    69     val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
    70     val thy = Proof.theory_of state;
    71     val sign = Theory.sign_of thy;
    72 
    73     (*obtain vars*)
    74     val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, raw_vars);
    75     val xs = flat (map fst vars);
    76     val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;
    77 
    78     (*obtain asms*)
    79     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    80     val asm_props = flat (map (map fst) proppss);
    81     val asms = map fst raw_asms ~~ proppss;
    82 
    83     val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
    84 
    85     (*obtain statements*)
    86     val thesisN = Term.variant xs (Syntax.internal AutoBind.thesisN);
    87     val bind_thesis = ProofContext.bind_skolem fix_ctxt [thesisN];
    88     val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment sign thesisN);
    89     val bound_thesis_raw as (bound_thesis_name, _) =
    90       Term.dest_Free (bind_thesis (Free (thesisN, propT)));
    91     val bound_thesis_var =
    92       foldl_aterms (fn (v, Free (x, T)) => if x = bound_thesis_name then (x, T) else v
    93         | (v, t) => v) (bound_thesis_raw, bound_thesis);
    94 
    95     fun occs_var x = Library.get_first (fn t =>
    96       ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
    97     val raw_parms = map occs_var xs;
    98     val parms = mapfilter I raw_parms;
    99     val parm_names =
   100       mapfilter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
   101 
   102     val that_prop =
   103       Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
   104       |> Library.curry Logic.list_rename_params (map #2 parm_names);
   105     val obtain_prop =
   106       Logic.list_rename_params ([AutoBind.thesisN],
   107         Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
   108 
   109     fun after_qed st = st
   110       |> Method.local_qed false NONE print
   111       |> Seq.map (fn st' => st'
   112         |> Proof.fix_i vars
   113         |> Proof.assm_i (export_obtain state parms (Proof.the_fact st')) asms);
   114   in
   115     state
   116     |> Proof.enter_forward
   117     |> Proof.have_i Seq.single true [(("", []), [(obtain_prop, ([], []))])]
   118     |> Method.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
   119     |> Proof.fix_i [([thesisN], NONE)]
   120     |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
   121     |> (fn state' =>
   122         state'
   123         |> Proof.from_facts chain_facts
   124         |> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
   125         |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
   126   end;
   127 
   128 val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
   129 val obtain_i = gen_obtain ProofContext.cert_vars ProofContext.cert_propp;
   130 
   131 end;