src/HOL/Library/Code_Target_Nat.thy
 author haftmann Sun Oct 08 22:28:21 2017 +0200 (20 months ago) changeset 66808 1907167b6038 parent 66190 a41435469559 child 68028 1f9f973eed2a permissions -rw-r--r--
elementary definition of division on natural numbers
 haftmann@50023 ` 1` ```(* Title: HOL/Library/Code_Target_Nat.thy ``` haftmann@51113 ` 2` ``` Author: Florian Haftmann, TU Muenchen ``` haftmann@50023 ` 3` ```*) ``` haftmann@50023 ` 4` wenzelm@60500 ` 5` ```section \Implementation of natural numbers by target-language integers\ ``` haftmann@50023 ` 6` haftmann@50023 ` 7` ```theory Code_Target_Nat ``` haftmann@51143 ` 8` ```imports Code_Abstract_Nat ``` haftmann@50023 ` 9` ```begin ``` haftmann@50023 ` 10` wenzelm@60500 ` 11` ```subsection \Implementation for @{typ nat}\ ``` haftmann@50023 ` 12` kuncar@55736 ` 13` ```context ``` kuncar@55736 ` 14` ```includes natural.lifting integer.lifting ``` kuncar@55736 ` 15` ```begin ``` kuncar@55736 ` 16` haftmann@51114 ` 17` ```lift_definition Nat :: "integer \ nat" ``` haftmann@51114 ` 18` ``` is nat ``` haftmann@51114 ` 19` ``` . ``` haftmann@50023 ` 20` haftmann@51095 ` 21` ```lemma [code_post]: ``` haftmann@51095 ` 22` ``` "Nat 0 = 0" ``` haftmann@51095 ` 23` ``` "Nat 1 = 1" ``` haftmann@51095 ` 24` ``` "Nat (numeral k) = numeral k" ``` haftmann@51114 ` 25` ``` by (transfer, simp)+ ``` haftmann@50023 ` 26` haftmann@51095 ` 27` ```lemma [code_abbrev]: ``` haftmann@51095 ` 28` ``` "integer_of_nat = of_nat" ``` haftmann@51114 ` 29` ``` by transfer rule ``` haftmann@50023 ` 30` haftmann@50023 ` 31` ```lemma [code_unfold]: ``` haftmann@50023 ` 32` ``` "Int.nat (int_of_integer k) = nat_of_integer k" ``` haftmann@51114 ` 33` ``` by transfer rule ``` haftmann@50023 ` 34` haftmann@50023 ` 35` ```lemma [code abstype]: ``` haftmann@50023 ` 36` ``` "Code_Target_Nat.Nat (integer_of_nat n) = n" ``` haftmann@51114 ` 37` ``` by transfer simp ``` haftmann@50023 ` 38` haftmann@50023 ` 39` ```lemma [code abstract]: ``` haftmann@50023 ` 40` ``` "integer_of_nat (nat_of_integer k) = max 0 k" ``` haftmann@51114 ` 41` ``` by transfer auto ``` haftmann@50023 ` 42` haftmann@50023 ` 43` ```lemma [code_abbrev]: ``` haftmann@51095 ` 44` ``` "nat_of_integer (numeral k) = nat_of_num k" ``` haftmann@51114 ` 45` ``` by transfer (simp add: nat_of_num_numeral) ``` haftmann@50023 ` 46` haftmann@64997 ` 47` ```context ``` haftmann@64997 ` 48` ```begin ``` haftmann@64997 ` 49` haftmann@64997 ` 50` ```qualified definition natural :: "num \ nat" ``` haftmann@64997 ` 51` ``` where [simp]: "natural = nat_of_num" ``` haftmann@64997 ` 52` haftmann@64997 ` 53` ```lemma [code_computation_unfold]: ``` haftmann@64997 ` 54` ``` "numeral = natural" ``` haftmann@64997 ` 55` ``` "nat_of_num = natural" ``` haftmann@64997 ` 56` ``` by (simp_all add: nat_of_num_numeral) ``` haftmann@64997 ` 57` haftmann@64997 ` 58` ```end ``` haftmann@64997 ` 59` haftmann@50023 ` 60` ```lemma [code abstract]: ``` haftmann@50023 ` 61` ``` "integer_of_nat (nat_of_num n) = integer_of_num n" ``` haftmann@66190 ` 62` ``` by (simp add: nat_of_num_numeral integer_of_nat_numeral) ``` haftmann@50023 ` 63` haftmann@50023 ` 64` ```lemma [code abstract]: ``` haftmann@50023 ` 65` ``` "integer_of_nat 0 = 0" ``` haftmann@51114 ` 66` ``` by transfer simp ``` haftmann@50023 ` 67` haftmann@50023 ` 68` ```lemma [code abstract]: ``` haftmann@50023 ` 69` ``` "integer_of_nat 1 = 1" ``` haftmann@51114 ` 70` ``` by transfer simp ``` haftmann@50023 ` 71` haftmann@51113 ` 72` ```lemma [code]: ``` haftmann@51113 ` 73` ``` "Suc n = n + 1" ``` haftmann@51113 ` 74` ``` by simp ``` haftmann@51113 ` 75` haftmann@50023 ` 76` ```lemma [code abstract]: ``` haftmann@50023 ` 77` ``` "integer_of_nat (m + n) = of_nat m + of_nat n" ``` haftmann@51114 ` 78` ``` by transfer simp ``` haftmann@50023 ` 79` haftmann@50023 ` 80` ```lemma [code abstract]: ``` haftmann@50023 ` 81` ``` "integer_of_nat (m - n) = max 0 (of_nat m - of_nat n)" ``` haftmann@51114 ` 82` ``` by transfer simp ``` haftmann@50023 ` 83` haftmann@50023 ` 84` ```lemma [code abstract]: ``` haftmann@50023 ` 85` ``` "integer_of_nat (m * n) = of_nat m * of_nat n" ``` haftmann@51114 ` 86` ``` by transfer (simp add: of_nat_mult) ``` haftmann@50023 ` 87` haftmann@50023 ` 88` ```lemma [code abstract]: ``` haftmann@50023 ` 89` ``` "integer_of_nat (m div n) = of_nat m div of_nat n" ``` haftmann@51114 ` 90` ``` by transfer (simp add: zdiv_int) ``` haftmann@50023 ` 91` haftmann@50023 ` 92` ```lemma [code abstract]: ``` haftmann@50023 ` 93` ``` "integer_of_nat (m mod n) = of_nat m mod of_nat n" ``` haftmann@51114 ` 94` ``` by transfer (simp add: zmod_int) ``` haftmann@50023 ` 95` haftmann@50023 ` 96` ```lemma [code]: ``` haftmann@50023 ` 97` ``` "Divides.divmod_nat m n = (m div n, m mod n)" ``` haftmann@66808 ` 98` ``` by (fact divmod_nat_def) ``` haftmann@50023 ` 99` haftmann@50023 ` 100` ```lemma [code]: ``` haftmann@61275 ` 101` ``` "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)" ``` haftmann@61275 ` 102` ``` by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv) ``` haftmann@61275 ` 103` ``` (transfer, simp_all only: nat_div_distrib nat_mod_distrib ``` haftmann@61275 ` 104` ``` zero_le_numeral nat_numeral) ``` haftmann@61275 ` 105` ``` ``` haftmann@61275 ` 106` ```lemma [code]: ``` haftmann@50023 ` 107` ``` "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)" ``` haftmann@51114 ` 108` ``` by transfer (simp add: equal) ``` haftmann@50023 ` 109` haftmann@50023 ` 110` ```lemma [code]: ``` haftmann@50023 ` 111` ``` "m \ n \ (of_nat m :: integer) \ of_nat n" ``` haftmann@50023 ` 112` ``` by simp ``` haftmann@50023 ` 113` haftmann@50023 ` 114` ```lemma [code]: ``` haftmann@50023 ` 115` ``` "m < n \ (of_nat m :: integer) < of_nat n" ``` haftmann@50023 ` 116` ``` by simp ``` haftmann@50023 ` 117` haftmann@50023 ` 118` ```lemma num_of_nat_code [code]: ``` haftmann@50023 ` 119` ``` "num_of_nat = num_of_integer \ of_nat" ``` haftmann@51114 ` 120` ``` by transfer (simp add: fun_eq_iff) ``` haftmann@50023 ` 121` kuncar@55736 ` 122` ```end ``` kuncar@55736 ` 123` haftmann@54796 ` 124` ```lemma (in semiring_1) of_nat_code_if: ``` haftmann@50023 ` 125` ``` "of_nat n = (if n = 0 then 0 ``` haftmann@50023 ` 126` ``` else let ``` haftmann@61433 ` 127` ``` (m, q) = Divides.divmod_nat n 2; ``` haftmann@50023 ` 128` ``` m' = 2 * of_nat m ``` haftmann@50023 ` 129` ``` in if q = 0 then m' else m' + 1)" ``` haftmann@50023 ` 130` ```proof - ``` haftmann@64242 ` 131` ``` from div_mult_mod_eq have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp ``` haftmann@50023 ` 132` ``` show ?thesis ``` haftmann@66808 ` 133` ``` by (simp add: Let_def divmod_nat_def of_nat_add [symmetric]) ``` haftmann@57512 ` 134` ``` (simp add: * mult.commute of_nat_mult add.commute) ``` haftmann@50023 ` 135` ```qed ``` haftmann@50023 ` 136` haftmann@54796 ` 137` ```declare of_nat_code_if [code] ``` haftmann@50023 ` 138` haftmann@50023 ` 139` ```definition int_of_nat :: "nat \ int" where ``` haftmann@50023 ` 140` ``` [code_abbrev]: "int_of_nat = of_nat" ``` haftmann@50023 ` 141` haftmann@50023 ` 142` ```lemma [code]: ``` haftmann@50023 ` 143` ``` "int_of_nat n = int_of_integer (of_nat n)" ``` haftmann@50023 ` 144` ``` by (simp add: int_of_nat_def) ``` haftmann@50023 ` 145` haftmann@50023 ` 146` ```lemma [code abstract]: ``` haftmann@50023 ` 147` ``` "integer_of_nat (nat k) = max 0 (integer_of_int k)" ``` kuncar@55736 ` 148` ``` including integer.lifting by transfer auto ``` haftmann@50023 ` 149` Andreas@53027 ` 150` ```lemma term_of_nat_code [code]: ``` wenzelm@61585 ` 151` ``` \ \Use @{term Code_Numeral.nat_of_integer} in term reconstruction ``` Andreas@53027 ` 152` ``` instead of @{term Code_Target_Nat.Nat} such that reconstructed ``` wenzelm@60500 ` 153` ``` terms can be fed back to the code generator\ ``` Andreas@53027 ` 154` ``` "term_of_class.term_of n = ``` Andreas@53027 ` 155` ``` Code_Evaluation.App ``` Andreas@53027 ` 156` ``` (Code_Evaluation.Const (STR ''Code_Numeral.nat_of_integer'') ``` Andreas@53027 ` 157` ``` (typerep.Typerep (STR ''fun'') ``` Andreas@53027 ` 158` ``` [typerep.Typerep (STR ''Code_Numeral.integer'') [], ``` Andreas@53027 ` 159` ``` typerep.Typerep (STR ''Nat.nat'') []])) ``` Andreas@53027 ` 160` ``` (term_of_class.term_of (integer_of_nat n))" ``` haftmann@54796 ` 161` ``` by (simp add: term_of_anything) ``` Andreas@53027 ` 162` Andreas@53027 ` 163` ```lemma nat_of_integer_code_post [code_post]: ``` Andreas@53027 ` 164` ``` "nat_of_integer 0 = 0" ``` Andreas@53027 ` 165` ``` "nat_of_integer 1 = 1" ``` Andreas@53027 ` 166` ``` "nat_of_integer (numeral k) = numeral k" ``` kuncar@55736 ` 167` ``` including integer.lifting by (transfer, simp)+ ``` Andreas@53027 ` 168` haftmann@52435 ` 169` ```code_identifier ``` haftmann@52435 ` 170` ``` code_module Code_Target_Nat \ ``` haftmann@52435 ` 171` ``` (SML) Arith and (OCaml) Arith and (Haskell) Arith ``` haftmann@50023 ` 172` haftmann@50023 ` 173` ```end ```