src/Pure/Isar/obtain.ML
author wenzelm
Fri Apr 07 17:36:25 2000 +0200 (2000-04-07 ago)
changeset 8681 957a5fe9b212
parent 8614 30cc975727f1
child 8807 0046be1769f9
permissions -rw-r--r--
apply etc.: comments;
     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 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 hyps: 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 
    43 signature OBTAIN_DATA =
    44 sig
    45   val that_atts: Proof.context attribute list
    46 end;
    47 
    48 signature OBTAIN =
    49 sig
    50   val obtain: ((string list * string option) * Comment.text) list
    51     * ((string * Args.src list * (string * (string list * string list)) list)
    52       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    53   val obtain_i: ((string list * typ option) * Comment.text) list
    54     * ((string * Proof.context attribute list * (term * (term list * term list)) list)
    55       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    56 end;
    57 
    58 functor ObtainFun(Data: OBTAIN_DATA): OBTAIN =
    59 struct
    60 
    61 
    62 (** obtain(_i) **)
    63 
    64 val thatN = "that";
    65 val hypsN = "hyps";
    66 
    67 fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
    68   let
    69     val _ = Proof.assert_backward 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 
    76     (*obtain asms*)
    77     fun prep_asm (ctxt, (name, src, raw_propps)) =
    78       let
    79         val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
    80         val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
    81       in (ctxt', (name, atts, propps)) end;
    82 
    83     val (asms_ctxt, asms) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
    84     val asm_props = flat (map (map fst o #3) asms);
    85     val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
    86 
    87     (*thesis*)
    88     val (prop, (goal_facts, goal)) = Proof.get_goal state;
    89 
    90     val parms = Logic.strip_params prop;
    91     val parm_names = Term.variantlist (map #1 parms, Term.add_term_names (prop, xs));
    92     val parm_types = map #2 parms;
    93     val parm_vars = map Library.single parm_names ~~ map Some parm_types;
    94 
    95     val frees = map2 Free (parm_names, parm_types);
    96     val rev_frees = rev frees;
    97 
    98     val hyps = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp prop);
    99     val concl = Term.subst_bounds (rev_frees, Logic.strip_assums_concl prop);
   100     val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl;
   101 
   102     (*that_prop*)
   103     fun find_free x t =
   104       (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
   105     fun occs_var x = Library.get_first (find_free x) asm_props;
   106     val that_prop =
   107       Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, atomic_thesis));
   108 
   109     fun after_qed st =
   110       st
   111       |> Proof.next_block
   112       |> Proof.fix_i vars
   113       |> Proof.assume_i asms
   114       |> Seq.single;
   115   in
   116     state
   117     |> Method.proof (Some (Method.Basic (K Method.succeed)))
   118     |> Seq.map (fn st => st
   119       |> Proof.fix_i parm_vars
   120       |> Proof.assume_i [(hypsN, [], map (rpair ([], [])) hyps)]
   121       |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
   122       |> Proof.presume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
   123       |> Proof.from_facts goal_facts
   124       |> Proof.show_i after_qed "" [] (atomic_thesis, ([], [])))
   125   end;
   126 
   127 
   128 val obtain = ProofHistory.applys o
   129   (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
   130 
   131 val obtain_i = ProofHistory.applys o
   132   (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
   133 
   134 
   135 
   136 (** outer syntax **)
   137 
   138 local structure P = OuterParse and K = OuterSyntax.Keyword in
   139 
   140 val obtainP =
   141   OuterSyntax.command "obtain" "generalized existence"
   142     K.prf_asm_goal
   143     (Scan.optional
   144       (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
   145         --| P.$$$ "where") [] --
   146       P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
   147     >> (Toplevel.print oo (Toplevel.proof o obtain)));
   148 
   149 val _ = OuterSyntax.add_keywords ["where"];
   150 val _ = OuterSyntax.add_parsers [obtainP];
   151 
   152 end;
   153 
   154 
   155 end;