1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Aug 02 15:30:41 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Aug 03 19:16:27 2021 +0200
     1.3 @@ -121,7 +121,9 @@
     1.4  subsection \<open>Conversion term <--> poly\<close>
     1.5  subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close>
     1.6  ML \<open>
     1.7 -fun monom_of_term vs (c, es) (t as Const _) =
     1.8 +fun monom_of_term vs (_, es) (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
     1.9 +    (0, list_update es (find_index (curry op = t) vs) 1)
    1.10 +  | monom_of_term vs (c, es) (t as Const _) =
    1.11      (c, list_update es (find_index (curry op = t) vs) 1)
    1.12    | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
    1.13      (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
    1.14 @@ -129,10 +131,10 @@
    1.15      (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
    1.16    | monom_of_term  vs (c, es) (t as Free _) =
    1.17      (c, list_update es (find_index (curry op = t) vs) 1)
    1.18 -  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ (b as Free _) $
    1.19 +  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (b as Free _) $
    1.20        (e as Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
    1.21      (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
    1.22 -  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ (b as Free _) $
    1.23 +  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (b as Free _) $
    1.24        (e as Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
    1.25      (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
    1.26  
    1.27 @@ -142,7 +144,9 @@
    1.28    | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
    1.29  
    1.30  (*-------v------*)
    1.31 -fun monoms_of_term vs (t as Const _) =
    1.32 +fun monoms_of_term vs (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
    1.33 +    [monom_of_term  vs (0, replicate (length vs) 0) t]
    1.34 +  | monoms_of_term vs (t as Const _) =
    1.35      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.36    | monoms_of_term vs (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) =
    1.37      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.38 @@ -171,7 +175,7 @@
    1.39  fun poly_of_term vs (t as Const (\<^const_name>\<open>plus\<close>, _) $ _ $ _) =
    1.40      (SOME (t |> monoms_of_term vs |> order)
    1.41        handle ERROR _ => NONE)
    1.42 -  | poly_of_term vs t =
    1.43 +  | poly_of_term vs t =   (* 0 for zero polynomial *)
    1.44      (SOME [monom_of_term vs (1, replicate (length vs) 0) t]
    1.45        handle ERROR _ => NONE)
    1.46  
    1.47 @@ -271,7 +275,7 @@
    1.48  subsubsection \<open>Cancel a fraction\<close>
    1.49  ML \<open>
    1.50  (* cancel a term by the gcd ("" denote terms with internal algebraic structure)
    1.51 -  cancel_p_ :: theory \<Rightarrow> term  \<Rightarrow> (term \<times> term list) option
    1.52 +  cancel_p_ : theory \<Rightarrow> term  \<Rightarrow> (term \<times> term list) option
    1.53    cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])
    1.54    assumes: a is_polynomial  \<and>  b is_polynomial  \<and>  b \<noteq> 0
    1.55    yields
    1.56 @@ -324,7 +328,7 @@
    1.57      (Const (\<^const_name>\<open>plus\<close>, _) $ 
    1.58        nofrac $ 
    1.59        (Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
    1.60 -    = SOME ((nofrac, Free ("1", HOLogic.realT)), (n2, d2))
    1.61 +    = SOME ((nofrac, HOLogic.mk_number HOLogic.realT 1), (n2, d2))
    1.62    | check_frac_sum 
    1.63      (Const (\<^const_name>\<open>plus\<close>, _) $ 
    1.64        (Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $ 
    1.65 @@ -375,7 +379,8 @@
    1.66  ML \<open>
    1.67  (* add fractions
    1.68    assumes: is a term with outmost "+" and at least one outmost "/" in respective summands
    1.69 -  NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*)
    1.70 +  \<and> NONE of the summands is zero.
    1.71 +  NOTE: the case "(_ + _) + _" need not be considered due to iterated addition *)
    1.72  fun add_fraction_p_ (_: theory) t =
    1.73    case check_frac_sum t of 
    1.74      NONE => NONE