# HG changeset patch # User kuncar # Date 1392761029 -3600 # Node ID e81ee43ab2901e081b944ed7774f7e188a2f841a # Parent a64d49f49ca394a9f884a35c01579bc58cf1a2d0 delete or move now not necessary reflexivity rules due to 1726f46d2aa8 diff -r a64d49f49ca3 -r e81ee43ab290 src/Doc/IsarRef/HOL_Specific.thy --- 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 diff -r a64d49f49ca3 -r e81ee43ab290 src/HOL/Library/Quotient_List.thy --- 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 *: "\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)" diff -r a64d49f49ca3 -r e81ee43ab290 src/HOL/Library/Quotient_Option.thy --- 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 \ reflp (rel_option R)" + unfolding reflp_def split_option_all by simp + lemma option_symp: "symp R \ symp (rel_option R)" unfolding symp_def split_option_all diff -r a64d49f49ca3 -r e81ee43ab290 src/HOL/Library/Quotient_Sum.thy --- 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 \ reflp R2 \ reflp (sum_rel R1 R2)" + unfolding reflp_def split_sum_all sum_rel_simps by fast + lemma sum_symp: "symp R1 \ symp R2 \ symp (sum_rel R1 R2)" unfolding symp_def split_sum_all sum_rel_simps by fast diff -r a64d49f49ca3 -r e81ee43ab290 src/HOL/Lifting_Option.thy --- 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 \ reflp (rel_option R)" - unfolding reflp_def split_option_all by simp - lemma left_total_rel_option[reflexivity_rule]: "left_total R \ left_total (rel_option R)" unfolding left_total_def split_option_all split_option_ex by simp diff -r a64d49f49ca3 -r e81ee43ab290 src/HOL/Lifting_Product.thy --- 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" diff -r a64d49f49ca3 -r e81ee43ab290 src/HOL/Lifting_Set.thy --- 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. \x\A. T x y}" in exI, fast) done -lemma reflp_set_rel[reflexivity_rule]: "reflp R \ reflp (set_rel R)" - unfolding reflp_def set_rel_def by fast - lemma left_total_set_rel[reflexivity_rule]: "left_total A \ left_total (set_rel A)" unfolding left_total_def set_rel_def diff -r a64d49f49ca3 -r e81ee43ab290 src/HOL/Lifting_Sum.thy --- 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 \ reflp R2 \ 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 \ left_total R2 \ left_total (sum_rel R1 R2)" using assms unfolding left_total_def split_sum_all split_sum_ex by simp diff -r a64d49f49ca3 -r e81ee43ab290 src/HOL/List.thy --- 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 *: "\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 \ left_total (list_all2 R)" unfolding left_total_def diff -r a64d49f49ca3 -r e81ee43ab290 src/HOL/Topological_Spaces.thy --- 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 \ 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\\ = (filter_rel A)\\" by(auto simp add: filter_rel_eventually fun_eq_iff fun_rel_def)