some restructuring
authorkrauss
Tue Apr 10 21:52:38 2007 +0200 (2007-04-10)
changeset 226267e35b6c8ab5b
parent 22625 a2967023d674
child 22627 2b093ba973bc
some restructuring
src/HOL/Library/Graphs.thy
     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.5  
     1.6  
     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.86  
    1.87  instance graph :: (type, one) one 
    1.88    graph_one_def: "1 == Graph { (x, 1, x) |x. True}" ..
    1.89  
    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.105  
   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.109 -
   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.113 -
   1.114 -
   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.121  
   1.122 -instance graph :: (type, monoid_mult) monoid_mult
   1.123 -proof
   1.124 -  fix G1 G2 G3 :: "('a,'b) graph"
   1.125 -  
   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.131 -
   1.132 -
   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.137 -
   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.142 -
   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.147  
   1.148 -
   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.152 -
   1.153 -subsection {* Order on Graphs *}
   1.154 -
   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.160 -
   1.161 -  show "x \<le> x" unfolding graph_leq_def ..
   1.162 -  
   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.165 -
   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.168 -
   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.173 -
   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.178 -
   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.182 -
   1.183 -instance graph :: (type, monoid_mult) semiring_1
   1.184 +instance graph :: (type, monoid_mult) 
   1.185 +  "{semiring_1,idem_add,recpower,star}"
   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.190 -
   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.194 -
   1.195 -  show "0 + a = a" unfolding graph_zero_def graph_plus_def
   1.196 -    by simp
   1.197 -
   1.198 -  show "0 * a = 0" "a * 0 = 0" unfolding graph_zero_def graph_mult_def
   1.199 -    by (cases a, simp)+
   1.200 +  
   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.205  
   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.209  
   1.210    show "(0::('a,'b) graph) \<noteq> 1" unfolding graph_zero_def graph_one_def
   1.211      by simp
   1.212 -qed
   1.213  
   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.218 +  
   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.222  
   1.223  
   1.224 -(* define star on graphs *)
   1.225 -
   1.226 -
   1.227 -instance graph :: (type, monoid_mult) star
   1.228 -  graph_star_def: "star G == (SUP n. G ^ n)" ..
   1.229 -
   1.230 -
   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.237  
   1.238 -
   1.239 -
   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.244  
   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
   1.251 -  apply (simp add:graph_leq_def)
   1.252 -  apply auto
   1.253 -  apply (rule graph_union_least)
   1.254 -  apply (rule Sup_upper)
   1.255 -  by auto
   1.256 +proof (rule order_antisym)
   1.257 +  show "(SUP n. Graph (G n)) \<le> Graph (\<Union>n. G n)"
   1.258 +    by  (rule SUP_leI) (auto simp add: graph_leq_def)
   1.259 +
   1.260 +  show "Graph (\<Union>n. G n) \<le> (SUP n. Graph (G n))"
   1.261 +  by (rule graph_union_least, rule le_SUPI', rule) 
   1.262 +qed
   1.263  
   1.264  lemma has_edge_leq: "has_edge G p b q = (Graph {(p,b,q)} \<le> G)"
   1.265    unfolding has_edge_def graph_leq_def