# HG changeset patch # User Walther Neuper # Date 1331040308 -3600 # Node ID b37adb659ffed69999e71733bef5a2d9a62b9c67 # Parent cc5ba197f1b07768c1aa45b6aab950dad9397fb4 intermed. test/../biegelinie.sml + meeting dmeindl: Rational2.thy diff -r cc5ba197f1b0 -r b37adb659ffe src/Tools/isac/Interpret/ctree.sml --- a/src/Tools/isac/Interpret/ctree.sml Mon Mar 05 13:35:44 2012 +0100 +++ b/src/Tools/isac/Interpret/ctree.sml Tue Mar 06 14:25:08 2012 +0100 @@ -226,8 +226,8 @@ val subte2sube = map term2str; val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str)); val subst2subs' = map ((apfst term2str) o (apsnd term2str)); -fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s; -fun sube2subst thy s = map (dest_equals' o term_of o the o (parse thy)) s; +fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s; +fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s; val sube2subte = map str2term; val subte2subst = map HOLogic.dest_eq; diff -r cc5ba197f1b0 -r b37adb659ffe src/Tools/isac/Knowledge/Biegelinie.thy --- a/src/Tools/isac/Knowledge/Biegelinie.thy Mon Mar 05 13:35:44 2012 +0100 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Tue Mar 06 14:25:08 2012 +0100 @@ -8,7 +8,7 @@ consts - q_ :: "real => real" ("q'_") (* Streckenlast *) + qq :: "real => real" (* Streckenlast *) Q :: "real => real" (* Querkraft *) Q' :: "real => real" (* Ableitung der Querkraft *) M'_b :: "real => real" ("M'_b") (* Biegemoment *) @@ -58,8 +58,8 @@ axioms(*axiomatization where*) - Querkraft_Belastung: "Q' x = -q_ x" (*and*) - Belastung_Querkraft: "-q_ x = Q' x" (*and*) + Querkraft_Belastung: "Q' x = -qq x" (*and*) + Belastung_Querkraft: "-qq x = Q' x" (*and*) Moment_Querkraft: "M_b' x = Q x" (*and*) Querkraft_Moment: "Q x = M_b' x" (*and*) diff -r cc5ba197f1b0 -r b37adb659ffe src/Tools/isac/Knowledge/Rational2.thy --- a/src/Tools/isac/Knowledge/Rational2.thy Mon Mar 05 13:35:44 2012 +0100 +++ b/src/Tools/isac/Knowledge/Rational2.thy Tue Mar 06 14:25:08 2012 +0100 @@ -6,48 +6,147 @@ 10 20 30 40 50 60 70 80 90 100 *) -theory Rational2 imports Poly begin +theory Rational2 imports Complex_Main begin -ML {*member op= [1,2,3,4,5] 3; -union op= [1,2,3,4,5] [4,5,6,7]*} + +ML{*(*use modinv(r,m) to get rinv= r^-1 mod m*) +fun modi (r, rold, m, rinv) = + if rinv < m + then + if r mod m = 1 + then ( rinv + 1; + rinv) + else modi (rold * (rinv+1),rold,m,rinv+1) +else (0) +(*Errormeldung? es gibt kein Inverses sind nicht Teilerfremd!! schon zu Beginn darauf überprüfen!!*) + +fun modinv (r,m) = modi (r, r, m, 0); + +*} + +ML{* +infix modinvWN; +fun r modinvWN m = modi (r, r, m, 0); +(* chinese remainder theorem *) +fun CRA_2WN r1 r2 m1 m2 = + (r1 mod m1) + ((r2 - (r1 mod m1)) * (m1 modinvWN m2) mod m2) * m1; +*} + +ML{* +modinv(2,5); +modinv(3,5); +modinv(4,339); +4*85 +*} + +ML{* +(* chinese remainder theorem *) +fun CRA_2 (r1 : int, r2 : int, m1 : int, m2 : int)= +(*c=m1^-1 mod m2 + r1'=r1 mod m1 + s=(r2-r1')*c mod m2 + r= r1'+s*m1 + return r*) + (r1 mod m1) + ((r2 - (r1 mod m1)) * (modinv (m1, m2)) mod m2) * m1 +*} +ML{* + +*} +ML{* +(* old style -- above is better !!! NEW STYLE |> see test/Pure/General/Basics.thy +*) +fun CRA_2' (r1 : int, r2 : int, m1 : int, m2 : int)= + let + val c= modinv (m1, m2) + val r1'=r1 mod m1 + val s=(r2-r1')*c mod m2 + val r= r1'+s*m1 + in r end; +*} +ML{* + +*} +ML{* +print_depth 999; +print_depth 999; +*} +ML{* +CRA_2WN; +val intermed_res = CRA_2WN 1 2 3 ; +fun yyy f z = f z; +yyy; +yyy intermed_res; (*evaluation postponed to where it is required*) +yyy intermed_res 4; +*} +ML{* +modinv; +yyy modinv ; +yyy modinv (2 ,3); +*} +ML{* +(1,2) |> modinv + |> (curry op+ 2) +*} + +ML{* +(*. univariate polynomials (uv) .*) +(*. univariate polynomials are represented as a list + of the coefficent in reverse maximum degree order .*) +(*. 5 * x^5 + 4 * x^3 + 2 * x^2 + x + 19 => [19,1,2,4,0,5] .*) +type uv_poly = int list; + +*} + +ML{* +*} +ML{* +3 mod 2; +((3+5)*5)mod 9; +*} +ML{* +CRA_2(2,6,2,5); +modinv(2,5); +modinv(3,5); +CRA_2(2,6,3,5); +6 mod 5; + +*} +ML{* + +*} + + ML {* -type uv_poly = int list; +fun div_3_by d = 3 div d; +div_3_by 3; +(*div_3_by 0*) +can; +div_3_by; +can div_3_by; +can div_3_by 0; +fun xxx x = + if can div_3_by x then div_3_by x else 9999999; +xxx 1; +xxx 0; *} ML {* -fun uv_mod_null (p1 : int list, 0) = p1 - | uv_mod_null (p1 : int list, n1 : int) = uv_mod_null (p1, n1 - 1) @ [0]; +op div; +curry op div; +fun div' a b = + if can (curry op div a) b then SOME (a div b) else NONE *} ML {* -type mv_monom = - (int * (* coefficient or the monom *) - int list); (* list of exponents) *) +perhaps; +div' 128; +perhaps (div' 128) 8; +perhaps (div' 128) 0; *} ML {* -type mv_poly = mv_monom list; +val x = SOME 123; + the x *} ML {* -EQUAL (* !!! isac --- Isabelle2011 ????*) -*} -ML {* (*name?*) -fun mv_mg_hlp [] = EQUAL - | mv_mg_hlp (x :: xs) = - if x < 0 then LESS - else if x > 0 then GREATER - else mv_mg_hlp (xs : uv_poly); -*} -ML {* -mv_mg_hlp [0,0,1,0]; -mv_mg_hlp [0,0,~1,0]; -mv_mg_hlp [0,0,0,0]; -mv_mg_hlp [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,999]; -mv_mg_hlp [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,~999]; -*} -ML {* -mem -*} -ML {* -union *} ML {* *} diff -r cc5ba197f1b0 -r b37adb659ffe test/Tools/isac/Knowledge/algein.sml --- a/test/Tools/isac/Knowledge/algein.sml Mon Mar 05 13:35:44 2012 +0100 +++ b/test/Tools/isac/Knowledge/algein.sml Tue Mar 06 14:25:08 2012 +0100 @@ -1,9 +1,6 @@ (* tests on AlgEin, Algebra Einf"uhrung, , Unterrichtsversuch IMST-Projekt author: Walther Neuper 2007 (c) due to copyright terms - -use"../smltest/IsacKnowledge/algein.sml"; -use"algein.sml"; *) "-----------------------------------------------------------------"; @@ -27,37 +24,28 @@ "----------- build method 'Berechnung' 'erstSymbolisch' ----------"; "----------- build method 'Berechnung' 'erstSymbolisch' ----------"; val str = -"Script RechnenSymbolScript (k_::bool) (q__::bool) \ -\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\ -\ (let t_ = (l_ = 1)\ -\ in t_)" +"Script RechnenSymbolScript (k_k::bool) (q__q::bool) \ +\(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =\ +\ (let t_t = (l_l = 1)\ +\ in t_t)" ; -(*=== inhibit exn 110722============================================================= val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; -=== inhibit exn 110722=============================================================*) - - -(*=== inhibit exn 110722============================================================= -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; - atomty sc; atomt sc; -=== inhibit exn 110722=============================================================*) "----------- me 'Berechnung' 'erstNumerisch' ---------------------"; "----------- me 'Berechnung' 'erstNumerisch' ---------------------"; "----------- me 'Berechnung' 'erstNumerisch' ---------------------"; val fmz = - ["KantenLaenge (k=10)","Querschnitt (q=1)", - "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]", - "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]", - "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]", + ["KantenLaenge (k=(10::real))","Querschnitt (q=(1::real))", + "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]", + "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]", + "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]", "GesamtLaenge L"]; val (dI',pI',mI') = ("Isac",["numerischSymbolische", "Berechnung"], ["Berechnung","erstNumerisch"]); val p = e_pos'; val c = []; -(*=== inhibit exn 110722============================================================= val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*); val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*); val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*); @@ -88,63 +76,48 @@ if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then () else error "algein.sml diff.behav. in erstSymbolisch 99"; DEconstrCalcTree 1; -=== inhibit exn 110722=============================================================*) "----------- auto 'Berechnung' 'erstSymbolisch' ------------------"; "----------- auto 'Berechnung' 'erstSymbolisch' ------------------"; "----------- auto 'Berechnung' 'erstSymbolisch' ------------------"; CalcTree -[(["KantenLaenge (k=10)","Querschnitt (q=1)", - "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]", - "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]", - "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]", - "GesamtLaenge L"], +[(["KantenLaenge (k=(10::real))","Querschnitt (q=(1::real))", + "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]", + "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]", + "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]", + "GesamtLaenge L"], ("Isac",["numerischSymbolische", "Berechnung"], ["Berechnung","erstSymbolisch"]))]; Iterator 1; moveActiveRoot 1; autoCalculate 1 CompleteCalc; val ((pt,p),_) = get_calc 1; show_pt pt; -(*=== inhibit exn 110722============================================================= if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then() else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed"; -===== inhibit exn 110722===========================================================*) -(* -show_pt pt; -trace_rewrite:=true; -trace_rewrite:=false; -trace_script:=true; -trace_script:=false; -*) + "----------- Widerspruch 3 = 777 ---------------------------------"; "----------- Widerspruch 3 = 777 ---------------------------------"; "----------- Widerspruch 3 = 777 ---------------------------------"; val thy = @{theory "Isac"}; val rew_ord = dummy_ord; val erls = Erls; -(*===== inhibit exn 110722=========================================================== -val thm = assoc_thm' thy ("sym_real_mult_0_right",""); -val t = str2term "0 = 0"; +val thm = assoc_thm' thy ("sym_mult_zero_right",""); +val t = str2term "0 = (0::real)"; val SOME (t',_) = rewrite_ thy rew_ord erls false thm t; -term2str t'; -(********"0 = ?z1 * 0"*) +term2str t' = "0 = ?a1 * 0"; (* = true*) (*testing code in ME/appl.sml*) -val sube = ["?z1 = 3"]; +val sube = ["?a1 = (3::real)"]; val subte = sube2subte sube; +terms2str' subte = "[?a1 = 3]"; (* = true*) val subst = sube2subst thy sube; foldl and_ (true, map contains_Var subte); val t'' = subst_atomic subst t'; -term2str t''; -(********"0 = 3 * 0"*) -===== inhibit exn 110722===========================================================*) +term2str t'' = "0 = 3 * 0"; (* = true*) val thm = assoc_thm' thy ("sym",""); (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!! val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t''; *) -(* use"../smltest/IsacKnowledge/algein.sml"; - *) - diff -r cc5ba197f1b0 -r b37adb659ffe test/Tools/isac/Knowledge/biegelinie.sml --- a/test/Tools/isac/Knowledge/biegelinie.sml Mon Mar 05 13:35:44 2012 +0100 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Tue Mar 06 14:25:08 2012 +0100 @@ -1,9 +1,6 @@ (* tests on biegelinie author: Walther Neuper 050826 (c) due to copyright terms - -use"../smltest/IsacKnowledge/biegelinie.sml"; -use"biegelinie.sml"; *) "-----------------------------------------------------------------"; @@ -25,51 +22,42 @@ "-----------------------------------------------------------------"; val thy = @{theory "Biegelinie"}; -(*=== inhibit exn 110722============================================================= +val ctxt = thy2ctxt' "Biegelinie"; +fun str2term str = (term_of o the o (parse thy)) str; +fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt' "Biegelinie")) t; +fun rewrit thm str = + fst (the (rewrite_ thy tless_true e_rls true thm str)); "----------- the rules -------------------------------------------"; "----------- the rules -------------------------------------------"; "----------- the rules -------------------------------------------"; -fun str2term str = (term_of o the o (parse thy)) str; -fun term2s t = Syntax.string_of_term (thy2ctxt' "Biegelinie") t; -fun rewrit thm str = - fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str)); - -val t = rewrit Belastung_Querkraft (str2term "- q_ x = - q_0"); term2s t; +val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t; if term2s t = "Q' x = - q_0" then () else error "/biegelinie.sml: Belastung_Querkraft"; -val t = rewrit Querkraft_Moment (str2term "Q x = - q_0 * x + c"); term2s t; +val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t; if term2s t = "M_b' x = - q_0 * x + c" then () else error "/biegelinie.sml: Querkraft_Moment"; -val t = rewrit Moment_Neigung (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x"); +val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x"); term2s t; if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then () else error "biegelinie.sml: Moment_Neigung"; -=== inhibit exn 110722=============================================================*) - - -(*=== inhibit exn 110722============================================================= -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; - -atomty sc; -atomt sc; -=== inhibit exn 110722=============================================================*) - -(* use"../smltest/IsacKnowledge/biegelinie.sml"; - *) "----------- IntegrierenUndKonstanteBestimmen by rewriting -------"; "----------- IntegrierenUndKonstanteBestimmen by rewriting -------"; "----------- IntegrierenUndKonstanteBestimmen by rewriting -------"; +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------"; val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"; -(*=== inhibit exn 110722============================================================= -val t = rewrit Moment_Neigung t; term2s t; -(*was "EI * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" - ### before declaring "y''" as a constant *) -val t = rewrit make_fun_explicit t; term2s t; +val t = rewrit @{thm Moment_Neigung} t; +if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then () +else error "Moment_Neigung broken"; +(* was I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" + before declaring "y''" as a constant *) +val t = rewrit @{thm make_fun_explicit} t; +if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then () +else error "make_fun_explicit broken"; "----------- simplify_leaf for this script -----------------------"; "----------- simplify_leaf for this script -----------------------"; @@ -78,42 +66,35 @@ preconds = [], rew_ord = ("termlessI",termlessI), erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls - [(*for asm in nth_Cons_ ...*) + [(*for asm in NTH_CONS ...*) Calc ("Orderings.ord_class.less",eval_equ "#less_"), - (*2nd nth_Cons_ pushes n+-1 into asms*) + (*2nd NTH_CONS pushes n+-1 into asms*) Calc("Groups.plus_class.plus", eval_binop "#add_") ], srls = Erls, calc = [], - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), Calc("Groups.plus_class.plus", eval_binop "#add_"), - Thm ("nth_Nil_",num_str @{thm nth_Nil_}), - Calc("Tools.lhs", eval_lhs"eval_lhs_"), - Calc("Tools.rhs", eval_rhs"eval_rhs_"), - Calc("Atools.argument'_in", - eval_argument_in "Atools.argument'_in") + Thm ("NTH_NIL",num_str @{thm NTH_NIL}), + Calc("Tools.lhs", eval_lhs "eval_lhs_"), + Calc("Tools.rhs", eval_rhs "eval_rhs_"), + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in") ], scr = EmptyScr}; -=== inhibit exn 110722=============================================================*) val rm_ = str2term"[M_b 0 = 0, M_b L = 0]"; val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2"; -(*=== inhibit exn 110722============================================================= -val SOME (e1__l,_) = - rewrite_set_ thy false srls - (str2term"(nth_::[real,bool list]=>bool) 1 " $ rm_); -if term2str e1__ = "M_b 0 = 0" then () -else error "biegelinie.sml simplify nth_ 1 rm_"; +val SOME (e1__,_) = rewrite_set_ thy false srls + (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_); +if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_"; val SOME (x1__,_) = rewrite_set_ thy false srls (str2term"argument_in (lhs (M_b 0 = 0))"); if term2str x1__ = "0" then () else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)"; -=== inhibit exn 110722=============================================================*) trace_rewrite:=true; trace_rewrite:=false; - "----------- Bsp 7.27 me -----------------------------------------"; "----------- Bsp 7.27 me -----------------------------------------"; "----------- Bsp 7.27 me -----------------------------------------"; @@ -141,19 +122,21 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; case nxt of (_,Add_Given "FunktionsVariable x") => () | _ => error "biegelinie.sml: Bsp 7.27 #4a"; + val (p,_,f,nxt,_,pt) = me nxt p c pt; val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits); (*if itms2str_ ctxt mits = ... all 6 guard-items*) case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () | _ => error "biegelinie.sml: Bsp 7.27 #4b"; -(*=== inhibit exn 110722============================================================= +"===== Apply_Method IntegrierenUndKonstanteBestimmen ============================"; val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*)) | _ => error "biegelinie.sml: Bsp 7.27 #4c"; val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; +(*=== inhibit exn 110722============================================================= case nxt of (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => () | _ => error "biegelinie.sml: Bsp 7.27 #4c"; @@ -344,8 +327,6 @@ | _ => error "biegelinie.sml: Bsp 7.27 #24"; === inhibit exn 110722=============================================================*) -(* use"../smltest/IsacKnowledge/biegelinie.sml"; - *) show_pt pt; (*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])), (([1], Frm), q_ x = q_0), diff -r cc5ba197f1b0 -r b37adb659ffe test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Mon Mar 05 13:35:44 2012 +0100 +++ b/test/Tools/isac/Test_Isac.thy Tue Mar 06 14:25:08 2012 +0100 @@ -175,7 +175,7 @@ use "Knowledge/vect.sml" use "Knowledge/diffapp.sml" (*part.*) use "Knowledge/biegelinie.sml" (*part.*) - use "Knowledge/algein.sml" (*part.*) + use "Knowledge/algein.sml" use "Knowledge/diophanteq.sml" use "Knowledge/isac.sml" (*part.*) ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*} diff -r cc5ba197f1b0 -r b37adb659ffe test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Mon Mar 05 13:35:44 2012 +0100 +++ b/test/Tools/isac/Test_Some.thy Tue Mar 06 14:25:08 2012 +0100 @@ -1,19 +1,125 @@ theory Test_Some imports Isac begin -use"../../../test/Tools/isac/Knowledge/partial_fractions.sml" +use"../../../test/Tools/isac/Knowledge/biegelinie.sml" ML {* +val thy = @{theory "Biegelinie"}; +*} +ML {* +val ctxt = thy2ctxt' "Biegelinie"; +*} +ML {* +"----------- Bsp 7.27 me -----------------------------------------"; +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y", + "RandbedingungenBiegung [y 0 = 0, y L = 0]", + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]", + "FunktionsVariable x"]; +val (dI',pI',mI') = + ("Biegelinie",["MomentBestimmte","Biegelinien"], + ["IntegrierenUndKonstanteBestimmen"]); +val p = e_pos'; val c = []; +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; + +val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits); +(*if itms2str_ ctxt pits = ... all 5 model-items*) +val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits); +if itms2str_ ctxt mits = "[]" then () +else error "biegelinie.sml: Bsp 7.27 #2"; + +val (p,_,f,nxt,_,pt) = me nxt p c pt; +case nxt of (_,Add_Given "FunktionsVariable x") => () + | _ => error "biegelinie.sml: Bsp 7.27 #4a"; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +*} +ML {* +val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits); +*} +ML {* +(*if itms2str_ ctxt mits = ... all 6 guard-items*) +case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () + | _ => error "biegelinie.sml: Bsp 7.27 #4b"; +(*=========================^^^ correct until here ^^^===========================*) +*} +ML {* *} ML {* *} ML {* *} -ML {* (*==================*) +ML {* *} ML {* *} ML {* +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; +*} +ML {* +nxt +*} +ML {* +print_depth 999; +val ("Empty_Tac", xxx) = nxt; (*<<<-----------------------------------------------*) +print_depth 999; +*} +ML {* +*} +ML {* (*==================*) +"----------- Bsp 7.27 autoCalculate ------------------------------"; + states:=[]; + CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y", + "RandbedingungenBiegung [y 0 = 0, y L = 0]", + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]", + "FunktionsVariable x"], + ("Biegelinie", + ["MomentBestimmte","Biegelinien"], + ["IntegrierenUndKonstanteBestimmen"]))]; + moveActiveRoot 1; + autoCalculate 1 CompleteCalcHead; + + fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*); +(* +> val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis; +> is = e_scrstate; +val it = true : bool +*) + autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*); + val ((pt,_),_) = get_calc 1; + case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*)) + | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c"; + + autoCalculate 1 CompleteCalc; +val ((pt,p),_) = get_calc 1; +(*=== inhibit exn 110722============================================================= +if p = ([], Res) andalso length (children pt) = 23 andalso +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 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)" +then () else error "biegelinie.sml: 1st biegelin.7.27 changed"; +=== inhibit exn 110722=============================================================*) + + val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res)); + getFormulaeFromTo 1 unc gen 1 (*only level 1*) false; + show_pt pt; + +(*check all formulae for getTactic*) + getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*); + getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*); + getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*); + getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*); + getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*); + getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*); +*} +ML {* +*} +ML {* + +*} +ML {* *} ML {* (*==================*) *} @@ -25,10 +131,12 @@ end -(*============ inhibit exn WN120201 ============================================== -============ inhibit exn WN120201 ==============================================*) +(*============ inhibit exn WN120305 ============================================== +============ inhibit exn WN120305 ==============================================*) (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) +(*=========================^^^ correct until here ^^^===========================*) + diff -r cc5ba197f1b0 -r b37adb659ffe test/Tools/isac/thms-survey-Isa02-Isa09-2.sml --- a/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Mon Mar 05 13:35:44 2012 +0100 +++ b/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Tue Mar 06 14:25:08 2012 +0100 @@ -1,83 +1,87 @@ -WN110726 see ~/devel/isac/isac-10/isa2009-2/thms-replace-Isa02-Isa09-2.sml - Isabelle2002-isac Isabelle2009-2 - ok - \ to be checked - \? still misterious - # better would be the *_class.*(n) - // no rule outside *_class.*(n) -> rlsthmsNOTisac; -val it = - [("refl", "?t = ?t"), HOL.refl - ("o_apply", "(?f o ?g) ?x = ?f (?g ?x)"), Fun.o_apply - ("take_Nil", "take ?n [] = []"), List.take_Nil - ("take_Cons", List.take_Cons - "take ?n (?x # ?xs) = - (case ?n of 0 => [] | Suc m => ?x # take m ?xs)"), - ("if_True", "(if True then ?x else ?y) = ?x"), HOL.if_True ------------------------------------------------------------------------------------------------------------------ - ("if_False", "(if False then ?x else ?y) = ?y"), HOL.if_False - ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1" [.]), \??? - ("real_add_mult_distrib", Rings.semiring_class.left_distrib - "(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"), - ("real_add_mult_distrib2", Rings.semiring_class.right_distrib - "?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"), - ("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2" [.]), !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29) ------------------------------------------------------------------------------------------------------------------ - ("sym_realpow_addI", !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26) - "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)" [.]), - ("real_mult_1_right", "?z * 1 = ?z"), Groups.monoid_mult_class.mult_1_right - ("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1" [.]), #!^! Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(4): ?m + ?m = ((1::?'a) + (1::?'a)) * ?m - -''- // - ("real_mult_1", "1 * ?z = ?z"), Groups.monoid_mult_class.mult_1_left - ("real_mult_0", "0 * ?z = 0"), Rings.mult_zero_class.mult_zero_left ------------------------------------------------------------------------------------------------------------------ - ("real_mult_0_right", "?z * 0 = 0"), Rings.mult_zero_class.mult_zero_right - ("real_add_zero_left", "0 + ?z = ?z"), Groups.monoid_add_class.add_0_left - ("real_add_zero_right", "?z + 0 = ?z"), Groups.monoid_add_class.add_0_right - ("real_0_divide", "0 / ?x = 0"), Rings.division_ring_class.divide_zero_left - ("sym_real_mult_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18) + see sym_rmult_assoc - -''- // - "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1" [.]), ------------------------------------------------------------------------------------------------------------------ - ("le_refl", "?n <= ?n"), RealDef.real_le_refl - ("real_minus_minus", "- (- ?z) = ?z"), Groups.group_add_class.minus_minus - ("real_mult_commute", "?z * ?w = ?w * ?z"), RealDef.real_mult_commute - ("real_mult_left_commute", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19) - "?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"), - -''- // - ("real_mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"), RealDef.real_mult_assoc ------------------------------------------------------------------------------------------------------------------ - ("real_add_commute", "?z + ?w = ?w + ?z"), Groups.ab_semigroup_add_class.add_commute - ("real_add_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), Groups.ab_semigroup_add_class.add_left_commute - ("real_add_assoc", "?z1.0 + ?z2.0 + ?z3.0 = ?z1.0 + (?z2.0 + ?z3.0)"), Groups.semigroup_add_class.add_assoc - ("sym_real_mult_minus_eq1", "- (?x1 * ?y1) = - ?x1 * ?y1" [.]), Rings.ring_class.minus_mult_left - ("real_add_minus", "?z + - ?z = 0"), Groups.group_add_class.right_minus ------------------------------------------------------------------------------------------------------------------ - ("sym_real_add_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25) + see sym_radd_assoc - "?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1" [.]), - -''- // - ("sym_real_minus_divide_eq", "- (?x1 / ?y1) = - ?x1 / ?y1" [.]), Rings.division_ring_class.minus_divide_left - ("real_times_divide1_eq", "?x * (?y / ?z) = ?x * ?y / ?z"), # Fields.field_class.times_divide_eq(1) - -''- ! Rings.division_ring_class.times_divide_eq_right - ("real_times_divide2_eq", "?y / ?z * ?x = ?y * ?x / ?z"), Fields.field_class.times_divide_eq_left - ("real_divide_divide2_eq", "?x / ?y / ?z = ?x / (?y * ?z)"), Fields.field_inverse_zero_class.divide_divide_eq_left ------------------------------------------------------------------------------------------------------------------ - ("real_divide_divide1_eq", "?x / (?y / ?z) = ?x * ?z / ?y"), Fields.field_inverse_zero_class.divide_divide_eq_right - ("real_divide_1", "?x / 1 = ?x"), Rings.division_ring_class.divide_1 - ("real_diff_mult_distrib", Rings.ring_class.left_diff_distrib - "(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"), - ("real_diff_mult_distrib2", Rings.ring_class.right_diff_distrib - "?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"), - ("real_add_divide_distrib", "(?x + ?y) / ?z = ?x / ?z + ?y / ?z"), Rings.division_ring_class.add_divide_distrib ------------------------------------------------------------------------------------------------------------------ - ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), + see sym_real_add_assoc - ("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])] + see sym_real_mult_assoc -: (thmID * Thm.thm) list - "real_divide_minus1", "?x / -1 = - ?x" Int.divide_minus1 - -find_theorems -(999) name : -(999) simp : "?a * (?b + ?c)" -Tobias Nipkow 'searched for' ... "_ + _ + _ = _ + (_ + _)" - "_ + (_ + (_::nat)) = _ + _ + _" - +WN110726 see ~/devel/isac/isac-10/isa2009-2/thms-replace-Isa02-Isa09-2.sml + Isabelle2002-isac Isabelle2009-2 + ok + \ to be checked + \? still misterious + # better would be the *_class.*(n) + // no rule outside *_class.*(n) +> rlsthmsNOTisac; +val it = + [("refl", "?t = ?t"), HOL.refl + ("o_apply", "(?f o ?g) ?x = ?f (?g ?x)"), Fun.o_apply + ("take_Nil", "take ?n [] = []"), List.take_Nil + ("take_Cons", List.take_Cons + "take ?n (?x # ?xs) = + (case ?n of 0 => [] | Suc m => ?x # take m ?xs)"), + ("if_True", "(if True then ?x else ?y) = ?x"), HOL.if_True +----------------------------------------------------------------------------------------------------------------- + ("if_False", "(if False then ?x else ?y) = ?y"), HOL.if_False + ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1" [.]), \??? + ("real_add_mult_distrib", Rings.semiring_class.left_distrib + "(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"), + ("real_add_mult_distrib2", Rings.semiring_class.right_distrib + "?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"), + ("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2" [.]), !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29) +----------------------------------------------------------------------------------------------------------------- + ("sym_realpow_addI", !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26) + "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)" [.]), + ("real_mult_1_right", "?z * 1 = ?z"), Groups.monoid_mult_class.mult_1_right + ("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1" [.]), #!^! Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(4): ?m + ?m = ((1::?'a) + (1::?'a)) * ?m + -''- // + ("real_mult_1", "1 * ?z = ?z"), Groups.monoid_mult_class.mult_1_left + ("real_mult_0", "0 * ?z = 0"), Rings.mult_zero_class.mult_zero_left +----------------------------------------------------------------------------------------------------------------- + ("real_mult_0_right", "?z * 0 = 0"), Rings.mult_zero_class.mult_zero_right + ("real_add_zero_left", "0 + ?z = ?z"), Groups.monoid_add_class.add_0_left + ("real_add_zero_right", "?z + 0 = ?z"), Groups.monoid_add_class.add_0_right + ("real_0_divide", "0 / ?x = 0"), Rings.division_ring_class.divide_zero_left + ("sym_real_mult_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18) + see sym_rmult_assoc + -''- // + "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1" [.]), +----------------------------------------------------------------------------------------------------------------- + ("le_refl", "?n <= ?n"), RealDef.real_le_refl + ("real_minus_minus", "- (- ?z) = ?z"), Groups.group_add_class.minus_minus + ("real_mult_commute", "?z * ?w = ?w * ?z"), RealDef.real_mult_commute + ("real_mult_left_commute", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19) + "?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"), + -''- // + ("real_mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"), RealDef.real_mult_assoc +----------------------------------------------------------------------------------------------------------------- + ("real_add_commute", "?z + ?w = ?w + ?z"), Groups.ab_semigroup_add_class.add_commute + ("real_add_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), Groups.ab_semigroup_add_class.add_left_commute + ("real_add_assoc", "?z1.0 + ?z2.0 + ?z3.0 = ?z1.0 + (?z2.0 + ?z3.0)"), Groups.semigroup_add_class.add_assoc + ("sym_real_mult_minus_eq1", "- (?x1 * ?y1) = - ?x1 * ?y1" [.]), Rings.ring_class.minus_mult_left + ("real_add_minus", "?z + - ?z = 0"), Groups.group_add_class.right_minus +----------------------------------------------------------------------------------------------------------------- + ("sym_real_add_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25) + see sym_radd_assoc + "?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1" [.]), + -''- // + ("sym_real_minus_divide_eq", "- (?x1 / ?y1) = - ?x1 / ?y1" [.]), Rings.division_ring_class.minus_divide_left + ("real_times_divide1_eq", "?x * (?y / ?z) = ?x * ?y / ?z"), # Fields.field_class.times_divide_eq(1) + -''- ! Rings.division_ring_class.times_divide_eq_right + ("real_times_divide2_eq", "?y / ?z * ?x = ?y * ?x / ?z"), Fields.field_class.times_divide_eq_left + ("real_divide_divide2_eq", "?x / ?y / ?z = ?x / (?y * ?z)"), Fields.field_inverse_zero_class.divide_divide_eq_left +----------------------------------------------------------------------------------------------------------------- + ("real_divide_divide1_eq", "?x / (?y / ?z) = ?x * ?z / ?y"), Fields.field_inverse_zero_class.divide_divide_eq_right + ("real_divide_1", "?x / 1 = ?x"), Rings.division_ring_class.divide_1 + ("real_diff_mult_distrib", Rings.ring_class.left_diff_distrib + "(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"), + ("real_diff_mult_distrib2", Rings.ring_class.right_diff_distrib + "?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"), + ("real_add_divide_distrib", "(?x + ?y) / ?z = ?x / ?z + ?y / ?z"), Rings.division_ring_class.add_divide_distrib +----------------------------------------------------------------------------------------------------------------- + ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), + see sym_real_add_assoc + ("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])] + see sym_real_mult_assoc +: (thmID * Thm.thm) list + "real_divide_minus1", "?x / -1 = - ?x" Int.divide_minus1 + +find_theorems +(999) name : +(999) simp : "?a * (?b + ?c)" +Tobias Nipkow 'searched for' ... "_ + _ + _ = _ + (_ + _)" + "_ + (_ + (_::nat)) = _ + _ + _" + + +list funs: +nth_Cons_ NTH_CONS +nth_Nil_ NTH_NIL