%

\begin{isabellebody}%

\def\isabellecontext{Build{\isaliteral{5F}{\isacharunderscore}}Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform}%

%

\isadelimtheory

\isanewline

\isanewline

%

\endisadelimtheory

%

\isatagtheory

\isacommand{theory}\isamarkupfalse%

\ Build{\isaliteral{5F}{\isacharunderscore}}Inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{5F}{\isacharunderscore}}Transform\ \isakeyword{imports}\ Isac\isanewline

\ \ \isanewline

\isakeyword{begin}%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

%

\begin{isamarkuptext}%

We stepwise build \texttt{Inverse\_Z\_Transform.thy} as an exercise.

  Because subsection "Stepwise Check the Program" requires 

  \texttt{Inverse\_Z\_Transform.thy} as a subtheory of Isac.thy, the setup has been changed 

  from "theory Inverse_Z_Transform imports Isac begin.." to the above.

  ATTENTION WITH NAMES OF IDENTIFIERS WHEN GOING INTO INTERNALS:

  Here in this theory there are the internal names twice, for instance we have

  (Thm.derivation_name \isa{rule{\isadigit{1}}} = "Build_Inverse_Z_Transform.rule1") = true;

  but actually in us will be "Inverse_Z_Transform.rule1"%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}val\ thy\ {\isaliteral{3D}{\isacharequal}}\ %

\isaantiq

