equal
deleted
inserted
replaced
120 by force |
120 by force |
121 |
121 |
122 code_modulename SML |
122 code_modulename SML |
123 Implementation Graphs |
123 Implementation Graphs |
124 |
124 |
125 lemma [code func]: |
125 lemma [code]: |
126 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H" |
126 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H" |
127 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H" |
127 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H" |
128 unfolding graph_leq_def graph_less_def by rule+ |
128 unfolding graph_leq_def graph_less_def by rule+ |
129 |
129 |
130 lemma [code func]: |
130 lemma [code]: |
131 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)" |
131 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)" |
132 unfolding graph_plus_def .. |
132 unfolding graph_plus_def .. |
133 |
133 |
134 lemma [code func]: |
134 lemma [code]: |
135 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H" |
135 "(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H" |
136 unfolding graph_mult_def .. |
136 unfolding graph_mult_def .. |
137 |
137 |
138 |
138 |
139 |
139 |