1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Thu Jun 10 17:06:32 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Fri Jun 11 11:49:34 2021 +0200
1.3 @@ -63,7 +63,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.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.8 + [ \<^rule_eval>\<open>HOL.eq\<close> (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 @@ -84,18 +84,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.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.17 - Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.18 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.19 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.20
1.21 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.22 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
1.23 - Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
1.24 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
1.25 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.26 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
1.27 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
1.28 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (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.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.34 + [ \<^rule_eval>\<open>HOL.eq\<close> (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 @@ -110,27 +110,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.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.43 - Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.44 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.45 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.46
1.47 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.48 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
1.49 - Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
1.50 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
1.51 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.52 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
1.53 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
1.54 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (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.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.62 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.63 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.64 - Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.65 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.66 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
1.67 + [ \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.68 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.69 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.70 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.71 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.72 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
1.73
1.74 - Rule.Eval ("Prog_Expr.Vars",Prog_Expr.eval_var "#Vars_"),
1.75 + \<^rule_eval>\<open>Prog_Expr.Vars\<close> (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 @@ -139,8 +139,8 @@
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.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.84 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
1.85 + rules = [\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.86 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_")
1.87 (* ~~~~~~ for nth_Cons_*)],
1.88 scr = Rule.Empty_Prog},
1.89 srls = Rule_Set.Empty, calc = [], errpatts = [],