prep. re-organisation of thys in ProgLang
2 imports "../ProgLang/ProgLang" "../Interpret/Interpret" "../BridgeLibisabelle/BridgeLibisabelle"
3 (* ^^^ for KEStore_Elems.add_thes *)
5 subsection \<open>theorems for Base_Tools\<close>
6 axiomatization where (*for evaluating the assumptions of conditional rules*)
8 (*last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and*)
9 real_unari_minus: "- a = (-1) * a" and
10 radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
11 (* should be in Rational.thy, but:
12 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML...*)
13 rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
14 ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
16 ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*) and
18 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
20 subsection \<open>setup for ML-functions\<close>
21 text \<open>required by "eval_binop" below\<close>
22 setup \<open>KEStore_Elems.add_calcs
23 [ ("occurs_in", ("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
24 ("some_occur_in", ("Atools.some'_occur'_in", eval_some_occur_in "#some_occur_in_")),
25 ("is_atom", ("Atools.is'_atom", eval_is_atom "#is_atom_")),
26 ("is_even", ("Atools.is'_even", eval_is_even "#is_even_")),
27 ("is_const", ("Atools.is'_const", eval_const "#is_const_")),
28 ("le", ("Orderings.ord_class.less", eval_equ "#less_")),
29 ("leq", ("Orderings.ord_class.less_eq", eval_equ "#less_equal_")),
30 ("ident", ("Atools.ident", eval_ident "#ident_")),
31 ("equal", ("HOL.eq", eval_equal "#equal_")),
32 ("PLUS", ("Groups.plus_class.plus", eval_binop "#add_")),
33 ("MINUS", ("Groups.minus_class.minus", eval_binop "#sub_")),
34 ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")),
35 ("DIVIDE", ("Rings.divide_class.divide", eval_cancel "#divide_e")),
36 ("POWER",("Atools.pow", eval_binop "#power_")),
37 ("boollist2sum", ("Atools.boollist2sum", eval_boollist2sum ""))]\<close>
39 subsection \<open>rewrite-order for rule-sets\<close>
45 fun termlessI (_: Rule.subst) uv = LibraryC.termless uv;
46 fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
49 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
50 val tless_true = Rule.dummy_ord;
51 Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx here, too*)
52 [("tless_true", tless_true),
53 ("e_rew_ord'", tless_true),
54 ("dummy_ord", Rule.dummy_ord)]);
57 subsection \<open>rule-sets\<close>
60 val Atools_erls = Rule.append_rls "Atools_erls" Rule.e_rls
61 [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
62 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
63 (*"(~ True) = False"*)
64 Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
65 (*"(~ False) = True"*)
66 Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
67 (*"(?a & True) = ?a"*)
68 Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
69 (*"(?a & False) = False"*)
70 Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
71 (*"(?a | True) = True"*)
72 Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
73 (*"(?a | False) = ?a"*)
75 Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
76 Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
77 Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
78 Rule.Thm ("refl", TermC.num_str @{thm refl}),
79 Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
80 Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
82 Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
83 Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
85 Rule.Calc ("Atools.ident", eval_ident "#ident_"),
86 Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
87 Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),
88 Rule.Calc ("Tools.matches", Tools.eval_matches "")];
92 val Atools_crls = Rule.append_rls "Atools_crls" Rule.e_rls
93 [ Rule.Calc ("HOL.eq", eval_equal "#equal_"),
94 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
95 Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
96 Rule.Thm ("and_true", TermC.num_str @{thm and_true}),
97 Rule.Thm ("and_false", TermC.num_str @{thm and_false}),
98 Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
99 Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
101 Rule.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
102 Rule.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
103 Rule.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3}),
104 Rule.Thm ("refl", TermC.num_str @{thm refl}),
105 Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
106 Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
108 Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_"),
109 Rule.Calc ("Orderings.ord_class.less_eq", eval_equ "#less_equal_"),
111 Rule.Calc ("Atools.ident", eval_ident "#ident_"),
112 Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
113 Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),
114 Rule.Calc ("Tools.matches", Tools.eval_matches "")];
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>
120 val list_rls = Rule.append_rls "list_rls" list_rls
121 [ Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
122 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
123 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
124 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
125 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
126 Rule.Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
128 Rule.Calc ("Tools.Vars",Tools.eval_var "#Vars_"),
130 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
131 Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
133 val list_rls = LTool.prep_rls @{theory} (Rule.merge_rls "list_erls"
134 (Rule.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
135 erls = Rule.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
136 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
137 rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
138 Rule.Calc ("Orderings.ord_class.less", eval_equ "#less_")
139 (* ~~~~~~ for nth_Cons_*)],
140 scr = Rule.EmptyScr},
141 srls = Rule.Erls, calc = [], errpatts = [],
142 rules = [], scr = Rule.EmptyScr})
145 subsection \<open>setup for extended rule-set\<close>
146 setup \<open>KEStore_Elems.add_rlss
147 [("list_rls", (Context.theory_name @{theory}, LTool.prep_rls @{theory} list_rls))]\<close>