22 rat_leq2: "0 \<noteq> d \<Longrightarrow> (a \<le> c / d) = (a * d \<le> 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*) |
23 rat_leq3: "0 \<noteq> b \<Longrightarrow> (a / b \<le> c ) = (a \<le> b * c)"(*Quickcheck found a counterexample*) |
24 |
24 |
25 |
25 |
26 subsection \<open>setup for ML-functions\<close> |
26 subsection \<open>setup for ML-functions\<close> |
27 text \<open>required by "eval_binop" below\<close> |
27 text \<open>required by "Calc_Binop.numeric" below\<close> |
28 calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close> |
28 calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close> |
29 calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close> |
29 calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close> |
30 calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close> |
30 calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close> |
31 calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close> |
31 calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close> |
32 calculation le (less) = \<open>Prog_Expr.eval_equ "#less_"\<close> |
32 calculation le (less) = \<open>Prog_Expr.eval_equ "#less_"\<close> |
33 calculation leq (less_eq) = \<open>Prog_Expr.eval_equ "#less_equal_"\<close> |
33 calculation leq (less_eq) = \<open>Prog_Expr.eval_equ "#less_equal_"\<close> |
34 calculation ident = \<open>Prog_Expr.eval_ident "#ident_"\<close> |
34 calculation ident = \<open>Prog_Expr.eval_ident "#ident_"\<close> |
35 calculation equal (HOL.eq) = \<open>Prog_Expr.eval_equal "#equal_"\<close> |
35 calculation equal (HOL.eq) = \<open>Prog_Expr.eval_equal "#equal_"\<close> |
36 calculation PLUS (plus) = \<open>(**)eval_binop "#add_"\<close> |
36 calculation PLUS (plus) = \<open>(**)Calc_Binop.numeric "#add_"\<close> |
37 calculation MINUS (minus) = \<open>(**)eval_binop "#sub_"\<close> |
37 calculation MINUS (minus) = \<open>(**)Calc_Binop.numeric "#sub_"\<close> |
38 calculation TIMES (times) = \<open>(**)eval_binop "#mult_"\<close> |
38 calculation TIMES (times) = \<open>(**)Calc_Binop.numeric "#mult_"\<close> |
39 calculation DIVIDE (divide) = \<open>Prog_Expr.eval_cancel "#divide_e"\<close> |
39 calculation DIVIDE (divide) = \<open>Prog_Expr.eval_cancel "#divide_e"\<close> |
40 calculation POWER (realpow) = \<open>(**)eval_binop "#power_"\<close> |
40 calculation POWER (realpow) = \<open>(**)Calc_Binop.numeric "#power_"\<close> |
41 calculation boollist2sum = \<open>Prog_Expr.eval_boollist2sum ""\<close> |
41 calculation boollist2sum = \<open>Prog_Expr.eval_boollist2sum ""\<close> |
42 |
42 |
43 subsection \<open>rewrite-order for rule-sets\<close> |
43 subsection \<open>rewrite-order for rule-sets\<close> |
44 ML \<open> |
44 ML \<open> |
45 \<close> ML \<open> |
45 \<close> ML \<open> |
113 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""), |
113 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""), |
114 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")]; |
114 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")]; |
115 \<close> |
115 \<close> |
116 |
116 |
117 subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close> |
117 subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close> |
118 text \<open>requires "eval_binop" from above\<close> |
118 text \<open>requires "Calc_Binop.numeric" from above\<close> |
119 ML \<open> |
119 ML \<open> |
120 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [ |
120 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [ |
121 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"), |
121 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"), |
122 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
122 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
123 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
123 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
124 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"), |
124 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"), |
125 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"), |
125 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"), |
126 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*) |
126 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*) |
127 |
127 |
133 val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge "list_erls" |
133 val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge "list_erls" |
134 (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI), |
134 (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI), |
135 erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), |
135 erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), |
136 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
136 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
137 rules = [ |
137 rules = [ |
138 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
138 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
139 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_") (*..for nth_Cons_*)], |
139 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_") (*..for nth_Cons_*)], |
140 scr = Rule.Empty_Prog}, |
140 scr = Rule.Empty_Prog}, |
141 srls = Rule_Set.Empty, calc = [], errpatts = [], |
141 srls = Rule_Set.Empty, calc = [], errpatts = [], |
142 rules = [], scr = Rule.Empty_Prog}) |
142 rules = [], scr = Rule.Empty_Prog}) |
143 prog_expr); |
143 prog_expr); |