author berghofe Wed, 07 May 2008 10:59:23 +0200 changeset 26813 6a4d5ca6d2e5 parent 26812 c0fa62fa0e5b child 26814 b3e8d5ec721d
Rephrased calculational proofs to avoid problems with HO unification
 src/HOL/Isar_examples/MutilatedCheckerboard.thy file | annotate | diff | comparison | revisions src/HOL/ex/CTL.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed May 07 10:59:22 2008 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed May 07 10:59:23 2008 +0200
@@ -134,7 +134,7 @@
let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
have "?B (Suc n) = ?a Un ?B n"
by (auto simp add: Sigma_Suc Un_assoc)
-  also have "... : ?T"
+  moreover have "... : ?T"
proof (rule tiling.Un)
have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
by (rule domino.horiz)
@@ -143,7 +143,7 @@
show "?B n : ?T" by (rule Suc)
show "?a <= - ?B n" by blast
qed
-  finally show ?case .
+  ultimately show ?case by simp
qed

lemma dominoes_tile_matrix:
@@ -156,13 +156,13 @@
case (Suc m)
let ?t = "{m} <*> below (2 * n)"
have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
-  also have "... : ?T"
+  moreover have "... : ?T"
proof (rule tiling_Un)
show "?t : ?T" by (rule dominoes_tile_row)
show "?B m : ?T" by (rule Suc)
show "?t Int ?B m = {}" by blast
qed
-  finally show ?case .
+  ultimately show ?case by simp
qed

lemma domino_singleton:
@@ -224,8 +224,8 @@
have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
then show ?thesis by (blast intro: that)
qed
-    also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
-    also have "card ... = Suc (card (?e t b))"
+    moreover have "... Un ?e t b = insert (i, j) (?e t b)" by simp
+    moreover have "card ... = Suc (card (?e t b))"
proof (rule card_insert_disjoint)
from `t \<in> tiling domino` have "finite t"
by (rule tiling_domino_finite)
@@ -234,7 +234,7 @@
from e have "(i, j) : ?e a b" by simp
with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
qed
-    finally show "?thesis b" .
+    ultimately show "?thesis b" by simp
qed
then have "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
also from hyp have "card (?e t 0) = card (?e t 1)" .```
```--- a/src/HOL/ex/CTL.thy	Wed May 07 10:59:22 2008 +0200
+++ b/src/HOL/ex/CTL.thy	Wed May 07 10:59:23 2008 +0200
@@ -95,7 +95,7 @@
proof
assume "x \<in> gfp (\<lambda>s. - f (- s))"
then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
-	by (auto simp add: gfp_def Sup_set_def)
+	by (auto simp add: gfp_def Sup_set_eq)
then have "f (- u) \<subseteq> - u" by auto
then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
from l and this have "x \<notin> u" by auto
@@ -253,8 +253,8 @@
proof -
{
have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
-          also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
-          finally have "?lhs \<subseteq> \<AX> p" by auto
+          moreover have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
+          ultimately have "?lhs \<subseteq> \<AX> p" by auto
}
moreover
{
@@ -262,7 +262,8 @@
also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
}
-	ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
+	ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)"
+	  by (rule Int_greatest)
also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
finally show ?thesis .
qed```