summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 17 Aug 2000 10:38:43 +0200 | |

changeset 9627 | 31d4a77c89d6 |

parent 9626 | c4a45149cc46 |

child 9628 | 53a62fd8b2dc |

updated;
tuned;

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