author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 55636  9d120886c50b 
child 58839  ccda99401bc8 
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 

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 = 
36946  42 
if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct 
43 
else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct))) 

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; 
28326  69 
val (prems, cases) = dest_elim (prop_of th') 
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)) 
84 
(Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t))); 

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 
118 
(map (Syntax.pretty_term ctxt) (map fst (sort (int_ord o pairself 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 
55632  176 
val thy = Proof_Context.theory_of ctxt; 
177 
val cert = Thm.cterm_of thy; 

178 
val certT = Thm.ctyp_of thy; 

55627  179 
val _ = 
55632  180 
cond_trace ctxt (fn () => 
55634  181 
Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms))); 
55627  182 
val th' = 
183 
Drule.implies_elim_list 

184 
(Thm.instantiate 

55632  185 
(map (fn (ixn, (S, T)) => (certT (TVar ((ixn, S))), certT T)) (Vartab.dest tye), 
55627  186 
map (fn (ixn, (T, t)) => 
55632  187 
(cert (Var (ixn, Envir.subst_type tye T)), cert t)) (Vartab.dest env) @ 
188 
map (fn (ixnT, t) => (cert (Var ixnT), cert t)) insts) th) 

55627  189 
(map (nth asms) is); 
190 
val (_, cases) = dest_elim (prop_of th'); 

28326  191 
in 
55627  192 
(case (cases, prfs) of 
28326  193 
([([], [_])], []) => th' 
55632  194 
 ([([], [_])], [([], prf)]) => thm_of_cl_prf ctxt goal (asms @ [th']) prf 
55627  195 
 _ => 
196 
Drule.implies_elim_list 

197 
(Thm.instantiate (Thm.match 

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

55632  199 
(map (thm_of_case_prf ctxt goal asms) (prfs ~~ cases))) 
28326  200 
end 
201 

55632  202 
and thm_of_case_prf ctxt goal asms ((params, prf), (_, asms')) = 
28326  203 
let 
55632  204 
val thy = Proof_Context.theory_of ctxt; 
205 
val cert = Thm.cterm_of thy; 

206 
val cparams = map cert params; 

207 
val asms'' = map (cert o curry subst_bounds (rev params)) asms'; 

55634  208 
val (prems'', ctxt') = fold_map Thm.assume_hyps asms'' ctxt; 
28326  209 
in 
55627  210 
Drule.forall_intr_list cparams 
55634  211 
(Drule.implies_intr_list asms'' (thm_of_cl_prf ctxt' goal (asms @ prems'') prf)) 
28326  212 
end; 
213 

214 

215 
(** external interface **) 

216 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
46186
diff
changeset

217 
fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} => 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
46186
diff
changeset

218 
rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
46186
diff
changeset

219 
SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} => 
55627  220 
let 
221 
val xs = 

222 
map (term_of o #2) params @ 

223 
map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s))) 

224 
(rev (Variable.dest_fixes ctxt'')) (* FIXME !? *) 

28326  225 
in 
55632  226 
(case 
227 
valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl) 

228 
(mk_dom xs) Net.empty 0 0 of 

55627  229 
NONE => no_tac 
55632  230 
 SOME prf => rtac (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

231 
end) ctxt' 1) ctxt; 
28326  232 

55632  233 
val _ = Theory.setup 
234 
(trace_setup #> 

235 
Method.setup @{binding coherent} 

236 
(Attrib.thms >> (fn rules => fn ctxt => 

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

238 
"prove coherent formula"); 

28326  239 

240 
end; 