1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-isac/CTP-userinterfaces.bib	Tue Sep 17 09:50:52 2013 +0200
     1.3 @@ -0,0 +1,161 @@
     1.4 +@inproceedings{Aspinall:2007:FIP:1420412.1420429,
     1.5 + author = {Aspinall, David and L\"{u}th, Christoph and Winterstein, Daniel},
     1.6 + title = {A Framework for Interactive Proof},
     1.7 + booktitle = {Proceedings of the 14th symposium on Towards Mechanized Mathematical Assistants: 6th International Conference},
     1.8 + series = {Calculemus '07 / MKM '07},
     1.9 + year = {2007},
    1.10 + isbn = {978-3-540-73083-5},
    1.11 + location = {Hagenberg, Austria},
    1.12 + pages = {161--175},
    1.13 + numpages = {15},
    1.14 + url = {http://dx.doi.org/10.1007/978-3-540-73086-6_15},
    1.15 + doi = {http://dx.doi.org/10.1007/978-3-540-73086-6_15},
    1.16 + acmid = {1420429},
    1.17 + publisher = {Springer-Verlag},
    1.18 + address = {Berlin, Heidelberg},
    1.19 +}
    1.20 +
    1.21 +@Book{armstrong:erlang96,
    1.22 +  author = 	 {Armstrong, Joe and others},
    1.23 +  title = 	 {Concurrent Programming in Erlang},
    1.24 +  publisher = {Prentice Hall},
    1.25 +  year = 	 {1996}
    1.26 +}
    1.27 +
    1.28 +@TechReport{odersky:scala06,
    1.29 +  author = 	 {Odersky, Martin and others},
    1.30 +  title = 	 {An Overview of the Scala Programming Language},
    1.31 +  institution =  {\'Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL)},
    1.32 +  year = 	 {2006},
    1.33 +  type = 	 {Technical Report LAMP-REPORT-2006-001},
    1.34 +  address = 	 {1015 Lausanne, Switzerland},
    1.35 +  note = 	 {Second Edition},
    1.36 +  annote = 	 {http://www.scala-lang.org/sites/default/files/linuxsoft_archives/docu/files/ScalaOverview.pdf}
    1.37 +}
    1.38 +
    1.39 +@article{Haller:2009:SAU:1496391.1496422,
    1.40 + author = {Haller, Philipp and Odersky, Martin},
    1.41 + title = {Scala Actors: Unifying thread-based and event-based programming},
    1.42 + journal = {Theor. Comput. Sci.},
    1.43 + volume = {410},
    1.44 + issue = {2-3},
    1.45 + month = {February},
    1.46 + year = {2009},
    1.47 + issn = {0304-3975},
    1.48 + pages = {202--220},
    1.49 + numpages = {19},
    1.50 + url = {http://portal.acm.org/citation.cfm?id=1496391.1496422},
    1.51 + doi = {10.1016/j.tcs.2008.09.019},
    1.52 + acmid = {1496422},
    1.53 + publisher = {Elsevier Science Publishers Ltd.},
    1.54 + address = {Essex, UK},
    1.55 + keywords = {Actors, Concurrent programming, Events, Threads},
    1.56 +} 
    1.57 +
    1.58 +@InProceedings{scala:jmlc06,
    1.59 +  author =       {Philipp Haller and Martin Odersky},
    1.60 +  title =        {Event-Based Programming without Inversion of Control},
    1.61 +  booktitle =    {Proc. Joint Modular Languages Conference},
    1.62 +  year =         2006,
    1.63 +  series =       {Springer LNCS}
    1.64 +}
    1.65 +
    1.66 +
    1.67 +@InProceedings{makarius:isa-scala-jedit,
    1.68 +  author = 	 {Makarius Wenzel},
    1.69 +  title = 	 {Asyncronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}},
    1.70 +  booktitle = {User Interfaces for Theorem Provers (UITP 2010)},
    1.71 +  year = 	 {2010},
    1.72 +  editor = 	 {C. Sacerdoti Coen and D. Aspinall},
    1.73 +  address = 	 {Edinburgh, Scotland},
    1.74 +  month = 	 {July},
    1.75 +  organization = {FLOC 2010 Satellite Workshop},
    1.76 +  note = 	 {http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf}
    1.77 +}
    1.78 +
    1.79 +@Book{db:dom-eng,
    1.80 +  author = 	 {Bj{\o}rner, Dines},
    1.81 +  title = 	 {Domain Engineering. Technology Management, Research and Engineering},
    1.82 +  publisher = 	 {JAIST Press},
    1.83 +  year = 	 {2009},
    1.84 +  month = 	 {Feb},
    1.85 +  series = 	 {COE Research Monograph Series},
    1.86 +  volume = 	 {4},
    1.87 +  address = 	 {Nomi, Japan}
    1.88 +}
    1.89 +
    1.90 +@inproceedings{Haftmann-Nipkow:2010:code,
    1.91 +  author =      {Florian Haftmann and Tobias Nipkow},
    1.92 +  title =       {Code Generation via Higher-Order Rewrite Systems},
    1.93 +  booktitle =   {Functional and Logic Programming, 10th International
    1.94 +Symposium: {FLOPS} 2010},
    1.95 +  year =        {2010},
    1.96 +  publisher =   {Springer},
    1.97 +  series =      {Lecture Notes in Computer Science},
    1.98 +  volume =      {6009}
    1.99 +}
   1.100 +
   1.101 +@Manual{coq1999,
   1.102 +  title = 	 {The Coq Proof Assistant},
   1.103 +  author = 	 {Barras, B. and others},
   1.104 +  organization = {INRIA-Rocquencourt - CNRS-ENS Lyon},
   1.105 +  month = 	 {July},
   1.106 +  year = 	 {1999},
   1.107 +  pnote={},status={cited},source={mkm01.caprotti},location={}  
   1.108 +}
   1.109 +
   1.110 +@Book{meta-ML,
   1.111 +  author = 	 {Gordon,M. and Milner,R.  and Wadsworth,C. P.},
   1.112 +  title = 	 {Edinburgh LCF: A Mechanised Logic of Computation},
   1.113 +  publisher = 	 { Springer-Verlag},
   1.114 +  year = 	 {1979},
   1.115 +  volume = 	 {78},
   1.116 +  series = 	 {Lecture Notes in Computer Science}
   1.117 +}
   1.118 + 
   1.119 +@book{Paulson:Isa94,
   1.120 +        title={Isabelle: a generic theorem prover}, 
   1.121 +        author={Paulson, Lawrence C. }, publisher={Springer-Verlag},year={1994}, 
   1.122 +	volume={828},series={Lecture Notes in Computer Science},address={},edition={},month={}, 
   1.123 +	note={With contributions by Topias Nipkow},
   1.124 +        status={},source={},location={-} 
   1.125 +        }  
   1.126 +
   1.127 +@Book{pl:milner97,
   1.128 +  author = 	 {Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
   1.129 +  title = 	 {The Definition of Standard ML (Revised)},
   1.130 +  publisher = 	 {The MIT Press},
   1.131 +  year = 	 1997,
   1.132 +  address =	 {Cambridge, London},
   1.133 +  annote =	 {97bok375}
   1.134 +}
   1.135 +
   1.136 +@Article{back-grundy-wright-98,
   1.137 +  author = 	 {Back, Ralph and Grundy, Jim and von Wright, Joakim},
   1.138 +  title = 	 {Structured Calculational Proof},
   1.139 +  journal = 	 {Formal Aspects of Computing},
   1.140 +  year = 	 {1998},
   1.141 +  number = 	 {9},
   1.142 +  pages = 	 {469-483}
   1.143 +}
   1.144 +
   1.145 +@Manual{isar-impl,
   1.146 +  title = 	 {The {Isabelle/Isar} Implementation},
   1.147 +  author = 	 {Makarius Wenzel},
   1.148 +  month = 	 {April 19},
   1.149 +  year = 	 {2009},
   1.150 +  note = 	 {With contributions by Florian Haftmann and Larry Paulson}
   1.151 +}
   1.152 +
   1.153 +@InProceedings{wenzel:isar,
   1.154 +  author = 	 {Wenzel, Markus},
   1.155 +  title = 	 {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},
   1.156 +  booktitle = 	 {Theorem Proving in Higher Order Logics},
   1.157 +  year = 	 {1999},
   1.158 +  editor = 	 {G. Dowek, A. Hirschowitz, C. Paulin, L. Thery},
   1.159 +  series = 	 {LNCS 1690},
   1.160 +  organization = {12th International Conference TPHOLs'99},
   1.161 +  publisher = {Springer}
   1.162 +}
   1.163 +
   1.164 +

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-isac/CTP-userinterfaces.tex	Tue Sep 17 09:50:52 2013 +0200
     2.3 @@ -0,0 +1,445 @@
     2.4 +\documentclass{article}
     2.5 +\usepackage{a4}
     2.6 +\usepackage{times}
     2.7 +\usepackage{latexsym}
     2.8 +\bibliographystyle{alpha}
     2.9 +\usepackage{graphicx}
    2.10 +
    2.11 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    2.12 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
    2.13 +\def\Problem{ {\tt Problem }}
    2.14 +
    2.15 +\title{Userinterfaces for Computer Theorem Provers.\\
    2.16 +	Contributions to Isabelle
    2.17 +}
    2.18 +
    2.19 +\author{G. Schafhauser, A. Schulhofer, M. Steger\\
    2.20 +Knowledge Management Institute (KMI)\\
    2.21 +TU Graz}
    2.22 +
    2.23 +\begin{document}
    2.24 +\maketitle
    2.25 +\abstract{
    2.26 +This paper accompanies a pre-study on a sub-project planned within the \sisac-project. The goal of this sub-project is to extend the userinterface of the theorem prover Isabelle such, that Structured Derivations according to R.J.Back are interactively processed. The sub-project is one step towards using the upcoming Isabelle/Isar/Scala layer for \sisac.
    2.27 +
    2.28 +The paper comprises three parts: (1) Ample space is given to background information about the state of the art in user interfaces for theorem provers and about the upcoming requirements for future developments. (2) focuses the strategy of Isabelle and decisions in order to cope with future requirements. (3) provides a protocol of preparatory work for the sub-project.
    2.29 +
    2.30 +By the way, this paper shall serve as an entry point for students interested in joining the the work propared.}
    2.31 +
    2.32 +\section{Introduction}\label{intro}
    2.33 +Computer Theorem Provers (CTPs \footnote{The term CTP is used to address two different things in this paper: (1) the academic discipline comprising respective theories as well as (2) the products developed within this discipline, the provers and the respective technology.}) have a tradition as long as Computer Algebra Systems (CAS), another kind of mathematics assistants. However, CTPs task of proving is more challenging than calculating; so, in contrary to CASs, CTPs are not yet in widespread use --- not yet, because CTPs are on the step into industrial use in the current decade: Safe-critical software requires to be proven correct more and more \cite{db:dom-eng}, and the technology of CTP becomes ready to accomplish the task of efficiently proving hundreds of proof obligations.
    2.34 +
    2.35 +The present shift of the predominant user group from academic experts to software engineers raises novel user requirements for graphical user interfaces (GUI) of CTP. CTPs will become components of integrated development environments, and the knowledge bases have to scale up to industrial size.
    2.36 +
    2.37 +Two issues are particularly challenging: First, future knowledge bases (containing specifications, programs, tests etc) will under joint construction of many engineers. So requirements concerning cooperative work arise as already known from distributed repositories and version management.
    2.38 +
    2.39 +Second, CTP tends to exhaust resources in memory and in run-time. So, CTP will take profit from multicore processors upcoming in this decade --- and CTP are best suited to meet the architectural challenges raised by parallel programming, since this kind of mathematics assistants generally follow rigorous architectural principles and are comparably easy to adapt to these challenges \cite{makarius:isa-scala-jedit}.
    2.40 +
    2.41 +\medskip The paper is organised as follows: First a survey on CTP is given, Sect.\ref{ctp-techn} introduces two prominent CTPs, Sect.\ref{gui-coq-isa} describes their present user interfaces and Sect.\ref{gui-requir} goes into details with the novel requirements mentioned. Then Isabelle's plans for re-designing the user interface are presented: Sect.\ref{ml-users} motivates the strategy of how to approach the users' world, Sect.\ref{scala-medi} describes the rather recent programming language Scala connecting the world of languages for mathematics with the users' world and Sect.\ref{actors} goes into details with Scala's actor library. Finally possible contributions of the \sisac-team at TUG are discussed and prerequisites for such contributions presented: Sect.\ref{struct-der} presents a format for calculations particularly appropriate for education, which requires CTP support, Sect.\ref{plugin} describes plug-in technology required and Sect.\ref{netbeans} notes crucial details of proper project set-up in an integrated development environment.
    2.42 +
    2.43 +%Georg
    2.44 +\section{State of the art in CTP Interfaces}
    2.45 +
    2.46 +\subsection{A European technology: Coq and Isabelle}\label{ctp-techn}
    2.47 +%     http://en.wikipedia.org/wiki/Coq\\
    2.48 +%     http://coq.inria.fr/
    2.49 +%
    2.50 +%     http://en.wikipedia.org/wiki/Isabelle\_(theorem\_prover)\\
    2.51 +%     http://isabelle.in.tum.de/index.html
    2.52 +%
    2.53 +%why math -- functional: some of the languages have been specifically designed for constructing software for symbolic computation (SC). 
    2.54 +%%+ required for \ref{ml-users}
    2.55 +%
    2.56 +%SC http://en.wikipedia.org/wiki/Symbolic\_computation
    2.57 +%% mainly does not compute numerical values, but terms containing variables like functions (symbols)
    2.58 +%
    2.59 +%The LCF project
    2.60 +%http://hopl.murdoch.edu.au/showlanguage.prx?exp=8177
    2.61 +%specifically designed a 'meta language' (ML)
    2.62 +%http://en.wikipedia.org/wiki/ML\_(programming\_language)
    2.63 +%\cite{pl:milner97}
    2.64 +%for developing CTP
    2.65 +\subsubsection{Standard ML}
    2.66 +Standard ML is a general-purpose, modular, functional programming language \cite{pl:milner97}.
    2.67 +Programs written in Standard ML consist of expressions to be evaluated, as opposed to statements or commands. 
    2.68 +Functional programming languages constitute a family very different of object orientated languages, see Sect. \ref{ml-users}. ML originated from the LCF-project(Logic for Computable Functions)\cite{meta-Ml}, where it had been developed as a meta language. Since ML has been standardised this family of language is called Standard ML. Important for the logical foundation of SML is the $\lambda$-calculus.
    2.69 +%http://en.wikipedia.org/wiki/Standard_M 
    2.70 +\subsubsection{Coq}
    2.71 +Coq is an interactive theorem prover, developed in France.
    2.72 +It is programmed in Objective Caml, an ML based programming language.
    2.73 +It has the ability to express  mathematical  assertions and check proof of mathematical assertions. 
    2.74 +Furthermore Coq includes automatic theorem proving tactics and decision procedures.
    2.75 +Properties, programs and proofs are written a functional programming language called the Calculus of Inductive Constructions (CIC).
    2.76 +Proof development in Coq is done through a language of tactics that allows a user-guided proof process \cite{coq1999}.
    2.77 +Another feature of Coq is “that it can automatically extract executable programs from specifications, as either Objective Caml 
    2.78 +or Haskell source code.“
    2.79 +There are many easy-to-read introductions to Coq \footnote{http://coq.inria.fr/a-short-introduction-to-coq} on the internet.
    2.80 +\subsubsection{Isabelle}
    2.81 +Isabelle is an interactive theorem proving framework for high-level natural deduction proofs \cite{Paulson:Isa94}, written in Standard ML. 
    2.82 +Isabelle is developed at University of Cambridge, Technische Universit\"at M\"unchen
    2.83 +and Universit\'e Paris-Sud. Isabelle is called a framework, because it implements several object logics.
    2.84 +The most widespread logic of Isabelle is Isabelle/HOL, short for higher-order logic.
    2.85 +Isabelle/HOL includes several  specification tools, e.g. for data-types, inductive definitions and functions with complex pattern matching.
    2.86 +Proofs are written in the structured proof language Isar \cite{wenzel:isar}.Isabelle implements several tools, e.g. a reasoner, a simplifier and powerful automatic provers(Sledgehammer), increase the user's productivity in theorem proving. 
    2.87 +Isabelle provides notational support: new notations can be introduced, using normal mathematical symbols.
    2.88 +Definitions and proofs may include \LaTeX{} source, from which Isabelle can automatically generate typeset documents.
    2.89 +Isabelle/HOL allows to turn executable specifications directly into code in SML, OCaml, and Haskell \cite{Haftmann-Nipkow:2010:code}.
    2.90 +%(http://www.cl.cam.ac.uk/research/hvg/Isabelle/overview.html)
    2.91 +\subsection{Userinterfaces for CTP: Coq and Isabelle}\label{gui-coq-isa}
    2.92 +%     CoqIDE, ..
    2.93 +%         http://coq.inria.fr/what-is-coq?q=node/57\\
    2.94 +%         earlier than Isabelle/jEdit
    2.95 +%
    2.96 +%     ProofGeneral for Isabelle
    2.97 +%         http://proofgeneral.inf.ed.ac.uk/\\
    2.98 +%         emacs stone age ?
    2.99 +\subsubsection{Coq Integrated Development Environment}
   2.100 +CoqIDE\footnote{http://coq.inria.fr/V8.1/refman/Reference-Manual016.html}, short for Coq Integrated Development Environment, is a graphical interface for Coq. It is written in Ocaml.
   2.101 +Its main purpose is to allow the user to navigate forward and backward into a Coq file, 
   2.102 +executing corresponding commands or undoing them respectively. 
   2.103 +There are several  buffers for helping to write proof scripts.
   2.104 +Among all these buffers, there is always one which is the current running buffer, whose name is displayed on a green background,
   2.105 +which is the one where Coq commands are currently executed.  
   2.106 +CoqIDE provides also a feedback system for the user. 
   2.107 +Therefore the background is green when a command succeeds, otherwise an error message is displayed in the message window and the error location is underlined red.
   2.108 +CoqIDE offers only basic editing commands, therefore it is possible to launch another more sophisticated text editor. 
   2.109 +Furthermore CoqIde provides a proof wizard “for automatically trying to solve the current goal using simple tactics.”
   2.110 +Another features of this IDE are the customisation options, which can be accessed by the Edit menu. 
   2.111 +This allows the user to change the appearance of the IDE.
   2.112 +
   2.113 +
   2.114 +\begin{figure}[htbp]
   2.115 +\centering
   2.116 +%\includegraphics[bb=0 0 10 10]{coqide.png}
   2.117 +\includegraphics[scale=0.20]{fig/coqide}
   2.118 +\caption{CoqIDE main screen}
   2.119 +\end{figure}
   2.120 +
   2.121 +
   2.122 +%(http://coq.inria.fr/V8.1/refman/Reference-Manual016.html)
   2.123 +\subsubsection{Proof General for Isabelle}
   2.124 +Proof General is a generic front-end for proof assistants \cite{Aspinall:2007:FIP:1420412.1420429}, based on the text editor Emacs.
   2.125 +It has been developed at the University of Edinburgh with contributions from other sites.
   2.126 +Proof General supports the following proof assistants: Isabelle, Coq, PhoX, LEGO.
   2.127 +It is used to write proof scripts. A Proof Script is a sequence of commands sent to theorem prover. 
   2.128 +The communication between the user and the theorem prover takes place via two or  more Emacs text widgets.
   2.129 +Therefore the user sees only the output from the latest proof step.
   2.130 +
   2.131 +
   2.132 +Isabelle/Isar\footnote{http://proofgeneral.inf.ed.ac.uk/} Proof General has full support for multiple file scripting, with dependencies between theories communicated between Isabelle and Proof General. 
   2.133 +There is full support for Unicode Tokens, using the Isabelle print mode for X Symbol tokens. Many Isabelle theories have X Symbol syntax already defined 
   2.134 +and it's easy to add to your own theories. 
   2.135 +%(http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=releases%2FProofGeneral%2Fisar%2FREADME)
   2.136 +\begin{figure}[htbp]
   2.137 +\centering
   2.138 +\includegraphics[scale=0.30]{fig/pgisabelle}
   2.139 +\caption{Proof General for Isabelle}%
   2.140 +\end{figure}
   2.141 +
   2.142 +\subsubsection{Isabelle/Jedit}
   2.143 +jEdit is a text editor for programmers, written in Java.
   2.144 +Compared to fully-featured IDEs, such as Eclipse or NetBeans, jEdit is much 
   2.145 +smaller and better focused on its primary task of text editing.
   2.146 +The general look of the Isabelle/jEdit plug-in is similar to existing Java IDEs \cite{makarius:isa-scala-jedit}.
   2.147 +The main Isabelle/jEdit plug-in consists of ten small Scala files that augment some key jEdit components in order to provide a metaphor of asynchronous proof document editing. 
   2.148 +Isabelle/jEdit integrates the jEdit 4.3.2 framework  and some further  jEdit plug-ins. 
   2.149 +It also implements custom-made 'IsabelleText Unicode' font that actually contains the usual Isabelle symbols that users expect from long 
   2.150 +years of Proof General X-Symbol support.
   2.151 +The editor provides useful feedback, via semantic information from the processed document in the background. 
   2.152 +A lot of information can be directly attached 
   2.153 +to the source text, via colouring, tool-tips, pop-ups etc.
   2.154 +
   2.155 +\subsection{Upcoming requirements for userinterfaces in CTP}\label{gui-requir}
   2.156 +%     @ interaction close to tty (Telegraph)\\
   2.157 +%       BUT: separate parts in {\em one} proof could be processed in parallel
   2.158 +%
   2.159 +%     @ http://www.informatik.uni-bremen.de/uitp/
   2.160 +%
   2.161 +%     @ ... see\\
   2.162 +%       http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\
   2.163 +%       http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
   2.164 +"After several decades, most proof assistants are still centred around TTY-based interaction in a
   2.165 +tight read-eval-print loop.
   2.166 +All Emacs-based GUI's for CTPs follow this synchronous
   2.167 +model based on single commands with immediate response, meaning that the editor waits for the
   2.168 +prover after each command", according to \cite{makarius:isa-scala-jedit}. As to multicore politics of leading semiconductor chip manufacturer, parallelism in software technology has become an issue.
   2.169 +Therefore the support of parallelism in CTP technology improves the performance and multiuser support.
   2.170 +%So it is necessary to use proof documents instead of proof scripts.  
   2.171 +%Proof scripts are  sequences of commands however proof documents are structured texts. 
   2.172 +%So the proof document idea seems to guarantee the perfect support for parallelism in the CTP technology. 
   2.173 +Proof language Isar is structured such, that different parts can be interpreted in parallel. For instance, some might employ an 
   2.174 +an automated prover for some minutes, while the user wants to proceed with other parts of the same proof.
   2.175 +A well-established concept able to cope with such parallel processing in actors, as introduced by Erlang.
   2.176 +This will be discussed in more detail in Sect. \ref{actors}
   2.177 +
   2.178 +
   2.179 +%Andreas
   2.180 +\section{Isabelle's plans for new userinterfaces}\label{gui-plans}
   2.181 +
   2.182 +The following observations lead to novel requirements for CTPS' userinterface:
   2.183 +
   2.184 +\begin{itemize}
   2.185 +\item theorem proving will be integrated into software development
   2.186 +\item hundreds of proof obligations are generated during a software verification process
   2.187 +\item so the final goal of Isabelle's planning is integration with other software development tools in an integrated development environment (IDE)
   2.188 +\item still many principal issues need to be clarified with respect to integration of CTP and other development tools. So engaging into details makes no sense at the present, and Isabelle will approach the final goal via experimental intermediate steps of integration
   2.189 +\item favourite IDE is jEdit, because it is clearer than Eclipse or NetBeans. The reason behind this choice follows in section \ref{plugin}
   2.190 +\end{itemize}
   2.191 +
   2.192 +These indicate design decisions are sketched in the sequel.
   2.193 +
   2.194 +\subsection{Connect ML-world to the users' world via JVM}\label{ml-users}
   2.195 +In Sect.\ref{ctp-techn} reasons have been given, why mathematics software at the state-of-the-art cannot be written in Java or the like. On the other side, Sect.\ref{gui-requir} stated requirements for mathematical userinterfaces, which cannot be accomplished by ML-like languages. These requirements can be best accomplished by languages like Java, which have powerful libraries available for convenient assembly of GUIs.
   2.196 +
   2.197 +\paragraph{Example: a functional mathematics engine} as the experimental one in the \sisac-project is given by the following signature:
   2.198 +{\it
   2.199 +\begin{tabbing}
   2.200 +\=xx\=xxxxxxxxxxxxxxxxxxxxxxxxx\=\kill
   2.201 +\>signature INTERPRETER =\\
   2.202 +\>sig\\
   2.203 +\>\>type calcstate\\
   2.204 +\>\>type step = formula * position * tactic\\
   2.205 +\>\> \\
   2.206 +\>\>val do\_next : program $\rightarrow$ calcstate $\rightarrow$ (calcstate * step)\\
   2.207 +\>\>val apply\_tactic : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ tactic $\rightarrow$ (calcstate * step list)\\
   2.208 +\>\>val apply\_formula : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ formula $\rightarrow$ (calcstate * step list)\\
   2.209 +\>end
   2.210 +\end{tabbing}}
   2.211 +The three essential functions are \textit{do\_next}, which reads a \textit{program} for determining the next \textit{step} in a calculation, the function \textit{apply\_tactic}, which applies a \textit{tactic} input by the user to the current \textit{position} in a calculation and thus may produce a list of \textit{step}s and the function \textit{apply\_formula}, which applies an input \textit{formula} accordingly.
   2.212 +
   2.213 +Now, the point with functional programming is, that the functions do {\em not} cause persistent updates in some memory, rather: all three functions above take the current state of the calculation, \textit{calcstate}, as an argument and after they have done they work return the updated \textit{calcstate}.
   2.214 +
   2.215 +There are several advantages of this kind of programming: more straight forward verification, which is not discussed here, and other features. For instance, given the three functions above, it is easy to undo steps of calculations, or go back to an earlier step of calculations: one just needs to store the \textit{calcstate}s (in a list), even without knowing the details of the \textit{calcstate}, which thus can be encapsulated for internal access only.
   2.216 +
   2.217 +\paragraph{Example: an object-oriented wrapper} as required for embedding the above mathematics engine into an object-oriented system. Such a wrapper may look like this:
   2.218 +{\footnotesize
   2.219 +\begin{verbatim}
   2.220 +   public class Calcstate
   2.221 +   {
   2.222 +     private Program program_;
   2.223 +     private Tree<Step> calcstate_;
   2.224 +     private Position position_;
   2.225 +     
   2.226 +     public Calcstate(Program program) {...}
   2.227 +     public Step do_next() {...}
   2.228 +     public List<Step> apply_tactic(Tactic tactic) {...}
   2.229 +     public List<Step> apply_formular(Formular formular) {...}
   2.230 +   }
   2.231 +\end{verbatim} 
   2.232 +}
   2.233 +\subsection{Scala as a mediator between ML and JVM}\label{scala-medi}
   2.234 +Scala \footnote{http://www.scala-lang.org} is a hybrid programming language. It combines object-oriented programming and functional programming. Scala runs on the Java Virtual Machine and is byte-code compatible with existing Java programs. The compilation model of Scala is nearly the same as the Java's model. So existing tools, libraries and applications can be used with Scala. The syntax of Scala is similar to Java and ML. A number of keywords plus the block syntax is adopted from Java and from ML the syntax for type annotation and declaration. The source-code is typically reduced, concisely and more compact compared to equivalent Java code \footnote{http://www.scalasolutions.com/scala}.
   2.235 +
   2.236 +Scala is pure object-oriented, this means every value is an object \cite{odersky:scala06}. The same is true for primitive data types, because compiler-generated byte code is using primitive data types. Known design patterns from OOP can be used with Scala as well. "Data types and behaviours of objects are described by classes and traits" \footnote{http://en.wikipedia.org/wiki/Scala\_(programming\_language)}. Traits not only consist of definitions, they also can contain implementations of methods. To avoid the problems of multiple inheritance, classes are able to extend various traits, this is a flexible mixin-based mechanism. The keyword Object is used to implement a Singleton-Class.
   2.237 +
   2.238 +In Scala every function is a value, hence Scala is also a functional language \cite{odersky:scala06}. Functions in Scala are first-class objects, this means it is possible to pass a function as a parameter, return a function from a subroutine, or assign to a variable. Scala also supports case classes, which are used for pattern matching. Case classes are regular classes which export their constructor parameters \footnote{http://de.wikipedia.org/wiki/Scala\_(Programmiersprache)}. Furthermore Scala allows functions to be nested.
   2.239 +
   2.240 +Scala is more statically typed than Java, but is able to infer types by usage. So most static type declarations are optional. This static type system ensures a safe and coherent use of abstraction. Scala supports \footnote{http://en.wikipedia.org/wiki/Scala\_(programming\_language)}:
   2.241 +
   2.242 +\begin{itemize}
   2.243 +\item generic classes
   2.244 +\item variance annotations
   2.245 +\item upper and lower type bounds
   2.246 +\item classes and abstract types as object members
   2.247 +\item compound types
   2.248 +\item explicitly typed self references
   2.249 +\item views
   2.250 +\item polymorphic methods
   2.251 +\end{itemize}
   2.252 +
   2.253 +Static types need no explicit declaration but can be given to give the code some clarity.
   2.254 +
   2.255 +Scala supports threads, but the Scala library contains an actor model inspired from Erlang \cite{armstrong:erlang96}. Concurrency and Scala actors follow in the next section.
   2.256 +
   2.257 +\subsection{Support for parallel processing}\label{actors}
   2.258 +Concurrency has lately become more and more attention, because multicore processors make concurrency very important for efficient program execution, by running multiple threads parallel and so concurrent programming gets indispensable and distributed computing, web services and mobile environments are naturally concurrent. A very attractive model is message-based concurrency, which is based on the actor model.
   2.259 +
   2.260 +An actor is a concurrent process that executes a function. The state of an actor gets never shared, so it doesn't need to compete for locks of shared data. Actors own a mailbox where incoming messages are stored in. A mailbox is mainly a queue with actors, which operate as several producers and one consumer. Actors share data by sending messages which are sent asynchronously. Messages are unchangeable, so they don't require a lock. By creating new actors, by sending messages to known actors, or changing its behaviour, an actor is able to reply to a message. The actor-based process is combined with pattern matching for messages.
   2.261 +
   2.262 +The Erlang programming language is a functional programming language that supports message-based concurrency, which operates with actors. It was developed for real-time control systems. Such systems are telephone exchanges, network simulators and distributed resource controllers \cite{scala:jmlc06}. These systems use a very popular lightweight implementation and a large number of concurrent processes, which can be active simultaneously.
   2.263 +
   2.264 +Operating system threads and threads of virtual machines are too heavyweight for the implementation of such processes. The standard concurrency for mainstream platforms were shared-memory threads with locks. Such a platform is the Java Virtual Machine (JVM), which suffers from high memory consumption and context-switching overhead.
   2.265 +The most disadvantageous consequences are \cite{scala:jmlc06}:
   2.266 +\begin{enumerate}
   2.267 +\item quick exhaustion of virtual address space
   2.268 +\item locking mechanisms often lack suitable contention managers
   2.269 +\end{enumerate}
   2.270 +
   2.271 +For that reasons Erlang uses lightweight concurrent processes by its own run time system and not by the underlying operating system \cite{scala:jmlc06} and the computations on these platforms are often modelled in an event-driven style, which is complicated and error-prone.
   2.272 +\paragraph{Two different strategies for concurrency} are being used for implementation. This two strategies often follow different programming models, the benefit of thread-based models is that they are easier to use, but they still suffer from the memory consumption and the context-switching. The event-based models are just the opposite of the thread-based, they are more efficient, but in massive designs they are very difficult.
   2.273 +
   2.274 +\subparagraph{Thread-based implementation:} The behaviour of a concurrent process is defined by implementing a thread-specific method. The execution state is maintained by an associated thread stack \cite{Haller:2009:SAU:1496391.1496422}.
   2.275 +Supports blocking operations and can be executed on multicore processors in parallel.
   2.276 +
   2.277 +\subparagraph{Event-based implementation:} The behaviour is defined by a number of (non-nested) event-handlers which are called from inside an event loop. The execution state of a concurrent process is maintained by an associated record or object \cite{Haller:2009:SAU:1496391.1496422}. Targets to a large number of actor which can be active simultaneously, because they are more lightweight.
   2.278 +
   2.279 +\paragraph{Actors in Scala} are based on actors in Erlang. Scala uses the basic thread model of Erlang, but on the other hand all higher-level functions got implemented in the Scala library as classes or methods. The Scala-actors are a unification of the implementation models mentioned above and they are compatible with normal Virtual Machine (VM) thread. Normal VM threads can use the same communication and monitoring capabilities, because they are treated like an actor. A message-based concurrency seems to be more secure than shared-memory with locks, because accessing an actor's mailbox is race-free. The advantage of a implementation in a library is that it can be flexibly extended and adapted to new needs. The library makes use of Scala abstraction opportunities, like partial functions and pattern matching.
   2.280 +
   2.281 +The main idea of this model is that an actor is able to wait for a message by using two different operations, which try to remove a message from the current actor's mailbox. To do so, a partial function must be given to the operation, that specifies a set of message patterns. These are {\itshape receive} and {\itshape react}. 'An actor can suspend with a full thread stack (receive) or it can suspend with just a continuation closure (react)' \cite{Haller:2009:SAU:1496391.1496422}. The first operation of an actor to wait for an message is equal to thread-based programming and the second operation to event-based programming.
   2.282 +
   2.283 +\subparagraph{receive:} The current actor's mailbox get scanned and if there is one message which matches one of the patterns declared in the partial function, the message is removed from the mailbox and the partial function is applied to the message, the result is returned. The declaration of receive:
   2.284 +$$\mathit{def}\;\mathit{receive}\mathit{[R]}(f: \mathit{PartialFunction}[Any, R]): \mathit{R}$$
   2.285 +Otherwise the current thread blocks. Thus the receiving actor has the ability to execute normally when receiving a message which matches.  Note that receive retains the complete call stack of the receiving actor; the actor’s behaviour is therefore a sequential program which corresponds to thread-based programming \cite{Haller:2009:SAU:1496391.1496422}.
   2.286 +\subparagraph{react:} The action which is specified in the partial function is the last code that the current actor executes, if the message is matching. The declaration of react:
   2.287 +$$\mathit{def}\;\mathit{react}(f: \mathit{PartialFunction}[Any, Unit]): \mathit{Nothing}$$
   2.288 +The partial function gets registered by the current actor and the underlying thread gets released. React has the return type Nothing, this means that the method never returns normally. When the actor receives a matching message, the earlier registered partial function gets called and the actor's execution gets continued. The partial function f which corresponds to a set of event handlers \cite{Haller:2009:SAU:1496391.1496422}. 
   2.289 +
   2.290 +For this implementation multiple actors are executed by multiple threads and therefore a thread pool is used. Whenever it is necessary the pool can be re sized, to support the operations of the thread-based and event-based model. If only operations of the event-based model are executed then the thread pool could be fixed. To avoid system-included deadlocks, if some actors use thread-based operations, the thread pool has to grow, because if there are outstanding tasks and every worker thread is occupied by a blocked actor, new threads are necessary.
   2.291 +
   2.292 +Since the communication between actors takes place through asynchronous message passing, asynchronous operations get executed, tasks have to be created and submitted to a thread pool for execution. A new task is created, when an actor spawns a new actor or a message, which enables an actor to continue, is send to an actor which is suspended in a react operation or by calling react, where a message can be immediately removed from the mailbox \cite{Haller:2009:SAU:1496391.1496422}.
   2.293 +
   2.294 +% Marco
   2.295 +\section{Planned contributions at TU Graz}
   2.296 +
   2.297 +\subsection{Make Isabelle process structured derivations}\label{struct-der}
   2.298 +Structured Derivations (SD) is a format for calculational reasoning, which has been established by \cite{back-grundy-wright-98}. This is an example calculation:
   2.299 +{\it\begin{tabbing}
   2.300 +123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
   2.301 +\> $\bullet$\> \Problem [ maximum\_by, calculus ]\\
   2.302 +\>\> $\vdash$\> $A = 2\cdot u\cdot v - u^2$\\
   2.303 +\>\> $\bullet$\> \Problem [make, diffable, funtion]\\
   2.304 +\>\> \dots\> $\overline{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$\\
   2.305 +\>\> $\bullet$\> \Problem [on\_interval, for\_maximum, differentiate, function]\\
   2.306 +\>\>\> $\vdash$\> $\overline{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$\\
   2.307 +\>\>\> $\bullet$\> \Problem [differentiate, funtion]\\
   2.308 +\>\>\> \dots\> $\overline{A}^\prime(\alpha) = 8\cdot r^2\cdot(-(\sin\alpha)^2+(\cos\alpha)^2 - 2\cdot\sin\alpha\cdot\cos\alpha)$\\
   2.309 +\>\>\> $\bullet$\> \Problem [on\_interval, goniometric, equation]\\
   2.310 +\>\>\> \dots\> $\alpha = \tan^{-1}(-1+\sqrt{2})$\\
   2.311 +\>\> \dots\> $\alpha = \tan^{-1}(-1+\sqrt{2})$\\
   2.312 +\>\> $\bullet$\> \Problem [tool, find\_values]\\
   2.313 +\>\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ]\\
   2.314 +\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] %TODO calculate !
   2.315 +\end{tabbing}}
   2.316 +The plan is to use the machinery provided Isabelle/Isar as a 'logical operating system' ~\cite{isar-impl} and adapt the machinery such that is accepts SC in parallel to the Isar proof language~\cite{wenzel:isar}.
   2.317 +
   2.318 +This plan involves the following details.
   2.319 +
   2.320 +\subsection{Add a plug-in to jEdit}\label{plugin}
   2.321 +    % file structure, copied from example project ...
   2.322 +%Die von jEdit verfolgte Strategie im Bezug auf plug-in Management und natürlich generell die totale Offenlegegung des Codes ist für ein Projekt wie Isabelle und auch für das Isac-Project an der TU ideal. plug-ins lassen sich sehr einfach anfügen und durch die riesige Vielfalt von bereits bestehenden plug-ins ist auch die Adaption von plug-ins möglich bzw. zu empfehlen, denn warum sollte nicht bereits funktionierender Code verwendet werden?\\
   2.323 +The importance of connecting the ML-world with the world of user interfaces has been is discussed in Sect.\ref{ml-users}. jEdit follows these lines, it is an open-source, Java-based text editor that works on Windows, Mac OS X, and Linux. A big advantage of jEdit is, that there is a very good and also simple way to use and write a plug-in. There are a lot of useful and powerful plug-ins available in the net and it is also possible to use a existing plug-in as part of a new one. Because of this facts, jEdit is very suitable for a project like Isabelle and also for the \sisac-project at TU-Graz.
   2.324 +
   2.325 +Each jEdit plug-in\footnote{To get more information about the jEdit infrastructure see: http://jedit.org/users-guide/plugin-intro} basically consists of source files, written in Java or Scala, XML-files and property files. The XML-Files are important for the administration of a plug-in and provides information like the name, author, ... of the plug-in. They are also containing small pieces of BeanShell code which is executed upon a user request. (Like pressing the 'start plugin' button.) So the XML-files provide the “glue” between user input and specific plug-in routines located in the source files. As you see, this files are used as interface between the plug-in and the jEdit engine itself.
   2.326 +
   2.327 +Based on the jEdit API, you are allowed to design your code quit freely and don't have to use a prescribed way to implement your ideas.    
   2.328 +
   2.329 +
   2.330 +%isabell plugin beschreiben!!!!!!!!
   2.331 +The Isabelle-team also follow use this plug-in structure. In the next paragraph the involved files will be described. The jEdit-Isabelle plug-in consists of:
   2.332 +\begin{itemize}
   2.333 +\item 14 Scala-source-files
   2.334 +\item 3 XML-files
   2.335 +\item 1 property file
   2.336 +\end{itemize}
   2.337 +%Das vom Isabelle-Team erstellte jEdit plug-in folgt natürlich auch dem oben erklärten Muster. Es wird nun genauer auf dieses plug-in eingegangen. The plugin consits of 14 scala-source-files, three xml-files and one property-file. 
   2.338 +\begin{description}
   2.339 +\item[Isabelle.props] The property-file \textit{Isabelle.props} contains general information about the Isabelle plug-in and the needed dependencies between Isabelle and the other used plug-ins like sidekick.
   2.340 +\item[dockables.xml] The XML-file \textit{dockables.xml} is used to create the needed dock-able windows which are important to set up the GUI of the plug-in.
   2.341 +\item[actions.xml] In the file \textit{actions.xml}, the dockable windows are added to the window-manager \textit{wm} and there is also some BeanShell-code to activate the Isabelle-GUI.
   2.342 +\item[services.xml] The last XML-file is \textit{services.xml} and is used to create instances of needed jEdit plug-ins.
   2.343 +\end{description}
   2.344 +This four files are located in the folder \textit{plugin}.\\
   2.345 +
   2.346 +The more interesting files, the scala-files of the plug-in, can be found in the 'src/jedit'-directory. In this directory you can find the file \textit{Dummy.java} which is a dummy class and is simply used to make javadoc work. Just forget about this file. Also there is a folder/package \textit{jedit} which contains all Scala-source-files. Now it is time to take a closer look on the source-files: 
   2.347 +\begin{description}
   2.348 +\item[plugin.scala] The file \textit{plugin.scala} is the main-file of the Isabelle plug-in and there are two important parts. First the \textit{Isabelle object}. This object contains data like name and path and also few basic functions. The second part is the \textit{class Plugin} which is derived from EBPlugin. Here the basic methods \textit{handleMessage}, \textit{start} and \textit{stop} are implemented. Each jEdit plug-in should have this methods because they are very important for the handling of the plug-in!
   2.349 +\item[dockable.scala] jEdit and also the Isabelle plug-in work with dock-able windows. This means that you can move around each single window and dock it somewhere on the screen. So it is possible to customise the jEdit-GUI. To support this, the file \textit{dockable.scala} is needed. The file \textit{output-dockable.scala} is derived from \textit{dockable.scala} and is used to print the result/output in a dock-able window. The same thing with \textit{protocol-dockable.scala} and \textit{raw-output-dockable.scala}.
   2.350 +\item[scala-console.scala] The next interesting file is \textit{scala-console.scala} with the main-class Scala-Console. This class is used to expand the Console plug-in in a way, that it is possible to interpret Scala-code with a Shell inside of jEdit.
   2.351 +\item[isabelle-sidekick.scala] The file \textit{isabelle-sidekick.scala} is related to the file \textit{scala-console.scala} because it is also used to adapt the plug-in Sidekick for Isabelle.
   2.352 +\item[document-model.scala, document-view.scala] The files \textit{document-model.scala} and \textit{document-view.scala} are used to connect the jEdit-buffer/the text-area to Isabelle. Both classes offer, upon others, methods to activate and deactivate this features.
   2.353 +\end{description}
   2.354 +There also some other source-files but they aren’t discussed here, because the main goal of this paragraph is to give a basic idea how a jEdit plug-in should be set up and the remaining files are not as important for the Isabelle plug-in structure.
   2.355 +%\begin{itemize}
   2.356 +%\item $html_panel.scala$
   2.357 +%\item $isabelle_encoding.scala$
   2.358 +%\item $isabelle_hyperlinks.scala$
   2.359 +%\item $isabelle_options.scala$
   2.360 +%\item $isabelle_token_maker.scala$
   2.361 +%\item $isabelle_hyperlinks.scala$
   2.362 +%\end{itemize}
   2.363 +
   2.364 +
   2.365 +%  Like each other jEdit-Plugin also this 
   2.366 +
   2.367 +%Das Konzept des frei wählbaren Designs ist am Beginn villeicht etwas schwierig umzusetzten, da es leichter ist, sich irgendwo anzulehnen bzw. ein bereits bestehendes sowie funktionierendes Konzept zu übernehmen. So wurden auch die ersten Schritte an der TU gemacht. Zu diesem Zweck wurde das von den Entwicklern von jEdit zur Verfügung gestellte plugin 'QuickNotepad' übernommen und in Scala übersetzt. Obwohl Scala eng mit Java verknüpft ist, war doch einiges an 'rewritting' notwendig bis das Scala-plugin lauffähig wurde. Die benötigten XML-files konnten dazu nahezu unberührt gelassen werden.\\
   2.368 +
   2.369 +\subsection{Details of NetBeans projects}\label{netbeans}
   2.370 +%     Scala + Java: html project files
   2.371 +As described in the last paragraph, jEdit is a open-source-project. The jEdit-developers use a NetBeans-project to produce the source-code and so it is beneficial to use a NetBeans project too, because there is a quite good documentation about setting up a NetBeans-project with the jEdit-source. See http://wiki.netbeans.org/NetbeansedJEdit for further information.\\\\
   2.372 +If you want to set up a new jEdit plug-in project you have to attend that you have to create some source-files and that there must be a connection to the jEdit-source because you will need to exchange data with the jEdit engine. This could probably look like: \textit{jEdit.getProperty("options.isabelle.isabelle")}\\
   2.373 +As shown above, the jEdit-source is needed to compile and build your plug-in. There are two ways to organise your project:
   2.374 +\begin{itemize}
   2.375 +\item with jEdit source code - two projects in one
   2.376 +\item with jedit.jar library
   2.377 +\end{itemize}
   2.378 +\subsubsection{Plug-in with jEdit-source}
   2.379 +It is a good way to download the jEdit source as NetBeans project because then it is possible to add another sub-project to the existing jEdit-NetBeans-project. As you see it is also possible to mix Scala and Java. A big advantage is, that debugging will now work really fine. If you want to set up a project like this, you should complete the following steps.
   2.380 +\begin{enumerate}
   2.381 +\item {Create a new NetBeans-project for your plug-in like \textit{example-plugin}. This will probably be a Scala-Project.}
   2.382 +\item Download (and try out) the \textit{jEdit-NetBeans-project}
   2.383 +\item at project \textit{example-plugin}: \textit{Project-browser} $\rightarrow$ Right-click at \textit{Libraries} $\rightarrow$ \textit{add Project...} and then choose the \textit{jEdit-NetBeans-project}.
   2.384 +\item at project \textit{example-plugin}: \textit{Project-browser} $\rightarrow$ Right-click at project-name-label $\rightarrow$ \textit{Properties} $\rightarrow$ \textit{Run} $\rightarrow$ \textit{Main Class:} org.gjt.sp.jedit.jEdit
   2.385 +\item compile and run
   2.386 +\end{enumerate}
   2.387 +
   2.388 +\subsubsection{Plug-in with jedit.jar}
   2.389 +It is also possible to use the \textit{jedit.jar} file. This file is already included in \$ISABELLE-HOME/contrib/jedit-4.3.2. Now you just have to follow this steps:
   2.390 +\begin{enumerate}
   2.391 +\item {Create a new NetBeans-project for your plug-in like \textit{example-plugin}. This will probably be a Scala-Project.}
   2.392 +\item at project \textit{example-plugin}: \textit{Project-browser} $\rightarrow$ Right-click at \textit{Libraries} $\rightarrow$ \textit{add JAR/Folder...} and then choose the \textit{jedit.jar} file.
   2.393 +\item at project \textit{example-plugin}: \textit{Project-browser} $\rightarrow$ Right-click at project-name-label $\rightarrow$ \textit{Properties} $\rightarrow$ \textit{Run} $\rightarrow$ \textit{Main Class:} org.gjt.sp.jedit.jEdit
   2.394 +\item compile and run
   2.395 +\end{enumerate}
   2.396 +This are two different ways to get started. It is difficult to say what is better because both versions have advantages. Now it is time to start coding your own plug-in but there are still a few things to think about. Remember, that a plug-in consists of source-, XML- and property-files. On default, NetBeans will just pack the source-files in the \textit{example-plugin.jar}-package. So you have to add a copy/move-routine in the \textit{build.xml} file of your NetBeans-project to get a complemented package.
   2.397 +\begin{itemize}
   2.398 +\item $\langle target name="-pre-jar"\rangle$
   2.399 +\item $	\langle copy $file="plugin/services.xml" todir="\${build.classes.dir}" $/\rangle$
   2.400 +\item $	\langle copy $file="plugin/dockables.xml" todir="\${build.classes.dir}" $/\rangle$
   2.401 +\item $	\langle copy $file="plugin/actions.xml" todir="\${build.classes.dir}" $/\rangle$	
   2.402 +\item $	\langle copy $file="plugin/Isabelle.props" todir="\${build.classes.dir}" $/\rangle$
   2.403 +\item $	\langle /target\rangle$
   2.404 +\end{itemize}
   2.405 +%* kurze aufzählung der xml-netbeans-files + erklärung\\
   2.406 +\subsubsection{NetBeans project files}
   2.407 +As you see in the paragraph above, it is also important to have basic knowledge about NetBeans, the project structure and how to change the operational sequences. A typical NetBeans-project consist of the source- and library-files and administrative XML- and property-files. In this paragraph the administrative part of the project is of note. The most important file is \textit{build.xml}. This file can be found in the project directory. There is also a folder \textit{nbproject} which contains the remaining XML- and property-files and also a folder \textit{private}, where individual user information about the project is stored. The files in this \textit{private} folder are not important to describe (and they should not be pushed on the repository!).
   2.408 +
   2.409 +A build-file like \textit{build.xml} contains one project and at least one (default) target. Targets contain task elements. Each task element of the build-file can have an id attribute and can later be referred to by the value supplied to this. So the id has to be unique. Such targets can be "run", "debug", "build", ... and can have dependencies to other targets. Tasks define what should happen, if a target is executed. So like in the example above, the target is \textit{pre-jar}, that means that this things will happen before the jar-package is packed. The tasks of this target are copying some files into the package.
   2.410 +
   2.411 +The files inside the \textit{nbproject}-folder are not so important because some of it are generated from \textit{build.xml} and changes in this files are useless. Just the file project.properties is really interesting because this file gives a nice and tight overview about the project settings.
   2.412 +
   2.413 +\subsection{Use interfaces between Java and Scala}\label{java-scala}
   2.414 +%     how are data exchanged between Scala and Java ...
   2.415 +jEdit is completely written in Java and the required plugin(s) for \sisac{ }will be coded in Scala - so there must be ways to exchange data between Java and Scala. One way is to connect this two worlds with the in 4.2 described XML-files. Here you need to use a third type of code to get an interface between Java and Scala code. But there is also a way to get a direct connection.
   2.416 +
   2.417 +This link should be shown on the graphic-library \textit{Swing}. In both languages it is possible to use Swing which provides a lot of different shapes and useful functionality. So there is a Java-Swing and also a Scala-Swing-library. Now it is interesting to examine the connection between this two libraries.
   2.418 +
   2.419 +In Scala a direct use of Java-Libs (like Java-Swing) is possible. So if you are Java-Programmer and want to use Java-Swing in Scala, you can simply type\\ \textit{import javax.swing.JButton}\footnote{http://download.oracle.com/javase/1.4.2/docs/api/javax/swing/JButton.html} to work with a Java-button. But you can also use the Scala-equivalent \textit{scala.swing.Button}\footnote{http://www.scala-lang.org/api/current/scala/swing/Button.html}. This two button-types will provide nearly the same functionality.
   2.420 +
   2.421 +So what is the idea of creating a nearly similar library a second time? Why have the Scala-developers done such extra work? The answer is, that they have tried to improve and simplify the usage of the Swing-library(and many other libs too!). So big parts of this Scala-Libraries are just Wrapper-objects, Wrapper-Classes and Wrapper-Methods of already existing parts in Java-Libraries. Needless to say that they also added new useful shapes and functionality.
   2.422 +But there is one important question left: Is it possible to mix Scala- and Java-objects? And yes, it is possible. There is a really easy way to convert a Scala-object to the Java-equivalent:
   2.423 +\begin{enumerate}
   2.424 +\item \textit{import javax.swing.JButton}
   2.425 +\item \textit{import scala.swing.Button}
   2.426 +\item \textit{var b: scala.swing.Button}
   2.427 +\item \textit{var jb: javax.swing.JButton}
   2.428 +\item \textit{jb = b.peer}
   2.429 +\end{enumerate}
   2.430 +As the example above illustrates, a conversion of Scala- to Java-objects is possible. It looks easy but also a little bit useless. Why should you need this? Just imagine that there is a plug-in written in Scala and one coded in Java. With this connection between Scala and Java, it would be easy to connect this two plug-ins! 
   2.431 +%Diesen direkten Zusammenhang zwischen Java und Scala soll anhand der Grafik-Bibliotheken Swing. Beide Sprachen stellen diese Grafik-Bibliotheken zur Verfügung (und darin auch eigene Shapes und Funktionalität). Es ist jedoch möglich, Java-Bibliotheken, wie eben auch Java-Swing in Scala zu verwenden. Ein JButton kann zum Beispiel mittels \textit{import javax.swing.JButton} eingebunden und damit sofort auch verwendet werden. Auch Scala stellt in seiner Swing-Bibliothek zur Verfügung: \textit{scala.swing.Button}. Es wird nahezu die selbe Funktionalität angeboten und teilweise die Erzeugung bzw. Verwendung vereinfacht(???). Man kann sich nun fragen, warum sich die Scala-Entwickler einerseit die Mühe gemacht haben die Verwendung Java-Swing, wie in Java selbst, möglich zu machen und andererseits mit Scala-Swing eine nahezu idente Alternative geschaffen haben. Die Antwort darauf zeigt wie der objektorientierte Teil von Scala in vielen Bereichen aufgebaut wurden. Es wurde kein neues Konzept für diese Grafikklassen entworfen sondern Wrapper-Objekte/Methoden/Klassen erstellt, die das Arbeiten mit diesen Grafikkomponenten erleichtern soll. Ein Letztes Problem bleibt noch: Es ist zwar sehr einfach ein Java-Swing-Objekt an einen Scala-Swing-Container (zb. Frame) anzubinden, da eine Konvertierung von Java-Komponente in ein Scala-Äquivalent ist problemlos möglich. ...
   2.432 +\section{Conclusion and future work}
   2.433 +This paper collected background information on the topic of userinterfaces for theorem provers, which is not covered by the standard curriculum at Graz University of Technology: Computer theorem proving, respective interfaces and novel challenges for userinterfaces raised by integration of CTP into software engineering tools within the current decade.
   2.434 +
   2.435 +The general background information has been related to students' knowledge already gained during studies: functional and object-oriented programming paradigm, programming languages with focus on Scala and Scala's specific concept to handle asynchronous processing of proof documents, the concept of actors.
   2.436 +
   2.437 +An important part of the paper is a protocol of preparatory work already done on project-setup and software components required for the next goal which is: extend the theorem prover Isabelle with Structured Derivations.
   2.438 +
   2.439 +This part is considered an appropriate to start realising this goal and to prepare for future work, which will join the \sisac-project with front-of-the-wave technology in computer theorem proving and respective userinterfaces.
   2.440 +
   2.441 +\bigskip\noindent {\Large\textbf{Acknowledgements}}
   2.442 +
   2.443 +\medskip\noindent The authors thank the lecturer of 'Verfassen wissenschaftlicher Arbeiten' in winter semester 2010/11, Dipl.-Ing. Dr.techn. Markus Strohmaier, for his support on working on the topic they are interested in.\\
   2.444 +The leader of the \sisac-project expresses his pleasure about the efficient collaboration between the institutes IICM and IST at TUG.
   2.445 +
   2.446 +\bibliography{CTP-userinterfaces}
   2.447 +%\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl}
   2.448 +\end{document}
   2.449 \ No newline at end of file

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-isac/akargl/ferialprakt.tex	Tue Sep 17 09:50:52 2013 +0200
     3.3 @@ -0,0 +1,101 @@
     3.4 +\message{ !name(ferialprakt.tex)}\documentclass[a4paper,12pt]{article}
     3.5 +\usepackage{ngerman}
     3.6 +\usepackage{longtable}
     3.7 +
     3.8 +
     3.9 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    3.10 +\def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    3.11 +
    3.12 +\title{Ferialpraxis\\ am Institut f\"ur Softwaretechnologie\\
    3.13 +       der Technischen Universit\"at Graz\\ \ 
    3.14 +       \\Arbeitsprotokoll}
    3.15 +\author{Alexander Kargl\\
    3.16 +       akargl@brgkepler.net}
    3.17 +\date{\today}
    3.18 +
    3.19 +\begin{document}
    3.20 +
    3.21 +\message{ !name(ferialprakt.tex) !offset(-3) }
    3.22 +
    3.23 +\maketitle
    3.24 +$\;$\\
    3.25 +\vspace{0.2cm}
    3.26 +\section{Urspr\"ungliche Erwartungen}
    3.27 +In den letzten Sommerferien vor der Maturaklasse wollte ich mich genauer \"uber die Studienrichtungen im Bereich Informatik an der TU Graz informieren. Meine Interessen tendierten bereits in diese Richtung, aber ich war mir noch nicht sicher, ob das die richtige Entscheidung ist.
    3.28 +
    3.29 +Ich hatte das Gl\"uck ein Praktikum am Insitut f\"ur Softwaretechnologie absolvieren zu d\"urfen. Ich hoffte dadurch:
    3.30 +\begin{itemize}
    3.31 + \item einen Einblick in die Programmierung und Entstehung von gr\"o\3eren Softwareprojekten zu erhalten
    3.32 + \item neue Programmiertechniken und Sprachen kennenzulernen
    3.33 + \item und au\3erdem gleich wertvolle Erfahrung im Arbeitsleben sammeln zu k\"onnen
    3.34 +\end{itemize}
    3.35 +
    3.36 +\newpage
    3.37 +\section{Arbeitsprotokoll}
    3.38 +\begin{center}
    3.39 +\begin{tabular}{l|l||r}
    3.40 +\textbf{Datum}   &\textbf{T\"atigkeit} & \textbf{Std.} \\[1pt] \hline \hline\noalign{\smallskip}
    3.41 +12.7.2011
    3.42 + & Demonstration von ``educational math assistant \isac{}'', Isabelle & 1.6\\
    3.43 + %& Demonstration des Theorem Provers  & 0.6\\
    3.44 + & Einf\"uhrung Linux, objektorientierte/funktionale Programmierung& 2.0\\
    3.45 + & Installation: Isabelle, \isac-core, Mercurial & 3.0\\[3pt] \hline\noalign{\smallskip}
    3.46 +13.7.2011
    3.47 + & Einf\"uhrung Latex,  Konfiguration von Mercurial & 2.6 \\
    3.48 + %& & 1.6 \\
    3.49 + & ML-Programmierung/Einf\"uhrung & 5.0 \\[3pt] \hline\noalign{\smallskip}
    3.50 +14.7.2011
    3.51 + & Einf\"uhrung und \"Ubung ML II & 4.6 \\
    3.52 +% & Programmierung ML & 2.0 \\
    3.53 + & Erstellung v. Beispielen f\"ur Kombinatoren in ML & 3.0 \\[3pt] \hline\noalign{\smallskip}
    3.54 +15.7.2011
    3.55 + & Einf\"uhrung ML/\isac\  IV & 2.1 \\
    3.56 + & ML- Programmierung & 5.5 \\ \hline \hline\noalign{\smallskip}
    3.57 +18.7.2011
    3.58 + & Fehlersuche/Debugging Isac-Tests & 7.6 \\[3pt] \hline\noalign{\smallskip}
    3.59 +19.7.2011
    3.60 + & Tests zu korrigiertem CompleteCalc auskommentiert & 7.6 \\
    3.61 + & interface.sml calchead.sml ctree.sml mathengine.sml rewtools.sml &  \\[3pt] \hline\noalign{\smallskip}
    3.62 +20.7.2011
    3.63 + & Fehlersuche/Debugging Isac-Tests & 7.6 \\[3pt] \hline\noalign{\smallskip}
    3.64 +21.7.2011
    3.65 + & Alle Fehler in Frontend/interface.sml behoben & 7.6 \\
    3.66 + & Beginn zugeh\"orige Tests auskommentieren & 7.6 \\[3pt] \hline\noalign{\smallskip}
    3.67 +22.7.2011
    3.68 + & Information \"uber Studienrichtungen etc. & 1.1 \\
    3.69 + & Fehlersuche/Debugging Isac-Tests & 6.5 \\[3pt] \hline \hline\noalign{\smallskip}
    3.70 +25.7.2011
    3.71 + & Fehlersuche/Debugging Isac-Tests & 7.6 \\[3pt] \hline\noalign{\smallskip}
    3.72 +26.7.2011
    3.73 + & Beginn: systematisches Aufr\"aumen von auskommentierten Tests & 7.6 \\
    3.74 + & Interpret/appl.sml Interpret/ctree.sml ProgLang/calculate.sml & \\[3pt] \hline\noalign{\smallskip} 
    3.75 +27.7.2011
    3.76 + & Fehlersuche/Debugging Isac-Tests & 7.6 \\[3pt] \hline\noalign{\smallskip}
    3.77 +28.7.2011
    3.78 + & Fehlersuche/Debugging Isac-Tests & 3.6 \\
    3.79 + & Fertigstellung Protokoll         & 4.0 \\[3pt] \hline\noalign{\smallskip}
    3.80 +29.7.2011
    3.81 + & Austausch mit Ferialpraktikanten anderer Studienrichtungen  & 1.0 \\
    3.82 + & Arbeit mit Robotern  & 5.0 \\[3pt] \hline\noalign{\smallskip}
    3.83 +\end{tabular}
    3.84 +\end{center}
    3.85 +Die Arbeiten am Update der Tests sind in das Repository des \isac-Projektes hochgeladen worden und sind auf {\tt https://intra.ist.tugraz.at/hg/isa/} einzusehen.
    3.86 +
    3.87 +
    3.88 +\newpage
    3.89 +\section{R\"uckblick auf das Praktikum}
    3.90 +Meine Erwartungen haben sich gr\"o\3tenteils alle erf\"ullt und ich habe viel Neues dazugelernt:
    3.91 +\begin{itemize}
    3.92 +  \item Grundlagen funktionaler Programmierung (SML)
    3.93 +  \item Zusammenarbeit an einem gro\3sem Softwareprojekt mit mehreren Programmierern (Benutzung von Versionsverwaltungssystemen (Mercurial) , Kommentaren etc.)
    3.94 +  \item Grundz\"uge der Funktionsweise eines Theorem Provers (Isabelle)
    3.95 +  \item ``Test driven development'' - Verifizierung von Softwarekomponenten
    3.96 +  \item schnelle Einarbeitung in neue komplexe Arbeitsumgebungen und Problemstellungen
    3.97 +\end{itemize}
    3.98 +Alles in allem hat sich dieses Praktikum f\"ur mich in jeder Hinsicht gelohnt.
    3.99 +
   3.100 +
   3.101 +
   3.102 +\end{document}
   3.103 +
   3.104 +\message{ !name(ferialprakt.tex) !offset(-78) }

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-isac/chuber/Functions.thy	Tue Sep 17 09:50:52 2013 +0200
     4.3 @@ -0,0 +1,27 @@
     4.4 +theory Functions imports Main begin
     4.5 +
     4.6 +fun fib :: "nat \<Rightarrow> nat"
     4.7 +where
     4.8 +"fib 0 = 1"
     4.9 +| "fib (Suc 0) = 1"
    4.10 +| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
    4.11 +
    4.12 +thm fib.simps
    4.13 +
    4.14 +(*"fib (Suc (Suc n))"*)
    4.15 +
    4.16 +lemma "fib 0 = 1"
    4.17 +by simp
    4.18 +lemma "fib (Suc 0) = 1"
    4.19 +by simp
    4.20 +lemma "fib (Suc (Suc (Suc 0))) = (Suc (Suc (Suc 0)))"
    4.21 +by simp
    4.22 +
    4.23 +(*fun sep :: "’a \<Rightarrow> ’a list \<Rightarrow> ’a list"
    4.24 +where
    4.25 +"sep a (x#y#xs) = x # a # sep a (y # xs)"
    4.26 +| "sep a xs
    4.27 += xs"*)
    4.28 +
    4.29 +
    4.30 +end

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-isac/chuber/bakk_thesis_prelim.tex	Tue Sep 17 09:50:52 2013 +0200
     5.3 @@ -0,0 +1,102 @@
     5.4 +\documentclass[12pt]{article}
     5.5 +\usepackage{a4}
     5.6 +\usepackage{times}
     5.7 +\usepackage{latexsym}
     5.8 +\bibliographystyle{alpha}
     5.9 +%\bibliographystyle{abbrv}
    5.10 +\usepackage{graphicx}
    5.11 +
    5.12 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    5.13 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
    5.14 +
    5.15 +\title{Tentative Title:\\
    5.16 +  Theory of Functional Programming\\
    5.17 +  Introduced by Isabelle and \isac}
    5.18 +\author{n.n\\
    5.19 +{\tt TODO@xxx.at}}
    5.20 +
    5.21 +\begin{document}
    5.22 +\maketitle
    5.23 +%\abstract{
    5.24 +%TODO
    5.25 +%}
    5.26 +
    5.27 +\section{Background}
    5.28 +
    5.29 +``Functional programing'' (FP) is one of the leading paradigms in programming besides ``object oriented programming'' %\cite{?} 
    5.30 +and ``logic (or constraint) programming'' \cite{?}. One advantage of FP are general and elegant approaches to the mathematical theory of programming \cite{?}.
    5.31 +
    5.32 +Presently FP gains importance in face of the ``multi-core crisis'' \cite{?}: functional programs are ready to exploit many cores in parallel. In spite of this fact, at Graz University of Technology (TUG) FP has vanished during recent years, and it is of actual importance to include FP again in education.
    5.33 +
    5.34 +In order to support such education this thesis will compile a course based on advanced tools developed in the intersection between computer science and mathematics: The computer theorem prover Isabelle \cite{Nipkow-Paulson-Wenzel:2002} and the educational math assistant \sisac.
    5.35 +
    5.36 +\section{Goal}
    5.37 +
    5.38 +The goal of this thesis is generation of interactive course material on FP and respective theory of programming, implemented in Isabelle and \sisac.
    5.39 +
    5.40 +The material shall use most recent developments, for instance the ``function package'' \cite{krauss:funs,krauss:termination07,krauss:partial06} recently implemented in Isabelle. This package supports all what is needed for programming and proving properties of programs.
    5.41 +
    5.42 +Although addressing most recent developments and theory at the state of the art, the material also shall serve in early phases of programming. Experience shows, that in early phases (in analogy to doing mathematics \cite{?}) proceeding step by step in a program is important for learning. This will be done by implementing selected programs into \sisac.
    5.43 +
    5.44 +The interactive course material shall serve in certain courses at TUG and in the recently established ``entry and orientation phase'' (Studien-Eingangs und -Orientierungs Phase, STEOP).
    5.45 +
    5.46 +\section{State of the Art}
    5.47 +The thesis cover a wide range of topics some of which will be presented in more detail to be agreed on.
    5.48 +
    5.49 +\paragraph{Theory of functional programming ?}
    5.50 +TODO
    5.51 +
    5.52 +\paragraph{Proof tools for FP}
    5.53 +Isabelle's function package \cite{krauss:funs} is the most advanced in comparison to other provers. It supports two different way of function definitions, one providing full automation (applicable in simple cases) and another featuring interactive proofs of termination.
    5.54 +
    5.55 +The function package covers the full range of FP:  mutual, nested and higher-order recursion, partiality
    5.56 +
    5.57 +The other European computer theorem prover, Coq \cite{}, has less powerful support for FP (TODO)
    5.58 +
    5.59 +\paragraph{Didactics of FP} is concern of very different opinions: At some universities FP is addressed in introductory courses, while at other universities FP is considered an abstract topic addressed in higher semesters. The choice between these extreme alternatives seems to be related to principcal considerations on software construction \cite{aichernig:ingenieur}.
    5.60 +
    5.61 +The planned course might provide a bridge between the alternatives, addressing novices as well as advanced students by employing computer theorem provers.
    5.62 +
    5.63 +\paragraph{Educational math assistants,} if based on computer theorem proving, are appropriate to serve introduction to FP in a specific way: If considering evaluation of functional programs as rewriting, there is an obstacle. Empirical data show that students do not learn to apply rules at high-school --- for instance, the cannot apply the law of distributivity in algebra consciously, they do algebra in the same way they they use their mother language.
    5.64 +
    5.65 +The experimental system \sisac{}\footnote{http://www.ist.tugraz.at/projects/isac/} developed at TU Graz seems appropriate to provide experience in rigorous application of rewrite rules as a prerequisite to understand evaluation in FP.
    5.66 +
    5.67 +
    5.68 +\section{Thesis Structure}
    5.69 +
    5.70 +The main result of this thesis is the interactive course material, accompanied by a thesis.
    5.71 +
    5.72 +\paragraph{The interactive course material} will be implemented as Isabelle theories. Isabelle provides a document preparation system for theories which shall lead for a twofold presentation of the course: as (a) pdf-file(s) and as theories supporting interactive learning.
    5.73 +
    5.74 +For stepwise exercises in \sisac{} an additional Isabelle theory is required, which contains the specifications and programs for the respective exercises in ML-sections.
    5.75 +
    5.76 +\paragraph{The thesis} completes the work as required for a bakkalaureate.
    5.77 +
    5.78 +%general survey on FP
    5.79 +%
    5.80 +%description of the state of the art in proof tools specialized on FP
    5.81 +%
    5.82 +%didactic consideration about the course (what has been omitted, ...)
    5.83 +%
    5.84 +%future work, probably extending the course to more advanced topics
    5.85 +%
    5.86 +%future work, extending the course to more elementary topics, probably usable at high school
    5.87 +%
    5.88 +%...
    5.89 +%
    5.90 +%... 
    5.91 +
    5.92 +
    5.93 +\section{Timeline}
    5.94 +
    5.95 +The main work shall be done during this summer as much as possible.
    5.96 +
    5.97 +%Milestones
    5.98 +%\subsection{TODO}
    5.99 +%study introductory material for Isabelle; contact Alexander Kraus and others for similar course material
   5.100 +%
   5.101 +%\subsection{TODO}
   5.102 +%\sisac =''=
   5.103 +
   5.104 +\bibliography{references}
   5.105 +\end{document}

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-isac/chuber/references.bib	Tue Sep 17 09:50:52 2013 +0200
     6.3 @@ -0,0 +1,55 @@
     6.4 +
     6.5 +@InCollection{krauss:partial06,
     6.6 +  author = 	 {Alexander Krauss},
     6.7 +  title = 	 {Partial recursive functions in higher-order logic},
     6.8 +  booktitle = 	 {Automated Reasoning (IJCAR 2006)},
     6.9 +  pages = 	 {589-603},
    6.10 +  publisher = {Springer Verlag},
    6.11 +  year = 	 {2006},
    6.12 +  editor = 	 {Ulrich Furbach and Natarajan Shankar},
    6.13 +  volume = 	 {4130},
    6.14 +  series = 	 {Lecture Notes in Artificial Intelligence},
    6.15 +  doi = {http://dx.doi.org/10.1007/11814771_48}
    6.16 +}
    6.17 +
    6.18 +@InCollection{krauss:termination07,
    6.19 +  author = 	 {Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow},
    6.20 +  title = 	 {Finding lexicographic orders for termination proofs in Isabelle/HOL},
    6.21 +  booktitle = 	 {Theorem Proving in Higher Order Logics (TPHOLs 2007)},
    6.22 +  pages = 	 {38-53},
    6.23 +  publisher = {Springer Verlag},
    6.24 +  year = 	 {2007},
    6.25 +  editor = 	 {Schneider and J. Brandt},
    6.26 +  volume = 	 {4732},
    6.27 +  series = 	 {Lecture Notes in Computer Science},
    6.28 +  doi = {http://dx.doi.org/10.1007/978-3-540-74591-4_5}
    6.29 +}
    6.30 +
    6.31 +@Article{aichernig:ingenieur,
    6.32 +  author = 	 {Bernhard K. Aichernig and Peter Lucas},
    6.33 +  title = 	 {Softwareentwicklung --- eine {I}ngenieursdisziplin!(?)},
    6.34 +  journal = 	 {Telematik, Zeitschrift des Telematik-Ingenieur-Verbandes (TIV)},
    6.35 +  year = 	 {1998},
    6.36 +  volume = 	 {4},
    6.37 +  number = 	 {2},
    6.38 +  pages = 	 {2-8},
    6.39 +  note = 	 {http://www.ist.tu-graz.ac.at/publications},
    6.40 +  annote = 	 {}
    6.41 +}
    6.42 +
    6.43 +@Book{Nipkow-Paulson-Wenzel:2002,
    6.44 +  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
    6.45 +  title		= {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
    6.46 +  publisher	= {Springer},
    6.47 +  series	= {LNCS},
    6.48 +  volume	= 2283,
    6.49 +  year		= 2002
    6.50 +}
    6.51 +@PhdThesis{krauss:funs,
    6.52 +  author = 	 {Alexander Krauss},
    6.53 +  title = 	 {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
    6.54 +  school = 	 {Technische Universit\"at M\"unchen},
    6.55 +  year = 	 {2009},
    6.56 +  OPTnote = 	 {http://www4.in.tum.de/~krauss/diss/}
    6.57 +}
    6.58 +

     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/doc-isac/dmeindl/Hauptdatei.tex	Tue Sep 17 09:50:52 2013 +0200
     7.3 @@ -0,0 +1,168 @@
     7.4 +\documentclass[12pt,a4paper]{article}
     7.5 +\usepackage{a4}
     7.6 +\usepackage[naustrian]{babel}
     7.7 +\usepackage[latin1]{inputenc}
     7.8 +\usepackage{calc}
     7.9 +\usepackage{amsmath}   
    7.10 +\usepackage{epsfig}
    7.11 +\usepackage{graphicx}
    7.12 +\usepackage{xcolor}
    7.13 +\usepackage{amsfonts}
    7.14 +
    7.15 +
    7.16 +% Seitenr�der einstellen und H�he der Seitenzahlen
    7.17 +\usepackage{geometry}
    7.18 +\geometry{a4paper, left=2.5cm, right=2cm, top=3cm, bottom=2.8cm}
    7.19 +\setlength{\footskip}{2cm}
    7.20 +
    7.21 +
    7.22 +\newcommand{\R}{\mathbb R}
    7.23 +%\newcommand{\N}{\mathbb N}
    7.24 +%\newcommand{\Q}{\mathbb Q}
    7.25 +%\newcommand{\C}{\mathbb C}
    7.26 +
    7.27 +%Z�hler definieren und Starwert setzen:
    7.28 +\newcounter{ctr}
    7.29 +\setcounter{ctr}{0}
    7.30 +
    7.31 +\newcounter{Teubner}
    7.32 +\newcounter{Klingenberg}
    7.33 +\newcounter{T}
    7.34 +\newcounter{Vo}
    7.35 +\newcounter{Se}
    7.36 +\newcounter{E}
    7.37 +\newcounter{Bwl}
    7.38 +\newcounter{Int}
    7.39 +\newcounter{Prim}
    7.40 +\newcounter{Z}
    7.41 +\setcounter{Z}{0}
    7.42 +\setcounter{Teubner}{1}
    7.43 +\setcounter{Klingenberg}{2}
    7.44 +\setcounter{T}{1}
    7.45 +\setcounter{Vo}{7}
    7.46 +\setcounter{Se}{2}
    7.47 +\setcounter{E}{3}
    7.48 +\setcounter{Bwl}{4}
    7.49 +\setcounter{Int}{5}
    7.50 +\setcounter{Prim}{6}
    7.51 +
    7.52 +%BSP
    7.53 +\newenvironment{myBsp}{
    7.54 +  \begin{list}{\textbf{\textsc{Bsp:}}}{
    7.55 +    \setlength{\labelwidth}{8Pc}
    7.56 +    \setlength{\labelsep}{0.5Pc}    
    7.57 +    \setlength{\rightmargin}{0Pc}
    7.58 +    \setlength{\leftmargin}{2Pc}
    7.59 +    \setlength{\parsep}{0ex plus 0.5ex}
    7.60 +    \setlength{\listparindent}{1em}
    7.61 +    \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
    7.62 +    \setlength{\topsep}{0.5Pc}
    7.63 +  }}
    7.64 +  {\end{list}
    7.65 +}
    7.66 +
    7.67 +
    7.68 +%Lemma
    7.69 +\newenvironment{myLemma}{
    7.70 +  \begin{list}{\textsc{\textbf{Lemma:\ \ \ }}}{
    7.71 +   \setlength{\labelsep}{-0.5Pc}    
    7.72 +    \setlength{\leftmargin}{1Pc}
    7.73 +    \setlength{\parsep}{0ex plus 0.5ex}
    7.74 +    \setlength{\listparindent}{1em}
    7.75 +    \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
    7.76 +    \setlength{\topsep}{0.5Pc}
    7.77 +  }}
    7.78 +  {\end{list}
    7.79 +}
    7.80 +%Korollar
    7.81 +\newenvironment{myKorollar}{
    7.82 +  \begin{list}{\textsc{\textbf{Korollar: }}}{
    7.83 +    \setlength{\labelwidth}{8Pc}
    7.84 +    \setlength{\labelsep}{0.5Pc}    
    7.85 +    \setlength{\rightmargin}{0Pc}
    7.86 +    \setlength{\leftmargin}{4Pc}
    7.87 +    \setlength{\parsep}{0ex plus 0.5ex}
    7.88 +    \setlength{\listparindent}{1em}
    7.89 +    \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
    7.90 +    \setlength{\topsep}{0.5Pc}
    7.91 +  }}
    7.92 +  {\end{list}
    7.93 +}
    7.94 +
    7.95 +%Theorem
    7.96 +\newenvironment{myTheorem}{
    7.97 +  \begin{list}{\textsc{\textbf{Theorem: }}}{
    7.98 +    \setlength{\labelwidth}{8Pc}
    7.99 +    \setlength{\labelsep}{0.5Pc}    
   7.100 +    \setlength{\rightmargin}{0Pc}
   7.101 +    \setlength{\leftmargin}{5Pc}
   7.102 +    \setlength{\parsep}{0ex plus 0.5ex}
   7.103 +    \setlength{\listparindent}{1em}
   7.104 +    \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
   7.105 +    \setlength{\topsep}{0.5Pc}
   7.106 +  }}
   7.107 +  {\end{list}
   7.108 +}
   7.109 +
   7.110 +
   7.111 +%Proportion
   7.112 +\newenvironment{myProp}{
   7.113 +  \begin{list}{\textsc{\textbf{Proportion: }}}{
   7.114 +    \setlength{\labelwidth}{8Pc}
   7.115 +    \setlength{\labelsep}{0.5Pc}    
   7.116 +    \setlength{\rightmargin}{0Pc}
   7.117 +    \setlength{\leftmargin}{4Pc}
   7.118 +    \setlength{\parsep}{0ex plus 0.5ex}
   7.119 +    \setlength{\listparindent}{1em}
   7.120 +    \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
   7.121 +    \setlength{\topsep}{0.5Pc}
   7.122 +  }}
   7.123 +  {\end{list}
   7.124 +}
   7.125 +
   7.126 +%Farben
   7.127 +
   7.128 +\newcommand{\red}[1]{\textcolor[rgb]{0.7,0,0}{\bf #1}}
   7.129 +\newcommand{\rd}[1]{\color{red}{#1}}
   7.130 +\newcommand{\white}[1]{\textcolor[rgb]{1,0,0}{\bf #1}}
   7.131 +\newcommand{\w}[1]{\color{white}{#1}}
   7.132 +\newcommand{\g}[1]{\color{myColor}{#1}}
   7.133 +
   7.134 +\usepackage{color}
   7.135 +\definecolor{myColor}{rgb}{0.9,0.9,0.9}% Wir definieren im RGB-Farbraum
   7.136 +
   7.137 +
   7.138 +\newcommand{\myDef}[1]{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\w .}\\[-0.2cm]\textbf{Definition\ \Nummer:}\\#1}}
   7.139 +\newcommand{\mySatz}[2]{\colorbox{myColor}{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\g .}\\[-0.2cm]\textbf{Satz\ \Nummer:}\ #1\\ #2}}}
   7.140 +\newcommand{\myBeweis}[1]{\textit{\textbf{Beweis:}\\ #1}}
   7.141 +\newcommand{\myAlg}[2]{\parbox{\columnwidth}{\addtocounter{ctr}{1}\textbf{Algorithmus\ \Nummer:}\ \ #1\\#2}}
   7.142 +\newcommand{\myProg}[1]{\fbox{\parbox{\columnwidth}{#1}}}
   7.143 +
   7.144 +\newcommand{\add}[1]{\addtocounter{#1}{1}}
   7.145 +\newcommand{\zahl}[1]{\setcounter{#1}{Z}}
   7.146 +\newcommand{\Q}[2]{\parbox{\columnwidth}{$^{[\arabic{#1}/#2]}$ }}
   7.147 +
   7.148 +\newcommand{\Nummer}{\thesection.\arabic{ctr}}
   7.149 +
   7.150 +%------------------------------------------------------------- Beginn -----------------------------------------------------------------------
   7.151 +
   7.152 +\title{Greates common divisor \\ for multivariable Polynomials}
   7.153 +\author{By\\Diana Meindl\\meindl$_-$diana@yahoo.com}
   7.154 +\date{}
   7.155 +
   7.156 +\begin{document}
   7.157 +\maketitle
   7.158 +{\w .}\\[12cm]
   7.159 +\begin{center}
   7.160 +Presented to \\
   7.161 +A.Univ.Prof. Dipl.-Ing. Dr. Wolfgang Schreiner (RISC Insitute)\\
   7.162 +and\\
   7.163 +Dr. techn. Walther Neuper (Institut f�r Softwaretechnologie, TU Graz)
   7.164 +\end{center}
   7.165 +\newpage
   7.166 +%\tableofcontents
   7.167 +\newpage
   7.168 +\input{proposal}
   7.169 +\newpage
   7.170 +
   7.171 +\end{document}
   7.172 \ No newline at end of file

     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/doc-isac/dmeindl/proposal.tex	Tue Sep 17 09:50:52 2013 +0200
     8.3 @@ -0,0 +1,504 @@
     8.4 +%WN mit diesen 3 Zeichen beginnen meine Kommentare
     8.5 +%WN111107: bitte spellchecker dr"uberlaufen lassen !!!
     8.6 +
     8.7 +\documentclass[12pt,a4paper]{article}
     8.8 +\bibliographystyle{alpha}
     8.9 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    8.10 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
    8.11 +%\usepackage{a4}
    8.12 +%\usepackage[naustrian]{babel}
    8.13 +%\usepackage[latin1]{inputenc}
    8.14 +%\usepackage{calc}
    8.15 +%\usepackage{amsmath}   
    8.16 +%\usepackage{epsfig}
    8.17 +%\usepackage{graphicx}
    8.18 +%\usepackage{xcolor}
    8.19 +%\usepackage{amsfonts}
    8.20 +%
    8.21 +%WN BITTE DIESE DEFINITIONEN WEGLASSEN ...
    8.22 +%% Seitenr�der einstellen und H�he der Seitenzahlen
    8.23 +%\usepackage{geometry}
    8.24 +%\geometry{a4paper, left=2.5cm, right=2cm, top=3cm, bottom=2.8cm}
    8.25 +%\setlength{\footskip}{2cm}
    8.26 +%
    8.27 +%
    8.28 +%%Z�hler definieren und Starwert setzen:
    8.29 +%\newcommand{\R}{\mathbb R}
    8.30 +%%\newcommand{\N}{\mathbb N}
    8.31 +%%\newcommand{\Q}{\mathbb Q}
    8.32 +%%\newcommand{\C}{\mathbb C}
    8.33 +%
    8.34 +%
    8.35 +%\newcounter{ctr}
    8.36 +%\setcounter{ctr}{0}
    8.37 +%
    8.38 +%\newcounter{Teubner}
    8.39 +%\newcounter{Klingenberg}
    8.40 +%\newcounter{T}
    8.41 +%\newcounter{Vo}
    8.42 +%\newcounter{Se}
    8.43 +%\newcounter{E}
    8.44 +%\newcounter{Bwl}
    8.45 +%\newcounter{Int}
    8.46 +%\newcounter{Prim}
    8.47 +%\newcounter{Z}
    8.48 +%\setcounter{Z}{0}
    8.49 +%\setcounter{Teubner}{1}
    8.50 +%\setcounter{Klingenberg}{2}
    8.51 +%\setcounter{T}{1}
    8.52 +%\setcounter{Vo}{7}
    8.53 +%\setcounter{Se}{2}
    8.54 +%\setcounter{E}{3}
    8.55 +%\setcounter{Bwl}{4}
    8.56 +%\setcounter{Int}{5}
    8.57 +%\setcounter{Prim}{6}
    8.58 +%%BSP
    8.59 +%\newenvironment{myBsp}{
    8.60 +%  \begin{list}{\textbf{\textsc{Bsp:}}}{
    8.61 +%    \setlength{\labelwidth}{8Pc}
    8.62 +%    \setlength{\labelsep}{0.5Pc}    
    8.63 +%    \setlength{\rightmargin}{0Pc}
    8.64 +%    \setlength{\leftmargin}{2Pc}
    8.65 +%    \setlength{\parsep}{0ex plus 0.5ex}
    8.66 +%    \setlength{\listparindent}{1em}
    8.67 +%    \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
    8.68 +%    \setlength{\topsep}{0.5Pc}
    8.69 +%  }}
    8.70 +%  {\end{list}
    8.71 +%}
    8.72 +%
    8.73 +%
    8.74 +%%Lemma
    8.75 +%\newenvironment{myLemma}{
    8.76 +%  \begin{list}{\textsc{\textbf{Lemma:\ \ \ }}}{
    8.77 +%   \setlength{\labelsep}{-0.5Pc}    
    8.78 +%    \setlength{\leftmargin}{1Pc}
    8.79 +%    \setlength{\parsep}{0ex plus 0.5ex}
    8.80 +%    \setlength{\listparindent}{1em}
    8.81 +%    \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
    8.82 +%    \setlength{\topsep}{0.5Pc}
    8.83 +%  }}
    8.84 +%  {\end{list}
    8.85 +%}
    8.86 +%%Korollar
    8.87 +%\newenvironment{myKorollar}{
    8.88 +%  \begin{list}{\textsc{\textbf{Korollar: }}}{
    8.89 +%    \setlength{\labelwidth}{8Pc}
    8.90 +%    \setlength{\labelsep}{0.5Pc}    
    8.91 +%    \setlength{\rightmargin}{0Pc}
    8.92 +%    \setlength{\leftmargin}{4Pc}
    8.93 +%    \setlength{\parsep}{0ex plus 0.5ex}
    8.94 +%    \setlength{\listparindent}{1em}
    8.95 +%    \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
    8.96 +%    \setlength{\topsep}{0.5Pc}
    8.97 +%  }}
    8.98 +%  {\end{list}
    8.99 +%}
   8.100 +%
   8.101 +%%Theorem
   8.102 +%\newenvironment{myTheorem}{
   8.103 +%  \begin{list}{\textsc{\textbf{Theorem: }}}{
   8.104 +%    \setlength{\labelwidth}{8Pc}
   8.105 +%    \setlength{\labelsep}{0.5Pc}    
   8.106 +%    \setlength{\rightmargin}{0Pc}
   8.107 +%    \setlength{\leftmargin}{5Pc}
   8.108 +%    \setlength{\parsep}{0ex plus 0.5ex}
   8.109 +%    \setlength{\listparindent}{1em}
   8.110 +%    \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
   8.111 +%    \setlength{\topsep}{0.5Pc}
   8.112 +%  }}
   8.113 +%  {\end{list}
   8.114 +%}
   8.115 +%
   8.116 +%
   8.117 +%%Proportion
   8.118 +%\newenvironment{myProp}{
   8.119 +%  \begin{list}{\textsc{\textbf{Proportion: }}}{
   8.120 +%    \setlength{\labelwidth}{8Pc}
   8.121 +%    \setlength{\labelsep}{0.5Pc}    
   8.122 +%    \setlength{\rightmargin}{0Pc}
   8.123 +%    \setlength{\leftmargin}{4Pc}
   8.124 +%    \setlength{\parsep}{0ex plus 0.5ex}
   8.125 +%    \setlength{\listparindent}{1em}
   8.126 +%    \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
   8.127 +%    \setlength{\topsep}{0.5Pc}
   8.128 +%  }}
   8.129 +%  {\end{list}
   8.130 +%}
   8.131 +%
   8.132 +%%Farben
   8.133 +%
   8.134 +%\newcommand{\red}[1]{\textcolor[rgb]{0.7,0,0}{\bf #1}}
   8.135 +%\newcommand{\rd}[1]{\color{red}{#1}}
   8.136 +%\newcommand{\white}[1]{\textcolor[rgb]{1,0,0}{\bf #1}}
   8.137 +%\newcommand{\w}[1]{\color{white}{#1}}
   8.138 +%\newcommand{\g}[1]{\color{myColor}{#1}}
   8.139 +%
   8.140 +%\usepackage{color}
   8.141 +%\definecolor{myColor}{rgb}{0.9,0.9,0.9}% Wir definieren im RGB-Farbraum
   8.142 +%
   8.143 +%
   8.144 +%\newcommand{\myDef}[1]{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\w .}\\[-0.2cm]\textbf{Definition\ \Nummer:}\\#1}}
   8.145 +%\newcommand{\mySatz}[2]{\colorbox{myColor}{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\g .}\\[-0.2cm]\textbf{Satz\ \Nummer:}\ #1\\ #2}}}
   8.146 +%\newcommand{\myBeweis}[1]{\textit{\textbf{Beweis:}\\ #1}}
   8.147 +%\newcommand{\myAlg}[2]{\parbox{\columnwidth}{\addtocounter{ctr}{1}\textbf{Algorithmus\ \Nummer:}\ \ #1\\#2}}
   8.148 +%\newcommand{\myProg}[1]{\fbox{\parbox{\columnwidth}{#1}}}
   8.149 +%
   8.150 +%\newcommand{\add}[1]{\addtocounter{#1}{1}}
   8.151 +%\newcommand{\zahl}[1]{\setcounter{#1}{Z}}
   8.152 +%\newcommand{\Q}[2]{\parbox{\columnwidth}{$^{[\arabic{#1}/#2]}$ }}
   8.153 +%
   8.154 +%\newcommand{\Nummer}{\thesection.\arabic{ctr}}
   8.155 +%
   8.156 +%---------- --------------------------------------------------- Beginn -----------------------------------------------------------------------
   8.157 +
   8.158 +\title{Greatest Common Divisor \\ for Multivariate Polynomials}
   8.159 +\author{Diana Meindl\\meindl\_diana@yahoo.com}
   8.160 +\date{\today}
   8.161 +
   8.162 +\begin{document}
   8.163 +\maketitle
   8.164 +%{\w .}\\[12cm]
   8.165 +%\begin{center}
   8.166 +%Presented to \\
   8.167 +%A.Univ.Prof. Dipl.-Ing. Dr. Wolfgang Schreiner (RISC Insitute)\\
   8.168 +%and\\
   8.169 +%Dr. techn. Walther Neuper (Institut f�r Softwaretechnologie, TU Graz)
   8.170 +%\end{center}
   8.171 +%\newpage
   8.172 +%{\w .}\hspace{6.5cm}\textbf{Abstact}\\[0.5cm]
   8.173 +
   8.174 +\abstract{
   8.175 +This is a proposal for a Masters Thesis at RISC, the Research Institute for Symbolic Computation at Linz University.\\
   8.176 +
   8.177 +Calculation with fractions is an important part of Computer Algebra Systems (CAS). This proposal aims at a specific part of such calculations, the greatest common divisor (GCD) used for cancellation, but in the very general context of multivariate polynomials. Cancellation of multivariate polynomials is a settled topic in Computer Algebra, respective algorithms well documented and implementations available in all CASs.
   8.178 +
   8.179 +This proposal claims for novelty with respect to the context of implementation, an implementation as a CAS-feature in Computer Theorem Proving (CTP). On CTP's present development towards industrial use in software and systems verification, specific domain models involve demand on more and more mathematics, and within mathematics involve demand for more and more features. Thus the proposed implementation of GCD and cancellation follows an actual demand.
   8.180 +
   8.181 +If the implementation is successful, it is planned to be included into the distribution of Isabelle, one of the two dominating CTPs in Europe. As part of the Isabelle distribution it will also serve the {\sisac} project aiming at an educational math assistant under development at RISC Linz and Graz University of Technology.
   8.182 +}
   8.183 +
   8.184 +\newpage
   8.185 +%WN vorerst zu Zwecken der "Ubersicht lassen ...
   8.186 +\tableofcontents
   8.187 +
   8.188 +\section{Background}
   8.189 +The \sisac-project is a research and development project launched at the Institute for Software Technology of the Graz University of Technology (TUG) and now continued at the Research Institute for Symbolic Computation (RISC) of University of Linz and at the Institute for Information Systems and Computer Media (IICM) of TUG. The resulting \sisac{} prototype is a ``transparent single-stepping system for applied mathematics'' based on the computer theorem prover Isabelle. The prototype has been proven useful in field tests at Austrain schools \cite{imst-htl06-SH,imst-htl07-SH,imst-hpts08-SH} and is now extended for wider use.
   8.190 +
   8.191 +Authoring knowledge in \sisac{} provides a strict separation of concerns between authoring math knowledge and authoring dialogues. The latter is pursued at IICM, the former is concern of this thesis. Math authoring is done by use of a CTP-based programming language \cite{plmms10} or by use of SML \cite{pl:milner97} as the meta language and implementation language of Isabelle. Since the code resulting from this thesis shall serve Isabelle, it will be written in SML. Via Isabelle distribution this thesis shall also serve \sisac; a re-implementation in \sisac's CTP-based language is planned as a subsequent project -- this will make cancellation transparent for singe-stepping.
   8.192 +
   8.193 +%The special is an easy readable knowledge base including Isabelles HOL-theories and a transparently working knowledge interpreter (a generalization of 'single stepping' algebra systems).
   8.194 +%The background to both, development and research, is given by actual needs in math education as well as by foundamental questions about 'the mechanization of thinking' as an essential aspect in mathematics and in technology.
   8.195 +%The \sisac-system under construction comprises a tutoring-system and an authoring-system. The latter provides for adaption to various needs of individual users and educational institutions and for extensions to arbitrary fields of applied mathematics.
   8.196 +
   8.197 +TODO.WN111107 bitte googeln und je einen Absatz kopieren + zitieren woher (PLAGIATsgefahr):\\
   8.198 +European provers: Isabelle \cite{Nipkow-Paulson-Wenzel:2002}, Coq \cite{Huet_all:94}\\
   8.199 +American provers: PVS~\cite{pvs}, ACL2~\footnote{http://userweb.cs.utexas.edu/~moore/acl2/}\\
   8.200 +
   8.201 +\section{Goal of the thesis}
   8.202 +\subsection{Current situation}
   8.203 +At the presetn time there is no implimentation for the problem of canceling fractions in Isabelle, and a deficient one in \sisac. But because canceling is important for calculating with fractions a new implimentation is necessary.
   8.204 +
   8.205 +\subsection{Problem} 
   8.206 +The wish is to handle fractions in \sisac{} not only in one variable also in more. So the goal of this thesis ist to find, assess and evaluate the existing algorithms and methods for finding the GCD. This will be an functional programm with the posibility to include it into Isabelle, where it will be used by \sisac{} as well.
   8.207 +
   8.208 +%WN eine pr"azisere Beschreibung des Problems kann ich mir nicht vorstellen (englische Version der Mail haben wir auch, aber sie passt nicht zur deutschen Antwort von Prof.Nipkow) ...
   8.209 +\bigskip
   8.210 +A mail to Prof. Nipkow, leader of the development of Isabelle \cite{Nipkow-Paulson-Wenzel:2002} at TU M\"unchen, Mon, 23 May 2011 08:58:14 +0200 describes the problem as follows:
   8.211 +\begin{verbatim}
   8.212 +Eine erste Idee, wie die Integration der Diplomarbeit f"ur
   8.213 +einen Benutzer von Isabelle aussehen k"onnte, w"are zum 
   8.214 +Beispiel im
   8.215 +
   8.216 +   lemma cancel:
   8.217 +     assumes asm3: "x2 - x*y \<noteq> 0" and asm4: "x \<noteq> 0"
   8.218 +     shows "(x2 - y2) / (x2 - x*y) = (x + y) / (x::real)"
   8.219 +     apply (insert asm3 asm4)
   8.220 +     apply simp
   8.221 +   sorry
   8.222 +
   8.223 +die Assumptions
   8.224 +
   8.225 +   asm1: "(x2 - y2) = (x + y) * (x - y)" and asm2: "x2 - x*y = x * (x - y)"
   8.226 +
   8.227 +im Hintergrund automatisch zu erzeugen (mit der Garantie, 
   8.228 +dass "(x - y)" der GCD ist) und sie dem Simplifier (f"ur die 
   8.229 +Rule nonzero_mult_divide_mult_cancel_right) zur Verf"ugung zu 
   8.230 +stellen, sodass anstelle von "sorry" einfach "done" stehen kann.
   8.231 +Und weiters w"are eventuell asm3 zu "x - y \<noteq> 0" zu vereinfachen, 
   8.232 +eine Rewriteorder zum Herstellen einer Normalform festzulegen, etc.
   8.233 +\end{verbatim}
   8.234 +%WN und eine bessere Motivation f"ur eine Master Thesis kann ich mir auch nicht vorstellen ...
   8.235 +Response of Prof. Nipkow:
   8.236 +
   8.237 +\begin{verbatim}
   8.238 +Unser Spezialist fuer die mathematischen Theorien ist Johannes H"olzl. 
   8.239 +Etwas allgemeinere Fragen sollten auf jeden Fall an isabelle-dev@ 
   8.240 +gestellt werden.
   8.241 +
   8.242 +Viel Erfolg bei der Arbeit!
   8.243 +Tobias Nipkow
   8.244 +\end{verbatim}
   8.245 +
   8.246 +
   8.247 +\subsection{Expected results}
   8.248 +Implementation of algorithms for the different problems, and find out which one will be the best for the specific requirements in Isabelle.\\
   8.249 +The program should accomplish:
   8.250 +\begin{itemize}
   8.251 +\item Real and rational coefficients. Maybe also imaginary coefficients.
   8.252 +\item Canceling and adding multivariate polynomials, when they are in normal form.
   8.253 +\end{itemize}
   8.254 +The program will be written in the functional programming language SML with appropriate comments. The resulting code shall meet the coding standards of Isabelle \cite{isar-impl} p.3-10. The integration of the code into the Isabelle distribution will be done by the Isabelle developer team.
   8.255 +
   8.256 +\section{State of the art}
   8.257 +In a broad view the context of this thesis can be seen as ``computation and deduction'': simplification and in particular cancellation of rational terms is concern of \textbf{computation} implemented in Computer Algebra Systems (CAS) --- whereas the novelty within the thesis is given by an implementation of cancellation in a computer theorem prover (CTP), i.e. in the domain of \textbf{deduction} with respective logical rigor not addressed in the realm of CAS.
   8.258 +
   8.259 +Below, after a general survey on computation, represented by CAS, and on deduction, represented by CTP, a more narrow view on ``CAS-functionality in CTP'' is pursued.
   8.260 +
   8.261 +\subsection{Computer Algebra and Proof Assistants}
   8.262 +%WN achtung: diese subsection is fast w"ortlich kopiert aus \cite{plmms10} -- also in der Endfassung bitte "uberarbeiten !!!
   8.263 +Computer Algebra and Proof Assistants have coexisted for a many years so there is much research trying to bridge the gap between these approaches from both sides. We shall continue to abbreviate Computer Algebra (Systems) by ``CAS'', and in analogy we shall abbreviate proof assistants by CTP, computer theorem provig (comprising both, interactive theorem proving (ITP) and automated theorem proving (ATP), since in CTP there are ATP-tools included today.)
   8.264 +
   8.265 +First, many CTPs already have CAS-like functionality,
   8.266 +especially for domains like arithmetic. They provide the user
   8.267 +with conversions, tactics or decision procedures that solve
   8.268 +problems in a particular domain. Such decision procedures present
   8.269 +in the standard library of HOL Light~\footnote{http://www.cl.cam.ac.uk/~jrh13/hol-light/} are used inside the
   8.270 +prototype described in Sect.\ref{cas-funct} on p.\pageref{part-cond} for arithmetic's,
   8.271 +symbolic differentiation and others.
   8.272 +
   8.273 +Similarly some CAS systems provide environments that allow
   8.274 +logical reasoning and proving properties within the system. Such
   8.275 +environments are provided either as logical
   8.276 +extensions (e.g.~\cite{logicalaxiom}) or are implemented within a
   8.277 +CAS using its language~\cite{theorema00}.
   8.278 +
   8.279 +There are numerous architectures for information exchange between
   8.280 +CAS and CTP with different levels of \emph{degree of trust}
   8.281 +between the prover and the CAS. In principle, there are several approaches. 
   8.282 +If CAS-functionality is not fully embedded in CTP, CAS can be called as ``oracles'' nevertheless (for efficiency reasons, in general) --- their results are regarded like prophecies of Pythia in Delphi. There are three kinds of checking oracles, however:
   8.283 +\begin{enumerate}
   8.284 +\item Just adopt the CAS result without any check. Isabelle internally marks such results.
   8.285 +\item Check the result inside CTP. There are many cases, where such checks are straight forward, for instance, checking the result of factorization by multiplication of the factors, or checking integrals by differentiation.
   8.286 +\item Generate a derivation of the result within CTP; in Isabelle this is called ``proof reconstruction''.
   8.287 +\end{enumerate}
   8.288 +A longer list of frameworks for
   8.289 +information exchange and bridges between systems can be found
   8.290 +in~\cite{casproto}.
   8.291 +
   8.292 +There are many approaches to defining partial functions in proof
   8.293 +assistants. Since we would like the user to define functions
   8.294 +without being exposed to the underlying logic of the proof
   8.295 +assistant we only mention some automated mechanisms for defining
   8.296 +partial functions in the logic of a CTP.
   8.297 +Krauss~\cite{krauss} has developed a framework for defining
   8.298 +partial recursive functions in Isabelle/HOL, which formally
   8.299 +proves termination by searching for lexicographic combinations of
   8.300 +size measures. Farmer~\cite{farmer} implements a scheme for
   8.301 +defining partial recursive functions in \textrm{IMPS}.
   8.302 +
   8.303 +\subsection{Motivation for CAS-functionality in CTP}
   8.304 +In the realm of CTP formuas are dominated by quantifiers $\forall$, $\exists$ and $\epsilon$ (such) and by operations like $\Rightarrow$, $\land$ and $\lor$. Numbers were strangers initially; numerals have been introduced to Isabelle not much before the year 2000~\footnote{In directory src/Provers/Arith/ see the files cancel\_numerals.ML and cancel\_numeral\_factor.ML in the Isabelle distribution 2011. They still use the notation $\#1,\#2,\#3,\dots$ from before 2000~!}. However, then numerals have been implemented with {\em polymorphic type} such that $2\cdot r\cdot\pi$ ($2$ is type \textit{real}) and $\pi_{\it approx}=3.14\,\land\, 2\cdot r\cdot\pi_{\it approx}$ can be written as well as $\sum_i^n i=\frac{n\cdot(n+1)}{2}$ ($2$ is type \textit{nat}). The different types are inferred by Hindle-Milner type inference \cite{damas-milner-82,Milner-78,Hindley-69}.
   8.305 +
   8.306 +1994 was an important year for CTP: the Pentium Bug caused excitement in the IT community all around the world and motivated INTEL to invest greatly into formal verification of circuits (which carried over to verification of software). Not much later John Harrison mechanized real numbers as Dedekind Cuts in HOL Light \footnote{http://www.cl.cam.ac.uk/~jrh13/hol-light/} and derived calculus, derivative and integral from that definition \cite{harr:thesis}, an implementation which has been transferred to Isabelle very soon after that~\footnote{In the directory src/HOL/Multivariate\_Analysis/ see the files Gauge\_Measure.thy, Integration.thy, Derivative.thy, Real\_Integration.thy, Brouwer\_Fixpoint.thy, Fashoda.thy}.
   8.307 +
   8.308 +Harrison also says that ``CAS are ill-defined'' and gives, among others, an example relevant for this thesis on cancellation: TODO.WN111104 search for ... meromorphic functions in http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-428.ps.gz
   8.309 +
   8.310 +\medskip
   8.311 +The main motivation for further introduction of CAS-functionality to CTP is also technology-driven: In this decade domain engineering is becoming an academic discipline with industrial relevance \cite{db:dom-eng}: vigorous efforts extend the scope of formal specifications even beyond software technology, and thus respective domains of mathematical knowledge are being mechanized in CTP. The Archive of Formal Proofs~\footnote{http://afp.sourceforge.net/} is Isabelle's repository for such work.
   8.312 +
   8.313 +\subsection{Simplification within CTP}
   8.314 +Cancellation, the topic of this thesis, is a specific part of simplification of rationals. In the realm of CAS cancellation is {\em not} an interesting part of the state of the art, because cancellation has been implemented in the prevailing CAS more than thirty years ago --- however, cancellation of multivariate polynomials is {\em not} yet implemted in any of the dominating CTPs.
   8.315 +%WN: bitte mit Anfragen an die Mailing-Listen nachpr"ufen: Coq, HOL, ACL2, PVS
   8.316 +
   8.317 +As in other CTPs, in Isabelle the simplifier is a powerful software component; the sets of rewrite rules, called \textit{simpsets}, contain several hundreds of elements. Rewriting is still very efficient, because the simpsets are transformed to term nets \cite{term-nets}.
   8.318 +
   8.319 +Rational terms of multivariate polynomials still have a normal form \cite{bb-loos} and thus equivalence of respective terms is decidable. This is not the case, however, with terms containing roots or transcedent functions. Thus, CAS are unreliable by design in these cases.
   8.320 +
   8.321 +In CTP, simplification of non-decidable domains is already an issue, as can be seem in the mail with subject ``simproc divide\_cancel\_factor produces error'' in the mailing-list \textit{isabelle-dev@mailbroy.informatik.tu-muenchen.de} from Thu, 15 Sep 2011 16:34:12 +0200
   8.322 +{%\footnotesize --- HILFT NICHTS
   8.323 +\begin{verbatim}
   8.324 +Hi everyone,
   8.325 +
   8.326 +in the following snippet, applying the simplifier causes an error:
   8.327 +
   8.328 +------------------------------------------
   8.329 +theory Scratch
   8.330 +  imports Complex_Main
   8.331 +begin
   8.332 +
   8.333 +lemma
   8.334 +  shows "(3 / 2) * ln n = ((6 * k * ln n) / n) * ((1 / 2 * n / k) / 2)"
   8.335 +apply simp
   8.336 +------------------------------------------
   8.337 +
   8.338 +outputs
   8.339 +
   8.340 +------------------------------------------
   8.341 +Proof failed.
   8.342 +(if n = 0 then 0 else 6 * (k * ln n) / 1) * 2 / (4 * k) =
   8.343 +2 * (Numeral1 * (if n = 0 then 0 else 6 * (k * ln n) / 1)) / (2 * (2 * k))
   8.344 + 1. n \not= Numeral0 \rightarrow k * (ln n * (2 * 6)) / (k * 4) = k * (ln n * 12) / (k * 4)
   8.345 +1 unsolved goal(s)!
   8.346 +The error(s) above occurred for the goal statement:
   8.347 +(if n = 0 then 0 else 6 * (k * ln n) / 1) * 2 / (4 * k) =
   8.348 +2 * (Numeral1 * (if n = 0 then 0 else 6 * (k * ln n) / 1)) / (2 * (2 * k))
   8.349 +------------------------------------------
   8.350 +\end{verbatim}
   8.351 +}
   8.352 +Mail ``Re: simproc divide\_cancel\_factor produces error'' on Fri, 16 Sep 2011 22:33:36 +0200
   8.353 +\begin{verbatim}
   8.354 +> > After the release, I'll have to think about doing a complete overhaul
   8.355 +> > of all of the cancellation simprocs.
   8.356 +You are very welcome to do so.  Before you start, call on me and I will
   8.357 +write down some ideas I had long ago (other may want to join, too).
   8.358 +\end{verbatim}
   8.359 +%WN: bist du schon angemeldet in den Mailing-Listen isabelle-users@ und isabelle-dev@ ? WENN NICHT, DANN WIRD ES H"OCHSTE ZEIT !!!
   8.360 +
   8.361 +\subsection{Open Issues with CAS-functionality in CTP}\label{cas-funct}
   8.362 +There is at least one effort explicitly dedicated to implement CAS-functionality in CTP \cite{cezary-phd}. %WN bitte unbedingt lesen (kann von mir in Papierform ausgeborgt werden) !!!
   8.363 +In this work three issues has been identified: partiality conditions, multi-valued functions and real numbers. These issues are addressed in the subsequent paragraphs, followed by a forth issue raised by \sisac{}.
   8.364 +
   8.365 +\paragraph{Partiality conditions}\label{part-cond} are introduced by partial functions or by conditional rewriting. An example of how the CAS-functionality \cite{cezary-phd} looks like is given on p.\pageref{fig:casproto}. 
   8.366 +\cite{cezary-phd} gives an introductory example (floated to p.\pageref{fig:casproto}) which will be referred to in the sequel.
   8.367 +\input{thol.tex}
   8.368 +%WN das nachfolgende Format-Problem l"osen wir sp"ater ...
   8.369 +\begin{figure}[hbt]
   8.370 +\begin{center}
   8.371 +\begin{holnb}
   8.372 +  In1 := vector [\&2; \&2] - vector [\&1; \&0] + vec 1
   8.373 + Out1 := vector [\&2; \&3]
   8.374 +  In2 := diff (diff (\Lam{}x. \&3 * sin (\&2 * x) +
   8.375 +         \&7 + exp (exp x)))
   8.376 + Out2 := \Lam{}x. exp x pow 2 * exp (exp x) +
   8.377 +         exp x * exp (exp x) + -- \&12 * sin (\&2 * x)
   8.378 +  In3 := N (exp (\&1)) 10
   8.379 + Out3 := #2.7182818284 + ... (exp (\&1)) 10 F
   8.380 +  In4 := x + \&1 - x / \&1 + \&7 * (y + x) pow 2
   8.381 + Out4 := \&7 * x pow 2 + \&14 * x * y + \&7 * y pow 2 + \&1
   8.382 +  In5 := sum (0,5) (\Lam{}x. \&x * \&x)
   8.383 + Out5 := \&30
   8.384 +  In6 := sqrt (x * x) assuming x > &1
   8.385 + Out6 := x
   8.386 +\end{holnb}
   8.387 +\end{center}
   8.388 +\caption{\label{fig:casproto}Example interaction with the prototype
   8.389 +  CAS-like input-response loop. For the user input given in the
   8.390 +  \texttt{In} lines, the system produces the output in \texttt{Out}
   8.391 +  lines together with HOL Light theorems that state the equality
   8.392 +  between the input and the output.}
   8.393 +\end{figure}
   8.394 +In lines {\tt In6, Out6} this examples shows how to reliably simplify $\sqrt{x}$. \cite{caspartial} gives more details on handling side conditions in formalized partial functions.
   8.395 +
   8.396 +Analoguous to this example, cancellations (this thesis is concerned with) like
   8.397 +$$\frac{x^2-y^2}{x^2-x\cdot y}=\frac{x+y}{x}\;\;\;\;{\it assuming}\;x-y\not=0\land x\not=0$$
   8.398 +produce assumptions, $x-y\not=0, x\not=0$ here. Since the code produced in the framework of this thesis will be implemented in Isabelle's simplifier (outside this thesis), the presentation to the user will be determined by Isabelle and \sisac{}{} using the respective component of Isabelle. Also reliable handling of assumptions like $x-y\not=0, x\not=0$ is up to these systems.
   8.399 +
   8.400 +\paragraph{Multi-valued functions:}\label{multi-valued}
   8.401 +\cite{seeingroots,davenp-multival-10} discuss cases where CAS are error prone when dropping a branch of a multi-valued function~\footnote{``Multivalued \textit{function}'' is a misnomer, since the value of a function applied to a certain argument is unique by definition of function.}. Familiar examples are ...
   8.402 +%TODO.WN111104 ... zur Erkl"arung ein paar Beispiele von http://en.wikipedia.org/wiki/Multivalued_function
   8.403 +
   8.404 +\paragraph{Real numbers} cannot be represented by numerals. In engineering applications, however, approximation by floating-point numbers are frequently useful. In CTP floating-point numbers must be handled rigorously as approximations. Already \cite{harr:thesis} introduced operations on real numerals accompanied by rigorous calculation of precision. \cite{russellphd} describes efficient implementation of infinite precision real numbers in Coq.
   8.405 +
   8.406 +\paragraph{All solutions for equations} must be guaranted, if equation solving is embedded within CTP. So, given an equation $f(x)=0$ and the set of solutions $S$ of this equation, we want to have both,
   8.407 +\begin{eqnarray}
   8.408 +   \exists x_s.\;x_s\in S &\Rightarrow& f(x_s) = 0 \\\label{is-solut}
   8.409 +  x_s\in S &\Leftarrow& \exists x_s.\;f(x_s) = 0    \label{all-solut}
   8.410 +\end{eqnarray}
   8.411 +where (\ref{all-solut}) ensures that $S$ contains {\em all} solutions of the equation. The \sisac{}-project has implemented a prototype of an equation solver~\footnote{See \textit{equations} in the hierarchy of specifications at http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}.
   8.412 +
   8.413 +There is demand for fullfledged equation solving in CTP, including equational systems and differential equations, because \sisac{}{} has a prototype of a CTP-based programming language calling CAS functions; and Lucas-Interpretation \cite{wn:lucas-interp-12} makes these functions accessible by single-stepping and ``next step guidance'', which would automatically generate a learning system for equation solving.
   8.414 +
   8.415 +\subsection{Algorithms for cancellation of multivariate polynomials}
   8.416 +The most appropriate book for implementing the required algorithms in this thesis is \cite{Winkler:96}. TODO.WN111104 welche noch ?
   8.417 +
   8.418 +\section{Thesis structure}
   8.419 +The proposed table of contents of the thesis on the chapter level is as follows:
   8.420 +\begin{enumerate}
   8.421 +	\item Introduction (2-3 pages)
   8.422 +	\item Computer Algebra Systems (CAS) (5 - 7 pages)\\
   8.423 +	Which different CAS exists and whats the focus of them.
   8.424 +	\item The \sisac{}-Project (5 - 7 pages)\\
   8.425 +	This chapter will describe the \sisac{}-Project and the goals of the project.
   8.426 +	\item Univariate Polynomials (15-20 pages)\\
   8.427 +	This chapter will describe different Algorithms for univariate polynomials, with different coefficients.
   8.428 +	\item Multivariate Polynomials (20-25 pages)\\
   8.429 +	This chapter will describe different Algorithms for multivariate polynomials,  with different coefficients
   8.430 +	\item Functional programming and SML(2-5 pages)\\
   8.431 +	The basic idea of this programming languages.
   8.432 +	\item Implimentation in \sisac{}-Project (15-20 pages)
   8.433 +	\item Conclusion (2-3 pages)
   8.434 +\end{enumerate}
   8.435 +%\newpage
   8.436 +
   8.437 +\section{Timeline}
   8.438 +%Werd nie fertig.\\
   8.439 +\begin{center}
   8.440 +		\begin{tabular}{|l|l|l|}
   8.441 +		\hline
   8.442 +			 \textbf{Time}&\textbf{Thesis}&\textbf{Project}\\
   8.443 +			 \hline
   8.444 +			 & Functional programming & Learning the basics and the idea\\
   8.445 +			 & & of funcional programming\\
   8.446 +			 \hline
   8.447 +			 & Different CAS & Can they handle the problem \\
   8.448 +			 & &and which algorithm do they use?\\ \hline
   8.449 +			 & Univariate Polynomials & Implementation of the Algorithm\\
   8.450 +			 & & for univariate Polynomials \\ \hline
   8.451 +		   & Multivariate Polynomials &  Implementation of the Algorithm\\
   8.452 +			 & & for multivariate Polynomials \\ \hline 
   8.453 +		   & The \sisac-Project &\\ \hline
   8.454 +		   & Conclusion and Introduction & Find good examples for testing\\
   8.455 +			\hline
   8.456 +		\end{tabular}
   8.457 +	\end{center}
   8.458 +
   8.459 +%WN oben an passender stelle einf"ugen
   8.460 +\cite{einf-funct-progr}
   8.461 +		
   8.462 +		
   8.463 +\bibliography{bib/math-eng,bib/didact,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,references}
   8.464 +%\section{Bibliography}
   8.465 +%%mindestens 10
   8.466 +%\begin{enumerate}
   8.467 +% \item Bird/Wadler, \textit{Einf�hrung in die funktionale Programmierung}, Carl Hanser and Prentice-Hall International, 1992
   8.468 +% \item Franz Winkler, \textit{Polynomial Algorithms in Computer Algebra}, Springer,1996
   8.469 +% \item %M. Mignotte, \textit{An inequality about factors of polynomial}
   8.470 +% \item %M. Mignotte, \textit{Some useful bounds}
   8.471 +% \item %W. S. Brown and J. F. Traub. \textit{On euclid's algorithm and the theory of subresultans}, Journal of the ACM (JACM), 1971
   8.472 +% \item %Bruno Buchberger, \textit{Algorhimic mathematics: Problem types, data types, algorithm types}, Lecture notes, RISC Jku A-4040 Linz, 1982
   8.473 +% 
   8.474 +% \item %Tateaki Sasaki and Masayuki Suzuki, \textit{Thre new algorithms for multivariate polynomial GCD}, J. Symbolic Combutation, 1992
   8.475 +% \item
   8.476 +% \item
   8.477 +% \item
   8.478 +%\end{enumerate} 
   8.479 +
   8.480 +\end{document}
   8.481 +
   8.482 +ALLES UNTERHALB \end{document} WIRD VON LATEX NICHT BERUECKSICHTIGT
   8.483 +WN110916 grep-ing through Isabelle code:
   8.484 +
   8.485 +neuper@neuper:/usr/local/isabisac/src$ find -name "*umeral*"
   8.486 +./HOL/ex/Numeral.thy
   8.487 +./HOL/Tools/nat_numeral_simprocs.ML
   8.488 +./HOL/Tools/numeral_syntax.ML
   8.489 +./HOL/Tools/numeral.ML
   8.490 +./HOL/Tools/numeral_simprocs.ML
   8.491 +./HOL/Matrix/ComputeNumeral.thy
   8.492 +./HOL/Library/Numeral_Type.thy
   8.493 +./HOL/Numeral_Simprocs.thy
   8.494 +./HOL/Import/HOL/numeral.imp
   8.495 +./HOL/Code_Numeral.thy
   8.496 +./HOL/Nat_Numeral.thy
   8.497 +./ZF/Tools/numeral_syntax.ML
   8.498 +./Provers/Arith/cancel_numeral_factor.ML
   8.499 +./Provers/Arith/cancel_numerals.ML
   8.500 +./Provers/Arith/combine_numerals.ML
   8.501 +
   8.502 +neuper@neuper:/usr/local/isabisac/src$ find -name "*ancel*"
   8.503 +./HOL/Tools/abel_cancel.ML                 
   8.504 +./Provers/Arith/cancel_div_mod.ML
   8.505 +./Provers/Arith/cancel_numeral_factor.ML  Paulson 2000 !!!
   8.506 +./Provers/Arith/cancel_sums.ML            
   8.507 +./Provers/Arith/cancel_numerals.ML        Paulson 2000

     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/doc-isac/dmeindl/references.bib	Tue Sep 17 09:50:52 2013 +0200
     9.3 @@ -0,0 +1,296 @@
     9.4 +@proceedings{DBLP:conf/mkm/2007,
     9.5 +  editor    = {Manuel Kauers and
     9.6 +               Manfred Kerber and
     9.7 +               Robert Miner and
     9.8 +               Wolfgang Windsteiger},
     9.9 +  title     = {Towards Mechanized Mathematical Assistants, 14th Symposium,
    9.10 +               Calculemus 2007, 6th International Conference, MKM 2007,
    9.11 +               Hagenberg, Austria, June 27-30, 2007, Proceedings},
    9.12 +  booktitle = {Calculemus/MKM},
    9.13 +  publisher = {Springer},
    9.14 +  series    = {Lecture Notes in Computer Science},
    9.15 +  volume    = {4573},
    9.16 +  year      = {2007},
    9.17 +  isbn      = {978-3-540-73083-5},
    9.18 +  bibsource = {DBLP, http://dblp.uni-trier.de}
    9.19 +}
    9.20 +
    9.21 +@proceedings{DBLP:conf/cade/2006,
    9.22 +  editor    = {Ulrich Furbach and
    9.23 +               Natarajan Shankar},
    9.24 +  title     = {Automated Reasoning, Third International Joint Conference,
    9.25 +               IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
    9.26 +  booktitle = {IJCAR},
    9.27 +  publisher = {Springer},
    9.28 +  series    = {Lecture Notes in Computer Science},
    9.29 +  volume    = {4130},
    9.30 +  year      = {2006},
    9.31 +  isbn      = {3-540-37187-7},
    9.32 +  bibsource = {DBLP, http://dblp.uni-trier.de}
    9.33 +}
    9.34 +
    9.35 +@proceedings{DBLP:conf/iwfm/1999,
    9.36 +  editor    = {Andrew Butterfield and
    9.37 +               Klemens Haegele},
    9.38 +  title     = {3rd Irish Workshop on Formal Methods, Galway, Eire, July
    9.39 +               1999},
    9.40 +  booktitle = {IWFM},
    9.41 +  publisher = {BCS},
    9.42 +  series    = {Workshops in Computing},
    9.43 +  year      = {1999},
    9.44 +  bibsource = {DBLP, http://dblp.uni-trier.de}
    9.45 +}
    9.46 +
    9.47 +@proceedings{DBLP:conf/aisc/2008,
    9.48 +  editor    = {Serge Autexier and
    9.49 +               John Campbell and
    9.50 +               Julio Rubio and
    9.51 +               Volker Sorge and
    9.52 +               Masakazu Suzuki and
    9.53 +               Freek Wiedijk},
    9.54 +  title     = {Intelligent Computer Mathematics, 9th International Conference,
    9.55 +               AISC 2008, 15th Symposium, Calculemus 2008, 7th International
    9.56 +               Conference, MKM 2008, Birmingham, UK, July 28 - August 1,
    9.57 +               2008. Proceedings},
    9.58 +  booktitle = {AISC/MKM/Calculemus},
    9.59 +  publisher = {Springer},
    9.60 +  series    = {Lecture Notes in Computer Science},
    9.61 +  volume    = {5144},
    9.62 +  year      = {2008},
    9.63 +  isbn      = {978-3-540-85109-7},
    9.64 +  bibsource = {DBLP, http://dblp.uni-trier.de}
    9.65 +}
    9.66 +
    9.67 +@InProceedings{wn:lucas-interp-12,
    9.68 +  author = 	 {Neuper, Walther},
    9.69 +  title = 	 {Automated Generation of User Guidance by Combining Computation and Deduction},
    9.70 +  booktitle = {THedu'11: CTP-compontents for educational software},
    9.71 +  year = 	 {2012},
    9.72 +  editor = 	 {Quaresma, Pedro},
    9.73 +  publisher = {EPTCS},
    9.74 +  note = {To appear}
    9.75 +}
    9.76 +
    9.77 +@InProceedings{davenp-multival-10,
    9.78 +  author = 	 {Davenport, James},
    9.79 +  title = 	 {The Challenges of Multivalued "Functions"},
    9.80 +  booktitle = {Proceedings of the Conferences on Intelligent Computer Mathematics (CICM)},
    9.81 +  year = 	 {2010}
    9.82 +}
    9.83 +
    9.84 +@PhdThesis{cezary-phd,
    9.85 +  author = 	 {Kalisyk, Cezary},
    9.86 +  title = 	 {Correctness and Availability. Building Computer Algebra on top of Proof Assistants and making Proof Assistants available over the Web},
    9.87 +  school = 	 {Radboud University Nijmegen},
    9.88 +  year = 	 {2009},
    9.89 +  type = 	 {IPA Dissertation Series 2009-18},
    9.90 +  note = 	 {Promotor Herman Geuvers}
    9.91 +}
    9.92 +
    9.93 +@Book{bb-loos,
    9.94 +  editor = 	 {Buchberger, Bruno and Collins, George Edwin and Loos, 
    9.95 +                  R\"udiger and Albrecht, Rudolf},
    9.96 +  title = 	 {Computer Algebra. Symbolic and Algebraic Computation},
    9.97 +  publisher = 	 {Springer Verlag},
    9.98 +  year = 	 {1982},
    9.99 +  edition = 	 {2}
   9.100 +}
   9.101 +
   9.102 +@Book{term-nets,
   9.103 +  author = 	 {Charniak, E. and Riesbeck, C. K. and McDermott, D. V.},
   9.104 +  title = 	 {Artificial Intelligence Programming},
   9.105 +  publisher = 	 {Lawrence Erlbaum Associates},
   9.106 +  year = 	 {1980},
   9.107 +  note = 	 {(Chapter 14)}
   9.108 +}
   9.109 +
   9.110 +@Book{db:dom-eng,
   9.111 +  author = 	 {Bj{\o}rner, Dines},
   9.112 +  title = 	 {Domain Engineering. Technology Management, Research and Engineering},
   9.113 +  publisher = 	 {JAIST Press},
   9.114 +  year = 	 {2009},
   9.115 +  month = 	 {Feb},
   9.116 +  series = 	 {COE Research Monograph Series},
   9.117 +  volume = 	 {4},
   9.118 +  address = 	 {Nomi, Japan}
   9.119 +}
   9.120 +
   9.121 +@techreport{harr:thesis,
   9.122 +        author={Harrison, John R.},
   9.123 +        title={Theorem proving with the real numbers},
   9.124 +        institution={University of Cambridge, Computer Laboratory},year={1996}, 
   9.125 +        type={Technical Report},number={408},address={},month={November},
   9.126 +        note={},status={},source={},location={loc?} 
   9.127 +        }  
   9.128 +
   9.129 +@InProceedings{damas-milner-82,
   9.130 +  author = 	 {Damas, Luis and Milner, Robin},
   9.131 +  title = 	 {Principal type-schemes for functional programs},
   9.132 +  booktitle = {9th Symposium on Principles of programming languages (POPL'82)},
   9.133 +  pages = 	 {207-212},
   9.134 +  year = 	 {1982},
   9.135 +  editor = 	 {ACM}
   9.136 +}
   9.137 +
   9.138 +@Article{Milner-78,
   9.139 +  author = 	 {Milner, R.},
   9.140 +  title = 	 {A Theory of Type Polymorphism in Programming},
   9.141 +  journal = 	 {Journal of Computer and System Science (JCSS)},
   9.142 +  year = 	 {1978},
   9.143 +  number = 	 {17},
   9.144 +  pages = 	 {348-374}
   9.145 +}
   9.146 +
   9.147 +@Article{Hindley-69,
   9.148 +  author = 	 {Hindley, R.},
   9.149 +  title = 	 {The Principal Type-Scheme of an Object in Combinatory Logic},
   9.150 +  journal = 	 {Transactions of the American Mathematical Society},
   9.151 +  year = 	 {1969},
   9.152 +  volume = 	 {146},
   9.153 +  pages = 	 {29-60}
   9.154 +}
   9.155 +
   9.156 +@article{seeingroots,
   9.157 + author = {Jeffrey, D.J. and Norman, A.C.},
   9.158 + title = {Not seeing the roots for the branches: multivalued functions in computer algebra},
   9.159 + journal = {SIGSAM Bull.},
   9.160 + volume = {38},
   9.161 + number = {3},
   9.162 + year = {2004},
   9.163 + issn = {0163-5824},
   9.164 + pages = {57--66},
   9.165 + doi = {http://doi.acm.org/10.1145/1040034.1040036},
   9.166 + publisher = {ACM},
   9.167 + address = {New York, NY, USA},
   9.168 + }
   9.169 +
   9.170 +@PhdThesis{russellphd,
   9.171 +  author =       {Russell O'Connor},
   9.172 +  title =        {Incompleteness and Completeness.},
   9.173 +  school =       {Radboud University Nijmegen},
   9.174 +  year =         {2009},
   9.175 +}
   9.176 +
   9.177 +@inproceedings{caspartial,
   9.178 +  author    = {Cezary Kaliszyk},
   9.179 +  title     = {Automating Side Conditions in Formalized Partial Functions},
   9.180 +  booktitle = {AISC/MKM/Calculemus},
   9.181 +  year      = {2008},
   9.182 +  pages     = {300-314},
   9.183 +  ee        = {http://dx.doi.org/10.1007/978-3-540-85110-3_26},
   9.184 +  crossref  = {DBLP:conf/aisc/2008},
   9.185 +  bibsource = {DBLP, http://dblp.uni-trier.de}
   9.186 +}
   9.187 +
   9.188 +@inproceedings{farmer,
   9.189 +  author    = {Farmer, William M.},
   9.190 +  title     = {A Scheme for Defining Partial Higher-Order Functions by
   9.191 +               Recursion.},
   9.192 +  booktitle = {IWFM},
   9.193 +  year      = {1999},
   9.194 +  crossref  = {DBLP:conf/iwfm/1999},
   9.195 +  bibsource = {DBLP, http://dblp.uni-trier.de}
   9.196 +}
   9.197 +
   9.198 +@inproceedings{krauss,
   9.199 +  author    = {Krauss, Alexander},
   9.200 +  title     = {Partial Recursive Functions in Higher-Order Logic},
   9.201 +  booktitle = {IJCAR},
   9.202 +  year      = {2006},
   9.203 +  pages     = {589-603},
   9.204 +  ee        = {http://dx.doi.org/10.1007/11814771_48},
   9.205 +  crossref  = {DBLP:conf/cade/2006},
   9.206 +  bibsource = {DBLP, http://dblp.uni-trier.de}
   9.207 +}
   9.208 +
   9.209 +@inproceedings{casproto,
   9.210 +  author    = {Cezary Kaliszyk and
   9.211 +               Freek Wiedijk},
   9.212 +  title     = {Certified Computer Algebra on Top of an Interactive Theorem
   9.213 +               Prover},
   9.214 +  booktitle = {Calculemus},
   9.215 +  year      = {2007},
   9.216 +  pages     = {94-105},
   9.217 +  ee        = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
   9.218 +  crossref  = {DBLP:conf/mkm/2007},
   9.219 +  bibsource = {DBLP, http://dblp.uni-trier.de}
   9.220 +}
   9.221 +
   9.222 +@inproceedings{theorema00,
   9.223 +  author = "Buchberger, B. and
   9.224 +    Dupre, C. and
   9.225 +    Jebelean, T. and
   9.226 +    Kriftner, F. and
   9.227 +    Nakagawa, K. and
   9.228 +    Vasaru, D. and
   9.229 +    Windsteiger, W.",
   9.230 +  title = "{The Theorema Project: A Progress Report}",
   9.231 +  booktitle = "Symbolic Computation and Automated Reasoning
   9.232 +    (Proceedings of CALCULEMUS 2000, Symposium on the Integration of
   9.233 +    Symbolic Computation and Mechanized Reasoning)",
   9.234 +  editor = "Kerber, M. and
   9.235 +    Kohlhase, M.",
   9.236 +  publisher = "A.K.~Peters",
   9.237 +  address = "Natick, Massachusetts",
   9.238 +  isbn = "1-56881-145-4",
   9.239 +  year = 2000
   9.240 +}
   9.241 +
   9.242 +@inproceedings{logicalaxiom,
   9.243 +	author = {E. Poll and S. Thompson},
   9.244 +	title = {{Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor}},
   9.245 +  booktitle = {Calculemus and Types '98},
   9.246 +	year = {1998},
   9.247 +  place = {Eindhoven, The Netherlands},
   9.248 +	month = {July},
   9.249 +	note = {Also as technical report 6-98, Computing Laboratory, University of Kent}
   9.250 +}
   9.251 +
   9.252 +@InProceedings{pvs,
   9.253 +  author = 	 {Owre, S. and Rajan, S. and Rushby, J. and Shankar, N. and Srivas, M.},
   9.254 +  title = 	 {{PVS}: Combining specification, proof checking, and model checking},
   9.255 +  booktitle = 	 {Computer-Aided Verification},
   9.256 +  pages = 	 {411-414},
   9.257 +  year = 	 {1996},
   9.258 +  editor = 	 {Alur, R. and Henzinger, T.A.},
   9.259 +  organization = {CAV'96},
   9.260 +  annote = 	 {}
   9.261 +}
   9.262 +
   9.263 +@Book{Nipkow-Paulson-Wenzel:2002,
   9.264 +  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
   9.265 +  title		= {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
   9.266 +  publisher	= {Springer},
   9.267 +  series	= {LNCS},
   9.268 +  volume	= 2283,
   9.269 +  year		= 2002
   9.270 +}
   9.271 +
   9.272 +@Manual{Huet_all:94,
   9.273 +  author = 	 {Huet, G. and Kahn, G. and and Paulin-Mohring, C.},
   9.274 +  title = 	 {The Coq Proof Assistant},
   9.275 +  institution =  {INRIA-Rocquencourt},
   9.276 +  year = 	 {1994},
   9.277 +  type = 	 {Tutorial},
   9.278 +  number = 	 {Version 5.10},
   9.279 +  address = 	 {CNRS-ENS Lyon},
   9.280 +  status={},source={Theorema},location={-}
   9.281 +}
   9.282 +
   9.283 +@Book{einf-funct-progr,
   9.284 +  author = 	 {Richard Bird and Philip Wadler},
   9.285 +  title = 	 {Introduction to Functional Programming},
   9.286 +  publisher = 	 {Prentice Hall},
   9.287 +  year = 	 1988,
   9.288 +  editor =	 {C. A. R. Hoare},
   9.289 +  series =	 {Prentice Hall International Series in Computer Science},
   9.290 +  address =	 {New York, London, Toronto, Sydney, Tokyo},
   9.291 +  annote =	 {88bok371}
   9.292 +}
   9.293 +@Book{Winkler:96,
   9.294 +  author =       {F. Winkler},
   9.295 +  title =        {{Polynomial Algorithms in Computer Algebra}},
   9.296 +  publisher =    {Springer-Verlag Wien New York},
   9.297 +  year =         {1996}
   9.298 +}
   9.299 +

    10.1 Binary file doc-isac/dmeindl/thol.tex has changed

    11.1 Binary file doc-isac/fig/coqide.png has changed

    12.1 Binary file doc-isac/fig/jrocnik/isac-Ztrans-math-3.png has changed

    13.1 Binary file doc-isac/fig/jrocnik/math-universe-small.png has changed

    14.1 Binary file doc-isac/fig/jrocnik/math-universe.odg has changed

    15.1 Binary file doc-isac/fig/jrocnik/math-universe.png has changed

    16.1 Binary file doc-isac/fig/pgisabelle.png has changed

    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/doc-isac/jrocnik/CLEANUP	Tue Sep 17 09:50:52 2013 +0200
    17.3 @@ -0,0 +1,10 @@
    17.4 +rm *.dvi
    17.5 +rm *.bbl
    17.6 +rm *.blg
    17.7 +rm *.aux
    17.8 +rm *.log
    17.9 +rm *.nav
   17.10 +rm *.out
   17.11 +rm *.snm
   17.12 +rm *.toc
   17.13 +rm *~

    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/doc-isac/jrocnik/FFT.thy	Tue Sep 17 09:50:52 2013 +0200
    18.3 @@ -0,0 +1,532 @@
    18.4 +(*  Title:      Fast Fourier Transform
    18.5 +    Author:     Clemens Ballarin <ballarin at in.tum.de>, started 12 April 2005
    18.6 +    Maintainer: Clemens Ballarin <ballarin at in.tum.de>
    18.7 +*)
    18.8 +
    18.9 +theory FFT
   18.10 +imports Complex_Main
   18.11 +begin
   18.12 +
   18.13 +text {* We formalise a functional implementation of the FFT algorithm
   18.14 +  over the complex numbers, and its inverse.  Both are shown
   18.15 +  equivalent to the usual definitions
   18.16 +  of these operations through Vandermonde matrices.  They are also
   18.17 +  shown to be inverse to each other, more precisely, that composition
   18.18 +  of the inverse and the transformation yield the identity up to a
   18.19 +  scalar.
   18.20 +
   18.21 +  The presentation closely follows Section 30.2 of Cormen \textit{et
   18.22 +  al.}, \emph{Introduction to Algorithms}, 2nd edition, MIT Press,
   18.23 +  2003. *}
   18.24 +
   18.25 +
   18.26 +section {* Preliminaries *}
   18.27 +
   18.28 +lemma of_nat_cplx:
   18.29 +  "of_nat n = Complex (of_nat n) 0"
   18.30 +  by (induct n) (simp_all add: complex_one_def)
   18.31 +
   18.32 +
   18.33 +text {* The following two lemmas are useful for experimenting with the
   18.34 +  transformations, at a vector length of four. *}
   18.35 +
   18.36 +lemma Ivl4:
   18.37 +  "{0..<4::nat} = {0, 1, 2, 3}"
   18.38 +proof -
   18.39 +  have "{0..<4::nat} = {0..<Suc (Suc (Suc (Suc 0)))}" by (simp add: eval_nat_numeral)
   18.40 +  also have "... = {0, 1, 2, 3}"
   18.41 +    by (simp add: atLeastLessThanSuc eval_nat_numeral insert_commute)
   18.42 +  finally show ?thesis .
   18.43 +qed
   18.44 +
   18.45 +lemma Sum4:
   18.46 +  "(\<Sum>i=0..<4::nat. x i) = x 0 + x 1 + x 2 + x 3"
   18.47 +  by (simp add: Ivl4 eval_nat_numeral)
   18.48 +
   18.49 +
   18.50 +text {* A number of specialised lemmas for the summation operator,
   18.51 +  where the index set is the natural numbers *}
   18.52 +
   18.53 +lemma setsum_add_nat_ivl_singleton:
   18.54 +  assumes less: "m < (n::nat)"
   18.55 +  shows "f m + setsum f {m<..<n} = setsum f {m..<n}"
   18.56 +proof -
   18.57 +  have "f m + setsum f {m<..<n} = setsum f ({m} \<union> {m<..<n})"
   18.58 +    by (simp add: setsum_Un_disjoint ivl_disj_int)
   18.59 +  also from less have "... = setsum f {m..<n}"
   18.60 +    by (simp only: ivl_disj_un)
   18.61 +  finally show ?thesis .
   18.62 +qed
   18.63 +
   18.64 +lemma setsum_add_split_nat_ivl_singleton:
   18.65 +  assumes less: "m < (n::nat)"
   18.66 +    and g: "!!i. [| m < i; i < n |] ==> g i = f i"
   18.67 +  shows "f m + setsum g {m<..<n} = setsum f {m..<n}"
   18.68 +  using less g
   18.69 +  by(simp add: setsum_add_nat_ivl_singleton cong: strong_setsum_cong)
   18.70 +
   18.71 +lemma setsum_add_split_nat_ivl:
   18.72 +  assumes le: "m <= (k::nat)" "k <= n"
   18.73 +    and g: "!!i. [| m <= i; i < k |] ==> g i = f i"
   18.74 +    and h: "!!i. [| k <= i; i < n |] ==> h i = f i"
   18.75 +  shows "setsum g {m..<k} + setsum h {k..<n} = setsum f {m..<n}"
   18.76 +  using le g h by (simp add: setsum_add_nat_ivl cong: strong_setsum_cong)
   18.77 +
   18.78 +lemma ivl_splice_Un:
   18.79 +  "{0..<2*n::nat} = (op * 2 ` {0..<n}) \<union> ((%i. Suc (2*i)) ` {0..<n})"
   18.80 +  apply (unfold image_def Bex_def)
   18.81 +  apply auto
   18.82 +  apply arith
   18.83 +  done
   18.84 +
   18.85 +lemma ivl_splice_Int:
   18.86 +  "(op * 2 ` {0..<n}) \<inter> ((%i. Suc (2*i)) ` {0..<n}) = {}"
   18.87 +  by auto arith
   18.88 +
   18.89 +lemma double_inj_on:
   18.90 +  "inj_on (%i. 2*i::nat) A"
   18.91 +  by (simp add: inj_onI)
   18.92 +
   18.93 +lemma Suc_double_inj_on:
   18.94 +  "inj_on (%i. Suc (2*i)) A"
   18.95 +  by (rule inj_onI) simp
   18.96 +
   18.97 +lemma setsum_splice:
   18.98 +  "(\<Sum>i::nat = 0..<2*n. f i) = (\<Sum>i = 0..<n. f (2*i)) + (\<Sum>i = 0..<n. f (2*i+1))"
   18.99 +proof -
  18.100 +  have "(\<Sum>i::nat = 0..<2*n. f i) =
  18.101 +    setsum f (op * 2 ` {0..<n}) + setsum f ((%i. 2*i+1) ` {0..<n})"
  18.102 +    by (simp add: ivl_splice_Un ivl_splice_Int setsum_Un_disjoint)
  18.103 +  also have "... = (\<Sum>i = 0..<n. f (2*i)) + (\<Sum>i = 0..<n. f (2*i+1))"
  18.104 +    by (simp add: setsum_reindex [OF double_inj_on]
  18.105 +      setsum_reindex [OF Suc_double_inj_on])
  18.106 +  finally show ?thesis .
  18.107 +qed
  18.108 +
  18.109 +
  18.110 +section {* Complex Roots of Unity *}
  18.111 +
  18.112 +text {* The function @{term cis} from the complex library returns the
  18.113 +  point on the unity circle corresponding to the argument angle.  It
  18.114 +  is the base for our definition of @{text root}.  The main property,
  18.115 +  De Moirve's formula is already there in the library. *}
  18.116 +
  18.117 +definition root :: "nat => complex" where
  18.118 +  "root n == cis (2*pi/(real (n::nat)))"
  18.119 +
  18.120 +lemma sin_periodic_pi_diff [simp]: "sin (x - pi) = - sin x"
  18.121 +  by (simp add: sin_diff)
  18.122 +
  18.123 +lemma sin_cos_between_zero_two_pi:
  18.124 +  assumes 0: "0 < x" and pi: "x < 2 * pi"
  18.125 +  shows "sin x \<noteq> 0 \<or> cos x \<noteq> 1"
  18.126 +proof -
  18.127 +  { assume "0 < x" and "x < pi"
  18.128 +    then have "sin x \<noteq> 0" by (auto dest: sin_gt_zero_pi) }
  18.129 +  moreover
  18.130 +  { assume "x = pi"
  18.131 +    then have "cos x \<noteq> 1" by simp }
  18.132 +  moreover
  18.133 +  { assume pi1: "pi < x" and pi2: "x < 2 * pi"
  18.134 +    then have "0 < x - pi" and "x - pi < pi" by arith+
  18.135 +    then have "sin (x - pi) \<noteq> 0" by (auto dest: sin_gt_zero_pi)
  18.136 +    with pi1 pi2 have "sin x \<noteq> 0" by simp }
  18.137 +  ultimately show ?thesis using 0 pi by arith
  18.138 +qed
  18.139 +
  18.140 +
  18.141 +subsection {* Basic Lemmas *}
  18.142 +
  18.143 +lemma root_nonzero:
  18.144 +  "root n ~= 0"
  18.145 +  apply (unfold root_def)
  18.146 +  apply (unfold cis_def)
  18.147 +  apply auto
  18.148 +  apply (drule sin_zero_abs_cos_one)
  18.149 +  apply arith
  18.150 +  done
  18.151 +
  18.152 +lemma root_unity:
  18.153 +  "root n ^ n = 1"
  18.154 +  apply (unfold root_def)
  18.155 +  apply (simp add: DeMoivre)
  18.156 +  apply (simp add: cis_def)
  18.157 +  done
  18.158 +
  18.159 +lemma root_cancel:
  18.160 +  "0 < d ==> root (d * n) ^ (d * k) = root n ^ k"
  18.161 +  apply (unfold root_def)
  18.162 +  apply (simp add: DeMoivre)
  18.163 +  done
  18.164 +
  18.165 +lemma root_summation:
  18.166 +  assumes k: "0 < k" "k < n"
  18.167 +  shows "(\<Sum>i=0..<n. (root n ^ k) ^ i) = 0"
  18.168 +proof -
  18.169 +  from k have real0: "0 < real k * (2 * pi) / real n"
  18.170 +    by (simp add: zero_less_divide_iff
  18.171 +      mult_strict_right_mono [where a = 0, simplified])
  18.172 +  from k mult_strict_right_mono [where a = "real k" and
  18.173 +    b = "real n" and c = "2 * pi / real n", simplified]
  18.174 +  have realk: "real k * (2 * pi) / real n < 2 * pi"
  18.175 +    by (simp add: zero_less_divide_iff)
  18.176 +  txt {* Main part of the proof *}
  18.177 +  have "(\<Sum>i=0..<n. (root n ^ k) ^ i) =
  18.178 +    ((root n ^ k) ^ n - 1) / (root n ^ k - 1)"
  18.179 +    apply (rule geometric_sum)
  18.180 +    apply (unfold root_def)
  18.181 +    apply (simp add: DeMoivre)
  18.182 +    using real0 realk sin_cos_between_zero_two_pi 
  18.183 +    apply (auto simp add: cis_def complex_one_def)
  18.184 +    done
  18.185 +  also have "... = ((root n ^ n) ^ k - 1) / (root n ^ k - 1)"
  18.186 +    by (simp add: power_mult [THEN sym] mult_ac)
  18.187 +  also have "... = 0"
  18.188 +    by (simp add: root_unity)
  18.189 +  finally show ?thesis .
  18.190 +qed
  18.191 +
  18.192 +lemma root_summation_inv:
  18.193 +  assumes k: "0 < k" "k < n"
  18.194 +  shows "(\<Sum>i=0..<n. ((1 / root n) ^ k) ^ i) = 0"
  18.195 +proof -
  18.196 +  from k have real0: "0 < real k * (2 * pi) / real n"
  18.197 +    by (simp add: zero_less_divide_iff
  18.198 +      mult_strict_right_mono [where a = 0, simplified])
  18.199 +  from k mult_strict_right_mono [where a = "real k" and
  18.200 +    b = "real n" and c = "2 * pi / real n", simplified]
  18.201 +  have realk: "real k * (2 * pi) / real n < 2 * pi"
  18.202 +    by (simp add: zero_less_divide_iff)
  18.203 +  txt {* Main part of the proof *}
  18.204 +  have "(\<Sum>i=0..<n. ((1 / root n) ^ k) ^ i) =
  18.205 +    (((1 / root n) ^ k) ^ n - 1) / ((1 / root n) ^ k - 1)"
  18.206 +    apply (rule geometric_sum)
  18.207 +    apply (simp add: nonzero_inverse_eq_divide [THEN sym] root_nonzero)
  18.208 +    apply (unfold root_def)
  18.209 +    apply (simp add: DeMoivre)
  18.210 +    using real0 realk sin_cos_between_zero_two_pi
  18.211 +    apply (auto simp add: cis_def complex_one_def)
  18.212 +    done
  18.213 +  also have "... = (((1 / root n) ^ n) ^ k - 1) / ((1 / root n) ^ k - 1)"
  18.214 +    by (simp add: power_mult [THEN sym] mult_ac)
  18.215 +  also have "... = 0"
  18.216 +    by (simp add: power_divide root_unity)
  18.217 +  finally show ?thesis .
  18.218 +qed
  18.219 +
  18.220 +lemma root0 [simp]:
  18.221 +  "root 0 = 1"
  18.222 +  by (simp add: root_def cis_def)
  18.223 +
  18.224 +lemma root1 [simp]:
  18.225 +  "root 1 = 1"
  18.226 +  by (simp add: root_def cis_def)
  18.227 +
  18.228 +lemma root2 [simp]:
  18.229 +  "root 2 = Complex -1 0"
  18.230 +  by (simp add: root_def cis_def)
  18.231 +
  18.232 +lemma root4 [simp]:
  18.233 +  "root 4 = ii"
  18.234 +  by (simp add: root_def cis_def)
  18.235 +
  18.236 +
  18.237 +subsection {* Derived Lemmas *}
  18.238 +
  18.239 +lemma root_cancel1:
  18.240 +  "root (2 * m) ^ (i * (2 * j)) = root m ^ (i * j)"
  18.241 +proof -
  18.242 +  have "root (2 * m) ^ (i * (2 * j)) = root (2 * m) ^ (2 * (i * j))"
  18.243 +    by (simp add: mult_ac)
  18.244 +  also have "... = root m ^ (i * j)"
  18.245 +    by (simp add: root_cancel)
  18.246 +  finally show ?thesis .
  18.247 +qed
  18.248 +
  18.249 +lemma root_cancel2:
  18.250 +  "0 < n ==> root (2 * n) ^ n = - 1"
  18.251 +  txt {* Note the space between @{text "-"} and @{text "1"}. *}
  18.252 +  using root_cancel [where n = 2 and k = 1]
  18.253 +  apply (simp only: mult_ac)
  18.254 +  apply (simp add: complex_one_def)
  18.255 +  done
  18.256 +
  18.257 +
  18.258 +section {* Discrete Fourier Transformation *}
  18.259 +
  18.260 +text {*
  18.261 +  We define operations  @{text DFT} and @{text IDFT} for the discrete
  18.262 +  Fourier Transform and its inverse.  Vectors are simply functions of
  18.263 +  type @{text "nat => complex"}. *}
  18.264 +
  18.265 +text {*
  18.266 +  @{text "DFT n a"} is the transform of vector @{text a}
  18.267 +  of length @{text n}, @{text IDFT} its inverse. *}
  18.268 +
  18.269 +definition DFT :: "nat => (nat => complex) => (nat => complex)" where
  18.270 +  "DFT n a == (%i. \<Sum>j=0..<n. (root n) ^ (i * j) * (a j))"
  18.271 +
  18.272 +definition IDFT :: "nat => (nat => complex) => (nat => complex)" where
  18.273 +  "IDFT n a == (%i. (\<Sum>k=0..<n. (a k) / (root n) ^ (i * k)))"
  18.274 +
  18.275 +schematic_lemma "map (DFT 4 a) [0, 1, 2, 3] = ?x"
  18.276 +  by(simp add: DFT_def Sum4)
  18.277 +
  18.278 +text {* Lemmas for the correctness proof. *}
  18.279 +
  18.280 +lemma DFT_lower:
  18.281 +  "DFT (2 * m) a i =
  18.282 +  DFT m (%i. a (2 * i)) i +
  18.283 +  (root (2 * m)) ^ i * DFT m (%i. a (2 * i + 1)) i"
  18.284 +proof (unfold DFT_def)
  18.285 +  have "(\<Sum>j = 0..<2 * m. root (2 * m) ^ (i * j) * a j) =
  18.286 +    (\<Sum>j = 0..<m. root (2 * m) ^ (i * (2 * j)) * a (2 * j)) +
  18.287 +    (\<Sum>j = 0..<m. root (2 * m) ^ (i * (2 * j + 1)) * a (2 * j + 1))"
  18.288 +    (is "?s = _")
  18.289 +    by (simp add: setsum_splice)
  18.290 +  also have "... = (\<Sum>j = 0..<m. root m ^ (i * j) * a (2 * j)) +
  18.291 +    root (2 * m) ^ i *
  18.292 +    (\<Sum>j = 0..<m. root m ^ (i * j) * a (2 * j + 1))"
  18.293 +    (is "_ = ?t")
  18.294 +    txt {* First pair of sums *}
  18.295 +    apply (simp add: root_cancel1)
  18.296 +    txt {* Second pair of sums *}
  18.297 +    apply (simp add: setsum_right_distrib)
  18.298 +    apply (simp add: power_add)
  18.299 +    apply (simp add: root_cancel1)
  18.300 +    apply (simp add: mult_ac)
  18.301 +    done
  18.302 +  finally show "?s = ?t" .
  18.303 +qed
  18.304 +
  18.305 +lemma DFT_upper:
  18.306 +  assumes mbound: "0 < m" and ibound: "m <= i"
  18.307 +  shows "DFT (2 * m) a i =
  18.308 +    DFT m (%i. a (2 * i)) (i - m) -
  18.309 +    root (2 * m) ^ (i - m) * DFT m (%i. a (2 * i + 1)) (i - m)"
  18.310 +proof (unfold DFT_def)
  18.311 +  have "(\<Sum>j = 0..<2 * m. root (2 * m) ^ (i * j) * a j) =
  18.312 +    (\<Sum>j = 0..<m. root (2 * m) ^ (i * (2 * j)) * a (2 * j)) +
  18.313 +    (\<Sum>j = 0..<m. root (2 * m) ^ (i * (2 * j + 1)) * a (2 * j + 1))"
  18.314 +    (is "?s = _")
  18.315 +    by (simp add: setsum_splice)
  18.316 +  also have "... =
  18.317 +    (\<Sum>j = 0..<m. root m ^ ((i - m) * j) * a (2 * j)) -
  18.318 +    root (2 * m) ^ (i - m) *
  18.319 +    (\<Sum>j = 0..<m. root m ^ ((i - m) * j) * a (2 * j + 1))"
  18.320 +    (is "_ = ?t")
  18.321 +    txt {* First pair of sums *}
  18.322 +    apply (simp add: root_cancel1)
  18.323 +    apply (simp add: root_unity ibound root_nonzero power_diff power_mult)
  18.324 +    txt {* Second pair of sums *}
  18.325 +    apply (simp add: mbound root_cancel2)
  18.326 +    apply (simp add: setsum_right_distrib)
  18.327 +    apply (simp add: power_add)
  18.328 +    apply (simp add: root_cancel1)
  18.329 +    apply (simp add: power_mult)
  18.330 +    apply (simp add: mult_ac)
  18.331 +    done
  18.332 +  finally show "?s = ?t" .
  18.333 +qed
  18.334 +
  18.335 +lemma IDFT_lower:
  18.336 +  "IDFT (2 * m) a i =
  18.337 +  IDFT m (%i. a (2 * i)) i +
  18.338 +  (1 / root (2 * m)) ^ i * IDFT m (%i. a (2 * i + 1)) i"
  18.339 +proof (unfold IDFT_def)
  18.340 +  have "(\<Sum>j = 0..<2 * m. a j / root (2 * m) ^ (i * j)) =
  18.341 +    (\<Sum>j = 0..<m. a (2 * j) / root (2 * m) ^ (i * (2 * j))) +
  18.342 +    (\<Sum>j = 0..<m. a (2 * j + 1) / root (2 * m) ^ (i * (2 * j + 1)))"
  18.343 +    (is "?s = _")
  18.344 +    by (simp add: setsum_splice)
  18.345 +  also have "... = (\<Sum>j = 0..<m. a (2 * j) / root m ^ (i * j)) +
  18.346 +    (1 / root (2 * m)) ^ i *
  18.347 +    (\<Sum>j = 0..<m. a (2 * j + 1) / root m ^ (i * j))"
  18.348 +    (is "_ = ?t")
  18.349 +    txt {* First pair of sums *}
  18.350 +    apply (simp add: root_cancel1)
  18.351 +    txt {* Second pair of sums *}
  18.352 +    apply (simp add: setsum_right_distrib)
  18.353 +    apply (simp add: power_add)
  18.354 +    apply (simp add: nonzero_power_divide root_nonzero)
  18.355 +    apply (simp add: root_cancel1)
  18.356 +    done
  18.357 +  finally show "?s = ?t" .
  18.358 +qed
  18.359 +
  18.360 +lemma IDFT_upper:
  18.361 +  assumes mbound: "0 < m" and ibound: "m <= i"
  18.362 +  shows "IDFT (2 * m) a i =
  18.363 +    IDFT m (%i. a (2 * i)) (i - m) -
  18.364 +    (1 / root (2 * m)) ^ (i - m) *
  18.365 +    IDFT m (%i. a (2 * i + 1)) (i - m)"
  18.366 +proof (unfold IDFT_def)
  18.367 +  have "(\<Sum>j = 0..<2 * m. a j / root (2 * m) ^ (i * j)) =
  18.368 +    (\<Sum>j = 0..<m. a (2 * j) / root (2 * m) ^ (i * (2 * j))) +
  18.369 +    (\<Sum>j = 0..<m. a (2 * j + 1) / root (2 * m) ^ (i * (2 * j + 1)))"
  18.370 +    (is "?s = _")
  18.371 +    by (simp add: setsum_splice)
  18.372 +  also have "... =
  18.373 +    (\<Sum>j = 0..<m. a (2 * j) / root m ^ ((i - m) * j)) -
  18.374 +    (1 / root (2 * m)) ^ (i - m) *
  18.375 +    (\<Sum>j = 0..<m. a (2 * j + 1) / root m ^ ((i - m) * j))"
  18.376 +    (is "_ = ?t")
  18.377 +    txt {* First pair of sums *}
  18.378 +    apply (simp add: root_cancel1)
  18.379 +    apply (simp add: root_unity ibound root_nonzero power_diff power_mult)
  18.380 +    txt {* Second pair of sums *}
  18.381 +    apply (simp add: nonzero_power_divide root_nonzero)
  18.382 +    apply (simp add: mbound root_cancel2)
  18.383 +    apply (simp add: setsum_divide_distrib)
  18.384 +    apply (simp add: power_add)
  18.385 +    apply (simp add: root_cancel1)
  18.386 +    apply (simp add: power_mult)
  18.387 +    apply (simp add: mult_ac)
  18.388 +    done
  18.389 +  finally show "?s = ?t" .
  18.390 +qed
  18.391 +
  18.392 +text {* @{text DFT} und @{text IDFT} are inverses. *}
  18.393 +
  18.394 +declare divide_divide_eq_right [simp del]
  18.395 +  divide_divide_eq_left [simp del]
  18.396 +
  18.397 +lemma power_diff_inverse:
  18.398 +  assumes nz: "(a::'a::field) ~= 0"
  18.399 +  shows "m <= n ==> (inverse a) ^ (n-m) = (a^m) / (a^n)"
  18.400 +  apply (induct n m rule: diff_induct)
  18.401 +    apply (simp add: nonzero_power_inverse
  18.402 +      nonzero_inverse_eq_divide [THEN sym] nz)
  18.403 +   apply simp
  18.404 +  apply (simp add: nz)
  18.405 +  done
  18.406 +
  18.407 +lemma power_diff_rev_if:
  18.408 +  assumes nz: "(a::'a::field) ~= 0"
  18.409 +  shows "(a^m) / (a^n) = (if n <= m then a ^ (m-n) else (1/a) ^ (n-m))"
  18.410 +proof (cases "n <= m")
  18.411 +  case True with nz show ?thesis
  18.412 +    by (simp add: power_diff)
  18.413 +next
  18.414 +  case False with nz show ?thesis
  18.415 +    by (simp add: power_diff_inverse nonzero_inverse_eq_divide [THEN sym])
  18.416 +qed
  18.417 +
  18.418 +lemma power_divides_special:
  18.419 +  "(a::'a::field) ~= 0 ==>
  18.420 +  a ^ (i * j) / a ^ (k * i) = (a ^ j / a ^ k) ^ i"
  18.421 +  by (simp add: nonzero_power_divide power_mult [THEN sym] mult_ac)
  18.422 +
  18.423 +theorem DFT_inverse:
  18.424 +  assumes i_less: "i < n"
  18.425 +  shows  "IDFT n (DFT n a) i = of_nat n * a i"
  18.426 +  using [[linarith_split_limit = 0]]
  18.427 +  apply (unfold DFT_def IDFT_def)
  18.428 +  apply (simp add: setsum_divide_distrib)
  18.429 +  apply (subst setsum_commute)
  18.430 +  apply (simp only: times_divide_eq_left [THEN sym])
  18.431 +  apply (simp only: power_divides_special [OF root_nonzero])
  18.432 +  apply (simp add: power_diff_rev_if root_nonzero)
  18.433 +  apply (simp add: setsum_divide_distrib [THEN sym]
  18.434 +    setsum_left_distrib [THEN sym])
  18.435 +  proof -
  18.436 +    from i_less have i_diff: "!!k. i - k < n" by arith
  18.437 +    have diff_i: "!!k. k < n ==> k - i < n" by arith
  18.438 +
  18.439 +    let ?sum = "%i j n. setsum (op ^ (if i <= j then root n ^ (j - i)
  18.440 +                  else (1 / root n) ^ (i - j))) {0..<n} * a j"
  18.441 +    let ?sum1 = "%i j n. setsum (op ^ (root n ^ (j - i))) {0..<n} * a j"
  18.442 +    let ?sum2 = "%i j n. setsum (op ^ ((1 / root n) ^ (i - j))) {0..<n} * a j"
  18.443 +
  18.444 +    from i_less have "(\<Sum>j = 0..<n. ?sum i j n) =
  18.445 +      (\<Sum>j = 0..<i. ?sum2 i j n) + (\<Sum>j = i..<n. ?sum1 i j n)"
  18.446 +      (is "?s = _")
  18.447 +      by (simp add: root_summation_inv nat_dvd_not_less
  18.448 +        setsum_add_split_nat_ivl [where f = "%j. ?sum i j n"])
  18.449 +    also from i_less i_diff
  18.450 +    have "... = (\<Sum>j = i..<n. ?sum1 i j n)"
  18.451 +      by (simp add: root_summation_inv nat_dvd_not_less)
  18.452 +    also from i_less have "... =
  18.453 +      (\<Sum>j\<in>{i} \<union> {i<..<n}. ?sum1 i j n)"
  18.454 +      by (simp only: ivl_disj_un)
  18.455 +    also have "... =
  18.456 +      (?sum1 i i n + (\<Sum>j\<in>{i<..<n}. ?sum1 i j n))"
  18.457 +      by (simp add: setsum_Un_disjoint ivl_disj_int)
  18.458 +    also from i_less diff_i have "... = ?sum1 i i n"
  18.459 +      by (simp add: root_summation nat_dvd_not_less)
  18.460 +    also from i_less have "... = of_nat n * a i" (is "_ = ?t")
  18.461 +      by (simp add: of_nat_cplx)
  18.462 +    finally show "?s = ?t" .
  18.463 +  qed
  18.464 +
  18.465 +
  18.466 +section {* Discrete, Fast Fourier Transformation *}
  18.467 +
  18.468 +text {* @{text "FFT k a"} is the transform of vector @{text a}
  18.469 +  of length @{text "2 ^ k"}, @{text IFFT} its inverse. *}
  18.470 +
  18.471 +primrec FFT :: "nat => (nat => complex) => (nat => complex)" where
  18.472 +  "FFT 0 a = a"
  18.473 +| "FFT (Suc k) a =
  18.474 +     (let (x, y) = (FFT k (%i. a (2*i)), FFT k (%i. a (2*i+1)))
  18.475 +      in (%i. if i < 2^k
  18.476 +            then x i + (root (2 ^ (Suc k))) ^ i * y i
  18.477 +            else x (i- 2^k) - (root (2 ^ (Suc k))) ^ (i- 2^k) * y (i- 2^k)))"
  18.478 +
  18.479 +primrec IFFT :: "nat => (nat => complex) => (nat => complex)" where
  18.480 +  "IFFT 0 a = a"
  18.481 +| "IFFT (Suc k) a =
  18.482 +     (let (x, y) = (IFFT k (%i. a (2*i)), IFFT k (%i. a (2*i+1)))
  18.483 +      in (%i. if i < 2^k
  18.484 +            then x i + (1 / root (2 ^ (Suc k))) ^ i * y i
  18.485 +            else x (i - 2^k) -
  18.486 +              (1 / root (2 ^ (Suc k))) ^ (i - 2^k) * y (i - 2^k)))"
  18.487 +
  18.488 +text {* Finally, for vectors of length @{text "2 ^ k"},
  18.489 +  @{text DFT} and @{text FFT}, and @{text IDFT} and
  18.490 +  @{text IFFT} are equivalent. *}
  18.491 +
  18.492 +theorem DFT_FFT:
  18.493 +  "!!a i. i < 2 ^ k ==> DFT (2 ^ k) a i = FFT k a i"
  18.494 +proof (induct k)
  18.495 +  case 0
  18.496 +  then show ?case by (simp add: DFT_def)
  18.497 +next
  18.498 +  case (Suc k)
  18.499 +  assume i: "i < 2 ^ Suc k"
  18.500 +  show ?case proof (cases "i < 2 ^ k")
  18.501 +    case True
  18.502 +    then show ?thesis apply simp apply (simp add: DFT_lower)
  18.503 +      apply (simp add: Suc) done
  18.504 +  next
  18.505 +    case False
  18.506 +    from i have "i - 2 ^ k < 2 ^ k" by simp
  18.507 +    with False i show ?thesis apply simp apply (simp add: DFT_upper)
  18.508 +      apply (simp add: Suc) done
  18.509 +  qed
  18.510 +qed
  18.511 +
  18.512 +theorem IDFT_IFFT:
  18.513 +  "!!a i. i < 2 ^ k ==> IDFT (2 ^ k) a i = IFFT k a i"
  18.514 +proof (induct k)
  18.515 +  case 0
  18.516 +  then show ?case by (simp add: IDFT_def)
  18.517 +next
  18.518 +  case (Suc k)
  18.519 +  assume i: "i < 2 ^ Suc k"
  18.520 +  show ?case proof (cases "i < 2 ^ k")
  18.521 +    case True
  18.522 +    then show ?thesis apply simp apply (simp add: IDFT_lower)
  18.523 +      apply (simp add: Suc) done
  18.524 +  next
  18.525 +    case False
  18.526 +    from i have "i - 2 ^ k < 2 ^ k" by simp
  18.527 +    with False i show ?thesis apply simp apply (simp add: IDFT_upper)
  18.528 +      apply (simp add: Suc) done
  18.529 +  qed
  18.530 +qed
  18.531 +
  18.532 +schematic_lemma "map (FFT (Suc (Suc 0)) a) [0, 1, 2, 3] = ?x"
  18.533 +  by simp
  18.534 +
  18.535 +end

    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/doc-isac/jrocnik/Makefile	Tue Sep 17 09:50:52 2013 +0200
    19.3 @@ -0,0 +1,81 @@
    19.4 +## targets
    19.5 +
    19.6 +default: thesis clean
    19.7 +all: thesis docu present clean
    19.8 +thesis: thesis clean
    19.9 +docu: docu clean
   19.10 +present: present1 present2 clean
   19.11 +cadgme: cadgme clean
   19.12 +
   19.13 +
   19.14 +## dependencies
   19.15 +
   19.16 +
   19.17 +## settings
   19.18 +
   19.19 +LATEX = latex
   19.20 +PDFLATEX = pdflatex
   19.21 +BIBTEX = bibtex
   19.22 +RAIL = rail -a
   19.23 +SEDINDEX = ./sedindex
   19.24 +FIXBOOKMARKS = perl -pi fixbookmarks.pl
   19.25 +
   19.26 +DEFAULT_GARBAGE = *.aux *.log *.toc *.idx *.rai *.rao *.bbl *.ind *.ilg *.blg *.out *.lof
   19.27 +DEFAULT_OUTPUT = *.dvi jrocnik_present1.pdf jrocnik_present2.pdf jrocnik_bakk.pdf *.ps
   19.28 +GARBAGE =
   19.29 +OUTPUT =
   19.30 +
   19.31 +## special targets
   19.32 +
   19.33 +.DELETE_ON_ERROR:
   19.34 +
   19.35 +## actions
   19.36 +
   19.37 +nothing:
   19.38 +
   19.39 +clean:
   19.40 +	@rm -f $(DEFAULT_GARBAGE) $(GARBAGE)
   19.41 +
   19.42 +mrproper:
   19.43 +	@rm -f $(DEFAULT_GARBAGE) $(DEFAULT_OUTPUT) $(GARBAGE) $(OUTPUT)
   19.44 +
   19.45 +THESIS_NAME = jrocnik_bakk
   19.46 +THESIS_FILES = jrocnik_bakk.tex
   19.47 +
   19.48 +DOCU_NAME = Inverse_Z_Transform/doc/Inverse_Z_Transform
   19.49 +DOCU_FILES = Inverse_Z_Transform/doc/root.tex 
   19.50 +
   19.51 +PRESENT1_NAME = jrocnik_present1
   19.52 +PRESENT1_FILES = jrocnik_present1.tex
   19.53 +
   19.54 +PRESENT2_NAME = jrocnik_present2
   19.55 +PRESENT2_FILES = jrocnik_present2.tex
   19.56 +
   19.57 +CADGME_NAME = jrocnik_cadgme
   19.58 +CADGME_FILES = cadgme.tex
   19.59 +
   19.60 +thesis: $(THESIS_NAME).pdf
   19.61 +
   19.62 +$(THESIS_NAME).pdf: $(THESIS_FILES)
   19.63 +	$(PDFLATEX) $(THESIS_NAME)
   19.64 +	$(BIBTEX) $(THESIS_NAME)
   19.65 +	$(PDFLATEX) $(THESIS_NAME)
   19.66 +	$(PDFLATEX) $(THESIS_NAME)
   19.67 +  
   19.68 +present1: $(PRESENT1_NAME).pdf
   19.69 +
   19.70 +$(PRESENT1_NAME).pdf: $(PRESENT1_FILES)
   19.71 +	$(PDFLATEX) $(PRESENT1_NAME)
   19.72 +	$(PDFLATEX) $(PRESENT1_NAME)
   19.73 +  
   19.74 +present2: $(PRESENT2_NAME).pdf
   19.75 +
   19.76 +$(PRESENT2_NAME).pdf: $(PRESENT2_FILES)
   19.77 +	$(PDFLATEX) $(PRESENT2_NAME)
   19.78 +	$(PDFLATEX) $(PRESENT2_NAME)
   19.79 +  
   19.80 +cadgme: $(CADGME_NAME).pdf
   19.81 +
   19.82 +$(CADGME_NAME).pdf: $(CADGME_FILES)
   19.83 +	$(PDFLATEX) $(CADGME_NAME)
   19.84 +	$(PDFLATEX) $(CADGME_NAME)

    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/doc-isac/jrocnik/TUGlogo.pdf	Tue Sep 17 09:50:52 2013 +0200
    20.3 @@ -0,0 +1,219 @@
    20.4 +%PDF-1.3
    20.5 +%����
    20.6 +2 0 obj
    20.7 +<<
    20.8 +/Length 2930
    20.9 +>>
   20.10 +stream
   20.11 +0 0.957 0.569 0 k
   20.12 +/GS1 gs
   20.13 +0 31.119 20.745 -20.746 re
   20.14 +f
   20.15 +22.819 31.119 20.746 -20.746 re
   20.16 +f
   20.17 +q
   20.18 +1 i 
   20.19 +0 41.492 112.876 -41.432 re
   20.20 +W n
   20.21 +45.641 31.119 20.744 -20.746 re
   20.22 +f
   20.23 +10.372 20.746 20.747 -20.686 re
   20.24 +f
   20.25 +Q
   20.26 +35.268 41.492 20.744 -20.746 re
   20.27 +f
   20.28 +0.941 0.82 0.808 0.894 k
   20.29 +1 i 
   20.30 +75.104 27.791 m
   20.31 +68.462 27.791 l
   20.32 +68.462 31.11 l
   20.33 +85.581 31.11 l
   20.34 +85.581 27.791 l
   20.35 +78.94 27.791 l
   20.36 +78.94 10.417 l
   20.37 +75.104 10.417 l
   20.38 +75.104 27.791 l
   20.39 +f
   20.40 +q
   20.41 +0 41.492 112.876 -41.432 re
   20.42 +W n
   20.43 +104.828 18.021 m
   20.44 +104.828 16.774 104.604 15.649 104.156 14.646 c
   20.45 +103.708 13.643 103.097 12.79 102.321 12.09 c
   20.46 +101.546 11.387 100.631 10.848 99.57 10.469 c
   20.47 +98.511 10.088 97.359 9.898 96.115 9.898 c
   20.48 +94.873 9.898 93.722 10.088 92.661 10.469 c
   20.49 +91.601 10.848 90.678 11.387 89.895 12.09 c
   20.50 +89.109 12.79 88.497 13.643 88.061 14.646 c
   20.51 +87.621 15.649 87.403 16.774 87.403 18.021 c
   20.52 +87.403 31.11 l
   20.53 +91.241 31.11 l
   20.54 +91.241 18.153 l
   20.55 +91.241 17.648 91.321 17.117 91.485 16.562 c
   20.56 +91.648 16.008 91.919 15.497 92.298 15.029 c
   20.57 +92.676 14.563 93.177 14.178 93.801 13.877 c
   20.58 +94.423 13.576 95.194 13.425 96.115 13.425 c
   20.59 +97.035 13.425 97.808 13.576 98.431 13.877 c
   20.60 +99.054 14.178 99.556 14.563 99.934 15.029 c
   20.61 +100.312 15.497 100.582 16.008 100.746 16.562 c
   20.62 +100.909 17.117 100.991 17.648 100.991 18.153 c
   20.63 +100.991 31.11 l
   20.64 +104.828 31.11 l
   20.65 +104.828 18.021 l
   20.66 +f
   20.67 +83.257 7.566 m
   20.68 +82.496 7.895 81.511 8.052 80.723 8.052 c
   20.69 +78.43 8.052 77.162 6.609 77.162 4.734 c
   20.70 +77.162 2.873 78.401 1.471 80.497 1.471 c
   20.71 +81.032 1.471 81.456 1.523 81.793 1.602 c
   20.72 +81.793 3.987 l
   20.73 +79.71 3.987 l
   20.74 +79.71 5.43 l
   20.75 +83.679 5.43 l
   20.76 +83.679 0.5 l
   20.77 +82.638 0.238 81.553 0.028 80.497 0.028 c
   20.78 +77.316 0.028 75.106 1.51 75.106 4.604 c
   20.79 +75.106 7.737 77.162 9.494 80.497 9.494 c
   20.80 +81.638 9.494 82.538 9.35 83.383 9.113 c
   20.81 +83.257 7.566 l
   20.82 +f
   20.83 +85.62 6.938 m
   20.84 +87.296 6.938 l
   20.85 +87.296 5.403 l
   20.86 +87.324 5.403 l
   20.87 +87.408 6.033 88.182 7.095 89.308 7.095 c
   20.88 +89.491 7.095 89.689 7.095 89.885 7.042 c
   20.89 +89.885 5.272 l
   20.90 +89.717 5.363 89.379 5.416 89.04 5.416 c
   20.91 +87.507 5.416 87.507 3.633 87.507 2.664 c
   20.92 +87.507 0.186 l
   20.93 +85.62 0.186 l
   20.94 +85.62 6.938 l
   20.95 +f
   20.96 +93.587 1.312 m
   20.97 +94.164 1.312 94.614 1.549 94.909 1.916 c
   20.98 +95.219 2.296 95.304 2.781 95.304 3.306 c
   20.99 +94.487 3.306 l
  20.100 +93.644 3.306 92.391 3.175 92.391 2.139 c
  20.101 +92.391 1.563 92.911 1.312 93.587 1.312 c
  20.102 +h
  20.103 +91.376 6.583 m
  20.104 +92.107 6.898 93.094 7.095 93.896 7.095 c
  20.105 +96.105 7.095 97.021 6.242 97.021 4.249 c
  20.106 +97.021 3.384 l
  20.107 +97.021 2.703 97.035 2.191 97.049 1.693 c
  20.108 +97.063 1.182 97.091 0.71 97.134 0.186 c
  20.109 +95.473 0.186 l
  20.110 +95.402 0.539 95.402 0.985 95.389 1.195 c
  20.111 +95.359 1.195 l
  20.112 +94.924 0.448 93.979 0.028 93.122 0.028 c
  20.113 +91.842 0.028 90.588 0.749 90.588 2.034 c
  20.114 +90.588 3.043 91.108 3.633 91.827 3.961 c
  20.115 +92.546 4.289 93.474 4.355 94.263 4.355 c
  20.116 +95.304 4.355 l
  20.117 +95.304 5.442 94.783 5.81 93.671 5.81 c
  20.118 +92.869 5.81 92.066 5.522 91.434 5.076 c
  20.119 +91.376 6.583 l
  20.120 +f
  20.121 +98.569 6.938 m
  20.122 +104.312 6.938 l
  20.123 +104.312 5.495 l
  20.124 +100.707 1.549 l
  20.125 +104.438 1.549 l
  20.126 +104.438 0.186 l
  20.127 +98.414 0.186 l
  20.128 +98.414 1.615 l
  20.129 +102.087 5.574 l
  20.130 +98.569 5.574 l
  20.131 +98.569 6.938 l
  20.132 +f
  20.133 +0 0.957 0.569 0 k
  20.134 +105.965 6.911 6.911 -6.851 re
  20.135 +f
  20.136 +Q
  20.137 +endstream
  20.138 +endobj
  20.139 +3 0 obj
  20.140 +<<
  20.141 +/ProcSet [/PDF ]
  20.142 +/ExtGState <<
  20.143 +/GS1 4 0 R
  20.144 +>>
  20.145 +>>
  20.146 +endobj
  20.147 +4 0 obj
  20.148 +<<
  20.149 +/Type /ExtGState
  20.150 +/SA false
  20.151 +/SM 0.02
  20.152 +/OP false
  20.153 +/op false
  20.154 +/OPM 1
  20.155 +/BG2 /Default
  20.156 +/UCR2 /Default
  20.157 +/HT /Default
  20.158 +/TR2 /Default
  20.159 +>>
  20.160 +endobj
  20.161 +1 0 obj
  20.162 +<<
  20.163 +/Type /Page
  20.164 +/Parent 5 0 R
  20.165 +/Resources 3 0 R
  20.166 +/Contents 2 0 R
  20.167 +>>
  20.168 +endobj
  20.169 +6 0 obj
  20.170 +<<
  20.171 +/S /D
  20.172 +>>
  20.173 +endobj
  20.174 +7 0 obj
  20.175 +<<
  20.176 +/Nums [0 6 0 R ]
  20.177 +>>
  20.178 +endobj
  20.179 +5 0 obj
  20.180 +<<
  20.181 +/Type /Pages
  20.182 +/Kids [1 0 R]
  20.183 +/Count 1
  20.184 +/MediaBox [0 0 113 42]
  20.185 +>>
  20.186 +endobj
  20.187 +8 0 obj
  20.188 +<<
  20.189 +/CreationDate (D:20060111234722+13'00')
  20.190 +/ModDate (D:20060111234722+13'00')
  20.191 +/Producer (PSNormalizer.framework)
  20.192 +>>
  20.193 +endobj
  20.194 +9 0 obj
  20.195 +<<
  20.196 +/Type /Catalog
  20.197 +/Pages 5 0 R
  20.198 +/PageLabels 7 0 R
  20.199 +>>
  20.200 +endobj
  20.201 +xref
  20.202 +0 10
  20.203 +0000000000 65535 f 
  20.204 +0000003204 00000 n 
  20.205 +0000000016 00000 n 
  20.206 +0000002998 00000 n 
  20.207 +0000003064 00000 n 
  20.208 +0000003349 00000 n 
  20.209 +0000003284 00000 n 
  20.210 +0000003311 00000 n 
  20.211 +0000003429 00000 n 
  20.212 +0000003560 00000 n 
  20.213 +trailer
  20.214 +<<
  20.215 +/Size 10
  20.216 +/Root 9 0 R
  20.217 +/Info 8 0 R
  20.218 +/ID [<99444215e2a4a31d5c4ca09b38102d5e><99444215e2a4a31d5c4ca09b38102d5e>]
  20.219 +>>
  20.220 +startxref
  20.221 +3627
  20.222 +%%EOF

    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/doc-isac/jrocnik/Test_Complex.thy	Tue Sep 17 09:50:52 2013 +0200
    21.3 @@ -0,0 +1,113 @@
    21.4 +theory Test_Complex imports Isac begin
    21.5 +
    21.6 +section {*terms and operations*}
    21.7 +ML {*
    21.8 +  print_depth 999; @{term "Complex 1 (2::real)"};
    21.9 +*}
   21.10 +ML {*
   21.11 +@{term "Complex 1 2 + Complex 3 4"};
   21.12 +print_depth 999; str2term "Complex 1 2 + Complex 3 4"; print_depth 999;
   21.13 +*}
   21.14 +ML {*
   21.15 +@{term "Complex 1 2 * Complex 3 4"};
   21.16 +@{term "Complex 1 2 - Complex 3 4"};
   21.17 +@{term "Complex 1 2 / Complex 3 4"};
   21.18 +(*@{term "Complex 1 2 ^ Complex 3 4"};
   21.19 +  Type unification failed: Clash of types "complex" and "nat"
   21.20 +  Operator:  op ^ (Complex 1 2) :: nat \<Rightarrow> complex
   21.21 +  Operand:   Complex 3 4 :: complex*)
   21.22 +*}
   21.23 +ML {*
   21.24 +term2str @{term "Complex 1 2 + Complex 3 4"};
   21.25 +term2str @{term "Complex 1 2 / Complex 3 4"};
   21.26 +*}
   21.27 +
   21.28 +ML {*
   21.29 +val a = @{term "Complex 1 2"};
   21.30 +atomty a;
   21.31 +val a = str2term "Complex 1 2";
   21.32 +atomty a;
   21.33 +*}
   21.34 +ML {*
   21.35 +val b = @{term "Complex 3 4"};
   21.36 +val b = str2term "Complex 3 4";
   21.37 +(*a + (b::complex); ERROR: term + term*)
   21.38 +*}
   21.39 +
   21.40 +section {*use the operations for simplification*}
   21.41 +
   21.42 +
   21.43 +
   21.44 +subsection {*example 1 -- ADD*}
   21.45 +ML {*
   21.46 +  print_depth 1;
   21.47 +  val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
   21.48 +*}
   21.49 +ML {*
   21.50 +  val thm = @{thm "complex_add"};
   21.51 +  val t = str2term "Complex 1 2 + Complex 3 4";
   21.52 +  val SOME _ = rewrite_ thy ro er true thm t;
   21.53 +  val SOME (t', _) = rewrite_ thy ro er true thm t;
   21.54 +  "Complex (1 + 3) (2 + 4)" = term2str t';
   21.55 +*}
   21.56 +
   21.57 +
   21.58 +
   21.59 +
   21.60 +subsection {*example 2 -- ADD, MULT*}
   21.61 +ML {*
   21.62 +
   21.63 +val Simplify_complex = append_rls "Simplify_complex" e_rls
   21.64 +  [ Thm  ("complex_add",num_str @{thm complex_add}),
   21.65 +		    Thm  ("complex_mult",num_str @{thm complex_mult}),
   21.66 +		    Rls_ norm_Poly
   21.67 +		  ];
   21.68 +
   21.69 +*}
   21.70 +ML {*
   21.71 +
   21.72 +val t = str2term "(Complex 1 2 * (Complex 3 4 + Complex 5 (6::real)))";
   21.73 +term2str t = "Complex 1 2 * (Complex 3 4 + Complex 5 6)";
   21.74 +atomty t;
   21.75 +
   21.76 +*}
   21.77 +ML {*
   21.78 +
   21.79 +
   21.80 +val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
   21.81 +
   21.82 +term2str t = "Complex -12 26";
   21.83 +atomty t;
   21.84 +
   21.85 +*}
   21.86 +
   21.87 +subsection {*example 3*}
   21.88 +ML {*
   21.89 +val Simplify_complex = append_rls "Simplify_complex" e_rls
   21.90 +  [ Thm  ("complex_mult",num_str @{thm complex_mult}),
   21.91 +    Thm  ("complex_inverse",num_str @{thm complex_inverse}),
   21.92 +		    Rls_ norm_Poly
   21.93 +		  ];
   21.94 +*}
   21.95 +ML {*
   21.96 +val t = str2term "inverse (Complex (2::real) (4::real))";
   21.97 +term2str t = "inverse Complex (2) (4)";
   21.98 +atomty t;
   21.99 +*}
  21.100 +ML {*
  21.101 +trace_rewrite := true;
  21.102 +val SOME (t, _) = rewrite_set_ thy true Simplify_complex t;
  21.103 +trace_rewrite := false;
  21.104 +term2str t = "Complex -12 26";
  21.105 +atomty t;
  21.106 +*}
  21.107 +
  21.108 +
  21.109 +
  21.110 +ML {*
  21.111 +trace_rewrite := true;
  21.112 +trace_rewrite := false;
  21.113 +*}
  21.114 +
  21.115 +end
  21.116 +

    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/doc-isac/jrocnik/Test_Integral.thy	Tue Sep 17 09:50:52 2013 +0200
    22.3 @@ -0,0 +1,17 @@
    22.4 +(*
    22.5 +doc-src/isac/jrocnik$ /usr/local/isabisac/bin/isabelle jedit Test_Integral.thy &
    22.6 +*)
    22.7 +
    22.8 +theory Test_Integral imports "../../../src/HOL/Multivariate_Analysis/Integration"
    22.9 +Integration begin
   22.10 +
   22.11 +ML {*
   22.12 +@{term "Integral s f k"}
   22.13 +*}
   22.14 +ML {*
   22.15 +*}
   22.16 +ML {*
   22.17 +*}
   22.18 +
   22.19 +end
   22.20 +

    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/doc-isac/jrocnik/Test_SUM.thy	Tue Sep 17 09:50:52 2013 +0200
    23.3 @@ -0,0 +1,28 @@
    23.4 +
    23.5 +theory Test_SUM imports Isac begin
    23.6 +
    23.7 +section {*trials with implicit function, probably required*}
    23.8 +ML {*
    23.9 +@{term "(%n :: nat. n) 2"};
   23.10 +@{term "(%n. n) 2"};
   23.11 +@{term "2"};
   23.12 +*}
   23.13 +ML {*
   23.14 +@{term "(%n. n+n)"};
   23.15 +@{term "(%n. n+n) a"};
   23.16 +@{term "a+a"};
   23.17 +*}
   23.18 +section {*sums*}
   23.19 +ML {*
   23.20 +val x = @{term "(SUM i = 0..< k. f i)"};
   23.21 +term2str x
   23.22 +*}
   23.23 +ML {*
   23.24 +*}
   23.25 +ML {*
   23.26 +*}
   23.27 +ML {*
   23.28 +*}
   23.29 +
   23.30 +end
   23.31 +

    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/doc-isac/jrocnik/bakkarbeit.tcp	Tue Sep 17 09:50:52 2013 +0200
    24.3 @@ -0,0 +1,12 @@
    24.4 +[FormatInfo]
    24.5 +Type=TeXnicCenterProjectInformation
    24.6 +Version=4
    24.7 +
    24.8 +[ProjectInfo]
    24.9 +MainFile=jrocnik_bakk.tex
   24.10 +UseBibTeX=1
   24.11 +UseMakeIndex=0
   24.12 +ActiveProfile=LaTeX => PDF (Sumatra)
   24.13 +ProjectLanguage=en
   24.14 +ProjectDialect=US
   24.15 +

    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/doc-isac/jrocnik/bakkarbeit.tps	Tue Sep 17 09:50:52 2013 +0200
    25.3 @@ -0,0 +1,154 @@
    25.4 +[FormatInfo]
    25.5 +Type=TeXnicCenterProjectSessionInformation
    25.6 +Version=2
    25.7 +
    25.8 +[SessionInfo]
    25.9 +ActiveTab=0
   25.10 +FrameCount=5
   25.11 +ActiveFrame=0
   25.12 +
   25.13 +[Frame0]
   25.14 +Columns=1
   25.15 +Rows=1
   25.16 +Flags=2
   25.17 +ShowCmd=3
   25.18 +MinPos.x=-1
   25.19 +MinPos.y=-1
   25.20 +MaxPos.x=-4
   25.21 +MaxPos.y=-23
   25.22 +NormalPos.left=0
   25.23 +NormalPos.top=0
   25.24 +NormalPos.right=112
   25.25 +NormalPos.bottom=299
   25.26 +Class=CLatexEdit
   25.27 +Document=jrocnik_bakk.tex
   25.28 +
   25.29 +[Frame0_Row0]
   25.30 +cyCur=848
   25.31 +cyMin=10
   25.32 +
   25.33 +[Frame0_Col0]
   25.34 +cxCur=992
   25.35 +cxMin=10
   25.36 +
   25.37 +[Frame0_View0,0]
   25.38 +Cursor.row=143
   25.39 +Cursor.column=297
   25.40 +TopSubLine=145
   25.41 +
   25.42 +[Frame1]
   25.43 +Columns=1
   25.44 +Rows=1
   25.45 +Flags=0
   25.46 +ShowCmd=1
   25.47 +MinPos.x=-1
   25.48 +MinPos.y=-1
   25.49 +MaxPos.x=-4
   25.50 +MaxPos.y=-23
   25.51 +NormalPos.left=44
   25.52 +NormalPos.top=44
   25.53 +NormalPos.right=676
   25.54 +NormalPos.bottom=512
   25.55 +Class=CLatexEdit
   25.56 +Document=calulations.tex
   25.57 +
   25.58 +[Frame1_Row0]
   25.59 +cyCur=421
   25.60 +cyMin=10
   25.61 +
   25.62 +[Frame1_Col0]
   25.63 +cxCur=604
   25.64 +cxMin=10
   25.65 +
   25.66 +[Frame1_View0,0]
   25.67 +Cursor.row=52
   25.68 +Cursor.column=25
   25.69 +TopSubLine=35
   25.70 +
   25.71 +[Frame2]
   25.72 +Columns=1
   25.73 +Rows=1
   25.74 +Flags=0
   25.75 +ShowCmd=1
   25.76 +MinPos.x=-1
   25.77 +MinPos.y=-1
   25.78 +MaxPos.x=-4
   25.79 +MaxPos.y=-23
   25.80 +NormalPos.left=66
   25.81 +NormalPos.top=66
   25.82 +NormalPos.right=698
   25.83 +NormalPos.bottom=534
   25.84 +Class=CLatexEdit
   25.85 +Document=bakkarbeit_titlepage.tex
   25.86 +
   25.87 +[Frame2_Row0]
   25.88 +cyCur=421
   25.89 +cyMin=10
   25.90 +
   25.91 +[Frame2_Col0]
   25.92 +cxCur=604
   25.93 +cxMin=10
   25.94 +
   25.95 +[Frame2_View0,0]
   25.96 +Cursor.row=7
   25.97 +Cursor.column=0
   25.98 +TopSubLine=0
   25.99 +
  25.100 +[Frame3]
  25.101 +Columns=1
  25.102 +Rows=1
  25.103 +Flags=0
  25.104 +ShowCmd=1
  25.105 +MinPos.x=-1
  25.106 +MinPos.y=-1
  25.107 +MaxPos.x=-4
  25.108 +MaxPos.y=-23
  25.109 +NormalPos.left=88
  25.110 +NormalPos.top=88
  25.111 +NormalPos.right=1134
  25.112 +NormalPos.bottom=670
  25.113 +Class=CLatexEdit
  25.114 +Document=preambleForGeneratedDocuments.tex
  25.115 +
  25.116 +[Frame3_Row0]
  25.117 +cyCur=535
  25.118 +cyMin=10
  25.119 +
  25.120 +[Frame3_Col0]
  25.121 +cxCur=1018
  25.122 +cxMin=10
  25.123 +
  25.124 +[Frame3_View0,0]
  25.125 +Cursor.row=3
  25.126 +Cursor.column=30
  25.127 +TopSubLine=0
  25.128 +
  25.129 +[Frame4]
  25.130 +Columns=1
  25.131 +Rows=1
  25.132 +Flags=0
  25.133 +ShowCmd=1
  25.134 +MinPos.x=-1
  25.135 +MinPos.y=-1
  25.136 +MaxPos.x=-4
  25.137 +MaxPos.y=-23
  25.138 +NormalPos.left=110
  25.139 +NormalPos.top=110
  25.140 +NormalPos.right=1156
  25.141 +NormalPos.bottom=692
  25.142 +Class=CLatexEdit
  25.143 +Document=references.bib
  25.144 +
  25.145 +[Frame4_Row0]
  25.146 +cyCur=535
  25.147 +cyMin=10
  25.148 +
  25.149 +[Frame4_Col0]
  25.150 +cxCur=1018
  25.151 +cxMin=10
  25.152 +
  25.153 +[Frame4_View0,0]
  25.154 +Cursor.row=24
  25.155 +Cursor.column=15
  25.156 +TopSubLine=0
  25.157 +

    26.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.2 +++ b/doc-isac/jrocnik/bakkarbeit_titlepage.tex	Tue Sep 17 09:50:52 2013 +0200
    26.3 @@ -0,0 +1,44 @@
    26.4 +\begin{titlepage}
    26.5 +
    26.6 +	% Top of the page
    26.7 +	\vspace*{-2cm}
    26.8 +	\hfill
    26.9 +	\begin{minipage}{4cm}
   26.10 +		\includegraphics[width=40mm]{./TUGlogo.pdf}
   26.11 +	\end{minipage}
   26.12 +	
   26.13 +	% Center of the page
   26.14 +	\begin{center}
   26.15 +		\vspace{1cm}  
   26.16 +		
   26.17 +		\normalsize{Baccalaureate Thesis}\\
   26.18 +		
   26.19 +		\HRule
   26.20 +		\vspace{0.3cm}
   26.21 +		\Large{
   26.22 +		  	\bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\
   26.23 +		  }
   26.24 +		\HRule
   26.25 +			
   26.26 +			\vspace{1cm}
   26.27 +			\normalsize{conducted at the}\\
   26.28 +			\normalsize{Institute for Software Technology}\\
   26.29 +			\normalsize{Institute of Signal Processing and Speech Communication}\\
   26.30 +			\vspace{0.3cm}
   26.31 +			\normalsize{Graz University of Technology}\\
   26.32 +			
   26.33 +			\vspace{1cm}
   26.34 +			\normalsize{by}\\
   26.35 +			Jan Simon Ro\v{c}nik\\\href{mailto:student.tugraz.at}{\tt jan.rocnik@student.tugraz.at}
   26.36 +			
   26.37 +			\vspace{1cm}
   26.38 +			\normalsize{Supervisor}\\
   26.39 +			Univ.-Prof. Dipl.-Ing. Dr.techn. Franz Wotawa
   26.40 +		\vfill
   26.41 +		
   26.42 +		% Bottom of the page
   26.43 +		{\large Graz, \today}
   26.44 +	
   26.45 +	\end{center}
   26.46 +
   26.47 +\end{titlepage}
   26.48 \ No newline at end of file

    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/doc-isac/jrocnik/calulations.tex	Tue Sep 17 09:50:52 2013 +0200
    27.3 @@ -0,0 +1,202 @@
    27.4 +%\documentclass[a4paper]{scrartcl}
    27.5 +%\usepackage[top=2cm, bottom=2.5cm, left=3cm, right=2cm, footskip=1cm]{geometry}
    27.6 +%\usepackage[german]{babel}
    27.7 +%\usepackage[T1]{fontenc}
    27.8 +%\usepackage[latin1]{inputenc}
    27.9 +%\usepackage{endnotes}
   27.10 +%\usepackage{trfsigns}
   27.11 +%\usepackage{setspace}
   27.12 +%
   27.13 +%\setlength{\parindent}{0ex}
   27.14 +%\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
   27.15 +%\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
   27.16 +%
   27.17 +%\begin{document}
   27.18 +%\title{Interactive Course Material for Signal Processing based on Isabelle/\isac}
   27.19 +%\subtitle{Problemsolutions (Calculations)}
   27.20 +%\author{Walther Neuper, Jan Rocnik}
   27.21 +%\maketitle
   27.22 +
   27.23 +
   27.24 +%------------------------------------------------------------------------------
   27.25 +%FOURIER
   27.26 +
   27.27 +\subsection{Fourier Transformation}
   27.28 +\subsubsection*{Problem\endnote{Problem submitted by Bernhard Geiger. Originally fragment of the exam to \emph{Signaltransformationen VO} from 04.03.2011. Translated from German.}}
   27.29 +\textbf{(a)} Determine the fourier transform for the given rectangular impulse:
   27.30 +
   27.31 +\begin{center}
   27.32 +$x(t)= \left\{
   27.33 +     \begin{array}{lr}
   27.34 +       1 & -1\leq t\geq1\\
   27.35 +       0 & else
   27.36 +     \end{array}
   27.37 +   \right.$
   27.38 +\end{center}
   27.39 +
   27.40 +\textbf{\noindent (b)} Now consider the given delayed impulse, determine its fourie transformation and calculate phase and magnitude:
   27.41 +
   27.42 +\begin{center}
   27.43 +$x(t)= \left\{
   27.44 +     \begin{array}{lr}
   27.45 +       1 & -1\leq t\leq1\\
   27.46 +       0 & else
   27.47 +     \end{array}
   27.48 +   \right.$
   27.49 +\end{center}
   27.50 +
   27.51 +\subsubsection{Solution}
   27.52 +\textbf{(a)} \textsf{Subproblem 1}
   27.53 +\onehalfspace{
   27.54 +\begin{tabbing}
   27.55 +000\=\kill
   27.56 +\texttt{\footnotesize{01}} \> Definition: $X(j\omega)=\int_\infty^\infty{x(t)\cdot e^{-j\omega t}}$\\
   27.57 +\`Insert Condition: $x(t) = 1\;$ for $\;\{-1\leq t\;\land\;t\leq 1\}\;$ and $\;x(t)=0\;$ otherwise\\
   27.58 +\texttt{\footnotesize{02}} \> $X(j\omega)=\int_{-1}^{1}{1\cdot e^{-j\omega t}}$\\
   27.59 +      \` $\int_a^b f\;t\;dt = \int f\;t\;dt\;|_a^b$\\
   27.60 +\texttt{\footnotesize{03}} \> $\int 1\cdot e^{-j\cdot\omega\cdot t} d t\;|_{-1}^1$\\
   27.61 +       \` pbl: integration in $\cal C$\\
   27.62 +\texttt{\footnotesize{04}} \> $\left(\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot t} \;|_{-1}^1\right)$\\
   27.63 +      \` $f\;t\;|_a^b = f\;b-f\;a$\\
   27.64 +\texttt{\footnotesize{05}} \> $\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot 1} -  \frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot -1}$\\
   27.65 +\texttt{\footnotesize{06}} \> $\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega} -  \frac{1}{-j\cdot\omega}\cdot e^{j\cdot\omega}$\\
   27.66 +\` Lift $\frac{1}{j\omega}$\\
   27.67 +\texttt{\footnotesize{07}} \> $\frac{1}{j\cdot\omega}\cdot(e^{j\cdot\omega} - e^{-j\cdot\omega})$\\
   27.68 +      \` trick~!\\
   27.69 +\texttt{\footnotesize{08}} \> $\frac{1}{\omega}\cdot(\frac{-e^{j\cdot\omega} + e^{-j\cdot\omega}}{j})$\\
   27.70 +      \` table\\
   27.71 +\texttt{\footnotesize{09}} \> $2\cdot\frac{\sin\;\omega}{\omega}$
   27.72 +\end{tabbing}
   27.73 +}
   27.74 +
   27.75 +\noindent\textbf{(b)} \textsf{Subproblem 1}
   27.76 +\onehalfspace{
   27.77 +\begin{tabbing}
   27.78 +000\=\kill
   27.79 +\texttt{\footnotesize{01}} \> Definition: $X(j\omega)=\int_\infty^\infty{x(t)\cdot e^{-j\omega t}}$\\
   27.80 +\`Insert Condition: $x(t) = 1\;$ for $\;\{1\leq t\;\land\;t\leq 3\}\;$ and $\;x(t)=0\;$ otherwise\\
   27.81 +\texttt{\footnotesize{02}} \> $X(j\omega)=\int_{-1}^{1}{1\cdot e^{-j\omega t}}$\\
   27.82 +      \` $\int_a^b f\;t\;dt = \int f\;t\;dt\;|_a^b$\\
   27.83 +\texttt{\footnotesize{03}} \> $\int 1\cdot e^{-j\cdot\omega\cdot t} d t\;|_{1}^3$\\
   27.84 +       \` pbl: integration in $\cal C$\\
   27.85 +\texttt{\footnotesize{04}} \> $\left(\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot t} \;|_{1}^3\right)$\\
   27.86 +      \` $f\;t\;|_a^b = f\;b-f\;a$\\
   27.87 +\texttt{\footnotesize{05}} \> $\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot 3} -  \frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot 1}$\\
   27.88 +\`Lift $\frac{1}{-j\omega}$\\
   27.89 +\texttt{\footnotesize{06}} \> $\frac{1}{j\cdot\omega}\cdot(e^{-j\cdot\omega} - e^{-j\cdot\omega3})$\\
   27.90 +      \`Lift $e^{j\omega2}$ (trick)\\
   27.91 +\texttt{\footnotesize{07}} \> $\frac{1}{j\omega}\cdot e^{j\omega2}\cdot(e^{j\omega} - e^{-j\omega})$\\
   27.92 +\`Simplification (trick)\\
   27.93 +\texttt{\footnotesize{08}} \> $\frac{1}{\omega}\cdot e^{j\omega2}\cdot(\frac{e^{j\omega} - e^{-j\omega}}{j})$\\
   27.94 +      \` table\\
   27.95 +\texttt{\footnotesize{09}} \> $2\cdot e^{j\omega2}\cdot\frac{\sin\;\omega}{\omega}$\\
   27.96 +\noindent\textbf{(b)} \textsf{Subproblem 2}\\
   27.97 +\`Definition: $X(j\omega)=|X(j\omega)|\cdot e^{arg(X(j\omega))}$\\
   27.98 +\`$|X(j\omega)|$ is called \emph{Magnitude}\\
   27.99 +\`$arg(X(j\omega))$ is called \emph{Phase}\\
  27.100 +\texttt{\footnotesize{10}} \> $|X(j\omega)|=\frac{2}{\omega}\cdot sin(\omega)$\\
  27.101 +\texttt{\footnotesize{11}} \> $arg(X(j\omega)=-2\omega$\\
  27.102 +\end{tabbing}
  27.103 +}
  27.104 +%------------------------------------------------------------------------------
  27.105 +%CONVOLUTION
  27.106 +
  27.107 +\subsection{Convolution}
  27.108 +\subsubsection*{Problem\endnote{Problem submitted by Bernhard Geiger. Originally part of the SPSC Problem Class 2, Summer term 2008}}
  27.109 +Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response:
  27.110 +
  27.111 +\begin{center}
  27.112 +$h_1[n]=\left(\frac{3}{5}\right)^n\cdot u[n]$\\
  27.113 +$h_1[n]=\left(-\frac{2}{3}\right)^n\cdot u[n]$
  27.114 +\end{center}
  27.115 +
  27.116 +The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$.
  27.117 +\subsubsection*{Solution}
  27.118 +
  27.119 +\doublespace{
  27.120 +\begin{tabbing}
  27.121 +000\=\kill
  27.122 +\texttt{\footnotesize{01}} \> $h_c[n]=h_1[n]*h_2[n]$\\
  27.123 +\texttt{\footnotesize{02}} \> $h_c[n]=\left(\left(\frac{3}{5}\right)^n\cdot u[n]\right)*\left(\left(-\frac{2}{3}\right)^n\cdot u[n]\right)$\\
  27.124 +\`Definition: $a^n\cdot u[n]\,*\,b^n\cdot u[n]=\sum\limits_{k=-\infty}^{\infty}{a^k\cdot u[k]\cdot b^{n-k}\cdot u[n-k]}$\\
  27.125 +\texttt{\footnotesize{03}} \> $h_c[n]=\sum\limits_{k=-\infty}^{\infty}{\left(\frac{3}{5}\right)^k\cdot u[n]\,\cdot \,\left(-\frac{2}{3}\right)^{n-k}\cdot u[n-k]}$\\
  27.126 +\`$u[n]= \left\{
  27.127 +     \begin{array}{lr}
  27.128 +       1 & for\ n>=0\\
  27.129 +       0 & else
  27.130 +     \end{array}
  27.131 +   \right.$\\
  27.132 +\`We can leave the unitstep through simplification.\\
  27.133 +\`So the lower limit is 0, the upper limit is n.\\
  27.134 +\texttt{\footnotesize{04}} \> $h_c[n]=\sum\limits_{k=0}^{n}{\left(\frac{3}{5}\right)^k\cdot \left(-\frac{2}{3}\right)^{n-k}}$\\
  27.135 +\`Expand\\
  27.136 +\texttt{\footnotesize{05}} \> $h_c[n]=\sum\limits_{k=0}^{n}{\left(\frac{3}{5}\right)^k\cdot \left(-\frac{2}{3}\right)^{n}\cdot \left(-\frac{2}{3}\right)^{-k}}$\\
  27.137 +\`Lift\\
  27.138 +\texttt{\footnotesize{06}} \> $h_c[n]=\left(-\frac{2}{3}\right)^{n}\cdot\sum\limits_{k=0}^{\infty}{\left(\frac{3}{5}\right)^k\cdot \left(-\frac{2}{3}\right)^{-k}}$\\
  27.139 +\texttt{\footnotesize{07}} \> $h_c[n]=\left(-\frac{2}{3}\right)^{n}\cdot\sum\limits_{k=0}^{n}{\left(\frac{3}{5}\right)^k\cdot \left(-\frac{3}{2}\right)^{k}}$\\
  27.140 +\texttt{\footnotesize{08}} \> $h_c[n]=\left(-\frac{2}{3}\right)^{n}\cdot\sum\limits_{k=0}^{n}{\left(-\frac{9}{10}\right)^{k}}$\\
  27.141 +\`Geometric Series: $\sum\limits_{k=0}^{n}{q^k}=\frac{1-q^{n+1}}{1-q}$\\
  27.142 +\`Now we have to consider the limits again.\\
  27.143 +\`It is neccesarry to put the unitstep in again.\\
  27.144 +\texttt{\footnotesize{09}} \> $h_c[n]=\left(-\frac{2}{3}\right)^{n}\cdot\frac{1-\left(-\frac{9}{10}\right)^{n+1}}{1-\left(-\frac{9}{10}\right)}\cdot u[n]$\\
  27.145 +\texttt{\footnotesize{10}} \> $h_c[n]=\left(-\frac{2}{3}\right)^{n}\cdot\frac{1-\left(-\frac{9}{10}\right)^{n}\cdot\left(-\frac{9}{10}\right)}{1-\left(-\frac{9}{10}\right)}\cdot u[n]$\\
  27.146 +\texttt{\footnotesize{11}} \> $h_c[n]=\left(-\frac{2}{3}\right)^{n}\cdot\frac{1-\left(-\frac{9}{10}\right)^{n}\cdot\left(-\frac{9}{10}\right)}{\left(\frac{19}{10}\right)}\cdot u[n]$\\
  27.147 +\texttt{\footnotesize{12}} \> $h_c[n]=\left(-\frac{2}{3}\right)^{n}\cdot \left(1-\left(-\frac{9}{10}\right)^{n}\cdot\left(-\frac{9}{10}\right)\right)\cdot\left(\frac{10}{19}\right)\cdot u[n]$\\
  27.148 +\`Lift $u[n]$\\
  27.149 +\texttt{\footnotesize{13}} \> $\left(\frac{10}{19}\cdot\left(-\frac{2}{3}\right)^n+\frac{9}{19}\cdot\left(\frac{3}{5}\right)^n\right)\cdot u[n]$\\
  27.150 +\end{tabbing}
  27.151 +}
  27.152 +
  27.153 +%------------------------------------------------------------------------------
  27.154 +%Z-Transformation
  27.155 +
  27.156 +\subsection{Z-Transformation\label{sec:calc:ztrans}}
  27.157 +\subsubsection*{Problem\endnote{Problem submitted by Bernhard Geiger. Originally part of the signal processing problem class 5, summer term 2008.}}
  27.158 +Determine the inverse $\cal{z}$ transform of the following expression. Hint: applay the partial fraction expansion.
  27.159 +
  27.160 +\begin{center}
  27.161 +$X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable
  27.162 +\end{center}
  27.163 +
  27.164 +\subsubsection*{Solution}
  27.165 +\onehalfspace{
  27.166 +\begin{tabbing}
  27.167 +000\=\kill
  27.168 +\textsf{Main Problem}\\
  27.169 +\texttt{\footnotesize{01}} \> $\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}}$ \\
  27.170 +\`Divide through z, neccesary for z-transformation\\
  27.171 +\texttt{\footnotesize{02}} \> $\frac{3}{z^2-\frac{1}{4}z-\frac{1}{8}}$ \\
  27.172 +\`Start with partial fraction expansion\\
  27.173 +\texttt{\footnotesize{03}} \> $\frac{3}{z^2-\frac{1}{4}z-\frac{1}{8}}=\frac{A}{z-z_1}+\frac{B}{z-z_2}$ \\
  27.174 +\`Eliminate Fractions\\
  27.175 +\texttt{\footnotesize{04}} \> $3=A(z-z_2)+B(z-z_1)$ \\
  27.176 +\textsf{Subproblem 1}\\
  27.177 +\`Setup a linear equation system by inserting the zeros $z_1$ and $z_2$ for $z$\\
  27.178 +\texttt{\footnotesize{05}} \> $3=A(z_1-z_2)$ \& $3=B(z_2-z_1)$\\
  27.179 +\texttt{\footnotesize{06}} \> $\frac{3}{z_1-z_2}=A$ \& $\frac{3}{z_2-z_1}=B$\\
  27.180 +\textsf{Subproblem 2}\\
  27.181 +\`Determine $z_1$ and $z_2$\\
  27.182 +\texttt{\footnotesize{07}} \> $z_1=\frac{1}{8}+\sqrt{\frac{1}{64}+\frac{1}{8}}$ \& $z_2=\frac{1}{8}-\sqrt{\frac{1}{64}+\frac{1}{8}}$\\
  27.183 +\texttt{\footnotesize{08}} \> $z_1=\frac{1}{8}+\sqrt{\frac{9}{64}}$ \& $z_2=\frac{1}{8}-\sqrt{\frac{9}{64}}$\\
  27.184 +\texttt{\footnotesize{09}} \> $z_1=\frac{1}{8}+\frac{3}{8}$ \& $z_2=\frac{1}{8}-\frac{3}{8}$\\
  27.185 +\texttt{\footnotesize{10}} \> $z_1=\frac{1}{2}$ \& $z_2=-\frac{1}{4}$\\
  27.186 +\textsf{Continiue with Subproblem 1}\\
  27.187 +\`Get the coeffizients $A$ and $B$\\
  27.188 +\texttt{\footnotesize{11}} \> $\frac{3}{\frac{1}{2}-(-\frac{1}{4})}=A$ \& $\frac{3}{-\frac{1}{4}-\frac{1}{2}}=B$\\
  27.189 +\texttt{\footnotesize{12}} \> $\frac{3}{\frac{1}{2}+\frac{1}{4}}=A$ \& $\frac{3}{-\frac{1}{4}-\frac{1}{2}}=B$\\
  27.190 +\texttt{\footnotesize{13}} \> $\frac{3}{\frac{3}{4}}=A$ \& $\frac{3}{-\frac{3}{4}}=B$\\
  27.191 +\texttt{\footnotesize{14}} \> $\frac{12}{3}=A$ \& $-\frac{12}{3}=B$\\
  27.192 +\texttt{\footnotesize{15}} \> $4=A$ \& $-4=B$\\
  27.193 +\textsf{Continiue with Main Problem}\\
  27.194 +\texttt{\footnotesize{16}} \> $\frac{A}{z-z_1}+\frac{B}{z-z_2}$\\
  27.195 +\texttt{\footnotesize{17}} \> $\frac{4}{z-\frac{1}{2}}+\frac{4}{z-\left(-\frac{1}{4}\right)}$ \\
  27.196 +\texttt{\footnotesize{18}} \> $\frac{4}{z-\frac{1}{2}}-\frac{4}{z+\frac{1}{4}}$ \\
  27.197 +\`Multiply with z, neccesary for z-transformation\\
  27.198 +\texttt{\footnotesize{19}} \> $\frac{4z}{z-\frac{1}{2}}-\frac{4z}{z+\frac{1}{4}}$ \\
  27.199 +\texttt{\footnotesize{20}} \> $4\cdot\frac{z}{z-\frac{1}{2}}+(-4)\cdot\frac{z}{z+\frac{1}{4}}$ \\
  27.200 +\`Transformation\\
  27.201 +\texttt{\footnotesize{21}} \> $4\cdot\frac{z}{z-\frac{1}{2}}+(-4)\cdot\frac{z}{z+\frac{1}{4}}\ \Ztransf\ 4\cdot\left(-\frac{1}{2}\right)^n\cdot u[n]+(-4)\cdot\left(\frac{1}{4}\right)^n\cdot u[n]$\\
  27.202 +\end{tabbing}
  27.203 +}
  27.204 +\theendnotes
  27.205 +%\end{document}
  27.206 \ No newline at end of file