|
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; |