# HG changeset patch
# User wenzelm
# Date 966501523 -7200
# Node ID 31d4a77c89d61631dea497cecc35f50d21261374
# Parent  c4a45149cc461b2da8aa06b01c902811fc26ea6c
updated;
tuned;

diff -r c4a45149cc46 -r 31d4a77c89d6 src/HOL/ex/Points.thy
--- 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 *}