1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Wed Apr 15 11:11:54 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Wed Apr 15 11:37:43 2020 +0200
1.3 @@ -58,7 +58,7 @@
1.4 ML \<open>
1.5 \<close> ML \<open>
1.6 val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty
1.7 - [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.8 + [ Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.9 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.10 (*"(~ True) = False"*)
1.11 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
1.12 @@ -79,18 +79,18 @@
1.13 Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
1.14 Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
1.15
1.16 - Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.17 - Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.18 + Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.19 + Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.20
1.21 - Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.22 - Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
1.23 - Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
1.24 - Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
1.25 + Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.26 + Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
1.27 + Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
1.28 + Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
1.29 \<close>
1.30
1.31 ML \<open>
1.32 val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty
1.33 - [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.34 + [ Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.35 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.36 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
1.37 Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
1.38 @@ -105,27 +105,27 @@
1.39 Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
1.40 Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
1.41
1.42 - Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.43 - Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.44 + Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.45 + Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.46
1.47 - Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.48 - Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
1.49 - Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
1.50 - Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
1.51 + Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.52 + Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
1.53 + Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
1.54 + Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
1.55 \<close>
1.56
1.57 subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
1.58 text \<open>requires "eval_binop" from above\<close>
1.59 ML \<open>
1.60 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr
1.61 - [ Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.62 - Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.63 - Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.64 - Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.65 - Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.66 - Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
1.67 + [ Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.68 + Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.69 + Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.70 + Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.71 + Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.72 + Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
1.73
1.74 - Rule.Num_Calc ("Prog_Expr.Vars",Prog_Expr.eval_var "#Vars_"),
1.75 + Rule.Eval ("Prog_Expr.Vars",Prog_Expr.eval_var "#Vars_"),
1.76
1.77 Rule.Thm ("if_True",ThmC.numerals_to_Free @{thm if_True}),
1.78 Rule.Thm ("if_False",ThmC.numerals_to_Free @{thm if_False})];
1.79 @@ -134,12 +134,12 @@
1.80 (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
1.81 erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
1.82 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.83 - rules = [Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.84 - Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
1.85 + rules = [Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.86 + Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
1.87 (* ~~~~~~ for nth_Cons_*)],
1.88 - scr = Rule.EmptyScr},
1.89 + scr = Rule.Empty_Prog},
1.90 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.91 - rules = [], scr = Rule.EmptyScr})
1.92 + rules = [], scr = Rule.Empty_Prog})
1.93 prog_expr);
1.94 \<close>
1.95 subsection \<open>setup for extended rule-set\<close>