17980
|
1 |
(* Title: Pure/goal.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius and Lawrence C Paulson
|
|
4 |
|
|
5 |
Internal goals. NB: by attaching the Goal constant the conclusion of
|
|
6 |
a goal state is guaranteed to be atomic.
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature BASIC_GOAL =
|
|
10 |
sig
|
|
11 |
val SELECT_GOAL: tactic -> int -> tactic
|
|
12 |
end;
|
|
13 |
|
|
14 |
signature GOAL =
|
|
15 |
sig
|
|
16 |
include BASIC_GOAL
|
|
17 |
val init: cterm -> thm
|
|
18 |
val conclude: thm -> thm
|
|
19 |
val finish: thm -> thm
|
|
20 |
val prove_raw: theory -> term -> tactic -> thm
|
|
21 |
val norm_hhf_rule: thm -> thm
|
|
22 |
val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
|
|
23 |
val prove_multi: theory -> string list -> term list -> term list ->
|
|
24 |
(thm list -> tactic) -> thm list
|
|
25 |
|
|
26 |
(* FIXME remove *)
|
|
27 |
val norm_hhf_plain: thm -> thm
|
|
28 |
val prove_multi_plain: theory -> string list -> term list -> term list ->
|
|
29 |
(thm list -> tactic) -> thm list
|
|
30 |
val prove_plain: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
|
|
31 |
end;
|
|
32 |
|
|
33 |
structure Goal: GOAL =
|
|
34 |
struct
|
|
35 |
|
|
36 |
(* managing goal states *)
|
|
37 |
|
|
38 |
(*
|
|
39 |
----------------- (init)
|
|
40 |
Goal C ==> Goal C
|
|
41 |
*)
|
|
42 |
fun init ct = Drule.instantiate' [] [SOME ct] Drule.goalI;
|
|
43 |
|
|
44 |
(*
|
|
45 |
A ==> ... ==> Goal C
|
|
46 |
-------------------- (conclude)
|
|
47 |
A ==> ... ==> C
|
|
48 |
*)
|
|
49 |
fun conclude th =
|
|
50 |
(case SINGLE (Thm.bicompose false (false, th, Thm.nprems_of th) 1)
|
|
51 |
(Drule.incr_indexes_wrt [] [] [] [th] Drule.goalD) of
|
|
52 |
SOME th' => th'
|
|
53 |
| NONE => raise THM ("Failed to conclude goal", 0, [th]));
|
|
54 |
|
|
55 |
(*
|
|
56 |
Goal C
|
|
57 |
------ (finish)
|
|
58 |
C
|
|
59 |
*)
|
|
60 |
fun finish th =
|
|
61 |
(case Thm.nprems_of th of
|
|
62 |
0 => conclude th
|
|
63 |
| n => raise THM ("Proof failed.\n" ^
|
|
64 |
Pretty.string_of (Pretty.chunks (Display.pretty_goals n th)) ^
|
|
65 |
("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
|
|
66 |
|
|
67 |
|
|
68 |
(* prove_raw -- minimal checks, no normalization *)
|
|
69 |
|
|
70 |
fun prove_raw thy goal tac =
|
|
71 |
(case SINGLE tac (init (Thm.cterm_of thy goal)) of
|
|
72 |
SOME th => finish th
|
|
73 |
| NONE => raise ERROR_MESSAGE "Tactic failed.");
|
|
74 |
|
|
75 |
|
|
76 |
(* tactical proving *)
|
|
77 |
|
|
78 |
val norm_hhf_plain = (* FIXME remove *)
|
|
79 |
(not o Drule.is_norm_hhf o Thm.prop_of) ?
|
|
80 |
MetaSimplifier.simplify_aux (K (K NONE)) true [Drule.norm_hhf_eq];
|
|
81 |
|
|
82 |
val norm_hhf_rule =
|
|
83 |
norm_hhf_plain
|
|
84 |
#> Thm.adjust_maxidx_thm
|
|
85 |
#> Drule.gen_all;
|
|
86 |
|
|
87 |
local
|
|
88 |
|
|
89 |
fun gen_prove finish_thm thy xs asms props tac =
|
|
90 |
let
|
|
91 |
val prop = Logic.mk_conjunction_list props;
|
|
92 |
val statement = Logic.list_implies (asms, prop);
|
|
93 |
val frees = map Term.dest_Free (Term.term_frees statement);
|
|
94 |
val fixed_frees = filter_out (member (op =) xs o #1) frees;
|
|
95 |
val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees);
|
|
96 |
val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
|
|
97 |
|
|
98 |
fun err msg = raise ERROR_MESSAGE
|
|
99 |
(msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
|
|
100 |
Sign.string_of_term thy (Term.list_all_free (params, statement)));
|
|
101 |
|
|
102 |
fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
|
|
103 |
handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
|
|
104 |
|
|
105 |
val _ = cert_safe statement;
|
|
106 |
val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg;
|
|
107 |
|
|
108 |
val cparams = map (cert_safe o Free) params;
|
|
109 |
val casms = map cert_safe asms;
|
|
110 |
val prems = map (norm_hhf_rule o Thm.assume) casms;
|
|
111 |
|
|
112 |
val goal = init (cert_safe prop);
|
|
113 |
val goal' = (case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed.");
|
|
114 |
val raw_result = finish goal' handle THM (msg, _, _) => err msg;
|
|
115 |
|
|
116 |
val prop' = Thm.prop_of raw_result;
|
|
117 |
val _ = conditional (not (Pattern.matches thy (prop, prop'))) (fn () =>
|
|
118 |
err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
|
|
119 |
in
|
|
120 |
Drule.conj_elim_precise (length props) raw_result
|
|
121 |
|> map
|
|
122 |
(Drule.implies_intr_list casms
|
|
123 |
#> Drule.forall_intr_list cparams
|
|
124 |
#> finish_thm fixed_tfrees)
|
|
125 |
end;
|
|
126 |
|
|
127 |
in
|
|
128 |
|
|
129 |
fun prove_multi thy xs asms prop tac =
|
|
130 |
gen_prove (fn fixed_tfrees => Drule.zero_var_indexes o
|
|
131 |
(#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule)
|
|
132 |
thy xs asms prop tac;
|
|
133 |
|
|
134 |
fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac);
|
|
135 |
|
|
136 |
fun prove_multi_plain thy xs asms prop tac = gen_prove (K norm_hhf_plain) thy xs asms prop tac;
|
|
137 |
fun prove_plain thy xs asms prop tac = hd (prove_multi_plain thy xs asms [prop] tac);
|
|
138 |
|
|
139 |
end;
|
|
140 |
|
|
141 |
|
|
142 |
(* SELECT_GOAL *)
|
|
143 |
|
|
144 |
(*Tactical for restricting the effect of a tactic to subgoal i. Works
|
|
145 |
by making a new state from subgoal i, applying tac to it, and
|
|
146 |
composing the resulting thm with the original state.*)
|
|
147 |
|
|
148 |
fun SELECT tac i st =
|
|
149 |
init (Thm.adjust_maxidx (List.nth (Drule.cprems_of st, i - 1)))
|
|
150 |
|> tac
|
|
151 |
|> Seq.maps (fn st' => Thm.bicompose false (false, conclude st', Thm.nprems_of st') i st);
|
|
152 |
|
|
153 |
fun SELECT_GOAL tac i st =
|
|
154 |
let val n = Thm.nprems_of st in
|
|
155 |
if 1 <= i andalso i <= n then
|
|
156 |
if n = 1 then tac st else SELECT tac i st
|
|
157 |
else Seq.empty
|
|
158 |
end;
|
|
159 |
|
|
160 |
|
|
161 |
end;
|
|
162 |
|
|
163 |
structure BasicGoal: BASIC_GOAL = Goal;
|
|
164 |
open BasicGoal;
|