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