src/HOL/Fun.thy
changeset 23878 bd651ecd4b8a
parent 23738 3a801ffdc58c
child 24017 363287741ebe
     1.1 --- a/src/HOL/Fun.thy	Fri Jul 20 00:01:40 2007 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Jul 20 14:27:56 2007 +0200
     1.3 @@ -460,87 +460,6 @@
     1.4  by (simp add: bij_def)
     1.5  
     1.6  
     1.7 -subsection {* Order and lattice on functions *}
     1.8 -
     1.9 -instance "fun" :: (type, ord) ord
    1.10 -  le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
    1.11 -  less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
    1.12 -
    1.13 -lemmas [code func del] = le_fun_def less_fun_def
    1.14 -
    1.15 -instance "fun" :: (type, order) order
    1.16 -  by default
    1.17 -    (auto simp add: le_fun_def less_fun_def expand_fun_eq
    1.18 -       intro: order_trans order_antisym)
    1.19 -
    1.20 -lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
    1.21 -  unfolding le_fun_def by simp
    1.22 -
    1.23 -lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
    1.24 -  unfolding le_fun_def by simp
    1.25 -
    1.26 -lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
    1.27 -  unfolding le_fun_def by simp
    1.28 -
    1.29 -text {*
    1.30 -  Handy introduction and elimination rules for @{text "\<le>"}
    1.31 -  on unary and binary predicates
    1.32 -*}
    1.33 -
    1.34 -lemma predicate1I [Pure.intro!, intro!]:
    1.35 -  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    1.36 -  shows "P \<le> Q"
    1.37 -  apply (rule le_funI)
    1.38 -  apply (rule le_boolI)
    1.39 -  apply (rule PQ)
    1.40 -  apply assumption
    1.41 -  done
    1.42 -
    1.43 -lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    1.44 -  apply (erule le_funE)
    1.45 -  apply (erule le_boolE)
    1.46 -  apply assumption+
    1.47 -  done
    1.48 -
    1.49 -lemma predicate2I [Pure.intro!, intro!]:
    1.50 -  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
    1.51 -  shows "P \<le> Q"
    1.52 -  apply (rule le_funI)+
    1.53 -  apply (rule le_boolI)
    1.54 -  apply (rule PQ)
    1.55 -  apply assumption
    1.56 -  done
    1.57 -
    1.58 -lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
    1.59 -  apply (erule le_funE)+
    1.60 -  apply (erule le_boolE)
    1.61 -  apply assumption+
    1.62 -  done
    1.63 -
    1.64 -lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
    1.65 -  by (rule predicate1D)
    1.66 -
    1.67 -lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
    1.68 -  by (rule predicate2D)
    1.69 -
    1.70 -instance "fun" :: (type, lattice) lattice
    1.71 -  inf_fun_eq: "inf f g \<equiv> (\<lambda>x. inf (f x) (g x))"
    1.72 -  sup_fun_eq: "sup f g \<equiv> (\<lambda>x. sup (f x) (g x))"
    1.73 -apply intro_classes
    1.74 -unfolding inf_fun_eq sup_fun_eq
    1.75 -apply (auto intro: le_funI)
    1.76 -apply (rule le_funI)
    1.77 -apply (auto dest: le_funD)
    1.78 -apply (rule le_funI)
    1.79 -apply (auto dest: le_funD)
    1.80 -done
    1.81 -
    1.82 -lemmas [code func del] = inf_fun_eq sup_fun_eq
    1.83 -
    1.84 -instance "fun" :: (type, distrib_lattice) distrib_lattice
    1.85 -  by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
    1.86 -
    1.87 -
    1.88  subsection {* Proof tool setup *} 
    1.89  
    1.90  text {* simplifies terms of the form
    1.91 @@ -600,8 +519,6 @@
    1.92  val datatype_injI = @{thm datatype_injI}
    1.93  val range_ex1_eq = @{thm range_ex1_eq}
    1.94  val expand_fun_eq = @{thm expand_fun_eq}
    1.95 -val sup_fun_eq = @{thm sup_fun_eq}
    1.96 -val sup_bool_eq = @{thm sup_bool_eq}
    1.97  *}
    1.98  
    1.99  end