src/Pure/Isar/obtain.ML
author wenzelm
Thu Aug 18 11:17:46 2005 +0200 (2005-08-18)
changeset 17111 d2ea9c974570
parent 17034 b4d9b87c102e
child 17357 ee2bdca144c7
permissions -rw-r--r--
prepare attributes here;
tuned;
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@8543
     5
The 'obtain' language element -- generalized existence at the level of
wenzelm@8543
     6
proof texts.
wenzelm@7674
     7
wenzelm@9468
     8
  <chain_facts>
wenzelm@9468
     9
  obtain x where "P x" <proof> ==
wenzelm@7674
    10
wenzelm@12970
    11
  have "!!thesis. (!!x. P x ==> thesis) ==> thesis"
wenzelm@12970
    12
  proof succeed
wenzelm@9468
    13
    fix thesis
wenzelm@12970
    14
    assume that [intro?]: "!!x. P x ==> thesis"
wenzelm@12970
    15
    <chain_facts> show thesis <proof (insert that)>
wenzelm@12970
    16
  qed
wenzelm@10379
    17
  fix x assm (obtained) "P x"
wenzelm@8094
    18
*)
wenzelm@7674
    19
wenzelm@7674
    20
signature OBTAIN =
wenzelm@7674
    21
sig
wenzelm@11890
    22
  val obtain: (string list * string option) list ->
wenzelm@17111
    23
    ((string * Attrib.src list) * (string * (string list * string list)) list) list
wenzelm@12970
    24
    -> (Proof.context -> string * (string * thm list) list -> unit) *
wenzelm@12970
    25
      (Proof.context -> thm -> unit) -> 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@12970
    28
    -> (Proof.context -> string * (string * thm list) list -> unit) *
wenzelm@12970
    29
      (Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq
wenzelm@7674
    30
end;
wenzelm@7674
    31
wenzelm@10379
    32
structure Obtain: OBTAIN =
wenzelm@7674
    33
struct
wenzelm@7674
    34
wenzelm@8094
    35
wenzelm@11816
    36
(** export_obtain **)
wenzelm@9468
    37
wenzelm@11816
    38
fun export_obtain state parms rule _ cprops thm =
wenzelm@9468
    39
  let
wenzelm@17111
    40
    val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
wenzelm@17111
    41
    val cparms = map (Thm.cterm_of thy) parms;
wenzelm@9468
    42
wenzelm@9468
    43
    val thm' = thm
wenzelm@11816
    44
      |> Drule.implies_intr_goals cprops
wenzelm@9468
    45
      |> Drule.forall_intr_list cparms
wenzelm@9468
    46
      |> Drule.forall_elim_vars (maxidx + 1);
wenzelm@11816
    47
    val elim_tacs = replicate (length cprops) (Tactic.etac Drule.triv_goal);
wenzelm@9468
    48
wenzelm@9468
    49
    val concl = Logic.strip_assums_concl prop;
wenzelm@9468
    50
    val bads = parms inter (Term.term_frees concl);
wenzelm@9468
    51
  in
wenzelm@9468
    52
    if not (null bads) then
wenzelm@9481
    53
      raise Proof.STATE ("Conclusion contains obtained parameters: " ^
wenzelm@12055
    54
        space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
wenzelm@17111
    55
    else if not (ObjectLogic.is_judgment thy (Logic.strip_assums_concl prop)) then
wenzelm@10379
    56
      raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
wenzelm@9468
    57
    else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
wenzelm@9468
    58
  end;
wenzelm@9468
    59
wenzelm@9468
    60
wenzelm@9468
    61
wenzelm@8094
    62
(** obtain(_i) **)
wenzelm@8094
    63
wenzelm@7674
    64
val thatN = "that";
wenzelm@7674
    65
wenzelm@17111
    66
fun gen_obtain prep_att prep_vars prep_propp raw_vars raw_asms print state =
wenzelm@7674
    67
  let
wenzelm@9468
    68
    val _ = Proof.assert_forward_or_chain state;
wenzelm@9468
    69
    val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
wenzelm@10464
    70
    val thy = Proof.theory_of state;
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);
skalberg@15570
    74
    val xs = List.concat (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);
skalberg@15570
    79
    val asm_props = List.concat (map (map fst) proppss);
wenzelm@17111
    80
    val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
wenzelm@10464
    81
wenzelm@10582
    82
    val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
wenzelm@7674
    83
wenzelm@12970
    84
    (*obtain statements*)
wenzelm@16606
    85
    val thesisN = Term.variant xs AutoBind.thesisN;
wenzelm@12970
    86
    val bind_thesis = ProofContext.bind_skolem fix_ctxt [thesisN];
wenzelm@17111
    87
    val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment thy thesisN);
wenzelm@12970
    88
    val bound_thesis_raw as (bound_thesis_name, _) =
wenzelm@12970
    89
      Term.dest_Free (bind_thesis (Free (thesisN, propT)));
wenzelm@12970
    90
    val bound_thesis_var =
haftmann@16787
    91
      fold_aterms (fn Free (x, T) => (fn v => if x = bound_thesis_name then (x, T) else v)
haftmann@16787
    92
        | _ => I) bound_thesis bound_thesis_raw;
wenzelm@9468
    93
wenzelm@10582
    94
    fun occs_var x = Library.get_first (fn t =>
wenzelm@10582
    95
      ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
wenzelm@10582
    96
    val raw_parms = map occs_var xs;
skalberg@15570
    97
    val parms = List.mapPartial I raw_parms;
wenzelm@10582
    98
    val parm_names =
skalberg@15570
    99
      List.mapPartial (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
wenzelm@10582
   100
wenzelm@10582
   101
    val that_prop =
wenzelm@10582
   102
      Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
wenzelm@10582
   103
      |> Library.curry Logic.list_rename_params (map #2 parm_names);
wenzelm@12970
   104
    val obtain_prop =
wenzelm@12970
   105
      Logic.list_rename_params ([AutoBind.thesisN],
wenzelm@12970
   106
        Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis)));
wenzelm@7674
   107
wenzelm@17111
   108
    fun after_qed _ =
wenzelm@17111
   109
      Proof.local_qed false NONE print
wenzelm@17111
   110
      #> Seq.map (fn st => st
wenzelm@9468
   111
        |> Proof.fix_i vars
wenzelm@17111
   112
        |> Proof.assm_i (export_obtain state parms (Proof.the_fact st)) asms);
wenzelm@7674
   113
  in
wenzelm@8094
   114
    state
wenzelm@9468
   115
    |> Proof.enter_forward
ballarin@17034
   116
    |> Proof.have_i (K Seq.single) true [(("", []), [(obtain_prop, ([], []))])]
wenzelm@17111
   117
    |> Proof.proof (SOME (Method.Basic (K Method.succeed))) |> Seq.hd
skalberg@15531
   118
    |> Proof.fix_i [([thesisN], NONE)]
skalberg@15531
   119
    |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])]
wenzelm@16842
   120
    |> `Proof.the_facts
wenzelm@16842
   121
    ||> Proof.from_facts chain_facts
wenzelm@16842
   122
    ||> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false
wenzelm@17111
   123
    |-> (fn facts => Proof.refine (Method.Basic (K (Method.insert facts))))
wenzelm@7674
   124
  end;
wenzelm@7674
   125
wenzelm@17111
   126
val obtain = gen_obtain Attrib.local_attribute ProofContext.read_vars ProofContext.read_propp;
wenzelm@17111
   127
val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
wenzelm@8094
   128
wenzelm@8094
   129
end;