src/HOL/Nat_Transfer.thy
 changeset 66836 4eb431c3f974 parent 66817 0b12755ccbb2
```     1.1 --- a/src/HOL/Nat_Transfer.thy	Tue Oct 10 22:18:58 2017 +0100
1.2 +++ b/src/HOL/Nat_Transfer.thy	Mon Oct 09 19:10:47 2017 +0200
1.3 @@ -3,7 +3,7 @@
1.4  section \<open>Generic transfer machinery;  specific transfer from nats to ints and back.\<close>
1.5
1.6  theory Nat_Transfer
1.7 -imports Int Divides
1.8 +imports List GCD
1.9  begin
1.10
1.11  subsection \<open>Generic transfer machinery\<close>
1.12 @@ -90,34 +90,11 @@
1.13
1.14  text \<open>first-order quantifiers\<close>
1.15
1.16 -lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
1.17 -  by (simp split: split_nat)
1.18 -
1.19 -lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
1.20 -proof
1.21 -  assume "\<exists>x. P x"
1.22 -  then obtain x where "P x" ..
1.23 -  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
1.24 -  then show "\<exists>x\<ge>0. P (nat x)" ..
1.25 -next
1.26 -  assume "\<exists>x\<ge>0. P (nat x)"
1.27 -  then show "\<exists>x. P x" by auto
1.28 -qed
1.29 -
1.30  lemma transfer_nat_int_quantifiers [no_atp, transfer key: transfer_morphism_nat_int]:
1.31      "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
1.32      "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
1.33    by (rule all_nat, rule ex_nat)
1.34
1.35 -(* should we restrict these? *)
1.36 -lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
1.37 -    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
1.38 -  by auto
1.39 -
1.40 -lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
1.41 -    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
1.42 -  by auto
1.43 -
1.45    cong: all_cong ex_cong]
1.46
1.47 @@ -142,17 +119,10 @@
1.48      "A Un B = nat ` (int ` A Un int ` B)"
1.49      "A Int B = nat ` (int ` A Int int ` B)"
1.50      "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
1.51 -  apply (rule card_image [symmetric])
1.52 -  apply (auto simp add: inj_on_def image_def)
1.53 -  apply (rule_tac x = "int x" in bexI)
1.54 -  apply auto
1.55 -  apply (rule_tac x = "int x" in bexI)
1.56 -  apply auto
1.57 -  apply (rule_tac x = "int x" in bexI)
1.58 -  apply auto
1.59 -  apply (rule_tac x = "int x" in exI)
1.60 -  apply auto
1.61 -done
1.62 +    "{..n} = nat ` {0..int n}"
1.63 +    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
1.64 +  by (rule card_image [symmetric])
1.65 +    (auto simp add: inj_on_def image_def intro: bexI [of _ "int x" for x] exI [of _ "int x" for x])
1.66
1.67  lemma transfer_nat_int_set_function_closures [no_atp]:
1.68      "nat_set {}"
1.69 @@ -161,6 +131,7 @@
1.70      "nat_set {x. x >= 0 & P x}"
1.71      "nat_set (int ` C)"
1.72      "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
1.73 +    "x >= 0 \<Longrightarrow> nat_set {x..y}"
1.74    unfolding nat_set_def apply auto
1.75  done
1.76
1.77 @@ -361,6 +332,7 @@
1.78      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
1.79      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
1.80      "{x. x >= 0 & P x} = int ` {x. P(int x)}"
1.81 +    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
1.82         (* need all variants of these! *)
1.83    by (simp_all only: is_nat_def transfer_nat_int_set_functions
1.84            transfer_nat_int_set_function_closures
1.85 @@ -374,6 +346,7 @@
1.86      "nat_set {x. x >= 0 & P x}"
1.87      "nat_set (int ` C)"
1.88      "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
1.89 +    "is_nat x \<Longrightarrow> nat_set {x..y}"
1.90    by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
1.91
1.92  lemma transfer_int_nat_set_relations [no_atp]:
1.93 @@ -430,4 +403,62 @@
1.94
1.95  declare transfer_morphism_int_nat [transfer add return: even_int_iff]
1.96
1.97 +lemma transfer_nat_int_gcd [no_atp]:
1.98 +  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
1.99 +  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
1.100 +  for x y :: int
1.101 +  unfolding gcd_int_def lcm_int_def by auto
1.102 +
1.103 +lemma transfer_nat_int_gcd_closures [no_atp]:
1.104 +  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
1.105 +  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
1.106 +  for x y :: int
1.107 +  by (auto simp add: gcd_int_def lcm_int_def)
1.108 +
1.109 +declare transfer_morphism_nat_int
1.110 +  [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
1.111 +
1.112 +lemma transfer_int_nat_gcd [no_atp]:
1.113 +  "gcd (int x) (int y) = int (gcd x y)"
1.114 +  "lcm (int x) (int y) = int (lcm x y)"
1.115 +  by (auto simp: gcd_int_def lcm_int_def)
1.116 +
1.117 +lemma transfer_int_nat_gcd_closures [no_atp]:
1.118 +  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
1.119 +  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
1.120 +  by (auto simp: gcd_int_def lcm_int_def)
1.121 +
1.122 +declare transfer_morphism_int_nat
1.123 +  [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
1.124 +
1.125 +definition embed_list :: "nat list \<Rightarrow> int list" where
1.126 +"embed_list l = map int l"
1.127 +
1.128 +definition nat_list :: "int list \<Rightarrow> bool" where
1.129 +"nat_list l = nat_set (set l)"
1.130 +
1.131 +definition return_list :: "int list \<Rightarrow> nat list" where
1.132 +"return_list l = map nat l"
1.133 +
1.134 +lemma transfer_nat_int_list_return_embed [no_atp]:
1.135 +  "nat_list l \<longrightarrow> embed_list (return_list l) = l"
1.136 +  unfolding embed_list_def return_list_def nat_list_def nat_set_def
1.137 +  apply (induct l)
1.138 +  apply auto
1.139 +done
1.140 +
1.141 +lemma transfer_nat_int_list_functions [no_atp]:
1.142 +  "l @ m = return_list (embed_list l @ embed_list m)"
1.143 +  "[] = return_list []"
1.144 +  unfolding return_list_def embed_list_def
1.145 +  apply auto
1.146 +  apply (induct l, auto)
1.147 +  apply (induct m, auto)
1.148 +done
1.149 +
1.150 +(*
1.151 +lemma transfer_nat_int_fold1: "fold f l x =
1.152 +    fold (%x. f (nat x)) (embed_list l) x";
1.153 +*)
1.154 +
1.155  end
```