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.24  by (simp add: rat.domain_eq)
    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.94          by (simp add: coprime_crossproduct_int)
    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.124      by (simp add: zero_less_mult_iff)
   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.149    #> Lin_Arith.add_simprocs Numeral_Simprocs.field_divide_cancel_numeral_factor
   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.177  by (induct n) (simp_all add: of_rat_add)
   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.219    by (simp_all add: Fract_of_int_quotient)
   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