src/Pure/Isar/obtain.ML
author wenzelm
Sun, 30 Jul 2000 12:54:07 +0200
changeset 9468 9adbcf6375c1
parent 9293 3da2533e0a61
child 9481 b16624f1ea38
permissions -rw-r--r--
turned into plain context element; exporter setup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/obtain.ML
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
8807
wenzelm
parents: 8614
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
     5
8543
f54926bded7b handle general case: params and hyps of thesis;
wenzelm
parents: 8109
diff changeset
     6
The 'obtain' language element -- generalized existence at the level of
f54926bded7b handle general case: params and hyps of thesis;
wenzelm
parents: 8109
diff changeset
     7
proof texts.
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
     8
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
     9
  <chain_facts>
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    10
  obtain x where "P x" <proof> ==
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    11
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    12
  {
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    13
    fix thesis
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    14
    assume that: "!!x. P x ==> thesis"
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    15
    <chain_facts> have thesis <proof>
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    16
  }
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    17
  fix x assm(obtained) "P x"
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    18
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    19
*)
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    20
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    21
signature OBTAIN_DATA =
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    22
sig
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    23
  val atomic_thesis: string -> term
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    24
  val that_atts: Proof.context attribute list
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    25
end;
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    26
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    27
signature OBTAIN =
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    28
sig
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    29
  val obtain: ((string list * string option) * Comment.text) list
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    30
    * ((string * Args.src list * (string * (string list * string list)) list)
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    31
      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    32
  val obtain_i: ((string list * typ option) * Comment.text) list
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    33
    * ((string * Proof.context attribute list * (term * (term list * term list)) list)
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    34
      * Comment.text) list -> ProofHistory.T -> ProofHistory.T
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    35
end;
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    36
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    37
functor ObtainFun(Data: OBTAIN_DATA): OBTAIN =
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    38
struct
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    39
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    40
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    41
(** export_obtained **)
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    42
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    43
fun disch_obtained state parms rule cprops thm =
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    44
  let
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    45
    val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    46
    val cparms = map (Thm.cterm_of sign) parms;
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    47
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    48
    val thm' = thm
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    49
      |> Drule.implies_intr_list cprops
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    50
      |> Drule.forall_intr_list cparms
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    51
      |> Drule.forall_elim_vars (maxidx + 1);
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    52
    val elim_tacs = replicate (length cprops) Proof.hard_asm_tac;
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    53
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    54
    val concl = Logic.strip_assums_concl prop;
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    55
    val bads = parms inter (Term.term_frees concl);
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    56
  in
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    57
    if not (null bads) then
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    58
      raise Proof.STATE ("Result contains illegal parameters: " ^
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    59
        space_implode " " (map (Sign.string_of_term sign) bads), state)
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    60
    else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    61
      raise Proof.STATE ("Conclusion of result is not an object-logic judgment", state)
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    62
    else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    63
  end;
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    64
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    65
fun export_obtained state parms rule =
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    66
  (disch_obtained state parms rule, fn _ => fn _ => []);
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    67
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    68
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    69
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    70
(** obtain(_i) **)
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    71
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    72
val thatN = "that";
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    73
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    74
fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    75
  let
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    76
    val _ = Proof.assert_forward_or_chain state;
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    77
    val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    78
8543
f54926bded7b handle general case: params and hyps of thesis;
wenzelm
parents: 8109
diff changeset
    79
    (*obtain vars*)
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    80
    val (vars_ctxt, vars) =
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    81
      foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    82
    val xs = flat (map fst vars);
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    83
    val thesisN = Term.variant xs AutoBind.thesisN;
9293
3da2533e0a61 bind_skolem;
wenzelm
parents: 8807
diff changeset
    84
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
    85
    val bind_skolem = ProofContext.bind_skolem vars_ctxt (xs @ [thesisN]);
9293
3da2533e0a61 bind_skolem;
wenzelm
parents: 8807
diff changeset
    86
    fun bind_propp (prop, (pats1, pats2)) =
3da2533e0a61 bind_skolem;
wenzelm
parents: 8807
diff changeset
    87
      (bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2));
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    88
8543
f54926bded7b handle general case: params and hyps of thesis;
wenzelm
parents: 8109
diff changeset
    89
    (*obtain asms*)
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    90
    fun prep_asm (ctxt, (name, src, raw_propps)) =
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    91
      let
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    92
        val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    93
        val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
