Generalized version of SUP and INF (with index set).
authorberghofe
Sat Mar 10 16:23:28 2007 +0100 (2007-03-10)
changeset 224306a56bf1b3a64
parent 22429 09e794384323
child 22431 28344ccffc35
Generalized version of SUP and INF (with index set).
src/HOL/FixedPoint.thy
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/FixedPoint.thy	Sat Mar 10 16:13:08 2007 +0100
     1.2 +++ b/src/HOL/FixedPoint.thy	Sat Mar 10 16:23:28 2007 +0100
     1.3 @@ -20,15 +20,6 @@
     1.4    Sup :: "'a::order set \<Rightarrow> 'a" where
     1.5    "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
     1.6  
     1.7 -definition
     1.8 -  SUP :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'b"  (binder "SUP " 10) where
     1.9 -  "(SUP x. f x) = Sup (f ` UNIV)"
    1.10 -
    1.11 -(*
    1.12 -abbreviation
    1.13 -  bot :: "'a::order" where
    1.14 -  "bot == Sup {}"
    1.15 -*)
    1.16  class comp_lat = order +
    1.17    assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x"
    1.18    assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A"
    1.19 @@ -39,6 +30,54 @@
    1.20  theorem Sup_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
    1.21    by (auto simp: Sup_def intro: Inf_lower)
    1.22  
    1.23 +definition
    1.24 +  SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
    1.25 +  "SUPR A f == Sup (f ` A)"
    1.26 +
    1.27 +definition
    1.28 +  INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::comp_lat) \<Rightarrow> 'b" where
    1.29 +  "INFI A f == Inf (f ` A)"
    1.30 +
    1.31 +syntax
    1.32 +  "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" 10)
    1.33 +  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" 10)
    1.34 +  "_INF1"     :: "pttrns => 'b => 'b"           ("(3INF _./ _)" 10)
    1.35 +  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" 10)
    1.36 +
    1.37 +translations
    1.38 +  "SUP x y. B"   == "SUP x. SUP y. B"
    1.39 +  "SUP x. B"     == "CONST SUPR UNIV (%x. B)"
    1.40 +  "SUP x. B"     == "SUP x:UNIV. B"
    1.41 +  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
    1.42 +  "INF x y. B"   == "INF x. INF y. B"
    1.43 +  "INF x. B"     == "CONST INFI UNIV (%x. B)"
    1.44 +  "INF x. B"     == "INF x:UNIV. B"
    1.45 +  "INF x:A. B"   == "CONST INFI A (%x. B)"
    1.46 +
    1.47 +(* To avoid eta-contraction of body: *)
    1.48 +print_translation {*
    1.49 +let
    1.50 +  fun btr' syn (A :: Abs abs :: ts) =
    1.51 +    let val (x,t) = atomic_abs_tr' abs
    1.52 +    in list_comb (Syntax.const syn $ x $ A $ t, ts) end
    1.53 +  val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
    1.54 +in
    1.55 +[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
    1.56 +end
    1.57 +*}
    1.58 +
    1.59 +lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
    1.60 +  by (auto simp add: SUPR_def intro: Sup_upper)
    1.61 +
    1.62 +lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
    1.63 +  by (auto simp add: SUPR_def intro: Sup_least)
    1.64 +
    1.65 +lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
    1.66 +  by (auto simp add: INFI_def intro: Inf_lower)
    1.67 +
    1.68 +lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
    1.69 +  by (auto simp add: INFI_def intro: Inf_greatest)
    1.70 +
    1.71  text {* A complete lattice is a lattice *}
    1.72  
    1.73  lemma is_meet_Inf: "is_meet (\<lambda>(x::'a::comp_lat) y. Inf {x, y})"
    1.74 @@ -62,59 +101,48 @@
    1.75    by (auto simp add: mono_def)
    1.76  
    1.77  lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = sup a (Sup A)"
    1.78 -apply(simp add:Sup_def)
    1.79 -apply(rule order_antisym)
    1.80 - apply(rule Inf_lower)
    1.81 - apply(clarsimp)
    1.82 - apply(rule le_supI2)
    1.83 - apply(rule Inf_greatest)
    1.84 - apply blast
    1.85 -apply simp
    1.86 -apply rule
    1.87 - apply(rule Inf_greatest)apply blast
    1.88 -apply(rule Inf_greatest)
    1.89 -apply(rule Inf_lower)
    1.90 -apply blast
    1.91 -done
    1.92 +  apply (rule order_antisym)
    1.93 +  apply (rule Sup_least)
    1.94 +  apply (erule insertE)
    1.95 +  apply (rule le_supI1)
    1.96 +  apply simp
    1.97 +  apply (rule le_supI2)
    1.98 +  apply (erule Sup_upper)
    1.99 +  apply (rule le_supI)
   1.100 +  apply (rule Sup_upper)
   1.101 +  apply simp
   1.102 +  apply (rule Sup_least)
   1.103 +  apply (rule Sup_upper)
   1.104 +  apply simp
   1.105 +  done
   1.106 +
   1.107 +lemma Inf_insert[simp]: "Inf (insert (a::'a::comp_lat) A) = inf a (Inf A)"
   1.108 +  apply (rule order_antisym)
   1.109 +  apply (rule le_infI)
   1.110 +  apply (rule Inf_lower)
   1.111 +  apply simp
   1.112 +  apply (rule Inf_greatest)
   1.113 +  apply (rule Inf_lower)
   1.114 +  apply simp
   1.115 +  apply (rule Inf_greatest)
   1.116 +  apply (erule insertE)
   1.117 +  apply (rule le_infI1)
   1.118 +  apply simp
   1.119 +  apply (rule le_infI2)
   1.120 +  apply (erule Inf_lower)
   1.121 +  done
   1.122  
   1.123  lemma bot_least[simp]: "Sup{} \<le> (x::'a::comp_lat)"
   1.124 -apply(simp add: Sup_def)
   1.125 -apply(rule Inf_lower)
   1.126 -apply blast
   1.127 -done
   1.128 -(*
   1.129 -lemma Inf_singleton[simp]: "Inf{a} = (a::'a::comp_lat)"
   1.130 -apply(rule order_antisym)
   1.131 - apply(simp add: Inf_lower)
   1.132 -apply(rule Inf_greatest)
   1.133 -apply(simp)
   1.134 -done
   1.135 -*)
   1.136 -lemma le_SupI: "(l::'a::comp_lat) : M \<Longrightarrow> l \<le> Sup M"
   1.137 -apply(simp add:Sup_def)
   1.138 -apply(rule Inf_greatest)
   1.139 -apply(simp)
   1.140 -done
   1.141 +  by (rule Sup_least) simp
   1.142 +
   1.143 +lemma top_greatest[simp]: "(x::'a::comp_lat) \<le> Inf{}"
   1.144 +  by (rule Inf_greatest) simp
   1.145  
   1.146 -lemma le_SUPI: "(l::'a::comp_lat) = M i \<Longrightarrow> l \<le> (SUP i. M i)"
   1.147 -apply(simp add:SUP_def)
   1.148 -apply(blast intro:le_SupI)
   1.149 -done
   1.150 +lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
   1.151 +  by (auto intro: order_antisym SUP_leI le_SUPI)
   1.152  
   1.153 -lemma Sup_leI: "(!!x. x:M \<Longrightarrow> x \<le> u) \<Longrightarrow> Sup M \<le> (u::'a::comp_lat)"
   1.154 -apply(simp add:Sup_def)
   1.155 -apply(rule Inf_lower)
   1.156 -apply(blast)
   1.157 -done
   1.158 -
   1.159 -
   1.160 -lemma SUP_leI: "(!!i. M i \<le> u) \<Longrightarrow> (SUP i. M i) \<le> (u::'a::comp_lat)"
   1.161 -apply(simp add:SUP_def)
   1.162 -apply(blast intro!:Sup_leI)
   1.163 -done
   1.164 -
   1.165 -lemma SUP_const[simp]: "(SUP i. M) = (M::'a::comp_lat)"
   1.166 -by(simp add:SUP_def image_constant_conv sup_absorb1)
   1.167 +lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
   1.168 +  by (auto intro: order_antisym INF_leI le_INFI)
   1.169  
   1.170  
   1.171  subsection {* Some instances of the type class of complete lattices *}
     2.1 --- a/src/HOL/Predicate.thy	Sat Mar 10 16:13:08 2007 +0100
     2.2 +++ b/src/HOL/Predicate.thy	Sat Mar 10 16:23:28 2007 +0100
     2.3 @@ -286,28 +286,61 @@
     2.4  subsubsection {* Unions of families *}
     2.5  
     2.6  lemma member_SUP: "(SUP i. member (r i)) = member (UN i. r i)"
     2.7 -  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
     2.8 +  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
     2.9  
    2.10  lemma member2_SUP: "(SUP i. member2 (r i)) = member2 (UN i. r i)"
    2.11 -  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
    2.12 +  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
    2.13  
    2.14 -lemma SUP1_iff [simp]: "((SUP x. B x) b) = (EX x. B x b)"
    2.15 -  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast
    2.16 +lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
    2.17 +  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
    2.18 +
    2.19 +lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
    2.20 +  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
    2.21  
    2.22 -lemma SUP2_iff [simp]: "((SUP x. B x) b c) = (EX x. B x b c)"
    2.23 -  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast
    2.24 +lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
    2.25 +  by auto
    2.26  
    2.27 -lemma SUP1_I [intro]: "B a b ==> (SUP x. B x) b"
    2.28 +lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
    2.29 +  by auto
    2.30 +
    2.31 +lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
    2.32 +  by auto
    2.33 +
    2.34 +lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
    2.35    by auto
    2.36  
    2.37 -lemma SUP2_I [intro]: "B a b c ==> (SUP x. B x) b c"
    2.38 +
    2.39 +subsubsection {* Intersections of families *}
    2.40 +
    2.41 +lemma member_INF: "(INF i. member (r i)) = member (INT i. r i)"
    2.42 +  by (simp add: INFI_def Inf_fun_def Inf_bool_def expand_fun_eq) blast
    2.43 +
    2.44 +lemma member2_INF: "(INF i. member2 (r i)) = member2 (INT i. r i)"
    2.45 +  by (simp add: INFI_def Inf_fun_def Inf_bool_def expand_fun_eq) blast
    2.46 +
    2.47 +lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)"
    2.48 +  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
    2.49 +
    2.50 +lemma INF2_iff [simp]: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
    2.51 +  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
    2.52 +
    2.53 +lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
    2.54    by auto
    2.55  
    2.56 -lemma SUP1_E [elim!]: "(SUP x. B x) b ==> (!!x. B x b ==> R) ==> R"
    2.57 -  by simp iprover
    2.58 +lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
    2.59 +  by auto
    2.60 +
    2.61 +lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
    2.62 +  by auto
    2.63  
    2.64 -lemma SUP2_E [elim!]: "(SUP x. B x) b c ==> (!!x. B x b c ==> R) ==> R"
    2.65 -  by simp iprover
    2.66 +lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
    2.67 +  by auto
    2.68 +
    2.69 +lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
    2.70 +  by auto
    2.71 +
    2.72 +lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
    2.73 +  by auto
    2.74  
    2.75  
    2.76  subsection {* Composition of two relations *}