src/Pure/Isar/obtain.ML
author wenzelm
Mon Nov 13 22:01:07 2000 +0100 (2000-11-13)
changeset 10464 b7b916a82dca
parent 10379 93630e0c5ae9
child 10582 49ebade930ea
permissions -rw-r--r--
tuned statement args;
     1 (*  Title:      Pure/Isar/obtain.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 The 'obtain' language element -- generalized existence at the level of
     7 proof texts.
     8 
     9   <chain_facts>
    10   obtain x where "P x" <proof> ==
    11 
    12   {
    13     fix thesis
    14     assume that: "!!x. P x ==> thesis"
    15     <chain_facts> have thesis <proof (insert that)>
    16   }
    17   fix x assm (obtained) "P x"
    18 
    19 *)
    20 
    21 signature OBTAIN =
    22 sig
    23   val obtain: ((string list * string option) * Comment.text) list
    24     * (((string * Args.src list) * (string * (string list * string list)) list)
    25       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    26   val obtain_i: ((string list * typ option) * Comment.text) list
    27     * (((string * Proof.context attribute list) * (term * (term list * term list)) list)
    28       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    29 end;
    30 
    31 structure Obtain: OBTAIN =
    32 struct
    33 
    34 
    35 (** disch_obtained **)
    36 
    37 fun disch_obtained state parms rule cprops thm =
    38   let
    39     val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
    40     val cparms = map (Thm.cterm_of sign) parms;
    41 
    42     val thm' = thm
    43       |> Drule.implies_intr_list cprops
    44       |> Drule.forall_intr_list cparms
    45       |> Drule.forall_elim_vars (maxidx + 1);
    46     val elim_tacs = replicate (length cprops) Proof.hard_asm_tac;
    47 
    48     val concl = Logic.strip_assums_concl prop;
    49     val bads = parms inter (Term.term_frees concl);
    50   in
    51     if not (null bads) then
    52       raise Proof.STATE ("Conclusion contains obtained parameters: " ^
    53         space_implode " " (map (Sign.string_of_term sign) bads), state)
    54     else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
    55       raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
    56     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    57   end;
    58 
    59 
    60 
    61 (** obtain(_i) **)
    62 
    63 val thatN = "that";
    64 
    65 fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
    66   let
    67     val _ = Proof.assert_forward_or_chain state;
    68     val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
    69     val thy = Proof.theory_of state;
    70 
    71     (*obtain vars*)
    72     val (vars_ctxt, vars) =
    73       foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
    74     val xs = flat (map fst vars);
    75     val thesisN = Term.variant xs AutoBind.thesisN;
    76 
    77     val bind_skolem = ProofContext.bind_skolem vars_ctxt (xs @ [thesisN]);
    78     fun bind_propp (prop, (pats1, pats2)) =
    79       (bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2));
    80 
    81     (*obtain asms*)
    82     val (asms_ctxt, proppss) = prep_propp (vars_ctxt, map (snd o Comment.ignore) raw_asms);
    83     val asm_props = flat (map (map fst) proppss);
    84 
    85     fun prep_asm ((name, src), propps) = ((name, map (prep_att thy) src), map bind_propp propps);
    86     val asms = map2 prep_asm (map (fst o Comment.ignore) raw_asms, proppss);
    87 
    88     val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
    89 
    90     (*that_prop*)
    91     fun find_free x t =
    92       (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
    93     fun occs_var x = Library.get_first (find_free x) asm_props;
    94     val xs' = mapfilter occs_var xs;
    95     val parms = map (bind_skolem o Free) xs';
    96 
    97     val bound_thesis = bind_skolem (AutoBind.atomic_judgment thy thesisN);
    98     val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
    99 
   100     fun export_obtained rule =
   101       (disch_obtained state parms rule, fn _ => fn _ => []);
   102 
   103     fun after_qed st = st
   104       |> Proof.end_block
   105       |> Seq.map (fn st' => st'
   106         |> Proof.fix_i vars
   107         |> Proof.assm_i (export_obtained (Proof.the_fact st')) asms);
   108   in
   109     state
   110     |> Proof.enter_forward
   111     |> Proof.begin_block
   112     |> Proof.fix_i [([thesisN], None)]
   113     |> Proof.assume_i [((thatN, [Method.intro_local]), [(that_prop, ([], []))])]
   114     |> (fn state' =>
   115       state'
   116       |> Proof.from_facts chain_facts
   117       |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
   118       |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
   119   end;
   120 
   121 
   122 val obtain = ProofHistory.applys o
   123   (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
   124 
   125 val obtain_i = ProofHistory.applys o
   126   (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
   127 
   128 
   129 
   130 (** outer syntax **)
   131 
   132 local structure P = OuterParse and K = OuterSyntax.Keyword in
   133 
   134 val obtainP =
   135   OuterSyntax.command "obtain" "generalized existence"
   136     K.prf_asm_goal
   137     (Scan.optional
   138       (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
   139         --| P.$$$ "where") [] --
   140       P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment)
   141     >> (Toplevel.print oo (Toplevel.proof o obtain)));
   142 
   143 val _ = OuterSyntax.add_keywords ["where"];
   144 val _ = OuterSyntax.add_parsers [obtainP];
   145 
   146 end;
   147 
   148 end;