tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
authornoschinl
Mon Mar 12 15:12:22 2012 +0100 (2012-03-12)
changeset 46883eec472dae593
parent 46882 6242b4bc05bc
child 46884 154dc6ec0041
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
src/HOL/Relation.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Relation.thy	Mon Mar 12 15:11:24 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Mon Mar 12 15:12:22 2012 +0100
     1.3 @@ -71,17 +71,17 @@
     1.4  lemma pred_subset_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S) \<longleftrightarrow> R \<subseteq> S"
     1.5    by (simp add: subset_iff le_fun_def)
     1.6  
     1.7 -lemma bot_empty_eq (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x. x \<in> {})"
     1.8 +lemma bot_empty_eq [pred_set_conv]: "\<bottom> = (\<lambda>x. x \<in> {})"
     1.9    by (auto simp add: fun_eq_iff)
    1.10  
    1.11 -lemma bot_empty_eq2 (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    1.12 +lemma bot_empty_eq2 [pred_set_conv]: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    1.13    by (auto simp add: fun_eq_iff)
    1.14  
    1.15 -(* CANDIDATE lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)"
    1.16 -  by (auto simp add: fun_eq_iff) *)
    1.17 +lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)"
    1.18 +  by (auto simp add: fun_eq_iff)
    1.19  
    1.20 -(* CANDIDATE lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)"
    1.21 -  by (auto simp add: fun_eq_iff) *)
    1.22 +lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)"
    1.23 +  by (auto simp add: fun_eq_iff)
    1.24  
    1.25  lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
    1.26    by (simp add: inf_fun_def)
    1.27 @@ -98,7 +98,6 @@
    1.28  lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
    1.29    by (simp add: fun_eq_iff Inf_apply)
    1.30  
    1.31 -(* CANDIDATE
    1.32  lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
    1.33    by (simp add: fun_eq_iff INF_apply)
    1.34  
    1.35 @@ -119,35 +118,19 @@
    1.36  
    1.37  lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
    1.38    by (simp add: fun_eq_iff SUP_apply)
    1.39 -*)
    1.40  
    1.41 -(* CANDIDATE prefer those generalized versions:
    1.42 -lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i\<in>S. r i))"
    1.43 +lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
    1.44    by (simp add: INF_apply fun_eq_iff)
    1.45  
    1.46  lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))"
    1.47    by (simp add: INF_apply fun_eq_iff)
    1.48 -*)
    1.49  
    1.50 -lemma INF_INT_eq (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
    1.51 -  by (simp add: INF_apply fun_eq_iff)
    1.52 -
    1.53 -lemma INF_INT_eq2 (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
    1.54 -  by (simp add: INF_apply fun_eq_iff)
    1.55 -
    1.56 -(* CANDIDATE prefer those generalized versions:
    1.57 -lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i\<in>S. r i))"
    1.58 +lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
    1.59    by (simp add: SUP_apply fun_eq_iff)
    1.60  
    1.61  lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
    1.62    by (simp add: SUP_apply fun_eq_iff)
    1.63 -*)
    1.64  
    1.65 -lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
    1.66 -  by (simp add: SUP_apply fun_eq_iff)
    1.67 -
    1.68 -lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
    1.69 -  by (simp add: SUP_apply fun_eq_iff)
    1.70  
    1.71  
    1.72  subsection {* Properties of relations *}
    1.73 @@ -557,22 +540,23 @@
    1.74    "{} O R = {}"
    1.75    by blast
    1.76  
    1.77 -(* CANDIDATE lemma pred_comp_bot1 [simp]:
    1.78 -  ""
    1.79 -  by (fact rel_comp_empty1 [to_pred]) *)
    1.80 +lemma prod_comp_bot1 [simp]:
    1.81 +  "\<bottom> OO R = \<bottom>"
    1.82 +  by (fact rel_comp_empty1 [to_pred])
    1.83  
    1.84  lemma rel_comp_empty2 [simp]:
    1.85    "R O {} = {}"
    1.86    by blast
    1.87  
    1.88 -(* CANDIDATE lemma pred_comp_bot2 [simp]:
    1.89 -  ""
    1.90 -  by (fact rel_comp_empty2 [to_pred]) *)
    1.91 +lemma pred_comp_bot2 [simp]:
    1.92 +  "R OO \<bottom> = \<bottom>"
    1.93 +  by (fact rel_comp_empty2 [to_pred])
    1.94  
    1.95  lemma O_assoc:
    1.96    "(R O S) O T = R O (S O T)"
    1.97    by blast
    1.98  
    1.99 +
   1.100  lemma pred_comp_assoc:
   1.101    "(r OO s) OO t = r OO (s OO t)"
   1.102    by (fact O_assoc [to_pred])
     2.1 --- a/src/HOL/Wellfounded.thy	Mon Mar 12 15:11:24 2012 +0100
     2.2 +++ b/src/HOL/Wellfounded.thy	Mon Mar 12 15:12:22 2012 +0100
     2.3 @@ -298,7 +298,7 @@
     2.4  
     2.5  lemma wfP_SUP:
     2.6    "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
     2.7 -  apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred])
     2.8 +  apply (rule wf_UN[to_pred])
     2.9    apply simp_all
    2.10    done
    2.11