1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue May 28 16:52:30 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed May 29 10:36:16 2019 +0200
1.3 @@ -520,14 +520,14 @@
1.4 (["EqSystem"], [],
1.5 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.6 errpats = [], nrls = Rule.Erls},
1.7 - "empty_script"),
1.8 + @{thm refl}),
1.9 Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID
1.10 (["EqSystem","top_down_substitution"], [],
1.11 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.12 errpats = [], nrls = Rule.Erls},
1.13 - "empty_script")]
1.14 + @{thm refl})]
1.15 \<close>
1.16 -(*ok
1.17 +
1.18 partial_function (tailrec) solve_system :: "bool list => real list => bool list"
1.19 where
1.20 "solve_system e_s v_s =
1.21 @@ -546,7 +546,6 @@
1.22 ''simplify_System'' False))) e_2;
1.23 e__s = Take [e_1, e_2]
1.24 in Try (Rewrite_Set ''order_system'' False) e__s) "
1.25 -*)
1.26 setup \<open>KEStore_Elems.add_mets
1.27 [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
1.28 (["EqSystem", "top_down_substitution", "2x2"],
1.29 @@ -561,7 +560,8 @@
1.30 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.31 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.32 prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.33 - "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.34 + @{thm solve_system.simps}
1.35 + (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.36 " (let e_1 = Take (hd e_s); " ^
1.37 " e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.38 " ''isolate_bdvs'' False)) @@ " ^
1.39 @@ -576,7 +576,7 @@
1.40 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.41 " ''simplify_System'' False))) e_2; " ^
1.42 " e__s = Take [e_1, e_2] " ^
1.43 - " in (Try (Rewrite_Set ''order_system'' False)) e__s)"
1.44 + " in (Try (Rewrite_Set ''order_system'' False)) e__s)"*)
1.45 (*---------------------------------------------------------------------------
1.46 this script does NOT separate the equations as above,
1.47 but it does not yet work due to preliminary script-interpreter,
1.48 @@ -600,12 +600,12 @@
1.49 (["EqSystem", "normalise"], [],
1.50 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.51 errpats = [], nrls = Rule.Erls},
1.52 - "empty_script")]
1.53 + @{thm refl})]
1.54 \<close>
1.55 -(*ok
1.56 +
1.57 partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
1.58 where
1.59 -"solve_system e_s v_s =
1.60 +"solve_system2 e_s v_s =
1.61 (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@
1.62 (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
1.63 ''simplify_System_parenthesized'' False)) @@
1.64 @@ -616,7 +616,6 @@
1.65 (Try (Rewrite_Set ''order_system'' False))) e_s
1.66 in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
1.67 [BOOL_LIST e__s, REAL_LIST v_s]))"
1.68 -*)
1.69 setup \<open>KEStore_Elems.add_mets
1.70 [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
1.71 (["EqSystem","normalise","2x2"],
1.72 @@ -628,7 +627,8 @@
1.73 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.74 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.75 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.76 - "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.77 + @{thm solve_system2.simps}
1.78 + (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.79 " (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
1.80 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.81 " ''simplify_System_parenthesized'' False)) @@ " ^
1.82 @@ -638,12 +638,12 @@
1.83 " ''simplify_System_parenthesized'' False)) @@ " ^
1.84 " (Try (Rewrite_Set ''order_system'' False))) e_s " ^
1.85 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
1.86 - " [BOOL_LIST e__s, REAL_LIST v_s]))")]
1.87 + " [BOOL_LIST e__s, REAL_LIST v_s]))"*))]
1.88 \<close>
1.89 -(*ok
1.90 +
1.91 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
1.92 where
1.93 -"solve_system e_s v_s =
1.94 +"solve_system3 e_s v_s =
1.95 (let e__s =
1.96 ((Try (Rewrite_Set ''norm_Rational'' False)) @@
1.97 (Repeat (Rewrite ''commute_0_equality'' False)) @@
1.98 @@ -659,7 +659,6 @@
1.99 (Try (Rewrite_Set ''order_system'' False))) e_s
1.100 in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
1.101 [BOOL_LIST e__s, REAL_LIST v_s]))"
1.102 -*)
1.103 setup \<open>KEStore_Elems.add_mets
1.104 [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
1.105 (["EqSystem","normalise","4x4"],
1.106 @@ -672,7 +671,8 @@
1.107 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.108 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.109 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.110 - "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.111 + @{thm solve_system3.simps}
1.112 + (*""Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.113 " (let e__s = " ^
1.114 " ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
1.115 " (Repeat (Rewrite ''commute_0_equality'' False)) @@ " ^
1.116 @@ -687,12 +687,12 @@
1.117 " ''simplify_System_parenthesized'' False)) @@ " ^
1.118 " (Try (Rewrite_Set ''order_system'' False))) e_s " ^
1.119 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
1.120 - " [BOOL_LIST e__s, REAL_LIST v_s]))")]
1.121 + " [BOOL_LIST e__s, REAL_LIST v_s]))"*))]
1.122 \<close>
1.123 -(*ok
1.124 +
1.125 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
1.126 where
1.127 -"solve_system e_s v_s =
1.128 +"solve_system4 e_s v_s =
1.129 (let e_1 = NTH 1 e_s;
1.130 e_2 = Take (NTH 2 e_s);
1.131 e_2 = ((Substitute [e_1]) @@
1.132 @@ -706,7 +706,6 @@
1.133 (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
1.134 ''norm_Rational'' False))) e_2
1.135 in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
1.136 -*)
1.137 setup \<open>KEStore_Elems.add_mets
1.138 [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
1.139 (["EqSystem","top_down_substitution","4x4"],
1.140 @@ -723,7 +722,8 @@
1.141 [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.142 crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.143 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
1.144 - "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.145 + @{thm solve_system4.simps}
1.146 + (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.147 " (let e_1 = NTH 1 e_s; " ^
1.148 " e_2 = Take (NTH 2 e_s); " ^
1.149 " e_2 = ((Substitute [e_1]) @@ " ^
1.150 @@ -736,7 +736,7 @@
1.151 " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
1.152 " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
1.153 " ''norm_Rational'' False))) e_2 " ^
1.154 - " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])")]
1.155 + " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"*))]
1.156 \<close>
1.157
1.158 end
1.159 \ No newline at end of file