src/HOL/ex/Transfer_Int_Nat.thy
author huffman
Sat Apr 21 13:49:31 2012 +0200 (2012-04-21)
changeset 47654 f7df7104d13e
child 51956 a4d81cdebf8b
permissions -rw-r--r--
new example theory for transfer package
huffman@47654
     1
(*  Title:      HOL/ex/Transfer_Int_Nat.thy
huffman@47654
     2
    Author:     Brian Huffman, TU Muenchen
huffman@47654
     3
*)
huffman@47654
     4
huffman@47654
     5
header {* Using the transfer method between nat and int *}
huffman@47654
     6
huffman@47654
     7
theory Transfer_Int_Nat
huffman@47654
     8
imports GCD "~~/src/HOL/Library/Quotient_List"
huffman@47654
     9
begin
huffman@47654
    10
huffman@47654
    11
subsection {* Correspondence relation *}
huffman@47654
    12
huffman@47654
    13
definition ZN :: "int \<Rightarrow> nat \<Rightarrow> bool"
huffman@47654
    14
  where "ZN = (\<lambda>z n. z = of_nat n)"
huffman@47654
    15
huffman@47654
    16
subsection {* Transfer rules *}
huffman@47654
    17
huffman@47654
    18
lemma bi_unique_ZN [transfer_rule]: "bi_unique ZN"
huffman@47654
    19
  unfolding ZN_def bi_unique_def by simp
huffman@47654
    20
huffman@47654
    21
lemma right_total_ZN [transfer_rule]: "right_total ZN"
huffman@47654
    22
  unfolding ZN_def right_total_def by simp
huffman@47654
    23
huffman@47654
    24
lemma ZN_0 [transfer_rule]: "ZN 0 0"
huffman@47654
    25
  unfolding ZN_def by simp
huffman@47654
    26
huffman@47654
    27
lemma ZN_1 [transfer_rule]: "ZN 1 1"
huffman@47654
    28
  unfolding ZN_def by simp
huffman@47654
    29
huffman@47654
    30
lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (op +) (op +)"
huffman@47654
    31
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    32
huffman@47654
    33
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (op *) (op *)"
huffman@47654
    34
  unfolding fun_rel_def ZN_def by (simp add: int_mult)
huffman@47654
    35
huffman@47654
    36
lemma ZN_diff [transfer_rule]: "(ZN ===> ZN ===> ZN) tsub (op -)"
huffman@47654
    37
  unfolding fun_rel_def ZN_def tsub_def by (simp add: zdiff_int)
huffman@47654
    38
huffman@47654
    39
lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
huffman@47654
    40
  unfolding fun_rel_def ZN_def by (simp add: int_power)
huffman@47654
    41
huffman@47654
    42
lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
huffman@47654
    43
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    44
huffman@47654
    45
lemma ZN_id_int [transfer_rule]: "(ZN ===> op =) id int"
huffman@47654
    46
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    47
huffman@47654
    48
lemma ZN_All [transfer_rule]:
huffman@47654
    49
  "((ZN ===> op =) ===> op =) (Ball {0..}) All"
huffman@47654
    50
  unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
huffman@47654
    51
huffman@47654
    52
lemma ZN_transfer_forall [transfer_rule]:
huffman@47654
    53
  "((ZN ===> op =) ===> op =) (transfer_bforall (\<lambda>x. 0 \<le> x)) transfer_forall"
huffman@47654
    54
  unfolding transfer_forall_def transfer_bforall_def
huffman@47654
    55
  unfolding fun_rel_def ZN_def by (auto dest: zero_le_imp_eq_int)
huffman@47654
    56
huffman@47654
    57
lemma ZN_Ex [transfer_rule]: "((ZN ===> op =) ===> op =) (Bex {0..}) Ex"
huffman@47654
    58
  unfolding fun_rel_def ZN_def Bex_def atLeast_iff
huffman@47654
    59
  by (metis zero_le_imp_eq_int zero_zle_int)
huffman@47654
    60
huffman@47654
    61
lemma ZN_le [transfer_rule]: "(ZN ===> ZN ===> op =) (op \<le>) (op \<le>)"
huffman@47654
    62
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    63
huffman@47654
    64
lemma ZN_less [transfer_rule]: "(ZN ===> ZN ===> op =) (op <) (op <)"
huffman@47654
    65
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    66
huffman@47654
    67
lemma ZN_eq [transfer_rule]: "(ZN ===> ZN ===> op =) (op =) (op =)"
huffman@47654
    68
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    69
huffman@47654
    70
lemma ZN_Suc [transfer_rule]: "(ZN ===> ZN) (\<lambda>x. x + 1) Suc"
huffman@47654
    71
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    72
huffman@47654
    73
lemma ZN_numeral [transfer_rule]:
huffman@47654
    74
  "(op = ===> ZN) numeral numeral"
huffman@47654
    75
  unfolding fun_rel_def ZN_def by simp
huffman@47654
    76
huffman@47654
    77
lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
huffman@47654
    78
  unfolding fun_rel_def ZN_def by (simp add: zdvd_int)
huffman@47654
    79
huffman@47654
    80
lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
huffman@47654
    81
  unfolding fun_rel_def ZN_def by (simp add: zdiv_int)
huffman@47654
    82
huffman@47654
    83
lemma ZN_mod [transfer_rule]: "(ZN ===> ZN ===> ZN) (op mod) (op mod)"
huffman@47654
    84
  unfolding fun_rel_def ZN_def by (simp add: zmod_int)
huffman@47654
    85
huffman@47654
    86
lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
huffman@47654
    87
  unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
