src/HOL/SizeChange/Graphs.thy
changeset 28685 275122631271
parent 28562 4e74209f113e
child 30282 a16af775e08d
     1.1 --- a/src/HOL/SizeChange/Graphs.thy	Fri Oct 24 17:48:36 2008 +0200
     1.2 +++ b/src/HOL/SizeChange/Graphs.thy	Fri Oct 24 17:48:37 2008 +0200
     1.3 @@ -89,6 +89,12 @@
     1.4    graph_less_def [code del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
     1.5  
     1.6  definition
     1.7 +  [code del]: "bot = Graph {}"
     1.8 +
     1.9 +definition
    1.10 +  [code del]: "top = Graph UNIV"
    1.11 +
    1.12 +definition
    1.13    [code del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
    1.14  
    1.15  definition
    1.16 @@ -131,6 +137,10 @@
    1.17  
    1.18    { assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x"
    1.19        unfolding sup_graph_def graph_leq_def graph_plus_def by auto }
    1.20 +
    1.21 +  show "bot \<le> x" unfolding graph_leq_def bot_graph_def by simp
    1.22 +
    1.23 +  show "x \<le> top" unfolding graph_leq_def top_graph_def by simp
    1.24    
    1.25    show "sup x (inf y z) = inf (sup x y) (sup x z)"
    1.26      unfolding inf_graph_def sup_graph_def graph_leq_def graph_plus_def by auto