Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
authornoschinl
Mon, 12 Mar 2012 15:12:22 +0100
changeset 46883 eec472dae593
parent 46882 6242b4bc05bc
child 46884 154dc6ec0041
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
src/HOL/Relation.thy file | annotate | diff | comparison | revisions
src/HOL/Wellfounded.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Relation.thy	Mon Mar 12 15:11:24 2012 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 12 15:12:22 2012 +0100
@@ -71,17 +71,17 @@
 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"
   by (simp add: subset_iff le_fun_def)
 
-lemma bot_empty_eq (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x. x \<in> {})"
+lemma bot_empty_eq [pred_set_conv]: "\<bottom> = (\<lambda>x. x \<in> {})"
   by (auto simp add: fun_eq_iff)
 
-lemma bot_empty_eq2 (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
+lemma bot_empty_eq2 [pred_set_conv]: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
   by (auto simp add: fun_eq_iff)
 
-(* CANDIDATE lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)"
-  by (auto simp add: fun_eq_iff) *)
+lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)"
+  by (auto simp add: fun_eq_iff)
 
-(* CANDIDATE lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)"
-  by (auto simp add: fun_eq_iff) *)
+lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)"
+  by (auto simp add: fun_eq_iff)
 
 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)"
   by (simp add: inf_fun_def)
@@ -98,7 +98,6 @@
 lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
   by (simp add: fun_eq_iff Inf_apply)
 
-(* CANDIDATE
 lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
   by (simp add: fun_eq_iff INF_apply)
 
@@ -119,35 +118,19 @@
 
 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)"
   by (simp add: fun_eq_iff SUP_apply)
-*)
 
-(* CANDIDATE prefer those generalized versions:
-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))"
+lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
   by (simp add: INF_apply fun_eq_iff)
 
 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))"
   by (simp add: INF_apply fun_eq_iff)
-*)
 
-lemma INF_INT_eq (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
-  by (simp add: INF_apply fun_eq_iff)
-
-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))"
-  by (simp add: INF_apply fun_eq_iff)
-
-(* CANDIDATE prefer those generalized versions:
-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))"
+lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   by (simp add: SUP_apply fun_eq_iff)
 
 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))"
   by (simp add: SUP_apply fun_eq_iff)
-*)
 
-lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
-  by (simp add: SUP_apply fun_eq_iff)
-
-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))"
-  by (simp add: SUP_apply fun_eq_iff)
 
 
 subsection {* Properties of relations *}
@@ -557,22 +540,23 @@
   "{} O R = {}"
   by blast
 
-(* CANDIDATE lemma pred_comp_bot1 [simp]:
-  ""
-  by (fact rel_comp_empty1 [to_pred]) *)
+lemma prod_comp_bot1 [simp]:
+  "\<bottom> OO R = \<bottom>"
+  by (fact rel_comp_empty1 [to_pred])
 
 lemma rel_comp_empty2 [simp]:
   "R O {} = {}"
   by blast
 
-(* CANDIDATE lemma pred_comp_bot2 [simp]:
-  ""
-  by (fact rel_comp_empty2 [to_pred]) *)
+lemma pred_comp_bot2 [simp]:
+  "R OO \<bottom> = \<bottom>"
+  by (fact rel_comp_empty2 [to_pred])
 
 lemma O_assoc:
   "(R O S) O T = R O (S O T)"
   by blast
 
+
 lemma pred_comp_assoc:
   "(r OO s) OO t = r OO (s OO t)"
   by (fact O_assoc [to_pred])
--- a/src/HOL/Wellfounded.thy	Mon Mar 12 15:11:24 2012 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Mar 12 15:12:22 2012 +0100
@@ -298,7 +298,7 @@
 
 lemma wfP_SUP:
   "\<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)"
-  apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred])
+  apply (rule wf_UN[to_pred])
   apply simp_all
   done
isabelle