--- a/src/HOL/Library/Code_Index.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Code_Index.thy Fri Oct 10 06:45:53 2008 +0200
@@ -64,7 +64,7 @@
instantiation index :: zero
begin
-definition [simp, code func del]:
+definition [simp, code del]:
"0 = index_of_nat 0"
instance ..
@@ -87,12 +87,12 @@
then show "P k" by simp
qed simp_all
-lemmas [code func del] = index.recs index.cases
+lemmas [code del] = index.recs index.cases
declare index_case [case_names nat, cases type: index]
declare index.induct [case_names nat, induct type: index]
-lemma [code func]:
+lemma [code]:
"index_size = nat_of_index"
proof (rule ext)
fix k
@@ -102,7 +102,7 @@
finally show "index_size k = nat_of_index k" .
qed
-lemma [code func]:
+lemma [code]:
"size = nat_of_index"
proof (rule ext)
fix k
@@ -110,7 +110,7 @@
by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
qed
-lemma [code func]:
+lemma [code]:
"eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)"
by (cases k, cases l) (simp add: eq)
@@ -143,63 +143,63 @@
instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
begin
-lemma zero_index_code [code inline, code func]:
+lemma zero_index_code [code inline, code]:
"(0\<Colon>index) = Numeral0"
by (simp add: number_of_index_def Pls_def)
lemma [code post]: "Numeral0 = (0\<Colon>index)"
using zero_index_code ..
-definition [simp, code func del]:
+definition [simp, code del]:
"(1\<Colon>index) = index_of_nat 1"
-lemma one_index_code [code inline, code func]:
+lemma one_index_code [code inline, code]:
"(1\<Colon>index) = Numeral1"
by (simp add: number_of_index_def Pls_def Bit1_def)
lemma [code post]: "Numeral1 = (1\<Colon>index)"
using one_index_code ..
-definition [simp, code func del]:
+definition [simp, code del]:
"n + m = index_of_nat (nat_of_index n + nat_of_index m)"
-lemma plus_index_code [code func]:
+lemma plus_index_code [code]:
"index_of_nat n + index_of_nat m = index_of_nat (n + m)"
by simp
-definition [simp, code func del]:
+definition [simp, code del]:
"n - m = index_of_nat (nat_of_index n - nat_of_index m)"
-definition [simp, code func del]:
+definition [simp, code del]:
"n * m = index_of_nat (nat_of_index n * nat_of_index m)"
-lemma times_index_code [code func]:
+lemma times_index_code [code]:
"index_of_nat n * index_of_nat m = index_of_nat (n * m)"
by simp
-definition [simp, code func del]:
+definition [simp, code del]:
"n div m = index_of_nat (nat_of_index n div nat_of_index m)"
-definition [simp, code func del]:
+definition [simp, code del]:
"n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
-lemma div_index_code [code func]:
+lemma div_index_code [code]:
"index_of_nat n div index_of_nat m = index_of_nat (n div m)"
by simp
-lemma mod_index_code [code func]:
+lemma mod_index_code [code]:
"index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
by simp
-definition [simp, code func del]:
+definition [simp, code del]:
"n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
-definition [simp, code func del]:
+definition [simp, code del]:
"n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
-lemma less_eq_index_code [code func]:
+lemma less_eq_index_code [code]:
"index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
by simp
-lemma less_index_code [code func]:
+lemma less_index_code [code]:
"index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
by simp
@@ -260,25 +260,25 @@
definition
minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
where
- [code func del]: "minus_index_aux = op -"
+ [code del]: "minus_index_aux = op -"
-lemma [code func]: "op - = minus_index_aux"
+lemma [code]: "op - = minus_index_aux"
using minus_index_aux_def ..
definition
div_mod_index :: "index \<Rightarrow> index \<Rightarrow> index \<times> index"
where
- [code func del]: "div_mod_index n m = (n div m, n mod m)"
+ [code del]: "div_mod_index n m = (n div m, n mod m)"
-lemma [code func]:
+lemma [code]:
"div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
unfolding div_mod_index_def by auto
-lemma [code func]:
+lemma [code]:
"n div m = fst (div_mod_index n m)"
unfolding div_mod_index_def by simp
-lemma [code func]:
+lemma [code]:
"n mod m = snd (div_mod_index n m)"
unfolding div_mod_index_def by simp
@@ -340,7 +340,7 @@
text {* Evaluation *}
-lemma [code func, code func del]:
+lemma [code, code del]:
"(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"