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