src/Pure/Isar/obtain.ML
author wenzelm
Sun Jul 30 12:54:07 2000 +0200 (2000-07-30)
changeset 9468 9adbcf6375c1
parent 9293 3da2533e0a61
child 9481 b16624f1ea38
permissions -rw-r--r--
turned into plain context element;
exporter setup;
     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>
    16   }
    17   fix x assm(obtained) "P x"
    18 
    19 *)
    20 
    21 signature OBTAIN_DATA =
    22 sig
    23   val atomic_thesis: string -> term
    24   val that_atts: Proof.context attribute list
    25 end;
    26 
    27 signature OBTAIN =
    28 sig
    29   val obtain: ((string list * string option) * Comment.text) list
    30     * ((string * Args.src list * (string * (string list * string list)) list)
    31       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    32   val obtain_i: ((string list * typ option) * Comment.text) list
    33     * ((string * Proof.context attribute list * (term * (term list * term list)) list)
    34       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    35 end;
    36 
    37 functor ObtainFun(Data: OBTAIN_DATA): OBTAIN =
    38 struct
    39 
    40 
    41 (** export_obtained **)
    42 
    43 fun disch_obtained state parms rule cprops thm =
    44   let
    45     val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
    46     val cparms = map (Thm.cterm_of sign) parms;
    47 
    48     val thm' = thm
    49       |> Drule.implies_intr_list cprops
    50       |> Drule.forall_intr_list cparms
    51       |> Drule.forall_elim_vars (maxidx + 1);
    52     val elim_tacs = replicate (length cprops) Proof.hard_asm_tac;
    53 
    54     val concl = Logic.strip_assums_concl prop;
    55     val bads = parms inter (Term.term_frees concl);
    56   in
    57     if not (null bads) then
    58       raise Proof.STATE ("Result contains illegal parameters: " ^
    59         space_implode " " (map (Sign.string_of_term sign) bads), state)
    60     else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
    61       raise Proof.STATE ("Conclusion of result is not an object-logic judgment", state)
    62     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    63   end;
    64 
    65 fun export_obtained state parms rule =
    66   (disch_obtained state parms rule, fn _ => fn _ => []);
    67 
    68 
    69 
    70 (** obtain(_i) **)
    71 
    72 val thatN = "that";
    73 
    74 fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
    75   let
    76     val _ = Proof.assert_forward_or_chain state;
    77     val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
    78 
    79     (*obtain vars*)
    80     val (vars_ctxt, vars) =
    81       foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
    82     val xs = flat (map fst vars);
    83     val thesisN = Term.variant xs AutoBind.thesisN;
    84 
    85     val bind_skolem = ProofContext.bind_skolem vars_ctxt (xs @ [thesisN]);
    86     fun bind_propp (prop, (pats1, pats2)) =
    87       (bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2));
    88 
    89     (*obtain asms*)
    90     fun prep_asm (ctxt, (name, src, raw_propps)) =
    91       let
    92         val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
    93         val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
    94       in (ctxt', ((name, atts, map bind_propp propps), map #1 propps)) end;
    95 
    96     val (asms_ctxt, asms_result) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
    97     val (asms, asm_propss) = Library.split_list asms_result;
    98     val asm_props = flat asm_propss;
    99     val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
   100 
   101     (*that_prop*)
   102     fun find_free x t =
   103       (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
   104     fun occs_var x = Library.get_first (find_free x) asm_props;
   105     val xs' = mapfilter occs_var xs;
   106     val parms = map (bind_skolem o Free) xs';
   107 
   108     val bound_thesis = bind_skolem (Data.atomic_thesis thesisN);
   109     val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
   110 
   111     fun after_qed st = st
   112       |> Proof.end_block
   113       |> Seq.map (fn st' => st'
   114         |> Proof.fix_i vars
   115         |> Proof.assm_i (export_obtained state parms (Proof.the_fact st')) asms);
   116   in
   117     state
   118     |> Proof.enter_forward
   119     |> Proof.begin_block
   120     |> Proof.fix_i [([thesisN], None)]
   121     |> Proof.assume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
   122     |> Proof.from_facts chain_facts
   123     |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
   124   end;
   125 
   126 
   127 val obtain = ProofHistory.apply o
   128   (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
   129 
   130 val obtain_i = ProofHistory.apply o
   131   (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
   132 
   133 
   134 
   135 (** outer syntax **)
   136 
   137 local structure P = OuterParse and K = OuterSyntax.Keyword in
   138 
   139 val obtainP =
   140   OuterSyntax.command "obtain" "generalized existence"
   141     K.prf_asm_goal
   142     (Scan.optional
   143       (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
   144         --| P.$$$ "where") [] --
   145       P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
   146     >> (Toplevel.print oo (Toplevel.proof o obtain)));
   147 
   148 val _ = OuterSyntax.add_keywords ["where"];
   149 val _ = OuterSyntax.add_parsers [obtainP];
   150 
   151 end;
   152 
   153 end;