1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri May 07 13:23:24 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri May 07 18:12:51 2021 +0200
1.3 @@ -14,8 +14,8 @@
1.4 section \<open>Constants for evaluation by "Rule.Eval"\<close>
1.5 consts
1.6
1.7 - is'_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
1.8 - is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp")
1.9 + is_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
1.10 + is_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp")
1.11 get_denominator :: "real => real"
1.12 get_numerator :: "real => real"
1.13
1.14 @@ -39,9 +39,9 @@
1.15 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
1.16 | is_ratpolyexp _ = false;
1.17
1.18 -(*("is_ratpolyexp", ("Rational.is'_ratpolyexp", eval_is_ratpolyexp ""))*)
1.19 +(*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
1.20 fun eval_is_ratpolyexp (thmid:string) _
1.21 - (t as (Const("Rational.is'_ratpolyexp", _) $ arg)) thy =
1.22 + (t as (Const("Rational.is_ratpolyexp", _) $ arg)) thy =
1.23 if is_ratpolyexp arg
1.24 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
1.25 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.26 @@ -395,7 +395,7 @@
1.27 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.28 rules =
1.29 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.30 - Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
1.31 + Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
1.32 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.33 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
1.34 scr = Rule.Empty_Prog});
1.35 @@ -448,9 +448,9 @@
1.36 scr = Rule.Empty_Prog})
1.37 calculate_Poly);
1.38
1.39 -(*("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))*)
1.40 +(*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
1.41 fun eval_is_expanded (thmid:string) _
1.42 - (t as (Const("Rational.is'_expanded", _) $ arg)) thy =
1.43 + (t as (Const("Rational.is_expanded", _) $ arg)) thy =
1.44 if is_expanded arg
1.45 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
1.46 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.47 @@ -459,12 +459,12 @@
1.48 | eval_is_expanded _ _ _ _ = NONE;
1.49 \<close>
1.50 setup \<open>KEStore_Elems.add_calcs
1.51 - [("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))]\<close>
1.52 + [("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))]\<close>
1.53 ML \<open>
1.54 val rational_erls =
1.55 Rule_Set.merge "rational_erls" calculate_Rational
1.56 (Rule_Set.append_rules "is_expanded" Atools_erls
1.57 - [Rule.Eval ("Rational.is'_expanded", eval_is_expanded "")]);
1.58 + [Rule.Eval ("Rational.is_expanded", eval_is_expanded "")]);
1.59 \<close>
1.60
1.61 subsection \<open>Embed cancellation into rewriting\<close>
1.62 @@ -604,8 +604,8 @@
1.63 val powers_erls = prep_rls'(
1.64 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.65 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.66 - rules = [Rule.Eval ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"),
1.67 - Rule.Eval ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_"),
1.68 + rules = [Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
1.69 + Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"),
1.70 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.71 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
1.72 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.73 @@ -706,7 +706,7 @@
1.74 val norm_rat_erls = prep_rls'(
1.75 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.76 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.77 - rules = [Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")
1.78 + rules = [Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")
1.79 ], scr = Rule.Empty_Prog});
1.80
1.81 (* consists of rls containing the absolute minimum of thms *)
1.82 @@ -778,7 +778,7 @@
1.83 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
1.84 val rat_mult_poly = prep_rls'(
1.85 Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.86 - erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
1.87 + erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
1.88 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.89 rules =
1.90 [Rule.Thm ("rat_mult_poly_l",ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
1.91 @@ -913,9 +913,10 @@
1.92 ("#Find" ,["normalform n_n"])],
1.93 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.94 prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty
1.95 - [(*for preds in where_*) Rule.Eval ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
1.96 + [(*for preds in where_*) Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")],
1.97 crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls},
1.98 @{thm simplify.simps})]
1.99 +\<close> ML \<open>
1.100 +\<close> ML \<open>
1.101 \<close>
1.102 -
1.103 end