--- a/src/HOL/Predicate.thy Wed Dec 08 14:52:23 2010 +0100
+++ b/src/HOL/Predicate.thy Wed Dec 08 15:05:46 2010 +0100
@@ -9,18 +9,18 @@
begin
notation
+ bot ("\<bottom>") and
+ top ("\<top>") and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
Inf ("\<Sqinter>_" [900] 900) and
- Sup ("\<Squnion>_" [900] 900) and
- top ("\<top>") and
- bot ("\<bottom>")
+ Sup ("\<Squnion>_" [900] 900)
syntax (xsymbols)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
subsection {* Predicates as (complete) lattices *}
@@ -92,12 +92,6 @@
subsubsection {* Top and bottom elements *}
-lemma top1I [intro!]: "top x"
- by (simp add: top_fun_def top_bool_def)
-
-lemma top2I [intro!]: "top x y"
- by (simp add: top_fun_def top_bool_def)
-
lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
by (simp add: bot_fun_def bot_bool_def)
@@ -110,6 +104,45 @@
lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
by (auto simp add: fun_eq_iff)
+lemma top1I [intro!]: "top x"
+ by (simp add: top_fun_def top_bool_def)
+
+lemma top2I [intro!]: "top x y"
+ by (simp add: top_fun_def top_bool_def)
+
+
+subsubsection {* Binary intersection *}
+
+lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf1D1: "inf A B x ==> A x"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf2D1: "inf A B x y ==> A x y"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf1D2: "inf A B x ==> B x"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf2D2: "inf A B x y ==> B x y"
+ by (simp add: inf_fun_def inf_bool_def)
+
+lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
+ by (simp add: inf_fun_def inf_bool_def mem_def)
+
+lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
+ by (simp add: inf_fun_def inf_bool_def mem_def)
+
subsubsection {* Binary union *}
@@ -149,66 +182,6 @@
by (simp add: sup_fun_def sup_bool_def mem_def)
-subsubsection {* Binary intersection *}
-
-lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
- by (simp add: inf_fun_def inf_bool_def)
-
-lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
- by (simp add: inf_fun_def inf_bool_def)
-
-lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
- by (simp add: inf_fun_def inf_bool_def)
-
-lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
- by (simp add: inf_fun_def inf_bool_def)
-
-lemma inf1D1: "inf A B x ==> A x"
- by (simp add: inf_fun_def inf_bool_def)
-
-lemma inf2D1: "inf A B x y ==> A x y"
- by (simp add: inf_fun_def inf_bool_def)
-
-lemma inf1D2: "inf A B x ==> B x"
- by (simp add: inf_fun_def inf_bool_def)
-
-lemma inf2D2: "inf A B x y ==> B x y"
- by (simp add: inf_fun_def inf_bool_def)
-
-lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
- by (simp add: inf_fun_def inf_bool_def mem_def)
-
-lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
- by (simp add: inf_fun_def inf_bool_def mem_def)
-
-
-subsubsection {* Unions of families *}
-
-lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
- by (simp add: SUPR_apply)
-
-lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
- by (simp add: SUPR_apply)
-
-lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
- by (auto simp add: SUPR_apply)
-
-lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
- by (auto simp add: SUPR_apply)
-
-lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
- by (auto simp add: SUPR_apply)
-
-lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
- by (auto simp add: SUPR_apply)
-
-lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
- by (simp add: SUPR_apply fun_eq_iff)
-
-lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
- by (simp add: SUPR_apply fun_eq_iff)
-
-
subsubsection {* Intersections of families *}
lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
@@ -242,6 +215,33 @@
by (simp add: INFI_apply fun_eq_iff)
+subsubsection {* Unions of families *}
+
+lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
+ by (simp add: SUPR_apply)
+
+lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
+ by (simp add: SUPR_apply)
+
+lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
+ by (auto simp add: SUPR_apply)
+
+lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
+ by (auto simp add: SUPR_apply)
+
+lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
+ by (auto simp add: SUPR_apply)
+
+lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
+ by (auto simp add: SUPR_apply)
+
+lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
+ by (simp add: SUPR_apply fun_eq_iff)
+
+lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
+ by (simp add: SUPR_apply fun_eq_iff)
+
+
subsection {* Predicates as relations *}
subsubsection {* Composition *}
@@ -1027,19 +1027,19 @@
*}
no_notation
+ bot ("\<bottom>") and
+ top ("\<top>") and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
Inf ("\<Sqinter>_" [900] 900) and
Sup ("\<Squnion>_" [900] 900) and
- top ("\<top>") and
- bot ("\<bottom>") and
bind (infixl "\<guillemotright>=" 70)
no_syntax (xsymbols)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
hide_type (open) pred seq
hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds