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