28326
|
1 |
(* Title: Provers/coherent.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Stefan Berghofer, TU Muenchen
|
|
4 |
Marc Bezem, Institutt for Informatikk, Universitetet i Bergen
|
|
5 |
|
|
6 |
Prover for coherent logic, see e.g.
|
|
7 |
|
|
8 |
Marc Bezem and Thierry Coquand, Automating Coherent Logic, LPAR 2005
|
|
9 |
|
|
10 |
for a description of the algorithm.
|
|
11 |
*)
|
|
12 |
|
|
13 |
signature COHERENT_DATA =
|
|
14 |
sig
|
|
15 |
val atomize_elimL: thm
|
|
16 |
val atomize_exL: thm
|
|
17 |
val atomize_conjL: thm
|
|
18 |
val atomize_disjL: thm
|
|
19 |
val operator_names: string list
|
|
20 |
end;
|
|
21 |
|
|
22 |
signature COHERENT =
|
|
23 |
sig
|
|
24 |
val verbose: bool ref
|
|
25 |
val show_facts: bool ref
|
|
26 |
val coherent_tac: thm list -> Proof.context -> int -> tactic
|
|
27 |
val coherent_meth: thm list -> Proof.context -> Proof.method
|
|
28 |
val setup: theory -> theory
|
|
29 |
end;
|
|
30 |
|
|
31 |
functor CoherentFun(Data: COHERENT_DATA) : COHERENT =
|
|
32 |
struct
|
|
33 |
|
|
34 |
val verbose = ref false;
|
|
35 |
|
|
36 |
fun message f = if !verbose then tracing (f ()) else ();
|
|
37 |
|
|
38 |
datatype cl_prf =
|
|
39 |
ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
|
|
40 |
int list * (term list * cl_prf) list;
|
|
41 |
|
|
42 |
fun is_atomic t = null (term_consts t inter Data.operator_names);
|
|
43 |
|
|
44 |
local open Conv in
|
|
45 |
|
|
46 |
fun rulify_elim_conv ct =
|
|
47 |
if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
|
|
48 |
else concl_conv (length (Logic.strip_imp_prems (term_of ct)))
|
|
49 |
(rewr_conv (symmetric Data.atomize_elimL) then_conv
|
|
50 |
MetaSimplifier.rewrite true (map symmetric
|
|
51 |
[Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
|
|
52 |
|
|
53 |
end;
|
|
54 |
|
|
55 |
fun rulify_elim th = MetaSimplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
|
|
56 |
|
|
57 |
(* Decompose elimination rule of the form
|
|
58 |
A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P
|
|
59 |
*)
|
|
60 |
fun dest_elim prop =
|
|
61 |
let
|
|
62 |
val prems = Logic.strip_imp_prems prop;
|
|
63 |
val concl = Logic.strip_imp_concl prop;
|
|
64 |
val (prems1, prems2) =
|
|
65 |
take_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
|
|
66 |
in
|
|
67 |
(prems1,
|
|
68 |
if null prems2 then [([], [concl])]
|
|
69 |
else map (fn t =>
|
|
70 |
(map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2)
|
|
71 |
end;
|
|
72 |
|
|
73 |
fun mk_rule th =
|
|
74 |
let
|
|
75 |
val th' = rulify_elim th;
|
|
76 |
val (prems, cases) = dest_elim (prop_of th')
|
|
77 |
in (th', prems, cases) end;
|
|
78 |
|
|
79 |
fun mk_dom ts = fold (fn t =>
|
|
80 |
Typtab.map_default (fastype_of t, []) (fn us => us @ [t])) ts Typtab.empty;
|
|
81 |
|
|
82 |
val empty_env = (Vartab.empty, Vartab.empty);
|
|
83 |
|
|
84 |
(* Find matcher that makes conjunction valid in given state *)
|
|
85 |
fun valid_conj ctxt facts env [] = Seq.single (env, [])
|
|
86 |
| valid_conj ctxt facts env (t :: ts) =
|
|
87 |
Seq.maps (fn (u, x) => Seq.map (apsnd (cons x))
|
|
88 |
(valid_conj ctxt facts
|
|
89 |
(Pattern.match (ProofContext.theory_of ctxt) (t, u) env) ts
|
|
90 |
handle Pattern.MATCH => Seq.empty))
|
|
91 |
(Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t)));
|
|
92 |
|
|
93 |
(* Instantiate variables that only occur free in conlusion *)
|
|
94 |
fun inst_extra_vars ctxt dom cs =
|
|
95 |
let
|
|
96 |
val vs = fold Term.add_vars (maps snd cs) [];
|
|
97 |
fun insts [] inst = Seq.single inst
|
|
98 |
| insts ((ixn, T) :: vs') inst = Seq.maps
|
|
99 |
(fn t => insts vs' (((ixn, T), t) :: inst))
|
|
100 |
(Seq.of_list (case Typtab.lookup dom T of
|
|
101 |
NONE => error ("Unknown domain: " ^
|
|
102 |
Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
|
|
103 |
commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
|
|
104 |
| SOME ts => ts))
|
|
105 |
in Seq.map (fn inst =>
|
|
106 |
(inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
|
|
107 |
(insts vs [])
|
|
108 |
end;
|
|
109 |
|
|
110 |
(* Check whether disjunction is valid in given state *)
|
|
111 |
fun is_valid_disj ctxt facts [] = false
|
|
112 |
| is_valid_disj ctxt facts ((Ts, ts) :: ds) =
|
|
113 |
let val vs = rev (map_index (fn (i, T) => Var (("x", i), T)) Ts)
|
|
114 |
in case Seq.pull (valid_conj ctxt facts empty_env
|
|
115 |
(map (fn t => subst_bounds (vs, t)) ts)) of
|
|
116 |
SOME _ => true
|
|
117 |
| NONE => is_valid_disj ctxt facts ds
|
|
118 |
end;
|
|
119 |
|
|
120 |
val show_facts = ref false;
|
|
121 |
|
|
122 |
fun string_of_facts ctxt s facts = space_implode "\n"
|
|
123 |
(s :: map (Syntax.string_of_term ctxt)
|
|
124 |
(map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
|
|
125 |
|
|
126 |
fun print_facts ctxt facts =
|
|
127 |
if !show_facts then message (fn () => string_of_facts ctxt "Facts:" facts)
|
|
128 |
else ();
|
|
129 |
|
|
130 |
fun valid ctxt rules goal dom facts nfacts nparams =
|
|
131 |
let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
|
|
132 |
valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
|
|
133 |
let val cs' = map (fn (Ts, ts) =>
|
|
134 |
(map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs
|
|
135 |
in
|
|
136 |
inst_extra_vars ctxt dom cs' |>
|
|
137 |
Seq.map_filter (fn (inst, cs'') =>
|
|
138 |
if is_valid_disj ctxt facts cs'' then NONE
|
|
139 |
else SOME (th, env, inst, is, cs''))
|
|
140 |
end))
|
|
141 |
in
|
|
142 |
case Seq.pull seq of
|
|
143 |
NONE => (tracing (string_of_facts ctxt "Countermodel found:" facts); NONE)
|
|
144 |
| SOME ((th, env, inst, is, cs), _) =>
|
|
145 |
if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, []))
|
|
146 |
else
|
|
147 |
(case valid_cases ctxt rules goal dom facts nfacts nparams cs of
|
|
148 |
NONE => NONE
|
|
149 |
| SOME prfs => SOME (ClPrf (th, env, inst, is, prfs)))
|
|
150 |
end
|
|
151 |
|
|
152 |
and valid_cases ctxt rules goal dom facts nfacts nparams [] = SOME []
|
|
153 |
| valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
|
|
154 |
let
|
|
155 |
val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
|
|
156 |
val params = rev (map_index (fn (i, T) =>
|
|
157 |
Free ("par" ^ string_of_int (nparams + i), T)) Ts);
|
|
158 |
val ts' = map_index (fn (i, t) =>
|
|
159 |
(subst_bounds (params, t), nfacts + i)) ts;
|
|
160 |
val dom' = fold (fn (T, p) =>
|
|
161 |
Typtab.map_default (T, []) (fn ps => ps @ [p]))
|
|
162 |
(Ts ~~ params) dom;
|
|
163 |
val facts' = fold (fn (t, i) => Net.insert_term op =
|
|
164 |
(t, (t, i))) ts' facts
|
|
165 |
in
|
|
166 |
case valid ctxt rules goal dom' facts'
|
|
167 |
(nfacts + length ts) (nparams + length Ts) of
|
|
168 |
NONE => NONE
|
|
169 |
| SOME prf => (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
|
|
170 |
NONE => NONE
|
|
171 |
| SOME prfs => SOME ((params, prf) :: prfs))
|
|
172 |
end;
|
|
173 |
|
|
174 |
(** proof replaying **)
|
|
175 |
|
|
176 |
fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
|
|
177 |
let
|
|
178 |
val _ = message (fn () => space_implode "\n"
|
|
179 |
("asms:" :: map Display.string_of_thm asms) ^ "\n\n");
|
|
180 |
val th' = Drule.implies_elim_list
|
|
181 |
(Thm.instantiate
|
|
182 |
(map (fn (ixn, (S, T)) =>
|
|
183 |
(Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
|
|
184 |
(Vartab.dest tye),
|
|
185 |
map (fn (ixn, (T, t)) =>
|
|
186 |
(Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)),
|
|
187 |
Thm.cterm_of thy t)) (Vartab.dest env) @
|
|
188 |
map (fn (ixnT, t) =>
|
|
189 |
(Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
|
|
190 |
(map (nth asms) is);
|
|
191 |
val (_, cases) = dest_elim (prop_of th')
|
|
192 |
in
|
|
193 |
case (cases, prfs) of
|
|
194 |
([([], [_])], []) => th'
|
|
195 |
| ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf
|
|
196 |
| _ => Drule.implies_elim_list
|
|
197 |
(Thm.instantiate (Thm.match
|
|
198 |
(Drule.strip_imp_concl (cprop_of th'), goal)) th')
|
|
199 |
(map (thm_of_case_prf thy goal asms) (prfs ~~ cases))
|
|
200 |
end
|
|
201 |
|
|
202 |
and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) =
|
|
203 |
let
|
|
204 |
val cparams = map (cterm_of thy) params;
|
|
205 |
val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms'
|
|
206 |
in
|
|
207 |
Drule.forall_intr_list cparams (Drule.implies_intr_list asms''
|
|
208 |
(thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf))
|
|
209 |
end;
|
|
210 |
|
|
211 |
|
|
212 |
(** external interface **)
|
|
213 |
|
|
214 |
fun coherent_tac rules ctxt = SUBPROOF (fn {prems, concl, params, context, ...} =>
|
|
215 |
rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
|
|
216 |
SUBPROOF (fn {prems = prems', concl, context, ...} =>
|
|
217 |
let val xs = map term_of params @
|
|
218 |
map (fn (_, s) => Free (s, the (Variable.default_type context s)))
|
|
219 |
(Variable.fixes_of context)
|
|
220 |
in
|
|
221 |
case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
|
|
222 |
(mk_dom xs) Net.empty 0 0 of
|
|
223 |
NONE => no_tac
|
|
224 |
| SOME prf =>
|
|
225 |
rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1
|
|
226 |
end) ctxt 1) ctxt;
|
|
227 |
|
|
228 |
fun coherent_meth rules ctxt =
|
|
229 |
Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
|
|
230 |
|
|
231 |
val setup = Method.add_method
|
|
232 |
("coherent", Method.thms_ctxt_args coherent_meth, "Prove coherent formula");
|
|
233 |
|
|
234 |
end;
|