author  blanchet 
Thu, 06 Mar 2014 14:57:14 +0100  
changeset 55938  f20d1db5aa3c 
parent 53013  3fbcfa911863 
child 55945  e96383acecf9 
permissions  rwrr 
47654  1 
(* Title: HOL/ex/Transfer_Int_Nat.thy 
2 
Author: Brian Huffman, TU Muenchen 

3 
*) 

4 

5 
header {* Using the transfer method between nat and int *} 

6 

7 
theory Transfer_Int_Nat 

53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset

8 
imports GCD 
47654  9 
begin 
10 

11 
subsection {* Correspondence relation *} 

12 

13 
definition ZN :: "int \<Rightarrow> nat \<Rightarrow> bool" 

14 
where "ZN = (\<lambda>z n. z = of_nat n)" 

15 

51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset

16 
subsection {* Transfer domain rules *} 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset

17 

a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset

18 
lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\<lambda>x. x \<ge> 0)" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset

19 
unfolding ZN_def Domainp_iff[abs_def] by (auto intro: zero_le_imp_eq_int) 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset

20 

47654  21 
subsection {* Transfer rules *} 
22 

53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset

23 
context 
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset

24 
begin 
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset

25 
interpretation lifting_syntax . 
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset

26 

47654  27 
lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN" 
28 
unfolding ZN_def bi_unique_def by simp 

29 

30 
lemma right_total_ZN [transfer_rule]: "right_total ZN" 

31 
unfolding ZN_def right_total_def by simp 

32 

33 
lemma ZN_0 [transfer_rule]: "ZN 0 0" 

34 
unfolding ZN_def by simp 

35 

36 
lemma ZN_1 [transfer_rule]: "ZN 1 1" 

37 
unfolding ZN_def by simp 

38 

39 
lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)" 

40 
unfolding fun_rel_def ZN_def by simp 

41 

42 
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)" 

43 
unfolding fun_rel_def ZN_def by (simp add: int_mult) 

44 

45 
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op )" 

46 
unfolding fun_rel_def ZN_def tsub_def by (simp add: zdiff_int) 

47 

48 
lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)" 

49 
unfolding fun_rel_def ZN_def by (simp add: int_power) 

50 

51 
lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id" 

52 
unfolding fun_rel_def ZN_def by simp 

53 

54 
lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int" 

55 
unfolding fun_rel_def ZN_def by simp 

56 

57 
lemma ZN_All [transfer_rule]: 

58 
"((ZN ===> op =) ===> op =) (Ball {0..}) All" 

59 
unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int) 

60 

61 
lemma ZN_transfer_forall [transfer_rule]: 

62 
"((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall" 

63 
unfolding transfer_forall_def transfer_bforall_def 

64 
unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int) 

65 

66 
lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex" 

67 
unfolding fun_rel_def ZN_def Bex_def atLeast_iff 

68 
by (metis zero_le_imp_eq_int zero_zle_int) 

69 

70 
lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)" 

71 
unfolding fun_rel_def ZN_def by simp 

72 

73 
lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)" 

74 
unfolding fun_rel_def ZN_def by simp 

75 

76 
lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)" 

77 
unfolding fun_rel_def ZN_def by simp 

78 

79 
lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc" 

80 
unfolding fun_rel_def ZN_def by simp 

81 

82 
lemma ZN_numeral [transfer_rule]: 

83 
"(op = ===> ZN) numeral numeral" 

84 
unfolding fun_rel_def ZN_def by simp 

85 

86 
lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)" 

87 
unfolding fun_rel_def ZN_def by (simp add: zdvd_int) 

88 

89 
lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)" 

90 
unfolding fun_rel_def ZN_def by (simp add: zdiv_int) 

91 

92 
lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)" 

93 
unfolding fun_rel_def ZN_def by (simp add: zmod_int) 

94 

95 
lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd" 

96 
unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd) 

97 

52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

98 
lemma ZN_atMost [transfer_rule]: 
55938  99 
"(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost" 
100 
unfolding fun_rel_def ZN_def rel_set_def 

52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

101 
by (clarsimp simp add: Bex_def, arith) 
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

102 

ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

103 
lemma ZN_atLeastAtMost [transfer_rule]: 
55938  104 
"(ZN ===> ZN ===> rel_set ZN) atLeastAtMost atLeastAtMost" 
105 
unfolding fun_rel_def ZN_def rel_set_def 

52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

106 
by (clarsimp simp add: Bex_def, arith) 
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

107 

ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

