author wenzelm Thu, 17 Aug 2000 10:38:43 +0200 changeset 9627 31d4a77c89d6 parent 9626 c4a45149cc46 child 9628 53a62fd8b2dc
updated; tuned;
 src/HOL/ex/Points.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/ex/Points.thy	Thu Aug 17 10:38:20 2000 +0200
+++ b/src/HOL/ex/Points.thy	Thu Aug 17 10:38:43 2000 +0200
@@ -64,6 +64,9 @@

text {* Basic simplifications *}

+lemma "point.make n p = (| x = n, y = p |)"
+  by simp
+
lemma "x (| x = m, y = n, ... = p |) = m"
by simp

@@ -71,6 +74,38 @@
by simp

+text {* Equality of records *}
+
+lemma "n = n' ==> p = p' ==> (| x = n, y = p |) = (| x = n', y = p' |)"
+  -- "introduction of concrete record equality"
+  by simp
+
+lemma "(| x = n, y = p |) = (| x = n', y = p' |) ==> n = n'"
+  -- "elimination of concrete record equality"
+  by simp
+
+lemma "r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)"
+  -- "introduction of abstract record equality"
+  by simp
+
+lemma "r (| x := n |) = r (| x := n' |) ==> n = n'"
+  -- "elimination of abstract record equality (manual proof)"
+proof -
+  assume "r (| x := n |) = r (| x := n' |)" (is "?lhs = ?rhs")
+  hence "x ?lhs = x ?rhs" by simp
+  thus ?thesis by simp
+qed
+
+
+text {* Surjective pairing *}
+
+lemma "r = (| x = x r, y = y r |)"
+  by simp
+
+lemma "r = (| x = x r, y = y r, ... = more r |)"
+  by simp
+
+
text {* Splitting quantifiers: the !!r is NECESSARY here *}

lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)"
@@ -90,11 +125,6 @@
qed

-text {* Equality of records *}
-
-lemma "(| x = n, y = p |) = (| x = n', y = p' |) ==> n = n'"
-  by simp
-

text {* Concrete records are type instances of record schemes *}
```