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 Walther Neuper <neuper@ist.tugraz.at>
Wed, 08 Sep 2010 16:47:22 +0200
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37960 ec20007095f2
child 38031 460c24a6a6ba
permissions -rw-r--r--
tuned src + test

find . -type f -exec sed -i s/nadd_divide_distrib/add_divide_distrib/g {} \;
find . -type f -exec sed -i s/"\.thy\""/"\""/g {} \;
find . -type f -exec sed -i s/" indexname_ord"/" Term_Ord.indexname_ord"/g {} \;
find . -type f -exec sed -i s/"(string_of_cterm o cterm_of(sign_of thy))"/"(Syntax.string_of_term (thy2ctxt thy))"/g {} \;
find . -type f -exec sed -i s/" L_"/" L_L"/g {} \;
find . -type f -exec sed -i s/" L_:"/" L_L:"/g {} \;
find . -type f -exec sed -i s/"e_;"/"e_e;"/g {} \;
find . -type f -exec sed -i s/"v_)"/"v_v)"/g {} \;
find . -type f -exec sed -i s/"v_:"/"v_v:"/g {} \; 
     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 val thy = AlgEin.thy;

     9 

    10 "-----------------------------------------------------------------";

    11 "table of contents -----------------------------------------------";

    12 "-----------------------------------------------------------------";

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

    14 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    15 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

    16 "----------- Widerspruch 3 = 777 ---------------------------------";

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

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

    19 "-----------------------------------------------------------------";

    20 

    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 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

    36 (*---^^^-OK-----------------------------------------------------------------*)

    37 val str =

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

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

    40 \ (let t_ = Take (l_ = Oben + Senkrecht + Unten);            \

    41 \      sum_ = boollist2sum o_;\

    42 \      t_ = Substitute [Oben = sum_] t_;\

    43 \      t_ = Substitute o_ t_;\

    44 \      t_ = Substitute [k_, q__] t_;\

    45 \      t_ = Repeat (Try (Rewrite_Set norm_Poly False)) t_\

    46 \ in t_)"

    47 ;

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

    49 (*---vvv-NOTok--------------------------------------------------------------*)

    50 

    51 

    52 

    53 atomty sc;

    54 atomt sc;

    55 

    56 

    57 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    58 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    59 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    60 val fmz = 

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

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

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

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

    65      "GesamtLaenge L"];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    85 f2str f;

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

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

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

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

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

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

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

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

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

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

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

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

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

    99 

   100 

   101 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

   102 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

   103 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

   104 states:=[];

   105 CalcTree

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

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

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

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

   110    "GesamtLaenge L"], 

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

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

   113 Iterator 1;

   114 moveActiveRoot 1;

   115 autoCalculate 1 CompleteCalc;

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

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

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

   119 

   120 (*

   121 show_pt pt;

   122 trace_rewrite:=true;

   123 trace_rewrite:=false;

   124 trace_script:=true;

   125 trace_script:=false;

   126 *)

   127 

   128 "----------- Widerspruch 3 = 777 ---------------------------------";

   129 "----------- Widerspruch 3 = 777 ---------------------------------";

   130 "----------- Widerspruch 3 = 777 ---------------------------------";

   131 val thy = Isac.thy; 

   132 val rew_ord = dummy_ord;

   133 val erls = Erls;

   134 

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

   136 val t = str2term "0 = 0";

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

   138 term2str t';

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

   140 

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

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

   143 val subte = sube2subte sube;

   144 val subst = sube2subst thy sube;

   145 foldl and_ (true, map contains_Var subte);

   146 

   147 val t'' = subst_atomic subst t';

   148 term2str t'';

   149 (********"0 = 3 * 0"*)

   150 

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

   152 (*----- GOON Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!

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

   154 *)

   155 

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

   157    *)

   158
wneuper/isa