src/HOL/Predicate.thy
changeset 34065 6f8f9835e219
parent 34007 aea892559fc5
child 36008 23dfa8678c7c
     1.1 --- a/src/HOL/Predicate.thy	Fri Dec 11 14:43:55 2009 +0100
     1.2 +++ b/src/HOL/Predicate.thy	Fri Dec 11 14:43:56 2009 +0100
     1.3 @@ -19,6 +19,53 @@
     1.4  
     1.5  subsection {* Predicates as (complete) lattices *}
     1.6  
     1.7 +
     1.8 +text {*
     1.9 +  Handy introduction and elimination rules for @{text "\<le>"}
    1.10 +  on unary and binary predicates
    1.11 +*}
    1.12 +
    1.13 +lemma predicate1I:
    1.14 +  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    1.15 +  shows "P \<le> Q"
    1.16 +  apply (rule le_funI)
    1.17 +  apply (rule le_boolI)
    1.18 +  apply (rule PQ)
    1.19 +  apply assumption
    1.20 +  done
    1.21 +
    1.22 +lemma predicate1D [Pure.dest?, dest?]:
    1.23 +  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    1.24 +  apply (erule le_funE)
    1.25 +  apply (erule le_boolE)
    1.26 +  apply assumption+
    1.27 +  done
    1.28 +
    1.29 +lemma rev_predicate1D:
    1.30 +  "P x ==> P <= Q ==> Q x"
    1.31 +  by (rule predicate1D)
    1.32 +
    1.33 +lemma predicate2I [Pure.intro!, intro!]:
    1.34 +  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
    1.35 +  shows "P \<le> Q"
    1.36 +  apply (rule le_funI)+
    1.37 +  apply (rule le_boolI)
    1.38 +  apply (rule PQ)
    1.39 +  apply assumption
    1.40 +  done
    1.41 +
    1.42 +lemma predicate2D [Pure.dest, dest]:
    1.43 +  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
    1.44 +  apply (erule le_funE)+
    1.45 +  apply (erule le_boolE)
    1.46 +  apply assumption+
    1.47 +  done
    1.48 +
    1.49 +lemma rev_predicate2D:
    1.50 +  "P x y ==> P <= Q ==> Q x y"
    1.51 +  by (rule predicate2D)
    1.52 +
    1.53 +
    1.54  subsubsection {* Equality *}
    1.55  
    1.56  lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"