--- 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")
--- 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))"
--- 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"
--- 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)
--- 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
--- 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]: