intermed. Build_Inverse_Z_Transform:
got ambiguous parse trees from get_denominator in 2 theories ?!?
thus get_denominator shifted to Rational.thy
ATTENTION: "Rational.is'_ratpolyexp" has '
but get_denominator only works without '
1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Oct 06 16:15:29 2011 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Oct 06 17:43:00 2011 +0200
1.3 @@ -3450,13 +3450,12 @@
1.4 Trueprop $ (mk_equality (t, HOLogic.false_const)))
1.5 | eval_is_ratpolyexp _ _ _ _ = NONE;
1.6
1.7 -(*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*)
1.8 +(*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
1.9 fun eval_get_denominator (thmid:string) _
1.10 - (t as Const ("Rational.get'_denominator", _) $
1.11 + (t as Const ("Rational.get_denominator", _) $
1.12 (Const ("Rings.inverse_class.divide", _) $ num $
1.13 denom)) thy =
1.14 -
1.15 - SOME (mk_thmid thmid ""
1.16 + SOME (mk_thmid thmid ""
1.17 (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "",
1.18 Trueprop $ (mk_equality (t, denom)))
1.19
2.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Oct 06 16:15:29 2011 +0200
2.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Oct 06 17:43:00 2011 +0200
2.3 @@ -1,4 +1,4 @@
2.4 -(* Title: Test_Z_Transform
2.5 +(* Title: Build_Inverse_Z_Transform
2.6 Author: Jan Rocnik
2.7 (c) copyright due to lincense terms.
2.8 12345678901234567890123456789012345678901234567890123456789012345678901234567890
2.9 @@ -78,8 +78,7 @@
2.10 ML {*
2.11 val SOME (t, asm1) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
2.12 term2str t = "- ?u [- ?n - 1] + z / (z - \<alpha>) + 1"; (*- real *)
2.13 -term2str t;
2.14 -*}
2.15 +term2str t;*}
2.16 ML {*
2.17 val SOME (t, asm2) = rewrite_ thy ro er true (num_str @{thm rule4}) t;
2.18 term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1"; (*- real *)
2.19 @@ -155,9 +154,9 @@
2.20
2.21 ML {*
2.22
2.23 -(*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*)
2.24 +(*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
2.25 fun eval_get_denominator (thmid:string) _
2.26 - (t as Const ("Build_Inverse_Z_Transform.get_denominator", _) $
2.27 + (t as Const ("Rational.get_denominator", _) $
2.28 (Const ("Rings.inverse_class.divide", _) $ num $
2.29 denom)) thy =
2.30
2.31 @@ -169,24 +168,23 @@
2.32
2.33 *}
2.34
2.35 -
2.36 -
2.37 -
2.38 ML {*
2.39 -val t = @{term "get_denominator ((a +x)/b)"};
2.40 -val SOME (_, t') = eval_get_denominator "" 0 t @{theory};
2.41 +val thy = @{theory Isac};
2.42 +val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
2.43 +*}
2.44 +ML {*
2.45 +val Const ("Rational.get_denominator", _) $
2.46 + (Const ("Rings.inverse_class.divide", _) $ numerator $ denominator) = t;
2.47 +term2str numerator;
2.48 +term2str denominator
2.49 +*}
2.50 +ML {*
2.51 +val SOME (_, t') = eval_get_denominator "" 0 t thy;
2.52 term2str t';
2.53 *}
2.54
2.55
2.56 ML {*
2.57 -val t as Const ("Build_Inverse_Z_Transform.get_denominator", _) $
2.58 - (Const ("Rings.inverse_class.divide", _) $ num $
2.59 - denom) = t;
2.60 -*}
2.61 -
2.62 -
2.63 -ML {*
2.64 (*
2.65 if term2s t' = "(argument_in M_b x) = x" then ()
2.66 else error "atools.sml:(argument_in M_b x) = x ???";
2.67 @@ -598,7 +596,8 @@
2.68 Calc("Tools.lhs", eval_lhs"eval_lhs_"), (*<=== ONLY USED*)
2.69 Calc("Tools.rhs", eval_rhs"eval_rhs_"), (*<=== ONLY USED*)
2.70 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
2.71 - Calc("Rationals.get'_denominator", eval_get_denominator "Rationals.get'_denominator")
2.72 + Calc("Rational.get_denominator",
2.73 + eval_get_denominator "Rational.get_denominator")
2.74 ],
2.75 scr = EmptyScr};
2.76 *}
2.77 @@ -633,10 +632,16 @@
2.78 ));
2.79 *}
2.80 ML {*
2.81 -
2.82 val Script scr = (#scr o get_met) ["SignalProcessing", "Z_Transform", "inverse"];
2.83 atomty scr
2.84 -
2.85 +*}
2.86 +ML {*
2.87 +val t = term_of (the (parse thy "get_denominator (24 / (-1 + -2 * z + 8 * z ^^^ 2))"));
2.88 +atomty t;
2.89 +*}
2.90 +ML {*
2.91 +trace_rewrite := true;
2.92 +rewrite_set_ thy true srls t;
2.93 *}
2.94
2.95 subsection {*Check the Program*}
2.96 @@ -661,7 +666,7 @@
2.97
2.98 subsubsection {*Stepwise check the program*}
2.99 ML {*
2.100 -trace_script := false; print_depth 999;
2.101 +trace_script := true; print_depth 9;
2.102 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
2.103 "stepResponse (x[n::real]::bool)"];
2.104 val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"],
2.105 @@ -677,7 +682,19 @@
2.106 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
2.107 *}
2.108 ML {*
2.109 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Take 24 / (-1 + -2 * z + 8 * z ^^^ 2)";
2.110 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Subproblem";
2.111 +*}
2.112 +ML {*
2.113 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Model_Problem";
2.114 +*}
2.115 +ML {*
2.116 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";
2.117 +*}
2.118 +ML {*
2.119 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "solveFor z";
2.120 +*}
2.121 +ML {*
2.122 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Add_Find";
2.123 *}
2.124 ML {*
2.125 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Thu Oct 06 16:15:29 2011 +0200
3.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Oct 06 17:43:00 2011 +0200
3.3 @@ -12,11 +12,4 @@
3.4 "--------------------------------------------------------";
3.5
3.6
3.7 -"----------- get_denominator ----------------------------";
3.8 -"----------- get_denominator ----------------------------";
3.9 -"----------- get_denominator ----------------------------";
3.10 -val t = @{term "a/(b::real)"};
3.11 -val SOME (str, t') = eval_get_denominator "" 0 t @{theory Isac};
3.12 -if term2str t' = "a / b = b" then () else error "eval_get_denominator";
3.13
3.14 -
4.1 --- a/test/Tools/isac/Knowledge/rational.sml Thu Oct 06 16:15:29 2011 +0200
4.2 +++ b/test/Tools/isac/Knowledge/rational.sml Thu Oct 06 17:43:00 2011 +0200
4.3 @@ -48,6 +48,7 @@
4.4 "-------- investigate rulesets for cancel_p -------------";
4.5 "-------- investigate format of factout_ and factout_p_ -";
4.6 "-------- how to stepwise construct Scripts -------------";
4.7 +"----------- get_denominator ----------------------------";
4.8 "--------------------------------------------------------";
4.9 "--------------------------------------------------------";
4.10 "--------------------------------------------------------";
4.11 @@ -2078,3 +2079,13 @@
4.12 " Try (Rewrite_Set discard_parentheses False)) " ^
4.13 " t_t)"
4.14 );
4.15 +
4.16 +"----------- get_denominator ----------------------------";
4.17 +"----------- get_denominator ----------------------------";
4.18 +"----------- get_denominator ----------------------------";
4.19 +val thy = @{theory Isac};
4.20 +val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
4.21 +val SOME (_, t') = eval_get_denominator "" 0 t thy;
4.22 +if term2str t' = "get_denominator ((a + x) / b) = b" then ()
4.23 +else error "get_denominator ((a + x) / b) = b"
4.24 +