author  berghofe 
Mon, 29 Jun 2009 20:05:44 +0200  
changeset 31855  7c2a5e79a654 
parent 31241  b3c7044d47b6 
child 32035  8e77b6a250d5 
permissions  rwrr 
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 

23 
val verbose: bool ref 

24 
val show_facts: bool ref 

31241  25 
val coherent_tac: Proof.context > thm list > int > tactic 
28326  26 
val setup: theory > theory 
27 
end; 

28 

29 
functor CoherentFun(Data: COHERENT_DATA) : COHERENT = 

30 
struct 

31 

31241  32 
(** misc tools **) 
33 

28326  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 

29273  42 
val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1); 
28326  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 

30552
58db56278478
provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
wenzelm
parents:
30510
diff
changeset

55 
fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th); 
28326  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) = 

31855  113 
let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts 
28326  114 
in case Seq.pull (valid_conj ctxt facts empty_env 
31855  115 
(map (fn t => subst_bounds (rev vs, t)) ts)) of 
28326  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)); 

31855  156 
val params = map_index (fn (i, T) => 
157 
Free ("par" ^ string_of_int (nparams + i), T)) Ts; 

28326  158 
val ts' = map_index (fn (i, t) => 
31855  159 
(subst_bounds (rev params, t), nfacts + i)) ts; 
28326  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 

31241  174 

28326  175 
(** proof replaying **) 
176 

177 
fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) = 

178 
let 

179 
val _ = message (fn () => space_implode "\n" 

180 
("asms:" :: map Display.string_of_thm asms) ^ "\n\n"); 

181 
val th' = Drule.implies_elim_list 

182 
(Thm.instantiate 

183 
(map (fn (ixn, (S, T)) => 

184 
(Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T)) 

185 
(Vartab.dest tye), 

186 
map (fn (ixn, (T, t)) => 

187 
(Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)), 

188 
Thm.cterm_of thy t)) (Vartab.dest env) @ 

189 
map (fn (ixnT, t) => 

190 
(Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th) 

191 
(map (nth asms) is); 

192 
val (_, cases) = dest_elim (prop_of th') 

193 
in 

194 
case (cases, prfs) of 

195 
([([], [_])], []) => th' 

196 
 ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf 

197 
 _ => Drule.implies_elim_list 

198 
(Thm.instantiate (Thm.match 

199 
(Drule.strip_imp_concl (cprop_of th'), goal)) th') 

200 
(map (thm_of_case_prf thy goal asms) (prfs ~~ cases)) 

201 
end 

202 

203 
and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) = 

204 
let 

205 
val cparams = map (cterm_of thy) params; 

206 
val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms' 

207 
in 

208 
Drule.forall_intr_list cparams (Drule.implies_intr_list asms'' 

209 
(thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf)) 

210 
end; 

211 

212 

213 
(** external interface **) 

214 

31241  215 
fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} => 
28326  216 
rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN 
217 
SUBPROOF (fn {prems = prems', concl, context, ...} => 

218 
let val xs = map term_of params @ 

219 
map (fn (_, s) => Free (s, the (Variable.default_type context s))) 

220 
(Variable.fixes_of context) 

221 
in 

222 
case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl) 

223 
(mk_dom xs) Net.empty 0 0 of 

224 
NONE => no_tac 

225 
 SOME prf => 

226 
rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1 

28339
6f6fa16543f5
Corrected call of SUBPROOF in coherent_tac that used wrong context.
berghofe
parents:
28326
diff
changeset

227 
end) context 1) ctxt; 
28326  228 

31241  229 
val setup = Method.setup @{binding coherent} 
230 
(Attrib.thms >> (fn rules => fn ctxt => 

231 
METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules))))) 

232 
"prove coherent formula"; 

28326  233 

234 
end; 