1.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML Fri Sep 01 10:15:43 2006 +0200
1.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML Fri Sep 01 15:00:42 2006 +0200
1.3 @@ -6,6 +6,7 @@
1.4 use"IsacKnowledge/Biegelinie.ML";
1.5 use"Biegelinie.ML";
1.6
1.7 +remove_thy"Typefix";
1.8 remove_thy"Biegelinie";
1.9 use_thy"IsacKnowledge/Isac";
1.10 *)
1.11 @@ -108,11 +109,11 @@
1.12 store_pbt
1.13 (prep_pbt Biegelinie.thy "pbl_equ_fromfun" [] e_pblID
1.14 (["makeFunctionTo","equation"],
1.15 - [("#Given" ,["functionEq funs_","substitution subs_"]),
1.16 + [("#Given" ,["functionEq fun_","substitution sub_"]),
1.17 ("#Find" ,["equality equ___"])],
1.18 append_rls "e_rls" e_rls [],
1.19 None,
1.20 - [(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)["",""]]));
1.21 + [["Equation","fromFunction"]]));
1.22
1.23
1.24
1.25 @@ -350,5 +351,43 @@
1.26 "empty_script"
1.27 ));
1.28
1.29 +store_met
1.30 + (prep_met Biegelinie.thy "met_equ" [] e_metID
1.31 + (["Equation"],
1.32 + [],
1.33 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.34 + srls = e_rls,
1.35 + prls=e_rls,
1.36 + crls = Atools_erls, nrls = e_rls},
1.37 +"empty_script"
1.38 +));
1.39 +
1.40 +store_met
1.41 + (prep_met Biegelinie.thy "met_equ_fromfun" [] e_metID
1.42 + (["Equation","fromFunction"],
1.43 + [("#Given" ,["functionEq fun_","substitution sub_"]),
1.44 + ("#Find" ,["equality equ___"])],
1.45 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.46 + srls = append_rls "srls_in_EquationfromFunc" e_rls
1.47 + [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.48 + Calc("Atools.argument'_in",
1.49 + eval_argument_in
1.50 + "Atools.argument'_in")],
1.51 + prls=e_rls,
1.52 + crls = Atools_erls, nrls = e_rls},
1.53 +(*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
1.54 + 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.55 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
1.56 +\ (let fun_ = Take fun_; \
1.57 +\ bdv_ = argument_in (lhs fun_); \
1.58 +\ val_ = argument_in (lhs sub_); \
1.59 +\ equ_ = (Substitute [bdv_ = val_]) fun_; \
1.60 +\ equ_ = (Substitute [sub_]) fun_ \
1.61 +\ in (Rewrite_Set norm_Poly False) equ_) "
1.62 +(*FIXME.WN060901.ERROR in nxt_tac without Take above !?!*)
1.63 +));
1.64 +
1.65 +
1.66 +
1.67 (* use"Biegelinie.ML";
1.68 *)
1.69 \ No newline at end of file
2.1 --- a/src/sml/IsacKnowledge/Biegelinie.thy Fri Sep 01 10:15:43 2006 +0200
2.2 +++ b/src/sml/IsacKnowledge/Biegelinie.thy Fri Sep 01 15:00:42 2006 +0200
2.3 @@ -12,7 +12,7 @@
2.4 use_thy"IsacKnowledge/Isac";
2.5 *)
2.6
2.7 -Biegelinie = Integrate + EqSystem +
2.8 +Biegelinie = Integrate + Equation + EqSystem +
2.9
2.10 consts
2.11
3.1 --- a/src/sml/IsacKnowledge/Equation.thy Fri Sep 01 10:15:43 2006 +0200
3.2 +++ b/src/sml/IsacKnowledge/Equation.thy Fri Sep 01 15:00:42 2006 +0200
3.3 @@ -21,4 +21,9 @@
3.4 solve :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)
3.5 solveTest :: "[bool * 'a] => bool list" (* for test collection *)
3.6
3.7 + (*Script-names*)
3.8 + Function2Equality :: "[bool, bool, bool] \
3.9 + \=> bool"
3.10 + ("((Script Function2Equality (_ _ =))// (_))" 9)
3.11 +
3.12 end
3.13 \ No newline at end of file
4.1 --- a/src/sml/ME/mathengine.sml Fri Sep 01 10:15:43 2006 +0200
4.2 +++ b/src/sml/ME/mathengine.sml Fri Sep 01 15:00:42 2006 +0200
4.3 @@ -161,10 +161,10 @@
4.4
4.5 (*iterated by nxt_me; there (the resulting) ptp dropped
4.6 may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
4.7 +(* val (ptp as (pt, pos as (p,p_))) = ptp;
4.8 + val (ptp as (pt, pos as (p,p_))) = (pt,ip);
4.9 + *)
4.10 fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
4.11 -(* val (ptp as (pt, pos as (p,p_))) = ptp;
4.12 - (*1*)val (ptp as (pt, pos as (p,p_))) = (pt,ip);
4.13 - *)
4.14 let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
4.15 probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
4.16 in if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
4.17 @@ -227,10 +227,10 @@
4.18 arg ip:
4.19 calcstate
4.20 .*)
4.21 -(* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
4.22 - val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);
4.23 - (*1*)val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
4.24 +(* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);
4.25 + val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
4.26 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (pos, cs);
4.27 + val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
4.28 *)
4.29 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
4.30 let val pIopt = get_pblID (pt,ip);
4.31 @@ -253,7 +253,7 @@
4.32 | _ => (case pIopt of
4.33 None => ("no-fmz-spec", ([], [], ptp))
4.34 | Some pI =>
4.35 -(* (*1*)val Some pI = pIopt;
4.36 +(* val Some pI = pIopt;
4.37 val cs = (if p_ mem [Pbl,Met] andalso is_none (get_obj g_env pt (fst p))
4.38 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
4.39 handle _ => ([], ptp);
4.40 @@ -454,10 +454,10 @@
4.41 NEW loeschen, eigene Version von locatetac, step
4.42 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
4.43
4.44 -
4.45 +(* val ((_,tac), p, _, pt) = (nxt, p, c, pt);
4.46 + *)
4.47 fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
4.48 -(* val (_,tac) = nxt;
4.49 - *) let val (pt, p) =
4.50 + let val (pt, p) =
4.51 (* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p);
4.52 f2str (TESTg_form (pt', p'));
4.53 (writeln o (itms2str thy)) (get_obj g_pbl pt' (fst p'));
4.54 @@ -481,7 +481,9 @@
4.55 | ("no-fmz-spec",_) => raise error "no-fmz-spec"
4.56 | ("end-of-calculation", (ts, _, _)) => ("",ts))
4.57 handle _ => raise error "sys-error";
4.58 - val tac = case ts of tacis as (_::_) =>
4.59 + val tac = case ts of tacis as (_::_) =>
4.60 +(* val tacis as (_::_) = ts;
4.61 + *)
4.62 let val (tac,_,_) = last_elem tacis
4.63 in tac end
4.64 | _ => if p = ([],Res) then End_Proof'
5.1 --- a/src/sml/ME/script.sml Fri Sep 01 10:15:43 2006 +0200
5.2 +++ b/src/sml/ME/script.sml Fri Sep 01 15:00:42 2006 +0200
5.3 @@ -1984,6 +1984,7 @@
5.4 | is_spec_pos Met = true
5.5 | is_spec_pos _ = false;
5.6
5.7 +(*..*)
5.8 fun sel_rules _ (([],Res):pos') =
5.9 raise PTREE "no tactics applicable at the end of a calculation"
5.10 | sel_rules pt (p,p_) =
6.1 --- a/src/sml/ME/solve.sml Fri Sep 01 10:15:43 2006 +0200
6.2 +++ b/src/sml/ME/solve.sml Fri Sep 01 15:00:42 2006 +0200
6.3 @@ -422,6 +422,7 @@
6.4 val (ptp as (pt, pos as (p,p_))) = ptp'';
6.5 val (ptp as (pt, pos as (p,p_))) = (pt,ip);
6.6 val (ptp as (pt, pos as (p,p_))) = ptp;
6.7 + val (ptp as (pt, pos as (p,p_))) = (pt, pos);
6.8 *)
6.9 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
6.10 if e_metID = get_obj g_metID pt (par_pblobj pt p)
7.1 --- a/src/smltest/IsacKnowledge/biegelinie.sml Fri Sep 01 10:15:43 2006 +0200
7.2 +++ b/src/smltest/IsacKnowledge/biegelinie.sml Fri Sep 01 15:00:42 2006 +0200
7.3 @@ -470,9 +470,69 @@
7.4 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
7.5 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
7.6 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
7.7 +val str =
7.8 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
7.9 +\(equ___::bool)"
7.10 +;
7.11 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.12 +val str =
7.13 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
7.14 +\ (let v_ = argument_in (lhs fun_)\
7.15 +\ in (equ___::bool))"
7.16 +;
7.17 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.18 +val str =
7.19 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
7.20 +\ (let v_ = argument_in (lhs fun_);\
7.21 +\ (equ_) = (Substitute [sub_]) fun_\
7.22 +\ in (equ_::bool))"
7.23 +;
7.24 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.25 +val str =
7.26 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
7.27 +\ (let v_ = argument_in (lhs fun_);\
7.28 +\ equ_ = (Substitute [sub_]) fun_\
7.29 +\ in (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False) equ_)"
7.30 +;
7.31 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.32 +(*---^^^-OK-----------------------------------------------------------------*)
7.33 +val str =
7.34 +(*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
7.35 + 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
7.36 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
7.37 +\ (let bdv_ = argument_in (lhs fun_);\
7.38 +\ val_ = argument_in (lhs sub_);\
7.39 +\ equ_ = (Substitute [bdv_ = val_]) fun_;\
7.40 +\ equ_ = (Substitute [sub_]) fun_\
7.41 +\ in (Rewrite_Set_Inst [(bdv_, v_)] make_ratpoly_in False) equ_)"
7.42 +;
7.43 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.44 +(*---vvv-NOTok--------------------------------------------------------------*)
7.45 +atomty sc;
7.46
7.47 +val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
7.48 + "substitution (M_b L = 0)",
7.49 + "equality equ___"];
7.50 +val (dI',pI',mI') = ("Biegelinie.thy", ["makeFunctionTo","equation"],
7.51 + ["Equation","fromFunction"]);
7.52 +val p = e_pos'; val c = [];
7.53 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.54 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.55 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.56 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.57 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.58
7.59 -
7.60 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.61 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
7.62 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.63 + "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
7.64 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.65 + "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
7.66 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
7.67 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
7.68 +if nxt = ("End_Proof'", End_Proof') andalso
7.69 + f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2"
7.70 +then () else raise error "biegelinie.sml: SubProblem (_,[setzeRandbed";
7.71
7.72
7.73 "----------- IntegrierenUndKonstanteBestimmen2 -------------------";
7.74 @@ -574,7 +634,15 @@
7.75 | _ => raise error "biegelinie.sml met2 d";
7.76
7.77
7.78 -
7.79 +(* WRONG returnvalue from (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung])....
7.80 +"
7.81 +[Q' x = - q_0,
7.82 +M_b' x = c + -1 * q_0 * x,\n
7.83 +y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4),\n
7.84 +y' x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n
7.85 +y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)
7.86 +]"
7.87 +*)
7.88
7.89 (*
7.90 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;