1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Sat Jun 22 13:15:52 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Sat Jun 22 14:34:06 2019 +0200
1.3 @@ -76,10 +76,8 @@
1.4 case prog of
1.5 Rule.EmptyScr => NONE
1.6 | Rule.Prog t =>
1.7 - (* version introduced BEFORE switch to partial_function
1.8 - (case t of Free ("empty_script", _) => NONE | _ => SOME (LTool.get_fun_id t))*)
1.9 (case t of
1.10 - Const ("HOL.eq", _) $ Free ("t", _) $ Free ("t", _) (*@{thm refl}*) => NONE
1.11 + Const ("HOL.eq", _) $ Free ("t", _) $ Free ("t", _) (*=@{thm refl}*) => NONE
1.12 | _ => SOME (LTool.get_fun_id t))
1.13 | Rule.Rfuns _ => NONE
1.14
2.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Sat Jun 22 13:15:52 2019 +0200
2.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Sat Jun 22 14:34:06 2019 +0200
2.3 @@ -19,11 +19,6 @@
2.4 senkrecht :: real
2.5 unten :: real
2.6
2.7 - (*Script-names*)
2.8 - RechnenSymbolScript :: "[bool,bool,bool list,bool list,bool list,real,
2.9 - bool] => bool"
2.10 - ("((Script RechnenSymbolScript (_ _ _ _ _ _ =))// (_))" 9)
2.11 -
2.12 ML \<open>
2.13 val thy = @{theory};
2.14 \<close>
2.15 @@ -81,26 +76,7 @@
2.16 srls = Rule.append_rls "srls_..Berechnung-erstSymbolisch" Rule.e_rls
2.17 [Rule.Calc ("Atools.boollist2sum", eval_boollist2sum "")],
2.18 prls = Rule.e_rls, crls =Rule.e_rls , errpats = [], nrls = norm_Rational},
2.19 - @{thm symbolisch_rechnen.simps}
2.20 - (*"Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
2.21 - "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
2.22 - " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
2.23 - " su_m = boollist2sum o_o; " ^
2.24 - " t_t = Substitute [oben = su_m] t_t; " ^
2.25 - " t_t = Substitute o_o t_t; " ^
2.26 - " t_t = Substitute [k_k, q__q] t_t; " ^
2.27 - " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
2.28 - " su_m = boollist2sum s_s; " ^
2.29 - " t_t = Substitute [senkrecht = su_m] t_t; " ^
2.30 - " t_t = Substitute s_s t_t; " ^
2.31 - " t_t = Substitute [k_k, q__q] t_t; " ^
2.32 - " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
2.33 - " su_m = boollist2sum u_u; " ^
2.34 - " t_t = Substitute [unten = su_m] t_t; " ^
2.35 - " t_t = Substitute u_u t_t; " ^
2.36 - " t_t = Substitute [k_k, q__q] t_t; " ^
2.37 - " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t " ^
2.38 - " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t) "*))]
2.39 + @{thm symbolisch_rechnen.simps})]
2.40 \<close>
2.41
2.42 partial_function (tailrec) symbolisch_rechnen_2 :: "bool \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> bool"
2.43 @@ -132,24 +108,7 @@
2.44 srls = Rule.append_rls "srls_..Berechnung-erstSymbolisch" Rule.e_rls
2.45 [Rule.Calc ("Atools.boollist2sum", eval_boollist2sum "")],
2.46 prls = Rule.e_rls, crls =Rule.e_rls , errpats = [], nrls = norm_Rational},
2.47 - @{thm symbolisch_rechnen.simps}
2.48 - (*"Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
2.49 - "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
2.50 - " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
2.51 - " su_m = boollist2sum o_o; " ^
2.52 - " t_t = Substitute [oben = su_m] t_t; " ^
2.53 - " t_t = Substitute o_o t_t; " ^
2.54 - " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
2.55 - " su_m = boollist2sum s_s; " ^
2.56 - " t_t = Substitute [senkrecht = su_m] t_t; " ^
2.57 - " t_t = Substitute s_s t_t; " ^
2.58 - " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
2.59 - " su_m = boollist2sum u_u; " ^
2.60 - " t_t = Substitute [unten = su_m] t_t; " ^
2.61 - " t_t = Substitute u_u t_t; " ^
2.62 - " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
2.63 - " t_t = Substitute [k_k, q__q] t_t " ^
2.64 - " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t) "*))]
2.65 + @{thm symbolisch_rechnen.simps})]
2.66 \<close>
2.67
2.68 end
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sat Jun 22 13:15:52 2019 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sat Jun 22 14:34:06 2019 +0200
3.3 @@ -34,21 +34,6 @@
3.4 Gleichungen :: "bool list => una"
3.5 GleichungsVariablen :: "real list => una"
3.6
3.7 - (*Script-names*)
3.8 - Biegelinie2Script :: "[real, real, real, real => real, real => real, bool list, real list,
3.9 - bool] => bool"
3.10 - ("((Script Biegelinie2Script (_ _ _ _ _ _ _=))// (_))" 9)
3.11 - Biege1xIntegrierenScript ::
3.12 - "[real,real,real,real=>real,bool list,bool list,bool list,
3.13 - bool] => bool"
3.14 - ("((Script Biege1xIntegrierenScript (_ _ _ _ _ _ _ =))// (_))" 9)
3.15 - Belastung2BiegelScript :: "[real,real,real=>real,real=>real,
3.16 - bool list] => bool list"
3.17 - ("((Script Belastung2BiegelScript (_ _ _ _ =))// (_))" 9)
3.18 - SetzeRandbedScript :: "[bool list,bool list,
3.19 - bool list] => bool list"
3.20 - ("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
3.21 -
3.22 axiomatization where
3.23
3.24 Querkraft_Belastung: "Q' x = -qq x" and
3.25 @@ -223,23 +208,7 @@
3.26 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
3.27 Rule.Thm ("if_False",TermC.num_str @{thm if_False})],
3.28 prls = Rule.Erls, crls = Atools_erls, errpats = [], nrls = Rule.Erls},
3.29 - @{thm biegelinie.simps}
3.30 - (*""Script Biegelinie2Script " ^
3.31 - "(l::real) (q :: real) (v :: real) (id_abl::real\<Rightarrow>real) (b :: real => real) (s :: bool list) (vs :: real list) = " ^
3.32 - " (let " ^
3.33 - " (funs :: bool list) = (SubProblem (''Biegelinie'', " ^
3.34 - " [''vonBelastungZu'', ''Biegelinien''], [''Biegelinien'', ''ausBelastung'']) " ^
3.35 - " [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]); " ^
3.36 - " (equs :: bool list) = (SubProblem (''Biegelinie'', " ^
3.37 - " [''setzeRandbedingungen'', ''Biegelinien''], [''Biegelinien'', ''setzeRandbedingungenEin'']) " ^
3.38 - " [BOOL_LIST funs, BOOL_LIST s]); " ^
3.39 - " (cons :: bool list) = (SubProblem (''Biegelinie'', " ^
3.40 - " [''LINEAR'', ''system''], [''no_met'']) " ^
3.41 - " [BOOL_LIST equs, REAL_LIST vs]); " ^
3.42 - " B = Take (lastI funs); " ^
3.43 - " B = ((Substitute cons) @@ " ^
3.44 - " (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B " ^
3.45 - " in B) "*))]
3.46 + @{thm biegelinie.simps})]
3.47 \<close>
3.48 setup \<open>KEStore_Elems.add_mets
3.49 [Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID
3.50 @@ -300,31 +269,7 @@
3.51 srls = Rule.append_rls "srls_ausBelastung" Rule.e_rls
3.52 [Rule.Calc ("Tools.rhs", Tools.eval_rhs "eval_rhs_")],
3.53 prls = Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
3.54 - @{thm belastung_zu_biegelinie.simps}
3.55 - (*"Script Belastung2BiegelScript (q__q::real) (v_v::real) (id_fun::real\<Rightarrow>real) (id_abl::real\<Rightarrow>real) = " ^
3.56 - " (let q___q = Take (qq v_v = q__q); " ^
3.57 - " q___q = ((Rewrite ''sym_neg_equal_iff_equal'' True) @@ " ^
3.58 - " (Rewrite ''Belastung_Querkraft'' True)) q___q; " ^
3.59 - " (Q__Q:: bool) = " ^
3.60 - " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
3.61 - " [''diff'',''integration'',''named'']) " ^
3.62 - " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
3.63 - " M__M = Rewrite ''Querkraft_Moment'' True Q__Q; " ^
3.64 - " (M__M::bool) = " ^
3.65 - " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
3.66 - " [''diff'',''integration'',''named'']) " ^
3.67 - " [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
3.68 - " N__N = ((Rewrite ''Moment_Neigung'' False) @@ " ^
3.69 - " (Rewrite ''make_fun_explicit'' False)) M__M; " ^
3.70 - " (N__N:: bool) = " ^
3.71 - " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
3.72 - " [''diff'',''integration'', ''named'']) " ^
3.73 - " [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl]); " ^
3.74 - " (B__B:: bool) = " ^
3.75 - " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
3.76 - " [''diff'',''integration'',''named'']) " ^
3.77 - " [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]) " ^
3.78 - " in [Q__Q, M__M, N__N, B__B]) "*))]
3.79 + @{thm belastung_zu_biegelinie.simps})]
3.80 \<close>
3.81 subsection \<open>Substitute the constraints into the equations\<close>
3.82
3.83 @@ -355,60 +300,7 @@
3.84 ("#Find" , ["Gleichungen equs'''"])],
3.85 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = srls2, prls=Rule.e_rls, crls = Atools_erls,
3.86 errpats = [], nrls = Rule.e_rls},
3.87 - @{thm setzte_randbedingungen.simps}
3.88 - (*"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
3.89 - " (let b_1 = NTH 1 r_b; " ^
3.90 - " f_s = filter_sameFunId (lhs b_1) fun_s; " ^
3.91 - " (e_1::bool) = " ^
3.92 - " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
3.93 - " [''Equation'',''fromFunction'']) " ^
3.94 - " [BOOL (hd f_s), BOOL b_1]); " ^
3.95 - " b_2 = NTH 2 r_b; " ^
3.96 - " f_s = filter_sameFunId (lhs b_2) fun_s; " ^
3.97 - " (e_2::bool) = " ^
3.98 - " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
3.99 - " [''Equation'',''fromFunction'']) " ^
3.100 - " [BOOL (hd f_s), BOOL b_2]); " ^
3.101 - " b_3 = NTH 3 r_b; " ^
3.102 - " f_s = filter_sameFunId (lhs b_3) fun_s; " ^
3.103 - " (e_3::bool) = " ^
3.104 - " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
3.105 - " [''Equation'',''fromFunction'']) " ^
3.106 - " [BOOL (hd f_s), BOOL b_3]); " ^
3.107 - " b_4 = NTH 4 r_b; " ^
3.108 - " f_s = filter_sameFunId (lhs b_4) fun_s; " ^
3.109 - " (e_4::bool) = " ^
3.110 - " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
3.111 - " [''Equation'',''fromFunction'']) " ^
3.112 - " [BOOL (hd f_s), BOOL b_4]) " ^
3.113 - " in [e_1, e_2, e_3, e_4])"*)
3.114 - (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
3.115 - "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
3.116 - " (let b_1 = NTH 1 r_b; " ^
3.117 - " f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
3.118 - " (e_1::bool) = " ^
3.119 - " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
3.120 - " [''Equation'',''fromFunction'']) " ^
3.121 - " [BOOL (hd f_s), BOOL b_1]); " ^
3.122 - " b_2 = NTH 2 r_b; " ^
3.123 - " f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
3.124 - " (e_2::bool) = " ^
3.125 - " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
3.126 - " [''Equation'',''fromFunction'']) " ^
3.127 - " [BOOL (hd f_s), BOOL b_2]); " ^
3.128 - " b_3 = NTH 3 r_b; " ^
3.129 - " f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
3.130 - " (e_3::bool) = " ^
3.131 - " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
3.132 - " [''Equation'',''fromFunction'']) " ^
3.133 - " [BOOL (hd f_s), BOOL b_3]); " ^
3.134 - " b_4 = NTH 4 r_b; " ^
3.135 - " f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
3.136 - " (e_4::bool) = " ^
3.137 - " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
3.138 - " [''Equation'',''fromFunction'']) " ^
3.139 - " [BOOL (hd f_s), BOOL b_4]) " ^
3.140 - " in [e_1,e_2,e_3,e_4])"*))]
3.141 + @{thm setzte_randbedingungen.simps})]
3.142 \<close>
3.143 subsection \<open>Transform an equality into a function\<close>
3.144
3.145 @@ -436,15 +328,7 @@
3.146 prls=Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
3.147 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
3.148 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
3.149 - @{thm function_to_equality.simps}
3.150 - (*"Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
3.151 - " (let fu_n = Take fu_n; " ^
3.152 - " bd_v = argument_in (lhs fu_n); " ^
3.153 - " va_l = argument_in (lhs su_b); " ^
3.154 - " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
3.155 - (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
3.156 - " eq_u = (Substitute [su_b]) eq_u " ^
3.157 - " in (Rewrite_Set ''norm_Rational'' False) eq_u) "*))]
3.158 + @{thm function_to_equality.simps})]
3.159 \<close>
3.160 ML \<open>
3.161 \<close> ML \<open>
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Sat Jun 22 13:15:52 2019 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Sat Jun 22 14:34:06 2019 +0200
4.3 @@ -12,12 +12,7 @@
4.4 consts
4.5
4.6 d_d :: "[real, real]=> real"
4.7 -(*sin, cos :: "real => real" already in Isabelle2009-2*)
4.8 -(*
4.9 - log, ln :: "real => real"
4.10 - nlog :: "[real, real] => real"
4.11 - exp :: "real => real" ("E'_ ^^^ _" 80)
4.12 -*)
4.13 +
4.14 (*descriptions in the related problems*)
4.15 derivativeEq :: "bool => una"
4.16
4.17 @@ -29,13 +24,9 @@
4.18 Diff :: "[real * real] => real"
4.19 Differentiate :: "[bool * real] => bool"
4.20
4.21 - (*subproblem and script-name*)
4.22 + (*subproblem-name*)
4.23 differentiate :: "[char list * char list list * char list, real, real] => real"
4.24 ("(differentiate (_)/ (_ _ ))" 9)
4.25 - DiffScr :: "[real,real, real] => real"
4.26 - ("((Script DiffScr (_ _ =))// (_))" 9)
4.27 - DiffEqScr :: "[bool,real, bool] => bool"
4.28 - ("((Script DiffEqScr (_ _ =))// (_))" 9)
4.29
4.30 text \<open>a variant of the derivatives defintion:
4.31
4.32 @@ -319,29 +310,7 @@
4.33 ("#Find" ,["derivative f_f'"])],
4.34 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
4.35 crls = Atools_erls, errpats = [], nrls = norm_diff},
4.36 - @{thm differentiate_on_R.simps}
4.37 - (*"Script DiffScr (f_f::real) (v_v::real) = " ^
4.38 - " (let f_f' = Take (d_d v_v f_f) " ^
4.39 - " in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^
4.40 - " (Repeat " ^
4.41 - " ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or " ^
4.42 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or " ^
4.43 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or " ^
4.44 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' True )) Or " ^
4.45 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or " ^
4.46 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or " ^
4.47 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or " ^
4.48 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or " ^
4.49 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or " ^
4.50 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or " ^
4.51 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or " ^
4.52 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or " ^
4.53 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or " ^
4.54 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or " ^
4.55 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^
4.56 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^
4.57 - " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^
4.58 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')"*))]
4.59 + @{thm differentiate_on_R.simps})]
4.60 \<close>
4.61
4.62 partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real"
4.63 @@ -375,29 +344,7 @@
4.64 ("#Find" , ["derivative f_f'"])],
4.65 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
4.66 crls = Atools_erls, errpats = [], nrls = norm_diff},
4.67 - @{thm differentiateX.simps}
4.68 - (*"Script DiffScr (f_f::real) (v_v::real) = " ^
4.69 - " (let f_f' = Take (d_d v_v f_f) " ^
4.70 - " in (( " ^
4.71 - " (Repeat " ^
4.72 - " ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or " ^
4.73 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or " ^
4.74 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or " ^
4.75 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' False)) Or " ^
4.76 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or " ^
4.77 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or " ^
4.78 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or " ^
4.79 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or " ^
4.80 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or " ^
4.81 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or " ^
4.82 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or " ^
4.83 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or " ^
4.84 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or " ^
4.85 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or " ^
4.86 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^
4.87 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^
4.88 - " (Repeat (Rewrite_Set ''make_polynomial'' False)))) " ^
4.89 - " )) f_f')"*))]
4.90 + @{thm differentiateX.simps})]
4.91 \<close>
4.92
4.93 partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool"
4.94 @@ -434,30 +381,7 @@
4.95 ("#Find" ,["derivativeEq f_f'"])],
4.96 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Rule.e_rls,
4.97 crls=Atools_erls, errpats = [], nrls = norm_diff},
4.98 - @{thm differentiate_equality.simps}
4.99 - (*"Script DiffEqScr (f_f::bool) (v_v::real) = " ^
4.100 - " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^
4.101 - " in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^
4.102 - " (Repeat " ^
4.103 - " ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or " ^
4.104 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_dif'' False)) Or " ^
4.105 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or " ^
4.106 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or " ^
4.107 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' True )) Or " ^
4.108 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or " ^
4.109 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or " ^
4.110 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or " ^
4.111 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or " ^
4.112 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or " ^
4.113 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or " ^
4.114 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or " ^
4.115 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or " ^
4.116 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or " ^
4.117 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or " ^
4.118 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^
4.119 - " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^
4.120 - " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^
4.121 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f') "*))]
4.122 + @{thm differentiate_equality.simps})]
4.123 \<close>
4.124
4.125 partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real"
4.126 @@ -477,14 +401,7 @@
4.127 ("#Find" ,["derivative f_f'"])],
4.128 {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
4.129 crls=Atools_erls, errpats = [], nrls = norm_Rational},
4.130 - @{thm simplify_derivative.simps}
4.131 - (*"Script DiffScr (f_f::real) (v_v::real) = " ^
4.132 - " (let f_f' = Take (d_d v_v f_f) " ^
4.133 - " in ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
4.134 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^
4.135 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''norm_diff'' False)) @@ " ^
4.136 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)) @@ " ^
4.137 - " (Try (Rewrite_Set ''norm_Rational'' False))) f_f')"*))]
4.138 + @{thm simplify_derivative.simps})]
4.139 \<close>
4.140 setup \<open>KEStore_Elems.add_cas
4.141 [((Thm.term_of o the o (TermC.parse thy)) "Diff",
5.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Sat Jun 22 13:15:52 2019 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Sat Jun 22 14:34:06 2019 +0200
5.3 @@ -7,20 +7,6 @@
5.4
5.5 consts
5.6
5.7 - Maximum'_value
5.8 - :: "[bool list,real,bool list,real,real set,bool,
5.9 - bool list] => bool list"
5.10 - ("((Script Maximum'_value (_ _ _ _ _ _ =))// (_))" 9)
5.11 -
5.12 - Make'_fun'_by'_new'_variable
5.13 - :: "[real,real,bool list,
5.14 - bool] => bool"
5.15 - ("((Script Make'_fun'_by'_new'_variable (_ _ _ =))// (_))" 9)
5.16 - Make'_fun'_by'_explicit
5.17 - :: "[real,real,bool list,
5.18 - bool] => bool"
5.19 - ("((Script Make'_fun'_by'_explicit (_ _ _ =))// (_))" 9)
5.20 -
5.21 dummy :: real
5.22
5.23 (*for script Maximum_value*)
5.24 @@ -147,21 +133,7 @@
5.25 ("#Relate",[])],
5.26 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=Rule.e_rls, crls = eval_rls,
5.27 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
5.28 - @{thm maximum_value.simps}
5.29 - (*"Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^
5.30 - " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^
5.31 - " (let e_e = (hd o (filterVar m_m)) r_s; " ^
5.32 - " t_t = (if 1 < LENGTH r_s " ^
5.33 - " then (SubProblem (''DiffApp'',[''make'',''function''],[''no_met'']) " ^
5.34 - " [REAL m_m, REAL v_v, BOOL_LIST r_s]) " ^
5.35 - " else (hd r_s)); " ^
5.36 - " (m_x::real) = " ^
5.37 - "SubProblem(''DiffApp'',[''on_interval'',''maximum_of'',''function''], " ^
5.38 - " [''DiffApp'',''max_on_interval_by_calculus'']) " ^
5.39 - " [BOOL t_t, REAL v_v, REAL_SET i_tv] " ^
5.40 - " in ((SubProblem (''DiffApp'',[''find_values'',''tool''],[''Isac'',''find_values'']) " ^
5.41 - " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^
5.42 - " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) "*))]
5.43 + @{thm maximum_value.simps})]
5.44 \<close>
5.45
5.46 partial_function (tailrec) make_fun_by_new_variable :: "real => real => bool list => bool"
5.47 @@ -186,23 +158,7 @@
5.48 ("#Find" ,["functionEq f_1"])],
5.49 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=Rule.e_rls, calc=[], crls = eval_rls,
5.50 errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)},
5.51 - @{thm make_fun_by_new_variable.simps}
5.52 - (*"Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^
5.53 - " (eqs::bool list) = " ^
5.54 - "(let h_h = (hd o (filterVar f_f)) eqs; " ^
5.55 - " e_s = dropWhile (ident h_h) eqs; " ^
5.56 - " v_s = dropWhile (ident f_f) (Vars h_h); " ^
5.57 - " v_1 = NTH 1 v_s; " ^
5.58 - " v_2 = NTH 2 v_s; " ^
5.59 - " e_1 = (hd o (filterVar v_1)) e_s; " ^
5.60 - " e_2 = (hd o (filterVar v_2)) e_s; " ^
5.61 - " (s_1::bool list) = " ^
5.62 - " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
5.63 - " [BOOL e_1, REAL v_1]); " ^
5.64 - " (s_2::bool list) = " ^
5.65 - " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
5.66 - " [BOOL e_2, REAL v_2])" ^
5.67 - "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"*))]
5.68 + @{thm make_fun_by_new_variable.simps})]
5.69 \<close>
5.70
5.71 partial_function (tailrec) make_fun_by_explicit :: "real => real => bool list => bool"
5.72 @@ -222,17 +178,7 @@
5.73 ("#Find" ,["functionEq f_1"])],
5.74 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=Rule.e_rls, crls = eval_rls,
5.75 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
5.76 - @{thm make_fun_by_explicit.simps}
5.77 - (*""Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^
5.78 - " (eqs::bool list) = " ^
5.79 - " (let h_h = (hd o (filterVar f_f)) eqs; " ^
5.80 - " e_1 = hd (dropWhile (ident h_h) eqs); " ^
5.81 - " v_s = dropWhile (ident f_f) (Vars h_h); " ^
5.82 - " v_1 = hd (dropWhile (ident v_v) v_s); " ^
5.83 - " (s_1::bool list)= " ^
5.84 - " (SubProblem(DiffApp',[univariate,equation],[no_met])" ^
5.85 - " [BOOL e_1, REAL v_1]) " ^
5.86 - " in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "*))]
5.87 + @{thm make_fun_by_explicit.simps})]
5.88 \<close>
5.89 setup \<open>KEStore_Elems.add_mets
5.90 [Specify.prep_met thy "met_diffapp_max_oninterval" [] Celem.e_metID
6.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Sat Jun 22 13:15:52 2019 +0200
6.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Sat Jun 22 14:34:06 2019 +0200
6.3 @@ -8,11 +8,6 @@
6.4 theory DiophantEq imports Base_Tools Equation Test
6.5 begin
6.6
6.7 -consts
6.8 - Diophant'_equation :: "[bool, int, bool ]
6.9 - => bool "
6.10 - ("((Script Diophant'_equation (_ _ =))//(_))" 9)
6.11 -
6.12 axiomatization where
6.13 int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
6.14
6.15 @@ -46,12 +41,7 @@
6.16 ("#Find" ,["boolTestFind s_s"])],
6.17 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [],
6.18 crls = tval_rls, errpats = [], nrls = Test_simplify},
6.19 - @{thm diophant_equation.simps}
6.20 - (*"Script Diophant_equation (e_e::bool) (v_v::int)= " ^
6.21 - "(Repeat " ^
6.22 - " ((Try (Rewrite_Inst [(''bdv'',v_v::int)] ''int_isolate_add'' False)) @@" ^
6.23 - " (Try (Calculate ''PLUS'')) @@ " ^
6.24 - " (Try (Calculate ''TIMES''))) e_e::bool)"*))]
6.25 + @{thm diophant_equation.simps})]
6.26 \<close>
6.27
6.28 end
6.29 \ No newline at end of file
7.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 22 13:15:52 2019 +0200
7.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 22 14:34:06 2019 +0200
7.3 @@ -18,11 +18,6 @@
7.4 (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
7.5 solveSystem :: "[bool list, real list] => bool list"
7.6
7.7 - (*Script-names*)
7.8 - SolveSystemScript :: "[bool list, real list, bool list]
7.9 - => bool list"
7.10 - ("((Script SolveSystemScript (_ _ =))// (_))" 9)
7.11 -
7.12 axiomatization where
7.13 (*stated as axioms, todo: prove as theorems
7.14 'bdv' is a constant handled on the meta-level
7.15 @@ -560,40 +555,7 @@
7.16 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
7.17 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
7.18 prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
7.19 - @{thm solve_system.simps}
7.20 - (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
7.21 - " (let e_1 = Take (hd e_s); " ^
7.22 - " e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
7.23 - " ''isolate_bdvs'' False)) @@ " ^
7.24 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
7.25 - " ''simplify_System'' False))) e_1; " ^
7.26 - " e_2 = Take (hd (tl e_s)); " ^
7.27 - " e_2 = ((Substitute [e_1]) @@ " ^
7.28 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
7.29 - " ''simplify_System_parenthesized'' False)) @@ " ^
7.30 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
7.31 - " ''isolate_bdvs'' False)) @@ " ^
7.32 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
7.33 - " ''simplify_System'' False))) e_2; " ^
7.34 - " e__s = Take [e_1, e_2] " ^
7.35 - " in (Try (Rewrite_Set ''order_system'' False)) e__s)"*)
7.36 - (*---------------------------------------------------------------------------
7.37 - this script does NOT separate the equations as above,
7.38 - but it does not yet work due to preliminary script-interpreter,
7.39 - see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2'
7.40 -
7.41 - "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
7.42 - " (let e__s = Take e_s; " ^
7.43 - " e_1 = hd e__s; " ^
7.44 - " e_2 = hd (tl e__s); " ^
7.45 - " e__s = [e_1, Substitute [e_1] e_2] " ^
7.46 - " in ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
7.47 - " ''simplify_System_parenthesized'' False)) @@ " ^
7.48 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))] " ^
7.49 - " ''isolate_bdvs'' False)) @@ " ^
7.50 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
7.51 - " ''simplify_System'' False))) e__s)"
7.52 - ---------------------------------------------------------------------------*))]
7.53 + @{thm solve_system.simps})]
7.54 \<close>
7.55 setup \<open>KEStore_Elems.add_mets
7.56 [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
7.57 @@ -627,18 +589,7 @@
7.58 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
7.59 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
7.60 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
7.61 - @{thm solve_system2.simps}
7.62 - (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
7.63 - " (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
7.64 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
7.65 - " ''simplify_System_parenthesized'' False)) @@ " ^
7.66 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
7.67 - " ''isolate_bdvs'' False)) @@ " ^
7.68 - " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
7.69 - " ''simplify_System_parenthesized'' False)) @@ " ^
7.70 - " (Try (Rewrite_Set ''order_system'' False))) e_s " ^
7.71 - " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
7.72 - " [BOOL_LIST e__s, REAL_LIST v_s]))"*))]
7.73 + @{thm solve_system2.simps})]
7.74 \<close>
7.75
7.76 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
7.77 @@ -671,23 +622,7 @@
7.78 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
7.79 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
7.80 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
7.81 - @{thm solve_system3.simps}
7.82 - (*""Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
7.83 - " (let e__s = " ^
7.84 - " ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
7.85 - " (Repeat (Rewrite ''commute_0_equality'' False)) @@ " ^
7.86 - " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^
7.87 - " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^
7.88 - " ''simplify_System_parenthesized'' False)) @@ " ^
7.89 - " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^
7.90 - " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^
7.91 - " ''isolate_bdvs_4x4'' False)) @@ " ^
7.92 - " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^
7.93 - " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^
7.94 - " ''simplify_System_parenthesized'' False)) @@ " ^
7.95 - " (Try (Rewrite_Set ''order_system'' False))) e_s " ^
7.96 - " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
7.97 - " [BOOL_LIST e__s, REAL_LIST v_s]))"*))]
7.98 + @{thm solve_system3.simps})]
7.99 \<close>
7.100
7.101 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
7.102 @@ -722,21 +657,7 @@
7.103 [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")],
7.104 crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
7.105 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
7.106 - @{thm solve_system4.simps}
7.107 - (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
7.108 - " (let e_1 = NTH 1 e_s; " ^
7.109 - " e_2 = Take (NTH 2 e_s); " ^
7.110 - " e_2 = ((Substitute [e_1]) @@ " ^
7.111 - " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
7.112 - " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
7.113 - " ''simplify_System_parenthesized'' False)) @@ " ^
7.114 - " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
7.115 - " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
7.116 - " ''isolate_bdvs'' False)) @@ " ^
7.117 - " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
7.118 - " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
7.119 - " ''norm_Rational'' False))) e_2 " ^
7.120 - " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"*))]
7.121 + @{thm solve_system4.simps})]
7.122 \<close>
7.123
7.124 end
7.125 \ No newline at end of file
8.1 --- a/src/Tools/isac/Knowledge/Equation.thy Sat Jun 22 13:15:52 2019 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Sat Jun 22 14:34:06 2019 +0200
8.3 @@ -24,11 +24,6 @@
8.4 solve :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)
8.5 solveTest :: "[bool * 'a] => bool list" (* for test collection *)
8.6
8.7 - (*Script-names*)
8.8 - Function2Equality :: "[bool, bool, bool]
8.9 - => bool"
8.10 - ("((Script Function2Equality (_ _ =))// (_))" 9)
8.11 -
8.12 text \<open>defines equation and univariate-equation
8.13 created by: rlang
8.14 date: 02.09
9.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Sat Jun 22 13:15:52 2019 +0200
9.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Sat Jun 22 14:34:06 2019 +0200
9.3 @@ -9,14 +9,6 @@
9.4 (* CAS-command *)
9.5 Sort :: "int xlist \<Rightarrow> int xlist"
9.6
9.7 - (* subproblem and script-name *)
9.8 - Ins'_sort :: "[int xlist,
9.9 - int xlist] => int xlist"
9.10 - ("((Script Ins'_sort (_ =))// (_))" 9)
9.11 - Sortprog :: "[int xlist,
9.12 - int xlist] => int xlist"
9.13 - ("((Script Sortprog (_ =))// (_))" 9)
9.14 -
9.15 section \<open>functions\<close>
9.16 primrec ins :: "int \<Rightarrow> int xlist \<Rightarrow> int xlist"
9.17 where
9.18 @@ -117,12 +109,7 @@
9.19 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
9.20 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
9.21 crls = Atools_crls, errpats = [], nrls = norm_Rational},
9.22 - @{thm sort_program.simps}
9.23 - (*"Script Sortprog (unso :: int xlist) = " ^
9.24 - " (let uns = Take (sort unso) " ^
9.25 - " in " ^
9.26 - " (Rewrite_Set ''ins_sort'' False) uns" ^
9.27 - " )"*))]
9.28 + @{thm sort_program.simps})]
9.29 \<close>
9.30
9.31 partial_function (tailrec) sort_program2 :: "int xlist => int xlist"
9.32 @@ -149,26 +136,7 @@
9.33 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
9.34 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
9.35 crls = Atools_crls, errpats = [], nrls = norm_Rational},
9.36 - @{thm sort_program2.simps}
9.37 - (*"Script Sortprog (unso :: int xlist) = " ^
9.38 - " (let uns = Take (sort unso) " ^
9.39 - " in " ^
9.40 - " (Repeat " ^
9.41 - " ((Repeat (Rewrite ''xfoldr_Nil'' False)) Or " ^
9.42 - " (Repeat (Rewrite ''xfoldr_Cons'' False)) Or " ^
9.43 - " (Repeat (Rewrite ''ins_Nil'' False)) Or " ^
9.44 - " (Repeat (Rewrite ''ins_Cons'' False)) Or " ^
9.45 - " (Repeat (Rewrite ''sort_deff'' False)) Or " ^
9.46 - " (Repeat (Rewrite ''o_id'' False)) Or " ^
9.47 - " (Repeat (Rewrite ''o_assoc'' False)) Or " ^
9.48 - " (Repeat (Rewrite ''o_apply'' False)) Or " ^
9.49 - " (Repeat (Rewrite ''id_apply'' False)) Or " ^
9.50 - " (Repeat (Calculate ''le'' )) Or " ^
9.51 - " (Repeat (Rewrite ''If_def'' False)) Or " ^
9.52 - " (Repeat (Rewrite ''if_True'' False)) Or " ^
9.53 - " (Repeat (Rewrite ''if_False'' False)))) uns" ^
9.54 - " )"*))
9.55 - ]
9.56 + @{thm sort_program2.simps})]
9.57 \<close>
9.58
9.59 subsection \<open>CAS-commands\<close>
10.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sat Jun 22 13:15:52 2019 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sat Jun 22 14:34:06 2019 +0200
10.3 @@ -20,12 +20,6 @@
10.4 (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)
10.5 Integrate :: "[real * real] => real"
10.6
10.7 - (*Script-names*)
10.8 - IntegrationScript :: "[real,real, real] => real"
10.9 - ("((Script IntegrationScript (_ _ =))// (_))" 9)
10.10 - NamedIntegrationScript :: "[real,real, real=>real, bool] => bool"
10.11 - ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
10.12 -
10.13 axiomatization where
10.14 (*stated as axioms, todo: prove as theorems
10.15 'bdv' is a constant handled on the meta-level
10.16 @@ -367,10 +361,7 @@
10.17 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
10.18 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
10.19 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
10.20 - @{thm integrate.simps}
10.21 - (*"Script IntegrationScript (f_f::real) (v_v::real) = " ^
10.22 - " (let t_t = Take (Integral f_f D v_v) " ^
10.23 - " in (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False) (t_t::real))"*))]
10.24 + @{thm integrate.simps})]
10.25 \<close>
10.26
10.27 partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
10.28 @@ -385,11 +376,7 @@
10.29 ("#Find" ,["antiDerivativeName F_F"])],
10.30 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
10.31 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
10.32 - @{thm intergrate_named.simps}
10.33 - (*"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
10.34 - " (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^
10.35 - " in ((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) @@ " ^
10.36 - " (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False)) t_t) "*))]
10.37 + @{thm intergrate_named.simps})]
10.38 \<close>
10.39
10.40 end
10.41 \ No newline at end of file
11.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 22 13:15:52 2019 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 22 14:34:06 2019 +0200
11.3 @@ -56,13 +56,6 @@
11.4 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
11.5 [["SignalProcessing","Z_Transform","Inverse"]]))]\<close>
11.6
11.7 -subsection \<open>Define Name and Signature for the Method\<close>
11.8 -consts
11.9 - InverseZTransform1 :: "[bool, bool] => bool"
11.10 - ("((Script InverseZTransform1 (_ =))// (_))" 9)
11.11 - InverseZTransform2 :: "[bool, real, bool] => bool"
11.12 - ("((Script InverseZTransform2 (_ _ =))// (_))" 9)
11.13 -
11.14 subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
11.15 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
11.16 setup \<open>KEStore_Elems.add_mets
11.17 @@ -99,22 +92,7 @@
11.18 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
11.19 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
11.20 errpats = [], nrls = Rule.e_rls},
11.21 - @{thm inverse_ztransform.simps}
11.22 - (*"Script InverseZTransform1 (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
11.23 - " (let X = Take X_eq;" ^
11.24 - " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*)
11.25 - " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*)
11.26 - " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*)
11.27 - " denom = (Rewrite_Set ''partial_fraction'' False) funterm;" ^ (*get_denominator*)
11.28 - " equ = (denom = (0::real));" ^
11.29 - " fun_arg = Take (lhs X');" ^
11.30 - " arg = (Rewrite_Set ''partial_fraction'' False) X';" ^ (*get_argument TODO*)
11.31 - " (L_L::bool list) = " ^
11.32 - " (SubProblem (''Test'', " ^
11.33 - " [''LINEAR'',''univariate'',''equation'',''test'']," ^
11.34 - " [''Test'',''solve_linear'']) " ^
11.35 - " [BOOL equ, REAL z]) " ^
11.36 - " in X)"*))]
11.37 + @{thm inverse_ztransform.simps})]
11.38 \<close>
11.39
11.40 partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
11.41 @@ -160,22 +138,7 @@
11.42 eval_factors_from_solution "#factors_from_solution")
11.43 ], scr = Rule.EmptyScr},
11.44 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational},
11.45 - @{thm inverse_ztransform2.simps}
11.46 - (*" Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
11.47 - " (let X = Take X_eq; "^ (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
11.48 - " X' = Rewrite ''ruleZY'' False X; "^ (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
11.49 - " (X'_z::real) = lhs X'; "^ (* ?X' z*)
11.50 - " (zzz::real) = argument_in X'_z; "^ (* z *)
11.51 - " (funterm::real) = rhs X'; "^ (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
11.52 - " (pbz::real) = (SubProblem (''Isac'', "^ (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
11.53 - " [''partial_fraction'',''rational'',''simplification''], "^
11.54 - " [''simplification'',''of_rationals'',''to_partial_fraction'']) "^
11.55 - " [REAL funterm, REAL zzz]); "^
11.56 - " (pbz_eq::bool) = Take (X'_z = pbz); "^ (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
11.57 - " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
11.58 - " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
11.59 - " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq "^ (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
11.60 - " in n_eq) "*))](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
11.61 + @{thm inverse_ztransform2.simps})]
11.62 \<close>
11.63 ML \<open>
11.64 \<close> ML \<open>
12.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sat Jun 22 13:15:52 2019 +0200
12.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Sat Jun 22 14:34:06 2019 +0200
12.3 @@ -9,12 +9,6 @@
12.4
12.5 theory LinEq imports Poly Equation begin
12.6
12.7 -consts
12.8 - Solve'_lineq'_equation
12.9 - :: "[bool,real,
12.10 - bool list] => bool list"
12.11 - ("((Script Solve'_lineq'_equation (_ _ =))// (_))" 9)
12.12 -
12.13 axiomatization where
12.14 (*-- normalise --*)
12.15 (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
12.16 @@ -162,18 +156,7 @@
12.17 ("#Find", ["solutions v_v'i'"])],
12.18 {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule.e_rls, prls = LinEq_prls, calc = [],
12.19 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
12.20 - @{thm solve_linear_equation.simps}
12.21 - (*"Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^
12.22 - "(let e_e =((Try (Rewrite ''all_left'' False)) @@ " ^
12.23 - " (Try (Repeat (Rewrite ''makex1_x'' False))) @@ " ^
12.24 - " (Try (Rewrite_Set ''expand_binoms'' False)) @@ " ^
12.25 - " (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v::real)] " ^
12.26 - " ''make_ratpoly_in'' False))) @@ " ^
12.27 - " (Try (Repeat (Rewrite_Set ''LinPoly_simplify'' False))))e_e;" ^
12.28 - " e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)] " ^
12.29 - " ''LinEq_simplify'' True)) @@ " ^
12.30 - " (Repeat(Try (Rewrite_Set ''LinPoly_simplify'' False)))) e_e " ^
12.31 - " in ((Or_to_List e_e)::bool list))"*))]
12.32 + @{thm solve_linear_equation.simps})]
12.33 \<close>
12.34 ML \<open>Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"];\<close>
12.35
13.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Sat Jun 22 13:15:52 2019 +0200
13.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Sat Jun 22 14:34:06 2019 +0200
13.3 @@ -8,15 +8,8 @@
13.4
13.5 ln :: "real => real"
13.6 exp :: "real => real" ("E'_ ^^^ _" 80)
13.7 -
13.8 -(*--------------------------------------------------*)
13.9 alog :: "[real, real] => real" ("_ log _" 90)
13.10
13.11 - (*Script-names*)
13.12 - Solve'_log :: "[bool,real, bool list]
13.13 - => bool list"
13.14 - ("((Script Solve'_log (_ _=))//(_))" 9)
13.15 -
13.16 axiomatization where
13.17
13.18 equality_pow: "0 < a ==> (l = r) = (a^^^l = a^^^r)" and
13.19 @@ -55,12 +48,7 @@
13.20 ("#Find" ,["solutions v_v'i'"])],
13.21 {rew_ord' = "termlessI", rls' = PolyEq_erls, srls = Rule.e_rls, prls = PolyEq_prls, calc = [],
13.22 crls = PolyEq_crls, errpats = [], nrls = norm_Rational},
13.23 - @{thm solve_log.simps}
13.24 - (*"Script Solve_log (e_e::bool) (v_v::real) = " ^
13.25 - "(let e_e = ((Rewrite ''equality_power'' False) @@ " ^
13.26 - " (Rewrite ''exp_invers_log'' False) @@ " ^
13.27 - " (Rewrite_Set ''norm_Poly'' False)) e_e " ^
13.28 - " in [e_e])"*))]
13.29 + @{thm solve_log.simps})]
13.30 \<close>
13.31
13.32 end
13.33 \ No newline at end of file
14.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat Jun 22 13:15:52 2019 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat Jun 22 14:34:06 2019 +0200
14.3 @@ -161,10 +161,6 @@
14.4 [["simplification","of_rationals","to_partial_fraction"]]))]\<close>
14.5
14.6 subsection \<open>Method\<close>
14.7 -consts
14.8 - PartFracScript :: "[real,real, real] => real"
14.9 - ("((Script PartFracScript (_ _ =))// (_))" 9)
14.10 -
14.11 text \<open>rule set for functions called in the Script\<close>
14.12 ML \<open>
14.13 val srls_partial_fraction = Rule.Rls {id="srls_partial_fraction",
14.14 @@ -242,74 +238,7 @@
14.15 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = srls_partial_fraction, prls = Rule.e_rls,
14.16 crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls},
14.17 (*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*)
14.18 - @{thm partial_fraction.simps}
14.19 - (*"Script PartFracScript (f_f::real) (zzz::real) = " ^
14.20 - (*([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
14.21 - "(let f_f = Take f_f; " ^
14.22 - (* num_orig = 3*)
14.23 - " (num_orig::real) = get_numerator f_f; " ^
14.24 - (*([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
14.25 - " f_f = (Rewrite_Set ''norm_Rational'' False) f_f; " ^
14.26 - (* denom = -1 + -2 * z + 8 * z ^^^ 2*)
14.27 - " (denom::real) = get_denominator f_f; " ^
14.28 - (* equ = -1 + -2 * z + 8 * z ^^^ 2 = 0*)
14.29 - " (equ::bool) = (denom = (0::real)); " ^
14.30 -
14.31 - (*([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)*)
14.32 - " (L_L::bool list) = (SubProblem (''Partial_Fractions'', " ^
14.33 - " [''abcFormula'', ''degree_2'', ''polynomial'', ''univariate'', ''equation''], " ^
14.34 - (*([2], Res), [z = 1 / 2, z = -1 / 4]*)
14.35 - " [''no_met'']) [BOOL equ, REAL zzz]); " ^
14.36 - (* facs: (z - 1 / 2) * (z - -1 / 4)*)
14.37 - " (facs::real) = factors_from_solution L_L; " ^
14.38 - (*([3], Frm), 33 / ((z - 1 / 2) * (z - -1 / 4)) *)
14.39 - " (eql::real) = Take (num_orig / facs); " ^
14.40 - (*([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
14.41 - " (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; " ^
14.42 - (*([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
14.43 - " (eq::bool) = Take (eql = eqr); " ^
14.44 - (*([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
14.45 - " eq = (Try (Rewrite_Set ''equival_trans'' False)) eq;" ^
14.46 - (* eq = 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)*)
14.47 - (* z1 = 1 / 2*)
14.48 - " (z1::real) = (rhs (NTH 1 L_L)); " ^
14.49 - (* z2 = -1 / 4*)
14.50 - " (z2::real) = (rhs (NTH 2 L_L)); " ^
14.51 - (*([5], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)*)
14.52 - " (eq_a::bool) = Take eq; " ^
14.53 - (*([5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)*)
14.54 - " eq_a = (Substitute [zzz = z1]) eq; " ^
14.55 - (*([6], Res), 3 = 3 * AA / 4*)
14.56 - " eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a; " ^
14.57 -
14.58 - (*([7], Pbl), solve (3 = 3 * AA / 4, AA)*)
14.59 - " (sol_a::bool list) = " ^
14.60 - " (SubProblem (''Isac'', [''univariate'',''equation''], [''no_met'']) " ^
14.61 - (*([7], Res), [AA = 4]*)
14.62 - " [BOOL eq_a, REAL (AA::real)]); " ^
14.63 - (* a = 4*)
14.64 - " (a::real) = (rhs (NTH 1 sol_a)); " ^
14.65 - (*([8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)*)
14.66 - " (eq_b::bool) = Take eq; " ^
14.67 - (*([8], Res), 3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)*)
14.68 - " eq_b = (Substitute [zzz = z2]) eq_b; " ^
14.69 - (*([9], Res), 3 = -3 * BB / 4*)
14.70 - " eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; " ^
14.71 - (*([10], Pbl), solve (3 = -3 * BB / 4, BB)*)
14.72 - " (sol_b::bool list) = " ^
14.73 - " (SubProblem (''Isac'', [''univariate'',''equation''], [''no_met'']) " ^
14.74 - (*([10], Res), [BB = -4]*)
14.75 - " [BOOL eq_b, REAL (BB::real)]); " ^
14.76 - (* b = -4*)
14.77 - " (b::real) = (rhs (NTH 1 sol_b)); " ^
14.78 - (* eqr = AA / (z - 1 / 2) + BB / (z - -1 / 4)*)
14.79 - (*([11], Frm), AA / (z - 1 / 2) + BB / (z - -1 / 4)*)
14.80 - " (pbz::real) = Take eqr; " ^
14.81 - (*([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
14.82 - " pbz = ((Substitute [AA = a, BB = b]) pbz) " ^
14.83 - (*([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
14.84 - "in pbz)"*)
14.85 -)]
14.86 + @{thm partial_fraction.simps})]
14.87 \<close>
14.88 ML \<open>
14.89 (*
15.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sat Jun 22 13:15:52 2019 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sat Jun 22 14:34:06 2019 +0200
15.3 @@ -61,11 +61,6 @@
15.4 is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*)
15.5 is'_polyexp :: "real => bool" ("_ is'_polyexp")
15.6
15.7 - Expand'_binoms
15.8 - :: "['y,
15.9 - 'y] => 'y"
15.10 - ("((Script Expand'_binoms (_ =))// (_))" 9)
15.11 -
15.12 subsection \<open>theorems not yet adopted from Isabelle\<close>
15.13 axiomatization where (*.not contained in Isabelle2002,
15.14 stated as axioms, TODO: prove as theorems;
16.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sat Jun 22 13:15:52 2019 +0200
16.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sat Jun 22 14:34:06 2019 +0200
16.3 @@ -12,59 +12,6 @@
16.4
16.5 theory PolyEq imports LinEq RootRatEq begin
16.6
16.7 -consts
16.8 -
16.9 -(*---------scripts--------------------------*)
16.10 - Complete'_square
16.11 - :: "[bool,real,
16.12 - bool list] => bool list"
16.13 - ("((Script Complete'_square (_ _ =))// (_))" 9)
16.14 - (*----- poly ----- *)
16.15 - Normalize'_poly
16.16 - :: "[bool,real,
16.17 - bool list] => bool list"
16.18 - ("((Script Normalize'_poly (_ _=))// (_))" 9)
16.19 - Solve'_d0'_polyeq'_equation
16.20 - :: "[bool,real,
16.21 - bool list] => bool list"
16.22 - ("((Script Solve'_d0'_polyeq'_equation (_ _ =))// (_))" 9)
16.23 - Solve'_d1'_polyeq'_equation
16.24 - :: "[bool,real,
16.25 - bool list] => bool list"
16.26 - ("((Script Solve'_d1'_polyeq'_equation (_ _ =))// (_))" 9)
16.27 - Solve'_d2'_polyeq'_equation
16.28 - :: "[bool,real,
16.29 - bool list] => bool list"
16.30 - ("((Script Solve'_d2'_polyeq'_equation (_ _ =))// (_))" 9)
16.31 - Solve'_d2'_polyeq'_sqonly'_equation
16.32 - :: "[bool,real,
16.33 - bool list] => bool list"
16.34 - ("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))// (_))" 9)
16.35 - Solve'_d2'_polyeq'_bdvonly'_equation
16.36 - :: "[bool,real,
16.37 - bool list] => bool list"
16.38 - ("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))// (_))" 9)
16.39 - Solve'_d2'_polyeq'_pq'_equation
16.40 - :: "[bool,real,
16.41 - bool list] => bool list"
16.42 - ("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))// (_))" 9)
16.43 - Solve'_d2'_polyeq'_abc'_equation
16.44 - :: "[bool,real,
16.45 - bool list] => bool list"
16.46 - ("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))// (_))" 9)
16.47 - Solve'_d3'_polyeq'_equation
16.48 - :: "[bool,real,
16.49 - bool list] => bool list"
16.50 - ("((Script Solve'_d3'_polyeq'_equation (_ _ =))// (_))" 9)
16.51 - Solve'_d4'_polyeq'_equation
16.52 - :: "[bool,real,
16.53 - bool list] => bool list"
16.54 - ("((Script Solve'_d4'_polyeq'_equation (_ _ =))// (_))" 9)
16.55 - Biquadrat'_poly
16.56 - :: "[bool,real,
16.57 - bool list] => bool list"
16.58 - ("((Script Biquadrat'_poly (_ _=))// (_))" 9)
16.59 -
16.60 (*-------------------- rules -------------------------------------------------*)
16.61 (* type real enforced by op "^^^" *)
16.62 axiomatization where
16.63 @@ -952,20 +899,6 @@
16.64 ("#Find", ["solutions v_v'i'"])],
16.65 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","complete_square"]]))]\<close>
16.66
16.67 -ML\<open>
16.68 -val scr =
16.69 - "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
16.70 - "(let e_e =((Try (Rewrite ''all_left'' False)) @@ " ^
16.71 - " (Try (Repeat (Rewrite ''makex1_x'' False))) @@ " ^
16.72 - " (Try (Repeat (Rewrite_Set ''expand_binoms'' False))) @@ " ^
16.73 - " (Try (Repeat (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.74 - " ''make_ratpoly_in'' False))) @@ " ^
16.75 - " (Try (Repeat (Rewrite_Set ''polyeq_simplify'' False)))) e_e " ^
16.76 - " in (SubProblem (''PolyEq'',[''polynomial'',''univariate'',''equation''], [''no_met'']) " ^
16.77 - " [BOOL e_e, REAL v_v]))";
16.78 -TermC.parse thy scr;
16.79 -\<close>
16.80 -
16.81 text \<open>"-------------------------methods-----------------------"\<close>
16.82 setup \<open>KEStore_Elems.add_mets
16.83 [Specify.prep_met thy "met_polyeq" [] Celem.e_metID
16.84 @@ -993,16 +926,7 @@
16.85 ("#Find" ,["solutions v_v'i'"])],
16.86 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls, calc=[],
16.87 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
16.88 - @{thm normalize_poly_eq.simps}
16.89 - (*"Script Normalize_poly (e_e::bool) (v_v::real) = " ^
16.90 - "(let e_e =((Try (Rewrite ''all_left'' False)) @@ " ^
16.91 - " (Try (Repeat (Rewrite ''makex1_x'' False))) @@ " ^
16.92 - " (Try (Repeat (Rewrite_Set ''expand_binoms'' False))) @@ " ^
16.93 - " (Try (Repeat (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.94 - " ''make_ratpoly_in'' False))) @@ " ^
16.95 - " (Try (Repeat (Rewrite_Set ''polyeq_simplify'' False)))) e_e " ^
16.96 - " in (SubProblem (''PolyEq'',[''polynomial'',''univariate'',''equation''], [''no_met'']) " ^
16.97 - " [BOOL e_e, REAL v_v]))"*))]
16.98 + @{thm normalize_poly_eq.simps})]
16.99 \<close>
16.100
16.101 partial_function (tailrec) solve_poly_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
16.102 @@ -1019,11 +943,7 @@
16.103 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
16.104 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
16.105 nrls = norm_Rational},
16.106 - @{thm solve_poly_equ.simps}
16.107 - (*"Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
16.108 - "(let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.109 - " ''d0_polyeq_simplify'' False))) e_e " ^
16.110 - " in ((Or_to_List e_e)::bool list))"*))]
16.111 + @{thm solve_poly_equ.simps})]
16.112 \<close>
16.113
16.114 partial_function (tailrec) solve_poly_eq1 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
16.115 @@ -1042,14 +962,7 @@
16.116 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
16.117 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
16.118 nrls = norm_Rational},
16.119 - @{thm solve_poly_eq1.simps}
16.120 - (*"Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
16.121 - "(let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.122 - " ''d1_polyeq_simplify'' True)) @@ " ^
16.123 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
16.124 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
16.125 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
16.126 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
16.127 + @{thm solve_poly_eq1.simps})]
16.128 \<close>
16.129
16.130 partial_function (tailrec) solve_poly_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
16.131 @@ -1071,17 +984,7 @@
16.132 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
16.133 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
16.134 nrls = norm_Rational},
16.135 - @{thm solve_poly_equ2.simps}
16.136 - (*"Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
16.137 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.138 - " ''d2_polyeq_simplify'' True)) @@ " ^
16.139 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
16.140 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.141 - " ''d1_polyeq_simplify'' True)) @@ " ^
16.142 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
16.143 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
16.144 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
16.145 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
16.146 + @{thm solve_poly_equ2.simps})]
16.147 \<close>
16.148
16.149 partial_function (tailrec) solve_poly_equ0 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
16.150 @@ -1103,17 +1006,7 @@
16.151 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
16.152 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
16.153 nrls = norm_Rational},
16.154 - @{thm solve_poly_equ0.simps}
16.155 - (*"Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
16.156 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.157 - " ''d2_polyeq_bdv_only_simplify'' True)) @@ " ^
16.158 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
16.159 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.160 - " ''d1_polyeq_simplify'' True)) @@ " ^
16.161 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
16.162 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
16.163 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
16.164 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
16.165 + @{thm solve_poly_equ0.simps})]
16.166 \<close>
16.167
16.168 partial_function (tailrec) solve_poly_equ_sqrt :: "bool \<Rightarrow> real \<Rightarrow> bool list"
16.169 @@ -1134,14 +1027,7 @@
16.170 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
16.171 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
16.172 nrls = norm_Rational},
16.173 - @{thm solve_poly_equ_sqrt.simps}
16.174 - (*"Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
16.175 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.176 - " ''d2_polyeq_sq_only_simplify'' True)) @@ " ^
16.177 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
16.178 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e; " ^
16.179 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
16.180 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
16.181 + @{thm solve_poly_equ_sqrt.simps})]
16.182 \<close>
16.183
16.184 partial_function (tailrec) solve_poly_equ_pq :: "bool \<Rightarrow> real \<Rightarrow> bool list"
16.185 @@ -1160,14 +1046,7 @@
16.186 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
16.187 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
16.188 nrls = norm_Rational},
16.189 - @{thm solve_poly_equ_pq.simps}
16.190 - (*"Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
16.191 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.192 - " ''d2_polyeq_pqFormula_simplify'' True)) @@ " ^
16.193 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
16.194 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
16.195 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
16.196 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
16.197 + @{thm solve_poly_equ_pq.simps})]
16.198 \<close>
16.199
16.200 partial_function (tailrec) solve_poly_equ_abc :: "bool \<Rightarrow> real \<Rightarrow> bool list"
16.201 @@ -1187,14 +1066,7 @@
16.202 {rew_ord'="termlessI", rls'=PolyEq_erls,srls=Rule.e_rls, prls=PolyEq_prls,
16.203 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
16.204 nrls = norm_Rational},
16.205 - @{thm solve_poly_equ_abc.simps}
16.206 - (*"Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
16.207 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.208 - " ''d2_polyeq_abcFormula_simplify'' True)) @@ " ^
16.209 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
16.210 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
16.211 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
16.212 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
16.213 + @{thm solve_poly_equ_abc.simps})]
16.214 \<close>
16.215
16.216 partial_function (tailrec) solve_poly_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
16.217 @@ -1217,20 +1089,7 @@
16.218 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
16.219 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
16.220 nrls = norm_Rational},
16.221 - @{thm solve_poly_equ3.simps}
16.222 - (*"Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
16.223 - " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.224 - " ''d3_polyeq_simplify'' True)) @@ " ^
16.225 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
16.226 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.227 - " ''d2_polyeq_simplify'' True)) @@ " ^
16.228 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
16.229 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
16.230 - " ''d1_polyeq_simplify'' True)) @@ " ^
16.231 - " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
16.232 - " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
16.233 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
16.234 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
16.235 + @{thm solve_poly_equ3.simps})]
16.236 \<close>
16.237 (*.solves all expanded (ie. normalised) terms of degree 2.*)
16.238 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
16.239 @@ -1259,21 +1118,7 @@
16.240 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=Rule.e_rls,prls=PolyEq_prls,
16.241 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
16.242 nrls = norm_Rational},
16.243 - @{thm solve_by_completing_square.simps}
16.244 - (*"Script Complete_square (e_e::bool) (v_v::real) = " ^
16.245 - "(let e_e = " ^
16.246 - " ((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''cancel_leading_coeff'' True)) " ^
16.247 - " @@ (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''complete_square'' True)) " ^
16.248 - " @@ (Try (Rewrite ''square_explicit1'' False)) " ^
16.249 - " @@ (Try (Rewrite ''square_explicit2'' False)) " ^
16.250 - " @@ (Rewrite ''root_plus_minus'' True) " ^
16.251 - " @@ (Try (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''bdv_explicit1'' False))) " ^
16.252 - " @@ (Try (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''bdv_explicit2'' False))) " ^
16.253 - " @@ (Try (Repeat " ^
16.254 - " (Rewrite_Inst [(''bdv'',v_v)] ''bdv_explicit3'' False))) " ^
16.255 - " @@ (Try (Rewrite_Set ''calculate_RootRat'' False)) " ^
16.256 - " @@ (Try (Repeat (Calculate ''SQRT'')))) e_e " ^
16.257 - " in ((Or_to_List e_e)::bool list))"*))]
16.258 + @{thm solve_by_completing_square.simps})]
16.259 \<close>
16.260
16.261 ML\<open>
17.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Sat Jun 22 13:15:52 2019 +0200
17.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Sat Jun 22 14:34:06 2019 +0200
17.3 @@ -20,11 +20,6 @@
17.4 mitWert :: "bool list => tobooll"
17.5 Geprueft :: "bool => una"
17.6
17.7 - (*Script-name*)
17.8 - ProbeScript :: "[bool, bool list, bool]
17.9 - => bool"
17.10 - ("((Script ProbeScript (_ _ =))// (_))" 9)
17.11 -
17.12 axiomatization where
17.13
17.14 null_minus: "0 - a = -a" and
17.15 @@ -505,11 +500,7 @@
17.16 Rule.Thm ("not_false",TermC.num_str @{thm not_false})
17.17 (*"(~ False) = True"*)],
17.18 crls = Rule.e_rls, errpats = [], nrls = rls_p_33},
17.19 - @{thm simplify.simps}
17.20 - (*"Script SimplifyScript (t_t::real) = " ^
17.21 - " ((Repeat((Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@ " ^
17.22 - " (Try (Rewrite_Set ''fasse_zusammen'' False)) @@ " ^
17.23 - " (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"*))]
17.24 + @{thm simplify.simps})]
17.25 \<close>
17.26
17.27 partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"
17.28 @@ -529,12 +520,7 @@
17.29 prls = Rule.append_rls "simplification_for_polynomials_prls" Rule.e_rls
17.30 [(*for preds in where_*) Rule.Calc("Poly.is'_polyexp",eval_is_polyexp"")],
17.31 crls = Rule.e_rls, errpats = [], nrls = rls_p_34},
17.32 - @{thm simplify2.simps}
17.33 - (*"Script SimplifyScript (t_t::real) = " ^
17.34 - " ((Repeat((Try (Rewrite_Set ''klammern_aufloesen'' False)) @@ " ^
17.35 - " (Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@ " ^
17.36 - " (Try (Rewrite_Set ''fasse_zusammen'' False)) @@ " ^
17.37 - " (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"*))]
17.38 + @{thm simplify2.simps})]
17.39 \<close>
17.40
17.41 partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"
17.42 @@ -555,15 +541,7 @@
17.43 prls = Rule.append_rls "simplification_for_polynomials_prls" Rule.e_rls
17.44 [(*for preds in where_*) Rule.Calc("Poly.is'_polyexp",eval_is_polyexp"")],
17.45 crls = Rule.e_rls, errpats = [], nrls = rls_p_34},
17.46 - @{thm simplify3.simps}
17.47 - (*"Script SimplifyScript (t_t::real) = " ^
17.48 - " ((Repeat((Try (Rewrite_Set ''klammern_ausmultiplizieren'' False)) @@ " ^
17.49 - " (Try (Rewrite_Set ''discard_parentheses'' False)) @@ " ^
17.50 - " (Try (Rewrite_Set ''ordne_monome'' False)) @@ " ^
17.51 - " (Try (Rewrite_Set ''klammern_aufloesen'' False)) @@ " ^
17.52 - " (Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@ " ^
17.53 - " (Try (Rewrite_Set ''fasse_zusammen'' False)) @@ " ^
17.54 - " (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"*))]
17.55 + @{thm simplify3.simps})]
17.56 \<close>
17.57 setup \<open>KEStore_Elems.add_mets
17.58 [Specify.prep_met thy "met_probe" [] Celem.e_metID
17.59 @@ -591,13 +569,7 @@
17.60 prls = Rule.append_rls "prls_met_probe_bruch" Rule.e_rls
17.61 [(*for preds in where_*) Rule.Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
17.62 crls = Rule.e_rls, errpats = [], nrls = rechnen},
17.63 - @{thm mache_probe.simps}
17.64 - (*"Script ProbeScript (e_e::bool) (w_w::bool list) = " ^
17.65 - " (let e_e = Take e_e; " ^
17.66 - " e_e = Substitute w_w e_e " ^
17.67 - " in (Repeat((Try (Repeat (Calculate ''TIMES''))) @@ " ^
17.68 - " (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
17.69 - " (Try (Repeat (Calculate ''MINUS''))))) e_e)"*))]
17.70 + @{thm mache_probe.simps})]
17.71 \<close>
17.72 setup \<open>KEStore_Elems.add_mets
17.73 [Specify.prep_met thy "met_probe_bruch" [] Celem.e_metID
18.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sat Jun 22 13:15:52 2019 +0200
18.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Sat Jun 22 14:34:06 2019 +0200
18.3 @@ -24,11 +24,6 @@
18.4 subsection \<open>consts definition for predicates in specifications\<close>
18.5 consts
18.6 is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")
18.7 - (*----------------------scripts-----------------------*)
18.8 - Solve'_rat'_equation
18.9 - :: "[bool,real,
18.10 - bool list] => bool list"
18.11 - ("((Script Solve'_rat'_equation (_ _ =))// (_))" 9)
18.12
18.13 subsection \<open>theorems not yet adopted from Isabelle\<close>
18.14 axiomatization where
18.15 @@ -197,15 +192,7 @@
18.16 ("#Find" ,["solutions v_v'i'"])],
18.17 {rew_ord'="termlessI", rls'=rateq_erls, srls=Rule.e_rls, prls=RatEq_prls, calc=[],
18.18 crls=RatEq_crls, errpats = [], nrls = norm_Rational},
18.19 - @{thm solve_rational_equ.simps}
18.20 - (*"Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^
18.21 - "(let e_e = ((Repeat(Try (Rewrite_Set ''RatEq_simplify'' True))) @@ " ^
18.22 - " (Repeat(Try (Rewrite_Set ''norm_Rational'' False))) @@ " ^
18.23 - " (Repeat(Try (Rewrite_Set ''add_fractions_p'' False))) @@ " ^
18.24 - " (Repeat(Try (Rewrite_Set ''RatEq_eliminate'' True)))) e_e;" ^
18.25 - " (L_L::bool list) = (SubProblem (''RatEq'',[''univariate'',''equation''], [''no_met''])" ^
18.26 - " [BOOL e_e, REAL v_v]) " ^
18.27 - " in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
18.28 + @{thm solve_rational_equ.simps})]
18.29 \<close>
18.30 ML \<open>
18.31 \<close> ML \<open>
19.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sat Jun 22 13:15:52 2019 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sat Jun 22 14:34:06 2019 +0200
19.3 @@ -915,20 +915,7 @@
19.4 prls = Rule.append_rls "simplification_of_rationals_prls" Rule.e_rls
19.5 [(*for preds in where_*) Rule.Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
19.6 crls = Rule.e_rls, errpats = [], nrls = norm_Rational_rls},
19.7 - @{thm simplify.simps}
19.8 - (*"Script SimplifyScript (t_t::real) = " ^
19.9 - " ((Try (Rewrite_Set ''discard_minus'' False) @@ " ^
19.10 - " Try (Rewrite_Set ''rat_mult_poly'' False) @@ " ^
19.11 - " Try (Rewrite_Set ''make_rat_poly_with_parentheses'' False) @@ " ^
19.12 - " Try (Rewrite_Set ''cancel_p_rls'' False) @@ " ^
19.13 - " (Repeat " ^
19.14 - " ((Try (Rewrite_Set ''add_fractions_p_rls'' False) @@ " ^
19.15 - " Try (Rewrite_Set ''rat_mult_div_pow'' False) @@ " ^
19.16 - " Try (Rewrite_Set ''make_rat_poly_with_parentheses'' False) @@" ^
19.17 - " Try (Rewrite_Set ''cancel_p_rls'' False) @@ " ^
19.18 - " Try (Rewrite_Set ''rat_reduce_1'' False)))) @@ " ^
19.19 - " Try (Rewrite_Set ''discard_parentheses1'' False)) " ^
19.20 - " t_t)"*))]
19.21 + @{thm simplify.simps})]
19.22 \<close>
19.23
19.24 end
20.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sat Jun 22 13:15:52 2019 +0200
20.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sat Jun 22 14:34:06 2019 +0200
20.3 @@ -24,23 +24,6 @@
20.4 is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _")
20.5 is'_sqrtTerm'_in :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _")
20.6 is'_normSqrtTerm'_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _")
20.7 - (*----------------------scripts-----------------------*)
20.8 - Norm'_sq'_root'_equation
20.9 - :: "[bool,real,
20.10 - bool list] => bool list"
20.11 - ("((Script Norm'_sq'_root'_equation (_ _ =))// (_))" 9)
20.12 - Solve'_sq'_root'_equation
20.13 - :: "[bool,real,
20.14 - bool list] => bool list"
20.15 - ("((Script Solve'_sq'_root'_equation (_ _ =))// (_))" 9)
20.16 - Solve'_left'_sq'_root'_equation
20.17 - :: "[bool,real,
20.18 - bool list] => bool list"
20.19 - ("((Script Solve'_left'_sq'_root'_equation (_ _ =))// (_))" 9)
20.20 - Solve'_right'_sq'_root'_equation
20.21 - :: "[bool,real,
20.22 - bool list] => bool list"
20.23 - ("((Script Solve'_right'_sq'_root'_equation (_ _ =))// (_))" 9)
20.24
20.25 subsection \<open>theorems not yet adopted from Isabelle\<close>
20.26 axiomatization where
20.27 @@ -518,15 +501,7 @@
20.28 ("#Find" ,["solutions v_v'i'"])],
20.29 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[],
20.30 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
20.31 - @{thm norm_sqrt_equ.simps}
20.32 - (*"Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
20.33 - "(let e_e = ((Repeat(Try (Rewrite ''makex1_x'' False))) @@ " ^
20.34 - " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
20.35 - " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^
20.36 - " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
20.37 - " (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e " ^
20.38 - " in ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
20.39 - " [''no_met'']) [BOOL e_e, REAL v_v])))"*))]
20.40 + @{thm norm_sqrt_equ.simps})]
20.41 \<close>
20.42
20.43 partial_function (tailrec) solve_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.44 @@ -557,21 +532,7 @@
20.45 ("#Find" ,["solutions v_v'i'"])],
20.46 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [],
20.47 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
20.48 - @{thm solve_sqrt_equ.simps}
20.49 - (*"Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
20.50 - "(let e_e = " ^
20.51 - " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''sqrt_isolate'' True)) @@ " ^
20.52 - " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^
20.53 - " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
20.54 - " (Try (Repeat (Rewrite_Set ''make_rooteq '' False))) @@ " ^
20.55 - " (Try (Rewrite_Set ''rooteq_simplify'' True)) ) e_e; " ^
20.56 - " (L_L::bool list) = " ^
20.57 - " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
20.58 - " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
20.59 - " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
20.60 - " else (SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met'']) " ^
20.61 - " [BOOL e_e, REAL v_v])) " ^
20.62 - "in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
20.63 + @{thm solve_sqrt_equ.simps})]
20.64 \<close>
20.65 (*-- right 28.08.02 --*)
20.66 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.67 @@ -596,19 +557,7 @@
20.68 ("#Find" ,["solutions v_v'i'"])],
20.69 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule.e_rls, prls = RootEq_prls, calc = [],
20.70 crls = RootEq_crls, errpats = [], nrls = norm_Poly},
20.71 - @{thm solve_sqrt_equ_right.simps}
20.72 - (*"Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
20.73 - "(let e_e = " ^
20.74 - " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''r_sqrt_isolate'' False)) @@ " ^
20.75 - " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
20.76 - " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
20.77 - " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
20.78 - " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^
20.79 - " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
20.80 - " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
20.81 - " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
20.82 - " else ((SubProblem (''RootEq'',[''univariate'',equation''], " ^
20.83 - " [''no_met'']) [BOOL e_e, REAL v_v])))"*))]
20.84 + @{thm solve_sqrt_equ_right.simps})]
20.85 \<close>
20.86 (*-- left 28.08.02 --*)
20.87 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.88 @@ -634,19 +583,7 @@
20.89 ("#Find" ,["solutions v_v'i'"])],
20.90 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[],
20.91 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
20.92 - @{thm solve_sqrt_equ_left.simps}
20.93 - (*"Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
20.94 - "(let e_e = " ^
20.95 - " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''l_sqrt_isolate'' False)) @@ " ^
20.96 - " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
20.97 - " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
20.98 - " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
20.99 - " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^
20.100 - " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^
20.101 - " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
20.102 - " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
20.103 - " else ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
20.104 - " [''no_met'']) [BOOL e_e, REAL v_v])))"*))]
20.105 + @{thm solve_sqrt_equ_left.simps})]
20.106 \<close>
20.107 ML \<open>
20.108 \<close> ML \<open>
21.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sat Jun 22 13:15:52 2019 +0200
21.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Sat Jun 22 14:34:06 2019 +0200
21.3 @@ -19,11 +19,6 @@
21.4 consts
21.5 is'_rootRatAddTerm'_in :: "[real, real] => bool"
21.6 ("_ is'_rootRatAddTerm'_in _") (*RL*)
21.7 -(*---------scripts--------------------------*)
21.8 - Elim'_rootrat'_equation
21.9 - :: "[bool,real,
21.10 - bool list] => bool list"
21.11 - ("((Script Elim'_rootrat'_equation (_ _ =))// (_))" 9)
21.12
21.13 subsection \<open>theorems not yet adopted from Isabelle\<close>
21.14 axiomatization where
21.15 @@ -168,15 +163,6 @@
21.16 ("#Find" ,["solutions v_v'i'"])],
21.17 {rew_ord'="termlessI", rls'=RooRatEq_erls, srls=Rule.e_rls, prls=RootRatEq_prls, calc=[],
21.18 crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},
21.19 - @{thm solve_rootrat_equ.simps}
21.20 - (*"Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^
21.21 - "(let e_e = ((Try (Rewrite_Set ''expand_rootbinoms'' False)) @@ " ^
21.22 - " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
21.23 - " (Try (Rewrite_Set ''make_rooteq'' False)) @@ " ^
21.24 - " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
21.25 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] " ^
21.26 - " ''rootrat_solve'' False))) e_e " ^
21.27 - " in (SubProblem (''RootEq'',[''univariate'',''equation''], " ^
21.28 - " [''no_met'']) [BOOL e_e, REAL v_v]))"*))]
21.29 + @{thm solve_rootrat_equ.simps})]
21.30 \<close>
21.31 end
22.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Sat Jun 22 13:15:52 2019 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Sat Jun 22 14:34:06 2019 +0200
22.3 @@ -20,10 +20,6 @@
22.4 Simplify :: "real => real" (*"Simplify (1+2a+3+4a)*)
22.5 Vereinfache :: "real => real" (*"Vereinfache (1+2a+3+4a)*)
22.6
22.7 - (*Script-name*)
22.8 - SimplifyScript :: "[real, real] => real"
22.9 - ("((Script SimplifyScript (_ =))// (_))" 9)
22.10 -
22.11 ML \<open>
22.12 val thy = @{theory};
22.13 \<close>
23.1 --- a/src/Tools/isac/Knowledge/Test.thy Sat Jun 22 13:15:52 2019 +0200
23.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sat Jun 22 14:34:06 2019 +0200
23.3 @@ -14,36 +14,7 @@
23.4
23.5 theory Test imports Base_Tools Poly Rational Root Diff begin
23.6
23.7 -section \<open>consts\<close>
23.8 -subsection \<open>for scripts\<close>
23.9 -consts
23.10 - Solve'_univar'_err
23.11 - :: "[bool,real,bool,
23.12 - bool list] => bool list"
23.13 - ("((Script Solve'_univar'_err (_ _ _ =))// (_))" 9)
23.14 - Solve'_linear
23.15 - :: "[bool,real,
23.16 - bool list] => bool list"
23.17 - ("((Script Solve'_linear (_ _ =))// (_))" 9)
23.18 - Solve'_root'_equation
23.19 - :: "[bool,real,
23.20 - bool list] => bool list"
23.21 - ("((Script Solve'_root'_equation (_ _ =))// (_))" 9)
23.22 - Solve'_plain'_square
23.23 - :: "[bool,real,
23.24 - bool list] => bool list"
23.25 - ("((Script Solve'_plain'_square (_ _ =))// (_))" 9)
23.26 - Norm'_univar'_equation
23.27 - :: "[bool,real,
23.28 - bool] => bool"
23.29 - ("((Script Norm'_univar'_equation (_ _ =))// (_))" 9)
23.30 - STest'_simplify
23.31 - :: "['z,
23.32 - 'z] => 'z"
23.33 - ("((Script STest'_simplify (_ =))// (_))" 9)
23.34 -
23.35 -
23.36 -subsection \<open>for problems\<close>
23.37 +section \<open>consts for problems\<close>
23.38 consts
23.39 "is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10)
23.40 "contains'_root" :: "'a => bool" ("contains'_root _" 10)
23.41 @@ -885,13 +856,7 @@
23.42 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,
23.43 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
23.44 nrls = Test_simplify},
23.45 - @{thm solve_linear.simps}
23.46 - (*"Script Solve_linear (e_e::bool) (v_v::real)= " ^
23.47 - "(let e_e = " ^
23.48 - " Repeat " ^
23.49 - " (((Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@ " ^
23.50 - " (Rewrite_Set ''Test_simplify'' False))) e_e" ^
23.51 - " in [e_e::bool])"*))]
23.52 + @{thm solve_linear.simps})]
23.53 \<close>
23.54 subsection \<open>root equation\<close>
23.55
23.56 @@ -924,69 +889,8 @@
23.57 [Rule.Calc ("Test.contains'_root",eval_contains_root "")],
23.58 calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],
23.59 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
23.60 - @{thm solve_root_equ.simps}
23.61 - (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.62 - "(let e_e = " ^
23.63 - " ((While (contains_root e_e) Do" ^
23.64 - " ((Rewrite ''square_equation_left'' True) @@" ^
23.65 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
23.66 - " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
23.67 - " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
23.68 - " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
23.69 - " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
23.70 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
23.71 - " (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@" ^
23.72 - " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
23.73 - " e_e" ^
23.74 - " in [e_e::bool])"*))]
23.75 + @{thm solve_root_equ.simps})]
23.76 \<close>
23.77 -(* UNUSED?
23.78 -partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
23.79 - where "solve_root_equ e_e v_v =
23.80 -(let e_e =
23.81 - ((While (contains_root e_e) Do
23.82 - ((Rewrite ''square_equation_left'' True) @@
23.83 - (Try (Rewrite_Set ''Test_simplify'' False)) @@
23.84 - (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
23.85 - (Try (Rewrite_Set ''isolate_root'' False)) @@
23.86 - (Try (Rewrite_Set ''Test_simplify'' False)))) @@
23.87 - (Try (Rewrite_Set ''norm_equation'' False)) @@
23.88 - (Try (Rewrite_Set ''Test_simplify'' False)) @@
23.89 - (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@
23.90 - (Try (Rewrite_Set ''Test_simplify'' False)))
23.91 - e_e;
23.92 - (L_L::bool list) = Tac ''subproblem_equation_dummy'';
23.93 - L_L = Tac ''solve_equation_dummy''
23.94 - in Check_elementwise L_L {(v_v::real). Assumptions}) "
23.95 -setup \<open>KEStore_Elems.add_mets
23.96 - [Specify.prep_met thy "met_test_sqrt2" [] Celem.e_metID
23.97 - (*root-equation ... for test-*.sml until 8.01*)
23.98 - (["Test","squ-equ-test2"],
23.99 - [("#Given" ,["equality e_e","solveFor v_v"]),
23.100 - ("#Find" ,["solutions v_v'i'"])],
23.101 - {rew_ord'="e_rew_ord",rls'=tval_rls,
23.102 - srls = Rule.append_rls "srls_contains_root" Rule.e_rls
23.103 - [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
23.104 - prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[],
23.105 - asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
23.106 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.107 - "(let e_e = " ^
23.108 - " ((While (contains_root e_e) Do" ^
23.109 - " ((Rewrite ''square_equation_left'' True) @@" ^
23.110 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
23.111 - " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
23.112 - " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
23.113 - " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
23.114 - " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
23.115 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
23.116 - " (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@" ^
23.117 - " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
23.118 - " e_e;" ^
23.119 - " (L_L::bool list) = Tac subproblem_equation_dummy; " ^
23.120 - " L_L = Tac solve_equation_dummy " ^
23.121 - " in Check_elementwise L_L {(v_v::real). Assumptions})")]
23.122 -\<close>
23.123 -*)
23.124
23.125 partial_function (tailrec) minisubpbl ::
23.126 "bool \<Rightarrow> real \<Rightarrow> bool list"
23.127 @@ -1008,16 +912,7 @@
23.128 prls = Rule.append_rls "prls_met_test_squ_sub" Rule.e_rls
23.129 [Rule.Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
23.130 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
23.131 - @{thm minisubpbl.simps}
23.132 - (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.133 - " (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@ " ^
23.134 - " (Try (Rewrite_Set ''Test_simplify'' False))) e_e; " ^
23.135 - " (L_L::bool list) = " ^
23.136 - " (SubProblem (''Test'', " ^
23.137 - " [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^
23.138 - " [''Test'', ''solve_linear'']) " ^
23.139 - " [BOOL e_e, REAL v_v]) " ^
23.140 - " in Check_elementwise L_L {(v_v::real). Assumptions}) "*))]
23.141 + @{thm minisubpbl.simps})]
23.142 \<close>
23.143
23.144 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
23.145 @@ -1045,21 +940,7 @@
23.146 [Rule.Calc ("Test.contains'_root",eval_contains_root"")], prls=Rule.e_rls, calc=[], crls=tval_rls,
23.147 errpats = [], nrls = Rule.e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),
23.148 ("square_equation_right","")]*)},
23.149 - @{thm solve_root_equ2.simps}
23.150 - (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.151 - "(let e_e = " ^
23.152 - " ((While (contains_root e_e) Do" ^
23.153 - " ((Rewrite ''square_equation_left'' True) @@" ^
23.154 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
23.155 - " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
23.156 - " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
23.157 - " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
23.158 - " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
23.159 - " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
23.160 - " e_e;" ^
23.161 - " (L_L::bool list) = (SubProblem (''Test'',[''LINEAR'',''univariate'',''equation'',''test'']," ^
23.162 - " [''Test'',''solve_linear'']) [BOOL e_e, REAL v_v])" ^
23.163 - " in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
23.164 + @{thm solve_root_equ2.simps})]
23.165 \<close>
23.166
23.167 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
23.168 @@ -1089,22 +970,7 @@
23.169 [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
23.170 prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[],
23.171 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
23.172 - @{thm solve_root_equ3.simps}
23.173 - (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.174 - "(let e_e = " ^
23.175 - " ((While (contains_root e_e) Do" ^
23.176 - " (((Rewrite ''square_equation_left'' True) Or " ^
23.177 - " (Rewrite ''square_equation_right'' True)) @@" ^
23.178 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
23.179 - " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
23.180 - " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
23.181 - " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
23.182 - " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
23.183 - " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
23.184 - " e_e;" ^
23.185 - " (L_L::bool list) = (SubProblem (''Test'',[''plain_square'',''univariate'',''equation'',''test'']," ^
23.186 - " [''Test'',''solve_plain_square'']) [BOOL e_e, REAL v_v])" ^
23.187 - " in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
23.188 + @{thm solve_root_equ3.simps})]
23.189 \<close>
23.190
23.191 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
23.192 @@ -1134,22 +1000,7 @@
23.193 [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
23.194 prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],
23.195 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
23.196 - @{thm solve_root_equ4.simps}
23.197 - (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
23.198 - "(let e_e = " ^
23.199 - " ((While (contains_root e_e) Do" ^
23.200 - " (((Rewrite ''square_equation_left'' True) Or" ^
23.201 - " (Rewrite ''square_equation_right'' True)) @@" ^
23.202 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
23.203 - " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
23.204 - " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
23.205 - " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
23.206 - " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
23.207 - " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
23.208 - " e_e;" ^
23.209 - " (L_L::bool list) = (SubProblem (''Test'',[''univariate'',''equation'',''test'']," ^
23.210 - " [''no_met'']) [BOOL e_e, REAL v_v])" ^
23.211 - " in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
23.212 + @{thm solve_root_equ4.simps})]
23.213 \<close>
23.214
23.215 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
23.216 @@ -1174,14 +1025,7 @@
23.217 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule.e_rls,
23.218 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,
23.219 asm_rls=[],asm_thm=[]*)},
23.220 - @{thm solve_plain_square.simps}
23.221 - (*"Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
23.222 - " (let e_e = ((Try (Rewrite_Set ''isolate_bdv'' False)) @@ " ^
23.223 - " (Try (Rewrite_Set ''Test_simplify'' False)) @@ " ^
23.224 - " ((Rewrite ''square_equality_0'' False) Or " ^
23.225 - " (Rewrite ''square_equality'' True)) @@ " ^
23.226 - " (Try (Rewrite_Set ''tval_rls'' False))) e_e " ^
23.227 - " in ((Or_to_List e_e)::bool list))"*))]
23.228 + @{thm solve_plain_square.simps})]
23.229 \<close>
23.230 subsection \<open>polynomial equation\<close>
23.231
23.232 @@ -1200,12 +1044,7 @@
23.233 ("#Find" ,["solutions v_v'i'"])],
23.234 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule.e_rls,prls=Rule.e_rls, calc=[], crls=tval_rls,
23.235 errpats = [], nrls = Rule.e_rls},
23.236 - @{thm norm_univariate_equ.simps}
23.237 - (*"Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
23.238 - " (let e_e = ((Try (Rewrite ''rnorm_equation_add'' False)) @@ " ^
23.239 - " (Try (Rewrite_Set ''Test_simplify'' False))) e_e " ^
23.240 - " in (SubProblem (''Test'',[''univariate'',''equation'',''test''], " ^
23.241 - " [''no_met'']) [BOOL e_e, REAL v_v]))"*))]
23.242 + @{thm norm_univariate_equ.simps})]
23.243 \<close>
23.244 subsection \<open>diophantine equation\<close>
23.245
23.246 @@ -1223,11 +1062,7 @@
23.247 ("#Find" ,["intTestFind s_s"])],
23.248 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [],
23.249 crls = tval_rls, errpats = [], nrls = Test_simplify},
23.250 - @{thm test_simplify.simps}
23.251 - (*"Script STest_simplify (t_t::int) = " ^
23.252 - "(Repeat " ^
23.253 - " ((Try (Calculate ''PLUS'')) @@ " ^
23.254 - " (Try (Calculate ''TIMES''))) t_t::int)"*))]
23.255 + @{thm test_simplify.simps})]
23.256 \<close>
23.257
23.258 end
24.1 --- a/src/Tools/isac/ProgLang/Script.thy Sat Jun 22 13:15:52 2019 +0200
24.2 +++ b/src/Tools/isac/ProgLang/Script.thy Sat Jun 22 14:34:06 2019 +0200
24.3 @@ -73,56 +73,6 @@
24.4 idletac :: 'a
24.5 (*... + RECORD IN 'screxpr' in Script.ML *)
24.6
24.7 -(*for scripts generated automatically from rls*)
24.8 - Stepwise :: "['z, 'z] => 'z" ("((Script Stepwise (_ =))// (_))" 9)
24.9 - Stepwise'_inst:: "['z,real,'z] => 'z"
24.10 - ("((Script Stepwise'_inst (_ _ =))// (_))" 9)
24.11 -
24.12 -
24.13 -(*SHIFT -> resp.thys ----vvv---------------------------------------------*)
24.14 -(*script-names: initial capital letter,
24.15 - type of last arg (=script-body) == result-type !
24.16 - Xxxx :: script ids, duplicate result-type 'r in last argument:
24.17 - "['a, ... , \
24.18 - \ 'r] => 'r
24.19 -*)
24.20 -
24.21 -(*make'_solution'_set :: "bool => bool list"
24.22 - ("(make'_solution'_set (_))" 11)
24.23 -
24.24 - max'_on'_interval
24.25 - :: "[ID * (ID list) * ID, bool,real,real set] => real"
24.26 - ("(max'_on'_interval (_)/ (_ _ _))" 9)
24.27 - find'_vals
24.28 - :: "[ID * (ID list) * ID,
24.29 - real,real,real,real,bool list] => bool list"
24.30 - ("(find'_vals (_)/ (_ _ _ _ _))" 9)
24.31 -
24.32 - make'_fun :: "[ID * (ID list) * ID, real,real,bool list] => bool"
24.33 - ("(make'_fun (_)/ (_ _ _))" 9)
24.34 -
24.35 - solve'_univar
24.36 - :: "[ID * (ID list) * ID, bool,real] => bool list"
24.37 - ("(solve'_univar (_)/ (_ _ ))" 9)
24.38 - solve'_univar'_err
24.39 - :: "[ID * (ID list) * ID, bool,real,bool] => bool list"
24.40 - ("(solve'_univar (_)/ (_ _ _))" 9)
24.41 -----------*)
24.42 -
24.43 - Testeq :: "[bool, bool] => bool"
24.44 - ("((Script Testeq (_ =))// (_))" 9)
24.45 -
24.46 - Testeq2 :: "[bool, bool list] => bool list"
24.47 - ("((Script Testeq2 (_ =))// (_))" 9)
24.48 -
24.49 - Testterm :: "[real, real] => real"
24.50 - ("((Script Testterm (_ =))// (_))" 9)
24.51 -
24.52 - Testchk :: "[bool, real, real list] => real list"
24.53 - ("((Script Testchk (_ _ =))// (_))" 9)
24.54 - (*... + RECORD IN 'subpbls' in Script.ML *)
24.55 -(*SHIFT -> resp.thys ----^^^----------------------------*)
24.56 -
24.57 (*Makarius 10.03
24.58 syntax
24.59
25.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Sat Jun 22 13:15:52 2019 +0200
25.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Sat Jun 22 14:34:06 2019 +0200
25.3 @@ -44,10 +44,6 @@
25.4 struct
25.5 (**)
25.6
25.7 -(* prepare program for Lucas-Interpretation *)
25.8 -(* version introduced BEFORE switch to partial_function *)
25.9 -fun prep_program thy str = (TermC.inst_abs o Thm.term_of o the o (TermC.parse thy)) str
25.10 -(* version for later switch to partial_function *)
25.11 fun prep_program thm = (thm
25.12 |> Thm.prop_of
25.13 |> HOLogic.dest_Trueprop
25.14 @@ -308,11 +304,11 @@
25.15 | contain_bdv (r :: _) =
25.16 error ("contain_bdv called with [" ^ Rule.id_rule r ^ ",...]");
25.17
25.18 -fun rules2scr_Rls thy rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
25.19 +fun rules2scr_Rls thy rules =
25.20 if contain_bdv rules
25.21 then FunID_Term_Bdv $ (Repeat $ (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term))
25.22 else FunID_Term $ (Repeat $ (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term));
25.23 -fun rules2scr_Seq thy rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
25.24 +fun rules2scr_Seq thy rules =
25.25 if contain_bdv rules
25.26 then FunID_Term_Bdv $ (((@@ o (map (rule2stac_inst thy))) rules) $ Rule.e_term)
25.27 else FunID_Term $ (((@@ o (map (rule2stac thy))) rules) $ Rule.e_term);
26.1 --- a/test/Tools/isac/ProgLang/termC.sml Sat Jun 22 13:15:52 2019 +0200
26.2 +++ b/test/Tools/isac/ProgLang/termC.sml Sat Jun 22 14:34:06 2019 +0200
26.3 @@ -699,49 +699,6 @@
26.4 val ty = (Term.type_of o Thm.term_of) ct;
26.5 if is_list t = true then () else error "is_list [a, b, c]";
26.6
26.7 -"----------- fun inst_abs ----------------------------------------------------------------------";
26.8 -"----------- fun inst_abs ----------------------------------------------------------------------";
26.9 -"----------- fun inst_abs ----------------------------------------------------------------------";
26.10 -(* cp from Biegelinie.thy*)
26.11 -val scr = str2term
26.12 - ("Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
26.13 - " (let fu_n = Take fu_n; " ^
26.14 - " bd_v = argument_in (lhs fu_n); " ^
26.15 - " va_l = argument_in (lhs su_b); " ^
26.16 - " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
26.17 - " eq_u = (Substitute [su_b]) eq_u " ^
26.18 - " in (Rewrite_Set ''norm_Rational'' False) eq_u) ")
26.19 -val Const ("Equation.Function2Equality", _) $ Free ("fu_n", _) $ Free ("su_b", _) $
26.20 - (Const ("HOL.Let", _) $ (Const ("Script.Take", _) $ Free ("fu_n", _)) $
26.21 - Abs ("fu_n", _, (* <-- ID taken from here ------------------------------*)
26.22 - Const ("HOL.Let", _) $
26.23 - (Const ("Atools.argument'_in", _) $ (Const ("Tools.lhs", _) $
26.24 - Bound 0)) $ (* difference --vvv ------------------------------------*)
26.25 - Abs _)) = scr;
26.26 -
26.27 -val scr' = inst_abs scr;
26.28 -val Const ("Equation.Function2Equality", _) $ Free ("fu_n", _) $ Free ("su_b", _) $
26.29 - (Const ("HOL.Let", _) $ (Const ("Script.Take", _) $ Free ("fu_n", _)) $
26.30 - Abs ("fu_n", _,
26.31 - Const ("HOL.Let", _) $
26.32 - (Const ("Atools.argument'_in", _) $ (Const ("Tools.lhs", _) $
26.33 - Free ("fu_n", _))) $ (* difference --^^^ -----------------------------------*)
26.34 - Abs _)) = scr';
26.35 -if term2str scr' = (* see the ugly IDs ...*)
26.36 - ("Script Function2Equality fu_n su_b =\n " ^
26.37 - "let fu_na = Take fu_n; " ^
26.38 - "bd_va = argument_in lhs fu_n;\n " ^
26.39 - "va_la = argument_in lhs su_b; " ^
26.40 - "eq_ua = Substitute [bd_v = va_l] fu_n;\n " ^
26.41 - "eq_ua = Substitute [su_b] eq_u\n " ^
26.42 - "in (Rewrite_Set ''norm_Rational'' False) eq_u")
26.43 - then () else error "inst_abs changed";
26.44 -
26.45 -val {scr = Prog original, ...} = get_met ["Equation","fromFunction"];
26.46 -val Const ("Equation.Function2Equality", _) $ Free ("fu_n", _) $ Free ("su_b", _) $ scr'_body = scr'
26.47 -;
26.48 -if scr'_body = LTool.body_of original then () else error "inst_abs changed";
26.49 -
26.50 "----------- fun numbers_to_string -------------------------------------------------------------";
26.51 "----------- fun numbers_to_string -------------------------------------------------------------";
26.52 "----------- fun numbers_to_string -------------------------------------------------------------";