modernized tool setup;
authorwenzelm
Thu Feb 20 20:19:41 2014 +0100 (2014-02-20)
changeset 556320f9d03649a9c
parent 55631 7f428e08111b
child 55633 460f4801b5cb
modernized tool setup;
tuned;
src/HOL/HOL.thy
src/Tools/coherent.ML
     1.1 --- a/src/HOL/HOL.thy	Thu Feb 20 19:55:39 2014 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Feb 20 20:19:41 2014 +0100
     1.3 @@ -24,7 +24,6 @@
     1.4  ML_file "~~/src/Provers/classical.ML"
     1.5  ML_file "~~/src/Provers/blast.ML"
     1.6  ML_file "~~/src/Provers/clasimp.ML"
     1.7 -ML_file "~~/src/Tools/coherent.ML"
     1.8  ML_file "~~/src/Tools/eqsubst.ML"
     1.9  ML_file "~~/src/Provers/quantifier1.ML"
    1.10  ML_file "~~/src/Tools/atomize_elim.ML"
    1.11 @@ -1561,20 +1560,18 @@
    1.12  
    1.13  subsubsection {* Coherent logic *}
    1.14  
    1.15 +ML_file "~~/src/Tools/coherent.ML"
    1.16  ML {*
    1.17  structure Coherent = Coherent
    1.18  (
    1.19 -  val atomize_elimL = @{thm atomize_elimL}
    1.20 -  val atomize_exL = @{thm atomize_exL}
    1.21 -  val atomize_conjL = @{thm atomize_conjL}
    1.22 -  val atomize_disjL = @{thm atomize_disjL}
    1.23 -  val operator_names =
    1.24 -    [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}]
    1.25 +  val atomize_elimL = @{thm atomize_elimL};
    1.26 +  val atomize_exL = @{thm atomize_exL};
    1.27 +  val atomize_conjL = @{thm atomize_conjL};
    1.28 +  val atomize_disjL = @{thm atomize_disjL};
    1.29 +  val operator_names = [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}];
    1.30  );
    1.31  *}
    1.32  
    1.33 -setup Coherent.setup
    1.34 -
    1.35  
    1.36  subsubsection {* Reorienting equalities *}
    1.37  
     2.1 --- a/src/Tools/coherent.ML	Thu Feb 20 19:55:39 2014 +0100
     2.2 +++ b/src/Tools/coherent.ML	Thu Feb 20 20:19:41 2014 +0100
     2.3 @@ -20,9 +20,8 @@
     2.4  
     2.5  signature COHERENT =
     2.6  sig
     2.7 -  val verbose: bool Unsynchronized.ref
     2.8 +  val trace: bool Config.T
     2.9    val coherent_tac: Proof.context -> thm list -> int -> tactic
    2.10 -  val setup: theory -> theory
    2.11  end;
    2.12  
    2.13  functor Coherent(Data: COHERENT_DATA) : COHERENT =
    2.14 @@ -30,9 +29,8 @@
    2.15  
    2.16  (** misc tools **)
    2.17  
    2.18 -val verbose = Unsynchronized.ref false;
    2.19 -
    2.20 -fun message f = if !verbose then tracing (f ()) else ();
    2.21 +val (trace, trace_setup) = Attrib.config_bool @{binding coherent_trace} (K false);
    2.22 +fun cond_trace ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ();
    2.23  
    2.24  datatype cl_prf =
    2.25    ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
    2.26 @@ -147,7 +145,7 @@
    2.27  and valid_cases _ _ _ _ _ _ _ [] = SOME []
    2.28    | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
    2.29        let
    2.30 -        val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
    2.31 +        val _ = cond_trace ctxt (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
    2.32          val params = map_index (fn (i, T) => Free ("par" ^ string_of_int (nparams + i), T)) Ts;
    2.33          val ts' = map_index (fn (i, t) => (subst_bounds (rev params, t), nfacts + i)) ts;
    2.34          val dom' =
    2.35 @@ -165,43 +163,44 @@
    2.36  
    2.37  (** proof replaying **)
    2.38  
    2.39 -fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
    2.40 +fun thm_of_cl_prf ctxt goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
    2.41    let
    2.42 +    val thy = Proof_Context.theory_of ctxt;
    2.43 +    val cert = Thm.cterm_of thy;
    2.44 +    val certT = Thm.ctyp_of thy;
    2.45      val _ =
    2.46 -      message (fn () =>
    2.47 -        cat_lines ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
    2.48 +      cond_trace ctxt (fn () =>
    2.49 +        cat_lines ("asms:" :: map (Display.string_of_thm ctxt) asms) ^ "\n\n");
    2.50      val th' =
    2.51        Drule.implies_elim_list
    2.52          (Thm.instantiate
    2.53 -           (map (fn (ixn, (S, T)) =>
    2.54 -              (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
    2.55 -                 (Vartab.dest tye),
    2.56 +           (map (fn (ixn, (S, T)) => (certT (TVar ((ixn, S))), certT T)) (Vartab.dest tye),
    2.57              map (fn (ixn, (T, t)) =>
    2.58 -              (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
    2.59 -               Thm.cterm_of thy t)) (Vartab.dest env) @
    2.60 -            map (fn (ixnT, t) =>
    2.61 -              (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
    2.62 +              (cert (Var (ixn, Envir.subst_type tye T)), cert t)) (Vartab.dest env) @
    2.63 +            map (fn (ixnT, t) => (cert (Var ixnT), cert t)) insts) th)
    2.64          (map (nth asms) is);
    2.65      val (_, cases) = dest_elim (prop_of th');
    2.66    in
    2.67      (case (cases, prfs) of
    2.68        ([([], [_])], []) => th'
    2.69 -    | ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf
    2.70 +    | ([([], [_])], [([], prf)]) => thm_of_cl_prf ctxt goal (asms @ [th']) prf
    2.71      | _ =>
    2.72          Drule.implies_elim_list
    2.73            (Thm.instantiate (Thm.match
    2.74               (Drule.strip_imp_concl (cprop_of th'), goal)) th')
    2.75 -          (map (thm_of_case_prf thy goal asms) (prfs ~~ cases)))
    2.76 +          (map (thm_of_case_prf ctxt goal asms) (prfs ~~ cases)))
    2.77    end
    2.78  
    2.79 -and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) =
    2.80 +and thm_of_case_prf ctxt goal asms ((params, prf), (_, asms')) =
    2.81    let
    2.82 -    val cparams = map (cterm_of thy) params;
    2.83 -    val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms';
    2.84 +    val thy = Proof_Context.theory_of ctxt;
    2.85 +    val cert = Thm.cterm_of thy;
    2.86 +    val cparams = map cert params;
    2.87 +    val asms'' = map (cert o curry subst_bounds (rev params)) asms';
    2.88    in
    2.89      Drule.forall_intr_list cparams
    2.90        (Drule.implies_intr_list asms''
    2.91 -        (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf))
    2.92 +        (thm_of_cl_prf ctxt goal (asms @ map Thm.assume asms'') prf))
    2.93    end;
    2.94  
    2.95  
    2.96 @@ -216,15 +215,18 @@
    2.97          map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
    2.98            (rev (Variable.dest_fixes ctxt''))  (* FIXME !? *)
    2.99      in
   2.100 -      (case valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
   2.101 -           (mk_dom xs) Net.empty 0 0 of
   2.102 +      (case
   2.103 +        valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
   2.104 +          (mk_dom xs) Net.empty 0 0 of
   2.105          NONE => no_tac
   2.106 -      | SOME prf => rtac (thm_of_cl_prf (Proof_Context.theory_of ctxt'') concl [] prf) 1)
   2.107 +      | SOME prf => rtac (thm_of_cl_prf ctxt'' concl [] prf) 1)
   2.108      end) ctxt' 1) ctxt;
   2.109  
   2.110 -val setup = Method.setup @{binding coherent}
   2.111 -  (Attrib.thms >> (fn rules => fn ctxt =>
   2.112 -      METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
   2.113 -    "prove coherent formula";
   2.114 +val _ = Theory.setup
   2.115 +  (trace_setup #>
   2.116 +   Method.setup @{binding coherent}
   2.117 +    (Attrib.thms >> (fn rules => fn ctxt =>
   2.118 +        METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
   2.119 +      "prove coherent formula");
   2.120  
   2.121  end;