author | haftmann |
Thu, 08 Nov 2012 10:02:38 +0100 | |
changeset 50023 | 28f3263d4d1b |
child 51095 | 7ae79f2e3cc7 |
permissions | -rw-r--r-- |
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/Code_Numeral_Types.thy |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
3 |
*) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
4 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
5 |
header {* Numeric types for code generation onto target language numerals only *} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
6 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
7 |
theory Code_Numeral_Types |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
8 |
imports Main Nat_Transfer Divides Lifting |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
9 |
begin |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
10 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
11 |
subsection {* Type of target language integers *} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
12 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
13 |
typedef integer = "UNIV \<Colon> int set" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
14 |
morphisms int_of_integer integer_of_int .. |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
15 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
16 |
lemma integer_eq_iff: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
17 |
"k = l \<longleftrightarrow> int_of_integer k = int_of_integer l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
18 |
using int_of_integer_inject [of k l] .. |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
19 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
20 |
lemma integer_eqI: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
21 |
"int_of_integer k = int_of_integer l \<Longrightarrow> k = l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
22 |
using integer_eq_iff [of k l] by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
23 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
24 |
lemma int_of_integer_integer_of_int [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
25 |
"int_of_integer (integer_of_int k) = k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
26 |
using integer_of_int_inverse [of k] by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
27 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
28 |
lemma integer_of_int_int_of_integer [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
29 |
"integer_of_int (int_of_integer k) = k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
30 |
using int_of_integer_inverse [of k] by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
31 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
32 |
instantiation integer :: ring_1 |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
33 |
begin |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
34 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
35 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
36 |
"0 = integer_of_int 0" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
37 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
38 |
lemma int_of_integer_zero [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
39 |
"int_of_integer 0 = 0" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
40 |
by (simp add: zero_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
41 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
42 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
43 |
"1 = integer_of_int 1" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
44 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
45 |
lemma int_of_integer_one [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
46 |
"int_of_integer 1 = 1" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
47 |
by (simp add: one_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
48 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
49 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
50 |
"k + l = integer_of_int (int_of_integer k + int_of_integer l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
51 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
52 |
lemma int_of_integer_plus [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
53 |
"int_of_integer (k + l) = int_of_integer k + int_of_integer l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
54 |
by (simp add: plus_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
55 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
56 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
57 |
"- k = integer_of_int (- int_of_integer k)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
58 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
59 |
lemma int_of_integer_uminus [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
60 |
"int_of_integer (- k) = - int_of_integer k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
61 |
by (simp add: uminus_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
62 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
63 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
64 |
"k - l = integer_of_int (int_of_integer k - int_of_integer l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
65 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
66 |
lemma int_of_integer_minus [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
67 |
"int_of_integer (k - l) = int_of_integer k - int_of_integer l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
68 |
by (simp add: minus_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
69 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
70 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
71 |
"k * l = integer_of_int (int_of_integer k * int_of_integer l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
72 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
73 |
lemma int_of_integer_times [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
74 |
"int_of_integer (k * l) = int_of_integer k * int_of_integer l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
75 |
by (simp add: times_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
76 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
77 |
instance proof |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
78 |
qed (auto simp add: integer_eq_iff algebra_simps) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
79 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
80 |
end |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
81 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
82 |
lemma int_of_integer_of_nat [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
83 |
"int_of_integer (of_nat n) = of_nat n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
84 |
by (induct n) simp_all |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
85 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
86 |
definition nat_of_integer :: "integer \<Rightarrow> nat" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
87 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
88 |
"nat_of_integer k = Int.nat (int_of_integer k)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
89 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
90 |
lemma nat_of_integer_of_nat [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
91 |
"nat_of_integer (of_nat n) = n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
92 |
by (simp add: nat_of_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
93 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
94 |
lemma int_of_integer_of_int [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
95 |
"int_of_integer (of_int k) = k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
96 |
by (induct k) (simp_all, simp only: neg_numeral_def numeral_One int_of_integer_uminus int_of_integer_one) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
97 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
98 |
lemma integer_integer_of_int_eq_of_integer_integer_of_int [simp, code_abbrev]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
99 |
"integer_of_int = of_int" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
100 |
by rule (simp add: integer_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
101 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
102 |
lemma of_int_integer_of [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
103 |
"of_int (int_of_integer k) = (k :: integer)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
104 |
by (simp add: integer_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
105 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
106 |
lemma int_of_integer_numeral [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
107 |
"int_of_integer (numeral k) = numeral k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
108 |
using int_of_integer_of_int [of "numeral k"] by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
109 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
110 |
lemma int_of_integer_neg_numeral [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
111 |
"int_of_integer (neg_numeral k) = neg_numeral k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
112 |
by (simp only: neg_numeral_def int_of_integer_uminus) simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
113 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
114 |
lemma int_of_integer_sub [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
115 |
"int_of_integer (Num.sub k l) = Num.sub k l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
116 |
by (simp only: Num.sub_def int_of_integer_minus int_of_integer_numeral) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
117 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
118 |
instantiation integer :: "{ring_div, equal, linordered_idom}" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
119 |
begin |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
120 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
121 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
122 |
"k div l = of_int (int_of_integer k div int_of_integer l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
123 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
124 |
lemma int_of_integer_div [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
125 |
"int_of_integer (k div l) = int_of_integer k div int_of_integer l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
126 |
by (simp add: div_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
127 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
128 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
129 |
"k mod l = of_int (int_of_integer k mod int_of_integer l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
130 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
131 |
lemma int_of_integer_mod [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
132 |
"int_of_integer (k mod l) = int_of_integer k mod int_of_integer l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
133 |
by (simp add: mod_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
134 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
135 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
136 |
"\<bar>k\<bar> = of_int \<bar>int_of_integer k\<bar>" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
137 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
138 |
lemma int_of_integer_abs [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
139 |
"int_of_integer \<bar>k\<bar> = \<bar>int_of_integer k\<bar>" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
140 |
by (simp add: abs_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
141 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
142 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
143 |
"sgn k = of_int (sgn (int_of_integer k))" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
144 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
145 |
lemma int_of_integer_sgn [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
146 |
"int_of_integer (sgn k) = sgn (int_of_integer k)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
147 |
by (simp add: sgn_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
148 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
149 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
150 |
"k \<le> l \<longleftrightarrow> int_of_integer k \<le> int_of_integer l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
151 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
152 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
153 |
"k < l \<longleftrightarrow> int_of_integer k < int_of_integer l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
154 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
155 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
156 |
"HOL.equal k l \<longleftrightarrow> HOL.equal (int_of_integer k) (int_of_integer l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
157 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
158 |
instance proof |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
159 |
qed (auto simp add: integer_eq_iff algebra_simps |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
160 |
less_eq_integer_def less_integer_def equal_integer_def equal |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
161 |
intro: mult_strict_right_mono) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
162 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
163 |
end |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
164 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
165 |
lemma int_of_integer_min [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
166 |
"int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
167 |
by (simp add: min_def less_eq_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
168 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
169 |
lemma int_of_integer_max [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
170 |
"int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
171 |
by (simp add: max_def less_eq_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
172 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
173 |
lemma nat_of_integer_non_positive [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
174 |
"k \<le> 0 \<Longrightarrow> nat_of_integer k = 0" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
175 |
by (simp add: nat_of_integer_def less_eq_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
176 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
177 |
lemma of_nat_of_integer [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
178 |
"of_nat (nat_of_integer k) = max 0 k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
179 |
by (simp add: nat_of_integer_def integer_eq_iff less_eq_integer_def max_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
180 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
181 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
182 |
subsection {* Code theorems for target language integers *} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
183 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
184 |
text {* Constructors *} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
185 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
186 |
definition Pos :: "num \<Rightarrow> integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
187 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
188 |
[simp, code_abbrev]: "Pos = numeral" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
189 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
190 |
definition Neg :: "num \<Rightarrow> integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
191 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
192 |
[simp, code_abbrev]: "Neg = neg_numeral" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
193 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
194 |
code_datatype "0::integer" Pos Neg |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
195 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
196 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
197 |
text {* Auxiliary operations *} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
198 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
199 |
definition dup :: "integer \<Rightarrow> integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
200 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
201 |
[simp]: "dup k = k + k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
202 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
203 |
lemma dup_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
204 |
"dup 0 = 0" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
205 |
"dup (Pos n) = Pos (Num.Bit0 n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
206 |
"dup (Neg n) = Neg (Num.Bit0 n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
207 |
unfolding Pos_def Neg_def neg_numeral_def |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
208 |
by (simp_all add: numeral_Bit0) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
209 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
210 |
definition sub :: "num \<Rightarrow> num \<Rightarrow> integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
211 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
212 |
[simp]: "sub m n = numeral m - numeral n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
213 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
214 |
lemma sub_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
215 |
"sub Num.One Num.One = 0" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
216 |
"sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
217 |
"sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
218 |
"sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
219 |
"sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
220 |
"sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
221 |
"sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
222 |
"sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
223 |
"sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
224 |
unfolding sub_def dup_def numeral.simps Pos_def Neg_def |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
225 |
neg_numeral_def numeral_BitM |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
226 |
by (simp_all only: algebra_simps add.comm_neutral) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
227 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
228 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
229 |
text {* Implementations *} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
230 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
231 |
lemma one_integer_code [code, code_unfold]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
232 |
"1 = Pos Num.One" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
233 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
234 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
235 |
lemma plus_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
236 |
"k + 0 = (k::integer)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
237 |
"0 + l = (l::integer)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
238 |
"Pos m + Pos n = Pos (m + n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
239 |
"Pos m + Neg n = sub m n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
240 |
"Neg m + Pos n = sub n m" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
241 |
"Neg m + Neg n = Neg (m + n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
242 |
by simp_all |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
243 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
244 |
lemma uminus_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
245 |
"uminus 0 = (0::integer)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
246 |
"uminus (Pos m) = Neg m" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
247 |
"uminus (Neg m) = Pos m" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
248 |
by simp_all |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
249 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
250 |
lemma minus_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
251 |
"k - 0 = (k::integer)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
252 |
"0 - l = uminus (l::integer)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
253 |
"Pos m - Pos n = sub m n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
254 |
"Pos m - Neg n = Pos (m + n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
255 |
"Neg m - Pos n = Neg (m + n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
256 |
"Neg m - Neg n = sub n m" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
257 |
by simp_all |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
258 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
259 |
lemma abs_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
260 |
"\<bar>k\<bar> = (if (k::integer) < 0 then - k else k)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
261 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
262 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
263 |
lemma sgn_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
264 |
"sgn k = (if k = 0 then 0 else if (k::integer) < 0 then - 1 else 1)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
265 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
266 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
267 |
lemma times_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
268 |
"k * 0 = (0::integer)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
269 |
"0 * l = (0::integer)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
270 |
"Pos m * Pos n = Pos (m * n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
271 |
"Pos m * Neg n = Neg (m * n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
272 |
"Neg m * Pos n = Neg (m * n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
273 |
"Neg m * Neg n = Pos (m * n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
274 |
by simp_all |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
275 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
276 |
definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
277 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
278 |
"divmod_integer k l = (k div l, k mod l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
279 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
280 |
lemma fst_divmod [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
281 |
"fst (divmod_integer k l) = k div l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
282 |
by (simp add: divmod_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
283 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
284 |
lemma snd_divmod [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
285 |
"snd (divmod_integer k l) = k mod l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
286 |
by (simp add: divmod_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
287 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
288 |
definition divmod_abs :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
289 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
290 |
"divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
291 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
292 |
lemma fst_divmod_abs [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
293 |
"fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
294 |
by (simp add: divmod_abs_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
295 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
296 |
lemma snd_divmod_abs [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
297 |
"snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
298 |
by (simp add: divmod_abs_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
299 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
300 |
lemma divmod_abs_terminate_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
301 |
"divmod_abs (Neg k) (Neg l) = divmod_abs (Pos k) (Pos l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
302 |
"divmod_abs (Neg k) (Pos l) = divmod_abs (Pos k) (Pos l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
303 |
"divmod_abs (Pos k) (Neg l) = divmod_abs (Pos k) (Pos l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
304 |
"divmod_abs j 0 = (0, \<bar>j\<bar>)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
305 |
"divmod_abs 0 j = (0, 0)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
306 |
by (simp_all add: prod_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
307 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
308 |
lemma divmod_abs_rec_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
309 |
"divmod_abs (Pos k) (Pos l) = |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
310 |
(let j = sub k l in |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
311 |
if j < 0 then (0, Pos k) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
312 |
else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
313 |
by (auto simp add: prod_eq_iff integer_eq_iff Let_def prod_case_beta |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
314 |
sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
315 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
316 |
lemma divmod_integer_code [code]: "divmod_integer k l = |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
317 |
(if k = 0 then (0, 0) else if l = 0 then (0, k) else |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
318 |
(apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
319 |
then divmod_abs k l |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
320 |
else (let (r, s) = divmod_abs k l in |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
321 |
if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
322 |
proof - |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
323 |
have aux1: "\<And>k l::int. sgn k = sgn l \<longleftrightarrow> k = 0 \<and> l = 0 \<or> 0 < l \<and> 0 < k \<or> l < 0 \<and> k < 0" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
324 |
by (auto simp add: sgn_if) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
325 |
have aux2: "\<And>q::int. - int_of_integer k = int_of_integer l * q \<longleftrightarrow> int_of_integer k = int_of_integer l * - q" by auto |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
326 |
show ?thesis |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
327 |
by (simp add: prod_eq_iff integer_eq_iff prod_case_beta aux1) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
328 |
(auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
329 |
qed |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
330 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
331 |
lemma div_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
332 |
"k div l = fst (divmod_integer k l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
333 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
334 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
335 |
lemma mod_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
336 |
"k mod l = snd (divmod_integer k l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
337 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
338 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
339 |
lemma equal_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
340 |
"HOL.equal 0 (0::integer) \<longleftrightarrow> True" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
341 |
"HOL.equal 0 (Pos l) \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
342 |
"HOL.equal 0 (Neg l) \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
343 |
"HOL.equal (Pos k) 0 \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
344 |
"HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
345 |
"HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
346 |
"HOL.equal (Neg k) 0 \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
347 |
"HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
348 |
"HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
349 |
by (simp_all add: equal integer_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
350 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
351 |
lemma equal_integer_refl [code nbe]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
352 |
"HOL.equal (k::integer) k \<longleftrightarrow> True" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
353 |
by (fact equal_refl) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
354 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
355 |
lemma less_eq_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
356 |
"0 \<le> (0::integer) \<longleftrightarrow> True" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
357 |
"0 \<le> Pos l \<longleftrightarrow> True" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
358 |
"0 \<le> Neg l \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
359 |
"Pos k \<le> 0 \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
360 |
"Pos k \<le> Pos l \<longleftrightarrow> k \<le> l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
361 |
"Pos k \<le> Neg l \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
362 |
"Neg k \<le> 0 \<longleftrightarrow> True" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
363 |
"Neg k \<le> Pos l \<longleftrightarrow> True" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
364 |
"Neg k \<le> Neg l \<longleftrightarrow> l \<le> k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
365 |
by (simp_all add: less_eq_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
366 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
367 |
lemma less_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
368 |
"0 < (0::integer) \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
369 |
"0 < Pos l \<longleftrightarrow> True" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
370 |
"0 < Neg l \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
371 |
"Pos k < 0 \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
372 |
"Pos k < Pos l \<longleftrightarrow> k < l" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
373 |
"Pos k < Neg l \<longleftrightarrow> False" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
374 |
"Neg k < 0 \<longleftrightarrow> True" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
375 |
"Neg k < Pos l \<longleftrightarrow> True" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
376 |
"Neg k < Neg l \<longleftrightarrow> l < k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
377 |
by (simp_all add: less_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
378 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
379 |
definition integer_of_num :: "num \<Rightarrow> integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
380 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
381 |
"integer_of_num = numeral" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
382 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
383 |
lemma integer_of_num [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
384 |
"integer_of_num num.One = 1" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
385 |
"integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
386 |
"integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
387 |
by (simp_all only: Let_def) (simp_all only: integer_of_num_def numeral.simps) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
388 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
389 |
definition num_of_integer :: "integer \<Rightarrow> num" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
390 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
391 |
"num_of_integer = num_of_nat \<circ> nat_of_integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
392 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
393 |
lemma num_of_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
394 |
"num_of_integer k = (if k \<le> 1 then Num.One |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
395 |
else let |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
396 |
(l, j) = divmod_integer k 2; |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
397 |
l' = num_of_integer l; |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
398 |
l'' = l' + l' |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
399 |
in if j = 0 then l'' else l'' + Num.One)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
400 |
proof - |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
401 |
{ |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
402 |
assume "int_of_integer k mod 2 = 1" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
403 |
then have "nat (int_of_integer k mod 2) = nat 1" by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
404 |
moreover assume *: "1 < int_of_integer k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
405 |
ultimately have **: "nat (int_of_integer k) mod 2 = 1" by (simp add: nat_mod_distrib) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
406 |
have "num_of_nat (nat (int_of_integer k)) = |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
407 |
num_of_nat (2 * (nat (int_of_integer k) div 2) + nat (int_of_integer k) mod 2)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
408 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
409 |
then have "num_of_nat (nat (int_of_integer k)) = |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
410 |
num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + nat (int_of_integer k) mod 2)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
411 |
by (simp add: mult_2) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
412 |
with ** have "num_of_nat (nat (int_of_integer k)) = |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
413 |
num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + 1)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
414 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
415 |
} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
416 |
note aux = this |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
417 |
show ?thesis |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
418 |
by (auto simp add: num_of_integer_def nat_of_integer_def Let_def prod_case_beta |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
419 |
not_le integer_eq_iff less_eq_integer_def |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
420 |
nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
421 |
mult_2 [where 'a=nat] aux add_One) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
422 |
qed |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
423 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
424 |
lemma nat_of_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
425 |
"nat_of_integer k = (if k \<le> 0 then 0 |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
426 |
else let |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
427 |
(l, j) = divmod_integer k 2; |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
428 |
l' = nat_of_integer l; |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
429 |
l'' = l' + l' |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
430 |
in if j = 0 then l'' else l'' + 1)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
431 |
proof - |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
432 |
obtain j where "k = integer_of_int j" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
433 |
proof |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
434 |
show "k = integer_of_int (int_of_integer k)" by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
435 |
qed |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
436 |
moreover have "2 * (j div 2) = j - j mod 2" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
437 |
by (simp add: zmult_div_cancel mult_commute) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
438 |
ultimately show ?thesis |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
439 |
by (auto simp add: split_def Let_def mod_integer_def nat_of_integer_def not_le |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
440 |
nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
441 |
qed |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
442 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
443 |
lemma int_of_integer_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
444 |
"int_of_integer k = (if k < 0 then - (int_of_integer (- k)) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
445 |
else if k = 0 then 0 |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
446 |
else let |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
447 |
(l, j) = divmod_integer k 2; |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
448 |
l' = 2 * int_of_integer l |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
449 |
in if j = 0 then l' else l' + 1)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
450 |
by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
451 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
452 |
lemma integer_of_int_code [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
453 |
"integer_of_int k = (if k < 0 then - (integer_of_int (- k)) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
454 |
else if k = 0 then 0 |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
455 |
else let |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
456 |
(l, j) = divmod_int k 2; |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
457 |
l' = 2 * integer_of_int l |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
458 |
in if j = 0 then l' else l' + 1)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
459 |
by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
460 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
461 |
hide_const (open) Pos Neg sub dup divmod_abs |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
462 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
463 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
464 |
subsection {* Serializer setup for target language integers *} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
465 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
466 |
code_reserved Eval abs |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
467 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
468 |
code_type integer |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
469 |
(SML "IntInf.int") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
470 |
(OCaml "Big'_int.big'_int") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
471 |
(Haskell "Integer") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
472 |
(Scala "BigInt") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
473 |
(Eval "int") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
474 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
475 |
code_instance integer :: equal |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
476 |
(Haskell -) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
477 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
478 |
code_const "0::integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
479 |
(SML "0") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
480 |
(OCaml "Big'_int.zero'_big'_int") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
481 |
(Haskell "0") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
482 |
(Scala "BigInt(0)") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
483 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
484 |
setup {* |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
485 |
fold (Numeral.add_code @{const_name Code_Numeral_Types.Pos} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
486 |
false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
487 |
*} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
488 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
489 |
setup {* |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
490 |
fold (Numeral.add_code @{const_name Code_Numeral_Types.Neg} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
491 |
true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
492 |
*} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
493 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
494 |
code_const "plus :: integer \<Rightarrow> _ \<Rightarrow> _" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
495 |
(SML "IntInf.+ ((_), (_))") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
496 |
(OCaml "Big'_int.add'_big'_int") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
497 |
(Haskell infixl 6 "+") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
498 |
(Scala infixl 7 "+") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
499 |
(Eval infixl 8 "+") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
500 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
501 |
code_const "uminus :: integer \<Rightarrow> _" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
502 |
(SML "IntInf.~") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
503 |
(OCaml "Big'_int.minus'_big'_int") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
504 |
(Haskell "negate") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
505 |
(Scala "!(- _)") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
506 |
(Eval "~/ _") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
507 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
508 |
code_const "minus :: integer \<Rightarrow> _" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
509 |
(SML "IntInf.- ((_), (_))") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
510 |
(OCaml "Big'_int.sub'_big'_int") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
511 |
(Haskell infixl 6 "-") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
512 |
(Scala infixl 7 "-") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
513 |
(Eval infixl 8 "-") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
514 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
515 |
code_const Code_Numeral_Types.dup |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
516 |
(SML "IntInf.*/ (2,/ (_))") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
517 |
(OCaml "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
518 |
(Haskell "!(2 * _)") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
519 |
(Scala "!(2 * _)") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
520 |
(Eval "!(2 * _)") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
521 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
522 |
code_const Code_Numeral_Types.sub |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
523 |
(SML "!(raise/ Fail/ \"sub\")") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
524 |
(OCaml "failwith/ \"sub\"") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
525 |
(Haskell "error/ \"sub\"") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
526 |
(Scala "!sys.error(\"sub\")") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
527 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
528 |
code_const "times :: integer \<Rightarrow> _ \<Rightarrow> _" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
529 |
(SML "IntInf.* ((_), (_))") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
530 |
(OCaml "Big'_int.mult'_big'_int") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
531 |
(Haskell infixl 7 "*") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
532 |
(Scala infixl 8 "*") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
533 |
(Eval infixl 9 "*") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
534 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
535 |
code_const Code_Numeral_Types.divmod_abs |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
536 |
(SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
537 |
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
538 |
(Haskell "divMod/ (abs _)/ (abs _)") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
539 |
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
540 |
(Eval "Integer.div'_mod/ (abs _)/ (abs _)") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
541 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
542 |
code_const "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
543 |
(SML "!((_ : IntInf.int) = _)") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
544 |
(OCaml "Big'_int.eq'_big'_int") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
545 |
(Haskell infix 4 "==") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
546 |
(Scala infixl 5 "==") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
547 |
(Eval infixl 6 "=") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
548 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
549 |
code_const "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
550 |
(SML "IntInf.<= ((_), (_))") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
551 |
(OCaml "Big'_int.le'_big'_int") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
552 |
(Haskell infix 4 "<=") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
553 |
(Scala infixl 4 "<=") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
554 |
(Eval infixl 6 "<=") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
555 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
556 |
code_const "less :: integer \<Rightarrow> _ \<Rightarrow> bool" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
557 |
(SML "IntInf.< ((_), (_))") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
558 |
(OCaml "Big'_int.lt'_big'_int") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
559 |
(Haskell infix 4 "<") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
560 |
(Scala infixl 4 "<") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
561 |
(Eval infixl 6 "<") |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
562 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
563 |
code_modulename SML |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
564 |
Code_Numeral_Types Arith |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
565 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
566 |
code_modulename OCaml |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
567 |
Code_Numeral_Types Arith |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
568 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
569 |
code_modulename Haskell |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
570 |
Code_Numeral_Types Arith |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
571 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
572 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
573 |
subsection {* Type of target language naturals *} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
574 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
575 |
typedef natural = "UNIV \<Colon> nat set" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
576 |
morphisms nat_of_natural natural_of_nat .. |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
577 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
578 |
lemma natural_eq_iff [termination_simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
579 |
"m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
580 |
using nat_of_natural_inject [of m n] .. |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
581 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
582 |
lemma natural_eqI: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
583 |
"nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
584 |
using natural_eq_iff [of m n] by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
585 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
586 |
lemma nat_of_natural_of_nat_inverse [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
587 |
"nat_of_natural (natural_of_nat n) = n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
588 |
using natural_of_nat_inverse [of n] by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
589 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
590 |
lemma natural_of_nat_of_natural_inverse [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
591 |
"natural_of_nat (nat_of_natural n) = n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
592 |
using nat_of_natural_inverse [of n] by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
593 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
594 |
instantiation natural :: "{comm_monoid_diff, semiring_1}" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
595 |
begin |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
596 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
597 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
598 |
"0 = natural_of_nat 0" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
599 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
600 |
lemma nat_of_natural_zero [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
601 |
"nat_of_natural 0 = 0" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
602 |
by (simp add: zero_natural_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
603 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
604 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
605 |
"1 = natural_of_nat 1" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
606 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
607 |
lemma nat_of_natural_one [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
608 |
"nat_of_natural 1 = 1" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
609 |
by (simp add: one_natural_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
610 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
611 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
612 |
"m + n = natural_of_nat (nat_of_natural m + nat_of_natural n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
613 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
614 |
lemma nat_of_natural_plus [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
615 |
"nat_of_natural (m + n) = nat_of_natural m + nat_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
616 |
by (simp add: plus_natural_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
617 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
618 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
619 |
"m - n = natural_of_nat (nat_of_natural m - nat_of_natural n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
620 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
621 |
lemma nat_of_natural_minus [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
622 |
"nat_of_natural (m - n) = nat_of_natural m - nat_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
623 |
by (simp add: minus_natural_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
624 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
625 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
626 |
"m * n = natural_of_nat (nat_of_natural m * nat_of_natural n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
627 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
628 |
lemma nat_of_natural_times [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
629 |
"nat_of_natural (m * n) = nat_of_natural m * nat_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
630 |
by (simp add: times_natural_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
631 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
632 |
instance proof |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
633 |
qed (auto simp add: natural_eq_iff algebra_simps) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
634 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
635 |
end |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
636 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
637 |
lemma nat_of_natural_of_nat [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
638 |
"nat_of_natural (of_nat n) = n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
639 |
by (induct n) simp_all |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
640 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
641 |
lemma natural_of_nat_of_nat [simp, code_abbrev]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
642 |
"natural_of_nat = of_nat" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
643 |
by rule (simp add: natural_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
644 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
645 |
lemma of_nat_of_natural [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
646 |
"of_nat (nat_of_natural n) = n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
647 |
using natural_of_nat_of_natural_inverse [of n] by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
648 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
649 |
lemma nat_of_natural_numeral [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
650 |
"nat_of_natural (numeral k) = numeral k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
651 |
using nat_of_natural_of_nat [of "numeral k"] by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
652 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
653 |
instantiation natural :: "{semiring_div, equal, linordered_semiring}" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
654 |
begin |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
655 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
656 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
657 |
"m div n = natural_of_nat (nat_of_natural m div nat_of_natural n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
658 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
659 |
lemma nat_of_natural_div [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
660 |
"nat_of_natural (m div n) = nat_of_natural m div nat_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
661 |
by (simp add: div_natural_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
662 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
663 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
664 |
"m mod n = natural_of_nat (nat_of_natural m mod nat_of_natural n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
665 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
666 |
lemma nat_of_natural_mod [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
667 |
"nat_of_natural (m mod n) = nat_of_natural m mod nat_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
668 |
by (simp add: mod_natural_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
669 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
670 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
671 |
[termination_simp]: "m \<le> n \<longleftrightarrow> nat_of_natural m \<le> nat_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
672 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
673 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
674 |
[termination_simp]: "m < n \<longleftrightarrow> nat_of_natural m < nat_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
675 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
676 |
definition |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
677 |
"HOL.equal m n \<longleftrightarrow> HOL.equal (nat_of_natural m) (nat_of_natural n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
678 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
679 |
instance proof |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
680 |
qed (auto simp add: natural_eq_iff algebra_simps |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
681 |
less_eq_natural_def less_natural_def equal_natural_def equal) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
682 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
683 |
end |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
684 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
685 |
lemma nat_of_natural_min [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
686 |
"nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
687 |
by (simp add: min_def less_eq_natural_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
688 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
689 |
lemma nat_of_natural_max [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
690 |
"nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
691 |
by (simp add: max_def less_eq_natural_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
692 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
693 |
definition natural_of_integer :: "integer \<Rightarrow> natural" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
694 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
695 |
"natural_of_integer = of_nat \<circ> nat_of_integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
696 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
697 |
definition integer_of_natural :: "natural \<Rightarrow> integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
698 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
699 |
"integer_of_natural = of_nat \<circ> nat_of_natural" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
700 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
701 |
lemma natural_of_integer_of_natural [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
702 |
"natural_of_integer (integer_of_natural n) = n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
703 |
by (simp add: natural_of_integer_def integer_of_natural_def natural_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
704 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
705 |
lemma integer_of_natural_of_integer [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
706 |
"integer_of_natural (natural_of_integer k) = max 0 k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
707 |
by (simp add: natural_of_integer_def integer_of_natural_def integer_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
708 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
709 |
lemma int_of_integer_of_natural [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
710 |
"int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
711 |
by (simp add: integer_of_natural_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
712 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
713 |
lemma integer_of_natural_of_nat [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
714 |
"integer_of_natural (of_nat n) = of_nat n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
715 |
by (simp add: integer_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
716 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
717 |
lemma [measure_function]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
718 |
"is_measure nat_of_natural" by (rule is_measure_trivial) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
719 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
720 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
721 |
subsection {* Inductive represenation of target language naturals *} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
722 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
723 |
definition Suc :: "natural \<Rightarrow> natural" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
724 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
725 |
"Suc = natural_of_nat \<circ> Nat.Suc \<circ> nat_of_natural" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
726 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
727 |
lemma nat_of_natural_Suc [simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
728 |
"nat_of_natural (Suc n) = Nat.Suc (nat_of_natural n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
729 |
by (simp add: Suc_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
730 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
731 |
rep_datatype "0::natural" Suc |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
732 |
proof - |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
733 |
fix P :: "natural \<Rightarrow> bool" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
734 |
fix n :: natural |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
735 |
assume "P 0" then have init: "P (natural_of_nat 0)" by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
736 |
assume "\<And>n. P n \<Longrightarrow> P (Suc n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
737 |
then have "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (Suc (natural_of_nat n))" . |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
738 |
then have step: "\<And>n. P (natural_of_nat n) \<Longrightarrow> P (natural_of_nat (Nat.Suc n))" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
739 |
by (simp add: Suc_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
740 |
from init step have "P (natural_of_nat (nat_of_natural n))" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
741 |
by (rule nat.induct) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
742 |
with natural_of_nat_of_natural_inverse show "P n" by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
743 |
qed (simp_all add: natural_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
744 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
745 |
lemma natural_case [case_names nat, cases type: natural]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
746 |
fixes m :: natural |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
747 |
assumes "\<And>n. m = of_nat n \<Longrightarrow> P" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
748 |
shows P |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
749 |
by (rule assms [of "nat_of_natural m"]) simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
750 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
751 |
lemma [simp, code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
752 |
"natural_size = nat_of_natural" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
753 |
proof (rule ext) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
754 |
fix n |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
755 |
show "natural_size n = nat_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
756 |
by (induct n) simp_all |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
757 |
qed |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
758 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
759 |
lemma [simp, code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
760 |
"size = nat_of_natural" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
761 |
proof (rule ext) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
762 |
fix n |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
763 |
show "size n = nat_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
764 |
by (induct n) simp_all |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
765 |
qed |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
766 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
767 |
lemma natural_decr [termination_simp]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
768 |
"n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
769 |
by (simp add: natural_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
770 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
771 |
lemma natural_zero_minus_one: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
772 |
"(0::natural) - 1 = 0" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
773 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
774 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
775 |
lemma Suc_natural_minus_one: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
776 |
"Suc n - 1 = n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
777 |
by (simp add: natural_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
778 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
779 |
hide_const (open) Suc |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
780 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
781 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
782 |
subsection {* Code refinement for target language naturals *} |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
783 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
784 |
definition Nat :: "integer \<Rightarrow> natural" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
785 |
where |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
786 |
"Nat = natural_of_integer" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
787 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
788 |
lemma [code abstype]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
789 |
"Nat (integer_of_natural n) = n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
790 |
by (unfold Nat_def) (fact natural_of_integer_of_natural) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
791 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
792 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
793 |
"integer_of_natural (natural_of_nat n) = of_nat n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
794 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
795 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
796 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
797 |
"integer_of_natural (natural_of_integer k) = max 0 k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
798 |
by simp |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
799 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
800 |
lemma [code_abbrev]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
801 |
"natural_of_integer (Code_Numeral_Types.Pos k) = numeral k" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
802 |
by (simp add: nat_of_integer_def natural_of_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
803 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
804 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
805 |
"integer_of_natural 0 = 0" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
806 |
by (simp add: integer_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
807 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
808 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
809 |
"integer_of_natural 1 = 1" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
810 |
by (simp add: integer_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
811 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
812 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
813 |
"integer_of_natural (Code_Numeral_Types.Suc n) = integer_of_natural n + 1" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
814 |
by (simp add: integer_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
815 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
816 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
817 |
"nat_of_natural = nat_of_integer \<circ> integer_of_natural" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
818 |
by (simp add: integer_of_natural_def fun_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
819 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
820 |
lemma [code, code_unfold]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
821 |
"natural_case f g n = (if n = 0 then f else g (n - 1))" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
822 |
by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
823 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
824 |
declare natural.recs [code del] |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
825 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
826 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
827 |
"integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
828 |
by (simp add: integer_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
829 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
830 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
831 |
"integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
832 |
by (simp add: integer_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
833 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
834 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
835 |
"integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
836 |
by (simp add: integer_eq_iff of_nat_mult) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
837 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
838 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
839 |
"integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
840 |
by (simp add: integer_eq_iff zdiv_int) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
841 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
842 |
lemma [code abstract]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
843 |
"integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
844 |
by (simp add: integer_eq_iff zmod_int) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
845 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
846 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
847 |
"HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
848 |
by (simp add: equal natural_eq_iff integer_eq_iff) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
849 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
850 |
lemma [code nbe]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
851 |
"HOL.equal n (n::natural) \<longleftrightarrow> True" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
852 |
by (simp add: equal) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
853 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
854 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
855 |
"m \<le> n \<longleftrightarrow> (integer_of_natural m) \<le> integer_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
856 |
by (simp add: less_eq_natural_def less_eq_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
857 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
858 |
lemma [code]: |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
859 |
"m < n \<longleftrightarrow> (integer_of_natural m) < integer_of_natural n" |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
860 |
by (simp add: less_natural_def less_integer_def) |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
861 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
862 |
hide_const (open) Nat |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
863 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
864 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
865 |
code_reflect Code_Numeral_Types |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
866 |
datatypes natural = _ |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
867 |
functions integer_of_natural natural_of_integer |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
868 |
|
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
869 |
end |
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
diff
changeset
|
870 |