author  blanchet 
Tue, 07 Dec 2010 11:56:01 +0100  
changeset 41051  2ed1b971fc20 
parent 36946  4eba866311df 
child 41228  e1fce873b814 
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 

32740  23 
val verbose: bool Unsynchronized.ref 
24 
val show_facts: bool Unsynchronized.ref 

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

28 

32734  29 
functor Coherent(Data: COHERENT_DATA) : COHERENT = 
28326  30 
struct 
31 

31241  32 
(** misc tools **) 
33 

32740  34 
val verbose = Unsynchronized.ref false; 
28326  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 
fun rulify_elim_conv ct = 

36946  45 
if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct 
46 
else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct))) 

47 
(Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv 

36945  48 
MetaSimplifier.rewrite true (map Thm.symmetric 
28326  49 
[Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct 
50 

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

51 
fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th); 
28326  52 

53 
(* Decompose elimination rule of the form 

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

55 
*) 

56 
fun dest_elim prop = 

57 
let 

58 
val prems = Logic.strip_imp_prems prop; 

59 
val concl = Logic.strip_imp_concl prop; 

60 
val (prems1, prems2) = 

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

62 
in 

63 
(prems1, 

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

65 
else map (fn t => 

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

67 
end; 

68 

69 
fun mk_rule th = 

70 
let 

71 
val th' = rulify_elim th; 

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

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

74 

75 
fun mk_dom ts = fold (fn t => 

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

77 

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

79 

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

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

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

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

84 
(valid_conj ctxt facts 

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

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

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

88 

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

90 
fun inst_extra_vars ctxt dom cs = 

91 
let 

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

93 
fun insts [] inst = Seq.single inst 

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

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

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

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

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

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

100 
 SOME ts => ts)) 

101 
in Seq.map (fn inst => 

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

103 
(insts vs []) 

104 
end; 

105 

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

107 
fun is_valid_disj ctxt facts [] = false 

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

31855  109 
let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts 
28326  110 
in case Seq.pull (valid_conj ctxt facts empty_env 
31855  111 
(map (fn t => subst_bounds (rev vs, t)) ts)) of 
28326  112 
SOME _ => true 
113 
 NONE => is_valid_disj ctxt facts ds 

114 
end; 

115 

32740  116 
val show_facts = Unsynchronized.ref false; 
28326  117 

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

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

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

121 

122 
fun print_facts ctxt facts = 

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

124 
else (); 

125 

126 
fun valid ctxt rules goal dom facts nfacts nparams = 

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

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

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

32035  130 
(map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs 
28326  131 
in 
132 
inst_extra_vars ctxt dom cs' > 

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

134 
if is_valid_disj ctxt facts cs'' then NONE 

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

136 
end)) 

137 
in 

138 
case Seq.pull seq of 

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

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

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

142 
else 

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

144 
NONE => NONE 

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

146 
end 

147 

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

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

150 
let 

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

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

28326  154 
val ts' = map_index (fn (i, t) => 
31855  155 
(subst_bounds (rev params, t), nfacts + i)) ts; 
28326  156 
val dom' = fold (fn (T, p) => 
157 
Typtab.map_default (T, []) (fn ps => ps @ [p])) 

158 
(Ts ~~ params) dom; 

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

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

161 
in 

162 
case valid ctxt rules goal dom' facts' 

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

164 
NONE => NONE 

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

166 
NONE => NONE 

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

168 
end; 

169 

31241  170 

28326  171 
(** proof replaying **) 
172 

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

174 
let 

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

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32035
diff
changeset

176 
("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n"); 
28326  177 
val th' = Drule.implies_elim_list 
178 
(Thm.instantiate 

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

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

181 
(Vartab.dest tye), 

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

32035  183 
(Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)), 
28326  184 
Thm.cterm_of thy t)) (Vartab.dest env) @ 
185 
map (fn (ixnT, t) => 

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

187 
(map (nth asms) is); 

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

189 
in 

190 
case (cases, prfs) of 

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

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

193 
 _ => Drule.implies_elim_list 

194 
(Thm.instantiate (Thm.match 

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

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

197 
end 

198 

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

200 
let 

201 
val cparams = map (cterm_of thy) params; 

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

203 
in 

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

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

206 
end; 

207 

208 

209 
(** external interface **) 

210 

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

32199  214 
let val xs = map (term_of o #2) params @ 
28326  215 
map (fn (_, s) => Free (s, the (Variable.default_type context s))) 
216 
(Variable.fixes_of context) 

217 
in 

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

219 
(mk_dom xs) Net.empty 0 0 of 

220 
NONE => no_tac 

221 
 SOME prf => 

222 
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

223 
end) context 1) ctxt; 
28326  224 

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

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

228 
"prove coherent formula"; 

28326  229 

230 
end; 