--- a/src/Doc/IsarRef/HOL_Specific.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy Tue Feb 18 23:03:49 2014 +0100
@@ -1761,7 +1761,7 @@
"~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
\item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
- that a relator respects reflexivity, left-totality and left_uniqueness. For examples
+ that a relator respects left-totality and left_uniqueness. For examples
see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
in the same directory.
The property is used in a reflexivity prover, which is used for discharging respectfulness
--- a/src/HOL/Library/Quotient_List.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/Library/Quotient_List.thy Tue Feb 18 23:03:49 2014 +0100
@@ -22,6 +22,16 @@
by (induct xs ys rule: list_induct2') simp_all
qed
+lemma reflp_list_all2:
+ assumes "reflp R"
+ shows "reflp (list_all2 R)"
+proof (rule reflpI)
+ from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
+ fix xs
+ show "list_all2 R xs xs"
+ by (induct xs) (simp_all add: *)
+qed
+
lemma list_symp:
assumes "symp R"
shows "symp (list_all2 R)"
--- a/src/HOL/Library/Quotient_Option.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/Library/Quotient_Option.thy Tue Feb 18 23:03:49 2014 +0100
@@ -22,6 +22,10 @@
map_option.id [id_simps]
rel_option_eq [id_simps]
+lemma reflp_rel_option:
+ "reflp R \<Longrightarrow> reflp (rel_option R)"
+ unfolding reflp_def split_option_all by simp
+
lemma option_symp:
"symp R \<Longrightarrow> symp (rel_option R)"
unfolding symp_def split_option_all
--- a/src/HOL/Library/Quotient_Sum.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy Tue Feb 18 23:03:49 2014 +0100
@@ -26,6 +26,10 @@
"sum_rel (op =) (op =) = (op =)"
by (simp add: sum_rel_def fun_eq_iff split: sum.split)
+lemma reflp_sum_rel:
+ "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
+ unfolding reflp_def split_sum_all sum_rel_simps by fast
+
lemma sum_symp:
"symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
unfolding symp_def split_sum_all sum_rel_simps by fast
--- a/src/HOL/Lifting_Option.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/Lifting_Option.thy Tue Feb 18 23:03:49 2014 +0100
@@ -39,10 +39,6 @@
using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
by (auto iff: fun_eq_iff split: option.split)
-lemma reflp_rel_option[reflexivity_rule]:
- "reflp R \<Longrightarrow> reflp (rel_option R)"
- unfolding reflp_def split_option_all by simp
-
lemma left_total_rel_option[reflexivity_rule]:
"left_total R \<Longrightarrow> left_total (rel_option R)"
unfolding left_total_def split_option_all split_option_ex by simp
--- a/src/HOL/Lifting_Product.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/Lifting_Product.thy Tue Feb 18 23:03:49 2014 +0100
@@ -30,12 +30,6 @@
shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
using assms unfolding prod_rel_def prod_pred_def by blast
-lemma reflp_prod_rel [reflexivity_rule]:
- assumes "reflp R1"
- assumes "reflp R2"
- shows "reflp (prod_rel R1 R2)"
-using assms by (auto intro!: reflpI elim: reflpE)
-
lemma left_total_prod_rel [reflexivity_rule]:
assumes "left_total R1"
assumes "left_total R2"
--- a/src/HOL/Lifting_Set.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/Lifting_Set.thy Tue Feb 18 23:03:49 2014 +0100
@@ -54,9 +54,6 @@
apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
done
-lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
- unfolding reflp_def set_rel_def by fast
-
lemma left_total_set_rel[reflexivity_rule]:
"left_total A \<Longrightarrow> left_total (set_rel A)"
unfolding left_total_def set_rel_def
--- a/src/HOL/Lifting_Sum.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/Lifting_Sum.thy Tue Feb 18 23:03:49 2014 +0100
@@ -26,10 +26,6 @@
using assms
by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
-lemma reflp_sum_rel[reflexivity_rule]:
- "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
- unfolding reflp_def split_sum_all sum_rel_simps by fast
-
lemma left_total_sum_rel[reflexivity_rule]:
"left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
using assms unfolding left_total_def split_sum_all split_sum_ex by simp
--- a/src/HOL/List.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/List.thy Tue Feb 18 23:03:49 2014 +0100
@@ -6582,16 +6582,6 @@
by (auto iff: fun_eq_iff)
qed
-lemma reflp_list_all2[reflexivity_rule]:
- assumes "reflp R"
- shows "reflp (list_all2 R)"
-proof (rule reflpI)
- from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
- fix xs
- show "list_all2 R xs xs"
- by (induct xs) (simp_all add: *)
-qed
-
lemma left_total_list_all2[reflexivity_rule]:
"left_total R \<Longrightarrow> left_total (list_all2 R)"
unfolding left_total_def
--- a/src/HOL/Topological_Spaces.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Tue Feb 18 23:03:49 2014 +0100
@@ -2375,10 +2375,6 @@
unfolding filter_rel_eventually[abs_def]
by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
-lemma reflp_filter_rel [reflexivity_rule]: "reflp R \<Longrightarrow> reflp (filter_rel R)"
-unfolding filter_rel_eventually[abs_def]
-by(blast intro!: reflpI eventually_subst always_eventually dest: fun_relD reflpD)
-
lemma filter_rel_conversep [simp]: "filter_rel A\<inverse>\<inverse> = (filter_rel A)\<inverse>\<inverse>"
by(auto simp add: filter_rel_eventually fun_eq_iff fun_rel_def)