--- a/src/HOL/HOL.thy Thu Feb 20 19:55:39 2014 +0100
+++ b/src/HOL/HOL.thy Thu Feb 20 20:19:41 2014 +0100
@@ -24,7 +24,6 @@
ML_file "~~/src/Provers/classical.ML"
ML_file "~~/src/Provers/blast.ML"
ML_file "~~/src/Provers/clasimp.ML"
-ML_file "~~/src/Tools/coherent.ML"
ML_file "~~/src/Tools/eqsubst.ML"
ML_file "~~/src/Provers/quantifier1.ML"
ML_file "~~/src/Tools/atomize_elim.ML"
@@ -1561,20 +1560,18 @@
subsubsection {* Coherent logic *}
+ML_file "~~/src/Tools/coherent.ML"
ML {*
structure Coherent = Coherent
(
- val atomize_elimL = @{thm atomize_elimL}
- val atomize_exL = @{thm atomize_exL}
- val atomize_conjL = @{thm atomize_conjL}
- val atomize_disjL = @{thm atomize_disjL}
- val operator_names =
- [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}]
+ val atomize_elimL = @{thm atomize_elimL};
+ val atomize_exL = @{thm atomize_exL};
+ val atomize_conjL = @{thm atomize_conjL};
+ val atomize_disjL = @{thm atomize_disjL};
+ val operator_names = [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}];
);
*}
-setup Coherent.setup
-
subsubsection {* Reorienting equalities *}
--- a/src/Tools/coherent.ML Thu Feb 20 19:55:39 2014 +0100
+++ b/src/Tools/coherent.ML Thu Feb 20 20:19:41 2014 +0100
@@ -20,9 +20,8 @@
signature COHERENT =
sig
- val verbose: bool Unsynchronized.ref
+ val trace: bool Config.T
val coherent_tac: Proof.context -> thm list -> int -> tactic
- val setup: theory -> theory
end;
functor Coherent(Data: COHERENT_DATA) : COHERENT =
@@ -30,9 +29,8 @@
(** misc tools **)
-val verbose = Unsynchronized.ref false;
-
-fun message f = if !verbose then tracing (f ()) else ();
+val (trace, trace_setup) = Attrib.config_bool @{binding coherent_trace} (K false);
+fun cond_trace ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ();
datatype cl_prf =
ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
@@ -147,7 +145,7 @@
and valid_cases _ _ _ _ _ _ _ [] = SOME []
| valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
let
- val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
+ val _ = cond_trace ctxt (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
val params = map_index (fn (i, T) => Free ("par" ^ string_of_int (nparams + i), T)) Ts;
val ts' = map_index (fn (i, t) => (subst_bounds (rev params, t), nfacts + i)) ts;
val dom' =
@@ -165,43 +163,44 @@
(** proof replaying **)
-fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
+fun thm_of_cl_prf ctxt goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
let
+ val thy = Proof_Context.theory_of ctxt;
+ val cert = Thm.cterm_of thy;
+ val certT = Thm.ctyp_of thy;
val _ =
- message (fn () =>
- cat_lines ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
+ cond_trace ctxt (fn () =>
+ cat_lines ("asms:" :: map (Display.string_of_thm ctxt) asms) ^ "\n\n");
val th' =
Drule.implies_elim_list
(Thm.instantiate
- (map (fn (ixn, (S, T)) =>
- (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
- (Vartab.dest tye),
+ (map (fn (ixn, (S, T)) => (certT (TVar ((ixn, S))), certT T)) (Vartab.dest tye),
map (fn (ixn, (T, t)) =>
- (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
- Thm.cterm_of thy t)) (Vartab.dest env) @
- map (fn (ixnT, t) =>
- (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
+ (cert (Var (ixn, Envir.subst_type tye T)), cert t)) (Vartab.dest env) @
+ map (fn (ixnT, t) => (cert (Var ixnT), cert t)) insts) th)
(map (nth asms) is);
val (_, cases) = dest_elim (prop_of th');
in
(case (cases, prfs) of
([([], [_])], []) => th'
- | ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf
+ | ([([], [_])], [([], prf)]) => thm_of_cl_prf ctxt goal (asms @ [th']) prf
| _ =>
Drule.implies_elim_list
(Thm.instantiate (Thm.match
(Drule.strip_imp_concl (cprop_of th'), goal)) th')
- (map (thm_of_case_prf thy goal asms) (prfs ~~ cases)))
+ (map (thm_of_case_prf ctxt goal asms) (prfs ~~ cases)))
end
-and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) =
+and thm_of_case_prf ctxt goal asms ((params, prf), (_, asms')) =
let
- val cparams = map (cterm_of thy) params;
- val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms';
+ val thy = Proof_Context.theory_of ctxt;
+ val cert = Thm.cterm_of thy;
+ val cparams = map cert params;
+ val asms'' = map (cert o curry subst_bounds (rev params)) asms';
in
Drule.forall_intr_list cparams
(Drule.implies_intr_list asms''
- (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf))
+ (thm_of_cl_prf ctxt goal (asms @ map Thm.assume asms'') prf))
end;
@@ -216,15 +215,18 @@
map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
(rev (Variable.dest_fixes ctxt'')) (* FIXME !? *)
in
- (case valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
- (mk_dom xs) Net.empty 0 0 of
+ (case
+ valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
+ (mk_dom xs) Net.empty 0 0 of
NONE => no_tac
- | SOME prf => rtac (thm_of_cl_prf (Proof_Context.theory_of ctxt'') concl [] prf) 1)
+ | SOME prf => rtac (thm_of_cl_prf ctxt'' concl [] prf) 1)
end) ctxt' 1) ctxt;
-val setup = Method.setup @{binding coherent}
- (Attrib.thms >> (fn rules => fn ctxt =>
- METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
- "prove coherent formula";
+val _ = Theory.setup
+ (trace_setup #>
+ Method.setup @{binding coherent}
+ (Attrib.thms >> (fn rules => fn ctxt =>
+ METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
+ "prove coherent formula");
end;