author krauss Tue Apr 10 21:52:38 2007 +0200 (2007-04-10) changeset 22626 7e35b6c8ab5b parent 22625 a2967023d674 child 22627 2b093ba973bc
some restructuring
1.1 --- a/src/HOL/Library/Graphs.thy	Tue Apr 10 21:51:08 2007 +0200
1.2 +++ b/src/HOL/Library/Graphs.thy	Tue Apr 10 21:52:38 2007 +0200
1.3 @@ -60,21 +60,87 @@
1.4    by (cases G, cases H, auto simp:split_paired_all has_edge_def)
1.7 -instance graph :: (type, times) times
1.8 -  graph_mult_def: "G * H == grcomp G H" ..
1.9 +instance graph :: (type, type) "{comm_monoid_add}"
1.10 +  graph_zero_def: "0 == Graph {}"
1.11 +  graph_plus_def: "G + H == Graph (dest_graph G \<union> dest_graph H)"
1.12 +proof
1.13 +  fix x y z :: "('a,'b) graph"
1.14 +
1.15 +  show "x + y + z = x + (y + z)"
1.16 +   and "x + y = y + x"
1.17 +   and "0 + x = x"
1.18 +  unfolding graph_plus_def graph_zero_def
1.19 +  by auto
1.20 +qed
1.21 +
1.22 +
1.23 +instance graph :: (type, type) "{distrib_lattice, complete_lattice}"
1.24 +  graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
1.25 +  graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
1.26 +  "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
1.27 +  "sup G H \<equiv> G + H"
1.28 +  Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
1.29 +proof
1.30 +  fix x y z :: "('a,'b) graph"
1.31 +
1.32 +  show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
1.33 +    unfolding graph_leq_def graph_less_def
1.34 +    by (cases x, cases y) auto
1.35 +
1.36 +  show "x \<le> x" unfolding graph_leq_def ..
1.37 +
1.38 +  show "\<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y" unfolding graph_leq_def
1.39 +    by (cases x, cases y) simp
1.40 +
1.41 +  show "inf x y \<le> x" "inf x y \<le> y"
1.42 +    "\<lbrakk>x \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> x \<le> inf y z"
1.43 +    unfolding inf_graph_def graph_leq_def by auto
1.44 +
1.45 +  show "x \<le> sup x y" "y \<le> sup x y"
1.46 +    "\<lbrakk>y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> sup y z \<le> x"
1.47 +    unfolding sup_graph_def graph_leq_def graph_plus_def by auto
1.48 +
1.49 +  show "sup x (inf y z) = inf (sup x y) (sup x z)"
1.50 +    unfolding inf_graph_def sup_graph_def graph_leq_def graph_plus_def by auto
1.51 +
1.52 +  fix A :: "('a, 'b) graph set"
1.53 +  show "x \<in> A \<Longrightarrow> Inf A \<le> x"
1.54 +    and "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf A"
1.55 +    unfolding Inf_graph_def graph_leq_def by auto
1.56 +
1.57 +  from order_trans
1.58 +  show "\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z"
1.59 +    unfolding graph_leq_def .
1.60 +qed auto
1.61 +
1.62 +lemma in_grplus:
1.63 +  "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
1.64 +  by (cases G, cases H, auto simp:has_edge_def graph_plus_def)
1.65 +
1.66 +lemma in_grzero:
1.67 +  "has_edge 0 p b q = False"
1.68 +  by (simp add:graph_zero_def has_edge_def)
1.69 +
1.70 +
1.71 +
1.72 +subsection {* Multiplicative Structure *}
1.73 +
1.74 +instance graph :: (type, times) mult_zero
1.75 +  graph_mult_def: "G * H == grcomp G H"
1.76 +proof
1.77 +  fix a :: "('a, 'b) graph"
1.78 +
1.79 +  show "0 * a = 0"
1.80 +    unfolding graph_mult_def graph_zero_def
1.81 +    by (cases a) (simp add:grcomp.simps)
1.82 +  show "a * 0 = 0"
1.83 +    unfolding graph_mult_def graph_zero_def
1.84 +    by (cases a) (simp add:grcomp.simps)
1.85 +qed
1.87  instance graph :: (type, one) one
1.88    graph_one_def: "1 == Graph { (x, 1, x) |x. True}" ..
1.90 -instance graph :: (type, type) zero
1.91 -  graph_zero_def: "0 == Graph {}" ..
1.92 -
1.93 -instance graph :: (type, type) plus
1.94 -  graph_plus_def: "G + H == Graph (dest_graph G \<union> dest_graph H)" ..
1.95 -
1.96 -
1.97 -subsection {* Simprules for the graph operations *}
1.98 -
1.99  lemma in_grcomp:
1.100    "has_edge (G * H) p b q
1.101    = (\<exists>k e e'. has_edge G p e k \<and> has_edge H k e' q \<and> b = e * e')"
1.102 @@ -84,15 +150,6 @@
1.103    "has_edge 1 p b q = (p = q \<and> b = 1)"
1.104    by (auto simp:graph_one_def has_edge_def)
1.106 -lemma in_grplus:
1.107 -  "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
1.108 -  by (cases G, cases H, auto simp:has_edge_def graph_plus_def)
1.110 -lemma in_grzero:
1.111 -  "has_edge 0 p b q = False"
1.112 -  by (simp add:graph_zero_def has_edge_def)
1.115  instance graph :: (type, semigroup_mult) semigroup_mult
1.116  proof
1.117    fix G1 G2 G3 :: "('a,'b) graph"
1.118 @@ -112,80 +169,22 @@
1.119    qed
1.120  qed
1.122 -instance graph :: (type, monoid_mult) monoid_mult
1.123 -proof
1.124 -  fix G1 G2 G3 :: "('a,'b) graph"
1.126 -  show "1 * G1 = G1"
1.127 -    by (rule graph_ext) (auto simp:in_grcomp in_grunit)
1.128 -  show "G1 * 1 = G1"
1.129 -    by (rule graph_ext) (auto simp:in_grcomp in_grunit)
1.130 -qed
1.133 -lemma grcomp_rdist:
1.134 -  fixes G :: "('a::type, 'b::semigroup_mult) graph"
1.135 -  shows "G * (H + I) = G * H + G * I"
1.136 -  by (rule graph_ext, simp add:in_grcomp in_grplus) blast
1.138 -lemma grcomp_ldist:
1.139 -  fixes G :: "('a::type, 'b::semigroup_mult) graph"
1.140 -  shows "(G + H) * I = G * I + H * I"
1.141 -  by (rule graph_ext, simp add:in_grcomp in_grplus) blast
1.143  fun grpow :: "nat \<Rightarrow> ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a, 'b) graph"
1.144  where
1.145    "grpow 0 A = 1"
1.146  | "grpow (Suc n) A = A * (grpow n A)"
1.149 -instance graph :: (type, monoid_mult) recpower
1.150 -  graph_pow_def: "A ^ n == grpow n A"
1.151 -  by default (simp_all add:graph_pow_def)
1.153 -subsection {* Order on Graphs *}
1.155 -instance graph :: (type, type) order
1.156 -  graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
1.157 -  graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
1.158 -proof
1.159 -  fix x y z :: "('a,'b) graph"
1.161 -  show "x \<le> x" unfolding graph_leq_def ..
1.163 -  from order_trans
1.164 -  show "\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z" unfolding graph_leq_def .
1.166 -  show "\<lbrakk>x \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> x = y" unfolding graph_leq_def
1.167 -    by (cases x, cases y) simp
1.169 -  show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
1.170 -    unfolding graph_leq_def graph_less_def
1.171 -    by (cases x, cases y) auto
1.172 -qed
1.174 -instance graph :: (type, type) distrib_lattice
1.175 -  "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
1.176 -  "sup G H \<equiv> G + H"
1.177 -  by default (auto simp add: split_graph_all graph_plus_def inf_graph_def sup_graph_def graph_leq_def graph_less_def)
1.179 -instance graph :: (type, type) complete_lattice
1.180 -  Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
1.181 -  by default (auto simp: Inf_graph_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
1.183 -instance graph :: (type, monoid_mult) semiring_1
1.184 +instance graph :: (type, monoid_mult)
1.186 +  graph_pow_def: "A ^ n == grpow n A"
1.187 +  graph_star_def: "star G == (SUP n. G ^ n)"
1.188  proof
1.189    fix a b c :: "('a, 'b) graph"
1.191 -  show "a + b + c = a + (b + c)"
1.192 -    and "a + b = b + a" unfolding graph_plus_def
1.193 -    by auto
1.195 -  show "0 + a = a" unfolding graph_zero_def graph_plus_def
1.196 -    by simp
1.198 -  show "0 * a = 0" "a * 0 = 0" unfolding graph_zero_def graph_mult_def
1.199 -    by (cases a, simp)+
1.201 +  show "1 * a = a"
1.202 +    by (rule graph_ext) (auto simp:in_grcomp in_grunit)
1.203 +  show "a * 1 = a"
1.204 +    by (rule graph_ext) (auto simp:in_grcomp in_grunit)
1.206    show "(a + b) * c = a * c + b * c"
1.207      by (rule graph_ext, simp add:in_grcomp in_grplus) blast
1.208 @@ -195,22 +194,14 @@
1.210    show "(0::('a,'b) graph) \<noteq> 1" unfolding graph_zero_def graph_one_def
1.211      by simp
1.212 -qed
1.214 -instance graph :: (type, monoid_mult) idem_add
1.215 -proof
1.216 -  fix a :: "('a, 'b) graph"
1.217    show "a + a = a" unfolding graph_plus_def by simp
1.219 +  show "a ^ 0 = 1" "\<And>n. a ^ (Suc n) = a * a ^ n"
1.220 +    unfolding graph_pow_def by simp_all
1.221  qed
1.224 -(* define star on graphs *)
1.227 -instance graph :: (type, monoid_mult) star
1.228 -  graph_star_def: "star G == (SUP n. G ^ n)" ..
1.231  lemma graph_leqI:
1.232    assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
1.233    shows "G \<le> H"
1.234 @@ -227,8 +218,6 @@
1.235    using prems
1.236    by (auto simp: in_grplus)
1.240  lemma
1.241    assumes "x \<in> S k"
1.242    shows "x \<in> (\<Union>k. S k)"
1.243 @@ -242,15 +231,13 @@
1.245  lemma Sup_graph_eq:
1.246    "(SUP n. Graph (G n)) = Graph (\<Union>n. G n)"
1.247 -  unfolding SUPR_def
1.248 -  apply (rule order_antisym)
1.249 -  apply (rule Sup_least)
1.250 -  apply auto