huffman@47654
    88
huffman@47654
    89
text {* For derived operations, we can use the @{text "transfer_prover"}
huffman@47654
    90
  method to help generate transfer rules. *}
huffman@47654
    91
huffman@47654
    92
lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
huffman@47654
    93
  unfolding listsum_def [abs_def] by transfer_prover
huffman@47654
    94
huffman@47654
    95
subsection {* Transfer examples *}
huffman@47654
    96
huffman@47654
    97
lemma
huffman@47654
    98
  assumes "\<And>i::int. 0 \<le> i \<Longrightarrow> i + 0 = i"
huffman@47654
    99
  shows "\<And>i::nat. i + 0 = i"
huffman@47654
   100
apply transfer
huffman@47654
   101
apply fact
huffman@47654
   102
done
huffman@47654
   103
huffman@47654
   104
lemma
huffman@47654
   105
  assumes "\<And>i k::int. \<lbrakk>0 \<le> i; 0 \<le> k; i < k\<rbrakk> \<Longrightarrow> \<exists>j\<in>{0..}. i + j = k"
huffman@47654
   106
  shows "\<And>i k::nat. i < k \<Longrightarrow> \<exists>j. i + j = k"
huffman@47654
   107
apply transfer
huffman@47654
   108
apply fact
huffman@47654
   109
done
huffman@47654
   110
huffman@47654
   111
lemma
huffman@47654
   112
  assumes "\<forall>x\<in>{0::int..}. \<forall>y\<in>{0..}. x * y div y = x"
huffman@47654
   113
  shows "\<forall>x y :: nat. x * y div y = x"
huffman@47654
   114
apply transfer
huffman@47654
   115
apply fact
huffman@47654
   116
done
huffman@47654
   117
huffman@47654
   118
lemma
huffman@47654
   119
  assumes "\<And>m n::int. \<lbrakk>0 \<le> m; 0 \<le> n; m * n = 0\<rbrakk> \<Longrightarrow> m = 0 \<or> n = 0"
huffman@47654
   120
  shows "m * n = (0::nat) \<Longrightarrow> m = 0 \<or> n = 0"
huffman@47654
   121
apply transfer
huffman@47654
   122
apply fact
huffman@47654
   123
done
huffman@47654
   124
huffman@47654
   125
lemma
huffman@47654
   126
  assumes "\<forall>x\<in>{0::int..}. \<exists>y\<in>{0..}. \<exists>z\<in>{0..}. x + 3 * y = 5 * z"
huffman@47654
   127
  shows "\<forall>x::nat. \<exists>y z. x + 3 * y = 5 * z"
huffman@47654
   128
apply transfer
huffman@47654
   129
apply fact
huffman@47654
   130
done
huffman@47654
   131
huffman@47654
   132
text {* The @{text "fixing"} option prevents generalization over the free
huffman@47654
   133
  variable @{text "n"}, allowing the local transfer rule to be used. *}
huffman@47654
   134
huffman@47654
   135
lemma
huffman@47654
   136
  assumes [transfer_rule]: "ZN x n"
huffman@47654
   137
  assumes "\<forall>i\<in>{0..}. i < x \<longrightarrow> 2 * i < 3 * x"
huffman@47654
   138
  shows "\<forall>i. i < n \<longrightarrow> 2 * i < 3 * n"
huffman@47654
   139
apply (transfer fixing: n)
huffman@47654
   140
apply fact
huffman@47654
   141
done
huffman@47654
   142
huffman@47654
   143
lemma
huffman@47654
   144
  assumes "gcd (2^i) (3^j) = (1::int)"
huffman@47654
   145
  shows "gcd (2^i) (3^j) = (1::nat)"
huffman@47654
   146
apply (transfer fixing: i j)
huffman@47654
   147
apply fact
huffman@47654
   148
done
huffman@47654
   149
huffman@47654
   150
lemma
huffman@47654
   151
  assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow> 
huffman@47654
   152
    listsum [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
huffman@47654
   153
  shows "listsum [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
huffman@47654
   154
apply transfer
huffman@47654
   155
apply fact
huffman@47654
   156
done
huffman@47654
   157
huffman@47654
   158
text {* Quantifiers over higher types (e.g. @{text "nat list"}) may
huffman@47654
   159
  generate @{text "Domainp"} assumptions when transferred. *}
huffman@47654
   160
huffman@47654
   161
lemma
huffman@47654
   162
  assumes "\<And>xs::int list. Domainp (list_all2 ZN) xs \<Longrightarrow>
huffman@47654
   163
    (listsum xs = 0) = list_all (\<lambda>x. x = 0) xs"
huffman@47654
   164
  shows "listsum xs = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) xs"
huffman@47654
   165
apply transfer
huffman@47654
   166
apply fact
huffman@47654
   167
done
huffman@47654
   168
huffman@47654
   169
text {* Equality on a higher type can be transferred if the relations
huffman@47654
   170
  involved are bi-unique. *}
huffman@47654
   171
huffman@47654
   172
lemma
huffman@47654
   173
  assumes "\<And>xs\<Colon>int list. \<lbrakk>Domainp (list_all2 ZN) xs; xs \<noteq> []\<rbrakk> \<Longrightarrow>
huffman@47654
   174
    listsum xs < listsum (map (\<lambda>x. x + 1) xs)"
huffman@47654
   175
  shows "xs \<noteq> [] \<Longrightarrow> listsum xs < listsum (map Suc xs)"
huffman@47654
   176
apply transfer
huffman@47654
   177
apply fact
huffman@47654
   178
done
huffman@47654
   179
huffman@47654
   180
end