src/HOL/Lattices.thy
changeset 54857 5c05f7c5f8ae
parent 54555 e8c5e95d338b
child 54858 c1c334198504
     1.1 --- a/src/HOL/Lattices.thy	Tue Dec 24 11:24:14 2013 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Tue Dec 24 11:24:16 2013 +0100
     1.3 @@ -190,7 +190,7 @@
     1.4    by (rule order_trans) auto
     1.5  
     1.6  lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
     1.7 -  by (rule inf_greatest) (* FIXME: duplicate lemma *)
     1.8 +  by (fact inf_greatest) (* FIXME: duplicate lemma *)
     1.9  
    1.10  lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    1.11    by (blast intro: order_trans inf_le1 inf_le2)
    1.12 @@ -226,7 +226,7 @@
    1.13  
    1.14  lemma le_supI:
    1.15    "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    1.16 -  by (rule sup_least) (* FIXME: duplicate lemma *)
    1.17 +  by (fact sup_least) (* FIXME: duplicate lemma *)
    1.18  
    1.19  lemma le_supE:
    1.20    "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    1.21 @@ -856,16 +856,16 @@
    1.22    by (simp add: inf_fun_def)
    1.23  
    1.24  lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
    1.25 -  by (simp add: inf_fun_def)
    1.26 +  by (rule inf1E)
    1.27  
    1.28  lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
    1.29 -  by (simp add: inf_fun_def)
    1.30 +  by (rule inf2E)
    1.31  
    1.32  lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
    1.33 -  by (simp add: inf_fun_def)
    1.34 +  by (rule inf1E)
    1.35  
    1.36  lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
    1.37 -  by (simp add: inf_fun_def)
    1.38 +  by (rule inf2E)
    1.39  
    1.40  lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x"
    1.41    by (simp add: sup_fun_def)