equal
deleted
inserted
replaced
71 and "0 + x = x" |
71 and "0 + x = x" |
72 unfolding graph_plus_def graph_zero_def |
72 unfolding graph_plus_def graph_zero_def |
73 by auto |
73 by auto |
74 qed |
74 qed |
75 |
75 |
|
76 lemmas [code nofunc] = graph_plus_def |
76 |
77 |
77 instance graph :: (type, type) "{distrib_lattice, complete_lattice}" |
78 instance graph :: (type, type) "{distrib_lattice, complete_lattice}" |
78 graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H" |
79 graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H" |
79 graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H" |
80 graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H" |
80 "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)" |
81 "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)" |
81 "sup G H \<equiv> G + H" |
82 "sup G H \<equiv> G + H" |
82 Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))" |
83 Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))" |
83 proof |
84 proof |
84 fix x y z :: "('a,'b) graph" |
85 fix x y z :: "('a,'b) graph" |
85 fix A :: "('a, 'b) graph set" |
86 fix A :: "('a, 'b) graph set" |
86 |
87 |
87 show "(x < y) = (x \<le> y \<and> x \<noteq> y)" |
88 show "(x < y) = (x \<le> y \<and> x \<noteq> y)" |
120 |
121 |
121 { assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" thus "z \<le> Inf A" |
122 { assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" thus "z \<le> Inf A" |
122 unfolding Inf_graph_def graph_leq_def by auto } |
123 unfolding Inf_graph_def graph_leq_def by auto } |
123 qed |
124 qed |
124 |
125 |
|
126 lemmas [code nofunc] = graph_leq_def graph_less_def |
|
127 inf_graph_def sup_graph_def Inf_graph_def |
|
128 |
125 lemma in_grplus: |
129 lemma in_grplus: |
126 "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)" |
130 "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)" |
127 by (cases G, cases H, auto simp:has_edge_def graph_plus_def) |
131 by (cases G, cases H, auto simp:has_edge_def graph_plus_def) |
128 |
132 |
129 lemma in_grzero: |
133 lemma in_grzero: |
143 by (cases a) (simp add:grcomp.simps) |
147 by (cases a) (simp add:grcomp.simps) |
144 show "a * 0 = 0" |
148 show "a * 0 = 0" |
145 unfolding graph_mult_def graph_zero_def |
149 unfolding graph_mult_def graph_zero_def |
146 by (cases a) (simp add:grcomp.simps) |
150 by (cases a) (simp add:grcomp.simps) |
147 qed |
151 qed |
|
152 |
|
153 lemmas [code nofunc] = graph_mult_def |
148 |
154 |
149 instance graph :: (type, one) one |
155 instance graph :: (type, one) one |
150 graph_one_def: "1 == Graph { (x, 1, x) |x. True}" .. |
156 graph_one_def: "1 == Graph { (x, 1, x) |x. True}" .. |
151 |
157 |
152 lemma in_grcomp: |
158 lemma in_grcomp: |