src/HOL/Rat.thy
 changeset 60758 d8d85a8172b5 parent 60688 01488b559910 child 61070 b72a990adfe2
```     1.1 --- a/src/HOL/Rat.thy	Sat Jul 18 21:44:18 2015 +0200
1.2 +++ b/src/HOL/Rat.thy	Sat Jul 18 22:58:50 2015 +0200
1.3 @@ -2,15 +2,15 @@
1.4      Author: Markus Wenzel, TU Muenchen
1.5  *)
1.6
1.7 -section {* Rational numbers *}
1.8 +section \<open>Rational numbers\<close>
1.9
1.10  theory Rat
1.11  imports GCD Archimedean_Field
1.12  begin
1.13
1.14 -subsection {* Rational numbers as quotient *}
1.15 +subsection \<open>Rational numbers as quotient\<close>
1.16
1.17 -subsubsection {* Construction of the type of rational numbers *}
1.18 +subsubsection \<open>Construction of the type of rational numbers\<close>
1.19
1.20  definition
1.21    ratrel :: "(int \<times> int) \<Rightarrow> (int \<times> int) \<Rightarrow> bool" where
1.22 @@ -52,7 +52,7 @@
1.23  lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp pcr_rat = (\<lambda>x. snd x \<noteq> 0)"
1.25
1.26 -subsubsection {* Representation and basic operations *}
1.27 +subsubsection \<open>Representation and basic operations\<close>
1.28
1.29  lift_definition Fract :: "int \<Rightarrow> int \<Rightarrow> rat"
1.30    is "\<lambda>a b. if b = 0 then (0, 1) else (a, b)"
1.31 @@ -72,12 +72,12 @@
1.32      by transfer simp
1.33    let ?a = "a div gcd a b"
1.34    let ?b = "b div gcd a b"
1.35 -  from `b \<noteq> 0` have "?b * gcd a b = b"
1.36 +  from \<open>b \<noteq> 0\<close> have "?b * gcd a b = b"
1.37      by simp
1.38 -  with `b \<noteq> 0` have "?b \<noteq> 0" by fastforce
1.39 -  from `q = Fract a b` `b \<noteq> 0` `?b \<noteq> 0` have q: "q = Fract ?a ?b"
1.40 +  with \<open>b \<noteq> 0\<close> have "?b \<noteq> 0" by fastforce
1.41 +  from \<open>q = Fract a b\<close> \<open>b \<noteq> 0\<close> \<open>?b \<noteq> 0\<close> have q: "q = Fract ?a ?b"
1.42      by (simp add: eq_rat dvd_div_mult mult.commute [of a])
1.43 -  from `b \<noteq> 0` have coprime: "coprime ?a ?b"
1.44 +  from \<open>b \<noteq> 0\<close> have coprime: "coprime ?a ?b"
1.45      by (auto intro: div_gcd_coprime_int)
1.46    show C proof (cases "b > 0")
1.47      case True
1.48 @@ -90,7 +90,7 @@
1.49      case False
1.50      note assms
1.51      moreover have "q = Fract (- ?a) (- ?b)" unfolding q by transfer simp
1.52 -    moreover from False `b \<noteq> 0` have "- ?b > 0" by (simp add: pos_imp_zdiv_neg_iff)
1.53 +    moreover from False \<open>b \<noteq> 0\<close> have "- ?b > 0" by (simp add: pos_imp_zdiv_neg_iff)
1.54      moreover from coprime have "coprime (- ?a) (- ?b)" by simp
1.55      ultimately show C .
1.56    qed
1.57 @@ -240,11 +240,11 @@
1.58    case False
1.59    then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto
1.60    with False have "0 \<noteq> Fract a b" by simp
1.61 -  with `b > 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
1.62 -  with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast
1.63 +  with \<open>b > 0\<close> have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
1.64 +  with Fract \<open>q = Fract a b\<close> \<open>b > 0\<close> \<open>coprime a b\<close> show C by blast
1.65  qed
1.66
1.67 -subsubsection {* Function @{text normalize} *}
1.68 +subsubsection \<open>Function @{text normalize}\<close>
1.69
1.70  lemma Fract_coprime: "Fract (a div gcd a b) (b div gcd a b) = Fract a b"
1.71  proof (cases "b = 0")
1.72 @@ -302,9 +302,9 @@
1.73    "q < 0 \<Longrightarrow> normalize (p, q) = normalize (- p, - q)"
1.74    by (simp add: normalize_def Let_def dvd_div_neg dvd_neg_div)
1.75
1.76 -text{*
1.77 +text\<open>
1.78    Decompose a fraction into normalized, i.e. coprime numerator and denominator:
1.79 -*}
1.80 +\<close>
1.81
1.82  definition quotient_of :: "rat \<Rightarrow> int \<times> int" where
1.83    "quotient_of x = (THE pair. x = Fract (fst pair) (snd pair) &
1.84 @@ -327,11 +327,11 @@
1.85        case False
1.86        with Fract Fract' have *: "c * b = a * d" and "c \<noteq> 0" by (auto simp add: eq_rat)
1.87        then have "c * b > 0 \<longleftrightarrow> a * d > 0" by auto
1.88 -      with `b > 0` `d > 0` have "a > 0 \<longleftrightarrow> c > 0" by (simp add: zero_less_mult_iff)
1.89 -      with `a \<noteq> 0` `c \<noteq> 0` have sgn: "sgn a = sgn c" by (auto simp add: not_less)
1.90 -      from `coprime a b` `coprime c d` have "\<bar>a\<bar> * \<bar>d\<bar> = \<bar>c\<bar> * \<bar>b\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> \<bar>d\<bar> = \<bar>b\<bar>"
1.91 +      with \<open>b > 0\<close> \<open>d > 0\<close> have "a > 0 \<longleftrightarrow> c > 0" by (simp add: zero_less_mult_iff)
1.92 +      with \<open>a \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have sgn: "sgn a = sgn c" by (auto simp add: not_less)
1.93 +      from \<open>coprime a b\<close> \<open>coprime c d\<close> have "\<bar>a\<bar> * \<bar>d\<bar> = \<bar>c\<bar> * \<bar>b\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> \<bar>d\<bar> = \<bar>b\<bar>"
1.95 -      with `b > 0` `d > 0` have "\<bar>a\<bar> * d = \<bar>c\<bar> * b \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> d = b" by simp
1.96 +      with \<open>b > 0\<close> \<open>d > 0\<close> have "\<bar>a\<bar> * d = \<bar>c\<bar> * b \<longleftrightarrow> \<bar>a\<bar> = \<bar>c\<bar> \<and> d = b" by simp
1.97        then have "a * sgn a * d = c * sgn c * b \<longleftrightarrow> a * sgn a = c * sgn c \<and> d = b" by (simp add: abs_sgn)
1.98        with sgn * show ?thesis by (auto simp add: sgn_0_0)
1.99      qed
1.100 @@ -387,7 +387,7 @@
1.101    by (auto simp add: quotient_of_inject)
1.102
1.103
1.104 -subsubsection {* Various *}
1.105 +subsubsection \<open>Various\<close>
1.106
1.107  lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
1.108    by (simp add: Fract_of_int_eq [symmetric])
1.109 @@ -404,7 +404,7 @@
1.110    thus ?thesis using Fract_of_int_quotient by simp
1.111  qed
1.112
1.113 -subsubsection {* The ordered field of rational numbers *}
1.114 +subsubsection \<open>The ordered field of rational numbers\<close>
1.115
1.116  lift_definition positive :: "rat \<Rightarrow> bool"
1.117    is "\<lambda>x. 0 < fst x * snd x"
1.118 @@ -418,7 +418,7 @@
1.119    hence "0 < a * b * d\<^sup>2 \<longleftrightarrow> 0 < c * d * b\<^sup>2"
1.120      by simp
1.121    thus "0 < a * b \<longleftrightarrow> 0 < c * d"
1.122 -    using `b \<noteq> 0` and `d \<noteq> 0`
1.123 +    using \<open>b \<noteq> 0\<close> and \<open>d \<noteq> 0\<close>
1.125  qed
1.126
1.127 @@ -570,7 +570,7 @@
1.128    by (simp add: One_rat_def mult_le_cancel_right)
1.129
1.130
1.131 -subsubsection {* Rationals are an Archimedean field *}
1.132 +subsubsection \<open>Rationals are an Archimedean field\<close>
1.133
1.134  lemma rat_floor_lemma:
1.135    shows "of_int (a div b) \<le> Fract a b \<and> Fract a b < of_int (a div b + 1)"
1.136 @@ -613,9 +613,9 @@
1.137    by (simp add: Fract_of_int_quotient floor_divide_of_int_eq)
1.138
1.139
1.140 -subsection {* Linear arithmetic setup *}
1.141 +subsection \<open>Linear arithmetic setup\<close>
1.142
1.143 -declaration {*
1.144 +declaration \<open>
1.145    K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
1.146      (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
1.147    #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2]
1.148 @@ -632,10 +632,10 @@
1.150    #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"})
1.151    #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"}))
1.152 -*}
1.153 +\<close>
1.154
1.155
1.156 -subsection {* Embedding from Rationals to other Fields *}
1.157 +subsection \<open>Embedding from Rationals to other Fields\<close>
1.158
1.159  context field_char_0
1.160  begin
1.161 @@ -735,7 +735,7 @@
1.162      using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq)
1.163    show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d)
1.164      \<longleftrightarrow> Fract a b < Fract c d"
1.165 -    using not_zero `b * d > 0`
1.166 +    using not_zero \<open>b * d > 0\<close>
1.167      by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult)
1.168  qed
1.169
1.170 @@ -775,7 +775,7 @@
1.171       (simp add: of_rat_rat Fract_of_int_eq [symmetric])
1.172  qed
1.173
1.174 -text{*Collapse nested embeddings*}
1.175 +text\<open>Collapse nested embeddings\<close>
1.176  lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n"
1.178
1.179 @@ -803,7 +803,7 @@
1.180  where
1.181    "rat_of_int \<equiv> of_int"
1.182
1.183 -subsection {* The Set of Rational Numbers *}
1.184 +subsection \<open>The Set of Rational Numbers\<close>
1.185
1.186  context field_char_0
1.187  begin
1.188 @@ -909,7 +909,7 @@
1.189    assumes "q \<in> \<rat>"
1.190    obtains (of_rat) r where "q = of_rat r"
1.191  proof -
1.192 -  from `q \<in> \<rat>` have "q \<in> range of_rat" unfolding Rats_def .
1.193 +  from \<open>q \<in> \<rat>\<close> have "q \<in> range of_rat" unfolding Rats_def .
1.194    then obtain r where "q = of_rat r" ..
1.195    then show thesis ..
1.196  qed
1.197 @@ -921,9 +921,9 @@
1.198  lemma Rats_infinite: "\<not> finite \<rat>"
1.199    by (auto dest!: finite_imageD simp: inj_on_def infinite_UNIV_char_0 Rats_def)
1.200
1.201 -subsection {* Implementation of rational numbers as pairs of integers *}
1.202 +subsection \<open>Implementation of rational numbers as pairs of integers\<close>
1.203
1.204 -text {* Formal constructor *}
1.205 +text \<open>Formal constructor\<close>
1.206
1.207  definition Frct :: "int \<times> int \<Rightarrow> rat" where
1.208    [simp]: "Frct p = Fract (fst p) (snd p)"
1.209 @@ -933,7 +933,7 @@
1.210    by (cases q) (auto intro: quotient_of_eq)
1.211
1.212
1.213 -text {* Numerals *}
1.214 +text \<open>Numerals\<close>
1.215
1.216  declare quotient_of_Fract [code abstract]
1.217
1.218 @@ -967,7 +967,7 @@
1.220
1.221
1.222 -text {* Operations *}
1.223 +text \<open>Operations\<close>
1.224
1.225  lemma rat_zero_code [code abstract]:
1.226    "quotient_of 0 = (0, 1)"
1.227 @@ -1052,7 +1052,7 @@
1.228    by (cases p) (simp add: quotient_of_Fract of_rat_rat)
1.229
1.230
1.231 -text {* Quickcheck *}
1.232 +text \<open>Quickcheck\<close>
1.233
1.234  definition (in term_syntax)
1.235    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.236 @@ -1126,9 +1126,9 @@
1.237  end
1.238
1.239
1.240 -subsection {* Setup for Nitpick *}
1.241 +subsection \<open>Setup for Nitpick\<close>
1.242
1.243 -declaration {*
1.244 +declaration \<open>
1.245    Nitpick_HOL.register_frac_type @{type_name rat}
1.246     [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
1.247      (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
1.248 @@ -1139,7 +1139,7 @@
1.249      (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}),
1.250      (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
1.251      (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac})]
1.252 -*}
1.253 +\<close>
1.254
1.255  lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat
1.256    one_rat_inst.one_rat ord_rat_inst.less_rat
1.257 @@ -1147,11 +1147,11 @@
1.258    uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
1.259
1.260
1.261 -subsection {* Float syntax *}
1.262 +subsection \<open>Float syntax\<close>
1.263
1.264  syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
1.265
1.266 -parse_translation {*
1.267 +parse_translation \<open>
1.268    let
1.269      fun mk_frac str =
1.270        let
1.271 @@ -1165,14 +1165,14 @@
1.272        | float_tr [t as Const (str, _)] = mk_frac str
1.273        | float_tr ts = raise TERM ("float_tr", ts);
1.274    in [(@{syntax_const "_Float"}, K float_tr)] end
1.275 -*}
1.276 +\<close>
1.277
1.278 -text{* Test: *}
1.279 +text\<open>Test:\<close>
1.280  lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
1.281    by simp
1.282
1.283
1.284 -subsection {* Hiding implementation details *}
1.285 +subsection \<open>Hiding implementation details\<close>
1.286
1.287  hide_const (open) normalize positive
1.288
```