Isar command 'calculation' as front-end for KEStore_Elems.add_calcs, without change of semantics;
2 imports Interpret.Interpret
3 (** )"../BridgeJEdit/BridgeJEdit" ( *activate after devel.of BridgeJEdit*)
4 (**) "../BridgeLibisabelle/BridgeLibisabelle" (*remove after devel.of BridgeJEdit*)
5 (* ^^^ for KEStore_Elems.add_thes *)
7 subsection \<open>theorems for Base_Tools\<close>
9 lemma real_unari_minus: "- a = (-1) * (a::real)" by auto
10 (*Semiring_Normalization.comm_ring_1_class.ring_normalization_rules(1)*)
12 (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
13 lemma radd_left_cancel_le: "((k::real) + m \<le> k + n) = (m \<le> n)" by auto
14 (*Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left*)
16 thm "Fields.linordered_field_class.mult_imp_le_div_pos" (*0 < ?y \<Longrightarrow> ?z * ?y \<le> ?x \<Longrightarrow> ?z \<le> ?x / ?y*)
18 axiomatization where (*for evaluating the assumptions of conditional rules*)
19 (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
20 rat_leq1: "0 \<noteq> b \<Longrightarrow> 0 \<noteq> d \<Longrightarrow> (a / b \<le> c / d) = (a * d \<le> b * c)"(*Quickcheck found a counterexample*) and
21 rat_leq2: "0 \<noteq> d \<Longrightarrow> (a \<le> c / d) = (a * d \<le> c)"(*Quickcheck found a counterexample*) and
22 rat_leq3: "0 \<noteq> b \<Longrightarrow> (a / b \<le> c ) = (a \<le> b * c)"(*Quickcheck found a counterexample*)
25 subsection \<open>setup for ML-functions\<close>
26 text \<open>required by "eval_binop" below\<close>
27 calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>
28 calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
29 calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
30 calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close>
31 calculation is_const = \<open>Prog_Expr.eval_const "#is_const_"\<close>
32 calculation le (less) = \<open>Prog_Expr.eval_equ "#less_"\<close>
33 calculation leq (less_eq) = \<open>Prog_Expr.eval_equ "#less_equal_"\<close>
34 calculation ident = \<open>Prog_Expr.eval_ident "#ident_"\<close>
35 calculation equal (HOL.eq) = \<open>Prog_Expr.eval_equal "#equal_"\<close>
36 calculation PLUS (plus) = \<open>(**)eval_binop "#add_"\<close>
37 calculation MINUS (minus) = \<open>(**)eval_binop "#sub_"\<close>
38 calculation TIMES (times) = \<open>(**)eval_binop "#mult_"\<close>
39 calculation DIVIDE (divide) = \<open>Prog_Expr.eval_cancel "#divide_e"\<close>
40 calculation POWER (powr) = \<open>(**)eval_binop "#power_"\<close>
41 calculation boollist2sum = \<open>Prog_Expr.eval_boollist2sum ""\<close>
43 subsection \<open>rewrite-order for rule-sets\<close>
49 fun termlessI (_: subst) uv = LibraryC.termless uv;
50 fun term_ordI (_: subst) uv = Term_Ord.term_ord uv;
53 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
54 val tless_true = Rewrite_Ord.dummy_ord;
55 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx here, too*)
56 [("tless_true", tless_true),
57 ("e_rew_ord'", tless_true),
58 ("dummy_ord", Rewrite_Ord.dummy_ord)]);
61 subsection \<open>rule-sets\<close>
64 val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty
65 [ \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
66 \<^rule_thm>\<open>not_true\<close>,
67 (*"(~ True) = False"*)
68 \<^rule_thm>\<open>not_false\<close>,
69 (*"(~ False) = True"*)
70 \<^rule_thm>\<open>and_true\<close>,
71 (*"(?a & True) = ?a"*)
72 \<^rule_thm>\<open>and_false\<close>,
73 (*"(?a & False) = False"*)
74 \<^rule_thm>\<open>or_true\<close>,
75 (*"(?a | True) = True"*)
76 \<^rule_thm>\<open>or_false\<close>,
77 (*"(?a | False) = ?a"*)
79 \<^rule_thm>\<open>rat_leq1\<close>,
80 \<^rule_thm>\<open>rat_leq2\<close>,
81 \<^rule_thm>\<open>rat_leq3\<close>,
82 \<^rule_thm>\<open>refl\<close>,
83 \<^rule_thm>\<open>order_refl\<close>,
84 \<^rule_thm>\<open>radd_left_cancel_le\<close>,
86 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
87 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
89 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
90 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
91 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
92 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
96 val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty
97 [ \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
98 \<^rule_thm>\<open>not_true\<close>,
99 \<^rule_thm>\<open>not_false\<close>,
100 \<^rule_thm>\<open>and_true\<close>,
101 \<^rule_thm>\<open>and_false\<close>,
102 \<^rule_thm>\<open>or_true\<close>,
103 \<^rule_thm>\<open>or_false\<close>,
105 \<^rule_thm>\<open>rat_leq1\<close>,
106 \<^rule_thm>\<open>rat_leq2\<close>,
107 \<^rule_thm>\<open>rat_leq3\<close>,
108 \<^rule_thm>\<open>refl\<close>,
109 \<^rule_thm>\<open>order_refl\<close>,
110 \<^rule_thm>\<open>radd_left_cancel_le\<close>,
112 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
113 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
115 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
116 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
117 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
118 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
121 subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
122 text \<open>requires "eval_binop" from above\<close>
124 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr
125 [ \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
126 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
127 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
128 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
129 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
130 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
132 \<^rule_eval>\<open>Prog_Expr.Vars\<close> (Prog_Expr.eval_var "#Vars_"),
134 \<^rule_thm>\<open>if_True\<close>,
135 \<^rule_thm>\<open>if_False\<close>];
137 val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge "list_erls"
138 (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
139 erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
140 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
141 rules = [\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
142 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_")
143 (* ~~~~~~ for nth_Cons_*)],
144 scr = Rule.Empty_Prog},
145 srls = Rule_Set.Empty, calc = [], errpatts = [],
146 rules = [], scr = Rule.Empty_Prog})
150 subsection \<open>setup for extended rule-set\<close>
152 rule_set_knowledge prog_expr = \<open>Auto_Prog.prep_rls @{theory} prog_expr\<close>