70 end; |
70 end; |
71 |
71 |
72 (*WN080222 |
72 (*WN080222 |
73 (*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*) |
73 (*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*) |
74 fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ = |
74 fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ = |
75 SOME ((Rule.term2str p) ^ " = " ^ Rule.term2str (new_c p), |
75 SOME ((UnparseC.term2str p) ^ " = " ^ UnparseC.term2str (new_c p), |
76 Trueprop $ (mk_equality (p, new_c p))) |
76 Trueprop $ (mk_equality (p, new_c p))) |
77 | eval_new_c _ _ _ _ = NONE; |
77 | eval_new_c _ _ _ _ = NONE; |
78 *) |
78 *) |
79 |
79 |
80 (*WN080222:*) |
80 (*WN080222:*) |
84 fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) = |
84 fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) = |
85 let val p' = case p of |
85 let val p' = case p of |
86 Const ("HOL.eq", T) $ lh $ rh => |
86 Const ("HOL.eq", T) $ lh $ rh => |
87 Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh) |
87 Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh) |
88 | p => TermC.mk_add p (new_c p) |
88 | p => TermC.mk_add p (new_c p) |
89 in SOME ((Rule.term2str p) ^ " = " ^ Rule.term2str p', |
89 in SOME ((UnparseC.term2str p) ^ " = " ^ UnparseC.term2str p', |
90 HOLogic.Trueprop $ (TermC.mk_equality (p, p'))) |
90 HOLogic.Trueprop $ (TermC.mk_equality (p, p'))) |
91 end |
91 end |
92 | eval_add_new_c _ _ _ _ = NONE; |
92 | eval_add_new_c _ _ _ _ = NONE; |
93 |
93 |
94 |
94 |
95 (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*) |
95 (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*) |
96 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _) |
96 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _) |
97 $ arg)) _ = |
97 $ arg)) _ = |
98 if TermC.is_f_x arg |
98 if TermC.is_f_x arg |
99 then SOME ((Rule.term2str p) ^ " = True", |
99 then SOME ((UnparseC.term2str p) ^ " = True", |
100 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) |
100 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True}))) |
101 else SOME ((Rule.term2str p) ^ " = False", |
101 else SOME ((UnparseC.term2str p) ^ " = False", |
102 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
102 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))) |
103 | eval_is_f_x _ _ _ _ = NONE; |
103 | eval_is_f_x _ _ _ _ = NONE; |
104 \<close> |
104 \<close> |
105 setup \<open>KEStore_Elems.add_calcs |
105 setup \<open>KEStore_Elems.add_calcs |
106 [("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")), |
106 [("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")), |