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 wneuper <Walther.Neuper@jku.at>
Thu, 04 Aug 2022 12:48:37 +0200
changeset 60509 2e0b7ca391dc
parent 60500 59a3af532717
child 60549 c0a775618258
permissions -rw-r--r--
polish naming in Rewrite_Order 
     1 (* tests on AlgEin, Algebra Einf"uhrung, , Unterrichtsversuch IMST-Projekt

     2    author: Walther Neuper 2007

     3    (c) due to copyright terms

     4 *)

     5 

     6 "-----------------------------------------------------------------";

     7 "table of contents -----------------------------------------------";

     8 "-----------------------------------------------------------------";

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

    10 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    11 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

    12 "----------- Widerspruch 3 = 777 ---------------------------------";

    13 "-----------------------------------------------------------------";

    14 "-----------------------------------------------------------------";

    15 "-----------------------------------------------------------------";

    16 

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

    18 val ctxt = Proof_Context.init_global thy;

    19 

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

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

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

    23 val str =

    24 "Program RechnenSymbolScript (k_k::bool) (q__q::bool) \

    25 \(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =\

    26 \ (let t_t = (l_l = 1)\

    27 \ in t_t)"

    28 ;

    29 val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;

    30 TermC.atomty sc;

    31 atomt sc;

    32 

    33 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    34 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    35 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";

    36 val fmz = 

    37     ["KantenLaenge (k=(10::real))", "Querschnitt (q=(1::real))",

    38      "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]", 

    39      "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]", 

    40      "KantenOben  [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",

    41      "GesamtLaenge L"];

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

    43   ("Isac_Knowledge",["numerischSymbolische", "Berechnung"],

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    61 f2str f;

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

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

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

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

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

    67 else error "algein.sml diff.behav. in erstNumerisch 1";

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

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

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

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

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

    73 if f2str f = "L = 104"

    74 then case nxt of End_Proof' => ()

    75   | _ => error "algein.sml diff.behav. in erstNumerisch 99 1"

    76 else error "algein.sml diff.behav. in erstNumerisch 99 2";

    77 DEconstrCalcTree 1;

    78 

    79 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

    80 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

    81 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

    82 CalcTree

    83 [(["KantenLaenge (k=(10::real))", "Querschnitt (q=(1::real))",

    84      "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]", 

    85      "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]", 

    86      "KantenOben  [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",

    87      "GesamtLaenge L"], 

    88   ("Isac_Knowledge",["numerischSymbolische", "Berechnung"],

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

    90 Iterator 1;

    91 moveActiveRoot 1;

    92 autoCalculate 1 CompleteCalc;

    93 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;

    94 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "L = 104" then()

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

    96 

    97 "----------- Widerspruch 3 = 777 ---------------------------------";

    98 "----------- Widerspruch 3 = 777 ---------------------------------";

    99 "----------- Widerspruch 3 = 777 ---------------------------------";

   100 val thy = @{theory "Isac_Knowledge"}; 

   101 val ctxt = Proof_Context.init_global thy;

   102 val rew_ord = Rewrite_Ord.function_empty;

   103 val erls = Rule_Set.Empty;

   104 val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";

   105 val t = TermC.str2term "0 = (0::real)";

   106 val SOME (t',_) = rewrite_ ctxt rew_ord erls false thm t;

   107 UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)

   108 

   109 val sube = ["?a1 = (3::real)"];

   110 val subte = Subst.input_to_terms sube;

   111 UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*)

   112 val subst = Subst.T_from_string_eqs thy sube;

   113 foldl and_ (true, map TermC.contains_Var subte);

   114 

   115 val t'' = subst_atomic subst t';

   116 UnparseC.term t'' = "0 = 3 * 0"; (* = true*)

   117 

   118 val thm = ThmC.thm_from_thy thy "sym";

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

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

   121 *)

   122
wneuper/isa