src/HOL/Algebra/ringsimp.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16568 e02fe7ae212b
child 19931 fb32b43e7f80
permissions -rw-r--r--
Constant "If" is now local
     1 (*
     2   Title:     Normalisation method for locale cring
     3   Id:        $Id$
     4   Author:    Clemens Ballarin
     5   Copyright: TU Muenchen
     6 *)
     7 
     8 (*** Term order for commutative rings ***)
     9 
    10 fun ring_ord a =
    11   find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
    12   "CRing.minus", "Group.monoid.one", "Group.monoid.mult"];
    13 
    14 fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
    15 
    16 val cring_ss = HOL_ss settermless termless_ring;
    17 
    18 fun cring_normalise ctxt = let
    19     fun ring_filter t = (case HOLogic.dest_Trueprop t of
    20         Const ("CRing.ring_axioms", _) $ Free (s, _) => [s]
    21       | _ => [])
    22       handle TERM _ => [];
    23     fun comm_filter t = (case HOLogic.dest_Trueprop t of
    24         Const ("Group.comm_monoid_axioms", _) $ Free (s, _) => [s]
    25       | _ => [])
    26       handle TERM _ => [];
    27 
    28     val prems = ProofContext.prems_of ctxt;
    29     val rings = List.concat (map (ring_filter o #prop o rep_thm) prems);
    30     val comms = List.concat (map (comm_filter o #prop o rep_thm) prems);
    31     val non_comm_rings = rings \\ comms;
    32     val comm_rings = rings inter_string comms;
    33     val _ = tracing
    34       ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^
    35        "\nCommutative rings in proof context: " ^ commas comm_rings);
    36     val simps =
    37       List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".ring_simprules")))
    38         non_comm_rings) @
    39       List.concat (map (fn s => ProofContext.get_thms ctxt (Name (s ^ ".cring_simprules")))
    40         comm_rings);
    41   in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
    42   end;
    43 
    44 (*
    45 val ring_ss = HOL_basic_ss settermless termless_ring addsimps
    46   [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def,
    47    r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
    48    a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus];
    49 *)