# HG changeset patch
# User berghofe
# Date 1210150763 -7200
# Node ID 6a4d5ca6d2e5ccc4247d5ad4e271d00e43ab861a
# Parent  c0fa62fa0e5b07790d3870158150eb6a64434298
Rephrased calculational proofs to avoid problems with HO unification

diff -r c0fa62fa0e5b -r 6a4d5ca6d2e5 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- 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)" .
diff -r c0fa62fa0e5b -r 6a4d5ca6d2e5 src/HOL/ex/CTL.thy
--- 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