1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Fri Feb 15 16:52:05 2019 +0100
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Feb 19 19:35:12 2019 +0100
1.3 @@ -527,6 +527,24 @@
1.4 errpats = [], nrls = Rule.Erls},
1.5 "empty_script")]
1.6 \<close>
1.7 +partial_function (tailrec) solve_system :: "bool list => real list => bool list"
1.8 + where
1.9 +"solve_system e_s v_s =
1.10 + (let e_1 = Take (hd e_s);
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 + e__s = Take [e_1, e_2]
1.24 + in Try (Rewrite_Set ''order_system'' False) e__s) "
1.25 setup \<open>KEStore_Elems.add_mets
1.26 [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
1.27 (["EqSystem", "top_down_substitution", "2x2"],
1.28 @@ -582,6 +600,19 @@
1.29 errpats = [], nrls = Rule.Erls},
1.30 "empty_script")]
1.31 \<close>
1.32 +partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
1.33 + where
1.34 +"solve_system e_s v_s =
1.35 + (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@
1.36 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
1.37 + ''simplify_System_parenthesized'' False)) @@
1.38 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
1.39 + ''isolate_bdvs'' False)) @@
1.40 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
1.41 + ''simplify_System_parenthesized'' False)) @@
1.42 + (Try (Rewrite_Set ''order_system'' False))) e_s
1.43 + in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
1.44 + [BOOL_LIST e__s, REAL_LIST v_s]))"
1.45 setup \<open>KEStore_Elems.add_mets
1.46 [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
1.47 (["EqSystem","normalise","2x2"],
1.48 @@ -605,6 +636,24 @@
1.49 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
1.50 " [BOOL_LIST e__s, REAL_LIST v_s]))")]
1.51 \<close>
1.52 +partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
1.53 + where
1.54 +"solve_system e_s v_s =
1.55 + (let e__s =
1.56 + ((Try (Rewrite_Set ''norm_Rational'' False)) @@
1.57 + (Repeat (Rewrite ''commute_0_equality'' False)) @@
1.58 + (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
1.59 + (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
1.60 + ''simplify_System_parenthesized'' False)) @@
1.61 + (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
1.62 + (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
1.63 + ''isolate_bdvs_4x4'' False)) @@
1.64 + (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
1.65 + (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
1.66 + ''simplify_System_parenthesized'' False)) @@
1.67 + (Try (Rewrite_Set ''order_system'' False))) e_s
1.68 + in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
1.69 + [BOOL_LIST e__s, REAL_LIST v_s]))"
1.70 setup \<open>KEStore_Elems.add_mets
1.71 [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
1.72 (["EqSystem","normalise","4x4"],
1.73 @@ -634,6 +683,22 @@
1.74 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
1.75 " [BOOL_LIST e__s, REAL_LIST v_s]))")]
1.76 \<close>
1.77 +partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
1.78 + where
1.79 +"solve_system e_s v_s =
1.80 + (let e_1 = NTH 1 e_s;
1.81 + e_2 = Take (NTH 2 e_s);
1.82 + e_2 = ((Substitute [e_1]) @@
1.83 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
1.84 + (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
1.85 + ''simplify_System_parenthesized'' False)) @@
1.86 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
1.87 + (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
1.88 + ''isolate_bdvs'' False)) @@
1.89 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
1.90 + (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
1.91 + ''norm_Rational'' False))) e_2
1.92 + in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
1.93 setup \<open>KEStore_Elems.add_mets
1.94 [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
1.95 (["EqSystem","top_down_substitution","4x4"],