1.1 --- a/src/Pure/thm.ML Sun Feb 19 10:04:04 2012 +0100
1.2 +++ b/src/Pure/thm.ML Mon Feb 20 18:18:03 2012 +0100
1.3 @@ -703,18 +703,9 @@
1.4 tpairs = [],
1.5 prop = prop})
1.6 end; (*WN ---^^^ *)
1.7 -(* WN120208 uncomment after test
1.8 fun assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop = (*WN*)
1.9 - Thm (deriv, {thy_ref=thy_ref, tags=tags, maxidx=maxidx,
1.10 - shyps=shyps, hyps=hyps, tpairs=tpairs, prop=prop});
1.11 -*)
1.12 -fun assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop = (*WN*)
1.13 - let
1.14 - val thm = Thm (deriv, {thy_ref=thy_ref, tags=tags, maxidx=maxidx,
1.15 - shyps=shyps, hyps=hyps, tpairs=tpairs, prop=prop})
1.16 - val _ = writeln ("###in assbl_thm: deriv= " ^ PolyML.makestring deriv);
1.17 - val _ = writeln ("###in assbl_thm: derivation_name= " ^ derivation_name thm)
1.18 - in thm end;
1.19 + Thm (deriv, {thy_ref=thy_ref, tags=tags, maxidx=maxidx,
1.20 + shyps=shyps, hyps=hyps, tpairs=tpairs, prop=prop});
1.21
1.22 (*Implication introduction
1.23 [A]
2.1 --- a/src/Tools/isac/Interpret/rewtools.sml Sun Feb 19 10:04:04 2012 +0100
2.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Mon Feb 20 18:18:03 2012 +0100
2.3 @@ -357,7 +357,7 @@
2.4 (*.lookup the missing theorems in some thy (of Isabelle).*)
2.5 fun make_isa missthms thy =
2.6 map (pair (theory2thyID thy))
2.7 - ((inter eq_thmI') missthms [] (*Global_Theory.all_thms_of thy*))
2.8 + ((inter eq_thmI) missthms [] (*Global_Theory.all_thms_of thy*))
2.9 : (thyID * (thmID * Thm.thm)) list;
2.10
2.11 (*.separate handling of sym_thms.*)
2.12 @@ -381,7 +381,7 @@
2.13 (* version with term instead of thm, for Theory.axioms_of in isa02*)
2.14 fun make_isa missthms thy =
2.15 map (pair (theory2thyID thy))
2.16 - ((inter eq_thmI) missthms (Theory.axioms_of thy))
2.17 + ((inter eq_thmI') missthms (Theory.axioms_of thy))
2.18 : (thyID * (thmID * term)) list;
2.19 (* separate handling of sym_thms *)
2.20 fun make_isab rlsthmsNOTisac isab_thys =
3.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Feb 19 10:04:04 2012 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Feb 20 18:18:03 2012 +0100
3.3 @@ -1,4 +1,4 @@
3.4 -(* Partial_Fractions
3.5 +(* Partial_Fractions
3.6 author: Jan Rocnik, isac team
3.7 Copyright (c) isac team 2011
3.8 Use is subject to license terms.
3.9 @@ -6,58 +6,40 @@
3.10 1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
3.11 10 20 30 40 50 60 70 80 90 100
3.12 *)
3.13 +header {* Partial Fraction Decomposition *}
3.14
3.15 -theory Partial_Fractions imports Rational begin
3.16
3.17 -ML {*Context.theory_name thy = "Isac"*}
3.18 +theory Partial_Fractions imports RootRatEq begin
3.19
3.20 ML{*
3.21 -val thy = @{theory};
3.22 -
3.23 +(*
3.24 signature PARTFRAC =
3.25 sig
3.26 val ansatz_rls : rls
3.27 val ansatz_rls_ : theory -> term -> (term * term list) option
3.28 end
3.29 +*)
3.30 *}
3.31
3.32 +subsection {* eval_ functions *}
3.33 consts
3.34 -
3.35 factors_from_solution :: "bool list => real"
3.36 drop_questionmarks :: "'a => 'a"
3.37
3.38 -subsection {*get the denominator out of a fraction*}
3.39 -text {*this functions have been stored in Rationals.thy and can be put into rule sets*}
3.40 -
3.41 -ML {*
3.42 -(*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*)
3.43 -fun eval_get_denominator (thmid:string) _
3.44 - (t as (Const("Rings.inverse_class.divide", _) $ num $ denom)) thy =
3.45 - SOME (mk_thmid thmid ""
3.46 - (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "",
3.47 - Trueprop $ (mk_equality (t, denom)))
3.48 - | eval_get_denominator _ _ _ _ = NONE;
3.49 -*}
3.50 -
3.51 -
3.52 -subsubsection {*get solutions out of list*}
3.53 -
3.54 -
3.55 +text {* these might be used for variants of fac_from_sol *}
3.56 ML {*
3.57 fun mk_minus_1 T = Free("-1", T); (*TODO DELETE WITH numbers_to_string*)
3.58 fun flip_sign t = (*TODO improve for use in factors_from_solution: -(-1) etc*)
3.59 let val minus_1 = t |> type_of |> mk_minus_1
3.60 in HOLogic.mk_binop "Groups.times_class.times" (minus_1, t) end;
3.61 +*}
3.62 +
3.63 +text {* from solutions (e.g. [z = 1, z = -2]) make linear factors (e.g. (z - 1)*(z - -2)) *}
3.64 +ML {*
3.65 fun fac_from_sol s =
3.66 let val (lhs, rhs) = HOLogic.dest_eq s
3.67 in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end;
3.68 -*}
3.69
3.70 -ML {*
3.71 -e_term
3.72 -*}
3.73 -
3.74 -ML {*
3.75 fun mk_prod prod [] =
3.76 if prod = e_term then error "mk_prod called with []" else prod
3.77 | mk_prod prod (t :: []) =
3.78 @@ -70,19 +52,13 @@
3.79 else
3.80 let val p = HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
3.81 in mk_prod p (t2 :: ts) end
3.82 -*}
3.83 -
3.84 -ML {*
3.85 -
3.86
3.87 fun factors_from_solution sol =
3.88 let val ts = HOLogic.dest_list sol
3.89 in mk_prod e_term (map fac_from_sol ts) end;
3.90
3.91 -*}
3.92 -
3.93 -ML {*
3.94 -(*("factors_from_solution", ("Partial_Fractions.factors_from_solution", eval_factors_from_solution ""))*)
3.95 +(*("factors_from_solution", ("Partial_Fractions.factors_from_solution",
3.96 + eval_factors_from_solution ""))*)
3.97 fun eval_factors_from_solution (thmid:string) _
3.98 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
3.99 ((let val prod = factors_from_solution sol
3.100 @@ -94,6 +70,7 @@
3.101 | eval_factors_from_solution _ _ _ _ = NONE;
3.102 *}
3.103
3.104 +text {* 'ansatz' introduces '?Vars' (questionable design); drop these again *}
3.105 ML {*
3.106 (*("drop_questionmarks", ("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks ""))*)
3.107 fun eval_drop_questionmarks (thmid:string) _
3.108 @@ -108,29 +85,32 @@
3.109 end
3.110 else NONE
3.111 | eval_drop_questionmarks _ _ _ _ = NONE;
3.112 +*}
3.113
3.114 +text {* store eval_ functions for calls from Scripts *}
3.115 +ML {*
3.116 calclist':= overwritel (!calclist',
3.117 [("drop_questionmarks", ("Partial_Fractions.drop'_questionmarks", eval_drop_questionmarks ""))
3.118 ]);
3.119 *}
3.120
3.121 -text {* this definition's scope is all Isac; so no equation etc with "A" would be possible:
3.122 -consts
3.123 - A :: "real"
3.124 - B :: "real"
3.125 -However, such a solution would be cleanest w.r.t logics
3.126 -*}
3.127 -
3.128 +subsection {* 'ansatz' for partial fractions *}
3.129 axiomatization where
3.130 ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
3.131 - equival_trans_2nd_order: "( n/(a*b) = A/a + B/b ) = ( n = A*b + B*a )"
3.132 + ansatz_3rd_order: "n / (a*b*c) = A/a + B/b + C/c" and
3.133 + ansatz_4th_order: "n / (a*b*c*d) = A/a + B/b + C/c + D/d" and
3.134 + equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)" and
3.135 + equival_trans_3rd_order: "(n/(a*b*c) = A/a + B/b + C/c) = (n = A*b*c + B*a*c + C*a*b)" and
3.136 + equival_trans_4th_order: "(n/(a*b*c*d) = A/a + B/b + C/c + D/d) =
3.137 + (n = A*b*c*d + B*a*c*d + C*a*b*d + D*a*b*c)"
3.138
3.139 ML {*
3.140 val ansatz_rls = prep_rls(
3.141 Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
3.142 erls = Erls, srls = Erls, calc = [],
3.143 rules =
3.144 - [Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order})
3.145 + [Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order}),
3.146 + Thm ("ansatz_3rd_order",num_str @{thm ansatz_3rd_order})
3.147 ],
3.148 scr = EmptyScr}:rls);
3.149 *}
3.150 @@ -140,14 +120,13 @@
3.151 Rls {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
3.152 erls = Erls, srls = Erls, calc = [],
3.153 rules =
3.154 - [Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
3.155 + [Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order}),
3.156 + Thm ("equival_trans_3rd_order",num_str @{thm equival_trans_3rd_order})
3.157 ],
3.158 scr = EmptyScr}:rls);
3.159 *}
3.160
3.161 -
3.162 text {*store the rule set for math engine*}
3.163 -
3.164 ML {*
3.165 ruleset' := overwritelthy @{theory} (!ruleset',
3.166 [("ansatz_rls", ansatz_rls),
3.167 @@ -155,19 +134,132 @@
3.168 ]);
3.169 *}
3.170
3.171 +subsection {* Specification *}
3.172
3.173 -text {*rule set for partial fractions*}
3.174 +consts
3.175 + decomposedFunction :: "real => una"
3.176 +
3.177 ML {*
3.178 -val partial_fraction =
3.179 - Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI),
3.180 - erls = Erls, srls = Erls, calc = [],
3.181 - rules = [
3.182 - Calc ("Rings.inverse_class.divide", eval_get_denominator "#")
3.183 - ],
3.184 - scr = EmptyScr};
3.185 +store_pbt
3.186 + (prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID
3.187 + (["partial_fraction", "rational", "simplification"],
3.188 + [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
3.189 + (* TODO: call this sub-problem with appropriate functionTerm:
3.190 + leading coefficient of the denominator is 1: to be checked here! and..
3.191 + ("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
3.192 + ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
3.193 + ("#Find" ,["decomposedFunction p_p"])
3.194 + ],
3.195 + append_rls "e_rls" e_rls [(*for preds in where_ TODO*)],
3.196 + NONE,
3.197 + [["simplification","of_rationals","to_partial_fraction"]]));
3.198 *}
3.199
3.200 +subsection {* Method *}
3.201 +consts
3.202 + PartFracScript :: "[real,real, real] => real"
3.203 + ("((Script PartFracScript (_ _ =))// (_))" 9)
3.204
3.205 +text {* rule set for functions called in the Script *}
3.206 +ML {*
3.207 + val srls = Rls {id="srls_partial_fraction",
3.208 + preconds = [],
3.209 + rew_ord = ("termlessI",termlessI),
3.210 + erls = append_rls "erls_in_srls_partial_fraction" e_rls
3.211 + [(*for asm in NTH_CONS ...*)
3.212 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
3.213 + (*2nd NTH_CONS pushes n+-1 into asms*)
3.214 + Calc("Groups.plus_class.plus", eval_binop "#add_")],
3.215 + srls = Erls, calc = [],
3.216 + rules = [
3.217 + Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
3.218 + Calc("Groups.plus_class.plus", eval_binop "#add_"),
3.219 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
3.220 + Calc("Tools.lhs", eval_lhs "eval_lhs_"),
3.221 + Calc("Tools.rhs", eval_rhs"eval_rhs_"),
3.222 + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
3.223 + Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
3.224 + Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
3.225 + Calc("Partial_Fractions.factors_from_solution",
3.226 + eval_factors_from_solution "#factors_from_solution"),
3.227 + Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
3.228 + scr = EmptyScr};
3.229 +*}
3.230 +ML {*
3.231 +eval_drop_questionmarks;
3.232 +*}
3.233 +ML {*
3.234 +val ctxt = ProofContext.init_global @{theory};
3.235 +val SOME t = parseNEW ctxt "eqr = drop_questionmarks eqr";
3.236 +*}
3.237 +ML {*
3.238 +parseNEW ctxt "decomposedFunction p_p";
3.239 +parseNEW ctxt "decomposedFunction";
3.240 +*}
3.241 +ML {*
3.242 +*}
3.243 +ML {* (* current version, error outcommented *)
3.244 +store_met
3.245 + (prep_met @{theory} "met_partial_fraction" [] e_metID
3.246 + (["simplification","of_rationals","to_partial_fraction"],
3.247 + [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
3.248 + (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
3.249 + ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
3.250 + ("#Find" ,["decomposedFunction p_p"])],
3.251 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls, prls = e_rls,
3.252 + crls = e_rls, nrls = e_rls},
3.253 + "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
3.254 + " (let f_f = Take f_f; " ^
3.255 + " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*)
3.256 + " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
3.257 + " (denom::real) = get_denominator f_f; " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*)
3.258 + " (equ::bool) = (denom = (0::real)); " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*)
3.259 + " (L_L::bool list) = (SubProblem (PolyEq', " ^
3.260 + " [abcFormula, degree_2, polynomial, univariate, equation], " ^
3.261 + " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = -1 / 4]*)
3.262 + " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*)
3.263 + " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - -1 / 4)) *)
3.264 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
3.265 + " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
3.266 + " eq = (Try (Rewrite_Set equival_trans False)) eq; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
3.267 + " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
3.268 + " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*)
3.269 + " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: -1 / 4*)
3.270 + " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
3.271 + " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
3.272 + " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*)
3.273 + " (sol_a::bool list) = " ^
3.274 + " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
3.275 + " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*)
3.276 + " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*)
3.277 + " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
3.278 + " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *)
3.279 + " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *)
3.280 + " (sol_b::bool list) = " ^
3.281 + " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
3.282 + " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*)
3.283 + " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*)
3.284 + " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)
3.285 + " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*)
3.286 + " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
3.287 + " in pbz)"
3.288 +));
3.289 +*}
3.290 +ML {*
3.291 +(*
3.292 + val fmz =
3.293 + ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
3.294 + "solveFor z", "functionTerm p_p"];
3.295 + val (dI',pI',mI') =
3.296 + ("Partial_Fractions",
3.297 + ["partial_fraction", "rational", "simplification"],
3.298 + ["simplification","of_rationals","to_partial_fraction"]);
3.299 + val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.300 +*)
3.301 +*}
3.302
3.303
3.304 +
3.305 +subsection {**}
3.306 +
3.307 end
3.308 \ No newline at end of file
4.1 --- a/src/Tools/isac/ProgLang/termC.sml Sun Feb 19 10:04:04 2012 +0100
4.2 +++ b/src/Tools/isac/ProgLang/termC.sml Mon Feb 20 18:18:03 2012 +0100
4.3 @@ -105,8 +105,24 @@
4.4 ^ ato body (n + 1)
4.5 | ato (f $ t) n = ato f n ^ ato t (n + 1)
4.6 in "\n*** " ^ ato t 0 ^ "\n***" end;
4.7 +fun term_detail2str_thy thy t =
4.8 + let fun ato (Const (a, T)) n =
4.9 + "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ string_of_typ_thy thy T ^ ")"
4.10 + | ato (Free (a, T)) n =
4.11 + "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ string_of_typ_thy thy T ^ ")"
4.12 + | ato (Var ((a, i), T)) n =
4.13 + "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), "^
4.14 + string_of_typ_thy thy T ^ ")"
4.15 + | ato (Bound i) n =
4.16 + "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
4.17 + | ato (Abs(a, T, body)) n =
4.18 + "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ string_of_typ_thy thy T ^ ",.."
4.19 + ^ ato body (n + 1)
4.20 + | ato (f $ t) n = ato f n ^ ato t (n + 1)
4.21 + in "\n*** " ^ ato t 0 ^ "\n***" end;
4.22 fun atomwy t = (writeln o term_detail2str) t;
4.23 fun atomty t = (tracing o term_detail2str) t;
4.24 +fun atomty_thy thy t = (tracing o (term_detail2str_thy thy)) t;
4.25
4.26 fun term_str thy (Const(s,_)) = s
4.27 | term_str thy (Free(s,_)) = s
5.1 --- a/src/Tools/isac/calcelems.sml Sun Feb 19 10:04:04 2012 +0100
5.2 +++ b/src/Tools/isac/calcelems.sml Mon Feb 20 18:18:03 2012 +0100
5.3 @@ -2,7 +2,7 @@
5.4 they are partially held in association lists as ref's for
5.5 switching language levels (meta-string, object-values).
5.6 in order to keep these ref's during re-evaluation of code,
5.7 - they are defined here at the beginning of the code.
5.8 + they are defined here the beginning of the code.
5.9 author: Walther Neuper
5.10 (c) isac-team 2003
5.11 *)
5.12 @@ -622,8 +622,10 @@
5.13 | termopt2str NONE = "NONE";
5.14
5.15 fun type2str typ =
5.16 - Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
5.17 + Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt' "Isac")) typ;
5.18 val string_of_typ = type2str;
5.19 +fun string_of_typ_thy thy typ =
5.20 + Print_Mode.setmp [] (Syntax.string_of_typ (thy2ctxt thy)) typ;
5.21
5.22 fun subst2str (s:subst) =
5.23 (strs2str o
6.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sun Feb 19 10:04:04 2012 +0100
6.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Feb 20 18:18:03 2012 +0100
6.3 @@ -1,6 +1,6 @@
6.4 (* Title: Build_Inverse_Z_Transform
6.5 Author: Jan Rocnik
6.6 - (c) copyright due to lincense terms.
6.7 + (c) copyright due to license terms.
6.8 12345678901234567890123456789012345678901234567890123456789012345678901234567890
6.9 10 20 30 40 50 60 70 80
6.10 *)
6.11 @@ -9,11 +9,11 @@
6.12
6.13 begin
6.14
6.15 -text{* We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont as an
6.16 - exercise. Because subsection~\ref{sec:stepcheck} requires
6.17 - \ttfamily Inverse\_Z\_Transform.thy \normalfont as a subtheory of \ttfamily
6.18 +text{* We stepwise build \ttfamily Inverse\_Z\_Transform.thy \normalfont.
6.19 + Because subsection~\ref{sec:stepcheck} requires
6.20 + \ttfamily Inverse\_Z\_Transform.thy \normalfont as a sub-theory of \ttfamily
6.21 Isac.thy\normalfont, the setup has been changed from \ttfamily theory
6.22 - Inverse\_Z\_Transform imports Isac \normalfont to the above one.
6.23 + Inverse\_Z\_Transform imports Isac \normalfont to the above one ('Build\_').
6.24 \par \noindent
6.25 \begin{center}
6.26 \textbf{ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS}
6.27 @@ -114,8 +114,8 @@
6.28
6.29 section{*Prepare Steps for CTP-based programming Language\label{sec:prepstep}*}
6.30 text{*
6.31 - \par \noindent The following sections are challanging with the CTP-based
6.32 - possibilities of building the programm. The goal is realized in
6.33 + \par \noindent The following sections are challenging with the CTP-based
6.34 + possibilities of building the program. The goal is realized in
6.35 Section~\ref{spec-meth} and Section~\ref{prog-steps}.
6.36 \par The reader is advised to jump between the subsequent subsections and
6.37 the respective steps in Section~\ref{prog-steps}. By comparing
6.38 @@ -125,7 +125,7 @@
6.39
6.40 subsection {*Prepare Expression\label{prep-expr}*}
6.41 text{*\noindent We try two different notations and check which of them
6.42 - isabelle can handle best.*}
6.43 + Isabelle can handle best.*}
6.44 ML {*
6.45 val ctxt = ProofContext.init_global @{theory Isac};
6.46 val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
6.47 @@ -137,7 +137,7 @@
6.48 *}
6.49
6.50 subsubsection {*Prepare Numerator and Denominator*}
6.51 -text{*\noindent The partial fraction decomposion is only possible ig we
6.52 +text{*\noindent The partial fraction decomposition is only possible if we
6.53 get the bound variable out of the numerator. Therefor we divide
6.54 the expression by $z$. Follow up the Calculation at
6.55 Section~\ref{sec:calc:ztrans} line number 02.*}
6.56 @@ -173,7 +173,7 @@
6.57 Tools.thy \normalfont contain general utilities: \ttfamily
6.58 eval\_argument\_in, eval\_rhs, eval\_lhs,\ldots \normalfont
6.59 \ttfamily grep -r "fun eva\_" * \normalfont shows all functions
6.60 - witch can be used in a script. Lookup this files how to build
6.61 + witch can be used in a script. Look-up this files how to build
6.62 and handle such functions.
6.63 \par The next section shows how to introduce such a function.
6.64 *}
6.65 @@ -192,8 +192,8 @@
6.66 we need a function which gets the denominator of a fraction.*}
6.67
6.68 subsubsection{*Get the Denominator and Numerator out of a Fraction*}
6.69 -text{*\noindent The selv written functions in e.g. \texttt{get\_denominator}
6.70 - should become a constant for the isabelle parser:*}
6.71 +text{*\noindent The self written functions in e.g. \texttt{get\_denominator}
6.72 + should become a constant for the Isabelle parser:*}
6.73
6.74 consts
6.75 get_denominator :: "real => real"
6.76 @@ -206,7 +206,7 @@
6.77 \par \noindent ATTENTION: From now on \ttfamily
6.78 Build\_Inverse\_Z\_Transform \normalfont mimics a build from scratch;
6.79 it only works due to re-building {\sisac} several times (indicated
6.80 - explicityl).
6.81 + explicitly).
6.82 *}
6.83
6.84 ML {*
6.85 @@ -228,8 +228,8 @@
6.86 see \ttfamily test/Knowledge/rational.sml\normalfont*}
6.87
6.88 text {*\noindent \ttfamily get\_numerator \normalfont should also become a
6.89 - constant for the isabelle parser, follow up the \texttt{const}
6.90 - decleration above.*}
6.91 + constant for the Isabelle parser, follow up the \texttt{const}
6.92 + declaration above.*}
6.93
6.94 ML {*
6.95 (*
6.96 @@ -247,7 +247,7 @@
6.97 | eval_get_numerator _ _ _ _ = NONE;
6.98 *}
6.99
6.100 -text {*\noindent We discovered severell problems by implementing the
6.101 +text {*\noindent We discovered several problems by implementing the
6.102 \ttfamily get\_numerator \normalfont function. Remember when
6.103 putting new functions to {\sisac}, put them in a thy file and rebuild
6.104 {\sisac}, also put them in the ruleset for the script!*}
6.105 @@ -255,7 +255,7 @@
6.106 subsection {*Solve Equation\label{sec:solveq}*}
6.107 text {*\noindent We have to find the zeros of the term, therefor we use our
6.108 \ttfamily get\_denominator \normalfont function from the step before
6.109 - and try to solve the second order eqeuation. (Follow up the Calculation
6.110 + and try to solve the second order equation. (Follow up the Calculation
6.111 in Section~\ref{sec:calc:ztrans} Subproblem 2) Note: This type of
6.112 equation is too general for the present program.
6.113 \par We know that this equation can be categorized as \em univariate
6.114 @@ -270,7 +270,7 @@
6.115 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
6.116 *}
6.117 text {*\noindent Check if the given equation matches the specification of this
6.118 - quation type.*}
6.119 + equation type.*}
6.120 ML {*
6.121 match_pbl fmz (get_pbt ["univariate","equation"]);
6.122 *}
6.123 @@ -293,7 +293,7 @@
6.124 *}
6.125
6.126 text {*\noindent Check if the (other) given equation matches the
6.127 - specification of this quation type.*}
6.128 + specification of this equation type.*}
6.129
6.130 ML {*
6.131 match_pbl fmz (get_pbt
6.132 @@ -330,7 +330,7 @@
6.133 *}
6.134
6.135 subsection {*Partial Fraction Decomposition\label{sec:pbz}*}
6.136 -text{*\noindent We go on with the decomposion of our expression. Follow up the
6.137 +text{*\noindent We go on with the decomposition of our expression. Follow up the
6.138 Calculation in Section~\ref{sec:calc:ztrans} Step~3 and later on
6.139 Subproblem~1.*}
6.140 subsubsection {*Solutions of the Equation*}
6.141 @@ -345,7 +345,7 @@
6.142 subsubsection {*Get Solutions out of a List*}
6.143 text {*\noindent In {\sisac}'s CTP-based programming language:
6.144 \ttfamily let\$ \$s\_1 = NTH 1\$ solutions; \$s\_2 = NTH 2...\$ \normalfont
6.145 - can be usefull.*}
6.146 + can be useful.*}
6.147
6.148 ML {*
6.149 val Const ("List.list.Cons", _) $ s_1 $ (Const ("List.list.Cons", _)
6.150 @@ -354,7 +354,7 @@
6.151 term2str s_2;
6.152 *}
6.153
6.154 -text{*\noindent The ansatz for the \em Partial Fraction Decomposion \normalfont
6.155 +text{*\noindent The ansatz for the \em Partial Fraction Decomposition \normalfont
6.156 requires to get the denominators of the partial fractions out of the
6.157 Solutions as:
6.158 \begin{itemize}
6.159 @@ -402,7 +402,7 @@
6.160 in mk_prod p (t2 :: ts) end
6.161 *}
6.162 (* ML {*
6.163 -probably keept these test in test/Tools/isac/...
6.164 +probably keep these test in test/Tools/isac/...
6.165 (*mk_prod e_term [];*)
6.166
6.167 val prod = mk_prod e_term [str2term "x + 123"];
6.168 @@ -431,7 +431,7 @@
6.169 text {*\noindent This function needs to be packed such that it can be evaluated
6.170 by the Lucas-Interpreter. Therefor we moved the function to the
6.171 corresponding \ttfamily Equation.thy \normalfont in our case
6.172 - \ttfamily PartialFractions.thy \normalfont. The neccessary steps
6.173 + \ttfamily PartialFractions.thy \normalfont. The necessary steps
6.174 are quit the same as we have done with \ttfamliy get\_denominator
6.175 \normalfont before.*}
6.176 ML {*
6.177 @@ -451,7 +451,7 @@
6.178 | eval_factors_from_solution _ _ _ _ = NONE;
6.179 *}
6.180
6.181 -text {*\noindent The tracing output of the calc tree after apllying this
6.182 +text {*\noindent The tracing output of the calc tree after applying this
6.183 function was \ttfamily 24 / factors\_from\_solution
6.184 [z = 1/ 2, z = -1 / 4])] \normalfont and the next step \ttfamily
6.185 val nxt = ("Empty\_Tac", ...): tac'\_)\normalfont. These observations
6.186 @@ -533,7 +533,7 @@
6.187 eval\_factors\_from\_solution
6.188 "Partial\_Fractions.factors\_from\_solution")\rbrack\rbrace\\
6.189
6.190 - \par \noindent \normalfont Here everthing is perfect. So the error can
6.191 + \par \noindent \normalfont Here everything is perfect. So the error can
6.192 only be in the SML code of \ttfamily eval\_factors\_from\_solution.
6.193 \normalfont We try to check the code with an existing test; since the
6.194 \emph{code} is in
6.195 @@ -544,7 +544,7 @@
6.196 \normalfont\end{center}
6.197 \par \noindent After updating the function \ttfamily
6.198 factors\_from\_solution \normalfont to a new version and putting a
6.199 - testcase to \ttfamily Partial\_Fractions.sml \normalfont we tried again
6.200 + test-case to \ttfamily Partial\_Fractions.sml \normalfont we tried again
6.201 to evaluate the term with the same result.
6.202 \par We opened the test \ttfamily Test\_Isac.thy \normalfont and saw that
6.203 everything is working fine. Also we checked that the test \ttfamily
6.204 @@ -568,7 +568,7 @@
6.205
6.206 ML {*
6.207 (*
6.208 - * The main denominator is the multiplikation of the denominators of
6.209 + * The main denominator is the multiplication of the denominators of
6.210 * all partial fractions.
6.211 *)
6.212
6.213 @@ -583,17 +583,17 @@
6.214
6.215 subsubsection {*Apply the Partial Fraction Decomposion Ansatz*}
6.216
6.217 -text{*\noindent We use the Ansatz of the Partial Fraction Decomposen for our
6.218 +text{*\noindent We use the Ansatz of the Partial Fraction Decomposition for our
6.219 expression 2nd order. Follow up the calculation in
6.220 Section~\ref{sec:calc:ztrans} Step~03.*}
6.221
6.222 ML {*Context.theory_name thy = "Isac"*}
6.223
6.224 -text{*\noindent We define two aximatizations, the first one is the main ansatz,
6.225 - the next one is just an eqivalent transformation of the resulting
6.226 +text{*\noindent We define two axiomatization, the first one is the main ansatz,
6.227 + the next one is just an equivalent transformation of the resulting
6.228 equation. Both axiomatizations were moved to \ttfamily
6.229 Partial\_Fractions.thy \normalfont and got their own rulesets. In later
6.230 - programms it is possible to use the rulesets and the machine will find
6.231 + programs it is possible to use the rulesets and the machine will find
6.232 the correct ansatz and equivalent transformation itself.*}
6.233
6.234 axiomatization where
6.235 @@ -601,7 +601,7 @@
6.236 equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)"
6.237
6.238 text{*\noindent We use our \ttfamily ansatz\_2nd\_order \normalfont to rewrite
6.239 - our expression and get an equilation with our expression on the left
6.240 + our expression and get an equation with our expression on the left
6.241 and the partial fractions of it on the right hand side.*}
6.242
6.243 ML {*
6.244 @@ -613,7 +613,7 @@
6.245 term2str eq1;
6.246 *}
6.247
6.248 -text{*\noindent Eliminate the demoninators by multiplying the left and the
6.249 +text{*\noindent Eliminate the denominators by multiplying the left and the
6.250 right hand side of the equation with the main denominator. This is an
6.251 simple equivalent transformation. Later on we use an own ruleset
6.252 defined in \ttfamily Partial\_Fractions.thy \normalfont for doing this.
6.253 @@ -637,9 +637,9 @@
6.254 *)
6.255 *}
6.256
6.257 -text{*\noindent In Example~\ref{eg:gap} of my thesis I'm describin a problem about
6.258 +text{*\noindent In Example~\ref{eg:gap} of my thesis I'm describing a problem about
6.259 simplifications. The problem that we would like to have only a specific degree
6.260 - of simplification occours right here, in the next step.*}
6.261 + of simplification occurs right here, in the next step.*}
6.262
6.263 ML {*
6.264 val SOME fract1 =
6.265 @@ -710,14 +710,14 @@
6.266 term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
6.267 *}
6.268
6.269 -subsubsection {*Get the First Koeffizient*}
6.270 +subsubsection {*Get the First Coefficient*}
6.271
6.272 -text{*\noindent Now it's up to get the two koeffizients A and B, which will be
6.273 - the numerators of our partial fractions. Continiue following up the
6.274 +text{*\noindent Now it's up to get the two coefficients A and B, which will be
6.275 + the numerators of our partial fractions. Continue following up the
6.276 Calculation in Section~\ref{sec:calc:ztrans} Subproblem~1.*}
6.277
6.278 -text{*\noindent To get the first koeffizient we substitude $z$ with the first
6.279 - zeropoint we determined in section~\ref{sec:solveq}.*}
6.280 +text{*\noindent To get the first coefficient we substitute $z$ with the first
6.281 + zero-point we determined in section~\ref{sec:solveq}.*}
6.282
6.283 ML {*
6.284 val SOME (eq4_1,_) =
6.285 @@ -730,7 +730,7 @@
6.286 val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
6.287 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
6.288 (*
6.289 - * Solve the simple linear equilation for A TODO:
6.290 + * Solve the simple linear equation for A TODO:
6.291 * Return eq, not list of eq's
6.292 *)
6.293 val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.294 @@ -789,15 +789,15 @@
6.295 f2str fa;
6.296 *}
6.297
6.298 -subsubsection {*Get Second Koeffizient*}
6.299 +subsubsection {*Get Second Coefficient*}
6.300
6.301 text{*\noindent With the use of \texttt{thy} we check which theories the
6.302 interpreter knows.*}
6.303
6.304 ML {*thy*}
6.305
6.306 -text{*\noindent To get the second koeffizient we substitude $z$ with the second
6.307 - zeropoint we determined in section~\ref{sec:solveq}.*}
6.308 +text{*\noindent To get the second coefficient we substitute $z$ with the second
6.309 + zero-point we determined in section~\ref{sec:solveq}.*}
6.310
6.311 ML {*
6.312 val SOME (eq4b_1,_) =
6.313 @@ -851,13 +851,13 @@
6.314
6.315 text{*\noindent Now everything we need for solving the problem has been
6.316 tested out. We now start by creating new nodes for our methods and
6.317 - further on our new programm in the interpreter.*}
6.318 + further on our new program in the interpreter.*}
6.319
6.320 subsection{*Define the Field Descriptions for the
6.321 Specification\label{sec:deffdes}*}
6.322
6.323 text{*\noindent We define the fields \em filterExpression \normalfont and
6.324 - \em stepResponse \normalfont both as quations, they represent the in- and
6.325 + \em stepResponse \normalfont both as equations, they represent the in- and
6.326 output of the program.*}
6.327
6.328 consts
6.329 @@ -867,7 +867,7 @@
6.330 subsection{*Define the Specification*}
6.331
6.332 text{*\noindent The next step is defining the specifications as nodes in the
6.333 - designated part. We have to create the hierachy node by node and start
6.334 + designated part. We have to create the hierarchy node by node and start
6.335 with \em SignalProcessing \normalfont and go on by creating the node
6.336 \em Z\_Transform\normalfont.*}
6.337
6.338 @@ -881,7 +881,7 @@
6.339 *}
6.340
6.341 text{*\noindent For the suddenly created node we have to define the input
6.342 - and output parameters. We already prepaired their definition in
6.343 + and output parameters. We already prepared their definition in
6.344 section~\ref{sec:deffdes}.*}
6.345
6.346 ML {*
6.347 @@ -971,8 +971,8 @@
6.348 show_mets();
6.349 *}
6.350
6.351 -text{*\noindent If yes we can get the method by steping backwards through
6.352 - the hierachy.*}
6.353 +text{*\noindent If yes we can get the method by stepping backwards through
6.354 + the hierarchy.*}
6.355
6.356 ML {*
6.357 get_met ["SignalProcessing","Z_Transform","inverse"];
6.358 @@ -980,8 +980,8 @@
6.359
6.360 section {*Program in CTP-based language \label{prog-steps}*}
6.361
6.362 -text{*\noindent We start stepwise expanding our programm. The script is a
6.363 - simple string containing severell manipulation instructions.
6.364 +text{*\noindent We start stepwise expanding our program. The script is a
6.365 + simple string containing several manipulation instructions.
6.366 \par The first script we try contains no instruction, we only test if
6.367 building scripts that way work.*}
6.368
6.369 @@ -1034,7 +1034,7 @@
6.370 " in X)";
6.371 *}
6.372
6.373 -text{*\noindent To solve the equation it is neccessary to drop the left hand
6.374 +text{*\noindent To solve the equation it is necessary to drop the left hand
6.375 side, now we only need the denominator of the right hand side. The first
6.376 equation solves the zeros of our expression.*}
6.377
6.378 @@ -1147,6 +1147,7 @@
6.379 "Script InverseZTransform (X_eq::bool) = "^
6.380 (*(1/z) instead of z ^^^ -1*)
6.381 "(let X = Take X_eq; "^
6.382 + (*ruleZY _only_ because ISAC *)
6.383 " X' = Rewrite ruleZY False X; "^
6.384 (*z * denominator*)
6.385 " (num_orig::real) = get_numerator (rhs X'); "^
6.386 @@ -1177,8 +1178,8 @@
6.387 " eq = drop_questionmarks eq; "^
6.388 " (z1::real) = (rhs (NTH 1 L_L)); "^
6.389 (*
6.390 - * prepare equliation for a - eq_a
6.391 - * therfor subsitude z with solution 1 - z1
6.392 + * prepare equation for a - eq_a
6.393 + * therefor substitute z with solution 1 - z1
6.394 *)
6.395 " (z2::real) = (rhs (NTH 2 L_L)); "^
6.396
6.397 @@ -1202,16 +1203,14 @@
6.398
6.399 " eqr = drop_questionmarks eqr; "^
6.400 " (pbz::real) = Take eqr; "^
6.401 - " pbz = ((Substitute [A=a]) pbz); "^
6.402 - " pbz = ((Substitute [B=b]) pbz); "^
6.403 + " pbz = ((Substitute [A=a, B=b]) pbz); "^
6.404
6.405 " pbz = Rewrite ruleYZ False pbz; "^
6.406 " pbz = drop_questionmarks pbz; "^
6.407
6.408 - " (iztrans::real) = Take pbz; "^
6.409 - " iztrans = (Rewrite_Set inverse_z False) iztrans; "^
6.410 - " iztrans = drop_questionmarks iztrans; "^
6.411 - " (n_eq::bool) = Take (X_n = iztrans) "^
6.412 + " (X_z::bool) = Take (X_z = pbz); "^
6.413 + " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
6.414 + " n_eq = drop_questionmarks n_eq "^
6.415 "in n_eq)"
6.416 )
6.417 );
6.418 @@ -1222,7 +1221,7 @@
6.419 text{*\noindent When the script is ready we can start checking our work.*}
6.420 subsubsection {*Check the Formalization*}
6.421 text{*\noindent First we want to check the formalization of the in and
6.422 - output of our programm.*}
6.423 + output of our program.*}
6.424
6.425 ML {*
6.426 val fmz =
6.427 @@ -1258,7 +1257,7 @@
6.428 *}
6.429
6.430 subsubsection {*Stepwise Check the Program\label{sec:stepcheck}*}
6.431 -text{*\noindent We start to stepwise execute our new programm in a calculation
6.432 +text{*\noindent We start to stepwise execute our new program in a calculation
6.433 tree and check if every node implements that what we have wanted.*}
6.434
6.435 ML {*
6.436 @@ -1296,7 +1295,7 @@
6.437 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.438 "Rewrite_Set norm_Rational";
6.439 " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
6.440 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.441 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; \normalfont
6.442 "SubProblem";
6.443 *}
6.444
6.445 @@ -1325,7 +1324,7 @@
6.446 step (program text !!!--->!!! STac (script tactic) with arguments
6.447 evaluated.)
6.448 \item Do we have the right Script \ldots difference in the
6.449 - argumentsdifference in the arguments\ldots\\
6.450 + arguments in the arguments\ldots\\
6.451 \ttfamily val Script s =\\
6.452 (#scr o get\_met) ["SignalProcessing","Z\_Transform","inverse"];\\
6.453 writeln (term2str s);\normalfont\\
6.454 @@ -1393,6 +1392,7 @@
6.455 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
6.456 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
6.457 selection of the appropriate type to isac as done in the final Script ;-))
6.458 +
6.459 \end{itemize}*}
6.460
6.461 ML {*
6.462 @@ -1403,7 +1403,7 @@
6.463 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.464 (*Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";*)
6.465 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.466 - (*Rewrite_Set_Inst ([(bdv, z)], d2_polyeq_abcFormula_simplify";*)
6.467 + (*Rewrite_Set_Inst ([(bdv, z)], d2_polyeq_abcFormula_simplifify";*)
6.468 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.469 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.470 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.471 @@ -1497,11 +1497,90 @@
6.472 text{*\noindent As a last step we check the tracing output of the last calc
6.473 tree instruction and compare it with the pre-calculated result.*}
6.474
6.475 -ML {*
6.476 - trace_script := true;
6.477 - val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.478 - show_pt pt;
6.479 +section {* Improve and Transfer into Knowledge *}
6.480 +text {*
6.481 + We want to improve the very long program \ttfamily InverseZTransform
6.482 + \normalfont by modularisation: partial fraction decomposition shall
6.483 + become a sub-problem.
6.484 +
6.485 + We could transfer all knowledge in \ttfamily Build\_Inverse\_Z\_Transform.thy
6.486 + \normalfont first to the \ttfamily Knowledge/Inverse\_Z\_Transform.thy
6.487 + \normalfont and then modularise. In this case TODO problems?!?
6.488 +
6.489 + We chose another way and go bottom up: first we build the sub-problem in
6.490 + \ttfamily Partial\_Fractions.thy \normalfont with the term
6.491 +
6.492 + $$\frac{3}{x\cdot(z - \fract{1}{4} + \frac{-1}{8}\cdot\fract{1}{z})}$$
6.493 +
6.494 + (how this still can be improved see \ttfamily Partial\_Fractions.thy \normalfont),
6.495 + and re-use all stuff prepared in \ttfamily Build\_Inverse\_Z\_Transform.thy:
6.496 + The knowledge will be transferred to \ttfamily src/../Partial\_Fractions.thy
6.497 + \normalfont and the respective tests to \ttfamily test/../sartial\_fractions.sml.
6.498 *}
6.499
6.500 +subsection {* Transfer to Partial\_Fractions.thy *}
6.501 +text {*
6.502 + First we transfer both, knowledge and tests into \ttfamily src/../Partial\_Fractions.thy
6.503 + \normalfont in order to immediately have the test results.
6.504 +
6.505 + We copy \ttfamily factors_from_solution, drop_questionmarks,
6.506 + ansatz_2nd_order \normalfont and rule-sets --- no problem.
6.507 + Also \ttfamily store_pbt .. "pbl_simp_rat_partfrac"
6.508 + \normalfont is easy.
6.509 +
6.510 + But then we copy from (1) \ttfamily Build\_Inverse\_Z\_Transform.thy
6.511 + store_met .. "met_SP_Ztrans_inv" to (2) \ttfamily Partial\_Fractions.thy
6.512 + store_met .. "met_SP_Ztrans_inv"
6.513 + \normalfont and cut out the respective part from the program. First we ensure that
6.514 + the string is correct. When we insert the string into (2)
6.515 + \ttfamily store_met .. "met_partial_fraction" \normalfont --- and get an error.
6.516 +*}
6.517 +
6.518 +subsubsection {* 'Programming' in \sisac}'s TP-based Language *}
6.519 +text {*
6.520 + At the present state writing programs in {\sisac} is particularly cumbersome.
6.521 + So we give hints how to cope with the many obstacles. Below we describe the
6.522 + steps we did in making (2) run.
6.523 +
6.524 + \begin{enumerate}
6.525 + \item We check if the \textbf{string} containing the program is correct.
6.526 + \item We check if the \textbf{types in the program} are correct.
6.527 + For this purpose we start start with the first and last lines
6.528 + \begin{verbatim}
6.529 + "PartFracScript (f_f::real) (v_v::real) = " ^
6.530 + " (let X = Take f_f; " ^
6.531 + " pbz = ((Substitute []) X) " ^
6.532 + " in pbz)"
6.533 + \end{verbatim}
6.534 + The last but one line helps not to bother with ';'.
6.535 + \item Then we add line by line. Already the first line causes the error.
6.536 + So we investigate it by
6.537 + \begin{verbatim}
6.538 + val ctxt = ProofContext.init_global @{theory};
6.539 + val SOME t = parseNEW ctxt "(num_orig::real) = get_numerator (rhs f_f)";
6.540 + \end{verbatim}
6.541 + and see a type clash: \ttfamily rhs \normalfont from (1) requires type
6.542 + \ttfamily bool \normalfont while (2) wants to have \ttfamily (f_f::real).
6.543 + \normalfont Of course, we don't need \ttfamily rhs \normalfont anymore.
6.544 + \item Type-checking can be very tedious. One might even inspect the
6.545 + parse-tree of the program with \sisac's specific debug tools:
6.546 + \begin{verbatim}
6.547 + val {scr = Script t,...} = get_met ["simplification","of_rationals","to_partial_fraction"];
6.548 + atomty_thy @{theory} t;
6.549 + \end{verbatim}
6.550 + \item We check if the \textbf{semantics of the program} by stepwise evaluation
6.551 + of the program. Evaluation is done by the Lucas-Interpreter, which works
6.552 + using the knowledge in theory Isac; so we have to re-build Isac. And the
6.553 + test are performed simplest in a file which is loaded with Isac.
6.554 + See \ttfamily tests/../partial_fractions.sml \normalfont.
6.555 + \end{enumerate}
6.556 +*}
6.557 +
6.558 +subsection {* Transfer to Inverse\_Z\_Transform.thy *}
6.559 +text {*
6.560 +
6.561 +*}
6.562 +
6.563 +
6.564 end
6.565
7.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Sun Feb 19 10:04:04 2012 +0100
7.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Mon Feb 20 18:18:03 2012 +0100
7.3 @@ -11,6 +11,7 @@
7.4 "----------- fun factors_from_solution ------------------";
7.5 "----------- Logic.unvarify_global ----------------------";
7.6 "----------- eval_drop_questionmarks --------------------";
7.7 +"----------- = me for met_partial_fraction --------------";
7.8 "--------------------------------------------------------";
7.9 "--------------------------------------------------------";
7.10 "--------------------------------------------------------";
7.11 @@ -74,7 +75,7 @@
7.12 val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
7.13 val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
7.14 if term2str t' =
7.15 - "factors_from_solution [z = 1 / 2, z = -1 / 4] =\n(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
7.16 + "factors_from_solution [z = 1 / 2, z = -1 / 4] = (z - 1 / 2) * (z - -1 / 4)"
7.17 then () else error "factors_from_solution broken";
7.18
7.19 "----------- Logic.unvarify_global ----------------------";
7.20 @@ -110,3 +111,111 @@
7.21 "\nA / (z + -1 * (1 / 2)) + B / (z + -1 * (-1 / 4))"
7.22 then () else error "eval_drop_questionmarks broken";
7.23
7.24 +"----------- = me for met_partial_fraction --------------";
7.25 +"----------- = me for met_partial_fraction --------------";
7.26 +"----------- = me for met_partial_fraction --------------";
7.27 + val fmz =
7.28 + ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
7.29 + "solveFor z", "decomposedFunction p_p"];
7.30 + val (dI',pI',mI') =
7.31 + ("Partial_Fractions",
7.32 + ["partial_fraction", "rational", "simplification"],
7.33 + ["simplification","of_rationals","to_partial_fraction"]);
7.34 + val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.35 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.36 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.37 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.38 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.39 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.40 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.41 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.42 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.43 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.44 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.45 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.46 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.47 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.48 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.49 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.50 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.51 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.52 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.53 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.54 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.55 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.56 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.57 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.58 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.59 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.60 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.61 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.62 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.63 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.64 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.65 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.66 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.67 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.68 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.69 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.70 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.71 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.72 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.73 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.74 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.75 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.76 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.77 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.78 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.79 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.80 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.81 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.82 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.83 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.84 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.85 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.86 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.87 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.88 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.89 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.90 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.91 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.92 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.93 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.94 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.95 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.96 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.97 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.98 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.99 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.100 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.101 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.102 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.103 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.104 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.105 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.106 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.107 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.108 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.109 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.110 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.111 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.112 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.113 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.114 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.115 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.116 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.117 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.118 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.119 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.120 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.121 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.122 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.123 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.124 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.125 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.126 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.127 +
7.128 +show_pt pt;
7.129 +if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then()
7.130 +else error "= me .. met_partial_fraction broken";
7.131 +
8.1 --- a/test/Tools/isac/Test_Some.thy Sun Feb 19 10:04:04 2012 +0100
8.2 +++ b/test/Tools/isac/Test_Some.thy Mon Feb 20 18:18:03 2012 +0100
8.3 @@ -1,116 +1,8 @@
8.4
8.5 theory Test_Some imports Isac begin
8.6
8.7 -use"../../../test/Tools/isac/Knowledge/isac.sml"
8.8 +use"../../../test/Tools/isac/Knowledge/partial_fractions.sml"
8.9
8.10 -ML {* (*================== redo thm.ML fun assbl_thm,
8.11 - build Isac hangs: revert --all AFTER SAVING -- FOR DIFF !!!*)
8.12 -*}
8.13 -ML {*
8.14 -*}
8.15 -ML {*
8.16 -*}
8.17 -ML {* (*==================
8.18 - use"../../../test/Tools/isac/Knowledge/isac.sml"*)
8.19 -! ruleset';
8.20 -*}
8.21 -ML {*
8.22 -isacrlsthms;
8.23 -*}
8.24 -ML {*
8.25 -@{thm NTH_CONS}
8.26 -(*"1 < ?n \<Longrightarrow> NTH ?n (?x # ?xs) = NTH (?n + - 1) ?xs"*)
8.27 -*}
8.28 -ML {*
8.29 -Thm.derivation_name @{thm NTH_CONS}
8.30 -*}
8.31 -ML {*
8.32 -val isacrlsthms = ! ruleset'
8.33 - |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
8.34 -*}
8.35 -ML {*
8.36 -val isacrlsthms = ! ruleset'
8.37 - |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
8.38 - |> flat
8.39 -*}
8.40 -ML {*
8.41 -val isacrlsthms = ! ruleset'
8.42 - |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
8.43 - |> flat
8.44 - |> map thm_of_thm
8.45 -*}
8.46 -ML {*
8.47 -val isacrlsthms = ! ruleset'
8.48 - |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
8.49 - |> flat
8.50 - |> map thm_of_thm
8.51 - |> gen_distinct Thm.eq_thm;
8.52 -*}
8.53 -ML {*
8.54 -nth 3 isacrlsthms;
8.55 -Thm.derivation_name (nth 3 isacrlsthms);
8.56 -*}
8.57 -ML {*
8.58 -@{thm NTH_CONS};
8.59 -Thm.derivation_name @{thm NTH_CONS};
8.60 -*}
8.61 -ML {*
8.62 -Thm.derivation_name (num_str @{thm NTH_CONS})
8.63 -*}
8.64 -ML {*(*-------------------termC.sml, thm.ML-----vvvvv*)
8.65 -*}
8.66 -ML {* (*termC.sml*)
8.67 -fun num_str thm =
8.68 - let val (deriv,
8.69 - {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps,
8.70 - hyps = hyps, tpairs = tpairs, prop = prop}) = rep_thm_G thm
8.71 - val prop' = numbers_to_string prop;
8.72 - val _ = writeln ("###in num_str: deriv= " ^ PolyML.makestring deriv);
8.73 - val thm = assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop'
8.74 - val _ = writeln ("###in num_str: derivation_name= " ^ Thm.derivation_name thm)
8.75 - in thm end;
8.76 -*}
8.77 -ML {*
8.78 -val thm = @{thm NTH_CONS};
8.79 -*}
8.80 -ML {*
8.81 -Thm.derivation_name (thm);
8.82 -*}
8.83 -ML {*
8.84 -Thm.derivation_name (num_str thm);
8.85 -*}
8.86 -ML {*
8.87 -Thm; (*fn: string * thm -> rule ... FROM ISAC !!!*)
8.88 -rep_thm_G; (*fn: thm -> Basic_Thm.deriv * {hyps: ...*)
8.89 -assbl_thm (*fn: Basic_Thm.deriv -> theory_ref ->...*)
8.90 -*}
8.91 -ML {*
8.92 -*}
8.93 -ML {*
8.94 -*}
8.95 -ML {*
8.96 -*}
8.97 -ML {*(*-------------------termC.sml, thm.ML-----^^^^^*)
8.98 -*}
8.99 -ML {*
8.100 -val isacrlsthms = ! ruleset'
8.101 - |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
8.102 - |> flat
8.103 - |> map thm_of_thm
8.104 - |> gen_distinct Thm.eq_thm
8.105 - |> map (` I)
8.106 -*}
8.107 -ML {*
8.108 -val isacrlsthms = ! ruleset'
8.109 - |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
8.110 - |> flat
8.111 - |> map thm_of_thm
8.112 - |> gen_distinct Thm.eq_thm
8.113 - |> map (` I)
8.114 - |> map (apfst Thm.derivation_name)
8.115 -*}
8.116 -ML {*
8.117 -*}
8.118 ML {*
8.119 *}
8.120 ML {*