src/HOL/SizeChange/Graphs.thy

 subsection {* Basic types, Size Change Graphs *}
 
 datatype ('a, 'b) graph = 
   Graph "('a \<times> 'b \<times> 'a) set"
 
-fun dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set"
+primrec dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set"
   where "dest_graph (Graph G) = G"
 
 lemma graph_dest_graph[simp]:
   "Graph (dest_graph G) = G"
   by (cases G) simp

   shows "G = H"
   using assms
   by (cases G, cases H) (auto simp:split_paired_all has_edge_def)
 
 
-instance graph :: (type, type) "{comm_monoid_add}"
-  graph_zero_def: "0 == Graph {}" 
-  graph_plus_def: "G + H == Graph (dest_graph G \<union> dest_graph H)"
-proof
+instantiation graph :: (type, type) comm_monoid_add
+begin
+
+definition
+  graph_zero_def: "0 = Graph {}" 
+
+definition
+  graph_plus_def [code func del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
+
+instance proof
   fix x y z :: "('a,'b) graph"
-
   show "x + y + z = x + (y + z)" 
    and "x + y = y + x" 
    and "0 + x = x"
-  unfolding graph_plus_def graph_zero_def 
-  by auto
-qed
-
-lemmas [code func del] = graph_plus_def
-
-instance graph :: (type, type) "{distrib_lattice, complete_lattice}"
-  graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
-  graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
-  "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
-  "sup (G \<Colon> ('a, 'b) graph)  H \<equiv> G + H"
-  Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
-  Sup_graph_def: "Sup \<equiv> \<lambda>Gs. Graph (\<Union>(dest_graph ` Gs))"
-proof
+  unfolding graph_plus_def graph_zero_def by auto
+qed
+
+end
+
+instantiation graph :: (type, type) "{distrib_lattice, complete_lattice}"
+begin
+
+definition
+  graph_leq_def [code func del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
+
+definition
+  graph_less_def [code func del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
+
+definition
+  [code func del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
+
+definition
+  [code func del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
+
+definition
+  Inf_graph_def [code func del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
+
+definition
+  Sup_graph_def [code func del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
+
+instance 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

 
   { assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" thus "Sup A \<le> z"
     unfolding Sup_graph_def graph_leq_def by auto }
 qed
 
-lemmas [code func del] = graph_leq_def graph_less_def
-  inf_graph_def sup_graph_def Inf_graph_def Sup_graph_def
+end
 
 lemma in_grplus:
   "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
   by (cases G, cases H, auto simp:has_edge_def graph_plus_def)
 

   by (simp add:graph_zero_def has_edge_def)
 
 
 subsubsection {* Multiplicative Structure *}
 
-instance graph :: (type, times) mult_zero
-  graph_mult_def: "G * H == grcomp G H" 
-proof
+instantiation graph :: (type, times) mult_zero
+begin
+
+definition
+  graph_mult_def [code func del]: "G * H = grcomp G H" 
+
+instance proof
   fix a :: "('a, 'b) graph"
 
   show "0 * a = 0" 
     unfolding graph_mult_def graph_zero_def
     by (cases a) (simp add:grcomp.simps)
   show "a * 0 = 0" 
     unfolding graph_mult_def graph_zero_def
     by (cases a) (simp add:grcomp.simps)
 qed
 
-lemmas [code func del] = graph_mult_def
-
-instance graph :: (type, one) one 
-  graph_one_def: "1 == Graph { (x, 1, x) |x. True}" ..
+end
+
+instantiation graph :: (type, one) one 
+begin
+
+definition
+  graph_one_def: "1 = Graph { (x, 1, x) |x. True}"
+
+instance ..
+
+end
 
 lemma in_grcomp:
   "has_edge (G * H) p b q
   = (\<exists>k e e'. has_edge G p e k \<and> has_edge H k e' q \<and> b = e * e')"
   by (cases G, cases H) (auto simp:graph_mult_def has_edge_def image_def)

     show "\<dots> = has_edge (G1 * (G2 * G3)) p J q"
       by (simp only:in_grcomp mult_assoc) blast
   qed
 qed
 
-fun grpow :: "nat \<Rightarrow> ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a, 'b) graph"
-where
-  "grpow 0 A = 1"
-| "grpow (Suc n) A = A * (grpow n A)"
-
-instance graph :: (type, monoid_mult)
-  "{semiring_1,idem_add,recpower,star}"
-  graph_pow_def: "A ^ n == grpow n A"
-  graph_star_def: "star (G \<Colon> ('a, 'b) graph) == (SUP n. G ^ n)" 
-proof
+instantiation graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower, star}"
+begin
+
+primrec power_graph :: "('a\<Colon>type, 'b\<Colon>monoid_mult) graph \<Rightarrow> nat => ('a, 'b) graph"
+where
+  "(A \<Colon> ('a, 'b) graph) ^ 0 = 1"
+| "(A \<Colon> ('a, 'b) graph) ^ Suc n = A * (A ^ n)"
+
+definition
+  graph_star_def: "star (G \<Colon> ('a, 'b) graph) = (SUP n. G ^ n)" 
+
+instance proof
   fix a b c :: "('a, 'b) graph"
   
   show "1 * a = a" 
     by (rule graph_ext) (auto simp:in_grcomp in_grunit)
   show "a * 1 = a"

     by simp
 
   show "a + a = a" unfolding graph_plus_def by simp
   
   show "a ^ 0 = 1" "\<And>n. a ^ (Suc n) = a * a ^ n"
-    unfolding graph_pow_def by simp_all
-qed
+    by simp_all
+qed
+
+end
 
 lemma graph_leqI:
   assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
   shows "G \<le> H"
   using assms

   by (simp add:power_Suc power_commutes)
 
 
 lemma in_tcl: 
   "has_edge (tcl G) a x b = (\<exists>n>0. has_edge (G ^ n) a x b)"
-  apply (auto simp: tcl_is_SUP in_SUP)
+  apply (auto simp: tcl_is_SUP in_SUP simp del: power_graph.simps)
   apply (rule_tac x = "n - 1" in exI, auto)
   done
 
 
 subsection {* Infinite Paths *}