tuned imports
authorhaftmann
Mon Oct 09 19:10:47 2017 +0200 (19 months ago)
changeset 668364eb431c3f974
parent 66835 ecc99a5a1ab8
child 66837 6ba663ff2b1c
tuned imports
src/HOL/Code_Numeral.thy
src/HOL/GCD.thy
src/HOL/HOL.thy
src/HOL/Int.thy
src/HOL/List.thy
src/HOL/Nat_Transfer.thy
src/HOL/Semiring_Normalization.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Tue Oct 10 22:18:58 2017 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Oct 09 19:10:47 2017 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  section \<open>Numeric types for code generation onto target language numerals only\<close>
     1.5  
     1.6  theory Code_Numeral
     1.7 -imports Nat_Transfer Divides Lifting
     1.8 +imports Divides Lifting
     1.9  begin
    1.10  
    1.11  subsection \<open>Type of target language integers\<close>
     2.1 --- a/src/HOL/GCD.thy	Tue Oct 10 22:18:58 2017 +0100
     2.2 +++ b/src/HOL/GCD.thy	Mon Oct 09 19:10:47 2017 +0200
     2.3 @@ -1708,36 +1708,6 @@
     2.4  
     2.5  end
     2.6  
     2.7 -text \<open>Transfer setup\<close>
     2.8 -
     2.9 -lemma transfer_nat_int_gcd:
    2.10 -  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
    2.11 -  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
    2.12 -  for x y :: int
    2.13 -  unfolding gcd_int_def lcm_int_def by auto
    2.14 -
    2.15 -lemma transfer_nat_int_gcd_closures:
    2.16 -  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
    2.17 -  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
    2.18 -  for x y :: int
    2.19 -  by (auto simp add: gcd_int_def lcm_int_def)
    2.20 -
    2.21 -declare transfer_morphism_nat_int
    2.22 -  [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
    2.23 -
    2.24 -lemma transfer_int_nat_gcd:
    2.25 -  "gcd (int x) (int y) = int (gcd x y)"
    2.26 -  "lcm (int x) (int y) = int (lcm x y)"
    2.27 -  by (auto simp: gcd_int_def lcm_int_def)
    2.28 -
    2.29 -lemma transfer_int_nat_gcd_closures:
    2.30 -  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
    2.31 -  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
    2.32 -  by (auto simp: gcd_int_def lcm_int_def)
    2.33 -
    2.34 -declare transfer_morphism_int_nat
    2.35 -  [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
    2.36 -
    2.37  lemma gcd_nat_induct:
    2.38    fixes m n :: nat
    2.39    assumes "\<And>m. P m 0"
     3.1 --- a/src/HOL/HOL.thy	Tue Oct 10 22:18:58 2017 +0100
     3.2 +++ b/src/HOL/HOL.thy	Mon Oct 09 19:10:47 2017 +0200
     3.3 @@ -1574,6 +1574,14 @@
     3.4  
     3.5  subsection \<open>Other simple lemmas and lemma duplicates\<close>
     3.6  
     3.7 +lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
     3.8 +    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
     3.9 +  by auto
    3.10 +
    3.11 +lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
    3.12 +    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
    3.13 +  by auto
    3.14 +
    3.15  lemma ex1_eq [iff]: "\<exists>!x. x = t" "\<exists>!x. t = x"
    3.16    by blast+
    3.17  
     4.1 --- a/src/HOL/Int.thy	Tue Oct 10 22:18:58 2017 +0100
     4.2 +++ b/src/HOL/Int.thy	Mon Oct 09 19:10:47 2017 +0200
     4.3 @@ -556,6 +556,43 @@
     4.4    "nat (of_bool P) = of_bool P"
     4.5    by auto
     4.6  
     4.7 +lemma split_nat [arith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
     4.8 +  (is "?P = (?L \<and> ?R)")
     4.9 +  for i :: int
    4.10 +proof (cases "i < 0")
    4.11 +  case True
    4.12 +  then show ?thesis
    4.13 +    by auto
    4.14 +next
    4.15 +  case False
    4.16 +  have "?P = ?L"
    4.17 +  proof
    4.18 +    assume ?P
    4.19 +    then show ?L using False by auto
    4.20 +  next
    4.21 +    assume ?L
    4.22 +    moreover from False have "int (nat i) = i"
    4.23 +      by (simp add: not_less)
    4.24 +    ultimately show ?P
    4.25 +      by simp
    4.26 +  qed
    4.27 +  with False show ?thesis by simp
    4.28 +qed
    4.29 +
    4.30 +lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
    4.31 +  by (auto split: split_nat)
    4.32 +
    4.33 +lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
    4.34 +proof
    4.35 +  assume "\<exists>x. P x"
    4.36 +  then obtain x where "P x" ..
    4.37 +  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
    4.38 +  then show "\<exists>x\<ge>0. P (nat x)" ..
    4.39 +next
    4.40 +  assume "\<exists>x\<ge>0. P (nat x)"
    4.41 +  then show "\<exists>x. P x" by auto
    4.42 +qed
    4.43 +
    4.44  
    4.45  text \<open>For termination proofs:\<close>
    4.46  lemma measure_function_int[measure_function]: "is_measure (nat \<circ> abs)" ..
    4.47 @@ -1043,25 +1080,6 @@
    4.48  \<close>
    4.49  lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
    4.50  
    4.51 -lemma split_nat [arith_split]: "P (nat i) = ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
    4.52 -  (is "?P = (?L \<and> ?R)")
    4.53 -  for i :: int
    4.54 -proof (cases "i < 0")
    4.55 -  case True
    4.56 -  then show ?thesis by auto
    4.57 -next
    4.58 -  case False
    4.59 -  have "?P = ?L"
    4.60 -  proof
    4.61 -    assume ?P
    4.62 -    then show ?L using False by auto
    4.63 -  next
    4.64 -    assume ?L
    4.65 -    then show ?P using False by simp
    4.66 -  qed
    4.67 -  with False show ?thesis by simp
    4.68 -qed
    4.69 -
    4.70  lemma nat_abs_int_diff: "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
    4.71    by auto
    4.72  
     5.1 --- a/src/HOL/List.thy	Tue Oct 10 22:18:58 2017 +0100
     5.2 +++ b/src/HOL/List.thy	Mon Oct 09 19:10:47 2017 +0200
     5.3 @@ -6600,39 +6600,6 @@
     5.4    by (induction xs) simp_all
     5.5  
     5.6  
     5.7 -subsection \<open>Transfer\<close>
     5.8 -
     5.9 -definition embed_list :: "nat list \<Rightarrow> int list" where
    5.10 -"embed_list l = map int l"
    5.11 -
    5.12 -definition nat_list :: "int list \<Rightarrow> bool" where
    5.13 -"nat_list l = nat_set (set l)"
    5.14 -
    5.15 -definition return_list :: "int list \<Rightarrow> nat list" where
    5.16 -"return_list l = map nat l"
    5.17 -
    5.18 -lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
    5.19 -    embed_list (return_list l) = l"
    5.20 -  unfolding embed_list_def return_list_def nat_list_def nat_set_def
    5.21 -  apply (induct l)
    5.22 -  apply auto
    5.23 -done
    5.24 -
    5.25 -lemma transfer_nat_int_list_functions:
    5.26 -  "l @ m = return_list (embed_list l @ embed_list m)"
    5.27 -  "[] = return_list []"
    5.28 -  unfolding return_list_def embed_list_def
    5.29 -  apply auto
    5.30 -  apply (induct l, auto)
    5.31 -  apply (induct m, auto)
    5.32 -done
    5.33 -
    5.34 -(*
    5.35 -lemma transfer_nat_int_fold1: "fold f l x =
    5.36 -    fold (%x. f (nat x)) (embed_list l) x";
    5.37 -*)
    5.38 -
    5.39 -
    5.40  subsection \<open>Code generation\<close>
    5.41  
    5.42  text\<open>Optional tail recursive version of @{const map}. Can avoid
     6.1 --- a/src/HOL/Nat_Transfer.thy	Tue Oct 10 22:18:58 2017 +0100
     6.2 +++ b/src/HOL/Nat_Transfer.thy	Mon Oct 09 19:10:47 2017 +0200
     6.3 @@ -3,7 +3,7 @@
     6.4  section \<open>Generic transfer machinery;  specific transfer from nats to ints and back.\<close>
     6.5  
     6.6  theory Nat_Transfer
     6.7 -imports Int Divides
     6.8 +imports List GCD
     6.9  begin
    6.10  
    6.11  subsection \<open>Generic transfer machinery\<close>
    6.12 @@ -90,34 +90,11 @@
    6.13  
    6.14  text \<open>first-order quantifiers\<close>
    6.15  
    6.16 -lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
    6.17 -  by (simp split: split_nat)
    6.18 -
    6.19 -lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
    6.20 -proof
    6.21 -  assume "\<exists>x. P x"
    6.22 -  then obtain x where "P x" ..
    6.23 -  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
    6.24 -  then show "\<exists>x\<ge>0. P (nat x)" ..
    6.25 -next
    6.26 -  assume "\<exists>x\<ge>0. P (nat x)"
    6.27 -  then show "\<exists>x. P x" by auto
    6.28 -qed
    6.29 -
    6.30  lemma transfer_nat_int_quantifiers [no_atp, transfer key: transfer_morphism_nat_int]:
    6.31      "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
    6.32      "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
    6.33    by (rule all_nat, rule ex_nat)
    6.34  
    6.35 -(* should we restrict these? *)
    6.36 -lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
    6.37 -    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
    6.38 -  by auto
    6.39 -
    6.40 -lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
    6.41 -    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
    6.42 -  by auto
    6.43 -
    6.44  declare transfer_morphism_nat_int [transfer add
    6.45    cong: all_cong ex_cong]
    6.46  
    6.47 @@ -142,17 +119,10 @@
    6.48      "A Un B = nat ` (int ` A Un int ` B)"
    6.49      "A Int B = nat ` (int ` A Int int ` B)"
    6.50      "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
    6.51 -  apply (rule card_image [symmetric])
    6.52 -  apply (auto simp add: inj_on_def image_def)
    6.53 -  apply (rule_tac x = "int x" in bexI)
    6.54 -  apply auto
    6.55 -  apply (rule_tac x = "int x" in bexI)
    6.56 -  apply auto
    6.57 -  apply (rule_tac x = "int x" in bexI)
    6.58 -  apply auto
    6.59 -  apply (rule_tac x = "int x" in exI)
    6.60 -  apply auto
    6.61 -done
    6.62 +    "{..n} = nat ` {0..int n}"
    6.63 +    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
    6.64 +  by (rule card_image [symmetric])
    6.65 +    (auto simp add: inj_on_def image_def intro: bexI [of _ "int x" for x] exI [of _ "int x" for x])
    6.66  
    6.67  lemma transfer_nat_int_set_function_closures [no_atp]:
    6.68      "nat_set {}"
    6.69 @@ -161,6 +131,7 @@
    6.70      "nat_set {x. x >= 0 & P x}"
    6.71      "nat_set (int ` C)"
    6.72      "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
    6.73 +    "x >= 0 \<Longrightarrow> nat_set {x..y}"
    6.74    unfolding nat_set_def apply auto
    6.75  done
    6.76  
    6.77 @@ -361,6 +332,7 @@
    6.78      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
    6.79      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
    6.80      "{x. x >= 0 & P x} = int ` {x. P(int x)}"
    6.81 +    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
    6.82         (* need all variants of these! *)
    6.83    by (simp_all only: is_nat_def transfer_nat_int_set_functions
    6.84            transfer_nat_int_set_function_closures
    6.85 @@ -374,6 +346,7 @@
    6.86      "nat_set {x. x >= 0 & P x}"
    6.87      "nat_set (int ` C)"
    6.88      "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
    6.89 +    "is_nat x \<Longrightarrow> nat_set {x..y}"
    6.90    by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
    6.91  
    6.92  lemma transfer_int_nat_set_relations [no_atp]:
    6.93 @@ -430,4 +403,62 @@
    6.94  
    6.95  declare transfer_morphism_int_nat [transfer add return: even_int_iff]
    6.96  
    6.97 +lemma transfer_nat_int_gcd [no_atp]:
    6.98 +  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
    6.99 +  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
   6.100 +  for x y :: int
   6.101 +  unfolding gcd_int_def lcm_int_def by auto
   6.102 +
   6.103 +lemma transfer_nat_int_gcd_closures [no_atp]:
   6.104 +  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
   6.105 +  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
   6.106 +  for x y :: int
   6.107 +  by (auto simp add: gcd_int_def lcm_int_def)
   6.108 +
   6.109 +declare transfer_morphism_nat_int
   6.110 +  [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   6.111 +
   6.112 +lemma transfer_int_nat_gcd [no_atp]:
   6.113 +  "gcd (int x) (int y) = int (gcd x y)"
   6.114 +  "lcm (int x) (int y) = int (lcm x y)"
   6.115 +  by (auto simp: gcd_int_def lcm_int_def)
   6.116 +
   6.117 +lemma transfer_int_nat_gcd_closures [no_atp]:
   6.118 +  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   6.119 +  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   6.120 +  by (auto simp: gcd_int_def lcm_int_def)
   6.121 +
   6.122 +declare transfer_morphism_int_nat
   6.123 +  [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   6.124 +
   6.125 +definition embed_list :: "nat list \<Rightarrow> int list" where
   6.126 +"embed_list l = map int l"
   6.127 +
   6.128 +definition nat_list :: "int list \<Rightarrow> bool" where
   6.129 +"nat_list l = nat_set (set l)"
   6.130 +
   6.131 +definition return_list :: "int list \<Rightarrow> nat list" where
   6.132 +"return_list l = map nat l"
   6.133 +
   6.134 +lemma transfer_nat_int_list_return_embed [no_atp]:
   6.135 +  "nat_list l \<longrightarrow> embed_list (return_list l) = l"
   6.136 +  unfolding embed_list_def return_list_def nat_list_def nat_set_def
   6.137 +  apply (induct l)
   6.138 +  apply auto
   6.139 +done
   6.140 +
   6.141 +lemma transfer_nat_int_list_functions [no_atp]:
   6.142 +  "l @ m = return_list (embed_list l @ embed_list m)"
   6.143 +  "[] = return_list []"
   6.144 +  unfolding return_list_def embed_list_def
   6.145 +  apply auto
   6.146 +  apply (induct l, auto)
   6.147 +  apply (induct m, auto)
   6.148 +done
   6.149 +
   6.150 +(*
   6.151 +lemma transfer_nat_int_fold1: "fold f l x =
   6.152 +    fold (%x. f (nat x)) (embed_list l) x";
   6.153 +*)
   6.154 +
   6.155  end
     7.1 --- a/src/HOL/Semiring_Normalization.thy	Tue Oct 10 22:18:58 2017 +0100
     7.2 +++ b/src/HOL/Semiring_Normalization.thy	Mon Oct 09 19:10:47 2017 +0200
     7.3 @@ -5,7 +5,7 @@
     7.4  section \<open>Semiring normalization\<close>
     7.5  
     7.6  theory Semiring_Normalization
     7.7 -imports Numeral_Simprocs Nat_Transfer
     7.8 +imports Numeral_Simprocs
     7.9  begin
    7.10  
    7.11  text \<open>Prelude\<close>
     8.1 --- a/src/HOL/Set_Interval.thy	Tue Oct 10 22:18:58 2017 +0100
     8.2 +++ b/src/HOL/Set_Interval.thy	Mon Oct 09 19:10:47 2017 +0200
     8.3 @@ -14,7 +14,7 @@
     8.4  section \<open>Set intervals\<close>
     8.5  
     8.6  theory Set_Interval
     8.7 -imports Lattices_Big Divides Nat_Transfer
     8.8 +imports Divides
     8.9  begin
    8.10  
    8.11  context ord
    8.12 @@ -2231,42 +2231,4 @@
    8.13  
    8.14  (* TODO: Add support for more kinds of intervals here *)
    8.15  
    8.16 -
    8.17 -subsection \<open>Transfer setup\<close>
    8.18 -
    8.19 -lemma transfer_nat_int_set_functions:
    8.20 -    "{..n} = nat ` {0..int n}"
    8.21 -    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
    8.22 -  apply (auto simp add: image_def)
    8.23 -  apply (rule_tac x = "int x" in bexI)
    8.24 -  apply auto
    8.25 -  apply (rule_tac x = "int x" in bexI)
    8.26 -  apply auto
    8.27 -  done
    8.28 -
    8.29 -lemma transfer_nat_int_set_function_closures:
    8.30 -    "x >= 0 \<Longrightarrow> nat_set {x..y}"
    8.31 -  by (simp add: nat_set_def)
    8.32 -
    8.33 -declare transfer_morphism_nat_int[transfer add
    8.34 -  return: transfer_nat_int_set_functions
    8.35 -    transfer_nat_int_set_function_closures
    8.36 -]
    8.37 -
    8.38 -lemma transfer_int_nat_set_functions:
    8.39 -    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
    8.40 -  by (simp only: is_nat_def transfer_nat_int_set_functions
    8.41 -    transfer_nat_int_set_function_closures
    8.42 -    transfer_nat_int_set_return_embed nat_0_le
    8.43 -    cong: transfer_nat_int_set_cong)
    8.44 -
    8.45 -lemma transfer_int_nat_set_function_closures:
    8.46 -    "is_nat x \<Longrightarrow> nat_set {x..y}"
    8.47 -  by (simp only: transfer_nat_int_set_function_closures is_nat_def)
    8.48 -
    8.49 -declare transfer_morphism_int_nat[transfer add
    8.50 -  return: transfer_int_nat_set_functions
    8.51 -    transfer_int_nat_set_function_closures
    8.52 -]
    8.53 -
    8.54  end