# HG changeset patch # User nipkow # Date 1073259966 -3600 # Node ID e13731554e50626b07571b2c3692a0292ef37d70 # Parent 8f731d3cd65b2357ad753467c95aedcc9864f744 undid split_comp_eq[simp] because it leads to nontermination together with split_def! diff -r 8f731d3cd65b -r e13731554e50 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Sat Jan 03 16:09:39 2004 +0100 +++ b/src/HOL/Product_Type.thy Mon Jan 05 00:46:06 2004 +0100 @@ -484,7 +484,11 @@ apply (rule ext, blast) done -lemma split_comp_eq [simp]: +(* Do NOT make this a simp rule as it + a) only helps in special situations + b) can lead to nontermination in the presence of split_def +*) +lemma split_comp_eq: "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))" by (rule ext, auto) diff -r 8f731d3cd65b -r e13731554e50 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Sat Jan 03 16:09:39 2004 +0100 +++ b/src/HOL/Transitive_Closure.thy Mon Jan 05 00:46:06 2004 +0100 @@ -402,6 +402,16 @@ text {* More about converse @{text rtrancl} and @{text trancl}, should be merged with main body. *} +lemma single_valued_confluent: + "\ single_valued r; (x,y) \ r^*; (x,z) \ r^* \ + \ (y,z) \ r^* \ (z,y) \ r^*" +apply(erule rtrancl_induct) + apply simp +apply(erule disjE) + apply(blast elim:converse_rtranclE dest:single_valuedD) +apply(blast intro:rtrancl_trans) +done + lemma r_r_into_trancl: "(a, b) \ R ==> (b, c) \ R ==> (a, c) \ R^+" by (fast intro: trancl_trans)