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