author | wenzelm |
Wed, 27 Feb 2002 21:53:33 +0100 | |
changeset 12970 | c9b1838a2cc0 |
parent 12404 | 968213967c07 |
child 14981 | e73f8140af78 |
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 |
|
12970 | 12 |
have "!!thesis. (!!x. P x ==> thesis) ==> thesis" |
13 |
proof succeed |
|
9468 | 14 |
fix thesis |
12970 | 15 |
assume that [intro?]: "!!x. P x ==> thesis" |
16 |
<chain_facts> show thesis <proof (insert that)> |
|
17 |
qed |
|
10379
93630e0c5ae9
improved handling of "that": insert into goal, only declare as Pure "intro";
wenzelm
parents:
9481
diff
changeset
|
18 |
fix x assm (obtained) "P x" |
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 |
11890 | 23 |
val obtain: (string list * string option) list -> |
24 |
((string * Proof.context attribute list) * (string * (string list * string list)) list) list |
|
12970 | 25 |
-> (Proof.context -> string * (string * thm list) list -> unit) * |
26 |
(Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq |
|
11890 | 27 |
val obtain_i: (string list * typ option) list -> |
28 |
((string * Proof.context attribute list) * (term * (term list * term list)) list) list |
|
12970 | 29 |
-> (Proof.context -> string * (string * thm list) list -> unit) * |
30 |
(Proof.context -> thm -> unit) -> Proof.state -> Proof.state Seq.seq |
|
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
31 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
32 |
|
10379
93630e0c5ae9
improved handling of "that": insert into goal, only declare as Pure "intro";
wenzelm
parents:
9481
diff
changeset
|
33 |
structure Obtain: OBTAIN = |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
34 |
struct |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
35 |
|
8094 | 36 |
|
11816 | 37 |
(** export_obtain **) |
9468 | 38 |
|
11816 | 39 |
fun export_obtain state parms rule _ cprops thm = |
9468 | 40 |
let |
41 |
val {sign, prop, maxidx, ...} = Thm.rep_thm thm; |
|
42 |
val cparms = map (Thm.cterm_of sign) parms; |
|
43 |
||
44 |
val thm' = thm |
|
11816 | 45 |
|> Drule.implies_intr_goals cprops |
9468 | 46 |
|> Drule.forall_intr_list cparms |
47 |
|> Drule.forall_elim_vars (maxidx + 1); |
|
11816 | 48 |
val elim_tacs = replicate (length cprops) (Tactic.etac Drule.triv_goal); |
9468 | 49 |
|
50 |
val concl = Logic.strip_assums_concl prop; |
|
51 |
val bads = parms inter (Term.term_frees concl); |
|
52 |
in |
|
53 |
if not (null bads) then |
|
9481 | 54 |
raise Proof.STATE ("Conclusion contains obtained parameters: " ^ |
12055 | 55 |
space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state) |
11764 | 56 |
else if not (ObjectLogic.is_judgment sign (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
|
57 |
raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state) |
9468 | 58 |
else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule |
59 |
end; |
|
60 |
||
61 |
||
62 |
||
8094 | 63 |
(** obtain(_i) **) |
64 |
||
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
65 |
val thatN = "that"; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
66 |
|
12970 | 67 |
fun gen_obtain prep_vars prep_propp raw_vars raw_asms print state = |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
68 |
let |
9468 | 69 |
val _ = Proof.assert_forward_or_chain state; |
70 |
val chain_facts = if Proof.is_chain state then Proof.the_facts state else []; |
|
10464 | 71 |
val thy = Proof.theory_of state; |
11764 | 72 |
val sign = Theory.sign_of thy; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
73 |
|
8543 | 74 |
(*obtain vars*) |
11890 | 75 |
val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, raw_vars); |
8094 | 76 |
val xs = flat (map fst vars); |
10582 | 77 |
val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
78 |
|
8543 | 79 |
(*obtain asms*) |
11890 | 80 |
val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); |
10464 | 81 |
val asm_props = flat (map (map fst) proppss); |
11890 | 82 |
val asms = map fst raw_asms ~~ proppss; |
10464 | 83 |
|
10582 | 84 |
val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt; |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
85 |
|
12970 | 86 |
(*obtain statements*) |
12404 | 87 |
val thesisN = Term.variant xs (Syntax.internal AutoBind.thesisN); |
12970 | 88 |
val bind_thesis = ProofContext.bind_skolem fix_ctxt [thesisN]; |
89 |
val bound_thesis = bind_thesis (ObjectLogic.fixed_judgment sign thesisN); |
|
90 |
val bound_thesis_raw as (bound_thesis_name, _) = |
|
91 |
Term.dest_Free (bind_thesis (Free (thesisN, propT))); |
|
92 |
val bound_thesis_var = |
|
93 |
foldl_aterms (fn (v, Free (x, T)) => if x = bound_thesis_name then (x, T) else v |
|
94 |
| (v, t) => v) (bound_thesis_raw, bound_thesis); |
|
9468 | 95 |
|
10582 | 96 |
fun occs_var x = Library.get_first (fn t => |
97 |
ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props; |
|
98 |
val raw_parms = map occs_var xs; |
|
99 |
val parms = mapfilter I raw_parms; |
|
100 |
val parm_names = |
|
101 |
mapfilter (fn (Some (Free a), x) => Some (a, x) | _ => None) (raw_parms ~~ xs); |
|
102 |
||
103 |
val that_prop = |
|
104 |
Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis)) |
|
105 |
|> Library.curry Logic.list_rename_params (map #2 parm_names); |
|
12970 | 106 |
val obtain_prop = |
107 |
Logic.list_rename_params ([AutoBind.thesisN], |
|
108 |
Term.list_all_free ([bound_thesis_var], Logic.mk_implies (that_prop, bound_thesis))); |
|
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
109 |
|
9468 | 110 |
fun after_qed st = st |
12970 | 111 |
|> Method.local_qed false None print |
9468 | 112 |
|> Seq.map (fn st' => st' |
113 |
|> Proof.fix_i vars |
|
11816 | 114 |
|> Proof.assm_i (export_obtain state parms (Proof.the_fact st')) asms); |
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
115 |
in |
8094 | 116 |
state |
9468 | 117 |
|> Proof.enter_forward |
12970 | 118 |
|> Proof.have_i Seq.single true [(("", []), [(obtain_prop, ([], []))])] |
119 |
|> Method.proof (Some (Method.Basic (K Method.succeed))) |> Seq.hd |
|
9468 | 120 |
|> Proof.fix_i [([thesisN], None)] |
12350 | 121 |
|> Proof.assume_i [((thatN, [ContextRules.intro_query_local None]), [(that_prop, ([], []))])] |
10379
93630e0c5ae9
improved handling of "that": insert into goal, only declare as Pure "intro";
wenzelm
parents:
9481
diff
changeset
|
122 |
|> (fn state' => |
12970 | 123 |
state' |
124 |
|> Proof.from_facts chain_facts |
|
125 |
|> Proof.show_i (K I) after_qed false [(("", []), [(bound_thesis, ([], []))])] false |
|
126 |
|> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state'))))) |
|
7674
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
127 |
end; |
99305245f6bd
The 'obtain' language element -- achieves (eliminated) existential
wenzelm
parents:
diff
changeset
|
128 |
|
11890 | 129 |
val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp; |
130 |
val obtain_i = gen_obtain ProofContext.cert_vars ProofContext.cert_propp; |
|
8094 | 131 |
|
132 |
end; |