removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
authorwenzelm
Tue Mar 18 20:33:31 2008 +0100 (2008-03-18)
changeset 263169e9e67e33557
parent 26315 cb3badaa192e
child 26317 01a98fd72eae
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
src/HOL/HoareParallel/Gar_Coll.thy
src/HOL/HoareParallel/Graph.thy
src/HOL/HoareParallel/Mul_Gar_Coll.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Library/Permutation.thy
src/HOL/NumberTheory/Factorization.thy
     1.1 --- a/src/HOL/HoareParallel/Gar_Coll.thy	Tue Mar 18 20:33:29 2008 +0100
     1.2 +++ b/src/HOL/HoareParallel/Gar_Coll.thy	Tue Mar 18 20:33:31 2008 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4    apply (erule_tac x=i in allE , erule (1) notE impE)
     1.5    apply simp
     1.6    apply clarify
     1.7 -  apply (drule Nat.le_imp_less_or_eq)
     1.8 +  apply (drule_tac y = r in le_imp_less_or_eq)
     1.9    apply (erule disjE)
    1.10     apply (subgoal_tac "Suc (ind x)\<le>r")
    1.11      apply fast
    1.12 @@ -276,7 +276,7 @@
    1.13     apply (erule_tac x=i in allE , erule (1) notE impE)
    1.14     apply simp
    1.15     apply clarify
    1.16 -   apply (drule Nat.le_imp_less_or_eq)
    1.17 +   apply (drule_tac y = r in le_imp_less_or_eq)
    1.18     apply (erule disjE)
    1.19      apply (subgoal_tac "Suc (ind x)\<le>r")
    1.20       apply fast
    1.21 @@ -309,7 +309,7 @@
    1.22   apply (erule_tac x=i in allE , erule (1) notE impE)
    1.23   apply simp
    1.24   apply clarify
    1.25 - apply (drule Nat.le_imp_less_or_eq)
    1.26 + apply (drule_tac y = r in le_imp_less_or_eq)
    1.27   apply (erule disjE)
    1.28    apply (subgoal_tac "Suc (ind x)\<le>r")
    1.29     apply fast
     2.1 --- a/src/HOL/HoareParallel/Graph.thy	Tue Mar 18 20:33:29 2008 +0100
     2.2 +++ b/src/HOL/HoareParallel/Graph.thy	Tue Mar 18 20:33:31 2008 +0100
     2.3 @@ -336,7 +336,7 @@
     2.4   apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
     2.5   apply simp
     2.6   apply(case_tac "j\<le>R")
     2.7 -  apply(drule Nat.le_imp_less_or_eq)
     2.8 +  apply(drule le_imp_less_or_eq [of _ R])
     2.9    apply(erule disjE)
    2.10     apply(erule allE , erule (1) notE impE)
    2.11     apply force
     3.1 --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Tue Mar 18 20:33:29 2008 +0100
     3.2 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Tue Mar 18 20:33:31 2008 +0100
     3.3 @@ -383,7 +383,7 @@
     3.4  apply force
     3.5  --{* 1 subgoal left *}
     3.6  apply clarify
     3.7 -apply(drule Nat.le_imp_less_or_eq)
     3.8 +apply(drule_tac x = "ind x" in le_imp_less_or_eq)
     3.9  apply (simp_all add:Blacks_def)
    3.10  done
    3.11  
     4.1 --- a/src/HOL/Hyperreal/Integration.thy	Tue Mar 18 20:33:29 2008 +0100
     4.2 +++ b/src/HOL/Hyperreal/Integration.thy	Tue Mar 18 20:33:31 2008 +0100
     4.3 @@ -561,7 +561,7 @@
     4.4  apply (frule partition_eq_bound)
     4.5  apply (drule_tac [2] partition_gt, auto)
     4.6  apply (metis dense_linear_order_class.dlo_simps(8) not_less partition_rhs partition_rhs2)
     4.7 -apply (metis Nat.le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2)
     4.8 +apply (metis le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2)
     4.9  done
    4.10  
    4.11  lemma lemma_additivity4_psize_eq:
    4.12 @@ -574,7 +574,7 @@
    4.13  apply (auto intro: partition_lt_Suc)
    4.14  apply (drule_tac n = n in partition_lt_gen, assumption)
    4.15  apply (arith, arith)
    4.16 -apply (cut_tac m = na and n = "psize D" in Nat.less_linear)
    4.17 +apply (cut_tac x = na and y = "psize D" in less_linear)
    4.18  apply (auto dest: partition_lt_cancel)
    4.19  apply (rule_tac x=N and y=n in linorder_cases)
    4.20  apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
     5.1 --- a/src/HOL/Hyperreal/Poly.thy	Tue Mar 18 20:33:29 2008 +0100
     5.2 +++ b/src/HOL/Hyperreal/Poly.thy	Tue Mar 18 20:33:31 2008 +0100
     5.3 @@ -739,7 +739,7 @@
     5.4        ==> EX! n. ([-a, 1] %^ n) divides p &
     5.5                   ~(([-a, 1] %^ (Suc n)) divides p)"
     5.6  apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
     5.7 -apply (metis Suc_leI Nat.less_linear poly_exp_divides)
     5.8 +apply (metis Suc_leI less_linear poly_exp_divides)
     5.9  done
    5.10  
    5.11  text{*Order*}
     6.1 --- a/src/HOL/Library/Permutation.thy	Tue Mar 18 20:33:29 2008 +0100
     6.2 +++ b/src/HOL/Library/Permutation.thy	Tue Mar 18 20:33:31 2008 +0100
     6.3 @@ -188,7 +188,7 @@
     6.4     apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
     6.5      apply (fastsimp simp add: insert_ident)
     6.6     apply (metis distinct_remdups set_remdups)
     6.7 -  apply (metis Nat.le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le)
     6.8 +  apply (metis le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le)
     6.9    done
    6.10  
    6.11  lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
     7.1 --- a/src/HOL/NumberTheory/Factorization.thy	Tue Mar 18 20:33:29 2008 +0100
     7.2 +++ b/src/HOL/NumberTheory/Factorization.thy	Tue Mar 18 20:33:31 2008 +0100
     7.3 @@ -295,7 +295,7 @@
     7.4  lemma primel_prod_less:
     7.5    "primel (x # xs) ==>
     7.6      primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys"
     7.7 -  by (metis Nat.less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff
     7.8 +  by (metis less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff
     7.9      nat_less_le nat_mult_1 prime_def primel_hd_tl primel_prod_gz prod.simps(2))
    7.10  
    7.11  lemma prod_one_empty: