# HG changeset patch
# User krauss
# Date 1176460247 -7200
# Node ID 2d1179ad431c60a49f059faacd84ea1767d7474f
# Parent  f792579b6e59ae6a1d35295921670999622fc343
more robust proof

diff -r f792579b6e59 -r 2d1179ad431c src/HOL/Library/Graphs.thy
--- a/src/HOL/Library/Graphs.thy	Fri Apr 13 10:02:30 2007 +0200
+++ b/src/HOL/Library/Graphs.thy	Fri Apr 13 12:30:47 2007 +0200
@@ -82,6 +82,7 @@
   Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
 proof
   fix x y z :: "('a,'b) graph"
+  fix A :: "('a, 'b) graph set"
 
   show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
     unfolding graph_leq_def graph_less_def
@@ -89,29 +90,37 @@
 
   show "x \<le> x" unfolding graph_leq_def ..
 
-  show "\<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y" unfolding graph_leq_def 
-    by (cases x, cases y) simp
+  { assume "x \<le> y" "y \<le> z" 
+    with order_trans show "x \<le> z"
+      unfolding graph_leq_def . }
+
+  { assume "x \<le> y" "y \<le> x" thus "x = y" 
+      unfolding graph_leq_def 
+      by (cases x, cases y) simp }
 
   show "inf x y \<le> x" "inf x y \<le> y"
-    "\<lbrakk>x \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> x \<le> inf y z"
-    unfolding inf_graph_def graph_leq_def by auto
+    unfolding inf_graph_def graph_leq_def 
+    by auto    
+  
+  { assume "x \<le> y" "x \<le> z" thus "x \<le> inf y z"
+      unfolding inf_graph_def graph_leq_def 
+      by auto }
 
   show "x \<le> sup x y" "y \<le> sup x y"
-    "\<lbrakk>y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> sup y z \<le> x"
     unfolding sup_graph_def graph_leq_def graph_plus_def by auto
+
+  { assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x"
+      unfolding sup_graph_def graph_leq_def graph_plus_def by auto }
   
   show "sup x (inf y z) = inf (sup x y) (sup x z)"
     unfolding inf_graph_def sup_graph_def graph_leq_def graph_plus_def by auto
 
-  fix A :: "('a, 'b) graph set"
-  show "x \<in> A \<Longrightarrow> Inf A \<le> x"
-    and "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf A"
-    unfolding Inf_graph_def graph_leq_def by auto
+  { assume "x \<in> A" thus "Inf A \<le> x" 
+      unfolding Inf_graph_def graph_leq_def by auto }
 
-  from order_trans
-  show "\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z" 
-    unfolding graph_leq_def .
-qed auto
+  { assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" thus "z \<le> Inf A"
+    unfolding Inf_graph_def graph_leq_def by auto }
+qed
 
 lemma in_grplus:
   "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"