1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Oct 02 15:14:51 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Oct 02 16:02:17 2019 +0200
1.3 @@ -528,14 +528,14 @@
1.4 let
1.5 e_1 = Take (hd e_s);
1.6 e_1 = (
1.7 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'')) @@
1.8 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'')) #>
1.9 (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System''))
1.10 ) e_1;
1.11 e_2 = Take (hd (tl e_s));
1.12 e_2 = (
1.13 - (Substitute [e_1]) @@
1.14 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) @@
1.15 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) @@
1.16 + (Substitute [e_1]) #>
1.17 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) #>
1.18 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) #>
1.19 (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System'' ))
1.20 ) e_2;
1.21 e__s = Take [e_1, e_2]
1.22 @@ -570,10 +570,10 @@
1.23 "solve_system2 e_s v_s = (
1.24 let
1.25 e__s = (
1.26 - (Try (Rewrite_Set ''norm_Rational'' )) @@
1.27 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) @@
1.28 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) @@
1.29 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) @@
1.30 + (Try (Rewrite_Set ''norm_Rational'' )) #>
1.31 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) #>
1.32 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) #>
1.33 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) #>
1.34 (Try (Rewrite_Set ''order_system'' ))
1.35 ) e_s
1.36 in
1.37 @@ -598,14 +598,14 @@
1.38 "solve_system3 e_s v_s = (
1.39 let
1.40 e__s = (
1.41 - (Try (Rewrite_Set ''norm_Rational'' )) @@
1.42 - (Repeat (Rewrite ''commute_0_equality'' )) @@
1.43 + (Try (Rewrite_Set ''norm_Rational'' )) #>
1.44 + (Repeat (Rewrite ''commute_0_equality'' )) #>
1.45 (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ),
1.46 - (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) @@
1.47 + (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) #>
1.48 (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ),
1.49 - (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''isolate_bdvs_4x4'' )) @@
1.50 + (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''isolate_bdvs_4x4'' )) #>
1.51 (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ),
1.52 - (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) @@
1.53 + (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) #>
1.54 (Try (Rewrite_Set ''order_system''))
1.55 ) e_s
1.56 in
1.57 @@ -622,7 +622,7 @@
1.58 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.59 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.60 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.61 - (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.62 + (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
1.63 @{thm solve_system3.simps})]
1.64 \<close>
1.65
1.66 @@ -633,11 +633,11 @@
1.67 e_1 = NTH 1 e_s;
1.68 e_2 = Take (NTH 2 e_s);
1.69 e_2 = (
1.70 - (Substitute [e_1]) @@
1.71 + (Substitute [e_1]) #>
1.72 (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
1.73 - (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''simplify_System_parenthesized'' )) @@
1.74 + (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''simplify_System_parenthesized'' )) #>
1.75 (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
1.76 - (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''isolate_bdvs'' )) @@
1.77 + (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''isolate_bdvs'' )) #>
1.78 (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
1.79 (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''norm_Rational'' ))
1.80 ) e_2
1.81 @@ -658,7 +658,7 @@
1.82 prls = Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.83 [Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.84 crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.85 - (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
1.86 + (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
1.87 @{thm solve_system4.simps})]
1.88 \<close>
1.89