11 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml' |
11 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml' |
12 *******************************************************************) |
12 *******************************************************************) |
13 "-----------------------------------------------------------------"; |
13 "-----------------------------------------------------------------"; |
14 "table of contents -----------------------------------------------"; |
14 "table of contents -----------------------------------------------"; |
15 "-----------------------------------------------------------------"; |
15 "-----------------------------------------------------------------"; |
|
16 "-------- build Script Expand_binoms -----------------------------"; |
16 "-------- investigate new uniary minus ---------------------------"; |
17 "-------- investigate new uniary minus ---------------------------"; |
17 "-------- Bsple aus Schalk I -------------------------------------"; |
18 "-------- Bsple aus Schalk I -------------------------------------"; |
18 "-------- Script 'simplification for_polynomials' ----------------"; |
19 "-------- Script 'simplification for_polynomials' ----------------"; |
19 "-------- check pbl 'polynomial simplification' -----------------"; |
20 "-------- check pbl 'polynomial simplification' -----------------"; |
20 "-------- me 'polynomial simplification' Schalk I p.63 No.267b ---"; |
21 "-------- me 'polynomial simplification' Schalk I p.63 No.267b ---"; |
22 "-------- ord_make_polynomial ------------------------------------"; |
23 "-------- ord_make_polynomial ------------------------------------"; |
23 "-----------------------------------------------------------------"; |
24 "-----------------------------------------------------------------"; |
24 "-----------------------------------------------------------------"; |
25 "-----------------------------------------------------------------"; |
25 "-----------------------------------------------------------------"; |
26 "-----------------------------------------------------------------"; |
26 |
27 |
|
28 |
|
29 "-------- build Script Expand_binoms -----------------------------"; |
|
30 "-------- build Script Expand_binoms -----------------------------"; |
|
31 "-------- build Script Expand_binoms -----------------------------"; |
|
32 val scr_expand_binoms = |
|
33 "Script Expand_binoms t_t =" ^ |
|
34 "(Repeat " ^ |
|
35 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^ |
|
36 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^ |
|
37 " (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^ |
|
38 " (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^ |
|
39 " (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^ |
|
40 " (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^ |
|
41 |
|
42 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^ |
|
43 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^ |
|
44 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^ |
|
45 |
|
46 " (Try (Repeat (Calculate plus ))) @@ " ^ |
|
47 " (Try (Repeat (Calculate times ))) @@ " ^ |
|
48 " (Try (Repeat (Calculate power_))) @@ " ^ |
|
49 |
|
50 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^ |
|
51 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^ |
|
52 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^ |
|
53 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^ |
|
54 |
|
55 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^ |
|
56 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^ |
|
57 |
|
58 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^ |
|
59 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^ |
|
60 |
|
61 " (Try (Repeat (Calculate plus ))) @@ " ^ |
|
62 " (Try (Repeat (Calculate times ))) @@ " ^ |
|
63 " (Try (Repeat (Calculate power_)))) " ^ |
|
64 " t_t)"; |
|
65 val scr_expand_binoms = |
|
66 "Script Expand_binoms t_t = t_t"; |
|
67 |
|
68 val ---------------------------------------------- = "11111"; |
|
69 parse thy scr_expand_binoms; |
|
70 val ---------------------------------------------- = "22222"; |
|
71 (*---------------------------------------------- |
27 |
72 |
28 "-------- investigate new uniary minus ---------------------------"; |
73 "-------- investigate new uniary minus ---------------------------"; |
29 "-------- investigate new uniary minus ---------------------------"; |
74 "-------- investigate new uniary minus ---------------------------"; |
30 "-------- investigate new uniary minus ---------------------------"; |
75 "-------- investigate new uniary minus ---------------------------"; |
31 val t = (#prop o rep_thm) real_diff_0; (*"0 - ?x = - ?x"*) |
76 val t = (#prop o rep_thm) real_diff_0; (*"0 - ?x = - ?x"*) |