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