1.1 --- a/src/HOL/Predicate.thy	Tue Oct 06 15:51:34 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Tue Oct 06 18:44:06 2009 +0200
     1.3 @@ -60,29 +60,23 @@
     1.4  
     1.5  subsubsection {* Binary union *}
     1.6  
     1.7 -lemma sup1_iff: "sup A B x \<longleftrightarrow> A x | B x"
     1.8 +lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
     1.9    by (simp add: sup_fun_eq sup_bool_eq)
    1.10  
    1.11 -lemma sup2_iff: "sup A B x y \<longleftrightarrow> A x y | B x y"
    1.12 +lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
    1.13    by (simp add: sup_fun_eq sup_bool_eq)
    1.14  
    1.15 -lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
    1.16 -  by (simp add: sup1_iff expand_fun_eq)
    1.17 -
    1.18 -lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
    1.19 -  by (simp add: sup2_iff expand_fun_eq)
    1.20 -
    1.21 -lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
    1.22 -  by (simp add: sup1_iff)
    1.23 -
    1.24 -lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
    1.25 -  by (simp add: sup2_iff)
    1.26 -
    1.27  lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
    1.28 -  by (simp add: sup1_iff)
    1.29 +  by (simp add: sup_fun_eq sup_bool_eq)
    1.30  
    1.31  lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
    1.32 -  by (simp add: sup2_iff)
    1.33 +  by (simp add: sup_fun_eq sup_bool_eq)
    1.34 +
    1.35 +lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
    1.36 +  by (simp add: sup_fun_eq sup_bool_eq) iprover
    1.37 +
    1.38 +lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
    1.39 +  by (simp add: sup_fun_eq sup_bool_eq) iprover
    1.40  
    1.41  text {*
    1.42    \medskip Classical introduction rule: no commitment to @{text A} vs
    1.43 @@ -90,55 +84,49 @@
    1.44  *}
    1.45  
    1.46  lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
    1.47 -  by (auto simp add: sup1_iff)
    1.48 +  by (auto simp add: sup_fun_eq sup_bool_eq)
    1.49  
    1.50  lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
    1.51 -  by (auto simp add: sup2_iff)
    1.52 +  by (auto simp add: sup_fun_eq sup_bool_eq)
    1.53  
    1.54 -lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
    1.55 -  by (simp add: sup1_iff) iprover
    1.56 +lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
    1.57 +  by (simp add: sup_fun_eq sup_bool_eq mem_def)
    1.58  
    1.59 -lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
    1.60 -  by (simp add: sup2_iff) iprover
    1.61 +lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
    1.62 +  by (simp add: sup_fun_eq sup_bool_eq mem_def)
    1.63  
    1.64  
    1.65  subsubsection {* Binary intersection *}
    1.66  
    1.67 -lemma inf1_iff: "inf A B x \<longleftrightarrow> A x \<and> B x"
    1.68 +lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
    1.69    by (simp add: inf_fun_eq inf_bool_eq)
    1.70  
    1.71 -lemma inf2_iff: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
    1.72 +lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
    1.73 +  by (simp add: inf_fun_eq inf_bool_eq)
    1.74 +
    1.75 +lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
    1.76 +  by (simp add: inf_fun_eq inf_bool_eq)
    1.77 +
    1.78 +lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
    1.79 +  by (simp add: inf_fun_eq inf_bool_eq)
    1.80 +
    1.81 +lemma inf1D1: "inf A B x ==> A x"
    1.82 +  by (simp add: inf_fun_eq inf_bool_eq)
    1.83 +
    1.84 +lemma inf2D1: "inf A B x y ==> A x y"
    1.85 +  by (simp add: inf_fun_eq inf_bool_eq)
    1.86 +
    1.87 +lemma inf1D2: "inf A B x ==> B x"
    1.88 +  by (simp add: inf_fun_eq inf_bool_eq)
    1.89 +
    1.90 +lemma inf2D2: "inf A B x y ==> B x y"
    1.91    by (simp add: inf_fun_eq inf_bool_eq)
    1.92  
    1.93  lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
    1.94 -  by (simp add: inf1_iff expand_fun_eq)
    1.95 +  by (simp add: inf_fun_eq inf_bool_eq mem_def)
    1.96  
    1.97  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)"
    1.98 -  by (simp add: inf2_iff expand_fun_eq)
    1.99 -
   1.100 -lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
   1.101 -  by (simp add: inf1_iff)
   1.102 -
   1.103 -lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
   1.104 -  by (simp add: inf2_iff)
   1.105 -
   1.106 -lemma inf1D1: "inf A B x ==> A x"
   1.107 -  by (simp add: inf1_iff)
   1.108 -
   1.109 -lemma inf2D1: "inf A B x y ==> A x y"
   1.110 -  by (simp add: inf2_iff)
   1.111 -
   1.112 -lemma inf1D2: "inf A B x ==> B x"
   1.113 -  by (simp add: inf1_iff)
   1.114 -
   1.115 -lemma inf2D2: "inf A B x y ==> B x y"
   1.116 -  by (simp add: inf2_iff)
   1.117 -
   1.118 -lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
   1.119 -  by (simp add: inf1_iff)
   1.120 -
   1.121 -lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
   1.122 -  by (simp add: inf2_iff)
   1.123 +  by (simp add: inf_fun_eq inf_bool_eq mem_def)
   1.124  
   1.125  
   1.126  subsubsection {* Unions of families *}
   1.127 @@ -447,10 +435,10 @@
   1.128    unfolding bot_pred_def by auto
   1.129  
   1.130  lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x"
   1.131 -  unfolding sup_pred_def by (simp add: sup1_iff)
   1.132 +  unfolding sup_pred_def by (simp add: sup_fun_eq sup_bool_eq)
   1.133  
   1.134  lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" 
   1.135 -  unfolding sup_pred_def by (simp add: sup1_iff)
   1.136 +  unfolding sup_pred_def by (simp add: sup_fun_eq sup_bool_eq)
   1.137  
   1.138  lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
   1.139    unfolding sup_pred_def by auto

     2.1 --- a/src/HOL/Transitive_Closure.thy	Tue Oct 06 15:51:34 2009 +0200
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Oct 06 18:44:06 2009 +0200
     2.3 @@ -76,8 +76,8 @@
     2.4  
     2.5  subsection {* Reflexive-transitive closure *}
     2.6  
     2.7 -lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r Un Id)"
     2.8 -  by (simp add: expand_fun_eq sup2_iff)
     2.9 +lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"
    2.10 +  by (simp add: mem_def pair_in_Id_conv [simplified mem_def] sup_fun_eq sup_bool_eq)
    2.11  
    2.12  lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
    2.13    -- {* @{text rtrancl} of @{text r} contains @{text r} *}