1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Sep 26 17:47:10 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Oct 01 10:47:25 2019 +0200
1.3 @@ -524,22 +524,23 @@
1.4
1.5 partial_function (tailrec) solve_system :: "bool list => real list => bool list"
1.6 where
1.7 -"solve_system e_s v_s =
1.8 - (let e_1 = Take (hd e_s);
1.9 - e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
1.10 - ''isolate_bdvs'' False)) @@
1.11 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
1.12 - ''simplify_System'' False))) e_1;
1.13 - e_2 = Take (hd (tl e_s));
1.14 - e_2 = ((Substitute [e_1]) @@
1.15 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
1.16 - ''simplify_System_parenthesized'' False)) @@
1.17 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
1.18 - ''isolate_bdvs'' False)) @@
1.19 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
1.20 - ''simplify_System'' False))) e_2;
1.21 - e__s = Take [e_1, e_2]
1.22 - in Try (Rewrite_Set ''order_system'' False) e__s) "
1.23 +"solve_system e_s v_s = (
1.24 + let
1.25 + e_1 = Take (hd e_s);
1.26 + e_1 = (
1.27 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'')) @@
1.28 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System''))
1.29 + ) e_1;
1.30 + e_2 = Take (hd (tl e_s));
1.31 + e_2 = (
1.32 + (Substitute [e_1]) @@
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_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) @@
1.35 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System'' ))
1.36 + ) e_2;
1.37 + e__s = Take [e_1, e_2]
1.38 + in
1.39 + Try (Rewrite_Set ''order_system'' ) e__s) "
1.40 setup \<open>KEStore_Elems.add_mets
1.41 [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
1.42 (["EqSystem", "top_down_substitution", "2x2"],
1.43 @@ -566,17 +567,18 @@
1.44
1.45 partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
1.46 where
1.47 -"solve_system2 e_s v_s =
1.48 - (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@
1.49 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
1.50 - ''simplify_System_parenthesized'' False)) @@
1.51 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
1.52 - ''isolate_bdvs'' False)) @@
1.53 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
1.54 - ''simplify_System_parenthesized'' False)) @@
1.55 - (Try (Rewrite_Set ''order_system'' False))) e_s
1.56 - in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
1.57 - [BOOL_LIST e__s, REAL_LIST v_s]))"
1.58 +"solve_system2 e_s v_s = (
1.59 + let
1.60 + e__s = (
1.61 + (Try (Rewrite_Set ''norm_Rational'' )) @@
1.62 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) @@
1.63 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) @@
1.64 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) @@
1.65 + (Try (Rewrite_Set ''order_system'' ))
1.66 + ) e_s
1.67 + in
1.68 + 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_2x2" [] Celem.e_metID
1.72 (["EqSystem","normalise","2x2"],
1.73 @@ -593,22 +595,22 @@
1.74
1.75 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
1.76 where
1.77 -"solve_system3 e_s v_s =
1.78 - (let e__s =
1.79 - ((Try (Rewrite_Set ''norm_Rational'' False)) @@
1.80 - (Repeat (Rewrite ''commute_0_equality'' False)) @@
1.81 - (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
1.82 - (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
1.83 - ''simplify_System_parenthesized'' False)) @@
1.84 - (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
1.85 - (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
1.86 - ''isolate_bdvs_4x4'' False)) @@
1.87 - (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
1.88 - (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
1.89 - ''simplify_System_parenthesized'' False)) @@
1.90 - (Try (Rewrite_Set ''order_system'' False))) e_s
1.91 - in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
1.92 - [BOOL_LIST e__s, REAL_LIST v_s]))"
1.93 +"solve_system3 e_s v_s = (
1.94 + let
1.95 + e__s = (
1.96 + (Try (Rewrite_Set ''norm_Rational'' )) @@
1.97 + (Repeat (Rewrite ''commute_0_equality'' )) @@
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 )] ''simplify_System_parenthesized'' )) @@
1.100 + (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ),
1.101 + (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''isolate_bdvs_4x4'' )) @@
1.102 + (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ),
1.103 + (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) @@
1.104 + (Try (Rewrite_Set ''order_system''))
1.105 + ) e_s
1.106 + in
1.107 + SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
1.108 + [BOOL_LIST e__s, REAL_LIST v_s])"
1.109 setup \<open>KEStore_Elems.add_mets
1.110 [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
1.111 (["EqSystem","normalise","4x4"],
1.112 @@ -626,20 +628,21 @@
1.113
1.114 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
1.115 where
1.116 -"solve_system4 e_s v_s =
1.117 - (let e_1 = NTH 1 e_s;
1.118 - e_2 = Take (NTH 2 e_s);
1.119 - e_2 = ((Substitute [e_1]) @@
1.120 - (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
1.121 - (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
1.122 - ''simplify_System_parenthesized'' False)) @@
1.123 - (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
1.124 - (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
1.125 - ''isolate_bdvs'' False)) @@
1.126 - (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
1.127 - (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
1.128 - ''norm_Rational'' False))) e_2
1.129 - in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
1.130 +"solve_system4 e_s v_s = (
1.131 + let
1.132 + e_1 = NTH 1 e_s;
1.133 + e_2 = Take (NTH 2 e_s);
1.134 + e_2 = (
1.135 + (Substitute [e_1]) @@
1.136 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
1.137 + (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''simplify_System_parenthesized'' )) @@
1.138 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
1.139 + (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''isolate_bdvs'' )) @@
1.140 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
1.141 + (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''norm_Rational'' ))
1.142 + ) e_2
1.143 + in
1.144 + [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
1.145 setup \<open>KEStore_Elems.add_mets
1.146 [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
1.147 (["EqSystem","top_down_substitution","4x4"],