theory Base_Tools

  imports  "../ProgLang/ProgLang" "../Interpret/Interpret" "../BridgeLibisabelle/BridgeLibisabelle"

                                                          (*  ^^^ for KEStore_Elems.add_thes *)

begin

subsection \<open>theorems for Base_Tools\<close>

axiomatization where (*for evaluating the assumptions of conditional rules*)

(*last_thmI:	        "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and*)

  real_unari_minus:   "- a = (-1) * a" and

  radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and

  (* should be in Rational.thy, but: 

   needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML...*)

  rat_leq1:	      "[| b ~= 0; d ~= 0 |] ==>

		       ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and

  rat_leq2:	      "d ~= 0 ==>

		       ( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*) and

  rat_leq3:	      "b ~= 0 ==>

		       ((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)

subsection \<open>setup for ML-functions\<close>

text \<open>required by "eval_binop" below\<close>

setup \<open>KEStore_Elems.add_calcs

  [ ("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_")),

    ("some_occur_in", ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_")),

    ("is_atom", ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_")),

    ("is_even", ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_")),

    ("is_const", ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")),

    ("le", ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")),

    ("leq", ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_")),

    ("ident", ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")),

    ("equal", ("HOL.eq", Prog_Expr.eval_equal "#equal_")),

    ("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),

    ("MINUS", ("Groups.minus_class.minus", (**)eval_binop "#sub_")),

    ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),

    ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),

    ("POWER",("Prog_Expr.pow", (**)eval_binop "#power_")),

    ("boollist2sum", ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum ""))]\<close>

subsection \<open>rewrite-order for rule-sets\<close>

ML \<open>

\<close> ML \<open>

local

  open Term;

in

  fun termlessI (_: subst) uv = LibraryC.termless uv;

  fun term_ordI (_: subst) uv = Term_Ord.term_ord uv;

end;

\<close> ML \<open>

(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)

val tless_true = Rewrite_Ord.dummy_ord;

Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx here, too*)

			[("tless_true", tless_true),

			 ("e_rew_ord'", tless_true),

			 ("dummy_ord", Rewrite_Ord.dummy_ord)]);

\<close>

subsection \<open>rule-sets\<close>

ML \<open>

\<close> ML \<open>

val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty

  [ Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),

    Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),

		(*"(~ True) = False"*)

		Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),

		(*"(~ False) = True"*)

		Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),

		(*"(?a & True) = ?a"*)

		Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),

		(*"(?a & False) = False"*)

		Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),

		(*"(?a | True) = True"*)

		Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),

		(*"(?a | False) = ?a"*)

		Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),

		Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),

		Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3}),

      Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),

		Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),

		Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),

		Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),

		Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),

		Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),    

		Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),

		Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    

		Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];

\<close>

ML \<open>

val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty

  [ Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),

    Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),

		Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),

		Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),

		Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),

		Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),

		Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),

		Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),

		Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),

		Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3}),

		Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),

		Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),

		Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),

		Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),

		Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),

		Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),    

		Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),

		Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    

		Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];

\<close>

subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>

text \<open>requires "eval_binop" from above\<close>

ML \<open>

val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr

	[ Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),

		Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"), 

		Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),

		Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),

		Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),

		Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)

		Rule.Eval ("Prog_Expr.Vars",Prog_Expr.eval_var "#Vars_"),

		Rule.Thm ("if_True",ThmC.numerals_to_Free @{thm if_True}),

		Rule.Thm ("if_False",ThmC.numerals_to_Free @{thm if_False})];

val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge "list_erls"

	(Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),

    erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 

    erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],

    rules = [Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),

      Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")

      (*    ~~~~~~ for nth_Cons_*)],

    scr = Rule.Empty_Prog},

    srls = Rule_Set.Empty, calc = [], errpatts = [],

    rules = [], scr = Rule.Empty_Prog})

  prog_expr);

\<close>

subsection \<open>setup for extended rule-set\<close>

setup \<open>KEStore_Elems.add_rlss

  [("prog_expr", (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} prog_expr))]\<close>

end