moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
authorhaftmann
Fri Dec 11 14:43:56 2009 +0100 (2009-12-11)
changeset 340656f8f9835e219
parent 34064 eee04bbbae7e
child 34066 23407a527fe4
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
src/HOL/Orderings.thy
src/HOL/Predicate.thy
src/HOL/Tools/Function/function_core.ML
     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
     2.1 --- a/src/HOL/Predicate.thy	Fri Dec 11 14:43:55 2009 +0100
     2.2 +++ b/src/HOL/Predicate.thy	Fri Dec 11 14:43:56 2009 +0100
     2.3 @@ -19,6 +19,53 @@
     2.4  
     2.5  subsection {* Predicates as (complete) lattices *}
     2.6  
     2.7 +
     2.8 +text {*
     2.9 +  Handy introduction and elimination rules for @{text "\<le>"}
    2.10 +  on unary and binary predicates
    2.11 +*}
    2.12 +
    2.13 +lemma predicate1I:
    2.14 +  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    2.15 +  shows "P \<le> Q"
    2.16 +  apply (rule le_funI)
    2.17 +  apply (rule le_boolI)
    2.18 +  apply (rule PQ)
    2.19 +  apply assumption
    2.20 +  done
    2.21 +
    2.22 +lemma predicate1D [Pure.dest?, dest?]:
    2.23 +  "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    2.24 +  apply (erule le_funE)
    2.25 +  apply (erule le_boolE)
    2.26 +  apply assumption+
    2.27 +  done
    2.28 +
    2.29 +lemma rev_predicate1D:
    2.30 +  "P x ==> P <= Q ==> Q x"
    2.31 +  by (rule predicate1D)
    2.32 +
    2.33 +lemma predicate2I [Pure.intro!, intro!]:
    2.34 +  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
    2.35 +  shows "P \<le> Q"
    2.36 +  apply (rule le_funI)+
    2.37 +  apply (rule le_boolI)
    2.38 +  apply (rule PQ)
    2.39 +  apply assumption
    2.40 +  done
    2.41 +
    2.42 +lemma predicate2D [Pure.dest, dest]:
    2.43 +  "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
    2.44 +  apply (erule le_funE)+
    2.45 +  apply (erule le_boolE)
    2.46 +  apply assumption+
    2.47 +  done
    2.48 +
    2.49 +lemma rev_predicate2D:
    2.50 +  "P x y ==> P <= Q ==> Q x y"
    2.51 +  by (rule predicate2D)
    2.52 +
    2.53 +
    2.54  subsubsection {* Equality *}
    2.55  
    2.56  lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
     3.1 --- a/src/HOL/Tools/Function/function_core.ML	Fri Dec 11 14:43:55 2009 +0100
     3.2 +++ b/src/HOL/Tools/Function/function_core.ML	Fri Dec 11 14:43:56 2009 +0100
     3.3 @@ -605,7 +605,7 @@
     3.4  (** Induction rule **)
     3.5  
     3.6  
     3.7 -val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
     3.8 +val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct}
     3.9  
    3.10  
    3.11  fun mk_partial_induct_rule thy globals R complete_thm clauses =