1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Thu Aug 29 10:59:57 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Thu Aug 29 13:52:47 2019 +0200
1.3 @@ -2,4 +2,148 @@
1.4 imports "../ProgLang/ProgLang" "../Interpret/Interpret" "../BridgeLibisabelle/BridgeLibisabelle"
1.5 (* ^^^ for KEStore_Elems.add_thes *)
1.6 begin
1.7 +subsection \<open>theorems for Base_Tools\<close>
1.8 +axiomatization where (*for evaluating the assumptions of conditional rules*)
1.9 +
1.10 +(*last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and*)
1.11 + real_unari_minus: "- a = (-1) * a" and
1.12 + radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
1.13 + (* should be in Rational.thy, but:
1.14 + needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML...*)
1.15 + rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
1.16 + ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
1.17 + rat_leq2: "d ~= 0 ==>
1.18 + ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*) and
1.19 + rat_leq3: "b ~= 0 ==>
1.20 + ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
1.21 +
1.22 +subsection \<open>setup for ML-functions\<close>
1.23 +text \<open>required by "eval_binop" below\<close>
1.24 +setup \<open>KEStore_Elems.add_calcs
1.25 + [ ("occurs_in", ("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
1.26 + ("some_occur_in", ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
1.27 + ("is_atom", ("Atools.is'_atom", eval_is_atom "#is_atom_")),
1.28 + ("is_even", ("Atools.is'_even", eval_is_even "#is_even_")),
1.29 + ("is_const", ("Atools.is'_const", eval_const "#is_const_")),
1.30 + ("le", ("Orderings.ord_class.less", eval_equ "#less_")),
1.31 + ("leq", ("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),
1.32 + ("ident", ("Atools.ident", eval_ident "#ident_")),
1.33 + ("equal", ("HOL.eq", eval_equal "#equal_")),
1.34 + ("PLUS", ("Groups.plus_class.plus", eval_binop "#add_")),
1.35 + ("MINUS", ("Groups.minus_class.minus", eval_binop "#sub_")),
1.36 + ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")),
1.37 + ("DIVIDE", ("Rings.divide_class.divide", eval_cancel "#divide_e")),
1.38 + ("POWER",("Atools.pow", eval_binop "#power_")),
1.39 + ("boollist2sum", ("Atools.boollist2sum", eval_boollist2sum ""))]\<close>
1.40 +
1.41 +subsection \<open>rewrite-order for rule-sets\<close>
1.42 +ML \<open>
1.43 +\<close> ML \<open>
1.44 +local
1.45 + open Term;
1.46 +in
1.47 + fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
1.48 + fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
1.49 +end;
1.50 +\<close> ML \<open>
1.51 +(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
1.52 +val tless_true = Rule.dummy_ord;
1.53 +Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx here, too*)
1.54 + [("tless_true", tless_true),
1.55 + ("e_rew_ord'", tless_true),
1.56 + ("dummy_ord", Rule.dummy_ord)]);
1.57 +\<close>
1.58 +
1.59 +subsection \<open>rule-sets\<close>
1.60 +ML \<open>
1.61 +\<close> ML \<open>
1.62 +val Atools_erls = Rule.append_rls "Atools_erls" Rule.e_rls
1.63 + [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
1.64 + Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.65 + (*"(~ True) = False"*)
1.66 + Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
1.67 + (*"(~ False) = True"*)
1.68 + Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
1.69 + (*"(?a & True) = ?a"*)
1.70 + Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
1.71 + (*"(?a & False) = False"*)
1.72 + Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
1.73 + (*"(?a | True) = True"*)
1.74 + Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
1.75 + (*"(?a | False) = ?a"*)
1.76 +
1.77 + Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
1.78 + Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
1.79 + Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
1.80 + Rule.Thm ("refl", TermC.num_str @{thm refl}),
1.81 + Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
1.82 + Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
1.83 +
1.84 + Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
1.85 + Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
1.86 +
1.87 + Rule.Calc ("Atools.ident", eval_ident "#ident_"),
1.88 + Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
1.89 + Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),
1.90 + Rule.Calc ("Tools.matches", Tools.eval_matches "")];
1.91 +\<close>
1.92 +
1.93 +ML \<open>
1.94 +val Atools_crls = Rule.append_rls "Atools_crls" Rule.e_rls
1.95 + [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
1.96 + Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.97 + Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
1.98 + Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
1.99 + Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
1.100 + Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
1.101 + Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
1.102 +
1.103 + Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
1.104 + Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
1.105 + Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
1.106 + Rule.Thm ("refl", TermC.num_str @{thm refl}),
1.107 + Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
1.108 + Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
1.109 +
1.110 + Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
1.111 + Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
1.112 +
1.113 + Rule.Calc ("Atools.ident", eval_ident "#ident_"),
1.114 + Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
1.115 + Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),
1.116 + Rule.Calc ("Tools.matches", Tools.eval_matches "")];
1.117 +\<close>
1.118 +
1.119 +subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
1.120 +text \<open>requires "eval_binop" from above\<close>
1.121 +ML \<open>
1.122 +val list_rls = Rule.append_rls "list_rls" list_rls
1.123 + [ Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.124 + Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.125 + Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.126 + Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
1.127 + Rule.Calc ("Atools.ident",eval_ident "#ident_"),
1.128 + Rule.Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
1.129 +
1.130 + Rule.Calc ("Tools.Vars",Tools.eval_var "#Vars_"),
1.131 +
1.132 + Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
1.133 + Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
1.134 +
1.135 +val list_rls = LTool.prep_rls @{theory} (Rule.merge_rls "list_erls"
1.136 + (Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
1.137 + erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
1.138 + erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
1.139 + rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.140 + Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")
1.141 + (* ~~~~~~ for nth_Cons_*)],
1.142 + scr = Rule.EmptyScr},
1.143 + srls = Rule.Erls, calc = [], errpatts = [],
1.144 + rules = [], scr = Rule.EmptyScr})
1.145 + list_rls);
1.146 +\<close>
1.147 +subsection \<open>setup for extended rule-set\<close>
1.148 +setup \<open>KEStore_Elems.add_rlss
1.149 + [("list_rls", (Context.theory_name @{theory}, LTool.prep_rls @{theory} list_rls))]\<close>
1.150 +
1.151 end
1.152 \ No newline at end of file