author  kuncar 
Tue, 25 Feb 2014 19:07:14 +0100  
changeset 55736  f1ed1e9cd080 
parent 55642  63beb38e9258 
child 55945  e96383acecf9 
permissions  rwrr 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

1 
(* Title: HOL/Code_Numeral.thy 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

2 
Author: Florian Haftmann, TU Muenchen 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

3 
*) 
24999  4 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

5 
header {* Numeric types for code generation onto target language numerals only *} 
24999  6 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

7 
theory Code_Numeral 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

8 
imports Nat_Transfer Divides Lifting 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

9 
begin 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

10 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

11 
subsection {* Type of target language integers *} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

12 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

13 
typedef integer = "UNIV \<Colon> int set" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

14 
morphisms int_of_integer integer_of_int .. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

15 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

16 
setup_lifting (no_code) type_definition_integer 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

17 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

18 
lemma integer_eq_iff: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

19 
"k = l \<longleftrightarrow> int_of_integer k = int_of_integer l" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

20 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

21 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

22 
lemma integer_eqI: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

23 
"int_of_integer k = int_of_integer l \<Longrightarrow> k = l" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

24 
using integer_eq_iff [of k l] by simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

25 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

26 
lemma int_of_integer_integer_of_int [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

27 
"int_of_integer (integer_of_int k) = k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

28 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

29 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

30 
lemma integer_of_int_int_of_integer [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

31 
"integer_of_int (int_of_integer k) = k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

32 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

33 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

34 
instantiation integer :: ring_1 
24999  35 
begin 
36 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

37 
lift_definition zero_integer :: integer 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

38 
is "0 :: int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

39 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

40 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

41 
declare zero_integer.rep_eq [simp] 
24999  42 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

43 
lift_definition one_integer :: integer 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

44 
is "1 :: int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

45 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

46 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

47 
declare one_integer.rep_eq [simp] 
24999  48 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

49 
lift_definition plus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

50 
is "plus :: int \<Rightarrow> int \<Rightarrow> int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

51 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

52 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

53 
declare plus_integer.rep_eq [simp] 
24999  54 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

55 
lift_definition uminus_integer :: "integer \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

56 
is "uminus :: int \<Rightarrow> int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

57 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

58 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

59 
declare uminus_integer.rep_eq [simp] 
24999  60 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

61 
lift_definition minus_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

62 
is "minus :: int \<Rightarrow> int \<Rightarrow> int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

63 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

64 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

65 
declare minus_integer.rep_eq [simp] 
24999  66 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

67 
lift_definition times_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

68 
is "times :: int \<Rightarrow> int \<Rightarrow> int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

69 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

70 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

71 
declare times_integer.rep_eq [simp] 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

72 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

73 
instance proof 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

74 
qed (transfer, simp add: algebra_simps)+ 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

75 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

76 
end 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

77 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

78 
lemma [transfer_rule]: 
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

79 
"fun_rel HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)" 
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

80 
by (unfold of_nat_def [abs_def]) transfer_prover 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

81 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

82 
lemma [transfer_rule]: 
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

83 
"fun_rel HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

84 
proof  
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

85 
have "fun_rel HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

86 
by (unfold of_int_of_nat [abs_def]) transfer_prover 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

87 
then show ?thesis by (simp add: id_def) 
24999  88 
qed 
89 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

90 
lemma [transfer_rule]: 
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

91 
"fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)" 
26140  92 
proof  
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

93 
have "fun_rel HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (\<lambda>n. of_int (numeral n))" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

94 
by transfer_prover 
26140  95 
then show ?thesis by simp 
96 
qed 

97 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

98 
lemma [transfer_rule]: 
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

99 
"fun_rel HOL.eq (fun_rel HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

100 
by (unfold Num.sub_def [abs_def]) transfer_prover 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

101 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

102 
lemma int_of_integer_of_nat [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

103 
"int_of_integer (of_nat n) = of_nat n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

104 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

105 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

106 
lift_definition integer_of_nat :: "nat \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

107 
is "of_nat :: nat \<Rightarrow> int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

108 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

109 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

110 
lemma integer_of_nat_eq_of_nat [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

111 
"integer_of_nat = of_nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

112 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

113 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

114 
lemma int_of_integer_integer_of_nat [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

115 
"int_of_integer (integer_of_nat n) = of_nat n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

116 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

117 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

118 
lift_definition nat_of_integer :: "integer \<Rightarrow> nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

119 
is Int.nat 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

120 
. 
26140  121 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

122 
lemma nat_of_integer_of_nat [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

123 
"nat_of_integer (of_nat n) = n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

124 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

125 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

126 
lemma int_of_integer_of_int [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

127 
"int_of_integer (of_int k) = k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

128 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

129 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

130 
lemma nat_of_integer_integer_of_nat [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

131 
"nat_of_integer (integer_of_nat n) = n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

132 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

133 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

134 
lemma integer_of_int_eq_of_int [simp, code_abbrev]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

135 
"integer_of_int = of_int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

136 
by transfer (simp add: fun_eq_iff) 
26140  137 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

138 
lemma of_int_integer_of [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

139 
"of_int (int_of_integer k) = (k :: integer)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

140 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

141 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

142 
lemma int_of_integer_numeral [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

143 
"int_of_integer (numeral k) = numeral k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

144 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

145 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

146 
lemma int_of_integer_sub [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

147 
"int_of_integer (Num.sub k l) = Num.sub k l" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

148 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

149 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

150 
instantiation integer :: "{ring_div, equal, linordered_idom}" 
26140  151 
begin 
152 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

153 
lift_definition div_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

154 
is "Divides.div :: int \<Rightarrow> int \<Rightarrow> int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

155 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

156 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

157 
declare div_integer.rep_eq [simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

158 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

159 
lift_definition mod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

160 
is "Divides.mod :: int \<Rightarrow> int \<Rightarrow> int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

161 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

162 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

163 
declare mod_integer.rep_eq [simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

164 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

165 
lift_definition abs_integer :: "integer \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

166 
is "abs :: int \<Rightarrow> int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

167 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

168 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

169 
declare abs_integer.rep_eq [simp] 
26140  170 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

171 
lift_definition sgn_integer :: "integer \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

172 
is "sgn :: int \<Rightarrow> int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

173 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

174 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

175 
declare sgn_integer.rep_eq [simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

176 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

177 
lift_definition less_eq_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

178 
is "less_eq :: int \<Rightarrow> int \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

179 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

180 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

181 
lift_definition less_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

182 
is "less :: int \<Rightarrow> int \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

183 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

184 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

185 
lift_definition equal_integer :: "integer \<Rightarrow> integer \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

186 
is "HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

187 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

188 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

189 
instance proof 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

190 
qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+ 
26140  191 

192 
end 

193 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

194 
lemma [transfer_rule]: 
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

195 
"fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

196 
by (unfold min_def [abs_def]) transfer_prover 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

197 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

198 
lemma [transfer_rule]: 
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

199 
"fun_rel pcr_integer (fun_rel pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

200 
by (unfold max_def [abs_def]) transfer_prover 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

201 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

202 
lemma int_of_integer_min [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

203 
"int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

204 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

205 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

206 
lemma int_of_integer_max [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

207 
"int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

208 
by transfer rule 
26140  209 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

210 
lemma nat_of_integer_non_positive [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

211 
"k \<le> 0 \<Longrightarrow> nat_of_integer k = 0" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

212 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

213 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

214 
lemma of_nat_of_integer [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

215 
"of_nat (nat_of_integer k) = max 0 k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

216 
by transfer auto 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

217 

53069
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

218 
instance integer :: semiring_numeral_div 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

219 
by intro_classes (transfer, 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

220 
fact semiring_numeral_div_class.diff_invert_add1 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

221 
semiring_numeral_div_class.le_add_diff_inverse2 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

222 
semiring_numeral_div_class.mult_div_cancel 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

223 
semiring_numeral_div_class.div_less 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

224 
semiring_numeral_div_class.mod_less 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

225 
semiring_numeral_div_class.div_positive 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

226 
semiring_numeral_div_class.mod_less_eq_dividend 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

227 
semiring_numeral_div_class.pos_mod_bound 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

228 
semiring_numeral_div_class.pos_mod_sign 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

229 
semiring_numeral_div_class.mod_mult2_eq 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

230 
semiring_numeral_div_class.div_mult2_eq 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

231 
semiring_numeral_div_class.discrete)+ 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

232 

55427
ff54d22fe357
make integer_of_char and char_of_integer work with NBE and code_simp
Andreas Lochbihler
parents:
54489
diff
changeset

233 
lemma integer_of_nat_0: "integer_of_nat 0 = 0" 
ff54d22fe357
make integer_of_char and char_of_integer work with NBE and code_simp
Andreas Lochbihler
parents:
54489
diff
changeset

234 
by transfer simp 
ff54d22fe357
make integer_of_char and char_of_integer work with NBE and code_simp
Andreas Lochbihler
parents:
54489
diff
changeset

235 

ff54d22fe357
make integer_of_char and char_of_integer work with NBE and code_simp
Andreas Lochbihler
parents:
54489
diff
changeset

236 
lemma integer_of_nat_1: "integer_of_nat 1 = 1" 
ff54d22fe357
make integer_of_char and char_of_integer work with NBE and code_simp
Andreas Lochbihler
parents:
54489
diff
changeset

237 
by transfer simp 
ff54d22fe357
make integer_of_char and char_of_integer work with NBE and code_simp
Andreas Lochbihler
parents:
54489
diff
changeset

238 

ff54d22fe357
make integer_of_char and char_of_integer work with NBE and code_simp
Andreas Lochbihler
parents:
54489
diff
changeset

239 
lemma integer_of_nat_numeral: 
ff54d22fe357
make integer_of_char and char_of_integer work with NBE and code_simp
Andreas Lochbihler
parents:
54489
diff
changeset

240 
"integer_of_nat (numeral n) = numeral n" 
ff54d22fe357
make integer_of_char and char_of_integer work with NBE and code_simp
Andreas Lochbihler
parents:
54489
diff
changeset

241 
by transfer simp 
26140  242 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

243 
subsection {* Code theorems for target language integers *} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

244 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

245 
text {* Constructors *} 
26140  246 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

247 
definition Pos :: "num \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

248 
where 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

249 
[simp, code_abbrev]: "Pos = numeral" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

250 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

251 
lemma [transfer_rule]: 
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

252 
"fun_rel HOL.eq pcr_integer numeral Pos" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

253 
by simp transfer_prover 
30245
e67f42ac1157
consequent rewrite of index_size, size [index] to nat_of; support pseudoprimrec sepcifications with fun
haftmann
parents:
29823
diff
changeset

254 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

255 
definition Neg :: "num \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

256 
where 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
53069
diff
changeset

257 
[simp, code_abbrev]: "Neg n =  Pos n" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

258 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

259 
lemma [transfer_rule]: 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
53069
diff
changeset

260 
"fun_rel HOL.eq pcr_integer (\<lambda>n.  numeral n) Neg" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
53069
diff
changeset

261 
by (simp add: Neg_def [abs_def]) transfer_prover 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

262 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

263 
code_datatype "0::integer" Pos Neg 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

264 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

265 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

266 
text {* Auxiliary operations *} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

267 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

268 
lift_definition dup :: "integer \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

269 
is "\<lambda>k::int. k + k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

270 
. 
26140  271 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

272 
lemma dup_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

273 
"dup 0 = 0" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

274 
"dup (Pos n) = Pos (Num.Bit0 n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

275 
"dup (Neg n) = Neg (Num.Bit0 n)" 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
53069
diff
changeset

276 
by (transfer, simp only: numeral_Bit0 minus_add_distrib)+ 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

277 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

278 
lift_definition sub :: "num \<Rightarrow> num \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

279 
is "\<lambda>m n. numeral m  numeral n :: int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

280 
. 
26140  281 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

282 
lemma sub_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

283 
"sub Num.One Num.One = 0" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

284 
"sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

285 
"sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

286 
"sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

287 
"sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

288 
"sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

289 
"sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

290 
"sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

291 
"sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n)  1" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

292 
by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+ 
28351  293 

24999  294 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

295 
text {* Implementations *} 
24999  296 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

297 
lemma one_integer_code [code, code_unfold]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

298 
"1 = Pos Num.One" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

299 
by simp 
24999  300 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

301 
lemma plus_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

302 
"k + 0 = (k::integer)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

303 
"0 + l = (l::integer)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

304 
"Pos m + Pos n = Pos (m + n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

305 
"Pos m + Neg n = sub m n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

306 
"Neg m + Pos n = sub n m" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

307 
"Neg m + Neg n = Neg (m + n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

308 
by (transfer, simp)+ 
24999  309 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

310 
lemma uminus_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

311 
"uminus 0 = (0::integer)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

312 
"uminus (Pos m) = Neg m" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

313 
"uminus (Neg m) = Pos m" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

314 
by simp_all 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

315 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

316 
lemma minus_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

317 
"k  0 = (k::integer)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

318 
"0  l = uminus (l::integer)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

319 
"Pos m  Pos n = sub m n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

320 
"Pos m  Neg n = Pos (m + n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

321 
"Neg m  Pos n = Neg (m + n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

322 
"Neg m  Neg n = sub n m" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

323 
by (transfer, simp)+ 
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
45694
diff
changeset

324 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

325 
lemma abs_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

326 
"\<bar>k\<bar> = (if (k::integer) < 0 then  k else k)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

327 
by simp 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

328 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

329 
lemma sgn_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

330 
"sgn k = (if k = 0 then 0 else if (k::integer) < 0 then  1 else 1)" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

331 
by simp 
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
45694
diff
changeset

332 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

333 
lemma times_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

334 
"k * 0 = (0::integer)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

335 
"0 * l = (0::integer)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

336 
"Pos m * Pos n = Pos (m * n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

337 
"Pos m * Neg n = Neg (m * n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

338 
"Neg m * Pos n = Neg (m * n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

339 
"Neg m * Neg n = Pos (m * n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

340 
by simp_all 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

341 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

342 
definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

343 
where 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

344 
"divmod_integer k l = (k div l, k mod l)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

345 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

346 
lemma fst_divmod [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

347 
"fst (divmod_integer k l) = k div l" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

348 
by (simp add: divmod_integer_def) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

349 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

350 
lemma snd_divmod [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

351 
"snd (divmod_integer k l) = k mod l" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

352 
by (simp add: divmod_integer_def) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

353 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

354 
definition divmod_abs :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

355 
where 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

356 
"divmod_abs k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

357 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

358 
lemma fst_divmod_abs [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

359 
"fst (divmod_abs k l) = \<bar>k\<bar> div \<bar>l\<bar>" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

360 
by (simp add: divmod_abs_def) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

361 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

362 
lemma snd_divmod_abs [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

363 
"snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

364 
by (simp add: divmod_abs_def) 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

365 

53069
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

366 
lemma divmod_abs_code [code]: 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

367 
"divmod_abs (Pos k) (Pos l) = divmod k l" 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

368 
"divmod_abs (Neg k) (Neg l) = divmod k l" 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

369 
"divmod_abs (Neg k) (Pos l) = divmod k l" 
d165213e3924
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
haftmann
parents:
52435
diff
changeset

370 
"divmod_abs (Pos k) (Neg l) = divmod k l" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

371 
"divmod_abs j 0 = (0, \<bar>j\<bar>)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

372 
"divmod_abs 0 j = (0, 0)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

373 
by (simp_all add: prod_eq_iff) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

374 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

375 
lemma divmod_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

376 
"divmod_integer k l = 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

377 
(if k = 0 then (0, 0) else if l = 0 then (0, k) else 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

378 
(apsnd \<circ> times \<circ> sgn) l (if sgn k = sgn l 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

379 
then divmod_abs k l 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

380 
else (let (r, s) = divmod_abs k l in 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

381 
if s = 0 then ( r, 0) else ( r  1, \<bar>l\<bar>  s))))" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

382 
proof  
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

383 
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" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

384 
by (auto simp add: sgn_if) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

385 
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 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

386 
show ?thesis 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
54489
diff
changeset

387 
by (simp add: prod_eq_iff integer_eq_iff case_prod_beta aux1) 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

388 
(auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

389 
qed 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

390 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

391 
lemma div_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

392 
"k div l = fst (divmod_integer k l)" 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

393 
by simp 
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

394 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

395 
lemma mod_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

396 
"k mod l = snd (divmod_integer k l)" 
25767  397 
by simp 
24999  398 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

399 
lemma equal_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

400 
"HOL.equal 0 (0::integer) \<longleftrightarrow> True" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

401 
"HOL.equal 0 (Pos l) \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

402 
"HOL.equal 0 (Neg l) \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

403 
"HOL.equal (Pos k) 0 \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

404 
"HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

405 
"HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

406 
"HOL.equal (Neg k) 0 \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

407 
"HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

408 
"HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

409 
by (simp_all add: equal) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

410 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

411 
lemma equal_integer_refl [code nbe]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

412 
"HOL.equal (k::integer) k \<longleftrightarrow> True" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

413 
by (fact equal_refl) 
31266  414 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

415 
lemma less_eq_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

416 
"0 \<le> (0::integer) \<longleftrightarrow> True" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

417 
"0 \<le> Pos l \<longleftrightarrow> True" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

418 
"0 \<le> Neg l \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

419 
"Pos k \<le> 0 \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

420 
"Pos k \<le> Pos l \<longleftrightarrow> k \<le> l" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

421 
"Pos k \<le> Neg l \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

422 
"Neg k \<le> 0 \<longleftrightarrow> True" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

423 
"Neg k \<le> Pos l \<longleftrightarrow> True" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

424 
"Neg k \<le> Neg l \<longleftrightarrow> l \<le> k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

425 
by simp_all 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

426 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

427 
lemma less_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

428 
"0 < (0::integer) \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

429 
"0 < Pos l \<longleftrightarrow> True" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

430 
"0 < Neg l \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

431 
"Pos k < 0 \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

432 
"Pos k < Pos l \<longleftrightarrow> k < l" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

433 
"Pos k < Neg l \<longleftrightarrow> False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

434 
"Neg k < 0 \<longleftrightarrow> True" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

435 
"Neg k < Pos l \<longleftrightarrow> True" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

436 
"Neg k < Neg l \<longleftrightarrow> l < k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

437 
by simp_all 
26140  438 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

439 
lift_definition integer_of_num :: "num \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

440 
is "numeral :: num \<Rightarrow> int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

441 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

442 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

443 
lemma integer_of_num [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

444 
"integer_of_num num.One = 1" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

445 
"integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

446 
"integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

447 
by (transfer, simp only: numeral.simps Let_def)+ 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

448 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

449 
lift_definition num_of_integer :: "integer \<Rightarrow> num" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

450 
is "num_of_nat \<circ> nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

451 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

452 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

453 
lemma num_of_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

454 
"num_of_integer k = (if k \<le> 1 then Num.One 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

455 
else let 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

456 
(l, j) = divmod_integer k 2; 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

457 
l' = num_of_integer l; 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

458 
l'' = l' + l' 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

459 
in if j = 0 then l'' else l'' + Num.One)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

460 
proof  
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

461 
{ 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

462 
assume "int_of_integer k mod 2 = 1" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

463 
then have "nat (int_of_integer k mod 2) = nat 1" by simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

464 
moreover assume *: "1 < int_of_integer k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

465 
ultimately have **: "nat (int_of_integer k) mod 2 = 1" by (simp add: nat_mod_distrib) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

466 
have "num_of_nat (nat (int_of_integer k)) = 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

467 
num_of_nat (2 * (nat (int_of_integer k) div 2) + nat (int_of_integer k) mod 2)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

468 
by simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

469 
then have "num_of_nat (nat (int_of_integer k)) = 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

470 
num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + nat (int_of_integer k) mod 2)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

471 
by (simp add: mult_2) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

472 
with ** have "num_of_nat (nat (int_of_integer k)) = 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

473 
num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + 1)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

474 
by simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

475 
} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

476 
note aux = this 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

477 
show ?thesis 
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
54489
diff
changeset

478 
by (auto simp add: num_of_integer_def nat_of_integer_def Let_def case_prod_beta 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

479 
not_le integer_eq_iff less_eq_integer_def 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

480 
nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

481 
mult_2 [where 'a=nat] aux add_One) 
25918  482 
qed 
483 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

484 
lemma nat_of_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

485 
"nat_of_integer k = (if k \<le> 0 then 0 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

486 
else let 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

487 
(l, j) = divmod_integer k 2; 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

488 
l' = nat_of_integer l; 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

489 
l'' = l' + l' 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

490 
in if j = 0 then l'' else l'' + 1)" 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

491 
proof  
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

492 
obtain j where "k = integer_of_int j" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

493 
proof 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

494 
show "k = integer_of_int (int_of_integer k)" by simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

495 
qed 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

496 
moreover have "2 * (j div 2) = j  j mod 2" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

497 
by (simp add: zmult_div_cancel mult_commute) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

498 
ultimately show ?thesis 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

499 
by (auto simp add: split_def Let_def mod_integer_def nat_of_integer_def not_le 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

500 
nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

501 
(auto simp add: mult_2 [symmetric]) 
33340
a165b97f3658
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33318
diff
changeset

502 
qed 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

503 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

504 
lemma int_of_integer_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

505 
"int_of_integer k = (if k < 0 then  (int_of_integer ( k)) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

506 
else if k = 0 then 0 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

507 
else let 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

508 
(l, j) = divmod_integer k 2; 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

509 
l' = 2 * int_of_integer l 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

510 
in if j = 0 then l' else l' + 1)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

511 
by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel) 
28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

512 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

513 
lemma integer_of_int_code [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

514 
"integer_of_int k = (if k < 0 then  (integer_of_int ( k)) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

515 
else if k = 0 then 0 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

516 
else let 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

517 
(l, j) = divmod_int k 2; 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

518 
l' = 2 * integer_of_int l 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

519 
in if j = 0 then l' else l' + 1)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

520 
by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

521 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

522 
hide_const (open) Pos Neg sub dup divmod_abs 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

523 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

524 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

525 
subsection {* Serializer setup for target language integers *} 
24999  526 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

527 
code_reserved Eval int Integer abs 
25767  528 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

529 
code_printing 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

530 
type_constructor integer \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

531 
(SML) "IntInf.int" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

532 
and (OCaml) "Big'_int.big'_int" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

533 
and (Haskell) "Integer" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

534 
and (Scala) "BigInt" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

535 
and (Eval) "int" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

536 
 class_instance integer :: equal \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

537 
(Haskell)  
24999  538 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

539 
code_printing 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

540 
constant "0::integer" \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

541 
(SML) "0" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

542 
and (OCaml) "Big'_int.zero'_big'_int" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

543 
and (Haskell) "0" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

544 
and (Scala) "BigInt(0)" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46664
diff
changeset

545 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

546 
setup {* 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

547 
fold (Numeral.add_code @{const_name Code_Numeral.Pos} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

548 
false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

549 
*} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

550 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

551 
setup {* 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

552 
fold (Numeral.add_code @{const_name Code_Numeral.Neg} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

553 
true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

554 
*} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

555 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

556 
code_printing 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

557 
constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

558 
(SML) "IntInf.+ ((_), (_))" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

559 
and (OCaml) "Big'_int.add'_big'_int" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

560 
and (Haskell) infixl 6 "+" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

561 
and (Scala) infixl 7 "+" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

562 
and (Eval) infixl 8 "+" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

563 
 constant "uminus :: integer \<Rightarrow> _" \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

564 
(SML) "IntInf.~" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

565 
and (OCaml) "Big'_int.minus'_big'_int" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

566 
and (Haskell) "negate" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

567 
and (Scala) "!( _)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

568 
and (Eval) "~/ _" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

569 
 constant "minus :: integer \<Rightarrow> _" \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

570 
(SML) "IntInf. ((_), (_))" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

571 
and (OCaml) "Big'_int.sub'_big'_int" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

572 
and (Haskell) infixl 6 "" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

573 
and (Scala) infixl 7 "" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

574 
and (Eval) infixl 8 "" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

575 
 constant Code_Numeral.dup \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

576 
(SML) "IntInf.*/ (2,/ (_))" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

577 
and (OCaml) "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

578 
and (Haskell) "!(2 * _)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

579 
and (Scala) "!(2 * _)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

580 
and (Eval) "!(2 * _)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

581 
 constant Code_Numeral.sub \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

582 
(SML) "!(raise/ Fail/ \"sub\")" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

583 
and (OCaml) "failwith/ \"sub\"" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

584 
and (Haskell) "error/ \"sub\"" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

585 
and (Scala) "!sys.error(\"sub\")" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

586 
 constant "times :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

587 
(SML) "IntInf.* ((_), (_))" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

588 
and (OCaml) "Big'_int.mult'_big'_int" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

589 
and (Haskell) infixl 7 "*" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

590 
and (Scala) infixl 8 "*" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

591 
and (Eval) infixl 9 "*" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

592 
 constant Code_Numeral.divmod_abs \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

593 
(SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

594 
and (OCaml) "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

595 
and (Haskell) "divMod/ (abs _)/ (abs _)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

596 
and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

597 
and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

598 
 constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

599 
(SML) "!((_ : IntInf.int) = _)" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

600 
and (OCaml) "Big'_int.eq'_big'_int" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

601 
and (Haskell) infix 4 "==" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

602 
and (Scala) infixl 5 "==" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

603 
and (Eval) infixl 6 "=" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

604 
 constant "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

605 
(SML) "IntInf.<= ((_), (_))" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

606 
and (OCaml) "Big'_int.le'_big'_int" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

607 
and (Haskell) infix 4 "<=" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

608 
and (Scala) infixl 4 "<=" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

609 
and (Eval) infixl 6 "<=" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

610 
 constant "less :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup> 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

611 
(SML) "IntInf.< ((_), (_))" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

612 
and (OCaml) "Big'_int.lt'_big'_int" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

613 
and (Haskell) infix 4 "<" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

614 
and (Scala) infixl 4 "<" 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

615 
and (Eval) infixl 6 "<" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

616 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

617 
code_identifier 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
51375
diff
changeset

618 
code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46028
diff
changeset

619 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

620 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

621 
subsection {* Type of target language naturals *} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

622 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

623 
typedef natural = "UNIV \<Colon> nat set" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

624 
morphisms nat_of_natural natural_of_nat .. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

625 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

626 
setup_lifting (no_code) type_definition_natural 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

627 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

628 
lemma natural_eq_iff [termination_simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

629 
"m = n \<longleftrightarrow> nat_of_natural m = nat_of_natural n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

630 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

631 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

632 
lemma natural_eqI: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

633 
"nat_of_natural m = nat_of_natural n \<Longrightarrow> m = n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

634 
using natural_eq_iff [of m n] by simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

635 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

636 
lemma nat_of_natural_of_nat_inverse [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

637 
"nat_of_natural (natural_of_nat n) = n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

638 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

639 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

640 
lemma natural_of_nat_of_natural_inverse [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

641 
"natural_of_nat (nat_of_natural n) = n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

642 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

643 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

644 
instantiation natural :: "{comm_monoid_diff, semiring_1}" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

645 
begin 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

646 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

647 
lift_definition zero_natural :: natural 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

648 
is "0 :: nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

649 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

650 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

651 
declare zero_natural.rep_eq [simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

652 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

653 
lift_definition one_natural :: natural 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

654 
is "1 :: nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

655 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

656 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

657 
declare one_natural.rep_eq [simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

658 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

659 
lift_definition plus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

660 
is "plus :: nat \<Rightarrow> nat \<Rightarrow> nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

661 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

662 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

663 
declare plus_natural.rep_eq [simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

664 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

665 
lift_definition minus_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

666 
is "minus :: nat \<Rightarrow> nat \<Rightarrow> nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

667 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

668 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

669 
declare minus_natural.rep_eq [simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

670 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

671 
lift_definition times_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

672 
is "times :: nat \<Rightarrow> nat \<Rightarrow> nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

673 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

674 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

675 
declare times_natural.rep_eq [simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

676 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

677 
instance proof 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

678 
qed (transfer, simp add: algebra_simps)+ 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

679 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

680 
end 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

681 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

682 
lemma [transfer_rule]: 
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

683 
"fun_rel HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

684 
proof  
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

685 
have "fun_rel HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

686 
by (unfold of_nat_def [abs_def]) transfer_prover 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

687 
then show ?thesis by (simp add: id_def) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

688 
qed 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

689 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

690 
lemma [transfer_rule]: 
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

691 
"fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

692 
proof  
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

693 
have "fun_rel HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

694 
by transfer_prover 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

695 
then show ?thesis by simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

696 
qed 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

697 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

698 
lemma nat_of_natural_of_nat [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

699 
"nat_of_natural (of_nat n) = n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

700 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

701 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

702 
lemma natural_of_nat_of_nat [simp, code_abbrev]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

703 
"natural_of_nat = of_nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

704 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

705 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

706 
lemma of_nat_of_natural [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

707 
"of_nat (nat_of_natural n) = n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

708 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

709 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

710 
lemma nat_of_natural_numeral [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

711 
"nat_of_natural (numeral k) = numeral k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

712 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

713 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

714 
instantiation natural :: "{semiring_div, equal, linordered_semiring}" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

715 
begin 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

716 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

717 
lift_definition div_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

718 
is "Divides.div :: nat \<Rightarrow> nat \<Rightarrow> nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

719 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

720 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

721 
declare div_natural.rep_eq [simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

722 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

723 
lift_definition mod_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

724 
is "Divides.mod :: nat \<Rightarrow> nat \<Rightarrow> nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

725 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

726 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

727 
declare mod_natural.rep_eq [simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

728 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

729 
lift_definition less_eq_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

730 
is "less_eq :: nat \<Rightarrow> nat \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

731 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

732 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

733 
declare less_eq_natural.rep_eq [termination_simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

734 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

735 
lift_definition less_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

736 
is "less :: nat \<Rightarrow> nat \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

737 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

738 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

739 
declare less_natural.rep_eq [termination_simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

740 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

741 
lift_definition equal_natural :: "natural \<Rightarrow> natural \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

742 
is "HOL.equal :: nat \<Rightarrow> nat \<Rightarrow> bool" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

743 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

744 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

745 
instance proof 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

746 
qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+ 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

747 

24999  748 
end 
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

749 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

750 
lemma [transfer_rule]: 
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

751 
"fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

752 
by (unfold min_def [abs_def]) transfer_prover 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

753 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

754 
lemma [transfer_rule]: 
51375
d9e62d9c98de
patch Isabelle ditribution to conform to changes regarding the parametricity
kuncar
parents:
51143
diff
changeset

755 
"fun_rel pcr_natural (fun_rel pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

756 
by (unfold max_def [abs_def]) transfer_prover 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

757 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

758 
lemma nat_of_natural_min [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

759 
"nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

760 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

761 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

762 
lemma nat_of_natural_max [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

763 
"nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

764 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

765 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

766 
lift_definition natural_of_integer :: "integer \<Rightarrow> natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

767 
is "nat :: int \<Rightarrow> nat" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

768 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

769 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

770 
lift_definition integer_of_natural :: "natural \<Rightarrow> integer" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

771 
is "of_nat :: nat \<Rightarrow> int" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

772 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

773 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

774 
lemma natural_of_integer_of_natural [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

775 
"natural_of_integer (integer_of_natural n) = n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

776 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

777 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

778 
lemma integer_of_natural_of_integer [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

779 
"integer_of_natural (natural_of_integer k) = max 0 k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

780 
by transfer auto 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

781 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

782 
lemma int_of_integer_of_natural [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

783 
"int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

784 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

785 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

786 
lemma integer_of_natural_of_nat [simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

787 
"integer_of_natural (of_nat n) = of_nat n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

788 
by transfer rule 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

789 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

790 
lemma [measure_function]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

791 
"is_measure nat_of_natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

792 
by (rule is_measure_trivial) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

793 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

794 

55416  795 
subsection {* Inductive representation of target language naturals *} 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

796 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

797 
lift_definition Suc :: "natural \<Rightarrow> natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

798 
is Nat.Suc 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

799 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

800 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

801 
declare Suc.rep_eq [simp] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

802 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

803 
rep_datatype "0::natural" Suc 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

804 
by (transfer, fact nat.induct nat.inject nat.distinct)+ 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

805 

55416  806 
lemma natural_cases [case_names nat, cases type: natural]: 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

807 
fixes m :: natural 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

808 
assumes "\<And>n. m = of_nat n \<Longrightarrow> P" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

809 
shows P 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

810 
using assms by transfer blast 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

811 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

812 
lemma [simp, code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

813 
"natural_size = nat_of_natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

814 
proof (rule ext) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

815 
fix n 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

816 
show "natural_size n = nat_of_natural n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

817 
by (induct n) simp_all 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

818 
qed 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

819 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

820 
lemma [simp, code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

821 
"size = nat_of_natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

822 
proof (rule ext) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

823 
fix n 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

824 
show "size n = nat_of_natural n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

825 
by (induct n) simp_all 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

826 
qed 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

827 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

828 
lemma natural_decr [termination_simp]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

829 
"n \<noteq> 0 \<Longrightarrow> nat_of_natural n  Nat.Suc 0 < nat_of_natural n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

830 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

831 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

832 
lemma natural_zero_minus_one: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

833 
"(0::natural)  1 = 0" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

834 
by simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

835 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

836 
lemma Suc_natural_minus_one: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

837 
"Suc n  1 = n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

838 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

839 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

840 
hide_const (open) Suc 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

841 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

842 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

843 
subsection {* Code refinement for target language naturals *} 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

844 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

845 
lift_definition Nat :: "integer \<Rightarrow> natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

846 
is nat 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

847 
. 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

848 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

849 
lemma [code_post]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

850 
"Nat 0 = 0" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

851 
"Nat 1 = 1" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

852 
"Nat (numeral k) = numeral k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

853 
by (transfer, simp)+ 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

854 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

855 
lemma [code abstype]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

856 
"Nat (integer_of_natural n) = n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

857 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

858 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

859 
lemma [code abstract]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

860 
"integer_of_natural (natural_of_nat n) = of_nat n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

861 
by simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

862 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

863 
lemma [code abstract]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

864 
"integer_of_natural (natural_of_integer k) = max 0 k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

865 
by simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

866 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

867 
lemma [code_abbrev]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

868 
"natural_of_integer (Code_Numeral.Pos k) = numeral k" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

869 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

870 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

871 
lemma [code abstract]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

872 
"integer_of_natural 0 = 0" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

873 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

874 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

875 
lemma [code abstract]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

876 
"integer_of_natural 1 = 1" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

877 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

878 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

879 
lemma [code abstract]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

880 
"integer_of_natural (Code_Numeral.Suc n) = integer_of_natural n + 1" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

881 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

882 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

883 
lemma [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

884 
"nat_of_natural = nat_of_integer \<circ> integer_of_natural" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

885 
by transfer (simp add: fun_eq_iff) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

886 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

887 
lemma [code, code_unfold]: 
55416  888 
"case_natural f g n = (if n = 0 then f else g (n  1))" 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

889 
by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

890 

55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55428
diff
changeset

891 
declare natural.rec [code del] 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

892 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

893 
lemma [code abstract]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

894 
"integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

895 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

896 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

897 
lemma [code abstract]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

898 
"integer_of_natural (m  n) = max 0 (integer_of_natural m  integer_of_natural n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

899 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

900 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

901 
lemma [code abstract]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

902 
"integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

903 
by transfer (simp add: of_nat_mult) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

904 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

905 
lemma [code abstract]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

906 
"integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

907 
by transfer (simp add: zdiv_int) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

908 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

909 
lemma [code abstract]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

910 
"integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

911 
by transfer (simp add: zmod_int) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

912 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

913 
lemma [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

914 
"HOL.equal m n \<longleftrightarrow> HOL.equal (integer_of_natural m) (integer_of_natural n)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

915 
by transfer (simp add: equal) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

916 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

917 
lemma [code nbe]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

918 
"HOL.equal n (n::natural) \<longleftrightarrow> True" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

919 
by (simp add: equal) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

920 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

921 
lemma [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

922 
"m \<le> n \<longleftrightarrow> integer_of_natural m \<le> integer_of_natural n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

923 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

924 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

925 
lemma [code]: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

926 
"m < n \<longleftrightarrow> integer_of_natural m < integer_of_natural n" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

927 
by transfer simp 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

928 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

929 
hide_const (open) Nat 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

930 

55736
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
55642
diff
changeset

931 
lifting_update integer.lifting 
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
55642
diff
changeset

932 
lifting_forget integer.lifting 
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
55642
diff
changeset

933 

f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
55642
diff
changeset

934 
lifting_update natural.lifting 
f1ed1e9cd080
unregister lifting setup following the best practice of Lifting
kuncar
parents:
55642
diff
changeset

935 
lifting_forget natural.lifting 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

936 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

937 
code_reflect Code_Numeral 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

938 
datatypes natural = _ 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

939 
functions integer_of_natural natural_of_integer 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

940 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

941 
end 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
49962
diff
changeset

942 