1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 22 13:15:52 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 22 14:34:06 2019 +0200
1.3 @@ -18,11 +18,6 @@
1.4 (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
1.5 solveSystem :: "[bool list, real list] => bool list"
1.6
1.7 - (*Script-names*)
1.8 - SolveSystemScript :: "[bool list, real list, bool list]
1.9 - => bool list"
1.10 - ("((Script SolveSystemScript (_ _ =))// (_))" 9)
1.11 -
1.12 axiomatization where
1.13 (*stated as axioms, todo: prove as theorems
1.14 'bdv' is a constant handled on the meta-level
1.15 @@ -560,40 +555,7 @@
1.16 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.17 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.18 prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.19 - @{thm solve_system.simps}
1.20 - (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.21 - " (let e_1 = Take (hd e_s); " ^
1.22 - " e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.23 - " ''isolate_bdvs'' False)) @@ " ^
1.24 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.25 - " ''simplify_System'' False))) e_1; " ^
1.26 - " e_2 = Take (hd (tl e_s)); " ^
1.27 - " e_2 = ((Substitute [e_1]) @@ " ^
1.28 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.29 - " ''simplify_System_parenthesized'' False)) @@ " ^
1.30 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.31 - " ''isolate_bdvs'' False)) @@ " ^
1.32 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.33 - " ''simplify_System'' False))) e_2; " ^
1.34 - " e__s = Take [e_1, e_2] " ^
1.35 - " in (Try (Rewrite_Set ''order_system'' False)) e__s)"*)
1.36 - (*---------------------------------------------------------------------------
1.37 - this script does NOT separate the equations as above,
1.38 - but it does not yet work due to preliminary script-interpreter,
1.39 - see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2'
1.40 -
1.41 - "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.42 - " (let e__s = Take e_s; " ^
1.43 - " e_1 = hd e__s; " ^
1.44 - " e_2 = hd (tl e__s); " ^
1.45 - " e__s = [e_1, Substitute [e_1] e_2] " ^
1.46 - " in ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.47 - " ''simplify_System_parenthesized'' False)) @@ " ^
1.48 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))] " ^
1.49 - " ''isolate_bdvs'' False)) @@ " ^
1.50 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.51 - " ''simplify_System'' False))) e__s)"
1.52 - ---------------------------------------------------------------------------*))]
1.53 + @{thm solve_system.simps})]
1.54 \<close>
1.55 setup \<open>KEStore_Elems.add_mets
1.56 [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
1.57 @@ -627,18 +589,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 - @{thm solve_system2.simps}
1.62 - (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.63 - " (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
1.64 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.65 - " ''simplify_System_parenthesized'' False)) @@ " ^
1.66 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
1.67 - " ''isolate_bdvs'' 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 ''order_system'' False))) e_s " ^
1.71 - " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
1.72 - " [BOOL_LIST e__s, REAL_LIST v_s]))"*))]
1.73 + @{thm solve_system2.simps})]
1.74 \<close>
1.75
1.76 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
1.77 @@ -671,23 +622,7 @@
1.78 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.79 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.80 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.81 - @{thm solve_system3.simps}
1.82 - (*""Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.83 - " (let e__s = " ^
1.84 - " ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
1.85 - " (Repeat (Rewrite ''commute_0_equality'' 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_3'', NTH 4 v_s )] " ^
1.88 - " ''simplify_System_parenthesized'' 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_3'', NTH 4 v_s )] " ^
1.91 - " ''isolate_bdvs_4x4'' False)) @@ " ^
1.92 - " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^
1.93 - " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^
1.94 - " ''simplify_System_parenthesized'' False)) @@ " ^
1.95 - " (Try (Rewrite_Set ''order_system'' False))) e_s " ^
1.96 - " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
1.97 - " [BOOL_LIST e__s, REAL_LIST v_s]))"*))]
1.98 + @{thm solve_system3.simps})]
1.99 \<close>
1.100
1.101 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
1.102 @@ -722,21 +657,7 @@
1.103 [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.104 crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.105 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
1.106 - @{thm solve_system4.simps}
1.107 - (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.108 - " (let e_1 = NTH 1 e_s; " ^
1.109 - " e_2 = Take (NTH 2 e_s); " ^
1.110 - " e_2 = ((Substitute [e_1]) @@ " ^
1.111 - " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
1.112 - " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
1.113 - " ''simplify_System_parenthesized'' False)) @@ " ^
1.114 - " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
1.115 - " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
1.116 - " ''isolate_bdvs'' False)) @@ " ^
1.117 - " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
1.118 - " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
1.119 - " ''norm_Rational'' False))) e_2 " ^
1.120 - " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"*))]
1.121 + @{thm solve_system4.simps})]
1.122 \<close>
1.123
1.124 end
1.125 \ No newline at end of file