author | wenzelm |
Wed, 09 Nov 2005 16:26:54 +0100 | |
changeset 18139 | b15981aedb7b |
parent 18119 | 63901a9b99dc |
child 18145 | 6757627acf59 |
permissions | -rw-r--r-- |
17980 | 1 |
(* Title: Pure/goal.ML |
2 |
ID: $Id$ |
|
3 |
Author: Makarius and Lawrence C Paulson |
|
4 |
||
18139 | 5 |
Goals in tactical theorem proving. |
17980 | 6 |
*) |
7 |
||
8 |
signature BASIC_GOAL = |
|
9 |
sig |
|
10 |
val SELECT_GOAL: tactic -> int -> tactic |
|
11 |
end; |
|
12 |
||
13 |
signature GOAL = |
|
14 |
sig |
|
15 |
include BASIC_GOAL |
|
16 |
val init: cterm -> thm |
|
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
17 |
val protect: thm -> thm |
17980 | 18 |
val conclude: thm -> thm |
19 |
val finish: thm -> thm |
|
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
20 |
val norm_hhf: thm -> thm |
18119 | 21 |
val compose_hhf: thm -> int -> thm -> thm Seq.seq |
22 |
val compose_hhf_tac: thm -> int -> tactic |
|
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
23 |
val comp_hhf: thm -> thm -> thm |
17980 | 24 |
val prove_multi: theory -> string list -> term list -> term list -> |
25 |
(thm list -> tactic) -> thm list |
|
18139 | 26 |
val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm |
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
27 |
val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm |
17980 | 28 |
end; |
29 |
||
30 |
structure Goal: GOAL = |
|
31 |
struct |
|
32 |
||
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
33 |
(** goals **) |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
34 |
|
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
35 |
(* |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
36 |
-------- (init) |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
37 |
C ==> #C |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
38 |
*) |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
39 |
fun init ct = Drule.instantiate' [] [SOME ct] Drule.protectI; |
17980 | 40 |
|
41 |
(* |
|
18119 | 42 |
C |
43 |
--- (protect) |
|
44 |
#C |
|
17980 | 45 |
*) |
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
46 |
fun protect th = th COMP Drule.incr_indexes th Drule.protectI; |
17980 | 47 |
|
48 |
(* |
|
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
49 |
A ==> ... ==> #C |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
50 |
---------------- (conclude) |
17980 | 51 |
A ==> ... ==> C |
52 |
*) |
|
53 |
fun conclude th = |
|
54 |
(case SINGLE (Thm.bicompose false (false, th, Thm.nprems_of th) 1) |
|
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
55 |
(Drule.incr_indexes th Drule.protectD) of |
17980 | 56 |
SOME th' => th' |
57 |
| NONE => raise THM ("Failed to conclude goal", 0, [th])); |
|
58 |
||
59 |
(* |
|
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
60 |
#C |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
61 |
--- (finish) |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
62 |
C |
17983 | 63 |
*) |
17980 | 64 |
fun finish th = |
65 |
(case Thm.nprems_of th of |
|
66 |
0 => conclude th |
|
67 |
| n => raise THM ("Proof failed.\n" ^ |
|
68 |
Pretty.string_of (Pretty.chunks (Display.pretty_goals n th)) ^ |
|
69 |
("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th])); |
|
70 |
||
71 |
||
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
72 |
|
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
73 |
(** results **) |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
74 |
|
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
75 |
(* HHF normal form *) |
17980 | 76 |
|
18119 | 77 |
val norm_hhf = |
17980 | 78 |
(not o Drule.is_norm_hhf o Thm.prop_of) ? |
18119 | 79 |
MetaSimplifier.simplify_aux (K (K NONE)) true [Drule.norm_hhf_eq] |
17980 | 80 |
#> Thm.adjust_maxidx_thm |
81 |
#> Drule.gen_all; |
|
82 |
||
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
83 |
|
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
84 |
(* composition of normal results *) |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
85 |
|
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
86 |
fun compose_hhf tha i thb = |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
87 |
Thm.bicompose false (false, Drule.lift_all (Thm.cgoal_of thb i) tha, 0) i thb; |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
88 |
|
18119 | 89 |
fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i); |
90 |
||
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
91 |
fun comp_hhf tha thb = |
18119 | 92 |
(case Seq.chop (2, compose_hhf tha 1 thb) of |
93 |
([th], _) => th |
|
94 |
| ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb]) |
|
95 |
| _ => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb])); |
|
17986 | 96 |
|
97 |
||
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
98 |
|
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
99 |
(** tactical theorem proving **) |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
100 |
|
18119 | 101 |
(* prove_multi *) |
17986 | 102 |
|
18119 | 103 |
fun prove_multi thy xs asms props tac = |
17980 | 104 |
let |
105 |
val prop = Logic.mk_conjunction_list props; |
|
106 |
val statement = Logic.list_implies (asms, prop); |
|
18139 | 107 |
val frees = Term.add_frees statement []; |
17980 | 108 |
val fixed_frees = filter_out (member (op =) xs o #1) frees; |
18139 | 109 |
val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees []; |
17980 | 110 |
val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs; |
111 |
||
112 |
fun err msg = raise ERROR_MESSAGE |
|
113 |
(msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^ |
|
114 |
Sign.string_of_term thy (Term.list_all_free (params, statement))); |
|
115 |
||
116 |
fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t) |
|
117 |
handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; |
|
118 |
||
119 |
val _ = cert_safe statement; |
|
120 |
val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg; |
|
121 |
||
122 |
val cparams = map (cert_safe o Free) params; |
|
123 |
val casms = map cert_safe asms; |
|
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
124 |
val prems = map (norm_hhf o Thm.assume) casms; |
17980 | 125 |
|
126 |
val goal = init (cert_safe prop); |
|
18119 | 127 |
val goal' = case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed."; |
17980 | 128 |
val raw_result = finish goal' handle THM (msg, _, _) => err msg; |
129 |
||
130 |
val prop' = Thm.prop_of raw_result; |
|
17986 | 131 |
val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () => |
17980 | 132 |
err ("Proved a different theorem: " ^ Sign.string_of_term thy prop')); |
133 |
in |
|
134 |
Drule.conj_elim_precise (length props) raw_result |
|
135 |
|> map |
|
136 |
(Drule.implies_intr_list casms |
|
137 |
#> Drule.forall_intr_list cparams |
|
18119 | 138 |
#> norm_hhf |
18139 | 139 |
#> Thm.varifyT' fixed_tfrees |
140 |
#-> K Drule.zero_var_indexes) |
|
17980 | 141 |
end; |
142 |
||
143 |
||
18119 | 144 |
(* prove *) |
17980 | 145 |
|
146 |
fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac); |
|
147 |
||
148 |
||
18027
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
149 |
(* prove_raw -- no checks, no normalization of result! *) |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
150 |
|
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
151 |
fun prove_raw casms cprop tac = |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
152 |
(case SINGLE (tac (map (norm_hhf o Thm.assume) casms)) (init cprop) of |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
153 |
SOME th => Drule.implies_intr_list casms (finish th) |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
154 |
| NONE => raise ERROR_MESSAGE "Tactic failed."); |
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
155 |
|
09ab79d4e8e1
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17986
diff
changeset
|
156 |
|
17980 | 157 |
(* SELECT_GOAL *) |
158 |
||
159 |
(*Tactical for restricting the effect of a tactic to subgoal i. Works |
|
160 |
by making a new state from subgoal i, applying tac to it, and |
|
161 |
composing the resulting thm with the original state.*) |
|
162 |
||
163 |
fun SELECT tac i st = |
|
164 |
init (Thm.adjust_maxidx (List.nth (Drule.cprems_of st, i - 1))) |
|
165 |
|> tac |
|
166 |
|> Seq.maps (fn st' => Thm.bicompose false (false, conclude st', Thm.nprems_of st') i st); |
|
167 |
||
168 |
fun SELECT_GOAL tac i st = |
|
169 |
let val n = Thm.nprems_of st in |
|
170 |
if 1 <= i andalso i <= n then |
|
171 |
if n = 1 then tac st else SELECT tac i st |
|
172 |
else Seq.empty |
|
173 |
end; |
|
174 |
||
175 |
end; |
|
176 |
||
177 |
structure BasicGoal: BASIC_GOAL = Goal; |
|
178 |
open BasicGoal; |