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/Test_Some.thy
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 07 Sep 2011 10:07:13 +0200
branchdecompose-isar
changeset 42248 ac50595ffe6b
parent 42226 7fff709d1a72
child 42255 6201b34bd323
permissions -rw-r--r--
intermed. pqformula for Z-transform 
     1 (* Title:  run tests on a particular test file

     2    Author: Walther Neuper 101001

     3    (c) copyright due to lincense terms.

     4 12345678901234567890123456789012345678901234567890123456789012345678901234567890

     5         10        20        30        40        50        60        70        80

     6 *)

     7 

     8 theory Test_Some imports Isac begin

     9 

    10 text{*

    11 use"../../../test/Tools/isac/Knowledge/polyeq.sml" 

    12 *}

    13 

    14 ML {*

    15 val c = [];

    16 print_depth 5;

    17 *}

    18 

    19 ML {*

    20 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";

    21 "----- d2_pqformula1 ------!!!!";

    22 val fmz = ["equality (-2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];

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

    24   ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], 

    25    ["PolyEq","solve_d2_polyeq_pq_equation"]);

    26 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

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

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

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

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

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

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

    33 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*f = .. "x = 2 | x = -1", nxt = (". ", Or_to_List)*)

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

    35      (*f = "..[x = 2, x = -1]", nxt = ("..Check_elementwise "Assumptions")*)

    36 *}

    37 ML{*

    38 "~~~~~ fun me, args:"; val (_,tac) = nxt;

    39 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));

    40 val (mI,m) = mk_tac'_ tac; (*m = Check_elementwise "Assumptions"*)

    41 val  Appl m = applicable_in p pt m

    42 *}

    43 ML{*

    44 print_depth 5; PolyML.makestring m

    45 *}

    46 ML{*

    47 val Check_elementwise' (a,b,(c,d)) = m;

    48 term2str a;

    49 term2str c;

    50 terms2str d;

    51 *}

    52 ML{*

    53 print_depth 99; m;

    54 *}

    55 ML{*

    56 *}

    57 ML{*

    58 *}

    59 ML{*

    60 locatetac tac (pt,p)

    61 val it = ("failure", ([], [], (Nd (PblObj {...}, [...]), ([4], ...)))): string * 

    62 *}

    63 ML{* (*error*)

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

    65 

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

    67 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()

    68 	 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";

    69 

    70 "----- d2_pqformula1_neg ------";

    71 

    72 *}

    73 ML{*

    74 val xxx = @{theory};

    75 (writeln o PolyML.makestring) xxx;

    76 *}

    77 ML {*

    78 NotLocatable

    79 *}

    80 ML {*

    81 NasApp (e_scrstate,[])

    82 *}

    83 ML{*

    84 ((writeln o PolyML.makestring) xxx; NasApp (e_scrstate,[]))

    85 *}

    86 text{*

    87 *** NasNap 

    88 (Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $ 

    89   (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 

    90     Free ("x", "RealDef.real") $ 

    91     Free ("2", "RealDef.real")) $ 

    92   (Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $ 

    93     (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 

    94       Free ("x", "RealDef.real") $ 

    95       Free ("-1", "RealDef.real")) $ 

    96     Const ("List.list.Nil", "HOL.bool List.list")), 

    97 

    98 [(Free ("e_e", "HOL.bool"), 

    99     Const ("HOL.disj", "HOL.bool \<Rightarrow> HOL.bool \<Rightarrow> HOL.bool") $ 

   100       (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 

   101         Free ("x", "RealDef.real") $ 

   102         Free ("2", "RealDef.real")) $ 

   103       (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 

   104         Free ("x", "RealDef.real") $ 

   105         Free ("-1", "RealDef.real"))), 

   106   (Free ("v_v", "RealDef.real"), Free ("x", "RealDef.real")), 

   107   (Free ("L_L", "HOL.bool List.list"), 

   108     Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $ 

   109       (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 

   110         Free ("x", "RealDef.real") $ 

   111         Free ("2", "RealDef.real")) $ 

   112     (Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $ 

   113       (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $ 

   114         Free ("x", "RealDef.real") $ 

   115         Free ("-1", "RealDef.real")) $ 

   116       Const ("List.list.Nil", "HOL.bool List.list")))]) 

   117 *}

   118 ML{*

   119 *}

   120 ML{*

   121 *}

   122 ML{*

   123 *}

   124 ML{*

   125 *}

   126 ML{*

   127 "~~~~~ fun , args:"; val () = ();

   128 *}

   129 end

   130 

   131 

   132 (*============ inhibit exn WN110906 ==============================================

   133 ============ inhibit exn WN110906 ==============================================*)

   134 

   135 

   136 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

   137 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

   138
wneuper/isa