obey underscore naming convention
authorhaftmann
Thu Sep 10 15:26:51 2009 +0200 (2009-09-10)
changeset 32558e6e1fc2e73cb
parent 32557 3cfe4c13aa6e
child 32559 6b5d478114f0
obey underscore naming convention
src/HOL/Fact.thy
src/HOL/IsaMakefile
src/HOL/NatTransfer.thy
src/HOL/Nat_Transfer.thy
     1.1 --- a/src/HOL/Fact.thy	Thu Sep 10 15:23:09 2009 +0200
     1.2 +++ b/src/HOL/Fact.thy	Thu Sep 10 15:26:51 2009 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  header{*Factorial Function*}
     1.5  
     1.6  theory Fact
     1.7 -imports NatTransfer
     1.8 +imports Nat_Transfer
     1.9  begin
    1.10  
    1.11  class fact =
     2.1 --- a/src/HOL/IsaMakefile	Thu Sep 10 15:23:09 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Thu Sep 10 15:26:51 2009 +0200
     2.3 @@ -291,7 +291,7 @@
     2.4    Log.thy \
     2.5    Lubs.thy \
     2.6    MacLaurin.thy \
     2.7 -  NatTransfer.thy \
     2.8 +  Nat_Transfer.thy \
     2.9    NthRoot.thy \
    2.10    SEQ.thy \
    2.11    Series.thy \
     3.1 --- a/src/HOL/NatTransfer.thy	Thu Sep 10 15:23:09 2009 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,484 +0,0 @@
     3.4 -
     3.5 -(* Authors: Jeremy Avigad and Amine Chaieb *)
     3.6 -
     3.7 -header {* Sets up transfer from nats to ints and back. *}
     3.8 -
     3.9 -theory NatTransfer
    3.10 -imports Main Parity
    3.11 -begin
    3.12 -
    3.13 -subsection {* Set up transfer from nat to int *}
    3.14 -
    3.15 -(* set up transfer direction *)
    3.16 -
    3.17 -lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
    3.18 -  by (simp add: TransferMorphism_def)
    3.19 -
    3.20 -declare TransferMorphism_nat_int[transfer
    3.21 -  add mode: manual
    3.22 -  return: nat_0_le
    3.23 -  labels: natint
    3.24 -]
    3.25 -
    3.26 -(* basic functions and relations *)
    3.27 -
    3.28 -lemma transfer_nat_int_numerals:
    3.29 -    "(0::nat) = nat 0"
    3.30 -    "(1::nat) = nat 1"
    3.31 -    "(2::nat) = nat 2"
    3.32 -    "(3::nat) = nat 3"
    3.33 -  by auto
    3.34 -
    3.35 -definition
    3.36 -  tsub :: "int \<Rightarrow> int \<Rightarrow> int"
    3.37 -where
    3.38 -  "tsub x y = (if x >= y then x - y else 0)"
    3.39 -
    3.40 -lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
    3.41 -  by (simp add: tsub_def)
    3.42 -
    3.43 -
    3.44 -lemma transfer_nat_int_functions:
    3.45 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
    3.46 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
    3.47 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
    3.48 -    "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
    3.49 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
    3.50 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
    3.51 -  by (auto simp add: eq_nat_nat_iff nat_mult_distrib
    3.52 -      nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
    3.53 -
    3.54 -lemma transfer_nat_int_function_closures:
    3.55 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
    3.56 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
    3.57 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
    3.58 -    "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
    3.59 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
    3.60 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
    3.61 -    "(0::int) >= 0"
    3.62 -    "(1::int) >= 0"
    3.63 -    "(2::int) >= 0"
    3.64 -    "(3::int) >= 0"
    3.65 -    "int z >= 0"
    3.66 -  apply (auto simp add: zero_le_mult_iff tsub_def)
    3.67 -  apply (case_tac "y = 0")
    3.68 -  apply auto
    3.69 -  apply (subst pos_imp_zdiv_nonneg_iff, auto)
    3.70 -  apply (case_tac "y = 0")
    3.71 -  apply force
    3.72 -  apply (rule pos_mod_sign)
    3.73 -  apply arith
    3.74 -done
    3.75 -
    3.76 -lemma transfer_nat_int_relations:
    3.77 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    3.78 -      (nat (x::int) = nat y) = (x = y)"
    3.79 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    3.80 -      (nat (x::int) < nat y) = (x < y)"
    3.81 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    3.82 -      (nat (x::int) <= nat y) = (x <= y)"
    3.83 -    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    3.84 -      (nat (x::int) dvd nat y) = (x dvd y)"
    3.85 -  by (auto simp add: zdvd_int even_nat_def)
    3.86 -
    3.87 -declare TransferMorphism_nat_int[transfer add return:
    3.88 -  transfer_nat_int_numerals
    3.89 -  transfer_nat_int_functions
    3.90 -  transfer_nat_int_function_closures
    3.91 -  transfer_nat_int_relations
    3.92 -]
    3.93 -
    3.94 -
    3.95 -(* first-order quantifiers *)
    3.96 -
    3.97 -lemma transfer_nat_int_quantifiers:
    3.98 -    "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
    3.99 -    "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
   3.100 -  by (rule all_nat, rule ex_nat)
   3.101 -
   3.102 -(* should we restrict these? *)
   3.103 -lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
   3.104 -    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
   3.105 -  by auto
   3.106 -
   3.107 -lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
   3.108 -    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
   3.109 -  by auto
   3.110 -
   3.111 -declare TransferMorphism_nat_int[transfer add
   3.112 -  return: transfer_nat_int_quantifiers
   3.113 -  cong: all_cong ex_cong]
   3.114 -
   3.115 -
   3.116 -(* if *)
   3.117 -
   3.118 -lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
   3.119 -    nat (if P then x else y)"
   3.120 -  by auto
   3.121 -
   3.122 -declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
   3.123 -
   3.124 -
   3.125 -(* operations with sets *)
   3.126 -
   3.127 -definition
   3.128 -  nat_set :: "int set \<Rightarrow> bool"
   3.129 -where
   3.130 -  "nat_set S = (ALL x:S. x >= 0)"
   3.131 -
   3.132 -lemma transfer_nat_int_set_functions:
   3.133 -    "card A = card (int ` A)"
   3.134 -    "{} = nat ` ({}::int set)"
   3.135 -    "A Un B = nat ` (int ` A Un int ` B)"
   3.136 -    "A Int B = nat ` (int ` A Int int ` B)"
   3.137 -    "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
   3.138 -    "{..n} = nat ` {0..int n}"
   3.139 -    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
   3.140 -  apply (rule card_image [symmetric])
   3.141 -  apply (auto simp add: inj_on_def image_def)
   3.142 -  apply (rule_tac x = "int x" in bexI)
   3.143 -  apply auto
   3.144 -  apply (rule_tac x = "int x" in bexI)
   3.145 -  apply auto
   3.146 -  apply (rule_tac x = "int x" in bexI)
   3.147 -  apply auto
   3.148 -  apply (rule_tac x = "int x" in exI)
   3.149 -  apply auto
   3.150 -  apply (rule_tac x = "int x" in bexI)
   3.151 -  apply auto
   3.152 -  apply (rule_tac x = "int x" in bexI)
   3.153 -  apply auto
   3.154 -done
   3.155 -
   3.156 -lemma transfer_nat_int_set_function_closures:
   3.157 -    "nat_set {}"
   3.158 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   3.159 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   3.160 -    "x >= 0 \<Longrightarrow> nat_set {x..y}"
   3.161 -    "nat_set {x. x >= 0 & P x}"
   3.162 -    "nat_set (int ` C)"
   3.163 -    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
   3.164 -  unfolding nat_set_def apply auto
   3.165 -done
   3.166 -
   3.167 -lemma transfer_nat_int_set_relations:
   3.168 -    "(finite A) = (finite (int ` A))"
   3.169 -    "(x : A) = (int x : int ` A)"
   3.170 -    "(A = B) = (int ` A = int ` B)"
   3.171 -    "(A < B) = (int ` A < int ` B)"
   3.172 -    "(A <= B) = (int ` A <= int ` B)"
   3.173 -
   3.174 -  apply (rule iffI)
   3.175 -  apply (erule finite_imageI)
   3.176 -  apply (erule finite_imageD)
   3.177 -  apply (auto simp add: image_def expand_set_eq inj_on_def)
   3.178 -  apply (drule_tac x = "int x" in spec, auto)
   3.179 -  apply (drule_tac x = "int x" in spec, auto)
   3.180 -  apply (drule_tac x = "int x" in spec, auto)
   3.181 -done
   3.182 -
   3.183 -lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
   3.184 -    (int ` nat ` A = A)"
   3.185 -  by (auto simp add: nat_set_def image_def)
   3.186 -
   3.187 -lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
   3.188 -    {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
   3.189 -  by auto
   3.190 -
   3.191 -declare TransferMorphism_nat_int[transfer add
   3.192 -  return: transfer_nat_int_set_functions
   3.193 -    transfer_nat_int_set_function_closures
   3.194 -    transfer_nat_int_set_relations
   3.195 -    transfer_nat_int_set_return_embed
   3.196 -  cong: transfer_nat_int_set_cong
   3.197 -]
   3.198 -
   3.199 -
   3.200 -(* setsum and setprod *)
   3.201 -
   3.202 -(* this handles the case where the *domain* of f is nat *)
   3.203 -lemma transfer_nat_int_sum_prod:
   3.204 -    "setsum f A = setsum (%x. f (nat x)) (int ` A)"
   3.205 -    "setprod f A = setprod (%x. f (nat x)) (int ` A)"
   3.206 -  apply (subst setsum_reindex)
   3.207 -  apply (unfold inj_on_def, auto)
   3.208 -  apply (subst setprod_reindex)
   3.209 -  apply (unfold inj_on_def o_def, auto)
   3.210 -done
   3.211 -
   3.212 -(* this handles the case where the *range* of f is nat *)
   3.213 -lemma transfer_nat_int_sum_prod2:
   3.214 -    "setsum f A = nat(setsum (%x. int (f x)) A)"
   3.215 -    "setprod f A = nat(setprod (%x. int (f x)) A)"
   3.216 -  apply (subst int_setsum [symmetric])
   3.217 -  apply auto
   3.218 -  apply (subst int_setprod [symmetric])
   3.219 -  apply auto
   3.220 -done
   3.221 -
   3.222 -lemma transfer_nat_int_sum_prod_closure:
   3.223 -    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
   3.224 -    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
   3.225 -  unfolding nat_set_def
   3.226 -  apply (rule setsum_nonneg)
   3.227 -  apply auto
   3.228 -  apply (rule setprod_nonneg)
   3.229 -  apply auto
   3.230 -done
   3.231 -
   3.232 -(* this version doesn't work, even with nat_set A \<Longrightarrow>
   3.233 -      x : A \<Longrightarrow> x >= 0 turned on. Why not?
   3.234 -
   3.235 -  also: what does =simp=> do?
   3.236 -
   3.237 -lemma transfer_nat_int_sum_prod_closure:
   3.238 -    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
   3.239 -    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
   3.240 -  unfolding nat_set_def simp_implies_def
   3.241 -  apply (rule setsum_nonneg)
   3.242 -  apply auto
   3.243 -  apply (rule setprod_nonneg)
   3.244 -  apply auto
   3.245 -done
   3.246 -*)
   3.247 -
   3.248 -(* Making A = B in this lemma doesn't work. Why not?
   3.249 -   Also, why aren't setsum_cong and setprod_cong enough,
   3.250 -   with the previously mentioned rule turned on? *)
   3.251 -
   3.252 -lemma transfer_nat_int_sum_prod_cong:
   3.253 -    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
   3.254 -      setsum f A = setsum g B"
   3.255 -    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
   3.256 -      setprod f A = setprod g B"
   3.257 -  unfolding nat_set_def
   3.258 -  apply (subst setsum_cong, assumption)
   3.259 -  apply auto [2]
   3.260 -  apply (subst setprod_cong, assumption, auto)
   3.261 -done
   3.262 -
   3.263 -declare TransferMorphism_nat_int[transfer add
   3.264 -  return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
   3.265 -    transfer_nat_int_sum_prod_closure
   3.266 -  cong: transfer_nat_int_sum_prod_cong]
   3.267 -
   3.268 -(* lists *)
   3.269 -
   3.270 -definition
   3.271 -  embed_list :: "nat list \<Rightarrow> int list"
   3.272 -where
   3.273 -  "embed_list l = map int l";
   3.274 -
   3.275 -definition
   3.276 -  nat_list :: "int list \<Rightarrow> bool"
   3.277 -where
   3.278 -  "nat_list l = nat_set (set l)";
   3.279 -
   3.280 -definition
   3.281 -  return_list :: "int list \<Rightarrow> nat list"
   3.282 -where
   3.283 -  "return_list l = map nat l";
   3.284 -
   3.285 -thm nat_0_le;
   3.286 -
   3.287 -lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
   3.288 -    embed_list (return_list l) = l";
   3.289 -  unfolding embed_list_def return_list_def nat_list_def nat_set_def
   3.290 -  apply (induct l);
   3.291 -  apply auto;
   3.292 -done;
   3.293 -
   3.294 -lemma transfer_nat_int_list_functions:
   3.295 -  "l @ m = return_list (embed_list l @ embed_list m)"
   3.296 -  "[] = return_list []";
   3.297 -  unfolding return_list_def embed_list_def;
   3.298 -  apply auto;
   3.299 -  apply (induct l, auto);
   3.300 -  apply (induct m, auto);
   3.301 -done;
   3.302 -
   3.303 -(*
   3.304 -lemma transfer_nat_int_fold1: "fold f l x =
   3.305 -    fold (%x. f (nat x)) (embed_list l) x";
   3.306 -*)
   3.307 -
   3.308 -
   3.309 -
   3.310 -
   3.311 -subsection {* Set up transfer from int to nat *}
   3.312 -
   3.313 -(* set up transfer direction *)
   3.314 -
   3.315 -lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
   3.316 -  by (simp add: TransferMorphism_def)
   3.317 -
   3.318 -declare TransferMorphism_int_nat[transfer add
   3.319 -  mode: manual
   3.320 -(*  labels: int-nat *)
   3.321 -  return: nat_int
   3.322 -]
   3.323 -
   3.324 -
   3.325 -(* basic functions and relations *)
   3.326 -
   3.327 -definition
   3.328 -  is_nat :: "int \<Rightarrow> bool"
   3.329 -where
   3.330 -  "is_nat x = (x >= 0)"
   3.331 -
   3.332 -lemma transfer_int_nat_numerals:
   3.333 -    "0 = int 0"
   3.334 -    "1 = int 1"
   3.335 -    "2 = int 2"
   3.336 -    "3 = int 3"
   3.337 -  by auto
   3.338 -
   3.339 -lemma transfer_int_nat_functions:
   3.340 -    "(int x) + (int y) = int (x + y)"
   3.341 -    "(int x) * (int y) = int (x * y)"
   3.342 -    "tsub (int x) (int y) = int (x - y)"
   3.343 -    "(int x)^n = int (x^n)"
   3.344 -    "(int x) div (int y) = int (x div y)"
   3.345 -    "(int x) mod (int y) = int (x mod y)"
   3.346 -  by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
   3.347 -
   3.348 -lemma transfer_int_nat_function_closures:
   3.349 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
   3.350 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
   3.351 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
   3.352 -    "is_nat x \<Longrightarrow> is_nat (x^n)"
   3.353 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
   3.354 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   3.355 -    "is_nat 0"
   3.356 -    "is_nat 1"
   3.357 -    "is_nat 2"
   3.358 -    "is_nat 3"
   3.359 -    "is_nat (int z)"
   3.360 -  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
   3.361 -
   3.362 -lemma transfer_int_nat_relations:
   3.363 -    "(int x = int y) = (x = y)"
   3.364 -    "(int x < int y) = (x < y)"
   3.365 -    "(int x <= int y) = (x <= y)"
   3.366 -    "(int x dvd int y) = (x dvd y)"
   3.367 -    "(even (int x)) = (even x)"
   3.368 -  by (auto simp add: zdvd_int even_nat_def)
   3.369 -
   3.370 -lemma UNIV_apply:
   3.371 -  "UNIV x = True"
   3.372 -  by (simp add: top_fun_eq top_bool_eq)
   3.373 -
   3.374 -declare TransferMorphism_int_nat[transfer add return:
   3.375 -  transfer_int_nat_numerals
   3.376 -  transfer_int_nat_functions
   3.377 -  transfer_int_nat_function_closures
   3.378 -  transfer_int_nat_relations
   3.379 -  UNIV_apply
   3.380 -]
   3.381 -
   3.382 -
   3.383 -(* first-order quantifiers *)
   3.384 -
   3.385 -lemma transfer_int_nat_quantifiers:
   3.386 -    "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
   3.387 -    "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
   3.388 -  apply (subst all_nat)
   3.389 -  apply auto [1]
   3.390 -  apply (subst ex_nat)
   3.391 -  apply auto
   3.392 -done
   3.393 -
   3.394 -declare TransferMorphism_int_nat[transfer add
   3.395 -  return: transfer_int_nat_quantifiers]
   3.396 -
   3.397 -
   3.398 -(* if *)
   3.399 -
   3.400 -lemma int_if_cong: "(if P then (int x) else (int y)) =
   3.401 -    int (if P then x else y)"
   3.402 -  by auto
   3.403 -
   3.404 -declare TransferMorphism_int_nat [transfer add return: int_if_cong]
   3.405 -
   3.406 -
   3.407 -
   3.408 -(* operations with sets *)
   3.409 -
   3.410 -lemma transfer_int_nat_set_functions:
   3.411 -    "nat_set A \<Longrightarrow> card A = card (nat ` A)"
   3.412 -    "{} = int ` ({}::nat set)"
   3.413 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
   3.414 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
   3.415 -    "{x. x >= 0 & P x} = int ` {x. P(int x)}"
   3.416 -    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
   3.417 -       (* need all variants of these! *)
   3.418 -  by (simp_all only: is_nat_def transfer_nat_int_set_functions
   3.419 -          transfer_nat_int_set_function_closures
   3.420 -          transfer_nat_int_set_return_embed nat_0_le
   3.421 -          cong: transfer_nat_int_set_cong)
   3.422 -
   3.423 -lemma transfer_int_nat_set_function_closures:
   3.424 -    "nat_set {}"
   3.425 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   3.426 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   3.427 -    "is_nat x \<Longrightarrow> nat_set {x..y}"
   3.428 -    "nat_set {x. x >= 0 & P x}"
   3.429 -    "nat_set (int ` C)"
   3.430 -    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
   3.431 -  by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
   3.432 -
   3.433 -lemma transfer_int_nat_set_relations:
   3.434 -    "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
   3.435 -    "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
   3.436 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
   3.437 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
   3.438 -    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
   3.439 -  by (simp_all only: is_nat_def transfer_nat_int_set_relations
   3.440 -    transfer_nat_int_set_return_embed nat_0_le)
   3.441 -
   3.442 -lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
   3.443 -  by (simp only: transfer_nat_int_set_relations
   3.444 -    transfer_nat_int_set_function_closures
   3.445 -    transfer_nat_int_set_return_embed nat_0_le)
   3.446 -
   3.447 -lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
   3.448 -    {(x::nat). P x} = {x. P' x}"
   3.449 -  by auto
   3.450 -
   3.451 -declare TransferMorphism_int_nat[transfer add
   3.452 -  return: transfer_int_nat_set_functions
   3.453 -    transfer_int_nat_set_function_closures
   3.454 -    transfer_int_nat_set_relations
   3.455 -    transfer_int_nat_set_return_embed
   3.456 -  cong: transfer_int_nat_set_cong
   3.457 -]
   3.458 -
   3.459 -
   3.460 -(* setsum and setprod *)
   3.461 -
   3.462 -(* this handles the case where the *domain* of f is int *)
   3.463 -lemma transfer_int_nat_sum_prod:
   3.464 -    "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
   3.465 -    "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
   3.466 -  apply (subst setsum_reindex)
   3.467 -  apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
   3.468 -  apply (subst setprod_reindex)
   3.469 -  apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
   3.470 -            cong: setprod_cong)
   3.471 -done
   3.472 -
   3.473 -(* this handles the case where the *range* of f is int *)
   3.474 -lemma transfer_int_nat_sum_prod2:
   3.475 -    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
   3.476 -    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
   3.477 -      setprod f A = int(setprod (%x. nat (f x)) A)"
   3.478 -  unfolding is_nat_def
   3.479 -  apply (subst int_setsum, auto)
   3.480 -  apply (subst int_setprod, auto simp add: cong: setprod_cong)
   3.481 -done
   3.482 -
   3.483 -declare TransferMorphism_int_nat[transfer add
   3.484 -  return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   3.485 -  cong: setsum_cong setprod_cong]
   3.486 -
   3.487 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Nat_Transfer.thy	Thu Sep 10 15:26:51 2009 +0200
     4.3 @@ -0,0 +1,484 @@
     4.4 +
     4.5 +(* Authors: Jeremy Avigad and Amine Chaieb *)
     4.6 +
     4.7 +header {* Sets up transfer from nats to ints and back. *}
     4.8 +
     4.9 +theory Nat_Transfer
    4.10 +imports Main Parity
    4.11 +begin
    4.12 +
    4.13 +subsection {* Set up transfer from nat to int *}
    4.14 +
    4.15 +(* set up transfer direction *)
    4.16 +
    4.17 +lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
    4.18 +  by (simp add: TransferMorphism_def)
    4.19 +
    4.20 +declare TransferMorphism_nat_int[transfer
    4.21 +  add mode: manual
    4.22 +  return: nat_0_le
    4.23 +  labels: natint
    4.24 +]
    4.25 +
    4.26 +(* basic functions and relations *)
    4.27 +
    4.28 +lemma transfer_nat_int_numerals:
    4.29 +    "(0::nat) = nat 0"
    4.30 +    "(1::nat) = nat 1"
    4.31 +    "(2::nat) = nat 2"
    4.32 +    "(3::nat) = nat 3"
    4.33 +  by auto
    4.34 +
    4.35 +definition
    4.36 +  tsub :: "int \<Rightarrow> int \<Rightarrow> int"
    4.37 +where
    4.38 +  "tsub x y = (if x >= y then x - y else 0)"
    4.39 +
    4.40 +lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
    4.41 +  by (simp add: tsub_def)
    4.42 +
    4.43 +
    4.44 +lemma transfer_nat_int_functions:
    4.45 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
    4.46 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
    4.47 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
    4.48 +    "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
    4.49 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
    4.50 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
    4.51 +  by (auto simp add: eq_nat_nat_iff nat_mult_distrib
    4.52 +      nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
    4.53 +
    4.54 +lemma transfer_nat_int_function_closures:
    4.55 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
    4.56 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
    4.57 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
    4.58 +    "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
    4.59 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
    4.60 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
    4.61 +    "(0::int) >= 0"
    4.62 +    "(1::int) >= 0"
    4.63 +    "(2::int) >= 0"
    4.64 +    "(3::int) >= 0"
    4.65 +    "int z >= 0"
    4.66 +  apply (auto simp add: zero_le_mult_iff tsub_def)
    4.67 +  apply (case_tac "y = 0")
    4.68 +  apply auto
    4.69 +  apply (subst pos_imp_zdiv_nonneg_iff, auto)
    4.70 +  apply (case_tac "y = 0")
    4.71 +  apply force
    4.72 +  apply (rule pos_mod_sign)
    4.73 +  apply arith
    4.74 +done
    4.75 +
    4.76 +lemma transfer_nat_int_relations:
    4.77 +    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    4.78 +      (nat (x::int) = nat y) = (x = y)"
    4.79 +    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    4.80 +      (nat (x::int) < nat y) = (x < y)"
    4.81 +    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    4.82 +      (nat (x::int) <= nat y) = (x <= y)"
    4.83 +    "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    4.84 +      (nat (x::int) dvd nat y) = (x dvd y)"
    4.85 +  by (auto simp add: zdvd_int)
    4.86 +
    4.87 +declare TransferMorphism_nat_int[transfer add return:
    4.88 +  transfer_nat_int_numerals
    4.89 +  transfer_nat_int_functions
    4.90 +  transfer_nat_int_function_closures
    4.91 +  transfer_nat_int_relations
    4.92 +]
    4.93 +
    4.94 +
    4.95 +(* first-order quantifiers *)
    4.96 +
    4.97 +lemma transfer_nat_int_quantifiers:
    4.98 +    "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
    4.99 +    "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
   4.100 +  by (rule all_nat, rule ex_nat)
   4.101 +
   4.102 +(* should we restrict these? *)
   4.103 +lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
   4.104 +    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
   4.105 +  by auto
   4.106 +
   4.107 +lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
   4.108 +    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
   4.109 +  by auto
   4.110 +
   4.111 +declare TransferMorphism_nat_int[transfer add
   4.112 +  return: transfer_nat_int_quantifiers
   4.113 +  cong: all_cong ex_cong]
   4.114 +
   4.115 +
   4.116 +(* if *)
   4.117 +
   4.118 +lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
   4.119 +    nat (if P then x else y)"
   4.120 +  by auto
   4.121 +
   4.122 +declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
   4.123 +
   4.124 +
   4.125 +(* operations with sets *)
   4.126 +
   4.127 +definition
   4.128 +  nat_set :: "int set \<Rightarrow> bool"
   4.129 +where
   4.130 +  "nat_set S = (ALL x:S. x >= 0)"
   4.131 +
   4.132 +lemma transfer_nat_int_set_functions:
   4.133 +    "card A = card (int ` A)"
   4.134 +    "{} = nat ` ({}::int set)"
   4.135 +    "A Un B = nat ` (int ` A Un int ` B)"
   4.136 +    "A Int B = nat ` (int ` A Int int ` B)"
   4.137 +    "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
   4.138 +    "{..n} = nat ` {0..int n}"
   4.139 +    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
   4.140 +  apply (rule card_image [symmetric])
   4.141 +  apply (auto simp add: inj_on_def image_def)
   4.142 +  apply (rule_tac x = "int x" in bexI)
   4.143 +  apply auto
   4.144 +  apply (rule_tac x = "int x" in bexI)
   4.145 +  apply auto
   4.146 +  apply (rule_tac x = "int x" in bexI)
   4.147 +  apply auto
   4.148 +  apply (rule_tac x = "int x" in exI)
   4.149 +  apply auto
   4.150 +  apply (rule_tac x = "int x" in bexI)
   4.151 +  apply auto
   4.152 +  apply (rule_tac x = "int x" in bexI)
   4.153 +  apply auto
   4.154 +done
   4.155 +
   4.156 +lemma transfer_nat_int_set_function_closures:
   4.157 +    "nat_set {}"
   4.158 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   4.159 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   4.160 +    "x >= 0 \<Longrightarrow> nat_set {x..y}"
   4.161 +    "nat_set {x. x >= 0 & P x}"
   4.162 +    "nat_set (int ` C)"
   4.163 +    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
   4.164 +  unfolding nat_set_def apply auto
   4.165 +done
   4.166 +
   4.167 +lemma transfer_nat_int_set_relations:
   4.168 +    "(finite A) = (finite (int ` A))"
   4.169 +    "(x : A) = (int x : int ` A)"
   4.170 +    "(A = B) = (int ` A = int ` B)"
   4.171 +    "(A < B) = (int ` A < int ` B)"
   4.172 +    "(A <= B) = (int ` A <= int ` B)"
   4.173 +
   4.174 +  apply (rule iffI)
   4.175 +  apply (erule finite_imageI)
   4.176 +  apply (erule finite_imageD)
   4.177 +  apply (auto simp add: image_def expand_set_eq inj_on_def)
   4.178 +  apply (drule_tac x = "int x" in spec, auto)
   4.179 +  apply (drule_tac x = "int x" in spec, auto)
   4.180 +  apply (drule_tac x = "int x" in spec, auto)
   4.181 +done
   4.182 +
   4.183 +lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
   4.184 +    (int ` nat ` A = A)"
   4.185 +  by (auto simp add: nat_set_def image_def)
   4.186 +
   4.187 +lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
   4.188 +    {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
   4.189 +  by auto
   4.190 +
   4.191 +declare TransferMorphism_nat_int[transfer add
   4.192 +  return: transfer_nat_int_set_functions
   4.193 +    transfer_nat_int_set_function_closures
   4.194 +    transfer_nat_int_set_relations
   4.195 +    transfer_nat_int_set_return_embed
   4.196 +  cong: transfer_nat_int_set_cong
   4.197 +]
   4.198 +
   4.199 +
   4.200 +(* setsum and setprod *)
   4.201 +
   4.202 +(* this handles the case where the *domain* of f is nat *)
   4.203 +lemma transfer_nat_int_sum_prod:
   4.204 +    "setsum f A = setsum (%x. f (nat x)) (int ` A)"
   4.205 +    "setprod f A = setprod (%x. f (nat x)) (int ` A)"
   4.206 +  apply (subst setsum_reindex)
   4.207 +  apply (unfold inj_on_def, auto)
   4.208 +  apply (subst setprod_reindex)
   4.209 +  apply (unfold inj_on_def o_def, auto)
   4.210 +done
   4.211 +
   4.212 +(* this handles the case where the *range* of f is nat *)
   4.213 +lemma transfer_nat_int_sum_prod2:
   4.214 +    "setsum f A = nat(setsum (%x. int (f x)) A)"
   4.215 +    "setprod f A = nat(setprod (%x. int (f x)) A)"
   4.216 +  apply (subst int_setsum [symmetric])
   4.217 +  apply auto
   4.218 +  apply (subst int_setprod [symmetric])
   4.219 +  apply auto
   4.220 +done
   4.221 +
   4.222 +lemma transfer_nat_int_sum_prod_closure:
   4.223 +    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
   4.224 +    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
   4.225 +  unfolding nat_set_def
   4.226 +  apply (rule setsum_nonneg)
   4.227 +  apply auto
   4.228 +  apply (rule setprod_nonneg)
   4.229 +  apply auto
   4.230 +done
   4.231 +
   4.232 +(* this version doesn't work, even with nat_set A \<Longrightarrow>
   4.233 +      x : A \<Longrightarrow> x >= 0 turned on. Why not?
   4.234 +
   4.235 +  also: what does =simp=> do?
   4.236 +
   4.237 +lemma transfer_nat_int_sum_prod_closure:
   4.238 +    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
   4.239 +    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
   4.240 +  unfolding nat_set_def simp_implies_def
   4.241 +  apply (rule setsum_nonneg)
   4.242 +  apply auto
   4.243 +  apply (rule setprod_nonneg)
   4.244 +  apply auto
   4.245 +done
   4.246 +*)
   4.247 +
   4.248 +(* Making A = B in this lemma doesn't work. Why not?
   4.249 +   Also, why aren't setsum_cong and setprod_cong enough,
   4.250 +   with the previously mentioned rule turned on? *)
   4.251 +
   4.252 +lemma transfer_nat_int_sum_prod_cong:
   4.253 +    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
   4.254 +      setsum f A = setsum g B"
   4.255 +    "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
   4.256 +      setprod f A = setprod g B"
   4.257 +  unfolding nat_set_def
   4.258 +  apply (subst setsum_cong, assumption)
   4.259 +  apply auto [2]
   4.260 +  apply (subst setprod_cong, assumption, auto)
   4.261 +done
   4.262 +
   4.263 +declare TransferMorphism_nat_int[transfer add
   4.264 +  return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
   4.265 +    transfer_nat_int_sum_prod_closure
   4.266 +  cong: transfer_nat_int_sum_prod_cong]
   4.267 +
   4.268 +(* lists *)
   4.269 +
   4.270 +definition
   4.271 +  embed_list :: "nat list \<Rightarrow> int list"
   4.272 +where
   4.273 +  "embed_list l = map int l";
   4.274 +
   4.275 +definition
   4.276 +  nat_list :: "int list \<Rightarrow> bool"
   4.277 +where
   4.278 +  "nat_list l = nat_set (set l)";
   4.279 +
   4.280 +definition
   4.281 +  return_list :: "int list \<Rightarrow> nat list"
   4.282 +where
   4.283 +  "return_list l = map nat l";
   4.284 +
   4.285 +thm nat_0_le;
   4.286 +
   4.287 +lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
   4.288 +    embed_list (return_list l) = l";
   4.289 +  unfolding embed_list_def return_list_def nat_list_def nat_set_def
   4.290 +  apply (induct l);
   4.291 +  apply auto;
   4.292 +done;
   4.293 +
   4.294 +lemma transfer_nat_int_list_functions:
   4.295 +  "l @ m = return_list (embed_list l @ embed_list m)"
   4.296 +  "[] = return_list []";
   4.297 +  unfolding return_list_def embed_list_def;
   4.298 +  apply auto;
   4.299 +  apply (induct l, auto);
   4.300 +  apply (induct m, auto);
   4.301 +done;
   4.302 +
   4.303 +(*
   4.304 +lemma transfer_nat_int_fold1: "fold f l x =
   4.305 +    fold (%x. f (nat x)) (embed_list l) x";
   4.306 +*)
   4.307 +
   4.308 +
   4.309 +
   4.310 +
   4.311 +subsection {* Set up transfer from int to nat *}
   4.312 +
   4.313 +(* set up transfer direction *)
   4.314 +
   4.315 +lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
   4.316 +  by (simp add: TransferMorphism_def)
   4.317 +
   4.318 +declare TransferMorphism_int_nat[transfer add
   4.319 +  mode: manual
   4.320 +(*  labels: int-nat *)
   4.321 +  return: nat_int
   4.322 +]
   4.323 +
   4.324 +
   4.325 +(* basic functions and relations *)
   4.326 +
   4.327 +definition
   4.328 +  is_nat :: "int \<Rightarrow> bool"
   4.329 +where
   4.330 +  "is_nat x = (x >= 0)"
   4.331 +
   4.332 +lemma transfer_int_nat_numerals:
   4.333 +    "0 = int 0"
   4.334 +    "1 = int 1"
   4.335 +    "2 = int 2"
   4.336 +    "3 = int 3"
   4.337 +  by auto
   4.338 +
   4.339 +lemma transfer_int_nat_functions:
   4.340 +    "(int x) + (int y) = int (x + y)"
   4.341 +    "(int x) * (int y) = int (x * y)"
   4.342 +    "tsub (int x) (int y) = int (x - y)"
   4.343 +    "(int x)^n = int (x^n)"
   4.344 +    "(int x) div (int y) = int (x div y)"
   4.345 +    "(int x) mod (int y) = int (x mod y)"
   4.346 +  by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
   4.347 +
   4.348 +lemma transfer_int_nat_function_closures:
   4.349 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
   4.350 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
   4.351 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
   4.352 +    "is_nat x \<Longrightarrow> is_nat (x^n)"
   4.353 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
   4.354 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   4.355 +    "is_nat 0"
   4.356 +    "is_nat 1"
   4.357 +    "is_nat 2"
   4.358 +    "is_nat 3"
   4.359 +    "is_nat (int z)"
   4.360 +  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
   4.361 +
   4.362 +lemma transfer_int_nat_relations:
   4.363 +    "(int x = int y) = (x = y)"
   4.364 +    "(int x < int y) = (x < y)"
   4.365 +    "(int x <= int y) = (x <= y)"
   4.366 +    "(int x dvd int y) = (x dvd y)"
   4.367 +    "(even (int x)) = (even x)"
   4.368 +  by (auto simp add: zdvd_int even_nat_def)
   4.369 +
   4.370 +lemma UNIV_apply:
   4.371 +  "UNIV x = True"
   4.372 +  by (simp add: top_fun_eq top_bool_eq)
   4.373 +
   4.374 +declare TransferMorphism_int_nat[transfer add return:
   4.375 +  transfer_int_nat_numerals
   4.376 +  transfer_int_nat_functions
   4.377 +  transfer_int_nat_function_closures
   4.378 +  transfer_int_nat_relations
   4.379 +  UNIV_apply
   4.380 +]
   4.381 +
   4.382 +
   4.383 +(* first-order quantifiers *)
   4.384 +
   4.385 +lemma transfer_int_nat_quantifiers:
   4.386 +    "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
   4.387 +    "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
   4.388 +  apply (subst all_nat)
   4.389 +  apply auto [1]
   4.390 +  apply (subst ex_nat)
   4.391 +  apply auto
   4.392 +done
   4.393 +
   4.394 +declare TransferMorphism_int_nat[transfer add
   4.395 +  return: transfer_int_nat_quantifiers]
   4.396 +
   4.397 +
   4.398 +(* if *)
   4.399 +
   4.400 +lemma int_if_cong: "(if P then (int x) else (int y)) =
   4.401 +    int (if P then x else y)"
   4.402 +  by auto
   4.403 +
   4.404 +declare TransferMorphism_int_nat [transfer add return: int_if_cong]
   4.405 +
   4.406 +
   4.407 +
   4.408 +(* operations with sets *)
   4.409 +
   4.410 +lemma transfer_int_nat_set_functions:
   4.411 +    "nat_set A \<Longrightarrow> card A = card (nat ` A)"
   4.412 +    "{} = int ` ({}::nat set)"
   4.413 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
   4.414 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
   4.415 +    "{x. x >= 0 & P x} = int ` {x. P(int x)}"
   4.416 +    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
   4.417 +       (* need all variants of these! *)
   4.418 +  by (simp_all only: is_nat_def transfer_nat_int_set_functions
   4.419 +          transfer_nat_int_set_function_closures
   4.420 +          transfer_nat_int_set_return_embed nat_0_le
   4.421 +          cong: transfer_nat_int_set_cong)
   4.422 +
   4.423 +lemma transfer_int_nat_set_function_closures:
   4.424 +    "nat_set {}"
   4.425 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   4.426 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   4.427 +    "is_nat x \<Longrightarrow> nat_set {x..y}"
   4.428 +    "nat_set {x. x >= 0 & P x}"
   4.429 +    "nat_set (int ` C)"
   4.430 +    "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
   4.431 +  by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
   4.432 +
   4.433 +lemma transfer_int_nat_set_relations:
   4.434 +    "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
   4.435 +    "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
   4.436 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
   4.437 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
   4.438 +    "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
   4.439 +  by (simp_all only: is_nat_def transfer_nat_int_set_relations
   4.440 +    transfer_nat_int_set_return_embed nat_0_le)
   4.441 +
   4.442 +lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
   4.443 +  by (simp only: transfer_nat_int_set_relations
   4.444 +    transfer_nat_int_set_function_closures
   4.445 +    transfer_nat_int_set_return_embed nat_0_le)
   4.446 +
   4.447 +lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
   4.448 +    {(x::nat). P x} = {x. P' x}"
   4.449 +  by auto
   4.450 +
   4.451 +declare TransferMorphism_int_nat[transfer add
   4.452 +  return: transfer_int_nat_set_functions
   4.453 +    transfer_int_nat_set_function_closures
   4.454 +    transfer_int_nat_set_relations
   4.455 +    transfer_int_nat_set_return_embed
   4.456 +  cong: transfer_int_nat_set_cong
   4.457 +]
   4.458 +
   4.459 +
   4.460 +(* setsum and setprod *)
   4.461 +
   4.462 +(* this handles the case where the *domain* of f is int *)
   4.463 +lemma transfer_int_nat_sum_prod:
   4.464 +    "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
   4.465 +    "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
   4.466 +  apply (subst setsum_reindex)
   4.467 +  apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
   4.468 +  apply (subst setprod_reindex)
   4.469 +  apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
   4.470 +            cong: setprod_cong)
   4.471 +done
   4.472 +
   4.473 +(* this handles the case where the *range* of f is int *)
   4.474 +lemma transfer_int_nat_sum_prod2:
   4.475 +    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
   4.476 +    "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
   4.477 +      setprod f A = int(setprod (%x. nat (f x)) A)"
   4.478 +  unfolding is_nat_def
   4.479 +  apply (subst int_setsum, auto)
   4.480 +  apply (subst int_setprod, auto simp add: cong: setprod_cong)
   4.481 +done
   4.482 +
   4.483 +declare TransferMorphism_int_nat[transfer add
   4.484 +  return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   4.485 +  cong: setsum_cong setprod_cong]
   4.486 +
   4.487 +end