--- 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 *}