Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/algein.sml
author Thomas Leh <t.leh@gmx.at>
Mon, 25 Jul 2011 08:31:53 +0200
branchdecompose-isar
changeset 42195 ac2c5fb8fedd
parent 42166 911c49949ba9
child 42385 b37adb659ffe
permissions -rw-r--r--
tuned 
     1 (* tests on AlgEin, Algebra Einf"uhrung, , Unterrichtsversuch IMST-Projekt

     2    author: Walther Neuper 2007

     3    (c) due to copyright terms

     4 

     5 use"../smltest/IsacKnowledge/algein.sml";

     6 use"algein.sml";

     7 *)

     8 

     9 "-----------------------------------------------------------------";

    10 "table of contents -----------------------------------------------";

    11 "-----------------------------------------------------------------";

    12 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";

    13 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    14 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

    15 "----------- Widerspruch 3 = 777 ---------------------------------";

    16 "-----------------------------------------------------------------";

    17 "-----------------------------------------------------------------";

    18 "-----------------------------------------------------------------";

    19 

    20 val thy = @{theory "AlgEin"};

    21 

    22 

    23 (* use"../smltest/IsacKnowledge/algein.sml";

    24    *)

    25 

    26 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";

    27 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";

    28 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";

    29 val str =

    30 "Script RechnenSymbolScript (k_::bool) (q__::bool) \

    31 \(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\

    32 \ (let t_ = (l_ = 1)\

    33 \ in t_)"

    34 ;

    35 (*=== inhibit exn 110722=============================================================

    36 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

    37 === inhibit exn 110722=============================================================*)

    38 

    39 

    40 (*=== inhibit exn 110722=============================================================

    41 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

    42 

    43 atomty sc;

    44 atomt sc;

    45 === inhibit exn 110722=============================================================*)

    46 

    47 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    48 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    49 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    50 val fmz = 

    51     ["KantenLaenge (k=10)","Querschnitt (q=1)",

    52      "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]", 

    53      "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]", 

    54      "KantenOben  [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",

    55      "GesamtLaenge L"];

    56 val (dI',pI',mI') =

    57   ("Isac",["numerischSymbolische", "Berechnung"],

    58    ["Berechnung","erstNumerisch"]);

    59 val p = e_pos'; val c = [];

    60 (*=== inhibit exn 110722=============================================================

    61 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);

    62 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);

    63 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);

    64 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenUnten [b1 = k - 2*q]"*);

    65 val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenUnten [b2 = k - 2 * q, b3=..b4*);

    66 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenSenkrecht [v1 = k]"*);

    67 val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenSenkrecht [v2 = k, v3 = k, v4]*);

    68 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenOben [b1 = k - 2 *q])*);

    69 val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenOben [b2 = k - 2 * q, b3 =, b4*);

    70 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Find "GesamtLaenge L"*);

    71 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Theory "AlgEin"*);

    72 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Problem ["numerischSymbolis,Be*);

    73 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Method ["Berechnung", "erstSym*);

    74 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Apply_Method*);

    75 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute["Oben = boollist2sum [b1 =*);

    76 f2str f;

    77 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["t1 = k - 2 * q", *);f2str f;

    78 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["k = 10", "q = 1"]*);f2str f;

    79 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Rewrite_Set "norm_Rational"*);f2str f;

    80 val (p,_,f,nxt,_,pt) = me nxt p c pt(**);

    81 if f2str f = "L = 32 + senkrecht + unten" then ()

    82 else error "algein.sml diff.behav. in erstSymbolisch 1";

    83 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;

    84 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;

    85 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;

    86 val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;

    87 val (p,_,f,nxt,_,pt) = me nxt p c pt;

    88 if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()

    89 else error "algein.sml diff.behav. in erstSymbolisch 99";

    90  DEconstrCalcTree 1;

    91 === inhibit exn 110722=============================================================*)

    92 

    93 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

    94 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

    95 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

    96 CalcTree

    97 [(["KantenLaenge (k=10)","Querschnitt (q=1)",

    98    "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]", 

    99    "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]", 

   100    "KantenOben  [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",

   101    "GesamtLaenge L"], 

   102   ("Isac",["numerischSymbolische", "Berechnung"],

   103    ["Berechnung","erstSymbolisch"]))];

   104 Iterator 1;

   105 moveActiveRoot 1;

   106 autoCalculate 1 CompleteCalc;

   107 val ((pt,p),_) = get_calc 1; show_pt pt;

   108 (*=== inhibit exn 110722=============================================================

   109 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()

   110 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";

   111 ===== inhibit exn 110722===========================================================*)

   112 (*

   113 show_pt pt;

   114 trace_rewrite:=true;

   115 trace_rewrite:=false;

   116 trace_script:=true;

   117 trace_script:=false;

   118 *)

   119 "----------- Widerspruch 3 = 777 ---------------------------------";

   120 "----------- Widerspruch 3 = 777 ---------------------------------";

   121 "----------- Widerspruch 3 = 777 ---------------------------------";

   122 val thy = @{theory "Isac"}; 

   123 val rew_ord = dummy_ord;

   124 val erls = Erls;

   125 (*===== inhibit exn 110722===========================================================

   126 val thm = assoc_thm' thy ("sym_real_mult_0_right","");

   127 val t = str2term "0 = 0";

   128 val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;

   129 term2str t';

   130 (********"0 = ?z1 * 0"*)

   131 

   132 (*testing code in ME/appl.sml*)

   133 val sube = ["?z1 = 3"];

   134 val subte = sube2subte sube;

   135 val subst = sube2subst thy sube;

   136 foldl and_ (true, map contains_Var subte);

   137 

   138 val t'' = subst_atomic subst t';

   139 term2str t'';

   140 (********"0 = 3 * 0"*)

   141 ===== inhibit exn 110722===========================================================*)

   142 

   143 val thm = assoc_thm' thy ("sym","");

   144 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!

   145 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';

   146 *)

   147 

   148 (* use"../smltest/IsacKnowledge/algein.sml";

   149    *)

   150
wneuper/isa