src/HOL/Algebra/ringsimp.ML
author ballarin
Thu Feb 19 16:44:21 2004 +0100 (2004-02-19)
changeset 14399 dc677b35e54f
parent 13936 d3671b878828
child 14963 d584e32f7d46
permissions -rw-r--r--
New lemmas about inversion of restricted functions.
HOL-Algebra: new locale "ring" for non-commutative rings.
ballarin@13854
     1
(*
ballarin@13854
     2
  Title:     Normalisation method for locale cring
ballarin@13854
     3
  Id:        $Id$
ballarin@13854
     4
  Author:    Clemens Ballarin
ballarin@13854
     5
  Copyright: TU Muenchen
ballarin@13854
     6
*)
ballarin@13854
     7
ballarin@13854
     8
local
ballarin@13854
     9
ballarin@13854
    10
(*** Lexicographic path order on terms.
ballarin@13854
    11
ballarin@13854
    12
  See Baader & Nipkow, Term rewriting, CUP 1998.
ballarin@13854
    13
  Without variables.  Const, Var, Bound, Free and Abs are treated all as
ballarin@13854
    14
  constants.
ballarin@13854
    15
ballarin@13854
    16
  f_ord maps strings to integers and serves two purposes:
ballarin@13854
    17
  - Predicate on constant symbols.  Those that are not recognised by f_ord
ballarin@13854
    18
    must be mapped to ~1.
ballarin@13854
    19
  - Order on the recognised symbols.  These must be mapped to distinct
ballarin@13854
    20
    integers >= 0.
ballarin@13854
    21
ballarin@13854
    22
***)
ballarin@13854
    23
ballarin@13854
    24
fun dest_hd f_ord (Const (a, T)) = 
ballarin@13854
    25
      let val ord = f_ord a in
ballarin@13854
    26
        if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
ballarin@13854
    27
      end
ballarin@13854
    28
  | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
ballarin@13854
    29
  | dest_hd _ (Var v) = ((1, v), 1)
ballarin@13854
    30
  | dest_hd _ (Bound i) = ((1, (("", i), Term.dummyT)), 2)
ballarin@13854
    31
  | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
ballarin@13854
    32
ballarin@13854
    33
fun term_lpo f_ord (s, t) =
ballarin@13854
    34
  let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
ballarin@13854
    35
    if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
ballarin@13854
    36
    then case hd_ord f_ord (f, g) of
ballarin@13854
    37
	GREATER =>
ballarin@13854
    38
	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
ballarin@13854
    39
	  then GREATER else LESS
ballarin@13854
    40
      | EQUAL =>
ballarin@13854
    41
	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
ballarin@13854
    42
	  then list_ord (term_lpo f_ord) (ss, ts)
ballarin@13854
    43
	  else LESS
ballarin@13854
    44
      | LESS => LESS
ballarin@13854
    45
    else GREATER
ballarin@13854
    46
  end
ballarin@13854
    47
and hd_ord f_ord (f, g) = case (f, g) of
ballarin@13854
    48
    (Abs (_, T, t), Abs (_, U, u)) =>
ballarin@13854
    49
      (case term_lpo f_ord (t, u) of EQUAL => Term.typ_ord (T, U) | ord => ord)
ballarin@13854
    50
  | (_, _) => prod_ord (prod_ord int_ord
ballarin@13854
    51
                  (prod_ord Term.indexname_ord Term.typ_ord)) int_ord
ballarin@13854
    52
                (dest_hd f_ord f, dest_hd f_ord g)
ballarin@13854
    53
ballarin@13854
    54
in
ballarin@13854
    55
ballarin@13854
    56
(*** Term order for commutative rings ***)
ballarin@13854
    57
ballarin@13854
    58
fun ring_ord a =
ballarin@13936
    59
  find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
ballarin@13936
    60
  "CRing.minus", "Group.monoid.one", "Group.semigroup.mult"];
ballarin@13854
    61
ballarin@13854
    62
fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
ballarin@13854
    63
ballarin@13854
    64
val cring_ss = HOL_ss settermless termless_ring;
ballarin@13854
    65
ballarin@13854
    66
fun cring_normalise ctxt = let
ballarin@14399
    67
    fun ring_filter t = (case HOLogic.dest_Trueprop t of
ballarin@14399
    68
        Const ("CRing.ring_axioms", _) $ Free (s, _) => [s]
ballarin@14399
    69
      | _ => [])
ballarin@14399
    70
      handle TERM _ => [];
ballarin@14399
    71
    fun comm_filter t = (case HOLogic.dest_Trueprop t of
ballarin@14399
    72
        Const ("Group.comm_semigroup_axioms", _) $ Free (s, _) => [s]
ballarin@13864
    73
      | _ => [])
ballarin@13854
    74
      handle TERM _ => [];
ballarin@14399
    75
ballarin@14399
    76
    val prems = ProofContext.prems_of ctxt;
ballarin@14399
    77
    val rings = flat (map (ring_filter o #prop o rep_thm) prems);
ballarin@14399
    78
    val comms = flat (map (comm_filter o #prop o rep_thm) prems);
ballarin@14399
    79
    val non_comm_rings = rings \\ comms;
ballarin@14399
    80
    val comm_rings = rings inter_string comms;
ballarin@14399
    81
    val _ = tracing
ballarin@14399
    82
      ("Non-commutative rings in proof context: " ^ commas non_comm_rings ^
ballarin@14399
    83
       "\nCommutative rings in proof context: " ^ commas comm_rings);
ballarin@13854
    84
    val simps =
ballarin@14399
    85
      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".ring_simprules"))
ballarin@14399
    86
        non_comm_rings) @
ballarin@13854
    87
      flat (map (fn s => ProofContext.get_thms ctxt (s ^ ".cring_simprules"))
ballarin@14399
    88
        comm_rings);
ballarin@13854
    89
  in Method.SIMPLE_METHOD' HEADGOAL (asm_full_simp_tac (cring_ss addsimps simps))
ballarin@13854
    90
  end;
ballarin@13854
    91
ballarin@13854
    92
(*
ballarin@13854
    93
val ring_ss = HOL_basic_ss settermless termless_ring addsimps
ballarin@13854
    94
  [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def,
ballarin@13854
    95
   r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
ballarin@13854
    96
   a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus];
ballarin@13854
    97
*)
ballarin@13854
    98
ballarin@13854
    99
end;