1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Dec 20 18:02:25 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Dec 26 14:24:05 2018 +0100
1.3 @@ -918,38 +918,38 @@
1.4 val scr_make_polynomial =
1.5 "Script Expand_binoms t_t = " ^
1.6 "(Repeat " ^
1.7 -"((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
1.8 +"((Try (Repeat (Rewrite ''real_diff_minus'' False))) @@ " ^
1.9
1.10 -" (Try (Repeat (Rewrite distrib_right False))) @@ " ^
1.11 -" (Try (Repeat (Rewrite distrib_left False))) @@ " ^
1.12 -" (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
1.13 -" (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
1.14 +" (Try (Repeat (Rewrite ''distrib_right'' False))) @@ " ^
1.15 +" (Try (Repeat (Rewrite ''distrib_left'' False))) @@ " ^
1.16 +" (Try (Repeat (Rewrite ''left_diff_distrib'' False))) @@ " ^
1.17 +" (Try (Repeat (Rewrite ''right_diff_distrib'' False))) @@ " ^
1.18
1.19 -" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
1.20 -" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
1.21 -" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
1.22 +" (Try (Repeat (Rewrite ''mult_1_left'' False))) @@ " ^
1.23 +" (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@ " ^
1.24 +" (Try (Repeat (Rewrite ''add_0_left'' False))) @@ " ^
1.25
1.26 -" (Try (Repeat (Rewrite mult_commute False))) @@ " ^
1.27 -" (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
1.28 -" (Try (Repeat (Rewrite mult_assoc False))) @@ " ^
1.29 -" (Try (Repeat (Rewrite add_commute False))) @@ " ^
1.30 -" (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
1.31 -" (Try (Repeat (Rewrite add_assoc False))) @@ " ^
1.32 +" (Try (Repeat (Rewrite ''mult_commute'' False))) @@ " ^
1.33 +" (Try (Repeat (Rewrite ''real_mult_left_commute'' False))) @@ " ^
1.34 +" (Try (Repeat (Rewrite ''mult_assoc'' False))) @@ " ^
1.35 +" (Try (Repeat (Rewrite ''add_commute'' False))) @@ " ^
1.36 +" (Try (Repeat (Rewrite ''add_left_commute'' False))) @@ " ^
1.37 +" (Try (Repeat (Rewrite ''add_assoc'' False))) @@ " ^
1.38
1.39 -" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
1.40 -" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
1.41 -" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
1.42 -" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
1.43 +" (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@ " ^
1.44 +" (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@ " ^
1.45 +" (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@ " ^
1.46 +" (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@ " ^
1.47
1.48 -" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
1.49 -" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
1.50 +" (Try (Repeat (Rewrite ''real_num_collect'' False))) @@ " ^
1.51 +" (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@ " ^
1.52
1.53 -" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
1.54 -" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
1.55 +" (Try (Repeat (Rewrite ''real_one_collect'' False))) @@ " ^
1.56 +" (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@ " ^
1.57
1.58 -" (Try (Repeat (Calculate PLUS ))) @@ " ^
1.59 -" (Try (Repeat (Calculate TIMES ))) @@ " ^
1.60 -" (Try (Repeat (Calculate POWER)))) " ^
1.61 +" (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
1.62 +" (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
1.63 +" (Try (Repeat (Calculate ''POWER'')))) " ^
1.64 " t_t)";
1.65
1.66 (*version used by MG.02/03, overwritten by version AG in 04 below
1.67 @@ -973,35 +973,35 @@
1.68 val scr_expand_binoms =
1.69 "Script Expand_binoms t_t =" ^
1.70 "(Repeat " ^
1.71 -"((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
1.72 -" (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
1.73 -" (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
1.74 -" (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
1.75 -" (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
1.76 -" (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
1.77 +"((Try (Repeat (Rewrite ''real_plus_binom_pow2'' False))) @@ " ^
1.78 +" (Try (Repeat (Rewrite ''real_plus_binom_times'' False))) @@ " ^
1.79 +" (Try (Repeat (Rewrite ''real_minus_binom_pow2'' False))) @@ " ^
1.80 +" (Try (Repeat (Rewrite ''real_minus_binom_times'' False))) @@ " ^
1.81 +" (Try (Repeat (Rewrite ''real_plus_minus_binom1'' False))) @@ " ^
1.82 +" (Try (Repeat (Rewrite ''real_plus_minus_binom2'' False))) @@ " ^
1.83
1.84 -" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
1.85 -" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
1.86 -" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
1.87 +" (Try (Repeat (Rewrite ''mult_1_left'' False))) @@ " ^
1.88 +" (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@ " ^
1.89 +" (Try (Repeat (Rewrite ''add_0_left'' False))) @@ " ^
1.90
1.91 -" (Try (Repeat (Calculate PLUS ))) @@ " ^
1.92 -" (Try (Repeat (Calculate TIMES ))) @@ " ^
1.93 -" (Try (Repeat (Calculate POWER))) @@ " ^
1.94 +" (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
1.95 +" (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
1.96 +" (Try (Repeat (Calculate ''POWER''))) @@ " ^
1.97
1.98 -" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
1.99 -" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
1.100 -" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
1.101 -" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
1.102 +" (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@ " ^
1.103 +" (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@ " ^
1.104 +" (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@ " ^
1.105 +" (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@ " ^
1.106
1.107 -" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
1.108 -" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
1.109 +" (Try (Repeat (Rewrite ''real_num_collect'' False))) @@ " ^
1.110 +" (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@ " ^
1.111
1.112 -" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
1.113 -" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
1.114 +" (Try (Repeat (Rewrite ''real_one_collect'' False))) @@ " ^
1.115 +" (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@ " ^
1.116
1.117 -" (Try (Repeat (Calculate PLUS ))) @@ " ^
1.118 -" (Try (Repeat (Calculate TIMES ))) @@ " ^
1.119 -" (Try (Repeat (Calculate POWER)))) " ^
1.120 +" (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
1.121 +" (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
1.122 +" (Try (Repeat (Calculate ''POWER'')))) " ^
1.123 " t_t)";
1.124
1.125 val expand_binoms =
1.126 @@ -1614,7 +1614,7 @@
1.127 norm_Poly :: ID
1.128 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
1.129 where
1.130 - "simplify term = ((Rewrite_Set norm_Poly False) term)"
1.131 + "simplify term = ((Rewrite_Set ''norm_Poly'' False) term)"
1.132
1.133 -----*)
1.134 setup \<open>KEStore_Elems.add_mets
1.135 @@ -1629,7 +1629,7 @@
1.136 Rule.Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
1.137 crls = Rule.e_rls, errpats = [], nrls = norm_Poly},
1.138 "Script SimplifyScript (t_t::real) = " ^
1.139 - " ((Rewrite_Set norm_Poly False) t_t)")]
1.140 + " ((Rewrite_Set ''norm_Poly'' False) t_t)")]
1.141 \<close>
1.142
1.143 ML \<open>