Replaced forward proofs of existential statements by backward proofs
to avoid problems with HO unification

--- a/src/HOL/Algebra/Group.thy	Wed May 07 10:56:55 2008 +0200
+++ b/src/HOL/Algebra/Group.thy	Wed May 07 10:56:58 2008 +0200
@@ -735,38 +735,42 @@
 proof (rule partial_order.complete_lattice_criterion1)
   show "partial_order ?L" by (rule subgroups_partial_order)
 next
-  have "greatest ?L (carrier G) (carrier ?L)"
-    by (unfold greatest_def)
-      (simp add: subgroup.subset subgroup_self)
-  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
+  show "\<exists>G. greatest ?L G (carrier ?L)"
+  proof
+    show "greatest ?L (carrier G) (carrier ?L)"
+      by (unfold greatest_def)
+        (simp add: subgroup.subset subgroup_self)
+  qed
 next
   fix A
   assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
   then have Int_subgroup: "subgroup (\<Inter>A) G"
     by (fastsimp intro: subgroups_Inter)
-  have "greatest ?L (\<Inter>A) (Lower ?L A)"
-    (is "greatest _ ?Int _")
-  proof (rule greatest_LowerI)
-    fix H
-    assume H: "H \<in> A"
-    with L have subgroupH: "subgroup H G" by auto
-    from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
-      by (rule subgroup_imp_group)
-    from groupH have monoidH: "monoid ?H"
-      by (rule group.is_monoid)
-    from H have Int_subset: "?Int \<subseteq> H" by fastsimp
-    then show "le ?L ?Int H" by simp
-  next
-    fix H
-    assume H: "H \<in> Lower ?L A"
-    with L Int_subgroup show "le ?L H ?Int"
-      by (fastsimp simp: Lower_def intro: Inter_greatest)
-  next
-    show "A \<subseteq> carrier ?L" by (rule L)
-  next
-    show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
+  show "\<exists>I. greatest ?L I (Lower ?L A)"
+  proof
+    show "greatest ?L (\<Inter>A) (Lower ?L A)"
+      (is "greatest _ ?Int _")
+    proof (rule greatest_LowerI)
+      fix H
+      assume H: "H \<in> A"
+      with L have subgroupH: "subgroup H G" by auto
+      from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H")
+	by (rule subgroup_imp_group)
+      from groupH have monoidH: "monoid ?H"
+	by (rule group.is_monoid)
+      from H have Int_subset: "?Int \<subseteq> H" by fastsimp
+      then show "le ?L ?Int H" by simp
+    next
+      fix H
+      assume H: "H \<in> Lower ?L A"
+      with L Int_subgroup show "le ?L H ?Int"
+	by (fastsimp simp: Lower_def intro: Inter_greatest)
+    next
+      show "A \<subseteq> carrier ?L" by (rule L)
+    next
+      show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
+    qed
   qed
-  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
 qed
 
 end

--- a/src/HOL/Algebra/Lattice.thy	Wed May 07 10:56:55 2008 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Wed May 07 10:56:58 2008 +0200
@@ -847,18 +847,22 @@
     by (rule partial_order.intro) auto
 next
   fix B
-  assume "B \<subseteq> carrier ?L"
-  then have "least ?L (\<Union> B) (Upper ?L B)"
-    by (fastsimp intro!: least_UpperI simp: Upper_def)
-  then show "EX s. least ?L s (Upper ?L B)" ..
+  assume B: "B \<subseteq> carrier ?L"
+  show "EX s. least ?L s (Upper ?L B)"
+  proof
+    from B show "least ?L (\<Union> B) (Upper ?L B)"
+      by (fastsimp intro!: least_UpperI simp: Upper_def)
+  qed
 next
   fix B
-  assume "B \<subseteq> carrier ?L"
-  then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
-    txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
-      @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
-    by (fastsimp intro!: greatest_LowerI simp: Lower_def)
-  then show "EX i. greatest ?L i (Lower ?L B)" ..
+  assume B: "B \<subseteq> carrier ?L"
+  show "EX i. greatest ?L i (Lower ?L B)"
+  proof
+    from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
+      txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
+	@{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
+      by (fastsimp intro!: greatest_LowerI simp: Lower_def)
+  qed
 qed
 
 text {* An other example, that of the lattice of subgroups of a group,

--- a/src/HOL/Hyperreal/Filter.thy	Wed May 07 10:56:55 2008 +0200
+++ b/src/HOL/Hyperreal/Filter.thy	Wed May 07 10:56:58 2008 +0200
@@ -394,10 +394,12 @@
     fix A assume "A \<in> U"
     with U show "infinite A" by (rule mem_superfrechet_all_infinite)
   qed
-  from fil ultra free have "freeultrafilter U"
-    by (rule freeultrafilter.intro [OF ultrafilter.intro])
-    (* FIXME: unfold_locales should use chained facts *)
-  thus ?thesis ..
+  show ?thesis
+  proof
+    from fil ultra free show "freeultrafilter U"
+      by (rule freeultrafilter.intro [OF ultrafilter.intro])
+      (* FIXME: unfold_locales should use chained facts *)
+  qed
 qed
 
 lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex