src/HOL/Algebra/abstract/order.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 15661 9ef583b08647
child 16706 3a7eee8cc0ff
permissions -rw-r--r--
Constant "If" is now local
     1 (*
     2   Title:     Term order, needed for normal forms in rings
     3   Id:        $Id$
     4   Author:    Clemens Ballarin
     5   Copyright: TU Muenchen
     6 *)
     7 
     8 local
     9 
    10 (*** Lexicographic path order on terms.
    11 
    12   See Baader & Nipkow, Term rewriting, CUP 1998.
    13   Without variables.  Const, Var, Bound, Free and Abs are treated all as
    14   constants.
    15 
    16   f_ord maps strings to integers and serves two purposes:
    17   - Predicate on constant symbols.  Those that are not recognised by f_ord
    18     must be mapped to ~1.
    19   - Order on the recognised symbols.  These must be mapped to distinct
    20     integers >= 0.
    21 
    22 ***)
    23 
    24 fun dest_hd f_ord (Const (a, T)) = 
    25       let val ord = f_ord a in
    26         if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
    27       end
    28   | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
    29   | dest_hd _ (Var v) = ((1, v), 1)
    30   | dest_hd _ (Bound i) = ((1, (("", i), Term.dummyT)), 2)
    31   | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
    32 
    33 fun term_lpo f_ord (s, t) =
    34   let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
    35     if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
    36     then case hd_ord f_ord (f, g) of
    37 	GREATER =>
    38 	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
    39 	  then GREATER else LESS
    40       | EQUAL =>
    41 	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
    42 	  then list_ord (term_lpo f_ord) (ss, ts)
    43 	  else LESS
    44       | LESS => LESS
    45     else GREATER
    46   end
    47 and hd_ord f_ord (f, g) = case (f, g) of
    48     (Abs (_, T, t), Abs (_, U, u)) =>
    49       (case term_lpo f_ord (t, u) of EQUAL => Term.typ_ord (T, U) | ord => ord)
    50   | (_, _) => prod_ord (prod_ord int_ord
    51                   (prod_ord Term.indexname_ord Term.typ_ord)) int_ord
    52                 (dest_hd f_ord f, dest_hd f_ord g)
    53 
    54 in
    55 
    56 (*** Term order for commutative rings ***)
    57 
    58 fun ring_ord a =
    59   find_index_eq a ["0", "op +", "uminus", "op -", "1", "op *"];
    60 
    61 fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
    62 
    63 (* Some code useful for debugging
    64 
    65 val intT = HOLogic.intT;
    66 val a = Free ("a", intT);
    67 val b = Free ("b", intT);
    68 val c = Free ("c", intT);
    69 val plus = Const ("op +", [intT, intT]--->intT);
    70 val mult = Const ("op *", [intT, intT]--->intT);
    71 val uminus = Const ("uminus", intT-->intT);
    72 val one = Const ("1", intT);
    73 val f = Const("f", intT-->intT);
    74 
    75 *)
    76 
    77 (*** Rewrite rules ***)
    78 
    79 val a_assoc = thm "ring.a_assoc";
    80 val l_zero = thm "ring.l_zero";
    81 val l_neg = thm "ring.l_neg";
    82 val a_comm = thm "ring.a_comm";
    83 val m_assoc = thm "ring.m_assoc";
    84 val l_one = thm "ring.l_one";
    85 val l_distr = thm "ring.l_distr";
    86 val m_comm = thm "ring.m_comm";
    87 val minus_def = thm "ring.minus_def";
    88 val inverse_def = thm "ring.inverse_def";
    89 val divide_def = thm "ring.divide_def";
    90 val power_def = thm "ring.power_def";
    91 
    92 (* These are the following axioms:
    93 
    94   a_assoc:      "(a + b) + c = a + (b + c)"
    95   l_zero:       "0 + a = a"
    96   l_neg:        "(-a) + a = 0"
    97   a_comm:       "a + b = b + a"
    98 
    99   m_assoc:      "(a * b) * c = a * (b * c)"
   100   l_one:        "1 * a = a"
   101 
   102   l_distr:      "(a + b) * c = a * c + b * c"
   103 
   104   m_comm:       "a * b = b * a"
   105 
   106   -- {* Definition of derived operations *}
   107 
   108   minus_def:    "a - b = a + (-b)"
   109   inverse_def:  "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
   110   divide_def:   "a / b = a * inverse b"
   111   power_def:    "a ^ n = nat_rec 1 (%u b. b * a) n"
   112 *)
   113 
   114 (* These lemmas are needed in the proofs *)
   115 val trans = thm "trans";
   116 val sym = thm "sym";
   117 val subst = thm "subst";
   118 val box_equals = thm "box_equals";
   119 val arg_cong = thm "arg_cong";
   120 (* current theory *)
   121 val thy = the_context ();
   122 
   123 (* derived rewrite rules *)
   124 val a_lcomm = prove_goal thy "(a::'a::ring)+(b+c) = b+(a+c)"
   125   (fn _ => [rtac (a_comm RS trans) 1, rtac (a_assoc RS trans) 1,
   126      rtac (a_comm RS arg_cong) 1]);
   127 val r_zero = prove_goal thy "(a::'a::ring) + 0 = a"
   128   (fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]);
   129 val r_neg = prove_goal thy "(a::'a::ring) + (-a) = 0"
   130   (fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]);
   131 val r_neg2 = prove_goal thy "(a::'a::ring) + (-a + b) = b"
   132   (fn _ => [rtac (a_assoc RS sym RS trans) 1,
   133      simp_tac (simpset() addsimps [r_neg, l_zero]) 1]);
   134 val r_neg1 = prove_goal thy "-(a::'a::ring) + (a + b) = b"
   135   (fn _ => [rtac (a_assoc RS sym RS trans) 1,
   136      simp_tac (simpset() addsimps [l_neg, l_zero]) 1]);
   137 (* auxiliary *)
   138 val a_lcancel = prove_goal thy "!! a::'a::ring. a + b = a + c ==> b = c"
   139   (fn _ => [rtac box_equals 1, rtac l_zero 2, rtac l_zero 2,
   140      res_inst_tac [("a1", "a")] (l_neg RS subst) 1,
   141      asm_simp_tac (simpset() addsimps [a_assoc]) 1]);
   142 val minus_add = prove_goal thy "-((a::'a::ring) + b) = (-a) + (-b)"
   143   (fn _ => [res_inst_tac [("a", "a+b")] a_lcancel 1,
   144      simp_tac (simpset() addsimps [r_neg, l_neg, l_zero, 
   145                                    a_assoc, a_comm, a_lcomm]) 1]);
   146 val minus_minus = prove_goal thy "-(-(a::'a::ring)) = a"
   147   (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1, rtac (l_neg RS sym) 1]);
   148 val minus0 = prove_goal thy "- 0 = (0::'a::ring)"
   149   (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1,
   150      rtac (l_zero RS sym) 1]);
   151 
   152 (* derived rules for multiplication *)
   153 val m_lcomm = prove_goal thy "(a::'a::ring)*(b*c) = b*(a*c)"
   154   (fn _ => [rtac (m_comm RS trans) 1, rtac (m_assoc RS trans) 1,
   155      rtac (m_comm RS arg_cong) 1]);
   156 val r_one = prove_goal thy "(a::'a::ring) * 1 = a"
   157   (fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]);
   158 val r_distr = prove_goal thy "(a::'a::ring) * (b + c) = a * b + a * c"
   159   (fn _ => [rtac (m_comm RS trans) 1, rtac (l_distr RS trans) 1,
   160      simp_tac (simpset() addsimps [m_comm]) 1]);
   161 (* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *)
   162 val l_null = prove_goal thy "0 * (a::'a::ring) = 0"
   163   (fn _ => [rtac a_lcancel 1, rtac (l_distr RS sym RS trans) 1,
   164      simp_tac (simpset() addsimps [r_zero]) 1]);
   165 val r_null = prove_goal thy "(a::'a::ring) * 0 = 0"
   166   (fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]);
   167 val l_minus = prove_goal thy "(-(a::'a::ring)) * b = - (a * b)"
   168   (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1,
   169      rtac (l_distr RS sym RS trans) 1,
   170      simp_tac (simpset() addsimps [l_null, r_neg]) 1]);
   171 val r_minus = prove_goal thy "(a::'a::ring) * (-b) = - (a * b)"
   172   (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1,
   173      rtac (r_distr RS sym RS trans) 1,
   174      simp_tac (simpset() addsimps [r_null, r_neg]) 1]);
   175 
   176 val ring_ss = HOL_basic_ss settermless termless_ring addsimps
   177   [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def,
   178    r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
   179    a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus];
   180 
   181 (* Note: r_one is not necessary in ring_ss *)
   182 
   183 val x = bind_thms ("ring_simps", 
   184   [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0, 
   185   l_one, r_one, l_null, r_null, l_minus, r_minus]);
   186 
   187 (* note: not added (and not proved):
   188   a_lcancel_eq, a_rcancel_eq, power_one, power_Suc, power_zero, power_one,
   189   m_lcancel_eq, m_rcancel_eq,
   190   thms involving dvd, integral domains, fields
   191 *)
   192 
   193 end;