wneuper/isa: test/Tools/isac/OLDTESTS/script

     1 (* 1.if-te-else- 8.02 f"ur Richard

     3    use"ifthenelse.sml";

     4    use"tests/rationals2.sml";

     5    *)

     9 (*---------------- 25.7.02 ---------------------*)

    11 val thy = (theory "Isac_Knowledge");

    12 val t = (Thm.term_of o the o (parse thy)) "contains_root (sqrt(x)=1)";

    13 val SOME(ss,tt) = eval_contains_root "xxx" 1 t thy;

    15 val t = (Thm.term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x";

    16 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;

    18 (*---

    19 val v = (Thm.term_of o the o (parse thy)) "x";

    20 val t = (Thm.term_of o the o (parse thy)) "sqrt(#3+#4*x)";

    21 scan t v;

    22 val t = (Thm.term_of o the o (parse thy)) "sqrt(#3+#4*a)";

    23 scan t v;

    24 val t = (Thm.term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)";

    25 scan t v;

    26 val t = (Thm.term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)";

    27 scan t v;

    28 ---*)

    29 val t = (Thm.term_of o the o (parse thy))

    30 	    "is_rootequation_in (1 + 2*sqrt(3+4*x)=0) x";

    31 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;

    33 val t = (Thm.term_of o the o (parse thy))

    34 	    "is_rootequation_in (x + 2*sqrt(3+4*a)=0) x";

    35 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;

    37 val t = (Thm.term_of o the o (parse Test.thy))

    38 	    "is_rootequation_in (sqrt(x)=1) x";

    39 atomty t;

    40 val t = (Thm.term_of o the o (parse (theory "Isac_Knowledge")))

    41 	    "is_rootequation_in (sqrt(x)=1) x";

    42 atomty t;

    44 (*

    45 val SOME(tt,_) = rewrite_set_ Test.thytrue tval_rls t;

    46 *)

    47 val SOME(tt,_) = rewrite_set_ (theory "Isac_Knowledge") true tval_rls t;

    49 rewrite_set "Isac_Knowledge" true

    50 	    "tval_rls" "is_rootequation_in (sqrt(x)=1) x";

    51 rewrite_set "Test" true

    52 	    "tval_rls" "is_rootequation_in (sqrt(x)=1) x";

    55 (*WN: ^^^--- bitte nimm vorerst immer (theory "Isac_Knowledge"), damit wird richtig gematcht,

    56   siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*)

    58 KEStore_Elems.add_pbts

    59   [Problem.prep_input (*Test.thy*) (theory "Isac_Knowledge")

    60       (["rootX","univariate","equation","test"],

    61         [("#Given" ,["equality e_e","solveFor v_v"]),

    62           ("#Where" ,["is_rootequation_in (e_e::bool) (v_::real)"]),

    63           ("#Find"  ,["solutions v_i_"])],

    64         Rule_Set.append_rules Rule_Set.empty [Eval ("Test.is'_rootequation'_in", eval_is_rootequation_in "")],

    65         [("Test","methode")])]

    66   thy;

    68 M_Match.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (Problem.from_store ["rootX","univariate","equation","test"]);

    70 KEStore_Elems.add_pbts

    71   [Problem.prep_input (theory "Isac_Knowledge")

    72       (["approximate","univariate","equation","test"],

    73         [("#Given", ["equality e_e","solveFor v_v","errorBound err_"]),

    74           ("#Where", ["matches (?a = ?b) e_e"]),

    75           ("#Find", ["solutions v_i_"])],

    76         Rule_Set.append_rules Rule_Set.empty [Eval ("Prog_Expr.matches",eval_matches "#matches_")], [])]

    77   thy;

    79 methods:= overwritel (!methods,

    80 [

    81  Method.prep_input

    82  (("Isac_Knowledge","solve_univar_err"):metID,

    83    [("#Given" ,["equality e_e","solveFor v_v","errorBound err_"]),

    84     ("#Find"  ,["solutions v_i_"])

    85     ],

    86    {rew_ord'="tless_true",rls'="tval_rls",erls=Rule_Set.empty,prls=Rule_Set.empty,calc=[],

    87     asm_rls=[],asm_thm=[]},

    88  "Program Solve_univar_err (e_e::bool) (v_::real) (err_::bool) =  \

    89  \ (if (is_rootequation_in e_e v_v)\

    90  \  then ((SubProblem (IsacX,[squareroot,univariate,equation],\

    91  \         (SqRoot_,square_equation)) [BOOL e_e, REAL v_v, BOOL err_]))\

    92  \  else ((SubProblem (IsacX,[linear,univariate,equation],\

    93  \         (RatArith_,solve_linear)) [BOOL e_e, REAL v_])))"

    94  )]);

    96 val fmz = ["equality (1+2*x=0)","solveFor x","errorBound (eps=0)",

    97 	   "solutions L"];

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

    99   ("Isac_Knowledge",["approximate","univariate","equation","test"],

   100    ("Isac_Knowledge","solve_univar_err"));

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

   102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   105 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   109 (*val nxt = ("Apply_Method",Apply_Method ("Isac_Knowledge","solve_univar_err"))*)

   110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   111 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;

   112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   114 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   119 (*val nxt = ("Apply_Method",Apply_Method ("RatArith","solve_linear"))*)

   120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   125 if f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = -1 / 2]"))

   126    andalso nxt = ("End_Proof'",End_Proof') then ()

   127 else error "new behaviour in testexample rationals2.sml 1+2*x=0";

   129 (*---------------------------------*)

   130 "-------------- is_rootequ_in - SubProblem -------------------------";

   131 "-------------- is_rootequ_in - SubProblem -------------------------";

   132 "-------------- is_rootequ_in - SubProblem -------------------------";

   133 val fmz = ["equality (sqrt(x) - 1 = 0)","solveFor x","errorBound (eps=0)",

   134 	   "solutions L"];

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

   136   ("Isac_Knowledge",["approximate","univariate","equation","test"],

   137    ("Isac_Knowledge","solve_univar_err"));

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

   139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   142 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   143 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   144 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   146 (*val nxt = ("Apply_Method",Apply_Method ("Isac_Knowledge","solve_univar_err"))*)

   147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   148 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;

   149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   152 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   154 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   155 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   156 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   158 if p = ([1,1],Frm) andalso

   159    f = Form' (Test_Out.FormKF (~1,EdUndef,2,Nundef,"sqrt x - 1 = 0")) andalso

   160    nxt = ("Empty_Tac",Empty_Tac) (*script ist noch 'helpless'*) then ()

   161 else error "new behaviour in testexample rationals2.sml sqrt(x) - 1 = 0";

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 15 May 2020 14:22:05 +0200
changeset 59984	08296690e7a6
parent 59973	8a46c2e7c27a
child 59997	46fe5a8c3911
permissions	-rw-r--r--