\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0,field})" +lemma Ndiv[simp]: "INum (x \

\<^sub>N y) = INum x / (INum y :: 'a::{field_char_0,field})" by (simp add: Ndiv_def) lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" - shows "((INum x :: 'a::{field_char_0,linordered_field})< 0) = 0>\<^sub>N x" + shows "((INum x :: 'a::{field_char_0,linordered_field}) < 0) = 0>\<^sub>N x" proof - obtain a b where x: "x = (a, b)" by (cases x) show ?thesis @@ -401,7 +395,7 @@ lemma Ngt0_iff[simp]: assumes nx: "isnormNum x" - shows "((INum x :: 'a::{field_char_0,linordered_field})> 0) = 0<\<^sub>N x" + shows "((INum x :: 'a::{field_char_0,linordered_field}) > 0) = 0<\<^sub>N x" proof - obtain a b where x: "x = (a, b)" by (cases x) show ?thesis @@ -421,7 +415,7 @@ lemma Nge0_iff[simp]: assumes nx: "isnormNum x" - shows "((INum x :: 'a::{field_char_0,linordered_field}) \ 0) = 0\\<^sub>N x" + shows "(INum x :: 'a::{field_char_0,linordered_field}) \ 0 \ 0\\<^sub>N x" proof - obtain a b where x: "x = (a, b)" by (cases x) show ?thesis @@ -442,12 +436,12 @@ lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" - shows "((INum x :: 'a::{field_char_0,linordered_field}) < INum y) = (x <\<^sub>N y)" + shows "((INum x :: 'a::{field_char_0,linordered_field}) < INum y) \ x <\<^sub>N y" proof - let ?z = "0::'a" - have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" + have "((INum x ::'a) < INum y) \ INum (x -\<^sub>N y) < ?z" using nx ny by simp - also have "\ = (0>\<^sub>N (x -\<^sub>N y))" + also have "\ \ 0>\<^sub>N (x -\<^sub>N y)" using Nlt0_iff[OF Nsub_normN[OF ny]] by simp finally show ?thesis by (simp add: Nlt_def) @@ -456,11 +450,11 @@ lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" - shows "((INum x :: 'a::{field_char_0,linordered_field})\ INum y) = (x \\<^sub>N y)" + shows "((INum x :: 'a::{field_char_0,linordered_field}) \ INum y) \ x \\<^sub>N y" proof - - have "((INum x ::'a) \ INum y) = (INum (x -\<^sub>N y) \ (0::'a))" + have "((INum x ::'a) \ INum y) \ INum (x -\<^sub>N y) \ (0::'a)" using nx ny by simp - also have "\ = (0\\<^sub>N (x -\<^sub>N y))" + also have "\ \ 0\\<^sub>N (x -\<^sub>N y)" using Nle0_iff[OF Nsub_normN[OF ny]] by simp finally show ?thesis by (simp add: Nle_def) @@ -508,7 +502,7 @@ shows "normNum (normNum x) = normNum x" by simp -lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N" +lemma normNum0[simp]: "normNum (0, b) = 0\<^sub>N" "normNum (a, 0) = 0\<^sub>N" by (simp_all add: normNum_def) lemma normNum_Nadd: @@ -520,29 +514,40 @@ assumes "SORT_CONSTRAINT('a::{field_char_0,field})" shows "normNum x +\<^sub>N y = x +\<^sub>N y" proof - - have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all - have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp - also have "\ = INum (x +\<^sub>N y)" by simp - finally show ?thesis using isnormNum_unique[OF n] by simp + have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" + by simp_all + have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" + by simp + also have "\ = INum (x +\<^sub>N y)" + by simp + finally show ?thesis + using isnormNum_unique[OF n] by simp qed lemma Nadd_normNum2[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0,field})" shows "x +\<^sub>N normNum y = x +\<^sub>N y" proof - - have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all - have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp - also have "\ = INum (x +\<^sub>N y)" by simp - finally show ?thesis using isnormNum_unique[OF n] by simp + have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" + by simp_all + have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" + by simp + also have "\ = INum (x +\<^sub>N y)" + by simp + finally show ?thesis + using isnormNum_unique[OF n] by simp qed lemma Nadd_assoc: assumes "SORT_CONSTRAINT('a::{field_char_0,field})" shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" proof - - have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all - have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp - with isnormNum_unique[OF n] show ?thesis by simp + have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" + by simp_all + have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" + by simp + with isnormNum_unique[OF n] show ?thesis + by simp qed lemma Nmul_commute: "isnormNum x \ isnormNum y \ x *\<^sub>N y = y *\<^sub>N x" @@ -557,8 +562,10 @@ proof - from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" by simp_all - have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp - with isnormNum_unique[OF n] show ?thesis by simp + have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" + by simp + with isnormNum_unique[OF n] show ?thesis + by simp qed lemma Nsub0: @@ -568,9 +575,12 @@ shows "x -\<^sub>N y = 0\<^sub>N \ x = y" proof - from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] - have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp - also have "\ = (INum x = (INum y :: 'a))" by simp - also have "\ = (x = y)" using x y by simp + have "x -\<^sub>N y = 0\<^sub>N \ INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)" + by simp + also have "\ \ INum x = (INum y :: 'a)" + by simp + also have "\ \ x = y" + using x y by simp finally show ?thesis . qed diff -r a9e45c9588c3 -r 7536369a5546 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Wed Jul 08 20:19:12 2015 +0200 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Jul 09 16:49:08 2015 +0200 @@ -8,7 +8,7 @@ imports Complex_Main Rat_Pair Polynomial_List begin -subsection\Datatype of polynomial expressions\ +subsection \Datatype of polynomial expressions\ datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly @@ -66,7 +66,7 @@ | "decrpoly a = a" -subsection\Degrees and heads and coefficients\ +subsection \Degrees and heads and coefficients\ fun degree :: "poly \ nat" where @@ -78,7 +78,8 @@ "head (CN c 0 p) = head p" | "head p = p" -(* More general notions of degree and head *) +text \More general notions of degree and head.\ + fun degreen :: "poly \ nat \ nat" where "degreen (CN c n p) = (\m. if n = m then 1 + degreen p n else 0)" @@ -110,7 +111,7 @@ | "headconst (C n) = n" -subsection\Operations for normalization\ +subsection \Operations for normalization\ declare if_cong[fundef_cong del] declare let_cong[fundef_cong del] @@ -179,7 +180,7 @@ | "polynate (Pw p n) = polynate p ^\<^sub>p n" | "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))" | "polynate (C c) = C (normNum c)" -by pat_completeness auto + by pat_completeness auto termination by (relation "measure polysize") auto fun poly_cmul :: "Num \ poly \ poly" @@ -233,7 +234,7 @@ | "poly_deriv p = 0\<^sub>p" -subsection\Semantics of the polynomial representation\ +subsection \Semantics of the polynomial representation\ primrec Ipoly :: "'a list \ poly \ 'a::{field_char_0,field,power}" where @@ -246,8 +247,7 @@ | "Ipoly bs (Pw t n) = Ipoly bs t ^ n" | "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p" -abbreviation Ipoly_syntax :: "poly \ 'a list \'a::{field_char_0,field,power}" - ("\_\\<^sub>p\<^bsup>_\<^esup>") +abbreviation Ipoly_syntax :: "poly \ 'a list \'a::{field_char_0,field,power}" ("\_\\<^sub>p\<^bsup>_\<^esup>") where "\p\\<^sub>p\<^bsup>bs\<^esup> \ Ipoly bs p" lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i" @@ -273,14 +273,14 @@ definition isnpoly :: "poly \ bool" where "isnpoly p = isnpolyh p 0" -text\polyadd preserves normal forms\ +text \polyadd preserves normal forms\ lemma polyadd_normh: "isnpolyh p n0 \ isnpolyh q n1 \ isnpolyh (polyadd p q) (min n0 n1)" proof (induct p q arbitrary: n0 n1 rule: polyadd.induct) case (2 ab c' n' p' n0 n1) from 2 have th1: "isnpolyh (C ab) (Suc n')" by simp - from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \ n1" + from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \ n1" by simp_all with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp @@ -314,11 +314,11 @@ by simp from 4 have n'gen1: "n' \ n1" by simp - have "n < n' \ n' < n \ n = n'" - by auto - moreover - { - assume eq: "n = n'" + consider (eq) "n = n'" | (lt) "n < n'" | (gt) "n > n'" + by arith + then show ?case + proof cases + case eq with "4.hyps"(3)[OF nc nc'] have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto @@ -329,12 +329,10 @@ by simp have minle: "min n0 n1 \ n'" using ngen0 n'gen1 eq by simp - from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case + from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' show ?thesis by (simp add: Let_def) - } - moreover - { - assume lt: "n < n'" + next + case lt have "min n0 n1 \ n0" by simp with 4 lt have th1:"min n0 n1 \ n" @@ -347,12 +345,10 @@ by arith from "4.hyps"(1)[OF th21 th22] have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)" using th23 by simp - with 4 lt th1 have ?case + with 4 lt th1 show ?thesis by simp - } - moreover - { - assume gt: "n' < n" + next + case gt then have gt': "n' < n \ \ n < n'" by simp have "min n0 n1 \ n1" @@ -367,10 +363,9 @@ by arith from "4.hyps"(2)[OF th22 th21] have "isnpolyh (polyadd (CN c n p) c') (Suc n')" using th23 by simp - with 4 gt th1 have ?case + with 4 gt th1 show ?thesis by simp - } - ultimately show ?case by blast + qed qed auto lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q" @@ -378,9 +373,9 @@ (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left_NO_MATCH) lemma polyadd_norm: "isnpoly p \ isnpoly q \ isnpoly (polyadd p q)" - using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp + using polyadd_normh[of p 0 q 0] isnpoly_def by simp -text\The degree of addition and other general lemmas needed for the normal form of polymul\ +text \The degree of addition and other general lemmas needed for the normal form of polymul.\ lemma polyadd_different_degreen: assumes "isnpolyh p n0" @@ -391,17 +386,13 @@ using assms proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct) case (4 c n p c' n' p' m n0 n1) - have "n' = n \ n < n' \ n' < n" by arith - then show ?case - proof (elim disjE) - assume [simp]: "n' = n" - from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7) + show ?case + proof (cases "n = n'") + case True + with 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7) show ?thesis by (auto simp: Let_def) next - assume "n < n'" - with 4 show ?thesis by auto - next - assume "n' < n" + case False with 4 show ?thesis by auto qed qed auto @@ -441,13 +432,15 @@ by (cases n) auto next case (4 c n p c' n' p' n0 n1 m) - have "n' = n \ n < n' \ n' < n" by arith - then show ?case - proof (elim disjE) - assume [simp]: "n' = n" - from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7) + show ?case + proof (cases "n = n'") + case True + with 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7) show ?thesis by (auto simp: Let_def) - qed simp_all + next + case False + then show ?thesis by simp + qed qed auto lemma polyadd_eq_const_degreen: @@ -458,26 +451,16 @@ using assms proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct) case (4 c n p c' n' p' m n0 n1 x) - { - assume nn': "n' < n" - then have ?case using 4 by simp - } - moreover - { - assume nn': "\ n' < n" - then have "n < n' \ n = n'" by arith - moreover { assume "n < n'" with 4 have ?case by simp } - moreover - { - assume eq: "n = n'" - then have ?case using 4 - apply (cases "p +\<^sub>p p' = 0\<^sub>p") - apply (auto simp add: Let_def) - done - } - ultimately have ?case by blast - } - ultimately show ?case by blast + consider "n = n'" | "n > n' \ n < n'" by arith + then show ?case + proof cases + case 1 + with 4 show ?thesis + by (cases "p +\<^sub>p p' = 0\<^sub>p") (auto simp add: Let_def) + next + case 2 + with 4 show ?thesis by auto + qed qed simp_all lemma polymul_properties: @@ -500,7 +483,7 @@ then show ?case by auto next case (3 n0 n1) - then show ?case using "2.hyps" by auto + then show ?case using "2.hyps" by auto } next case (3 c n p c') @@ -720,7 +703,7 @@ qed -text\polyneg is a negation and preserves normal forms\ +text \polyneg is a negation and preserves normal forms\ lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p" by (induct p rule: polyneg.induct) auto @@ -738,7 +721,7 @@ using isnpoly_def polyneg_normh by simp -text\polysub is a substraction and preserves normal forms\ +text \polysub is a substraction and preserves normal forms\ lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p - Ipoly bs q" by (simp add: polysub_def) @@ -762,7 +745,7 @@ by (induct p q arbitrary: n0 n1 rule:polyadd.induct) (auto simp: Nsub0[simplified Nsub_def] Let_def) -text\polypow is a power function and preserves normal forms\ +text \polypow is a power function and preserves normal forms\ lemma polypow[simp]: "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n" @@ -830,7 +813,7 @@ shows "isnpoly p \ isnpoly (polypow k p)" by (simp add: polypow_normh isnpoly_def) -text\Finally the whole normalization\ +text \Finally the whole normalization\ lemma polynate [simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})" @@ -843,7 +826,7 @@ (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm, simp_all add: isnpoly_def) -text\shift1\ +text \shift1\ lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)" @@ -1254,7 +1237,7 @@ qed -text\consequences of unicity on the algorithms for polynomial normalization\ +text \consequences of unicity on the algorithms for polynomial normalization\ lemma polyadd_commute: assumes "SORT_CONSTRAINT('a::{field_char_0,field})" @@ -1328,7 +1311,7 @@ unfolding poly_nate_polypoly' by auto -subsection\heads, degrees and all that\ +subsection \heads, degrees and all that\ lemma degree_eq_degreen0: "degree p = degreen p 0" by (induct p rule: degree.induct) simp_all diff -r a9e45c9588c3 -r 7536369a5546 src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Wed Jul 08 20:19:12 2015 +0200 +++ b/src/HOL/Eisbach/match_method.ML Thu Jul 09 16:49:08 2015 +0200 @@ -304,7 +304,7 @@ fun prep_fact_pat ((x, args), pat) ctxt = let - val ((params, pat'), ctxt') = Variable.focus pat ctxt; + val ((params, pat'), ctxt') = Variable.focus NONE pat ctxt; val params' = map (Free o snd) params; val morphism = @@ -500,10 +500,10 @@ (* Fix schematics in the goal *) -fun focus_concl ctxt i goal = +fun focus_concl ctxt i bindings goal = let val ({context = ctxt', concl, params, prems, asms, schematics}, goal') = - Subgoal.focus_params ctxt i goal; + Subgoal.focus_params ctxt i bindings goal; val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt'; val (_, schematic_terms) = Thm.certify_inst ctxt'' inst; @@ -711,7 +711,7 @@ val (goal_thins, goal) = get_thinned_prems goal; val ((local_premids, {context = focus_ctxt, params, asms, concl, ...}), focused_goal) = - focus_cases (K Subgoal.focus_prems) (focus_concl) ctxt 1 goal + focus_cases (K Subgoal.focus_prems) focus_concl ctxt 1 NONE goal |>> augment_focus; val texts = diff -r a9e45c9588c3 -r 7536369a5546 src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Wed Jul 08 20:19:12 2015 +0200 +++ b/src/HOL/Library/Float.thy Thu Jul 09 16:49:08 2015 +0200 @@ -22,6 +22,7 @@ real_of_float_def[code_unfold]: "real \ real_of_float" instance .. + end lemma type_definition_float': "type_definition real float_of float" @@ -34,7 +35,8 @@ declare [[coercion "real :: float \ real"]] lemma real_of_float_eq: - fixes f1 f2 :: float shows "f1 = f2 \ real f1 = real f2" + fixes f1 f2 :: float + shows "f1 = f2 \ real f1 = real f2" unfolding real_of_float_def real_of_float_inject .. lemma float_of_real[simp]: "float_of (real x) = x" @@ -43,40 +45,63 @@ lemma real_float[simp]: "x \ float \ real (float_of x) = x" unfolding real_of_float_def by (rule float_of_inverse) + subsection \Real operations preserving the representation as floating point number\ lemma floatI: fixes m e :: int shows "m * 2 powr e = x \ x \ float" by (auto simp: float_def) -lemma zero_float[simp]: "0 \ float" by (auto simp: float_def) -lemma one_float[simp]: "1 \ float" by (intro floatI[of 1 0]) simp -lemma numeral_float[simp]: "numeral i \ float" by (intro floatI[of "numeral i" 0]) simp -lemma neg_numeral_float[simp]: "- numeral i \ float" by (intro floatI[of "- numeral i" 0]) simp -lemma real_of_int_float[simp]: "real (x :: int) \ float" by (intro floatI[of x 0]) simp -lemma real_of_nat_float[simp]: "real (x :: nat) \ float" by (intro floatI[of x 0]) simp -lemma two_powr_int_float[simp]: "2 powr (real (i::int)) \ float" by (intro floatI[of 1 i]) simp -lemma two_powr_nat_float[simp]: "2 powr (real (i::nat)) \ float" by (intro floatI[of 1 i]) simp -lemma two_powr_minus_int_float[simp]: "2 powr - (real (i::int)) \ float" by (intro floatI[of 1 "-i"]) simp -lemma two_powr_minus_nat_float[simp]: "2 powr - (real (i::nat)) \ float" by (intro floatI[of 1 "-i"]) simp -lemma two_powr_numeral_float[simp]: "2 powr numeral i \ float" by (intro floatI[of 1 "numeral i"]) simp -lemma two_powr_neg_numeral_float[simp]: "2 powr - numeral i \ float" by (intro floatI[of 1 "- numeral i"]) simp -lemma two_pow_float[simp]: "2 ^ n \ float" by (intro floatI[of 1 "n"]) (simp add: powr_realpow) -lemma real_of_float_float[simp]: "real (f::float) \ float" by (cases f) simp +lemma zero_float[simp]: "0 \ float" + by (auto simp: float_def) +lemma one_float[simp]: "1 \ float" + by (intro floatI[of 1 0]) simp +lemma numeral_float[simp]: "numeral i \ float" + by (intro floatI[of "numeral i" 0]) simp +lemma neg_numeral_float[simp]: "- numeral i \ float" + by (intro floatI[of "- numeral i" 0]) simp +lemma real_of_int_float[simp]: "real (x :: int) \ float" + by (intro floatI[of x 0]) simp +lemma real_of_nat_float[simp]: "real (x :: nat) \ float" + by (intro floatI[of x 0]) simp +lemma two_powr_int_float[simp]: "2 powr (real (i::int)) \ float" + by (intro floatI[of 1 i]) simp +lemma two_powr_nat_float[simp]: "2 powr (real (i::nat)) \ float" + by (intro floatI[of 1 i]) simp +lemma two_powr_minus_int_float[simp]: "2 powr - (real (i::int)) \ float" + by (intro floatI[of 1 "-i"]) simp +lemma two_powr_minus_nat_float[simp]: "2 powr - (real (i::nat)) \ float" + by (intro floatI[of 1 "-i"]) simp +lemma two_powr_numeral_float[simp]: "2 powr numeral i \ float" + by (intro floatI[of 1 "numeral i"]) simp +lemma two_powr_neg_numeral_float[simp]: "2 powr - numeral i \ float" + by (intro floatI[of 1 "- numeral i"]) simp +lemma two_pow_float[simp]: "2 ^ n \ float" + by (intro floatI[of 1 "n"]) (simp add: powr_realpow) +lemma real_of_float_float[simp]: "real (f::float) \ float" + by (cases f) simp lemma plus_float[simp]: "r \ float \ p \ float \ r + p \ float" unfolding float_def proof (safe, simp) - fix e1 m1 e2 m2 :: int - { fix e1 m1 e2 m2 :: int assume "e1 \ e2" - then have "m1 * 2 powr e1 + m2 * 2 powr e2 = (m1 + m2 * 2 ^ nat (e2 - e1)) * 2 powr e1" + have *: "\(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e" + if "e1 \ e2" for e1 m1 e2 m2 :: int + proof - + from that have "m1 * 2 powr e1 + m2 * 2 powr e2 = (m1 + m2 * 2 ^ nat (e2 - e1)) * 2 powr e1" by (simp add: powr_realpow[symmetric] powr_divide2[symmetric] field_simps) - then have "\(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e" - by blast } - note * = this - show "\(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e" - proof (cases e1 e2 rule: linorder_le_cases) - assume "e2 \ e1" from *[OF this, of m2 m1] show ?thesis by (simp add: ac_simps) - qed (rule *) + then show ?thesis + by blast + qed + fix e1 m1 e2 m2 :: int + consider "e2 \ e1" | "e1 \ e2" by (rule linorder_le_cases) + then show "\(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e" + proof cases + case 1 + from *[OF this, of m2 m1] show ?thesis + by (simp add: ac_simps) + next + case 2 + then show ?thesis by (rule *) + qed qed lemma uminus_float[simp]: "x \ float \ -x \ float" @@ -125,7 +150,8 @@ done lemma div_numeral_Bit0_float[simp]: - assumes x: "x / numeral n \ float" shows "x / (numeral (Num.Bit0 n)) \ float" + assumes x: "x / numeral n \ float" + shows "x / (numeral (Num.Bit0 n)) \ float" proof - have "(x / numeral n) / 2^1 \ float" by (intro x div_power_2_float) @@ -135,32 +161,38 @@ qed lemma div_neg_numeral_Bit0_float[simp]: - assumes x: "x / numeral n \ float" shows "x / (- numeral (Num.Bit0 n)) \ float" + assumes x: "x / numeral n \ float" + shows "x / (- numeral (Num.Bit0 n)) \ float" proof - - have "- (x / numeral (Num.Bit0 n)) \ float" using x by simp + have "- (x / numeral (Num.Bit0 n)) \ float" + using x by simp also have "- (x / numeral (Num.Bit0 n)) = x / - numeral (Num.Bit0 n)" by simp finally show ?thesis . qed -lemma power_float[simp]: assumes "a \ float" shows "a ^ b \ float" +lemma power_float[simp]: + assumes "a \ float" + shows "a ^ b \ float" proof - - from assms obtain m e::int where "a = m * 2 powr e" + from assms obtain m e :: int where "a = m * 2 powr e" by (auto simp: float_def) - thus ?thesis + then show ?thesis by (auto intro!: floatI[where m="m^b" and e = "e*b"] simp: power_mult_distrib powr_realpow[symmetric] powr_powr) qed -lift_definition Float :: "int \ int \ float" is "\(m::int) (e::int). m * 2 powr e" by simp +lift_definition Float :: "int \ int \ float" is "\(m::int) (e::int). m * 2 powr e" + by simp declare Float.rep_eq[simp] lemma compute_real_of_float[code]: "real_of_float (Float m e) = (if e \ 0 then m * 2 ^ nat e else m / 2 ^ (nat (-e)))" -by (simp add: real_of_float_def[symmetric] powr_int) + by (simp add: real_of_float_def[symmetric] powr_int) code_datatype Float + subsection \Arithmetic operations on floating point numbers\ instantiation float :: "{ring_1, linorder, linordered_ring, linordered_idom, numeral, equal}" @@ -192,16 +224,20 @@ declare less_float.rep_eq[simp] instance - proof qed (transfer, fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+ + by (standard; transfer; fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+ + end lemma Float_0_eq_0[simp]: "Float 0 e = 0" by transfer simp -lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n" +lemma real_of_float_power[simp]: + fixes f :: float + shows "real (f^n) = real f^n" by (induct n) simp_all -lemma fixes x y::float +lemma + fixes x y :: float shows real_of_float_min: "real (min x y) = min (real x) (real y)" and real_of_float_max: "real (max x y) = max (real x) (real y)" by (simp_all add: min_def max_def) @@ -219,9 +255,9 @@ apply transfer apply simp done - assume "a < b" - then show "\c. a < c \ c < b" - apply (intro exI[of _ "(a + b) * Float 1 (- 1)"]) + show "\c. a < c \ c < b" if "a < b" + apply (rule exI[of _ "(a + b) * Float 1 (- 1)"]) + using that apply transfer apply (simp add: powr_minus) done @@ -230,11 +266,11 @@ instantiation float :: lattice_ab_group_add begin -definition inf_float::"float\float\float" -where "inf_float a b = min a b" +definition inf_float :: "float \ float \ float" + where "inf_float a b = min a b" -definition sup_float::"float\float\float" -where "sup_float a b = max a b" +definition sup_float :: "float \ float \ float" + where "sup_float a b = max a b" instance by (standard; transfer; simp add: inf_float_def sup_float_def real_of_float_min real_of_float_max) @@ -250,20 +286,21 @@ lemma transfer_numeral [transfer_rule]: "rel_fun (op =) pcr_float (numeral :: _ \ real) (numeral :: _ \ float)" - unfolding rel_fun_def float.pcr_cr_eq cr_float_def by simp + by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def) lemma float_neg_numeral[simp]: "real (- numeral x :: float) = - numeral x" by simp lemma transfer_neg_numeral [transfer_rule]: "rel_fun (op =) pcr_float (- numeral :: _ \ real) (- numeral :: _ \ float)" - unfolding rel_fun_def float.pcr_cr_eq cr_float_def by simp + by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def) lemma shows float_of_numeral[simp]: "numeral k = float_of (numeral k)" and float_of_neg_numeral[simp]: "- numeral k = float_of (- numeral k)" unfolding real_of_float_eq by simp_all + subsection \Quickcheck\ instantiation float :: exhaustive @@ -311,39 +348,51 @@ assumes H: "\n. (\i. \i\ < \n\ \ P i) \ P n" shows "P j" proof (induct "nat \j\" arbitrary: j rule: less_induct) - case less show ?case by (rule H[OF less]) simp + case less + show ?case by (rule H[OF less]) simp qed lemma int_cancel_factors: - fixes n :: int assumes "1 < r" shows "n = 0 \ (\k i. n = k * r ^ i \ \ r dvd k)" + fixes n :: int + assumes "1 < r" + shows "n = 0 \ (\k i. n = k * r ^ i \ \ r dvd k)" proof (induct n rule: int_induct_abs) case (less n) - { fix m assume n: "n \ 0" "n = m * r" - then have "\m \ < \n\" + have "\k i. n = k * r ^ Suc i \ \ r dvd k" if "n \ 0" "n = m * r" for m + proof - + from that have "\m \ < \n\" using \1 < r\ by (simp add: abs_mult) - from less[OF this] n have "\k i. n = k * r ^ Suc i \ \ r dvd k" by auto } + from less[OF this] that show ?thesis by auto + qed then show ?case by (metis dvd_def monoid_mult_class.mult.right_neutral mult.commute power_0) qed lemma mult_powr_eq_mult_powr_iff_asym: fixes m1 m2 e1 e2 :: int - assumes m1: "\ 2 dvd m1" and "e1 \ e2" + assumes m1: "\ 2 dvd m1" + and "e1 \ e2" shows "m1 * 2 powr e1 = m2 * 2 powr e2 \ m1 = m2 \ e1 = e2" + (is "?lhs \ ?rhs") proof - have "m1 \ 0" using m1 unfolding dvd_def by auto - assume eq: "m1 * 2 powr e1 = m2 * 2 powr e2" - with \e1 \ e2\ have "m1 = m2 * 2 powr nat (e2 - e1)" - by (simp add: powr_divide2[symmetric] field_simps) - also have "\ = m2 * 2^nat (e2 - e1)" - by (simp add: powr_realpow) - finally have m1_eq: "m1 = m2 * 2^nat (e2 - e1)" - unfolding real_of_int_inject . - with m1 have "m1 = m2" - by (cases "nat (e2 - e1)") (auto simp add: dvd_def) - then show "m1 = m2 \ e1 = e2" - using eq \m1 \ 0\ by (simp add: powr_inj) -qed simp + show ?rhs if eq: ?lhs + proof - + have "m1 \ 0" + using m1 unfolding dvd_def by auto + from \e1 \ e2\ eq have "m1 = m2 * 2 powr nat (e2 - e1)" + by (simp add: powr_divide2[symmetric] field_simps) + also have "\ = m2 * 2^nat (e2 - e1)" + by (simp add: powr_realpow) + finally have m1_eq: "m1 = m2 * 2^nat (e2 - e1)" + unfolding real_of_int_inject . + with m1 have "m1 = m2" + by (cases "nat (e2 - e1)") (auto simp add: dvd_def) + then show ?thesis + using eq \m1 \ 0\ by (simp add: powr_inj) + qed + show ?lhs if ?rhs + using that by simp +qed lemma mult_powr_eq_mult_powr_iff: fixes m1 m2 e1 e2 :: int @@ -356,16 +405,18 @@ assumes x: "x \ float" obtains (zero) "x = 0" | (powr) m e :: int where "x = m * 2 powr e" "\ 2 dvd m" "x \ 0" -proof atomize_elim - { assume "x \ 0" - from x obtain m e :: int where x: "x = m * 2 powr e" by (auto simp: float_def) +proof - + { + assume "x \ 0" + from x obtain m e :: int where x: "x = m * 2 powr e" + by (auto simp: float_def) with \x \ 0\ int_cancel_factors[of 2 m] obtain k i where "m = k * 2 ^ i" "\ 2 dvd k" by auto with \\ 2 dvd k\ x have "\(m::int) (e::int). x = m * 2 powr e \ \ (2::int) dvd m" by (rule_tac exI[of _ "k"], rule_tac exI[of _ "e + int i"]) - (simp add: powr_add powr_realpow) } - then show "x = 0 \ (\(m::int) (e::int). x = m * 2 powr e \ \ (2::int) dvd m \ x \ 0)" - by blast + (simp add: powr_add powr_realpow) + } + with that show thesis by blast qed lemma float_normed_cases: @@ -373,7 +424,8 @@ obtains (zero) "f = 0" | (powr) m e :: int where "real f = m * 2 powr e" "\ 2 dvd m" "f \ 0" proof (atomize_elim, induct f) - case (float_of y) then show ?case + case (float_of y) + then show ?case by (cases rule: floatE_normed) (auto simp: zero_float_def) qed @@ -389,7 +441,8 @@ shows exponent_0[simp]: "exponent (float_of 0) = 0" (is ?E) and mantissa_0[simp]: "mantissa (float_of 0) = 0" (is ?M) proof - - have "\p::int \ int. fst p = 0 \ snd p = 0 \ p = (0, 0)" by auto + have "\p::int \ int. fst p = 0 \ snd p = 0 \ p = (0, 0)" + by auto then show ?E ?M by (auto simp add: mantissa_def exponent_def zero_float_def) qed @@ -398,17 +451,20 @@ shows mantissa_exponent: "real f = mantissa f * 2 powr exponent f" (is ?E) and mantissa_not_dvd: "f \ (float_of 0) \ \ 2 dvd mantissa f" (is "_ \ ?D") proof cases - assume [simp]: "f \ (float_of 0)" + assume [simp]: "f \ float_of 0" have "f = mantissa f * 2 powr exponent f \ \ 2 dvd mantissa f" proof (cases f rule: float_normed_cases) + case zero + then show ?thesis by (simp add: zero_float_def) + next case (powr m e) - then have "\p::int \ int. (f = 0 \ fst p = 0 \ snd p = 0) - \ (f \ 0 \ real f = real (fst p) * 2 powr real (snd p) \ \ 2 dvd fst p)" + then have "\p::int \ int. (f = 0 \ fst p = 0 \ snd p = 0) \ + (f \ 0 \ real f = real (fst p) * 2 powr real (snd p) \ \ 2 dvd fst p)" by auto then show ?thesis unfolding exponent_def mantissa_def by (rule someI2_ex) (simp add: zero_float_def) - qed (simp add: zero_float_def) + qed then show ?E ?D by auto qed simp @@ -422,31 +478,33 @@ shows mantissa_float: "mantissa f = m" (is "?M") and exponent_float: "m \ 0 \ exponent f = e" (is "_ \ ?E") proof cases - assume "m = 0" with dvd show "mantissa f = m" by auto + assume "m = 0" + with dvd show "mantissa f = m" by auto next assume "m \ 0" then have f_not_0: "f \ float_of 0" by (simp add: f_def) - from mantissa_exponent[of f] - have "m * 2 powr e = mantissa f * 2 powr exponent f" + from mantissa_exponent[of f] have "m * 2 powr e = mantissa f * 2 powr exponent f" by (auto simp add: f_def) then show "?M" "?E" using mantissa_not_dvd[OF f_not_0] dvd by (auto simp: mult_powr_eq_mult_powr_iff) qed + subsection \Compute arithmetic operations\ lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f" unfolding real_of_float_eq mantissa_exponent[of f] by simp -lemma Float_cases[case_names Float, cases type: float]: +lemma Float_cases [cases type: float]: fixes f :: float obtains (Float) m e :: int where "f = Float m e" using Float_mantissa_exponent[symmetric] by (atomize_elim) auto lemma denormalize_shift: - assumes f_def: "f \ Float m e" and not_0: "f \ float_of 0" + assumes f_def: "f \ Float m e" + and not_0: "f \ float_of 0" obtains i where "m = mantissa f * 2 ^ i" "e = exponent f - i" proof from mantissa_exponent[of f] f_def @@ -481,87 +539,75 @@ unfolding real_of_int_inject by auto qed -lemma compute_float_zero[code_unfold, code]: "0 = Float 0 0" - by transfer simp -hide_fact (open) compute_float_zero +context +begin -lemma compute_float_one[code_unfold, code]: "1 = Float 1 0" +qualified lemma compute_float_zero[code_unfold, code]: "0 = Float 0 0" by transfer simp -hide_fact (open) compute_float_one + +qualified lemma compute_float_one[code_unfold, code]: "1 = Float 1 0" + by transfer simp lift_definition normfloat :: "float \ float" is "\x. x" . lemma normloat_id[simp]: "normfloat x = x" by transfer rule -lemma compute_normfloat[code]: "normfloat (Float m e) = +qualified lemma compute_normfloat[code]: "normfloat (Float m e) = (if m mod 2 = 0 \ m \ 0 then normfloat (Float (m div 2) (e + 1)) else if m = 0 then 0 else Float m e)" by transfer (auto simp add: powr_add zmod_eq_0_iff) -hide_fact (open) compute_normfloat -lemma compute_float_numeral[code_abbrev]: "Float (numeral k) 0 = numeral k" +qualified lemma compute_float_numeral[code_abbrev]: "Float (numeral k) 0 = numeral k" by transfer simp -hide_fact (open) compute_float_numeral -lemma compute_float_neg_numeral[code_abbrev]: "Float (- numeral k) 0 = - numeral k" +qualified lemma compute_float_neg_numeral[code_abbrev]: "Float (- numeral k) 0 = - numeral k" by transfer simp -hide_fact (open) compute_float_neg_numeral -lemma compute_float_uminus[code]: "- Float m1 e1 = Float (- m1) e1" +qualified lemma compute_float_uminus[code]: "- Float m1 e1 = Float (- m1) e1" by transfer simp -hide_fact (open) compute_float_uminus -lemma compute_float_times[code]: "Float m1 e1 * Float m2 e2 = Float (m1 * m2) (e1 + e2)" +qualified lemma compute_float_times[code]: "Float m1 e1 * Float m2 e2 = Float (m1 * m2) (e1 + e2)" by transfer (simp add: field_simps powr_add) -hide_fact (open) compute_float_times -lemma compute_float_plus[code]: "Float m1 e1 + Float m2 e2 = +qualified lemma compute_float_plus[code]: "Float m1 e1 + Float m2 e2 = (if m1 = 0 then Float m2 e2 else if m2 = 0 then Float m1 e1 else if e1 \ e2 then Float (m1 + m2 * 2^nat (e2 - e1)) e1 else Float (m2 + m1 * 2^nat (e1 - e2)) e2)" by transfer (simp add: field_simps powr_realpow[symmetric] powr_divide2[symmetric]) -hide_fact (open) compute_float_plus -lemma compute_float_minus[code]: fixes f g::float shows "f - g = f + (-g)" +qualified lemma compute_float_minus[code]: fixes f g::float shows "f - g = f + (-g)" by simp -hide_fact (open) compute_float_minus -lemma compute_float_sgn[code]: "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)" +qualified lemma compute_float_sgn[code]: "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)" by transfer (simp add: sgn_times) -hide_fact (open) compute_float_sgn lift_definition is_float_pos :: "float \ bool" is "op < 0 :: real \ bool" . -lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \ 0 < m" +qualified lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \ 0 < m" by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0]) -hide_fact (open) compute_is_float_pos -lemma compute_float_less[code]: "a < b \ is_float_pos (b - a)" +qualified lemma compute_float_less[code]: "a < b \ is_float_pos (b - a)" by transfer (simp add: field_simps) -hide_fact (open) compute_float_less lift_definition is_float_nonneg :: "float \ bool" is "op \ 0 :: real \ bool" . -lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \ 0 \ m" +qualified lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \ 0 \ m" by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0]) -hide_fact (open) compute_is_float_nonneg -lemma compute_float_le[code]: "a \ b \ is_float_nonneg (b - a)" +qualified lemma compute_float_le[code]: "a \ b \ is_float_nonneg (b - a)" by transfer (simp add: field_simps) -hide_fact (open) compute_float_le lift_definition is_float_zero :: "float \ bool" is "op = 0 :: real \ bool" . -lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \ 0 = m" +qualified lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \ 0 = m" by transfer (auto simp add: is_float_zero_def) -hide_fact (open) compute_is_float_zero -lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e" +qualified lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e" by transfer (simp add: abs_mult) -hide_fact (open) compute_float_abs -lemma compute_float_eq[code]: "equal_class.equal f g = is_float_zero (f - g)" +qualified lemma compute_float_eq[code]: "equal_class.equal f g = is_float_zero (f - g)" by transfer simp -hide_fact (open) compute_float_eq + +end subsection \Lemmas for types @{typ real}, @{typ nat}, @{typ int}\ @@ -590,11 +636,11 @@ subsection \Rounding Real Numbers\ -definition round_down :: "int \ real \ real" where - "round_down prec x = floor (x * 2 powr prec) * 2 powr -prec" +definition round_down :: "int \ real \ real" + where "round_down prec x = floor (x * 2 powr prec) * 2 powr -prec" -definition round_up :: "int \ real \ real" where - "round_up prec x = ceiling (x * 2 powr prec) * 2 powr -prec" +definition round_up :: "int \ real \ real" + where "round_up prec x = ceiling (x * 2 powr prec) * 2 powr -prec" lemma round_down_float[simp]: "round_down prec x \