1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Aug 26 11:20:41 2013 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Aug 26 15:37:48 2013 +0200
1.3 @@ -280,6 +280,162 @@
1.4 infix mem ins union; (*WN100819 updating to Isabelle2009-2*)
1.5 fun x mem [] = false
1.6 | x mem (y :: ys) = x = y orelse x mem ys;
1.7 +
1.8 +
1.9 +
1.10 +val is_expanded = is_poly
1.11 +val is_polynomial = is_poly
1.12 +
1.13 +fun mk_noteq_0 baseT t =
1.14 + Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $
1.15 + (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ Free ("0", HOLogic.realT))
1.16 +
1.17 +fun check_fraction t =
1.18 + let val Const ("Fields.inverse_class.divide", _) $ numerator $ denominator = t
1.19 + in SOME (numerator, denominator) end
1.20 + handle Bind => NONE
1.21 +
1.22 +(* prepare a term for cancellation by factoring out the gcd
1.23 + assumes: is a fraction with outmost "/"*)
1.24 +fun factout_p_ (thy: theory) t =
1.25 + let val opt = check_fraction t
1.26 + in
1.27 + case opt of
1.28 + NONE => NONE
1.29 + | SOME (numerator, denominator) =>
1.30 + let
1.31 + val vs = t |> vars |> map free2str |> sort string_ord
1.32 + val baseT = type_of numerator
1.33 + val expT = HOLogic.realT
1.34 + in
1.35 + case (poly_of_term vs numerator, poly_of_term vs denominator) of
1.36 + (SOME a, SOME b) =>
1.37 + let
1.38 + val ((a', b'), c) = gcd_poly a b
1.39 + val b't = term_of_poly baseT expT vs b'
1.40 + val ct = term_of_poly baseT expT vs c
1.41 + val t' =
1.42 + HOLogic.mk_binop "Fields.inverse_class.divide"
1.43 + (HOLogic.mk_binop "Groups.times_class.times" (term_of_poly baseT expT vs a', ct),
1.44 + HOLogic.mk_binop "Groups.times_class.times" (b't, ct))
1.45 + val asm = map (mk_noteq_0 baseT) [b't, ct]
1.46 + in SOME (t', asm) end
1.47 + | _ => NONE : (term * term list) option
1.48 + end
1.49 + end
1.50 +
1.51 +(* prepare a term for cancellation by factoring out the gcd
1.52 + assumes: is a fraction with outmost "/"*)
1.53 +fun cancel_p_ (thy: theory) t =
1.54 + let val opt = check_fraction t
1.55 + in
1.56 + case opt of
1.57 + NONE => NONE
1.58 + | SOME (numerator, denominator) =>
1.59 + let
1.60 + val vs = t |> vars |> map free2str |> sort string_ord
1.61 + val baseT = type_of numerator
1.62 + val expT = HOLogic.realT
1.63 + in
1.64 + case (poly_of_term vs numerator, poly_of_term vs denominator) of
1.65 + (SOME a, SOME b) =>
1.66 + let
1.67 + val ((a', b'), c) = gcd_poly a b
1.68 + val b't = term_of_poly baseT expT vs b'
1.69 + val ct = term_of_poly baseT expT vs c
1.70 + val t' =
1.71 + HOLogic.mk_binop "Fields.inverse_class.divide"
1.72 + (term_of_poly baseT expT vs a', b't)
1.73 + val asm = map (mk_noteq_0 baseT) [b't, ct]
1.74 + in SOME (t', asm) end
1.75 + | _ => NONE : (term * term list) option
1.76 + end
1.77 + end
1.78 +
1.79 +(* addition of fractions allows (at most) one non-fraction ---postponed after 1st integration*)
1.80 +fun norm_frac_sum
1.81 + (Const ("Groups.plus_class.plus", _) $
1.82 + (Const ("Fields.inverse_class.divide", _) $ n1 $ d1) $
1.83 + (Const ("Fields.inverse_class.divide", _) $ n2 $ d2))
1.84 + = SOME ((n1, d1), (n2, d2))
1.85 + | norm_frac_sum
1.86 + (Const ("Groups.plus_class.plus", _) $
1.87 + nofrac $
1.88 + (Const ("Fields.inverse_class.divide", _) $ n2 $ d2))
1.89 + = SOME ((nofrac, Free ("1", HOLogic.realT)), (n2, d2))
1.90 + | norm_frac_sum
1.91 + (Const ("Groups.plus_class.plus", _) $
1.92 + (Const ("Fields.inverse_class.divide", _) $ n1 $ d1) $
1.93 + nofrac)
1.94 + = SOME ((n1, d1), (nofrac, Free ("1", HOLogic.realT)))
1.95 + | norm_frac_sum _ = NONE
1.96 +
1.97 +(* prepare a term for addition by providing the least common denominator as a product
1.98 + assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)
1.99 +fun common_nominator_p_ (thy: theory) t =
1.100 + let val opt = norm_frac_sum t
1.101 + in
1.102 + case opt of
1.103 + NONE => NONE
1.104 + | SOME ((n1, d1), (n2, d2)) =>
1.105 + let
1.106 + val vs = t |> vars |> map free2str |> sort string_ord
1.107 + val baseT = type_of n1
1.108 + val expT = HOLogic.realT
1.109 + in
1.110 + case (poly_of_term vs d1, poly_of_term vs d2) of
1.111 + (SOME a, SOME b) =>
1.112 + let
1.113 + val ((a', b'), c) = gcd_poly a b
1.114 + val d1' = term_of_poly baseT expT vs a'
1.115 + val d2' = term_of_poly baseT expT vs b'
1.116 + val c' = term_of_poly baseT expT vs c
1.117 + (*----- minimum of parentheses & nice result, but breaks tests: -------------
1.118 + val denom = HOLogic.mk_binop "Groups.times_class.times"
1.119 + (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c')
1.120 + --------------------------------------------------------------------------*)
1.121 + val denom = HOLogic.mk_binop "Groups.times_class.times" (c',
1.122 + HOLogic.mk_binop "Groups.times_class.times" (d1', d2'))
1.123 + (*--------------------------------------------------------------------------*)
1.124 + val t' =
1.125 + HOLogic.mk_binop "Groups.plus_class.plus"
1.126 + (HOLogic.mk_binop "Fields.inverse_class.divide"
1.127 + (HOLogic.mk_binop "Groups.times_class.times" (n1, d2'), denom),
1.128 + HOLogic.mk_binop "Fields.inverse_class.divide"
1.129 + (HOLogic.mk_binop "Groups.times_class.times" (n2, d1'), denom))
1.130 + val asm = map (mk_noteq_0 baseT) [d1', d2', c']
1.131 + in SOME (t', asm) end
1.132 + | _ => NONE : (term * term list) option
1.133 + end
1.134 + end
1.135 +
1.136 +(* add fractions
1.137 + assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)
1.138 +fun add_fraction_p_ (thy: theory) t =
1.139 + let val opt = norm_frac_sum t
1.140 + in
1.141 + case opt of
1.142 + NONE => NONE
1.143 + | SOME ((n1, d1), (n2, d2)) =>
1.144 + let
1.145 + val vs = t |> vars |> map free2str |> sort string_ord
1.146 + val baseT = type_of n1
1.147 + val expT = HOLogic.realT
1.148 + in
1.149 + case (poly_of_term vs d1, poly_of_term vs d2) of
1.150 + (SOME a, SOME b) =>
1.151 + let
1.152 + val ((a', b'), c) = gcd_poly a b
1.153 + val nomin = term_of_poly baseT expT vs
1.154 + (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))
1.155 + val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
1.156 + val t' = HOLogic.mk_binop "Fields.inverse_class.divide" (nomin, denom)
1.157 + val asm = [mk_noteq_0 baseT denom]
1.158 + in SOME (t', asm) end
1.159 + | _ => NONE : (term * term list) option
1.160 + end
1.161 + end
1.162 +
1.163 fun (x ins xs) = if x mem xs then xs else x :: xs;
1.164 fun xs union [] = xs
1.165 | [] union ys = ys