| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Fri, 01 Mar 2013 17:13:32 +0000 | |
| changeset 375 | 44c4450152e3 |
| parent 374 | 01d223421ba0 |
| child 376 | 209fd285c86f |
--- a/Journal/Paper.thy Wed Dec 12 11:45:04 2012 +0000 +++ b/Journal/Paper.thy Fri Mar 01 17:13:32 2013 +0000 @@ -611,7 +611,7 @@ strings are related, provided there is no distinguishing extension in this language. This can be defined as a ternary relation. - \begin{dfntn}[(Myhill-Nerode Relation)]\label{myhillneroderel} + \begin{dfntn}[Myhill-Nerode Relation]\label{myhillneroderel} Given a language @{text A}, two strings @{text x} and @{text y} are Myhill-Nerode related provided \begin{center} @@ -1190,7 +1190,7 @@ the base cases are straightforward. - \begin{proof}[(Base Cases)] + \begin{proof}[Base Cases] The cases for @{const ZERO}, @{const ONE} and @{const ATOM} are routine, because we can easily establish that @@ -1275,7 +1275,7 @@ as follows. - \begin{dfntn}[(Tagging-Relation)] Given a tagging-function @{text tag}, then two strings @{text x} + \begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x} and @{text y} are \emph{tag-related} provided \begin{center} @{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y \<equiv> tag x = tag y"}\;. @@ -1353,7 +1353,7 @@ @{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. As we shall see, this definition will provide us with just the right assumptions in order to get the proof through. - \begin{proof}[(@{const "PLUS"}-Case)] + \begin{proof}[@{const "PLUS"}-Case] We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"} then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of @{term "tag_Plus A B"} is a subset of this product @@ -1477,7 +1477,7 @@ With this definition in place, let us prove the @{const "Times"}-case. - \begin{proof}[(@{const TIMES}-Case)] + \begin{proof}[@{const TIMES}-Case] If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"} then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of @{term "tag_Times A B"} is a subset of this product set, and therefore finite. @@ -1602,7 +1602,7 @@ @{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"} \end{center} - \begin{proof}[(@{const Star}-Case)] + \begin{proof}[@{const Star}-Case] If @{term "finite (UNIV // \<approx>A)"} then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of @{term "tag_Star A"} is a subset of this set, and therefore finite. @@ -2275,7 +2275,7 @@ the non-regularity of languages. For this we use the following version of the Continuation Lemma (see for example~\cite{Rosenberg06}). - \begin{lmm}[(Continuation Lemma)] + \begin{lmm}[Continuation Lemma] If a language @{text A} is regular and a set of strings @{text B} is infinite, then there exist two distinct strings @{text x} and @{text y} in @{text B} such that @{term "x \<approx>A y"}. @@ -2300,7 +2300,7 @@ \begin{proof} After unfolding the definition of @{text "B"}, we need to establish that given @{term "i \<noteq> j"}, the strings @{text "a\<^sup>i"} and @{text "a\<^sup>j"} are not Myhill-Nerode related by @{text "A"}. - That means we have to show that \mbox{@{text "\<forall>z. a\<^sup>i @ z \<in> A = a\<^sup>j @ z \<in> A"}} leads to + That means we have to show that @{text "\<forall>z. a\<^sup>i @ z \<in> A = a\<^sup>j @ z \<in> A"} leads to a contradiction. Let us take @{text "b\<^sup>i"} for @{text "z"}. Then we know @{text "a\<^sup>i @ b\<^sup>i \<in> A"}. But since @{term "i \<noteq> j"}, @{text "a\<^sup>j @ b\<^sup>i \<notin> A"}. Therefore @{text "a\<^sup>i"} and @{text "a\<^sup>j"} cannot be Myhill-Nerode related by @{text "A"}, and we are done. @@ -2323,10 +2323,28 @@ exists a regular expression that matches all of its strings. Regular expressions can conveniently be defined as a datatype in theorem provers. For us it was therefore interesting to find out how far we can push - this point of view. We have established in Isabelle/HOL both directions + this point of view. But this question whether formal language theory can + be done without automata crops up also in non-theorem prover contexts. For + example, Gasarch asked in the Computational Complexity blog by \citeN{GasarchBlog} + whether the complementation of + regular-expression languages can be proved without using automata. He concluded + + \begin{quote} + {\it \ldots it can't be done} + \end{quote} + + \noindent + and even pondered + + \begin{quote} + {\it \ldots [b]ut is there a rigorous way to even state that?} + \end{quote} + + \noindent + We have established in Isabelle/HOL both directions of the Myhill-Nerode Theorem. % - \begin{thrm}[(Myhill-Nerode Theorem)]\mbox{}\\ + \begin{thrm}[Myhill-Nerode Theorem]\mbox{}\\ A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}. \end{thrm} @@ -2336,11 +2354,9 @@ regular---by establishing that it has infinitely many equivalence classes generated by the Myhill-Nerode Relation (this is usually the purpose of the Pumping Lemma). We can also use it to establish the standard - textbook results about closure properties of regular languages. Interesting - is the case of closure under complement, because it seems difficult to - construct a regular expression for the complement language by direct - means. However the existence of such a regular expression can be easily - proved using the Myhill-Nerode Theorem. + textbook results about closure properties of regular languages. The case of + closure under complement follows easily from the Myhill-Nerode Theorem. + So our answer to Gasarch is ``{\it it can be done!''} %Our insistence on regular expressions for proving the Myhill-Nerode Theorem %arose from the problem of defining formally the regularity of a language. @@ -2377,6 +2393,10 @@ %language theory---the Myhill-Nerode Theorem. While regular expressions are convenient, they have some limitations. One is + that there are some regular expressions for which the smallest regular + expression for the complement language has a doubly-exponential blowup in size + as shown by \citeN{Gelade12}. + Another is that there seems to be no method of calculating a minimal regular expression (for example in terms of length) for a regular language, like there is for automata. On the other hand, efficient regular expression matching, without
--- a/Journal/document/root.bib Wed Dec 12 11:45:04 2012 +0000 +++ b/Journal/document/root.bib Fri Mar 01 17:13:32 2013 +0000 @@ -1,3 +1,25 @@ + + +@Unpublished{GasarchBlog, + author = {L.~Fortnow and W.~I.~Gasarch}, + title = {{P}roving {DFA}-{L}angs {C}losed {U}nder {C}oncat and * {W}ithout {U}sing {E}quiv to + {NDFA's}}, + note = {Retrieved \today, from \url{http://blog.computationalcomplexity.org}}, + year = {2013} +} + +@article{Gelade12, + author = {W.~Gelade and F.~Neven}, + title = {{S}uccinctness of the {C}omplement and {I}ntersection of {R}egular + {E}xpressions}, + journal = {ACM Transactions on Computational Logic}, + volume = {13}, + number = {1}, + year = {2012}, + pages = {4:1--4:21}, +} + + @InProceedings{CoquandSiles12, author = {T.~Coquand and V.~Siles}, title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},
--- a/Journal/document/root.tex Wed Dec 12 11:45:04 2012 +0000 +++ b/Journal/document/root.tex Fri Mar 01 17:13:32 2013 +0000 @@ -1,4 +1,5 @@ -\documentclass[acmtocl,final]{acmtrans2m} +\documentclass[final, natbib]{svjour3} +%\documentclass[acmtocl,final]{acmtrans2m} \usepackage{isabelle} \usepackage{isabellesym} \usepackage{amsmath} @@ -9,12 +10,17 @@ \usetikzlibrary{shapes,shapes.arrows,snakes,positioning} \usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf \usetikzlibrary{matrix} -%%%\usepackage{pdfsetup} +\usepackage{pdfsetup} \usepackage{ot1patch} \usepackage{times} \usepackage{stmaryrd} \usepackage{mathpartir} \usepackage{longtable} +%%\usepackage{chicago} + +\def\citeN{\citet} + +%%\journalname{Journal of Automated Reasoning} \urlstyle{rm} \isabellestyle{it} @@ -40,16 +46,24 @@ \newtheorem{dfntn}{Definition}[section] \newtheorem{prpstn}{Proposition}[section] +\begin{document} \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular - Expressions$^\star$} -%%\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.} -\author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and -Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and -Christian Urban\\ King's College London, United Kingdom} + Expressions$^\star$\thanks{$^\star$ This is a revised and much expanded version of \cite{WuZhangUrban11}.}} +%\author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and +%Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and +%Christian Urban\\ King's College London, United Kingdom} -\markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular - Expressions} +\author{Chunhan Wu \and Xingyuan Zhang \and Christian Urban} +\institute{Chunhan Wu \and Xingyuan Zhang \at PLA University of Science and Technology Nanjing, China \and +Christian Urban \at King's College London, United Kingdom} + +\date{Received: date / Accepted: date} + +%\markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular +% Expressions} +\maketitle + \begin{abstract} There are numerous textbooks on regular languages. Many of them focus @@ -64,17 +78,18 @@ only regular expressions. From this theorem many closure properties of regular languages follow. \end{abstract} -\category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving} -\category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages} -\terms{Interactive theorem proving, regular languages} -\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover} -\begin{document} -\begin{bottomstuff} -Corresponding Author: Christian Urban, Department of Informatics, King's College London, -Strand, London WC2R 2LS, UK. Email: christian.urban@kcl.ac.uk.\\ -$^\star$This is a revised and expanded version of \cite{WuZhangUrban11}. -\end{bottomstuff} -\maketitle +%\category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving} +%\category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages} +%\terms{Interactive theorem proving, regular languages} +%\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover} +%\begin{document} + +%\begin{bottomstuff} +%Corresponding Author: Christian Urban, Department of Informatics, King's College London, +%Strand, London WC2R 2LS, UK. Email: christian.urban@kcl.ac.uk.\\ +%$^\star$This is a revised and expanded version of \cite{WuZhangUrban11}. +%\end{bottomstuff} +%%\maketitle \input{session}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Journal/document/svglov3.clo Fri Mar 01 17:13:32 2013 +0000 @@ -0,0 +1,113 @@ +% SVJour3 DOCUMENT CLASS OPTION SVGLOV3 -- for standardised journals +% +% This is an enhancement for the LaTeX +% SVJour3 document class for Springer journals +% +%% +%% +%% \CharacterTable +%% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z +%% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z +%% Digits \0\1\2\3\4\5\6\7\8\9 +%% Exclamation \! Double quote \" Hash (number) \# +%% Dollar \$ Percent \% Ampersand \& +%% Acute accent \' Left paren \( Right paren \) +%% Asterisk \* Plus \+ Comma \, +%% Minus \- Point \. Solidus \/ +%% Colon \: Semicolon \; Less than \< +%% Equals \= Greater than \> Question mark \? +%% Commercial at \@ Left bracket \[ Backslash \\ +%% Right bracket \] Circumflex \^ Underscore \_ +%% Grave accent \` Left brace \{ Vertical bar \| +%% Right brace \} Tilde \~} +\ProvidesFile{svglov3.clo} + [2009/12/18 v3.2 + style option for standardised journals] +\typeout{SVJour Class option: svglov3.clo for standardised journals} +\def\validfor{svjour3} +\global\let\if@runhead\iftrue +\ExecuteOptions{final,10pt} +% No size changing allowed, hence a "copy" of size10.clo is included +\DeclareFontShape{OT1}{cmr}{m}{n}{ + <-6> cmr5 + <6-7> cmr6 + <7-8> cmr7 + <8-9> cmr8 + <9-10> cmr9 + <10-12> cmr10 + <12-17> cmr12 + <17-> cmr17 + }{} +% +\renewcommand\normalsize{% +\if@twocolumn + \@setfontsize\normalsize\@xpt{12.5pt}% +\else + \if@smallext + \@setfontsize\normalsize\@xpt\@xiipt + \else + \@setfontsize\normalsize{9.5pt}{11.5pt}% + \fi +\fi + \abovedisplayskip=3 mm plus6pt minus 4pt + \belowdisplayskip=3 mm plus6pt minus 4pt + \abovedisplayshortskip=0.0 mm plus6pt + \belowdisplayshortskip=2 mm plus4pt minus 4pt + \let\@listi\@listI} +\normalsize +\newcommand\small{% +\if@twocolumn + \@setfontsize\small{8.5pt}\@xpt +\else + \if@smallext + \@setfontsize\small\@viiipt{9.5pt}% + \else + \@setfontsize\small\@viiipt{9.25pt}% + \fi +\fi + \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@ + \abovedisplayshortskip \z@ \@plus2\p@ + \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@ + \def\@listi{\leftmargin\leftmargini + \parsep 0\p@ \@plus1\p@ \@minus\p@ + \topsep 4\p@ \@plus2\p@ \@minus4\p@ + \itemsep0\p@}% + \belowdisplayskip \abovedisplayskip +} +\let\footnotesize\small +\newcommand\scriptsize{\@setfontsize\scriptsize\@viipt\@viiipt} +\newcommand\tiny{\@setfontsize\tiny\@vpt\@vipt} +\if@twocolumn + \newcommand\large{\@setfontsize\large\@xiipt\@xivpt} + \newcommand\LARGE{\@setfontsize\LARGE{16pt}{18pt}} +\else + \newcommand\large{\@setfontsize\large\@xipt\@xiipt} + \newcommand\LARGE{\@setfontsize\LARGE{13pt}{15pt}} +\fi +\newcommand\Large{\@setfontsize\Large\@xivpt{16dd}} +\newcommand\huge{\@setfontsize\huge\@xxpt{25}} +\newcommand\Huge{\@setfontsize\Huge\@xxvpt{30}} +% +\def\runheadhook{\rlap{\smash{\lower6.5pt\hbox to\textwidth{\hrulefill}}}} +\if@twocolumn +\setlength{\textwidth}{17.4cm} +\setlength{\textheight}{234mm} +\AtEndOfClass{\setlength\columnsep{6mm}} +\else + \if@smallext + \setlength{\textwidth}{11.9cm} + \setlength{\textheight}{19.4cm} + \else + \setlength{\textwidth}{12.2cm} + \setlength{\textheight}{19.8cm} + \fi +\fi +% +\AtBeginDocument{% +\@ifundefined{@journalname} + {\typeout{Unknown journal: specify \string\journalname\string{% +<name of your journal>\string} in preambel^^J}}{}} +% +\endinput +%% +%% End of file `svglov3.clo'.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Journal/document/svjour3.cls Fri Mar 01 17:13:32 2013 +0000 @@ -0,0 +1,1431 @@ +% SVJour3 DOCUMENT CLASS -- version 3.2 for LaTeX2e +% +% LaTeX document class for Springer journals +% +%% +%% +%% \CharacterTable +%% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z +%% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z +%% Digits \0\1\2\3\4\5\6\7\8\9 +%% Exclamation \! Double quote \" Hash (number) \# +%% Dollar \$ Percent \% Ampersand \& +%% Acute accent \' Left paren \( Right paren \) +%% Asterisk \* Plus \+ Comma \, +%% Minus \- Point \. Solidus \/ +%% Colon \: Semicolon \; Less than \< +%% Equals \= Greater than \> Question mark \? +%% Commercial at \@ Left bracket \[ Backslash \\ +%% Right bracket \] Circumflex \^ Underscore \_ +%% Grave accent \` Left brace \{ Vertical bar \| +%% Right brace \} Tilde \~} +\NeedsTeXFormat{LaTeX2e}[1995/12/01] +\ProvidesClass{svjour3}[2007/05/08 v3.2 +^^JLaTeX document class for Springer journals] +\newcommand\@ptsize{} +\newif\if@restonecol +\newif\if@titlepage +\@titlepagefalse +\DeclareOption{a4paper} + {\setlength\paperheight {297mm}% + \setlength\paperwidth {210mm}} +\DeclareOption{10pt}{\renewcommand\@ptsize{0}} +\DeclareOption{twoside}{\@twosidetrue \@mparswitchtrue} +\DeclareOption{draft}{\setlength\overfullrule{5pt}} +\DeclareOption{final}{\setlength\overfullrule{0pt}} +\DeclareOption{fleqn}{\input{fleqn.clo}\AtBeginDocument{\mathindent\z@}% +\AtBeginDocument{\@ifpackageloaded{amsmath}{\@mathmargin\z@}{}}% +\PassOptionsToPackage{fleqn}{amsmath}} +%%% +\DeclareOption{onecolumn}{} +\DeclareOption{smallcondensed}{} +\DeclareOption{twocolumn}{\@twocolumntrue\ExecuteOptions{fleqn}} +\newif\if@smallext\@smallextfalse +\DeclareOption{smallextended}{\@smallexttrue} +\let\if@mathematic\iftrue +\let\if@numbook\iffalse +\DeclareOption{numbook}{\let\if@envcntsect\iftrue + \AtEndOfPackage{% + \renewcommand\thefigure{\thesection.\@arabic\c@figure}% + \renewcommand\thetable{\thesection.\@arabic\c@table}% + \renewcommand\theequation{\thesection.\@arabic\c@equation}% + \@addtoreset{figure}{section}% + \@addtoreset{table}{section}% + \@addtoreset{equation}{section}% + }% +} +\DeclareOption{openbib}{% + \AtEndOfPackage{% + \renewcommand\@openbib@code{% + \advance\leftmargin\bibindent + \itemindent -\bibindent + \listparindent \itemindent + \parsep \z@ + }% + \renewcommand\newblock{\par}}% +} +\DeclareOption{natbib}{% +\AtEndOfClass{\RequirePackage{natbib}% +% Changing some parameters of NATBIB +\setlength{\bibhang}{\parindent}% +%\setlength{\bibsep}{0mm}% +\let\bibfont=\small +\def\@biblabel#1{#1.}% +\newcommand{\etal}{et al.}% +\bibpunct{(}{)}{;}{a}{}{,}}} +% +\let\if@runhead\iffalse +\DeclareOption{runningheads}{\let\if@runhead\iftrue} +\let\if@smartrunh\iffalse +\DeclareOption{smartrunhead}{\let\if@smartrunh\iftrue} +\DeclareOption{nosmartrunhead}{\let\if@smartrunh\iffalse} +\let\if@envcntreset\iffalse +\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue} +\let\if@envcntsame\iffalse +\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue} +\let\if@envcntsect\iffalse +\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue} +\let\if@referee\iffalse +\DeclareOption{referee}{\let\if@referee\iftrue} +\def\makereferee{\def\baselinestretch{2}} +\let\if@instindent\iffalse +\DeclareOption{instindent}{\let\if@instindent\iftrue} +\let\if@smartand\iffalse +\DeclareOption{smartand}{\let\if@smartand\iftrue} +\let\if@spthms\iftrue +\DeclareOption{nospthms}{\let\if@spthms\iffalse} +% +% language and babel dependencies +\DeclareOption{deutsch}{\def\switcht@@therlang{\switcht@deutsch}% +\gdef\svlanginfo{\typeout{Man spricht deutsch.}\global\let\svlanginfo\relax}} +\DeclareOption{francais}{\def\switcht@@therlang{\switcht@francais}% +\gdef\svlanginfo{\typeout{On parle francais.}\global\let\svlanginfo\relax}} +\let\switcht@@therlang\relax +\let\svlanginfo\relax +% +\AtBeginDocument{\@ifpackageloaded{babel}{% +\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}% +\@ifundefined{extrasUKenglish}{}{\addto\extrasUKenglish{\switcht@albion}}% +\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}% +\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}% +\@ifundefined{extrasngerman}{}{\addto\extrasngerman{\switcht@deutsch}}% +}{\switcht@@therlang}% +} +% +\def\ClassInfoNoLine#1#2{% + \ClassInfo{#1}{#2\@gobble}% +} +\let\journalopt\@empty +\DeclareOption*{% +\InputIfFileExists{sv\CurrentOption.clo}{% +\global\let\journalopt\CurrentOption}{% +\ClassWarning{Springer-SVJour3}{Specified option or subpackage +"\CurrentOption" not found -}\OptionNotUsed}} +\ExecuteOptions{a4paper,twoside,10pt,instindent} +\ProcessOptions +% +\ifx\journalopt\@empty\relax +\ClassInfoNoLine{Springer-SVJour3}{extra/valid Springer sub-package (-> *.clo) +\MessageBreak not found in option list of \string\documentclass +\MessageBreak - autoactivating "global" style}{} +\input{svglov3.clo} +\else +\@ifundefined{validfor}{% +\ClassError{Springer-SVJour3}{Possible option clash for sub-package +\MessageBreak "sv\journalopt.clo" - option file not valid +\MessageBreak for this class}{Perhaps you used an option of the old +Springer class SVJour!} +}{} +\fi +% +\if@smartrunh\AtEndDocument{\islastpageeven\getlastpagenumber}\fi +% +\newcommand{\twocoltest}[2]{\if@twocolumn\def\@gtempa{#2}\else\def\@gtempa{#1}\fi +\@gtempa\makeatother} +\newcommand{\columncase}{\makeatletter\twocoltest} +% +\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00} +\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01} +\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02} +\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03} +\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04} +\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05} +\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06} +\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07} +\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08} +\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09} +\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A} +% +\setlength\parindent{15\p@} +\setlength\smallskipamount{3\p@ \@plus 1\p@ \@minus 1\p@} +\setlength\medskipamount{6\p@ \@plus 2\p@ \@minus 2\p@} +\setlength\bigskipamount{12\p@ \@plus 4\p@ \@minus 4\p@} +\setlength\headheight{12\p@} +\setlength\headsep {14.50dd} +\setlength\topskip {10\p@} +\setlength\footskip{30\p@} +\setlength\maxdepth{.5\topskip} +% +\@settopoint\textwidth +\setlength\marginparsep {10\p@} +\setlength\marginparpush{5\p@} +\setlength\topmargin{-10pt} +\if@twocolumn + \setlength\oddsidemargin {-30\p@} + \setlength\evensidemargin{-30\p@} +\else + \setlength\oddsidemargin {\z@} + \setlength\evensidemargin{\z@} +\fi +\setlength\marginparwidth {48\p@} +\setlength\footnotesep{8\p@} +\setlength{\skip\footins}{9\p@ \@plus 4\p@ \@minus 2\p@} +\setlength\floatsep {12\p@ \@plus 2\p@ \@minus 2\p@} +\setlength\textfloatsep{20\p@ \@plus 2\p@ \@minus 4\p@} +\setlength\intextsep {20\p@ \@plus 2\p@ \@minus 2\p@} +\setlength\dblfloatsep {12\p@ \@plus 2\p@ \@minus 2\p@} +\setlength\dbltextfloatsep{20\p@ \@plus 2\p@ \@minus 4\p@} +\setlength\@fptop{0\p@} +\setlength\@fpsep{12\p@ \@plus 2\p@ \@minus 2\p@} +\setlength\@fpbot{0\p@ \@plus 1fil} +\setlength\@dblfptop{0\p@} +\setlength\@dblfpsep{12\p@ \@plus 2\p@ \@minus 2\p@} +\setlength\@dblfpbot{0\p@ \@plus 1fil} +\setlength\partopsep{2\p@ \@plus 1\p@ \@minus 1\p@} +\def\@listi{\leftmargin\leftmargini + \parsep \z@ + \topsep 6\p@ \@plus2\p@ \@minus4\p@ + \itemsep\parsep} +\let\@listI\@listi +\@listi +\def\@listii {\leftmargin\leftmarginii + \labelwidth\leftmarginii + \advance\labelwidth-\labelsep + \topsep \z@ + \parsep \topsep + \itemsep \parsep} +\def\@listiii{\leftmargin\leftmarginiii + \labelwidth\leftmarginiii + \advance\labelwidth-\labelsep + \topsep \z@ + \parsep \topsep + \itemsep \parsep} +\def\@listiv {\leftmargin\leftmarginiv + \labelwidth\leftmarginiv + \advance\labelwidth-\labelsep} +\def\@listv {\leftmargin\leftmarginv + \labelwidth\leftmarginv + \advance\labelwidth-\labelsep} +\def\@listvi {\leftmargin\leftmarginvi + \labelwidth\leftmarginvi + \advance\labelwidth-\labelsep} +% +\setlength\lineskip{1\p@} +\setlength\normallineskip{1\p@} +\renewcommand\baselinestretch{} +\setlength\parskip{0\p@ \@plus \p@} +\@lowpenalty 51 +\@medpenalty 151 +\@highpenalty 301 +\setcounter{topnumber}{4} +\renewcommand\topfraction{.9} +\setcounter{bottomnumber}{2} +\renewcommand\bottomfraction{.7} +\setcounter{totalnumber}{6} +\renewcommand\textfraction{.1} +\renewcommand\floatpagefraction{.85} +\setcounter{dbltopnumber}{3} +\renewcommand\dbltopfraction{.85} +\renewcommand\dblfloatpagefraction{.85} +\def\ps@headings{% + \let\@oddfoot\@empty\let\@evenfoot\@empty + \def\@evenhead{\small\csname runheadhook\endcsname + \rlap{\thepage}\hfil\leftmark\unskip}% + \def\@oddhead{\small\csname runheadhook\endcsname + \ignorespaces\rightmark\hfil\llap{\thepage}}% + \let\@mkboth\@gobbletwo + \let\sectionmark\@gobble + \let\subsectionmark\@gobble + } +% make indentations changeable +\def\setitemindent#1{\settowidth{\labelwidth}{#1}% + \leftmargini\labelwidth + \advance\leftmargini\labelsep + \def\@listi{\leftmargin\leftmargini + \labelwidth\leftmargini\advance\labelwidth by -\labelsep + \parsep=\parskip + \topsep=\medskipamount + \itemsep=\parskip \advance\itemsep by -\parsep}} +\def\setitemitemindent#1{\settowidth{\labelwidth}{#1}% + \leftmarginii\labelwidth + \advance\leftmarginii\labelsep +\def\@listii{\leftmargin\leftmarginii + \labelwidth\leftmarginii\advance\labelwidth by -\labelsep + \parsep=\parskip + \topsep=\z@ + \itemsep=\parskip \advance\itemsep by -\parsep}} +% labels of description +\def\descriptionlabel#1{\hspace\labelsep #1\hfil} +% adjusted environment "description" +% if an optional parameter (at the first two levels of lists) +% is present, its width is considered to be the widest mark +% throughout the current list. +\def\description{\@ifnextchar[{\@describe}{\list{}{\labelwidth\z@ + \itemindent-\leftmargin \let\makelabel\descriptionlabel}}} +\let\enddescription\endlist +% +\def\describelabel#1{#1\hfil} +\def\@describe[#1]{\relax\ifnum\@listdepth=0 +\setitemindent{#1}\else\ifnum\@listdepth=1 +\setitemitemindent{#1}\fi\fi +\list{--}{\let\makelabel\describelabel}} +% +\newdimen\logodepth +\logodepth=1.2cm +\newdimen\headerboxheight +\headerboxheight=163pt % 18 10.5dd-lines - 2\baselineskip +\if@twocolumn\else\advance\headerboxheight by-14.5mm\fi +\newdimen\betweenumberspace % dimension for space between +\betweenumberspace=3.33pt % number and text of titles. +\newdimen\aftertext % dimension for space after +\aftertext=5pt % text of title. +\newdimen\headlineindent % dimension for space between +\headlineindent=1.166cm % number and text of headings. +\if@mathematic + \def\runinend{} % \enspace} + \def\floatcounterend{\enspace} + \def\sectcounterend{} +\else + \def\runinend{.} + \def\floatcounterend{.\ } + \def\sectcounterend{.} +\fi +\def\email#1{\emailname: #1} +\def\keywords#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm +\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$ +}\noindent\keywordname\enspace\ignorespaces#1\par}} +% +\def\subclassname{{\bfseries Mathematics Subject Classification +(2000)}\enspace} +\def\subclass#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm +\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$ +}\noindent\subclassname\ignorespaces#1\par}} +% +\def\PACSname{\textbf{PACS}\enspace} +\def\PACS#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm +\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$ +}\noindent\PACSname\ignorespaces#1\par}} +% +\def\CRclassname{{\bfseries CR Subject Classification}\enspace} +\def\CRclass#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm +\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$ +}\noindent\CRclassname\ignorespaces#1\par}} +% +\def\ESMname{\textbf{Electronic Supplementary Material}\enspace} +\def\ESM#1{\par\addvspace\medskipamount +\noindent\ESMname\ignorespaces#1\par} +% +\newcounter{inst} +\newcounter{auth} +\def\authdepth{2} +\newdimen\instindent +\newbox\authrun +\newtoks\authorrunning +\newbox\titrun +\newtoks\titlerunning +\def\authorfont{\bfseries} + +\def\combirunning#1{\gdef\@combi{#1}} +\def\@combi{} +\newbox\combirun +% +\def\ps@last{\def\@evenhead{\small\rlap{\thepage}\hfil +\lastevenhead}} +\newcounter{lastpage} +\def\islastpageeven{\@ifundefined{lastpagenumber} +{\setcounter{lastpage}{0}}{\setcounter{lastpage}{\lastpagenumber}} +\ifnum\value{lastpage}>0 + \ifodd\value{lastpage}% + \else + \if@smartrunh + \thispagestyle{last}% + \fi + \fi +\fi} +\def\getlastpagenumber{\clearpage +\addtocounter{page}{-1}% + \immediate\write\@auxout{\string\gdef\string\lastpagenumber{\thepage}}% + \immediate\write\@auxout{\string\newlabel{LastPage}{{}{\thepage}}}% + \addtocounter{page}{1}} + +\def\journalname#1{\gdef\@journalname{#1}} + +\def\dedication#1{\gdef\@dedic{#1}} +\def\@dedic{} + +\let\@date\undefined +\def\notused{~} + +\def\institute#1{\gdef\@institute{#1}} + +\def\offprints#1{\begingroup +\def\protect{\noexpand\protect\noexpand}\xdef\@thanks{\@thanks +\protect\footnotetext[0]{\unskip\hskip-15pt{\itshape Send offprint requests +to\/}: \ignorespaces#1}}\endgroup\ignorespaces} + +%\def\mail#1{\gdef\@mail{#1}} +%\def\@mail{} + +\def\@thanks{} + +\def\@fnsymbol#1{\ifcase#1\or\star\or{\star\star}\or{\star\star\star}% + \or \dagger\or \ddagger\or + \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger + \or \ddagger\ddagger \else\@ctrerr\fi\relax} +% +%\def\invthanks#1{\footnotetext[0]{\kern-\bibindent#1}} +% +\def\nothanksmarks{\def\thanks##1{\protected@xdef\@thanks{\@thanks + \protect\footnotetext[0]{\kern-\bibindent##1}}}} +% +\def\subtitle#1{\gdef\@subtitle{#1}} +\def\@subtitle{} + +\def\headnote#1{\gdef\@headnote{#1}} +\def\@headnote{} + +\def\papertype#1{\gdef\paper@type{\MakeUppercase{#1}}} +\def\paper@type{} + +\def\ch@ckobl#1#2{\@ifundefined{@#1} + {\typeout{SVJour3 warning: Missing +\expandafter\string\csname#1\endcsname}% + \csname #1\endcsname{#2}} + {}} +% +\def\ProcessRunnHead{% + \def\\{\unskip\ \ignorespaces}% + \def\thanks##1{\unskip{}}% + \instindent=\textwidth + \advance\instindent by-\headlineindent + \if!\the\titlerunning!\else + \edef\@title{\the\titlerunning}% + \fi + \global\setbox\titrun=\hbox{\small\rmfamily\unboldmath\ignorespaces\@title + \unskip}% + \ifdim\wd\titrun>\instindent + \typeout{^^JSVJour3 Warning: Title too long for running head.}% + \typeout{Please supply a shorter form with \string\titlerunning + \space prior to \string\maketitle}% + \global\setbox\titrun=\hbox{\small\rmfamily + Title Suppressed Due to Excessive Length}% + \fi + \xdef\@title{\copy\titrun}% +% + \if!\the\authorrunning! + \else + \setcounter{auth}{1}% + \edef\@author{\the\authorrunning}% + \fi + \ifnum\value{inst}>\authdepth + \def\stripauthor##1\and##2\endauthor{% + \protected@xdef\@author{##1\unskip\unskip\if!##2!\else\ et al.\fi}}% + \expandafter\stripauthor\@author\and\endauthor + \else + \gdef\and{\unskip, \ignorespaces}% + {\def\and{\noexpand\protect\noexpand\and}% + \protected@xdef\@author{\@author}} + \fi + \global\setbox\authrun=\hbox{\small\rmfamily\unboldmath\ignorespaces + \@author\unskip}% + \ifdim\wd\authrun>\instindent + \typeout{^^JSVJour3 Warning: Author name(s) too long for running head. + ^^JPlease supply a shorter form with \string\authorrunning + \space prior to \string\maketitle}% + \global\setbox\authrun=\hbox{\small\rmfamily Please give a shorter version + with: {\tt\string\authorrunning\space and + \string\titlerunning\space prior to \string\maketitle}}% + \fi + \xdef\@author{\copy\authrun}% + \markboth{\@author}{\@title}% +} +% +\let\orithanks=\thanks +\def\thanks#1{\ClassWarning{SVJour3}{\string\thanks\space may only be +used inside of \string\title, \string\author,\MessageBreak +and \string\date\space prior to \string\maketitle}} +% +\def\maketitle{\par\let\thanks=\orithanks +\ch@ckobl{journalname}{Noname} +\ch@ckobl{date}{the date of receipt and acceptance should be inserted +later} +\ch@ckobl{title}{A title should be given} +\ch@ckobl{author}{Name(s) and initial(s) of author(s) should be given} +\ch@ckobl{institute}{Address(es) of author(s) should be given} +\begingroup +% + \renewcommand\thefootnote{\@fnsymbol\c@footnote}% + \def\@makefnmark{$^{\@thefnmark}$}% + \renewcommand\@makefntext[1]{% + \noindent + \hb@xt@\bibindent{\hss\@makefnmark\enspace}##1\vrule height0pt + width0pt depth8pt} +% + \def\lastand{\ifnum\value{inst}=2\relax + \unskip{} \andname\ + \else + \unskip, \andname\ + \fi}% + \def\and{\stepcounter{auth}\relax + \if@smartand + \ifnum\value{auth}=\value{inst}% + \lastand + \else + \unskip, + \fi + \else + \unskip, + \fi}% + \thispagestyle{empty} + \ifnum \col@number=\@ne + \@maketitle + \else + \twocolumn[\@maketitle]% + \fi +% + \global\@topnum\z@ + \if!\@thanks!\else + \@thanks +\insert\footins{\vskip-3pt\hrule\@width\if@twocolumn\columnwidth +\else 38mm\fi\vskip3pt}% + \fi + {\def\thanks##1{\unskip{}}% + \def\iand{\\[5pt]\let\and=\nand}% + \def\nand{\ifhmode\unskip\nobreak\fi\ $\cdot$ }% + \let\and=\nand + \def\at{\\\let\and=\iand}% + \footnotetext[0]{\kern-\bibindent + \ignorespaces\@institute}\vspace{5dd}}% +%\if!\@mail!\else +% \footnotetext[0]{\kern-\bibindent\mailname\ +% \ignorespaces\@mail}% +%\fi +% + \if@runhead + \ProcessRunnHead + \fi +% + \endgroup + \setcounter{footnote}{0} + \global\let\thanks\relax + \global\let\maketitle\relax + \global\let\@maketitle\relax + \global\let\@thanks\@empty + \global\let\@author\@empty + \global\let\@date\@empty + \global\let\@title\@empty + \global\let\@subtitle\@empty + \global\let\title\relax + \global\let\author\relax + \global\let\date\relax + \global\let\and\relax} + +\def\makeheadbox{{% +\hbox to0pt{\vbox{\baselineskip=10dd\hrule\hbox +to\hsize{\vrule\kern3pt\vbox{\kern3pt +\hbox{\bfseries\@journalname\ manuscript No.} +\hbox{(will be inserted by the editor)} +\kern3pt}\hfil\kern3pt\vrule}\hrule}% +\hss}}} +% +\def\rubric{\setbox0=\hbox{\small\strut}\@tempdima=\ht0\advance +\@tempdima\dp0\advance\@tempdima2\fboxsep\vrule\@height\@tempdima +\@width\z@} +\newdimen\rubricwidth +% +\def\@maketitle{\newpage +\normalfont +\vbox to0pt{\if@twocolumn\vskip-39pt\else\vskip-49pt\fi +\nointerlineskip +\makeheadbox\vss}\nointerlineskip +\vbox to 0pt{\offinterlineskip\rubricwidth=\columnwidth +%%%%\vskip-12.5pt % -12.5pt +\if@twocolumn\else % one column journal + \divide\rubricwidth by144\multiply\rubricwidth by89 % perform golden section + \vskip-\topskip +\fi +\hrule\@height0.35mm\noindent +\advance\fboxsep by.25mm +\global\advance\rubricwidth by0pt +\rubric +\vss}\vskip19.5pt % war 9pt +% +\if@twocolumn\else + \gdef\footnoterule{% + \kern-3\p@ + \hrule\@width38mm % \columnwidth \rubricwidth + \kern2.6\p@} +\fi +% + \setbox\authrun=\vbox\bgroup + \if@twocolumn + \hrule\@height10.5mm\@width0\p@ + \else + \hrule\@height 2mm\@width0\p@ + \fi + \pretolerance=10000 + \rightskip=0pt plus 4cm + \nothanksmarks +% \if!\@headnote!\else +% \noindent +% {\LARGE\normalfont\itshape\ignorespaces\@headnote\par}\vskip 3.5mm +% \fi + {\LARGE\bfseries + \noindent\ignorespaces + \@title \par}\vskip 17pt\relax + \if!\@subtitle!\else + {\large\bfseries + \pretolerance=10000 + \rightskip=0pt plus 3cm + \vskip-12pt +% \noindent\ignorespaces\@subtitle \par}\vskip 11.24pt\relax + \noindent\ignorespaces\@subtitle \par}\vskip 17pt\relax + \fi + {\authorfont + \setbox0=\vbox{\setcounter{auth}{1}\def\and{\stepcounter{auth} }% + \hfuzz=2\textwidth\def\thanks##1{}\@author}% + \setcounter{footnote}{0}% + \global\value{inst}=\value{auth}% + \setcounter{auth}{1}% + \if@twocolumn + \rightskip43mm plus 4cm minus 3mm + \else % one column journal + \rightskip=\linewidth + \advance\rightskip by-\rubricwidth + \advance\rightskip by0pt plus 4cm minus 3mm + \fi +% +\def\and{\unskip\nobreak\enskip{\boldmath$\cdot$}\enskip\ignorespaces}% + \noindent\ignorespaces\@author\vskip7.23pt} +% + \small + \if!\@dedic!\else + \par + \normalsize\it + \addvspace\baselineskip + \noindent\@dedic + \fi + \egroup % end of header box + \@tempdima=\headerboxheight + \advance\@tempdima by-\ht\authrun + \unvbox\authrun + \ifdim\@tempdima>0pt + \vrule width0pt height\@tempdima\par + \fi + \noindent{\small\@date\if@twocolumn\vskip 7.2mm\else\vskip 5.2mm\fi} + \global\@minipagetrue + \global\everypar{\global\@minipagefalse\global\everypar{}}% +%\vskip22.47pt +} +% +\if@mathematic + \def\vec#1{\ensuremath{\mathchoice + {\mbox{\boldmath$\displaystyle\mathbf{#1}$}} + {\mbox{\boldmath$\textstyle\mathbf{#1}$}} + {\mbox{\boldmath$\scriptstyle\mathbf{#1}$}} + {\mbox{\boldmath$\scriptscriptstyle\mathbf{#1}$}}}} +\else + \def\vec#1{\ensuremath{\mathchoice + {\mbox{\boldmath$\displaystyle#1$}} + {\mbox{\boldmath$\textstyle#1$}} + {\mbox{\boldmath$\scriptstyle#1$}} + {\mbox{\boldmath$\scriptscriptstyle#1$}}}} +\fi +% +\def\tens#1{\ensuremath{\mathsf{#1}}} +% +\setcounter{secnumdepth}{3} +\newcounter {section} +\newcounter {subsection}[section] +\newcounter {subsubsection}[subsection] +\newcounter {paragraph}[subsubsection] +\newcounter {subparagraph}[paragraph] +\renewcommand\thesection {\@arabic\c@section} +\renewcommand\thesubsection {\thesection.\@arabic\c@subsection} +\renewcommand\thesubsubsection{\thesubsection.\@arabic\c@subsubsection} +\renewcommand\theparagraph {\thesubsubsection.\@arabic\c@paragraph} +\renewcommand\thesubparagraph {\theparagraph.\@arabic\c@subparagraph} +% +\def\@hangfrom#1{\setbox\@tempboxa\hbox{#1}% + \hangindent \z@\noindent\box\@tempboxa} +% +\def\@seccntformat#1{\csname the#1\endcsname\sectcounterend +\hskip\betweenumberspace} +% +% \newif\if@sectrule +% \if@twocolumn\else\let\@sectruletrue=\relax\fi +% \if@avier\let\@sectruletrue=\relax\fi +% \def\makesectrule{\if@sectrule\global\@sectrulefalse\null\vglue-\topskip +% \hrule\nobreak\parskip=5pt\relax\fi} +% % +% \let\makesectruleori=\makesectrule +% \def\restoresectrule{\global\let\makesectrule=\makesectruleori\global\@sectrulefalse} +% \def\nosectrule{\let\makesectrule=\restoresectrule} +% +\def\@startsection#1#2#3#4#5#6{% + \if@noskipsec \leavevmode \fi + \par + \@tempskipa #4\relax + \@afterindenttrue + \ifdim \@tempskipa <\z@ + \@tempskipa -\@tempskipa \@afterindentfalse + \fi + \if@nobreak + \everypar{}% + \else + \addpenalty\@secpenalty\addvspace\@tempskipa + \fi +% \ifnum#2=1\relax\@sectruletrue\fi + \@ifstar + {\@ssect{#3}{#4}{#5}{#6}}% + {\@dblarg{\@sect{#1}{#2}{#3}{#4}{#5}{#6}}}} +% +\def\@sect#1#2#3#4#5#6[#7]#8{% + \ifnum #2>\c@secnumdepth + \let\@svsec\@empty + \else + \refstepcounter{#1}% + \protected@edef\@svsec{\@seccntformat{#1}\relax}% + \fi + \@tempskipa #5\relax + \ifdim \@tempskipa>\z@ + \begingroup + #6{% \makesectrule + \@hangfrom{\hskip #3\relax\@svsec}% + \raggedright + \hyphenpenalty \@M% + \interlinepenalty \@M #8\@@par}% + \endgroup + \csname #1mark\endcsname{#7}% + \addcontentsline{toc}{#1}{% + \ifnum #2>\c@secnumdepth \else + \protect\numberline{\csname the#1\endcsname\sectcounterend}% + \fi + #7}% + \else + \def\@svsechd{% + #6{\hskip #3\relax + \@svsec #8\/\hskip\aftertext}% + \csname #1mark\endcsname{#7}% + \addcontentsline{toc}{#1}{% + \ifnum #2>\c@secnumdepth \else + \protect\numberline{\csname the#1\endcsname}% + \fi + #7}}% + \fi + \@xsect{#5}} +% +\def\@ssect#1#2#3#4#5{% + \@tempskipa #3\relax + \ifdim \@tempskipa>\z@ + \begingroup + #4{% \makesectrule + \@hangfrom{\hskip #1}% + \interlinepenalty \@M #5\@@par}% + \endgroup + \else + \def\@svsechd{#4{\hskip #1\relax #5}}% + \fi + \@xsect{#3}} + +% +% measures and setting of sections +% +\def\section{\@startsection{section}{1}{\z@}% + {-21dd plus-8pt minus-4pt}{10.5dd} + {\normalsize\bfseries\boldmath}} +\def\subsection{\@startsection{subsection}{2}{\z@}% + {-21dd plus-8pt minus-4pt}{10.5dd} + {\normalsize\upshape}} +\def\subsubsection{\@startsection{subsubsection}{3}{\z@}% + {-13dd plus-8pt minus-4pt}{10.5dd} + {\normalsize\itshape}} +\def\paragraph{\@startsection{paragraph}{4}{\z@}% + {-13pt plus-8pt minus-4pt}{\z@}{\normalsize\itshape}} + +\setlength\leftmargini {\parindent} +\leftmargin \leftmargini +\setlength\leftmarginii {\parindent} +\setlength\leftmarginiii {1.87em} +\setlength\leftmarginiv {1.7em} +\setlength\leftmarginv {.5em} +\setlength\leftmarginvi {.5em} +\setlength \labelsep {.5em} +\setlength \labelwidth{\leftmargini} +\addtolength\labelwidth{-\labelsep} +\@beginparpenalty -\@lowpenalty +\@endparpenalty -\@lowpenalty +\@itempenalty -\@lowpenalty +\renewcommand\theenumi{\@arabic\c@enumi} +\renewcommand\theenumii{\@alph\c@enumii} +\renewcommand\theenumiii{\@roman\c@enumiii} +\renewcommand\theenumiv{\@Alph\c@enumiv} +\newcommand\labelenumi{\theenumi.} +\newcommand\labelenumii{(\theenumii)} +\newcommand\labelenumiii{\theenumiii.} +\newcommand\labelenumiv{\theenumiv.} +\renewcommand\p@enumii{\theenumi} +\renewcommand\p@enumiii{\theenumi(\theenumii)} +\renewcommand\p@enumiv{\p@enumiii\theenumiii} +\newcommand\labelitemi{\normalfont\bfseries --} +\newcommand\labelitemii{\normalfont\bfseries --} +\newcommand\labelitemiii{$\m@th\bullet$} +\newcommand\labelitemiv{$\m@th\cdot$} + +\if@spthms +% definition of the "\spnewtheorem" command. +% +% Usage: +% +% \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font} +% or \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font} +% or \spnewtheorem*{env_nam}{caption}{cap_font}{body_font} +% +% New is "cap_font" and "body_font". It stands for +% fontdefinition of the caption and the text itself. +% +% "\spnewtheorem*" gives a theorem without number. +% +% A defined spnewthoerem environment is used as described +% by Lamport. +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\def\@thmcountersep{} +\def\@thmcounterend{} +\newcommand\nocaption{\noexpand\@gobble} +\newdimen\spthmsep \spthmsep=5pt + +\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}} + +% definition of \spnewtheorem with number + +\def\@spnthm#1#2{% + \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}} +\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}} + +\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname + {\@definecounter{#1}\@addtoreset{#1}{#3}% + \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand + \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}% + \expandafter\xdef\csname #1name\endcsname{#2}% + \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}% + \global\@namedef{end#1}{\@endtheorem}}} + +\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname + {\@definecounter{#1}% + \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}% + \expandafter\xdef\csname #1name\endcsname{#2}% + \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}% + \global\@namedef{end#1}{\@endtheorem}}} + +\def\@spothm#1[#2]#3#4#5{% + \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}% + {\expandafter\@ifdefinable\csname #1\endcsname + {\global\@namedef{the#1}{\@nameuse{the#2}}% + \expandafter\xdef\csname #1name\endcsname{#3}% + \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}% + \global\@namedef{end#1}{\@endtheorem}}}} + +\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@ +\labelsep=\spthmsep\refstepcounter{#1}% +\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}} + +\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}% + \ignorespaces} + +\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname + the#1\endcsname}{#5}{#3}{#4}\ignorespaces} + +\def\normalthmheadings{\def\@spbegintheorem##1##2##3##4{\trivlist\normalfont + \item[\hskip\labelsep{##3##1\ ##2\@thmcounterend}]##4} +\def\@spopargbegintheorem##1##2##3##4##5{\trivlist + \item[\hskip\labelsep{##4##1\ ##2}]{##4(##3)\@thmcounterend\ }##5}} +\normalthmheadings + +\def\reversethmheadings{\def\@spbegintheorem##1##2##3##4{\trivlist\normalfont + \item[\hskip\labelsep{##3##2\ ##1\@thmcounterend}]##4} +\def\@spopargbegintheorem##1##2##3##4##5{\trivlist + \item[\hskip\labelsep{##4##2\ ##1}]{##4(##3)\@thmcounterend\ }##5}} + +% definition of \spnewtheorem* without number + +\def\@sthm#1#2{\@Ynthm{#1}{#2}} + +\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname + {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}% + \expandafter\xdef\csname #1name\endcsname{#2}% + \global\@namedef{end#1}{\@endtheorem}}} + +\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@ +\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}} + +\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces} + +\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1} + {#4}{#2}{#3}\ignorespaces} + +\def\@Begintheorem#1#2#3{#3\trivlist + \item[\hskip\labelsep{#2#1\@thmcounterend}]} + +\def\@Opargbegintheorem#1#2#3#4{#4\trivlist + \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }} + +% initialize theorem environment + +\if@envcntsect + \def\@thmcountersep{.} + \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape} +\else + \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape} + \if@envcntreset + \@addtoreset{theorem}{section} + \else + \@addtoreset{theorem}{chapter} + \fi +\fi + +%definition of divers theorem environments +\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily} +\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily} +\if@envcntsame % all environments like "Theorem" - using its counter + \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}} +\else % all environments with their own counter + \if@envcntsect % show section counter + \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}} + \else % not numbered with section + \if@envcntreset + \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4} + \@addtoreset{#1}{section}} + \else + \let\spn@wtheorem=\@spynthm + \fi + \fi +\fi +% +\let\spdefaulttheorem=\spn@wtheorem +% +\spn@wtheorem{case}{Case}{\itshape}{\rmfamily} +\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily} +\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape} +\spn@wtheorem{definition}{Definition}{\bfseries}{\rmfamily} +\spn@wtheorem{example}{Example}{\itshape}{\rmfamily} +\spn@wtheorem{exercise}{Exercise}{\bfseries}{\rmfamily} +\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape} +\spn@wtheorem{note}{Note}{\itshape}{\rmfamily} +\spn@wtheorem{problem}{Problem}{\bfseries}{\rmfamily} +\spn@wtheorem{property}{Property}{\itshape}{\rmfamily} +\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape} +\spn@wtheorem{question}{Question}{\itshape}{\rmfamily} +\spn@wtheorem{solution}{Solution}{\bfseries}{\rmfamily} +\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily} +% +\newenvironment{theopargself} + {\def\@spopargbegintheorem##1##2##3##4##5{\trivlist + \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5} + \def\@Opargbegintheorem##1##2##3##4{##4\trivlist + \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}}{} +\newenvironment{theopargself*} + {\def\@spopargbegintheorem##1##2##3##4##5{\trivlist + \item[\hskip\labelsep{##4##1\ ##2}]{\hspace*{-\labelsep}##4##3\@thmcounterend}##5} + \def\@Opargbegintheorem##1##2##3##4{##4\trivlist + \item[\hskip\labelsep{##3##1}]{\hspace*{-\labelsep}##3##2\@thmcounterend}}}{} +% +\fi + +\def\@takefromreset#1#2{% + \def\@tempa{#1}% + \let\@tempd\@elt + \def\@elt##1{% + \def\@tempb{##1}% + \ifx\@tempa\@tempb\else + \@addtoreset{##1}{#2}% + \fi}% + \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname + \expandafter\def\csname cl@#2\endcsname{}% + \@tempc + \let\@elt\@tempd} + +\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}} +\def\qed{\ifmmode\else\unskip\quad\fi\squareforqed} +\def\smartqed{\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil +\penalty50\hskip1em\null\nobreak\hfil\squareforqed +\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}} + +% Define `abstract' environment +\def\abstract{\topsep=0pt\partopsep=0pt\parsep=0pt\itemsep=0pt\relax +\trivlist\item[\hskip\labelsep +{\bfseries\abstractname}]\if!\abstractname!\hskip-\labelsep\fi} +\if@twocolumn +% \if@avier +% \def\endabstract{\endtrivlist\addvspace{5mm}\strich} +% \def\strich{\hrule\vskip1ptplus12pt} +% \else + \def\endabstract{\endtrivlist\addvspace{3mm}} +% \fi +\else +\fi +% +\newenvironment{verse} + {\let\\\@centercr + \list{}{\itemsep \z@ + \itemindent -1.5em% + \listparindent\itemindent + \rightmargin \leftmargin + \advance\leftmargin 1.5em}% + \item\relax} + {\endlist} +\newenvironment{quotation} + {\list{}{\listparindent 1.5em% + \itemindent \listparindent + \rightmargin \leftmargin + \parsep \z@ \@plus\p@}% + \item\relax} + {\endlist} +\newenvironment{quote} + {\list{}{\rightmargin\leftmargin}% + \item\relax} + {\endlist} +\newcommand\appendix{\par\small + \setcounter{section}{0}% + \setcounter{subsection}{0}% + \renewcommand\thesection{\@Alph\c@section}} +\setlength\arraycolsep{1.5\p@} +\setlength\tabcolsep{6\p@} +\setlength\arrayrulewidth{.4\p@} +\setlength\doublerulesep{2\p@} +\setlength\tabbingsep{\labelsep} +\skip\@mpfootins = \skip\footins +\setlength\fboxsep{3\p@} +\setlength\fboxrule{.4\p@} +\renewcommand\theequation{\@arabic\c@equation} +\newcounter{figure} +\renewcommand\thefigure{\@arabic\c@figure} +\def\fps@figure{tbp} +\def\ftype@figure{1} +\def\ext@figure{lof} +\def\fnum@figure{\figurename~\thefigure} +\newenvironment{figure} + {\@float{figure}} + {\end@float} +\newenvironment{figure*} + {\@dblfloat{figure}} + {\end@dblfloat} +\newcounter{table} +\renewcommand\thetable{\@arabic\c@table} +\def\fps@table{tbp} +\def\ftype@table{2} +\def\ext@table{lot} +\def\fnum@table{\tablename~\thetable} +\newenvironment{table} + {\@float{table}} + {\end@float} +\newenvironment{table*} + {\@dblfloat{table}} + {\end@dblfloat} +% +\def \@floatboxreset {% + \reset@font + \small + \@setnobreak + \@setminipage +} +% +\newcommand{\tableheadseprule}{\noalign{\hrule height.375mm}} +% +\newlength\abovecaptionskip +\newlength\belowcaptionskip +\setlength\abovecaptionskip{10\p@} +\setlength\belowcaptionskip{0\p@} +\newcommand\leftlegendglue{} + +\def\fig@type{figure} + +\newdimen\figcapgap\figcapgap=3pt +\newdimen\tabcapgap\tabcapgap=5.5pt + +\@ifundefined{floatlegendstyle}{\def\floatlegendstyle{\bfseries}}{} + +\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname + ext@#1\endcsname}{#1}{\protect\numberline{\csname + the#1\endcsname}{\ignorespaces #2}}\begingroup + \@parboxrestore + \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par + \endgroup} + +\def\capstrut{\vrule\@width\z@\@height\topskip} + +\@ifundefined{captionstyle}{\def\captionstyle{\normalfont\small}}{} + +\long\def\@makecaption#1#2{% + \captionstyle + \ifx\@captype\fig@type + \vskip\figcapgap + \fi + \setbox\@tempboxa\hbox{{\floatlegendstyle #1\floatcounterend}% + \capstrut #2}% + \ifdim \wd\@tempboxa >\hsize + {\floatlegendstyle #1\floatcounterend}\capstrut #2\par + \else + \hbox to\hsize{\leftlegendglue\unhbox\@tempboxa\hfil}% + \fi + \ifx\@captype\fig@type\else + \vskip\tabcapgap + \fi} + +\newdimen\figgap\figgap=1cc +\long\def\@makesidecaption#1#2{% + \parbox[b]{\@tempdimb}{\captionstyle{\floatlegendstyle + #1\floatcounterend}#2}} +\def\sidecaption#1\caption{% +\setbox\@tempboxa=\hbox{#1\unskip}% +\if@twocolumn + \ifdim\hsize<\textwidth\else + \ifdim\wd\@tempboxa<\columnwidth + \typeout{Double column float fits into single column - + ^^Jyou'd better switch the environment. }% + \fi + \fi +\fi +\@tempdimb=\hsize +\advance\@tempdimb by-\figgap +\advance\@tempdimb by-\wd\@tempboxa +\ifdim\@tempdimb<3cm + \typeout{\string\sidecaption: No sufficient room for the legend; + using normal \string\caption. }% + \unhbox\@tempboxa + \let\@capcommand=\@caption +\else + \let\@capcommand=\@sidecaption + \leavevmode + \unhbox\@tempboxa + \hfill +\fi +\refstepcounter\@captype +\@dblarg{\@capcommand\@captype}} + +\long\def\@sidecaption#1[#2]#3{\addcontentsline{\csname + ext@#1\endcsname}{#1}{\protect\numberline{\csname + the#1\endcsname}{\ignorespaces #2}}\begingroup + \@parboxrestore + \@makesidecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par + \endgroup} + +% Define `acknowledgement' environment +\def\acknowledgement{\par\addvspace{17pt}\small\rmfamily +\trivlist\if!\ackname!\item[]\else +\item[\hskip\labelsep +{\bfseries\ackname}]\fi} +\def\endacknowledgement{\endtrivlist\addvspace{6pt}} +\newenvironment{acknowledgements}{\begin{acknowledgement}} +{\end{acknowledgement}} +% Define `noteadd' environment +\def\noteadd{\par\addvspace{17pt}\small\rmfamily +\trivlist\item[\hskip\labelsep +{\itshape\noteaddname}]} +\def\endnoteadd{\endtrivlist\addvspace{6pt}} + +\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm} +\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf} +\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt} +\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf} +\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit} +\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl} +\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc} +\DeclareRobustCommand*\cal{\@fontswitch\relax\mathcal} +\DeclareRobustCommand*\mit{\@fontswitch\relax\mathnormal} +\newcommand\@pnumwidth{1.55em} +\newcommand\@tocrmarg{2.55em} +\newcommand\@dotsep{4.5} +\setcounter{tocdepth}{1} +\newcommand\tableofcontents{% + \section*{\contentsname}% + \@starttoc{toc}% + \addtocontents{toc}{\begingroup\protect\small}% + \AtEndDocument{\addtocontents{toc}{\endgroup}}% + } +\newcommand*\l@part[2]{% + \ifnum \c@tocdepth >-2\relax + \addpenalty\@secpenalty + \addvspace{2.25em \@plus\p@}% + \begingroup + \setlength\@tempdima{3em}% + \parindent \z@ \rightskip \@pnumwidth + \parfillskip -\@pnumwidth + {\leavevmode + \large \bfseries #1\hfil \hb@xt@\@pnumwidth{\hss #2}}\par + \nobreak + \if@compatibility + \global\@nobreaktrue + \everypar{\global\@nobreakfalse\everypar{}}% + \fi + \endgroup + \fi} +\newcommand*\l@section{\@dottedtocline{1}{0pt}{1.5em}} +\newcommand*\l@subsection{\@dottedtocline{2}{1.5em}{2.3em}} +\newcommand*\l@subsubsection{\@dottedtocline{3}{3.8em}{3.2em}} +\newcommand*\l@paragraph{\@dottedtocline{4}{7.0em}{4.1em}} +\newcommand*\l@subparagraph{\@dottedtocline{5}{10em}{5em}} +\newcommand\listoffigures{% + \section*{\listfigurename + \@mkboth{\listfigurename}% + {\listfigurename}}% + \@starttoc{lof}% + } +\newcommand*\l@figure{\@dottedtocline{1}{1.5em}{2.3em}} +\newcommand\listoftables{% + \section*{\listtablename + \@mkboth{\listtablename}{\listtablename}}% + \@starttoc{lot}% + } +\let\l@table\l@figure +\newdimen\bibindent +\setlength\bibindent{\parindent} +\def\@biblabel#1{#1.} +\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw + {\let\protect\noexpand + \immediate + \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces} +\newenvironment{thebibliography}[1] + {\section*{\refname + \@mkboth{\refname}{\refname}}\small + \list{\@biblabel{\@arabic\c@enumiv}}% + {\settowidth\labelwidth{\@biblabel{#1}}% + \leftmargin\labelwidth + \advance\leftmargin\labelsep + \@openbib@code + \usecounter{enumiv}% + \let\p@enumiv\@empty + \renewcommand\theenumiv{\@arabic\c@enumiv}}% + \sloppy\clubpenalty4000\widowpenalty4000% + \sfcode`\.\@m} + {\def\@noitemerr + {\@latex@warning{Empty `thebibliography' environment}}% + \endlist} +% +\newcount\@tempcntc +\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi + \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do + {\@ifundefined + {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries + ?}\@warning + {Citation `\@citeb' on page \thepage \space undefined}}% + {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}% + \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne + \@citea\def\@citea{,\hskip0.1em\ignorespaces}\hbox{\csname b@\@citeb\endcsname}% + \else + \advance\@tempcntb\@ne + \ifnum\@tempcntb=\@tempcntc + \else\advance\@tempcntb\m@ne\@citeo + \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}} +\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else + \@citea\def\@citea{,\hskip0.1em\ignorespaces}% + \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else + {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else \def\@citea{--}\fi + \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi} +% +\newcommand\newblock{\hskip .11em\@plus.33em\@minus.07em} +\let\@openbib@code\@empty +\newenvironment{theindex} + {\if@twocolumn + \@restonecolfalse + \else + \@restonecoltrue + \fi + \columnseprule \z@ + \columnsep 35\p@ + \twocolumn[\section*{\indexname}]% + \@mkboth{\indexname}{\indexname}% + \thispagestyle{plain}\parindent\z@ + \parskip\z@ \@plus .3\p@\relax + \let\item\@idxitem} + {\if@restonecol\onecolumn\else\clearpage\fi} +\newcommand\@idxitem{\par\hangindent 40\p@} +\newcommand\subitem{\@idxitem \hspace*{20\p@}} +\newcommand\subsubitem{\@idxitem \hspace*{30\p@}} +\newcommand\indexspace{\par \vskip 10\p@ \@plus5\p@ \@minus3\p@\relax} + +\if@twocolumn + \renewcommand\footnoterule{% + \kern-3\p@ + \hrule\@width\columnwidth + \kern2.6\p@} +\else + \renewcommand\footnoterule{% + \kern-3\p@ + \hrule\@width.382\columnwidth + \kern2.6\p@} +\fi +\newcommand\@makefntext[1]{% + \noindent + \hb@xt@\bibindent{\hss\@makefnmark\enspace}#1} +% +\def\trans@english{\switcht@albion} +\def\trans@french{\switcht@francais} +\def\trans@german{\switcht@deutsch} +\newenvironment{translation}[1]{\if!#1!\else +\@ifundefined{selectlanguage}{\csname trans@#1\endcsname}{\selectlanguage{#1}}% +\fi}{} +% languages +% English section +\def\switcht@albion{%\typeout{English spoken.}% + \def\abstractname{Abstract}% + \def\ackname{Acknowledgements}% + \def\andname{and}% + \def\lastandname{, and}% + \def\appendixname{Appendix}% + \def\chaptername{Chapter}% + \def\claimname{Claim}% + \def\conjecturename{Conjecture}% + \def\contentsname{Contents}% + \def\corollaryname{Corollary}% + \def\definitionname{Definition}% + \def\emailname{E-mail}% + \def\examplename{Example}% + \def\exercisename{Exercise}% + \def\figurename{Fig.}% + \def\keywordname{{\bfseries Keywords}}% + \def\indexname{Index}% + \def\lemmaname{Lemma}% + \def\contriblistname{List of Contributors}% + \def\listfigurename{List of Figures}% + \def\listtablename{List of Tables}% + \def\mailname{{\itshape Correspondence to\/}:}% + \def\noteaddname{Note added in proof}% + \def\notename{Note}% + \def\partname{Part}% + \def\problemname{Problem}% + \def\proofname{Proof}% + \def\propertyname{Property}% + \def\questionname{Question}% + \def\refname{References}% + \def\remarkname{Remark}% + \def\seename{see}% + \def\solutionname{Solution}% + \def\tablename{Table}% + \def\theoremname{Theorem}% +}\switcht@albion % make English default +% +% French section +\def\switcht@francais{\svlanginfo +%\typeout{On parle francais.}% + \def\abstractname{R\'esum\'e\runinend}% + \def\ackname{Remerciements\runinend}% + \def\andname{et}% + \def\lastandname{ et}% + \def\appendixname{Appendice}% + \def\chaptername{Chapitre}% + \def\claimname{Pr\'etention}% + \def\conjecturename{Hypoth\`ese}% + \def\contentsname{Table des mati\`eres}% + \def\corollaryname{Corollaire}% + \def\definitionname{D\'efinition}% + \def\emailname{E-mail}% + \def\examplename{Exemple}% + \def\exercisename{Exercice}% + \def\figurename{Fig.}% + \def\keywordname{{\bfseries Mots-cl\'e\runinend}}% + \def\indexname{Index}% + \def\lemmaname{Lemme}% + \def\contriblistname{Liste des contributeurs}% + \def\listfigurename{Liste des figures}% + \def\listtablename{Liste des tables}% + \def\mailname{{\itshape Correspondence to\/}:}% + \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}% + \def\notename{Remarque}% + \def\partname{Partie}% + \def\problemname{Probl\`eme}% + \def\proofname{Preuve}% + \def\propertyname{Caract\'eristique}% +%\def\propositionname{Proposition}% + \def\questionname{Question}% + \def\refname{Bibliographie}% + \def\remarkname{Remarque}% + \def\seename{voyez}% + \def\solutionname{Solution}% +%\def\subclassname{{\it Subject Classifications\/}:}% + \def\tablename{Tableau}% + \def\theoremname{Th\'eor\`eme}% +} +% +% German section +\def\switcht@deutsch{\svlanginfo +%\typeout{Man spricht deutsch.}% + \def\abstractname{Zusammenfassung\runinend}% + \def\ackname{Danksagung\runinend}% + \def\andname{und}% + \def\lastandname{ und}% + \def\appendixname{Anhang}% + \def\chaptername{Kapitel}% + \def\claimname{Behauptung}% + \def\conjecturename{Hypothese}% + \def\contentsname{Inhaltsverzeichnis}% + \def\corollaryname{Korollar}% +%\def\definitionname{Definition}% + \def\emailname{E-Mail}% + \def\examplename{Beispiel}% + \def\exercisename{\"Ubung}% + \def\figurename{Abb.}% + \def\keywordname{{\bfseries Schl\"usselw\"orter\runinend}}% + \def\indexname{Index}% +%\def\lemmaname{Lemma}% + \def\contriblistname{Mitarbeiter}% + \def\listfigurename{Abbildungsverzeichnis}% + \def\listtablename{Tabellenverzeichnis}% + \def\mailname{{\itshape Correspondence to\/}:}% + \def\noteaddname{Nachtrag}% + \def\notename{Anmerkung}% + \def\partname{Teil}% +%\def\problemname{Problem}% + \def\proofname{Beweis}% + \def\propertyname{Eigenschaft}% +%\def\propositionname{Proposition}% + \def\questionname{Frage}% + \def\refname{Literatur}% + \def\remarkname{Anmerkung}% + \def\seename{siehe}% + \def\solutionname{L\"osung}% +%\def\subclassname{{\it Subject Classifications\/}:}% + \def\tablename{Tabelle}% +%\def\theoremname{Theorem}% +} +\newcommand\today{} +\edef\today{\ifcase\month\or + January\or February\or March\or April\or May\or June\or + July\or August\or September\or October\or November\or December\fi + \space\number\day, \number\year} +\setlength\columnsep{1.5cc} +\setlength\columnseprule{0\p@} +% +\frenchspacing +\clubpenalty=10000 +\widowpenalty=10000 +\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil +\global\let\@textbottom\relax}} +\pagestyle{headings} +\pagenumbering{arabic} +\if@twocolumn + \twocolumn +\fi +%\if@avier +% \onecolumn +% \setlength{\textwidth}{156mm} +% \setlength{\textheight}{226mm} +%\fi +\if@referee + \makereferee +\fi +\flushbottom +\endinput +%% +%% End of file `svjour3.cls'.
--- a/utm/uncomputable.thy Wed Dec 12 11:45:04 2012 +0000 +++ b/utm/uncomputable.thy Fri Mar 01 17:13:32 2013 +0000 @@ -37,136 +37,110 @@ *} fun tcopy_F0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F0 x tp = (let (ln, rn) = tp in - list_all isBk ln & rn = replicate x Oc - @ [Bk] @ replicate x Oc)" + "tcopy_F0 x (l, r) = (\<exists> i. l = Bk\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)" fun tcopy_F1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F1 x (ln, rn) = (ln = [] & rn = replicate x Oc)" + "tcopy_F1 x (l, r) = (l = [] \<and> r = Oc\<^bsup>x\<^esup>)" fun tcopy_F2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" - where - "tcopy_F2 0 tp = False" | - "tcopy_F2 (Suc x) (ln, rn) = (length ln > 0 & - ln @ rn = replicate (Suc x) Oc)" + where + "tcopy_F2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>j\<^esup>)" fun tcopy_F3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F3 0 tp = False" | - "tcopy_F3 (Suc x) (ln, rn) = - (ln = Bk # replicate (Suc x) Oc & length rn <= 1)" + "tcopy_F3 x (l, r) = (x > 0 \<and> l = Bk # Oc\<^bsup>x\<^esup> \<and> tl r = [])" fun tcopy_F4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F4 0 tp = False" | - "tcopy_F4 (Suc x) (ln, rn) = - ((ln = replicate x Oc & rn = [Oc, Bk, Oc]) - | (ln = replicate (Suc x) Oc & rn = [Bk, Oc])) " + "tcopy_F4 x (l, r) = (x > 0 \<and> ((l = Oc\<^bsup>x\<^esup> \<and> r = [Bk, Oc]) \<or> (l = Oc\<^bsup>x - 1\<^esup> \<and> r = [Oc, Bk, Oc])))" + +fun tcopy_F5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" + where + "tcopy_F5_loop x (l, r) = + (\<exists> i j. i + j + 1 = x \<and> l = Oc\<^bsup>i\<^esup> \<and> r = Oc # Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup> \<and> j > 0)" + +fun tcopy_F5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" + where + "tcopy_F5_exit x (l, r) = + (l = [] \<and> r = Bk # Oc # Bk\<^bsup>x\<^esup> @ Oc\<^bsup>x\<^esup> \<and> x > 0 )" fun tcopy_F5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F5 0 tp = False" | - "tcopy_F5 (Suc x) (ln, rn) = - (if rn = [] then False - else if hd rn = Bk then (ln = [] & - rn = Bk # (Oc # replicate (Suc x) Bk - @ replicate (Suc x) Oc)) - else if hd rn = Oc then - (\<exists>n. ln = replicate (x - n) Oc - & rn = Oc # (Oc # replicate n Bk @ replicate n Oc) - & n > 0 & n <= x) - else False)" - + "tcopy_F5 x (l, r) = (tcopy_F5_loop x (l, r) \<or> tcopy_F5_exit x (l, r))" fun tcopy_F6 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F6 0 tp = False" | - "tcopy_F6 (Suc x) (ln, rn) = - (\<exists>n. ln = replicate (Suc x -n) Oc - & tl rn = replicate n Bk @ replicate n Oc - & n > 0 & n <= x)" - + "tcopy_F6 x (l, r) = + (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<^bsup>i\<^esup> \<and> r = any#Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)" + fun tcopy_F7 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F7 0 tp = False" | - "tcopy_F7 (Suc x) (ln, rn) = - (let lrn = (rev ln) @ rn in - (\<exists>n. lrn = replicate ((Suc x) - n) Oc @ - replicate (Suc n) Bk @ replicate n Oc - & n > 0 & n <= x & - length rn >= n & length rn <= 2 * n ))" - + "tcopy_F7 x (l, r) = + (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = Suc j \<and> l = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk\<^bsup>t\<^esup> @ Oc\<^bsup>j\<^esup>)" + fun tcopy_F8 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F8 0 tp = False" | - "tcopy_F8 (Suc x) (ln, rn) = - (let lrn = (rev ln) @ rn in - (\<exists>n. lrn = replicate ((Suc x) - n) Oc @ - replicate (Suc n) Bk @ replicate n Oc - & n > 0 & n <= x & length rn < n)) " + "tcopy_F8 x (l, r) = + (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> l = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>Suc j\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>t\<^esup>)" + +fun tcopy_F9_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" +where + "tcopy_F9_loop x (l, r) = + (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0\<and> l = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>j\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Oc\<^bsup>t\<^esup>)" + +fun tcopy_F9_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" + where + "tcopy_F9_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> l = Bk\<^bsup>j - 1\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk # Oc\<^bsup>j\<^esup>)" fun tcopy_F9 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F9 0 tp = False" | - "tcopy_F9 (Suc x) (ln, rn) = - (let lrn = (rev ln) @ rn in - (\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc - @ replicate n Bk @ replicate n Oc - & n > Suc 0 & n <= Suc x & length rn > 0 - & length rn <= Suc n))" + "tcopy_F9 x (l, r) = (tcopy_F9_loop x (l, r) \<or> + tcopy_F9_exit x (l, r))" + +fun tcopy_F10_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" + where + "tcopy_F10_loop x (l, r) = + (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>i\<^esup> \<and> r = Bk\<^bsup>Suc t\<^esup> @ Oc\<^bsup>j\<^esup>)" + +fun tcopy_F10_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" + where + "tcopy_F10_exit x (l, r) = + (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<^bsup>i\<^esup> \<and> r = Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)" fun tcopy_F10 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F10 0 tp = False" | - "tcopy_F10 (Suc x) (ln, rn) = - (let lrn = (rev ln) @ rn in - (\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc - @ replicate n Bk @ replicate n Oc & n > Suc 0 - & n <= Suc x & length rn > Suc n & - length rn <= 2*n + 1 ))" + "tcopy_F10 x (l, r) = (tcopy_F10_loop x (l, r) \<or> tcopy_F10_exit x (l, r))" fun tcopy_F11 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F11 0 tp = False" | - "tcopy_F11 (Suc x) (ln, rn) = - (ln = [Bk] & rn = Oc # replicate (Suc x) Bk - @ replicate (Suc x) Oc)" + "tcopy_F11 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<^bsup>x\<^esup> @ Oc\<^bsup>x\<^esup>)" fun tcopy_F12 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F12 0 tp = False" | - "tcopy_F12 (Suc x) (ln, rn) = - (let lrn = ((rev ln) @ rn) in - (\<exists>n. n > 0 & n <= Suc (Suc x) - & lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk - @ replicate (Suc x) Oc - & length ln = Suc n))" + "tcopy_F12 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Bk\<^bsup>j\<^esup> @ Oc\<^bsup>x\<^esup>)" fun tcopy_F13 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F13 0 tp = False" | - "tcopy_F13 (Suc x) (ln, rn) = - (let lrn = ((rev ln) @ rn) in - (\<exists>n. n > Suc 0 & n <= Suc (Suc x) - & lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk - @ replicate (Suc x) Oc - & length ln = n))" - + "tcopy_F13 x (l, r) = + (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Oc # Bk\<^bsup>j\<^esup> @ Oc\<^bsup>x\<^esup> )" + fun tcopy_F14 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F14 0 tp = False" | - "tcopy_F14 (Suc x) (ln, rn) = - (ln = replicate (Suc x) Oc @ [Bk] & - tl rn = replicate (Suc x) Oc)" + "tcopy_F14 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<^bsup>x\<^esup> @ [Bk] \<and> r = any#Oc\<^bsup>x\<^esup>)" + +fun tcopy_F15_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" + where + "tcopy_F15_loop x (l, r) = + (\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<^bsup>i\<^esup> @ [Bk] \<and> r = Oc\<^bsup>j\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)" + +fun tcopy_F15_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" + where + "tcopy_F15_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)" fun tcopy_F15 :: "nat \<Rightarrow> tape \<Rightarrow> bool" where - "tcopy_F15 0 tp = False" | - "tcopy_F15 (Suc x) (ln, rn) = - (let lrn = ((rev ln) @ rn) in - lrn = Bk # replicate (Suc x) Oc @ [Bk] @ - replicate (Suc x) Oc & length ln <= (Suc x))" + "tcopy_F15 x (l, r) = (tcopy_F15_loop x (l, r) \<or> tcopy_F15_exit x (l, r))" text {* The following @{text "inv_tcopy"} is the invariant of the {\em Copying} TM. @@ -208,17 +182,12 @@ tcopy_F14.simps [simp del] tcopy_F15.simps [simp del] -lemma list_replicate_Bk[dest]: "list_all isBk list \<Longrightarrow> - list = replicate (length list) Bk" -apply(induct list) -apply(simp+) +lemma exp_zero_simp: "(a\<^bsup>b\<^esup> = []) = (b = 0)" +apply(auto simp: exponent_def) done -lemma [simp]: "dropWhile (\<lambda> a. a = b) (replicate x b @ ys) = - dropWhile (\<lambda> a. a = b) ys" -apply(induct x) -apply(simp) -apply(simp) +lemma exp_zero_simp2: "([] = a\<^bsup>b\<^esup> ) = (b = 0)" +apply(auto simp: exponent_def) done lemma [elim]: "\<lbrakk>tstep (0, a, b) tcopy = (s, l, r); s \<noteq> 0\<rbrakk> \<Longrightarrow> RR" @@ -300,6 +269,7 @@ by(simp add: tstep.simps tcopy_def fetch.simps split: block.splits list.splits) +(* lemma min_Suc4: "min (Suc (Suc x)) x = x" by auto @@ -330,22 +300,26 @@ replicate n b @ b # xs" apply(simp) done - +*) lemma [elim]: "\<lbrakk>tstep (14, b, c) tcopy = (15, ab, ba); tcopy_F14 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)" -apply(case_tac x) apply(auto simp: tstep.simps tcopy_def tcopy_F14.simps tcopy_F15.simps fetch.simps new_tape.simps split: if_splits list.splits block.splits) +apply(erule_tac [!] x = "x - 1" in allE) +apply(case_tac [!] x, simp_all add: exp_ind_def exp_zero) +apply(erule_tac [!] x = "Suc 0" in allE, simp_all) done +(* lemma dropWhile_drophd: "\<not> p a \<Longrightarrow> (dropWhile p xs @ (a # as)) = (dropWhile p (xs @ [a]) @ as)" apply(induct xs) apply(auto) done - +*) +(* lemma dropWhile_append3: "\<lbrakk>\<not> p a; listall ((dropWhile p xs) @ [a]) isBk\<rbrakk> \<Longrightarrow> listall (dropWhile p (xs @ [a])) isBk" @@ -364,495 +338,341 @@ apply(induct xs) apply(simp+) done +*) +lemma false_case1: + "\<lbrakk>Oc\<^bsup>j\<^esup> @ Bk # Oc\<^bsup>i + j\<^esup> = Oc # list; + 0 < i; + \<forall>ia. tl (Oc\<^bsup>i\<^esup> @ [Bk]) = Oc\<^bsup>ia\<^esup> @ [Bk] \<longrightarrow> (\<forall>ja. ia + ja = i + j + \<longrightarrow> hd (Oc\<^bsup>i\<^esup> @ [Bk]) # Oc # list \<noteq> Oc\<^bsup>ja\<^esup> @ Bk # Oc\<^bsup>i + j\<^esup>)\<rbrakk> + \<Longrightarrow> RR" +apply(case_tac i, auto simp: exp_ind_def) +apply(erule_tac x = nat in allE, simp add:exp_ind_def) +apply(erule_tac x = "Suc j" in allE, simp) +done + +lemma false_case3:"\<forall>ja. ja \<noteq> i \<Longrightarrow> RR" +by auto lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (15, ab, ba); - tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)" -apply(case_tac x) + tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)" apply(auto simp: tstep.simps tcopy_F15.simps tcopy_def fetch.simps new_tape.simps - split: if_splits list.splits block.splits) -apply(case_tac b, simp+) + split: if_splits list.splits block.splits elim: false_case1) +apply(case_tac [!] i, simp_all add: exp_zero exp_ind_def) +apply(erule_tac [!] x = nat in allE, simp_all add: exp_ind_def) +apply(auto elim: false_case3) done lemma [elim]: "\<lbrakk>tstep (14, b, c) tcopy = (14, ab, ba); tcopy_F14 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F14 x (ab, ba)" -apply(case_tac x) apply(auto simp: tcopy_F14.simps tcopy_def tstep.simps tcopy_F14.simps fetch.simps new_tape.simps split: if_splits list.splits block.splits) done -lemma [intro]: "list_all isBk (replicate x Bk)" -apply(induct x, simp+) -done - -lemma [elim]: "list_all isBk (dropWhile (\<lambda>a. a = Oc) b) \<Longrightarrow> - list_all isBk (dropWhile (\<lambda>a. a = Oc) (tl b))" -apply(case_tac b, auto split: if_splits) -apply(drule list_replicate_Bk) -apply(case_tac "length list", auto) -done - -lemma [elim]: "list_all (\<lambda> a. a = Oc) list \<Longrightarrow> - list = replicate (length list) Oc" -apply(induct list) -apply(simp+) -done - -lemma append_length: "\<lbrakk>as @ bs = cs @ ds; length bs = length ds\<rbrakk> - \<Longrightarrow> as = cs & bs = ds" -apply(auto) -done - -lemma Suc_elim: "Suc (Suc m) - n = Suc na \<Longrightarrow> Suc m - n = na" -apply(simp) -done - -lemma [elim]: "\<lbrakk>0 < n; n \<le> Suc (Suc na); - rev b @ Oc # list = - Bk # replicate n Oc @ replicate (Suc (Suc na) - n) Bk @ - Oc # replicate na Oc; - length b = Suc n; b \<noteq> []\<rbrakk> - \<Longrightarrow> list_all isBk (dropWhile (\<lambda>a. a = Oc) (tl b))" -apply(case_tac "rev b", auto) -done - -lemma b_cons_same: "b#bs = replicate x a @ as \<Longrightarrow> a \<noteq> b \<longrightarrow> x = 0" -apply(case_tac x, simp+) -done - -lemma tcopy_tmp[elim]: - "\<lbrakk>0 < n; n \<le> Suc (Suc na); - rev b @ Oc # list = - Bk # replicate n Oc @ replicate (Suc (Suc na) - n) Bk - @ Oc # replicate na Oc; length b = Suc n; b \<noteq> []\<rbrakk> - \<Longrightarrow> list = replicate na Oc" -apply(case_tac "rev b", simp+) -apply(auto) -apply(frule b_cons_same, auto) -done lemma [elim]: "\<lbrakk>tstep (12, b, c) tcopy = (14, ab, ba); tcopy_F12 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F14 x (ab, ba)" -apply(case_tac x) apply(auto simp:tcopy_F12.simps tcopy_F14.simps tcopy_def tstep.simps fetch.simps new_tape.simps split: if_splits list.splits block.splits) -apply(frule tcopy_tmp, simp+) -apply(case_tac n, simp+) -apply(case_tac nata, simp+) -done - -lemma replicate_app_Cons: "replicate a b @ b # replicate c b - = replicate (Suc (a + c)) b" -apply(simp) -apply(simp add: replicate_app_Cons_same) -apply(simp only: replicate_add[THEN sym]) -done - -lemma replicate_same_exE_pref: "\<exists>x. bs @ (b # cs) = replicate x y - \<Longrightarrow> (\<exists>n. bs = replicate n y)" -apply(induct bs) -apply(rule_tac x = 0 in exI, simp) -apply(drule impI) -apply(erule impE) -apply(erule exE, simp+) -apply(case_tac x, auto) -apply(case_tac x, auto) -apply(rule_tac x = "Suc n" in exI, simp+) -done - -lemma replicate_same_exE_inf: "\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> b = y" -apply(induct bs, auto) -apply(case_tac x, auto) -apply(drule impI) -apply(erule impE) -apply(case_tac x, simp+) -done - -lemma replicate_same_exE_suf: - "\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> \<exists>n. cs = replicate n y" -apply(induct bs, auto) -apply(case_tac x, simp+) -apply(drule impI, erule impE) -apply(case_tac x, simp+) -done - -lemma replicate_same_exE: "\<exists>x. bs @ (b # cs) = replicate x y - \<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)" -apply(rule conjI) -apply(drule replicate_same_exE_pref, simp) -apply(rule conjI) -apply(drule replicate_same_exE_inf, simp) -apply(drule replicate_same_exE_suf, simp) -done - -lemma replicate_same: "bs @ (b # cs) = replicate x y - \<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)" -apply(rule_tac replicate_same_exE) -apply(rule_tac x = x in exI) -apply(assumption) -done - -lemma [elim]: "\<lbrakk> 0 < n; n \<le> Suc (Suc na); - (rev ab @ Bk # list) = Bk # replicate n Oc - @ replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc; ab \<noteq> []\<rbrakk> - \<Longrightarrow> n \<le> Suc na" -apply(rule contrapos_pp, simp+) -apply(case_tac "rev ab", simp+) -apply(auto) -apply(simp only: replicate_app_Cons) -apply(drule replicate_same) -apply(auto) -done - - -lemma [elim]: "\<lbrakk>0 < n; n \<le> Suc (Suc na); - rev ab @ Bk # list = Bk # replicate n Oc @ - replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc; - length ab = Suc n; ab \<noteq> []\<rbrakk> - \<Longrightarrow> rev ab @ Oc # list = Bk # Oc # replicate n Oc @ - replicate (Suc na - n) Bk @ Oc # replicate na Oc" -apply(case_tac "rev ab", simp+) -apply(auto) -apply(simp only: replicate_Cons_simp) -apply(simp) -apply(case_tac "Suc (Suc na) - n", simp+) +apply(case_tac [!] j, simp_all add: exp_zero exp_ind_def) done lemma [elim]: "\<lbrakk>tstep (12, b, c) tcopy = (13, ab, ba); tcopy_F12 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F13 x (ab, ba)" -apply(case_tac x) -apply(simp_all add:tcopy_F12.simps tcopy_F13.simps - tcopy_def tstep.simps fetch.simps new_tape.simps) -apply(simp split: if_splits list.splits block.splits) -apply(auto) +apply(auto simp:tcopy_F12.simps tcopy_F13.simps + tcopy_def tstep.simps fetch.simps new_tape.simps + split: if_splits list.splits block.splits) +apply(case_tac x, simp_all add: exp_ind_def exp_zero) +apply(rule_tac [!] x = i in exI, simp_all) +apply(rule_tac [!] x = "j - 1" in exI) +apply(case_tac [!] j, simp_all add: exp_ind_def exp_zero) +apply(case_tac x, simp_all add: exp_ind_def exp_zero) done - lemma [elim]: "\<lbrakk>tstep (11, b, c) tcopy = (12, ab, ba); tcopy_F11 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 x (ab, ba)" -apply(case_tac x) apply(simp_all add:tcopy_F12.simps tcopy_F11.simps tcopy_def tstep.simps fetch.simps new_tape.simps) apply(auto) +apply(rule_tac x = "Suc 0" in exI, + rule_tac x = x in exI, simp add: exp_ind_def exp_zero) done -lemma equal_length: "a = b \<Longrightarrow> length a = length b" -by(simp) lemma [elim]: "\<lbrakk>tstep (13, b, c) tcopy = (12, ab, ba); tcopy_F13 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 x (ab, ba)" -apply(case_tac x) -apply(simp_all add:tcopy_F12.simps tcopy_F13.simps - tcopy_def tstep.simps fetch.simps new_tape.simps) -apply(simp split: if_splits list.splits block.splits) -apply(auto) -apply(drule equal_length, simp) +apply(auto simp:tcopy_F12.simps tcopy_F13.simps + tcopy_def tstep.simps fetch.simps new_tape.simps + split: if_splits list.splits block.splits) +apply(rule_tac [!] x = "Suc i" in exI, simp_all add: exp_ind_def) done lemma [elim]: "\<lbrakk>tstep (5, b, c) tcopy = (11, ab, ba); - tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F11 x (ab, ba)" -apply(case_tac x) + tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F11 x (ab, ba)" apply(simp_all add:tcopy_F11.simps tcopy_F5.simps tcopy_def tstep.simps fetch.simps new_tape.simps) apply(simp split: if_splits list.splits block.splits) done -lemma less_equal: "\<lbrakk>length xs <= b; \<not> Suc (length xs) <= b\<rbrakk> \<Longrightarrow> - length xs = b" -apply(simp) +lemma F10_false: "tcopy_F10 x (b, []) = False" +apply(auto simp: tcopy_F10.simps exp_ind_def) done -lemma length_cons_same: "\<lbrakk>xs @ b # ys = as @ bs; - length ys = length bs\<rbrakk> \<Longrightarrow> xs @ [b] = as & ys = bs" -apply(drule rev_equal) -apply(simp) -apply(auto) -apply(drule rev_equal, simp) +lemma F10_false2: "tcopy_F10 x ([], Bk # list) = False" +apply(auto simp:tcopy_F10.simps) +apply(case_tac i, simp_all add: exp_ind_def exp_zero) +done + +lemma [simp]: "tcopy_F10_exit x (b, Bk # list) = False" +apply(auto simp: tcopy_F10.simps) done -lemma replicate_set_equal: "\<lbrakk> xs @ [a] = replicate n b; a \<noteq> b\<rbrakk> \<Longrightarrow> RR" -apply(drule rev_equal, simp) -apply(case_tac n, simp+) +declare tcopy_F10_loop.simps[simp del] tcopy_F10_exit.simps[simp del] + +lemma [simp]: "tcopy_F10_loop x (b, [Bk]) = False" +apply(auto simp: tcopy_F10_loop.simps) +apply(simp add: exp_ind_def) done lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (10, ab, ba); tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)" -apply(case_tac x) -apply(auto simp:tcopy_F10.simps tcopy_def tstep.simps fetch.simps - new_tape.simps +apply(simp add: tcopy_def tstep.simps fetch.simps + new_tape.simps exp_ind_def exp_zero_simp exp_zero_simp2 F10_false F10_false2 split: if_splits list.splits block.splits) -apply(rule_tac x = n in exI, auto) -apply(case_tac b, simp+) -apply(rule contrapos_pp, simp+) -apply(frule less_equal, simp+) -apply(drule length_cons_same, auto) -apply(drule replicate_set_equal, simp+) +apply(simp add: tcopy_F10.simps del: tcopy_F10_loop.simps tcopy_F10_exit.simps) +apply(case_tac b, simp, case_tac aa) +apply(rule_tac disjI1) +apply(simp only: tcopy_F10_loop.simps) +apply(erule_tac exE)+ +apply(rule_tac x = i in exI, rule_tac x = j in exI, + rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, simp) +apply(case_tac k, simp_all add: exp_ind_def exp_zero) +apply(case_tac i, simp_all add: exp_ind_def exp_zero) +apply(rule_tac disjI2) +apply(simp only: tcopy_F10_loop.simps tcopy_F10_exit.simps) +apply(erule_tac exE)+ +apply(rule_tac x = "i - 1" in exI, rule_tac x = "j" in exI) +apply(case_tac k, simp_all add: exp_ind_def exp_zero) +apply(case_tac i, simp_all add: exp_ind_def exp_zero) +apply(auto) +apply(simp add: exp_ind_def) done -lemma less_equal2: "\<not> (n::nat) \<le> m \<Longrightarrow> \<exists>x. n = x + m & x > 0" -apply(rule_tac x = "n - m" in exI) -apply(auto) +(* +lemma false_case4: "\<lbrakk>i + (k + t) = Suc x; + 0 < i; + Bk # list = Oc\<^bsup>t\<^esup>; + \<forall>ia j. ia + j = Suc x \<longrightarrow> ia = 0 \<or> (\<forall>ka. tl (Oc\<^bsup>k\<^esup>) @ Bk\<^bsup>k + t\<^esup> @ Oc\<^bsup>i\<^esup> = Bk\<^bsup>ka\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow> (\<forall>ta. Suc (ka + ta) = j \<longrightarrow> Oc # Oc\<^bsup>t\<^esup> \<noteq> Bk\<^bsup>Suc ta\<^esup> @ Oc\<^bsup>j\<^esup>)); + 0 < k\<rbrakk> + \<Longrightarrow> RR" +apply(case_tac t, simp_all add: exp_ind_def exp_zero) +done + +lemma false_case5: " + \<lbrakk>Suc (i + nata) = x; + 0 < i; + \<forall>ia j. ia + j = Suc x \<longrightarrow> ia = 0 \<or> (\<forall>k. Bk\<^bsup>nata\<^esup> @ Oc\<^bsup>i\<^esup> = Bk\<^bsup>k\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow> (\<forall>t. Suc (k + t) = j \<longrightarrow> Bk # Oc # Oc # Oc\<^bsup>nata\<^esup> \<noteq> Bk\<^bsup>t\<^esup> @ Oc\<^bsup>j\<^esup>))\<rbrakk> + \<Longrightarrow> False" +apply(erule_tac x = i in allE, simp) +apply(erule_tac x = "Suc (Suc nata)" in allE, simp) +apply(erule_tac x = nata in allE, simp, simp add: exp_ind_def exp_zero) +done + +lemma false_case6: "\<lbrakk>0 < x; \<forall>i. tl (Oc\<^bsup>x\<^esup>) = Oc\<^bsup>i\<^esup> \<longrightarrow> (\<forall>j. i + j = x \<longrightarrow> j = 0 \<or> [Bk, Oc] \<noteq> Bk\<^bsup>j\<^esup> @ Oc\<^bsup>j\<^esup>)\<rbrakk> + \<Longrightarrow> False" +apply(erule_tac x = "x - 1" in allE) +apply(case_tac x, simp_all add: exp_ind_def exp_zero) +apply(erule_tac x = "Suc 0" in allE, simp) +done +*) + +lemma [simp]: "tcopy_F9 x ([], b) = False" +apply(auto simp: tcopy_F9.simps) +apply(case_tac [!] i, simp_all add: exp_ind_def exp_zero) done -lemma replicate_tail_length[dest]: - "\<lbrakk>rev b @ Bk # list = xs @ replicate n Bk @ replicate n Oc\<rbrakk> - \<Longrightarrow> length list >= n" -apply(rule contrapos_pp, simp+) -apply(drule less_equal2, auto) -apply(drule rev_equal) -apply(simp add: replicate_add) -apply(auto) -apply(case_tac x, simp+) +lemma [simp]: "tcopy_F9 x (b, []) = False" +apply(auto simp: tcopy_F9.simps) +apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero) +done + +declare tcopy_F9_loop.simps[simp del] tcopy_F9_exit.simps[simp del] +lemma [simp]: "tcopy_F9_loop x (b, Bk # list) = False" +apply(auto simp: tcopy_F9_loop.simps) +apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero) done +lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (10, ab, ba); + tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)" +apply(auto simp:tcopy_def + tstep.simps fetch.simps new_tape.simps exp_zero_simp + exp_zero_simp2 + split: if_splits list.splits block.splits) +apply(case_tac "hd b", simp add:tcopy_F9.simps tcopy_F10.simps ) +apply(simp only: tcopy_F9_exit.simps tcopy_F10_loop.simps) +apply(erule_tac exE)+ +apply(rule_tac x = i in exI, rule_tac x = j in exI, simp) +apply(rule_tac x = "j - 2" in exI, simp add: exp_ind_def) +apply(case_tac j, simp, simp) +apply(case_tac nat, simp_all add: exp_zero exp_ind_def) +apply(case_tac x, simp_all add: exp_ind_def exp_zero) +apply(simp add: tcopy_F9.simps tcopy_F10.simps) +apply(rule_tac disjI2) +apply(simp only: tcopy_F10_exit.simps tcopy_F9_exit.simps) +apply(erule_tac exE)+ +apply(simp) +apply(case_tac j, simp_all, case_tac nat, simp_all add: exp_ind_def exp_zero) +apply(case_tac x, simp_all add: exp_ind_def exp_zero) +apply(rule_tac x = nata in exI, rule_tac x = 1 in exI, simp add: exp_ind_def exp_zero) +done -lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (10, ab, ba); - tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)" -apply(case_tac x) -apply(auto simp:tcopy_F10.simps tcopy_F9.simps tcopy_def - tstep.simps fetch.simps new_tape.simps - split: if_splits list.splits block.splits) -apply(rule_tac x = n in exI, auto) -apply(case_tac b, simp+) +lemma false_case7: + "\<lbrakk>i + (n + t) = x; 0 < i; 0 < t; Oc # list = Oc\<^bsup>t\<^esup>; k = Suc n; + \<forall>j. i + j = Suc x \<longrightarrow> (\<forall>k. Oc\<^bsup>n\<^esup> @ Bk # Bk\<^bsup>n + t\<^esup> = Oc\<^bsup>k\<^esup> @ Bk\<^bsup>j\<^esup> \<longrightarrow> + (\<forall>ta. k + ta = j \<longrightarrow> ta = 0 \<or> Oc # Oc\<^bsup>t\<^esup> \<noteq> Oc\<^bsup>ta\<^esup>))\<rbrakk> + \<Longrightarrow> RR" +apply(erule_tac x = "k + t" in allE, simp) +apply(erule_tac x = n in allE, simp add: exp_ind_def) +apply(erule_tac x = "Suc t" in allE, simp) +done + +lemma false_case8: + "\<lbrakk>i + t = Suc x; + 0 < i; + 0 < t; + \<forall>ia j. tl (Bk\<^bsup>t\<^esup> @ Oc\<^bsup>i\<^esup>) = Bk\<^bsup>j - Suc 0\<^esup> @ Oc\<^bsup>ia\<^esup> \<longrightarrow> + ia + j = Suc x \<longrightarrow> ia = 0 \<or> j = 0 \<or> Oc\<^bsup>t\<^esup> \<noteq> Oc\<^bsup>j\<^esup>\<rbrakk> \<Longrightarrow> + RR" +apply(erule_tac x = i in allE, simp) +apply(erule_tac x = t in allE, simp) +apply(case_tac t, simp_all add: exp_ind_def exp_zero) done lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (9, ab, ba); tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)" -apply(case_tac x) -apply(simp_all add: tcopy_F9.simps tcopy_def - tstep.simps fetch.simps new_tape.simps +apply(auto simp: tcopy_F9.simps tcopy_def + tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2 + tcopy_F9_exit.simps tcopy_F9_loop.simps split: if_splits list.splits block.splits) -apply(rule_tac x = n in exI, auto) -apply(case_tac b, simp+) -apply(rule contrapos_pp, simp+) -apply(drule less_equal, simp+) -apply(drule rev_equal, auto) -apply(case_tac "length list", simp+) +apply(case_tac [!] k, simp_all add: exp_ind_def exp_zero) +apply(erule_tac [!] x = i in allE, simp) +apply(erule_tac false_case7, simp_all)+ +apply(case_tac t, simp_all add: exp_zero exp_ind_def) +apply(erule_tac false_case7, simp_all)+ +apply(erule_tac false_case8, simp_all) +apply(erule_tac false_case7, simp_all)+ +apply(case_tac t, simp_all add: exp_ind_def exp_zero) +apply(erule_tac false_case7, simp_all) +apply(erule_tac false_case8, simp_all) +apply(erule_tac false_case7, simp_all) +done + +lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (9, ab, ba); + tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)" +apply(auto simp:tcopy_F8.simps tcopy_F9.simps tcopy_def + tstep.simps fetch.simps new_tape.simps tcopy_F9_loop.simps + tcopy_F9_exit.simps + split: if_splits list.splits block.splits) +apply(case_tac [!] t, simp_all add: exp_ind_def exp_zero) +apply(rule_tac x = i in exI) +apply(rule_tac x = "Suc k" in exI, simp) +apply(rule_tac x = "k" in exI, simp add: exp_ind_def exp_zero) done -lemma app_cons_app_simp: "xs @ a # bs @ ys = (xs @ [a]) @ bs @ ys" -apply(simp) -done - -lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (9, ab, ba); - tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)" -apply(case_tac x) -apply(auto simp:tcopy_F8.simps tcopy_F9.simps tcopy_def - tstep.simps fetch.simps new_tape.simps - split: if_splits list.splits block.splits) -apply(rule_tac x = "Suc n" in exI, auto) -apply(rule_tac x = "n" in exI, auto) -apply(simp only: app_cons_app_simp) -apply(frule replicate_tail_length, simp) -done lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (8, ab, ba); tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)" -apply(case_tac x) -apply(simp_all add:tcopy_F8.simps tcopy_def tstep.simps - fetch.simps new_tape.simps) -apply(simp split: if_splits list.splits block.splits) -apply(rule_tac x = "n" in exI, auto) -done - -lemma ex_less_more: "\<lbrakk>(x::nat) >= m ; x <= n\<rbrakk> \<Longrightarrow> - \<exists>y. x = m + y & y <= n - m" -by(rule_tac x = "x -m" in exI, auto) - -lemma replicate_split: "x <= n \<Longrightarrow> - (\<exists>y. replicate n b = replicate (y + x) b)" -apply(rule_tac x = "n - x" in exI) -apply(simp) -done - -lemma app_app_app_app_simp: "as @ bs @ cs @ ds = - (as @ bs) @ (cs @ ds)" -by simp - -lemma lengthtailsame_append_elim: - "\<lbrakk>as @ bs = cs @ ds; length bs = length ds\<rbrakk> \<Longrightarrow> bs = ds" -apply(simp) +apply(auto simp:tcopy_F8.simps tcopy_def tstep.simps + fetch.simps new_tape.simps exp_zero_simp exp_zero split: if_splits list.splits + + block.splits) +apply(rule_tac x = i in exI, rule_tac x = "k + t" in exI, simp) +apply(rule_tac x = "Suc k" in exI, simp) +apply(rule_tac x = "t - 1" in exI, simp) +apply(case_tac t, simp_all add: exp_zero exp_ind_def) done -lemma rep_suc: "replicate (Suc n) x = replicate n x @ [x]" -by(induct n, auto) - -lemma length_append_diff_cons: - "\<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x; x \<noteq> y; - Suc (length ba) \<le> m + n\<rbrakk> - \<Longrightarrow> length ba < n" -apply(induct n arbitrary: ba, simp) -apply(drule_tac b = y in replicate_split, - simp add: replicate_add, erule exE, simp del: replicate.simps) -proof - - fix ba ya - assume h1: - "b @ x # ba = xs @ y # replicate ya y @ replicate (length ba) y" - and h2: "x \<noteq> y" - thus "False" - using append_eq_append_conv[of "b @ [x]" - "xs @ y # replicate ya y" "ba" "replicate (length ba) y"] - apply(auto) - apply(case_tac ya, simp, - simp add: rep_suc del: rep_suc_rev replicate.simps) - done -next - fix n ba - assume ind: "\<And>ba. \<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x; - x \<noteq> y; Suc (length ba) \<le> m + n\<rbrakk> - \<Longrightarrow> length ba < n" - and h1: "b @ x # ba = xs @ replicate m y @ replicate (Suc n) x" - and h2: "x \<noteq> y" and h3: "Suc (length ba) \<le> m + Suc n" - show "length ba < Suc n" - proof(cases "length ba") - case 0 thus "?thesis" by simp - next - fix nat - assume "length ba = Suc nat" - hence "\<exists> ys a. ba = ys @ [a]" - apply(rule_tac x = "butlast ba" in exI) - apply(rule_tac x = "last ba" in exI) - using append_butlast_last_id[of ba] - apply(case_tac ba, auto) - done - from this obtain ys where "\<exists> a. ba = ys @ [a]" .. - from this obtain a where "ba = ys @ [a]" .. - thus "?thesis" - using ind[of ys] h1 h2 h3 - apply(simp del: rep_suc_rev replicate.simps add: rep_suc) - done - qed -qed - -lemma [elim]: - "\<lbrakk>b @ Oc # ba = xs @ Bk # replicate n Bk @ replicate n Oc; - Suc (length ba) \<le> 2 * n\<rbrakk> - \<Longrightarrow> length ba < n" - apply(rule_tac length_append_diff_cons[of b Oc ba xs "Suc n" Bk n]) - apply(simp, simp, simp) - done - -lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (8, ab, ba); - tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)" -apply(case_tac x) -apply(simp_all add:tcopy_F8.simps tcopy_F7.simps - tcopy_def tstep.simps fetch.simps new_tape.simps) -apply(simp split: if_splits list.splits block.splits) -apply(rule_tac x = "n" in exI, auto) -done lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (7, ab, ba); tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)" -apply(case_tac x) -apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps - fetch.simps new_tape.simps - split: if_splits list.splits block.splits) -apply(rule_tac x = "n" in exI, auto) -apply(simp only: app_cons_app_simp) -apply(frule replicate_tail_length, simp) +apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps fetch.simps + new_tape.simps exp_ind_def exp_zero_simp + split: if_splits list.splits block.splits) +apply(rule_tac x = i in exI) +apply(rule_tac x = j in exI, simp) +apply(rule_tac x = "Suc k" in exI, simp) +apply(rule_tac x = "t - 1" in exI) +apply(case_tac t, simp_all add: exp_zero exp_ind_def) +apply(case_tac j, simp_all add: exp_zero exp_ind_def) done -lemma Suc_more: "n <= m \<Longrightarrow> Suc m - n = Suc (m - n)" -by simp +lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (8, ab, ba); + tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)" +apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps tcopy_F8.simps + fetch.simps new_tape.simps exp_zero_simp + split: if_splits list.splits block.splits) +apply(rule_tac x = i in exI, simp) +apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero) +apply(rule_tac x = "j - 1" in exI, simp) +apply(case_tac t, simp_all add: exp_ind_def ) +apply(case_tac j, simp_all add: exp_ind_def exp_zero) +done lemma [elim]: "\<lbrakk>tstep (6, b, c) tcopy = (7, ab, ba); tcopy_F6 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)" apply(case_tac x) apply(auto simp:tcopy_F7.simps tcopy_F6.simps - tcopy_def tstep.simps fetch.simps new_tape.simps + tcopy_def tstep.simps fetch.simps new_tape.simps exp_zero_simp split: if_splits list.splits block.splits) +apply(case_tac i, simp_all add: exp_ind_def exp_zero) +apply(rule_tac x = i in exI, simp) +apply(rule_tac x = j in exI, simp) +apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero) done lemma [elim]: "\<lbrakk>tstep (6, b, c) tcopy = (6, ab, ba); tcopy_F6 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)" -apply(case_tac x) apply(auto simp:tcopy_F6.simps tcopy_def tstep.simps new_tape.simps fetch.simps split: if_splits list.splits block.splits) done lemma [elim]: "\<lbrakk>tstep (5, b, c) tcopy = (6, ab, ba); - tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)" -apply(case_tac x) + tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)" apply(auto simp:tcopy_F5.simps tcopy_F6.simps tcopy_def - tstep.simps fetch.simps new_tape.simps + tstep.simps fetch.simps new_tape.simps exp_zero_simp2 split: if_splits list.splits block.splits) -apply(rule_tac x = n in exI, simp) -apply(rule_tac x = n in exI, simp) -apply(drule Suc_more, simp) -done - -lemma ex_less_more2: "\<lbrakk>(n::nat) < x ; x <= 2 * n\<rbrakk> \<Longrightarrow> - \<exists>y. (x = n + y & y <= n)" -apply(rule_tac x = "x - n" in exI) -apply(auto) -done - -lemma app_app_app_simp: "xs @ ys @ za = (xs @ ys) @ za" -apply(simp) -done - -lemma [elim]: "rev xs = replicate n b \<Longrightarrow> xs = replicate n b" -using rev_replicate[of n b] -thm rev_equal -by(drule_tac rev_equal, simp) - -lemma app_cons_tail_same[dest]: - "\<lbrakk>rev b @ Oc # list = - replicate (Suc (Suc na) - n) Oc @ replicate n Bk @ replicate n Oc; - Suc 0 < n; n \<le> Suc na; n < length list; length list \<le> 2 * n; b \<noteq> []\<rbrakk> - \<Longrightarrow> list = replicate n Bk @ replicate n Oc - & b = replicate (Suc na - n) Oc" -using length_append_diff_cons[of "rev b" Oc list - "replicate (Suc (Suc na) - n) Oc" n Bk n] -apply(case_tac "length list = 2*n", simp) -using append_eq_append_conv[of "rev b @ [Oc]" "replicate - (Suc (Suc na) - n) Oc" "list" "replicate n Bk @ replicate n Oc"] -apply(case_tac n, simp, simp add: Suc_more rep_suc - del: rep_suc_rev replicate.simps, auto) -done - -lemma hd_replicate_false1: "\<lbrakk>replicate x Oc \<noteq> []; - hd (replicate x Oc) = Bk\<rbrakk> \<Longrightarrow> RR" -apply(case_tac x, auto) -done - -lemma hd_replicate_false2: "\<lbrakk>replicate x Oc \<noteq> []; - hd (replicate x Oc) \<noteq> Oc\<rbrakk> \<Longrightarrow> RR" -apply(case_tac x, auto) -done - -lemma Suc_more_less: "\<lbrakk>n \<le> Suc m; n >= m\<rbrakk> \<Longrightarrow> n = m | n = Suc m" -apply(auto) -done - -lemma replicate_not_Nil: "replicate x a \<noteq> [] \<Longrightarrow> x > 0" -apply(case_tac x, simp+) +apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero) +apply(rule_tac x = "Suc i" in exI, simp add: exp_ind_def) done lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (5, ab, ba); tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F5 x (ab, ba)" -apply(case_tac x) apply(auto simp:tcopy_F5.simps tcopy_F10.simps tcopy_def - tstep.simps fetch.simps new_tape.simps - split: if_splits list.splits block.splits) -apply(frule app_cons_tail_same, simp+) -apply(rule_tac x = n in exI, auto) + tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2 + exp_ind_def tcopy_F10.simps tcopy_F10_loop.simps tcopy_F10_exit.simps + split: if_splits list.splits block.splits ) +apply(erule_tac [!] x = "i - 1" in allE) +apply(erule_tac [!] x = j in allE, simp_all) +apply(case_tac [!] i, simp_all add: exp_ind_def) done lemma [elim]: "\<lbrakk>tstep (4, b, c) tcopy = (5, ab, ba); tcopy_F4 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F5 x (ab, ba)" -apply(case_tac x) apply(auto simp:tcopy_F5.simps tcopy_F4.simps tcopy_def - tstep.simps fetch.simps new_tape.simps + tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2 split: if_splits list.splits block.splits) +apply(case_tac x, simp, simp add: exp_ind_def exp_zero) +apply(erule_tac [!] x = "x - 2" in allE) +apply(erule_tac [!] x = "Suc 0" in allE) +apply(case_tac [!] x, simp_all add: exp_ind_def exp_zero) +apply(case_tac [!] nat, simp_all add: exp_ind_def exp_zero) done lemma [elim]: "\<lbrakk>tstep (3, b, c) tcopy = (4, ab, ba); tcopy_F3 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F4 x (ab, ba)" -apply(case_tac x) apply(auto simp:tcopy_F3.simps tcopy_F4.simps tcopy_def tstep.simps fetch.simps new_tape.simps split: if_splits list.splits block.splits) @@ -862,86 +682,68 @@ tcopy_F4 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F4 x (ab, ba)" apply(case_tac x) apply(auto simp:tcopy_F3.simps tcopy_F4.simps - tcopy_def tstep.simps fetch.simps new_tape.simps + tcopy_def tstep.simps fetch.simps new_tape.simps exp_zero_simp exp_zero_simp2 exp_ind_def split: if_splits list.splits block.splits) done lemma [elim]: "\<lbrakk>tstep (3, b, c) tcopy = (3, ab, ba); tcopy_F3 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F3 x (ab, ba)" -apply(case_tac x) apply(auto simp:tcopy_F3.simps tcopy_F4.simps tcopy_def tstep.simps fetch.simps new_tape.simps split: if_splits list.splits block.splits) done -lemma replicate_cons_back: "y # replicate x y = replicate (Suc x) y" -apply(simp) -done - -lemma replicate_cons_same: "bs @ (b # cs) = y # replicate x y \<Longrightarrow> - (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)" -apply(simp only: replicate_cons_back) -apply(drule_tac replicate_same) -apply(simp) -done - lemma [elim]: "\<lbrakk>tstep (2, b, c) tcopy = (3, ab, ba); tcopy_F2 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F3 x (ab, ba)" apply(case_tac x) apply(auto simp:tcopy_F3.simps tcopy_F2.simps tcopy_def tstep.simps fetch.simps new_tape.simps + exp_zero_simp exp_zero_simp2 exp_zero split: if_splits list.splits block.splits) -apply(drule replicate_cons_same, auto)+ +apply(case_tac [!] j, simp_all add: exp_zero exp_ind_def) done lemma [elim]: "\<lbrakk>tstep (2, b, c) tcopy = (2, ab, ba); tcopy_F2 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)" -apply(case_tac x) apply(auto simp:tcopy_F3.simps tcopy_F2.simps - tcopy_def tstep.simps fetch.simps new_tape.simps + tcopy_def tstep.simps fetch.simps new_tape.simps + exp_zero_simp exp_zero_simp2 exp_zero split: if_splits list.splits block.splits) -apply(frule replicate_cons_same, auto) -apply(simp add: replicate_app_Cons_same) +apply(rule_tac x = "Suc i" in exI, simp add: exp_ind_def exp_zero) +apply(rule_tac x = "j - 1" in exI, simp) +apply(case_tac j, simp_all add: exp_ind_def exp_zero) done lemma [elim]: "\<lbrakk>tstep (Suc 0, b, c) tcopy = (2, ab, ba); - tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)" -apply(case_tac x) -apply(simp_all add:tcopy_F2.simps tcopy_F1.simps - tcopy_def tstep.simps fetch.simps new_tape.simps) -apply(auto) + tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)" +apply(auto simp:tcopy_F1.simps tcopy_F2.simps + tcopy_def tstep.simps fetch.simps new_tape.simps + exp_zero_simp exp_zero_simp2 exp_zero + split: if_splits list.splits block.splits) +apply(rule_tac x = "Suc 0" in exI, simp) +apply(rule_tac x = "x - 1" in exI, simp) +apply(case_tac x, simp_all add: exp_ind_def exp_zero) done lemma [elim]: "\<lbrakk>tstep (Suc 0, b, c) tcopy = (0, ab, ba); tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)" -apply(case_tac x) apply(simp_all add:tcopy_F0.simps tcopy_F1.simps - tcopy_def tstep.simps fetch.simps new_tape.simps) -done - -lemma ex_less: "Suc x <= y \<Longrightarrow> \<exists>z. y = x + z & z > 0" -apply(rule_tac x = "y - x" in exI, auto) -done - -lemma [elim]: "\<lbrakk>xs @ Bk # ba = - Bk # Oc # replicate n Oc @ Bk # Oc # replicate n Oc; - length xs \<le> Suc n; xs \<noteq> []\<rbrakk> \<Longrightarrow> RR" -apply(case_tac xs, auto) -apply(case_tac list, auto) -apply(drule ex_less, auto) -apply(simp add: replicate_add) -apply(auto) -apply(case_tac z, simp+) + tcopy_def tstep.simps fetch.simps new_tape.simps + exp_zero_simp exp_zero_simp2 exp_zero + split: if_splits list.splits block.splits ) +apply(case_tac x, simp_all add: exp_ind_def exp_zero, auto) done lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (0, ab, ba); tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)" -apply(case_tac x) apply(auto simp: tcopy_F15.simps tcopy_F0.simps tcopy_def tstep.simps new_tape.simps fetch.simps split: if_splits list.splits block.splits) +apply(rule_tac x = "Suc 0" in exI, simp add: exp_ind_def exp_zero) +apply(case_tac [!] j, simp_all add: exp_ind_def exp_zero) done + lemma [elim]: "\<lbrakk>tstep (0, b, c) tcopy = (0, ab, ba); tcopy_F0 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)" apply(case_tac x) @@ -968,7 +770,7 @@ Invariant under mult-step execution. *} lemma inv_tcopy_steps: - "inv_tcopy x (steps (Suc 0, [], replicate x Oc) tcopy stp) " + "inv_tcopy x (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy stp) " apply(induct stp) apply(simp add: tstep.simps tcopy_def steps.simps tcopy_F1.simps inv_tcopy.simps) @@ -976,18 +778,6 @@ done -text {* - The followng lemmas gives the parital correctness of Copying TM. -*} -theorem inv_tcopy_rs: - "steps (Suc 0, [], replicate x Oc) tcopy stp = (0, l, r) - \<Longrightarrow> \<exists> n. l = replicate n Bk \<and> - r = replicate x Oc @ Bk # replicate x Oc" -apply(insert inv_tcopy_steps[of x stp]) -apply(auto simp: inv_tcopy.simps tcopy_F0.simps isBk.simps) -done - - (*----------halt problem of tcopy----------------------------------------*) @@ -1183,7 +973,6 @@ tcopy_state.simps tcopy_step.simps) apply(simp split: if_splits list.splits block.splits taction.splits) apply(auto) -apply(case_tac x, simp+) done lemma [elim]: "tcopy_F4 x (b, c) \<Longrightarrow> @@ -1193,7 +982,7 @@ lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps tcopy_stage.simps tcopy_state.simps tcopy_step.simps) apply(simp split: if_splits list.splits block.splits taction.splits) -apply(auto) +apply(auto simp: exp_ind_def) done lemma[simp]: "takeWhile (\<lambda>a. a = b) (replicate x b @ ys) = @@ -1226,7 +1015,7 @@ apply(simp split: if_splits list.splits block.splits taction.splits) apply(auto) apply(simp_all add: tcopy_phase.simps tcopy_stage.simps - tcopy_state.simps tcopy_step.simps) + tcopy_state.simps tcopy_step.simps exponent_def) done lemma [elim]: "tcopy_F7 x (b, c) \<Longrightarrow> @@ -1235,7 +1024,7 @@ apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps) apply(simp split: if_splits list.splits block.splits taction.splits) -apply(auto) +apply(auto simp: exp_zero_simp) apply(simp_all add: tcopy_phase.simps tcopy_stage.simps tcopy_state.simps tcopy_step.simps) done @@ -1246,12 +1035,14 @@ apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps) apply(simp split: if_splits list.splits block.splits taction.splits) -apply(auto) +apply(auto simp: exp_zero_simp) apply(simp_all add: tcopy_phase.simps tcopy_stage.simps - tcopy_state.simps tcopy_step.simps) -apply(simp only: app_cons_app_simp, frule replicate_tail_length, simp) + tcopy_state.simps tcopy_step.simps exponent_def) done +lemma rev_equal_rev: "rev a = rev b \<Longrightarrow> a = b" +by simp + lemma app_app_app_equal: "xs @ ys @ zs = (xs @ ys) @ zs" by simp @@ -1266,34 +1057,40 @@ apply(simp) done +lemma[simp]: "takeWhile (\<lambda>a. a = b) (replicate x b @ ys) = + replicate x b @ (takeWhile (\<lambda>a. a = b) ys)" +apply(induct x) +apply(simp+) +done + lemma [elim]: "tcopy_F9 x (b, c) \<Longrightarrow> (tstep (9, b, c) tcopy, 9, b, c) \<in> tcopy_LE" -apply(case_tac x, simp) apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def - lex_triple_def lex_pair_def tcopy_phase.simps) + lex_triple_def lex_pair_def tcopy_phase.simps tcopy_F9.simps + tcopy_F9_loop.simps tcopy_F9_exit.simps) apply(simp split: if_splits list.splits block.splits taction.splits) apply(auto) -apply(simp_all add: tcopy_phase.simps tcopy_stage.simps - tcopy_state.simps tcopy_step.simps) -apply(drule_tac bs = b and as = "Bk # list" in rev_tl_hd_merge) -apply(simp) -apply(drule_tac bs = b and as = "Oc # list" in rev_tl_hd_merge) -apply(simp) +apply(simp_all add: tcopy_phase.simps tcopy_stage.simps tcopy_F9_loop.simps + tcopy_state.simps tcopy_step.simps tstep.simps exp_zero_simp + exponent_def) +apply(case_tac [1-2] t, simp_all add: rev_tl_hd_merge) +apply(case_tac j, simp, simp) +apply(case_tac nat, simp_all) +apply(case_tac nata, simp_all) done lemma [elim]: "tcopy_F10 x (b, c) \<Longrightarrow> (tstep (10, b, c) tcopy, 10, b, c) \<in> tcopy_LE" -apply(case_tac x, simp) apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def - lex_triple_def lex_pair_def tcopy_phase.simps) + lex_triple_def lex_pair_def tcopy_phase.simps tcopy_F10_loop.simps + tcopy_F10_exit.simps exp_zero_simp) apply(simp split: if_splits list.splits block.splits taction.splits) -apply(auto) +apply(auto simp: exp_zero_simp) apply(simp_all add: tcopy_phase.simps tcopy_stage.simps - tcopy_state.simps tcopy_step.simps) -apply(drule_tac bs = b and as = "Bk # list" in rev_tl_hd_merge) -apply(simp) -apply(drule_tac bs = b and as = "Oc # list" in rev_tl_hd_merge) -apply(simp) + tcopy_state.simps tcopy_step.simps exponent_def + rev_tl_hd_merge) +apply(case_tac k, simp_all) +apply(case_tac nat, simp_all) done lemma [elim]: "tcopy_F11 x (b, c) \<Longrightarrow> @@ -1313,6 +1110,7 @@ apply(auto) apply(simp_all add: tcopy_phase.simps tcopy_stage.simps tcopy_state.simps tcopy_step.simps) +apply(simp_all add: exp_ind_def) done lemma [elim]: "tcopy_F13 x (b, c) \<Longrightarrow> @@ -1324,7 +1122,6 @@ apply(auto) apply(simp_all add: tcopy_phase.simps tcopy_stage.simps tcopy_state.simps tcopy_step.simps) -apply(drule equal_length, simp)+ done lemma [elim]: "tcopy_F14 x (b, c) \<Longrightarrow> @@ -1349,24 +1146,37 @@ tcopy_state.simps tcopy_step.simps) done +lemma exp_length: "length (a\<^bsup>b\<^esup>) = b" +apply(induct b, simp_all add: exp_zero exp_ind_def) +done + +declare tcopy_F9.simps[simp del] tcopy_F10.simps[simp del] + +lemma length_eq: "xs = ys \<Longrightarrow> length xs = length ys" +by simp + lemma tcopy_wf_step:"\<lbrakk>a > 0; inv_tcopy x (a, b, c)\<rbrakk> \<Longrightarrow> (tstep (a, b, c) tcopy, (a, b, c)) \<in> tcopy_LE" apply(simp add:inv_tcopy.simps split: if_splits, auto) apply(auto simp: tstep.simps tcopy_def tcopy_LE_def lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps tcopy_stage.simps tcopy_state.simps tcopy_step.simps + exp_length exp_zero_simp exponent_def split: if_splits list.splits block.splits taction.splits) +apply(case_tac [!] t, simp_all) +apply(case_tac j, simp_all) +apply(drule_tac length_eq, simp) done lemma tcopy_wf: -"\<forall>n. let nc = steps (Suc 0, [], replicate x Oc) tcopy n in - let Sucnc = steps (Suc 0, [], replicate x Oc) tcopy (Suc n) in +"\<forall>n. let nc = steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n in + let Sucnc = steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy (Suc n) in \<not> isS0 nc \<longrightarrow> ((Sucnc, nc) \<in> tcopy_LE)" proof(rule allI, case_tac - "steps (Suc 0, [], replicate x Oc) tcopy n", auto simp: tstep_red) + "steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n", auto simp: tstep_red) fix n a b c assume h: "\<not> isS0 (a, b, c)" - "steps (Suc 0, [], replicate x Oc) tcopy n = (a, b, c)" + "steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n = (a, b, c)" hence "inv_tcopy x (a, b, c)" using inv_tcopy_steps[of x n] by(simp) thus "(tstep (a, b, c) tcopy, a, b, c) \<in> tcopy_LE" @@ -1378,9 +1188,9 @@ The termination of Copying TM: *} lemma tcopy_halt: - "\<exists>n. isS0 (steps (Suc 0, [], replicate x Oc) tcopy n)" + "\<exists>n. isS0 (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)" apply(insert halt_lemma - [of tcopy_LE isS0 "steps (Suc 0, [], replicate x Oc) tcopy"]) + [of tcopy_LE isS0 "steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy"]) apply(insert tcopy_wf [of x]) apply(simp only: Let_def) apply(insert wf_tcopy_le) @@ -1390,20 +1200,20 @@ text {* The total correntess of Copying TM: *} -theorem tcopy_halt_rs: "\<exists>stp m. - steps (Suc 0, [], replicate x Oc) tcopy stp = - (0, replicate m Bk, replicate x Oc @ Bk # replicate x Oc)" +theorem tcopy_halt_rs: + "\<exists>stp m. + steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy stp = + (0, Bk\<^bsup>m\<^esup>, Oc\<^bsup>x\<^esup> @ Bk # Oc\<^bsup>x\<^esup>)" using tcopy_halt[of x] proof(erule_tac exE) fix n - assume h: "isS0 (steps (Suc 0, [], replicate x Oc) tcopy n)" - have "inv_tcopy x (steps (Suc 0, [], replicate x Oc) tcopy n)" + assume h: "isS0 (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)" + have "inv_tcopy x (steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)" using inv_tcopy_steps[of x n] by simp thus "?thesis" using h - apply(cases "(steps (Suc 0, [], replicate x Oc) tcopy n)", + apply(cases "(steps (Suc 0, [], Oc\<^bsup>x\<^esup>) tcopy n)", auto simp: isS0_def inv_tcopy.simps) - apply(rule_tac x = n in exI, auto) done qed @@ -1505,10 +1315,10 @@ *} and h_case: "\<And> M n. \<lbrakk>(haltP M n)\<rbrakk> \<Longrightarrow> - \<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc]))" + \<exists> na nb. (steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc]))" and nh_case: "\<And> M n. \<lbrakk>(\<not> haltP M n)\<rbrakk> \<Longrightarrow> - \<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))" + \<exists> na nb. (steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))" begin term t_correct @@ -1519,6 +1329,117 @@ lemma [simp]: "a\<^bsup>0\<^esup> = []" by(simp add: exponent_def) + +lemma tinres_ex1: + "tinres (Bk\<^bsup>nb\<^esup>) b \<Longrightarrow> \<exists>nb. b = Bk\<^bsup>nb\<^esup>" +apply(auto simp: tinres_def) +proof - + fix n + assume "Bk\<^bsup>nb\<^esup> = b @ Bk\<^bsup>n\<^esup>" + thus "\<exists>nb. b = Bk\<^bsup>nb\<^esup>" + proof(induct b arbitrary: nb) + show "\<exists>nb. [] = Bk\<^bsup>nb\<^esup>" + by(rule_tac x = 0 in exI, simp add: exp_zero) + next + fix a b nb + assume ind: "\<And>nb. Bk\<^bsup>nb\<^esup> = b @ Bk\<^bsup>n\<^esup> \<Longrightarrow> \<exists>nb. b = Bk\<^bsup>nb\<^esup>" + and h: "Bk\<^bsup>nb\<^esup> = (a # b) @ Bk\<^bsup>n\<^esup>" + from h show "\<exists>nb. a # b = Bk\<^bsup>nb\<^esup>" + proof(case_tac a, case_tac nb, simp_all add: exp_ind_def) + fix nat + assume "Bk\<^bsup>nat\<^esup> = b @ Bk\<^bsup>n\<^esup>" + thus "\<exists>nb. Bk # b = Bk\<^bsup>nb\<^esup>" + using ind[of nat] + apply(auto) + apply(rule_tac x = "Suc nb" in exI, simp add: exp_ind_def) + done + next + assume "Bk\<^bsup>nb\<^esup> = Oc # b @ Bk\<^bsup>n\<^esup>" + thus "\<exists>nb. Oc # b = Bk\<^bsup>nb\<^esup>" + apply(case_tac nb, simp_all add: exp_ind_def) + done + qed + qed +next + fix n + show "\<exists>nba. Bk\<^bsup>nb\<^esup> @ Bk\<^bsup>n\<^esup> = Bk\<^bsup>nba\<^esup>" + apply(rule_tac x = "nb + n" in exI) + apply(simp add: exponent_def replicate_add) + done +qed + +lemma h_newcase: "\<And> M n. \<lbrakk>(haltP M n)\<rbrakk> \<Longrightarrow> + \<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc]))" +proof - + fix M n x + assume "haltP M n" + hence " \<exists> na nb. (steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na + = (0, Bk\<^bsup>nb\<^esup>, [Oc]))" + apply(erule_tac h_case) + done + from this obtain na nb where + cond1:"(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na + = (0, Bk\<^bsup>nb\<^esup>, [Oc]))" by blast + thus "\<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc]))" + proof(rule_tac x = na in exI, case_tac "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na", simp) + fix a b c + assume cond2: "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)" + have "tinres (Bk\<^bsup>nb\<^esup>) b \<and> [Oc] = c \<and> 0 = a" + proof(rule_tac tinres_steps) + show "tinres [] (Bk\<^bsup>x\<^esup>)" + apply(simp add: tinres_def) + apply(auto) + done + next + show "(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na + = (0, Bk\<^bsup>nb\<^esup>, [Oc]))" + by(simp add: cond1) + next + show "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)" + by(simp add: cond2) + qed + thus "a = 0 \<and> (\<exists>nb. b = Bk\<^bsup>nb\<^esup>) \<and> c = [Oc]" + apply(auto simp: tinres_ex1) + done + qed +qed + +lemma nh_newcase: "\<And> M n. \<lbrakk>\<not> (haltP M n)\<rbrakk> \<Longrightarrow> + \<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))" +proof - + fix M n + assume "\<not> haltP M n" + hence "\<exists> na nb. (steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na + = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))" + apply(erule_tac nh_case) + done + from this obtain na nb where + cond1: "(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na + = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))" by blast + thus "\<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))" + proof(rule_tac x = na in exI, case_tac "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na", simp) + fix a b c + assume cond2: "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)" + have "tinres (Bk\<^bsup>nb\<^esup>) b \<and> [Oc, Oc] = c \<and> 0 = a" + proof(rule_tac tinres_steps) + show "tinres [] (Bk\<^bsup>x\<^esup>)" + apply(simp add: tinres_def) + apply(auto) + done + next + show "(steps (Suc 0, [], Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na + = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))" + by(simp add: cond1) + next + show "steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (a, b, c)" + by(simp add: cond2) + qed + thus "a = 0 \<and> (\<exists>nb. b = Bk\<^bsup>nb\<^esup>) \<and> c = [Oc, Oc]" + apply(auto simp: tinres_ex1) + done + qed +qed + lemma haltP_weaking: "haltP (tcontra H) (code (tcontra H)) \<Longrightarrow> \<exists>stp. isS0 (steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) @@ -1541,7 +1462,7 @@ assume h: "haltP (tcontra H) (code (tcontra H))" hence h1: "\<And> x. \<exists> na nb. steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc])" - by(drule_tac x = x in h_case, simp) + by(drule_tac x = x in h_newcase, simp) have "?P1 \<turnstile>-> \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) (tcopy |+| H) stp = (0, tp') \<and> ?Q2 tp')" proof(rule_tac turing_merge.t_merge_halt[of tcopy H "?P1" "?P2" "?P3" "?P3" "?Q1" "?Q2"], auto simp: turing_merge_def) @@ -1605,7 +1526,7 @@ have h1: "\<And> x. \<exists> na nb. steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>?cn\<^esup> @ Bk # Oc\<^bsup>?cn\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc])" using uh - by(drule_tac x = x in nh_case, simp) + by(drule_tac x = x in nh_newcase, simp) let ?P1 = "\<lambda> tp. let (l, r) = tp in (l = [] \<and> (r::block list) = Oc\<^bsup>(?cn)\<^esup>)" let ?Q1 = "\<lambda> (l, r).(\<exists> na. l = Bk\<^bsup>na\<^esup> \<and> r = [Oc, Oc])"