1.1 --- a/src/HOL/Predicate.thy	Tue Mar 06 16:40:32 2007 +0100
     1.2 +++ b/src/HOL/Predicate.thy	Fri Mar 09 08:45:50 2007 +0100
     1.3 @@ -202,28 +202,28 @@
     1.4  
     1.5  subsubsection {* Binary union *}
     1.6  
     1.7 -lemma member_Un [pred_set_conv]: "join (member R) (member S) = member (R Un S)"
     1.8 -  by (simp add: expand_fun_eq join_fun_eq join_bool_eq)
     1.9 +lemma member_Un [pred_set_conv]: "sup (member R) (member S) = member (R Un S)"
    1.10 +  by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq)
    1.11  
    1.12 -lemma member2_Un [pred_set_conv]: "join (member2 R) (member2 S) = member2 (R Un S)"
    1.13 -  by (simp add: expand_fun_eq join_fun_eq join_bool_eq)
    1.14 +lemma member2_Un [pred_set_conv]: "sup (member2 R) (member2 S) = member2 (R Un S)"
    1.15 +  by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq)
    1.16  
    1.17 -lemma join1_iff [simp]: "(join A B x) = (A x | B x)"
    1.18 -  by (simp add: join_fun_eq join_bool_eq)
    1.19 +lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x | B x"
    1.20 +  by (simp add: sup_fun_eq sup_bool_eq)
    1.21  
    1.22 -lemma join2_iff [simp]: "(join A B x y) = (A x y | B x y)"
    1.23 -  by (simp add: join_fun_eq join_bool_eq)
    1.24 +lemma sup2_iff [simp]: "sup A B x y \<longleftrightarrow> A x y | B x y"
    1.25 +  by (simp add: sup_fun_eq sup_bool_eq)
    1.26  
    1.27 -lemma join1I1 [elim?]: "A x ==> join A B x"
    1.28 +lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
    1.29    by simp
    1.30  
    1.31 -lemma join2I1 [elim?]: "A x y ==> join A B x y"
    1.32 +lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
    1.33    by simp
    1.34  
    1.35 -lemma join1I2 [elim?]: "B x ==> join A B x"
    1.36 +lemma join1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
    1.37    by simp
    1.38  
    1.39 -lemma join2I2 [elim?]: "B x y ==> join A B x y"
    1.40 +lemma sup1I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
    1.41    by simp
    1.42  
    1.43  text {*
    1.44 @@ -231,55 +231,55 @@
    1.45    @{text B}.
    1.46  *}
    1.47  
    1.48 -lemma join1CI [intro!]: "(~ B x ==> A x) ==> join A B x"
    1.49 +lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
    1.50    by auto
    1.51  
    1.52 -lemma join2CI [intro!]: "(~ B x y ==> A x y) ==> join A B x y"
    1.53 +lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
    1.54    by auto
    1.55  
    1.56 -lemma join1E [elim!]: "join A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
    1.57 +lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
    1.58    by simp iprover
    1.59  
    1.60 -lemma join2E [elim!]: "join A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
    1.61 +lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
    1.62    by simp iprover
    1.63  
    1.64  
    1.65  subsubsection {* Binary intersection *}
    1.66  
    1.67 -lemma member_Int [pred_set_conv]: "meet (member R) (member S) = member (R Int S)"
    1.68 -  by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq)
    1.69 +lemma member_Int [pred_set_conv]: "inf (member R) (member S) = member (R Int S)"
    1.70 +  by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq)
    1.71  
    1.72 -lemma member2_Int [pred_set_conv]: "meet (member2 R) (member2 S) = member2 (R Int S)"
    1.73 -  by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq)
    1.74 +lemma member2_Int [pred_set_conv]: "inf (member2 R) (member2 S) = member2 (R Int S)"
    1.75 +  by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq)
    1.76  
    1.77 -lemma meet1_iff [simp]: "(meet A B x) = (A x & B x)"
    1.78 -  by (simp add: meet_fun_eq meet_bool_eq)
    1.79 +lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x"
    1.80 +  by (simp add: inf_fun_eq inf_bool_eq)
    1.81  
    1.82 -lemma meet2_iff [simp]: "(meet A B x y) = (A x y & B x y)"
    1.83 -  by (simp add: meet_fun_eq meet_bool_eq)
    1.84 +lemma inf2_iff [simp]: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
    1.85 +  by (simp add: inf_fun_eq inf_bool_eq)
    1.86  
    1.87 -lemma meet1I [intro!]: "A x ==> B x ==> meet A B x"
    1.88 +lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
    1.89    by simp
    1.90  
    1.91 -lemma meet2I [intro!]: "A x y ==> B x y ==> meet A B x y"
    1.92 +lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
    1.93    by simp
    1.94  
    1.95 -lemma meet1D1: "meet A B x ==> A x"
    1.96 +lemma inf1D1: "inf A B x ==> A x"
    1.97    by simp
    1.98  
    1.99 -lemma meet2D1: "meet A B x y ==> A x y"
   1.100 +lemma inf2D1: "inf A B x y ==> A x y"
   1.101    by simp
   1.102  
   1.103 -lemma meet1D2: "meet A B x ==> B x"
   1.104 +lemma inf1D2: "inf A B x ==> B x"
   1.105    by simp
   1.106  
   1.107 -lemma meet2D2: "meet A B x y ==> B x y"
   1.108 +lemma inf2D2: "inf A B x y ==> B x y"
   1.109    by simp
   1.110  
   1.111 -lemma meet1E [elim!]: "meet A B x ==> (A x ==> B x ==> P) ==> P"
   1.112 +lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
   1.113    by simp
   1.114  
   1.115 -lemma meet2E [elim!]: "meet A B x y ==> (A x y ==> B x y ==> P) ==> P"
   1.116 +lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
   1.117    by simp
   1.118  
   1.119  
   1.120 @@ -357,12 +357,12 @@
   1.121    by (iprover intro: order_antisym conversepI pred_compI
   1.122      elim: pred_compE dest: conversepD)
   1.123  
   1.124 -lemma converse_meet: "(meet r s)^--1 = meet r^--1 s^--1"
   1.125 -  by (simp add: meet_fun_eq meet_bool_eq)
   1.126 +lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
   1.127 +  by (simp add: inf_fun_eq inf_bool_eq)
   1.128      (iprover intro: conversepI ext dest: conversepD)
   1.129  
   1.130 -lemma converse_join: "(join r s)^--1 = join r^--1 s^--1"
   1.131 -  by (simp add: join_fun_eq join_bool_eq)
   1.132 +lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
   1.133 +  by (simp add: sup_fun_eq sup_bool_eq)
   1.134      (iprover intro: conversepI ext dest: conversepD)
   1.135  
   1.136  lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="