delete or move now not necessary reflexivity rules due to 1726f46d2aa8
authorkuncar
Tue Feb 18 23:03:49 2014 +0100 (2014-02-18)
changeset 55564e81ee43ab290
parent 55563 a64d49f49ca3
child 55565 f663fc1e653b
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
src/Doc/IsarRef/HOL_Specific.thy
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Lifting_Option.thy
src/HOL/Lifting_Product.thy
src/HOL/Lifting_Set.thy
src/HOL/Lifting_Sum.thy
src/HOL/List.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Tue Feb 18 23:03:47 2014 +0100
     1.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Tue Feb 18 23:03:49 2014 +0100
     1.3 @@ -1761,7 +1761,7 @@
     1.4      "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
     1.5  
     1.6    \item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
     1.7 -    that a relator respects reflexivity, left-totality and left_uniqueness. For examples 
     1.8 +    that a relator respects left-totality and left_uniqueness. For examples 
     1.9      see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files 
    1.10      in the same directory.
    1.11      The property is used in a reflexivity prover, which is used for discharging respectfulness
     2.1 --- a/src/HOL/Library/Quotient_List.thy	Tue Feb 18 23:03:47 2014 +0100
     2.2 +++ b/src/HOL/Library/Quotient_List.thy	Tue Feb 18 23:03:49 2014 +0100
     2.3 @@ -22,6 +22,16 @@
     2.4      by (induct xs ys rule: list_induct2') simp_all
     2.5  qed
     2.6  
     2.7 +lemma reflp_list_all2:
     2.8 +  assumes "reflp R"
     2.9 +  shows "reflp (list_all2 R)"
    2.10 +proof (rule reflpI)
    2.11 +  from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
    2.12 +  fix xs
    2.13 +  show "list_all2 R xs xs"
    2.14 +    by (induct xs) (simp_all add: *)
    2.15 +qed
    2.16 +
    2.17  lemma list_symp:
    2.18    assumes "symp R"
    2.19    shows "symp (list_all2 R)"
     3.1 --- a/src/HOL/Library/Quotient_Option.thy	Tue Feb 18 23:03:47 2014 +0100
     3.2 +++ b/src/HOL/Library/Quotient_Option.thy	Tue Feb 18 23:03:49 2014 +0100
     3.3 @@ -22,6 +22,10 @@
     3.4    map_option.id [id_simps]
     3.5    rel_option_eq [id_simps]
     3.6  
     3.7 +lemma reflp_rel_option:
     3.8 +  "reflp R \<Longrightarrow> reflp (rel_option R)"
     3.9 +  unfolding reflp_def split_option_all by simp
    3.10 +
    3.11  lemma option_symp:
    3.12    "symp R \<Longrightarrow> symp (rel_option R)"
    3.13    unfolding symp_def split_option_all
     4.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue Feb 18 23:03:47 2014 +0100
     4.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Feb 18 23:03:49 2014 +0100
     4.3 @@ -26,6 +26,10 @@
     4.4    "sum_rel (op =) (op =) = (op =)"
     4.5    by (simp add: sum_rel_def fun_eq_iff split: sum.split)
     4.6  
     4.7 +lemma reflp_sum_rel:
     4.8 +  "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
     4.9 +  unfolding reflp_def split_sum_all sum_rel_simps by fast
    4.10 +
    4.11  lemma sum_symp:
    4.12    "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    4.13    unfolding symp_def split_sum_all sum_rel_simps by fast
     5.1 --- a/src/HOL/Lifting_Option.thy	Tue Feb 18 23:03:47 2014 +0100
     5.2 +++ b/src/HOL/Lifting_Option.thy	Tue Feb 18 23:03:49 2014 +0100
     5.3 @@ -39,10 +39,6 @@
     5.4  using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
     5.5  by (auto iff: fun_eq_iff split: option.split)
     5.6  
     5.7 -lemma reflp_rel_option[reflexivity_rule]:
     5.8 -  "reflp R \<Longrightarrow> reflp (rel_option R)"
     5.9 -  unfolding reflp_def split_option_all by simp
    5.10 -
    5.11  lemma left_total_rel_option[reflexivity_rule]:
    5.12    "left_total R \<Longrightarrow> left_total (rel_option R)"
    5.13    unfolding left_total_def split_option_all split_option_ex by simp
     6.1 --- a/src/HOL/Lifting_Product.thy	Tue Feb 18 23:03:47 2014 +0100
     6.2 +++ b/src/HOL/Lifting_Product.thy	Tue Feb 18 23:03:49 2014 +0100
     6.3 @@ -30,12 +30,6 @@
     6.4    shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
     6.5  using assms unfolding prod_rel_def prod_pred_def by blast
     6.6  
     6.7 -lemma reflp_prod_rel [reflexivity_rule]:
     6.8 -  assumes "reflp R1"
     6.9 -  assumes "reflp R2"
    6.10 -  shows "reflp (prod_rel R1 R2)"
    6.11 -using assms by (auto intro!: reflpI elim: reflpE)
    6.12 -
    6.13  lemma left_total_prod_rel [reflexivity_rule]:
    6.14    assumes "left_total R1"
    6.15    assumes "left_total R2"
     7.1 --- a/src/HOL/Lifting_Set.thy	Tue Feb 18 23:03:47 2014 +0100
     7.2 +++ b/src/HOL/Lifting_Set.thy	Tue Feb 18 23:03:49 2014 +0100
     7.3 @@ -54,9 +54,6 @@
     7.4  apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
     7.5  done
     7.6  
     7.7 -lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
     7.8 -  unfolding reflp_def set_rel_def by fast
     7.9 -
    7.10  lemma left_total_set_rel[reflexivity_rule]: 
    7.11    "left_total A \<Longrightarrow> left_total (set_rel A)"
    7.12    unfolding left_total_def set_rel_def
     8.1 --- a/src/HOL/Lifting_Sum.thy	Tue Feb 18 23:03:47 2014 +0100
     8.2 +++ b/src/HOL/Lifting_Sum.thy	Tue Feb 18 23:03:49 2014 +0100
     8.3 @@ -26,10 +26,6 @@
     8.4  using assms
     8.5  by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
     8.6  
     8.7 -lemma reflp_sum_rel[reflexivity_rule]:
     8.8 -  "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
     8.9 -  unfolding reflp_def split_sum_all sum_rel_simps by fast
    8.10 -
    8.11  lemma left_total_sum_rel[reflexivity_rule]:
    8.12    "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
    8.13    using assms unfolding left_total_def split_sum_all split_sum_ex by simp
     9.1 --- a/src/HOL/List.thy	Tue Feb 18 23:03:47 2014 +0100
     9.2 +++ b/src/HOL/List.thy	Tue Feb 18 23:03:49 2014 +0100
     9.3 @@ -6582,16 +6582,6 @@
     9.4    by (auto iff: fun_eq_iff)
     9.5  qed 
     9.6  
     9.7 -lemma reflp_list_all2[reflexivity_rule]:
     9.8 -  assumes "reflp R"
     9.9 -  shows "reflp (list_all2 R)"
    9.10 -proof (rule reflpI)
    9.11 -  from assms have *: "\<And>xs. R xs xs" by (rule reflpE)
    9.12 -  fix xs
    9.13 -  show "list_all2 R xs xs"
    9.14 -    by (induct xs) (simp_all add: *)
    9.15 -qed
    9.16 -
    9.17  lemma left_total_list_all2[reflexivity_rule]:
    9.18    "left_total R \<Longrightarrow> left_total (list_all2 R)"
    9.19    unfolding left_total_def
    10.1 --- a/src/HOL/Topological_Spaces.thy	Tue Feb 18 23:03:47 2014 +0100
    10.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Feb 18 23:03:49 2014 +0100
    10.3 @@ -2375,10 +2375,6 @@
    10.4  unfolding filter_rel_eventually[abs_def]
    10.5  by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
    10.6  
    10.7 -lemma reflp_filter_rel [reflexivity_rule]: "reflp R \<Longrightarrow> reflp (filter_rel R)"
    10.8 -unfolding filter_rel_eventually[abs_def]
    10.9 -by(blast intro!: reflpI eventually_subst always_eventually dest: fun_relD reflpD)
   10.10 -
   10.11  lemma filter_rel_conversep [simp]: "filter_rel A\<inverse>\<inverse> = (filter_rel A)\<inverse>\<inverse>"
   10.12  by(auto simp add: filter_rel_eventually fun_eq_iff fun_rel_def)
   10.13