wneuper/isac: isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestsDATA.scala@b4e3883d7b66

     1 package isac.gui.mawen.scalaterm

     3 import edu.tum.cs.isabelle.pure._

     4 import isac.gui.mawen.syntax.Ast

     6 object TestsDATA {

     8   //---------------------------- for <code>MockCalcTreeSIMPLIFY</code>

     9   /* copied from ScalaTermFromString.testExampleForRef1

    10    1 App(Const(Simplify.Simplify,Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(1,Type(Real.real,List()))),App(App(Const(Fields.inverse_class.divide,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(2,Type(Real.real,List()))),Free(x,Type(Real.real,List())))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(y,Type(Real.real,List()))),Free(3,Type(Real.real,List()))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(4,Type(Real.real,List()))),Free(z,Type(Real.real,List())))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(y,Type(Real.real,List()))),Free(3,Type(Real.real,List()))))))),Free(5,Type(Real.real,List()))))

    11    2 App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(1,Type(Real.real,List()))),App(App(Const(Fields.inverse_class.divide,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(2,Type(Real.real,List()))),Free(x,Type(Real.real,List())))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(y,Type(Real.real,List()))),Free(3,Type(Real.real,List()))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(4,Type(Real.real,List()))),Free(z,Type(Real.real,List())))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(y,Type(Real.real,List()))),Free(3,Type(Real.real,List()))))))),Free(5,Type(Real.real,List())))

    12    3 App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(1,Type(Real.real,List()))),App(App(Const(Fields.inverse_class.divide,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(2,Type(Real.real,List()))),Free(x,Type(Real.real,List())))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(4,Type(Real.real,List()))),Free(z,Type(Real.real,List())))))),Free(5,Type(Real.real,List())))

    13    4 App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(1,Type(Real.real,List()))),App(App(Const(Fields.inverse_class.divide,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(x,Type(Real.real,List()))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(2,Type(Real.real,List()))),Free(z,Type(Real.real,List())))))),Free(5,Type(Real.real,List())))

    14    5 App(App(Const(Groups.plus_class.plus,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(6,Type(Real.real,List()))),App(App(Const(Fields.inverse_class.divide,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(x,Type(Real.real,List()))),App(App(Const(Groups.times_class.times,Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),Free(2,Type(Real.real,List()))),Free(z,Type(Real.real,List())))))

    15    */

    16   // below <REPLACE ALL> fun WITH "fun", etc (in a separate file in order to preserve the above copies)

    17   //                "Simplify ((1 + (2 * x * (y + 3)) / (4 * z * (y + 3))) + 5::real)";

    18   def tt1 (): Term = App(Const("Simplify.Simplify",Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List()))))

    19   //         "(1 + (2 * x * (y + 3)) / (4 * z * (y + 3))) + 5::real";

    20   def tt3 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))

    21   //         "(1 + (2 * x) / (4 * z)) + 5::real";

    22   def tt4 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))))),Free("5",Type("Real.real",List())))

    23   //         "???";

    24   def tt5 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("z",Type("Real.real",List())))))),Free("5",Type("Real.real",List())))

    25   //         "6 + (2 * x) / (4 * z::real)";

    26   def tt6 (): Term = App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("z",Type("Real.real",List())))))

    28   def tt3_math(): String =

    29             "<math xmlns="+"\"&mathml;\""+">"+

    30             "<mrow>"+

    31                 "<mn>1</mn>"+

    32                 "<mo> + </mo>"+

    33                 "<mfrac>"+

    34                    "<mrow>"+

    35                      "<mn>2</mn><mo> * </mo><mi>x</mi>"+

    36                      "<mo> * </mo>"+

    37                      "<mfenced separators=\'\'>"+

    38                        "<mi>y</mi><mo> + </mo><mn>3</mn>"+

    39                      "</mfenced>"+

    40                    "</mrow>"+

    41                     "<mrow>"+

    42                        "<mn>4</mn><mo> * </mo><mi>z</mi>"+

    43                        "<mo> * </mo>"+

    44                        "<mfenced separators=\'\'>"+

    45                         "<mi>y</mi><mo> + </mo><mn>3</mn>"+

    46                        "</mfenced>"+

    47                      "</mrow>"+

    48                   "</mfrac>"+

    49                "<mo> + </mo>"+

    50                "<mn>5</mn>"+

    51              "</mrow>" +

    52          "</math>";

    53   //scenario 1: http://www.ist.tugraz.at/projects/isac/publ/Masterthesis_NatalieKarl.pdf p.47

    54     def tt_me1_1 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("2",Type("Nat.nat",List())))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),Free("y",Type("Real.real",List()))))),Free("9",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))

    55     def tt_me1_2 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))),Free("2",Type("Nat.nat",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))

    56     def tt_me1_3 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),Free("1",Type("Real.real",List()))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))

    57   //scenario 4: http://www.ist.tugraz.at/projects/isac/publ/Masterthesis_NatalieKarl.pdf p.50

    58     def tt_me4_1 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("3",Type("Real.real",List()))),Free("b",Type("Real.real",List()))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("c",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))))

    59     def tt_me4_2 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List())))),Free("2",Type("Nat.nat",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("3",Type("Real.real",List()))),Free("b",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("c",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))))

    60     def tt_me4_3 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("5",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),Free("a",Type("Real.real",List()))),Free("2",Type("Nat.nat",List()))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("3",Type("Real.real",List()))),Free("b",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("c",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("a",Type("Real.real",List()))))))),Free("1",Type("Real.real",List())))

    61   //scenario 5: http://www.ist.tugraz.at/projects/isac/publ/Masterthesis_NatalieKarl.pdf p.51

    62     def tt_me5_1 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("2",Type("Nat.nat",List())))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),Free("y",Type("Real.real",List()))))),Free("9",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))

    63     def tt_me5_2 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Atools.pow",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))),Free("2",Type("Nat.nat",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))

    64     def tt_me5_3 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))

    65     def tt_me5_4 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),Free("1",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("y",Type("Real.real",List()))),Free("3",Type("Real.real",List()))))))),Free("5",Type("Real.real",List())))

    66     def tt_me5_5 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("1",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),Free("1",Type("Real.real",List())))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))))),Free("5",Type("Real.real",List())))

    67     def tt_me5_6 (): Term =  App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("6",Type("Real.real",List()))),App(App(Const("Fields.inverse_class.divide",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("2",Type("Real.real",List()))),Free("x",Type("Real.real",List())))),Free("1",Type("Real.real",List())))),App(App(Const("Groups.times_class.times",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("4",Type("Real.real",List()))),Free("z",Type("Real.real",List())))))

    69   //for re-use in different tests:

    70   //---------------------------- for <code>TestPIDE#testTermOneWay</code>

    71   def t1 = //"aaa + bbb = processed_by_Isabelle_Isac"

    72     App(App(Const("HOL.eq",                   Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("HOL.bool",List())))))),

    73       App(App(Const("Groups.plus_class.plus", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

    74         Free("aaa",                           Type("Real.real",List()))),

    75         Free("bbb",                           Type("Real.real",List())))),

    76       Const("processed_by_Isabelle_Isac",     Type("Real.real",List())))

    77   // console output:

    78   //App(App(

    79   //  Const(HOL.eq,                           Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(HOL.bool,List())))))),

    80   //    App(App(

    81   //      Const(Groups.plus_class.plus, Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),

    82   //        Free(aaa,Type(Real.real,List()))),

    83   //        Free(bbb,Type(Real.real,List())))),

    84   //      Const(processed_by_Isabelle_Isac,Type(Real.real,List())))

    86   //---------------------------- for viewing a (relatively) complicated term

    87   def t2 = //"a + 2 * b + 3 * (c + d)"

    88     App(App(Const("Groups.plus_class.plus", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

    89       App(App(Const("Groups.plus_class.plus", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

    90         Free("a", Type("Real.real",List()))),

    91         App(App(Const("Groups.times_class.times", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

    92           Free("2", Type("Real.real",List()))),

    93           Free("b", Type("Real.real",List()))))),

    94       App(App(Const("Groups.times_class.times", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

    95         Free("3", Type("Real.real",List()))),

    96         App(App(Const("Groups.plus_class.plus", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

    97           Free("c", Type("Real.real",List()))),

    98           Free("d", Type("Real.real",List())))))

   100   //---------------------------- for "infixl", left associativity

   101   def t31 = //"aaa + bbb + ccc"

   102     App(App(Const("Groups.plus_class.plus", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

   103       App(App(Const("Groups.plus_class.plus", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

   104         Free("aaa", Type("Real.real",List()))),

   105         Free("bbb", Type("Real.real",List())))),

   106       Free("ccc", Type("Real.real",List())))

   107   def t32 = //"aaa + (bbb + ccc)"

   108     App(App(Const("Groups.plus_class.plus", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

   109       Free("aaa", Type("Real.real",List()))),

   110       App(App(Const("Groups.plus_class.plus", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

   111         Free("bbb", Type("Real.real",List()))),

   112         Free("ccc", Type("Real.real",List()))))

   114   //---------------------------- for <code>TestWorksheetForMawen</code>

   115   // term at pos = ([], Frm)

   116   def t41 = //"Diff (x + sin (x ^ 2), x)"

   117     App(Const("Diff.Diff", Type("fun",List(Type("Product_Type.prod",List(Type("Real.real",List()), Type("Real.real",List()))), Type("Real.real",List())))),

   118       App(App(Const("Product_Type.Pair", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Product_Type.prod",List(Type("Real.real",List()), Type("Real.real",List())))))))),

   119         App(App(Const("Groups.plus_class.plus", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

   120           Free("x", Type("Real.real",List()))),

   121           App(Const("Transcendental.sin", Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))),

   122             App(App(Const("Atools.pow", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),

   123               Free("x", Type("Real.real",List()))),

   124               Free("2", Type("Nat.nat",List())))))),

   125       Free("x", Type("Real.real",List()))))

   126   // term at pos = ([1], Frm)

   127   def t42 = //"d_d x (x + sin (x ^ 2))"

   128     App(App(Const("Diff.d_d", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

   129       Free("x", Type("Real.real",List()))),

   130       App(App(Const("Groups.plus_class.plus", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),

   131         Free("x", Type("Real.real",List()))),

   132         App(Const("Transcendental.sin", Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))),

   133           App(App(Const("Atools.pow", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),

   134             Free("x", Type("Real.real",List()))),

   135             Free("2", Type("Nat.nat",List()))))))

   136   // term at pos = ([1], Res)

   137   //TODO "d_d x x + d_d x (sin (x ^ 2))"

   139   // rule at pos = ([2], Frm)

   140   //TODO "rule (d_d x sin (?a) = cos (?a) * d_d x ?a)"

   142   // term at pos = ([2], Res)

   143   //TODO "d_d x x + cos (x ^ 2) * (2 * x ^ (2 - 1))"

   146   def a_1 = Ast.Appl(List(

   147       Ast.Constant("HOL.eq"),

   148       Ast.Appl(List(

   149           Ast.Constant("Groups.plus_class.plus"),

   150             Ast.Variable("x"),

   151             Ast.Variable("1")

   152           )),

   153           Ast.Variable("2")

   154       ))

   156   def a_2 = Ast.Variable("yyy")

   158   def a_3 = Ast.Variable("zzz")

   159 }

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 26 Mar 2021 10:45:05 +0100
changeset 5239	b4e3883d7b66
parent 5229	6bf0e95981e3
permissions	-rw-r--r--