35 val thy = @{theory}; |
35 val thy = @{theory}; |
36 |
36 |
37 val eval_rls = prep_rls' ( |
37 val eval_rls = prep_rls' ( |
38 Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI), |
38 Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI), |
39 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
39 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
40 rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}), |
40 rules = [Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}), |
41 Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}), |
41 Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}), |
42 Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}), |
42 Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}), |
43 Rule.Thm ("not_true", TermC.num_str @{thm not_true}), |
43 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}), |
44 Rule.Thm ("not_false", TermC.num_str @{thm not_false}), |
44 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}), |
45 Rule.Thm ("and_true", TermC.num_str @{thm and_true}), |
45 Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}), |
46 Rule.Thm ("and_false", TermC.num_str @{thm and_false}), |
46 Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}), |
47 Rule.Thm ("or_true", TermC.num_str @{thm or_true}), |
47 Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}), |
48 Rule.Thm ("or_false", TermC.num_str @{thm or_false}), |
48 Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}), |
49 Rule.Thm ("and_commute", TermC.num_str @{thm and_commute}), |
49 Rule.Thm ("and_commute", ThmC.numerals_to_Free @{thm and_commute}), |
50 Rule.Thm ("or_commute", TermC.num_str @{thm or_commute}), |
50 Rule.Thm ("or_commute", ThmC.numerals_to_Free @{thm or_commute}), |
51 |
51 |
52 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
52 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
53 Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"), |
53 Rule.Num_Calc ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"), |
54 |
54 |
55 Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"), |
55 Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"), |
194 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)}, |
194 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)}, |
195 @{thm refl})] |
195 @{thm refl})] |
196 \<close> |
196 \<close> |
197 ML \<open> |
197 ML \<open> |
198 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr |
198 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr |
199 [Rule.Thm ("filterVar_Const", TermC.num_str @{thm filterVar_Const}), |
199 [Rule.Thm ("filterVar_Const", ThmC.numerals_to_Free @{thm filterVar_Const}), |
200 Rule.Thm ("filterVar_Nil", TermC.num_str @{thm filterVar_Nil})]; |
200 Rule.Thm ("filterVar_Nil", ThmC.numerals_to_Free @{thm filterVar_Nil})]; |
201 \<close> |
201 \<close> |
202 setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close> |
202 setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close> |
203 |
203 |
204 end |
204 end |