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.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.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.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.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
```