theory\ Isac{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isamarkupsection{trials towards Z transform%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

===============================%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{terms%

}

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

%

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

%

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

%

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

%

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{5B}{\isacharbrackleft}}\ {\isaliteral{5D}{\isacharbrackright}}\ denotes\ lists\ {\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

%

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}Isac\isanewline

%

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ %

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}alpha\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{3C}{\isacharless}}{\isaliteral{2F}{\isacharslash}}alpha{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

%

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

%

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

%

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

%

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\ {\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ %

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\ {\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isamarkupsubsection{rules%

}

\isamarkuptrue%

\isacommand{axiomatization}\isamarkupfalse%

\ \isakeyword{where}\ \isanewline

\ \ rule{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C64656C74613E}{\isasymdelta}}{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ rule{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ rule{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ \isanewline

\ \ rule{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ rule{\isadigit{5}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ rule{\isadigit{6}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ z\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3E}{\isachargreater}}\ {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ z{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ u\ {\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

%

\isaantiq

thm\ rule{\isadigit{1}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

%

\isaantiq

thm\ rule{\isadigit{2}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

%

\isaantiq

thm\ rule{\isadigit{3}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

%

\isaantiq

thm\ rule{\isadigit{4}}{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isamarkupsubsection{apply rules%

}

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{5F}{\isacharunderscore}}Z{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline

\ \ {\isaliteral{5B}{\isacharbrackleft}}\ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %

\isaantiq

thm\ rule{\isadigit{3}}{}%

\endisaantiq

{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline

\ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{4}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %

\isaantiq

thm\ rule{\isadigit{4}}{}%

\endisaantiq

{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline

\ \ \ \ Thm\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}rule{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %

\isaantiq

thm\ rule{\isadigit{1}}{}%

\endisaantiq

{\isaliteral{29}{\isacharparenright}}\ \ \ \isanewline

\ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

\isanewline

val\ t\ {\isaliteral{3D}{\isacharequal}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ thy\ true\ inverse{\isaliteral{5F}{\isacharunderscore}}Z\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ t{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}attention\ rule{\isadigit{1}}\ {\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}%

\isaantiq

theory\ Isac{}%

\endisaantiq

{\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %

\isaantiq

thm\ rule{\isadigit{3}}{}%

\endisaantiq

{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %

\isaantiq

thm\ rule{\isadigit{4}}{}%

\endisaantiq

{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ {\isaliteral{28}{\isacharparenleft}}num{\isaliteral{5F}{\isacharunderscore}}str\ %

\isaantiq

thm\ rule{\isadigit{1}}{}%

\endisaantiq

{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{3F}{\isacharquery}}n\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{3F}{\isacharquery}}u\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C64656C74613E}{\isasymdelta}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2D}{\isacharminus}}\ real\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

term{\isadigit{2}}str\ t{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

terms{\isadigit{2}}str\ {\isaliteral{28}{\isacharparenleft}}asm{\isadigit{1}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{2}}\ {\isaliteral{40}{\isacharat}}\ asm{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isamarkupsection{Prepare steps for CTP-based programming language%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

TODO insert Calculation (Referenz?!)

The goal... realized in sections below, in Sect.\ref{spec-meth} and Sect.\ref{prog-steps} 

the reader is advised to jump between the subsequent subsections and the respective steps in Sect.\ref{prog-steps}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{prepare expression \label{prep-expr}%

}

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ ProofContext{\isaliteral{2E}{\isachardot}}init{\isaliteral{5F}{\isacharunderscore}}global\ %

\isaantiq

theory\ Isac{}%

\endisaantiq

{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ ctxt\ {\isaliteral{3D}{\isacharequal}}\ declare{\isaliteral{5F}{\isacharunderscore}}constraints{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5B}{\isacharbrackleft}}%

\isaantiq

term\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{}%

\endisaantiq

{\isaliteral{5D}{\isacharbrackright}}\ ctxt{\isaliteral{3B}{\isacharsemicolon}}\isanewline

\isanewline

val\ SOME\ fun{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ SOME\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isamarkupsubsubsection{multply with z%

}

\isamarkuptrue%

\isacommand{axiomatization}\isamarkupfalse%

\ \isakeyword{where}\isanewline

\ \ ruleZY{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{27}{\isacharprime}}\ z\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

%

\isadelimML

\isanewline

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}thy{\isaliteral{2C}{\isacharcomma}}\ ro{\isaliteral{2C}{\isacharcomma}}\ er{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}%

\isaantiq

theory\ Isac{}%

\endisaantiq

{\isaliteral{2C}{\isacharcomma}}\ tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ %

\isaantiq

thm\ ruleZY{}%

\endisaantiq

\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ asm{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ thy\ ro\ er\ true\ \ %

\isaantiq

thm\ ruleZY{}%

\endisaantiq

\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

\isanewline

val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %

\isaantiq

theory\ Isac{}%

\endisaantiq

\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fun{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}fails\ on\ x{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ TODO{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

val\ SOME\ {\isaliteral{28}{\isacharparenleft}}fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %

\isaantiq

theory\ Isac{}%

\endisaantiq

\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ fun{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}OK{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isamarkupsubsubsection{get argument of X': z is the variable the equation is solved for%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

grep... Atools.thy, Tools.thy contain general utilities: eval_argument_in, eval_rhs, eval_lhs,...

grep -r "fun eva_" ... shows all functions witch can be used in a script.

lookup this files how to build and handle such functions.

the next section shows how to introduce such a function.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsubsection{Decompose given term into lhs = rhs%

}

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

\ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ expr{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ fun{\isadigit{3}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ expr{\isaliteral{3B}{\isacharsemicolon}}\isanewline

\ \ val\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}\ denom{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}bin\ {\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}type{\isaliteral{5F}{\isacharunderscore}}of\ expr{\isaliteral{29}{\isacharparenright}}\ expr{\isaliteral{3B}{\isacharsemicolon}}\isanewline

\ \ term{\isadigit{2}}str\ denom\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

we have rhs in the Script language, but we need a function 

  which gets the denominator of a fraction%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsubsection{get the denominator and numerator out of a fraction%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

get denominator should become a constant for the isabelle parser:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{consts}\isamarkupfalse%

\isanewline

\ \ get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}real\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ real{\isaliteral{22}{\isachardoublequoteclose}}\isanewline

\ \ get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}real\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ real{\isaliteral{22}{\isachardoublequoteclose}}%

\begin{isamarkuptext}%

With the above definition we run into problems with parsing the Script InverseZTransform:

  This leads to "ambiguous parse trees" and we avoid this by shifting the definition

  to Rational.thy and re-building Isac.

  ATTENTION: from now on Build_Inverse_Z_Transform mimics a build from scratch;

  it only works due to re-building Isac several times (indicated explicityl).%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

fun\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{28}{\isacharparenleft}}thmid{\isaliteral{3A}{\isacharcolon}}string{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5F}{\isacharunderscore}}\ \isanewline

		\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}t\ as\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}denominator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ num\ {\isaliteral{24}{\isachardollar}}\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ denom{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ thy\ {\isaliteral{3D}{\isacharequal}}\ \isanewline

\ \ \ \ \ \ \ \ SOME\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}thmid\ thmid\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline

\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Print{\isaliteral{5F}{\isacharunderscore}}Mode{\isaliteral{2E}{\isachardot}}setmp\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}Syntax{\isaliteral{2E}{\isachardot}}string{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}thy{\isadigit{2}}ctxt\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ denom{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline

	\ \ \ \ \ \ \ \ \ \ Trueprop\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}equality\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ denom{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ {\isaliteral{7C}{\isacharbar}}\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}denominator\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ NONE{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline

\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

tests of eval_get_denominator see test/Knowledge/rational.sml%

\end{isamarkuptext}%

\isamarkuptrue%

%

\begin{isamarkuptext}%

get numerator should also become a constant for the isabelle parser:%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

fun\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{28}{\isacharparenleft}}thmid{\isaliteral{3A}{\isacharcolon}}string{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5F}{\isacharunderscore}}\ \isanewline

		\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}t\ as\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rational{\isaliteral{2E}{\isachardot}}get{\isaliteral{5F}{\isacharunderscore}}numerator{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}num\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{24}{\isachardollar}}denom\ {\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ thy\ {\isaliteral{3D}{\isacharequal}}\ \isanewline

\ \ \ \ \ \ \ \ SOME\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}thmid\ thmid\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}\ \isanewline

\ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Print{\isaliteral{5F}{\isacharunderscore}}Mode{\isaliteral{2E}{\isachardot}}setmp\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}Syntax{\isaliteral{2E}{\isachardot}}string{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}thy{\isadigit{2}}ctxt\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ num{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline

	\ \ \ \ \ \ \ \ \ \ Trueprop\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}equality\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ num{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ {\isaliteral{7C}{\isacharbar}}\ eval{\isaliteral{5F}{\isacharunderscore}}get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ NONE{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

We discovered severell problems by implementing the get_numerator function.

Remember when putting new functions to Isac, put them in a thy file and rebuild 

isac, also put them in the ruleset for the script!%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{solve equation%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

this type of equation if too general for the present program%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ Minisubplb{\isaliteral{2F}{\isacharslash}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{2D}{\isacharminus}}init{\isaliteral{2D}{\isacharminus}}rootp\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}OK{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}bl{\isaliteral{2E}{\isachardot}}sml\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ denominator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}solveFor\ z{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ TODO{\isaliteral{3A}{\isacharcolon}}\ ISAC\ determines\ type\ of\ eq{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

Does the Equation Match the Specification ?%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

match{\isaliteral{5F}{\isacharunderscore}}pbl\ fmz\ {\isaliteral{28}{\isacharparenleft}}get{\isaliteral{5F}{\isacharunderscore}}pbt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}Context{\isaliteral{2E}{\isachardot}}theory{\isaliteral{5F}{\isacharunderscore}}name\ thy\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ denominator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}specification{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}equality{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \ {\isaliteral{22}{\isachardoublequote}}solveFor\ z{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}bound\ variable{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \ {\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}identifier\ for\ solution{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline

\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}abcFormula{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}no{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

Does the Other Equation Match the Specification ?%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

match{\isaliteral{5F}{\isacharunderscore}}pbl\ fmz\ {\isaliteral{28}{\isacharparenleft}}get{\isaliteral{5F}{\isacharunderscore}}pbt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}abcFormula{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}degree{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}polynomial{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}univariate{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}equation{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

Solve Equation Stepwise%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ CalcTreeTEST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}fmz{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}dI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}pI{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}mI{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}nxt\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2C}{\isacharcomma}}Check{\isaliteral{5F}{\isacharunderscore}}elementwise\ {\isaliteral{22}{\isachardoublequote}}Assumptions{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \isanewline

val\ {\isaliteral{28}{\isacharparenleft}}p{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}f{\isaliteral{2C}{\isacharcomma}}nxt{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}pt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ me\ nxt\ p\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ pt{\isaliteral{3B}{\isacharsemicolon}}\ f{\isadigit{2}}str\ f{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{5B}{\isacharbrackleft}}z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline

val\ SOME\ f\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{3D}{\isacharequal}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isamarkupsubsection{partial fraction decomposition%

}

\isamarkuptrue%

%

\isamarkupsubsubsection{solution of the equation%

}

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ SOME\ solutions\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{3D}{\isacharequal}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline

atomty\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isamarkupsubsubsection{get solutions out of list%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

in isac's CTP-based programming language: let$ $s_1 = NTH 1$ solutions; $s_2 = NTH 2...$%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}list{\isaliteral{2E}{\isachardot}}Cons{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{28}{\isacharparenleft}}Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}list{\isaliteral{2E}{\isachardot}}Cons{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\isanewline

\ \ \ \ \ \ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}\ {\isaliteral{24}{\isachardollar}}\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}list{\isaliteral{2E}{\isachardot}}Nil{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}Solutions\ as\ Denominator\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Denominator{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ z\ {\isaliteral{2D}{\isacharminus}}\ Zeropoint{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ Denominator{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{2D}{\isacharminus}}Zeropoint{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

val\ xx\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}minus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}minus{\isaliteral{22}{\isachardoublequote}}\ xx{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ xx\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}minus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}minus{\isaliteral{22}{\isachardoublequote}}\ xx{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

for the programming language a function 

  collecting all the above manipulations is helpful%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

fun\ mk{\isaliteral{5F}{\isacharunderscore}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}\ T\ {\isaliteral{3D}{\isacharequal}}\ Free{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ T{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}TODO\ DELETE\ WITH\ numbers{\isaliteral{5F}{\isacharunderscore}}to{\isaliteral{5F}{\isacharunderscore}}string{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

fun\ flip{\isaliteral{5F}{\isacharunderscore}}sign\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}TODO\ improve\ for\ use\ in\ factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ etc{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ let\ val\ minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ t\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ type{\isaliteral{5F}{\isacharunderscore}}of\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ mk{\isaliteral{5F}{\isacharunderscore}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}\isanewline

\ \ in\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}minus{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline

fun\ fac{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}sol\ s\ {\isaliteral{3D}{\isacharequal}}\isanewline

\ \ let\ val\ {\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{2C}{\isacharcomma}}\ rhs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}eq\ s\isanewline

\ \ in\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}lhs{\isaliteral{2C}{\isacharcomma}}\ flip{\isaliteral{5F}{\isacharunderscore}}sign\ rhs{\isaliteral{29}{\isacharparenright}}\ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

e{\isaliteral{5F}{\isacharunderscore}}term\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

fun\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ prod\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline

\ \ \ \ \ \ if\ prod\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}term\ then\ error\ {\isaliteral{22}{\isachardoublequote}}mk{\isaliteral{5F}{\isacharunderscore}}prod\ called\ with\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}\ else\ prod\isanewline

\ \ {\isaliteral{7C}{\isacharbar}}\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ prod\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline

\ \ \ \ \ \ if\ prod\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}term\ then\ t\ else\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}prod{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ {\isaliteral{7C}{\isacharbar}}\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ prod\ {\isaliteral{28}{\isacharparenleft}}t{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ t{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ ts{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline

\ \ \ \ \ \ \ \ if\ prod\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}term\ \isanewline

\ \ \ \ \ \ \ \ then\ \isanewline

\ \ \ \ \ \ \ \ \ \ \ let\ val\ p\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}t{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ t{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \ \ \ \ \ \ \ \ \ in\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ p\ ts\ end\ \isanewline

\ \ \ \ \ \ \ \ else\ \isanewline

\ \ \ \ \ \ \ \ \ \ \ let\ val\ p\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}prod{\isaliteral{2C}{\isacharcomma}}\ t{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \ \ \ \ \ \ \ \ \ in\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ p\ {\isaliteral{28}{\isacharparenleft}}t{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ ts{\isaliteral{29}{\isacharparenright}}\ end\ \isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}probably\ keept\ these\ test\ in\ test{\isaliteral{2F}{\isacharslash}}Tools{\isaliteral{2F}{\isacharslash}}isac{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}mk{\isaliteral{5F}{\isacharunderscore}}prod\ e{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

\isanewline

val\ prod\ {\isaliteral{3D}{\isacharequal}}\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ e{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{5B}{\isacharbrackleft}}str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isadigit{2}}{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline

term{\isadigit{2}}str\ prod\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isadigit{2}}{\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

\isanewline

val\ sol\ {\isaliteral{3D}{\isacharequal}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ sols\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}list\ sol{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ facs\ {\isaliteral{3D}{\isacharequal}}\ map\ fac{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}sol\ sols{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ prod\ {\isaliteral{3D}{\isacharequal}}\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ e{\isaliteral{5F}{\isacharunderscore}}term\ facs{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline

term{\isadigit{2}}str\ prod\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

\isanewline

val\ prod\ {\isaliteral{3D}{\isacharequal}}\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ e{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{5B}{\isacharbrackleft}}str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{3}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline

term{\isadigit{2}}str\ prod\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

\isanewline

fun\ factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ sol\ {\isaliteral{3D}{\isacharequal}}\ \isanewline

\ \ let\ val\ ts\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}dest{\isaliteral{5F}{\isacharunderscore}}list\ sol\isanewline

\ \ in\ mk{\isaliteral{5F}{\isacharunderscore}}prod\ e{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}map\ fac{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}sol\ ts{\isaliteral{29}{\isacharparenright}}\ end{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline

val\ sol\ {\isaliteral{3D}{\isacharequal}}\ str{\isadigit{2}}term\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ fs\ {\isaliteral{3D}{\isacharequal}}\ factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ sol{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ fs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}\isanewline

{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

This function needs to be packed such that it can be evaluated by the Lucas-Interpreter:

  # shift these functions into the related Equation.thy

  #  -- compare steps done with get_denominator above

  # done 02.12.2011 moved to PartialFractions.thy%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

fun\ eval{\isaliteral{5F}{\isacharunderscore}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ {\isaliteral{28}{\isacharparenleft}}thmid{\isaliteral{3A}{\isacharcolon}}string{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5F}{\isacharunderscore}}\isanewline

\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}t\ as\ Const\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Partial{\isaliteral{5F}{\isacharunderscore}}Fractions{\isaliteral{2E}{\isachardot}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{24}{\isachardollar}}\ sol{\isaliteral{29}{\isacharparenright}}\ thy\ {\isaliteral{3D}{\isacharequal}}\isanewline

\ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}let\ val\ prod\ {\isaliteral{3D}{\isacharequal}}\ factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ sol\isanewline

\ \ \ \ \ \ \ \ \ in\ SOME\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}thmid\ thmid\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}\isanewline

\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}Print{\isaliteral{5F}{\isacharunderscore}}Mode{\isaliteral{2E}{\isachardot}}setmp\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}Syntax{\isaliteral{2E}{\isachardot}}string{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}term\ {\isaliteral{28}{\isacharparenleft}}thy{\isadigit{2}}ctxt\ thy{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ prod{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline

\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Trueprop\ {\isaliteral{24}{\isachardollar}}\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}equality\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ prod{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \ \ \ \ \ \ \ end{\isaliteral{29}{\isacharparenright}}\isanewline

\ \ \ \ \ \ \ handle\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ NONE{\isaliteral{29}{\isacharparenright}}\isanewline

\ {\isaliteral{7C}{\isacharbar}}\ eval{\isaliteral{5F}{\isacharunderscore}}factors{\isaliteral{5F}{\isacharunderscore}}from{\isaliteral{5F}{\isacharunderscore}}solution\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ NONE{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\begin{isamarkuptext}%

The tracing output of the calc tree after apllying this function was

24 / factors_from_solution [z = 1/ 2, z = -1 / 4])]  and the next step

 val nxt = ("Empty_Tac", ...): tac'_).

These observations indicate, that the Lucas-Interpreter (LIP) does 

not know how to evaluate factors_from_solution, so there is something 

wrong or missing.

# First we isolate the difficulty in the program as follows:

  :

  "      (L_L::bool list) = (SubProblem (PolyEq'," ^

  "          [abcFormula,degree_2,polynomial,univariate,equation],[no_met])" ^

  "        [BOOL equ, REAL zzz]);              " ^

  "      (facs::real) = factors_from_solution L_L;" ^

  "      (foo::real) = Take facs" ^

  :

and see

  [

  (([], Frm), Problem (Isac, [inverse, Z_Transform, SignalProcessing])),

  (([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),

  (([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),

  (([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),

  (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),

  (([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),

  (([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |

                 z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),

  (([3,2], Res), z = 1 / 2 | z = -1 / 4),

  (([3,3], Res), [z = 1 / 2, z = -1 / 4]),

  (([3,4], Res), [z = 1 / 2, z = -1 / 4]),

  (([3], Res), [z = 1 / 2, z = -1 / 4]),

  (([4], Frm), factors_from_solution [z = 1 / 2, z = -1 / 4])]

in particular that

  (([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),

shows the equation which has been created in the program by

  "      (denom::real) = get_denominator funterm;" ^ (*get_denominator*)

  "      (equ::bool) = (denom = (0::real));" ^

# 'get_denominator' has been evaluated successfully, but not factors_from_solution.

So we stepwise compare with an analogous case, get_denominator 

successfully done above: We know that LIP evaluates expressions in the 

program by use of the "srls", so we

# try to get the original srls

  val {srls, ...} = get_met ["SignalProcessing","Z_Transform","inverse"];

# create 2 good example terms

  val SOME t1 = parseNEW ctxt "get_denominator ((111::real) / 222)";

  val SOME t2 = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";

# rewrite the terms using srls

  rewrite_set_ thy true srls t1;

  rewrite_set_ thy true srls t2;

and we see a difference: t1 gives SOME, t2 gives NONE.

Now we look at the srls:

  val srls = Rls {id="srls_InverseZTransform",

    :

    rules =

      [

        :

        Calc("Rational.get_numerator",

          eval_get_numerator "Rational.get_numerator"),

        Calc("Partial_Fractions.factors_from_solution",

          eval_factors_from_solution "Partial_Fractions.factors_from_solution")

      ],

    :

Here everthing is perfect. So the error can only be in the SML code of eval_factors_from_solution.

We try to check the code with an existing test; since the code is in

  src/Tools/isac/Knowledge/Partial_Fractions.thy

the test should be in

  test/Tools/isac/Knowledge/partial_fractions.sml

-------------------------------------------------------------------------------

After updating the function get_factors_from solution to a new version and 

putting a testcase to Partial_Fractions.sml we tried again to evaluate the

term with the same result.

We opened the test Test_Isac.thy and saw that everything is working fine.

Also we checked that the test partial_fractions.sml is used in Test_Isac.thy 

-->  use "Knowledge/partial_fractions.sml"

and Partial_Fractions.thy is part is part of isac by evaluating

val thy = \hyperlink{theory.Isac}{\mbox{\isa{Isac}}};

after rebuilding isac again it worked%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsubsection{build expression%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}The\ Main\ Denominator\ is\ the\ multiplikation\ of\ the\ partial\ fraction\ denominators{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

val\ denominator{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ SOME\ numerator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

\isanewline

val\ expr{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}numerator{\isaliteral{2C}{\isacharcomma}}\ denominator{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ expr{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

%

\isamarkupsubsubsection{Ansatz - create partial fractions out of our expression%

}

\isamarkuptrue%

%

\isadelimML

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}Context{\isaliteral{2E}{\isachardot}}theory{\isaliteral{5F}{\isacharunderscore}}name\ thy\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A7D}{\isacharverbatimclose}}%

\endisatagML

{\isafoldML}%

%

\isadelimML

%

\endisadelimML

\isanewline

\isanewline

\isacommand{axiomatization}\isamarkupfalse%

\ \isakeyword{where}\isanewline

\ \ ansatz{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}b{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline

\ \ multiply{\isaliteral{5F}{\isacharunderscore}}eq{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n\ \ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2A}{\isacharasterisk}}b{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2F}{\isacharslash}}a\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}b{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \ \isanewline

%

\isadelimML

\isanewline

%

\endisadelimML

%

\isatagML

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}we\ use\ our\ ansatz{\isadigit{2}}\ to\ rewrite\ our\ expression\ and\ get\ an\ equilation\ with\ our\ expression\ on\ the\ left\ and\ the\ partial\ fractions\ of\ it\ on\ the\ right\ side{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

val\ SOME\ {\isaliteral{28}{\isacharparenleft}}t{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ %

\isaantiq

theory\ Isac{}%

\endisaantiq

\ e{\isaliteral{5F}{\isacharunderscore}}rew{\isaliteral{5F}{\isacharunderscore}}ord\ e{\isaliteral{5F}{\isacharunderscore}}rls\ false\ %

\isaantiq

thm\ ansatz{\isadigit{2}}{}%

\endisaantiq

\ expr{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ t{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ atomty\ t{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

val\ eq{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{28}{\isacharparenleft}}expr{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ t{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ eq{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}eliminate\ the\ demoninators\ by\ multiplying\ the\ left\ and\ the\ right\ side\ with\ the\ main\ denominator{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}\ %

\isaantiq

theory\ Isac{}%

\endisaantiq

\ e{\isaliteral{5F}{\isacharunderscore}}rew{\isaliteral{5F}{\isacharunderscore}}ord\ e{\isaliteral{5F}{\isacharunderscore}}rls\ false\ %

\isaantiq

thm\ multiply{\isaliteral{5F}{\isacharunderscore}}eq{\isadigit{2}}{}%

\endisaantiq

\ eq{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ eq{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}simplificatoin{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

val\ SOME\ {\isaliteral{28}{\isacharparenleft}}eq{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rewrite{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{5F}{\isacharunderscore}}\ %

\isaantiq

theory\ Isac{}%

\endisaantiq

\ false\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ eq{\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline

term{\isadigit{2}}str\ eq{\isadigit{3}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{3F}{\isacharquery}}A\ {\isaliteral{3F}{\isacharquery}}B\ not\ simplified{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline

{\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline

\isacommand{ML}\isamarkupfalse%

\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline

val\ SOME\ fract{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\isanewline

\ \ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ B\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}A\ B\ {\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline