Simplified proofs due to transitivity reasoner setup.
authorballarin
Tue Sep 18 18:52:17 2007 +0200 (2007-09-18)
changeset 2464085a6c200ecd3
parent 24639 9b73bc9b05a1
child 24641 448edc627ee4
Simplified proofs due to transitivity reasoner setup.
src/HOL/Dense_Linear_Order.thy
src/HOL/Lattices.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Dense_Linear_Order.thy	Tue Sep 18 18:51:07 2007 +0200
     1.2 +++ b/src/HOL/Dense_Linear_Order.thy	Tue Sep 18 18:52:17 2007 +0200
     1.3 @@ -232,15 +232,8 @@
     1.4    from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<sqsubseteq> u" by auto
     1.5    from th1 th2 H have "?ML \<sqsubset> ?MU" by auto
     1.6    with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast
     1.7 -  from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w" 
     1.8 -    apply auto
     1.9 -    apply (erule_tac x="l" in ballE)
    1.10 -    by (auto intro: le_less_trans)
    1.11 -
    1.12 -  moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u" 
    1.13 -    apply auto
    1.14 -    apply (erule_tac x="u" in ballE)
    1.15 -    by (auto intro: less_le_trans)
    1.16 +  from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w" by auto
    1.17 +  moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u" by auto
    1.18    ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
    1.19  qed
    1.20  
     2.1 --- a/src/HOL/Lattices.thy	Tue Sep 18 18:51:07 2007 +0200
     2.2 +++ b/src/HOL/Lattices.thy	Tue Sep 18 18:52:17 2007 +0200
     2.3 @@ -289,8 +289,7 @@
     2.4    fix x y z
     2.5    show "max x (min y z) = min (max x y) (max x z)"
     2.6    unfolding min_def max_def
     2.7 -    by (auto simp add: intro: antisym, unfold not_le,
     2.8 -      auto intro: less_trans le_less_trans aux)
     2.9 +  by auto
    2.10  qed (auto simp add: min_def max_def not_le less_imp_le)
    2.11  
    2.12  interpretation min_max:
     3.1 --- a/src/HOL/List.thy	Tue Sep 18 18:51:07 2007 +0200
     3.2 +++ b/src/HOL/List.thy	Tue Sep 18 18:52:17 2007 +0200
     3.3 @@ -2509,7 +2509,6 @@
     3.4  lemma sorted_insort: "sorted (insort x xs) = sorted xs"
     3.5  apply (induct xs)
     3.6   apply(auto simp:sorted_Cons set_insort not_le less_imp_le)
     3.7 -apply(blast intro:order_trans)
     3.8  done
     3.9  
    3.10  theorem sorted_sort[simp]: "sorted (sort xs)"