src/Pure/Isar/obtain.ML
author wenzelm
Thu Jul 13 11:39:22 2000 +0200 (2000-07-13)
changeset 9293 3da2533e0a61
parent 8807 0046be1769f9
child 9468 9adbcf6375c1
permissions -rw-r--r--
bind_skolem;
     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 The common case:
    10 
    11     <goal_facts>
    12     have/show C
    13       obtain a in P[a] <proof>          ==
    14 
    15     <goal_facts>
    16     have/show C
    17     proof succeed
    18       def thesis == C
    19       presume that: !!a. P a ==> thesis
    20       from goal_facts show thesis <proof>
    21     next
    22       fix a
    23       assume P a
    24 
    25 The general case:
    26 
    27     <goal_facts>
    28     have/show !!x. G x ==> C x
    29       obtain a in P[a] <proof>          ==
    30 
    31     <goal_facts>
    32     have/show !!x. G x ==> C x
    33     proof succeed
    34       fix x
    35       assume hyps: G x
    36       def thesis == C x
    37       presume that: !!a. P a ==> thesis
    38       from goal_facts show thesis <proof>
    39     next
    40       fix a
    41       assume P a
    42 *)
    43 
    44 signature OBTAIN_DATA =
    45 sig
    46   val that_atts: Proof.context attribute list
    47 end;
    48 
    49 signature OBTAIN =
    50 sig
    51   val obtain: ((string list * string option) * Comment.text) list
    52     * ((string * Args.src list * (string * (string list * string list)) list)
    53       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    54   val obtain_i: ((string list * typ option) * Comment.text) list
    55     * ((string * Proof.context attribute list * (term * (term list * term list)) list)
    56       * Comment.text) list -> ProofHistory.T -> ProofHistory.T
    57 end;
    58 
    59 functor ObtainFun(Data: OBTAIN_DATA): OBTAIN =
    60 struct
    61 
    62 
    63 (** obtain(_i) **)
    64 
    65 val thatN = "that";
    66 val hypsN = "hyps";
    67 
    68 fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
    69   let
    70     val _ = Proof.assert_backward state;
    71 
    72     (*obtain vars*)
    73     val (vars_ctxt, vars) =
    74       foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
    75     val xs = flat (map fst vars);
    76     val xs_thesis = xs @ [AutoBind.thesisN];
    77 
    78     val bind_skolem = ProofContext.bind_skolem vars_ctxt xs_thesis;
    79     fun bind_propp (prop, (pats1, pats2)) =
    80       (bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2));
    81 
    82     (*obtain asms*)
    83     fun prep_asm (ctxt, (name, src, raw_propps)) =
    84       let
    85         val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
    86         val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
    87       in (ctxt', ((name, atts, map bind_propp propps), map #1 propps)) end;
    88 
    89     val (asms_ctxt, asms_result) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
    90     val (asms, asm_propss) = Library.split_list asms_result;
    91     val asm_props = flat asm_propss;
    92     val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
    93 
    94     (*thesis*)
    95     val (prop, (goal_facts, _)) = Proof.get_goal state;
    96 
    97     val parms = Logic.strip_params prop;
    98     val parm_names = Term.variantlist (map #1 parms, Term.add_term_names (prop, xs_thesis));
    99     val parm_types = map #2 parms;
   100     val parm_vars = map Library.single parm_names ~~ map Some parm_types;
   101 
   102     val frees = map2 Free (parm_names, parm_types);
   103     val rev_frees = rev frees;
   104 
   105     val hyps = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp prop);
   106     val concl = Term.subst_bounds (rev_frees, Logic.strip_assums_concl prop);
   107     val (thesis_term, atomic_thesis) = AutoBind.atomic_thesis concl;
   108     val bound_thesis = bind_skolem atomic_thesis;
   109 
   110     (*that_prop*)
   111     fun find_free x t =
   112       (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
   113     fun occs_var x = Library.get_first (find_free x) asm_props;
   114     val that_prop =
   115       Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, bound_thesis));
   116 
   117     fun after_qed st =
   118       st
   119       |> Proof.next_block
   120       |> Proof.fix_i vars
   121       |> Proof.assume_i asms
   122       |> Seq.single;
   123   in
   124     state
   125     |> Method.proof (Some (Method.Basic (K Method.succeed)))
   126     |> Seq.map (fn st => st
   127       |> Proof.fix_i parm_vars
   128       |> Proof.assume_i [(hypsN, [], map (rpair ([], [])) hyps)]
   129       |> LocalDefs.def_i "" [] ((AutoBind.thesisN, None), (thesis_term, []))
   130       |> Proof.presume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
   131       |> Proof.from_facts goal_facts
   132       |> Proof.show_i after_qed "" [] (bound_thesis, ([], [])))
   133   end;
   134 
   135 
   136 val obtain = ProofHistory.applys o
   137   (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
   138 
   139 val obtain_i = ProofHistory.applys o
   140   (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
   141 
   142 
   143 
   144 (** outer syntax **)
   145 
   146 local structure P = OuterParse and K = OuterSyntax.Keyword in
   147 
   148 val obtainP =
   149   OuterSyntax.command "obtain" "generalized existence"
   150     K.prf_asm_goal
   151     (Scan.optional
   152       (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
   153         --| P.$$$ "where") [] --
   154       P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
   155     >> (Toplevel.print oo (Toplevel.proof o obtain)));
   156 
   157 val _ = OuterSyntax.add_keywords ["where"];
   158 val _ = OuterSyntax.add_parsers [obtainP];
   159 
   160 end;
   161 
   162 
   163 end;