1.1 --- a/src/Tools/isac/Interpret/mstools.sml Tue May 28 16:52:30 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/mstools.sml Wed May 29 10:36:16 2019 +0200
1.3 @@ -33,8 +33,8 @@
1.4 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
1.5 val pblID_of_match : match -> Celem.pblID
1.6 val refined_IDitms : match list -> match option
1.7 -(*val prep_program : thm -> term *)
1.8 - val prep_program : theory -> string -> term
1.9 + val prep_program : thm -> term
1.10 +(*val prep_program : theory -> string -> term *)
1.11 end
1.12
1.13 structure Stool(**) : SPECIFY_TOOL(**) =
1.14 @@ -136,6 +136,8 @@
1.15 in transfer_asms_from_to sub_ctxt caller_ctxt end;
1.16
1.17 (* prepare program for Lucas-Interpretation *)
1.18 +(* version introduced BEFORE switch to partial_function *)
1.19 +fun prep_program thy str = (TermC.inst_abs o Thm.term_of o the o (TermC.parse thy)) str
1.20 (* version for later switch to partial_function *)
1.21 fun prep_program thm = (thm
1.22 |> Thm.prop_of
1.23 @@ -143,8 +145,6 @@
1.24 |> Logic.unvarify_global
1.25 |> TermC.inst_abs)
1.26 handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm])
1.27 -(* version introduced BEFORE switch to partial_function *)
1.28 -fun prep_program thy str = (TermC.inst_abs o Thm.term_of o the o (TermC.parse thy)) str
1.29
1.30 fun common_subthy (thy1, thy2) =
1.31 if Context.subthy (thy1, thy2) then thy2
2.1 --- a/src/Tools/isac/Interpret/ptyps.sml Tue May 28 16:52:30 2019 +0200
2.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Wed May 29 10:36:16 2019 +0200
2.3 @@ -44,7 +44,7 @@
2.4 val prep_met : theory -> string -> string list -> Celem.pblID ->
2.5 string list * (string * string list) list *
2.6 {calc: 'a, crls: Rule.rls, errpats: Rule.errpat list, nrls: Rule.rls, prls: Rule.rls,
2.7 - rew_ord': Rule.rew_ord', rls': Rule.rls, srls: Rule.rls} * string ->
2.8 + rew_ord': Rule.rew_ord', rls': Rule.rls, srls: Rule.rls} * thm ->
2.9 Celem.met * Celem.metID
2.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.11 val show_ptyps : unit -> unit
2.12 @@ -76,10 +76,11 @@
2.13 case prog of
2.14 Rule.EmptyScr => NONE
2.15 | Rule.Prog t =>
2.16 -(* version for later switch to partial_function
2.17 - => SOME (get_fun_id t) *)
2.18 -(* version introduced BEFORE switch to partial_function *)
2.19 - (case t of Free ("empty_script", _) => NONE | _ => SOME (LTool.get_fun_id t))
2.20 + (* version introduced BEFORE switch to partial_function
2.21 + (case t of Free ("empty_script", _) => NONE | _ => SOME (LTool.get_fun_id t))*)
2.22 + (case t of
2.23 + Const ("HOL.eq", _) $ Free ("t", _) $ Free ("t", _) (*@{thm refl}*) => NONE
2.24 + | _ => SOME (LTool.get_fun_id t))
2.25 | Rule.Rfuns _ => NONE
2.26
2.27 (* get all data from a Ptyp tree *)
2.28 @@ -368,8 +369,8 @@
2.29 | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
2.30 handle _ => error ("prep_pbt: syntax error in '#Where' of " ^ strs2str metID))
2.31 | _ => error ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
2.32 - val sc = Stool.prep_program thy scr
2.33 - val calc = if scr = "empty_script" then [] else LTool.get_calcs thy sc
2.34 + val sc = Stool.prep_program scr
2.35 + val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else LTool.get_calcs thy sc
2.36 in
2.37 ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,
2.38 erls = rls, srls = srls, prls = prls, calc = calc,
3.1 --- a/src/Tools/isac/Interpret/script.sml Tue May 28 16:52:30 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/script.sml Wed May 29 10:36:16 2019 +0200
3.3 @@ -197,15 +197,14 @@
3.4 fun formal_args scr = (fst o split_last o snd o strip_comb) scr;
3.5
3.6 (* get the body of a program *)
3.7 +(* version introduced BEFORE switch to partial_function *)
3.8 +fun body_of (_ $ body) = body
3.9 + | body_of t = raise TERM ("body_of", [t])
3.10 (* version for later switch to partial_function *)
3.11 fun body_of tm = (tm
3.12 |> HOLogic.dest_eq
3.13 |> snd)
3.14 handle TERM _ => raise TERM ("body_of", [tm])
3.15 -(* version introduced BEFORE switch to partial_function *)
3.16 -fun body_of (_ $ body) = body
3.17 - | body_of t = raise TERM ("body_of", [t])
3.18 -
3.19
3.20 (* get the identifier of the script out of the scripts parsetree *)
3.21 fun id_of_scr sc = (id_of o fst o strip_comb) sc;
4.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Tue May 28 16:52:30 2019 +0200
4.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Wed May 29 10:36:16 2019 +0200
4.3 @@ -43,14 +43,14 @@
4.4 (["Berechnung"], [],
4.5 {rew_ord'="tless_true", rls'= Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls =Rule.Erls,
4.6 errpats = [], nrls = Rule.Erls},
4.7 - "empty_script"),
4.8 + @{thm refl}),
4.9 Specify.prep_met thy "met_algein_numsym" [] Celem.e_metID
4.10 (["Berechnung","erstNumerisch"], [],
4.11 {rew_ord'="tless_true", rls'= Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls =Rule.Erls,
4.12 errpats = [], nrls = Rule.Erls},
4.13 - "empty_script")]
4.14 + @{thm refl})]
4.15 \<close>
4.16 -(*ok
4.17 +
4.18 partial_function (tailrec) symbolisch_rechnen :: "bool \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> bool"
4.19 where
4.20 "symbolisch_rechnen k_k q__q u_u s_s o_o l_l =
4.21 @@ -71,7 +71,6 @@
4.22 t_t = Substitute [k_k, q__q] t_t;
4.23 t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t
4.24 in Try (Rewrite_Set ''norm_Poly'' False) t_t)"
4.25 -*)
4.26 setup \<open>KEStore_Elems.add_mets
4.27 [Specify.prep_met thy "met_algein_numsym_1num" [] Celem.e_metID
4.28 (["Berechnung","erstNumerisch"],
4.29 @@ -82,7 +81,8 @@
4.30 srls = Rule.append_rls "srls_..Berechnung-erstSymbolisch" Rule.e_rls
4.31 [Rule.Calc ("Atools.boollist2sum", eval_boollist2sum "")],
4.32 prls = Rule.e_rls, crls =Rule.e_rls , errpats = [], nrls = norm_Rational},
4.33 - "Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
4.34 + @{thm symbolisch_rechnen.simps}
4.35 + (*"Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
4.36 "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
4.37 " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
4.38 " su_m = boollist2sum o_o; " ^
4.39 @@ -100,9 +100,9 @@
4.40 " t_t = Substitute u_u t_t; " ^
4.41 " t_t = Substitute [k_k, q__q] t_t; " ^
4.42 " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t " ^
4.43 - " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t) ")]
4.44 + " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t) "*))]
4.45 \<close>
4.46 -(*ok
4.47 +
4.48 partial_function (tailrec) symbolisch_rechnen_2 :: "bool \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> bool"
4.49 where
4.50 "symbolisch_rechnen (k_k::bool) (q__q::bool)
4.51 @@ -122,7 +122,6 @@
4.52 t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
4.53 t_t = Substitute [k_k, q__q] t_t
4.54 in (Try (Rewrite_Set ''norm_Poly'' False)) t_t)"
4.55 -*)
4.56 setup \<open>KEStore_Elems.add_mets
4.57 [Specify.prep_met thy "met_algein_symnum" [] Celem.e_metID
4.58 (["Berechnung","erstSymbolisch"],
4.59 @@ -133,7 +132,8 @@
4.60 srls = Rule.append_rls "srls_..Berechnung-erstSymbolisch" Rule.e_rls
4.61 [Rule.Calc ("Atools.boollist2sum", eval_boollist2sum "")],
4.62 prls = Rule.e_rls, crls =Rule.e_rls , errpats = [], nrls = norm_Rational},
4.63 - "Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
4.64 + @{thm symbolisch_rechnen.simps}
4.65 + (*"Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
4.66 "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
4.67 " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
4.68 " su_m = boollist2sum o_o; " ^
4.69 @@ -149,7 +149,7 @@
4.70 " t_t = Substitute u_u t_t; " ^
4.71 " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
4.72 " t_t = Substitute [k_k, q__q] t_t " ^
4.73 - " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t) ")]
4.74 + " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t) "*))]
4.75 \<close>
4.76
4.77 end
5.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Tue May 28 16:52:30 2019 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed May 29 10:36:16 2019 +0200
5.3 @@ -184,10 +184,10 @@
5.4 (["IntegrierenUndKonstanteBestimmen"], [],
5.5 {rew_ord'="tless_true", rls'= Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls =Rule.Erls,
5.6 errpats = [], nrls = Rule.Erls},
5.7 - "empty_script")]
5.8 + @{thm refl})]
5.9 \<close>
5.10 subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
5.11 -(*ok
5.12 +
5.13 partial_function (tailrec) biegelinie :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> bool"
5.14 where
5.15 "biegelinie l q v b s vs =
5.16 @@ -201,7 +201,6 @@
5.17 B = Take (lastI funs);
5.18 B = ((Substitute cons) @@ (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B
5.19 in B)"
5.20 -*)
5.21 setup \<open>KEStore_Elems.add_mets
5.22 [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
5.23 (["IntegrierenUndKonstanteBestimmen2"],
5.24 @@ -223,7 +222,8 @@
5.25 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
5.26 Rule.Thm ("if_False",TermC.num_str @{thm if_False})],
5.27 prls = Rule.Erls, crls = Atools_erls, errpats = [], nrls = Rule.Erls},
5.28 - "Script Biegelinie2Script " ^
5.29 + @{thm biegelinie.simps}
5.30 + (*""Script Biegelinie2Script " ^
5.31 "(l::real) (q :: real) (v :: real) (id_abl::real\<Rightarrow>real) (b :: real => real) (s :: bool list) (vs :: real list) = " ^
5.32 " (let " ^
5.33 " (funs :: bool list) = (SubProblem (''Biegelinie'', " ^
5.34 @@ -238,33 +238,32 @@
5.35 " B = Take (lastI funs); " ^
5.36 " B = ((Substitute cons) @@ " ^
5.37 " (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B " ^
5.38 - " in B) ")]
5.39 + " in B) "*))]
5.40 \<close>
5.41 setup \<open>KEStore_Elems.add_mets
5.42 [Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID
5.43 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
5.44 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
5.45 errpats = [], nrls = Rule.e_rls},
5.46 - "empty_script"),
5.47 + @{thm refl}),
5.48 Specify.prep_met @{theory} "met_biege_intconst_4" [] Celem.e_metID
5.49 (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
5.50 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
5.51 errpats = [], nrls = Rule.e_rls},
5.52 - "empty_script"),
5.53 + @{thm refl}),
5.54 Specify.prep_met @{theory} "met_biege_intconst_1" [] Celem.e_metID
5.55 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
5.56 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
5.57 errpats = [], nrls = Rule.e_rls},
5.58 - "empty_script"),
5.59 + @{thm refl}),
5.60 Specify.prep_met @{theory} "met_biege2" [] Celem.e_metID
5.61 (["Biegelinien"], [],
5.62 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
5.63 errpats = [], nrls = Rule.e_rls},
5.64 - "empty_script")]
5.65 + @{thm refl})]
5.66 \<close>
5.67 subsection \<open>Compute the general bending line\<close>
5.68
5.69 -(*ok
5.70 partial_function (tailrec) belastung_zu_biegelinie :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list"
5.71 where
5.72 "belastung_zu_biegelinie q__q v_v id_fun id_abl =
5.73 @@ -285,7 +284,6 @@
5.74 [''diff'', ''integration'', ''named''])
5.75 [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun] \<comment> \<open>PROG string\<close>
5.76 in [Q__Q, M__M, N__N, B__B])"
5.77 -*)
5.78 setup \<open>KEStore_Elems.add_mets
5.79 [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
5.80 (["Biegelinien", "ausBelastung"],
5.81 @@ -301,7 +299,8 @@
5.82 srls = Rule.append_rls "srls_ausBelastung" Rule.e_rls
5.83 [Rule.Calc ("Tools.rhs", Tools.eval_rhs "eval_rhs_")],
5.84 prls = Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
5.85 - "Script Belastung2BiegelScript (q__q::real) (v_v::real) (id_fun::real\<Rightarrow>real) (id_abl::real\<Rightarrow>real) = " ^
5.86 + @{thm belastung_zu_biegelinie.simps}
5.87 + (*"Script Belastung2BiegelScript (q__q::real) (v_v::real) (id_fun::real\<Rightarrow>real) (id_abl::real\<Rightarrow>real) = " ^
5.88 " (let q___q = Take (qq v_v = q__q); " ^
5.89 " q___q = ((Rewrite ''sym_neg_equal_iff_equal'' True) @@ " ^
5.90 " (Rewrite ''Belastung_Querkraft'' True)) q___q; " ^
5.91 @@ -324,11 +323,10 @@
5.92 " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
5.93 " [''diff'',''integration'',''named'']) " ^
5.94 " [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]) " ^
5.95 - " in [Q__Q, M__M, N__N, B__B]) ")]
5.96 + " in [Q__Q, M__M, N__N, B__B]) "*))]
5.97 \<close>
5.98 subsection \<open>Substitute the constraints into the equations\<close>
5.99
5.100 -(*ok
5.101 partial_function (tailrec) setzte_randbedingungen :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
5.102 where
5.103 "setzte_randbedingungen fun_s r_b =
5.104 @@ -349,7 +347,6 @@
5.105 e_4 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
5.106 [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_4]
5.107 in [e_1, e_2, e_3, e_4])"
5.108 -*)
5.109 setup \<open>KEStore_Elems.add_mets
5.110 [Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
5.111 (["Biegelinien", "setzeRandbedingungenEin"],
5.112 @@ -357,7 +354,8 @@
5.113 ("#Find" , ["Gleichungen equs'''"])],
5.114 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = srls2, prls=Rule.e_rls, crls = Atools_erls,
5.115 errpats = [], nrls = Rule.e_rls},
5.116 - "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
5.117 + @{thm setzte_randbedingungen.simps}
5.118 + (*"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
5.119 " (let b_1 = NTH 1 r_b; " ^
5.120 " f_s = filter_sameFunId (lhs b_1) fun_s; " ^
5.121 " (e_1::bool) = " ^
5.122 @@ -382,7 +380,7 @@
5.123 " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
5.124 " [''Equation'',''fromFunction'']) " ^
5.125 " [BOOL (hd f_s), BOOL b_4]) " ^
5.126 - " in [e_1, e_2, e_3, e_4])"
5.127 + " in [e_1, e_2, e_3, e_4])"*)
5.128 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
5.129 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
5.130 " (let b_1 = NTH 1 r_b; " ^
5.131 @@ -415,7 +413,6 @@
5.132
5.133 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
5.134 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
5.135 -(*ok
5.136 partial_function (tailrec) function_to_equality :: "bool \<Rightarrow> bool \<Rightarrow> bool"
5.137 where
5.138 "function_to_equality fu_n su_b =
5.139 @@ -426,7 +423,6 @@
5.140 \<comment> \<open>([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2\<close>
5.141 eq_u = Substitute [su_b] eq_u
5.142 in (Rewrite_Set ''norm_Rational'' False) eq_u)"
5.143 -*)
5.144 setup \<open>KEStore_Elems.add_mets
5.145 [Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
5.146 (["Equation","fromFunction"],
5.147 @@ -439,14 +435,15 @@
5.148 prls=Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
5.149 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
5.150 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
5.151 - "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
5.152 + @{thm function_to_equality.simps}
5.153 + (*"Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
5.154 " (let fu_n = Take fu_n; " ^
5.155 " bd_v = argument_in (lhs fu_n); " ^
5.156 " va_l = argument_in (lhs su_b); " ^
5.157 " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
5.158 (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
5.159 " eq_u = (Substitute [su_b]) eq_u " ^
5.160 - " in (Rewrite_Set ''norm_Rational'' False) eq_u) ")]
5.161 + " in (Rewrite_Set ''norm_Rational'' False) eq_u) "*))]
5.162 \<close>
5.163
5.164 end
6.1 --- a/src/Tools/isac/Knowledge/Diff.thy Tue May 28 16:52:30 2019 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed May 29 10:36:16 2019 +0200
6.3 @@ -285,9 +285,9 @@
6.4 (["diff"], [],
6.5 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
6.6 crls = Atools_erls, errpats = [], nrls = norm_diff},
6.7 - "empty_script")]
6.8 + @{thm refl})]
6.9 \<close>
6.10 -(*ok
6.11 +
6.12 partial_function (tailrec) differentiate_on_R :: "real \<Rightarrow> real \<Rightarrow> real"
6.13 where
6.14 "differentiate_on_R f_f v_v =
6.15 @@ -312,7 +312,6 @@
6.16 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or
6.17 (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@
6.18 (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')"
6.19 -*)
6.20 setup \<open>KEStore_Elems.add_mets
6.21 [Specify.prep_met thy "met_diff_onR" [] Celem.e_metID
6.22 (["diff","differentiate_on_R"],
6.23 @@ -320,7 +319,8 @@
6.24 ("#Find" ,["derivative f_f'"])],
6.25 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
6.26 crls = Atools_erls, errpats = [], nrls = norm_diff},
6.27 - "Script DiffScr (f_f::real) (v_v::real) = " ^
6.28 + @{thm differentiate_on_R.simps}
6.29 + (*"Script DiffScr (f_f::real) (v_v::real) = " ^
6.30 " (let f_f' = Take (d_d v_v f_f) " ^
6.31 " in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^
6.32 " (Repeat " ^
6.33 @@ -341,9 +341,9 @@
6.34 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^
6.35 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^
6.36 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^
6.37 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')")]
6.38 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')"*))]
6.39 \<close>
6.40 -(*ok
6.41 +
6.42 partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real"
6.43 where
6.44 "differentiateX f_f v_v =
6.45 @@ -368,7 +368,6 @@
6.46 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or
6.47 (Repeat (Rewrite_Set ''make_polynomial'' False))))
6.48 )) f_f')"
6.49 -*)
6.50 setup \<open>KEStore_Elems.add_mets
6.51 [Specify.prep_met thy "met_diff_simpl" [] Celem.e_metID
6.52 (["diff","diff_simpl"],
6.53 @@ -376,7 +375,8 @@
6.54 ("#Find" , ["derivative f_f'"])],
6.55 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
6.56 crls = Atools_erls, errpats = [], nrls = norm_diff},
6.57 - "Script DiffScr (f_f::real) (v_v::real) = " ^
6.58 + @{thm differentiateX.simps}
6.59 + (*"Script DiffScr (f_f::real) (v_v::real) = " ^
6.60 " (let f_f' = Take (d_d v_v f_f) " ^
6.61 " in (( " ^
6.62 " (Repeat " ^
6.63 @@ -397,9 +397,9 @@
6.64 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^
6.65 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^
6.66 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) " ^
6.67 - " )) f_f')")]
6.68 + " )) f_f')"*))]
6.69 \<close>
6.70 -(*ok
6.71 +
6.72 partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool"
6.73 where
6.74 "differentiate_equality f_f v_v =
6.75 @@ -427,7 +427,6 @@
6.76 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_var'' False)) Or
6.77 (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@
6.78 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' False)))) f_f')"
6.79 -*)
6.80 setup \<open>KEStore_Elems.add_mets
6.81 [Specify.prep_met thy "met_diff_equ" [] Celem.e_metID
6.82 (["diff","differentiate_equality"],
6.83 @@ -435,7 +434,8 @@
6.84 ("#Find" ,["derivativeEq f_f'"])],
6.85 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Rule.e_rls,
6.86 crls=Atools_erls, errpats = [], nrls = norm_diff},
6.87 - "Script DiffEqScr (f_f::bool) (v_v::real) = " ^
6.88 + @{thm differentiate_equality.simps}
6.89 + (*"Script DiffEqScr (f_f::bool) (v_v::real) = " ^
6.90 " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^
6.91 " in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^
6.92 " (Repeat " ^
6.93 @@ -457,9 +457,9 @@
6.94 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^
6.95 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^
6.96 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^
6.97 - " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f') ")]
6.98 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f') "*))]
6.99 \<close>
6.100 -(*ok
6.101 +
6.102 partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real"
6.103 where
6.104 "simplify_derivative f_f v_v =
6.105 @@ -470,7 +470,6 @@
6.106 (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''norm_diff'' False)) @@
6.107 (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)) @@
6.108 (Try (Rewrite_Set ''norm_Rational'' False))) f_f')"
6.109 -*)
6.110 setup \<open>KEStore_Elems.add_mets
6.111 [Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID
6.112 (["diff","after_simplification"],
6.113 @@ -478,13 +477,14 @@
6.114 ("#Find" ,["derivative f_f'"])],
6.115 {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
6.116 crls=Atools_erls, errpats = [], nrls = norm_Rational},
6.117 - "Script DiffScr (f_f::real) (v_v::real) = " ^
6.118 + @{thm simplify_derivative.simps}
6.119 + (*"Script DiffScr (f_f::real) (v_v::real) = " ^
6.120 " (let f_f' = Take (d_d v_v f_f) " ^
6.121 " in ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
6.122 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^
6.123 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''norm_diff'' False)) @@ " ^
6.124 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)) @@ " ^
6.125 - " (Try (Rewrite_Set ''norm_Rational'' False))) f_f')")]
6.126 + " (Try (Rewrite_Set ''norm_Rational'' False))) f_f')"*))]
6.127 \<close>
6.128 setup \<open>KEStore_Elems.add_cas
6.129 [((Thm.term_of o the o (TermC.parse thy)) "Diff",
7.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Tue May 28 16:52:30 2019 +0200
7.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed May 29 10:36:16 2019 +0200
7.3 @@ -121,9 +121,9 @@
7.4 (["DiffApp"], [],
7.5 {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
7.6 crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
7.7 - "empty_script")]
7.8 + @{thm refl})]
7.9 \<close>
7.10 -(*ok
7.11 +
7.12 partial_function (tailrec) maximum_value ::
7.13 "bool list \<Rightarrow> real \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> real set \<Rightarrow> bool \<Rightarrow> bool list"
7.14 where
7.15 @@ -138,7 +138,6 @@
7.16 [BOOL t_t, REAL v_v, REAL_SET itv_v]
7.17 in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac'', ''find_values''])
7.18 [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
7.19 -*)
7.20 setup \<open>KEStore_Elems.add_mets
7.21 [Specify.prep_met thy "met_diffapp_max" [] Celem.e_metID
7.22 (["DiffApp","max_by_calculus"],
7.23 @@ -148,7 +147,8 @@
7.24 ("#Relate",[])],
7.25 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=Rule.e_rls, crls = eval_rls,
7.26 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
7.27 - "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^
7.28 + @{thm maximum_value.simps}
7.29 + (*"Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^
7.30 " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^
7.31 " (let e_e = (hd o (filterVar m_m)) r_s; " ^
7.32 " t_t = (if 1 < LENGTH r_s " ^
7.33 @@ -161,9 +161,9 @@
7.34 " [BOOL t_t, REAL v_v, REAL_SET i_tv] " ^
7.35 " in ((SubProblem (''DiffApp'',[''find_values'',''tool''],[''Isac'',''find_values'']) " ^
7.36 " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^
7.37 - " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) ")]
7.38 + " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) "*))]
7.39 \<close>
7.40 -(*ok
7.41 +
7.42 partial_function (tailrec) make_fun_by_new_variable :: "real => real => bool list => bool"
7.43 where
7.44 "make_fun_by_new_variable f_f v_v eqs =
7.45 @@ -179,7 +179,6 @@
7.46 s_2 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])
7.47 [BOOL e_2, REAL v_2]
7.48 in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
7.49 -*)
7.50 setup \<open>KEStore_Elems.add_mets
7.51 [Specify.prep_met thy "met_diffapp_funnew" [] Celem.e_metID
7.52 (["DiffApp","make_fun_by_new_variable"],
7.53 @@ -187,7 +186,8 @@
7.54 ("#Find" ,["functionEq f_1"])],
7.55 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=Rule.e_rls, calc=[], crls = eval_rls,
7.56 errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)},
7.57 - "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^
7.58 + @{thm make_fun_by_new_variable.simps}
7.59 + (*"Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^
7.60 " (eqs::bool list) = " ^
7.61 "(let h_h = (hd o (filterVar f_f)) eqs; " ^
7.62 " e_s = dropWhile (ident h_h) eqs; " ^
7.63 @@ -202,9 +202,9 @@
7.64 " (s_2::bool list) = " ^
7.65 " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
7.66 " [BOOL e_2, REAL v_2])" ^
7.67 - "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)")]
7.68 + "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"*))]
7.69 \<close>
7.70 -(*ok
7.71 +
7.72 partial_function (tailrec) make_fun_by_explicit :: "real => real => bool list => bool"
7.73 where
7.74 "make_fun_by_explicit f_f v_v eqs =
7.75 @@ -215,7 +215,6 @@
7.76 s_1 = SubProblem(''DiffApp'', [''univariate'', ''equation''], [''no_met''])
7.77 [BOOL e_1, REAL v_1]
7.78 in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
7.79 -*)
7.80 setup \<open>KEStore_Elems.add_mets
7.81 [Specify.prep_met thy "met_diffapp_funexp" [] Celem.e_metID
7.82 (["DiffApp","make_fun_by_explicit"],
7.83 @@ -223,7 +222,8 @@
7.84 ("#Find" ,["functionEq f_1"])],
7.85 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=Rule.e_rls, crls = eval_rls,
7.86 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
7.87 - "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^
7.88 + @{thm make_fun_by_explicit.simps}
7.89 + (*""Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^
7.90 " (eqs::bool list) = " ^
7.91 " (let h_h = (hd o (filterVar f_f)) eqs; " ^
7.92 " e_1 = hd (dropWhile (ident h_h) eqs); " ^
7.93 @@ -232,7 +232,7 @@
7.94 " (s_1::bool list)= " ^
7.95 " (SubProblem(DiffApp',[univariate,equation],[no_met])" ^
7.96 " [BOOL e_1, REAL v_1]) " ^
7.97 - " in Substitute [(v_1 = (rhs o hd) s_1)] h_h) ")]
7.98 + " in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "*))]
7.99 \<close>
7.100 setup \<open>KEStore_Elems.add_mets
7.101 [Specify.prep_met thy "met_diffapp_max_oninterval" [] Celem.e_metID
7.102 @@ -241,12 +241,12 @@
7.103 ("#Find" ,["maxArgument v_0"])],
7.104 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule.e_rls,prls=Rule.e_rls, crls = eval_rls,
7.105 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
7.106 - "empty_script"),
7.107 + @{thm refl}),
7.108 Specify.prep_met thy "met_diffapp_findvals" [] Celem.e_metID
7.109 (["DiffApp","find_values"], [],
7.110 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule.e_rls,prls=Rule.e_rls, crls = eval_rls,
7.111 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)},
7.112 - "empty_script")]
7.113 + @{thm refl})]
7.114 \<close>
7.115 ML \<open>
7.116 val list_rls = Rule.append_rls "list_rls" list_rls
8.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Tue May 28 16:52:30 2019 +0200
8.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Wed May 29 10:36:16 2019 +0200
8.3 @@ -29,7 +29,7 @@
8.4 Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close>
8.5
8.6 text \<open>method solving the usecase\<close>
8.7 -(*ok
8.8 +
8.9 partial_function (tailrec) diophant_equation :: "bool => int => bool"
8.10 where
8.11 "diophant_equation e_e v_v =
8.12 @@ -37,7 +37,6 @@
8.13 ((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@
8.14 (Try (Calculate ''PLUS'')) @@
8.15 (Try (Calculate ''TIMES''))) e_e)"
8.16 -*)
8.17 setup \<open>KEStore_Elems.add_mets
8.18 [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
8.19 (["Test","solve_diophant"],
8.20 @@ -47,11 +46,12 @@
8.21 ("#Find" ,["boolTestFind s_s"])],
8.22 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [],
8.23 crls = tval_rls, errpats = [], nrls = Test_simplify},
8.24 - "Script Diophant_equation (e_e::bool) (v_v::int)= " ^
8.25 + @{thm diophant_equation.simps}
8.26 + (*"Script Diophant_equation (e_e::bool) (v_v::int)= " ^
8.27 "(Repeat " ^
8.28 " ((Try (Rewrite_Inst [(''bdv'',v_v::int)] ''int_isolate_add'' False)) @@" ^
8.29 " (Try (Calculate ''PLUS'')) @@ " ^
8.30 - " (Try (Calculate ''TIMES''))) e_e::bool)")]
8.31 + " (Try (Calculate ''TIMES''))) e_e::bool)"*))]
8.32 \<close>
8.33
8.34 end
8.35 \ No newline at end of file
9.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue May 28 16:52:30 2019 +0200
9.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed May 29 10:36:16 2019 +0200
9.3 @@ -520,14 +520,14 @@
9.4 (["EqSystem"], [],
9.5 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
9.6 errpats = [], nrls = Rule.Erls},
9.7 - "empty_script"),
9.8 + @{thm refl}),
9.9 Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID
9.10 (["EqSystem","top_down_substitution"], [],
9.11 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
9.12 errpats = [], nrls = Rule.Erls},
9.13 - "empty_script")]
9.14 + @{thm refl})]
9.15 \<close>
9.16 -(*ok
9.17 +
9.18 partial_function (tailrec) solve_system :: "bool list => real list => bool list"
9.19 where
9.20 "solve_system e_s v_s =
9.21 @@ -546,7 +546,6 @@
9.22 ''simplify_System'' False))) e_2;
9.23 e__s = Take [e_1, e_2]
9.24 in Try (Rewrite_Set ''order_system'' False) e__s) "
9.25 -*)
9.26 setup \<open>KEStore_Elems.add_mets
9.27 [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
9.28 (["EqSystem", "top_down_substitution", "2x2"],
9.29 @@ -561,7 +560,8 @@
9.30 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
9.31 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
9.32 prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
9.33 - "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
9.34 + @{thm solve_system.simps}
9.35 + (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
9.36 " (let e_1 = Take (hd e_s); " ^
9.37 " e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
9.38 " ''isolate_bdvs'' False)) @@ " ^
9.39 @@ -576,7 +576,7 @@
9.40 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
9.41 " ''simplify_System'' False))) e_2; " ^
9.42 " e__s = Take [e_1, e_2] " ^
9.43 - " in (Try (Rewrite_Set ''order_system'' False)) e__s)"
9.44 + " in (Try (Rewrite_Set ''order_system'' False)) e__s)"*)
9.45 (*---------------------------------------------------------------------------
9.46 this script does NOT separate the equations as above,
9.47 but it does not yet work due to preliminary script-interpreter,
9.48 @@ -600,12 +600,12 @@
9.49 (["EqSystem", "normalise"], [],
9.50 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
9.51 errpats = [], nrls = Rule.Erls},
9.52 - "empty_script")]
9.53 + @{thm refl})]
9.54 \<close>
9.55 -(*ok
9.56 +
9.57 partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
9.58 where
9.59 -"solve_system e_s v_s =
9.60 +"solve_system2 e_s v_s =
9.61 (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@
9.62 (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
9.63 ''simplify_System_parenthesized'' False)) @@
9.64 @@ -616,7 +616,6 @@
9.65 (Try (Rewrite_Set ''order_system'' False))) e_s
9.66 in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
9.67 [BOOL_LIST e__s, REAL_LIST v_s]))"
9.68 -*)
9.69 setup \<open>KEStore_Elems.add_mets
9.70 [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
9.71 (["EqSystem","normalise","2x2"],
9.72 @@ -628,7 +627,8 @@
9.73 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
9.74 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
9.75 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
9.76 - "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
9.77 + @{thm solve_system2.simps}
9.78 + (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
9.79 " (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
9.80 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
9.81 " ''simplify_System_parenthesized'' False)) @@ " ^
9.82 @@ -638,12 +638,12 @@
9.83 " ''simplify_System_parenthesized'' False)) @@ " ^
9.84 " (Try (Rewrite_Set ''order_system'' False))) e_s " ^
9.85 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
9.86 - " [BOOL_LIST e__s, REAL_LIST v_s]))")]
9.87 + " [BOOL_LIST e__s, REAL_LIST v_s]))"*))]
9.88 \<close>
9.89 -(*ok
9.90 +
9.91 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
9.92 where
9.93 -"solve_system e_s v_s =
9.94 +"solve_system3 e_s v_s =
9.95 (let e__s =
9.96 ((Try (Rewrite_Set ''norm_Rational'' False)) @@
9.97 (Repeat (Rewrite ''commute_0_equality'' False)) @@
9.98 @@ -659,7 +659,6 @@
9.99 (Try (Rewrite_Set ''order_system'' False))) e_s
9.100 in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
9.101 [BOOL_LIST e__s, REAL_LIST v_s]))"
9.102 -*)
9.103 setup \<open>KEStore_Elems.add_mets
9.104 [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
9.105 (["EqSystem","normalise","4x4"],
9.106 @@ -672,7 +671,8 @@
9.107 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
9.108 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
9.109 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
9.110 - "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
9.111 + @{thm solve_system3.simps}
9.112 + (*""Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
9.113 " (let e__s = " ^
9.114 " ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
9.115 " (Repeat (Rewrite ''commute_0_equality'' False)) @@ " ^
9.116 @@ -687,12 +687,12 @@
9.117 " ''simplify_System_parenthesized'' False)) @@ " ^
9.118 " (Try (Rewrite_Set ''order_system'' False))) e_s " ^
9.119 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
9.120 - " [BOOL_LIST e__s, REAL_LIST v_s]))")]
9.121 + " [BOOL_LIST e__s, REAL_LIST v_s]))"*))]
9.122 \<close>
9.123 -(*ok
9.124 +
9.125 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
9.126 where
9.127 -"solve_system e_s v_s =
9.128 +"solve_system4 e_s v_s =
9.129 (let e_1 = NTH 1 e_s;
9.130 e_2 = Take (NTH 2 e_s);
9.131 e_2 = ((Substitute [e_1]) @@
9.132 @@ -706,7 +706,6 @@
9.133 (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
9.134 ''norm_Rational'' False))) e_2
9.135 in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
9.136 -*)
9.137 setup \<open>KEStore_Elems.add_mets
9.138 [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
9.139 (["EqSystem","top_down_substitution","4x4"],
9.140 @@ -723,7 +722,8 @@
9.141 [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")],
9.142 crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
9.143 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
9.144 - "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
9.145 + @{thm solve_system4.simps}
9.146 + (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
9.147 " (let e_1 = NTH 1 e_s; " ^
9.148 " e_2 = Take (NTH 2 e_s); " ^
9.149 " e_2 = ((Substitute [e_1]) @@ " ^
9.150 @@ -736,7 +736,7 @@
9.151 " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
9.152 " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
9.153 " ''norm_Rational'' False))) e_2 " ^
9.154 - " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])")]
9.155 + " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"*))]
9.156 \<close>
9.157
9.158 end
9.159 \ No newline at end of file
10.1 --- a/src/Tools/isac/Knowledge/Equation.thy Tue May 28 16:52:30 2019 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed May 29 10:36:16 2019 +0200
10.3 @@ -90,7 +90,7 @@
10.4 (["Equation"], [],
10.5 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
10.6 errpats = [], nrls = Rule.e_rls},
10.7 - "empty_script")]
10.8 + @{thm refl})]
10.9 \<close>
10.10
10.11 end
10.12 \ No newline at end of file
11.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Tue May 28 16:52:30 2019 +0200
11.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Wed May 29 10:36:16 2019 +0200
11.3 @@ -96,14 +96,14 @@
11.4 [ Specify.prep_met @{theory} "met_Programming" [] Celem.e_metID
11.5 (["Programming"], [],
11.6 {rew_ord'="tless_true",rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
11.7 - crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls}, "empty_script"),
11.8 + crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls}, @{thm refl}),
11.9 Specify.prep_met @{theory} "met_Prog_sort" [] Celem.e_metID
11.10 (["Programming","SORT"], [],
11.11 {rew_ord'="tless_true",rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
11.12 crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls},
11.13 - "empty_script")]
11.14 + @{thm refl})]
11.15 \<close>
11.16 -(*ok
11.17 +
11.18 partial_function (tailrec) sort_program :: "int xlist => int xlist"
11.19 where
11.20 "sort_program unso =
11.21 @@ -111,20 +111,20 @@
11.22 uns = Take (sort unso)
11.23 in
11.24 (Rewrite_Set ''ins_sort'' False) uns)"
11.25 -*)
11.26 setup \<open>KEStore_Elems.add_mets
11.27 [Specify.prep_met @{theory} "met_Prog_sort_ins" [] Celem.e_metID
11.28 (["Programming","SORT","insertion"],
11.29 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
11.30 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
11.31 crls = Atools_crls, errpats = [], nrls = norm_Rational},
11.32 - "Script Sortprog (unso :: int xlist) = " ^
11.33 + @{thm sort_program.simps}
11.34 + (*"Script Sortprog (unso :: int xlist) = " ^
11.35 " (let uns = Take (sort unso) " ^
11.36 " in " ^
11.37 " (Rewrite_Set ''ins_sort'' False) uns" ^
11.38 - " )")]
11.39 + " )"*))]
11.40 \<close>
11.41 -(*ok
11.42 +
11.43 partial_function (tailrec) sort_program2 :: "int xlist => int xlist"
11.44 where
11.45 "sort_program2 unso =
11.46 @@ -143,14 +143,14 @@
11.47 (Repeat (Rewrite ''If_def'' False)) Or
11.48 (Repeat (Rewrite ''if_True'' False)) Or
11.49 (Repeat (Rewrite ''if_False'' False)))) uns)"
11.50 -*)
11.51 setup \<open>KEStore_Elems.add_mets
11.52 [Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Celem.e_metID
11.53 (["Programming","SORT","insertion_steps"],
11.54 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
11.55 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
11.56 crls = Atools_crls, errpats = [], nrls = norm_Rational},
11.57 - "Script Sortprog (unso :: int xlist) = " ^
11.58 + @{thm sort_program2.simps}
11.59 + (*"Script Sortprog (unso :: int xlist) = " ^
11.60 " (let uns = Take (sort unso) " ^
11.61 " in " ^
11.62 " (Repeat " ^
11.63 @@ -167,7 +167,7 @@
11.64 " (Repeat (Rewrite ''If_def'' False)) Or " ^
11.65 " (Repeat (Rewrite ''if_True'' False)) Or " ^
11.66 " (Repeat (Rewrite ''if_False'' False)))) uns" ^
11.67 - " )")
11.68 + " )"*))
11.69 ]
11.70 \<close>
11.71
12.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Tue May 28 16:52:30 2019 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed May 29 10:36:16 2019 +0200
12.3 @@ -355,30 +355,29 @@
12.4 [["diff","integration","named"]]))]\<close>
12.5
12.6 (** methods **)
12.7 -(*ok
12.8 +
12.9 partial_function (tailrec) integrate :: "real \<Rightarrow> real \<Rightarrow> real"
12.10 where
12.11 "integrate f_f v_v =
12.12 (let t_t = Take (Integral f_f D v_v)
12.13 in (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False) t_t)"
12.14 -*)
12.15 setup \<open>KEStore_Elems.add_mets
12.16 [Specify.prep_met thy "met_diffint" [] Celem.e_metID
12.17 (["diff","integration"],
12.18 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
12.19 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
12.20 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
12.21 - "Script IntegrationScript (f_f::real) (v_v::real) = " ^
12.22 + @{thm integrate.simps}
12.23 + (*"Script IntegrationScript (f_f::real) (v_v::real) = " ^
12.24 " (let t_t = Take (Integral f_f D v_v) " ^
12.25 - " in (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False) (t_t::real))")]
12.26 + " in (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False) (t_t::real))"*))]
12.27 \<close>
12.28 -(*ok
12.29 +
12.30 partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
12.31 where "intergrate_named f_f v_v F_F =
12.32 (let t_t = Take (F_F v_v = Integral f_f D v_v)
12.33 in ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'' False)) @@
12.34 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False)) t_t)"
12.35 -*)
12.36 setup \<open>KEStore_Elems.add_mets
12.37 [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
12.38 (["diff","integration","named"],
12.39 @@ -386,10 +385,11 @@
12.40 ("#Find" ,["antiDerivativeName F_F"])],
12.41 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
12.42 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
12.43 - "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
12.44 + @{thm intergrate_named.simps}
12.45 + (*"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
12.46 " (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^
12.47 " in ((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) @@ " ^
12.48 - " (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False)) t_t) ")]
12.49 + " (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False)) t_t) "*))]
12.50 \<close>
12.51
12.52 end
12.53 \ No newline at end of file
13.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Tue May 28 16:52:30 2019 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed May 29 10:36:16 2019 +0200
13.3 @@ -75,16 +75,17 @@
13.4 [Specify.prep_met thy "met_SP" [] Celem.e_metID
13.5 (["SignalProcessing"], [],
13.6 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
13.7 - errpats = [], nrls = Rule.e_rls}, "empty_script"),
13.8 + errpats = [], nrls = Rule.e_rls}, @{thm refl}),
13.9 Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID
13.10 (["SignalProcessing", "Z_Transform"], [],
13.11 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
13.12 - errpats = [], nrls = Rule.e_rls}, "empty_script")]
13.13 + errpats = [], nrls = Rule.e_rls}, @{thm refl})]
13.14 \<close>
13.15 -(*ok
13.16 -partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> bool"
13.17 +
13.18 +(*WARNING: Additional type variable(s) in specification of "inverse_ztransform": 'a *)
13.19 +partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
13.20 where
13.21 -"inverse_ztransform X_eq = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
13.22 +"inverse_ztransform X_eq z = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
13.23 (let X = Take X_eq;
13.24 X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
13.25 X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
13.26 @@ -96,7 +97,6 @@
13.27 L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],
13.28 [''Test'',''solve_linear'']) [BOOL equ, REAL z] \<comment> \<open>PROG string\<close>
13.29 in X) "
13.30 -*)
13.31 setup \<open>KEStore_Elems.add_mets
13.32 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
13.33 (["SignalProcessing", "Z_Transform", "Inverse"],
13.34 @@ -104,7 +104,8 @@
13.35 ("#Find" ,["stepResponse (n_eq::bool)"])],
13.36 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
13.37 errpats = [], nrls = Rule.e_rls},
13.38 - "Script InverseZTransform1 (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
13.39 + @{thm inverse_ztransform.simps}
13.40 + (*"Script InverseZTransform1 (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
13.41 " (let X = Take X_eq;" ^
13.42 " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*)
13.43 " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*)
13.44 @@ -118,10 +119,9 @@
13.45 " [''LINEAR'',''univariate'',''equation'',''test'']," ^
13.46 " [''Test'',''solve_linear'']) " ^
13.47 " [BOOL equ, REAL z]) " ^
13.48 - " in X)")]
13.49 + " in X)"*))]
13.50 \<close>
13.51
13.52 -(* ok
13.53 partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
13.54 where
13.55 "inverse_ztransform2 X_eq X_z =
13.56 @@ -139,7 +139,6 @@
13.57 X_zeq = Take (X_z = rhs pbz_eq);
13.58 n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq
13.59 in n_eq)"
13.60 -*)
13.61 setup \<open>KEStore_Elems.add_mets
13.62 [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
13.63 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
13.64 @@ -166,7 +165,8 @@
13.65 eval_factors_from_solution "#factors_from_solution")
13.66 ], scr = Rule.EmptyScr},
13.67 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational},
13.68 - " Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
13.69 + @{thm simplify.simps}
13.70 + (*" Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
13.71 " (let X = Take X_eq; "^ (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
13.72 " X' = Rewrite ''ruleZY'' False X; "^ (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
13.73 " (X'_z::real) = lhs X'; "^ (* ?X' z*)
13.74 @@ -180,7 +180,7 @@
13.75 " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
13.76 " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
13.77 " 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]*)
13.78 - " in n_eq) ")](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
13.79 + " in n_eq) "*))](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
13.80 \<close>
13.81
13.82 end
14.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Tue May 28 16:52:30 2019 +0200
14.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed May 29 10:36:16 2019 +0200
14.3 @@ -137,10 +137,10 @@
14.4 (["LinEq"], [],
14.5 {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
14.6 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
14.7 - "empty_script")]
14.8 + @{thm refl})]
14.9 \<close>
14.10 (* ansprechen mit ["LinEq","solve_univar_equation"] *)
14.11 -(*ok
14.12 +
14.13 partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.14 where
14.15 "solve_linear_equation e_e v_v =
14.16 @@ -154,7 +154,6 @@
14.17 ''LinEq_simplify'' True)) @@
14.18 (Repeat(Try (Rewrite_Set ''LinPoly_simplify'' False)))) e_e
14.19 in Or_to_List e_e)"
14.20 -*)
14.21 setup \<open>KEStore_Elems.add_mets
14.22 [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
14.23 (["LinEq","solve_lineq_equation"],
14.24 @@ -163,7 +162,8 @@
14.25 ("#Find", ["solutions v_v'i'"])],
14.26 {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule.e_rls, prls = LinEq_prls, calc = [],
14.27 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
14.28 - "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^
14.29 + @{thm solve_linear_equation.simps}
14.30 + (*"Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^
14.31 "(let e_e =((Try (Rewrite ''all_left'' False)) @@ " ^
14.32 " (Try (Repeat (Rewrite ''makex1_x'' False))) @@ " ^
14.33 " (Try (Rewrite_Set ''expand_binoms'' False)) @@ " ^
14.34 @@ -173,7 +173,7 @@
14.35 " e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)] " ^
14.36 " ''LinEq_simplify'' True)) @@ " ^
14.37 " (Repeat(Try (Rewrite_Set ''LinPoly_simplify'' False)))) e_e " ^
14.38 - " in ((Or_to_List e_e)::bool list))")]
14.39 + " in ((Or_to_List e_e)::bool list))"*))]
14.40 \<close>
14.41 ML \<open>Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"];\<close>
14.42
15.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Tue May 28 16:52:30 2019 +0200
15.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed May 29 10:36:16 2019 +0200
15.3 @@ -39,7 +39,7 @@
15.4 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]]))]\<close>
15.5
15.6 (** methods **)
15.7 -(*ok
15.8 +
15.9 partial_function (tailrec) solve_log :: "bool \<Rightarrow> real \<Rightarrow> bool list"
15.10 where
15.11 "solve_log e_e v_v =
15.12 @@ -47,7 +47,6 @@
15.13 (Rewrite ''exp_invers_log'' False) @@
15.14 (Rewrite_Set ''norm_Poly'' False)) e_e
15.15 in [e_e])"
15.16 -*)
15.17 setup \<open>KEStore_Elems.add_mets
15.18 [Specify.prep_met thy "met_equ_log" [] Celem.e_metID
15.19 (["Equation","solve_log"],
15.20 @@ -56,11 +55,12 @@
15.21 ("#Find" ,["solutions v_v'i'"])],
15.22 {rew_ord' = "termlessI", rls' = PolyEq_erls, srls = Rule.e_rls, prls = PolyEq_prls, calc = [],
15.23 crls = PolyEq_crls, errpats = [], nrls = norm_Rational},
15.24 - "Script Solve_log (e_e::bool) (v_v::real) = " ^
15.25 + @{thm solve_log.simps}
15.26 + (*"Script Solve_log (e_e::bool) (v_v::real) = " ^
15.27 "(let e_e = ((Rewrite ''equality_power'' False) @@ " ^
15.28 " (Rewrite ''exp_invers_log'' False) @@ " ^
15.29 " (Rewrite_Set ''norm_Poly'' False)) e_e " ^
15.30 - " in [e_e])")]
15.31 + " in [e_e])"*))]
15.32 \<close>
15.33
15.34 end
15.35 \ No newline at end of file
16.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Tue May 28 16:52:30 2019 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed May 29 10:36:16 2019 +0200
16.3 @@ -192,7 +192,6 @@
16.4 \<close>
16.5
16.6 (* current version, error outcommented *)
16.7 -(*ok
16.8 partial_function (tailrec) partial_fraction :: "real \<Rightarrow> real \<Rightarrow> real"
16.9 where
16.10 "partial_fraction f_f zzz = \<comment> \<open>([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))\<close>
16.11 @@ -232,7 +231,6 @@
16.12 pbz = Take eqr; \<comment> \<open>([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)\<close>
16.13 pbz = Substitute [AA = a, BB = b] pbz \<comment> \<open>([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)\<close>
16.14 in pbz) "
16.15 -*)
16.16 setup \<open>KEStore_Elems.add_mets
16.17 [Specify.prep_met @{theory} "met_partial_fraction" [] Celem.e_metID
16.18 (["simplification","of_rationals","to_partial_fraction"],
16.19 @@ -244,7 +242,8 @@
16.20 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = srls_partial_fraction, prls = Rule.e_rls,
16.21 crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls},
16.22 (*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*)
16.23 - "Script PartFracScript (f_f::real) (zzz::real) = " ^
16.24 + @{thm partial_fraction.simps}
16.25 + (*"Script PartFracScript (f_f::real) (zzz::real) = " ^
16.26 (*([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
16.27 "(let f_f = Take f_f; " ^
16.28 (* num_orig = 3*)
16.29 @@ -309,7 +308,7 @@
16.30 (*([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
16.31 " pbz = ((Substitute [AA = a, BB = b]) pbz) " ^
16.32 (*([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
16.33 - "in pbz)"
16.34 + "in pbz)"*)
16.35 )]
16.36 \<close>
16.37 ML \<open>
17.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue May 28 16:52:30 2019 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed May 29 10:36:16 2019 +0200
17.3 @@ -1582,11 +1582,10 @@
17.4 [["simplification","for_polynomials"]]))]\<close>
17.5
17.6 subsection \<open>methods\<close>
17.7 -(*ok
17.8 +
17.9 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
17.10 where
17.11 "simplify term = ((Rewrite_Set ''norm_Poly'' False) term)"
17.12 -*)
17.13 setup \<open>KEStore_Elems.add_mets
17.14 [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
17.15 (["simplification","for_polynomials"],
17.16 @@ -1598,8 +1597,9 @@
17.17 [(*for preds in where_*)
17.18 Rule.Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
17.19 crls = Rule.e_rls, errpats = [], nrls = norm_Poly},
17.20 - "Script SimplifyScript (t_t::real) = " ^
17.21 - " ((Rewrite_Set ''norm_Poly'' False) t_t)")]
17.22 + @{thm simplify.simps}
17.23 + (*"Script SimplifyScript (t_t::real) = " ^
17.24 + " ((Rewrite_Set ''norm_Poly'' False) t_t)"*))]
17.25 \<close>
17.26 ML \<open>
17.27 \<close> ML \<open>
18.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue May 28 16:52:30 2019 +0200
18.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed May 29 10:36:16 2019 +0200
18.3 @@ -972,9 +972,9 @@
18.4 (["PolyEq"], [],
18.5 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
18.6 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
18.7 - "empty_script")]
18.8 + @{thm refl})]
18.9 \<close>
18.10 -(*ok
18.11 +
18.12 partial_function (tailrec) normalize_poly_eq :: "bool \<Rightarrow> real \<Rightarrow> bool"
18.13 where
18.14 "normalize_poly_eq e_e v_v =
18.15 @@ -985,7 +985,6 @@
18.16 (Try (Repeat (Rewrite_Set ''polyeq_simplify'' False)))) e_e
18.17 in SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
18.18 [BOOL e_e, REAL v_v])"
18.19 -*)
18.20 setup \<open>KEStore_Elems.add_mets
18.21 [Specify.prep_met thy "met_polyeq_norm" [] Celem.e_metID
18.22 (["PolyEq","normalise_poly"],
18.23 @@ -994,7 +993,8 @@
18.24 ("#Find" ,["solutions v_v'i'"])],
18.25 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls, calc=[],
18.26 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
18.27 - "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
18.28 + @{thm normalize_poly_eq.simps}
18.29 + (*"Script Normalize_poly (e_e::bool) (v_v::real) = " ^
18.30 "(let e_e =((Try (Rewrite ''all_left'' False)) @@ " ^
18.31 " (Try (Repeat (Rewrite ''makex1_x'' False))) @@ " ^
18.32 " (Try (Repeat (Rewrite_Set ''expand_binoms'' False))) @@ " ^
18.33 @@ -1002,15 +1002,14 @@
18.34 " ''make_ratpoly_in'' False))) @@ " ^
18.35 " (Try (Repeat (Rewrite_Set ''polyeq_simplify'' False)))) e_e " ^
18.36 " in (SubProblem (''PolyEq'',[''polynomial'',''univariate'',''equation''], [''no_met'']) " ^
18.37 - " [BOOL e_e, REAL v_v]))")]
18.38 + " [BOOL e_e, REAL v_v]))"*))]
18.39 \<close>
18.40 -(*ok
18.41 +
18.42 partial_function (tailrec) solve_poly_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.43 where
18.44 "solve_poly_equ e_e v_v =
18.45 (let e_e = (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d0_polyeq_simplify'' False)) e_e
18.46 in Or_to_List e_e)"
18.47 -*)
18.48 setup \<open>KEStore_Elems.add_mets
18.49 [Specify.prep_met thy "met_polyeq_d0" [] Celem.e_metID
18.50 (["PolyEq","solve_d0_polyeq_equation"],
18.51 @@ -1020,12 +1019,13 @@
18.52 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
18.53 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
18.54 nrls = norm_Rational},
18.55 - "Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
18.56 + @{thm solve_poly_equ.simps}
18.57 + (*"Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
18.58 "(let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
18.59 " ''d0_polyeq_simplify'' False))) e_e " ^
18.60 - " in ((Or_to_List e_e)::bool list))")]
18.61 + " in ((Or_to_List e_e)::bool list))"*))]
18.62 \<close>
18.63 -(*ok
18.64 +
18.65 partial_function (tailrec) solve_poly_eq1 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.66 where "solve_poly_eq1 e_e v_v =
18.67 (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'' True)) @@
18.68 @@ -1033,7 +1033,6 @@
18.69 (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
18.70 L_L = Or_to_List e_e
18.71 in Check_elementwise L_L {(v_v::real). Assumptions})"
18.72 -*)
18.73 setup \<open>KEStore_Elems.add_mets
18.74 [Specify.prep_met thy "met_polyeq_d1" [] Celem.e_metID
18.75 (["PolyEq","solve_d1_polyeq_equation"],
18.76 @@ -1043,15 +1042,16 @@
18.77 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
18.78 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
18.79 nrls = norm_Rational},
18.80 - "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
18.81 + @{thm solve_poly_eq1.simps}
18.82 + (*"Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
18.83 "(let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
18.84 " ''d1_polyeq_simplify'' True)) @@ " ^
18.85 " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
18.86 " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
18.87 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
18.88 - " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
18.89 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
18.90 \<close>
18.91 -(*ok
18.92 +
18.93 partial_function (tailrec) solve_poly_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.94 where
18.95 "solve_poly_equ2 e_e v_v =
18.96 @@ -1062,7 +1062,6 @@
18.97 (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
18.98 L_L = Or_to_List e_e
18.99 in Check_elementwise L_L {(v_v::real). Assumptions})"
18.100 -*)
18.101 setup \<open>KEStore_Elems.add_mets
18.102 [Specify.prep_met thy "met_polyeq_d22" [] Celem.e_metID
18.103 (["PolyEq","solve_d2_polyeq_equation"],
18.104 @@ -1072,7 +1071,8 @@
18.105 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
18.106 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
18.107 nrls = norm_Rational},
18.108 - "Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
18.109 + @{thm solve_poly_equ2.simps}
18.110 + (*"Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
18.111 " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
18.112 " ''d2_polyeq_simplify'' True)) @@ " ^
18.113 " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
18.114 @@ -1081,9 +1081,9 @@
18.115 " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
18.116 " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
18.117 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
18.118 - " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
18.119 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
18.120 \<close>
18.121 -(*ok
18.122 +
18.123 partial_function (tailrec) solve_poly_equ0 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.124 where "solve_poly_equ0 e_e v_v =
18.125 (let
18.126 @@ -1094,7 +1094,6 @@
18.127 (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
18.128 L_L = Or_to_List e_e
18.129 in Check_elementwise L_L {(v_v::real). Assumptions})"
18.130 -*)
18.131 setup \<open>KEStore_Elems.add_mets
18.132 [Specify.prep_met thy "met_polyeq_d2_bdvonly" [] Celem.e_metID
18.133 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
18.134 @@ -1104,7 +1103,8 @@
18.135 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
18.136 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
18.137 nrls = norm_Rational},
18.138 - "Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
18.139 + @{thm solve_poly_equ0.simps}
18.140 + (*"Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
18.141 " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
18.142 " ''d2_polyeq_bdv_only_simplify'' True)) @@ " ^
18.143 " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
18.144 @@ -1113,9 +1113,9 @@
18.145 " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
18.146 " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
18.147 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
18.148 - " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
18.149 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
18.150 \<close>
18.151 -(*ok
18.152 +
18.153 partial_function (tailrec) solve_poly_equ_sqrt :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.154 where
18.155 "solve_poly_equ_sqrt e_e v_v =
18.156 @@ -1125,7 +1125,6 @@
18.157 (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
18.158 L_L = Or_to_List e_e
18.159 in Check_elementwise L_L {(v_v::real). Assumptions})"
18.160 -*)
18.161 setup \<open>KEStore_Elems.add_mets
18.162 [Specify.prep_met thy "met_polyeq_d2_sqonly" [] Celem.e_metID
18.163 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
18.164 @@ -1135,15 +1134,16 @@
18.165 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
18.166 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
18.167 nrls = norm_Rational},
18.168 - "Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
18.169 + @{thm solve_poly_equ_sqrt.simps}
18.170 + (*"Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
18.171 " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
18.172 " ''d2_polyeq_sq_only_simplify'' True)) @@ " ^
18.173 " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
18.174 " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e; " ^
18.175 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
18.176 - " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
18.177 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
18.178 \<close>
18.179 -(*ok
18.180 +
18.181 partial_function (tailrec) solve_poly_equ_pq :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.182 where "solve_poly_equ_pq e_e v_v =
18.183 (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_pqFormula_simplify'' True)) @@
18.184 @@ -1151,7 +1151,6 @@
18.185 (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
18.186 L_L = Or_to_List e_e
18.187 in Check_elementwise L_L {(v_v::real). Assumptions})"
18.188 -*)
18.189 setup \<open>KEStore_Elems.add_mets
18.190 [Specify.prep_met thy "met_polyeq_d2_pq" [] Celem.e_metID
18.191 (["PolyEq","solve_d2_polyeq_pq_equation"],
18.192 @@ -1161,15 +1160,16 @@
18.193 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
18.194 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
18.195 nrls = norm_Rational},
18.196 - "Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
18.197 + @{thm solve_poly_equ_pq.simps}
18.198 + (*"Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
18.199 " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
18.200 " ''d2_polyeq_pqFormula_simplify'' True)) @@ " ^
18.201 " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
18.202 " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
18.203 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
18.204 - " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
18.205 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
18.206 \<close>
18.207 -(*ok
18.208 +
18.209 partial_function (tailrec) solve_poly_equ_abc :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.210 where
18.211 "solve_poly_equ_abc e_e v_v =
18.212 @@ -1178,7 +1178,6 @@
18.213 (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
18.214 L_L = Or_to_List e_e
18.215 in Check_elementwise L_L {(v_v::real). Assumptions})"
18.216 -*)
18.217 setup \<open>KEStore_Elems.add_mets
18.218 [Specify.prep_met thy "met_polyeq_d2_abc" [] Celem.e_metID
18.219 (["PolyEq","solve_d2_polyeq_abc_equation"],
18.220 @@ -1188,15 +1187,16 @@
18.221 {rew_ord'="termlessI", rls'=PolyEq_erls,srls=Rule.e_rls, prls=PolyEq_prls,
18.222 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
18.223 nrls = norm_Rational},
18.224 - "Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
18.225 + @{thm solve_poly_equ_abc.simps}
18.226 + (*"Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
18.227 " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
18.228 " ''d2_polyeq_abcFormula_simplify'' True)) @@ " ^
18.229 " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
18.230 " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
18.231 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
18.232 - " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
18.233 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
18.234 \<close>
18.235 -(*ok
18.236 +
18.237 partial_function (tailrec) solve_poly_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.238 where "solve_poly_equ3 e_e v_v =
18.239 (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d3_polyeq_simplify'' True)) @@
18.240 @@ -1208,7 +1208,6 @@
18.241 (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
18.242 L_L = Or_to_List e_e
18.243 in Check_elementwise L_L {(v_v::real). Assumptions})"
18.244 -*)
18.245 setup \<open>KEStore_Elems.add_mets
18.246 [Specify.prep_met thy "met_polyeq_d3" [] Celem.e_metID
18.247 (["PolyEq","solve_d3_polyeq_equation"],
18.248 @@ -1218,7 +1217,8 @@
18.249 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls,
18.250 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
18.251 nrls = norm_Rational},
18.252 - "Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
18.253 + @{thm solve_poly_equ3.simps}
18.254 + (*"Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
18.255 " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
18.256 " ''d3_polyeq_simplify'' True)) @@ " ^
18.257 " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
18.258 @@ -1230,12 +1230,11 @@
18.259 " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
18.260 " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
18.261 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
18.262 - " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
18.263 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"*))]
18.264 \<close>
18.265 (*.solves all expanded (ie. normalised) terms of degree 2.*)
18.266 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
18.267 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
18.268 -(*ok
18.269 partial_function (tailrec) solve_by_completing_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.270 where
18.271 "solve_by_completing_square e_e v_v =
18.272 @@ -1251,7 +1250,6 @@
18.273 (Try (Rewrite_Set ''calculate_RootRat'' False)) @@
18.274 (Try (Repeat (Calculate ''SQRT'')))) e_e
18.275 in Or_to_List e_e)"
18.276 -*)
18.277 setup \<open>KEStore_Elems.add_mets
18.278 [Specify.prep_met thy "met_polyeq_complsq" [] Celem.e_metID
18.279 (["PolyEq","complete_square"],
18.280 @@ -1261,7 +1259,8 @@
18.281 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=Rule.e_rls,prls=PolyEq_prls,
18.282 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
18.283 nrls = norm_Rational},
18.284 - "Script Complete_square (e_e::bool) (v_v::real) = " ^
18.285 + @{thm solve_by_completing_square.simps}
18.286 + (*"Script Complete_square (e_e::bool) (v_v::real) = " ^
18.287 "(let e_e = " ^
18.288 " ((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''cancel_leading_coeff'' True)) " ^
18.289 " @@ (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''complete_square'' True)) " ^
18.290 @@ -1274,7 +1273,7 @@
18.291 " (Rewrite_Inst [(''bdv'',v_v)] ''bdv_explicit3'' False))) " ^
18.292 " @@ (Try (Rewrite_Set ''calculate_RootRat'' False)) " ^
18.293 " @@ (Try (Repeat (Calculate ''SQRT'')))) e_e " ^
18.294 - " in ((Or_to_List e_e)::bool list))")]
18.295 + " in ((Or_to_List e_e)::bool list))"*))]
18.296 \<close>
18.297
18.298 ML\<open>
19.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Tue May 28 16:52:30 2019 +0200
19.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed May 29 10:36:16 2019 +0200
19.3 @@ -475,14 +475,13 @@
19.4 SOME "Probe e_e w_w", [["probe","fuer_bruch"]]))]\<close>
19.5
19.6 (** methods **)
19.7 -(*ok
19.8 +
19.9 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
19.10 where
19.11 "simplify t_t =
19.12 ((Repeat((Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@
19.13 (Try (Rewrite_Set ''fasse_zusammen'' False)) @@
19.14 (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"
19.15 -*)
19.16 setup \<open>KEStore_Elems.add_mets
19.17 [Specify.prep_met thy "met_simp_poly_minus" [] Celem.e_metID
19.18 (["simplification","for_polynomials","with_minus"],
19.19 @@ -506,20 +505,20 @@
19.20 Rule.Thm ("not_false",TermC.num_str @{thm not_false})
19.21 (*"(~ False) = True"*)],
19.22 crls = Rule.e_rls, errpats = [], nrls = rls_p_33},
19.23 - "Script SimplifyScript (t_t::real) = " ^
19.24 + @{thm simplify.simps}
19.25 + (*"Script SimplifyScript (t_t::real) = " ^
19.26 " ((Repeat((Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@ " ^
19.27 " (Try (Rewrite_Set ''fasse_zusammen'' False)) @@ " ^
19.28 - " (Try (Rewrite_Set ''verschoenere'' False)))) t_t)")]
19.29 + " (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"*))]
19.30 \<close>
19.31 -(*ok
19.32 +
19.33 partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"
19.34 where
19.35 -"simplify t_t =
19.36 +"simplify2 t_t =
19.37 ((Repeat((Try (Rewrite_Set ''klammern_aufloesen'' False)) @@
19.38 (Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@
19.39 (Try (Rewrite_Set ''fasse_zusammen'' False)) @@
19.40 (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"
19.41 -*)
19.42 setup \<open>KEStore_Elems.add_mets
19.43 [Specify.prep_met thy "met_simp_poly_parenth" [] Celem.e_metID
19.44 (["simplification","for_polynomials","with_parentheses"],
19.45 @@ -530,16 +529,17 @@
19.46 prls = Rule.append_rls "simplification_for_polynomials_prls" Rule.e_rls
19.47 [(*for preds in where_*) Rule.Calc("Poly.is'_polyexp",eval_is_polyexp"")],
19.48 crls = Rule.e_rls, errpats = [], nrls = rls_p_34},
19.49 - "Script SimplifyScript (t_t::real) = " ^
19.50 + @{thm simplify2.simps}
19.51 + (*"Script SimplifyScript (t_t::real) = " ^
19.52 " ((Repeat((Try (Rewrite_Set ''klammern_aufloesen'' False)) @@ " ^
19.53 " (Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@ " ^
19.54 " (Try (Rewrite_Set ''fasse_zusammen'' False)) @@ " ^
19.55 - " (Try (Rewrite_Set ''verschoenere'' False)))) t_t)")]
19.56 + " (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"*))]
19.57 \<close>
19.58 -(*ok
19.59 +
19.60 partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"
19.61 where
19.62 -"simplify t_t =
19.63 +"simplify3 t_t =
19.64 ((Repeat((Try (Rewrite_Set ''klammern_ausmultiplizieren'' False)) @@
19.65 (Try (Rewrite_Set ''discard_parentheses'' False)) @@
19.66 (Try (Rewrite_Set ''ordne_monome'' False)) @@
19.67 @@ -547,7 +547,6 @@
19.68 (Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@
19.69 (Try (Rewrite_Set ''fasse_zusammen'' False)) @@
19.70 (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"
19.71 -*)
19.72 setup \<open>KEStore_Elems.add_mets
19.73 [Specify.prep_met thy "met_simp_poly_parenth_mult" [] Celem.e_metID
19.74 (["simplification","for_polynomials","with_parentheses_mult"],
19.75 @@ -556,23 +555,24 @@
19.76 prls = Rule.append_rls "simplification_for_polynomials_prls" Rule.e_rls
19.77 [(*for preds in where_*) Rule.Calc("Poly.is'_polyexp",eval_is_polyexp"")],
19.78 crls = Rule.e_rls, errpats = [], nrls = rls_p_34},
19.79 - "Script SimplifyScript (t_t::real) = " ^
19.80 + @{thm simplify3.simps}
19.81 + (*"Script SimplifyScript (t_t::real) = " ^
19.82 " ((Repeat((Try (Rewrite_Set ''klammern_ausmultiplizieren'' False)) @@ " ^
19.83 " (Try (Rewrite_Set ''discard_parentheses'' False)) @@ " ^
19.84 " (Try (Rewrite_Set ''ordne_monome'' False)) @@ " ^
19.85 " (Try (Rewrite_Set ''klammern_aufloesen'' False)) @@ " ^
19.86 " (Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@ " ^
19.87 " (Try (Rewrite_Set ''fasse_zusammen'' False)) @@ " ^
19.88 - " (Try (Rewrite_Set ''verschoenere'' False)))) t_t)")]
19.89 + " (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"*))]
19.90 \<close>
19.91 setup \<open>KEStore_Elems.add_mets
19.92 [Specify.prep_met thy "met_probe" [] Celem.e_metID
19.93 (["probe"], [],
19.94 {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.Erls, crls = Rule.e_rls,
19.95 errpats = [], nrls = Rule.Erls},
19.96 - "empty_script")]
19.97 + @{thm refl})]
19.98 \<close>
19.99 -(*ok
19.100 +
19.101 partial_function (tailrec) mache_probe :: "bool \<Rightarrow> bool list \<Rightarrow> bool"
19.102 where
19.103 "mache_probe e_e w_w =
19.104 @@ -581,7 +581,6 @@
19.105 in (Repeat ((Try (Repeat (Calculate ''TIMES''))) @@
19.106 (Try (Repeat (Calculate ''PLUS'' ))) @@
19.107 (Try (Repeat (Calculate ''MINUS''))))) e_e)"
19.108 -*)
19.109 setup \<open>KEStore_Elems.add_mets
19.110 [Specify.prep_met thy "met_probe_poly" [] Celem.e_metID
19.111 (["probe","fuer_polynom"],
19.112 @@ -592,12 +591,13 @@
19.113 prls = Rule.append_rls "prls_met_probe_bruch" Rule.e_rls
19.114 [(*for preds in where_*) Rule.Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
19.115 crls = Rule.e_rls, errpats = [], nrls = rechnen},
19.116 - "Script ProbeScript (e_e::bool) (w_w::bool list) = " ^
19.117 + @{thm mache_probe.simps}
19.118 + (*"Script ProbeScript (e_e::bool) (w_w::bool list) = " ^
19.119 " (let e_e = Take e_e; " ^
19.120 " e_e = Substitute w_w e_e " ^
19.121 " in (Repeat((Try (Repeat (Calculate ''TIMES''))) @@ " ^
19.122 " (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
19.123 - " (Try (Repeat (Calculate ''MINUS''))))) e_e)")]
19.124 + " (Try (Repeat (Calculate ''MINUS''))))) e_e)"*))]
19.125 \<close>
19.126 setup \<open>KEStore_Elems.add_mets
19.127 [Specify.prep_met thy "met_probe_bruch" [] Celem.e_metID
19.128 @@ -609,7 +609,7 @@
19.129 prls = Rule.append_rls "prls_met_probe_bruch" Rule.e_rls
19.130 [(*for preds in where_*) Rule.Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
19.131 crls = Rule.e_rls, errpats = [], nrls = Rule.Erls},
19.132 - "empty_script")]
19.133 + @{thm refl})]
19.134 \<close>
19.135
19.136 end
20.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Tue May 28 16:52:30 2019 +0200
20.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed May 29 10:36:16 2019 +0200
20.3 @@ -177,8 +177,8 @@
20.4 [Specify.prep_met thy "met_rateq" [] Celem.e_metID
20.5 (["RatEq"], [],
20.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
20.7 - crls=RatEq_crls, errpats = [], nrls = norm_Rational}, "empty_script")]\<close>
20.8 -(*ok
20.9 + crls=RatEq_crls, errpats = [], nrls = norm_Rational}, @{thm refl})]\<close>
20.10 +
20.11 partial_function (tailrec) solve_rational_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.12 where
20.13 "solve_rational_equ e_e v_v =
20.14 @@ -189,7 +189,6 @@
20.15 L_L = SubProblem (''RatEq'', [''univariate'', ''equation''], [''no_met''])
20.16 [BOOL e_e, REAL v_v]
20.17 in Check_elementwise L_L {(v_v::real). Assumptions})"
20.18 -*)
20.19 setup \<open>KEStore_Elems.add_mets
20.20 [Specify.prep_met thy "met_rat_eq" [] Celem.e_metID
20.21 (["RatEq", "solve_rat_equation"],
20.22 @@ -198,14 +197,15 @@
20.23 ("#Find" ,["solutions v_v'i'"])],
20.24 {rew_ord'="termlessI", rls'=rateq_erls, srls=Rule.e_rls, prls=RatEq_prls, calc=[],
20.25 crls=RatEq_crls, errpats = [], nrls = norm_Rational},
20.26 - "Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^
20.27 + @{thm solve_rational_equ.simps}
20.28 + (*"Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^
20.29 "(let e_e = ((Repeat(Try (Rewrite_Set ''RatEq_simplify'' True))) @@ " ^
20.30 " (Repeat(Try (Rewrite_Set ''norm_Rational'' False))) @@ " ^
20.31 " (Repeat(Try (Rewrite_Set ''add_fractions_p'' False))) @@ " ^
20.32 " (Repeat(Try (Rewrite_Set ''RatEq_eliminate'' True)))) e_e;" ^
20.33 " (L_L::bool list) = (SubProblem (''RatEq'',[''univariate'',''equation''], [''no_met''])" ^
20.34 " [BOOL e_e, REAL v_v]) " ^
20.35 - " in Check_elementwise L_L {(v_v::real). Assumptions})")]
20.36 + " in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
20.37 \<close>
20.38 ML \<open>
20.39 \<close> ML \<open>
21.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue May 28 16:52:30 2019 +0200
21.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed May 29 10:36:16 2019 +0200
21.3 @@ -889,7 +889,7 @@
21.4 section \<open>A methods for simplification of rationals\<close>
21.5 (*WN061025 this methods script is copied from (auto-generated) script
21.6 of norm_Rational in order to ease repair on inform*)
21.7 -(*ok
21.8 +
21.9 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
21.10 where
21.11 "simplify t_t =
21.12 @@ -905,7 +905,6 @@
21.13 Try (Rewrite_Set ''rat_reduce_1'' False)))) @@
21.14 Try (Rewrite_Set ''discard_parentheses1'' False))
21.15 t_t)"
21.16 -*)
21.17 setup \<open>KEStore_Elems.add_mets
21.18 [Specify.prep_met thy "met_simp_rat" [] Celem.e_metID
21.19 (["simplification","of_rationals"],
21.20 @@ -916,7 +915,8 @@
21.21 prls = Rule.append_rls "simplification_of_rationals_prls" Rule.e_rls
21.22 [(*for preds in where_*) Rule.Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
21.23 crls = Rule.e_rls, errpats = [], nrls = norm_Rational_rls},
21.24 - "Script SimplifyScript (t_t::real) = " ^
21.25 + @{thm simplify.simps}
21.26 + (*"Script SimplifyScript (t_t::real) = " ^
21.27 " ((Try (Rewrite_Set ''discard_minus'' False) @@ " ^
21.28 " Try (Rewrite_Set ''rat_mult_poly'' False) @@ " ^
21.29 " Try (Rewrite_Set ''make_rat_poly_with_parentheses'' False) @@ " ^
21.30 @@ -928,7 +928,7 @@
21.31 " Try (Rewrite_Set ''cancel_p_rls'' False) @@ " ^
21.32 " Try (Rewrite_Set ''rat_reduce_1'' False)))) @@ " ^
21.33 " Try (Rewrite_Set ''discard_parentheses1'' False)) " ^
21.34 - " t_t)")]
21.35 + " t_t)"*))]
21.36 \<close>
21.37
21.38 end
22.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Tue May 28 16:52:30 2019 +0200
22.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed May 29 10:36:16 2019 +0200
22.3 @@ -494,10 +494,9 @@
22.4 [Specify.prep_met thy "met_rooteq" [] Celem.e_metID
22.5 (["RootEq"], [],
22.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
22.7 - crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script")]
22.8 + crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})]
22.9 \<close>
22.10 (*-- normalise 20.10.02 --*)
22.11 -(*ok
22.12 partial_function (tailrec) norm_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
22.13 where
22.14 "norm_sqrt_equ e_e v_v =
22.15 @@ -508,7 +507,6 @@
22.16 (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e
22.17 in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
22.18 [BOOL e_e, REAL v_v])"
22.19 -*)
22.20 setup \<open>KEStore_Elems.add_mets
22.21 [Specify.prep_met thy "met_rooteq_norm" [] Celem.e_metID
22.22 (["RootEq","norm_sq_root_equation"],
22.23 @@ -520,16 +518,17 @@
22.24 ("#Find" ,["solutions v_v'i'"])],
22.25 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[],
22.26 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
22.27 - "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
22.28 + @{thm norm_sqrt_equ.simps}
22.29 + (*"Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
22.30 "(let e_e = ((Repeat(Try (Rewrite ''makex1_x'' False))) @@ " ^
22.31 " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
22.32 " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^
22.33 " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
22.34 " (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e " ^
22.35 " in ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
22.36 - " [''no_met'']) [BOOL e_e, REAL v_v])))")]
22.37 + " [''no_met'']) [BOOL e_e, REAL v_v])))"*))]
22.38 \<close>
22.39 -(*ok
22.40 +
22.41 partial_function (tailrec) solve_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
22.42 where
22.43 "solve_sqrt_equ e_e v_v =
22.44 @@ -547,7 +546,6 @@
22.45 else SubProblem (''RootEq'',[''univariate'',''equation''],
22.46 [''no_met'']) [BOOL e_e, REAL v_v])
22.47 in Check_elementwise L_L {(v_v::real). Assumptions})"
22.48 -*)
22.49 setup \<open>KEStore_Elems.add_mets
22.50 [Specify.prep_met thy "met_rooteq_sq" [] Celem.e_metID
22.51 (["RootEq","solve_sq_root_equation"],
22.52 @@ -559,7 +557,8 @@
22.53 ("#Find" ,["solutions v_v'i'"])],
22.54 {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [],
22.55 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
22.56 - "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
22.57 + @{thm solve_sqrt_equ.simps}
22.58 + (*"Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
22.59 "(let e_e = " ^
22.60 " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''sqrt_isolate'' True)) @@ " ^
22.61 " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^
22.62 @@ -572,10 +571,9 @@
22.63 " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
22.64 " else (SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met'']) " ^
22.65 " [BOOL e_e, REAL v_v])) " ^
22.66 - "in Check_elementwise L_L {(v_v::real). Assumptions})")]
22.67 + "in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
22.68 \<close>
22.69 (*-- right 28.08.02 --*)
22.70 -(*ok
22.71 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list"
22.72 where "solve_sqrt_equ_right e_e v_v =
22.73 (let e_e =
22.74 @@ -590,7 +588,6 @@
22.75 [''no_met'']) [BOOL e_e, REAL v_v]
22.76 else SubProblem (''RootEq'',[''univariate'', ''equation''],
22.77 [''no_met'']) [BOOL e_e, REAL v_v])"
22.78 -*)
22.79 setup \<open>KEStore_Elems.add_mets
22.80 [Specify.prep_met thy "met_rooteq_sq_right" [] Celem.e_metID
22.81 (["RootEq","solve_right_sq_root_equation"],
22.82 @@ -599,7 +596,8 @@
22.83 ("#Find" ,["solutions v_v'i'"])],
22.84 {rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule.e_rls, prls = RootEq_prls, calc = [],
22.85 crls = RootEq_crls, errpats = [], nrls = norm_Poly},
22.86 - "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
22.87 + @{thm solve_sqrt_equ_right.simps}
22.88 + (*"Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
22.89 "(let e_e = " ^
22.90 " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''r_sqrt_isolate'' False)) @@ " ^
22.91 " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
22.92 @@ -610,10 +608,9 @@
22.93 " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
22.94 " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
22.95 " else ((SubProblem (''RootEq'',[''univariate'',equation''], " ^
22.96 - " [''no_met'']) [BOOL e_e, REAL v_v])))")]
22.97 + " [''no_met'']) [BOOL e_e, REAL v_v])))"*))]
22.98 \<close>
22.99 (*-- left 28.08.02 --*)
22.100 -(*ok
22.101 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list"
22.102 where
22.103 "solve_sqrt_equ_left e_e v_v =
22.104 @@ -629,7 +626,6 @@
22.105 [''no_met'']) [BOOL e_e, REAL v_v]
22.106 else SubProblem (''RootEq'',[''univariate'',''equation''],
22.107 [''no_met'']) [BOOL e_e, REAL v_v])"
22.108 -*)
22.109 setup \<open>KEStore_Elems.add_mets
22.110 [Specify.prep_met thy "met_rooteq_sq_left" [] Celem.e_metID
22.111 (["RootEq","solve_left_sq_root_equation"],
22.112 @@ -638,7 +634,8 @@
22.113 ("#Find" ,["solutions v_v'i'"])],
22.114 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[],
22.115 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
22.116 - "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
22.117 + @{thm solve_sqrt_equ_left.simps}
22.118 + (*"Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
22.119 "(let e_e = " ^
22.120 " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''l_sqrt_isolate'' False)) @@ " ^
22.121 " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
22.122 @@ -649,7 +646,7 @@
22.123 " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
22.124 " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
22.125 " else ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
22.126 - " [''no_met'']) [BOOL e_e, REAL v_v])))")]
22.127 + " [''no_met'']) [BOOL e_e, REAL v_v])))"*))]
22.128 \<close>
22.129 ML \<open>
22.130 \<close> ML \<open>
23.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Tue May 28 16:52:30 2019 +0200
23.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed May 29 10:36:16 2019 +0200
23.3 @@ -147,10 +147,9 @@
23.4 [Specify.prep_met @{theory LinEq} "met_rootrateq" [] Celem.e_metID
23.5 (["RootRatEq"], [],
23.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
23.7 - crls=Atools_erls, errpats = [], nrls = norm_Rational}, "empty_script")]
23.8 + crls=Atools_erls, errpats = [], nrls = norm_Rational}, @{thm refl})]
23.9 \<close>
23.10 (*-- left 20.10.02 --*)
23.11 -(*ok
23.12 partial_function (tailrec) solve_rootrat_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
23.13 where
23.14 "solve_rootrat_equ e_e v_v =
23.15 @@ -160,7 +159,6 @@
23.16 (Try (Rewrite_Set ''rooteq_simplify'' False)) @@
23.17 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'' False))) e_e
23.18 in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"
23.19 -*)
23.20 setup \<open>KEStore_Elems.add_mets
23.21 [Specify.prep_met thy "met_rootrateq_elim" [] Celem.e_metID
23.22 (["RootRatEq","elim_rootrat_equation"],
23.23 @@ -170,7 +168,8 @@
23.24 ("#Find" ,["solutions v_v'i'"])],
23.25 {rew_ord'="termlessI", rls'=RooRatEq_erls, srls=Rule.e_rls, prls=RootRatEq_prls, calc=[],
23.26 crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},
23.27 - "Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^
23.28 + @{thm solve_rootrat_equ.simps}
23.29 + (*"Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^
23.30 "(let e_e = ((Try (Rewrite_Set ''expand_rootbinoms'' False)) @@ " ^
23.31 " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
23.32 " (Try (Rewrite_Set ''make_rooteq'' False)) @@ " ^
23.33 @@ -178,6 +177,6 @@
23.34 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] " ^
23.35 " ''rootrat_solve'' False))) e_e " ^
23.36 " in (SubProblem (''RootEq'',[''univariate'',''equation''], " ^
23.37 - " [''no_met'']) [BOOL e_e, REAL v_v]))")]
23.38 + " [''no_met'']) [BOOL e_e, REAL v_v]))"*))]
23.39 \<close>
23.40 end
24.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Tue May 28 16:52:30 2019 +0200
24.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Wed May 29 10:36:16 2019 +0200
24.3 @@ -48,7 +48,7 @@
24.4 ("#Find" ,["normalform n_n"])],
24.5 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Rule.e_rls,
24.6 errpats = [], nrls = Rule.e_rls},
24.7 - "empty_script")]
24.8 + @{thm refl})]
24.9 \<close>
24.10
24.11 ML \<open>
25.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue May 28 16:52:30 2019 +0200
25.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed May 29 10:36:16 2019 +0200
25.3 @@ -865,9 +865,9 @@
25.4 [Specify.prep_met @{theory "Diff"} "met_test" [] Celem.e_metID
25.5 (["Test"], [],
25.6 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
25.7 - crls=Atools_erls, errpats = [], nrls = Rule.e_rls}, "empty_script")]
25.8 + crls=Atools_erls, errpats = [], nrls = Rule.e_rls}, @{thm refl})]
25.9 \<close>
25.10 -(*ok
25.11 +
25.12 partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"
25.13 where
25.14 "solve_linear e_e v_v =
25.15 @@ -876,7 +876,6 @@
25.16 (((Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' False) @@
25.17 (Rewrite_Set ''Test_simplify'' False))) e_e
25.18 in [e_e])"
25.19 -*)
25.20 setup \<open>KEStore_Elems.add_mets
25.21 [Specify.prep_met thy "met_test_solvelin" [] Celem.e_metID
25.22 (["Test","solve_linear"],
25.23 @@ -886,15 +885,16 @@
25.24 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls,
25.25 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
25.26 nrls = Test_simplify},
25.27 - "Script Solve_linear (e_e::bool) (v_v::real)= " ^
25.28 + @{thm solve_linear.simps}
25.29 + (*"Script Solve_linear (e_e::bool) (v_v::real)= " ^
25.30 "(let e_e = " ^
25.31 " Repeat " ^
25.32 " (((Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@ " ^
25.33 " (Rewrite_Set ''Test_simplify'' False))) e_e" ^
25.34 - " in [e_e::bool])")]
25.35 + " in [e_e::bool])"*))]
25.36 \<close>
25.37 subsection \<open>root equation\<close>
25.38 -(*ok
25.39 +
25.40 partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
25.41 where
25.42 "solve_root_equ e_e v_v =
25.43 @@ -910,7 +910,6 @@
25.44 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' False) @@
25.45 (Try (Rewrite_Set ''Test_simplify'' False))) e_e
25.46 in [e_e])"
25.47 -*)
25.48 setup \<open>KEStore_Elems.add_mets
25.49 [Specify.prep_met thy "met_test_sqrt" [] Celem.e_metID
25.50 (*root-equation, version for tests before 8.01.01*)
25.51 @@ -925,7 +924,8 @@
25.52 [Rule.Calc ("Test.contains'_root",eval_contains_root "")],
25.53 calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],
25.54 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
25.55 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
25.56 + @{thm solve_root_equ.simps}
25.57 + (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
25.58 "(let e_e = " ^
25.59 " ((While (contains_root e_e) Do" ^
25.60 " ((Rewrite ''square_equation_left'' True) @@" ^
25.61 @@ -938,7 +938,7 @@
25.62 " (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@" ^
25.63 " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
25.64 " e_e" ^
25.65 - " in [e_e::bool])")]
25.66 + " in [e_e::bool])"*))]
25.67 \<close>
25.68 (* UNUSED?
25.69 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
25.70 @@ -988,8 +988,7 @@
25.71 \<close>
25.72 *)
25.73
25.74 -(*ok
25.75 -partial_function (tailrec) solve_root_equation ::
25.76 +partial_function (tailrec) minisubpbl ::
25.77 "bool \<Rightarrow> real \<Rightarrow> bool list"
25.78 where "minisubpbl e_e v_v =
25.79 (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@
25.80 @@ -998,7 +997,6 @@
25.81 SubProblem (''TestX'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
25.82 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
25.83 in Check_elementwise L_L {(v_v::real). Assumptions})"
25.84 -*)
25.85 setup \<open>KEStore_Elems.add_mets
25.86 [Specify.prep_met thy "met_test_squ_sub" [] Celem.e_metID
25.87 (*tests subproblem fixed linear*)
25.88 @@ -1010,7 +1008,8 @@
25.89 prls = Rule.append_rls "prls_met_test_squ_sub" Rule.e_rls
25.90 [Rule.Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
25.91 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
25.92 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
25.93 + @{thm minisubpbl.simps}
25.94 + (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
25.95 " (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@ " ^
25.96 " (Try (Rewrite_Set ''Test_simplify'' False))) e_e; " ^
25.97 " (L_L::bool list) = " ^
25.98 @@ -1018,11 +1017,11 @@
25.99 " [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^
25.100 " [''Test'', ''solve_linear'']) " ^
25.101 " [BOOL e_e, REAL v_v]) " ^
25.102 - " in Check_elementwise L_L {(v_v::real). Assumptions}) ")]
25.103 + " in Check_elementwise L_L {(v_v::real). Assumptions}) "*))]
25.104 \<close>
25.105 -(*ok
25.106 +
25.107 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
25.108 - where "solve_root_equ e_e v_v =
25.109 + where "solve_root_equ2 e_e v_v =
25.110 (let e_e =
25.111 ((While (contains_root e_e) Do
25.112 ((Rewrite ''square_equation_left'' True) @@
25.113 @@ -1035,7 +1034,6 @@
25.114 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
25.115 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
25.116 in Check_elementwise L_L {(v_v::real). Assumptions}) "
25.117 -*)
25.118 setup \<open>KEStore_Elems.add_mets
25.119 [Specify.prep_met thy "met_test_eq1" [] Celem.e_metID
25.120 (*root-equation1:*)
25.121 @@ -1047,7 +1045,8 @@
25.122 [Rule.Calc ("Test.contains'_root",eval_contains_root"")], prls=Rule.e_rls, calc=[], crls=tval_rls,
25.123 errpats = [], nrls = Rule.e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),
25.124 ("square_equation_right","")]*)},
25.125 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
25.126 + @{thm solve_root_equ2.simps}
25.127 + (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
25.128 "(let e_e = " ^
25.129 " ((While (contains_root e_e) Do" ^
25.130 " ((Rewrite ''square_equation_left'' True) @@" ^
25.131 @@ -1060,12 +1059,12 @@
25.132 " e_e;" ^
25.133 " (L_L::bool list) = (SubProblem (''Test'',[''LINEAR'',''univariate'',''equation'',''test'']," ^
25.134 " [''Test'',''solve_linear'']) [BOOL e_e, REAL v_v])" ^
25.135 - " in Check_elementwise L_L {(v_v::real). Assumptions})")]
25.136 + " in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
25.137 \<close>
25.138 -(*ok
25.139 +
25.140 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
25.141 where
25.142 -"solve_root_equ e_e v_v =
25.143 +"solve_root_equ3 e_e v_v =
25.144 (let e_e =
25.145 ((While (contains_root e_e) Do
25.146 (((Rewrite ''square_equation_left'' True) Or
25.147 @@ -1079,7 +1078,6 @@
25.148 L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],
25.149 [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]
25.150 in Check_elementwise L_L {(v_v::real). Assumptions})"
25.151 -*)
25.152 setup \<open>KEStore_Elems.add_mets
25.153 [Specify.prep_met thy "met_test_squ2" [] Celem.e_metID
25.154 (*root-equation2*)
25.155 @@ -1091,7 +1089,8 @@
25.156 [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
25.157 prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,asm_rls=[],
25.158 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
25.159 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
25.160 + @{thm solve_root_equ3.simps}
25.161 + (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
25.162 "(let e_e = " ^
25.163 " ((While (contains_root e_e) Do" ^
25.164 " (((Rewrite ''square_equation_left'' True) Or " ^
25.165 @@ -1105,12 +1104,12 @@
25.166 " e_e;" ^
25.167 " (L_L::bool list) = (SubProblem (''Test'',[''plain_square'',''univariate'',''equation'',''test'']," ^
25.168 " [''Test'',''solve_plain_square'']) [BOOL e_e, REAL v_v])" ^
25.169 - " in Check_elementwise L_L {(v_v::real). Assumptions})")]
25.170 + " in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
25.171 \<close>
25.172 -(*ok
25.173 +
25.174 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
25.175 where
25.176 -"solve_root_equ e_e v_v =
25.177 +"solve_root_equ4 e_e v_v =
25.178 (let e_e =
25.179 ((While (contains_root e_e) Do
25.180 (((Rewrite ''square_equation_left'' True) Or
25.181 @@ -1124,7 +1123,6 @@
25.182 L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
25.183 [''no_met'']) [BOOL e_e, REAL v_v]
25.184 in Check_elementwise L_L {(v_v::real). Assumptions})"
25.185 -*)
25.186 setup \<open>KEStore_Elems.add_mets
25.187 [Specify.prep_met thy "met_test_squeq" [] Celem.e_metID
25.188 (*root-equation*)
25.189 @@ -1136,7 +1134,8 @@
25.190 [Rule.Calc ("Test.contains'_root",eval_contains_root"")],
25.191 prls=Rule.e_rls,calc=[], crls=tval_rls, errpats = [], nrls = Rule.e_rls (*,asm_rls=[],
25.192 asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
25.193 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
25.194 + @{thm solve_root_equ4.simps}
25.195 + (*"Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
25.196 "(let e_e = " ^
25.197 " ((While (contains_root e_e) Do" ^
25.198 " (((Rewrite ''square_equation_left'' True) Or" ^
25.199 @@ -1150,9 +1149,9 @@
25.200 " e_e;" ^
25.201 " (L_L::bool list) = (SubProblem (''Test'',[''univariate'',''equation'',''test'']," ^
25.202 " [''no_met'']) [BOOL e_e, REAL v_v])" ^
25.203 - " in Check_elementwise L_L {(v_v::real). Assumptions})")]
25.204 + " in Check_elementwise L_L {(v_v::real). Assumptions})"*))]
25.205 \<close>
25.206 -(*ok
25.207 +
25.208 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
25.209 where
25.210 "solve_plain_square e_e v_v =
25.211 @@ -1162,7 +1161,6 @@
25.212 (Rewrite ''square_equality'' True)) @@
25.213 (Try (Rewrite_Set ''tval_rls'' False))) e_e
25.214 in Or_to_List e_e)"
25.215 -*)
25.216 setup \<open>KEStore_Elems.add_mets
25.217 [Specify.prep_met thy "met_test_eq_plain" [] Celem.e_metID
25.218 (*solve_plain_square*)
25.219 @@ -1176,16 +1174,17 @@
25.220 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule.e_rls,
25.221 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,
25.222 asm_rls=[],asm_thm=[]*)},
25.223 - "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
25.224 + @{thm solve_plain_square.simps}
25.225 + (*"Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
25.226 " (let e_e = ((Try (Rewrite_Set ''isolate_bdv'' False)) @@ " ^
25.227 " (Try (Rewrite_Set ''Test_simplify'' False)) @@ " ^
25.228 " ((Rewrite ''square_equality_0'' False) Or " ^
25.229 " (Rewrite ''square_equality'' True)) @@ " ^
25.230 " (Try (Rewrite_Set ''tval_rls'' False))) e_e " ^
25.231 - " in ((Or_to_List e_e)::bool list))")]
25.232 + " in ((Or_to_List e_e)::bool list))"*))]
25.233 \<close>
25.234 subsection \<open>polynomial equation\<close>
25.235 -(*ok
25.236 +
25.237 partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
25.238 where
25.239 "norm_univariate_equ e_e v_v =
25.240 @@ -1193,7 +1192,6 @@
25.241 (Try (Rewrite_Set ''Test_simplify'' False))) e_e
25.242 in SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
25.243 [''no_met'']) [BOOL e_e, REAL v_v])"
25.244 -*)
25.245 setup \<open>KEStore_Elems.add_mets
25.246 [Specify.prep_met thy "met_test_norm_univ" [] Celem.e_metID
25.247 (["Test","norm_univar_equation"],
25.248 @@ -1202,21 +1200,21 @@
25.249 ("#Find" ,["solutions v_v'i'"])],
25.250 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule.e_rls,prls=Rule.e_rls, calc=[], crls=tval_rls,
25.251 errpats = [], nrls = Rule.e_rls},
25.252 - "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
25.253 + @{thm norm_univariate_equ.simps}
25.254 + (*"Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
25.255 " (let e_e = ((Try (Rewrite ''rnorm_equation_add'' False)) @@ " ^
25.256 " (Try (Rewrite_Set ''Test_simplify'' False))) e_e " ^
25.257 " in (SubProblem (''Test'',[''univariate'',''equation'',''test''], " ^
25.258 - " [''no_met'']) [BOOL e_e, REAL v_v]))")]
25.259 + " [''no_met'']) [BOOL e_e, REAL v_v]))"*))]
25.260 \<close>
25.261 subsection \<open>diophantine equation\<close>
25.262 -(*ok
25.263 +
25.264 partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"
25.265 where
25.266 "test_simplify t_t =
25.267 (Repeat
25.268 ((Try (Calculate ''PLUS'')) @@
25.269 (Try (Calculate ''TIMES''))) t_t)"
25.270 -*)
25.271 setup \<open>KEStore_Elems.add_mets
25.272 [Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID
25.273 (["Test","intsimp"],
25.274 @@ -1225,10 +1223,11 @@
25.275 ("#Find" ,["intTestFind s_s"])],
25.276 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [],
25.277 crls = tval_rls, errpats = [], nrls = Test_simplify},
25.278 - "Script STest_simplify (t_t::int) = " ^
25.279 + @{thm test_simplify.simps}
25.280 + (*"Script STest_simplify (t_t::int) = " ^
25.281 "(Repeat " ^
25.282 " ((Try (Calculate ''PLUS'')) @@ " ^
25.283 - " (Try (Calculate ''TIMES''))) t_t::int)")]
25.284 + " (Try (Calculate ''TIMES''))) t_t::int)"*))]
25.285 \<close>
25.286
25.287 end
26.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Tue May 28 16:52:30 2019 +0200
26.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Wed May 29 10:36:16 2019 +0200
26.3 @@ -80,14 +80,14 @@
26.4 pbl_t $ (pair_t $ HOLogic.mk_string domID $
26.5 list_comb (Syntax.const @{const_syntax Char}, map HOLogic.mk_string pblID));
26.6
26.7 -(* version for later switch to partial_function *)
26.8 -(* get identifier of partial_function *)
26.9 -fun get_fun_id (Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ fun_and_args $ _)) =
26.10 - fun_and_args |> strip_comb |> fst |> dest_Const
26.11 - | get_fun_id t = raise TERM ("get_fun_id", [t])
26.12 (* version introduced BEFORE switch to partial_function *)
26.13 (* get identifier of parsed script code *)
26.14 fun get_fun_id tm = tm |> strip_comb |> fst |> dest_Const
26.15 +(* version for later switch to partial_function *)
26.16 +(* get identifier of partial_function *)
26.17 +fun get_fun_id (Const ("HOL.eq", _) $ fun_and_args $ _) =
26.18 + fun_and_args |> strip_comb |> fst |> dest_Const
26.19 + | get_fun_id t = raise TERM ("get_fun_id", [t])
26.20
26.21 (* construct scr-env from scr(created automatically) and Rewrite_Set *)
26.22 fun one_scr_arg (Const _ $ arg $ _) = arg
27.1 --- a/test/Tools/isac/Knowledge/integrate.thy Tue May 28 16:52:30 2019 +0200
27.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Wed May 29 10:36:16 2019 +0200
27.3 @@ -8,17 +8,23 @@
27.4 "----------- method analog to rls 'integration' ---------";
27.5 "----------- method analog to rls 'integration' ---------";
27.6 \<close>
27.7 -
27.8 +partial_function (tailrec) integration_test :: "real \<Rightarrow> real \<Rightarrow> real"
27.9 + where
27.10 +"integration_test f_f v_v =
27.11 + (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'' False) @@
27.12 + (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'' False) @@
27.13 + (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))"
27.14 setup \<open>KEStore_Elems.add_mets
27.15 [Specify.prep_met @{theory "Isac"} "met_testint" [] Celem.e_metID
27.16 (["diff","integration","test"],
27.17 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])],
27.18 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
27.19 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
27.20 - "Script IntegrationScript (f_f::real) (v_v::real) = \
27.21 + @{thm integration_test.simps}
27.22 + (*"Script IntegrationScript (f_f::real) (v_v::real) = \
27.23 \ (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'' False) @@ \
27.24 \ (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'' False) @@ \
27.25 - \ (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))")]
27.26 + \ (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))"*))]
27.27 \<close>
27.28
27.29 end
28.1 --- a/test/Tools/isac/ProgLang/calculate.thy Tue May 28 16:52:30 2019 +0200
28.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Wed May 29 10:36:16 2019 +0200
28.3 @@ -25,6 +25,14 @@
28.4 ("#Find" ,["realTestFind s_s"])],
28.5 Rule.e_rls, NONE, [["Test","test_calculate"]])]\<close>
28.6
28.7 +partial_function (tailrec) calc_test :: "real \<Rightarrow> real"
28.8 + where
28.9 +"calc_test t_t =
28.10 + (Repeat
28.11 + ((Try (Repeat (Calculate ''PLUS''))) @@
28.12 + (Try (Repeat (Calculate ''TIMES''))) @@
28.13 + (Try (Repeat (Calculate ''DIVIDE''))) @@
28.14 + (Try (Repeat (Calculate ''POWER''))))) t_t"
28.15 setup \<open>KEStore_Elems.add_mets
28.16 [Specify.prep_met (@{theory "Test"}) "met_testcal" [] Celem.e_metID
28.17 (["Test","test_calculate"],
28.18 @@ -35,12 +43,13 @@
28.19 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")),
28.20 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
28.21 crls=tval_rls, errpats = [], nrls= Rule.e_rls (*, asm_rls=[],asm_thm=[]*)},
28.22 - "Script STest_simplify (t_t::real) = \
28.23 + @{thm calc_test.simps}
28.24 + (*"Script STest_simplify (t_t::real) = \
28.25 \(Repeat \
28.26 \ ((Try (Repeat (Calculate ''PLUS''))) @@ \
28.27 \ (Try (Repeat (Calculate ''TIMES''))) @@ \
28.28 \ (Try (Repeat (Calculate ''DIVIDE''))) @@ \
28.29 - \ (Try (Repeat (Calculate ''POWER''))))) t_t")]
28.30 + \ (Try (Repeat (Calculate ''POWER''))))) t_t"*))]
28.31 \<close>
28.32
28.33 end
29.1 --- a/test/Tools/isac/ProgLang/scrtools.thy Tue May 28 16:52:30 2019 +0200
29.2 +++ b/test/Tools/isac/ProgLang/scrtools.thy Wed May 29 10:36:16 2019 +0200
29.3 @@ -4,13 +4,30 @@
29.4 begin
29.5
29.6 subsection \<open> Compare with scrtools.sml: "--- test auto-generated script" \<close>
29.7 +
29.8 +partial_function (tailrec) stepwise_test :: "real => real"
29.9 + where
29.10 +"stepwise_test t_t =
29.11 + (Try (Rewrite_Set ''discard_minus'' False) @@
29.12 + Try (Rewrite_Set ''expand_poly'' False) @@
29.13 + Try (Repeat (Calculate ''TIMES'')) @@
29.14 + Try (Rewrite_Set ''order_mult_rls'' False) @@
29.15 + Try (Rewrite_Set ''simplify_power'' False) @@
29.16 + Try (Rewrite_Set ''calc_add_mult_pow'' False) @@
29.17 + Try (Rewrite_Set ''reduce_012_mult'' False) @@
29.18 + Try (Rewrite_Set ''order_add_rls'' False) @@
29.19 + Try (Rewrite_Set ''collect_numerals'' False) @@
29.20 + Try (Rewrite_Set ''reduce_012'' False) @@
29.21 + Try (Rewrite_Set ''discard_parentheses'' False))
29.22 + t_t"
29.23 setup \<open>KEStore_Elems.add_mets
29.24 [Specify.prep_met @{theory "Test"} "met_testinter" [] Celem.e_metID
29.25 (["Test","test_interSteps_1"],
29.26 [("#Given" ,["Term t_t"]), ("#Find" ,["normalform n_n"])],
29.27 {rew_ord' = "dummy_ord", rls' = tval_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
29.28 crls=tval_rls, errpats = [], nrls = Rule.e_rls},
29.29 - "Script Stepwise t_t = \
29.30 + @{thm stepwise_test.simps}
29.31 + (*"Script Stepwise t_t = \
29.32 \(Try (Rewrite_Set ''discard_minus'' False) @@ \
29.33 \ Try (Rewrite_Set ''expand_poly'' False) @@ \
29.34 \ Try (Repeat (Calculate ''TIMES'')) @@ \
29.35 @@ -22,7 +39,7 @@
29.36 \ Try (Rewrite_Set ''collect_numerals'' False) @@ \
29.37 \ Try (Rewrite_Set ''reduce_012'' False) @@ \
29.38 \ Try (Rewrite_Set ''discard_parentheses'' False)) \
29.39 - \ t_t"
29.40 + \ t_t"*)
29.41 (*presently this script cannot become equal in types to auto_script, because:
29.42 this t_t must be either 'real' or 'bool' #1#,
29.43 while the auto_script must be 'z and type-instantiated before usage*))]