108 
lemma ZN_setsum [transfer_rule]: 
55938  109 
"bi_unique A \<Longrightarrow> ((A ===> ZN) ===> rel_set A ===> ZN) setsum setsum" 
52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

110 
apply (intro fun_relI) 
55938  111 
apply (erule (1) bi_unique_rel_set_lemma) 
52360
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

112 
apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def) 
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

113 
apply (rule setsum_cong2, simp) 
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

114 
done 
ac7ac2b242a2
more int/nat transfer rules; examples of new untransferred attribute
huffman
parents:
51956
diff
changeset

115 

47654  116 
text {* For derived operations, we can use the @{text "transfer_prover"} 
117 
method to help generate transfer rules. *} 

118 

119 
lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum" 

120 
unfolding listsum_def [abs_def] by transfer_prover 

121 

53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset

122 
end 
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52360
diff
changeset

123 

47654  124 
subsection {* Transfer examples *} 
125 

126 
lemma 

127 
assumes "\<And>i::int. 0 \<le> i \<Longrightarrow> i + 0 = i" 

128 
shows "\<And>i::nat. i + 0 = i" 

129 
apply transfer 

130 
apply fact 

131 
done 

132 

133 
lemma 

134 
assumes "\<And>i k::int. \<lbrakk>0 \<le> i; 0 \<le> k; i < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{0..}. i + j = k" 

135 
shows "\<And>i k::nat. i < k \<Longrightarrow> \<exists>j. i + j = k" 

136 
apply transfer 

137 
apply fact 

138 
done 

139 

140 
lemma 

141 
assumes "\<forall>x\<in>{0::int..}. \<forall>y\<in>{0..}. x * y div y = x" 

142 
shows "\<forall>x y :: nat. x * y div y = x" 

143 
apply transfer 

144 
apply fact 

145 
done 

146 

147 
lemma 

148 
assumes "\<And>m n::int. \<lbrakk>0 \<le> m; 0 \<le> n; m * n = 0\<rbrakk> \<Longrightarrow> m = 0 \<or> n = 0" 

149 
shows "m * n = (0::nat) \<Longrightarrow> m = 0 \<or> n = 0" 

150 
apply transfer 

151 
apply fact 

152 
done 

153 

154 
lemma 

155 
assumes "\<forall>x\<in>{0::int..}. \<exists>y\<in>{0..}. \<exists>z\<in>{0..}. x + 3 * y = 5 * z" 

156 
shows "\<forall>x::nat. \<exists>y z. x + 3 * y = 5 * z" 

157 
apply transfer 

158 
apply fact 

159 
done 

160 

161 
text {* The @{text "fixing"} option prevents generalization over the free 

162 
variable @{text "n"}, allowing the local transfer rule to be used. *} 

163 

164 
lemma 

165 
assumes [transfer_rule]: "ZN x n" 

166 
assumes "\<forall>i\<in>{0..}. i < x \<longrightarrow> 2 * i < 3 * x" 

167 
shows "\<forall>i. i < n \<longrightarrow> 2 * i < 3 * n" 

168 
apply (transfer fixing: n) 

169 
apply fact 

170 
done 

171 

172 
lemma 

173 
assumes "gcd (2^i) (3^j) = (1::int)" 

174 
shows "gcd (2^i) (3^j) = (1::nat)" 

175 
apply (transfer fixing: i j) 

176 
apply fact 

177 
done 

178 

179 
lemma 

180 
assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow> 

181 
listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]" 

182 
shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]" 

183 
apply transfer 

184 
apply fact 

185 
done 

186 

51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset

187 
text {* Quantifiers over higher types (e.g. @{text "nat list"}) are 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset

188 
transferred to a readable formula thanks to the transfer domain rule @{thm Domainp_ZN} *} 
47654  189 

190 
lemma 

51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset

191 
assumes "\<And>xs::int list. list_all (\<lambda>x. x \<ge> 0) xs \<Longrightarrow> 
47654  192 
(listsum xs = 0) = list_all (\<lambda>x. x = 0) xs" 
193 
shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs" 

194 
apply transfer 

195 
apply fact 

196 
done 

197 

198 
text {* Equality on a higher type can be transferred if the relations 

199 
involved are biunique. *} 

200 

201 
lemma 

51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
47654
diff
changeset

202 
assumes "\<And>xs\<Colon>int list. \<lbrakk>list_all (\<lambda>x. x \<ge> 0) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> 
47654  203 
listsum xs < listsum (map (\<lambda>x. x + 1) xs)" 
204 
shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)" 

205 
apply transfer 

206 
apply fact 

207 
done 

208 

209 
end 