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