qualify some names stemming from internal bootstrap constructions
authorhaftmann
Sat Oct 17 13:18:43 2015 +0200 (2015-10-17)
changeset 61433a4c0de1df3d8
parent 61432 1502f2410d8b
child 61465 79900ab5d50a
qualify some names stemming from internal bootstrap constructions
src/HOL/Divides.thy
src/HOL/Library/Code_Binary_Nat.thy
src/HOL/Library/Code_Target_Nat.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/ex/Parallel_Example.thy
     1.1 --- a/src/HOL/Divides.thy	Thu Oct 15 12:39:51 2015 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sat Oct 17 13:18:43 2015 +0200
     1.3 @@ -813,6 +813,9 @@
     1.4  
     1.5  subsection \<open>Division on @{typ nat}\<close>
     1.6  
     1.7 +context
     1.8 +begin
     1.9 +
    1.10  text \<open>
    1.11    We define @{const divide} and @{const mod} on @{typ nat} by means
    1.12    of a characteristic relation with two input arguments
    1.13 @@ -827,7 +830,7 @@
    1.14  
    1.15  text \<open>@{const divmod_nat_rel} is total:\<close>
    1.16  
    1.17 -lemma divmod_nat_rel_ex:
    1.18 +qualified lemma divmod_nat_rel_ex:
    1.19    obtains q r where "divmod_nat_rel m n (q, r)"
    1.20  proof (cases "n = 0")
    1.21    case True  with that show thesis
    1.22 @@ -860,7 +863,7 @@
    1.23  
    1.24  text \<open>@{const divmod_nat_rel} is injective:\<close>
    1.25  
    1.26 -lemma divmod_nat_rel_unique:
    1.27 +qualified lemma divmod_nat_rel_unique:
    1.28    assumes "divmod_nat_rel m n qr"
    1.29      and "divmod_nat_rel m n qr'"
    1.30    shows "qr = qr'"
    1.31 @@ -887,10 +890,10 @@
    1.32    means of @{const divmod_nat_rel}:
    1.33  \<close>
    1.34  
    1.35 -definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
    1.36 +qualified definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
    1.37    "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)"
    1.38  
    1.39 -lemma divmod_nat_rel_divmod_nat:
    1.40 +qualified lemma divmod_nat_rel_divmod_nat:
    1.41    "divmod_nat_rel m n (divmod_nat m n)"
    1.42  proof -
    1.43    from divmod_nat_rel_ex
    1.44 @@ -899,63 +902,65 @@
    1.45    by (auto simp add: divmod_nat_def intro: theI elim: divmod_nat_rel_unique)
    1.46  qed
    1.47  
    1.48 -lemma divmod_nat_unique:
    1.49 +qualified lemma divmod_nat_unique:
    1.50    assumes "divmod_nat_rel m n qr"
    1.51    shows "divmod_nat m n = qr"
    1.52    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
    1.53  
    1.54 +qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
    1.55 +  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
    1.56 +
    1.57 +qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
    1.58 +  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
    1.59 +
    1.60 +qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
    1.61 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
    1.62 +
    1.63 +qualified lemma divmod_nat_step:
    1.64 +  assumes "0 < n" and "n \<le> m"
    1.65 +  shows "divmod_nat m n = apfst Suc (divmod_nat (m - n) n)"
    1.66 +proof (rule divmod_nat_unique)
    1.67 +  have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
    1.68 +    by (fact divmod_nat_rel_divmod_nat)
    1.69 +  then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
    1.70 +    unfolding divmod_nat_rel_def using assms by auto
    1.71 +qed
    1.72 +
    1.73 +end
    1.74 +  
    1.75  instantiation nat :: semiring_div
    1.76  begin
    1.77  
    1.78  definition divide_nat where
    1.79 -  div_nat_def: "m div n = fst (divmod_nat m n)"
    1.80 +  div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
    1.81  
    1.82  definition mod_nat where
    1.83 -  "m mod n = snd (divmod_nat m n)"
    1.84 +  "m mod n = snd (Divides.divmod_nat m n)"
    1.85  
    1.86  lemma fst_divmod_nat [simp]:
    1.87 -  "fst (divmod_nat m n) = m div n"
    1.88 +  "fst (Divides.divmod_nat m n) = m div n"
    1.89    by (simp add: div_nat_def)
    1.90  
    1.91  lemma snd_divmod_nat [simp]:
    1.92 -  "snd (divmod_nat m n) = m mod n"
    1.93 +  "snd (Divides.divmod_nat m n) = m mod n"
    1.94    by (simp add: mod_nat_def)
    1.95  
    1.96  lemma divmod_nat_div_mod:
    1.97 -  "divmod_nat m n = (m div n, m mod n)"
    1.98 +  "Divides.divmod_nat m n = (m div n, m mod n)"
    1.99    by (simp add: prod_eq_iff)
   1.100  
   1.101  lemma div_nat_unique:
   1.102    assumes "divmod_nat_rel m n (q, r)"
   1.103    shows "m div n = q"
   1.104 -  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
   1.105 +  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   1.106  
   1.107  lemma mod_nat_unique:
   1.108    assumes "divmod_nat_rel m n (q, r)"
   1.109    shows "m mod n = r"
   1.110 -  using assms by (auto dest!: divmod_nat_unique simp add: prod_eq_iff)
   1.111 +  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
   1.112  
   1.113  lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
   1.114 -  using divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
   1.115 -
   1.116 -lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
   1.117 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
   1.118 -
   1.119 -lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
   1.120 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
   1.121 -
   1.122 -lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
   1.123 -  by (simp add: divmod_nat_unique divmod_nat_rel_def)
   1.124 -
   1.125 -lemma divmod_nat_step:
   1.126 -  assumes "0 < n" and "n \<le> m"
   1.127 -  shows "divmod_nat m n = (Suc ((m - n) div n), (m - n) mod n)"
   1.128 -proof (rule divmod_nat_unique)
   1.129 -  have "divmod_nat_rel (m - n) n ((m - n) div n, (m - n) mod n)"
   1.130 -    by (rule divmod_nat_rel)
   1.131 -  thus "divmod_nat_rel m n (Suc ((m - n) div n), (m - n) mod n)"
   1.132 -    unfolding divmod_nat_rel_def using assms by auto
   1.133 -qed
   1.134 +  using Divides.divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
   1.135  
   1.136  text \<open>The ''recursion'' equations for @{const divide} and @{const mod}\<close>
   1.137  
   1.138 @@ -963,25 +968,25 @@
   1.139    fixes m n :: nat
   1.140    assumes "m < n"
   1.141    shows "m div n = 0"
   1.142 -  using assms divmod_nat_base by (simp add: prod_eq_iff)
   1.143 +  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
   1.144  
   1.145  lemma le_div_geq:
   1.146    fixes m n :: nat
   1.147    assumes "0 < n" and "n \<le> m"
   1.148    shows "m div n = Suc ((m - n) div n)"
   1.149 -  using assms divmod_nat_step by (simp add: prod_eq_iff)
   1.150 +  using assms Divides.divmod_nat_step by (simp add: prod_eq_iff)
   1.151  
   1.152  lemma mod_less [simp]:
   1.153    fixes m n :: nat
   1.154    assumes "m < n"
   1.155    shows "m mod n = m"
   1.156 -  using assms divmod_nat_base by (simp add: prod_eq_iff)
   1.157 +  using assms Divides.divmod_nat_base by (simp add: prod_eq_iff)
   1.158  
   1.159  lemma le_mod_geq:
   1.160    fixes m n :: nat
   1.161    assumes "n \<le> m"
   1.162    shows "m mod n = (m - n) mod n"
   1.163 -  using assms divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
   1.164 +  using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
   1.165  
   1.166  instance proof
   1.167    fix m n :: nat
   1.168 @@ -1003,10 +1008,10 @@
   1.169    thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
   1.170  next
   1.171    fix n :: nat show "n div 0 = 0"
   1.172 -    by (simp add: div_nat_def divmod_nat_zero)
   1.173 +    by (simp add: div_nat_def Divides.divmod_nat_zero)
   1.174  next
   1.175    fix n :: nat show "0 div n = 0"
   1.176 -    by (simp add: div_nat_def divmod_nat_zero_left)
   1.177 +    by (simp add: div_nat_def Divides.divmod_nat_zero_left)
   1.178  qed
   1.179  
   1.180  end
   1.181 @@ -1030,8 +1035,9 @@
   1.182    
   1.183  end
   1.184  
   1.185 -lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   1.186 -  let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
   1.187 +lemma divmod_nat_if [code]:
   1.188 +  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   1.189 +    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   1.190    by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
   1.191  
   1.192  text \<open>Simproc for cancelling @{const divide} and @{const mod}\<close>
   1.193 @@ -1347,15 +1353,15 @@
   1.194    assume P: ?lhs
   1.195    then have "divmod_nat_rel m n (q, m - n * q)"
   1.196      unfolding divmod_nat_rel_def by (auto simp add: ac_simps)
   1.197 -  with divmod_nat_rel_unique divmod_nat_rel [of m n]
   1.198 -  have "(q, m - n * q) = (m div n, m mod n)" by auto
   1.199 +  then have "m div n = q"
   1.200 +    by (rule div_nat_unique)
   1.201    then show ?rhs by simp
   1.202  qed
   1.203  
   1.204  theorem split_div':
   1.205    "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
   1.206     (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
   1.207 -  apply (case_tac "0 < n")
   1.208 +  apply (cases "0 < n")
   1.209    apply (simp only: add: split_div_lemma)
   1.210    apply simp_all
   1.211    done
     2.1 --- a/src/HOL/Library/Code_Binary_Nat.thy	Thu Oct 15 12:39:51 2015 +0200
     2.2 +++ b/src/HOL/Library/Code_Binary_Nat.thy	Sat Oct 17 13:18:43 2015 +0200
     2.3 @@ -134,12 +134,12 @@
     2.4    by (simp_all add: nat_of_num_numeral)
     2.5  
     2.6  lemma [code, code del]:
     2.7 -  "divmod_nat = divmod_nat" ..
     2.8 +  "Divides.divmod_nat = Divides.divmod_nat" ..
     2.9    
    2.10  lemma divmod_nat_code [code]:
    2.11 -  "divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
    2.12 -  "divmod_nat m 0 = (0, m)"
    2.13 -  "divmod_nat 0 n = (0, 0)"
    2.14 +  "Divides.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
    2.15 +  "Divides.divmod_nat m 0 = (0, m)"
    2.16 +  "Divides.divmod_nat 0 n = (0, 0)"
    2.17    by (simp_all add: prod_eq_iff nat_of_num_numeral)
    2.18  
    2.19  end
     3.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Thu Oct 15 12:39:51 2015 +0200
     3.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Sat Oct 17 13:18:43 2015 +0200
     3.3 @@ -111,7 +111,7 @@
     3.4  lemma (in semiring_1) of_nat_code_if:
     3.5    "of_nat n = (if n = 0 then 0
     3.6       else let
     3.7 -       (m, q) = divmod_nat n 2;
     3.8 +       (m, q) = Divides.divmod_nat n 2;
     3.9         m' = 2 * of_nat m
    3.10       in if q = 0 then m' else m' + 1)"
    3.11  proof -
     4.1 --- a/src/HOL/Library/RBT_Impl.thy	Thu Oct 15 12:39:51 2015 +0200
     4.2 +++ b/src/HOL/Library/RBT_Impl.thy	Sat Oct 17 13:18:43 2015 +0200
     4.3 @@ -1166,7 +1166,7 @@
     4.4      else if n = 1 then
     4.5        case kvs of (k, v) # kvs' \<Rightarrow> 
     4.6          (Branch R Empty k v Empty, kvs')
     4.7 -    else let (n', r) = divmod_nat n 2 in
     4.8 +    else let (n', r) = Divides.divmod_nat n 2 in
     4.9        if r = 0 then
    4.10          case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
    4.11            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
    4.12 @@ -1177,7 +1177,7 @@
    4.13  lemma rbtreeify_g_code [code]:
    4.14    "rbtreeify_g n kvs =
    4.15     (if n = 0 \<or> n = 1 then (Empty, kvs)
    4.16 -    else let (n', r) = divmod_nat n 2 in
    4.17 +    else let (n', r) = Divides.divmod_nat n 2 in
    4.18        if r = 0 then
    4.19          case rbtreeify_g n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
    4.20            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
     5.1 --- a/src/HOL/ex/Parallel_Example.thy	Thu Oct 15 12:39:51 2015 +0200
     5.2 +++ b/src/HOL/ex/Parallel_Example.thy	Sat Oct 17 13:18:43 2015 +0200
     5.3 @@ -61,7 +61,7 @@
     5.4  function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
     5.5    "factorise_from k n = (if 1 < k \<and> k \<le> n
     5.6      then
     5.7 -      let (q, r) = divmod_nat n k 
     5.8 +      let (q, r) = Divides.divmod_nat n k 
     5.9        in if r = 0 then k # factorise_from k q
    5.10          else factorise_from (Suc k) n
    5.11      else [])" 
    5.12 @@ -105,4 +105,3 @@
    5.13  value "computation_parallel ()"
    5.14  
    5.15  end
    5.16 -