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