# HG changeset patch # User berghofe # Date 1173540208 -3600 # Node ID 6a56bf1b3a64997fa8d2f2eca9a854a294789ab5 # Parent 09e794384323cacf3cd7eaba07721e57a4ce62cc Generalized version of SUP and INF (with index set). diff -r 09e794384323 -r 6a56bf1b3a64 src/HOL/FixedPoint.thy --- a/src/HOL/FixedPoint.thy Sat Mar 10 16:13:08 2007 +0100 +++ b/src/HOL/FixedPoint.thy Sat Mar 10 16:23:28 2007 +0100 @@ -20,15 +20,6 @@ Sup :: "'a::order set \ 'a" where "Sup A = Inf {b. \a \ A. a \ b}" -definition - SUP :: "('a \ 'b::order) \ 'b" (binder "SUP " 10) where - "(SUP x. f x) = Sup (f ` UNIV)" - -(* -abbreviation - bot :: "'a::order" where - "bot == Sup {}" -*) class comp_lat = order + assumes Inf_lower: "x \ A \ Inf A \ x" assumes Inf_greatest: "(\x. x \ A \ z \ x) \ z \ Inf A" @@ -39,6 +30,54 @@ theorem Sup_least: "(\x::'a::comp_lat. x \ A \ x <= z) \ Sup A <= z" by (auto simp: Sup_def intro: Inf_lower) +definition + SUPR :: "'a set \ ('a \ 'b::comp_lat) \ 'b" where + "SUPR A f == Sup (f ` A)" + +definition + INFI :: "'a set \ ('a \ 'b::comp_lat) \ 'b" where + "INFI A f == Inf (f ` A)" + +syntax + "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" 10) + "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" 10) + "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" 10) + "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" 10) + +translations + "SUP x y. B" == "SUP x. SUP y. B" + "SUP x. B" == "CONST SUPR UNIV (%x. B)" + "SUP x. B" == "SUP x:UNIV. B" + "SUP x:A. B" == "CONST SUPR A (%x. B)" + "INF x y. B" == "INF x. INF y. B" + "INF x. B" == "CONST INFI UNIV (%x. B)" + "INF x. B" == "INF x:UNIV. B" + "INF x:A. B" == "CONST INFI A (%x. B)" + +(* To avoid eta-contraction of body: *) +print_translation {* +let + fun btr' syn (A :: Abs abs :: ts) = + let val (x,t) = atomic_abs_tr' abs + in list_comb (Syntax.const syn $ x $ A $ t, ts) end + val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const +in +[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")] +end +*} + +lemma le_SUPI: "i : A \ M i \ (SUP i:A. M i)" + by (auto simp add: SUPR_def intro: Sup_upper) + +lemma SUP_leI: "(\i. i : A \ M i \ u) \ (SUP i:A. M i) \ u" + by (auto simp add: SUPR_def intro: Sup_least) + +lemma INF_leI: "i : A \ (INF i:A. M i) \ M i" + by (auto simp add: INFI_def intro: Inf_lower) + +lemma le_INFI: "(\i. i : A \ u \ M i) \ u \ (INF i:A. M i)" + by (auto simp add: INFI_def intro: Inf_greatest) + text {* A complete lattice is a lattice *} lemma is_meet_Inf: "is_meet (\(x::'a::comp_lat) y. Inf {x, y})" @@ -62,59 +101,48 @@ by (auto simp add: mono_def) lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = sup a (Sup A)" -apply(simp add:Sup_def) -apply(rule order_antisym) - apply(rule Inf_lower) - apply(clarsimp) - apply(rule le_supI2) - apply(rule Inf_greatest) - apply blast -apply simp -apply rule - apply(rule Inf_greatest)apply blast -apply(rule Inf_greatest) -apply(rule Inf_lower) -apply blast -done + apply (rule order_antisym) + apply (rule Sup_least) + apply (erule insertE) + apply (rule le_supI1) + apply simp + apply (rule le_supI2) + apply (erule Sup_upper) + apply (rule le_supI) + apply (rule Sup_upper) + apply simp + apply (rule Sup_least) + apply (rule Sup_upper) + apply simp + done + +lemma Inf_insert[simp]: "Inf (insert (a::'a::comp_lat) A) = inf a (Inf A)" + apply (rule order_antisym) + apply (rule le_infI) + apply (rule Inf_lower) + apply simp + apply (rule Inf_greatest) + apply (rule Inf_lower) + apply simp + apply (rule Inf_greatest) + apply (erule insertE) + apply (rule le_infI1) + apply simp + apply (rule le_infI2) + apply (erule Inf_lower) + done lemma bot_least[simp]: "Sup{} \ (x::'a::comp_lat)" -apply(simp add: Sup_def) -apply(rule Inf_lower) -apply blast -done -(* -lemma Inf_singleton[simp]: "Inf{a} = (a::'a::comp_lat)" -apply(rule order_antisym) - apply(simp add: Inf_lower) -apply(rule Inf_greatest) -apply(simp) -done -*) -lemma le_SupI: "(l::'a::comp_lat) : M \ l \ Sup M" -apply(simp add:Sup_def) -apply(rule Inf_greatest) -apply(simp) -done + by (rule Sup_least) simp + +lemma top_greatest[simp]: "(x::'a::comp_lat) \ Inf{}" + by (rule Inf_greatest) simp -lemma le_SUPI: "(l::'a::comp_lat) = M i \ l \ (SUP i. M i)" -apply(simp add:SUP_def) -apply(blast intro:le_SupI) -done +lemma SUP_const[simp]: "A \ {} \ (SUP i:A. M) = M" + by (auto intro: order_antisym SUP_leI le_SUPI) -lemma Sup_leI: "(!!x. x:M \ x \ u) \ Sup M \ (u::'a::comp_lat)" -apply(simp add:Sup_def) -apply(rule Inf_lower) -apply(blast) -done - - -lemma SUP_leI: "(!!i. M i \ u) \ (SUP i. M i) \ (u::'a::comp_lat)" -apply(simp add:SUP_def) -apply(blast intro!:Sup_leI) -done - -lemma SUP_const[simp]: "(SUP i. M) = (M::'a::comp_lat)" -by(simp add:SUP_def image_constant_conv sup_absorb1) +lemma INF_const[simp]: "A \ {} \ (INF i:A. M) = M" + by (auto intro: order_antisym INF_leI le_INFI) subsection {* Some instances of the type class of complete lattices *} diff -r 09e794384323 -r 6a56bf1b3a64 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Sat Mar 10 16:13:08 2007 +0100 +++ b/src/HOL/Predicate.thy Sat Mar 10 16:23:28 2007 +0100 @@ -286,28 +286,61 @@ subsubsection {* Unions of families *} lemma member_SUP: "(SUP i. member (r i)) = member (UN i. r i)" - by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast + by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast lemma member2_SUP: "(SUP i. member2 (r i)) = member2 (UN i. r i)" - by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast + by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast -lemma SUP1_iff [simp]: "((SUP x. B x) b) = (EX x. B x b)" - by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast +lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)" + by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast + +lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)" + by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast -lemma SUP2_iff [simp]: "((SUP x. B x) b c) = (EX x. B x b c)" - by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast +lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b" + by auto -lemma SUP1_I [intro]: "B a b ==> (SUP x. B x) b" +lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c" + by auto + +lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R" + by auto + +lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R" by auto -lemma SUP2_I [intro]: "B a b c ==> (SUP x. B x) b c" + +subsubsection {* Intersections of families *} + +lemma member_INF: "(INF i. member (r i)) = member (INT i. r i)" + by (simp add: INFI_def Inf_fun_def Inf_bool_def expand_fun_eq) blast + +lemma member2_INF: "(INF i. member2 (r i)) = member2 (INT i. r i)" + by (simp add: INFI_def Inf_fun_def Inf_bool_def expand_fun_eq) blast + +lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)" + by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast + +lemma INF2_iff [simp]: "(INF x:A. B x) b c = (ALL x:A. B x b c)" + by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast + +lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b" by auto -lemma SUP1_E [elim!]: "(SUP x. B x) b ==> (!!x. B x b ==> R) ==> R" - by simp iprover +lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c" + by auto + +lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b" + by auto -lemma SUP2_E [elim!]: "(SUP x. B x) b c ==> (!!x. B x b c ==> R) ==> R" - by simp iprover +lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c" + by auto + +lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R" + by auto + +lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R" + by auto subsection {* Composition of two relations *}