author krauss Fri Apr 13 12:30:47 2007 +0200 (2007-04-13) changeset 22660 2d1179ad431c parent 22659 f792579b6e59 child 22661 f3ba63a2663e
more robust proof
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.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.13    show "x \<le> x" unfolding graph_leq_def ..
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.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.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.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.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.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.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)"