9293
3da2533e0a61 bind_skolem;
wenzelm
parents: 8807
diff changeset
    94
      in (ctxt', ((name, atts, map bind_propp propps), map #1 propps)) end;
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
    95
9293
3da2533e0a61 bind_skolem;
wenzelm
parents: 8807
diff changeset
    96
    val (asms_ctxt, asms_result) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
3da2533e0a61 bind_skolem;
wenzelm
parents: 8807
diff changeset
    97
    val (asms, asm_propss) = Library.split_list asms_result;
3da2533e0a61 bind_skolem;
wenzelm
parents: 8807
diff changeset
    98
    val asm_props = flat asm_propss;
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
    99
    val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
   100
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   101
    (*that_prop*)
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
   102
    fun find_free x t =
8614
30cc975727f1 ProofContext.find_free;
wenzelm
parents: 8543
diff changeset
   103
      (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   104
    fun occs_var x = Library.get_first (find_free x) asm_props;
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   105
    val xs' = mapfilter occs_var xs;
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   106
    val parms = map (bind_skolem o Free) xs';
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   107
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   108
    val bound_thesis = bind_skolem (Data.atomic_thesis thesisN);
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   109
    val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
   110
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   111
    fun after_qed st = st
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   112
      |> Proof.end_block
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   113
      |> Seq.map (fn st' => st'
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   114
        |> Proof.fix_i vars
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   115
        |> Proof.assm_i (export_obtained state parms (Proof.the_fact st')) asms);
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
   116
  in
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   117
    state
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   118
    |> Proof.enter_forward
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   119
    |> Proof.begin_block
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   120
    |> Proof.fix_i [([thesisN], None)]
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   121
    |> Proof.assume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   122
    |> Proof.from_facts chain_facts
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   123
    |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
   124
  end;
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
   125
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
   126
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   127
val obtain = ProofHistory.apply o
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   128
  (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   129
9468
9adbcf6375c1 turned into plain context element;
wenzelm
parents: 9293
diff changeset
   130
val obtain_i = ProofHistory.apply o
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   131
  (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   132
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   133
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   134
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   135
(** outer syntax **)
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   136
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   137
local structure P = OuterParse and K = OuterSyntax.Keyword in
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   138
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   139
val obtainP =
8543
f54926bded7b handle general case: params and hyps of thesis;
wenzelm
parents: 8109
diff changeset
   140
  OuterSyntax.command "obtain" "generalized existence"
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   141
    K.prf_asm_goal
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   142
    (Scan.optional
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   143
      (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
8109
aca11f954993 obtain: renamed 'in' to 'where';
wenzelm
parents: 8094
diff changeset
   144
        --| P.$$$ "where") [] --
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   145
      P.and_list1 ((P.opt_thm_name ":" -- Scan.repeat1 P.propp >> P.triple1) -- P.marg_comment)
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   146
    >> (Toplevel.print oo (Toplevel.proof o obtain)));
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   147
8109
aca11f954993 obtain: renamed 'in' to 'where';
wenzelm
parents: 8094
diff changeset
   148
val _ = OuterSyntax.add_keywords ["where"];
8094
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   149
val _ = OuterSyntax.add_parsers [obtainP];
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   150
62b45a2e6ecb ObtainFun;
wenzelm
parents: 7923
diff changeset
   151
end;
7674
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
   152
99305245f6bd The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff changeset
   153
end;