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 ----";
18 Note after CS "eliminate ThmC.numerals_to_Free" and "replace is_const with is_num" Aug.2021:
19 Output of this test is questionable, (*1*) is from long ago.
20 Input is questionable, too.
21 So this test is left for reactivating biegelinie-*.sml.
23 val thy = @{theory RootRat};
24 val ctxt = Proof_Context.init_global thy;
25 val t = (the o (ParseC.term_opt ctxt))
26 ("- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) | \nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))");
28 val rls = calculate_Rational;
29 val SOME (t', asm) = rewrite_set_ ctxt true rls t;
31 "- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - - 8) \<or>\nx = - 1 * (- 1 + - 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))"
32 (*"- 1 * x = - 1 + sqrt (1 \<up> 2 - -8) | x = - 1 * (- 1 + - 1 * sqrt (1 \<up> 2 - -8))" (*1*)*)
33 then () else error "rls calculate_Rational CHANGED";
35 val rls = calculate_RootRat;
36 val SOME (t, asm) = rewrite_set_ ctxt true rls t;
38 "- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - - 8) \<or>\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))"
39 then () else error "rls calculate_RootRat CHANGED";