1 (* Title: testexamples for RootRat.thy
2 Author: Walther Neuper 2011
3 (c) due to copyright terms
5 "-----------------------------------------------------------------";
6 "table of contents -----------------------------------------------";
7 "-----------------------------------------------------------------";
8 "----------- val rls = calculate_RootRat > calculate_Rational ----";
9 "-----------------------------------------------------------------";
10 "-----------------------------------------------------------------";
11 "-----------------------------------------------------------------";
14 "----------- val rls = calculate_RootRat > calculate_Rational ----";
15 "----------- val rls = calculate_RootRat > calculate_Rational ----";
16 "----------- val rls = calculate_RootRat > calculate_Rational ----";
17 (*val calculate_RootRat =
18 Rule_Set.append_rules "calculate_RootRat" calculate_Rational [...]
19 val calculate_Rational = prep_rls (merge_rls "calculate_Rational" [...]
22 Rule_Set.append_rules "calculate_PolyFIXXXME.not.impl." Rule_Set.empty [];
23 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
26 val thy = @{theory RootRat};
27 val ctxt = Proof_Context.init_global thy;
28 val ttt = (the o (parseNEW ctxt)) ("-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
29 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))");
30 TermC.atomty t; (*!real ?by sqrt and ^^^?*)
32 "--- val rls = calculate_Poly ---";
33 (*val rls = assoc_rls "calculate_Poly"; WAS ME_Isa: 'calculate_Poly' not in system
34 goon with what just started ...*)
35 val calculate_Poly = Rule_Set.append_rules "calculate_Poly" Rule_Set.empty
36 [ Eval ("Groups.plus_class.plus",eval_binop "#add_"),
37 Eval ("Groups.minus_class.minus",eval_binop "#sub_"),
38 Eval ("Groups.times_class.times",eval_binop "#mult_"),
39 Eval ("Prog_Expr.pow" ,eval_binop "#power_")
41 val rls = calculate_Poly;
43 (*val SOME (t,asm) = rewrite_set_ thy true rls ttt; WAS: NONE .. ok*)
45 "--- val rls = calculate_Rational ---";
46 val rls = assoc_rls "calculate_Rational";
47 val rls = calculate_Rational;
49 val SOME (t,asm) = rewrite_set_ thy true rls ttt;
51 "-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) \<or>\nx = -1 * (-1 + -1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
52 (*"-1 * x = -1 + sqrt (1 ^^^ 2 - -8) | x = -1 * (-1 + -1 * sqrt (1 ^^^ 2 - -8))"*)
53 then () else error "val rls = calculate_Rational goon";
55 "--- val rls = calculate_RootRat ---";
56 val rls = assoc_rls "calculate_RootRat";
57 val rls = calculate_RootRat;
59 val SOME (t,asm) = rewrite_set_ thy true rls ttt;
61 (*~~~~~ val rls = calculate_RootRat: rewrite stepwise*)
62 val thm = ThmC.numerals_to_Free @{thm complete_square2};