src/HOL/Library/Code_Integer.thy
 author Christian Sternagel Thu Aug 30 15:44:03 2012 +0900 (2012-08-30) changeset 49093 fdc301f592c4 parent 48431 6efff142bb54 permissions -rw-r--r--
forgot to add lemmas
 haftmann@24999 ` 1` ```(* Title: HOL/Library/Code_Integer.thy ``` haftmann@24999 ` 2` ``` Author: Florian Haftmann, TU Muenchen ``` haftmann@24999 ` 3` ```*) ``` haftmann@24999 ` 4` haftmann@24999 ` 5` ```header {* Pretty integer literals for code generation *} ``` haftmann@24999 ` 6` haftmann@24999 ` 7` ```theory Code_Integer ``` haftmann@37968 ` 8` ```imports Main Code_Natural ``` haftmann@24999 ` 9` ```begin ``` haftmann@24999 ` 10` haftmann@24999 ` 11` ```text {* ``` huffman@47108 ` 12` ``` Representation-ignorant code equations for conversions. ``` huffman@47108 ` 13` ```*} ``` huffman@47108 ` 14` huffman@47108 ` 15` ```lemma nat_code [code]: ``` huffman@47108 ` 16` ``` "nat k = (if k \ 0 then 0 else ``` huffman@47108 ` 17` ``` let ``` huffman@47108 ` 18` ``` (l, j) = divmod_int k 2; ``` huffman@47125 ` 19` ``` n = nat l; ``` huffman@47125 ` 20` ``` l' = n + n ``` huffman@47108 ` 21` ``` in if j = 0 then l' else Suc l')" ``` huffman@47108 ` 22` ```proof - ``` huffman@47108 ` 23` ``` have "2 = nat 2" by simp ``` huffman@47108 ` 24` ``` show ?thesis ``` huffman@47217 ` 25` ``` apply (subst mult_2 [symmetric]) ``` huffman@47108 ` 26` ``` apply (auto simp add: Let_def divmod_int_mod_div not_le ``` huffman@47108 ` 27` ``` nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int) ``` huffman@47108 ` 28` ``` apply (unfold `2 = nat 2`) ``` huffman@47108 ` 29` ``` apply (subst nat_mod_distrib [symmetric]) ``` huffman@47108 ` 30` ``` apply simp_all ``` huffman@47108 ` 31` ``` done ``` huffman@47108 ` 32` ```qed ``` huffman@47108 ` 33` huffman@47108 ` 34` ```lemma (in ring_1) of_int_code: ``` huffman@47108 ` 35` ``` "of_int k = (if k = 0 then 0 ``` huffman@47108 ` 36` ``` else if k < 0 then - of_int (- k) ``` huffman@47108 ` 37` ``` else let ``` huffman@47108 ` 38` ``` (l, j) = divmod_int k 2; ``` huffman@47108 ` 39` ``` l' = 2 * of_int l ``` huffman@47108 ` 40` ``` in if j = 0 then l' else l' + 1)" ``` huffman@47108 ` 41` ```proof - ``` huffman@47108 ` 42` ``` from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp ``` huffman@47108 ` 43` ``` show ?thesis ``` huffman@47108 ` 44` ``` by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int ``` huffman@47108 ` 45` ``` of_int_add [symmetric]) (simp add: * mult_commute) ``` huffman@47108 ` 46` ```qed ``` huffman@47108 ` 47` huffman@47108 ` 48` ```declare of_int_code [code] ``` huffman@47108 ` 49` huffman@47108 ` 50` ```text {* ``` haftmann@24999 ` 51` ``` HOL numeral expressions are mapped to integer literals ``` haftmann@24999 ` 52` ``` in target languages, using predefined target language ``` haftmann@24999 ` 53` ``` operations for abstract integer operations. ``` haftmann@24999 ` 54` ```*} ``` haftmann@24999 ` 55` haftmann@24999 ` 56` ```code_type int ``` haftmann@24999 ` 57` ``` (SML "IntInf.int") ``` haftmann@24999 ` 58` ``` (OCaml "Big'_int.big'_int") ``` haftmann@24999 ` 59` ``` (Haskell "Integer") ``` haftmann@34899 ` 60` ``` (Scala "BigInt") ``` haftmann@38053 ` 61` ``` (Eval "int") ``` haftmann@24999 ` 62` haftmann@38857 ` 63` ```code_instance int :: equal ``` haftmann@24999 ` 64` ``` (Haskell -) ``` haftmann@24999 ` 65` huffman@47108 ` 66` ```code_const "0::int" ``` huffman@47108 ` 67` ``` (SML "0") ``` huffman@47108 ` 68` ``` (OCaml "Big'_int.zero'_big'_int") ``` huffman@47108 ` 69` ``` (Haskell "0") ``` huffman@47108 ` 70` ``` (Scala "BigInt(0)") ``` huffman@47108 ` 71` haftmann@24999 ` 72` ```setup {* ``` huffman@47108 ` 73` ``` fold (Numeral.add_code @{const_name Int.Pos} ``` huffman@47108 ` 74` ``` false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] ``` haftmann@24999 ` 75` ```*} ``` haftmann@24999 ` 76` huffman@47108 ` 77` ```setup {* ``` huffman@47108 ` 78` ``` fold (Numeral.add_code @{const_name Int.Neg} ``` huffman@47108 ` 79` ``` true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] ``` huffman@47108 ` 80` ```*} ``` haftmann@24999 ` 81` haftmann@24999 ` 82` ```code_const "op + \ int \ int \ int" ``` haftmann@24999 ` 83` ``` (SML "IntInf.+ ((_), (_))") ``` haftmann@24999 ` 84` ``` (OCaml "Big'_int.add'_big'_int") ``` haftmann@24999 ` 85` ``` (Haskell infixl 6 "+") ``` haftmann@34899 ` 86` ``` (Scala infixl 7 "+") ``` haftmann@37958 ` 87` ``` (Eval infixl 8 "+") ``` haftmann@24999 ` 88` haftmann@24999 ` 89` ```code_const "uminus \ int \ int" ``` haftmann@24999 ` 90` ``` (SML "IntInf.~") ``` haftmann@24999 ` 91` ``` (OCaml "Big'_int.minus'_big'_int") ``` haftmann@24999 ` 92` ``` (Haskell "negate") ``` haftmann@34899 ` 93` ``` (Scala "!(- _)") ``` haftmann@37958 ` 94` ``` (Eval "~/ _") ``` haftmann@24999 ` 95` haftmann@24999 ` 96` ```code_const "op - \ int \ int \ int" ``` haftmann@24999 ` 97` ``` (SML "IntInf.- ((_), (_))") ``` haftmann@24999 ` 98` ``` (OCaml "Big'_int.sub'_big'_int") ``` haftmann@24999 ` 99` ``` (Haskell infixl 6 "-") ``` haftmann@34899 ` 100` ``` (Scala infixl 7 "-") ``` haftmann@37958 ` 101` ``` (Eval infixl 8 "-") ``` haftmann@24999 ` 102` huffman@47108 ` 103` ```code_const Int.dup ``` huffman@47108 ` 104` ``` (SML "IntInf.*/ (2,/ (_))") ``` huffman@47108 ` 105` ``` (OCaml "Big'_int.mult'_big'_int/ 2") ``` huffman@47108 ` 106` ``` (Haskell "!(2 * _)") ``` huffman@47108 ` 107` ``` (Scala "!(2 * _)") ``` huffman@47108 ` 108` ``` (Eval "!(2 * _)") ``` huffman@47108 ` 109` huffman@47108 ` 110` ```code_const Int.sub ``` huffman@47108 ` 111` ``` (SML "!(raise/ Fail/ \"sub\")") ``` huffman@47108 ` 112` ``` (OCaml "failwith/ \"sub\"") ``` huffman@47108 ` 113` ``` (Haskell "error/ \"sub\"") ``` haftmann@48073 ` 114` ``` (Scala "!sys.error(\"sub\")") ``` huffman@47108 ` 115` haftmann@24999 ` 116` ```code_const "op * \ int \ int \ int" ``` haftmann@24999 ` 117` ``` (SML "IntInf.* ((_), (_))") ``` haftmann@24999 ` 118` ``` (OCaml "Big'_int.mult'_big'_int") ``` haftmann@24999 ` 119` ``` (Haskell infixl 7 "*") ``` haftmann@34899 ` 120` ``` (Scala infixl 8 "*") ``` haftmann@37958 ` 121` ``` (Eval infixl 9 "*") ``` haftmann@24999 ` 122` haftmann@29936 ` 123` ```code_const pdivmod ``` haftmann@34899 ` 124` ``` (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") ``` haftmann@34899 ` 125` ``` (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") ``` haftmann@34944 ` 126` ``` (Haskell "divMod/ (abs _)/ (abs _)") ``` haftmann@37958 ` 127` ``` (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))") ``` haftmann@37958 ` 128` ``` (Eval "Integer.div'_mod/ (abs _)/ (abs _)") ``` haftmann@29936 ` 129` haftmann@38857 ` 130` ```code_const "HOL.equal \ int \ int \ bool" ``` haftmann@24999 ` 131` ``` (SML "!((_ : IntInf.int) = _)") ``` haftmann@24999 ` 132` ``` (OCaml "Big'_int.eq'_big'_int") ``` haftmann@39272 ` 133` ``` (Haskell infix 4 "==") ``` haftmann@34899 ` 134` ``` (Scala infixl 5 "==") ``` haftmann@37958 ` 135` ``` (Eval infixl 6 "=") ``` haftmann@24999 ` 136` haftmann@24999 ` 137` ```code_const "op \ \ int \ int \ bool" ``` haftmann@24999 ` 138` ``` (SML "IntInf.<= ((_), (_))") ``` haftmann@24999 ` 139` ``` (OCaml "Big'_int.le'_big'_int") ``` haftmann@24999 ` 140` ``` (Haskell infix 4 "<=") ``` haftmann@34899 ` 141` ``` (Scala infixl 4 "<=") ``` haftmann@37958 ` 142` ``` (Eval infixl 6 "<=") ``` haftmann@24999 ` 143` haftmann@24999 ` 144` ```code_const "op < \ int \ int \ bool" ``` haftmann@24999 ` 145` ``` (SML "IntInf.< ((_), (_))") ``` haftmann@24999 ` 146` ``` (OCaml "Big'_int.lt'_big'_int") ``` haftmann@24999 ` 147` ``` (Haskell infix 4 "<") ``` haftmann@37958 ` 148` ``` (Scala infixl 4 "<") ``` haftmann@37958 ` 149` ``` (Eval infixl 6 "<") ``` haftmann@24999 ` 150` haftmann@31205 ` 151` ```code_const Code_Numeral.int_of ``` haftmann@31192 ` 152` ``` (SML "IntInf.fromInt") ``` haftmann@31377 ` 153` ``` (OCaml "_") ``` haftmann@48431 ` 154` ``` (Haskell "Prelude.toInteger") ``` haftmann@37958 ` 155` ``` (Scala "!_.as'_BigInt") ``` haftmann@37958 ` 156` ``` (Eval "_") ``` haftmann@24999 ` 157` haftmann@32657 ` 158` ```code_const "Code_Evaluation.term_of \ int \ term" ``` haftmann@31192 ` 159` ``` (Eval "HOLogic.mk'_number/ HOLogic.intT") ``` haftmann@28228 ` 160` huffman@47108 ` 161` ```end ```