author | wenzelm |
Sat, 02 Apr 2016 23:29:05 +0200 | |
changeset 62826 | eb94e570c1a4 |
parent 61268 | abe08fb15a12 |
child 67149 | e61557884799 |
permissions | -rw-r--r-- |
30160
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
29273
diff
changeset
|
1 |
(* Title: Tools/coherent.ML |
28326 | 2 |
Author: Stefan Berghofer, TU Muenchen |
31241 | 3 |
Author: Marc Bezem, Institutt for Informatikk, Universitetet i Bergen |
28326 | 4 |
|
5 |
Prover for coherent logic, see e.g. |
|
6 |
||
7 |
Marc Bezem and Thierry Coquand, Automating Coherent Logic, LPAR 2005 |
|
8 |
||
9 |
for a description of the algorithm. |
|
10 |
*) |
|
11 |
||
12 |
signature COHERENT_DATA = |
|
13 |
sig |
|
14 |
val atomize_elimL: thm |
|
15 |
val atomize_exL: thm |
|
16 |
val atomize_conjL: thm |
|
17 |
val atomize_disjL: thm |
|
18 |
val operator_names: string list |
|
19 |
end; |
|
20 |
||
21 |
signature COHERENT = |
|
22 |
sig |
|
55632 | 23 |
val trace: bool Config.T |
31241 | 24 |
val coherent_tac: Proof.context -> thm list -> int -> tactic |
28326 | 25 |
end; |
26 |
||
32734 | 27 |
functor Coherent(Data: COHERENT_DATA) : COHERENT = |
28326 | 28 |
struct |
29 |
||
31241 | 30 |
(** misc tools **) |
31 |
||
55632 | 32 |
val (trace, trace_setup) = Attrib.config_bool @{binding coherent_trace} (K false); |
33 |
fun cond_trace ctxt msg = if Config.get ctxt trace then tracing (msg ()) else (); |
|
28326 | 34 |
|
35 |
datatype cl_prf = |
|
36 |
ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list * |
|
37 |
int list * (term list * cl_prf) list; |
|
38 |
||
29273 | 39 |
val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1); |
28326 | 40 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
46186
diff
changeset
|
41 |
fun rulify_elim_conv ctxt ct = |
59582 | 42 |
if is_atomic (Logic.strip_imp_concl (Thm.term_of ct)) then Conv.all_conv ct |
43 |
else Conv.concl_conv (length (Logic.strip_imp_prems (Thm.term_of ct))) |
|
36946 | 44 |
(Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
46186
diff
changeset
|
45 |
Raw_Simplifier.rewrite ctxt true (map Thm.symmetric |
28326 | 46 |
[Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct |
47 |
||
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
48 |
fun rulify_elim ctxt th = Simplifier.norm_hhf ctxt (Conv.fconv_rule (rulify_elim_conv ctxt) th); |
28326 | 49 |
|
50 |
(* Decompose elimination rule of the form |
|
51 |
A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P |
|
52 |
*) |
|
53 |
fun dest_elim prop = |
|
54 |
let |
|
55 |
val prems = Logic.strip_imp_prems prop; |
|
56 |
val concl = Logic.strip_imp_concl prop; |
|
57 |
val (prems1, prems2) = |
|
58 |
take_suffix (fn t => Logic.strip_assums_concl t = concl) prems; |
|
59 |
in |
|
60 |
(prems1, |
|
61 |
if null prems2 then [([], [concl])] |
|
62 |
else map (fn t => |
|
63 |
(map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2) |
|
64 |
end; |
|
65 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
46186
diff
changeset
|
66 |
fun mk_rule ctxt th = |
28326 | 67 |
let |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
46186
diff
changeset
|
68 |
val th' = rulify_elim ctxt th; |
59582 | 69 |
val (prems, cases) = dest_elim (Thm.prop_of th') |
28326 | 70 |
in (th', prems, cases) end; |
71 |
||
72 |
fun mk_dom ts = fold (fn t => |
|
73 |
Typtab.map_default (fastype_of t, []) (fn us => us @ [t])) ts Typtab.empty; |
|
74 |
||
75 |
val empty_env = (Vartab.empty, Vartab.empty); |
|
76 |
||
77 |
(* Find matcher that makes conjunction valid in given state *) |
|
55631 | 78 |
fun valid_conj _ _ env [] = Seq.single (env, []) |
28326 | 79 |
| valid_conj ctxt facts env (t :: ts) = |
80 |
Seq.maps (fn (u, x) => Seq.map (apsnd (cons x)) |
|
81 |
(valid_conj ctxt facts |
|
42361 | 82 |
(Pattern.match (Proof_Context.theory_of ctxt) (t, u) env) ts |
28326 | 83 |
handle Pattern.MATCH => Seq.empty)) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58839
diff
changeset
|
84 |
(Seq.of_list (sort (int_ord o apply2 snd) (Net.unify_term facts t))); |
28326 | 85 |
|
86 |
(* Instantiate variables that only occur free in conlusion *) |
|
87 |
fun inst_extra_vars ctxt dom cs = |
|
88 |
let |
|
89 |
val vs = fold Term.add_vars (maps snd cs) []; |
|
90 |
fun insts [] inst = Seq.single inst |
|
55627 | 91 |
| insts ((ixn, T) :: vs') inst = |
92 |
Seq.maps (fn t => insts vs' (((ixn, T), t) :: inst)) |
|
93 |
(Seq.of_list |
|
94 |
(case Typtab.lookup dom T of |
|
95 |
NONE => |
|
96 |
error ("Unknown domain: " ^ |
|
97 |
Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^ |
|
98 |
commas (maps (map (Syntax.string_of_term ctxt) o snd) cs)) |
|
99 |
| SOME ts => ts)) |
|
100 |
in |
|
101 |
Seq.map (fn inst => |
|
102 |
(inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs)) |
|
103 |
(insts vs []) |
|
28326 | 104 |
end; |
105 |
||
106 |
(* Check whether disjunction is valid in given state *) |
|
55631 | 107 |
fun is_valid_disj _ _ [] = false |
28326 | 108 |
| is_valid_disj ctxt facts ((Ts, ts) :: ds) = |
55627 | 109 |
let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts in |
110 |
(case Seq.pull (valid_conj ctxt facts empty_env |
|
111 |
(map (fn t => subst_bounds (rev vs, t)) ts)) of |
|
28326 | 112 |
SOME _ => true |
55627 | 113 |
| NONE => is_valid_disj ctxt facts ds) |
28326 | 114 |
end; |
115 |
||
55627 | 116 |
fun string_of_facts ctxt s facts = |
55634 | 117 |
Pretty.string_of (Pretty.big_list s |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58839
diff
changeset
|
118 |
(map (Syntax.pretty_term ctxt) (map fst (sort (int_ord o apply2 snd) (Net.content facts))))); |
28326 | 119 |
|
120 |
fun valid ctxt rules goal dom facts nfacts nparams = |
|
55627 | 121 |
let |
122 |
val seq = |
|
123 |
Seq.of_list rules |> Seq.maps (fn (th, ps, cs) => |
|
124 |
valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) => |
|
125 |
let val cs' = map (fn (Ts, ts) => |
|
126 |
(map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs |
|
127 |
in |
|
128 |
inst_extra_vars ctxt dom cs' |> |
|
129 |
Seq.map_filter (fn (inst, cs'') => |
|
130 |
if is_valid_disj ctxt facts cs'' then NONE |
|
131 |
else SOME (th, env, inst, is, cs'')) |
|
132 |
end)); |
|
28326 | 133 |
in |
55627 | 134 |
(case Seq.pull seq of |
55634 | 135 |
NONE => |
136 |
(if Context_Position.is_visible ctxt then |
|
137 |
warning (string_of_facts ctxt "Countermodel found:" facts) |
|
138 |
else (); NONE) |
|
28326 | 139 |
| SOME ((th, env, inst, is, cs), _) => |
140 |
if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, [])) |
|
141 |
else |
|
142 |
(case valid_cases ctxt rules goal dom facts nfacts nparams cs of |
|
55627 | 143 |
NONE => NONE |
144 |
| SOME prfs => SOME (ClPrf (th, env, inst, is, prfs)))) |
|
28326 | 145 |
end |
146 |
||
55631 | 147 |
and valid_cases _ _ _ _ _ _ _ [] = SOME [] |
28326 | 148 |
| valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) = |
149 |
let |
|
55634 | 150 |
val _ = |
151 |
cond_trace ctxt (fn () => |
|
152 |
Pretty.string_of (Pretty.block |
|
153 |
(Pretty.str "case" :: Pretty.brk 1 :: |
|
154 |
Pretty.commas (map (Syntax.pretty_term ctxt) ts)))); |
|
55636 | 155 |
|
156 |
val ps = map_index (fn (i, T) => ("par" ^ string_of_int (nparams + i), T)) Ts; |
|
157 |
val (params, ctxt') = fold_map Variable.next_bound ps ctxt; |
|
55627 | 158 |
val ts' = map_index (fn (i, t) => (subst_bounds (rev params, t), nfacts + i)) ts; |
159 |
val dom' = |
|
160 |
fold (fn (T, p) => Typtab.map_default (T, []) (fn ps => ps @ [p])) (Ts ~~ params) dom; |
|
161 |
val facts' = fold (fn (t, i) => Net.insert_term op = (t, (t, i))) ts' facts; |
|
28326 | 162 |
in |
55636 | 163 |
(case valid ctxt' rules goal dom' facts' (nfacts + length ts) (nparams + length Ts) of |
28326 | 164 |
NONE => NONE |
55627 | 165 |
| SOME prf => |
166 |
(case valid_cases ctxt rules goal dom facts nfacts nparams ds of |
|
167 |
NONE => NONE |
|
168 |
| SOME prfs => SOME ((params, prf) :: prfs))) |
|
28326 | 169 |
end; |
170 |
||
31241 | 171 |
|
28326 | 172 |
(** proof replaying **) |
173 |
||
55632 | 174 |
fun thm_of_cl_prf ctxt goal asms (ClPrf (th, (tye, env), insts, is, prfs)) = |
28326 | 175 |
let |
55627 | 176 |
val _ = |
55632 | 177 |
cond_trace ctxt (fn () => |
61268 | 178 |
Pretty.string_of (Pretty.big_list "asms:" (map (Thm.pretty_thm ctxt) asms))); |
55627 | 179 |
val th' = |
180 |
Drule.implies_elim_list |
|
181 |
(Thm.instantiate |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59642
diff
changeset
|
182 |
(map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye), |
55627 | 183 |
map (fn (ixn, (T, t)) => |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59642
diff
changeset
|
184 |
((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @ |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59642
diff
changeset
|
185 |
map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts) th) |
55627 | 186 |
(map (nth asms) is); |
59582 | 187 |
val (_, cases) = dest_elim (Thm.prop_of th'); |
28326 | 188 |
in |
55627 | 189 |
(case (cases, prfs) of |
28326 | 190 |
([([], [_])], []) => th' |
55632 | 191 |
| ([([], [_])], [([], prf)]) => thm_of_cl_prf ctxt goal (asms @ [th']) prf |
55627 | 192 |
| _ => |
193 |
Drule.implies_elim_list |
|
194 |
(Thm.instantiate (Thm.match |
|
59582 | 195 |
(Drule.strip_imp_concl (Thm.cprop_of th'), goal)) th') |
55632 | 196 |
(map (thm_of_case_prf ctxt goal asms) (prfs ~~ cases))) |
28326 | 197 |
end |
198 |
||
55632 | 199 |
and thm_of_case_prf ctxt goal asms ((params, prf), (_, asms')) = |
28326 | 200 |
let |
59642 | 201 |
val cparams = map (Thm.cterm_of ctxt) params; |
202 |
val asms'' = map (Thm.cterm_of ctxt o curry subst_bounds (rev params)) asms'; |
|
55634 | 203 |
val (prems'', ctxt') = fold_map Thm.assume_hyps asms'' ctxt; |
28326 | 204 |
in |
55627 | 205 |
Drule.forall_intr_list cparams |
55634 | 206 |
(Drule.implies_intr_list asms'' (thm_of_cl_prf ctxt' goal (asms @ prems'') prf)) |
28326 | 207 |
end; |
208 |
||
209 |
||
210 |
(** external interface **) |
|
211 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
46186
diff
changeset
|
212 |
fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
213 |
resolve_tac ctxt' [rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2] 1 THEN |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
46186
diff
changeset
|
214 |
SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} => |
55627 | 215 |
let |
216 |
val xs = |
|
59582 | 217 |
map (Thm.term_of o #2) params @ |
55627 | 218 |
map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s))) |
219 |
(rev (Variable.dest_fixes ctxt'')) (* FIXME !? *) |
|
28326 | 220 |
in |
55632 | 221 |
(case |
59582 | 222 |
valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (Thm.term_of concl) |
55632 | 223 |
(mk_dom xs) Net.empty 0 0 of |
55627 | 224 |
NONE => no_tac |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
225 |
| SOME prf => resolve_tac ctxt'' [thm_of_cl_prf ctxt'' concl [] prf] 1) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
46186
diff
changeset
|
226 |
end) ctxt' 1) ctxt; |
28326 | 227 |
|
55632 | 228 |
val _ = Theory.setup |
229 |
(trace_setup #> |
|
230 |
Method.setup @{binding coherent} |
|
231 |
(Attrib.thms >> (fn rules => fn ctxt => |
|
232 |
METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules))))) |
|
233 |
"prove coherent formula"); |
|
28326 | 234 |
|
235 |
end; |