Changes due to new abel_cancel.ML
authornipkow
Sat Jun 25 16:06:17 2005 +0200 (2005-06-25)
changeset 16568e02fe7ae212b
parent 16567 1ff73dc29166
child 16569 a12992c34c12
Changes due to new abel_cancel.ML
src/HOL/Algebra/ringsimp.ML
src/HOL/OrderedGroup.ML
src/HOL/Ring_and_Field.thy
src/HOL/ex/Lagrange.thy
     1.1 --- a/src/HOL/Algebra/ringsimp.ML	Sat Jun 25 12:37:07 2005 +0200
     1.2 +++ b/src/HOL/Algebra/ringsimp.ML	Sat Jun 25 16:06:17 2005 +0200
     1.3 @@ -5,61 +5,13 @@
     1.4    Copyright: TU Muenchen
     1.5  *)
     1.6  
     1.7 -local
     1.8 -
     1.9 -(*** Lexicographic path order on terms.
    1.10 -
    1.11 -  See Baader & Nipkow, Term rewriting, CUP 1998.
    1.12 -  Without variables.  Const, Var, Bound, Free and Abs are treated all as
    1.13 -  constants.
    1.14 -
    1.15 -  f_ord maps strings to integers and serves two purposes:
    1.16 -  - Predicate on constant symbols.  Those that are not recognised by f_ord
    1.17 -    must be mapped to ~1.
    1.18 -  - Order on the recognised symbols.  These must be mapped to distinct
    1.19 -    integers >= 0.
    1.20 -
    1.21 -***)
    1.22 -
    1.23 -fun dest_hd f_ord (Const (a, T)) = 
    1.24 -      let val ord = f_ord a in
    1.25 -        if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
    1.26 -      end
    1.27 -  | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
    1.28 -  | dest_hd _ (Var v) = ((1, v), 1)
    1.29 -  | dest_hd _ (Bound i) = ((1, (("", i), Term.dummyT)), 2)
    1.30 -  | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
    1.31 -
    1.32 -fun term_lpo f_ord (s, t) =
    1.33 -  let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
    1.34 -    if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
    1.35 -    then case hd_ord f_ord (f, g) of
    1.36 -	GREATER =>
    1.37 -	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
    1.38 -	  then GREATER else LESS
    1.39 -      | EQUAL =>
    1.40 -	  if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
    1.41 -	  then list_ord (term_lpo f_ord) (ss, ts)
    1.42 -	  else LESS
    1.43 -      | LESS => LESS
    1.44 -    else GREATER
    1.45 -  end
    1.46 -and hd_ord f_ord (f, g) = case (f, g) of
    1.47 -    (Abs (_, T, t), Abs (_, U, u)) =>
    1.48 -      (case term_lpo f_ord (t, u) of EQUAL => Term.typ_ord (T, U) | ord => ord)
    1.49 -  | (_, _) => prod_ord (prod_ord int_ord
    1.50 -                  (prod_ord Term.indexname_ord Term.typ_ord)) int_ord
    1.51 -                (dest_hd f_ord f, dest_hd f_ord g)
    1.52 -
    1.53 -in
    1.54 -
    1.55  (*** Term order for commutative rings ***)
    1.56  
    1.57  fun ring_ord a =
    1.58    find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
    1.59    "CRing.minus", "Group.monoid.one", "Group.monoid.mult"];
    1.60  
    1.61 -fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
    1.62 +fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
    1.63  
    1.64  val cring_ss = HOL_ss settermless termless_ring;
    1.65  
    1.66 @@ -95,5 +47,3 @@
    1.67     r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0,
    1.68     a_lcomm, m_lcomm, (*r_one,*) r_distr, l_null, r_null, l_minus, r_minus];
    1.69  *)
    1.70 -
    1.71 -end;
    1.72 \ No newline at end of file
     2.1 --- a/src/HOL/OrderedGroup.ML	Sat Jun 25 12:37:07 2005 +0200
     2.2 +++ b/src/HOL/OrderedGroup.ML	Sat Jun 25 16:06:17 2005 +0200
     2.3 @@ -1,40 +1,35 @@
     2.4  (*  Title:      HOL/OrderedGroup.ML
     2.5      ID:         $Id$
     2.6 -    Author:     Steven Obua, Technische Universität München
     2.7 +    Author:     Steven Obua, Tobias Nipkow, Technische Universität München
     2.8  *)
     2.9  
    2.10  structure ab_group_add_cancel_data :> ABEL_CANCEL  = 
    2.11  struct
    2.12 -  val ss = simpset_of HOL.thy
    2.13 +
    2.14 +(*** Term order for abelian groups ***)
    2.15 +
    2.16 +fun agrp_ord a = find_index_eq a ["0", "op +", "uminus", "op -"];
    2.17 +
    2.18 +fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
    2.19 +
    2.20 +val cancel_ss = HOL_basic_ss settermless termless_agrp addsimps
    2.21 +  [thm "add_assoc", thm "add_commute", thm "add_left_commute",
    2.22 +   thm "add_0", thm "add_0_right",
    2.23 +   thm "diff_def", thm "minus_add_distrib",
    2.24 +   thm "minus_minus", thm "minus_zero",
    2.25 +   thm "right_minus", thm "left_minus",
    2.26 +   thm "add_minus_cancel", thm "minus_add_cancel"];
    2.27 +  
    2.28    val eq_reflection = thm "eq_reflection"
    2.29    
    2.30    val thy_ref = Theory.self_ref (theory "OrderedGroup")
    2.31  
    2.32    val T = TFree("'a", ["OrderedGroup.ab_group_add"])
    2.33 -  
    2.34 -  val restrict_to_left = thm "restrict_to_left"
    2.35 -  val add_cancel_21 = thm "add_cancel_21"
    2.36 -  val add_cancel_end = thm "add_cancel_end"
    2.37 -  val add_left_cancel = thm "add_left_cancel"
    2.38 -  val add_assoc = thm "add_assoc"
    2.39 -  val add_commute = thm "add_commute"
    2.40 -  val add_left_commute = thm "add_left_commute"
    2.41 -  val add_0 = thm "add_0"
    2.42 -  val add_0_right = thm "add_0_right"
    2.43 -  
    2.44 -  val eq_diff_eq = thm "eq_diff_eq"
    2.45 -  
    2.46 +
    2.47    val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
    2.48    fun dest_eqI th = 
    2.49        #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
    2.50  	      (HOLogic.dest_Trueprop (concl_of th)))  
    2.51 -
    2.52 -  val diff_def		= thm "diff_def"
    2.53 -  val minus_add_distrib	= thm "minus_add_distrib"
    2.54 -  val minus_minus	= thm "minus_minus"
    2.55 -  val minus_0		= thm "minus_zero"
    2.56 -  val add_inverses	= [thm "right_minus", thm "left_minus"]
    2.57 -  val cancel_simps	= [thm "add_minus_cancel", thm "minus_add_cancel"]
    2.58  end;
    2.59  
    2.60  structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data);
     3.1 --- a/src/HOL/Ring_and_Field.thy	Sat Jun 25 12:37:07 2005 +0200
     3.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Jun 25 16:06:17 2005 +0200
     3.3 @@ -1555,13 +1555,13 @@
     3.4    have xy: "- ?x <= ?y"
     3.5      apply (simp)
     3.6      apply (rule_tac y="0::'a" in order_trans)
     3.7 -    apply (rule addm2)+
     3.8 +    apply (rule addm2)
     3.9      apply (simp_all add: mult_pos_le mult_neg_le)
    3.10 -    apply (rule addm)+
    3.11 +    apply (rule addm)
    3.12      apply (simp_all add: mult_pos_le mult_neg_le)
    3.13      done
    3.14    have yx: "?y <= ?x"
    3.15 -    apply (simp add: add_ac)
    3.16 +    apply (simp add:diff_def)
    3.17      apply (rule_tac y=0 in order_trans)
    3.18      apply (rule addm2, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)
    3.19      apply (rule addm, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)
    3.20 @@ -1687,7 +1687,7 @@
    3.21    have 6: "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <= abs (y * (A - A') + (y * A' - c') + (c'-c)) * abs x"
    3.22      by (simp add: abs_le_mult)
    3.23    have 7: "(abs (y * (A - A') + (y * A' - c') + (c'-c))) * abs x <= (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x"
    3.24 -    by (simp add: abs_triangle_ineq mult_right_mono)
    3.25 +    by(rule abs_triangle_ineq [THEN mult_right_mono]) simp
    3.26    have 8: " (abs (y * (A-A') + (y*A'-c')) + abs(c'-c)) * abs x <=  (abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x"
    3.27      by (simp add: abs_triangle_ineq mult_right_mono)    
    3.28    have 9: "(abs (y * (A-A')) + abs (y*A'-c') + abs(c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x"
    3.29 @@ -1712,7 +1712,7 @@
    3.30      by (simp)
    3.31    show ?thesis 
    3.32      apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
    3.33 -    apply (simp_all add: 5 14[simplified abs_of_ge_0[of y, simplified prems]])
    3.34 +    apply (simp_all only: 5 14[simplified abs_of_ge_0[of y, simplified prems]])
    3.35      done
    3.36  qed
    3.37  
     4.1 --- a/src/HOL/ex/Lagrange.thy	Sat Jun 25 12:37:07 2005 +0200
     4.2 +++ b/src/HOL/ex/Lagrange.thy	Sat Jun 25 16:06:17 2005 +0200
     4.3 @@ -21,6 +21,8 @@
     4.4  abstract theorem about commutative rings.  It has, a priori, nothing to do
     4.5  with nat.*)
     4.6  
     4.7 +ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]"
     4.8 +
     4.9  (*once a slow step, but now (2001) just three seconds!*)
    4.10  lemma Lagrange_lemma:
    4.11   "!!x1::'a::comm_ring.