1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sun Jul 18 21:19:25 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Jul 19 15:34:54 2021 +0200
1.3 @@ -41,7 +41,7 @@
1.4
1.5 (*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
1.6 fun eval_is_ratpolyexp (thmid:string) _
1.7 - (t as (Const("Rational.is_ratpolyexp", _) $ arg)) thy =
1.8 + (t as (Const (\<^const_name>\<open>Rational.is_ratpolyexp\<close>, _) $ arg)) thy =
1.9 if is_ratpolyexp arg
1.10 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
1.11 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.12 @@ -51,7 +51,7 @@
1.13
1.14 (*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
1.15 fun eval_get_denominator (thmid:string) _
1.16 - (t as Const ("Rational.get_denominator", _) $
1.17 + (t as Const (\<^const_name>\<open>Rational.get_denominator\<close>, _) $
1.18 (Const (\<^const_name>\<open>divide\<close>, _) $ _(*num*) $
1.19 denom)) thy =
1.20 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "",
1.21 @@ -60,7 +60,7 @@
1.22
1.23 (*("get_numerator", ("Rational.get_numerator", eval_get_numerator ""))*)
1.24 fun eval_get_numerator (thmid:string) _
1.25 - (t as Const ("Rational.get_numerator", _) $
1.26 + (t as Const (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
1.27 (Const (\<^const_name>\<open>divide\<close>, _) $num
1.28 $denom )) thy =
1.29 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "",
1.30 @@ -123,17 +123,17 @@
1.31 ML \<open>
1.32 fun monom_of_term vs (c, es) (t as Const _) =
1.33 (c, list_update es (find_index (curry op = t) vs) 1)
1.34 - | monom_of_term _ (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
1.35 + | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
1.36 (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
1.37 - | monom_of_term _ (c, es) (t as (Const ("Groups.uminus_class.uminus", _) $ _)) =
1.38 + | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
1.39 (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
1.40 | monom_of_term vs (c, es) (t as Free _) =
1.41 (c, list_update es (find_index (curry op = t) vs) 1)
1.42 - | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
1.43 - (e as Const ("Num.numeral_class.numeral", _) $ _)) =
1.44 + | monom_of_term vs (c, es) (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ (b as Free _) $
1.45 + (e as Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
1.46 (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
1.47 - | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
1.48 - (e as Const ("Groups.uminus_class.uminus", _) $ _)) =
1.49 + | monom_of_term vs (c, es) (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ (b as Free _) $
1.50 + (e as Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
1.51 (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
1.52
1.53 | monom_of_term vs (c, es) (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2) =
1.54 @@ -144,9 +144,9 @@
1.55 (*-------v------*)
1.56 fun monoms_of_term vs (t as Const _) =
1.57 [monom_of_term vs (1, replicate (length vs) 0) t]
1.58 - | monoms_of_term vs (t as Const ("Num.numeral_class.numeral", _) $ _) =
1.59 + | monoms_of_term vs (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) =
1.60 [monom_of_term vs (1, replicate (length vs) 0) t]
1.61 - | monoms_of_term vs (t as Const ("Groups.uminus_class.uminus", _) $ _) =
1.62 + | monoms_of_term vs (t as Const (\<^const_name>\<open>uminus\<close>, _) $ _) =
1.63 [monom_of_term vs (1, replicate (length vs) 0) t]
1.64 | monoms_of_term vs (t as Free _) =
1.65 [monom_of_term vs (1, replicate (length vs) 0) t]
1.66 @@ -191,7 +191,7 @@
1.67 | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
1.68 | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
1.69 | term_of_es baseT expT (v :: vs) (e :: es) =
1.70 - Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
1.71 + Const (\<^const_name>\<open>Transcendental.powr\<close>, [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
1.72 :: term_of_es baseT expT vs es
1.73 | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
1.74
1.75 @@ -215,8 +215,8 @@
1.76 subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
1.77 ML \<open>
1.78 fun mk_noteq_0 baseT t =
1.79 - Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $
1.80 - (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
1.81 + Const (\<^const_name>\<open>Not\<close>, HOLogic.boolT --> HOLogic.boolT) $
1.82 + (Const (\<^const_name>\<open>HOL.eq\<close>, [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
1.83
1.84 fun mk_asms baseT ts =
1.85 let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
1.86 @@ -464,7 +464,7 @@
1.87
1.88 (*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
1.89 fun eval_is_expanded (thmid:string) _
1.90 - (t as (Const("Rational.is_expanded", _) $ arg)) thy =
1.91 + (t as (Const (\<^const_name>\<open>Rational.is_expanded\<close>, _) $ arg)) thy =
1.92 if is_expanded arg
1.93 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
1.94 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))