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