1.1 --- a/src/HOL/Library/Code_Index.thy Fri Oct 10 06:45:50 2008 +0200
1.2 +++ b/src/HOL/Library/Code_Index.thy Fri Oct 10 06:45:53 2008 +0200
1.3 @@ -64,7 +64,7 @@
1.4 instantiation index :: zero
1.5 begin
1.6
1.7 -definition [simp, code func del]:
1.8 +definition [simp, code del]:
1.9 "0 = index_of_nat 0"
1.10
1.11 instance ..
1.12 @@ -87,12 +87,12 @@
1.13 then show "P k" by simp
1.14 qed simp_all
1.15
1.16 -lemmas [code func del] = index.recs index.cases
1.17 +lemmas [code del] = index.recs index.cases
1.18
1.19 declare index_case [case_names nat, cases type: index]
1.20 declare index.induct [case_names nat, induct type: index]
1.21
1.22 -lemma [code func]:
1.23 +lemma [code]:
1.24 "index_size = nat_of_index"
1.25 proof (rule ext)
1.26 fix k
1.27 @@ -102,7 +102,7 @@
1.28 finally show "index_size k = nat_of_index k" .
1.29 qed
1.30
1.31 -lemma [code func]:
1.32 +lemma [code]:
1.33 "size = nat_of_index"
1.34 proof (rule ext)
1.35 fix k
1.36 @@ -110,7 +110,7 @@
1.37 by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
1.38 qed
1.39
1.40 -lemma [code func]:
1.41 +lemma [code]:
1.42 "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)"
1.43 by (cases k, cases l) (simp add: eq)
1.44
1.45 @@ -143,63 +143,63 @@
1.46 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
1.47 begin
1.48
1.49 -lemma zero_index_code [code inline, code func]:
1.50 +lemma zero_index_code [code inline, code]:
1.51 "(0\<Colon>index) = Numeral0"
1.52 by (simp add: number_of_index_def Pls_def)
1.53 lemma [code post]: "Numeral0 = (0\<Colon>index)"
1.54 using zero_index_code ..
1.55
1.56 -definition [simp, code func del]:
1.57 +definition [simp, code del]:
1.58 "(1\<Colon>index) = index_of_nat 1"
1.59
1.60 -lemma one_index_code [code inline, code func]:
1.61 +lemma one_index_code [code inline, code]:
1.62 "(1\<Colon>index) = Numeral1"
1.63 by (simp add: number_of_index_def Pls_def Bit1_def)
1.64 lemma [code post]: "Numeral1 = (1\<Colon>index)"
1.65 using one_index_code ..
1.66
1.67 -definition [simp, code func del]:
1.68 +definition [simp, code del]:
1.69 "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
1.70
1.71 -lemma plus_index_code [code func]:
1.72 +lemma plus_index_code [code]:
1.73 "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
1.74 by simp
1.75
1.76 -definition [simp, code func del]:
1.77 +definition [simp, code del]:
1.78 "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
1.79
1.80 -definition [simp, code func del]:
1.81 +definition [simp, code del]:
1.82 "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
1.83
1.84 -lemma times_index_code [code func]:
1.85 +lemma times_index_code [code]:
1.86 "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
1.87 by simp
1.88
1.89 -definition [simp, code func del]:
1.90 +definition [simp, code del]:
1.91 "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
1.92
1.93 -definition [simp, code func del]:
1.94 +definition [simp, code del]:
1.95 "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
1.96
1.97 -lemma div_index_code [code func]:
1.98 +lemma div_index_code [code]:
1.99 "index_of_nat n div index_of_nat m = index_of_nat (n div m)"
1.100 by simp
1.101
1.102 -lemma mod_index_code [code func]:
1.103 +lemma mod_index_code [code]:
1.104 "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
1.105 by simp
1.106
1.107 -definition [simp, code func del]:
1.108 +definition [simp, code del]:
1.109 "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
1.110
1.111 -definition [simp, code func del]:
1.112 +definition [simp, code del]:
1.113 "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
1.114
1.115 -lemma less_eq_index_code [code func]:
1.116 +lemma less_eq_index_code [code]:
1.117 "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
1.118 by simp
1.119
1.120 -lemma less_index_code [code func]:
1.121 +lemma less_index_code [code]:
1.122 "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
1.123 by simp
1.124
1.125 @@ -260,25 +260,25 @@
1.126 definition
1.127 minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
1.128 where
1.129 - [code func del]: "minus_index_aux = op -"
1.130 + [code del]: "minus_index_aux = op -"
1.131
1.132 -lemma [code func]: "op - = minus_index_aux"
1.133 +lemma [code]: "op - = minus_index_aux"
1.134 using minus_index_aux_def ..
1.135
1.136 definition
1.137 div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index"
1.138 where
1.139 - [code func del]: "div_mod_index n m = (n div m, n mod m)"
1.140 + [code del]: "div_mod_index n m = (n div m, n mod m)"
1.141
1.142 -lemma [code func]:
1.143 +lemma [code]:
1.144 "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
1.145 unfolding div_mod_index_def by auto
1.146
1.147 -lemma [code func]:
1.148 +lemma [code]:
1.149 "n div m = fst (div_mod_index n m)"
1.150 unfolding div_mod_index_def by simp
1.151
1.152 -lemma [code func]:
1.153 +lemma [code]:
1.154 "n mod m = snd (div_mod_index n m)"
1.155 unfolding div_mod_index_def by simp
1.156
1.157 @@ -340,7 +340,7 @@
1.158
1.159 text {* Evaluation *}
1.160
1.161 -lemma [code func, code func del]:
1.162 +lemma [code, code del]:
1.163 "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
1.164
1.165 code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"