author  wenzelm 
Wed, 31 Dec 2008 18:53:18 +0100  
changeset 29273  285c00993bc2 
parent 28339  6f6fa16543f5 
permissions  rwrr 
28326  1 
(* Title: Provers/coherent.ML 
2 
Author: Stefan Berghofer, TU Muenchen 

29273  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 

25 
val coherent_tac: thm list > Proof.context > int > tactic 

26 
val coherent_meth: thm list > Proof.context > Proof.method 

27 
val setup: theory > theory 

28 
end; 

29 

30 
functor CoherentFun(Data: COHERENT_DATA) : COHERENT = 

31 
struct 

32 

33 
val verbose = ref false; 

34 

35 
fun message f = if !verbose then tracing (f ()) else (); 

36 

37 
datatype cl_prf = 

38 
ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list * 

39 
int list * (term list * cl_prf) list; 

40 

29273  41 
val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1); 
28326  42 

43 
local open Conv in 

44 

45 
fun rulify_elim_conv ct = 

46 
if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct 

47 
else concl_conv (length (Logic.strip_imp_prems (term_of ct))) 

48 
(rewr_conv (symmetric Data.atomize_elimL) then_conv 

49 
MetaSimplifier.rewrite true (map symmetric 

50 
[Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct 

51 

52 
end; 

53 

54 
fun rulify_elim th = MetaSimplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th); 

55 

56 
(* Decompose elimination rule of the form 

57 
A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P 

58 
*) 

59 
fun dest_elim prop = 

60 
let 

61 
val prems = Logic.strip_imp_prems prop; 

62 
val concl = Logic.strip_imp_concl prop; 

63 
val (prems1, prems2) = 

64 
take_suffix (fn t => Logic.strip_assums_concl t = concl) prems; 

65 
in 

66 
(prems1, 

67 
if null prems2 then [([], [concl])] 

68 
else map (fn t => 

69 
(map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2) 

70 
end; 

71 

72 
fun mk_rule th = 

73 
let 

74 
val th' = rulify_elim th; 

75 
val (prems, cases) = dest_elim (prop_of th') 

76 
in (th', prems, cases) end; 

77 

78 
fun mk_dom ts = fold (fn t => 

79 
Typtab.map_default (fastype_of t, []) (fn us => us @ [t])) ts Typtab.empty; 

80 

81 
val empty_env = (Vartab.empty, Vartab.empty); 

82 

83 
(* Find matcher that makes conjunction valid in given state *) 

84 
fun valid_conj ctxt facts env [] = Seq.single (env, []) 

85 
 valid_conj ctxt facts env (t :: ts) = 

86 
Seq.maps (fn (u, x) => Seq.map (apsnd (cons x)) 

87 
(valid_conj ctxt facts 

88 
(Pattern.match (ProofContext.theory_of ctxt) (t, u) env) ts 

89 
handle Pattern.MATCH => Seq.empty)) 

90 
(Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t))); 

91 

92 
(* Instantiate variables that only occur free in conlusion *) 

93 
fun inst_extra_vars ctxt dom cs = 

94 
let 

95 
val vs = fold Term.add_vars (maps snd cs) []; 

96 
fun insts [] inst = Seq.single inst 

97 
 insts ((ixn, T) :: vs') inst = Seq.maps 

98 
(fn t => insts vs' (((ixn, T), t) :: inst)) 

99 
(Seq.of_list (case Typtab.lookup dom T of 

100 
NONE => error ("Unknown domain: " ^ 

101 
Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^ 

102 
commas (maps (map (Syntax.string_of_term ctxt) o snd) cs)) 

103 
 SOME ts => ts)) 

104 
in Seq.map (fn inst => 

105 
(inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs)) 

106 
(insts vs []) 

107 
end; 

108 

109 
(* Check whether disjunction is valid in given state *) 

110 
fun is_valid_disj ctxt facts [] = false 

111 
 is_valid_disj ctxt facts ((Ts, ts) :: ds) = 

112 
let val vs = rev (map_index (fn (i, T) => Var (("x", i), T)) Ts) 

113 
in case Seq.pull (valid_conj ctxt facts empty_env 

114 
(map (fn t => subst_bounds (vs, t)) ts)) of 

115 
SOME _ => true 

116 
 NONE => is_valid_disj ctxt facts ds 

117 
end; 

118 

119 
val show_facts = ref false; 

120 

121 
fun string_of_facts ctxt s facts = space_implode "\n" 

122 
(s :: map (Syntax.string_of_term ctxt) 

123 
(map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n"; 

124 

125 
fun print_facts ctxt facts = 

126 
if !show_facts then message (fn () => string_of_facts ctxt "Facts:" facts) 

127 
else (); 

128 

129 
fun valid ctxt rules goal dom facts nfacts nparams = 

130 
let val seq = Seq.of_list rules > Seq.maps (fn (th, ps, cs) => 

131 
valid_conj ctxt facts empty_env ps > Seq.maps (fn (env as (tye, _), is) => 

132 
let val cs' = map (fn (Ts, ts) => 

133 
(map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs 

134 
in 

135 
inst_extra_vars ctxt dom cs' > 

136 
Seq.map_filter (fn (inst, cs'') => 

137 
if is_valid_disj ctxt facts cs'' then NONE 

138 
else SOME (th, env, inst, is, cs'')) 

139 
end)) 

140 
in 

141 
case Seq.pull seq of 

142 
NONE => (tracing (string_of_facts ctxt "Countermodel found:" facts); NONE) 

143 
 SOME ((th, env, inst, is, cs), _) => 

144 
if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, [])) 

145 
else 

146 
(case valid_cases ctxt rules goal dom facts nfacts nparams cs of 

147 
NONE => NONE 

148 
 SOME prfs => SOME (ClPrf (th, env, inst, is, prfs))) 

149 
end 

150 

151 
and valid_cases ctxt rules goal dom facts nfacts nparams [] = SOME [] 

152 
 valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) = 

153 
let 

154 
val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts)); 

155 
val params = rev (map_index (fn (i, T) => 

156 
Free ("par" ^ string_of_int (nparams + i), T)) Ts); 

157 
val ts' = map_index (fn (i, t) => 

158 
(subst_bounds (params, t), nfacts + i)) ts; 

159 
val dom' = fold (fn (T, p) => 

160 
Typtab.map_default (T, []) (fn ps => ps @ [p])) 

161 
(Ts ~~ params) dom; 

162 
val facts' = fold (fn (t, i) => Net.insert_term op = 

163 
(t, (t, i))) ts' facts 

164 
in 

165 
case valid ctxt rules goal dom' facts' 

166 
(nfacts + length ts) (nparams + length Ts) of 

167 
NONE => NONE 

168 
 SOME prf => (case valid_cases ctxt rules goal dom facts nfacts nparams ds of 

169 
NONE => NONE 

170 
 SOME prfs => SOME ((params, prf) :: prfs)) 

171 
end; 

172 

173 
(** proof replaying **) 

174 

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

176 
let 

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

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

179 
val th' = Drule.implies_elim_list 

180 
(Thm.instantiate 

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

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

183 
(Vartab.dest tye), 

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

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

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

187 
map (fn (ixnT, t) => 

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

189 
(map (nth asms) is); 

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

191 
in 

192 
case (cases, prfs) of 

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

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

195 
 _ => Drule.implies_elim_list 

196 
(Thm.instantiate (Thm.match 

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

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

199 
end 

200 

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

202 
let 

203 
val cparams = map (cterm_of thy) params; 

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

205 
in 

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

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

208 
end; 

209 

210 

211 
(** external interface **) 

212 

213 
fun coherent_tac rules ctxt = SUBPROOF (fn {prems, concl, params, context, ...} => 

214 
rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN 

215 
SUBPROOF (fn {prems = prems', concl, context, ...} => 

216 
let val xs = map term_of params @ 

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

218 
(Variable.fixes_of context) 

219 
in 

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

221 
(mk_dom xs) Net.empty 0 0 of 

222 
NONE => no_tac 

223 
 SOME prf => 

224 
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

225 
end) context 1) ctxt; 
28326  226 

227 
fun coherent_meth rules ctxt = 

228 
Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1); 

229 

230 
val setup = Method.add_method 

231 
("coherent", Method.thms_ctxt_args coherent_meth, "Prove coherent formula"); 

232 

233 
end; 