moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
authorhaftmann
Thu Oct 29 11:41:36 2009 +0100 (2009-10-29)
changeset 33318ddd97d9dfbfb
parent 33298 dfda74619509
child 33319 74f0dcc0b5fb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Fun.thy
src/HOL/GCD.thy
src/HOL/IntDiv.thy
src/HOL/IsaMakefile
src/HOL/List.thy
src/HOL/Nat_Transfer.thy
src/HOL/Parity.thy
src/HOL/Presburger.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Oct 29 08:14:39 2009 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Oct 29 11:41:36 2009 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  header {* Type of target language numerals *}
     1.5  
     1.6  theory Code_Numeral
     1.7 -imports Nat_Numeral Divides
     1.8 +imports Nat_Numeral Nat_Transfer Divides
     1.9  begin
    1.10  
    1.11  text {*
     2.1 --- a/src/HOL/Divides.thy	Thu Oct 29 08:14:39 2009 +0100
     2.2 +++ b/src/HOL/Divides.thy	Thu Oct 29 11:41:36 2009 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* The division operators div and mod *}
     2.5  
     2.6  theory Divides
     2.7 -imports Nat_Numeral
     2.8 +imports Nat_Numeral Nat_Transfer
     2.9  uses
    2.10    "~~/src/Provers/Arith/assoc_fold.ML"
    2.11    "~~/src/Provers/Arith/cancel_numerals.ML"
     3.1 --- a/src/HOL/Fun.thy	Thu Oct 29 08:14:39 2009 +0100
     3.2 +++ b/src/HOL/Fun.thy	Thu Oct 29 11:41:36 2009 +0100
     3.3 @@ -7,7 +7,6 @@
     3.4  
     3.5  theory Fun
     3.6  imports Complete_Lattice
     3.7 -uses ("Tools/transfer.ML")
     3.8  begin
     3.9  
    3.10  text{*As a simplification rule, it replaces all function equalities by
    3.11 @@ -604,16 +603,6 @@
    3.12  *}
    3.13  
    3.14  
    3.15 -subsection {* Generic transfer procedure *}
    3.16 -
    3.17 -definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
    3.18 -  where "TransferMorphism a B \<longleftrightarrow> True"
    3.19 -
    3.20 -use "Tools/transfer.ML"
    3.21 -
    3.22 -setup Transfer.setup
    3.23 -
    3.24 -
    3.25  subsection {* Code generator setup *}
    3.26  
    3.27  types_code
     4.1 --- a/src/HOL/GCD.thy	Thu Oct 29 08:14:39 2009 +0100
     4.2 +++ b/src/HOL/GCD.thy	Thu Oct 29 11:41:36 2009 +0100
     4.3 @@ -28,7 +28,7 @@
     4.4  header {* GCD *}
     4.5  
     4.6  theory GCD
     4.7 -imports Fact
     4.8 +imports Fact Parity
     4.9  begin
    4.10  
    4.11  declare One_nat_def [simp del]
     5.1 --- a/src/HOL/IntDiv.thy	Thu Oct 29 08:14:39 2009 +0100
     5.2 +++ b/src/HOL/IntDiv.thy	Thu Oct 29 11:41:36 2009 +0100
     5.3 @@ -1024,139 +1024,16 @@
     5.4  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
     5.5    dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
     5.6  
     5.7 -lemma zdvd_anti_sym:
     5.8 -    "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
     5.9 -  apply (simp add: dvd_def, auto)
    5.10 -  apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
    5.11 -  done
    5.12 -
    5.13 -lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a" 
    5.14 -  shows "\<bar>a\<bar> = \<bar>b\<bar>"
    5.15 -proof-
    5.16 -  from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
    5.17 -  from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
    5.18 -  from k k' have "a = a*k*k'" by simp
    5.19 -  with mult_cancel_left1[where c="a" and b="k*k'"]
    5.20 -  have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
    5.21 -  hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
    5.22 -  thus ?thesis using k k' by auto
    5.23 -qed
    5.24 -
    5.25 -lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
    5.26 -  apply (subgoal_tac "m = n + (m - n)")
    5.27 -   apply (erule ssubst)
    5.28 -   apply (blast intro: dvd_add, simp)
    5.29 -  done
    5.30 -
    5.31 -lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
    5.32 -apply (rule iffI)
    5.33 - apply (erule_tac [2] dvd_add)
    5.34 - apply (subgoal_tac "n = (n + k * m) - k * m")
    5.35 -  apply (erule ssubst)
    5.36 -  apply (erule dvd_diff)
    5.37 -  apply(simp_all)
    5.38 -done
    5.39 -
    5.40  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
    5.41    by (rule dvd_mod) (* TODO: remove *)
    5.42  
    5.43  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
    5.44    by (rule dvd_mod_imp_dvd) (* TODO: remove *)
    5.45  
    5.46 -lemma dvd_imp_le_int: "(i::int) ~= 0 ==> d dvd i ==> abs d <= abs i"
    5.47 -apply(auto simp:abs_if)
    5.48 -   apply(clarsimp simp:dvd_def mult_less_0_iff)
    5.49 -  using mult_le_cancel_left_neg[of _ "-1::int"]
    5.50 -  apply(clarsimp simp:dvd_def mult_less_0_iff)
    5.51 - apply(clarsimp simp:dvd_def mult_less_0_iff
    5.52 -         minus_mult_right simp del: mult_minus_right)
    5.53 -apply(clarsimp simp:dvd_def mult_less_0_iff)
    5.54 -done
    5.55 -
    5.56 -lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
    5.57 -  apply (auto elim!: dvdE)
    5.58 -  apply (subgoal_tac "0 < n")
    5.59 -   prefer 2
    5.60 -   apply (blast intro: order_less_trans)
    5.61 -  apply (simp add: zero_less_mult_iff)
    5.62 -  done
    5.63 -
    5.64  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
    5.65    using zmod_zdiv_equality[where a="m" and b="n"]
    5.66    by (simp add: algebra_simps)
    5.67  
    5.68 -lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
    5.69 -apply (subgoal_tac "m mod n = 0")
    5.70 - apply (simp add: zmult_div_cancel)
    5.71 -apply (simp only: dvd_eq_mod_eq_0)
    5.72 -done
    5.73 -
    5.74 -lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
    5.75 -  shows "m dvd n"
    5.76 -proof-
    5.77 -  from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
    5.78 -  {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
    5.79 -    with h have False by (simp add: mult_assoc)}
    5.80 -  hence "n = m * h" by blast
    5.81 -  thus ?thesis by simp
    5.82 -qed
    5.83 -
    5.84 -theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
    5.85 -proof -
    5.86 -  have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
    5.87 -  proof -
    5.88 -    fix k
    5.89 -    assume A: "int y = int x * k"
    5.90 -    then show "x dvd y" proof (cases k)
    5.91 -      case (1 n) with A have "y = x * n" by (simp add: zmult_int)
    5.92 -      then show ?thesis ..
    5.93 -    next
    5.94 -      case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
    5.95 -      also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
    5.96 -      also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int)
    5.97 -      finally have "- int (x * Suc n) = int y" ..
    5.98 -      then show ?thesis by (simp only: negative_eq_positive) auto
    5.99 -    qed
   5.100 -  qed
   5.101 -  then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult)
   5.102 -qed
   5.103 -
   5.104 -lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
   5.105 -proof
   5.106 -  assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
   5.107 -  hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
   5.108 -  hence "nat \<bar>x\<bar> = 1"  by simp
   5.109 -  thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
   5.110 -next
   5.111 -  assume "\<bar>x\<bar>=1" thus "x dvd 1" 
   5.112 -    by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0)
   5.113 -qed
   5.114 -lemma zdvd_mult_cancel1: 
   5.115 -  assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
   5.116 -proof
   5.117 -  assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
   5.118 -    by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
   5.119 -next
   5.120 -  assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
   5.121 -  from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
   5.122 -qed
   5.123 -
   5.124 -lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
   5.125 -  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
   5.126 -
   5.127 -lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
   5.128 -  unfolding zdvd_int by (cases "z \<ge> 0") simp_all
   5.129 -
   5.130 -lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
   5.131 -  by (auto simp add: dvd_int_iff)
   5.132 -
   5.133 -lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   5.134 -  apply (rule_tac z=n in int_cases)
   5.135 -  apply (auto simp add: dvd_int_iff)
   5.136 -  apply (rule_tac z=z in int_cases)
   5.137 -  apply (auto simp add: dvd_imp_le)
   5.138 -  done
   5.139 -
   5.140  lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
   5.141  apply (induct "y", auto)
   5.142  apply (rule zmod_zmult1_eq [THEN trans])
   5.143 @@ -1182,6 +1059,12 @@
   5.144  lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
   5.145  by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
   5.146  
   5.147 +lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
   5.148 +apply (subgoal_tac "m mod n = 0")
   5.149 + apply (simp add: zmult_div_cancel)
   5.150 +apply (simp only: dvd_eq_mod_eq_0)
   5.151 +done
   5.152 +
   5.153  text{*Suggested by Matthias Daum*}
   5.154  lemma int_power_div_base:
   5.155       "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
   5.156 @@ -1349,6 +1232,43 @@
   5.157  declare dvd_eq_mod_eq_0_number_of [simp]
   5.158  
   5.159  
   5.160 +subsection {* Transfer setup *}
   5.161 +
   5.162 +lemma transfer_nat_int_functions:
   5.163 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
   5.164 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
   5.165 +  by (auto simp add: nat_div_distrib nat_mod_distrib)
   5.166 +
   5.167 +lemma transfer_nat_int_function_closures:
   5.168 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
   5.169 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
   5.170 +  apply (cases "y = 0")
   5.171 +  apply (auto simp add: pos_imp_zdiv_nonneg_iff)
   5.172 +  apply (cases "y = 0")
   5.173 +  apply auto
   5.174 +done
   5.175 +
   5.176 +declare TransferMorphism_nat_int[transfer add return:
   5.177 +  transfer_nat_int_functions
   5.178 +  transfer_nat_int_function_closures
   5.179 +]
   5.180 +
   5.181 +lemma transfer_int_nat_functions:
   5.182 +    "(int x) div (int y) = int (x div y)"
   5.183 +    "(int x) mod (int y) = int (x mod y)"
   5.184 +  by (auto simp add: zdiv_int zmod_int)
   5.185 +
   5.186 +lemma transfer_int_nat_function_closures:
   5.187 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
   5.188 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   5.189 +  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
   5.190 +
   5.191 +declare TransferMorphism_int_nat[transfer add return:
   5.192 +  transfer_int_nat_functions
   5.193 +  transfer_int_nat_function_closures
   5.194 +]
   5.195 +
   5.196 +
   5.197  subsection {* Code generation *}
   5.198  
   5.199  definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
     6.1 --- a/src/HOL/IsaMakefile	Thu Oct 29 08:14:39 2009 +0100
     6.2 +++ b/src/HOL/IsaMakefile	Thu Oct 29 11:41:36 2009 +0100
     6.3 @@ -223,7 +223,6 @@
     6.4    Tools/sat_funcs.ML \
     6.5    Tools/sat_solver.ML \
     6.6    Tools/split_rule.ML \
     6.7 -  Tools/transfer.ML \
     6.8    Tools/typecopy.ML \
     6.9    Tools/typedef_codegen.ML \
    6.10    Tools/typedef.ML \
    6.11 @@ -255,6 +254,7 @@
    6.12    Main.thy \
    6.13    Map.thy \
    6.14    Nat_Numeral.thy \
    6.15 +  Nat_Transfer.thy \
    6.16    Presburger.thy \
    6.17    Predicate_Compile.thy \
    6.18    Quickcheck.thy \
    6.19 @@ -276,6 +276,7 @@
    6.20    Tools/Groebner_Basis/misc.ML \
    6.21    Tools/Groebner_Basis/normalizer.ML \
    6.22    Tools/Groebner_Basis/normalizer_data.ML \
    6.23 +  Tools/choice_specification.ML \
    6.24    Tools/int_arith.ML \
    6.25    Tools/list_code.ML \
    6.26    Tools/meson.ML \
    6.27 @@ -299,7 +300,6 @@
    6.28    Tools/Qelim/presburger.ML \
    6.29    Tools/Qelim/qelim.ML \
    6.30    Tools/recdef.ML \
    6.31 -  Tools/choice_specification.ML \
    6.32    Tools/res_atp.ML \
    6.33    Tools/res_axioms.ML \
    6.34    Tools/res_clause.ML \
    6.35 @@ -307,6 +307,7 @@
    6.36    Tools/res_reconstruct.ML \
    6.37    Tools/string_code.ML \
    6.38    Tools/string_syntax.ML \
    6.39 +  Tools/transfer.ML \
    6.40    Tools/TFL/casesplit.ML \
    6.41    Tools/TFL/dcterm.ML \
    6.42    Tools/TFL/post.ML \
    6.43 @@ -334,7 +335,6 @@
    6.44    Log.thy \
    6.45    Lubs.thy \
    6.46    MacLaurin.thy \
    6.47 -  Nat_Transfer.thy \
    6.48    NthRoot.thy \
    6.49    PReal.thy \
    6.50    Parity.thy \
     7.1 --- a/src/HOL/List.thy	Thu Oct 29 08:14:39 2009 +0100
     7.2 +++ b/src/HOL/List.thy	Thu Oct 29 11:41:36 2009 +0100
     7.3 @@ -3587,8 +3587,8 @@
     7.4  by (blast intro: listrel.intros)
     7.5  
     7.6  lemma listrel_Cons:
     7.7 -     "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
     7.8 -by (auto simp add: set_Cons_def intro: listrel.intros) 
     7.9 +     "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"
    7.10 +by (auto simp add: set_Cons_def intro: listrel.intros)
    7.11  
    7.12  
    7.13  subsection {* Size function *}
    7.14 @@ -3615,6 +3615,45 @@
    7.15  by (induct xs) force+
    7.16  
    7.17  
    7.18 +subsection {* Transfer *}
    7.19 +
    7.20 +definition
    7.21 +  embed_list :: "nat list \<Rightarrow> int list"
    7.22 +where
    7.23 +  "embed_list l = map int l"
    7.24 +
    7.25 +definition
    7.26 +  nat_list :: "int list \<Rightarrow> bool"
    7.27 +where
    7.28 +  "nat_list l = nat_set (set l)"
    7.29 +
    7.30 +definition
    7.31 +  return_list :: "int list \<Rightarrow> nat list"
    7.32 +where
    7.33 +  "return_list l = map nat l"
    7.34 +
    7.35 +lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
    7.36 +    embed_list (return_list l) = l"
    7.37 +  unfolding embed_list_def return_list_def nat_list_def nat_set_def
    7.38 +  apply (induct l)
    7.39 +  apply auto
    7.40 +done
    7.41 +
    7.42 +lemma transfer_nat_int_list_functions:
    7.43 +  "l @ m = return_list (embed_list l @ embed_list m)"
    7.44 +  "[] = return_list []"
    7.45 +  unfolding return_list_def embed_list_def
    7.46 +  apply auto
    7.47 +  apply (induct l, auto)
    7.48 +  apply (induct m, auto)
    7.49 +done
    7.50 +
    7.51 +(*
    7.52 +lemma transfer_nat_int_fold1: "fold f l x =
    7.53 +    fold (%x. f (nat x)) (embed_list l) x";
    7.54 +*)
    7.55 +
    7.56 +
    7.57  subsection {* Code generator *}
    7.58  
    7.59  subsubsection {* Setup *}
    7.60 @@ -4017,5 +4056,4 @@
    7.61    "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
    7.62  by(simp add: all_from_to_int_iff_ball list_ex_iff)
    7.63  
    7.64 -
    7.65  end
     8.1 --- a/src/HOL/Nat_Transfer.thy	Thu Oct 29 08:14:39 2009 +0100
     8.2 +++ b/src/HOL/Nat_Transfer.thy	Thu Oct 29 11:41:36 2009 +0100
     8.3 @@ -1,15 +1,26 @@
     8.4  
     8.5  (* Authors: Jeremy Avigad and Amine Chaieb *)
     8.6  
     8.7 -header {* Sets up transfer from nats to ints and back. *}
     8.8 +header {* Generic transfer machinery;  specific transfer from nats to ints and back. *}
     8.9  
    8.10  theory Nat_Transfer
    8.11 -imports Main Parity
    8.12 +imports Nat_Numeral
    8.13 +uses ("Tools/transfer.ML")
    8.14  begin
    8.15  
    8.16 +subsection {* Generic transfer machinery *}
    8.17 +
    8.18 +definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
    8.19 +  where "TransferMorphism a B \<longleftrightarrow> True"
    8.20 +
    8.21 +use "Tools/transfer.ML"
    8.22 +
    8.23 +setup Transfer.setup
    8.24 +
    8.25 +
    8.26  subsection {* Set up transfer from nat to int *}
    8.27  
    8.28 -(* set up transfer direction *)
    8.29 +text {* set up transfer direction *}
    8.30  
    8.31  lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
    8.32    by (simp add: TransferMorphism_def)
    8.33 @@ -20,7 +31,7 @@
    8.34    labels: natint
    8.35  ]
    8.36  
    8.37 -(* basic functions and relations *)
    8.38 +text {* basic functions and relations *}
    8.39  
    8.40  lemma transfer_nat_int_numerals:
    8.41      "(0::nat) = nat 0"
    8.42 @@ -43,31 +54,20 @@
    8.43      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
    8.44      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
    8.45      "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
    8.46 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
    8.47 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
    8.48    by (auto simp add: eq_nat_nat_iff nat_mult_distrib
    8.49 -      nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
    8.50 +      nat_power_eq tsub_def)
    8.51  
    8.52  lemma transfer_nat_int_function_closures:
    8.53      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
    8.54      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
    8.55      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
    8.56      "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
    8.57 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
    8.58 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
    8.59      "(0::int) >= 0"
    8.60      "(1::int) >= 0"
    8.61      "(2::int) >= 0"
    8.62      "(3::int) >= 0"
    8.63      "int z >= 0"
    8.64    apply (auto simp add: zero_le_mult_iff tsub_def)
    8.65 -  apply (case_tac "y = 0")
    8.66 -  apply auto
    8.67 -  apply (subst pos_imp_zdiv_nonneg_iff, auto)
    8.68 -  apply (case_tac "y = 0")
    8.69 -  apply force
    8.70 -  apply (rule pos_mod_sign)
    8.71 -  apply arith
    8.72  done
    8.73  
    8.74  lemma transfer_nat_int_relations:
    8.75 @@ -89,7 +89,21 @@
    8.76  ]
    8.77  
    8.78  
    8.79 -(* first-order quantifiers *)
    8.80 +text {* first-order quantifiers *}
    8.81 +
    8.82 +lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
    8.83 +  by (simp split add: split_nat)
    8.84 +
    8.85 +lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
    8.86 +proof
    8.87 +  assume "\<exists>x. P x"
    8.88 +  then obtain x where "P x" ..
    8.89 +  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
    8.90 +  then show "\<exists>x\<ge>0. P (nat x)" ..
    8.91 +next
    8.92 +  assume "\<exists>x\<ge>0. P (nat x)"
    8.93 +  then show "\<exists>x. P x" by auto
    8.94 +qed
    8.95  
    8.96  lemma transfer_nat_int_quantifiers:
    8.97      "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
    8.98 @@ -110,7 +124,7 @@
    8.99    cong: all_cong ex_cong]
   8.100  
   8.101  
   8.102 -(* if *)
   8.103 +text {* if *}
   8.104  
   8.105  lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
   8.106      nat (if P then x else y)"
   8.107 @@ -119,7 +133,7 @@
   8.108  declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
   8.109  
   8.110  
   8.111 -(* operations with sets *)
   8.112 +text {* operations with sets *}
   8.113  
   8.114  definition
   8.115    nat_set :: "int set \<Rightarrow> bool"
   8.116 @@ -132,8 +146,6 @@
   8.117      "A Un B = nat ` (int ` A Un int ` B)"
   8.118      "A Int B = nat ` (int ` A Int int ` B)"
   8.119      "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
   8.120 -    "{..n} = nat ` {0..int n}"
   8.121 -    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
   8.122    apply (rule card_image [symmetric])
   8.123    apply (auto simp add: inj_on_def image_def)
   8.124    apply (rule_tac x = "int x" in bexI)
   8.125 @@ -144,17 +156,12 @@
   8.126    apply auto
   8.127    apply (rule_tac x = "int x" in exI)
   8.128    apply auto
   8.129 -  apply (rule_tac x = "int x" in bexI)
   8.130 -  apply auto
   8.131 -  apply (rule_tac x = "int x" in bexI)
   8.132 -  apply auto
   8.133  done
   8.134  
   8.135  lemma transfer_nat_int_set_function_closures:
   8.136      "nat_set {}"
   8.137      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   8.138      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   8.139 -    "x >= 0 \<Longrightarrow> nat_set {x..y}"
   8.140      "nat_set {x. x >= 0 & P x}"
   8.141      "nat_set (int ` C)"
   8.142      "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
   8.143 @@ -167,7 +174,6 @@
   8.144      "(A = B) = (int ` A = int ` B)"
   8.145      "(A < B) = (int ` A < int ` B)"
   8.146      "(A <= B) = (int ` A <= int ` B)"
   8.147 -
   8.148    apply (rule iffI)
   8.149    apply (erule finite_imageI)
   8.150    apply (erule finite_imageD)
   8.151 @@ -194,7 +200,7 @@
   8.152  ]
   8.153  
   8.154  
   8.155 -(* setsum and setprod *)
   8.156 +text {* setsum and setprod *}
   8.157  
   8.158  (* this handles the case where the *domain* of f is nat *)
   8.159  lemma transfer_nat_int_sum_prod:
   8.160 @@ -262,52 +268,10 @@
   8.161      transfer_nat_int_sum_prod_closure
   8.162    cong: transfer_nat_int_sum_prod_cong]
   8.163  
   8.164 -(* lists *)
   8.165 -
   8.166 -definition
   8.167 -  embed_list :: "nat list \<Rightarrow> int list"
   8.168 -where
   8.169 -  "embed_list l = map int l";
   8.170 -
   8.171 -definition
   8.172 -  nat_list :: "int list \<Rightarrow> bool"
   8.173 -where
   8.174 -  "nat_list l = nat_set (set l)";
   8.175 -
   8.176 -definition
   8.177 -  return_list :: "int list \<Rightarrow> nat list"
   8.178 -where
   8.179 -  "return_list l = map nat l";
   8.180 -
   8.181 -thm nat_0_le;
   8.182 -
   8.183 -lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
   8.184 -    embed_list (return_list l) = l";
   8.185 -  unfolding embed_list_def return_list_def nat_list_def nat_set_def
   8.186 -  apply (induct l);
   8.187 -  apply auto;
   8.188 -done;
   8.189 -
   8.190 -lemma transfer_nat_int_list_functions:
   8.191 -  "l @ m = return_list (embed_list l @ embed_list m)"
   8.192 -  "[] = return_list []";
   8.193 -  unfolding return_list_def embed_list_def;
   8.194 -  apply auto;
   8.195 -  apply (induct l, auto);
   8.196 -  apply (induct m, auto);
   8.197 -done;
   8.198 -
   8.199 -(*
   8.200 -lemma transfer_nat_int_fold1: "fold f l x =
   8.201 -    fold (%x. f (nat x)) (embed_list l) x";
   8.202 -*)
   8.203 -
   8.204 -
   8.205 -
   8.206  
   8.207  subsection {* Set up transfer from int to nat *}
   8.208  
   8.209 -(* set up transfer direction *)
   8.210 +text {* set up transfer direction *}
   8.211  
   8.212  lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
   8.213    by (simp add: TransferMorphism_def)
   8.214 @@ -319,7 +283,11 @@
   8.215  ]
   8.216  
   8.217  
   8.218 -(* basic functions and relations *)
   8.219 +text {* basic functions and relations *}
   8.220 +
   8.221 +lemma UNIV_apply:
   8.222 +  "UNIV x = True"
   8.223 +  by (simp add: top_fun_eq top_bool_eq)
   8.224  
   8.225  definition
   8.226    is_nat :: "int \<Rightarrow> bool"
   8.227 @@ -338,17 +306,13 @@
   8.228      "(int x) * (int y) = int (x * y)"
   8.229      "tsub (int x) (int y) = int (x - y)"
   8.230      "(int x)^n = int (x^n)"
   8.231 -    "(int x) div (int y) = int (x div y)"
   8.232 -    "(int x) mod (int y) = int (x mod y)"
   8.233 -  by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
   8.234 +  by (auto simp add: int_mult tsub_def int_power)
   8.235  
   8.236  lemma transfer_int_nat_function_closures:
   8.237      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
   8.238      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
   8.239      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
   8.240      "is_nat x \<Longrightarrow> is_nat (x^n)"
   8.241 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
   8.242 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   8.243      "is_nat 0"
   8.244      "is_nat 1"
   8.245      "is_nat 2"
   8.246 @@ -361,12 +325,7 @@
   8.247      "(int x < int y) = (x < y)"
   8.248      "(int x <= int y) = (x <= y)"
   8.249      "(int x dvd int y) = (x dvd y)"
   8.250 -    "(even (int x)) = (even x)"
   8.251 -  by (auto simp add: zdvd_int even_nat_def)
   8.252 -
   8.253 -lemma UNIV_apply:
   8.254 -  "UNIV x = True"
   8.255 -  by (simp add: top_fun_eq top_bool_eq)
   8.256 +  by (auto simp add: zdvd_int)
   8.257  
   8.258  declare TransferMorphism_int_nat[transfer add return:
   8.259    transfer_int_nat_numerals
   8.260 @@ -377,7 +336,7 @@
   8.261  ]
   8.262  
   8.263  
   8.264 -(* first-order quantifiers *)
   8.265 +text {* first-order quantifiers *}
   8.266  
   8.267  lemma transfer_int_nat_quantifiers:
   8.268      "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
   8.269 @@ -392,7 +351,7 @@
   8.270    return: transfer_int_nat_quantifiers]
   8.271  
   8.272  
   8.273 -(* if *)
   8.274 +text {* if *}
   8.275  
   8.276  lemma int_if_cong: "(if P then (int x) else (int y)) =
   8.277      int (if P then x else y)"
   8.278 @@ -402,7 +361,7 @@
   8.279  
   8.280  
   8.281  
   8.282 -(* operations with sets *)
   8.283 +text {* operations with sets *}
   8.284  
   8.285  lemma transfer_int_nat_set_functions:
   8.286      "nat_set A \<Longrightarrow> card A = card (nat ` A)"
   8.287 @@ -410,7 +369,6 @@
   8.288      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
   8.289      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
   8.290      "{x. x >= 0 & P x} = int ` {x. P(int x)}"
   8.291 -    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
   8.292         (* need all variants of these! *)
   8.293    by (simp_all only: is_nat_def transfer_nat_int_set_functions
   8.294            transfer_nat_int_set_function_closures
   8.295 @@ -421,7 +379,6 @@
   8.296      "nat_set {}"
   8.297      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   8.298      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   8.299 -    "is_nat x \<Longrightarrow> nat_set {x..y}"
   8.300      "nat_set {x. x >= 0 & P x}"
   8.301      "nat_set (int ` C)"
   8.302      "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
   8.303 @@ -454,7 +411,7 @@
   8.304  ]
   8.305  
   8.306  
   8.307 -(* setsum and setprod *)
   8.308 +text {* setsum and setprod *}
   8.309  
   8.310  (* this handles the case where the *domain* of f is int *)
   8.311  lemma transfer_int_nat_sum_prod:
     9.1 --- a/src/HOL/Parity.thy	Thu Oct 29 08:14:39 2009 +0100
     9.2 +++ b/src/HOL/Parity.thy	Thu Oct 29 11:41:36 2009 +0100
     9.3 @@ -28,6 +28,13 @@
     9.4  
     9.5  end
     9.6  
     9.7 +lemma transfer_int_nat_relations:
     9.8 +  "even (int x) \<longleftrightarrow> even x"
     9.9 +  by (simp add: even_nat_def)
    9.10 +
    9.11 +declare TransferMorphism_int_nat[transfer add return:
    9.12 +  transfer_int_nat_relations
    9.13 +]
    9.14  
    9.15  lemma even_zero_int[simp]: "even (0::int)" by presburger
    9.16  
    9.17 @@ -310,6 +317,8 @@
    9.18  
    9.19  subsection {* General Lemmas About Division *}
    9.20  
    9.21 +(*FIXME move to Divides.thy*)
    9.22 +
    9.23  lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
    9.24  apply (induct "m")
    9.25  apply (simp_all add: mod_Suc)
    10.1 --- a/src/HOL/Presburger.thy	Thu Oct 29 08:14:39 2009 +0100
    10.2 +++ b/src/HOL/Presburger.thy	Thu Oct 29 11:41:36 2009 +0100
    10.3 @@ -385,20 +385,6 @@
    10.4  
    10.5  text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
    10.6  
    10.7 -lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
    10.8 -  by (simp split add: split_nat)
    10.9 -
   10.10 -lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
   10.11 -proof
   10.12 -  assume "\<exists>x. P x"
   10.13 -  then obtain x where "P x" ..
   10.14 -  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
   10.15 -  then show "\<exists>x\<ge>0. P (nat x)" ..
   10.16 -next
   10.17 -  assume "\<exists>x\<ge>0. P (nat x)"
   10.18 -  then show "\<exists>x. P x" by auto
   10.19 -qed
   10.20 -
   10.21  lemma zdiff_int_split: "P (int (x - y)) =
   10.22    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
   10.23    by (case_tac "y \<le> x", simp_all add: zdiff_int)
    11.1 --- a/src/HOL/SetInterval.thy	Thu Oct 29 08:14:39 2009 +0100
    11.2 +++ b/src/HOL/SetInterval.thy	Thu Oct 29 11:41:36 2009 +0100
    11.3 @@ -9,7 +9,7 @@
    11.4  header {* Set intervals *}
    11.5  
    11.6  theory SetInterval
    11.7 -imports Int
    11.8 +imports Int Nat_Transfer
    11.9  begin
   11.10  
   11.11  context ord
   11.12 @@ -1150,4 +1150,41 @@
   11.13    "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
   11.14    "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
   11.15  
   11.16 +subsection {* Transfer setup *}
   11.17 +
   11.18 +lemma transfer_nat_int_set_functions:
   11.19 +    "{..n} = nat ` {0..int n}"
   11.20 +    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
   11.21 +  apply (auto simp add: image_def)
   11.22 +  apply (rule_tac x = "int x" in bexI)
   11.23 +  apply auto
   11.24 +  apply (rule_tac x = "int x" in bexI)
   11.25 +  apply auto
   11.26 +  done
   11.27 +
   11.28 +lemma transfer_nat_int_set_function_closures:
   11.29 +    "x >= 0 \<Longrightarrow> nat_set {x..y}"
   11.30 +  by (simp add: nat_set_def)
   11.31 +
   11.32 +declare TransferMorphism_nat_int[transfer add
   11.33 +  return: transfer_nat_int_set_functions
   11.34 +    transfer_nat_int_set_function_closures
   11.35 +]
   11.36 +
   11.37 +lemma transfer_int_nat_set_functions:
   11.38 +    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
   11.39 +  by (simp only: is_nat_def transfer_nat_int_set_functions
   11.40 +    transfer_nat_int_set_function_closures
   11.41 +    transfer_nat_int_set_return_embed nat_0_le
   11.42 +    cong: transfer_nat_int_set_cong)
   11.43 +
   11.44 +lemma transfer_int_nat_set_function_closures:
   11.45 +    "is_nat x \<Longrightarrow> nat_set {x..y}"
   11.46 +  by (simp only: transfer_nat_int_set_function_closures is_nat_def)
   11.47 +
   11.48 +declare TransferMorphism_int_nat[transfer add
   11.49 +  return: transfer_int_nat_set_functions
   11.50 +    transfer_int_nat_set_function_closures
   11.51 +]
   11.52 +
   11.53  end