src/Tools/coherent.ML
changeset 32740 9dd0a2f83429
parent 32734 06c13b2e562e
child 36945 9bec62c10714
equal deleted inserted replaced
32739:31e75ad9ae17 32740:9dd0a2f83429
    18   val operator_names: string list
    18   val operator_names: string list
    19 end;
    19 end;
    20 
    20 
    21 signature COHERENT =
    21 signature COHERENT =
    22 sig
    22 sig
    23   val verbose: bool ref
    23   val verbose: bool Unsynchronized.ref
    24   val show_facts: bool ref
    24   val show_facts: bool Unsynchronized.ref
    25   val coherent_tac: Proof.context -> thm list -> int -> tactic
    25   val coherent_tac: Proof.context -> thm list -> int -> tactic
    26   val setup: theory -> theory
    26   val setup: theory -> theory
    27 end;
    27 end;
    28 
    28 
    29 functor Coherent(Data: COHERENT_DATA) : COHERENT =
    29 functor Coherent(Data: COHERENT_DATA) : COHERENT =
    30 struct
    30 struct
    31 
    31 
    32 (** misc tools **)
    32 (** misc tools **)
    33 
    33 
    34 val verbose = ref false;
    34 val verbose = Unsynchronized.ref false;
    35 
    35 
    36 fun message f = if !verbose then tracing (f ()) else ();
    36 fun message f = if !verbose then tracing (f ()) else ();
    37 
    37 
    38 datatype cl_prf =
    38 datatype cl_prf =
    39   ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
    39   ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
   115         (map (fn t => subst_bounds (rev vs, t)) ts)) of
   115         (map (fn t => subst_bounds (rev vs, t)) ts)) of
   116           SOME _ => true
   116           SOME _ => true
   117         | NONE => is_valid_disj ctxt facts ds
   117         | NONE => is_valid_disj ctxt facts ds
   118       end;
   118       end;
   119 
   119 
   120 val show_facts = ref false;
   120 val show_facts = Unsynchronized.ref false;
   121 
   121 
   122 fun string_of_facts ctxt s facts = space_implode "\n"
   122 fun string_of_facts ctxt s facts = space_implode "\n"
   123   (s :: map (Syntax.string_of_term ctxt)
   123   (s :: map (Syntax.string_of_term ctxt)
   124      (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
   124      (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
   125 
   125