# HG changeset patch
# User haftmann
# Date 1201269281 -3600
# Node ID 05df64f786a4834641d0b3da250fbac793461980
# Parent  080f89d89990f0a6f9441b0821743bb6b42cc8b3
improved code theorem setup

diff -r 080f89d89990 -r 05df64f786a4 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Fri Jan 25 14:53:58 2008 +0100
+++ b/src/HOL/Library/Code_Char.thy	Fri Jan 25 14:54:41 2008 +0100
@@ -9,6 +9,16 @@
 imports List
 begin
 
+declare char.recs [code func del] char.cases [code func del]
+
+lemma [code func]:
+  "size (c\<Colon>char) = 0"
+  by (cases c) simp
+
+lemma [code func]:
+  "char_size (c\<Colon>char) = 0"
+  by (cases c) simp
+
 code_type char
   (SML "char")
   (OCaml "char")
diff -r 080f89d89990 -r 05df64f786a4 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Jan 25 14:53:58 2008 +0100
+++ b/src/HOL/Map.thy	Fri Jan 25 14:54:41 2008 +0100
@@ -83,6 +83,13 @@
   "map_of [] = empty"
   "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
 
+declare map_of.simps [code del]
+
+lemma map_of_Cons_code [code]: 
+  "map_of [] k = None"
+  "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
+  by simp_all
+
 defs
   map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
 
diff -r 080f89d89990 -r 05df64f786a4 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Fri Jan 25 14:53:58 2008 +0100
+++ b/src/HOL/NatBin.thy	Fri Jan 25 14:54:41 2008 +0100
@@ -18,12 +18,16 @@
 begin
 
 definition
-  nat_number_of_def [code inline]: "number_of v = nat (number_of (v\<Colon>int))"
+  nat_number_of_def [code inline]: "number_of v = nat (number_of v)"
 
 instance ..
 
 end
 
+lemma [code post]:
+  "nat (number_of v) = number_of v"
+  unfolding nat_number_of_def ..
+
 abbreviation (xsymbols)
   square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
   "x\<twosuperior> == x^2"
diff -r 080f89d89990 -r 05df64f786a4 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Fri Jan 25 14:53:58 2008 +0100
+++ b/src/HOL/Real/Rational.thy	Fri Jan 25 14:54:41 2008 +0100
@@ -499,7 +499,7 @@
 begin
 
 definition
-  rat_number_of_def: "number_of w = (of_int w \<Colon> rat)"
+  rat_number_of_def [code func del]: "number_of w = (of_int w \<Colon> rat)"
 
 instance
   by default (simp add: rat_number_of_def)
@@ -640,11 +640,13 @@
 
 lemma zero_rat_code [code, code unfold]:
   "0 = Rational 0\<^sub>N" by simp
+declare zero_rat_code [symmetric, code post]
 
-lemma zero_rat_code [code, code unfold]:
+lemma one_rat_code [code, code unfold]:
   "1 = Rational 1\<^sub>N" by simp
+declare one_rat_code [symmetric, code post]
 
-lemma [code, code unfold]:
+lemma [code unfold, symmetric, code post]:
   "number_of k = rat_of_int (number_of k)"
   by (simp add: number_of_is_id rat_number_of_def)
 
diff -r 080f89d89990 -r 05df64f786a4 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Fri Jan 25 14:53:58 2008 +0100
+++ b/src/HOL/Real/RealDef.thy	Fri Jan 25 14:54:41 2008 +0100
@@ -852,14 +852,14 @@
 begin
 
 definition
-  real_number_of_def: "number_of w = real_of_int w"
+  real_number_of_def [code func del]: "number_of w = real_of_int w"
 
 instance
   by intro_classes (simp add: real_number_of_def)
 
 end
 
-lemma [code, code unfold]:
+lemma [code unfold, symmetric, code post]:
   "number_of k = real_of_int (number_of k)"
   unfolding number_of_is_id real_number_of_def ..
 
@@ -972,9 +972,11 @@
 
 lemma zero_real_code [code, code unfold]:
   "0 = Ratreal 0\<^sub>N" by simp
+declare zero_real_code [symmetric, code post]
 
 lemma one_real_code [code, code unfold]:
   "1 = Ratreal 1\<^sub>N" by simp
+declare one_real_code [symmetric, code post]
 
 instance real :: eq ..
 
@@ -1015,13 +1017,6 @@
 lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
   unfolding Ratreal_def by simp
 
-instance int :: lordered_ring
-proof  
-  fix a::int
-  show "abs a = sup a (- a)"
-    by (auto simp add: zabs_def sup_int_def)
-qed
-
 instance real :: lordered_ring
 proof
   fix a::real
diff -r 080f89d89990 -r 05df64f786a4 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Jan 25 14:53:58 2008 +0100
+++ b/src/HOL/Set.thy	Fri Jan 25 14:54:41 2008 +0100
@@ -2141,7 +2141,7 @@
 definition
   is_empty :: "'a set \<Rightarrow> bool"
 where
-  [code func del]: "is_empty A \<longleftrightarrow> A = {}"
+  [code func del, code post]: "is_empty A \<longleftrightarrow> A = {}"
 lemmas [code inline] = is_empty_def [symmetric]
 
 lemma is_empty_insert [code func]: