intermed. test/../biegelinie.sml
+ meeting dmeindl: Rational2.thy
1.1 --- a/src/Tools/isac/Interpret/ctree.sml Mon Mar 05 13:35:44 2012 +0100
1.2 +++ b/src/Tools/isac/Interpret/ctree.sml Tue Mar 06 14:25:08 2012 +0100
1.3 @@ -226,8 +226,8 @@
1.4 val subte2sube = map term2str;
1.5 val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
1.6 val subst2subs' = map ((apfst term2str) o (apsnd term2str));
1.7 -fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;
1.8 -fun sube2subst thy s = map (dest_equals' o term_of o the o (parse thy)) s;
1.9 +fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;
1.10 +fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;
1.11 val sube2subte = map str2term;
1.12 val subte2subst = map HOLogic.dest_eq;
1.13
2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Mon Mar 05 13:35:44 2012 +0100
2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Tue Mar 06 14:25:08 2012 +0100
2.3 @@ -8,7 +8,7 @@
2.4
2.5 consts
2.6
2.7 - q_ :: "real => real" ("q'_") (* Streckenlast *)
2.8 + qq :: "real => real" (* Streckenlast *)
2.9 Q :: "real => real" (* Querkraft *)
2.10 Q' :: "real => real" (* Ableitung der Querkraft *)
2.11 M'_b :: "real => real" ("M'_b") (* Biegemoment *)
2.12 @@ -58,8 +58,8 @@
2.13
2.14 axioms(*axiomatization where*)
2.15
2.16 - Querkraft_Belastung: "Q' x = -q_ x" (*and*)
2.17 - Belastung_Querkraft: "-q_ x = Q' x" (*and*)
2.18 + Querkraft_Belastung: "Q' x = -qq x" (*and*)
2.19 + Belastung_Querkraft: "-qq x = Q' x" (*and*)
2.20
2.21 Moment_Querkraft: "M_b' x = Q x" (*and*)
2.22 Querkraft_Moment: "Q x = M_b' x" (*and*)
3.1 --- a/src/Tools/isac/Knowledge/Rational2.thy Mon Mar 05 13:35:44 2012 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Rational2.thy Tue Mar 06 14:25:08 2012 +0100
3.3 @@ -6,48 +6,147 @@
3.4 10 20 30 40 50 60 70 80 90 100
3.5 *)
3.6
3.7 -theory Rational2 imports Poly begin
3.8 +theory Rational2 imports Complex_Main begin
3.9
3.10
3.11 -ML {*member op= [1,2,3,4,5] 3;
3.12 -union op= [1,2,3,4,5] [4,5,6,7]*}
3.13 +
3.14 +ML{*(*use modinv(r,m) to get rinv= r^-1 mod m*)
3.15 +fun modi (r, rold, m, rinv) =
3.16 + if rinv < m
3.17 + then
3.18 + if r mod m = 1
3.19 + then ( rinv + 1;
3.20 + rinv)
3.21 + else modi (rold * (rinv+1),rold,m,rinv+1)
3.22 +else (0)
3.23 +(*Errormeldung? es gibt kein Inverses sind nicht Teilerfremd!! schon zu Beginn darauf überprüfen!!*)
3.24 +
3.25 +fun modinv (r,m) = modi (r, r, m, 0);
3.26 +
3.27 +*}
3.28 +
3.29 +ML{*
3.30 +infix modinvWN;
3.31 +fun r modinvWN m = modi (r, r, m, 0);
3.32 +(* chinese remainder theorem *)
3.33 +fun CRA_2WN r1 r2 m1 m2 =
3.34 + (r1 mod m1) + ((r2 - (r1 mod m1)) * (m1 modinvWN m2) mod m2) * m1;
3.35 +*}
3.36 +
3.37 +ML{*
3.38 +modinv(2,5);
3.39 +modinv(3,5);
3.40 +modinv(4,339);
3.41 +4*85
3.42 +*}
3.43 +
3.44 +ML{*
3.45 +(* chinese remainder theorem *)
3.46 +fun CRA_2 (r1 : int, r2 : int, m1 : int, m2 : int)=
3.47 +(*c=m1^-1 mod m2
3.48 + r1'=r1 mod m1
3.49 + s=(r2-r1')*c mod m2
3.50 + r= r1'+s*m1
3.51 + return r*)
3.52 + (r1 mod m1) + ((r2 - (r1 mod m1)) * (modinv (m1, m2)) mod m2) * m1
3.53 +*}
3.54 +ML{*
3.55 +
3.56 +*}
3.57 +ML{*
3.58 +(* old style -- above is better !!! NEW STYLE |> see test/Pure/General/Basics.thy
3.59 +*)
3.60 +fun CRA_2' (r1 : int, r2 : int, m1 : int, m2 : int)=
3.61 + let
3.62 + val c= modinv (m1, m2)
3.63 + val r1'=r1 mod m1
3.64 + val s=(r2-r1')*c mod m2
3.65 + val r= r1'+s*m1
3.66 + in r end;
3.67 +*}
3.68 +ML{*
3.69 +
3.70 +*}
3.71 +ML{*
3.72 +print_depth 999;
3.73 +print_depth 999;
3.74 +*}
3.75 +ML{*
3.76 +CRA_2WN;
3.77 +val intermed_res = CRA_2WN 1 2 3 ;
3.78 +fun yyy f z = f z;
3.79 +yyy;
3.80 +yyy intermed_res; (*evaluation postponed to where it is required*)
3.81 +yyy intermed_res 4;
3.82 +*}
3.83 +ML{*
3.84 +modinv;
3.85 +yyy modinv ;
3.86 +yyy modinv (2 ,3);
3.87 +*}
3.88 +ML{*
3.89 +(1,2) |> modinv
3.90 + |> (curry op+ 2)
3.91 +*}
3.92 +
3.93 +ML{*
3.94 +(*. univariate polynomials (uv) .*)
3.95 +(*. univariate polynomials are represented as a list
3.96 + of the coefficent in reverse maximum degree order .*)
3.97 +(*. 5 * x^5 + 4 * x^3 + 2 * x^2 + x + 19 => [19,1,2,4,0,5] .*)
3.98 +type uv_poly = int list;
3.99 +
3.100 +*}
3.101 +
3.102 +ML{*
3.103 +*}
3.104 +ML{*
3.105 +3 mod 2;
3.106 +((3+5)*5)mod 9;
3.107 +*}
3.108 +ML{*
3.109 +CRA_2(2,6,2,5);
3.110 +modinv(2,5);
3.111 +modinv(3,5);
3.112 +CRA_2(2,6,3,5);
3.113 +6 mod 5;
3.114 +
3.115 +*}
3.116 +ML{*
3.117 +
3.118 +*}
3.119 +
3.120 +
3.121 ML {*
3.122 -type uv_poly = int list;
3.123 +fun div_3_by d = 3 div d;
3.124 +div_3_by 3;
3.125 +(*div_3_by 0*)
3.126 +can;
3.127 +div_3_by;
3.128 +can div_3_by;
3.129 +can div_3_by 0;
3.130 +fun xxx x =
3.131 + if can div_3_by x then div_3_by x else 9999999;
3.132 +xxx 1;
3.133 +xxx 0;
3.134 *}
3.135 ML {*
3.136 -fun uv_mod_null (p1 : int list, 0) = p1
3.137 - | uv_mod_null (p1 : int list, n1 : int) = uv_mod_null (p1, n1 - 1) @ [0];
3.138 +op div;
3.139 +curry op div;
3.140 +fun div' a b =
3.141 + if can (curry op div a) b then SOME (a div b) else NONE
3.142 *}
3.143 ML {*
3.144 -type mv_monom =
3.145 - (int * (* coefficient or the monom *)
3.146 - int list); (* list of exponents) *)
3.147 +perhaps;
3.148 +div' 128;
3.149 +perhaps (div' 128) 8;
3.150 +perhaps (div' 128) 0;
3.151 *}
3.152 ML {*
3.153 -type mv_poly = mv_monom list;
3.154 +val x = SOME 123;
3.155 + the x
3.156 *}
3.157 ML {*
3.158 -EQUAL (* !!! isac --- Isabelle2011 ????*)
3.159 -*}
3.160 -ML {* (*name?*)
3.161 -fun mv_mg_hlp [] = EQUAL
3.162 - | mv_mg_hlp (x :: xs) =
3.163 - if x < 0 then LESS
3.164 - else if x > 0 then GREATER
3.165 - else mv_mg_hlp (xs : uv_poly);
3.166 -*}
3.167 -ML {*
3.168 -mv_mg_hlp [0,0,1,0];
3.169 -mv_mg_hlp [0,0,~1,0];
3.170 -mv_mg_hlp [0,0,0,0];
3.171 -mv_mg_hlp [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,999];
3.172 -mv_mg_hlp [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,~999];
3.173 -*}
3.174 -ML {*
3.175 -mem
3.176 -*}
3.177 -ML {*
3.178 -union
3.179 *}
3.180 ML {*
3.181 *}
4.1 --- a/test/Tools/isac/Knowledge/algein.sml Mon Mar 05 13:35:44 2012 +0100
4.2 +++ b/test/Tools/isac/Knowledge/algein.sml Tue Mar 06 14:25:08 2012 +0100
4.3 @@ -1,9 +1,6 @@
4.4 (* tests on AlgEin, Algebra Einf"uhrung, , Unterrichtsversuch IMST-Projekt
4.5 author: Walther Neuper 2007
4.6 (c) due to copyright terms
4.7 -
4.8 -use"../smltest/IsacKnowledge/algein.sml";
4.9 -use"algein.sml";
4.10 *)
4.11
4.12 "-----------------------------------------------------------------";
4.13 @@ -27,37 +24,28 @@
4.14 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
4.15 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
4.16 val str =
4.17 -"Script RechnenSymbolScript (k_::bool) (q__::bool) \
4.18 -\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
4.19 -\ (let t_ = (l_ = 1)\
4.20 -\ in t_)"
4.21 +"Script RechnenSymbolScript (k_k::bool) (q__q::bool) \
4.22 +\(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =\
4.23 +\ (let t_t = (l_l = 1)\
4.24 +\ in t_t)"
4.25 ;
4.26 -(*=== inhibit exn 110722=============================================================
4.27 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.28 -=== inhibit exn 110722=============================================================*)
4.29 -
4.30 -
4.31 -(*=== inhibit exn 110722=============================================================
4.32 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.33 -
4.34 atomty sc;
4.35 atomt sc;
4.36 -=== inhibit exn 110722=============================================================*)
4.37
4.38 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
4.39 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
4.40 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
4.41 val fmz =
4.42 - ["KantenLaenge (k=10)","Querschnitt (q=1)",
4.43 - "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
4.44 - "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
4.45 - "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
4.46 + ["KantenLaenge (k=(10::real))","Querschnitt (q=(1::real))",
4.47 + "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]",
4.48 + "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]",
4.49 + "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
4.50 "GesamtLaenge L"];
4.51 val (dI',pI',mI') =
4.52 ("Isac",["numerischSymbolische", "Berechnung"],
4.53 ["Berechnung","erstNumerisch"]);
4.54 val p = e_pos'; val c = [];
4.55 -(*=== inhibit exn 110722=============================================================
4.56 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
4.57 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);
4.58 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);
4.59 @@ -88,63 +76,48 @@
4.60 if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
4.61 else error "algein.sml diff.behav. in erstSymbolisch 99";
4.62 DEconstrCalcTree 1;
4.63 -=== inhibit exn 110722=============================================================*)
4.64
4.65 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
4.66 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
4.67 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
4.68 CalcTree
4.69 -[(["KantenLaenge (k=10)","Querschnitt (q=1)",
4.70 - "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
4.71 - "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
4.72 - "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
4.73 - "GesamtLaenge L"],
4.74 +[(["KantenLaenge (k=(10::real))","Querschnitt (q=(1::real))",
4.75 + "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]",
4.76 + "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]",
4.77 + "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
4.78 + "GesamtLaenge L"],
4.79 ("Isac",["numerischSymbolische", "Berechnung"],
4.80 ["Berechnung","erstSymbolisch"]))];
4.81 Iterator 1;
4.82 moveActiveRoot 1;
4.83 autoCalculate 1 CompleteCalc;
4.84 val ((pt,p),_) = get_calc 1; show_pt pt;
4.85 -(*=== inhibit exn 110722=============================================================
4.86 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
4.87 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
4.88 -===== inhibit exn 110722===========================================================*)
4.89 -(*
4.90 -show_pt pt;
4.91 -trace_rewrite:=true;
4.92 -trace_rewrite:=false;
4.93 -trace_script:=true;
4.94 -trace_script:=false;
4.95 -*)
4.96 +
4.97 "----------- Widerspruch 3 = 777 ---------------------------------";
4.98 "----------- Widerspruch 3 = 777 ---------------------------------";
4.99 "----------- Widerspruch 3 = 777 ---------------------------------";
4.100 val thy = @{theory "Isac"};
4.101 val rew_ord = dummy_ord;
4.102 val erls = Erls;
4.103 -(*===== inhibit exn 110722===========================================================
4.104 -val thm = assoc_thm' thy ("sym_real_mult_0_right","");
4.105 -val t = str2term "0 = 0";
4.106 +val thm = assoc_thm' thy ("sym_mult_zero_right","");
4.107 +val t = str2term "0 = (0::real)";
4.108 val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
4.109 -term2str t';
4.110 -(********"0 = ?z1 * 0"*)
4.111 +term2str t' = "0 = ?a1 * 0"; (* = true*)
4.112
4.113 (*testing code in ME/appl.sml*)
4.114 -val sube = ["?z1 = 3"];
4.115 +val sube = ["?a1 = (3::real)"];
4.116 val subte = sube2subte sube;
4.117 +terms2str' subte = "[?a1 = 3]"; (* = true*)
4.118 val subst = sube2subst thy sube;
4.119 foldl and_ (true, map contains_Var subte);
4.120
4.121 val t'' = subst_atomic subst t';
4.122 -term2str t'';
4.123 -(********"0 = 3 * 0"*)
4.124 -===== inhibit exn 110722===========================================================*)
4.125 +term2str t'' = "0 = 3 * 0"; (* = true*)
4.126
4.127 val thm = assoc_thm' thy ("sym","");
4.128 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
4.129 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
4.130 *)
4.131
4.132 -(* use"../smltest/IsacKnowledge/algein.sml";
4.133 - *)
4.134 -
5.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Mon Mar 05 13:35:44 2012 +0100
5.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Tue Mar 06 14:25:08 2012 +0100
5.3 @@ -1,9 +1,6 @@
5.4 (* tests on biegelinie
5.5 author: Walther Neuper 050826
5.6 (c) due to copyright terms
5.7 -
5.8 -use"../smltest/IsacKnowledge/biegelinie.sml";
5.9 -use"biegelinie.sml";
5.10 *)
5.11
5.12 "-----------------------------------------------------------------";
5.13 @@ -25,51 +22,42 @@
5.14 "-----------------------------------------------------------------";
5.15
5.16 val thy = @{theory "Biegelinie"};
5.17 -(*=== inhibit exn 110722=============================================================
5.18 +val ctxt = thy2ctxt' "Biegelinie";
5.19 +fun str2term str = (term_of o the o (parse thy)) str;
5.20 +fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt' "Biegelinie")) t;
5.21 +fun rewrit thm str =
5.22 + fst (the (rewrite_ thy tless_true e_rls true thm str));
5.23
5.24 "----------- the rules -------------------------------------------";
5.25 "----------- the rules -------------------------------------------";
5.26 "----------- the rules -------------------------------------------";
5.27 -fun str2term str = (term_of o the o (parse thy)) str;
5.28 -fun term2s t = Syntax.string_of_term (thy2ctxt' "Biegelinie") t;
5.29 -fun rewrit thm str =
5.30 - fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));
5.31 -
5.32 -val t = rewrit Belastung_Querkraft (str2term "- q_ x = - q_0"); term2s t;
5.33 +val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
5.34 if term2s t = "Q' x = - q_0" then ()
5.35 else error "/biegelinie.sml: Belastung_Querkraft";
5.36
5.37 -val t = rewrit Querkraft_Moment (str2term "Q x = - q_0 * x + c"); term2s t;
5.38 +val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
5.39 if term2s t = "M_b' x = - q_0 * x + c" then ()
5.40 else error "/biegelinie.sml: Querkraft_Moment";
5.41
5.42 -val t = rewrit Moment_Neigung (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
5.43 +val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
5.44 term2s t;
5.45 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
5.46 else error "biegelinie.sml: Moment_Neigung";
5.47 -=== inhibit exn 110722=============================================================*)
5.48 -
5.49 -
5.50 -(*=== inhibit exn 110722=============================================================
5.51 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.52 -
5.53 -atomty sc;
5.54 -atomt sc;
5.55 -=== inhibit exn 110722=============================================================*)
5.56 -
5.57 -(* use"../smltest/IsacKnowledge/biegelinie.sml";
5.58 - *)
5.59
5.60 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
5.61 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
5.62 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
5.63 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
5.64 val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
5.65 -(*=== inhibit exn 110722=============================================================
5.66 -val t = rewrit Moment_Neigung t; term2s t;
5.67 -(*was "EI * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
5.68 - ### before declaring "y''" as a constant *)
5.69 -val t = rewrit make_fun_explicit t; term2s t;
5.70 +val t = rewrit @{thm Moment_Neigung} t;
5.71 +if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then ()
5.72 +else error "Moment_Neigung broken";
5.73 +(* was I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
5.74 + before declaring "y''" as a constant *)
5.75
5.76 +val t = rewrit @{thm make_fun_explicit} t;
5.77 +if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
5.78 +else error "make_fun_explicit broken";
5.79
5.80 "----------- simplify_leaf for this script -----------------------";
5.81 "----------- simplify_leaf for this script -----------------------";
5.82 @@ -78,42 +66,35 @@
5.83 preconds = [],
5.84 rew_ord = ("termlessI",termlessI),
5.85 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
5.86 - [(*for asm in nth_Cons_ ...*)
5.87 + [(*for asm in NTH_CONS ...*)
5.88 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
5.89 - (*2nd nth_Cons_ pushes n+-1 into asms*)
5.90 + (*2nd NTH_CONS pushes n+-1 into asms*)
5.91 Calc("Groups.plus_class.plus", eval_binop "#add_")
5.92 ],
5.93 srls = Erls, calc = [],
5.94 - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
5.95 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
5.96 Calc("Groups.plus_class.plus", eval_binop "#add_"),
5.97 - Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
5.98 - Calc("Tools.lhs", eval_lhs"eval_lhs_"),
5.99 - Calc("Tools.rhs", eval_rhs"eval_rhs_"),
5.100 - Calc("Atools.argument'_in",
5.101 - eval_argument_in "Atools.argument'_in")
5.102 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
5.103 + Calc("Tools.lhs", eval_lhs "eval_lhs_"),
5.104 + Calc("Tools.rhs", eval_rhs "eval_rhs_"),
5.105 + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
5.106 ],
5.107 scr = EmptyScr};
5.108 -=== inhibit exn 110722=============================================================*)
5.109 val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
5.110 val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
5.111 -(*=== inhibit exn 110722=============================================================
5.112 -val SOME (e1__l,_) =
5.113 - rewrite_set_ thy false srls
5.114 - (str2term"(nth_::[real,bool list]=>bool) 1 " $ rm_);
5.115 -if term2str e1__ = "M_b 0 = 0" then ()
5.116 -else error "biegelinie.sml simplify nth_ 1 rm_";
5.117 +val SOME (e1__,_) = rewrite_set_ thy false srls
5.118 + (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
5.119 +if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
5.120
5.121 val SOME (x1__,_) =
5.122 rewrite_set_ thy false srls
5.123 (str2term"argument_in (lhs (M_b 0 = 0))");
5.124 if term2str x1__ = "0" then ()
5.125 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
5.126 -=== inhibit exn 110722=============================================================*)
5.127
5.128 trace_rewrite:=true;
5.129 trace_rewrite:=false;
5.130
5.131 -
5.132 "----------- Bsp 7.27 me -----------------------------------------";
5.133 "----------- Bsp 7.27 me -----------------------------------------";
5.134 "----------- Bsp 7.27 me -----------------------------------------";
5.135 @@ -141,19 +122,21 @@
5.136 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.137 case nxt of (_,Add_Given "FunktionsVariable x") => ()
5.138 | _ => error "biegelinie.sml: Bsp 7.27 #4a";
5.139 +
5.140 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.141 val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
5.142 (*if itms2str_ ctxt mits = ... all 6 guard-items*)
5.143 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
5.144 | _ => error "biegelinie.sml: Bsp 7.27 #4b";
5.145
5.146 -(*=== inhibit exn 110722=============================================================
5.147 +"===== Apply_Method IntegrierenUndKonstanteBestimmen ============================";
5.148 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.149 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
5.150 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
5.151 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.152 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.153
5.154 +(*=== inhibit exn 110722=============================================================
5.155 case nxt of
5.156 (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => ()
5.157 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
5.158 @@ -344,8 +327,6 @@
5.159 | _ => error "biegelinie.sml: Bsp 7.27 #24";
5.160 === inhibit exn 110722=============================================================*)
5.161
5.162 -(* use"../smltest/IsacKnowledge/biegelinie.sml";
5.163 - *)
5.164 show_pt pt;
5.165 (*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
5.166 (([1], Frm), q_ x = q_0),
6.1 --- a/test/Tools/isac/Test_Isac.thy Mon Mar 05 13:35:44 2012 +0100
6.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Mar 06 14:25:08 2012 +0100
6.3 @@ -175,7 +175,7 @@
6.4 use "Knowledge/vect.sml"
6.5 use "Knowledge/diffapp.sml" (*part.*)
6.6 use "Knowledge/biegelinie.sml" (*part.*)
6.7 - use "Knowledge/algein.sml" (*part.*)
6.8 + use "Knowledge/algein.sml"
6.9 use "Knowledge/diophanteq.sml"
6.10 use "Knowledge/isac.sml" (*part.*)
6.11 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
7.1 --- a/test/Tools/isac/Test_Some.thy Mon Mar 05 13:35:44 2012 +0100
7.2 +++ b/test/Tools/isac/Test_Some.thy Tue Mar 06 14:25:08 2012 +0100
7.3 @@ -1,19 +1,125 @@
7.4
7.5 theory Test_Some imports Isac begin
7.6
7.7 -use"../../../test/Tools/isac/Knowledge/partial_fractions.sml"
7.8 +use"../../../test/Tools/isac/Knowledge/biegelinie.sml"
7.9
7.10 ML {*
7.11 +val thy = @{theory "Biegelinie"};
7.12 +*}
7.13 +ML {*
7.14 +val ctxt = thy2ctxt' "Biegelinie";
7.15 +*}
7.16 +ML {*
7.17 +"----------- Bsp 7.27 me -----------------------------------------";
7.18 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
7.19 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
7.20 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
7.21 + "FunktionsVariable x"];
7.22 +val (dI',pI',mI') =
7.23 + ("Biegelinie",["MomentBestimmte","Biegelinien"],
7.24 + ["IntegrierenUndKonstanteBestimmen"]);
7.25 +val p = e_pos'; val c = [];
7.26 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.27 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.28 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.29 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.30 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.31 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.32 +
7.33 +val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
7.34 +(*if itms2str_ ctxt pits = ... all 5 model-items*)
7.35 +val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
7.36 +if itms2str_ ctxt mits = "[]" then ()
7.37 +else error "biegelinie.sml: Bsp 7.27 #2";
7.38 +
7.39 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.40 +case nxt of (_,Add_Given "FunktionsVariable x") => ()
7.41 + | _ => error "biegelinie.sml: Bsp 7.27 #4a";
7.42 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.43 +*}
7.44 +ML {*
7.45 +val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
7.46 +*}
7.47 +ML {*
7.48 +(*if itms2str_ ctxt mits = ... all 6 guard-items*)
7.49 +case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
7.50 + | _ => error "biegelinie.sml: Bsp 7.27 #4b";
7.51 +(*=========================^^^ correct until here ^^^===========================*)
7.52 +*}
7.53 +ML {*
7.54 *}
7.55 ML {*
7.56 *}
7.57 ML {*
7.58 *}
7.59 -ML {* (*==================*)
7.60 +ML {*
7.61 *}
7.62 ML {*
7.63 *}
7.64 ML {*
7.65 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
7.66 +*}
7.67 +ML {*
7.68 +nxt
7.69 +*}
7.70 +ML {*
7.71 +print_depth 999;
7.72 +val ("Empty_Tac", xxx) = nxt; (*<<<-----------------------------------------------*)
7.73 +print_depth 999;
7.74 +*}
7.75 +ML {*
7.76 +*}
7.77 +ML {* (*==================*)
7.78 +"----------- Bsp 7.27 autoCalculate ------------------------------";
7.79 + states:=[];
7.80 + CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
7.81 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
7.82 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
7.83 + "FunktionsVariable x"],
7.84 + ("Biegelinie",
7.85 + ["MomentBestimmte","Biegelinien"],
7.86 + ["IntegrierenUndKonstanteBestimmen"]))];
7.87 + moveActiveRoot 1;
7.88 + autoCalculate 1 CompleteCalcHead;
7.89 +
7.90 + fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
7.91 +(*
7.92 +> val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
7.93 +> is = e_scrstate;
7.94 +val it = true : bool
7.95 +*)
7.96 + autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
7.97 + val ((pt,_),_) = get_calc 1;
7.98 + case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
7.99 + | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
7.100 +
7.101 + autoCalculate 1 CompleteCalc;
7.102 +val ((pt,p),_) = get_calc 1;
7.103 +(*=== inhibit exn 110722=============================================================
7.104 +if p = ([], Res) andalso length (children pt) = 23 andalso
7.105 +term2str (get_obj g_res pt (fst p)) =
7.106 +"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)"
7.107 +then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
7.108 +=== inhibit exn 110722=============================================================*)
7.109 +
7.110 + val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
7.111 + getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
7.112 + show_pt pt;
7.113 +
7.114 +(*check all formulae for getTactic*)
7.115 + getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
7.116 + getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
7.117 + getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
7.118 + getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
7.119 + getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
7.120 + getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
7.121 +*}
7.122 +ML {*
7.123 +*}
7.124 +ML {*
7.125 +
7.126 +*}
7.127 +ML {*
7.128 *}
7.129 ML {* (*==================*)
7.130 *}
7.131 @@ -25,10 +131,12 @@
7.132 end
7.133
7.134
7.135 -(*============ inhibit exn WN120201 ==============================================
7.136 -============ inhibit exn WN120201 ==============================================*)
7.137 +(*============ inhibit exn WN120305 ==============================================
7.138 +============ inhibit exn WN120305 ==============================================*)
7.139
7.140
7.141 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
7.142 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
7.143
7.144 +(*=========================^^^ correct until here ^^^===========================*)
7.145 +
8.1 --- a/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Mon Mar 05 13:35:44 2012 +0100
8.2 +++ b/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Tue Mar 06 14:25:08 2012 +0100
8.3 @@ -1,83 +1,87 @@
8.4 -WN110726 see ~/devel/isac/isac-10/isa2009-2/thms-replace-Isa02-Isa09-2.sml
8.5 - Isabelle2002-isac Isabelle2009-2
8.6 - ok
8.7 - \ to be checked
8.8 - \? still misterious
8.9 - # better would be the *_class.*(n)
8.10 - // no rule outside *_class.*(n)
8.11 -> rlsthmsNOTisac;
8.12 -val it =
8.13 - [("refl", "?t = ?t"), HOL.refl
8.14 - ("o_apply", "(?f o ?g) ?x = ?f (?g ?x)"), Fun.o_apply
8.15 - ("take_Nil", "take ?n [] = []"), List.take_Nil
8.16 - ("take_Cons", List.take_Cons
8.17 - "take ?n (?x # ?xs) =
8.18 - (case ?n of 0 => [] | Suc m => ?x # take m ?xs)"),
8.19 - ("if_True", "(if True then ?x else ?y) = ?x"), HOL.if_True
8.20 ------------------------------------------------------------------------------------------------------------------
8.21 - ("if_False", "(if False then ?x else ?y) = ?y"), HOL.if_False
8.22 - ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1" [.]), \???
8.23 - ("real_add_mult_distrib", Rings.semiring_class.left_distrib
8.24 - "(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"),
8.25 - ("real_add_mult_distrib2", Rings.semiring_class.right_distrib
8.26 - "?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"),
8.27 - ("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2" [.]), !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29)
8.28 ------------------------------------------------------------------------------------------------------------------
8.29 - ("sym_realpow_addI", !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26)
8.30 - "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)" [.]),
8.31 - ("real_mult_1_right", "?z * 1 = ?z"), Groups.monoid_mult_class.mult_1_right
8.32 - ("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
8.33 - -''- //
8.34 - ("real_mult_1", "1 * ?z = ?z"), Groups.monoid_mult_class.mult_1_left
8.35 - ("real_mult_0", "0 * ?z = 0"), Rings.mult_zero_class.mult_zero_left
8.36 ------------------------------------------------------------------------------------------------------------------
8.37 - ("real_mult_0_right", "?z * 0 = 0"), Rings.mult_zero_class.mult_zero_right
8.38 - ("real_add_zero_left", "0 + ?z = ?z"), Groups.monoid_add_class.add_0_left
8.39 - ("real_add_zero_right", "?z + 0 = ?z"), Groups.monoid_add_class.add_0_right
8.40 - ("real_0_divide", "0 / ?x = 0"), Rings.division_ring_class.divide_zero_left
8.41 - ("sym_real_mult_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18) + see sym_rmult_assoc
8.42 - -''- //
8.43 - "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1" [.]),
8.44 ------------------------------------------------------------------------------------------------------------------
8.45 - ("le_refl", "?n <= ?n"), RealDef.real_le_refl
8.46 - ("real_minus_minus", "- (- ?z) = ?z"), Groups.group_add_class.minus_minus
8.47 - ("real_mult_commute", "?z * ?w = ?w * ?z"), RealDef.real_mult_commute
8.48 - ("real_mult_left_commute", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)
8.49 - "?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"),
8.50 - -''- //
8.51 - ("real_mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"), RealDef.real_mult_assoc
8.52 ------------------------------------------------------------------------------------------------------------------
8.53 - ("real_add_commute", "?z + ?w = ?w + ?z"), Groups.ab_semigroup_add_class.add_commute
8.54 - ("real_add_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), Groups.ab_semigroup_add_class.add_left_commute
8.55 - ("real_add_assoc", "?z1.0 + ?z2.0 + ?z3.0 = ?z1.0 + (?z2.0 + ?z3.0)"), Groups.semigroup_add_class.add_assoc
8.56 - ("sym_real_mult_minus_eq1", "- (?x1 * ?y1) = - ?x1 * ?y1" [.]), Rings.ring_class.minus_mult_left
8.57 - ("real_add_minus", "?z + - ?z = 0"), Groups.group_add_class.right_minus
8.58 ------------------------------------------------------------------------------------------------------------------
8.59 - ("sym_real_add_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25) + see sym_radd_assoc
8.60 - "?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1" [.]),
8.61 - -''- //
8.62 - ("sym_real_minus_divide_eq", "- (?x1 / ?y1) = - ?x1 / ?y1" [.]), Rings.division_ring_class.minus_divide_left
8.63 - ("real_times_divide1_eq", "?x * (?y / ?z) = ?x * ?y / ?z"), # Fields.field_class.times_divide_eq(1)
8.64 - -''- ! Rings.division_ring_class.times_divide_eq_right
8.65 - ("real_times_divide2_eq", "?y / ?z * ?x = ?y * ?x / ?z"), Fields.field_class.times_divide_eq_left
8.66 - ("real_divide_divide2_eq", "?x / ?y / ?z = ?x / (?y * ?z)"), Fields.field_inverse_zero_class.divide_divide_eq_left
8.67 ------------------------------------------------------------------------------------------------------------------
8.68 - ("real_divide_divide1_eq", "?x / (?y / ?z) = ?x * ?z / ?y"), Fields.field_inverse_zero_class.divide_divide_eq_right
8.69 - ("real_divide_1", "?x / 1 = ?x"), Rings.division_ring_class.divide_1
8.70 - ("real_diff_mult_distrib", Rings.ring_class.left_diff_distrib
8.71 - "(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"),
8.72 - ("real_diff_mult_distrib2", Rings.ring_class.right_diff_distrib
8.73 - "?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"),
8.74 - ("real_add_divide_distrib", "(?x + ?y) / ?z = ?x / ?z + ?y / ?z"), Rings.division_ring_class.add_divide_distrib
8.75 ------------------------------------------------------------------------------------------------------------------
8.76 - ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), + see sym_real_add_assoc
8.77 - ("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])] + see sym_real_mult_assoc
8.78 -: (thmID * Thm.thm) list
8.79 - "real_divide_minus1", "?x / -1 = - ?x" Int.divide_minus1
8.80 -
8.81 -find_theorems
8.82 -(999) name :
8.83 -(999) simp : "?a * (?b + ?c)"
8.84 -Tobias Nipkow 'searched for' ... "_ + _ + _ = _ + (_ + _)"
8.85 - "_ + (_ + (_::nat)) = _ + _ + _"
8.86 -
8.87 +WN110726 see ~/devel/isac/isac-10/isa2009-2/thms-replace-Isa02-Isa09-2.sml
8.88 + Isabelle2002-isac Isabelle2009-2
8.89 + ok
8.90 + \ to be checked
8.91 + \? still misterious
8.92 + # better would be the *_class.*(n)
8.93 + // no rule outside *_class.*(n)
8.94 +> rlsthmsNOTisac;
8.95 +val it =
8.96 + [("refl", "?t = ?t"), HOL.refl
8.97 + ("o_apply", "(?f o ?g) ?x = ?f (?g ?x)"), Fun.o_apply
8.98 + ("take_Nil", "take ?n [] = []"), List.take_Nil
8.99 + ("take_Cons", List.take_Cons
8.100 + "take ?n (?x # ?xs) =
8.101 + (case ?n of 0 => [] | Suc m => ?x # take m ?xs)"),
8.102 + ("if_True", "(if True then ?x else ?y) = ?x"), HOL.if_True
8.103 +-----------------------------------------------------------------------------------------------------------------
8.104 + ("if_False", "(if False then ?x else ?y) = ?y"), HOL.if_False
8.105 + ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1" [.]), \???
8.106 + ("real_add_mult_distrib", Rings.semiring_class.left_distrib
8.107 + "(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"),
8.108 + ("real_add_mult_distrib2", Rings.semiring_class.right_distrib
8.109 + "?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"),
8.110 + ("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2" [.]), !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29)
8.111 +-----------------------------------------------------------------------------------------------------------------
8.112 + ("sym_realpow_addI", !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26)
8.113 + "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)" [.]),
8.114 + ("real_mult_1_right", "?z * 1 = ?z"), Groups.monoid_mult_class.mult_1_right
8.115 + ("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
8.116 + -''- //
8.117 + ("real_mult_1", "1 * ?z = ?z"), Groups.monoid_mult_class.mult_1_left
8.118 + ("real_mult_0", "0 * ?z = 0"), Rings.mult_zero_class.mult_zero_left
8.119 +-----------------------------------------------------------------------------------------------------------------
8.120 + ("real_mult_0_right", "?z * 0 = 0"), Rings.mult_zero_class.mult_zero_right
8.121 + ("real_add_zero_left", "0 + ?z = ?z"), Groups.monoid_add_class.add_0_left
8.122 + ("real_add_zero_right", "?z + 0 = ?z"), Groups.monoid_add_class.add_0_right
8.123 + ("real_0_divide", "0 / ?x = 0"), Rings.division_ring_class.divide_zero_left
8.124 + ("sym_real_mult_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18) + see sym_rmult_assoc
8.125 + -''- //
8.126 + "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1" [.]),
8.127 +-----------------------------------------------------------------------------------------------------------------
8.128 + ("le_refl", "?n <= ?n"), RealDef.real_le_refl
8.129 + ("real_minus_minus", "- (- ?z) = ?z"), Groups.group_add_class.minus_minus
8.130 + ("real_mult_commute", "?z * ?w = ?w * ?z"), RealDef.real_mult_commute
8.131 + ("real_mult_left_commute", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)
8.132 + "?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"),
8.133 + -''- //
8.134 + ("real_mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"), RealDef.real_mult_assoc
8.135 +-----------------------------------------------------------------------------------------------------------------
8.136 + ("real_add_commute", "?z + ?w = ?w + ?z"), Groups.ab_semigroup_add_class.add_commute
8.137 + ("real_add_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), Groups.ab_semigroup_add_class.add_left_commute
8.138 + ("real_add_assoc", "?z1.0 + ?z2.0 + ?z3.0 = ?z1.0 + (?z2.0 + ?z3.0)"), Groups.semigroup_add_class.add_assoc
8.139 + ("sym_real_mult_minus_eq1", "- (?x1 * ?y1) = - ?x1 * ?y1" [.]), Rings.ring_class.minus_mult_left
8.140 + ("real_add_minus", "?z + - ?z = 0"), Groups.group_add_class.right_minus
8.141 +-----------------------------------------------------------------------------------------------------------------
8.142 + ("sym_real_add_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25) + see sym_radd_assoc
8.143 + "?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1" [.]),
8.144 + -''- //
8.145 + ("sym_real_minus_divide_eq", "- (?x1 / ?y1) = - ?x1 / ?y1" [.]), Rings.division_ring_class.minus_divide_left
8.146 + ("real_times_divide1_eq", "?x * (?y / ?z) = ?x * ?y / ?z"), # Fields.field_class.times_divide_eq(1)
8.147 + -''- ! Rings.division_ring_class.times_divide_eq_right
8.148 + ("real_times_divide2_eq", "?y / ?z * ?x = ?y * ?x / ?z"), Fields.field_class.times_divide_eq_left
8.149 + ("real_divide_divide2_eq", "?x / ?y / ?z = ?x / (?y * ?z)"), Fields.field_inverse_zero_class.divide_divide_eq_left
8.150 +-----------------------------------------------------------------------------------------------------------------
8.151 + ("real_divide_divide1_eq", "?x / (?y / ?z) = ?x * ?z / ?y"), Fields.field_inverse_zero_class.divide_divide_eq_right
8.152 + ("real_divide_1", "?x / 1 = ?x"), Rings.division_ring_class.divide_1
8.153 + ("real_diff_mult_distrib", Rings.ring_class.left_diff_distrib
8.154 + "(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"),
8.155 + ("real_diff_mult_distrib2", Rings.ring_class.right_diff_distrib
8.156 + "?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"),
8.157 + ("real_add_divide_distrib", "(?x + ?y) / ?z = ?x / ?z + ?y / ?z"), Rings.division_ring_class.add_divide_distrib
8.158 +-----------------------------------------------------------------------------------------------------------------
8.159 + ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), + see sym_real_add_assoc
8.160 + ("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])] + see sym_real_mult_assoc
8.161 +: (thmID * Thm.thm) list
8.162 + "real_divide_minus1", "?x / -1 = - ?x" Int.divide_minus1
8.163 +
8.164 +find_theorems
8.165 +(999) name :
8.166 +(999) simp : "?a * (?b + ?c)"
8.167 +Tobias Nipkow 'searched for' ... "_ + _ + _ = _ + (_ + _)"
8.168 + "_ + (_ + (_::nat)) = _ + _ + _"
8.169 +
8.170 +
8.171 +list funs:
8.172 +nth_Cons_ NTH_CONS
8.173 +nth_Nil_ NTH_NIL