equal
deleted
inserted
replaced
102 "----- for 'd_d s a' we got 'a is_const' --> False --------vvv-----"; |
102 "----- for 'd_d s a' we got 'a is_const' --> False --------vvv-----"; |
103 trace_rewrite := true; |
103 trace_rewrite := true; |
104 val ct = "d_d s a"; |
104 val ct = "d_d s a"; |
105 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct); |
105 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct); |
106 (*got: NONE instead SOME*) |
106 (*got: NONE instead SOME*) |
107 eval_true Isac.thy [str2term "a is_const"] (assoc_rls"erls"); |
107 eval_true (theory "Isac") [str2term "a is_const"] (assoc_rls"erls"); |
108 (*got: false instead true; ~~~~~~~~~~~ replaced by 'is_atom'*) |
108 (*got: false instead true; ~~~~~~~~~~~ replaced by 'is_atom'*) |
109 val SOME (ctt,_) = |
109 val SOME (ctt,_) = |
110 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct); |
110 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct); |
111 if ctt = "0" then () else error "diff.sml: thm 'diff_const' diff.behav."; |
111 if ctt = "0" then () else error "diff.sml: thm 'diff_const' diff.behav."; |
112 trace_rewrite := false; |
112 trace_rewrite := false; |
261 val SOME (ct',_) = rewrite_set "Isac" false "make_polynomial" ct; |
261 val SOME (ct',_) = rewrite_set "Isac" false "make_polynomial" ct; |
262 |
262 |
263 trace_rewrite:=true; |
263 trace_rewrite:=true; |
264 val t = str2term ct; |
264 val t = str2term ct; |
265 term2str t; |
265 term2str t; |
266 val SOME (t',_) = rewrite_set_ Isac.thy false make_polynomial t; |
266 val SOME (t',_) = rewrite_set_ (theory "Isac") false make_polynomial t; |
267 term2str t'; |
267 term2str t'; |
268 trace_rewrite:=false; |
268 trace_rewrite:=false; |
269 |
269 |
270 val SOME (t'',_) = rewrite_set_ Isac.thy false make_polynomial t'; |
270 val SOME (t'',_) = rewrite_set_ (theory "Isac") false make_polynomial t'; |
271 term2str t''; |
271 term2str t''; |
272 |
272 |
273 val thm = num_str @{thm realpow_eq_oneI; |
273 val thm = num_str @{thm realpow_eq_oneI; |
274 case string_of_thm thm of |
274 case string_of_thm thm of |
275 |
275 |
479 |
479 |
480 val screxp1 = subst_atomic [(f_f, f), (v_, v)] screxp0; |
480 val screxp1 = subst_atomic [(f_f, f), (v_, v)] screxp0; |
481 term2str screxp1; |
481 term2str screxp1; |
482 atomty screxp1; |
482 atomty screxp1; |
483 |
483 |
484 val SOME (f'_,_) = rewrite_set_ Isac.thy false srls_diff screxp1; |
484 val SOME (f'_,_) = rewrite_set_ (theory "Isac") false srls_diff screxp1; |
485 if term2str f'_= "Take (A' = d_d s (s * (a - s)))" then () |
485 if term2str f'_= "Take (A' = d_d s (s * (a - s)))" then () |
486 else error "diff.sml: diff.behav. in 'primed'"; |
486 else error "diff.sml: diff.behav. in 'primed'"; |
487 atomty f'_; |
487 atomty f'_; |
488 |
488 |
489 val str = "Script DiffEqScr (f_f::bool) (v_v::real) = \ |
489 val str = "Script DiffEqScr (f_f::bool) (v_v::real) = \ |
664 "----- thm 'diff_prod_const'"; |
664 "----- thm 'diff_prod_const'"; |
665 val subs = [(str2term "bdv", str2term "l")]; |
665 val subs = [(str2term "bdv", str2term "l")]; |
666 val f = str2term "G' = d_d l (l * sqrt (7 * s ^ 2 - l ^ 2))"; |
666 val f = str2term "G' = d_d l (l * sqrt (7 * s ^ 2 - l ^ 2))"; |
667 (* |
667 (* |
668 trace_rewrite := true; |
668 trace_rewrite := true; |
669 rewrite_inst_ Isac.thy tless_true erls_diff true subs diff_prod_const f; |
669 rewrite_inst_ (theory "Isac") tless_true erls_diff true subs diff_prod_const f; |
670 trace_rewrite := false; |
670 trace_rewrite := false; |
671 *) |
671 *) |
672 |
672 |
673 "------------inform for x^2+x+1 ----------------------------------"; |
673 "------------inform for x^2+x+1 ----------------------------------"; |
674 "------------inform for x^2+x+1 ----------------------------------"; |
674 "------------inform for x^2+x+1 ----------------------------------"; |