author haftmann Thu, 20 Sep 2007 16:37:30 +0200 changeset 24658 49adbdcc52e2 parent 24657 185502d54c3d child 24659 6b7ac2a43df8
clarified code lemmas
 src/HOL/Set.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Set.thy	Thu Sep 20 16:37:29 2007 +0200
+++ b/src/HOL/Set.thy	Thu Sep 20 16:37:30 2007 +0200
@@ -2081,13 +2081,13 @@

subsection {* Getting the Contents of a Singleton Set *}

-constdefs
-  contents :: "'a set => 'a"
-  "contents X == THE x. X = {x}"
-lemmas [code func del] = contents_def
-
-lemma contents_eq [simp, code func]: "contents {x} = x"
+definition
+  contents :: "'a set \<Rightarrow> 'a"
+where
+  [code func del]: "contents X = (THE x. X = {x})"
+
+lemma contents_eq [simp]: "contents {x} = x"

subsection {* Transitivity rules for calculational reasoning *}
@@ -2140,7 +2140,7 @@
subsubsection {* Primitive operations *}

lemma minus_insert [code func]:
-  "insert a A - B = (let C = A - B in if a \<in> B then C else insert a C)"
+  "insert (a\<Colon>'a\<Colon>eq) A - B = (let C = A - B in if a \<in> B then C else insert a C)"

lemma minus_empty1 [code func]:
@@ -2191,6 +2191,11 @@
"UNION {} f = {}"
by auto

+lemma contents_insert [code func]:
+  "contents (insert a A) = contents (insert a (A - {a}))"
+  by auto
+declare contents_eq [code func]
+

subsubsection {* Derived predicates *}
```