|
wneuper@4885
|
1 |
package isac.gui.mawen.scalaterm
|
|
wneuper@4885
|
2 |
|
|
walther@5239
|
3 |
import edu.tum.cs.isabelle.pure._
|
|
s1520454056@5091
|
4 |
import isac.gui.mawen.syntax.Ast
|
|
wneuper@4885
|
5 |
|
|
wneuper@4885
|
6 |
object TestsDATA {
|
|
wneuper@4885
|
7 |
|
|
wneuper@4885
|
8 |
//---------------------------- for <code>MockCalcTreeSIMPLIFY</code>
|
|
wneuper@4885
|
9 |
/* copied from ScalaTermFromString.testExampleForRef1
|
|
wneuper@4885
|
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()))))
|
|
wneuper@4885
|
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())))
|
|
wneuper@4885
|
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())))
|
|
wneuper@4885
|
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())))
|
|
wneuper@4885
|
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())))))
|
|
wneuper@4885
|
15 |
*/
|
|
wneuper@4885
|
16 |
// below <REPLACE ALL> fun WITH "fun", etc (in a separate file in order to preserve the above copies)
|
|
wneuper@4885
|
17 |
// "Simplify ((1 + (2 * x * (y + 3)) / (4 * z * (y + 3))) + 5::real)";
|
|
wneuper@4885
|
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()))))
|
|
wneuper@4885
|
19 |
// "(1 + (2 * x * (y + 3)) / (4 * z * (y + 3))) + 5::real";
|
|
wneuper@4885
|
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())))
|
|
wneuper@4885
|
21 |
// "(1 + (2 * x) / (4 * z)) + 5::real";
|
|
wneuper@4885
|
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())))
|
|
wneuper@5017
|
23 |
// "???";
|
|
wneuper@5017
|
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())))
|
|
wneuper@4885
|
25 |
// "6 + (2 * x) / (4 * z::real)";
|
|
wneuper@4885
|
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())))))
|
|
S1420454023@4922
|
27 |
|
|
S1420454023@4922
|
28 |
def tt3_math(): String =
|
|
S1420454023@4922
|
29 |
"<math xmlns="+"\"&mathml;\""+">"+
|
|
S1420454023@4922
|
30 |
"<mrow>"+
|
|
S1420454023@4922
|
31 |
"<mn>1</mn>"+
|
|
S1420454023@4922
|
32 |
"<mo> + </mo>"+
|
|
S1420454023@4922
|
33 |
"<mfrac>"+
|
|
S1420454023@4922
|
34 |
"<mrow>"+
|
|
S1420454023@4922
|
35 |
"<mn>2</mn><mo> * </mo><mi>x</mi>"+
|
|
S1420454023@4922
|
36 |
"<mo> * </mo>"+
|
|
S1420454023@4922
|
37 |
"<mfenced separators=\'\'>"+
|
|
S1420454023@4922
|
38 |
"<mi>y</mi><mo> + </mo><mn>3</mn>"+
|
|
S1420454023@4922
|
39 |
"</mfenced>"+
|
|
S1420454023@4922
|
40 |
"</mrow>"+
|
|
S1420454023@4922
|
41 |
"<mrow>"+
|
|
S1420454023@4922
|
42 |
"<mn>4</mn><mo> * </mo><mi>z</mi>"+
|
|
S1420454023@4922
|
43 |
"<mo> * </mo>"+
|
|
S1420454023@4922
|
44 |
"<mfenced separators=\'\'>"+
|
|
S1420454023@4922
|
45 |
"<mi>y</mi><mo> + </mo><mn>3</mn>"+
|
|
S1420454023@4922
|
46 |
"</mfenced>"+
|
|
S1420454023@4922
|
47 |
"</mrow>"+
|
|
S1420454023@4922
|
48 |
"</mfrac>"+
|
|
S1420454023@4922
|
49 |
"<mo> + </mo>"+
|
|
S1420454023@4922
|
50 |
"<mn>5</mn>"+
|
|
S1420454023@4922
|
51 |
"</mrow>" +
|
|
S1420454023@4922
|
52 |
"</math>";
|
|
wneuper@4962
|
53 |
//scenario 1: http://www.ist.tugraz.at/projects/isac/publ/Masterthesis_NatalieKarl.pdf p.47
|
|
S1420454023@4952
|
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())))
|
|
S1420454023@4952
|
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())))
|
|
S1420454023@4952
|
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()))))))
|
|
wneuper@4962
|
57 |
//scenario 4: http://www.ist.tugraz.at/projects/isac/publ/Masterthesis_NatalieKarl.pdf p.50
|
|
S1420454023@4952
|
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()))))))
|
|
S1420454023@4952
|
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()))))))
|
|
S1420454023@4952
|
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())))
|
|
wneuper@4962
|
61 |
//scenario 5: http://www.ist.tugraz.at/projects/isac/publ/Masterthesis_NatalieKarl.pdf p.51
|
|
S1420454023@4952
|
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())))
|
|
S1420454023@4952
|
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())))
|
|
S1420454023@4952
|
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())))
|
|
S1420454023@4952
|
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())))
|
|
S1420454023@4952
|
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())))
|
|
S1420454023@4952
|
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())))))
|
|
S1420454023@4952
|
68 |
|
|
wneuper@5064
|
69 |
//for re-use in different tests:
|
|
wneuper@5064
|
70 |
//---------------------------- for <code>TestPIDE#testTermOneWay</code>
|
|
wneuper@5064
|
71 |
def t1 = //"aaa + bbb = processed_by_Isabelle_Isac"
|
|
wneuper@5064
|
72 |
App(App(Const("HOL.eq", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("HOL.bool",List())))))),
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
74 |
Free("aaa", Type("Real.real",List()))),
|
|
wneuper@5064
|
75 |
Free("bbb", Type("Real.real",List())))),
|
|
wneuper@5064
|
76 |
Const("processed_by_Isabelle_Isac", Type("Real.real",List())))
|
|
wneuper@5064
|
77 |
// console output:
|
|
wneuper@5064
|
78 |
//App(App(
|
|
wneuper@5064
|
79 |
// Const(HOL.eq, Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(HOL.bool,List())))))),
|
|
wneuper@5064
|
80 |
// App(App(
|
|
wneuper@5064
|
81 |
// Const(Groups.plus_class.plus, Type(fun,List(Type(Real.real,List()), Type(fun,List(Type(Real.real,List()), Type(Real.real,List())))))),
|
|
wneuper@5064
|
82 |
// Free(aaa,Type(Real.real,List()))),
|
|
wneuper@5064
|
83 |
// Free(bbb,Type(Real.real,List())))),
|
|
wneuper@5064
|
84 |
// Const(processed_by_Isabelle_Isac,Type(Real.real,List())))
|
|
wneuper@5064
|
85 |
|
|
wneuper@5064
|
86 |
//---------------------------- for viewing a (relatively) complicated term
|
|
wneuper@5064
|
87 |
def t2 = //"a + 2 * b + 3 * (c + d)"
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
90 |
Free("a", Type("Real.real",List()))),
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
92 |
Free("2", Type("Real.real",List()))),
|
|
wneuper@5064
|
93 |
Free("b", Type("Real.real",List()))))),
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
95 |
Free("3", Type("Real.real",List()))),
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
97 |
Free("c", Type("Real.real",List()))),
|
|
wneuper@5064
|
98 |
Free("d", Type("Real.real",List())))))
|
|
wneuper@5064
|
99 |
|
|
wneuper@5064
|
100 |
//---------------------------- for "infixl", left associativity
|
|
wneuper@5064
|
101 |
def t31 = //"aaa + bbb + ccc"
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
104 |
Free("aaa", Type("Real.real",List()))),
|
|
wneuper@5064
|
105 |
Free("bbb", Type("Real.real",List())))),
|
|
wneuper@5064
|
106 |
Free("ccc", Type("Real.real",List())))
|
|
wneuper@5064
|
107 |
def t32 = //"aaa + (bbb + ccc)"
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
109 |
Free("aaa", Type("Real.real",List()))),
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
111 |
Free("bbb", Type("Real.real",List()))),
|
|
wneuper@5064
|
112 |
Free("ccc", Type("Real.real",List()))))
|
|
wneuper@5064
|
113 |
|
|
wneuper@5064
|
114 |
//---------------------------- for <code>TestWorksheetForMawen</code>
|
|
wneuper@5064
|
115 |
// term at pos = ([], Frm)
|
|
wneuper@5064
|
116 |
def t41 = //"Diff (x + sin (x ^ 2), x)"
|
|
wneuper@5064
|
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())))),
|
|
wneuper@5064
|
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())))))))),
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
120 |
Free("x", Type("Real.real",List()))),
|
|
wneuper@5064
|
121 |
App(Const("Transcendental.sin", Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))),
|
|
wneuper@5064
|
122 |
App(App(Const("Atools.pow", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),
|
|
wneuper@5064
|
123 |
Free("x", Type("Real.real",List()))),
|
|
wneuper@5064
|
124 |
Free("2", Type("Nat.nat",List())))))),
|
|
wneuper@5064
|
125 |
Free("x", Type("Real.real",List()))))
|
|
wneuper@5064
|
126 |
// term at pos = ([1], Frm)
|
|
wneuper@5064
|
127 |
def t42 = //"d_d x (x + sin (x ^ 2))"
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
129 |
Free("x", Type("Real.real",List()))),
|
|
wneuper@5064
|
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())))))),
|
|
wneuper@5064
|
131 |
Free("x", Type("Real.real",List()))),
|
|
wneuper@5064
|
132 |
App(Const("Transcendental.sin", Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))),
|
|
wneuper@5064
|
133 |
App(App(Const("Atools.pow", Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Nat.nat",List()), Type("Real.real",List())))))),
|
|
wneuper@5064
|
134 |
Free("x", Type("Real.real",List()))),
|
|
wneuper@5064
|
135 |
Free("2", Type("Nat.nat",List()))))))
|
|
wneuper@5064
|
136 |
// term at pos = ([1], Res)
|
|
wneuper@5064
|
137 |
//TODO "d_d x x + d_d x (sin (x ^ 2))"
|
|
wneuper@5064
|
138 |
|
|
wneuper@5064
|
139 |
// rule at pos = ([2], Frm)
|
|
wneuper@5064
|
140 |
//TODO "rule (d_d x sin (?a) = cos (?a) * d_d x ?a)"
|
|
wneuper@5064
|
141 |
|
|
wneuper@5064
|
142 |
// term at pos = ([2], Res)
|
|
wneuper@5064
|
143 |
//TODO "d_d x x + cos (x ^ 2) * (2 * x ^ (2 - 1))"
|
|
wneuper@5064
|
144 |
|
|
s1520454056@5091
|
145 |
|
|
s1520454056@5108
|
146 |
def a_1 = Ast.Appl(List(
|
|
s1520454056@5126
|
147 |
Ast.Constant("HOL.eq"),
|
|
s1520454056@5108
|
148 |
Ast.Appl(List(
|
|
s1520454056@5126
|
149 |
Ast.Constant("Groups.plus_class.plus"),
|
|
s1520454056@5126
|
150 |
Ast.Variable("x"),
|
|
s1520454056@5126
|
151 |
Ast.Variable("1")
|
|
s1520454056@5126
|
152 |
)),
|
|
s1520454056@5126
|
153 |
Ast.Variable("2")
|
|
s1520454056@5108
|
154 |
))
|
|
s1520454056@5091
|
155 |
|
|
s1520454056@5108
|
156 |
def a_2 = Ast.Variable("yyy")
|
|
s1520454056@5091
|
157 |
|
|
s1520454056@5108
|
158 |
def a_3 = Ast.Variable("zzz")
|
|
walther@5239
|
159 |
}
|