src/Pure/Isar/obtain.ML
author wenzelm
Thu Jan 06 16:00:18 2000 +0100 (2000-01-06)
changeset 8109 aca11f954993
parent 8094 62b45a2e6ecb
child 8543 f54926bded7b
permissions -rw-r--r--
obtain: renamed 'in' to 'where';
     1 (*  Title:      Pure/Isar/obtain.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 The 'obtain' language element -- eliminated existential quantification
     6 at the level of proof texts.
     7 
     8 The common case:
     9 
    10     <goal_facts>
    11     have/show C
    12       obtain a in P[a] <proof>          ==
    13 
    14     <goal_facts>
    15     have/show C
    16     proof succeed
    17       def thesis == C
    18       presume that: !!a. P a ==> thesis
    19       from goal_facts show thesis <proof>
    20     next
    21       fix a
    22       assume P a
    23 
    24 The general case:
    25 
    26     <goal_facts>
    27     have/show !!x. G x ==> C x
    28       obtain a in P[a] <proof>          ==
    29 
    30     <goal_facts>
    31     have/show !!x. G x ==> C x
    32     proof succeed
    33       fix x
    34       assume antecedent: G x
    35       def thesis == C x
    36       presume that: !!a. P a ==> thesis
    37       from goal_facts show thesis <proof>
    38     next
    39       fix a
    40       assume P a
    41 
    42 TODO:
    43   - bind terms for goal as well (done?);
    44   - improve block structure (admit subsequent occurences of 'next') (no?);
    45   - handle general case (easy??);
    46 *)
    47 
    48 signature OBTAIN_DATA =
    49 sig
    50   val that_atts: Proof.context attribute list
    51 end;
    52 
    53 signature OBTAIN =
    54 sig
    55   val obtain: ((string list * string option) * Comment.text) list
    56     * ((string * Args.src list * (string * (string list * string list)) list)
    57       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    58   val obtain_i: ((string list * typ option) * Comment.text) list
    59     * ((string * Proof.context attribute list * (term * (term list * term list)) list)
    60       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    61 end;
    62 
    63 functor ObtainFun(Data: OBTAIN_DATA): OBTAIN =
    64 struct
    65 
    66 
    67 (** obtain(_i) **)
    68 
    69 val thatN = "that";
    70 
    71 fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
    72   let
    73     (*thesis*)
    74     val (prop, (goal_facts, goal)) = Proof.get_goal (Proof.assert_backward state);
    75 
    76     val parms = Logic.strip_params prop;        (* FIXME unused *)
    77     val _ =
    78       if null parms then () else raise Proof.STATE ("Cannot handle params in goal (yet)", state);
    79     val hyps = Logic.strip_assums_hyp prop;     (* FIXME unused *)
    80     val concl = Logic.strip_assums_concl prop;
    81     val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl;
    82 
    83     (*vars*)
    84     val (vars_ctxt, vars) =
    85       foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
    86     val xs = flat (map fst vars);
    87 
    88     (*asms*)
    89     fun prep_asm (ctxt, (name, src, raw_propps)) =
    90       let
    91         val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
    92         val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
    93       in (ctxt', (name, atts, propps)) end;
    94 
    95     val (asms_ctxt, asms) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
    96     val asm_props = flat (map (map fst o #3) asms);
    97     val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
    98 
    99     (*that_prop*)
   100     fun find_free x t =
   101       (case Proof.find_free t x of Some (Free a) => Some a | _ => None);
   102     fun occs_var x = Library.get_first (find_free x) asm_props;
   103     val that_prop =
   104       Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, atomic_thesis));
   105 
   106     fun after_qed st =
   107       st
   108       |> Proof.next_block
   109       |> Proof.fix_i vars
   110       |> Proof.assume_i asms
   111       |> Seq.single;
   112   in
   113     state
   114     |> Method.proof (Some (Method.Basic (K Method.succeed)))
   115     |> Seq.map (fn st => st
   116       |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
   117       |> Proof.presume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
   118       |> Proof.from_facts goal_facts
   119       |> Proof.show_i after_qed "" [] (atomic_thesis, ([], [])))
   120   end;
   121 
   122 
   123 val obtain = ProofHistory.applys o
   124   (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
   125 
   126 val obtain_i = ProofHistory.applys o
   127   (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
   128 
   129 
   130 
   131 (** outer syntax **)
   132 
   133 local structure P = OuterParse and K = OuterSyntax.Keyword in
   134 
   135 val obtainP =
   136   OuterSyntax.command "obtain" "proof text-level existential quantifier"
   137     K.prf_asm_goal
   138     (Scan.optional
   139       (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
   140         --| P.$$$ "where") [] --
   141       P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
   142     >> (Toplevel.print oo (Toplevel.proof o obtain)));
   143 
   144 val _ = OuterSyntax.add_keywords ["where"];
   145 val _ = OuterSyntax.add_parsers [obtainP];
   146 
   147 end;
   148 
   149 
   150 end;