# HG changeset patch
# User haftmann
# Date 1534941177 0
# Node ID 54fdc8bc73a3b1adff0be1f20535a085981e3cc4
# Parent  78d9b1783378ecb4251773ba933b56358dd9cddd
new simp rule

diff -r 78d9b1783378 -r 54fdc8bc73a3 src/HOL/HOLCF/Cont.thy
--- a/src/HOL/HOLCF/Cont.thy	Wed Aug 22 12:31:57 2018 +0200
+++ b/src/HOL/HOLCF/Cont.thy	Wed Aug 22 12:32:57 2018 +0000
@@ -217,7 +217,7 @@
   for f :: "'a::discrete_cpo \<Rightarrow> 'b::cpo"
   apply (rule contI)
   apply (drule discrete_chain_const, clarify)
-  apply (simp add: is_lub_const)
+  apply simp
   done
 
 end
diff -r 78d9b1783378 -r 54fdc8bc73a3 src/HOL/HOLCF/Library/List_Cpo.thy
--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Wed Aug 22 12:31:57 2018 +0200
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Wed Aug 22 12:32:57 2018 +0000
@@ -139,11 +139,18 @@
 instance list :: (cpo) cpo
 proof
   fix S :: "nat \<Rightarrow> 'a list"
-  assume "chain S" thus "\<exists>x. range S <<| x"
+  assume "chain S"
+  then show "\<exists>x. range S <<| x"
   proof (induct rule: list_chain_induct)
-    case Nil thus ?case by (auto intro: is_lub_const)
+    case Nil
+    have "{[]} <<| []"
+      by simp
+    then obtain x :: "'a list" where "{[]} <<| x" ..
+    then show ?case
+      by auto
   next
-    case (Cons A B) thus ?case by (auto intro: is_lub_Cons cpo_lubI)
+    case (Cons A B) then show ?case
+      by (auto intro: is_lub_Cons cpo_lubI)
   qed
 qed
 
diff -r 78d9b1783378 -r 54fdc8bc73a3 src/HOL/HOLCF/Porder.thy
--- a/src/HOL/HOLCF/Porder.thy	Wed Aug 22 12:31:57 2018 +0200
+++ b/src/HOL/HOLCF/Porder.thy	Wed Aug 22 12:32:57 2018 +0000
@@ -157,7 +157,7 @@
 lemma lub_eqI: "M <<| l \<Longrightarrow> lub M = l"
   by (rule is_lub_unique [OF is_lub_lub])
 
-lemma is_lub_singleton: "{x} <<| x"
+lemma is_lub_singleton [simp]: "{x} <<| x"
   by (simp add: is_lub_def)
 
 lemma lub_singleton [simp]: "lub {x} = x"
diff -r 78d9b1783378 -r 54fdc8bc73a3 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Wed Aug 22 12:31:57 2018 +0200
+++ b/src/HOL/HOLCF/Universal.thy	Wed Aug 22 12:32:57 2018 +0000
@@ -115,11 +115,7 @@
     (if P (node i a S) then node i a S else ubasis_until P a)"
    apply clarify
    apply (rule_tac x=b in node_cases)
-    apply simp
-   apply simp
-   apply fast
-  apply simp
- apply simp
+    apply simp_all
 done
 
 termination ubasis_until
diff -r 78d9b1783378 -r 54fdc8bc73a3 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Aug 22 12:31:57 2018 +0200
+++ b/src/HOL/Set.thy	Wed Aug 22 12:32:57 2018 +0000
@@ -981,6 +981,9 @@
 lemma range_composition: "range (\<lambda>x. f (g x)) = f ` range g"
   by auto
 
+lemma range_constant [simp]: "range (\<lambda>_. x) = {x}"
+  by (simp add: image_constant)
+
 lemma range_eq_singletonD: "range f = {a} \<Longrightarrow> f x = a"
   by auto