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: "Not (a is_const) ==> - a = (-1) * (a::real)" by auto
10 (*lemma real_unari_minus: "- a = (-1) * (a::real)" by auto LOOPS WITH NUMERALS*)
11 (*Semiring_Normalization.comm_ring_1_class.ring_normalization_rules(1)*)
13 (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
14 lemma radd_left_cancel_le: "((k::real) + m \<le> k + n) = (m \<le> n)" by auto
15 (*Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left*)
17 thm "Fields.linordered_field_class.mult_imp_le_div_pos" (*0 < ?y \<Longrightarrow> ?z * ?y \<le> ?x \<Longrightarrow> ?z \<le> ?x / ?y*)
19 axiomatization where (*for evaluating the assumptions of conditional rules*)
20 (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
21 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
22 rat_leq2: "0 \<noteq> d \<Longrightarrow> (a \<le> c / d) = (a * d \<le> c)"(*Quickcheck found a counterexample*) and
23 rat_leq3: "0 \<noteq> b \<Longrightarrow> (a / b \<le> c ) = (a \<le> b * c)"(*Quickcheck found a counterexample*)
26 subsection \<open>setup for ML-functions\<close>
27 text \<open>required by "eval_binop" below\<close>
28 setup \<open>KEStore_Elems.add_calcs
29 [ ("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "#occurs_in_")),
30 ("some_occur_in", ("Prog_Expr.some_occur_in", Prog_Expr.eval_some_occur_in "#some_occur_in_")),
31 ("is_atom", ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_")),
32 ("is_even", ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_")),
33 ("is_const", ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")),
34 ("le", ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")),
35 ("leq", ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_")),
36 ("ident", ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")),
37 ("equal", ("HOL.eq", Prog_Expr.eval_equal "#equal_")),
38 ("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
39 ("MINUS", ("Groups.minus_class.minus", (**)eval_binop "#sub_")),
40 ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
41 ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
42 ("POWER",("Transcendental.powr", (**)eval_binop "#power_")),
43 ("boollist2sum", ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum ""))]\<close>
45 subsection \<open>rewrite-order for rule-sets\<close>
51 fun termlessI (_: subst) uv = LibraryC.termless uv;
52 fun term_ordI (_: subst) uv = Term_Ord.term_ord uv;
55 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
56 val tless_true = Rewrite_Ord.dummy_ord;
57 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx here, too*)
58 [("tless_true", tless_true),
59 ("e_rew_ord'", tless_true),
60 ("dummy_ord", Rewrite_Ord.dummy_ord)]);
63 subsection \<open>rule-sets\<close>
66 val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty
67 [ Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
68 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
69 (*"(~ True) = False"*)
70 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
71 (*"(~ False) = True"*)
72 Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
73 (*"(?a & True) = ?a"*)
74 Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
75 (*"(?a & False) = False"*)
76 Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
77 (*"(?a | True) = True"*)
78 Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
79 (*"(?a | False) = ?a"*)
81 Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
82 Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),
83 Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3}),
84 Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),
85 Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
86 Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
88 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
89 Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
91 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
92 Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
93 Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
94 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
98 val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty
99 [ Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
100 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
101 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
102 Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
103 Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
104 Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
105 Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
107 Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
108 Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),
109 Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3}),
110 Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),
111 Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
112 Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
114 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
115 Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
117 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
118 Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
119 Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
120 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
123 subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
124 text \<open>requires "eval_binop" from above\<close>
126 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr
127 [ Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
128 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
129 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
130 Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
131 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
132 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
134 Rule.Eval ("Prog_Expr.Vars",Prog_Expr.eval_var "#Vars_"),
136 Rule.Thm ("if_True",ThmC.numerals_to_Free @{thm if_True}),
137 Rule.Thm ("if_False",ThmC.numerals_to_Free @{thm if_False})];
139 val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge "list_erls"
140 (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
141 erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
142 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
143 rules = [Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
144 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
145 (* ~~~~~~ for nth_Cons_*)],
146 scr = Rule.Empty_Prog},
147 srls = Rule_Set.Empty, calc = [], errpatts = [],
148 rules = [], scr = Rule.Empty_Prog})
151 subsection \<open>setup for extended rule-set\<close>
152 setup \<open>KEStore_Elems.add_rlss
153 [("prog_expr", (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} prog_expr))]\<close>