# HG changeset patch
# User haftmann
# Date 1285578721 -7200
# Node ID d1c12f4ee9ac7968d687c00ba06c96ec1f47087f
# Parent  9094200d79884c6d76fb7c9dfe4081f36977757a
treat equality on refs and arrays as primitive operation

diff -r 9094200d7988 -r d1c12f4ee9ac src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Mon Sep 27 11:11:59 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Mon Sep 27 11:12:01 2010 +0200
@@ -449,6 +449,7 @@
 code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
 code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
 code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
+code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (SML infixl 6 "=")
 
 code_reserved SML Array
 
@@ -464,6 +465,7 @@
 code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
 code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
 code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
+code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (OCaml infixl 4 "=")
 
 code_reserved OCaml Array
 
@@ -478,6 +480,8 @@
 code_const Array.len' (Haskell "Heap.lengthArray")
 code_const Array.nth' (Haskell "Heap.readArray")
 code_const Array.upd' (Haskell "Heap.writeArray")
+code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (Haskell infix 4 "==")
+code_instance array :: HOL.equal (Haskell -)
 
 
 text {* Scala *}
@@ -490,5 +494,6 @@
 code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
 code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
 code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
+code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (Scala infixl 5 "==")
 
 end
diff -r 9094200d7988 -r d1c12f4ee9ac src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Mon Sep 27 11:11:59 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Mon Sep 27 11:12:01 2010 +0200
@@ -282,6 +282,7 @@
 code_const ref' (Eval "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
 code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
 code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
+code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (SML infixl 6 "=")
 
 code_reserved Eval Unsynchronized
 
@@ -293,6 +294,7 @@
 code_const ref' (OCaml "(fun/ ()/ ->/ ref/ _)")
 code_const Ref.lookup (OCaml "(fun/ ()/ ->/ !/ _)")
 code_const Ref.update (OCaml "(fun/ ()/ ->/ _/ :=/ _)")
+code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (OCaml infixl 4 "=")
 
 code_reserved OCaml ref
 
@@ -304,6 +306,8 @@
 code_const ref' (Haskell "Heap.newSTRef")
 code_const Ref.lookup (Haskell "Heap.readSTRef")
 code_const Ref.update (Haskell "Heap.writeSTRef")
+code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (Haskell infix 4 "==")
+code_instance ref :: HOL.equal (Haskell -)
 
 
 text {* Scala *}
@@ -313,5 +317,6 @@
 code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
 code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
 code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
+code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (Scala infixl 5 "==")
 
 end