src/Pure/Isar/obtain.ML
author wenzelm
Fri Oct 01 20:38:16 1999 +0200 (1999-10-01)
changeset 7677 de2e468a42c8
parent 7674 99305245f6bd
child 7923 895d31b54da5
permissions -rw-r--r--
tuned comment;
     1 (*  Title:      Pure/Isar/obtain.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 The 'obtain' language element -- achieves (eliminated) existential
     6 quantification at proof command level.
     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 == ?thesis_prop 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 TODO:
    44   - handle general case;
    45 *)
    46 
    47 signature OBTAIN =
    48 sig
    49   val obtain: (string list * string option) list
    50     -> (string * Proof.context attribute list * (string * (string list * string list)) list) list
    51     -> Proof.state -> Proof.state Seq.seq
    52   val obtain_i: (string list * typ option) list
    53     -> (string * Proof.context attribute list * (term * (term list * term list)) list) list
    54     -> Proof.state -> Proof.state Seq.seq
    55 end;
    56 
    57 structure Obtain: OBTAIN =
    58 struct
    59 
    60 val thatN = "that";
    61 
    62 fun gen_obtain prep_typ prep_prop fix assume raw_vars raw_asms state =
    63   let
    64     val (prop, (goal_facts, goal)) = Proof.get_goal (Proof.assert_backward state);
    65 
    66     val parms = Logic.strip_params prop;
    67     val hyps = Logic.strip_assums_hyp prop;
    68     val concl = Logic.strip_assums_concl prop;
    69     val _ =
    70       if null parms then () else raise Proof.STATE ("Cannot handle params in goal (yet)", state);
    71 
    72     val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl;
    73 
    74 
    75     fun fix_vars (ctxt, (xs, raw_T)) =
    76       let
    77         val T = apsome (prep_typ ctxt) raw_T;
    78         val ctxt' = ProofContext.fix_i [(xs, T)] ctxt;
    79       in (ctxt', map (ProofContext.cert_skolem ctxt') xs) end;
    80 
    81     fun prep_asm (ctxt, (_, _, raw_propps)) =
    82       let val ts = map (prep_prop ctxt) (map fst raw_propps);
    83       in (ctxt |> ProofContext.declare_terms ts, ts) end;
    84 
    85     val (fix_ctxt, skolems) = apsnd flat (foldl_map fix_vars (Proof.context_of state, raw_vars));
    86     val (asms_ctxt, asms) = apsnd flat (foldl_map prep_asm (fix_ctxt, raw_asms));
    87 
    88     fun find_free x t =
    89       (case Proof.find_free t x of Some (Free a) => Some a | _ => None);
    90     fun find_skolem x = Library.get_first (find_free x) asms;
    91     val skolemTs = mapfilter find_skolem skolems;
    92 
    93     val that_prop =
    94       Logic.list_rename_params (map (Syntax.dest_skolem o #1) skolemTs,
    95         Term.list_all_free (skolemTs, Logic.list_implies (asms, atomic_thesis)));
    96 
    97     val presume_stateq =
    98       state
    99       |> Method.proof (Some (Method.Basic (K Method.succeed)))
   100       |> Seq.map (fn st => st
   101         |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
   102         |> Proof.presume_i [(thatN, [], [(that_prop, ([], []))])]);
   103 
   104     fun after_qed st =
   105       st
   106       |> Proof.next_block
   107       |> fix raw_vars           (*prepared twice!*)
   108       |> assume raw_asms        (*prepared twice!*)
   109       |> Seq.single;
   110   in
   111     presume_stateq
   112     |> Seq.map (fn st => st
   113       |> Proof.from_facts goal_facts
   114       |> Proof.show_i after_qed "" [] (atomic_thesis, ([], []))
   115       |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts st)))))
   116     |> Seq.flat
   117   end;
   118 
   119 
   120 val obtain = gen_obtain ProofContext.read_typ ProofContext.read_prop Proof.fix Proof.assume;
   121 val obtain_i = gen_obtain ProofContext.cert_typ ProofContext.cert_prop Proof.fix_i Proof.assume_i;
   122 
   123 
   124 end;