src/HOL/Nat_Transfer.thy
changeset 35683 70ace653fe77
parent 35644 d20cf282342e
child 35821 ee34f03a7d26
     1.1 --- a/src/HOL/Nat_Transfer.thy	Tue Mar 09 18:33:01 2010 +0100
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Tue Mar 09 21:19:48 2010 +0100
     1.3 @@ -27,17 +27,17 @@
     1.4  text {* set up transfer direction *}
     1.5  
     1.6  lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))"
     1.7 -  by (simp add: transfer_morphism_def)
     1.8 +  by (fact transfer_morphismI)
     1.9  
    1.10 -declare transfer_morphism_nat_int [transfer
    1.11 -  add mode: manual
    1.12 +declare transfer_morphism_nat_int [transfer add
    1.13 +  mode: manual
    1.14    return: nat_0_le
    1.15 -  labels: natint
    1.16 +  labels: nat_int
    1.17  ]
    1.18  
    1.19  text {* basic functions and relations *}
    1.20  
    1.21 -lemma transfer_nat_int_numerals:
    1.22 +lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]:
    1.23      "(0::nat) = nat 0"
    1.24      "(1::nat) = nat 1"
    1.25      "(2::nat) = nat 2"
    1.26 @@ -52,8 +52,7 @@
    1.27  lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
    1.28    by (simp add: tsub_def)
    1.29  
    1.30 -
    1.31 -lemma transfer_nat_int_functions:
    1.32 +lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]:
    1.33      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
    1.34      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
    1.35      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
    1.36 @@ -61,7 +60,7 @@
    1.37    by (auto simp add: eq_nat_nat_iff nat_mult_distrib
    1.38        nat_power_eq tsub_def)
    1.39  
    1.40 -lemma transfer_nat_int_function_closures:
    1.41 +lemma transfer_nat_int_function_closures [transfer key: transfer_morphism_nat_int]:
    1.42      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
    1.43      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
    1.44      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
    1.45 @@ -73,7 +72,7 @@
    1.46      "int z >= 0"
    1.47    by (auto simp add: zero_le_mult_iff tsub_def)
    1.48  
    1.49 -lemma transfer_nat_int_relations:
    1.50 +lemma transfer_nat_int_relations [transfer key: transfer_morphism_nat_int]:
    1.51      "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    1.52        (nat (x::int) = nat y) = (x = y)"
    1.53      "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    1.54 @@ -84,13 +83,6 @@
    1.55        (nat (x::int) dvd nat y) = (x dvd y)"
    1.56    by (auto simp add: zdvd_int)
    1.57  
    1.58 -declare transfer_morphism_nat_int [transfer add return:
    1.59 -  transfer_nat_int_numerals
    1.60 -  transfer_nat_int_functions
    1.61 -  transfer_nat_int_function_closures
    1.62 -  transfer_nat_int_relations
    1.63 -]
    1.64 -
    1.65  
    1.66  text {* first-order quantifiers *}
    1.67  
    1.68 @@ -108,7 +100,7 @@
    1.69    then show "\<exists>x. P x" by auto
    1.70  qed
    1.71  
    1.72 -lemma transfer_nat_int_quantifiers:
    1.73 +lemma transfer_nat_int_quantifiers [transfer key: transfer_morphism_nat_int]:
    1.74      "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
    1.75      "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
    1.76    by (rule all_nat, rule ex_nat)
    1.77 @@ -123,18 +115,15 @@
    1.78    by auto
    1.79  
    1.80  declare transfer_morphism_nat_int [transfer add
    1.81 -  return: transfer_nat_int_quantifiers
    1.82    cong: all_cong ex_cong]
    1.83  
    1.84  
    1.85  text {* if *}
    1.86  
    1.87 -lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
    1.88 -    nat (if P then x else y)"
    1.89 +lemma nat_if_cong [transfer key: transfer_morphism_nat_int]:
    1.90 +  "(if P then (nat x) else (nat y)) = nat (if P then x else y)"
    1.91    by auto
    1.92  
    1.93 -declare transfer_morphism_nat_int [transfer add return: nat_if_cong]
    1.94 -
    1.95  
    1.96  text {* operations with sets *}
    1.97  
    1.98 @@ -276,22 +265,18 @@
    1.99  
   1.100  text {* set up transfer direction *}
   1.101  
   1.102 -lemma transfer_morphism_int_nat: "transfer_morphism int (UNIV :: nat set)"
   1.103 -  by (simp add: transfer_morphism_def)
   1.104 +lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)"
   1.105 +  by (fact transfer_morphismI)
   1.106  
   1.107  declare transfer_morphism_int_nat [transfer add
   1.108    mode: manual
   1.109 -(*  labels: int-nat *)
   1.110    return: nat_int
   1.111 +  labels: int_nat
   1.112  ]
   1.113  
   1.114  
   1.115  text {* basic functions and relations *}
   1.116  
   1.117 -lemma UNIV_apply:
   1.118 -  "UNIV x = True"
   1.119 -  by (simp add: top_fun_eq top_bool_eq)
   1.120 -
   1.121  definition
   1.122    is_nat :: "int \<Rightarrow> bool"
   1.123  where
   1.124 @@ -335,7 +320,6 @@
   1.125    transfer_int_nat_functions
   1.126    transfer_int_nat_function_closures
   1.127    transfer_int_nat_relations
   1.128 -  UNIV_apply
   1.129  ]
   1.130  
   1.131