src/HOL/Nat_Transfer.thy
changeset 33318 ddd97d9dfbfb
parent 32558 e6e1fc2e73cb
child 33340 a165b97f3658
     1.1 --- a/src/HOL/Nat_Transfer.thy	Thu Oct 29 08:14:39 2009 +0100
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Thu Oct 29 11:41:36 2009 +0100
     1.3 @@ -1,15 +1,26 @@
     1.4  
     1.5  (* Authors: Jeremy Avigad and Amine Chaieb *)
     1.6  
     1.7 -header {* Sets up transfer from nats to ints and back. *}
     1.8 +header {* Generic transfer machinery;  specific transfer from nats to ints and back. *}
     1.9  
    1.10  theory Nat_Transfer
    1.11 -imports Main Parity
    1.12 +imports Nat_Numeral
    1.13 +uses ("Tools/transfer.ML")
    1.14  begin
    1.15  
    1.16 +subsection {* Generic transfer machinery *}
    1.17 +
    1.18 +definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
    1.19 +  where "TransferMorphism a B \<longleftrightarrow> True"
    1.20 +
    1.21 +use "Tools/transfer.ML"
    1.22 +
    1.23 +setup Transfer.setup
    1.24 +
    1.25 +
    1.26  subsection {* Set up transfer from nat to int *}
    1.27  
    1.28 -(* set up transfer direction *)
    1.29 +text {* set up transfer direction *}
    1.30  
    1.31  lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
    1.32    by (simp add: TransferMorphism_def)
    1.33 @@ -20,7 +31,7 @@
    1.34    labels: natint
    1.35  ]
    1.36  
    1.37 -(* basic functions and relations *)
    1.38 +text {* basic functions and relations *}
    1.39  
    1.40  lemma transfer_nat_int_numerals:
    1.41      "(0::nat) = nat 0"
    1.42 @@ -43,31 +54,20 @@
    1.43      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
    1.44      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
    1.45      "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
    1.46 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
    1.47 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
    1.48    by (auto simp add: eq_nat_nat_iff nat_mult_distrib
    1.49 -      nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
    1.50 +      nat_power_eq tsub_def)
    1.51  
    1.52  lemma transfer_nat_int_function_closures:
    1.53      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
    1.54      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
    1.55      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
    1.56      "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
    1.57 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
    1.58 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
    1.59      "(0::int) >= 0"
    1.60      "(1::int) >= 0"
    1.61      "(2::int) >= 0"
    1.62      "(3::int) >= 0"
    1.63      "int z >= 0"
    1.64    apply (auto simp add: zero_le_mult_iff tsub_def)
    1.65 -  apply (case_tac "y = 0")
    1.66 -  apply auto
    1.67 -  apply (subst pos_imp_zdiv_nonneg_iff, auto)
    1.68 -  apply (case_tac "y = 0")
    1.69 -  apply force
    1.70 -  apply (rule pos_mod_sign)
    1.71 -  apply arith
    1.72  done
    1.73  
    1.74  lemma transfer_nat_int_relations:
    1.75 @@ -89,7 +89,21 @@
    1.76  ]
    1.77  
    1.78  
    1.79 -(* first-order quantifiers *)
    1.80 +text {* first-order quantifiers *}
    1.81 +
    1.82 +lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
    1.83 +  by (simp split add: split_nat)
    1.84 +
    1.85 +lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
    1.86 +proof
    1.87 +  assume "\<exists>x. P x"
    1.88 +  then obtain x where "P x" ..
    1.89 +  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
    1.90 +  then show "\<exists>x\<ge>0. P (nat x)" ..
    1.91 +next
    1.92 +  assume "\<exists>x\<ge>0. P (nat x)"
    1.93 +  then show "\<exists>x. P x" by auto
    1.94 +qed
    1.95  
    1.96  lemma transfer_nat_int_quantifiers:
    1.97      "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
    1.98 @@ -110,7 +124,7 @@
    1.99    cong: all_cong ex_cong]
   1.100  
   1.101  
   1.102 -(* if *)
   1.103 +text {* if *}
   1.104  
   1.105  lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
   1.106      nat (if P then x else y)"
   1.107 @@ -119,7 +133,7 @@
   1.108  declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
   1.109  
   1.110  
   1.111 -(* operations with sets *)
   1.112 +text {* operations with sets *}
   1.113  
   1.114  definition
   1.115    nat_set :: "int set \<Rightarrow> bool"
   1.116 @@ -132,8 +146,6 @@
   1.117      "A Un B = nat ` (int ` A Un int ` B)"
   1.118      "A Int B = nat ` (int ` A Int int ` B)"
   1.119      "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
   1.120 -    "{..n} = nat ` {0..int n}"
   1.121 -    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
   1.122    apply (rule card_image [symmetric])
   1.123    apply (auto simp add: inj_on_def image_def)
   1.124    apply (rule_tac x = "int x" in bexI)
   1.125 @@ -144,17 +156,12 @@
   1.126    apply auto
   1.127    apply (rule_tac x = "int x" in exI)
   1.128    apply auto
   1.129 -  apply (rule_tac x = "int x" in bexI)
   1.130 -  apply auto
   1.131 -  apply (rule_tac x = "int x" in bexI)
   1.132 -  apply auto
   1.133  done
   1.134  
   1.135  lemma transfer_nat_int_set_function_closures:
   1.136      "nat_set {}"
   1.137      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   1.138      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   1.139 -    "x >= 0 \<Longrightarrow> nat_set {x..y}"
   1.140      "nat_set {x. x >= 0 & P x}"
   1.141      "nat_set (int ` C)"
   1.142      "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
   1.143 @@ -167,7 +174,6 @@
   1.144      "(A = B) = (int ` A = int ` B)"
   1.145      "(A < B) = (int ` A < int ` B)"
   1.146      "(A <= B) = (int ` A <= int ` B)"
   1.147 -
   1.148    apply (rule iffI)
   1.149    apply (erule finite_imageI)
   1.150    apply (erule finite_imageD)
   1.151 @@ -194,7 +200,7 @@
   1.152  ]
   1.153  
   1.154  
   1.155 -(* setsum and setprod *)
   1.156 +text {* setsum and setprod *}
   1.157  
   1.158  (* this handles the case where the *domain* of f is nat *)
   1.159  lemma transfer_nat_int_sum_prod:
   1.160 @@ -262,52 +268,10 @@
   1.161      transfer_nat_int_sum_prod_closure
   1.162    cong: transfer_nat_int_sum_prod_cong]
   1.163  
   1.164 -(* lists *)
   1.165 -
   1.166 -definition
   1.167 -  embed_list :: "nat list \<Rightarrow> int list"
   1.168 -where
   1.169 -  "embed_list l = map int l";
   1.170 -
   1.171 -definition
   1.172 -  nat_list :: "int list \<Rightarrow> bool"
   1.173 -where
   1.174 -  "nat_list l = nat_set (set l)";
   1.175 -
   1.176 -definition
   1.177 -  return_list :: "int list \<Rightarrow> nat list"
   1.178 -where
   1.179 -  "return_list l = map nat l";
   1.180 -
   1.181 -thm nat_0_le;
   1.182 -
   1.183 -lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
   1.184 -    embed_list (return_list l) = l";
   1.185 -  unfolding embed_list_def return_list_def nat_list_def nat_set_def
   1.186 -  apply (induct l);
   1.187 -  apply auto;
   1.188 -done;
   1.189 -
   1.190 -lemma transfer_nat_int_list_functions:
   1.191 -  "l @ m = return_list (embed_list l @ embed_list m)"
   1.192 -  "[] = return_list []";
   1.193 -  unfolding return_list_def embed_list_def;
   1.194 -  apply auto;
   1.195 -  apply (induct l, auto);
   1.196 -  apply (induct m, auto);
   1.197 -done;
   1.198 -
   1.199 -(*
   1.200 -lemma transfer_nat_int_fold1: "fold f l x =
   1.201 -    fold (%x. f (nat x)) (embed_list l) x";
   1.202 -*)
   1.203 -
   1.204 -
   1.205 -
   1.206  
   1.207  subsection {* Set up transfer from int to nat *}
   1.208  
   1.209 -(* set up transfer direction *)
   1.210 +text {* set up transfer direction *}
   1.211  
   1.212  lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
   1.213    by (simp add: TransferMorphism_def)
   1.214 @@ -319,7 +283,11 @@
   1.215  ]
   1.216  
   1.217  
   1.218 -(* basic functions and relations *)
   1.219 +text {* basic functions and relations *}
   1.220 +
   1.221 +lemma UNIV_apply:
   1.222 +  "UNIV x = True"
   1.223 +  by (simp add: top_fun_eq top_bool_eq)
   1.224  
   1.225  definition
   1.226    is_nat :: "int \<Rightarrow> bool"
   1.227 @@ -338,17 +306,13 @@
   1.228      "(int x) * (int y) = int (x * y)"
   1.229      "tsub (int x) (int y) = int (x - y)"
   1.230      "(int x)^n = int (x^n)"
   1.231 -    "(int x) div (int y) = int (x div y)"
   1.232 -    "(int x) mod (int y) = int (x mod y)"
   1.233 -  by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
   1.234 +  by (auto simp add: int_mult tsub_def int_power)
   1.235  
   1.236  lemma transfer_int_nat_function_closures:
   1.237      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
   1.238      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
   1.239      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
   1.240      "is_nat x \<Longrightarrow> is_nat (x^n)"
   1.241 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
   1.242 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   1.243      "is_nat 0"
   1.244      "is_nat 1"
   1.245      "is_nat 2"
   1.246 @@ -361,12 +325,7 @@
   1.247      "(int x < int y) = (x < y)"
   1.248      "(int x <= int y) = (x <= y)"
   1.249      "(int x dvd int y) = (x dvd y)"
   1.250 -    "(even (int x)) = (even x)"
   1.251 -  by (auto simp add: zdvd_int even_nat_def)
   1.252 -
   1.253 -lemma UNIV_apply:
   1.254 -  "UNIV x = True"
   1.255 -  by (simp add: top_fun_eq top_bool_eq)
   1.256 +  by (auto simp add: zdvd_int)
   1.257  
   1.258  declare TransferMorphism_int_nat[transfer add return:
   1.259    transfer_int_nat_numerals
   1.260 @@ -377,7 +336,7 @@
   1.261  ]
   1.262  
   1.263  
   1.264 -(* first-order quantifiers *)
   1.265 +text {* first-order quantifiers *}
   1.266  
   1.267  lemma transfer_int_nat_quantifiers:
   1.268      "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
   1.269 @@ -392,7 +351,7 @@
   1.270    return: transfer_int_nat_quantifiers]
   1.271  
   1.272  
   1.273 -(* if *)
   1.274 +text {* if *}
   1.275  
   1.276  lemma int_if_cong: "(if P then (int x) else (int y)) =
   1.277      int (if P then x else y)"
   1.278 @@ -402,7 +361,7 @@
   1.279  
   1.280  
   1.281  
   1.282 -(* operations with sets *)
   1.283 +text {* operations with sets *}
   1.284  
   1.285  lemma transfer_int_nat_set_functions:
   1.286      "nat_set A \<Longrightarrow> card A = card (nat ` A)"
   1.287 @@ -410,7 +369,6 @@
   1.288      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
   1.289      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
   1.290      "{x. x >= 0 & P x} = int ` {x. P(int x)}"
   1.291 -    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
   1.292         (* need all variants of these! *)
   1.293    by (simp_all only: is_nat_def transfer_nat_int_set_functions
   1.294            transfer_nat_int_set_function_closures
   1.295 @@ -421,7 +379,6 @@
   1.296      "nat_set {}"
   1.297      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   1.298      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   1.299 -    "is_nat x \<Longrightarrow> nat_set {x..y}"
   1.300      "nat_set {x. x >= 0 & P x}"
   1.301      "nat_set (int ` C)"
   1.302      "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
   1.303 @@ -454,7 +411,7 @@
   1.304  ]
   1.305  
   1.306  
   1.307 -(* setsum and setprod *)
   1.308 +text {* setsum and setprod *}
   1.309  
   1.310  (* this handles the case where the *domain* of f is int *)
   1.311  lemma transfer_int_nat_sum_prod: