src/Pure/Isar/obtain.ML
author wenzelm
Fri Nov 03 21:27:06 2000 +0100 (2000-11-03)
changeset 10379 93630e0c5ae9
parent 9481 b16624f1ea38
child 10464 b7b916a82dca
permissions -rw-r--r--
improved handling of "that": insert into goal, only declare as Pure "intro";
eliminated functor;
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@9468
     9
  <chain_facts>
wenzelm@9468
    10
  obtain x where "P x" <proof> ==
wenzelm@7674
    11
wenzelm@9468
    12
  {
wenzelm@9468
    13
    fix thesis
wenzelm@9468
    14
    assume that: "!!x. P x ==> thesis"
wenzelm@10379
    15
    <chain_facts> have thesis <proof (insert that)>
wenzelm@9468
    16
  }
wenzelm@10379
    17
  fix x assm (obtained) "P x"
wenzelm@7674
    18
wenzelm@8094
    19
*)
wenzelm@7674
    20
wenzelm@7674
    21
signature OBTAIN =
wenzelm@7674
    22
sig
wenzelm@8094
    23
  val obtain: ((string list * string option) * Comment.text) list
wenzelm@8094
    24
    * ((string * Args.src list * (string * (string list * string list)) list)
wenzelm@8094
    25
      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
wenzelm@8094
    26
  val obtain_i: ((string list * typ option) * Comment.text) list
wenzelm@8094
    27
    * ((string * Proof.context attribute list * (term * (term list * term list)) list)
wenzelm@8094
    28
      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
wenzelm@7674
    29
end;
wenzelm@7674
    30
wenzelm@10379
    31
structure Obtain: OBTAIN =
wenzelm@7674
    32
struct
wenzelm@7674
    33
wenzelm@8094
    34
wenzelm@9481
    35
(** disch_obtained **)
wenzelm@9468
    36
wenzelm@9468
    37
fun disch_obtained state parms rule cprops thm =
wenzelm@9468
    38
  let
wenzelm@9468
    39
    val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
wenzelm@9468
    40
    val cparms = map (Thm.cterm_of sign) parms;
wenzelm@9468
    41
wenzelm@9468
    42
    val thm' = thm
wenzelm@9468
    43
      |> Drule.implies_intr_list cprops
wenzelm@9468
    44
      |> Drule.forall_intr_list cparms
wenzelm@9468
    45
      |> Drule.forall_elim_vars (maxidx + 1);
wenzelm@9468
    46
    val elim_tacs = replicate (length cprops) Proof.hard_asm_tac;
wenzelm@9468
    47
wenzelm@9468
    48
    val concl = Logic.strip_assums_concl prop;
wenzelm@9468
    49
    val bads = parms inter (Term.term_frees concl);
wenzelm@9468
    50
  in
wenzelm@9468
    51
    if not (null bads) then
wenzelm@9481
    52
      raise Proof.STATE ("Conclusion contains obtained parameters: " ^
wenzelm@9468
    53
        space_implode " " (map (Sign.string_of_term sign) bads), state)
wenzelm@9468
    54
    else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
wenzelm@10379
    55
      raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
wenzelm@9468
    56
    else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
wenzelm@9468
    57
  end;
wenzelm@9468
    58
wenzelm@9468
    59
wenzelm@9468
    60
wenzelm@8094
    61
(** obtain(_i) **)
wenzelm@8094
    62
wenzelm@7674
    63
val thatN = "that";
wenzelm@7674
    64
wenzelm@8094
    65
fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
wenzelm@7674
    66
  let
wenzelm@9468
    67
    val _ = Proof.assert_forward_or_chain state;
wenzelm@9468
    68
    val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
wenzelm@7674
    69
wenzelm@8543
    70
    (*obtain vars*)
wenzelm@8094
    71
    val (vars_ctxt, vars) =
wenzelm@8094
    72
      foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
wenzelm@8094
    73
    val xs = flat (map fst vars);
wenzelm@9468
    74
    val thesisN = Term.variant xs AutoBind.thesisN;
wenzelm@9293
    75
wenzelm@9468
    76
    val bind_skolem = ProofContext.bind_skolem vars_ctxt (xs @ [thesisN]);
wenzelm@9293
    77
    fun bind_propp (prop, (pats1, pats2)) =
wenzelm@9293
    78
      (bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2));
wenzelm@7674
    79
wenzelm@8543
    80
    (*obtain asms*)
wenzelm@8094
    81
    fun prep_asm (ctxt, (name, src, raw_propps)) =
wenzelm@8094
    82
      let
wenzelm@8094
    83
        val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
wenzelm@8094
    84
        val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
wenzelm@9293
    85
      in (ctxt', ((name, atts, map bind_propp propps), map #1 propps)) end;
wenzelm@7674
    86
wenzelm@9293
    87
    val (asms_ctxt, asms_result) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
wenzelm@9293
    88
    val (asms, asm_propss) = Library.split_list asms_result;
wenzelm@9293
    89
    val asm_props = flat asm_propss;
wenzelm@8094
    90
    val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
wenzelm@7674
    91
wenzelm@8094
    92
    (*that_prop*)
wenzelm@7674
    93
    fun find_free x t =
wenzelm@8614
    94
      (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
wenzelm@8094
    95
    fun occs_var x = Library.get_first (find_free x) asm_props;
wenzelm@9468
    96
    val xs' = mapfilter occs_var xs;
wenzelm@9468
    97
    val parms = map (bind_skolem o Free) xs';
wenzelm@9468
    98
wenzelm@10379
    99
    val bound_thesis = bind_skolem (AutoBind.atomic_judgment (Proof.theory_of state) thesisN);
wenzelm@9468
   100
    val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
wenzelm@7674
   101
wenzelm@9481
   102
    fun export_obtained rule =
wenzelm@9481
   103
      (disch_obtained state parms rule, fn _ => fn _ => []);
wenzelm@9481
   104
wenzelm@9468
   105
    fun after_qed st = st
wenzelm@9468
   106
      |> Proof.end_block
wenzelm@9468
   107
      |> Seq.map (fn st' => st'
wenzelm@9468
   108
        |> Proof.fix_i vars
wenzelm@9481
   109
        |> Proof.assm_i (export_obtained (Proof.the_fact st')) asms);
wenzelm@7674
   110
  in
wenzelm@8094
   111
    state
wenzelm@9468
   112
    |> Proof.enter_forward
wenzelm@9468
   113
    |> Proof.begin_block
wenzelm@9468
   114
    |> Proof.fix_i [([thesisN], None)]
wenzelm@10379
   115
    |> Proof.assume_i [(thatN, [Method.intro_local], [(that_prop, ([], []))])]
wenzelm@10379
   116
    |> (fn state' =>
wenzelm@10379
   117
      state'
wenzelm@10379
   118
      |> Proof.from_facts chain_facts
wenzelm@10379
   119
      |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
wenzelm@10379
   120
      |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
wenzelm@7674
   121
  end;
wenzelm@7674
   122
wenzelm@7674
   123
wenzelm@10379
   124
val obtain = ProofHistory.applys o
wenzelm@8094
   125
  (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
wenzelm@8094
   126
wenzelm@10379
   127
val obtain_i = ProofHistory.applys o
wenzelm@8094
   128
  (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
wenzelm@8094
   129
wenzelm@8094
   130
wenzelm@8094
   131
wenzelm@8094
   132
(** outer syntax **)
wenzelm@8094
   133
wenzelm@8094
   134
local structure P = OuterParse and K = OuterSyntax.Keyword in
wenzelm@8094
   135
wenzelm@8094
   136
val obtainP =
wenzelm@8543
   137
  OuterSyntax.command "obtain" "generalized existence"
wenzelm@8094
   138
    K.prf_asm_goal
wenzelm@8094
   139
    (Scan.optional
wenzelm@8094
   140
      (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
wenzelm@8109
   141
        --| P.$$$ "where") [] --
wenzelm@8094
   142
      P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
wenzelm@8094
   143
    >> (Toplevel.print oo (Toplevel.proof o obtain)));
wenzelm@8094
   144
wenzelm@8109
   145
val _ = OuterSyntax.add_keywords ["where"];
wenzelm@8094
   146
val _ = OuterSyntax.add_parsers [obtainP];
wenzelm@8094
   147
wenzelm@8094
   148
end;
wenzelm@7674
   149
wenzelm@7674
   150
end;