src/Pure/Isar/obtain.ML
author wenzelm
Mon Oct 22 18:02:50 2001 +0200 (2001-10-22)
changeset 11890 28e42a90bea8
parent 11816 545aab7410ac
child 12055 a9c44895cc8c
permissions -rw-r--r--
improved source arrangement of obtain;
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@11021
    14
    assume that [intro]: "!!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@11890
    23
  val obtain: (string list * string option) list ->
wenzelm@11890
    24
    ((string * Proof.context attribute list) * (string * (string list * string list)) list) list
wenzelm@11890
    25
    -> Proof.state -> Proof.state Seq.seq
wenzelm@11890
    26
  val obtain_i: (string list * typ option) list ->
wenzelm@11890
    27
    ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
wenzelm@11890
    28
    -> Proof.state -> Proof.state Seq.seq
wenzelm@7674
    29
end;
wenzelm@7674
    30
wenzelm@10379
    31
structure Obtain: OBTAIN =
wenzelm@7674
    32
struct
wenzelm@7674
    33
wenzelm@8094
    34
wenzelm@11816
    35
(** export_obtain **)
wenzelm@9468
    36
wenzelm@11816
    37
fun export_obtain 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@11816
    43
      |> Drule.implies_intr_goals cprops
wenzelm@9468
    44
      |> Drule.forall_intr_list cparms
wenzelm@9468
    45
      |> Drule.forall_elim_vars (maxidx + 1);
wenzelm@11816
    46
    val elim_tacs = replicate (length cprops) (Tactic.etac Drule.triv_goal);
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@11764
    54
    else if not (ObjectLogic.is_judgment sign (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@11890
    65
fun gen_obtain prep_vars prep_propp 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@10464
    69
    val thy = Proof.theory_of state;
wenzelm@11764
    70
    val sign = Theory.sign_of thy;
wenzelm@7674
    71
wenzelm@8543
    72
    (*obtain vars*)
wenzelm@11890
    73
    val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, raw_vars);
wenzelm@8094
    74
    val xs = flat (map fst vars);
wenzelm@10582
    75
    val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;
wenzelm@7674
    76
wenzelm@8543
    77
    (*obtain asms*)
wenzelm@11890
    78
    val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
wenzelm@10464
    79
    val asm_props = flat (map (map fst) proppss);
wenzelm@11890
    80
    val asms = map fst raw_asms ~~ proppss;
wenzelm@10464
    81
wenzelm@10582
    82
    val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
wenzelm@7674
    83
wenzelm@8094
    84
    (*that_prop*)
wenzelm@10582
    85
    val thesisN = Term.variant xs AutoBind.thesisN;
wenzelm@10582
    86
    val bound_thesis =
wenzelm@11764
    87
      ProofContext.bind_skolem fix_ctxt [thesisN] (ObjectLogic.fixed_judgment sign thesisN);
wenzelm@9468
    88
wenzelm@10582
    89
    fun occs_var x = Library.get_first (fn t =>
wenzelm@10582
    90
      ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
wenzelm@10582
    91
    val raw_parms = map occs_var xs;
wenzelm@10582
    92
    val parms = mapfilter I raw_parms;
wenzelm@10582
    93
    val parm_names =
wenzelm@10582
    94
      mapfilter (fn (Some (Free a), x) => Some (a, x) | _ => None) (raw_parms ~~ xs);
wenzelm@10582
    95
wenzelm@10582
    96
    val that_prop =
wenzelm@10582
    97
      Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
wenzelm@10582
    98
      |> Library.curry Logic.list_rename_params (map #2 parm_names);
wenzelm@7674
    99
wenzelm@9468
   100
    fun after_qed st = st
wenzelm@9468
   101
      |> Proof.end_block
wenzelm@9468
   102
      |> Seq.map (fn st' => st'
wenzelm@9468
   103
        |> Proof.fix_i vars
wenzelm@11816
   104
        |> Proof.assm_i (export_obtain state parms (Proof.the_fact st')) asms);
wenzelm@7674
   105
  in
wenzelm@8094
   106
    state
wenzelm@9468
   107
    |> Proof.enter_forward
wenzelm@9468
   108
    |> Proof.begin_block
wenzelm@9468
   109
    |> Proof.fix_i [([thesisN], None)]
wenzelm@10464
   110
    |> Proof.assume_i [((thatN, [Method.intro_local]), [(that_prop, ([], []))])]
wenzelm@10379
   111
    |> (fn state' =>
wenzelm@10379
   112
      state'
wenzelm@10379
   113
      |> Proof.from_facts chain_facts
wenzelm@10379
   114
      |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
wenzelm@10379
   115
      |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
wenzelm@7674
   116
  end;
wenzelm@7674
   117
wenzelm@11890
   118
val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
wenzelm@11890
   119
val obtain_i = gen_obtain ProofContext.cert_vars ProofContext.cert_propp;
wenzelm@8094
   120
wenzelm@8094
   121
wenzelm@8094
   122
end;