1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Thu Aug 29 13:52:47 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Tue Sep 03 12:40:27 2019 +0200
1.3 @@ -20,21 +20,21 @@
1.4 subsection \<open>setup for ML-functions\<close>
1.5 text \<open>required by "eval_binop" below\<close>
1.6 setup \<open>KEStore_Elems.add_calcs
1.7 - [ ("occurs_in", ("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
1.8 - ("some_occur_in", ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
1.9 - ("is_atom", ("Atools.is'_atom", eval_is_atom "#is_atom_")),
1.10 - ("is_even", ("Atools.is'_even", eval_is_even "#is_even_")),
1.11 - ("is_const", ("Atools.is'_const", eval_const "#is_const_")),
1.12 - ("le", ("Orderings.ord_class.less", eval_equ "#less_")),
1.13 - ("leq", ("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),
1.14 - ("ident", ("Atools.ident", eval_ident "#ident_")),
1.15 - ("equal", ("HOL.eq", eval_equal "#equal_")),
1.16 - ("PLUS", ("Groups.plus_class.plus", eval_binop "#add_")),
1.17 - ("MINUS", ("Groups.minus_class.minus", eval_binop "#sub_")),
1.18 - ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")),
1.19 - ("DIVIDE", ("Rings.divide_class.divide", eval_cancel "#divide_e")),
1.20 - ("POWER",("Atools.pow", eval_binop "#power_")),
1.21 - ("boollist2sum", ("Atools.boollist2sum", eval_boollist2sum ""))]\<close>
1.22 + [ ("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_")),
1.23 + ("some_occur_in", ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_")),
1.24 + ("is_atom", ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_")),
1.25 + ("is_even", ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_")),
1.26 + ("is_const", ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")),
1.27 + ("le", ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")),
1.28 + ("leq", ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_")),
1.29 + ("ident", ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")),
1.30 + ("equal", ("HOL.eq", Prog_Expr.eval_equal "#equal_")),
1.31 + ("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1.32 + ("MINUS", ("Groups.minus_class.minus", (**)eval_binop "#sub_")),
1.33 + ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
1.34 + ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
1.35 + ("POWER",("Prog_Expr.pow", (**)eval_binop "#power_")),
1.36 + ("boollist2sum", ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum ""))]\<close>
1.37
1.38 subsection \<open>rewrite-order for rule-sets\<close>
1.39 ML \<open>
1.40 @@ -58,7 +58,7 @@
1.41 ML \<open>
1.42 \<close> ML \<open>
1.43 val Atools_erls = Rule.append_rls "Atools_erls" Rule.e_rls
1.44 - [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
1.45 + [ Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.46 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.47 (*"(~ True) = False"*)
1.48 Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
1.49 @@ -79,18 +79,18 @@
1.50 Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
1.51 Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
1.52
1.53 - Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
1.54 - Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
1.55 + Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.56 + Rule.Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.57
1.58 - Rule.Calc ("Atools.ident", eval_ident "#ident_"),
1.59 - Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
1.60 - Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),
1.61 - Rule.Calc ("Tools.matches", Tools.eval_matches "")];
1.62 + Rule.Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.63 + Rule.Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
1.64 + Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
1.65 + Rule.Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
1.66 \<close>
1.67
1.68 ML \<open>
1.69 val Atools_crls = Rule.append_rls "Atools_crls" Rule.e_rls
1.70 - [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
1.71 + [ Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.72 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.73 Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
1.74 Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
1.75 @@ -105,27 +105,27 @@
1.76 Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
1.77 Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
1.78
1.79 - Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
1.80 - Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
1.81 + Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.82 + Rule.Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.83
1.84 - Rule.Calc ("Atools.ident", eval_ident "#ident_"),
1.85 - Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
1.86 - Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),
1.87 - Rule.Calc ("Tools.matches", Tools.eval_matches "")];
1.88 + Rule.Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.89 + Rule.Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
1.90 + Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
1.91 + Rule.Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
1.92 \<close>
1.93
1.94 subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
1.95 text \<open>requires "eval_binop" from above\<close>
1.96 ML \<open>
1.97 val list_rls = Rule.append_rls "list_rls" list_rls
1.98 - [ Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.99 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.100 - Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.101 - Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
1.102 - Rule.Calc ("Atools.ident",eval_ident "#ident_"),
1.103 - Rule.Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
1.104 + [ Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.105 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.106 + Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.107 + Rule.Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
1.108 + Rule.Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.109 + Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
1.110
1.111 - Rule.Calc ("Tools.Vars",Tools.eval_var "#Vars_"),
1.112 + Rule.Calc ("Prog_Expr.Vars",Prog_Expr.eval_var "#Vars_"),
1.113
1.114 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
1.115 Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
1.116 @@ -134,8 +134,8 @@
1.117 (Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
1.118 erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
1.119 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
1.120 - rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.121 - Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")
1.122 + rules = [Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.123 + Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
1.124 (* ~~~~~~ for nth_Cons_*)],
1.125 scr = Rule.EmptyScr},
1.126 srls = Rule.Erls, calc = [], errpatts = [],