1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Oct 02 15:14:51 2019 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Oct 02 16:02:17 2019 +0200
1.3 @@ -91,6 +91,9 @@
1.4 (*declare [[ML_print_depth = 999]]*)
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 +parseNEW @{context} "xxx #> aaa bbb"
1.8 +\<close> ML \<open>
1.9 +#> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
1.10 \<close> ML \<open>
1.11 \<close>
1.12 ML \<open>Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close>
2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Oct 02 15:14:51 2019 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed Oct 02 16:02:17 2019 +0200
2.3 @@ -183,7 +183,7 @@
2.4 cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''],
2.5 [''no_met'']) [BOOL_LIST equs, REAL_LIST vs];
2.6 B = Take (lastI funs);
2.7 - B = ((Substitute cons) @@ (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'')) B
2.8 + B = ((Substitute cons) #> (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'')) B
2.9 in B)"
2.10 setup \<open>KEStore_Elems.add_mets
2.11 [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
2.12 @@ -238,7 +238,7 @@
2.13 let
2.14 q___q = Take (qq v_v = q__q);
2.15 q___q = (
2.16 - (Rewrite ''sym_neg_equal_iff_equal'') @@
2.17 + (Rewrite ''sym_neg_equal_iff_equal'') #>
2.18 (Rewrite ''Belastung_Querkraft'')) q___q;
2.19 Q__Q = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
2.20 [''diff'', ''integration'', ''named'']) [REAL (rhs q___q), REAL v_v, REAL_REAL Q];
2.21 @@ -246,7 +246,7 @@
2.22 M__M = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
2.23 [''diff'', ''integration'', ''named'']) [REAL (rhs M__M), REAL v_v, REAL_REAL M_b];
2.24 N__N = (
2.25 - (Rewrite ''Moment_Neigung'' ) @@ (Rewrite ''make_fun_explicit'' )) M__M;
2.26 + (Rewrite ''Moment_Neigung'' ) #> (Rewrite ''make_fun_explicit'' )) M__M;
2.27 N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
2.28 [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl];
2.29 B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
3.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed Oct 02 15:14:51 2019 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Oct 02 16:02:17 2019 +0200
3.3 @@ -285,7 +285,7 @@
3.4 let
3.5 f_f' = Take (d_d v_v f_f)
3.6 in (
3.7 - (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'')) @@ (
3.8 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'')) #> (
3.9 Repeat (
3.10 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'')) Or
3.11 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'')) Or
3.12 @@ -303,7 +303,7 @@
3.13 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'')) Or
3.14 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'')) Or
3.15 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or
3.16 - (Repeat (Rewrite_Set ''make_polynomial'')))) @@ (
3.17 + (Repeat (Rewrite_Set ''make_polynomial'')))) #> (
3.18 Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv''))
3.19 ) f_f')"
3.20 setup \<open>KEStore_Elems.add_mets
3.21 @@ -357,7 +357,7 @@
3.22 let
3.23 f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))
3.24 in (
3.25 - (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' )) @@ (
3.26 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' )) #> (
3.27 Repeat (
3.28 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sum'')) Or
3.29 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_dif'' )) Or
3.30 @@ -376,7 +376,7 @@
3.31 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp_chain'')) Or
3.32 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_const'')) Or
3.33 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_var'')) Or
3.34 - (Repeat (Rewrite_Set ''make_polynomial'')))) @@ (
3.35 + (Repeat (Rewrite_Set ''make_polynomial'')))) #> (
3.36 Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' ))
3.37 ) f_f')"
3.38 setup \<open>KEStore_Elems.add_mets
3.39 @@ -395,10 +395,10 @@
3.40 let
3.41 term' = Take (d_d bound_variable term)
3.42 in (
3.43 - (Try (Rewrite_Set ''norm_Rational'')) @@
3.44 - (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_conv'')) @@
3.45 - (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''norm_diff'')) @@
3.46 - (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_sym_conv'')) @@
3.47 + (Try (Rewrite_Set ''norm_Rational'')) #>
3.48 + (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_conv'')) #>
3.49 + (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''norm_diff'')) #>
3.50 + (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_sym_conv'')) #>
3.51 (Try (Rewrite_Set ''norm_Rational''))
3.52 ) term')"
3.53
4.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Wed Oct 02 15:14:51 2019 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Wed Oct 02 16:02:17 2019 +0200
4.3 @@ -29,8 +29,8 @@
4.4 where
4.5 "diophant_equation e_e v_v = (
4.6 Repeat (
4.7 - (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) @@
4.8 - (Try (Calculate ''PLUS'')) @@
4.9 + (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
4.10 + (Try (Calculate ''PLUS'')) #>
4.11 (Try (Calculate ''TIMES''))) e_e)"
4.12 setup \<open>KEStore_Elems.add_mets
4.13 [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Oct 02 15:14:51 2019 +0200
5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Oct 02 16:02:17 2019 +0200
5.3 @@ -528,14 +528,14 @@
5.4 let
5.5 e_1 = Take (hd e_s);
5.6 e_1 = (
5.7 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'')) @@
5.8 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'')) #>
5.9 (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System''))
5.10 ) e_1;
5.11 e_2 = Take (hd (tl e_s));
5.12 e_2 = (
5.13 - (Substitute [e_1]) @@
5.14 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) @@
5.15 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) @@
5.16 + (Substitute [e_1]) #>
5.17 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) #>
5.18 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) #>
5.19 (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System'' ))
5.20 ) e_2;
5.21 e__s = Take [e_1, e_2]
5.22 @@ -570,10 +570,10 @@
5.23 "solve_system2 e_s v_s = (
5.24 let
5.25 e__s = (
5.26 - (Try (Rewrite_Set ''norm_Rational'' )) @@
5.27 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) @@
5.28 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) @@
5.29 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) @@
5.30 + (Try (Rewrite_Set ''norm_Rational'' )) #>
5.31 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) #>
5.32 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) #>
5.33 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) #>
5.34 (Try (Rewrite_Set ''order_system'' ))
5.35 ) e_s
5.36 in
5.37 @@ -598,14 +598,14 @@
5.38 "solve_system3 e_s v_s = (
5.39 let
5.40 e__s = (
5.41 - (Try (Rewrite_Set ''norm_Rational'' )) @@
5.42 - (Repeat (Rewrite ''commute_0_equality'' )) @@
5.43 + (Try (Rewrite_Set ''norm_Rational'' )) #>
5.44 + (Repeat (Rewrite ''commute_0_equality'' )) #>
5.45 (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ),
5.46 - (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) @@
5.47 + (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) #>
5.48 (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ),
5.49 - (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''isolate_bdvs_4x4'' )) @@
5.50 + (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''isolate_bdvs_4x4'' )) #>
5.51 (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ),
5.52 - (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) @@
5.53 + (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) #>
5.54 (Try (Rewrite_Set ''order_system''))
5.55 ) e_s
5.56 in
5.57 @@ -622,7 +622,7 @@
5.58 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
5.59 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
5.60 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
5.61 - (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
5.62 + (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
5.63 @{thm solve_system3.simps})]
5.64 \<close>
5.65
5.66 @@ -633,11 +633,11 @@
5.67 e_1 = NTH 1 e_s;
5.68 e_2 = Take (NTH 2 e_s);
5.69 e_2 = (
5.70 - (Substitute [e_1]) @@
5.71 + (Substitute [e_1]) #>
5.72 (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
5.73 - (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''simplify_System_parenthesized'' )) @@
5.74 + (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''simplify_System_parenthesized'' )) #>
5.75 (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
5.76 - (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''isolate_bdvs'' )) @@
5.77 + (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''isolate_bdvs'' )) #>
5.78 (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
5.79 (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''norm_Rational'' ))
5.80 ) e_2
5.81 @@ -658,7 +658,7 @@
5.82 prls = Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
5.83 [Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
5.84 crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
5.85 - (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
5.86 + (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
5.87 @{thm solve_system4.simps})]
5.88 \<close>
5.89
6.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Oct 02 15:14:51 2019 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Oct 02 16:02:17 2019 +0200
6.3 @@ -371,7 +371,7 @@
6.4 let
6.5 t_t = Take (F_F v_v = Integral f_f D v_v)
6.6 in (
6.7 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) @@
6.8 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) #>
6.9 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
6.10 ) t_t)"
6.11 setup \<open>KEStore_Elems.add_mets
7.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Wed Oct 02 15:14:51 2019 +0200
7.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Oct 02 16:02:17 2019 +0200
7.3 @@ -140,13 +140,13 @@
7.4 "solve_linear_equation e_e v_v = (
7.5 let
7.6 e_e = (
7.7 - (Try (Rewrite ''all_left'')) @@
7.8 - (Try (Repeat (Rewrite ''makex1_x''))) @@
7.9 - (Try (Rewrite_Set ''expand_binoms'')) @@
7.10 - (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in''))) @@
7.11 + (Try (Rewrite ''all_left'')) #>
7.12 + (Try (Repeat (Rewrite ''makex1_x''))) #>
7.13 + (Try (Rewrite_Set ''expand_binoms'')) #>
7.14 + (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in''))) #>
7.15 (Try (Repeat (Rewrite_Set ''LinPoly_simplify''))) ) e_e;
7.16 e_e = (
7.17 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''LinEq_simplify'')) @@
7.18 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''LinEq_simplify'')) #>
7.19 (Repeat (Try (Rewrite_Set ''LinPoly_simplify''))) ) e_e
7.20 in
7.21 Or_to_List e_e)"
8.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Wed Oct 02 15:14:51 2019 +0200
8.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed Oct 02 16:02:17 2019 +0200
8.3 @@ -38,8 +38,8 @@
8.4 "solve_log e_e v_v = (
8.5 let
8.6 e_e = (
8.7 - (Rewrite ''equality_power'') @@
8.8 - (Rewrite ''exp_invers_log'') @@
8.9 + (Rewrite ''equality_power'') #>
8.10 + (Rewrite ''exp_invers_log'') #>
8.11 (Rewrite_Set ''norm_Poly'') ) e_e
8.12 in
8.13 [e_e])"
9.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Oct 02 15:14:51 2019 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Oct 02 16:02:17 2019 +0200
9.3 @@ -1265,34 +1265,34 @@
9.4 where
9.5 "expand_binoms_2 term = (
9.6 Repeat (
9.7 - (Try (Repeat (Rewrite ''real_plus_binom_pow2''))) @@
9.8 - (Try (Repeat (Rewrite ''real_plus_binom_times''))) @@
9.9 - (Try (Repeat (Rewrite ''real_minus_binom_pow2''))) @@
9.10 - (Try (Repeat (Rewrite ''real_minus_binom_times''))) @@
9.11 - (Try (Repeat (Rewrite ''real_plus_minus_binom1''))) @@
9.12 - (Try (Repeat (Rewrite ''real_plus_minus_binom2''))) @@
9.13 + (Try (Repeat (Rewrite ''real_plus_binom_pow2''))) #>
9.14 + (Try (Repeat (Rewrite ''real_plus_binom_times''))) #>
9.15 + (Try (Repeat (Rewrite ''real_minus_binom_pow2''))) #>
9.16 + (Try (Repeat (Rewrite ''real_minus_binom_times''))) #>
9.17 + (Try (Repeat (Rewrite ''real_plus_minus_binom1''))) #>
9.18 + (Try (Repeat (Rewrite ''real_plus_minus_binom2''))) #>
9.19
9.20 - (Try (Repeat (Rewrite ''mult_1_left''))) @@
9.21 - (Try (Repeat (Rewrite ''mult_zero_left''))) @@
9.22 - (Try (Repeat (Rewrite ''add_0_left''))) @@
9.23 + (Try (Repeat (Rewrite ''mult_1_left''))) #>
9.24 + (Try (Repeat (Rewrite ''mult_zero_left''))) #>
9.25 + (Try (Repeat (Rewrite ''add_0_left''))) #>
9.26
9.27 - (Try (Repeat (Calculate ''PLUS''))) @@
9.28 - (Try (Repeat (Calculate ''TIMES''))) @@
9.29 - (Try (Repeat (Calculate ''POWER''))) @@
9.30 + (Try (Repeat (Calculate ''PLUS''))) #>
9.31 + (Try (Repeat (Calculate ''TIMES''))) #>
9.32 + (Try (Repeat (Calculate ''POWER''))) #>
9.33
9.34 - (Try (Repeat (Rewrite ''sym_realpow_twoI''))) @@
9.35 - (Try (Repeat (Rewrite ''realpow_plus_1''))) @@
9.36 - (Try (Repeat (Rewrite ''sym_real_mult_2''))) @@
9.37 - (Try (Repeat (Rewrite ''real_mult_2_assoc''))) @@
9.38 + (Try (Repeat (Rewrite ''sym_realpow_twoI''))) #>
9.39 + (Try (Repeat (Rewrite ''realpow_plus_1''))) #>
9.40 + (Try (Repeat (Rewrite ''sym_real_mult_2''))) #>
9.41 + (Try (Repeat (Rewrite ''real_mult_2_assoc''))) #>
9.42
9.43 - (Try (Repeat (Rewrite ''real_num_collect''))) @@
9.44 - (Try (Repeat (Rewrite ''real_num_collect_assoc''))) @@
9.45 + (Try (Repeat (Rewrite ''real_num_collect''))) #>
9.46 + (Try (Repeat (Rewrite ''real_num_collect_assoc''))) #>
9.47
9.48 - (Try (Repeat (Rewrite ''real_one_collect''))) @@
9.49 - (Try (Repeat (Rewrite ''real_one_collect_assoc''))) @@
9.50 + (Try (Repeat (Rewrite ''real_one_collect''))) #>
9.51 + (Try (Repeat (Rewrite ''real_one_collect_assoc''))) #>
9.52
9.53 - (Try (Repeat (Calculate ''PLUS''))) @@
9.54 - (Try (Repeat (Calculate ''TIMES''))) @@
9.55 + (Try (Repeat (Calculate ''PLUS''))) #>
9.56 + (Try (Repeat (Calculate ''TIMES''))) #>
9.57 (Try (Repeat (Calculate ''POWER''))))
9.58 term)"
9.59 ML \<open>
10.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Oct 02 15:14:51 2019 +0200
10.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Oct 02 16:02:17 2019 +0200
10.3 @@ -913,10 +913,10 @@
10.4 "normalize_poly_eq e_e v_v = (
10.5 let
10.6 e_e = (
10.7 - (Try (Rewrite ''all_left'')) @@
10.8 - (Try (Repeat (Rewrite ''makex1_x''))) @@
10.9 - (Try (Repeat (Rewrite_Set ''expand_binoms''))) @@
10.10 - (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in''))) @@
10.11 + (Try (Rewrite ''all_left'')) #>
10.12 + (Try (Repeat (Rewrite ''makex1_x''))) #>
10.13 + (Try (Repeat (Rewrite_Set ''expand_binoms''))) #>
10.14 + (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in''))) #>
10.15 (Try (Repeat (Rewrite_Set ''polyeq_simplify''))) ) e_e
10.16 in
10.17 SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
10.18 @@ -956,8 +956,8 @@
10.19 "solve_poly_eq1 e_e v_v = (
10.20 let
10.21 e_e = (
10.22 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'')) @@
10.23 - (Try (Rewrite_Set ''polyeq_simplify'')) @@
10.24 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'')) #>
10.25 + (Try (Rewrite_Set ''polyeq_simplify'')) #>
10.26 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
10.27 L_L = Or_to_List e_e
10.28 in
10.29 @@ -979,10 +979,10 @@
10.30 "solve_poly_equ2 e_e v_v = (
10.31 let
10.32 e_e = (
10.33 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'')) @@
10.34 - (Try (Rewrite_Set ''polyeq_simplify'')) @@
10.35 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'')) @@
10.36 - (Try (Rewrite_Set ''polyeq_simplify'')) @@
10.37 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'')) #>
10.38 + (Try (Rewrite_Set ''polyeq_simplify'')) #>
10.39 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'')) #>
10.40 + (Try (Rewrite_Set ''polyeq_simplify'')) #>
10.41 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
10.42 L_L = Or_to_List e_e
10.43 in
10.44 @@ -1004,10 +1004,10 @@
10.45 "solve_poly_equ0 e_e v_v = (
10.46 let
10.47 e_e = (
10.48 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_bdv_only_simplify'')) @@
10.49 - (Try (Rewrite_Set ''polyeq_simplify'')) @@
10.50 - (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''d1_polyeq_simplify'')) @@
10.51 - (Try (Rewrite_Set ''polyeq_simplify'')) @@
10.52 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_bdv_only_simplify'')) #>
10.53 + (Try (Rewrite_Set ''polyeq_simplify'')) #>
10.54 + (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''d1_polyeq_simplify'')) #>
10.55 + (Try (Rewrite_Set ''polyeq_simplify'')) #>
10.56 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
10.57 L_L = Or_to_List e_e
10.58 in
10.59 @@ -1029,8 +1029,8 @@
10.60 "solve_poly_equ_sqrt e_e v_v = (
10.61 let
10.62 e_e = (
10.63 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_sq_only_simplify'')) @@
10.64 - (Try (Rewrite_Set ''polyeq_simplify'')) @@
10.65 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_sq_only_simplify'')) #>
10.66 + (Try (Rewrite_Set ''polyeq_simplify'')) #>
10.67 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
10.68 L_L = Or_to_List e_e
10.69 in
10.70 @@ -1052,8 +1052,8 @@
10.71 "solve_poly_equ_pq e_e v_v = (
10.72 let
10.73 e_e = (
10.74 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_pqFormula_simplify'')) @@
10.75 - (Try (Rewrite_Set ''polyeq_simplify'')) @@
10.76 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_pqFormula_simplify'')) #>
10.77 + (Try (Rewrite_Set ''polyeq_simplify'')) #>
10.78 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
10.79 L_L = Or_to_List e_e
10.80 in
10.81 @@ -1075,8 +1075,8 @@
10.82 "solve_poly_equ_abc e_e v_v = (
10.83 let
10.84 e_e = (
10.85 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_abcFormula_simplify'')) @@
10.86 - (Try (Rewrite_Set ''polyeq_simplify'')) @@
10.87 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_abcFormula_simplify'')) #>
10.88 + (Try (Rewrite_Set ''polyeq_simplify'')) #>
10.89 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
10.90 L_L = Or_to_List e_e
10.91 in Check_elementwise L_L {(v_v::real). Assumptions})"
10.92 @@ -1097,12 +1097,12 @@
10.93 "solve_poly_equ3 e_e v_v = (
10.94 let
10.95 e_e = (
10.96 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d3_polyeq_simplify'')) @@
10.97 - (Try (Rewrite_Set ''polyeq_simplify'')) @@
10.98 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'')) @@
10.99 - (Try (Rewrite_Set ''polyeq_simplify'')) @@
10.100 - (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''d1_polyeq_simplify'')) @@
10.101 - (Try (Rewrite_Set ''polyeq_simplify'')) @@
10.102 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d3_polyeq_simplify'')) #>
10.103 + (Try (Rewrite_Set ''polyeq_simplify'')) #>
10.104 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'')) #>
10.105 + (Try (Rewrite_Set ''polyeq_simplify'')) #>
10.106 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''d1_polyeq_simplify'')) #>
10.107 + (Try (Rewrite_Set ''polyeq_simplify'')) #>
10.108 (Try (Rewrite_Set ''norm_Rational_parenthesized''))) e_e;
10.109 L_L = Or_to_List e_e
10.110 in
10.111 @@ -1125,15 +1125,15 @@
10.112 where
10.113 "solve_by_completing_square e_e v_v = (
10.114 let e_e = (
10.115 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''cancel_leading_coeff'')) @@
10.116 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''complete_square'')) @@
10.117 - (Try (Rewrite ''square_explicit1'')) @@
10.118 - (Try (Rewrite ''square_explicit2'')) @@
10.119 - (Rewrite ''root_plus_minus'') @@
10.120 - (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit1''))) @@
10.121 - (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit2''))) @@
10.122 - (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit3''))) @@
10.123 - (Try (Rewrite_Set ''calculate_RootRat'')) @@
10.124 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''cancel_leading_coeff'')) #>
10.125 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''complete_square'')) #>
10.126 + (Try (Rewrite ''square_explicit1'')) #>
10.127 + (Try (Rewrite ''square_explicit2'')) #>
10.128 + (Rewrite ''root_plus_minus'') #>
10.129 + (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit1''))) #>
10.130 + (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit2''))) #>
10.131 + (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit3''))) #>
10.132 + (Try (Rewrite_Set ''calculate_RootRat'')) #>
10.133 (Try (Repeat (Calculate ''SQRT'')))) e_e
10.134 in
10.135 Or_to_List e_e)"
11.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed Oct 02 15:14:51 2019 +0200
11.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed Oct 02 16:02:17 2019 +0200
11.3 @@ -475,8 +475,8 @@
11.4 where
11.5 "simplify t_t = (
11.6 (Repeat(
11.7 - (Try (Rewrite_Set ''ordne_alphabetisch'')) @@
11.8 - (Try (Rewrite_Set ''fasse_zusammen'')) @@
11.9 + (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
11.10 + (Try (Rewrite_Set ''fasse_zusammen'')) #>
11.11 (Try (Rewrite_Set ''verschoenere'')))
11.12 ) t_t)"
11.13 setup \<open>KEStore_Elems.add_mets
11.14 @@ -509,9 +509,9 @@
11.15 where
11.16 "simplify2 t_t = (
11.17 (Repeat(
11.18 - (Try (Rewrite_Set ''klammern_aufloesen'')) @@
11.19 - (Try (Rewrite_Set ''ordne_alphabetisch'')) @@
11.20 - (Try (Rewrite_Set ''fasse_zusammen'')) @@
11.21 + (Try (Rewrite_Set ''klammern_aufloesen'')) #>
11.22 + (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
11.23 + (Try (Rewrite_Set ''fasse_zusammen'')) #>
11.24 (Try (Rewrite_Set ''verschoenere'')))
11.25 ) t_t)"
11.26 setup \<open>KEStore_Elems.add_mets
11.27 @@ -531,12 +531,12 @@
11.28 where
11.29 "simplify3 t_t = (
11.30 (Repeat(
11.31 - (Try (Rewrite_Set ''klammern_ausmultiplizieren'')) @@
11.32 - (Try (Rewrite_Set ''discard_parentheses'')) @@
11.33 - (Try (Rewrite_Set ''ordne_monome'')) @@
11.34 - (Try (Rewrite_Set ''klammern_aufloesen'')) @@
11.35 - (Try (Rewrite_Set ''ordne_alphabetisch'')) @@
11.36 - (Try (Rewrite_Set ''fasse_zusammen'')) @@
11.37 + (Try (Rewrite_Set ''klammern_ausmultiplizieren'')) #>
11.38 + (Try (Rewrite_Set ''discard_parentheses'')) #>
11.39 + (Try (Rewrite_Set ''ordne_monome'')) #>
11.40 + (Try (Rewrite_Set ''klammern_aufloesen'')) #>
11.41 + (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
11.42 + (Try (Rewrite_Set ''fasse_zusammen'')) #>
11.43 (Try (Rewrite_Set ''verschoenere'')))
11.44 ) t_t)"
11.45 setup \<open>KEStore_Elems.add_mets
11.46 @@ -565,8 +565,8 @@
11.47 e_e = Substitute w_w e_e
11.48 in (
11.49 Repeat (
11.50 - (Try (Repeat (Calculate ''TIMES''))) @@
11.51 - (Try (Repeat (Calculate ''PLUS'' ))) @@
11.52 + (Try (Repeat (Calculate ''TIMES''))) #>
11.53 + (Try (Repeat (Calculate ''PLUS'' ))) #>
11.54 (Try (Repeat (Calculate ''MINUS''))))
11.55 ) e_e)"
11.56 setup \<open>KEStore_Elems.add_mets
12.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Wed Oct 02 15:14:51 2019 +0200
12.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed Oct 02 16:02:17 2019 +0200
12.3 @@ -180,9 +180,9 @@
12.4 "solve_rational_equ e_e v_v =
12.5 (let
12.6 e_e = (
12.7 - (Repeat (Try (Rewrite_Set ''RatEq_simplify''))) @@
12.8 - (Repeat (Try (Rewrite_Set ''norm_Rational''))) @@
12.9 - (Repeat (Try (Rewrite_Set ''add_fractions_p''))) @@
12.10 + (Repeat (Try (Rewrite_Set ''RatEq_simplify''))) #>
12.11 + (Repeat (Try (Rewrite_Set ''norm_Rational''))) #>
12.12 + (Repeat (Try (Rewrite_Set ''add_fractions_p''))) #>
12.13 (Repeat (Try (Rewrite_Set ''RatEq_eliminate''))) ) e_e;
12.14 L_L = SubProblem (''RatEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v]
12.15 in
13.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Oct 02 15:14:51 2019 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Oct 02 16:02:17 2019 +0200
13.3 @@ -894,16 +894,16 @@
13.4 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
13.5 where
13.6 "simplify t_t = (
13.7 - (Try (Rewrite_Set ''discard_minus'') @@
13.8 - Try (Rewrite_Set ''rat_mult_poly'') @@
13.9 - Try (Rewrite_Set ''make_rat_poly_with_parentheses'') @@
13.10 - Try (Rewrite_Set ''cancel_p_rls'') @@
13.11 + (Try (Rewrite_Set ''discard_minus'') #>
13.12 + Try (Rewrite_Set ''rat_mult_poly'') #>
13.13 + Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
13.14 + Try (Rewrite_Set ''cancel_p_rls'') #>
13.15 (Repeat (
13.16 - Try (Rewrite_Set ''add_fractions_p_rls'') @@
13.17 - Try (Rewrite_Set ''rat_mult_div_pow'') @@
13.18 - Try (Rewrite_Set ''make_rat_poly_with_parentheses'') @@
13.19 - Try (Rewrite_Set ''cancel_p_rls'') @@
13.20 - Try (Rewrite_Set ''rat_reduce_1''))) @@
13.21 + Try (Rewrite_Set ''add_fractions_p_rls'') #>
13.22 + Try (Rewrite_Set ''rat_mult_div_pow'') #>
13.23 + Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
13.24 + Try (Rewrite_Set ''cancel_p_rls'') #>
13.25 + Try (Rewrite_Set ''rat_reduce_1''))) #>
13.26 Try (Rewrite_Set ''discard_parentheses1''))
13.27 t_t)"
13.28 setup \<open>KEStore_Elems.add_mets
14.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Wed Oct 02 15:14:51 2019 +0200
14.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Oct 02 16:02:17 2019 +0200
14.3 @@ -485,10 +485,10 @@
14.4 "norm_sqrt_equ e_e v_v = (
14.5 let
14.6 e_e = (
14.7 - (Repeat(Try (Rewrite ''makex1_x''))) @@
14.8 - (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) @@
14.9 - (Try (Rewrite_Set ''rooteq_simplify'')) @@
14.10 - (Try (Repeat (Rewrite_Set ''make_rooteq''))) @@
14.11 + (Repeat(Try (Rewrite ''makex1_x''))) #>
14.12 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
14.13 + (Try (Rewrite_Set ''rooteq_simplify'')) #>
14.14 + (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
14.15 (Try (Rewrite_Set ''rooteq_simplify''))
14.16 ) e_e
14.17 in
14.18 @@ -513,10 +513,10 @@
14.19 "solve_sqrt_equ e_e v_v =
14.20 (let
14.21 e_e = (
14.22 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''sqrt_isolate'')) @@
14.23 - (Try (Rewrite_Set ''rooteq_simplify'')) @@
14.24 - (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) @@
14.25 - (Try (Repeat (Rewrite_Set ''make_rooteq ''))) @@
14.26 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''sqrt_isolate'')) #>
14.27 + (Try (Rewrite_Set ''rooteq_simplify'')) #>
14.28 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
14.29 + (Try (Repeat (Rewrite_Set ''make_rooteq ''))) #>
14.30 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e;
14.31 L_L =
14.32 (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))
14.33 @@ -546,10 +546,10 @@
14.34 "solve_sqrt_equ_right e_e v_v =
14.35 (let
14.36 e_e = (
14.37 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'')) @@
14.38 - (Try (Rewrite_Set ''rooteq_simplify'')) @@
14.39 - (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) @@
14.40 - (Try (Repeat (Rewrite_Set ''make_rooteq''))) @@
14.41 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'')) #>
14.42 + (Try (Rewrite_Set ''rooteq_simplify'')) #>
14.43 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
14.44 + (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
14.45 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
14.46 in
14.47 if (rhs e_e) is_sqrtTerm_in v_v
14.48 @@ -575,10 +575,10 @@
14.49 "solve_sqrt_equ_left e_e v_v =
14.50 (let
14.51 e_e = (
14.52 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'')) @@
14.53 - (Try (Rewrite_Set ''rooteq_simplify'')) @@
14.54 - (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) @@
14.55 - (Try (Repeat (Rewrite_Set ''make_rooteq''))) @@
14.56 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'')) #>
14.57 + (Try (Rewrite_Set ''rooteq_simplify'')) #>
14.58 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) #>
14.59 + (Try (Repeat (Rewrite_Set ''make_rooteq''))) #>
14.60 (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
14.61 in
14.62 if (lhs e_e) is_sqrtTerm_in v_v
15.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Wed Oct 02 15:14:51 2019 +0200
15.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed Oct 02 16:02:17 2019 +0200
15.3 @@ -150,10 +150,10 @@
15.4 "solve_rootrat_equ e_e v_v =
15.5 (let
15.6 e_e = (
15.7 - (Try (Rewrite_Set ''expand_rootbinoms'')) @@
15.8 - (Try (Rewrite_Set ''rooteq_simplify'')) @@
15.9 - (Try (Rewrite_Set ''make_rooteq'')) @@
15.10 - (Try (Rewrite_Set ''rooteq_simplify'')) @@
15.11 + (Try (Rewrite_Set ''expand_rootbinoms'')) #>
15.12 + (Try (Rewrite_Set ''rooteq_simplify'')) #>
15.13 + (Try (Rewrite_Set ''make_rooteq'')) #>
15.14 + (Try (Rewrite_Set ''rooteq_simplify'')) #>
15.15 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'')) ) e_e
15.16 in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"
15.17 setup \<open>KEStore_Elems.add_mets
16.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Oct 02 15:14:51 2019 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Oct 02 16:02:17 2019 +0200
16.3 @@ -844,7 +844,7 @@
16.4 "solve_linear e_e v_v = (
16.5 let e_e =
16.6 Repeat (
16.7 - (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') @@
16.8 + (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') #>
16.9 (Rewrite_Set ''Test_simplify'')) e_e
16.10 in
16.11 [e_e])"
16.12 @@ -867,14 +867,14 @@
16.13 let
16.14 e_e = (
16.15 (While (contains_root e_e) Do (
16.16 - (Rewrite ''square_equation_left'' ) @@
16.17 - (Try (Rewrite_Set ''Test_simplify'' )) @@
16.18 - (Try (Rewrite_Set ''rearrange_assoc'' )) @@
16.19 - (Try (Rewrite_Set ''isolate_root'' )) @@
16.20 - (Try (Rewrite_Set ''Test_simplify'' )))) @@
16.21 - (Try (Rewrite_Set ''norm_equation'' )) @@
16.22 - (Try (Rewrite_Set ''Test_simplify'' )) @@
16.23 - (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' ) @@
16.24 + (Rewrite ''square_equation_left'' ) #>
16.25 + (Try (Rewrite_Set ''Test_simplify'' )) #>
16.26 + (Try (Rewrite_Set ''rearrange_assoc'' )) #>
16.27 + (Try (Rewrite_Set ''isolate_root'' )) #>
16.28 + (Try (Rewrite_Set ''Test_simplify'' )))) #>
16.29 + (Try (Rewrite_Set ''norm_equation'' )) #>
16.30 + (Try (Rewrite_Set ''Test_simplify'' )) #>
16.31 + (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' ) #>
16.32 (Try (Rewrite_Set ''Test_simplify'' ))
16.33 ) e_e
16.34 in
16.35 @@ -901,7 +901,7 @@
16.36 "minisubpbl e_e v_v = (
16.37 let
16.38 e_e = (
16.39 - (Try (Rewrite_Set ''norm_equation'' )) @@
16.40 + (Try (Rewrite_Set ''norm_equation'' )) #>
16.41 (Try (Rewrite_Set ''Test_simplify'' ))) e_e;
16.42 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
16.43 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
16.44 @@ -927,12 +927,12 @@
16.45 let
16.46 e_e = (
16.47 (While (contains_root e_e) Do (
16.48 - (Rewrite ''square_equation_left'' ) @@
16.49 - (Try (Rewrite_Set ''Test_simplify'' )) @@
16.50 - (Try (Rewrite_Set ''rearrange_assoc'' )) @@
16.51 - (Try (Rewrite_Set ''isolate_root'' )) @@
16.52 - (Try (Rewrite_Set ''Test_simplify'' )))) @@
16.53 - (Try (Rewrite_Set ''norm_equation'' )) @@
16.54 + (Rewrite ''square_equation_left'' ) #>
16.55 + (Try (Rewrite_Set ''Test_simplify'' )) #>
16.56 + (Try (Rewrite_Set ''rearrange_assoc'' )) #>
16.57 + (Try (Rewrite_Set ''isolate_root'' )) #>
16.58 + (Try (Rewrite_Set ''Test_simplify'' )))) #>
16.59 + (Try (Rewrite_Set ''norm_equation'' )) #>
16.60 (Try (Rewrite_Set ''Test_simplify'' ))
16.61 ) e_e;
16.62 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
16.63 @@ -960,12 +960,12 @@
16.64 e_e = (
16.65 (While (contains_root e_e) Do ((
16.66 (Rewrite ''square_equation_left'' ) Or
16.67 - (Rewrite ''square_equation_right'' )) @@
16.68 - (Try (Rewrite_Set ''Test_simplify'' )) @@
16.69 - (Try (Rewrite_Set ''rearrange_assoc'' )) @@
16.70 - (Try (Rewrite_Set ''isolate_root'' )) @@
16.71 - (Try (Rewrite_Set ''Test_simplify'' )))) @@
16.72 - (Try (Rewrite_Set ''norm_equation'' )) @@
16.73 + (Rewrite ''square_equation_right'' )) #>
16.74 + (Try (Rewrite_Set ''Test_simplify'' )) #>
16.75 + (Try (Rewrite_Set ''rearrange_assoc'' )) #>
16.76 + (Try (Rewrite_Set ''isolate_root'' )) #>
16.77 + (Try (Rewrite_Set ''Test_simplify'' )))) #>
16.78 + (Try (Rewrite_Set ''norm_equation'' )) #>
16.79 (Try (Rewrite_Set ''Test_simplify'' ))
16.80 ) e_e;
16.81 L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],
16.82 @@ -993,12 +993,12 @@
16.83 e_e = (
16.84 (While (contains_root e_e) Do ((
16.85 (Rewrite ''square_equation_left'' ) Or
16.86 - (Rewrite ''square_equation_right'' )) @@
16.87 - (Try (Rewrite_Set ''Test_simplify'' )) @@
16.88 - (Try (Rewrite_Set ''rearrange_assoc'' )) @@
16.89 - (Try (Rewrite_Set ''isolate_root'' )) @@
16.90 - (Try (Rewrite_Set ''Test_simplify'' )))) @@
16.91 - (Try (Rewrite_Set ''norm_equation'' )) @@
16.92 + (Rewrite ''square_equation_right'' )) #>
16.93 + (Try (Rewrite_Set ''Test_simplify'' )) #>
16.94 + (Try (Rewrite_Set ''rearrange_assoc'' )) #>
16.95 + (Try (Rewrite_Set ''isolate_root'' )) #>
16.96 + (Try (Rewrite_Set ''Test_simplify'' )))) #>
16.97 + (Try (Rewrite_Set ''norm_equation'' )) #>
16.98 (Try (Rewrite_Set ''Test_simplify'' ))
16.99 ) e_e;
16.100 L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
16.101 @@ -1024,10 +1024,10 @@
16.102 "solve_plain_square e_e v_v = (
16.103 let
16.104 e_e = (
16.105 - (Try (Rewrite_Set ''isolate_bdv'' )) @@
16.106 - (Try (Rewrite_Set ''Test_simplify'' )) @@
16.107 + (Try (Rewrite_Set ''isolate_bdv'' )) #>
16.108 + (Try (Rewrite_Set ''Test_simplify'' )) #>
16.109 ((Rewrite ''square_equality_0'' ) Or
16.110 - (Rewrite ''square_equality'' )) @@
16.111 + (Rewrite ''square_equality'' )) #>
16.112 (Try (Rewrite_Set ''tval_rls'' ))) e_e
16.113 in
16.114 Or_to_List e_e)"
16.115 @@ -1053,7 +1053,7 @@
16.116 "norm_univariate_equ e_e v_v = (
16.117 let
16.118 e_e = (
16.119 - (Try (Rewrite ''rnorm_equation_add'' )) @@
16.120 + (Try (Rewrite ''rnorm_equation_add'' )) #>
16.121 (Try (Rewrite_Set ''Test_simplify'' )) ) e_e
16.122 in
16.123 SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
16.124 @@ -1074,7 +1074,7 @@
16.125 where
16.126 "test_simplify t_t = (
16.127 Repeat (
16.128 - (Try (Calculate ''PLUS'')) @@
16.129 + (Try (Calculate ''PLUS'')) #>
16.130 (Try (Calculate ''TIMES''))) t_t)"
16.131 setup \<open>KEStore_Elems.add_mets
16.132 [Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID
17.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Oct 02 15:14:51 2019 +0200
17.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Oct 02 16:02:17 2019 +0200
17.3 @@ -41,7 +41,7 @@
17.4 val is_calc: term -> bool
17.5 val rule2stac: theory -> Rule.rule -> term
17.6 val rule2stac_inst: theory -> Rule.rule -> term
17.7 - val @@ : term list -> term
17.8 + val #> : term list -> term
17.9 val rules2scr_Rls : theory -> Rule.rule list -> term
17.10 val rules2scr_Seq : theory -> Rule.rule list -> term
17.11 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
17.12 @@ -125,8 +125,8 @@
17.13 val Rew_Set_Inst $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
17.14 "Rewrite_Set_Inst [(''bdv'',v)] ''real_diff_minus''";
17.15 val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
17.16 - " ((Try (Repeat (Rewrite ''real_diff_minus''))) @@ \
17.17 - \ (Try (Repeat (Rewrite ''add_commute''))) @@ \
17.18 + " ((Try (Repeat (Rewrite ''real_diff_minus''))) #> \
17.19 + \ (Try (Repeat (Rewrite ''add_commute''))) #> \
17.20 \ (Try (Repeat (Rewrite ''mult_commute'')))) t";
17.21
17.22 fun rule2stac _ (Rule.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ HOLogic.mk_string thmID))
17.23 @@ -145,15 +145,15 @@
17.24 | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.rule2str r ^ "\"");
17.25
17.26 (*for appropriate nesting take stacs in _reverse_ order*)
17.27 -fun op @@@ sts [s] = SEq $ s $ sts
17.28 - | op @@@ sts (s::ss) = op @@@ (SEq $ s $ sts) ss
17.29 - | op @@@ t ts =
17.30 - raise ERROR ("fun @@@ not applicable to \"" ^ Rule.term2str t ^ "\" \"" ^ Rule.terms2str ts ^ "\"");
17.31 -fun @@ [stac] = stac
17.32 - | @@ [s1, s2] = SEq $ s1 $ s2
17.33 - | @@ stacs = case rev stacs of
17.34 - s3 :: s2 :: ss => op @@@ (SEq $ s2 $ s3) ss
17.35 - | ts => raise ERROR ("fun @@ not applicable to \"" ^ Rule.terms2str ts ^ "\"")
17.36 +fun op #>@ sts [s] = SEq $ s $ sts
17.37 + | op #>@ sts (s::ss) = op #>@ (SEq $ s $ sts) ss
17.38 + | op #>@ t ts =
17.39 + raise ERROR ("fun #>@ not applicable to \"" ^ Rule.term2str t ^ "\" \"" ^ Rule.terms2str ts ^ "\"");
17.40 +fun #> [stac] = stac
17.41 + | #> [s1, s2] = SEq $ s1 $ s2
17.42 + | #> stacs = case rev stacs of
17.43 + s3 :: s2 :: ss => op #>@ (SEq $ s2 $ s3) ss
17.44 + | ts => raise ERROR ("fun #> not applicable to \"" ^ Rule.terms2str ts ^ "\"")
17.45
17.46 val contains_bdv = (not o null o (filter TermC.is_bdv) o TermC.ids2str o #prop o Thm.rep_thm);
17.47
17.48 @@ -194,12 +194,12 @@
17.49
17.50 fun rules2scr_Rls thy rules =
17.51 if contain_bdv rules
17.52 - then FunID_Term_Bdv $ (Repeat $ (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term))
17.53 - else FunID_Term $ (Repeat $ (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term));
17.54 + then FunID_Term_Bdv $ (Repeat $ (((#> o (map (rule2stac_inst thy))) rules) $ Rule.e_term))
17.55 + else FunID_Term $ (Repeat $ (((#> o (map (rule2stac thy))) rules) $ Rule.e_term));
17.56 fun rules2scr_Seq thy rules =
17.57 if contain_bdv rules
17.58 - then FunID_Term_Bdv $ (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term)
17.59 - else FunID_Term $ (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term);
17.60 + then FunID_Term_Bdv $ (((#> o (map (rule2stac_inst thy))) rules) $ Rule.e_term)
17.61 + else FunID_Term $ (((#> o (map (rule2stac thy))) rules) $ Rule.e_term);
17.62
17.63 (* prepare the input for an rls for use:
17.64 # generate a script for stepwise execution of the rls
18.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Oct 02 15:14:51 2019 +0200
18.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Oct 02 16:02:17 2019 +0200
18.3 @@ -258,8 +258,8 @@
18.4 (*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)
18.5 fun eval_occurs_in _ "Prog_Expr.occurs'_in"
18.6 (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
18.7 - ((*tracing("@@@ eval_occurs_in: v= "^(Rule.term2str v));
18.8 - tracing("@@@ eval_occurs_in: t= "^(Rule.term2str t));*)
18.9 + ((*tracing("#>@ eval_occurs_in: v= "^(Rule.term2str v));
18.10 + tracing("#>@ eval_occurs_in: t= "^(Rule.term2str t));*)
18.11 if occurs_in v t
18.12 then SOME ((Rule.term2str p) ^ " = True",
18.13 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
18.14 @@ -474,7 +474,7 @@
18.15 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
18.16 in SOME (TermC.mk_thmid thmid n1 n2, prop) end
18.17 end
18.18 - | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
18.19 + | _ => ((*tracing"#>@ eval_cancel NONE";*)NONE))
18.20 | eval_cancel _ _ _ _ = NONE;
18.21
18.22 (* get the argument from a function-definition *)
19.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Oct 02 15:14:51 2019 +0200
19.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Oct 02 16:02:17 2019 +0200
19.3 @@ -37,11 +37,11 @@
19.4 Calculate :: "[char list, 'a] => 'a"
19.5 Rewrite :: "[char list, 'a] => 'a"
19.6 Rewrite'_Inst:: "[(char list * 'b) list, char list, 'a] => 'a"
19.7 - ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for @@*)
19.8 + ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
19.9 Rewrite'_Set :: "[char list, 'a] => 'a" ("(Rewrite'_Set (_))" 11)
19.10 Rewrite'_Set'_Inst
19.11 :: "[((char list) * 'b) list, char list, 'a] => 'a"
19.12 - ("(Rewrite'_Set'_Inst (_ _))" 11) (*without last argument ^^ for @@*)
19.13 + ("(Rewrite'_Set'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
19.14 Or'_to'_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
19.15 SubProblem :: "[char list * char list list * char list list, arg list] => 'a"
19.16 Substitute :: "[bool list, 'a] => 'a"
19.17 @@ -82,7 +82,7 @@
19.18 (* get argument of first Prog_Tac in a progam for init_form *)
19.19 fun get_stac thy (_ $ body) =
19.20 let
19.21 - (* entries occur twice, for form curried by @@ or non-curried *)
19.22 + (* entries occur twice, for form curried by #> or non-curried *)
19.23 fun get_t y (Const ("Tactical.Seq",_) $ e1 $ e2) a =
19.24 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
19.25 | get_t y (Const ("Tactical.Seq",_) $ e1 $ e2 $ a) _ =
19.26 @@ -124,7 +124,7 @@
19.27
19.28 (* substitute the Istate.T's environment to a leaf of the program
19.29 and attach the curried argument of a tactic, if any.
19.30 -CAUTION: (1) currying with @@ requires 2 patterns for each tactic
19.31 +CAUTION: (1) currying with #> requires 2 patterns for each tactic
19.32 (2) the non-curried version must return NONE for a
19.33 (3) non-matching patterns become an Celem.Expr by fall-through.
19.34 WN060906 quick and dirty fix: due to (2) a is returned, too *)
20.1 --- a/src/Tools/isac/ProgLang/Tactical.thy Wed Oct 02 15:14:51 2019 +0200
20.2 +++ b/src/Tools/isac/ProgLang/Tactical.thy Wed Oct 02 16:02:17 2019 +0200
20.3 @@ -12,7 +12,7 @@
20.4 \<close>
20.5 subsection \<open>Consts for tacticals\<close>
20.6 consts
20.7 - Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*)
20.8 + Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10) (*@ used*)
20.9 Try :: "['a => 'a, 'a] => 'a"
20.10 Repeat :: "['a => 'a, 'a] => 'a"
20.11 Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
21.1 --- a/src/Tools/isac/TODO.thy Wed Oct 02 15:14:51 2019 +0200
21.2 +++ b/src/Tools/isac/TODO.thy Wed Oct 02 16:02:17 2019 +0200
21.3 @@ -14,12 +14,6 @@
21.4 text \<open>
21.5 \begin{itemize}
21.6 \item xxx
21.7 - \item generalise
21.8 - Rewrite'_Inst:: "[(char list * real) list, char list, 'a] => 'a"
21.9 - ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for @@*)
21.10 - ->Rewrite'_Inst:: "[(char list * 'b) list, char list, 'a] => 'a"
21.11 - ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for @@*)
21.12 -
21.13 \item xxx
21.14 \item fun handle_leaf: trace_prog .. separate message
21.15 \item xxx
21.16 @@ -30,7 +24,7 @@
21.17 ?consistency with subst term?
21.18 \item Tactic.Rewrite*: drop "bool"
21.19 \item xxx
21.20 - \item Prog_Tac.contain + Tactical.contain with contains_Const
21.21 + \item Prog_Tac.contain + Tactical.contain using contains_Const
21.22 \item exception PROG analogous to TERM
21.23 \item xxx
21.24 \item xxx
21.25 @@ -48,7 +42,7 @@
21.26 \item rename list_rls accordingly
21.27 \item ------------------------------------------------------------------/
21.28 \item xxx
21.29 - \item lucas-interpreter.sml ----- vvvvvvvvv
21.30 + \item lucas-interpreter.sml ----- vvvvvvvvv etc.
21.31 val (p'',_,_,pt'') = Generate.generate1 @ {theory} tac' (Istate.Pstate is, ctxt) (po', p_) pt
21.32 \item xxx
21.33 \item fun fun eval_* //thy//
21.34 @@ -158,8 +152,6 @@
21.35 \item xxx
21.36 \item xxx
21.37 \item xxx
21.38 - \item language definition: use (f #> g) x = x |> f |> g instead of @
21.39 - see implementation.pdf p.16
21.40 \item xxx
21.41 \item xxx
21.42 \item xxx
22.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Oct 02 15:14:51 2019 +0200
22.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Oct 02 16:02:17 2019 +0200
22.3 @@ -220,7 +220,8 @@
22.4 val theID = ["IsacKnowledge", "Poly", "Rulesets", "expand"]
22.5 val hrls = get_the theID
22.6 ;
22.7 -if thydata2xml (theID, hrls) = ("<RULESETDATA>\n" ^
22.8 +if thydata2xml (theID, hrls) = (
22.9 +"<RULESETDATA>\n" ^
22.10 " <GUH> thy_isac_Poly-rls-expand </GUH>\n" ^
22.11 " <STRINGLIST>\n" ^
22.12 " <STRING> IsacKnowledge </STRING>\n" ^
22.13 @@ -231,7 +232,7 @@
22.14 " <ID> expand </ID>\n" ^
22.15 " <TYPE> Rls </TYPE>\n" ^
22.16 " <RULES>\n" ^
22.17 -" <RULE>\n" ^
22.18 +" <RULE>\n" ^
22.19 " <TAG> Theorem </TAG>\n" ^
22.20 " <STRING> distrib_right </STRING>\n" ^
22.21 " <GUH> thy_isac_distrib_right-thm-distrib_right </GUH>\n" ^
22.22 @@ -242,7 +243,8 @@
22.23 " <GUH> thy_isac_distrib_left-thm-distrib_left </GUH>\n" ^
22.24 " </RULE>\n" ^
22.25 " </RULES>\n" ^
22.26 -" <PRECONDS> </PRECONDS>\n" ^
22.27 +" <PRECONDS>" ^
22.28 +" </PRECONDS>\n" ^
22.29 " <ORDER>\n" ^
22.30 " <STRING> dummy_ord </STRING>\n" ^
22.31 " </ORDER>\n" ^
22.32 @@ -258,10 +260,7 @@
22.33 " </SRLS>\n" ^
22.34 " <SCRIPT>\n" ^
22.35 " <MATHML>\n" ^
22.36 -" <ISA> auto_generated t_t =\nRepeat\n" ^
22.37 -" ((Try (Repeat (Rewrite ''distrib_right'')) @@\n" ^
22.38 -" Try (Repeat (Rewrite ''distrib_left'')))\n" ^
22.39 -" ??.empty) </ISA>\n" ^
22.40 +" <ISA> auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''distrib_right'')) #>\n Try (Repeat (Rewrite ''distrib_left'')))\n ??.empty) </ISA>\n" ^
22.41 " </MATHML>\n" ^
22.42 " </SCRIPT>\n" ^
22.43 " </RULESET>\n" ^
23.1 --- a/test/Tools/isac/Knowledge/diff.sml Wed Oct 02 15:14:51 2019 +0200
23.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Oct 02 16:02:17 2019 +0200
23.3 @@ -236,9 +236,9 @@
23.4
23.5 val str = "Program DiffEqScr (f_f::bool) (v_v::real) = \
23.6 \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) \
23.7 -\ in (((Try (Repeat (Rewrite frac_conv))) @@ \
23.8 - \ (Try (Repeat (Rewrite root_conv))) @@ \
23.9 - \ (Try (Repeat (Rewrite realpow_pow))) @@ \
23.10 +\ in (((Try (Repeat (Rewrite frac_conv))) #> \
23.11 + \ (Try (Repeat (Rewrite root_conv))) #> \
23.12 + \ (Try (Repeat (Rewrite realpow_pow))) #> \
23.13 \ (Repeat \
23.14 \ ((Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sum )) Or \
23.15 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod_const )) Or \
23.16 @@ -258,8 +258,8 @@
23.17 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt_chain )) Or \
23.18 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_const )) Or \
23.19 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var )) Or \
23.20 - \ (Repeat (Rewrite_Set make_polynomial)))) @@ \
23.21 - \ (Try (Repeat (Rewrite sym_frac_conv))) @@ \
23.22 + \ (Repeat (Rewrite_Set make_polynomial)))) #> \
23.23 + \ (Try (Repeat (Rewrite sym_frac_conv))) #> \
23.24 \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
23.25 ;
23.26 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
24.1 --- a/test/Tools/isac/Knowledge/integrate.thy Wed Oct 02 15:14:51 2019 +0200
24.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Wed Oct 02 16:02:17 2019 +0200
24.3 @@ -11,8 +11,8 @@
24.4 partial_function (tailrec) integration_test :: "real \<Rightarrow> real \<Rightarrow> real"
24.5 where
24.6 "integration_test f_f v_v =
24.7 - (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'') @@
24.8 - (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'') @@
24.9 + (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'') #>
24.10 + (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'') #>
24.11 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))"
24.12 setup \<open>KEStore_Elems.add_mets
24.13 [Specify.prep_met @{theory "Isac_Knowledge"} "met_testint" [] Celem.e_metID
25.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Oct 02 15:14:51 2019 +0200
25.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Oct 02 16:02:17 2019 +0200
25.3 @@ -235,8 +235,8 @@
25.4 "----------- met simplification for_polynomials with_minus -------";
25.5 val str =
25.6 "Program SimplifyScript (t_t::real) = \
25.7 -\ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \
25.8 -\ (Try (Rewrite_Set fasse_zusammen False)) @@ \
25.9 +\ (((Try (Rewrite_Set ordne_alphabetisch False)) #> \
25.10 +\ (Try (Rewrite_Set fasse_zusammen False)) #> \
25.11 \ (Try (Rewrite_Set verschoenere False))) t_t)"
25.12 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
25.13 atomty sc;
25.14 @@ -341,8 +341,8 @@
25.15 "Program ProbeScript (e_e::bool) (w_s::bool list) =\
25.16 \ (let e_e = Take e_e; \
25.17 \ e_e = Substitute w_s e_e \
25.18 -\ in (Repeat((Try (Repeat (Calculate ''TIMES''))) @@ \
25.19 -\ (Try (Repeat (Calculate ''PLUS''))) @@ \
25.20 +\ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #> \
25.21 +\ (Try (Repeat (Calculate ''PLUS''))) #> \
25.22 \ (Try (Repeat (Calculate ''MINUS''))))) e_e)"
25.23 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
25.24 atomty sc;
26.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Wed Oct 02 15:14:51 2019 +0200
26.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Oct 02 16:02:17 2019 +0200
26.3 @@ -572,13 +572,13 @@
26.4
26.5 val ttt = (Thm.term_of o the o (parse Test.thy))
26.6 "Let (((While contains_root e_e Do\
26.7 -\Rewrite square_equation_left @@\
26.8 -\Try (Rewrite_Set Test_simplify) @@\
26.9 -\Try (Rewrite_Set rearrange_assoc) @@\
26.10 -\Try (Rewrite_Set Test_simplify)) @@\
26.11 -\Try (Rewrite_Set norm_equation) @@\
26.12 -\Try (Rewrite_Set Test_simplify) @@\
26.13 -\Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv @@\
26.14 +\Rewrite square_equation_left #>\
26.15 +\Try (Rewrite_Set Test_simplify) #>\
26.16 +\Try (Rewrite_Set rearrange_assoc) #>\
26.17 +\Try (Rewrite_Set Test_simplify)) #>\
26.18 +\Try (Rewrite_Set norm_equation) #>\
26.19 +\Try (Rewrite_Set Test_simplify) #>\
26.20 +\Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv #>\
26.21 \Try (Rewrite_Set Test_simplify))\
26.22 \e_)";
26.23
27.1 --- a/test/Tools/isac/OLDTESTS/script.sml Wed Oct 02 15:14:51 2019 +0200
27.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Wed Oct 02 16:02:17 2019 +0200
27.3 @@ -25,7 +25,7 @@
27.4 " --- check_elementwise ------------------------------ ";
27.5
27.6 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
27.7 -" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
27.8 +" --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
27.9
27.10 "--------- sel_rules ---------------------------------------------";
27.11 "-----------------------------------------------------------------";
27.12 @@ -251,8 +251,8 @@
27.13 o Thm.term_of o the o (parse thy))
27.14 "Program Testeq (e_e::bool) = \
27.15 \(While (contains_root e_e) Do \
27.16 - \((Try (Repeat (Rewrite rroot_square_inv))) @@ \
27.17 - \ (Try (Repeat (Rewrite square_equation_left))) @@ \
27.18 + \((Try (Repeat (Rewrite rroot_square_inv))) #> \
27.19 + \ (Try (Repeat (Rewrite square_equation_left))) #> \
27.20 \ (Try (Repeat (Rewrite radd_0)))))\
27.21 \ e_e ");
27.22 atomty sc;
28.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Wed Oct 02 15:14:51 2019 +0200
28.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Wed Oct 02 16:02:17 2019 +0200
28.3 @@ -5,7 +5,7 @@
28.4
28.5 (*contents*)
28.6 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
28.7 -" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
28.8 +" --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
28.9 " --- test 11.5.02 Testeq: let e_e =... in [e_] ------------------ ";
28.10 " _________________ me + nxt_step from script ___________________ ";
28.11 " _________________ me + sqrt-equ-test: 1.norm_equation ________ ";
28.12 @@ -86,9 +86,9 @@
28.13
28.14
28.15
28.16 -" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
28.17 -" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
28.18 -" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
28.19 +" --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
28.20 +" --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
28.21 +" --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
28.22 KEStore_Elems.add_pbts
28.23 [prep_pbt Test.thy "pbl_testss_eq" [] e_pblID
28.24 (["met_testeq","tests"],
28.25 @@ -111,8 +111,8 @@
28.26 (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
28.27 "Program Testeq (e_e::bool) = \
28.28 \(While (contains_root e_e) Do \
28.29 - \((Try (Repeat (Rewrite rroot_square_inv))) @@ \
28.30 - \ (Try (Repeat (Rewrite square_equation_left))) @@ \
28.31 + \((Try (Repeat (Rewrite rroot_square_inv))) #> \
28.32 + \ (Try (Repeat (Rewrite square_equation_left))) #> \
28.33 \ (Try (Repeat (Rewrite radd_0)))))\
28.34 \ e_e"
28.35 ));
28.36 @@ -147,7 +147,7 @@
28.37 val (p,_,f,nxt,_,pt) = me nxt p c pt;
28.38 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso
28.39 nxt=("End_Proof'",End_Proof') then ()
28.40 -else error "different behaviour test 9.5.02 Testeq: While Try Repeat @@";
28.41 +else error "different behaviour test 9.5.02 Testeq: While Try Repeat #>";
28.42
28.43
28.44
28.45 @@ -488,9 +488,9 @@
28.46 \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_; \
28.47 \ L_0_ = (SubProblem (PolyEqX,[univariate,equation], [no_met]) \
28.48 \ [BOOL e_e, REAL v_0_]); \
28.49 - \ L_i_ = Map (((Substitute [(v_0_, v_^^^2)]) @@ \
28.50 + \ L_i_ = Map (((Substitute [(v_0_, v_^^^2)]) #> \
28.51 \ ((Rewrite real_root_positive) Or \
28.52 - \ (Rewrite real_root_negative)) @@ \
28.53 + \ (Rewrite real_root_negative)) #> \
28.54 \ OrToList) L_0_ \
28.55 \ in (flat ....))"
28.56 );
29.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Wed Oct 02 15:14:51 2019 +0200
29.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Wed Oct 02 16:02:17 2019 +0200
29.3 @@ -10,7 +10,7 @@
29.4 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
29.5 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
29.6 "-------- test the same called by interSteps norm_Rational -------------------------------------";
29.7 -"-------- fun op @@ ----------------------------------------------------------------------------";
29.8 +"-------- fun op #> ----------------------------------------------------------------------------";
29.9 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
29.10 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
29.11 "-------- fun stacpbls -------------------------------------------------------------------------";
29.12 @@ -43,16 +43,16 @@
29.13 val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
29.14 writeln(term2str auto_script);
29.15 (*Program Stepwise t_t =
29.16 - (Try (Rewrite_Set discard_minus) @@
29.17 - Try (Rewrite_Set expand_poly_) @@
29.18 - Try (Repeat (Calculate TIMES)) @@
29.19 - Try (Rewrite_Set order_mult_rls_) @@
29.20 - Try (Rewrite_Set simplify_power_) @@
29.21 - Try (Rewrite_Set calc_add_mult_pow_) @@
29.22 - Try (Rewrite_Set reduce_012_mult_) @@
29.23 - Try (Rewrite_Set order_add_rls_) @@
29.24 - Try (Rewrite_Set collect_numerals_) @@
29.25 - Try (Rewrite_Set reduce_012_) @@
29.26 + (Try (Rewrite_Set discard_minus) #>
29.27 + Try (Rewrite_Set expand_poly_) #>
29.28 + Try (Repeat (Calculate TIMES)) #>
29.29 + Try (Rewrite_Set order_mult_rls_) #>
29.30 + Try (Rewrite_Set simplify_power_) #>
29.31 + Try (Rewrite_Set calc_add_mult_pow_) #>
29.32 + Try (Rewrite_Set reduce_012_mult_) #>
29.33 + Try (Rewrite_Set order_add_rls_) #>
29.34 + Try (Rewrite_Set collect_numerals_) #>
29.35 + Try (Rewrite_Set reduce_012_) #>
29.36 Try (Rewrite_Set discard_parentheses1))
29.37 ??.empty ..WORKS, NEVERTHELESS *)
29.38 atomty auto_script;
29.39 @@ -174,19 +174,19 @@
29.40 ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
29.41 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
29.42
29.43 -"-------- fun op @@ ----------------------------------------------------------------------------";
29.44 -"-------- fun op @@ ----------------------------------------------------------------------------";
29.45 -"-------- fun op @@ ----------------------------------------------------------------------------";
29.46 +"-------- fun op #> ----------------------------------------------------------------------------";
29.47 +"-------- fun op #> ----------------------------------------------------------------------------";
29.48 +"-------- fun op #> ----------------------------------------------------------------------------";
29.49 val rules = (#rules o rep_rls) isolate_root;
29.50 val rs = map (rule2stac @{theory}) rules;
29.51 - val t = @@ rs;
29.52 -if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) @@\n" ^
29.53 - "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) @@\n" ^
29.54 - "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) @@\n" ^
29.55 - "Try (Repeat (Rewrite ''risolate_root_add'')) @@\n" ^
29.56 - "Try (Repeat (Rewrite ''risolate_root_mult'')) @@\n" ^
29.57 + val t = #> rs;
29.58 +if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^
29.59 + "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^
29.60 + "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^
29.61 + "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^
29.62 + "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^
29.63 "Try (Repeat (Rewrite ''risolate_root_div''))"
29.64 -then () else error "fun @@ changed"
29.65 +then () else error "fun #> changed"
29.66
29.67 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
29.68 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
29.69 @@ -197,14 +197,14 @@
29.70 writeln (t2str @{theory} prog);
29.71 (*auto_generated t_t =
29.72 Repeat
29.73 - ((Try (Repeat (Rewrite ''thm111'')) @@
29.74 + ((Try (Repeat (Rewrite ''thm111'')) #>
29.75 Try (Repeat (Rewrite ''refl'')))
29.76 ??.empty)*)
29.77 ;
29.78 if t2str @{theory} prog =
29.79 "auto_generated t_t =\n" ^
29.80 "Repeat\n" ^
29.81 - " ((Try (Repeat (Rewrite ''thm111'')) @@ Try (Repeat (Rewrite ''refl'')))\n" ^
29.82 + " ((Try (Repeat (Rewrite ''thm111'')) #> Try (Repeat (Rewrite ''refl'')))\n" ^
29.83 " ??.empty)"
29.84 then () else error "rules2scr_Rls auto_generated changed";
29.85
29.86 @@ -298,11 +298,11 @@
29.87 (* term2str prog |> writeln
29.88 auto_generated_inst t_t v =
29.89 Repeat
29.90 - ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) @@
29.91 - Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) @@
29.92 - Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) @@
29.93 - Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''mult_square'')) @@
29.94 - Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_square'')) @@
29.95 + ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) #>
29.96 + Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) #>
29.97 + Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) #>
29.98 + Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''mult_square'')) #>
29.99 + Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_square'')) #>
29.100 Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_mult_square'')))
29.101 ??.empty)
29.102 *)
30.1 --- a/test/Tools/isac/ProgLang/calculate.thy Wed Oct 02 15:14:51 2019 +0200
30.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Wed Oct 02 16:02:17 2019 +0200
30.3 @@ -29,9 +29,9 @@
30.4 where
30.5 "calc_test t_t =
30.6 (Repeat
30.7 - ((Try (Repeat (Calculate ''PLUS''))) @@
30.8 - (Try (Repeat (Calculate ''TIMES''))) @@
30.9 - (Try (Repeat (Calculate ''DIVIDE''))) @@
30.10 + ((Try (Repeat (Calculate ''PLUS''))) #>
30.11 + (Try (Repeat (Calculate ''TIMES''))) #>
30.12 + (Try (Repeat (Calculate ''DIVIDE''))) #>
30.13 (Try (Repeat (Calculate ''POWER''))))) t_t"
30.14 setup \<open>KEStore_Elems.add_mets
30.15 [Specify.prep_met (@{theory "Test"}) "met_testcal" [] Celem.e_metID
31.1 --- a/test/Tools/isac/ProgLang/prog-tools.sml Wed Oct 02 15:14:51 2019 +0200
31.2 +++ b/test/Tools/isac/ProgLang/prog-tools.sml Wed Oct 02 16:02:17 2019 +0200
31.3 @@ -14,7 +14,7 @@
31.4 "-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
31.5 "-------- fun is_calc, fun op_of_calc ----------------------------------------";
31.6 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
31.7 -"-------- fun op @@ ----------------------------------------------------------";
31.8 +"-------- fun op #> ----------------------------------------------------------";
31.9 "-------- fun get_fun_id -----------------------------------------------------";
31.10 "-------- fun rules2scr_Rls --------------------------------------------------";
31.11 "-----------------------------------------------------------------------------";
31.12 @@ -27,16 +27,16 @@
31.13 val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
31.14 writeln(term2str auto_script);
31.15 (*Program Stepwise t_t =
31.16 - (Try (Rewrite_Set discard_minus) @@
31.17 - Try (Rewrite_Set expand_poly_) @@
31.18 - Try (Repeat (Calculate TIMES)) @@
31.19 - Try (Rewrite_Set order_mult_rls_) @@
31.20 - Try (Rewrite_Set simplify_power_) @@
31.21 - Try (Rewrite_Set calc_add_mult_pow_) @@
31.22 - Try (Rewrite_Set reduce_012_mult_) @@
31.23 - Try (Rewrite_Set order_add_rls_) @@
31.24 - Try (Rewrite_Set collect_numerals_) @@
31.25 - Try (Rewrite_Set reduce_012_) @@
31.26 + (Try (Rewrite_Set discard_minus) #>
31.27 + Try (Rewrite_Set expand_poly_) #>
31.28 + Try (Repeat (Calculate TIMES)) #>
31.29 + Try (Rewrite_Set order_mult_rls_) #>
31.30 + Try (Rewrite_Set simplify_power_) #>
31.31 + Try (Rewrite_Set calc_add_mult_pow_) #>
31.32 + Try (Rewrite_Set reduce_012_mult_) #>
31.33 + Try (Rewrite_Set order_add_rls_) #>
31.34 + Try (Rewrite_Set collect_numerals_) #>
31.35 + Try (Rewrite_Set reduce_012_) #>
31.36 Try (Rewrite_Set discard_parentheses1))
31.37 ??.empty ..WORKS, NEVERTHELESS *)
31.38 atomty auto_script;
31.39 @@ -272,19 +272,19 @@
31.40 else error "rule2stac_inst changed 1")
31.41 | _ => error "rule2stac_inst changed 2"
31.42
31.43 -"-------- fun op @@ ----------------------------------------------------------";
31.44 -"-------- fun op @@ ----------------------------------------------------------";
31.45 -"-------- fun op @@ ----------------------------------------------------------";
31.46 +"-------- fun op #> ----------------------------------------------------------";
31.47 +"-------- fun op #> ----------------------------------------------------------";
31.48 +"-------- fun op #> ----------------------------------------------------------";
31.49 val rules = (#rules o rep_rls) isolate_root;
31.50 val rs = map (rule2stac @{theory}) rules;
31.51 - val t = @@ rs;
31.52 -if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) @@\n" ^
31.53 - "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) @@\n" ^
31.54 - "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) @@\n" ^
31.55 - "Try (Repeat (Rewrite ''risolate_root_add'')) @@\n" ^
31.56 - "Try (Repeat (Rewrite ''risolate_root_mult'')) @@\n" ^
31.57 + val t = #> rs;
31.58 +if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^
31.59 + "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^
31.60 + "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^
31.61 + "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^
31.62 + "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^
31.63 "Try (Repeat (Rewrite ''risolate_root_div''))"
31.64 -then () else error "fun @@ changed"
31.65 +then () else error "fun #> changed"
31.66
31.67 "-------- fun get_fun_id -----------------------------------------------------";
31.68 "-------- fun get_fun_id -----------------------------------------------------";
31.69 @@ -334,10 +334,10 @@
31.70 writeln (t2str @{theory} prog);
31.71 (*auto_generated t_t =
31.72 Repeat
31.73 - ((Try (Repeat (Rewrite ''thm111'')) @@
31.74 + ((Try (Repeat (Rewrite ''thm111'')) #>
31.75 Try (Repeat (Rewrite ''refl'')))
31.76 ??.empty)*)
31.77 ;
31.78 if t2str @{theory} prog =
31.79 -"auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'')) @@\n Try (Repeat (Rewrite ''refl'')))\n ??.empty)"
31.80 +"auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'')) #>\n Try (Repeat (Rewrite ''refl'')))\n ??.empty)"
31.81 then () else error "rules2scr_Rls auto_generated changed"