# HG changeset patch # User wenzelm # Date 1120639300 -7200 # Node ID 3a7eee8cc0ff17e2c2f33c9763e84d308bffd232 # Parent 33f38450cab674115e4406fab036fee4e4f3fe44 removed term_lpo (now in Pure/term.ML); diff -r 33f38450cab6 -r 3a7eee8cc0ff src/HOL/Algebra/abstract/order.ML --- a/src/HOL/Algebra/abstract/order.ML Wed Jul 06 10:41:38 2005 +0200 +++ b/src/HOL/Algebra/abstract/order.ML Wed Jul 06 10:41:40 2005 +0200 @@ -5,60 +5,12 @@ Copyright: TU Muenchen *) -local - -(*** Lexicographic path order on terms. - - See Baader & Nipkow, Term rewriting, CUP 1998. - Without variables. Const, Var, Bound, Free and Abs are treated all as - constants. - - f_ord maps strings to integers and serves two purposes: - - Predicate on constant symbols. Those that are not recognised by f_ord - must be mapped to ~1. - - Order on the recognised symbols. These must be mapped to distinct - integers >= 0. - -***) - -fun dest_hd f_ord (Const (a, T)) = - let val ord = f_ord a in - if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0) - end - | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0) - | dest_hd _ (Var v) = ((1, v), 1) - | dest_hd _ (Bound i) = ((1, (("", i), Term.dummyT)), 2) - | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3); - -fun term_lpo f_ord (s, t) = - let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in - if forall (fn si => term_lpo f_ord (si, t) = LESS) ss - then case hd_ord f_ord (f, g) of - GREATER => - if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts - then GREATER else LESS - | EQUAL => - if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts - then list_ord (term_lpo f_ord) (ss, ts) - else LESS - | LESS => LESS - else GREATER - end -and hd_ord f_ord (f, g) = case (f, g) of - (Abs (_, T, t), Abs (_, U, u)) => - (case term_lpo f_ord (t, u) of EQUAL => Term.typ_ord (T, U) | ord => ord) - | (_, _) => prod_ord (prod_ord int_ord - (prod_ord Term.indexname_ord Term.typ_ord)) int_ord - (dest_hd f_ord f, dest_hd f_ord g) - -in - (*** Term order for commutative rings ***) fun ring_ord a = find_index_eq a ["0", "op +", "uminus", "op -", "1", "op *"]; -fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS); +fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS); (* Some code useful for debugging @@ -117,58 +69,56 @@ val subst = thm "subst"; val box_equals = thm "box_equals"; val arg_cong = thm "arg_cong"; -(* current theory *) -val thy = the_context (); (* derived rewrite rules *) -val a_lcomm = prove_goal thy "(a::'a::ring)+(b+c) = b+(a+c)" +val a_lcomm = prove_goal (the_context ()) "(a::'a::ring)+(b+c) = b+(a+c)" (fn _ => [rtac (a_comm RS trans) 1, rtac (a_assoc RS trans) 1, rtac (a_comm RS arg_cong) 1]); -val r_zero = prove_goal thy "(a::'a::ring) + 0 = a" +val r_zero = prove_goal (the_context ()) "(a::'a::ring) + 0 = a" (fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]); -val r_neg = prove_goal thy "(a::'a::ring) + (-a) = 0" +val r_neg = prove_goal (the_context ()) "(a::'a::ring) + (-a) = 0" (fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]); -val r_neg2 = prove_goal thy "(a::'a::ring) + (-a + b) = b" +val r_neg2 = prove_goal (the_context ()) "(a::'a::ring) + (-a + b) = b" (fn _ => [rtac (a_assoc RS sym RS trans) 1, simp_tac (simpset() addsimps [r_neg, l_zero]) 1]); -val r_neg1 = prove_goal thy "-(a::'a::ring) + (a + b) = b" +val r_neg1 = prove_goal (the_context ()) "-(a::'a::ring) + (a + b) = b" (fn _ => [rtac (a_assoc RS sym RS trans) 1, simp_tac (simpset() addsimps [l_neg, l_zero]) 1]); (* auxiliary *) -val a_lcancel = prove_goal thy "!! a::'a::ring. a + b = a + c ==> b = c" +val a_lcancel = prove_goal (the_context ()) "!! a::'a::ring. a + b = a + c ==> b = c" (fn _ => [rtac box_equals 1, rtac l_zero 2, rtac l_zero 2, res_inst_tac [("a1", "a")] (l_neg RS subst) 1, asm_simp_tac (simpset() addsimps [a_assoc]) 1]); -val minus_add = prove_goal thy "-((a::'a::ring) + b) = (-a) + (-b)" +val minus_add = prove_goal (the_context ()) "-((a::'a::ring) + b) = (-a) + (-b)" (fn _ => [res_inst_tac [("a", "a+b")] a_lcancel 1, simp_tac (simpset() addsimps [r_neg, l_neg, l_zero, a_assoc, a_comm, a_lcomm]) 1]); -val minus_minus = prove_goal thy "-(-(a::'a::ring)) = a" +val minus_minus = prove_goal (the_context ()) "-(-(a::'a::ring)) = a" (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1, rtac (l_neg RS sym) 1]); -val minus0 = prove_goal thy "- 0 = (0::'a::ring)" +val minus0 = prove_goal (the_context ()) "- 0 = (0::'a::ring)" (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1, rtac (l_zero RS sym) 1]); (* derived rules for multiplication *) -val m_lcomm = prove_goal thy "(a::'a::ring)*(b*c) = b*(a*c)" +val m_lcomm = prove_goal (the_context ()) "(a::'a::ring)*(b*c) = b*(a*c)" (fn _ => [rtac (m_comm RS trans) 1, rtac (m_assoc RS trans) 1, rtac (m_comm RS arg_cong) 1]); -val r_one = prove_goal thy "(a::'a::ring) * 1 = a" +val r_one = prove_goal (the_context ()) "(a::'a::ring) * 1 = a" (fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]); -val r_distr = prove_goal thy "(a::'a::ring) * (b + c) = a * b + a * c" +val r_distr = prove_goal (the_context ()) "(a::'a::ring) * (b + c) = a * b + a * c" (fn _ => [rtac (m_comm RS trans) 1, rtac (l_distr RS trans) 1, simp_tac (simpset() addsimps [m_comm]) 1]); (* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *) -val l_null = prove_goal thy "0 * (a::'a::ring) = 0" +val l_null = prove_goal (the_context ()) "0 * (a::'a::ring) = 0" (fn _ => [rtac a_lcancel 1, rtac (l_distr RS sym RS trans) 1, simp_tac (simpset() addsimps [r_zero]) 1]); -val r_null = prove_goal thy "(a::'a::ring) * 0 = 0" +val r_null = prove_goal (the_context ()) "(a::'a::ring) * 0 = 0" (fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]); -val l_minus = prove_goal thy "(-(a::'a::ring)) * b = - (a * b)" +val l_minus = prove_goal (the_context ()) "(-(a::'a::ring)) * b = - (a * b)" (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1, rtac (l_distr RS sym RS trans) 1, simp_tac (simpset() addsimps [l_null, r_neg]) 1]); -val r_minus = prove_goal thy "(a::'a::ring) * (-b) = - (a * b)" +val r_minus = prove_goal (the_context ()) "(a::'a::ring) * (-b) = - (a * b)" (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1, rtac (r_distr RS sym RS trans) 1, simp_tac (simpset() addsimps [r_null, r_neg]) 1]); @@ -189,5 +139,3 @@ m_lcancel_eq, m_rcancel_eq, thms involving dvd, integral domains, fields *) - -end; \ No newline at end of file