more robust proof
authorkrauss
Fri Apr 13 12:30:47 2007 +0200 (2007-04-13)
changeset 226602d1179ad431c
parent 22659 f792579b6e59
child 22661 f3ba63a2663e
more robust proof
src/HOL/Library/Graphs.thy
     1.1 --- a/src/HOL/Library/Graphs.thy	Fri Apr 13 10:02:30 2007 +0200
     1.2 +++ b/src/HOL/Library/Graphs.thy	Fri Apr 13 12:30:47 2007 +0200
     1.3 @@ -82,6 +82,7 @@
     1.4    Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
     1.5  proof
     1.6    fix x y z :: "('a,'b) graph"
     1.7 +  fix A :: "('a, 'b) graph set"
     1.8  
     1.9    show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
    1.10      unfolding graph_leq_def graph_less_def
    1.11 @@ -89,29 +90,37 @@
    1.12  
    1.13    show "x \<le> x" unfolding graph_leq_def ..
    1.14  
    1.15 -  show "\<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y" unfolding graph_leq_def 
    1.16 -    by (cases x, cases y) simp
    1.17 +  { assume "x \<le> y" "y \<le> z" 
    1.18 +    with order_trans show "x \<le> z"
    1.19 +      unfolding graph_leq_def . }
    1.20 +
    1.21 +  { assume "x \<le> y" "y \<le> x" thus "x = y" 
    1.22 +      unfolding graph_leq_def 
    1.23 +      by (cases x, cases y) simp }
    1.24  
    1.25    show "inf x y \<le> x" "inf x y \<le> y"
    1.26 -    "\<lbrakk>x \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> x \<le> inf y z"
    1.27 -    unfolding inf_graph_def graph_leq_def by auto
    1.28 +    unfolding inf_graph_def graph_leq_def 
    1.29 +    by auto    
    1.30 +  
    1.31 +  { assume "x \<le> y" "x \<le> z" thus "x \<le> inf y z"
    1.32 +      unfolding inf_graph_def graph_leq_def 
    1.33 +      by auto }
    1.34  
    1.35    show "x \<le> sup x y" "y \<le> sup x y"
    1.36 -    "\<lbrakk>y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> sup y z \<le> x"
    1.37      unfolding sup_graph_def graph_leq_def graph_plus_def by auto
    1.38 +
    1.39 +  { assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x"
    1.40 +      unfolding sup_graph_def graph_leq_def graph_plus_def by auto }
    1.41    
    1.42    show "sup x (inf y z) = inf (sup x y) (sup x z)"
    1.43      unfolding inf_graph_def sup_graph_def graph_leq_def graph_plus_def by auto
    1.44  
    1.45 -  fix A :: "('a, 'b) graph set"
    1.46 -  show "x \<in> A \<Longrightarrow> Inf A \<le> x"
    1.47 -    and "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf A"
    1.48 -    unfolding Inf_graph_def graph_leq_def by auto
    1.49 +  { assume "x \<in> A" thus "Inf A \<le> x" 
    1.50 +      unfolding Inf_graph_def graph_leq_def by auto }
    1.51  
    1.52 -  from order_trans
    1.53 -  show "\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z" 
    1.54 -    unfolding graph_leq_def .
    1.55 -qed auto
    1.56 +  { assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" thus "z \<le> Inf A"
    1.57 +    unfolding Inf_graph_def graph_leq_def by auto }
    1.58 +qed
    1.59  
    1.60  lemma in_grplus:
    1.61    "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"