src/HOL/Rat.thy
changeset 47108 2a1953f0d20d
parent 46758 4106258260b3
child 47906 09a896d295bd
     1.1 --- a/src/HOL/Rat.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Rat.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -230,35 +230,23 @@
     1.4  lemma Fract_of_int_eq: "Fract k 1 = of_int k"
     1.5    by (rule of_int_rat [symmetric])
     1.6  
     1.7 -instantiation rat :: number_ring
     1.8 -begin
     1.9 -
    1.10 -definition
    1.11 -  rat_number_of_def: "number_of w = Fract w 1"
    1.12 -
    1.13 -instance proof
    1.14 -qed (simp add: rat_number_of_def of_int_rat)
    1.15 -
    1.16 -end
    1.17 -
    1.18  lemma rat_number_collapse:
    1.19    "Fract 0 k = 0"
    1.20    "Fract 1 1 = 1"
    1.21 -  "Fract (number_of k) 1 = number_of k"
    1.22 +  "Fract (numeral w) 1 = numeral w"
    1.23 +  "Fract (neg_numeral w) 1 = neg_numeral w"
    1.24    "Fract k 0 = 0"
    1.25 -  by (cases "k = 0")
    1.26 -    (simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def)
    1.27 +  using Fract_of_int_eq [of "numeral w"]
    1.28 +  using Fract_of_int_eq [of "neg_numeral w"]
    1.29 +  by (simp_all add: Zero_rat_def One_rat_def eq_rat)
    1.30  
    1.31 -lemma rat_number_expand [code_unfold]:
    1.32 +lemma rat_number_expand:
    1.33    "0 = Fract 0 1"
    1.34    "1 = Fract 1 1"
    1.35 -  "number_of k = Fract (number_of k) 1"
    1.36 +  "numeral k = Fract (numeral k) 1"
    1.37 +  "neg_numeral k = Fract (neg_numeral k) 1"
    1.38    by (simp_all add: rat_number_collapse)
    1.39  
    1.40 -lemma iszero_rat [simp]:
    1.41 -  "iszero (number_of k :: rat) \<longleftrightarrow> iszero (number_of k :: int)"
    1.42 -  by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat)
    1.43 -
    1.44  lemma Rat_cases_nonzero [case_names Fract 0]:
    1.45    assumes Fract: "\<And>a b. q = Fract a b \<Longrightarrow> b > 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> C"
    1.46    assumes 0: "q = 0 \<Longrightarrow> C"
    1.47 @@ -386,7 +374,8 @@
    1.48  lemma quotient_of_number [simp]:
    1.49    "quotient_of 0 = (0, 1)"
    1.50    "quotient_of 1 = (1, 1)"
    1.51 -  "quotient_of (number_of k) = (number_of k, 1)"
    1.52 +  "quotient_of (numeral k) = (numeral k, 1)"
    1.53 +  "quotient_of (neg_numeral k) = (neg_numeral k, 1)"
    1.54    by (simp_all add: rat_number_expand quotient_of_Fract)
    1.55  
    1.56  lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \<Longrightarrow> Fract p q = Fract a b"
    1.57 @@ -453,19 +442,12 @@
    1.58  
    1.59  subsubsection {* Various *}
    1.60  
    1.61 -lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
    1.62 -  by (simp add: rat_number_expand)
    1.63 -
    1.64  lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
    1.65    by (simp add: Fract_of_int_eq [symmetric])
    1.66  
    1.67 -lemma Fract_number_of_quotient:
    1.68 -  "Fract (number_of k) (number_of l) = number_of k / number_of l"
    1.69 -  unfolding Fract_of_int_quotient number_of_is_id number_of_eq ..
    1.70 +lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
    1.71 +  by (simp add: rat_number_expand)
    1.72  
    1.73 -lemma Fract_1_number_of:
    1.74 -  "Fract 1 (number_of k) = 1 / number_of k"
    1.75 -  unfolding Fract_of_int_quotient number_of_eq by simp
    1.76  
    1.77  subsubsection {* The ordered field of rational numbers *}
    1.78  
    1.79 @@ -771,7 +753,8 @@
    1.80      (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
    1.81    #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
    1.82        @{thm True_implies_equals},
    1.83 -      read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
    1.84 +      read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm right_distrib},
    1.85 +      read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm right_distrib},
    1.86        @{thm divide_1}, @{thm divide_zero_left},
    1.87        @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
    1.88        @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
    1.89 @@ -895,9 +878,13 @@
    1.90  lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z"
    1.91  by (cases z rule: int_diff_cases) (simp add: of_rat_diff)
    1.92  
    1.93 -lemma of_rat_number_of_eq [simp]:
    1.94 -  "of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})"
    1.95 -by (simp add: number_of_eq)
    1.96 +lemma of_rat_numeral_eq [simp]:
    1.97 +  "of_rat (numeral w) = numeral w"
    1.98 +using of_rat_of_int_eq [of "numeral w"] by simp
    1.99 +
   1.100 +lemma of_rat_neg_numeral_eq [simp]:
   1.101 +  "of_rat (neg_numeral w) = neg_numeral w"
   1.102 +using of_rat_of_int_eq [of "neg_numeral w"] by simp
   1.103  
   1.104  lemmas zero_rat = Zero_rat_def
   1.105  lemmas one_rat = One_rat_def
   1.106 @@ -935,9 +922,11 @@
   1.107  lemma Rats_of_nat [simp]: "of_nat n \<in> Rats"
   1.108  by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat)
   1.109  
   1.110 -lemma Rats_number_of [simp]:
   1.111 -  "(number_of w::'a::{number_ring,field_char_0}) \<in> Rats"
   1.112 -by (subst of_rat_number_of_eq [symmetric], rule Rats_of_rat)
   1.113 +lemma Rats_number_of [simp]: "numeral w \<in> Rats"
   1.114 +by (subst of_rat_numeral_eq [symmetric], rule Rats_of_rat)
   1.115 +
   1.116 +lemma Rats_neg_number_of [simp]: "neg_numeral w \<in> Rats"
   1.117 +by (subst of_rat_neg_numeral_eq [symmetric], rule Rats_of_rat)
   1.118  
   1.119  lemma Rats_0 [simp]: "0 \<in> Rats"
   1.120  apply (unfold Rats_def)
   1.121 @@ -1032,6 +1021,8 @@
   1.122  
   1.123  subsection {* Implementation of rational numbers as pairs of integers *}
   1.124  
   1.125 +text {* Formal constructor *}
   1.126 +
   1.127  definition Frct :: "int \<times> int \<Rightarrow> rat" where
   1.128    [simp]: "Frct p = Fract (fst p) (snd p)"
   1.129  
   1.130 @@ -1039,17 +1030,45 @@
   1.131    "Frct (quotient_of q) = q"
   1.132    by (cases q) (auto intro: quotient_of_eq)
   1.133  
   1.134 -lemma Frct_code_post [code_post]:
   1.135 -  "Frct (0, k) = 0"
   1.136 -  "Frct (k, 0) = 0"
   1.137 -  "Frct (1, 1) = 1"
   1.138 -  "Frct (number_of k, 1) = number_of k"
   1.139 -  "Frct (1, number_of k) = 1 / number_of k"
   1.140 -  "Frct (number_of k, number_of l) = number_of k / number_of l"
   1.141 -  by (simp_all add: rat_number_collapse Fract_number_of_quotient Fract_1_number_of)
   1.142 +
   1.143 +text {* Numerals *}
   1.144  
   1.145  declare quotient_of_Fract [code abstract]
   1.146  
   1.147 +definition of_int :: "int \<Rightarrow> rat"
   1.148 +where
   1.149 +  [code_abbrev]: "of_int = Int.of_int"
   1.150 +hide_const (open) of_int
   1.151 +
   1.152 +lemma quotient_of_int [code abstract]:
   1.153 +  "quotient_of (Rat.of_int a) = (a, 1)"
   1.154 +  by (simp add: of_int_def of_int_rat quotient_of_Fract)
   1.155 +
   1.156 +lemma [code_unfold]:
   1.157 +  "numeral k = Rat.of_int (numeral k)"
   1.158 +  by (simp add: Rat.of_int_def)
   1.159 +
   1.160 +lemma [code_unfold]:
   1.161 +  "neg_numeral k = Rat.of_int (neg_numeral k)"
   1.162 +  by (simp add: Rat.of_int_def)
   1.163 +
   1.164 +lemma Frct_code_post [code_post]:
   1.165 +  "Frct (0, a) = 0"
   1.166 +  "Frct (a, 0) = 0"
   1.167 +  "Frct (1, 1) = 1"
   1.168 +  "Frct (numeral k, 1) = numeral k"
   1.169 +  "Frct (neg_numeral k, 1) = neg_numeral k"
   1.170 +  "Frct (1, numeral k) = 1 / numeral k"
   1.171 +  "Frct (1, neg_numeral k) = 1 / neg_numeral k"
   1.172 +  "Frct (numeral k, numeral l) = numeral k / numeral l"
   1.173 +  "Frct (numeral k, neg_numeral l) = numeral k / neg_numeral l"
   1.174 +  "Frct (neg_numeral k, numeral l) = neg_numeral k / numeral l"
   1.175 +  "Frct (neg_numeral k, neg_numeral l) = neg_numeral k / neg_numeral l"
   1.176 +  by (simp_all add: Fract_of_int_quotient)
   1.177 +
   1.178 +
   1.179 +text {* Operations *}
   1.180 +
   1.181  lemma rat_zero_code [code abstract]:
   1.182    "quotient_of 0 = (0, 1)"
   1.183    by (simp add: Zero_rat_def quotient_of_Fract normalize_def)
   1.184 @@ -1132,6 +1151,9 @@
   1.185    "of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)"
   1.186    by (cases p) (simp add: quotient_of_Fract of_rat_rat)
   1.187  
   1.188 +
   1.189 +text {* Quickcheck *}
   1.190 +
   1.191  definition (in term_syntax)
   1.192    valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   1.193    [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\<cdot>} k {\<cdot>} l"
   1.194 @@ -1212,7 +1234,6 @@
   1.195      (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
   1.196      (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
   1.197      (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
   1.198 -    (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
   1.199      (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
   1.200      (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}),
   1.201      (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
   1.202 @@ -1220,7 +1241,7 @@
   1.203  *}
   1.204  
   1.205  lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat
   1.206 -  number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_rat
   1.207 +  one_rat_inst.one_rat ord_rat_inst.less_rat
   1.208    ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
   1.209    uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
   1.210