1.1 --- a/src/sml/FE-interface/interface.sml Mon Mar 24 17:20:15 2008 +0100
1.2 +++ b/src/sml/FE-interface/interface.sml Mon Mar 24 17:34:31 2008 +0100
1.3 @@ -161,6 +161,7 @@
1.4 end;
1.5
1.6 (*. apply a tactic at a position and update the calc-tree if applicable .*)
1.7 +(*WN080226 java-code is missing, errors smltest/IsacKnowledge/polyminus.sml*)
1.8 (* val (cI, ip, tac) = (1, p, hd appltacs);
1.9 val (cI, ip, tac) = (1, p, (hd (sel_appl_atomic_tacs pt p)));
1.10 *)
2.1 --- a/src/sml/IsacKnowledge/Integrate.ML Mon Mar 24 17:20:15 2008 +0100
2.2 +++ b/src/sml/IsacKnowledge/Integrate.ML Mon Mar 24 17:34:31 2008 +0100
2.3 @@ -51,15 +51,19 @@
2.4
2.5 (*WN080222:*)
2.6 (*("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "#add_new_c_"))
2.7 + add a new c to a term or a fun-equation;
2.8 this is _not in_ the term, because only applied to _whole_ term*)
2.9 -fun eval_add_new_c _ _ (p as (Const ("Integrate.add'_new'_c",_) $ t)) _ =
2.10 - Some ((term2str p) ^ " = " ^ term2str (new_c p),
2.11 - Trueprop $ (mk_equality (p, new_c p)))
2.12 - | eval_add_new_c _ _ (p as (Const ("Integrate.add'_new'_c",_) $ t)) _ =
2.13 - Some ((term2str p) ^ " = " ^ term2str (new_c p),
2.14 - Trueprop $ (mk_equality (p, new_c p)))
2.15 +fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) =
2.16 + let val p' = case p of
2.17 + Const ("op =", T) $ lh $ rh =>
2.18 + Const ("op =", T) $ lh $ mk_add rh (new_c rh)
2.19 + | p => mk_add p (new_c p)
2.20 + in Some ((term2str p) ^ " = " ^ term2str p',
2.21 + Trueprop $ (mk_equality (p, p')))
2.22 + end
2.23 | eval_add_new_c _ _ _ _ = None;
2.24
2.25 +
2.26 (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*)
2.27 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
2.28 $ arg)) _ =
3.1 --- a/src/sml/IsacKnowledge/LogExp.thy Mon Mar 24 17:20:15 2008 +0100
3.2 +++ b/src/sml/IsacKnowledge/LogExp.thy Mon Mar 24 17:34:31 2008 +0100
3.3 @@ -11,7 +11,7 @@
3.4 ln :: "real => real"
3.5 exp :: "real => real" ("E'_ ^^^ _" 80)
3.6
3.7 -(*--------------------------------------------------*)
3.8 +(*--------------------------------------------------*)
3.9 alog :: "[real, real] => real" ("_ log _" 90)
3.10
3.11 (*Script-names*)
4.1 --- a/src/sml/ROOT.ML Mon Mar 24 17:20:15 2008 +0100
4.2 +++ b/src/sml/ROOT.ML Mon Mar 24 17:34:31 2008 +0100
4.3 @@ -94,28 +94,6 @@
4.4 "**** run systests complete ******************************";
4.5 (*TODO copy the whole filestructure from sml to smltest*)
4.6
4.7 -(*----------WN040311 list_rls.sml doesnt work at other pos
4.8 - cd "systest";
4.9 - (*+ check kbtest/diffapp.sml for additional items in met-model*)
4.10 - use"FE-interface.sml";
4.11 - use"auto-inform.sml";
4.12 - use"calculate.sml";
4.13 -val me = meOLD;
4.14 - use"details.sml"; (*can notyet ackn. 'Rewrite_Set "cancel"' *)
4.15 -val me = meNEW; (*see FIXXXXXME.040216*)
4.16 - use"list_rls.sml"; WN040311.doesnt work at other pos
4.17 - use"ptree.sml";
4.18 - use"refine.sml";
4.19 - use"root-equ.sml";
4.20 - use"script.sml";
4.21 - (* use"script_if.sml"; missing: is_rootequation_in*)
4.22 - use"scriptnew.sml";
4.23 - use"subp-rooteq.sml";
4.24 - (*use"testdaten.sml"; no update after dropping 'errorBound'*)
4.25 - "******* systests complete *******";
4.26 - cd "..";
4.27 -----------------------------------------------------------------------*)
4.28 -
4.29 cd"smltest/Scripts";
4.30 use"calculate-float.sml";
4.31 use"calculate.sml";
4.32 @@ -148,7 +126,7 @@
4.33 use"complex.sml";
4.34 use"diff.sml";
4.35 use"diffapp.sml";
4.36 - (*use"integrate.sml";TODO.new_c: cvs before 071227, 11:50*)
4.37 + use"integrate.sml";
4.38 use"equation.sml";
4.39 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
4.40 use"logexp.sml";
4.41 @@ -169,7 +147,7 @@
4.42 use"vect.sml";
4.43 use"wn.sml";
4.44 use"eqsystem.sml";
4.45 - (*use"biegelinie.sml";TODO.new_c: cvs before 071227, 11:50*)
4.46 + use"biegelinie.sml";
4.47 use"algein.sml";
4.48 cd "../..";
4.49 "**** run tests on IsacKnowledge complete ****************";
5.1 --- a/src/sml/RTEST-root.sml Mon Mar 24 17:20:15 2008 +0100
5.2 +++ b/src/sml/RTEST-root.sml Mon Mar 24 17:34:31 2008 +0100
5.3 @@ -57,7 +57,7 @@
5.4 use"complex.sml";
5.5 use"diff.sml";
5.6 use"diffapp.sml";
5.7 - (*use"integrate.sml";TODO.new_c: cvs before 071227, 11:50*)
5.8 + use"integrate.sml";
5.9 use"equation.sml";
5.10 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
5.11 use"logexp.sml";
5.12 @@ -78,7 +78,7 @@
5.13 use"vect.sml";
5.14 use"wn.sml";
5.15 use"eqsystem.sml";
5.16 - (*use"biegelinie.sml";TODO.new_c: cvs before 071227, 11:50*)
5.17 + use"biegelinie.sml";
5.18 use"algein.sml";
5.19 cd "../..";
5.20 "**** run tests on IsacKnowledge complete ****************";
6.1 --- a/src/sml/Scripts/calculate.sml Mon Mar 24 17:20:15 2008 +0100
6.2 +++ b/src/sml/Scripts/calculate.sml Mon Mar 24 17:34:31 2008 +0100
6.3 @@ -218,7 +218,8 @@
6.4 (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e;
6.5 parse thy ""
6.6 *)
6.7 -(*.apply ONLY to (app_num_tr'2 term), app_num_tr'2 (- 4711) --> (-4711).*)
6.8 +(*.get a thm from an op_ somewhere in the term;
6.9 + apply ONLY to (app_num_tr'2 term), app_num_tr'2 (- 4711) --> (-4711).*)
6.10 fun get_calculation_ thy (op_, eval_fn) ct =
6.11 (* val (thy, (op_, eval_fn), ct) =
6.12 (thy, (the (assoc(!calclist',"order_system"))), t);
6.13 @@ -336,6 +337,21 @@
6.14 *)
6.15
6.16
6.17 +(*.get a thm applying an op_ to a term;
6.18 + apply ONLY to (app_num_tr'2 term), app_num_tr'2 (- 4711) --> (-4711).*)
6.19 +(* val (thy, (op_, eval_fn), ct) =
6.20 + (thy, ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"), term);
6.21 + *)
6.22 +fun get_calculation1_ thy ((op_, eval_fn):cal) ct =
6.23 + case eval_fn op_ ct thy of
6.24 + None => None
6.25 + | Some (thmid,t) =>
6.26 + Some (thmid, (make_thm o (cterm_of (sign_of thy))) t);
6.27 +
6.28 +
6.29 +
6.30 +
6.31 +
6.32 (*.substitute bdv in an rls and leave Calc as they are.(*28.10.02*)
6.33 fun inst_thm' subs (Thm (id, thm)) =
6.34 Thm (id, (*read_instantiate throws: *** No such variable in term: ?bdv*)
7.1 --- a/src/sml/Scripts/rewrite.sml Mon Mar 24 17:20:15 2008 +0100
7.2 +++ b/src/sml/Scripts/rewrite.sml Mon Mar 24 17:34:31 2008 +0100
7.3 @@ -173,7 +173,7 @@
7.4 (let val _= if !trace_rewrite andalso i < ! depth then
7.5 writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
7.6 val ct = app_num_tr'2 ct
7.7 - in case get_calculation_ thy cc ct of
7.8 + in case get_calculation1_ thy cc ct of
7.9 None => (ct, asm)
7.10 | Some (thmid, thm') =>
7.11 let
8.1 --- a/src/sml/Scripts/term_G.sml Mon Mar 24 17:20:15 2008 +0100
8.2 +++ b/src/sml/Scripts/term_G.sml Mon Mar 24 17:34:31 2008 +0100
8.3 @@ -1271,3 +1271,12 @@
8.4 | None => (false, t))
8.5 | subst t = (true, if_none (assoc(instl,t)) t)
8.6 in subst t end;
8.7 +
8.8 +(*.add two terms with a type give.*)
8.9 +fun mk_add t1 t2 =
8.10 + let val T1 = type_of t1
8.11 + val T2 = type_of t2
8.12 + in if T1 <> T2 then raise TYPE ("mk_add gets ",[T1, T2],[t1,t2])
8.13 + else (Const ("op +", [T1, T2] ---> T1) $ t1 $ t2)
8.14 + end;
8.15 +
9.1 --- a/src/smltest/IsacKnowledge/biegelinie.sml Mon Mar 24 17:20:15 2008 +0100
9.2 +++ b/src/smltest/IsacKnowledge/biegelinie.sml Mon Mar 24 17:34:31 2008 +0100
9.3 @@ -135,6 +135,25 @@
9.4 "----------- simplify_leaf for this script -----------------------";
9.5 "----------- simplify_leaf for this script -----------------------";
9.6 "----------- simplify_leaf for this script -----------------------";
9.7 +val srls = Rls {id="srls_IntegrierenUnd..",
9.8 + preconds = [],
9.9 + rew_ord = ("termlessI",termlessI),
9.10 + erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
9.11 + [(*for asm in nth_Cons_ ...*)
9.12 + Calc ("op <",eval_equ "#less_"),
9.13 + (*2nd nth_Cons_ pushes n+-1 into asms*)
9.14 + Calc("op +", eval_binop "#add_")
9.15 + ],
9.16 + srls = Erls, calc = [],
9.17 + rules = [Thm ("nth_Cons_",num_str nth_Cons_),
9.18 + Calc("op +", eval_binop "#add_"),
9.19 + Thm ("nth_Nil_",num_str nth_Nil_),
9.20 + Calc("Tools.lhs", eval_lhs"eval_lhs_"),
9.21 + Calc("Tools.rhs", eval_rhs"eval_rhs_"),
9.22 + Calc("Atools.argument'_in",
9.23 + eval_argument_in "Atools.argument'_in")
9.24 + ],
9.25 + scr = EmptyScr};
9.26 val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
9.27 val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
9.28 val Some (e1__,_) =
9.29 @@ -374,9 +393,10 @@
9.30 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.31 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.32 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.33 -if f2str f = "y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n\
9.34 - \(2 * L * q_0 / (-24 * EI) * x ^^^ 3 + \
9.35 - \-1 * q_0 / (-24 * EI) * x ^^^ 4)" then ()
9.36 +if f2str f =
9.37 +"y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n\
9.38 + \(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n\
9.39 + \ -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)" then ()
9.40 else raise error "biegelinie.sml: Bsp 7.27 #24 f";
9.41 case nxt of ("End_Proof'", End_Proof') => ()
9.42 | _ => raise error "biegelinie.sml: Bsp 7.27 #24";
9.43 @@ -454,7 +474,9 @@
9.44 autoCalculate 1 CompleteCalc;
9.45 val ((pt,p),_) = get_calc 1;
9.46 if p = ([], Res) andalso length (children pt) = 23 andalso
9.47 -term2str (get_obj g_res pt (fst p)) = "y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n(2 * L * q_0 / (-24 * EI) * x ^^^ 3 + -1 * q_0 / (-24 * EI) * x ^^^ 4)"then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed";
9.48 +term2str (get_obj g_res pt (fst p)) =
9.49 +"y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
9.50 +then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed";
9.51
9.52 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
9.53 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
9.54 @@ -834,8 +856,9 @@
9.55 | _ => raise error "biegelinie.sml met2 nn";
9.56 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.57 if nxt = ("End_Proof'", End_Proof') andalso f2str f =
9.58 - "[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]" then ()
9.59 -else raise error "biegelinie.sml met2 oo";
9.60 +(* "[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]" *)
9.61 +"[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /\n (-1 * EI * 24),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]"
9.62 +then () else raise error "biegelinie.sml met2 oo";
9.63
9.64 (*
9.65 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
10.1 --- a/src/smltest/IsacKnowledge/integrate.sml Mon Mar 24 17:20:15 2008 +0100
10.2 +++ b/src/smltest/IsacKnowledge/integrate.sml Mon Mar 24 17:34:31 2008 +0100
10.3 @@ -13,7 +13,7 @@
10.4 "-----------------------------------------------------------------";
10.5 "----------- parsing ---------------------------------------------";
10.6 "----------- integrate by rewriting ------------------------------";
10.7 -"----------- test new_c, is_f_x ----------------------------------";
10.8 +"----------- test add_new_c, is_f_x ------------------------------";
10.9 "----------- simplify by ruleset reducing make_ratpoly_in --------";
10.10 "----------- simplify by ruleset extending make_polynomial_in ----";
10.11 "----------- integrate by ruleset --------------------------------";
10.12 @@ -43,9 +43,9 @@
10.13 val t = str2t "Integral x^^^2 D x";
10.14 atomty t;
10.15
10.16 -val t = str2t "M_b x is_f_x";
10.17 +val t = str2t "ff x is_f_x";
10.18 case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
10.19 - | _ => raise error "integrate.sml: parsing: M_b x is_f_x";
10.20 + | _ => raise error "integrate.sml: parsing: ff x is_f_x";
10.21
10.22
10.23 "----------- integrate by rewriting ------------------------------";
10.24 @@ -87,13 +87,31 @@
10.25 val str = rewrit integral_pow (str2t "Integral x^^^3 D x"); term2s str;
10.26
10.27
10.28 -"----------- test new_c, is_f_x ----------------------------------";
10.29 -"----------- test new_c, is_f_x ----------------------------------";
10.30 -"----------- test new_c, is_f_x ----------------------------------";
10.31 -val term = str2t "x^^^2*c + c_2";
10.32 +"----------- test add_new_c, is_f_x ------------------------------";
10.33 +"----------- test add_new_c, is_f_x ------------------------------";
10.34 +"----------- test add_new_c, is_f_x ------------------------------";
10.35 +val term = str2term "x^^^2*c + c_2";
10.36 val cc = new_c term;
10.37 -if term2s cc = "c_3" then () else raise error "integrate.sml: new_c ???";
10.38 +if term2str cc = "c_3" then () else raise error "integrate.sml: new_c ???";
10.39
10.40 +val Some (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
10.41 +if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
10.42 +else raise error "intergrate.sml: diff. eval_add_new_c";
10.43 +
10.44 +val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
10.45 +val Some (thmstr, thm) = get_calculation1_ thy cc term;
10.46 +
10.47 +val Some (t',_) = rewrite_set_ thy true add_new_c term;
10.48 +if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()
10.49 +else raise error "intergrate.sml: diff. rewrite_set add_new_c 1";
10.50 +
10.51 +val term = str2term "ff x = x^^^2*c + c_2";
10.52 +val Some (t',_) = rewrite_set_ thy true add_new_c term;
10.53 +if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()
10.54 +else raise error "intergrate.sml: diff. rewrite_set add_new_c 2";
10.55 +
10.56 +
10.57 +(*WN080222 replace call_new_c with add_new_c----------------------
10.58 val term = str2t "new_c (c * x^^^2 + c_2)";
10.59 val Some (_,t') = eval_new_c 0 0 term 0;
10.60 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
10.61 @@ -109,9 +127,9 @@
10.62 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
10.63 then () else raise error "integrate.sml: matches new_c = True";
10.64
10.65 -val t = str2t "M_b x is_f_x";
10.66 +val t = str2t "ff x is_f_x";
10.67 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t';
10.68 -if term2s t' = "(M_b x is_f_x) = True" then ()
10.69 +if term2s t' = "(ff x is_f_x) = True" then ()
10.70 else raise error "integrate.sml: eval_is_f_x --> true";
10.71
10.72 val t = str2t "q_0/2 * L * x is_f_x";
10.73 @@ -140,10 +158,11 @@
10.74 handle OPTION => str2t "no_rewrite";
10.75
10.76 val t = rewrit call_for_new_c
10.77 - (str2t "M_b x = q_0/2 *L*x"); term2s t;
10.78 + (str2t "ff x = q_0/2 *L*x"); term2s t;
10.79 val t = (rewrit call_for_new_c
10.80 - (str2t "M_b x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
10.81 + (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
10.82 handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite";
10.83 +--------------------------------------------------------------------*)
10.84
10.85
10.86 "----------- simplify by ruleset reducing make_ratpoly_in --------";
10.87 @@ -247,9 +266,9 @@
10.88
10.89 val rls = "simplify_Integral";
10.90 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
10.91 -val str = "M_b x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
10.92 +val str = "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
10.93 val str = rewrit_sinst subs rls str;
10.94 -if str = "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
10.95 +if str = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
10.96 then () else raise error "integrate.sml: diff.behav. in simplify_I #1";
10.97
10.98 val rls = "integration";
10.99 @@ -328,7 +347,7 @@
10.100 if F1_ = F2_ then () else raise error "integrate.sml: unequal find's";
10.101
10.102 val ((dsc as Const ("Integrate.antiDerivativeName", _))
10.103 - $ Free ("M_b", F3_type)) = str2t "antiDerivativeName M_b";
10.104 + $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";
10.105 if is_dsc dsc then () else raise error "integrate.sml: no description";
10.106 if F1_type = F3_type then ()
10.107 else raise error "integrate.sml: unequal types in find's";