1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Jun 21 22:08:01 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sun Jul 18 18:15:27 2021 +0200
1.3 @@ -123,19 +123,31 @@
1.4 ML \<open>
1.5 fun monom_of_term vs (c, es) (t as Const _) =
1.6 (c, list_update es (find_index (curry op = t) vs) 1)
1.7 - | monom_of_term vs (c, es) (t as Free (id, _)) =
1.8 - if TermC.is_num' id
1.9 - then (id |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
1.10 - else (c, list_update es (find_index (curry op = t) vs) 1)
1.11 - | monom_of_term vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (t as Free _) $ Free (e, _)) =
1.12 - (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_opt_of_string e)))
1.13 + | monom_of_term _ (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
1.14 + (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
1.15 + | monom_of_term _ (c, es) (t as (Const ("Groups.uminus_class.uminus", _) $ _)) =
1.16 + (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
1.17 + | monom_of_term vs (c, es) (t as Free _) =
1.18 + (c, list_update es (find_index (curry op = t) vs) 1)
1.19 + | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
1.20 + (e as Const ("Num.numeral_class.numeral", _) $ _)) =
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 ("Transcendental.powr", _) $ (b as Free _) $
1.23 + (e as Const ("Groups.uminus_class.uminus", _) $ _)) =
1.24 + (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
1.25 +
1.26 | monom_of_term vs (c, es) (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2) =
1.27 let val (c', es') = monom_of_term vs (c, es) m1
1.28 in monom_of_term vs (c', es') m2 end
1.29 | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
1.30
1.31 +(*-------v------*)
1.32 fun monoms_of_term vs (t as Const _) =
1.33 [monom_of_term vs (1, replicate (length vs) 0) t]
1.34 + | monoms_of_term vs (t as Const ("Num.numeral_class.numeral", _) $ _) =
1.35 + [monom_of_term vs (1, replicate (length vs) 0) t]
1.36 + | monoms_of_term vs (t as Const ("Groups.uminus_class.uminus", _) $ _) =
1.37 + [monom_of_term vs (1, replicate (length vs) 0) t]
1.38 | monoms_of_term vs (t as Free _) =
1.39 [monom_of_term vs (1, replicate (length vs) 0) t]
1.40 | monoms_of_term vs (t as Const (\<^const_name>\<open>powr\<close>, _) $ _ $ _) =
1.41 @@ -179,7 +191,7 @@
1.42 | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
1.43 | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
1.44 | term_of_es baseT expT (v :: vs) (e :: es) =
1.45 - Const (\<^const_name>\<open>powr\<close>, [baseT, expT] ---> baseT) $ v $ (Free (TermC.isastr_of_int e, expT))
1.46 + Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
1.47 :: term_of_es baseT expT vs es
1.48 | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
1.49
1.50 @@ -189,9 +201,10 @@
1.51 if c = 1
1.52 then
1.53 if es' = [] (*if es = [0,0,0,...]*)
1.54 - then Free (TermC.isastr_of_int c, baseT)
1.55 - else foldl (HOLogic.mk_binop \<^const_name>\<open>times\<close>) (hd es', tl es')
1.56 - else foldl (HOLogic.mk_binop \<^const_name>\<open>times\<close>) (Free (TermC.isastr_of_int c, baseT), es')
1.57 + then HOLogic.mk_number baseT c
1.58 + else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')
1.59 + else foldl (HOLogic.mk_binop "Groups.times_class.times")
1.60 + (HOLogic.mk_number baseT c, es')
1.61 end
1.62
1.63 fun term_of_poly baseT expT vs p =
1.64 @@ -202,8 +215,8 @@
1.65 subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
1.66 ML \<open>
1.67 fun mk_noteq_0 baseT t =
1.68 - Const (\<^const_name>\<open>Not\<close>, HOLogic.boolT --> HOLogic.boolT) $
1.69 - (Const (\<^const_name>\<open>HOL.eq\<close>, [baseT, baseT] ---> HOLogic.boolT) $ t $ Free ("0", HOLogic.realT))
1.70 + Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $
1.71 + (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
1.72
1.73 fun mk_asms baseT ts =
1.74 let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
1.75 @@ -316,7 +329,7 @@
1.76 (Const (\<^const_name>\<open>plus\<close>, _) $
1.77 (Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $
1.78 nofrac)
1.79 - = SOME ((n1, d1), (nofrac, Free ("1", HOLogic.realT)))
1.80 + = SOME ((n1, d1), (nofrac, HOLogic.mk_number HOLogic.realT 1))
1.81 | check_frac_sum _ = NONE
1.82
1.83 (* prepare a term for addition by providing the least common denominator as a product
1.84 @@ -394,10 +407,11 @@
1.85 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.86 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.87 rules =
1.88 - [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.89 - \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
1.90 - \<^rule_thm>\<open>not_true\<close>,
1.91 - \<^rule_thm>\<open>not_false\<close>],
1.92 + [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),
1.93 + Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.94 + Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
1.95 + Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.96 + Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
1.97 scr = Rule.Empty_Prog});
1.98
1.99 (* simplifies expressions with numerals;
1.100 @@ -599,19 +613,6 @@
1.101
1.102 section \<open>Rulesets for general simplification\<close>
1.103 ML \<open>
1.104 -(*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
1.105 -val powers_erls = prep_rls'(
1.106 - Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.107 - erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.108 - rules = [\<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
1.109 - \<^rule_eval>\<open>Prog_Expr.is_even\<close> (Prog_Expr.eval_is_even "#is_even_"),
1.110 - \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.111 - \<^rule_thm>\<open>not_false\<close>,
1.112 - \<^rule_thm>\<open>not_true\<close>,
1.113 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.114 - ],
1.115 - scr = Rule.Empty_Prog
1.116 - });
1.117 (*.all powers over + distributed; atoms over * collected, other distributed
1.118 contains absolute minimum of thms for context in norm_Rational .*)
1.119 val powers = prep_rls'(