wneuper@59424: theory Base_Tools
walther@60149:   imports Interpret.Interpret
walther@60149: (** )"../BridgeJEdit/BridgeJEdit"                    ( *activate after devel.of BridgeJEdit*)
walther@60149: (**) "../BridgeLibisabelle/BridgeLibisabelle"           (*remove after devel.of BridgeJEdit*)
walther@60149:                       (*  ^^^ for KEStore_Elems.add_thes *)
wneuper@59424: begin
wneuper@59602: subsection \<open>theorems for Base_Tools\<close>
walther@60273: 
walther@60384: lemma real_unari_minus:   "Not (a is_num) ==> - a = (-1) * (a::real)" by auto
walther@60318: (*lemma real_unari_minus:   "- a = (-1) * (a::real)" by auto LOOPS WITH NUMERALS*)
walther@60273: (*Semiring_Normalization.comm_ring_1_class.ring_normalization_rules(1)*)
walther@60273: 
walther@60273: (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
walther@60274: lemma radd_left_cancel_le: "((k::real) + m \<le> k + n) = (m \<le> n)" by auto
walther@60273: (*Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left*)
walther@60273: 
walther@60274: thm "Fields.linordered_field_class.mult_imp_le_div_pos" (*0 < ?y \<Longrightarrow> ?z * ?y \<le> ?x \<Longrightarrow> ?z \<le> ?x / ?y*)
walther@60274: 
wneuper@59602: axiomatization where (*for evaluating the assumptions of conditional rules*)
walther@60273:   (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
walther@60274:   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:   rat_leq2:	          "0 \<noteq> d \<Longrightarrow> (a     \<le> c / d) = (a * d \<le>     c)"(*Quickcheck found a counterexample*) and
walther@60274:   rat_leq3:	"0 \<noteq> b           \<Longrightarrow> (a / b \<le> c    ) = (a     \<le> b * c)"(*Quickcheck found a counterexample*)
wneuper@59602: 
wneuper@59602: 
wneuper@59602: subsection \<open>setup for ML-functions\<close>
wneuper@59602: text \<open>required by "eval_binop" below\<close>
wenzelm@60313: calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>
wenzelm@60313: calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
wenzelm@60313: calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
wenzelm@60313: calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close>
wenzelm@60313: calculation le (less) = \<open>Prog_Expr.eval_equ "#less_"\<close>
wenzelm@60313: calculation leq (less_eq) = \<open>Prog_Expr.eval_equ "#less_equal_"\<close>
wenzelm@60313: calculation ident = \<open>Prog_Expr.eval_ident "#ident_"\<close>
wenzelm@60313: calculation equal (HOL.eq) = \<open>Prog_Expr.eval_equal "#equal_"\<close>
wenzelm@60313: calculation PLUS (plus) = \<open>(**)eval_binop "#add_"\<close>
wenzelm@60313: calculation MINUS (minus) = \<open>(**)eval_binop "#sub_"\<close>
wenzelm@60313: calculation TIMES (times) = \<open>(**)eval_binop "#mult_"\<close>
wenzelm@60313: calculation DIVIDE (divide) = \<open>Prog_Expr.eval_cancel "#divide_e"\<close>
wenzelm@60405: calculation POWER (realpow) = \<open>(**)eval_binop "#power_"\<close>
wenzelm@60313: calculation boollist2sum = \<open>Prog_Expr.eval_boollist2sum ""\<close>
wneuper@59602: 
wneuper@59602: subsection \<open>rewrite-order for rule-sets\<close>
wneuper@59602: ML \<open>
wneuper@59602: \<close> ML \<open>
wneuper@59602: local
wneuper@59602:   open Term;
wneuper@59602: in
walther@59910:   fun termlessI (_: subst) uv = LibraryC.termless uv;
walther@59910:   fun term_ordI (_: subst) uv = Term_Ord.term_ord uv;
wneuper@59602: end;
wneuper@59602: \<close> ML \<open>
Walther@60509: (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.function_empty = Rewrite_Ord.function_empty*)
Walther@60509: val tless_true = Rewrite_Ord.function_empty;
Walther@60506: \<close> ML \<open>
Walther@60506: \<close> 
Walther@60506: setup \<open>KEStore_Elems.add_rew_ord [
Walther@60506:   ("tless_true", tless_true),
Walther@60509: 	("Rewrite_Ord.id_empty", tless_true),
Walther@60506: 	("e_rew_ord'", tless_true),
Walther@60509: 	("dummy_ord", Rewrite_Ord.function_empty)]\<close>
wneuper@59602: 
wneuper@59602: subsection \<open>rule-sets\<close>
wneuper@59602: ML \<open>
wneuper@59602: \<close> ML \<open>
walther@60358: val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty [
walther@60358:   \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
walther@60358:   \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
walther@60358: 	\<^rule_thm>\<open>not_false\<close>, (*"(~ False) = True"*)
walther@60358: 	\<^rule_thm>\<open>and_true\<close>, (*"(?a & True) = ?a"*)
walther@60358: 	\<^rule_thm>\<open>and_false\<close>, (*"(?a & False) = False"*)
walther@60358: 	\<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*)
walther@60358: 	\<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
walther@60358:              
walther@60358: 	\<^rule_thm>\<open>rat_leq1\<close>,
walther@60358: 	\<^rule_thm>\<open>rat_leq2\<close>,
walther@60358: 	\<^rule_thm>\<open>rat_leq3\<close>,
walther@60358:   \<^rule_thm>\<open>refl\<close>,
walther@60358: 	\<^rule_thm>\<open>order_refl\<close>,
walther@60358: 	\<^rule_thm>\<open>radd_left_cancel_le\<close>,
walther@60358: 	
walther@60358: 	\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
walther@60358: 	\<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
walther@60358: 	
walther@60358: 	\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
walther@60385: 	\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
walther@60358: 	\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
walther@60358: 	\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
wneuper@59602: \<close>
wneuper@59602: 
wneuper@59602: ML \<open>
walther@60358: val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty [
walther@60358:   \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
walther@60358:   \<^rule_thm>\<open>not_true\<close>,
walther@60358:  	\<^rule_thm>\<open>not_false\<close>,
walther@60358:  	\<^rule_thm>\<open>and_true\<close>,
walther@60358:  	\<^rule_thm>\<open>and_false\<close>,
walther@60358:  	\<^rule_thm>\<open>or_true\<close>,
walther@60358:  	\<^rule_thm>\<open>or_false\<close>,
walther@60358:  
walther@60358:  	\<^rule_thm>\<open>rat_leq1\<close>,
walther@60358:  	\<^rule_thm>\<open>rat_leq2\<close>,
walther@60358:  	\<^rule_thm>\<open>rat_leq3\<close>,
walther@60358:  	\<^rule_thm>\<open>refl\<close>,
walther@60358:  	\<^rule_thm>\<open>order_refl\<close>,
walther@60358:  	\<^rule_thm>\<open>radd_left_cancel_le\<close>,
walther@60358:  	
walther@60358:  	\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
walther@60358:  	\<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
walther@60358:  	
walther@60358:  	\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
walther@60385: 	\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
walther@60358:  	\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
walther@60358:  	\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
wneuper@59602: \<close>
wneuper@59602: 
wneuper@59602: subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
wneuper@59602: text \<open>requires "eval_binop" from above\<close>
wneuper@59602: ML \<open>
walther@60358: val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [
walther@60358:   \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
walther@60358: 	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
walther@60358: 	\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
walther@60358: 	\<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
walther@60358: 	\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
walther@60358: 	\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
walther@60358:      
walther@60358: 	\<^rule_eval>\<open>Prog_Expr.Vars\<close> (Prog_Expr.eval_var "#Vars_"),
walther@60358: 	
walther@60358: 	\<^rule_thm>\<open>if_True\<close>,
walther@60358: 	\<^rule_thm>\<open>if_False\<close>];
wneuper@59602: 
walther@59852: val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge "list_erls"
walther@59851: 	(Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
walther@59851:     erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 
walther@59852:     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358:     rules = [
walther@60358:       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
walther@60358:       \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_") (*..for nth_Cons_*)],
walther@59878:     scr = Rule.Empty_Prog},
walther@59851:     srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@59878:     rules = [], scr = Rule.Empty_Prog})
walther@59801:   prog_expr);
wneuper@59602: \<close>
wenzelm@60286: 
wneuper@59602: subsection \<open>setup for extended rule-set\<close>
wenzelm@60286: 
wenzelm@60289: rule_set_knowledge prog_expr = \<open>Auto_Prog.prep_rls @{theory} prog_expr\<close>
wneuper@59602: 
walther@60278: ML \<open>
walther@60278: \<close> ML \<open>
walther@60278: \<close> ML \<open>
walther@60278: \<close>
walther@60077: end