Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/Test.sml
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 08 Sep 2010 16:47:22 +0200
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37982 66f3570ba808
child 37992 351a9e94c38d
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 val ttt = (term_of o the o (parse thy))

     2 "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e";

     3 val ttt = (term_of o the o (parse thy))

     4 "(Try (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e)";

     5 

     6 val ttt = (term_of o the o (parse thy))

     7  "(Rewrite_Set SqRoot_simplify False) e_e ";

     8 val ttt = (term_of o the o (parseold thy))

     9  "%e_. (Rewrite_Set SqRoot_simplify False) e_e";

    10 val ttt = (term_of o the o (parseold thy))

    11  "Repeat (%e_. (Rewrite_Set SqRoot_simplify False)) e_e";

    12 

    13 val ttt = (term_of o the o (parse thy))

    14  "Script Solve_linear (e_e::bool) (v_v::real)=             \

    15  \[e_]";

    16 val ttt = (term_of o the o (parse thy))

    17  "Script Solve_linear (e_e::bool) (v_v::real)=             \

    18  \((%e_. [e_]) e_e)";

    19 val ttt = (term_of o the o (parse thy))

    20  "Script Solve_linear (e_e::bool) (v_v::real)=             \

    21  \((%e_. (let e_e = e_e in [e_])) e_e)";

    22 val ttt = (term_of o the o (parse thy))

    23  "Script Solve_linear (e_e::bool) (v_v::real)=             \

    24  \((%e_. \

    25  \  (let e_e = ((Rewrite_Set SqRoot_simplify False) e_e)\

    26  \   in [e_]))\

    27  \  e_e)";

    28 val ttt = (term_of o the o (parse thy))

    29  "Script Solve_linear (e_e::bool) (v_v::real)=             \

    30  \((%ee_. (let e_e = ((Rewrite_Set SqRoot_simplify False) ee_) in [e_])) e_e)";

    31 

    32 val ttt = (term_of o the o (parse thy))

    33  "Script Solve_linear (e_e::bool) (v_v::real)=             \

    34  \(let e_e = \

    35  \   (Repeat ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False)) e_e)\

    36  \ in [e_])";

    37 (*----*)

    38 val ttt = (term_of o the o (parse thy))

    39 

    40 (*----*)

    41 val ttt = (term_of o the o (parse thy))

    42  "Script Solve_linear (e_e::bool) (v_v::real)=             \

    43  \(let e_e = \

    44  \  (Repeat\

    45  \    ((%ee_. (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\

    46  \      e_e)\

    47  \    e_e)\

    48  \ in [e_])";

    49 val ttt = (term_of o the o (parse thy))

    50  "Script Solve_linear (e_e::bool) (v_v::real)=             \

    51  \(let e_e = \

    52  \  (Repeat\

    53  \    ((%ee_.\

    54  \        ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_))\

    55  \      e_e)\

    56  \    e_e)\

    57  \ in [e_])";

    58 val ttt = (term_of o the o (parse thy))

    59  "Script Solve_linear (e_e::bool) (v_v::real)=             \

    60  \(let e_e = \

    61  \  (Repeat\

    62  \    ((%ee_.\

    63  \        (let e_e = ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) ee_)\

    64  \         in ((Rewrite_Set SqRoot_simplify False) e_e)) )\

    65  \      e_e)\

    66  \    e_e)\

    67  \ in [e_])";

    68 atomty ttt;

    69 atomt ttt;

    70 

    71 val ttt = (term_of o the o (parse thy))

    72  "Script Testterm (g_::real) =   \

    73  \Repeat\

    74  \  (Rewrite rmult_1 False) g_";

    75 val ttt = (term_of o the o (parse thy))

    76  "Script Testterm (g_::real) =   \

    77  \Repeat\

    78  \  (((Rewrite rmult_1 False)) Or ((Rewrite rmult_0 False))) g_";

    79 val ttt = (term_of o the o (parse thy))

    80  "Script Testterm (g_::real) =   \

    81  \Repeat\

    82  \  ((Repeat (Rewrite rmult_1 False)) Or (Repeat (Rewrite rmult_0 False))) g_";

    83 val ttt = (term_of o the o (parse thy))

    84  "Script Testterm (g_::real) =   \

    85  \Repeat\

    86  \  ((Repeat (Rewrite rmult_1 False)) Or\

    87  \   (Repeat (Rewrite rmult_0 False))) g_";

    88 val ttt = (term_of o the o (parse thy))

    89  "Script Testterm (g_::real) =   \

    90  \Repeat\

    91  \  ((Repeat (Rewrite rmult_1 False)) Or\

    92  \   (Repeat (Rewrite rmult_0 False)) Or\

    93  \   (Repeat (Rewrite rmult_0 False))) g_";

    94 val ttt = (term_of o the o (parse thy))

    95  "Script Testterm (g_::real) =   \

    96  \Repeat\

    97  \  ((Try Repeat (Rewrite rmult_1 False)) Or\

    98  \   (Try Repeat (Rewrite rmult_0 False)) Or\

    99  \   (Try Repeat (Rewrite rmult_0 False))) g_";

   100 

   101 

   102 

   103 

   104 

   105 

   106 

   107 

   108 

   109 

   110 

   111 

   112 

   113 (*################### 29.4.02: Rewrite o Rewrite o ...###############*)

   114 (*################### 29.4.02: Rewrite o Rewrite o ...###############*)

   115 (*################### 29.4.02: Rewrite o Rewrite o ...###############*)

   116 

   117 

   118 

   119 atomt ttt;

   120 val ttt = (term_of o the o (parse thy))

   121  "Script Solve_linear (e_e::bool) (v_v::real)=             \

   122  \(let e_e = \

   123  \  ((Repeat\

   124  \    (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\

   125  \      (Rewrite_Set SqRoot_simplify False)))) e_e)\

   126  \ in [e_])";

   127 atomty ttt;

   128 

   129 

   130 val ttt = (term_of o the o (parse thy))

   131 "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ yyy";

   132 atomty ttt;

   133 val ttt = (term_of o the o (parse thy))

   134  "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\

   135  \ (Rewrite_Set SqRoot_simplify False)";

   136 atomty ttt;

   137 val ttt = (term_of o the o (parse thy))

   138  "(Repeat\

   139  \  ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\

   140  \  (Rewrite_Set SqRoot_simplify False))) e_e";

   141 atomty ttt;

   142 val ttt = (term_of o the o (parseold thy))

   143 "(let e_e = Repeat xxx e_e in [e_::bool])";

   144 atomty ttt;

   145 val ttt = (term_of o the o (parseold thy))

   146  "Script Solve_linear (e_e::bool) (v_v::real)=             \

   147  \(let e_e = Repeat (xxx) e_e in [e_::bool])";

   148 atomty ttt;

   149 val ttt = (term_of o the o (parseold thy))

   150  "Script Solve_linear (e_e::bool) (v_v::real)=             \

   151  \(let e_e =\

   152  \  Repeat\

   153  \    (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\

   154  \      (Rewrite_Set SqRoot_simplify False))) e_\

   155  \ in [e_::bool])"

   156 ;

   157 atomty ttt;

   158
wneuper/isa