src/HOL/Orderings.thy
changeset 34065 6f8f9835e219
parent 33519 e31a85f92ce9
child 34250 3b619abaa67a
     1.1 --- a/src/HOL/Orderings.thy	Fri Dec 11 14:43:55 2009 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Fri Dec 11 14:43:56 2009 +0100
     1.3 @@ -1257,45 +1257,4 @@
     1.4  lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
     1.5    unfolding le_fun_def by simp
     1.6  
     1.7 -text {*
     1.8 -  Handy introduction and elimination rules for @{text "\<le>"}
     1.9 -  on unary and binary predicates
    1.10 -*}
    1.11 -
    1.12 -lemma predicate1I:
    1.13 -  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    1.14 -  shows "P \<le> Q"
    1.15 -  apply (rule le_funI)
    1.16 -  apply (rule le_boolI)
    1.17 -  apply (rule PQ)
    1.18 -  apply assumption
    1.19 -  done
    1.20 -
    1.21 -lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    1.22 -  apply (erule le_funE)
    1.23 -  apply (erule le_boolE)
    1.24 -  apply assumption+
    1.25 -  done
    1.26 -
    1.27 -lemma predicate2I [Pure.intro!, intro!]:
    1.28 -  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
    1.29 -  shows "P \<le> Q"
    1.30 -  apply (rule le_funI)+
    1.31 -  apply (rule le_boolI)
    1.32 -  apply (rule PQ)
    1.33 -  apply assumption
    1.34 -  done
    1.35 -
    1.36 -lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
    1.37 -  apply (erule le_funE)+
    1.38 -  apply (erule le_boolE)
    1.39 -  apply assumption+
    1.40 -  done
    1.41 -
    1.42 -lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
    1.43 -  by (rule predicate1D)
    1.44 -
    1.45 -lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
    1.46 -  by (rule predicate2D)
    1.47 -
    1.48  end