added lemma
authornipkow
Wed Jun 19 10:06:24 2013 +0200 (2013-06-19)
changeset 52392ee996ca08de3
parent 52391 e65dedce4a17
child 52393 ba73041fd5b3
added lemma
src/HOL/IMP/Denotation.thy
src/HOL/Relation.thy
     1.1 --- a/src/HOL/IMP/Denotation.thy	Tue Jun 18 15:52:47 2013 -0700
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Wed Jun 19 10:06:24 2013 +0200
     1.3 @@ -121,12 +121,9 @@
     1.4  lemma cont_W: "cont(W b r)"
     1.5  by(auto simp: cont_def W_def)
     1.6  
     1.7 +
     1.8  subsection{*The denotational semantics is deterministic*}
     1.9  
    1.10 -(* FIXME mv *)
    1.11 -lemma simgle_valued_empty[simp]: "single_valued {}"
    1.12 -by(simp add: single_valued_def)
    1.13 -
    1.14  lemma single_valued_UN_chain:
    1.15    assumes "chain S" "(\<And>n. single_valued (S n))"
    1.16    shows "single_valued(UN n. S n)"
     2.1 --- a/src/HOL/Relation.thy	Tue Jun 18 15:52:47 2013 -0700
     2.2 +++ b/src/HOL/Relation.thy	Wed Jun 19 10:06:24 2013 +0200
     2.3 @@ -416,6 +416,9 @@
     2.4    "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z"
     2.5    by (simp add: single_valued_def)
     2.6  
     2.7 +lemma simgle_valued_empty[simp]: "single_valued {}"
     2.8 +by(simp add: single_valued_def)
     2.9 +
    2.10  lemma single_valued_subset:
    2.11    "r \<subseteq> s ==> single_valued s ==> single_valued r"
    2.12    by (unfold single_valued_def) blast