# HG changeset patch
# User bulwahn
# Date 1272963617 -7200
# Node ID 7eadf5acdaf485d726341c65ab78c93a84d966db
# Parent  6243b49498ea7027b5b9604b8806bbf0e2568a3d
added lemma about irreflexivity of pointer inequality in Imperative_HOL

diff -r 6243b49498ea -r 7eadf5acdaf4 src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Tue May 04 11:00:16 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Tue May 04 11:00:17 2010 +0200
@@ -216,6 +216,9 @@
   and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
 unfolding noteq_refs_def noteq_arrs_def by auto
 
+lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False"
+  unfolding noteq_refs_def by auto
+
 lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
   by (simp add: ref_present_def new_ref_def ref_def Let_def noteq_refs_def)