1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Dec 20 18:02:25 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Dec 26 14:24:05 2018 +0100
1.3 @@ -543,20 +543,20 @@
1.4 prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.5 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.6 " (let e_1 = Take (hd e_s); " ^
1.7 - " e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.8 - " isolate_bdvs False)) @@ " ^
1.9 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.10 - " simplify_System False))) e_1; " ^
1.11 + " e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.12 + " ''isolate_bdvs'' False)) @@ " ^
1.13 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.14 + " ''simplify_System'' False))) e_1; " ^
1.15 " e_2 = Take (hd (tl e_s)); " ^
1.16 " e_2 = ((Substitute [e_1]) @@ " ^
1.17 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.18 - " simplify_System_parenthesized False)) @@ " ^
1.19 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.20 - " isolate_bdvs False)) @@ " ^
1.21 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.22 - " simplify_System False))) e_2; " ^
1.23 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.24 + " ''simplify_System_parenthesized'' False)) @@ " ^
1.25 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.26 + " ''isolate_bdvs'' False)) @@ " ^
1.27 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.28 + " ''simplify_System'' False))) e_2; " ^
1.29 " e__s = Take [e_1, e_2] " ^
1.30 - " in (Try (Rewrite_Set order_system False)) e__s)"
1.31 + " in (Try (Rewrite_Set ''order_system'' False)) e__s)"
1.32 (*---------------------------------------------------------------------------
1.33 this script does NOT separate the equations as above,
1.34 but it does not yet work due to preliminary script-interpreter,
1.35 @@ -567,12 +567,12 @@
1.36 " e_1 = hd e__s; " ^
1.37 " e_2 = hd (tl e__s); " ^
1.38 " e__s = [e_1, Substitute [e_1] e_2] " ^
1.39 - " in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.40 - " simplify_System_parenthesized False)) @@ " ^
1.41 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^
1.42 - " isolate_bdvs False)) @@ " ^
1.43 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.44 - " simplify_System False))) e__s)"
1.45 + " in ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.46 + " ''simplify_System_parenthesized'' False)) @@ " ^
1.47 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))] " ^
1.48 + " ''isolate_bdvs'' False)) @@ " ^
1.49 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.50 + " ''simplify_System'' False))) e__s)"
1.51 ---------------------------------------------------------------------------*))]
1.52 \<close>
1.53 setup \<open>KEStore_Elems.add_mets
1.54 @@ -594,15 +594,15 @@
1.55 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.56 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.57 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.58 - " (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@ " ^
1.59 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.60 - " simplify_System_parenthesized False)) @@ " ^
1.61 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.62 - " isolate_bdvs False)) @@ " ^
1.63 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.64 - " simplify_System_parenthesized False)) @@ " ^
1.65 - " (Try (Rewrite_Set order_system False))) e_s " ^
1.66 - " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^
1.67 + " (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
1.68 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.69 + " ''simplify_System_parenthesized'' False)) @@ " ^
1.70 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.71 + " ''isolate_bdvs'' False)) @@ " ^
1.72 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.73 + " ''simplify_System_parenthesized'' False)) @@ " ^
1.74 + " (Try (Rewrite_Set ''order_system'' False))) e_s " ^
1.75 + " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
1.76 " [BOOL_LIST e__s, REAL_LIST v_s]))")]
1.77 \<close>
1.78 setup \<open>KEStore_Elems.add_mets
1.79 @@ -619,19 +619,19 @@
1.80 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.81 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.82 " (let e__s = " ^
1.83 - " ((Try (Rewrite_Set norm_Rational False)) @@ " ^
1.84 - " (Repeat (Rewrite commute_0_equality False)) @@ " ^
1.85 - " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
1.86 - " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
1.87 - " simplify_System_parenthesized False)) @@ " ^
1.88 - " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
1.89 - " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
1.90 - " isolate_bdvs_4x4 False)) @@ " ^
1.91 - " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
1.92 - " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
1.93 - " simplify_System_parenthesized False)) @@ " ^
1.94 - " (Try (Rewrite_Set order_system False))) e_s " ^
1.95 - " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^
1.96 + " ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
1.97 + " (Repeat (Rewrite ''commute_0_equality'' False)) @@ " ^
1.98 + " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^
1.99 + " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^
1.100 + " ''simplify_System_parenthesized'' False)) @@ " ^
1.101 + " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^
1.102 + " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^
1.103 + " ''isolate_bdvs_4x4'' False)) @@ " ^
1.104 + " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^
1.105 + " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^
1.106 + " ''simplify_System_parenthesized'' False)) @@ " ^
1.107 + " (Try (Rewrite_Set ''order_system'' False))) e_s " ^
1.108 + " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
1.109 " [BOOL_LIST e__s, REAL_LIST v_s]))")]
1.110 \<close>
1.111 setup \<open>KEStore_Elems.add_mets
1.112 @@ -654,15 +654,15 @@
1.113 " (let e_1 = NTH 1 e_s; " ^
1.114 " e_2 = Take (NTH 2 e_s); " ^
1.115 " e_2 = ((Substitute [e_1]) @@ " ^
1.116 - " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
1.117 - " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
1.118 - " simplify_System_parenthesized False)) @@ " ^
1.119 - " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
1.120 - " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
1.121 - " isolate_bdvs False)) @@ " ^
1.122 - " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
1.123 - " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
1.124 - " norm_Rational False))) e_2 " ^
1.125 + " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
1.126 + " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
1.127 + " ''simplify_System_parenthesized'' False)) @@ " ^
1.128 + " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
1.129 + " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
1.130 + " ''isolate_bdvs'' False)) @@ " ^
1.131 + " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
1.132 + " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
1.133 + " ''norm_Rational'' False))) e_2 " ^
1.134 " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])")]
1.135 \<close>
1.136