130 subsection \<open>rule set for evaluating Porg_Expr, will be extended in several thys\<close> |
130 subsection \<open>rule set for evaluating Porg_Expr, will be extended in several thys\<close> |
131 ML \<open> |
131 ML \<open> |
132 \<close> ML \<open> |
132 \<close> ML \<open> |
133 val prog_expr = |
133 val prog_expr = |
134 Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
134 Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
135 erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [], |
135 asm_rls = Rule_Def.Empty, prog_rls = Rule_Def.Empty, calc = [], errpatts = [], |
136 rules = [Rule_Def.Thm ("refl", @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) |
136 rules = [Rule_Def.Thm ("refl", @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) |
137 Rule_Def.Thm ("o_apply", @{thm o_apply}), |
137 Rule_Def.Thm ("o_apply", @{thm o_apply}), |
138 |
138 |
139 Rule_Def.Thm ("NTH_CONS", @{thm NTH_CONS}),(*erls for cond. in Atools.ML*) |
139 Rule_Def.Thm ("NTH_CONS", @{thm NTH_CONS}),(*asm_rls for cond. in Atools.ML*) |
140 Rule_Def.Thm ("NTH_NIL", @{thm NTH_NIL}), |
140 Rule_Def.Thm ("NTH_NIL", @{thm NTH_NIL}), |
141 Rule_Def.Thm ("append_Cons", @{thm append_Cons}), |
141 Rule_Def.Thm ("append_Cons", @{thm append_Cons}), |
142 Rule_Def.Thm ("append_Nil", @{thm append_Nil}), |
142 Rule_Def.Thm ("append_Nil", @{thm append_Nil}), |
143 (* Thm ("butlast_Cons",num_str @{thm butlast_Cons}), |
143 (* Thm ("butlast_Cons",num_str @{thm butlast_Cons}), |
144 Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*) |
144 Thm ("butlast_Nil",num_str @{thm butlast_Nil}),*) |
174 Rule_Def.Thm ("take_Cons", @{thm take_Cons}), |
174 Rule_Def.Thm ("take_Cons", @{thm take_Cons}), |
175 Rule_Def.Thm ("tl_Cons", @{thm tl_Cons}), |
175 Rule_Def.Thm ("tl_Cons", @{thm tl_Cons}), |
176 Rule_Def.Thm ("tl_Nil", @{thm tl_Nil}), |
176 Rule_Def.Thm ("tl_Nil", @{thm tl_Nil}), |
177 Rule_Def.Thm ("zip_Cons", @{thm zip_Cons}), |
177 Rule_Def.Thm ("zip_Cons", @{thm zip_Cons}), |
178 Rule_Def.Thm ("zip_Nil", @{thm zip_Nil})], |
178 Rule_Def.Thm ("zip_Nil", @{thm zip_Nil})], |
179 scr = Rule_Def.Empty_Prog}: Rule_Set.T; |
179 program = Rule_Def.Empty_Prog}: Rule_Set.T; |
180 \<close> |
180 \<close> |
181 rule_set_knowledge prog_expr = prog_expr |
181 rule_set_knowledge prog_expr = prog_expr |
182 |
182 |
183 ML \<open> |
183 ML \<open> |
184 \<close> ML \<open> |
184 \<close> ML \<open> |