--- a/src/HOL/IMP/Denotational.thy Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/IMP/Denotational.thy Tue Nov 07 14:52:27 2017 +0100
@@ -90,9 +90,13 @@
lemma chain_iterates: fixes f :: "'a set \<Rightarrow> 'a set"
assumes "mono f" shows "chain(\<lambda>n. (f^^n) {})"
proof-
- { fix n have "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" using assms
- by(induction n) (auto simp: mono_def) }
- thus ?thesis by(auto simp: chain_def)
+ have "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" for n
+ proof (induction n)
+ case 0 show ?case by simp
+ next
+ case (Suc n) thus ?case using assms by (auto simp: mono_def)
+ qed
+ thus ?thesis by(auto simp: chain_def assms)
qed
theorem lfp_if_cont:
@@ -112,8 +116,9 @@
finally show "f ?U \<subseteq> ?U" by simp
qed
next
- { fix n p assume "f p \<subseteq> p"
- have "(f^^n){} \<subseteq> p"
+ have "(f^^n){} \<subseteq> p" if "f p \<subseteq> p" for n p
+ proof -
+ show ?thesis
proof(induction n)
case 0 show ?case by simp
next
@@ -121,7 +126,7 @@
from monoD[OF mono_if_cont[OF assms] Suc] `f p \<subseteq> p`
show ?case by simp
qed
- }
+ qed
thus "?U \<subseteq> lfp f" by(auto simp: lfp_def)
qed