src/HOL/Library/Code_Index.thy
changeset 28562 4e74209f113e
parent 28351 abfc66969d1f
child 28708 a1a436f09ec6
     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"