# HG changeset patch
# User nipkow
# Date 1356288855 -3600
# Node ID 5b6cf0fbc329efb9558634d00c84d7f6d035546f
# Parent  965d4c108584ee55cf2dfea43f449ab5e80c8a84
renamed and added lemmas

diff -r 965d4c108584 -r 5b6cf0fbc329 NEWS
--- a/NEWS	Sat Dec 22 00:04:50 2012 +0100
+++ b/NEWS	Sun Dec 23 19:54:15 2012 +0100
@@ -217,6 +217,10 @@
   - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> at_top".
     INCOMPATIBILITY
 
+* HOL/Transitive_Closure: renamed lemmas
+  reflcl_tranclp -> reflclp_tranclp
+  rtranclp_reflcl -> rtranclp_reflclp
+
 * HOL/Rings: renamed lemmas
 
 left_distrib ~> distrib_right
diff -r 965d4c108584 -r 5b6cf0fbc329 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sat Dec 22 00:04:50 2012 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sun Dec 23 19:54:15 2012 +0100
@@ -79,6 +79,8 @@
 lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans(r^=)"
 unfolding trans_def by blast
 
+lemma reflclp_idemp [simp]: "(P^==)^==  =  P^=="
+by blast
 
 subsection {* Reflexive-transitive closure *}
 
@@ -206,14 +208,14 @@
 lemmas rtrancl_subset = rtranclp_subset [to_set]
 
 lemma rtranclp_sup_rtranclp: "(sup (R^**) (S^**))^** = (sup R S)^**"
-  by (blast intro!: rtranclp_subset intro: rtranclp_mono [THEN predicate2D])
+by (blast intro!: rtranclp_subset intro: rtranclp_mono [THEN predicate2D])
 
 lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set]
 
-lemma rtranclp_reflcl [simp]: "(R^==)^** = R^**"
-  by (blast intro!: rtranclp_subset)
+lemma rtranclp_reflclp [simp]: "(R^==)^** = R^**"
+by (blast intro!: rtranclp_subset)
 
-lemmas rtrancl_reflcl [simp] = rtranclp_reflcl [to_set]
+lemmas rtrancl_reflcl [simp] = rtranclp_reflclp [to_set]
 
 lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*"
   apply (rule sym)
@@ -560,13 +562,13 @@
    apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+
   done
 
-lemma reflcl_tranclp [simp]: "(r^++)^== = r^**"
+lemma reflclp_tranclp [simp]: "(r^++)^== = r^**"
   apply (safe intro!: order_antisym)
    apply (erule tranclp_into_rtranclp)
   apply (blast elim: rtranclp.cases dest: rtranclp_into_tranclp1)
   done
 
-lemmas reflcl_trancl [simp] = reflcl_tranclp [to_set]
+lemmas reflcl_trancl [simp] = reflclp_tranclp [to_set]
 
 lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"
   apply safe
@@ -587,7 +589,7 @@
   by (rule subst [OF reflcl_trancl]) simp
 
 lemma rtranclpD: "R^** a b ==> a = b \<or> a \<noteq> b \<and> R^++ a b"
-  by (force simp add: reflcl_tranclp [symmetric] simp del: reflcl_tranclp)
+by (force simp add: reflclp_tranclp [symmetric] simp del: reflclp_tranclp)
 
 lemmas rtranclD = rtranclpD [to_set]