wneuper/isa: src/HOL/Nat_Transfer.thy@91c4d7397f0e

     2 (* Authors: Jeremy Avigad and Amine Chaieb *)

     4 header {* Generic transfer machinery;  specific transfer from nats to ints and back. *}

     6 theory Nat_Transfer

     7 imports Nat_Numeral

     8 uses ("Tools/transfer.ML")

     9 begin

    11 subsection {* Generic transfer machinery *}

    13 definition transfer_morphism:: "('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"

    14   where "transfer_morphism f A \<longleftrightarrow> True"

    16 lemma transfer_morphismI[intro]: "transfer_morphism f A"

    17   by (simp add: transfer_morphism_def)

    19 use "Tools/transfer.ML"

    21 setup Transfer.setup

    24 subsection {* Set up transfer from nat to int *}

    26 text {* set up transfer direction *}

    28 lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" ..

    30 declare transfer_morphism_nat_int [transfer add

    31   mode: manual

    32   return: nat_0_le

    33   labels: nat_int

    34 ]

    36 text {* basic functions and relations *}

    38 lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]:

    39     "(0::nat) = nat 0"

    40     "(1::nat) = nat 1"

    41     "(2::nat) = nat 2"

    42     "(3::nat) = nat 3"

    43   by auto

    45 definition

    46   tsub :: "int \<Rightarrow> int \<Rightarrow> int"

    47 where

    48   "tsub x y = (if x >= y then x - y else 0)"

    50 lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"

    51   by (simp add: tsub_def)

    53 lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]:

    54     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"

    55     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"

    56     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"

    57     "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"

    58   by (auto simp add: eq_nat_nat_iff nat_mult_distrib

    59       nat_power_eq tsub_def)

    61 lemma transfer_nat_int_function_closures [transfer key: transfer_morphism_nat_int]:

    62     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"

    63     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"

    64     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"

    65     "(x::int) >= 0 \<Longrightarrow> x^n >= 0"

    66     "(0::int) >= 0"

    67     "(1::int) >= 0"

    68     "(2::int) >= 0"

    69     "(3::int) >= 0"

    70     "int z >= 0"

    71   by (auto simp add: zero_le_mult_iff tsub_def)

    73 lemma transfer_nat_int_relations [transfer key: transfer_morphism_nat_int]:

    74     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>

    75       (nat (x::int) = nat y) = (x = y)"

    76     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>

    77       (nat (x::int) < nat y) = (x < y)"

    78     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>

    79       (nat (x::int) <= nat y) = (x <= y)"

    80     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>

    81       (nat (x::int) dvd nat y) = (x dvd y)"

    82   by (auto simp add: zdvd_int)

    85 text {* first-order quantifiers *}

    87 lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"

    88   by (simp split add: split_nat)

    90 lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"

    91 proof

    92   assume "\<exists>x. P x"

    93   then obtain x where "P x" ..

    94   then have "int x \<ge> 0 \<and> P (nat (int x))" by simp

    95   then show "\<exists>x\<ge>0. P (nat x)" ..

    96 next

    97   assume "\<exists>x\<ge>0. P (nat x)"

    98   then show "\<exists>x. P x" by auto

    99 qed

   101 lemma transfer_nat_int_quantifiers [transfer key: transfer_morphism_nat_int]:

   102     "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"

   103     "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"

   104   by (rule all_nat, rule ex_nat)

   106 (* should we restrict these? *)

   107 lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>

   108     (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"

   109   by auto

   111 lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>

   112     (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"

   113   by auto

   115 declare transfer_morphism_nat_int [transfer add

   116   cong: all_cong ex_cong]

   119 text {* if *}

   121 lemma nat_if_cong [transfer key: transfer_morphism_nat_int]:

   122   "(if P then (nat x) else (nat y)) = nat (if P then x else y)"

   123   by auto

   126 text {* operations with sets *}

   128 definition

   129   nat_set :: "int set \<Rightarrow> bool"

   130 where

   131   "nat_set S = (ALL x:S. x >= 0)"

   133 lemma transfer_nat_int_set_functions:

   134     "card A = card (int ` A)"

   135     "{} = nat ` ({}::int set)"

   136     "A Un B = nat ` (int ` A Un int ` B)"

   137     "A Int B = nat ` (int ` A Int int ` B)"

   138     "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"

   139   apply (rule card_image [symmetric])

   140   apply (auto simp add: inj_on_def image_def)

   141   apply (rule_tac x = "int x" in bexI)

   142   apply auto

   143   apply (rule_tac x = "int x" in bexI)

   144   apply auto

   145   apply (rule_tac x = "int x" in bexI)

   146   apply auto

   147   apply (rule_tac x = "int x" in exI)

   148   apply auto

   149 done

   151 lemma transfer_nat_int_set_function_closures:

   152     "nat_set {}"

   153     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"

   154     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"

   155     "nat_set {x. x >= 0 & P x}"

   156     "nat_set (int ` C)"

   157     "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)

   158   unfolding nat_set_def apply auto

   159 done

   161 lemma transfer_nat_int_set_relations:

   162     "(finite A) = (finite (int ` A))"

   163     "(x : A) = (int x : int ` A)"

   164     "(A = B) = (int ` A = int ` B)"

   165     "(A < B) = (int ` A < int ` B)"

   166     "(A <= B) = (int ` A <= int ` B)"

   167   apply (rule iffI)

   168   apply (erule finite_imageI)

   169   apply (erule finite_imageD)

   170   apply (auto simp add: image_def set_eq_iff inj_on_def)

   171   apply (drule_tac x = "int x" in spec, auto)

   172   apply (drule_tac x = "int x" in spec, auto)

   173   apply (drule_tac x = "int x" in spec, auto)

   174 done

   176 lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>

   177     (int ` nat ` A = A)"

   178   by (auto simp add: nat_set_def image_def)

   180 lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>

   181     {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"

   182   by auto

   184 declare transfer_morphism_nat_int [transfer add

   185   return: transfer_nat_int_set_functions

   186     transfer_nat_int_set_function_closures

   187     transfer_nat_int_set_relations

   188     transfer_nat_int_set_return_embed

   189   cong: transfer_nat_int_set_cong

   190 ]

   193 text {* setsum and setprod *}

   195 (* this handles the case where the *domain* of f is nat *)

   196 lemma transfer_nat_int_sum_prod:

   197     "setsum f A = setsum (%x. f (nat x)) (int ` A)"

   198     "setprod f A = setprod (%x. f (nat x)) (int ` A)"

   199   apply (subst setsum_reindex)

   200   apply (unfold inj_on_def, auto)

   201   apply (subst setprod_reindex)

   202   apply (unfold inj_on_def o_def, auto)

   203 done

   205 (* this handles the case where the *range* of f is nat *)

   206 lemma transfer_nat_int_sum_prod2:

   207     "setsum f A = nat(setsum (%x. int (f x)) A)"

   208     "setprod f A = nat(setprod (%x. int (f x)) A)"

   209   apply (subst int_setsum [symmetric])

   210   apply auto

   211   apply (subst int_setprod [symmetric])

   212   apply auto

   213 done

   215 lemma transfer_nat_int_sum_prod_closure:

   216     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"

   217     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"

   218   unfolding nat_set_def

   219   apply (rule setsum_nonneg)

   220   apply auto

   221   apply (rule setprod_nonneg)

   222   apply auto

   223 done

   225 (* this version doesn't work, even with nat_set A \<Longrightarrow>

   226       x : A \<Longrightarrow> x >= 0 turned on. Why not?

   228   also: what does =simp=> do?

   230 lemma transfer_nat_int_sum_prod_closure:

   231     "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"

   232     "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"

   233   unfolding nat_set_def simp_implies_def

   234   apply (rule setsum_nonneg)

   235   apply auto

   236   apply (rule setprod_nonneg)

   237   apply auto

   238 done

   239 *)

   241 (* Making A = B in this lemma doesn't work. Why not?

   242    Also, why aren't setsum_cong and setprod_cong enough,

   243    with the previously mentioned rule turned on? *)

   245 lemma transfer_nat_int_sum_prod_cong:

   246     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>

   247       setsum f A = setsum g B"

   248     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>

   249       setprod f A = setprod g B"

   250   unfolding nat_set_def

   251   apply (subst setsum_cong, assumption)

   252   apply auto [2]

   253   apply (subst setprod_cong, assumption, auto)

   254 done

   256 declare transfer_morphism_nat_int [transfer add

   257   return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2

   258     transfer_nat_int_sum_prod_closure

   259   cong: transfer_nat_int_sum_prod_cong]

   262 subsection {* Set up transfer from int to nat *}

   264 text {* set up transfer direction *}

   266 lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)" ..

   268 declare transfer_morphism_int_nat [transfer add

   269   mode: manual

   270   return: nat_int

   271   labels: int_nat

   272 ]

   275 text {* basic functions and relations *}

   277 definition

   278   is_nat :: "int \<Rightarrow> bool"

   279 where

   280   "is_nat x = (x >= 0)"

   282 lemma transfer_int_nat_numerals:

   283     "0 = int 0"

   284     "1 = int 1"

   285     "2 = int 2"

   286     "3 = int 3"

   287   by auto

   289 lemma transfer_int_nat_functions:

   290     "(int x) + (int y) = int (x + y)"

   291     "(int x) * (int y) = int (x * y)"

   292     "tsub (int x) (int y) = int (x - y)"

   293     "(int x)^n = int (x^n)"

   294   by (auto simp add: int_mult tsub_def int_power)

   296 lemma transfer_int_nat_function_closures:

   297     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"

   298     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"

   299     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"

   300     "is_nat x \<Longrightarrow> is_nat (x^n)"

   301     "is_nat 0"

   302     "is_nat 1"

   303     "is_nat 2"

   304     "is_nat 3"

   305     "is_nat (int z)"

   306   by (simp_all only: is_nat_def transfer_nat_int_function_closures)

   308 lemma transfer_int_nat_relations:

   309     "(int x = int y) = (x = y)"

   310     "(int x < int y) = (x < y)"

   311     "(int x <= int y) = (x <= y)"

   312     "(int x dvd int y) = (x dvd y)"

   313   by (auto simp add: zdvd_int)

   315 declare transfer_morphism_int_nat [transfer add return:

   316   transfer_int_nat_numerals

   317   transfer_int_nat_functions

   318   transfer_int_nat_function_closures

   319   transfer_int_nat_relations

   320 ]

   323 text {* first-order quantifiers *}

   325 lemma transfer_int_nat_quantifiers:

   326     "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"

   327     "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"

   328   apply (subst all_nat)

   329   apply auto [1]

   330   apply (subst ex_nat)

   331   apply auto

   332 done

   334 declare transfer_morphism_int_nat [transfer add

   335   return: transfer_int_nat_quantifiers]

   338 text {* if *}

   340 lemma int_if_cong: "(if P then (int x) else (int y)) =

   341     int (if P then x else y)"

   342   by auto

   344 declare transfer_morphism_int_nat [transfer add return: int_if_cong]

   348 text {* operations with sets *}

   350 lemma transfer_int_nat_set_functions:

   351     "nat_set A \<Longrightarrow> card A = card (nat ` A)"

   352     "{} = int ` ({}::nat set)"

   353     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"

   354     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"

   355     "{x. x >= 0 & P x} = int ` {x. P(int x)}"

   356        (* need all variants of these! *)

   357   by (simp_all only: is_nat_def transfer_nat_int_set_functions

   358           transfer_nat_int_set_function_closures

   359           transfer_nat_int_set_return_embed nat_0_le

   360           cong: transfer_nat_int_set_cong)

   362 lemma transfer_int_nat_set_function_closures:

   363     "nat_set {}"

   364     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"

   365     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"

   366     "nat_set {x. x >= 0 & P x}"

   367     "nat_set (int ` C)"

   368     "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"

   369   by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)

   371 lemma transfer_int_nat_set_relations:

   372     "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"

   373     "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"

   374     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"

   375     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"

   376     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"

   377   by (simp_all only: is_nat_def transfer_nat_int_set_relations

   378     transfer_nat_int_set_return_embed nat_0_le)

   380 lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"

   381   by (simp only: transfer_nat_int_set_relations

   382     transfer_nat_int_set_function_closures

   383     transfer_nat_int_set_return_embed nat_0_le)

   385 lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>

   386     {(x::nat). P x} = {x. P' x}"

   387   by auto

   389 declare transfer_morphism_int_nat [transfer add

   390   return: transfer_int_nat_set_functions

   391     transfer_int_nat_set_function_closures

   392     transfer_int_nat_set_relations

   393     transfer_int_nat_set_return_embed

   394   cong: transfer_int_nat_set_cong

   395 ]

   398 text {* setsum and setprod *}

   400 (* this handles the case where the *domain* of f is int *)

   401 lemma transfer_int_nat_sum_prod:

   402     "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"

   403     "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"

   404   apply (subst setsum_reindex)

   405   apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)

   406   apply (subst setprod_reindex)

   407   apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff

   408             cong: setprod_cong)

   409 done

   411 (* this handles the case where the *range* of f is int *)

   412 lemma transfer_int_nat_sum_prod2:

   413     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"

   414     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>

   415       setprod f A = int(setprod (%x. nat (f x)) A)"

   416   unfolding is_nat_def

   417   apply (subst int_setsum, auto)

   418   apply (subst int_setprod, auto simp add: cong: setprod_cong)

   419 done

   421 declare transfer_morphism_int_nat [transfer add

   422   return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2

   423   cong: setsum_cong setprod_cong]

   425 end

author	wenzelm
	Thu, 07 Jul 2011 23:55:15 +0200
changeset 44572	91c4d7397f0e
parent 43739	36abaf4cce1f
child 48116	30a1692557b0
permissions	-rw-r--r--