src/HOL/Algebra/ringsimp.ML
changeset 19931 fb32b43e7f80
parent 16568 e02fe7ae212b
child 20129 95e84d2c9f2c
     1.1 --- a/src/HOL/Algebra/ringsimp.ML	Tue Jun 20 14:51:59 2006 +0200
     1.2 +++ b/src/HOL/Algebra/ringsimp.ML	Tue Jun 20 15:53:44 2006 +0200
     1.3 @@ -16,20 +16,38 @@
     1.4  val cring_ss = HOL_ss settermless termless_ring;
     1.5  
     1.6  fun cring_normalise ctxt = let
     1.7 -    fun ring_filter t = (case HOLogic.dest_Trueprop t of
     1.8 -        Const ("CRing.ring_axioms", _) $ Free (s, _) => [s]
     1.9 +    fun filter p t = (case HOLogic.dest_Trueprop t of
    1.10 +        Const (p', _) $ Free (s, _) => if p = p' then [s] else []
    1.11 +      | _ => [])
    1.12 +      handle TERM _ => [];
    1.13 +    fun filter21 p t = (case HOLogic.dest_Trueprop t of
    1.14 +        Const (p', _) $ Free (s, _) $ _ => if p = p' then [s] else []
    1.15        | _ => [])
    1.16        handle TERM _ => [];
    1.17 -    fun comm_filter t = (case HOLogic.dest_Trueprop t of
    1.18 -        Const ("Group.comm_monoid_axioms", _) $ Free (s, _) => [s]
    1.19 +    fun filter22 p t = (case HOLogic.dest_Trueprop t of
    1.20 +        Const (p', _) $ _ $ Free (s, _) => if p = p' then [s] else []
    1.21 +      | _ => [])
    1.22 +      handle TERM _ => [];
    1.23 +    fun filter31 p t = (case HOLogic.dest_Trueprop t of
    1.24 +        Const (p', _) $ Free (s, _) $ _ $ _ => if p = p' then [s] else []
    1.25 +      | _ => [])
    1.26 +      handle TERM _ => [];
    1.27 +    fun filter32 p t = (case HOLogic.dest_Trueprop t of
    1.28 +        Const (p', _) $ _ $ Free (s, _) $ _ => if p = p' then [s] else []
    1.29        | _ => [])
    1.30        handle TERM _ => [];
    1.31  
    1.32      val prems = ProofContext.prems_of ctxt;
    1.33 -    val rings = List.concat (map (ring_filter o #prop o rep_thm) prems);
    1.34 -    val comms = List.concat (map (comm_filter o #prop o rep_thm) prems);
    1.35 -    val non_comm_rings = rings \\ comms;
    1.36 -    val comm_rings = rings inter_string comms;
    1.37 +    val non_comm_rings = List.concat (map (filter "CRing.ring" o #prop o rep_thm) prems);
    1.38 +    val comm_rings = List.concat (map (filter "CRing.cring" o #prop o rep_thm) prems) @
    1.39 +        List.concat (map (filter "CRing.domain" o #prop o rep_thm) prems) @
    1.40 +        List.concat (map (filter21 "Module.module" o #prop o rep_thm) prems) @
    1.41 +        List.concat (map (filter21 "Module.algebra" o #prop o rep_thm) prems) @
    1.42 +        List.concat (map (filter22 "Module.algebra" o #prop o rep_thm) prems) @
    1.43 +        List.concat (map (filter "UnivPoly.UP_cring" o #prop o rep_thm) prems) @
    1.44 +        List.concat (map (filter "UnivPoly.UP_domain" o #prop o rep_thm) prems) @
    1.45 +        List.concat (map (filter31 "CRing.ring_hom_cring" o #prop o rep_thm) prems) @
    1.46 +        List.concat (map (filter32 "CRing.ring_hom_cring" o #prop o rep_thm) prems);
    1.47      val _ = tracing
    1.48        ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^
    1.49         "\nCommutative rings in proof context: " ^ commas comm_rings);