wneuper@59424: theory Base_Tools
wneuper@59600:   imports  "../ProgLang/ProgLang" "../Interpret/Interpret" "../BridgeLibisabelle/BridgeLibisabelle"
wneuper@59600:                                                           (*  ^^^ for KEStore_Elems.add_thes *)
wneuper@59424: begin
wneuper@59602: subsection \<open>theorems for Base_Tools\<close>
wneuper@59602: axiomatization where (*for evaluating the assumptions of conditional rules*)
wneuper@59602: 
wneuper@59602: (*last_thmI:	        "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and*)
wneuper@59602:   real_unari_minus:   "- a = (-1) * a" and
wneuper@59602:   radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
wneuper@59602:   (* should be in Rational.thy, but: 
wneuper@59602:    needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML...*)
wneuper@59602:   rat_leq1:	      "[| b ~= 0; d ~= 0 |] ==>
wneuper@59602: 		       ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
wneuper@59602:   rat_leq2:	      "d ~= 0 ==>
wneuper@59602: 		       ( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*) and
wneuper@59602:   rat_leq3:	      "b ~= 0 ==>
wneuper@59602: 		       ((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)
wneuper@59602: 
wneuper@59602: subsection \<open>setup for ML-functions\<close>
wneuper@59602: text \<open>required by "eval_binop" below\<close>
wneuper@59602: setup \<open>KEStore_Elems.add_calcs
walther@59603:   [ ("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_")),
walther@59603:     ("some_occur_in", ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_")),
walther@59603:     ("is_atom", ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_")),
walther@59603:     ("is_even", ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_")),
walther@59603:     ("is_const", ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")),
walther@59603:     ("le", ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")),
walther@59603:     ("leq", ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_")),
walther@59603:     ("ident", ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")),
walther@59603:     ("equal", ("HOL.eq", Prog_Expr.eval_equal "#equal_")),
walther@59603:     ("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
walther@59603:     ("MINUS", ("Groups.minus_class.minus", (**)eval_binop "#sub_")),
walther@59603:     ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
walther@59603:     ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
walther@59603:     ("POWER",("Prog_Expr.pow", (**)eval_binop "#power_")),
walther@59603:     ("boollist2sum", ("Prog_Expr.boollist2sum", 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
wneuper@59602:   fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
wneuper@59602:   fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
wneuper@59602: end;
wneuper@59602: \<close> ML \<open>
wneuper@59602: (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
wneuper@59602: val tless_true = Rule.dummy_ord;
wneuper@59602: Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx here, too*)
wneuper@59602: 			[("tless_true", tless_true),
wneuper@59602: 			 ("e_rew_ord'", tless_true),
wneuper@59602: 			 ("dummy_ord", Rule.dummy_ord)]);
wneuper@59602: \<close>
wneuper@59602: 
wneuper@59602: subsection \<open>rule-sets\<close>
wneuper@59602: ML \<open>
wneuper@59602: \<close> ML \<open>
walther@59852: val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty
walther@59773:   [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
wneuper@59602:     Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
wneuper@59602: 		(*"(~ True) = False"*)
wneuper@59602: 		Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
wneuper@59602: 		(*"(~ False) = True"*)
wneuper@59602: 		Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
wneuper@59602: 		(*"(?a & True) = ?a"*)
wneuper@59602: 		Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
wneuper@59602: 		(*"(?a & False) = False"*)
wneuper@59602: 		Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
wneuper@59602: 		(*"(?a | True) = True"*)
wneuper@59602: 		Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
wneuper@59602: 		(*"(?a | False) = ?a"*)
wneuper@59602:                
wneuper@59602: 		Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
wneuper@59602: 		Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
wneuper@59602: 		Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
wneuper@59602:       Rule.Thm ("refl", TermC.num_str @{thm refl}),
wneuper@59602: 		Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
wneuper@59602: 		Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
wneuper@59602: 		
walther@59773: 		Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
walther@59773: 		Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
wneuper@59602: 		
walther@59773: 		Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),    
walther@59773: 		Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
walther@59773: 		Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
walther@59773: 		Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
wneuper@59602: \<close>
wneuper@59602: 
wneuper@59602: ML \<open>
walther@59852: val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty
walther@59773:   [ Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
wneuper@59602:     Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
wneuper@59602: 		Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
wneuper@59602: 		Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
wneuper@59602: 		Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
wneuper@59602: 		Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
wneuper@59602: 		Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
wneuper@59602:                
wneuper@59602: 		Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
wneuper@59602: 		Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
wneuper@59602: 		Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
wneuper@59602: 		Rule.Thm ("refl", TermC.num_str @{thm refl}),
wneuper@59602: 		Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
wneuper@59602: 		Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
wneuper@59602: 		
walther@59773: 		Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
walther@59773: 		Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
wneuper@59602: 		
walther@59773: 		Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),    
walther@59773: 		Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
walther@59773: 		Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),    
walther@59773: 		Rule.Num_Calc ("Prog_Expr.matches", 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@59852: val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr
walther@59773: 	[ Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
walther@59773: 		Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), 
walther@59773: 		Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
walther@59773: 		Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
walther@59773: 		Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
walther@59773: 		Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
wneuper@59602:        
walther@59773: 		Rule.Num_Calc ("Prog_Expr.Vars",Prog_Expr.eval_var "#Vars_"),
wneuper@59602: 		
wneuper@59602: 		Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
wneuper@59602: 		Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
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@59773:     rules = [Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
walther@59773:       Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
wneuper@59602:       (*    ~~~~~~ for nth_Cons_*)],
wneuper@59602:     scr = Rule.EmptyScr},
walther@59851:     srls = Rule_Set.Empty, calc = [], errpatts = [],
wneuper@59602:     rules = [], scr = Rule.EmptyScr})
walther@59801:   prog_expr);
wneuper@59602: \<close>
wneuper@59602: subsection \<open>setup for extended rule-set\<close>
wneuper@59602: setup \<open>KEStore_Elems.add_rlss
walther@59801:   [("prog_expr", (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} prog_expr))]\<close>
wneuper@59602: 
wneuper@59424: end