1.1 --- a/doc-src/isac/jrocnik/Test_Z_Transform.thy	Mon Sep 05 14:43:38 2011 +0200
     1.2 +++ b/doc-src/isac/jrocnik/Test_Z_Transform.thy	Tue Sep 06 15:57:25 2011 +0200
     1.3 @@ -132,7 +132,8 @@
     1.4  term2str s_1;
     1.5  term2str s_2;
     1.6  *}
     1.7 -ML {*
     1.8 +
     1.9 +ML {* (*Solutions as Denominator --> Denominator1 = z - Zeropoint1, Denominator2 = z-Zeropoint2,...*)
    1.10  val xx = HOLogic.dest_eq s_1;
    1.11  val s_1' = HOLogic.mk_binop "Groups.minus_class.minus" xx;
    1.12  val xx = HOLogic.dest_eq s_2;
    1.13 @@ -144,17 +145,22 @@
    1.14  subsubsection {*build expression*}
    1.15  text {*in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)*}
    1.16  ML {*
    1.17 +(*The Main Denominator is the multiplikation of the partial fraction denominators*)
    1.18  val denominator' = HOLogic.mk_binop "Groups.times_class.times" (s_1', s_2') ;
    1.19 -val SOME n3 = parseNEW ctxt "3::real";
    1.20 -val expression' = HOLogic.mk_binop "Rings.inverse_class.divide" (n3, denominator');
    1.21 +val SOME numerator = parseNEW ctxt "3::real";
    1.22 +
    1.23 +val expression' = HOLogic.mk_binop "Rings.inverse_class.divide" (numerator, denominator');
    1.24  term2str expression';
    1.25  *}
    1.26  
    1.27 -subsubsection {*Ansatz*}
    1.28 +subsubsection {*Ansatz - create partial fractions out of our expression*}
    1.29 +
    1.30  axiomatization where
    1.31    ansatz2: "n / (a*b) = A/a + B/(b::real)" and
    1.32    multiply_eq2: "(n / (a*b) = A/a + B/b) = (a*b*(n  / (a*b)) = a*b*(A/a + B/b))"
    1.33 +
    1.34  ML {*
    1.35 +(*we use our ansatz2 to rewrite our expression and get an equilation with our expression on the left and the partial fractions of it on the right side*)
    1.36  val SOME (t1,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm ansatz2} expression';
    1.37  term2str t1;
    1.38  atomty t1;
    1.39 @@ -162,10 +168,12 @@
    1.40  term2str eq1;
    1.41  *}
    1.42  ML {*
    1.43 +(*eliminate the demoninators by multiplying the left and the right side with the main denominator*)
    1.44  val SOME (eq2,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm multiply_eq2} eq1;
    1.45  term2str eq2;
    1.46  *}
    1.47  ML {*
    1.48 +(*simplificatoin*)
    1.49  val SOME (eq3,_) = rewrite_set_ @{theory Isac} false norm_Rational eq2;
    1.50  term2str eq3; (*?A ?B not simplified*)
    1.51  *}
    1.52 @@ -189,6 +197,7 @@
    1.53  subsubsection {*get first koeffizient*}
    1.54  
    1.55  ML {*
    1.56 +(*substitude z with the first zeropoint to get A*)
    1.57  val SOME (eq4_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3'';
    1.58  term2str eq4_1;
    1.59  *}
    1.60 @@ -202,6 +211,7 @@
    1.61  
    1.62  *}
    1.63  ML {*
    1.64 +(*solve the simple linear equilation for A*)
    1.65  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.66  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.67  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.68 @@ -238,6 +248,7 @@
    1.69  subsubsection {*get second koeffizient*}
    1.70  
    1.71  ML {*
    1.72 +(*substitude z with the second zeropoint to get B*)
    1.73  val SOME (eq4b_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3'';
    1.74  term2str eq4_1;
    1.75  *}
    1.76 @@ -248,6 +259,8 @@
    1.77  *}
    1.78  
    1.79  ML {*
    1.80 +(*solve the simple linear equilation for B*)
    1.81 +
    1.82  val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"];
    1.83  val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
    1.84