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.44  declare transfer_morphism_nat_int [transfer add
    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