1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Mon Aug 09 14:20:20 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Tue Aug 10 09:43:07 2021 +0200
1.3 @@ -62,86 +62,80 @@
1.4 subsection \<open>rule-sets\<close>
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 -val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty
1.8 - [ \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.9 - \<^rule_thm>\<open>not_true\<close>,
1.10 - (*"(~ True) = False"*)
1.11 - \<^rule_thm>\<open>not_false\<close>,
1.12 - (*"(~ False) = True"*)
1.13 - \<^rule_thm>\<open>and_true\<close>,
1.14 - (*"(?a & True) = ?a"*)
1.15 - \<^rule_thm>\<open>and_false\<close>,
1.16 - (*"(?a & False) = False"*)
1.17 - \<^rule_thm>\<open>or_true\<close>,
1.18 - (*"(?a | True) = True"*)
1.19 - \<^rule_thm>\<open>or_false\<close>,
1.20 - (*"(?a | False) = ?a"*)
1.21 -
1.22 - \<^rule_thm>\<open>rat_leq1\<close>,
1.23 - \<^rule_thm>\<open>rat_leq2\<close>,
1.24 - \<^rule_thm>\<open>rat_leq3\<close>,
1.25 - \<^rule_thm>\<open>refl\<close>,
1.26 - \<^rule_thm>\<open>order_refl\<close>,
1.27 - \<^rule_thm>\<open>radd_left_cancel_le\<close>,
1.28 -
1.29 - \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.30 - \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.31 -
1.32 - \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.33 - \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
1.34 - \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
1.35 - \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
1.36 +val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty [
1.37 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.38 + \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
1.39 + \<^rule_thm>\<open>not_false\<close>, (*"(~ False) = True"*)
1.40 + \<^rule_thm>\<open>and_true\<close>, (*"(?a & True) = ?a"*)
1.41 + \<^rule_thm>\<open>and_false\<close>, (*"(?a & False) = False"*)
1.42 + \<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*)
1.43 + \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
1.44 +
1.45 + \<^rule_thm>\<open>rat_leq1\<close>,
1.46 + \<^rule_thm>\<open>rat_leq2\<close>,
1.47 + \<^rule_thm>\<open>rat_leq3\<close>,
1.48 + \<^rule_thm>\<open>refl\<close>,
1.49 + \<^rule_thm>\<open>order_refl\<close>,
1.50 + \<^rule_thm>\<open>radd_left_cancel_le\<close>,
1.51 +
1.52 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.53 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.54 +
1.55 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.56 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
1.57 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
1.58 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
1.59 \<close>
1.60
1.61 ML \<open>
1.62 -val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty
1.63 - [ \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.64 - \<^rule_thm>\<open>not_true\<close>,
1.65 - \<^rule_thm>\<open>not_false\<close>,
1.66 - \<^rule_thm>\<open>and_true\<close>,
1.67 - \<^rule_thm>\<open>and_false\<close>,
1.68 - \<^rule_thm>\<open>or_true\<close>,
1.69 - \<^rule_thm>\<open>or_false\<close>,
1.70 -
1.71 - \<^rule_thm>\<open>rat_leq1\<close>,
1.72 - \<^rule_thm>\<open>rat_leq2\<close>,
1.73 - \<^rule_thm>\<open>rat_leq3\<close>,
1.74 - \<^rule_thm>\<open>refl\<close>,
1.75 - \<^rule_thm>\<open>order_refl\<close>,
1.76 - \<^rule_thm>\<open>radd_left_cancel_le\<close>,
1.77 -
1.78 - \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.79 - \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.80 -
1.81 - \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.82 - \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
1.83 - \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
1.84 - \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
1.85 +val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty [
1.86 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.87 + \<^rule_thm>\<open>not_true\<close>,
1.88 + \<^rule_thm>\<open>not_false\<close>,
1.89 + \<^rule_thm>\<open>and_true\<close>,
1.90 + \<^rule_thm>\<open>and_false\<close>,
1.91 + \<^rule_thm>\<open>or_true\<close>,
1.92 + \<^rule_thm>\<open>or_false\<close>,
1.93 +
1.94 + \<^rule_thm>\<open>rat_leq1\<close>,
1.95 + \<^rule_thm>\<open>rat_leq2\<close>,
1.96 + \<^rule_thm>\<open>rat_leq3\<close>,
1.97 + \<^rule_thm>\<open>refl\<close>,
1.98 + \<^rule_thm>\<open>order_refl\<close>,
1.99 + \<^rule_thm>\<open>radd_left_cancel_le\<close>,
1.100 +
1.101 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.102 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.103 +
1.104 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.105 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
1.106 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
1.107 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
1.108 \<close>
1.109
1.110 subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
1.111 text \<open>requires "eval_binop" from above\<close>
1.112 ML \<open>
1.113 -val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr
1.114 - [ \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.115 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.116 - \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.117 - \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.118 - \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.119 - \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
1.120 -
1.121 - \<^rule_eval>\<open>Prog_Expr.Vars\<close> (Prog_Expr.eval_var "#Vars_"),
1.122 -
1.123 - \<^rule_thm>\<open>if_True\<close>,
1.124 - \<^rule_thm>\<open>if_False\<close>];
1.125 +val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [
1.126 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.127 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.128 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.129 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.130 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.131 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
1.132 +
1.133 + \<^rule_eval>\<open>Prog_Expr.Vars\<close> (Prog_Expr.eval_var "#Vars_"),
1.134 +
1.135 + \<^rule_thm>\<open>if_True\<close>,
1.136 + \<^rule_thm>\<open>if_False\<close>];
1.137
1.138 val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge "list_erls"
1.139 (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
1.140 erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
1.141 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.142 - rules = [\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.143 - \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_")
1.144 - (* ~~~~~~ for nth_Cons_*)],
1.145 + rules = [
1.146 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.147 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_") (*..for nth_Cons_*)],
1.148 scr = Rule.Empty_Prog},
1.149 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.150 rules = [], scr = Rule.Empty_Prog})