1.1 --- a/doc-src/isac/jrocnik/Test_Z_Transform.thy	Sun Jul 24 19:38:53 2011 +0200
     1.2 +++ b/doc-src/isac/jrocnik/Test_Z_Transform.thy	Mon Jul 25 17:43:07 2011 +0200
     1.3 @@ -31,6 +31,8 @@
     1.4  term2str @{term "1 < || z || ==> z / (z - 1) = -u [-n - 1]"};
     1.5  *}
     1.6  ML {*
     1.7 +(*alpha -->  "< / alpha >" *)
     1.8 +
     1.9  @{term "\<alpha> "};
    1.10  @{term "\<delta> "};
    1.11  @{term "\<phi> "};
    1.12 @@ -41,46 +43,52 @@
    1.13  subsection {*rules*}
    1.14  (*axiomatization "z / (z - 1) = -u [-n - 1]" Illegal variable name: "z / (z - 1) = -u [-n - 1]" *)
    1.15  (*definition     "z / (z - 1) = -u [-n - 1]" Bad head of lhs: existing constant "op /"*)
    1.16 -axioms 
    1.17 -  rule1: "\<forall>x. \<delta>[n] = 1"
    1.18 -  rule3: "1 < || z || ==> z / (z - 1) = -u [-n - 1]"
    1.19 -(*rule4: "|| \<alpha> || < || z || ==> z / (z - \<alpha>) = \<alpha>^n * [n]" 
    1.20 -                            Type unification failed: Clash of types "_ list" and "real"*)
    1.21 -  rule4: "|| \<alpha> || < || z || ==> z / (z - \<alpha>) = \<alpha> * u [n]"
    1.22 +axiomatization where 
    1.23 +  rule1: "1 = \<delta>[n]" and
    1.24 +  rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
    1.25 +  rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and 
    1.26 +  rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^n * u [n]" and
    1.27 +  rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^n) * u [-n - 1]" and
    1.28 +  rule6: "|| z || > 1 ==> z/(z - 1)^2 = n * u [n]"
    1.29  ML {*
    1.30  @{thm rule1};
    1.31 +@{thm rule2};
    1.32  @{thm rule3};
    1.33  @{thm rule4};
    1.34  *}
    1.35  
    1.36 +
    1.37 +
    1.38 +
    1.39  subsection {*apply rules*}
    1.40 +
    1.41 +ML {*
    1.42 +val inverse_Z = append_rls "inverse_Z" e_rls
    1.43 +  [ Thm ("rule1",num_str @{thm rule3}), 
    1.44 +    Thm ("rule3",num_str @{thm rule4}),
    1.45 +    Thm ("rule4",num_str @{thm rule1})
    1.46 +  ];
    1.47 +*}
    1.48 +
    1.49  ML {*
    1.50  val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
    1.51  *}
    1.52  ML {*
    1.53 -val t = @{term "z / (z - 1) = -u [-n - 1]"};
    1.54 +val t = str2term "1 + z / (z - 1) = -u [-n - 1]";
    1.55 +val SOME (t', _) = rewrite_set_ thy true inverse_Z t;
    1.56 +term2str t';
    1.57  *}
    1.58 +
    1.59  ML {*
    1.60 -print_depth 999; Pattern.match thy;  print_depth 999
    1.61 +val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
    1.62 +val t = str2term "z / (z - 1) = -u [-n - 1]";
    1.63 +val SOME (t, _) = rewrite_ thy ro er true (num_str @{thm rule3}) t;
    1.64 +term2str t="";
    1.65  *}
    1.66 -ML {*
    1.67 -*}
    1.68 -ML {*
    1.69 -rewrite_ thy ro er true @{thm rule3} t
    1.70 -*}
    1.71 +
    1.72  ML {*
    1.73  
    1.74  *}
    1.75 -ML {*
    1.76 -@{term "LENGTH"};
    1.77 -val t = str2term "LENGTH [x+y=1,y=2] = 2";
    1.78 -
    1.79 -*}
    1.80 -ML {*
    1.81 -*}
    1.82 -ML {*
    1.83 -@{term "1"};
    1.84 -*}
    1.85  
    1.86  end
    1.87  

     2.1 --- a/doc-src/isac/jrocnik/present-1.tex	Sun Jul 24 19:38:53 2011 +0200
     2.2 +++ b/doc-src/isac/jrocnik/present-1.tex	Mon Jul 25 17:43:07 2011 +0200
     2.3 @@ -77,7 +77,7 @@
     2.4  
     2.5  \begin{itemize}
     2.6  
     2.7 -\item What knowledge is already mechanised in \emph{isabelle}?
     2.8 +\item What knowledge is already mechanised in \emph{Isabelle}?
     2.9  \item How can missing theorems and definitions be mechanised?
    2.10  \item What is the effort for such mechanisation?
    2.11  \item How do calculations look like, by using mechanised knowledge?
    2.12 @@ -173,7 +173,7 @@
    2.13  \begin{itemize}
    2.14  
    2.15  \item Standard integrals can be solved with tables
    2.16 -\item No real integration (yet avaiible)
    2.17 +\item No real integration (yet avaible)
    2.18  \item Math \emph{tricks} difficult to implement
    2.19  
    2.20  
    2.21 @@ -185,13 +185,14 @@
    2.22  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2.23  
    2.24  \section[LTI Systems]{LTI systems}
    2.25 -\subsection[Convolution]{Convolution}
    2.26 +\subsection[Convolution]{Convolution (Faltung)}
    2.27  
    2.28  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2.29  %%												LTI INTRO				                       %%
    2.30  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2.31  
    2.32  \begin{frame}\frametitle{Convolution: Introduction}
    2.33 +TODO!!!
    2.34  \begin{itemize}
    2.35  \item Calculation\ldots
    2.36  \item Visualisation\ldots
    2.37 @@ -218,7 +219,7 @@
    2.38  The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$.
    2.39  
    2.40  \hrulefill
    2.41 -
    2.42 +???
    2.43  \begin{tabbing}
    2.44  1\=postcond \=: \= \= $\;\;\;\;$\=\kill
    2.45  \>given    \>:\>  Signals h1[n], h2[n] \\
    2.46 @@ -263,7 +264,7 @@
    2.47  \begin{itemize}
    2.48  
    2.49  \item Standard example
    2.50 -\item Straight foreward
    2.51 +\item Straight forward
    2.52  \item Challenge are sum limits
    2.53  
    2.54  \end{itemize}
    2.55 @@ -363,7 +364,7 @@
    2.56  %-----------------------------------------------------------------%
    2.57  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2.58  
    2.59 -\section[Closing]{Closing}
    2.60 +\section[Conclusions]{Conclusions}
    2.61  
    2.62  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2.63  %--------------------------CONCLUSION-----------------------------%