1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Sep 01 15:19:47 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Sep 01 16:15:13 2010 +0200
1.3 @@ -935,21 +935,21 @@
1.4 "(Repeat " ^
1.5 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
1.6
1.7 -" (Try (Repeat (Rewrite real_add_mult_distrib False))) @@ " ^
1.8 -" (Try (Repeat (Rewrite real_add_mult_distrib2 False))) @@ " ^
1.9 -" (Try (Repeat (Rewrite real_diff_mult_distrib False))) @@ " ^
1.10 -" (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ " ^
1.11 +" (Try (Repeat (Rewrite left_distrib False))) @@ " ^
1.12 +" (Try (Repeat (Rewrite right_distrib False))) @@ " ^
1.13 +" (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
1.14 +" (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
1.15
1.16 -" (Try (Repeat (Rewrite real_mult_1 False))) @@ " ^
1.17 -" (Try (Repeat (Rewrite real_mult_0 False))) @@ " ^
1.18 -" (Try (Repeat (Rewrite real_add_zero_left False))) @@ " ^
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
1.23 " (Try (Repeat (Rewrite real_mult_commute False))) @@ " ^
1.24 " (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
1.25 " (Try (Repeat (Rewrite real_mult_assoc False))) @@ " ^
1.26 -" (Try (Repeat (Rewrite real_add_commute False))) @@ " ^
1.27 -" (Try (Repeat (Rewrite real_add_left_commute False))) @@ " ^
1.28 -" (Try (Repeat (Rewrite real_add_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
1.33 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
1.34 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
1.35 @@ -994,9 +994,9 @@
1.36 " (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
1.37 " (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
1.38
1.39 -" (Try (Repeat (Rewrite real_mult_1 False))) @@ " ^
1.40 -" (Try (Repeat (Rewrite real_mult_0 False))) @@ " ^
1.41 -" (Try (Repeat (Rewrite real_add_zero_left False))) @@ " ^
1.42 +" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
1.43 +" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
1.44 +" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
1.45
1.46 " (Try (Repeat (Calculate plus ))) @@ " ^
1.47 " (Try (Repeat (Calculate times ))) @@ " ^
2.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Sep 01 15:19:47 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Sep 01 16:15:13 2010 +0200
2.3 @@ -1219,21 +1219,21 @@
2.4 "(Repeat " ^
2.5 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
2.6
2.7 -" (Try (Repeat (Rewrite real_add_mult_distrib False))) @@ " ^
2.8 -" (Try (Repeat (Rewrite real_add_mult_distrib2 False))) @@ " ^
2.9 -" (Try (Repeat (Rewrite real_diff_mult_distrib False))) @@ " ^
2.10 -" (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ " ^
2.11 +" (Try (Repeat (Rewrite left_distrib False))) @@ " ^
2.12 +" (Try (Repeat (Rewrite right_distrib False))) @@ " ^
2.13 +" (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
2.14 +" (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
2.15
2.16 -" (Try (Repeat (Rewrite real_mult_1 False))) @@ " ^
2.17 -" (Try (Repeat (Rewrite real_mult_0 False))) @@ " ^
2.18 -" (Try (Repeat (Rewrite real_add_zero_left False))) @@ " ^
2.19 +" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
2.20 +" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
2.21 +" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
2.22
2.23 " (Try (Repeat (Rewrite real_mult_commute False))) @@ " ^
2.24 " (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
2.25 " (Try (Repeat (Rewrite real_mult_assoc False))) @@ " ^
2.26 -" (Try (Repeat (Rewrite real_add_commute False))) @@ " ^
2.27 -" (Try (Repeat (Rewrite real_add_left_commute False))) @@ " ^
2.28 -" (Try (Repeat (Rewrite real_add_assoc False))) @@ " ^
2.29 +" (Try (Repeat (Rewrite add_commute False))) @@ " ^
2.30 +" (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
2.31 +" (Try (Repeat (Rewrite add_assoc False))) @@ " ^
2.32
2.33 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
2.34 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
2.35 @@ -1331,9 +1331,9 @@
2.36 " (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
2.37 " (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
2.38
2.39 -" (Try (Repeat (Rewrite real_mult_1 False))) @@ " ^
2.40 -" (Try (Repeat (Rewrite real_mult_0 False))) @@ " ^
2.41 -" (Try (Repeat (Rewrite real_add_zero_left False))) @@ " ^
2.42 +" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
2.43 +" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
2.44 +" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
2.45
2.46 " (Try (Repeat (Calculate plus ))) @@ " ^
2.47 " (Try (Repeat (Calculate times ))) @@ " ^
3.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Wed Sep 01 15:19:47 2010 +0200
3.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Wed Sep 01 16:15:13 2010 +0200
3.3 @@ -328,7 +328,7 @@
3.4 "Script Stepwise (t::'z) =\
3.5 \(Repeat\
3.6 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
3.7 - \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
3.8 + \ (Try (Repeat (Rewrite add_commute False))) @@ \
3.9 \ (Try (Repeat (Rewrite real_mult_commute False)))) \
3.10 \ t_t)";
3.11 val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*)
3.12 @@ -336,7 +336,7 @@
3.13 "Script Stepwise (t::'z) =\
3.14 \(Repeat\
3.15 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
3.16 - \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
3.17 + \ (Try (Repeat (Rewrite add_commute False))) @@ \
3.18 \ (Try (Repeat (Rewrite real_mult_commute False)))) \
3.19 \ t_t)";
3.20 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body
3.21 @@ -346,7 +346,7 @@
3.22 "Script Stepwise_inst (t::'z) (v::real) =\
3.23 \(Repeat\
3.24 \ ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \
3.25 - \ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_add_commute False))) @@\
3.26 + \ (Try (Repeat (Rewrite_Inst [(bdv,v)] add_commute False))) @@\
3.27 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \
3.28 \ t)";
3.29 val Repeat $ _ =
3.30 @@ -376,7 +376,7 @@
3.31 val SEq $ _ $ _ $ _ =
3.32 ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
3.33 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
3.34 - \ (Try (Repeat (Rewrite real_add_commute False))) @@ \
3.35 + \ (Try (Repeat (Rewrite add_commute False))) @@ \
3.36 \ (Try (Repeat (Rewrite real_mult_commute False)))) t";
3.37
3.38 fun rule2stac _ (Thm (thmID, _)) =
4.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Sep 01 15:19:47 2010 +0200
4.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Sep 01 16:15:13 2010 +0200
4.3 @@ -79,13 +79,13 @@
4.4 val od = ord_make_polynomial true Poly.thy;
4.5 val t = str2term "((a + d) + c) + b";
4.6 "((a + d) + c) + b";
4.7 -val SOME (t,_) = rewrite_ thy od e_rls true real_add_commute t; term2str t;
4.8 +val SOME (t,_) = rewrite_ thy od e_rls true add_commute t; term2str t;
4.9 "b + ((a + d) + c)";
4.10 -val SOME (t,_) = rewrite_ thy od e_rls true real_add_commute t; term2str t;
4.11 +val SOME (t,_) = rewrite_ thy od e_rls true add_commute t; term2str t;
4.12 "b + (c + (a + d))";
4.13 -val SOME (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t;
4.14 +val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t;
4.15 "b + (a + (c + d))";
4.16 -val SOME (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t;
4.17 +val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t;
4.18 "a + (b + (c + d))";
4.19 if term2str t = "a + (b + (c + d))" then ()
4.20 else raise error "polyminus.sml 2 watch order_add_mult";
4.21 @@ -93,11 +93,11 @@
4.22 "----- if parentheses are right, left_commute is (almost) sufficient...";
4.23 val t = str2term "a + (d + (c + b))";
4.24 "a + (d + (c + b))";
4.25 -val SOME (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t;
4.26 +val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t;
4.27 "a + (c + (d + b))";
4.28 -val SOME (t,_) = rewrite_ thy od e_rls true real_add_commute t;term2str t;
4.29 +val SOME (t,_) = rewrite_ thy od e_rls true add_commute t;term2str t;
4.30 "a + (c + (b + d))";
4.31 -val SOME (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t;
4.32 +val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t;
4.33 "a + (b + (c + d))";
4.34
4.35 "----- but we do not want the parentheses at right; thus: cond.rew.";
4.36 @@ -110,8 +110,8 @@
4.37 "----- here we see rew_sub going into subterm with ord.rew....";
4.38 val od = ord_make_polynomial false Poly.thy;
4.39 val t = str2term "b + a + c + d";
4.40 -val SOME (t,_) = rewrite_ thy od e_rls false real_add_commute t; term2str t;
4.41 -val SOME (t,_) = rewrite_ thy od e_rls false real_add_commute t; term2str t;
4.42 +val SOME (t,_) = rewrite_ thy od e_rls false add_commute t; term2str t;
4.43 +val SOME (t,_) = rewrite_ thy od e_rls false add_commute t; term2str t;
4.44 (*@@@ rew_sub gosub: t = d + (b + a + c)
4.45 @@@ rew_sub begin: t = b + a + c*)
4.46