1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Jun 21 14:39:52 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Jun 21 15:36:09 2021 +0200
1.3 @@ -22,20 +22,20 @@
1.4 ML \<open>
1.5 (*.the expression contains + - * ^ / only ?.*)
1.6 fun is_ratpolyexp (Free _) = true
1.7 - | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
1.8 - | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
1.9 - | is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
1.10 - | is_ratpolyexp (Const ("Transcendental.powr",_) $ Free _ $ Free _) = true
1.11 - | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ Free _ $ Free _) = true
1.12 - | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1.13 + | is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ Free _ $ Free _) = true
1.14 + | is_ratpolyexp (Const (\<^const_name>\<open>minus\<close>,_) $ Free _ $ Free _) = true
1.15 + | is_ratpolyexp (Const (\<^const_name>\<open>times\<close>,_) $ Free _ $ Free _) = true
1.16 + | is_ratpolyexp (Const (\<^const_name>\<open>powr\<close>,_) $ Free _ $ Free _) = true
1.17 + | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ Free _ $ Free _) = true
1.18 + | is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) =
1.19 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
1.20 - | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
1.21 + | is_ratpolyexp (Const (\<^const_name>\<open>minus\<close>,_) $ t1 $ t2) =
1.22 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
1.23 - | is_ratpolyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
1.24 + | is_ratpolyexp (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ t2) =
1.25 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
1.26 - | is_ratpolyexp (Const ("Transcendental.powr",_) $ t1 $ t2) =
1.27 + | is_ratpolyexp (Const (\<^const_name>\<open>powr\<close>,_) $ t1 $ t2) =
1.28 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
1.29 - | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ t1 $ t2) =
1.30 + | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ t1 $ t2) =
1.31 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
1.32 | is_ratpolyexp _ = false;
1.33
1.34 @@ -52,7 +52,7 @@
1.35 (*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
1.36 fun eval_get_denominator (thmid:string) _
1.37 (t as Const ("Rational.get_denominator", _) $
1.38 - (Const ("Rings.divide_class.divide", _) $ _(*num*) $
1.39 + (Const (\<^const_name>\<open>divide\<close>, _) $ _(*num*) $
1.40 denom)) thy =
1.41 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "",
1.42 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
1.43 @@ -61,7 +61,7 @@
1.44 (*("get_numerator", ("Rational.get_numerator", eval_get_numerator ""))*)
1.45 fun eval_get_numerator (thmid:string) _
1.46 (t as Const ("Rational.get_numerator", _) $
1.47 - (Const ("Rings.divide_class.divide", _) $num
1.48 + (Const (\<^const_name>\<open>divide\<close>, _) $num
1.49 $denom )) thy =
1.50 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "",
1.51 HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
1.52 @@ -127,9 +127,9 @@
1.53 if TermC.is_num' id
1.54 then (id |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
1.55 else (c, list_update es (find_index (curry op = t) vs) 1)
1.56 - | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (t as Free _) $ Free (e, _)) =
1.57 + | monom_of_term vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (t as Free _) $ Free (e, _)) =
1.58 (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_opt_of_string e)))
1.59 - | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
1.60 + | monom_of_term vs (c, es) (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2) =
1.61 let val (c', es') = monom_of_term vs (c, es) m1
1.62 in monom_of_term vs (c', es') m2 end
1.63 | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
1.64 @@ -138,11 +138,11 @@
1.65 [monom_of_term vs (1, replicate (length vs) 0) t]
1.66 | monoms_of_term vs (t as Free _) =
1.67 [monom_of_term vs (1, replicate (length vs) 0) t]
1.68 - | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $ _) =
1.69 + | monoms_of_term vs (t as Const (\<^const_name>\<open>powr\<close>, _) $ _ $ _) =
1.70 [monom_of_term vs (1, replicate (length vs) 0) t]
1.71 - | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $ _) =
1.72 + | monoms_of_term vs (t as Const (\<^const_name>\<open>times\<close>, _) $ _ $ _) =
1.73 [monom_of_term vs (1, replicate (length vs) 0) t]
1.74 - | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =
1.75 + | monoms_of_term vs (Const (\<^const_name>\<open>plus\<close>, _) $ ms1 $ ms2) =
1.76 (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
1.77 | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)
1.78
1.79 @@ -156,7 +156,7 @@
1.80 The function requires the free variables as strings already given,
1.81 because the gcd involves 2 polynomials (with the same length for their list of exponents).
1.82 *)
1.83 -fun poly_of_term vs (t as Const ("Groups.plus_class.plus", _) $ _ $ _) =
1.84 +fun poly_of_term vs (t as Const (\<^const_name>\<open>plus\<close>, _) $ _ $ _) =
1.85 (SOME (t |> monoms_of_term vs |> order)
1.86 handle ERROR _ => NONE)
1.87 | poly_of_term vs t =
1.88 @@ -179,7 +179,7 @@
1.89 | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
1.90 | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
1.91 | term_of_es baseT expT (v :: vs) (e :: es) =
1.92 - Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (Free (TermC.isastr_of_int e, expT))
1.93 + Const (\<^const_name>\<open>powr\<close>, [baseT, expT] ---> baseT) $ v $ (Free (TermC.isastr_of_int e, expT))
1.94 :: term_of_es baseT expT vs es
1.95 | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
1.96
1.97 @@ -190,20 +190,20 @@
1.98 then
1.99 if es' = [] (*if es = [0,0,0,...]*)
1.100 then Free (TermC.isastr_of_int c, baseT)
1.101 - else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')
1.102 - else foldl (HOLogic.mk_binop "Groups.times_class.times") (Free (TermC.isastr_of_int c, baseT), es')
1.103 + else foldl (HOLogic.mk_binop \<^const_name>\<open>times\<close>) (hd es', tl es')
1.104 + else foldl (HOLogic.mk_binop \<^const_name>\<open>times\<close>) (Free (TermC.isastr_of_int c, baseT), es')
1.105 end
1.106
1.107 fun term_of_poly baseT expT vs p =
1.108 let val monos = map (term_of_monom baseT expT vs) p
1.109 - in foldl (HOLogic.mk_binop "Groups.plus_class.plus") (hd monos, tl monos) end
1.110 + in foldl (HOLogic.mk_binop \<^const_name>\<open>plus\<close>) (hd monos, tl monos) end
1.111 \<close>
1.112
1.113 subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
1.114 ML \<open>
1.115 fun mk_noteq_0 baseT t =
1.116 - Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $
1.117 - (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ Free ("0", HOLogic.realT))
1.118 + Const (\<^const_name>\<open>Not\<close>, HOLogic.boolT --> HOLogic.boolT) $
1.119 + (Const (\<^const_name>\<open>HOL.eq\<close>, [baseT, baseT] ---> HOLogic.boolT) $ t $ Free ("0", HOLogic.realT))
1.120
1.121 fun mk_asms baseT ts =
1.122 let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
1.123 @@ -214,7 +214,7 @@
1.124 ML \<open>
1.125 fun check_fraction t =
1.126 case t of
1.127 - Const ("Rings.divide_class.divide", _) $ numerator $ denominator
1.128 + Const (\<^const_name>\<open>divide\<close>, _) $ numerator $ denominator
1.129 => SOME (numerator, denominator)
1.130 | _ => NONE
1.131
1.132 @@ -244,10 +244,10 @@
1.133 val b't = term_of_poly baseT expT vs b'
1.134 val ct = term_of_poly baseT expT vs c
1.135 val t' =
1.136 - HOLogic.mk_binop "Rings.divide_class.divide"
1.137 - (HOLogic.mk_binop "Groups.times_class.times"
1.138 + HOLogic.mk_binop \<^const_name>\<open>divide\<close>
1.139 + (HOLogic.mk_binop \<^const_name>\<open>times\<close>
1.140 (term_of_poly baseT expT vs a', ct),
1.141 - HOLogic.mk_binop "Groups.times_class.times" (b't, ct))
1.142 + HOLogic.mk_binop \<^const_name>\<open>times\<close> (b't, ct))
1.143 in SOME (t', mk_asms baseT [b't, ct]) end
1.144 end
1.145 | _ => NONE : (term * term list) option
1.146 @@ -289,7 +289,7 @@
1.147 val bt' = term_of_poly baseT expT vs b'
1.148 val ct = term_of_poly baseT expT vs c
1.149 val t' =
1.150 - HOLogic.mk_binop "Rings.divide_class.divide"
1.151 + HOLogic.mk_binop \<^const_name>\<open>divide\<close>
1.152 (term_of_poly baseT expT vs a', bt')
1.153 val asm = mk_asms baseT [bt']
1.154 in SOME (t', asm) end
1.155 @@ -303,18 +303,18 @@
1.156 ML \<open>
1.157 (* addition of fractions allows (at most) one non-fraction (a monomial) *)
1.158 fun check_frac_sum
1.159 - (Const ("Groups.plus_class.plus", _) $
1.160 - (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $
1.161 - (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
1.162 + (Const (\<^const_name>\<open>plus\<close>, _) $
1.163 + (Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $
1.164 + (Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
1.165 = SOME ((n1, d1), (n2, d2))
1.166 | check_frac_sum
1.167 - (Const ("Groups.plus_class.plus", _) $
1.168 + (Const (\<^const_name>\<open>plus\<close>, _) $
1.169 nofrac $
1.170 - (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
1.171 + (Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
1.172 = SOME ((nofrac, Free ("1", HOLogic.realT)), (n2, d2))
1.173 | check_frac_sum
1.174 - (Const ("Groups.plus_class.plus", _) $
1.175 - (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $
1.176 + (Const (\<^const_name>\<open>plus\<close>, _) $
1.177 + (Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $
1.178 nofrac)
1.179 = SOME ((n1, d1), (nofrac, Free ("1", HOLogic.realT)))
1.180 | check_frac_sum _ = NONE
1.181 @@ -337,20 +337,20 @@
1.182 val (baseT, expT) = (type_of n1, HOLogic.realT)
1.183 val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]
1.184 (*----- minimum of parentheses & nice result, but breaks tests: -------------
1.185 - val denom = HOLogic.mk_binop "Groups.times_class.times"
1.186 - (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') -------------*)
1.187 + val denom = HOLogic.mk_binop \<^const_name>\<open>times\<close>
1.188 + (HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2'), c') -------------*)
1.189 val denom =
1.190 if c = [(1, replicate (length vs) 0)]
1.191 - then HOLogic.mk_binop "Groups.times_class.times" (d1', d2')
1.192 + then HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2')
1.193 else
1.194 - HOLogic.mk_binop "Groups.times_class.times" (c',
1.195 - HOLogic.mk_binop "Groups.times_class.times" (d1', d2')) (*--------------*)
1.196 + HOLogic.mk_binop \<^const_name>\<open>times\<close> (c',
1.197 + HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2')) (*--------------*)
1.198 val t' =
1.199 - HOLogic.mk_binop "Groups.plus_class.plus"
1.200 - (HOLogic.mk_binop "Rings.divide_class.divide"
1.201 - (HOLogic.mk_binop "Groups.times_class.times" (n1, d2'), denom),
1.202 - HOLogic.mk_binop "Rings.divide_class.divide"
1.203 - (HOLogic.mk_binop "Groups.times_class.times" (n2, d1'), denom))
1.204 + HOLogic.mk_binop \<^const_name>\<open>plus\<close>
1.205 + (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
1.206 + (HOLogic.mk_binop \<^const_name>\<open>times\<close> (n1, d2'), denom),
1.207 + HOLogic.mk_binop \<^const_name>\<open>divide\<close>
1.208 + (HOLogic.mk_binop \<^const_name>\<open>times\<close> (n2, d1'), denom))
1.209 val asm = mk_asms baseT [d1', d2', c']
1.210 in SOME (t', asm) end
1.211 | _ => NONE : (term * term list) option
1.212 @@ -378,7 +378,7 @@
1.213 val nomin = term_of_poly baseT expT vs
1.214 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))
1.215 val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
1.216 - val t' = HOLogic.mk_binop "Rings.divide_class.divide" (nomin, denom)
1.217 + val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom)
1.218 in SOME (t', mk_asms baseT [denom]) end
1.219 | _ => NONE : (term * term list) option
1.220 end
1.221 @@ -513,10 +513,10 @@
1.222 rew_ord=("ord_make_polynomial", ord_make_polynomial false \<^theory>),
1.223 erls = rational_erls,
1.224 calc =
1.225 - [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1.226 - ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
1.227 - ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
1.228 - ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
1.229 + [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
1.230 + ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
1.231 + ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
1.232 + ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
1.233 errpatts = [],
1.234 scr =
1.235 Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro,
1.236 @@ -580,10 +580,10 @@
1.237 Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
1.238 rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
1.239 erls = rational_erls,
1.240 - calc = [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1.241 - ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
1.242 - ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
1.243 - ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
1.244 + calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
1.245 + ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
1.246 + ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
1.247 + ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
1.248 errpatts = [],
1.249 scr = Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro,
1.250 normal_form = add_fraction_p_ \<^theory>,