src/HOL/NatTransfer.thy
author nipkow
Fri Aug 28 18:52:41 2009 +0200 (2009-08-28)
changeset 32436 10cd49e0c067
parent 32264 0be31453f698
child 32554 4ccd84fb19d3
permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
     1 (*  Title:      HOL/Library/NatTransfer.thy
     2     Authors:    Jeremy Avigad and Amine Chaieb
     3 
     4     Sets up transfer from nats to ints and
     5     back.
     6 *)
     7 
     8 
     9 header {* NatTransfer *}
    10 
    11 theory NatTransfer
    12 imports Main Parity
    13 uses ("Tools/transfer_data.ML")
    14 begin
    15 
    16 subsection {* A transfer Method between isomorphic domains*}
    17 
    18 definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
    19   where "TransferMorphism a B = True"
    20 
    21 use "Tools/transfer_data.ML"
    22 
    23 setup TransferData.setup
    24 
    25 
    26 subsection {* Set up transfer from nat to int *}
    27 
    28 (* set up transfer direction *)
    29 
    30 lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
    31   by (simp add: TransferMorphism_def)
    32 
    33 declare TransferMorphism_nat_int[transfer
    34   add mode: manual
    35   return: nat_0_le
    36   labels: natint
    37 ]
    38 
    39 (* basic functions and relations *)
    40 
    41 lemma transfer_nat_int_numerals:
    42     "(0::nat) = nat 0"
    43     "(1::nat) = nat 1"
    44     "(2::nat) = nat 2"
    45     "(3::nat) = nat 3"
    46   by auto
    47 
    48 definition
    49   tsub :: "int \<Rightarrow> int \<Rightarrow> int"
    50 where
    51   "tsub x y = (if x >= y then x - y else 0)"
    52 
    53 lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
    54   by (simp add: tsub_def)
    55 
    56 
    57 lemma transfer_nat_int_functions:
    58     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
    59     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
    60     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
    61     "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
    62     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
    63     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
    64   by (auto simp add: eq_nat_nat_iff nat_mult_distrib
    65       nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
    66 
    67 lemma transfer_nat_int_function_closures:
    68     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
    69     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
    70     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
    71     "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
    72     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
    73     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
    74     "(0::int) >= 0"
    75     "(1::int) >= 0"
    76     "(2::int) >= 0"
    77     "(3::int) >= 0"
    78     "int z >= 0"
    79   apply (auto simp add: zero_le_mult_iff tsub_def)
    80   apply (case_tac "y = 0")
    81   apply auto
    82   apply (subst pos_imp_zdiv_nonneg_iff, auto)
    83   apply (case_tac "y = 0")
    84   apply force
    85   apply (rule pos_mod_sign)
    86   apply arith
    87 done
    88 
    89 lemma transfer_nat_int_relations:
    90     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    91       (nat (x::int) = nat y) = (x = y)"
    92     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    93       (nat (x::int) < nat y) = (x < y)"
    94     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    95       (nat (x::int) <= nat y) = (x <= y)"
    96     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    97       (nat (x::int) dvd nat y) = (x dvd y)"
    98   by (auto simp add: zdvd_int even_nat_def)
    99 
   100 declare TransferMorphism_nat_int[transfer add return:
   101   transfer_nat_int_numerals
   102   transfer_nat_int_functions
   103   transfer_nat_int_function_closures
   104   transfer_nat_int_relations
   105 ]
   106 
   107 
   108 (* first-order quantifiers *)
   109 
   110 lemma transfer_nat_int_quantifiers:
   111     "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
   112     "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
   113   by (rule all_nat, rule ex_nat)
   114 
   115 (* should we restrict these? *)
   116 lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
   117     (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
   118   by auto
   119 
   120 lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
   121     (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
   122   by auto
   123 
   124 declare TransferMorphism_nat_int[transfer add
   125   return: transfer_nat_int_quantifiers
   126   cong: all_cong ex_cong]
   127 
   128 
   129 (* if *)
   130 
   131 lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
   132     nat (if P then x else y)"
   133   by auto
   134 
   135 declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
   136 
   137 
   138 (* operations with sets *)
   139 
   140 definition
   141   nat_set :: "int set \<Rightarrow> bool"
   142 where
   143   "nat_set S = (ALL x:S. x >= 0)"
   144 
   145 lemma transfer_nat_int_set_functions:
   146     "card A = card (int ` A)"
   147     "{} = nat ` ({}::int set)"
   148     "A Un B = nat ` (int ` A Un int ` B)"
   149     "A Int B = nat ` (int ` A Int int ` B)"
   150     "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
   151     "{..n} = nat ` {0..int n}"
   152     "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
   153   apply (rule card_image [symmetric])
   154   apply (auto simp add: inj_on_def image_def)
   155   apply (rule_tac x = "int x" in bexI)
   156   apply auto
   157   apply (rule_tac x = "int x" in bexI)
   158   apply auto
   159   apply (rule_tac x = "int x" in bexI)
   160   apply auto
   161   apply (rule_tac x = "int x" in exI)
   162   apply auto
   163   apply (rule_tac x = "int x" in bexI)
   164   apply auto
   165   apply (rule_tac x = "int x" in bexI)
   166   apply auto
   167 done
   168 
   169 lemma transfer_nat_int_set_function_closures:
   170     "nat_set {}"
   171     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   172     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   173     "x >= 0 \<Longrightarrow> nat_set {x..y}"
   174     "nat_set {x. x >= 0 & P x}"
   175     "nat_set (int ` C)"
   176     "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
   177   unfolding nat_set_def apply auto
   178 done
   179 
   180 lemma transfer_nat_int_set_relations:
   181     "(finite A) = (finite (int ` A))"
   182     "(x : A) = (int x : int ` A)"
   183     "(A = B) = (int ` A = int ` B)"
   184     "(A < B) = (int ` A < int ` B)"
   185     "(A <= B) = (int ` A <= int ` B)"
   186 
   187   apply (rule iffI)
   188   apply (erule finite_imageI)
   189   apply (erule finite_imageD)
   190   apply (auto simp add: image_def expand_set_eq inj_on_def)
   191   apply (drule_tac x = "int x" in spec, auto)
   192   apply (drule_tac x = "int x" in spec, auto)
   193   apply (drule_tac x = "int x" in spec, auto)
   194 done
   195 
   196 lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
   197     (int ` nat ` A = A)"
   198   by (auto simp add: nat_set_def image_def)
   199 
   200 lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
   201     {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
   202   by auto
   203 
   204 declare TransferMorphism_nat_int[transfer add
   205   return: transfer_nat_int_set_functions
   206     transfer_nat_int_set_function_closures
   207     transfer_nat_int_set_relations
   208     transfer_nat_int_set_return_embed
   209   cong: transfer_nat_int_set_cong
   210 ]
   211 
   212 
   213 (* setsum and setprod *)
   214 
   215 (* this handles the case where the *domain* of f is nat *)
   216 lemma transfer_nat_int_sum_prod:
   217     "setsum f A = setsum (%x. f (nat x)) (int ` A)"
   218     "setprod f A = setprod (%x. f (nat x)) (int ` A)"
   219   apply (subst setsum_reindex)
   220   apply (unfold inj_on_def, auto)
   221   apply (subst setprod_reindex)
   222   apply (unfold inj_on_def o_def, auto)
   223 done
   224 
   225 (* this handles the case where the *range* of f is nat *)
   226 lemma transfer_nat_int_sum_prod2:
   227     "setsum f A = nat(setsum (%x. int (f x)) A)"
   228     "setprod f A = nat(setprod (%x. int (f x)) A)"
   229   apply (subst int_setsum [symmetric])
   230   apply auto
   231   apply (subst int_setprod [symmetric])
   232   apply auto
   233 done
   234 
   235 lemma transfer_nat_int_sum_prod_closure:
   236     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
   237     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
   238   unfolding nat_set_def
   239   apply (rule setsum_nonneg)
   240   apply auto
   241   apply (rule setprod_nonneg)
   242   apply auto
   243 done
   244 
   245 (* this version doesn't work, even with nat_set A \<Longrightarrow>
   246       x : A \<Longrightarrow> x >= 0 turned on. Why not?
   247 
   248   also: what does =simp=> do?
   249 
   250 lemma transfer_nat_int_sum_prod_closure:
   251     "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
   252     "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
   253   unfolding nat_set_def simp_implies_def
   254   apply (rule setsum_nonneg)
   255   apply auto
   256   apply (rule setprod_nonneg)
   257   apply auto
   258 done
   259 *)
   260 
   261 (* Making A = B in this lemma doesn't work. Why not?
   262    Also, why aren't setsum_cong and setprod_cong enough,
   263    with the previously mentioned rule turned on? *)
   264 
   265 lemma transfer_nat_int_sum_prod_cong:
   266     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
   267       setsum f A = setsum g B"
   268     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
   269       setprod f A = setprod g B"
   270   unfolding nat_set_def
   271   apply (subst setsum_cong, assumption)
   272   apply auto [2]
   273   apply (subst setprod_cong, assumption, auto)
   274 done
   275 
   276 declare TransferMorphism_nat_int[transfer add
   277   return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
   278     transfer_nat_int_sum_prod_closure
   279   cong: transfer_nat_int_sum_prod_cong]
   280 
   281 (* lists *)
   282 
   283 definition
   284   embed_list :: "nat list \<Rightarrow> int list"
   285 where
   286   "embed_list l = map int l";
   287 
   288 definition
   289   nat_list :: "int list \<Rightarrow> bool"
   290 where
   291   "nat_list l = nat_set (set l)";
   292 
   293 definition
   294   return_list :: "int list \<Rightarrow> nat list"
   295 where
   296   "return_list l = map nat l";
   297 
   298 thm nat_0_le;
   299 
   300 lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
   301     embed_list (return_list l) = l";
   302   unfolding embed_list_def return_list_def nat_list_def nat_set_def
   303   apply (induct l);
   304   apply auto;
   305 done;
   306 
   307 lemma transfer_nat_int_list_functions:
   308   "l @ m = return_list (embed_list l @ embed_list m)"
   309   "[] = return_list []";
   310   unfolding return_list_def embed_list_def;
   311   apply auto;
   312   apply (induct l, auto);
   313   apply (induct m, auto);
   314 done;
   315 
   316 (*
   317 lemma transfer_nat_int_fold1: "fold f l x =
   318     fold (%x. f (nat x)) (embed_list l) x";
   319 *)
   320 
   321 
   322 
   323 
   324 subsection {* Set up transfer from int to nat *}
   325 
   326 (* set up transfer direction *)
   327 
   328 lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
   329   by (simp add: TransferMorphism_def)
   330 
   331 declare TransferMorphism_int_nat[transfer add
   332   mode: manual
   333 (*  labels: int-nat *)
   334   return: nat_int
   335 ]
   336 
   337 
   338 (* basic functions and relations *)
   339 
   340 definition
   341   is_nat :: "int \<Rightarrow> bool"
   342 where
   343   "is_nat x = (x >= 0)"
   344 
   345 lemma transfer_int_nat_numerals:
   346     "0 = int 0"
   347     "1 = int 1"
   348     "2 = int 2"
   349     "3 = int 3"
   350   by auto
   351 
   352 lemma transfer_int_nat_functions:
   353     "(int x) + (int y) = int (x + y)"
   354     "(int x) * (int y) = int (x * y)"
   355     "tsub (int x) (int y) = int (x - y)"
   356     "(int x)^n = int (x^n)"
   357     "(int x) div (int y) = int (x div y)"
   358     "(int x) mod (int y) = int (x mod y)"
   359   by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
   360 
   361 lemma transfer_int_nat_function_closures:
   362     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
   363     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
   364     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
   365     "is_nat x \<Longrightarrow> is_nat (x^n)"
   366     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
   367     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   368     "is_nat 0"
   369     "is_nat 1"
   370     "is_nat 2"
   371     "is_nat 3"
   372     "is_nat (int z)"
   373   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
   374 
   375 lemma transfer_int_nat_relations:
   376     "(int x = int y) = (x = y)"
   377     "(int x < int y) = (x < y)"
   378     "(int x <= int y) = (x <= y)"
   379     "(int x dvd int y) = (x dvd y)"
   380     "(even (int x)) = (even x)"
   381   by (auto simp add: zdvd_int even_nat_def)
   382 
   383 lemma UNIV_apply:
   384   "UNIV x = True"
   385   by (simp add: top_fun_eq top_bool_eq)
   386 
   387 declare TransferMorphism_int_nat[transfer add return:
   388   transfer_int_nat_numerals
   389   transfer_int_nat_functions
   390   transfer_int_nat_function_closures
   391   transfer_int_nat_relations
   392   UNIV_apply
   393 ]
   394 
   395 
   396 (* first-order quantifiers *)
   397 
   398 lemma transfer_int_nat_quantifiers:
   399     "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
   400     "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
   401   apply (subst all_nat)
   402   apply auto [1]
   403   apply (subst ex_nat)
   404   apply auto
   405 done
   406 
   407 declare TransferMorphism_int_nat[transfer add
   408   return: transfer_int_nat_quantifiers]
   409 
   410 
   411 (* if *)
   412 
   413 lemma int_if_cong: "(if P then (int x) else (int y)) =
   414     int (if P then x else y)"
   415   by auto
   416 
   417 declare TransferMorphism_int_nat [transfer add return: int_if_cong]
   418 
   419 
   420 
   421 (* operations with sets *)
   422 
   423 lemma transfer_int_nat_set_functions:
   424     "nat_set A \<Longrightarrow> card A = card (nat ` A)"
   425     "{} = int ` ({}::nat set)"
   426     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
   427     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
   428     "{x. x >= 0 & P x} = int ` {x. P(int x)}"
   429     "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
   430        (* need all variants of these! *)
   431   by (simp_all only: is_nat_def transfer_nat_int_set_functions
   432           transfer_nat_int_set_function_closures
   433           transfer_nat_int_set_return_embed nat_0_le
   434           cong: transfer_nat_int_set_cong)
   435 
   436 lemma transfer_int_nat_set_function_closures:
   437     "nat_set {}"
   438     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   439     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   440     "is_nat x \<Longrightarrow> nat_set {x..y}"
   441     "nat_set {x. x >= 0 & P x}"
   442     "nat_set (int ` C)"
   443     "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
   444   by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
   445 
   446 lemma transfer_int_nat_set_relations:
   447     "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
   448     "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
   449     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
   450     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
   451     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
   452   by (simp_all only: is_nat_def transfer_nat_int_set_relations
   453     transfer_nat_int_set_return_embed nat_0_le)
   454 
   455 lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
   456   by (simp only: transfer_nat_int_set_relations
   457     transfer_nat_int_set_function_closures
   458     transfer_nat_int_set_return_embed nat_0_le)
   459 
   460 lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
   461     {(x::nat). P x} = {x. P' x}"
   462   by auto
   463 
   464 declare TransferMorphism_int_nat[transfer add
   465   return: transfer_int_nat_set_functions
   466     transfer_int_nat_set_function_closures
   467     transfer_int_nat_set_relations
   468     transfer_int_nat_set_return_embed
   469   cong: transfer_int_nat_set_cong
   470 ]
   471 
   472 
   473 (* setsum and setprod *)
   474 
   475 (* this handles the case where the *domain* of f is int *)
   476 lemma transfer_int_nat_sum_prod:
   477     "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
   478     "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
   479   apply (subst setsum_reindex)
   480   apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
   481   apply (subst setprod_reindex)
   482   apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
   483             cong: setprod_cong)
   484 done
   485 
   486 (* this handles the case where the *range* of f is int *)
   487 lemma transfer_int_nat_sum_prod2:
   488     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
   489     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
   490       setprod f A = int(setprod (%x. nat (f x)) A)"
   491   unfolding is_nat_def
   492   apply (subst int_setsum, auto)
   493   apply (subst int_setprod, auto simp add: cong: setprod_cong)
   494 done
   495 
   496 declare TransferMorphism_int_nat[transfer add
   497   return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   498   cong: setsum_cong setprod_cong]
   499 
   500 
   501 subsection {* Test it out *}
   502 
   503 (* nat to int *)
   504 
   505 lemma ex1: "(x::nat) + y = y + x"
   506   by auto
   507 
   508 thm ex1 [transferred]
   509 
   510 lemma ex2: "(a::nat) div b * b + a mod b = a"
   511   by (rule mod_div_equality)
   512 
   513 thm ex2 [transferred]
   514 
   515 lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
   516   by auto
   517 
   518 thm ex3 [transferred natint]
   519 
   520 lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
   521   by auto
   522 
   523 thm ex4 [transferred]
   524 
   525 lemma ex5: "(2::nat) * (SUM i <= n. i) = n * (n + 1)"
   526   by (induct n rule: nat_induct, auto)
   527 
   528 thm ex5 [transferred]
   529 
   530 theorem ex6: "0 <= (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
   531   by (rule ex5 [transferred])
   532 
   533 thm ex6 [transferred]
   534 
   535 thm ex5 [transferred, transferred]
   536 
   537 end