be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
authorhaftmann
Fri Sep 18 09:07:48 2009 +0200 (2009-09-18)
changeset 3260147d0c967c64e
parent 32600 1b3b0cc604ce
child 32602 f2b741473860
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
src/HOL/Predicate.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Predicate.thy	Fri Sep 18 07:54:26 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Fri Sep 18 09:07:48 2009 +0200
     1.3 @@ -75,29 +75,29 @@
     1.4  
     1.5  subsubsection {* Binary union *}
     1.6  
     1.7 -lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x | B x"
     1.8 +lemma sup1_iff: "sup A B x \<longleftrightarrow> A x | B x"
     1.9    by (simp add: sup_fun_eq sup_bool_eq)
    1.10  
    1.11 -lemma sup2_iff [simp]: "sup A B x y \<longleftrightarrow> A x y | B x y"
    1.12 +lemma sup2_iff: "sup A B x y \<longleftrightarrow> A x y | B x y"
    1.13    by (simp add: sup_fun_eq sup_bool_eq)
    1.14  
    1.15  lemma sup_Un_eq [pred_set_conv]: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
    1.16 -  by (simp add: expand_fun_eq)
    1.17 +  by (simp add: sup1_iff expand_fun_eq)
    1.18  
    1.19  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.20 -  by (simp add: expand_fun_eq)
    1.21 +  by (simp add: sup2_iff expand_fun_eq)
    1.22  
    1.23  lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
    1.24 -  by simp
    1.25 +  by (simp add: sup1_iff)
    1.26  
    1.27  lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
    1.28 -  by simp
    1.29 +  by (simp add: sup2_iff)
    1.30  
    1.31  lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
    1.32 -  by simp
    1.33 +  by (simp add: sup1_iff)
    1.34  
    1.35  lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
    1.36 -  by simp
    1.37 +  by (simp add: sup2_iff)
    1.38  
    1.39  text {*
    1.40    \medskip Classical introduction rule: no commitment to @{text A} vs
    1.41 @@ -105,115 +105,115 @@
    1.42  *}
    1.43  
    1.44  lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
    1.45 -  by auto
    1.46 +  by (auto simp add: sup1_iff)
    1.47  
    1.48  lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
    1.49 -  by auto
    1.50 +  by (auto simp add: sup2_iff)
    1.51  
    1.52  lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
    1.53 -  by simp iprover
    1.54 +  by (simp add: sup1_iff) iprover
    1.55  
    1.56  lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
    1.57 -  by simp iprover
    1.58 +  by (simp add: sup2_iff) iprover
    1.59  
    1.60  
    1.61  subsubsection {* Binary intersection *}
    1.62  
    1.63 -lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x"
    1.64 +lemma inf1_iff: "inf A B x \<longleftrightarrow> A x \<and> B x"
    1.65    by (simp add: inf_fun_eq inf_bool_eq)
    1.66  
    1.67 -lemma inf2_iff [simp]: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
    1.68 +lemma inf2_iff: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
    1.69    by (simp add: inf_fun_eq inf_bool_eq)
    1.70  
    1.71  lemma inf_Int_eq [pred_set_conv]: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
    1.72 -  by (simp add: expand_fun_eq)
    1.73 +  by (simp add: inf1_iff expand_fun_eq)
    1.74  
    1.75  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.76 -  by (simp add: expand_fun_eq)
    1.77 +  by (simp add: inf2_iff expand_fun_eq)
    1.78  
    1.79  lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
    1.80 -  by simp
    1.81 +  by (simp add: inf1_iff)
    1.82  
    1.83  lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
    1.84 -  by simp
    1.85 +  by (simp add: inf2_iff)
    1.86  
    1.87  lemma inf1D1: "inf A B x ==> A x"
    1.88 -  by simp
    1.89 +  by (simp add: inf1_iff)
    1.90  
    1.91  lemma inf2D1: "inf A B x y ==> A x y"
    1.92 -  by simp
    1.93 +  by (simp add: inf2_iff)
    1.94  
    1.95  lemma inf1D2: "inf A B x ==> B x"
    1.96 -  by simp
    1.97 +  by (simp add: inf1_iff)
    1.98  
    1.99  lemma inf2D2: "inf A B x y ==> B x y"
   1.100 -  by simp
   1.101 +  by (simp add: inf2_iff)
   1.102  
   1.103  lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
   1.104 -  by simp
   1.105 +  by (simp add: inf1_iff)
   1.106  
   1.107  lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
   1.108 -  by simp
   1.109 +  by (simp add: inf2_iff)
   1.110  
   1.111  
   1.112  subsubsection {* Unions of families *}
   1.113  
   1.114 -lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
   1.115 +lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
   1.116    by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
   1.117  
   1.118 -lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
   1.119 +lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
   1.120    by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
   1.121  
   1.122  lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
   1.123 -  by auto
   1.124 +  by (auto simp add: SUP1_iff)
   1.125  
   1.126  lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
   1.127 -  by auto
   1.128 +  by (auto simp add: SUP2_iff)
   1.129  
   1.130  lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
   1.131 -  by auto
   1.132 +  by (auto simp add: SUP1_iff)
   1.133  
   1.134  lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
   1.135 -  by auto
   1.136 +  by (auto simp add: SUP2_iff)
   1.137  
   1.138  lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
   1.139 -  by (simp add: expand_fun_eq)
   1.140 +  by (simp add: SUP1_iff expand_fun_eq)
   1.141  
   1.142  lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
   1.143 -  by (simp add: expand_fun_eq)
   1.144 +  by (simp add: SUP2_iff expand_fun_eq)
   1.145  
   1.146  
   1.147  subsubsection {* Intersections of families *}
   1.148  
   1.149 -lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)"
   1.150 +lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
   1.151    by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
   1.152  
   1.153 -lemma INF2_iff [simp]: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
   1.154 +lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
   1.155    by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
   1.156  
   1.157  lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
   1.158 -  by auto
   1.159 +  by (auto simp add: INF1_iff)
   1.160  
   1.161  lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
   1.162 -  by auto
   1.163 +  by (auto simp add: INF2_iff)
   1.164  
   1.165  lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
   1.166 -  by auto
   1.167 +  by (auto simp add: INF1_iff)
   1.168  
   1.169  lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
   1.170 -  by auto
   1.171 +  by (auto simp add: INF2_iff)
   1.172  
   1.173  lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
   1.174 -  by auto
   1.175 +  by (auto simp add: INF1_iff)
   1.176  
   1.177  lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
   1.178 -  by auto
   1.179 +  by (auto simp add: INF2_iff)
   1.180  
   1.181  lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
   1.182 -  by (simp add: expand_fun_eq)
   1.183 +  by (simp add: INF1_iff expand_fun_eq)
   1.184  
   1.185  lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
   1.186 -  by (simp add: expand_fun_eq)
   1.187 +  by (simp add: INF2_iff expand_fun_eq)
   1.188  
   1.189  
   1.190  subsection {* Predicates as relations *}
   1.191 @@ -429,7 +429,7 @@
   1.192    by (auto simp add: bind_def sup_pred_def expand_fun_eq)
   1.193  
   1.194  lemma Sup_bind: "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
   1.195 -  by (auto simp add: bind_def Sup_pred_def expand_fun_eq)
   1.196 +  by (auto simp add: bind_def Sup_pred_def SUP1_iff expand_fun_eq)
   1.197  
   1.198  lemma pred_iffI:
   1.199    assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
   1.200 @@ -462,10 +462,10 @@
   1.201    unfolding bot_pred_def by auto
   1.202  
   1.203  lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x"
   1.204 -  unfolding sup_pred_def by simp
   1.205 +  unfolding sup_pred_def by (simp add: sup1_iff)
   1.206  
   1.207  lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" 
   1.208 -  unfolding sup_pred_def by simp
   1.209 +  unfolding sup_pred_def by (simp add: sup1_iff)
   1.210  
   1.211  lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P"
   1.212    unfolding sup_pred_def by auto
     2.1 --- a/src/HOL/Transitive_Closure.thy	Fri Sep 18 07:54:26 2009 +0200
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Sep 18 09:07:48 2009 +0200
     2.3 @@ -77,7 +77,7 @@
     2.4  subsection {* Reflexive-transitive closure *}
     2.5  
     2.6  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.7 -  by (simp add: expand_fun_eq)
     2.8 +  by (simp add: expand_fun_eq sup2_iff)
     2.9  
    2.10  lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
    2.11    -- {* @{text rtrancl} of @{text r} contains @{text r} *}