improved code theorem setup
authorhaftmann
Fri Jan 25 14:54:41 2008 +0100 (2008-01-25)
changeset 2596505df64f786a4
parent 25964 080f89d89990
child 25966 74f6817870f9
improved code theorem setup
src/HOL/Library/Code_Char.thy
src/HOL/Map.thy
src/HOL/NatBin.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Library/Code_Char.thy	Fri Jan 25 14:53:58 2008 +0100
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Fri Jan 25 14:54:41 2008 +0100
     1.3 @@ -9,6 +9,16 @@
     1.4  imports List
     1.5  begin
     1.6  
     1.7 +declare char.recs [code func del] char.cases [code func del]
     1.8 +
     1.9 +lemma [code func]:
    1.10 +  "size (c\<Colon>char) = 0"
    1.11 +  by (cases c) simp
    1.12 +
    1.13 +lemma [code func]:
    1.14 +  "char_size (c\<Colon>char) = 0"
    1.15 +  by (cases c) simp
    1.16 +
    1.17  code_type char
    1.18    (SML "char")
    1.19    (OCaml "char")
     2.1 --- a/src/HOL/Map.thy	Fri Jan 25 14:53:58 2008 +0100
     2.2 +++ b/src/HOL/Map.thy	Fri Jan 25 14:54:41 2008 +0100
     2.3 @@ -83,6 +83,13 @@
     2.4    "map_of [] = empty"
     2.5    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
     2.6  
     2.7 +declare map_of.simps [code del]
     2.8 +
     2.9 +lemma map_of_Cons_code [code]: 
    2.10 +  "map_of [] k = None"
    2.11 +  "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
    2.12 +  by simp_all
    2.13 +
    2.14  defs
    2.15    map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    2.16  
     3.1 --- a/src/HOL/NatBin.thy	Fri Jan 25 14:53:58 2008 +0100
     3.2 +++ b/src/HOL/NatBin.thy	Fri Jan 25 14:54:41 2008 +0100
     3.3 @@ -18,12 +18,16 @@
     3.4  begin
     3.5  
     3.6  definition
     3.7 -  nat_number_of_def [code inline]: "number_of v = nat (number_of (v\<Colon>int))"
     3.8 +  nat_number_of_def [code inline]: "number_of v = nat (number_of v)"
     3.9  
    3.10  instance ..
    3.11  
    3.12  end
    3.13  
    3.14 +lemma [code post]:
    3.15 +  "nat (number_of v) = number_of v"
    3.16 +  unfolding nat_number_of_def ..
    3.17 +
    3.18  abbreviation (xsymbols)
    3.19    square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
    3.20    "x\<twosuperior> == x^2"
     4.1 --- a/src/HOL/Real/Rational.thy	Fri Jan 25 14:53:58 2008 +0100
     4.2 +++ b/src/HOL/Real/Rational.thy	Fri Jan 25 14:54:41 2008 +0100
     4.3 @@ -499,7 +499,7 @@
     4.4  begin
     4.5  
     4.6  definition
     4.7 -  rat_number_of_def: "number_of w = (of_int w \<Colon> rat)"
     4.8 +  rat_number_of_def [code func del]: "number_of w = (of_int w \<Colon> rat)"
     4.9  
    4.10  instance
    4.11    by default (simp add: rat_number_of_def)
    4.12 @@ -640,11 +640,13 @@
    4.13  
    4.14  lemma zero_rat_code [code, code unfold]:
    4.15    "0 = Rational 0\<^sub>N" by simp
    4.16 +declare zero_rat_code [symmetric, code post]
    4.17  
    4.18 -lemma zero_rat_code [code, code unfold]:
    4.19 +lemma one_rat_code [code, code unfold]:
    4.20    "1 = Rational 1\<^sub>N" by simp
    4.21 +declare one_rat_code [symmetric, code post]
    4.22  
    4.23 -lemma [code, code unfold]:
    4.24 +lemma [code unfold, symmetric, code post]:
    4.25    "number_of k = rat_of_int (number_of k)"
    4.26    by (simp add: number_of_is_id rat_number_of_def)
    4.27  
     5.1 --- a/src/HOL/Real/RealDef.thy	Fri Jan 25 14:53:58 2008 +0100
     5.2 +++ b/src/HOL/Real/RealDef.thy	Fri Jan 25 14:54:41 2008 +0100
     5.3 @@ -852,14 +852,14 @@
     5.4  begin
     5.5  
     5.6  definition
     5.7 -  real_number_of_def: "number_of w = real_of_int w"
     5.8 +  real_number_of_def [code func del]: "number_of w = real_of_int w"
     5.9  
    5.10  instance
    5.11    by intro_classes (simp add: real_number_of_def)
    5.12  
    5.13  end
    5.14  
    5.15 -lemma [code, code unfold]:
    5.16 +lemma [code unfold, symmetric, code post]:
    5.17    "number_of k = real_of_int (number_of k)"
    5.18    unfolding number_of_is_id real_number_of_def ..
    5.19  
    5.20 @@ -972,9 +972,11 @@
    5.21  
    5.22  lemma zero_real_code [code, code unfold]:
    5.23    "0 = Ratreal 0\<^sub>N" by simp
    5.24 +declare zero_real_code [symmetric, code post]
    5.25  
    5.26  lemma one_real_code [code, code unfold]:
    5.27    "1 = Ratreal 1\<^sub>N" by simp
    5.28 +declare one_real_code [symmetric, code post]
    5.29  
    5.30  instance real :: eq ..
    5.31  
    5.32 @@ -1015,13 +1017,6 @@
    5.33  lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
    5.34    unfolding Ratreal_def by simp
    5.35  
    5.36 -instance int :: lordered_ring
    5.37 -proof  
    5.38 -  fix a::int
    5.39 -  show "abs a = sup a (- a)"
    5.40 -    by (auto simp add: zabs_def sup_int_def)
    5.41 -qed
    5.42 -
    5.43  instance real :: lordered_ring
    5.44  proof
    5.45    fix a::real
     6.1 --- a/src/HOL/Set.thy	Fri Jan 25 14:53:58 2008 +0100
     6.2 +++ b/src/HOL/Set.thy	Fri Jan 25 14:54:41 2008 +0100
     6.3 @@ -2141,7 +2141,7 @@
     6.4  definition
     6.5    is_empty :: "'a set \<Rightarrow> bool"
     6.6  where
     6.7 -  [code func del]: "is_empty A \<longleftrightarrow> A = {}"
     6.8 +  [code func del, code post]: "is_empty A \<longleftrightarrow> A = {}"
     6.9  lemmas [code inline] = is_empty_def [symmetric]
    6.10  
    6.11  lemma is_empty_insert [code func]: