made sure that " is shown in tutorial text
authornipkow
Tue Apr 03 08:55:06 2012 +0200 (2012-04-03)
changeset 4730656d72c923281
parent 47305 ce898681f700
child 47307 5e5ca36692b3
child 47433 07f4bf913230
made sure that " is shown in tutorial text
doc-src/ProgProve/Makefile
doc-src/ProgProve/Thys/Bool_nat_list.thy
doc-src/ProgProve/Thys/Isar.thy
doc-src/ProgProve/Thys/Logic.thy
doc-src/ProgProve/Thys/Types_and_funs.thy
doc-src/ProgProve/Thys/document/Bool_nat_list.tex
doc-src/ProgProve/Thys/document/Isar.tex
doc-src/ProgProve/Thys/document/Logic.tex
doc-src/ProgProve/Thys/document/Types_and_funs.tex
     1.1 --- a/doc-src/ProgProve/Makefile	Mon Apr 02 21:26:46 2012 +0100
     1.2 +++ b/doc-src/ProgProve/Makefile	Tue Apr 03 08:55:06 2012 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  NAME = prog-prove
     1.5  
     1.6  FILES = prog-prove.tex prog-prove.bib Thys/document/*.tex prelude.tex \
     1.7 -  svmono.cls mathpartir.sty isabelle.sty isabellesym.sty
     1.8 +  svmono.cls mathpartir.sty isabelle.sty isabellesym.sty Thys/MyList.thy
     1.9  
    1.10  dvi: $(NAME).dvi
    1.11  
     2.1 --- a/doc-src/ProgProve/Thys/Bool_nat_list.thy	Mon Apr 02 21:26:46 2012 +0100
     2.2 +++ b/doc-src/ProgProve/Thys/Bool_nat_list.thy	Tue Apr 03 08:55:06 2012 +0200
     2.3 @@ -387,10 +387,11 @@
     2.4  @{text"length :: 'a list \<Rightarrow> nat"} (with the obvious definition),
     2.5  and the map function that applies a function to all elements of a list:
     2.6  \begin{isabelle}
     2.7 -\isacom{fun} @{text "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\
     2.8 -@{thm map.simps(1)} @{text"|"}\\
     2.9 -@{thm map.simps(2)}
    2.10 +\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\
    2.11 +@{text"\""}@{thm map.simps(1)}@{text"\" |"}\\
    2.12 +@{text"\""}@{thm map.simps(2)}@{text"\""}
    2.13  \end{isabelle}
    2.14 +\sem
    2.15  Also useful are the \concept{head} of a list, its first element,
    2.16  and the \concept{tail}, the rest of the list:
    2.17  \begin{isabelle}
    2.18 @@ -405,6 +406,8 @@
    2.19  Note that since HOL is a logic of total functions, @{term"hd []"} is defined,
    2.20  but we do now know what the result is. That is, @{term"hd []"} is not undefined
    2.21  but underdefined.
    2.22 +\endsem
    2.23 +%
    2.24  *}
    2.25  (*<*)
    2.26  end
     3.1 --- a/doc-src/ProgProve/Thys/Isar.thy	Mon Apr 02 21:26:46 2012 +0100
     3.2 +++ b/doc-src/ProgProve/Thys/Isar.thy	Tue Apr 03 08:55:06 2012 +0200
     3.3 @@ -178,7 +178,7 @@
     3.4  \subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
     3.5  
     3.6  Lemmas can also be stated in a more structured fashion. To demonstrate this
     3.7 -feature with Cantor's theorem, we rephrase \noquotes{@{prop[source]"\<not> surj f"}}
     3.8 +feature with Cantor's theorem, we rephrase @{prop"\<not> surj f"}
     3.9  a little:
    3.10  *}
    3.11  
    3.12 @@ -190,7 +190,8 @@
    3.13  txt{* The optional \isacom{fixes} part allows you to state the types of
    3.14  variables up front rather than by decorating one of their occurrences in the
    3.15  formula with a type constraint. The key advantage of the structured format is
    3.16 -the \isacom{assumes} part that allows you to name each assumption. The
    3.17 +the \isacom{assumes} part that allows you to name each assumption; multiple
    3.18 +assumptions can be separated by \isacom{and}. The
    3.19  \isacom{shows} part gives the goal. The actual theorem that will come out of
    3.20  the proof is @{prop"surj f \<Longrightarrow> False"}, but during the proof the assumption
    3.21  @{prop"surj f"} is available under the name @{text s} like any other fact.
    3.22 @@ -393,7 +394,8 @@
    3.23  
    3.24  text_raw{*
    3.25  \begin{isamarkuptext}%
    3.26 -How to prove set equality and subset relationship:
    3.27 +
    3.28 +Finally, how to prove set equality and subset relationship:
    3.29  \end{isamarkuptext}%
    3.30  \begin{tabular}{@ {}ll@ {}}
    3.31  \begin{minipage}[t]{.4\textwidth}
    3.32 @@ -544,7 +546,7 @@
    3.33  
    3.34  \subsection{Raw proof blocks}
    3.35  
    3.36 -Sometimes one would like to prove some lemma locally with in a proof.
    3.37 +Sometimes one would like to prove some lemma locally within a proof.
    3.38  A lemma that shares the current context of assumptions but that
    3.39  has its own assumptions and is generalised over its locally fixed
    3.40  variables at the end. This is what a \concept{raw proof block} does:
    3.41 @@ -745,7 +747,7 @@
    3.42  \begin{quote}
    3.43  \isacom{fix} @{text n}\\
    3.44  \isacom{assume} @{text"Suc:"}
    3.45 -  \begin{tabular}[t]{l}@{text"A(n) \<Longrightarrow> P(n)"}\\@{text"A(Suc n)"}\end{tabular}\\
    3.46 +  \begin{tabular}[t]{l}@{text"\"A(n) \<Longrightarrow> P(n)\""}\\@{text"\"A(Suc n)\""}\end{tabular}\\
    3.47  \isacom{let} @{text"?case = \"P(Suc n)\""}
    3.48  \end{quote}
    3.49  The list of assumptions @{text Suc} is actually subdivided
    3.50 @@ -812,8 +814,8 @@
    3.51  ~\\
    3.52  \isacom{fix} @{text n}\\
    3.53  \isacom{assume} @{text"evSS:"}
    3.54 -  \begin{tabular}[t]{l} @{text"ev n"}\\@{text"even n"}\end{tabular}\\
    3.55 -\isacom{let} @{text"?case = even(Suc(Suc n))"}\\
    3.56 +  \begin{tabular}[t]{l} @{text"\"ev n\""}\\@{text"\"even n\""}\end{tabular}\\
    3.57 +\isacom{let} @{text"?case = \"even(Suc(Suc n))\""}\\
    3.58  \end{minipage}
    3.59  \end{tabular}
    3.60  \medskip
     4.1 --- a/doc-src/ProgProve/Thys/Logic.thy	Mon Apr 02 21:26:46 2012 +0100
     4.2 +++ b/doc-src/ProgProve/Thys/Logic.thy	Tue Apr 03 08:55:06 2012 +0200
     4.3 @@ -438,7 +438,7 @@
     4.4  inductive ev :: "nat \<Rightarrow> bool" where
     4.5  ev0:    "ev 0" |
     4.6  evSS:  (*<*)"ev n \<Longrightarrow> ev (Suc(Suc n))"(*>*)
     4.7 -text_raw{* @{prop"ev n \<Longrightarrow> ev (n + 2)"} *}
     4.8 +text_raw{* @{prop[source]"ev n \<Longrightarrow> ev (n + 2)"} *}
     4.9  
    4.10  text{* To get used to inductive definitions, we will first prove a few
    4.11  properties of @{const ev} informally before we descend to the Isabelle level.
     5.1 --- a/doc-src/ProgProve/Thys/Types_and_funs.thy	Mon Apr 02 21:26:46 2012 +0100
     5.2 +++ b/doc-src/ProgProve/Thys/Types_and_funs.thy	Tue Apr 03 08:55:06 2012 +0200
     5.3 @@ -55,7 +55,7 @@
     5.4  As an example, consider binary trees:
     5.5  *}
     5.6  
     5.7 -datatype 'a tree = Tip | Node "('a tree)" 'a "('a tree)"
     5.8 +datatype 'a tree = Tip | Node  "'a tree"  'a  "'a tree"
     5.9  
    5.10  text{* with a mirror function: *}
    5.11  
    5.12 @@ -86,8 +86,8 @@
    5.13  done
    5.14  (*>*)
    5.15  fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
    5.16 -"lookup [] x' = None" |
    5.17 -"lookup ((x,y) # ps) x' = (if x = x' then Some y else lookup ps x')"
    5.18 +"lookup [] x = None" |
    5.19 +"lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"
    5.20  
    5.21  text{*
    5.22  Note that @{text"\<tau>\<^isub>1 * \<tau>\<^isub>2"} is the type of pairs, also written @{text"\<tau>\<^isub>1 \<times> \<tau>\<^isub>2"}.
     6.1 --- a/doc-src/ProgProve/Thys/document/Bool_nat_list.tex	Mon Apr 02 21:26:46 2012 +0100
     6.2 +++ b/doc-src/ProgProve/Thys/document/Bool_nat_list.tex	Tue Apr 03 08:55:06 2012 +0200
     6.3 @@ -557,10 +557,11 @@
     6.4  \isa{length\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat} (with the obvious definition),
     6.5  and the map function that applies a function to all elements of a list:
     6.6  \begin{isabelle}
     6.7 -\isacom{fun} \isa{map\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list}\\
     6.8 -\isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} \isa{{\isaliteral{7C}{\isacharbar}}}\\
     6.9 -\isa{map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x\ {\isaliteral{23}{\isacharhash}}\ map\ f\ xs}
    6.10 +\isacom{fun} \isa{map} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list{\isaliteral{22}{\isachardoublequote}}}\\
    6.11 +\isa{{\isaliteral{22}{\isachardoublequote}}}\isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{7C}{\isacharbar}}}\\
    6.12 +\isa{{\isaliteral{22}{\isachardoublequote}}}\isa{map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x\ {\isaliteral{23}{\isacharhash}}\ map\ f\ xs}\isa{{\isaliteral{22}{\isachardoublequote}}}
    6.13  \end{isabelle}
    6.14 +\sem
    6.15  Also useful are the \concept{head} of a list, its first element,
    6.16  and the \concept{tail}, the rest of the list:
    6.17  \begin{isabelle}
    6.18 @@ -574,7 +575,9 @@
    6.19  \end{isabelle}
    6.20  Note that since HOL is a logic of total functions, \isa{hd\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is defined,
    6.21  but we do now know what the result is. That is, \isa{hd\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is not undefined
    6.22 -but underdefined.%
    6.23 +but underdefined.
    6.24 +\endsem
    6.25 +%%
    6.26  \end{isamarkuptext}%
    6.27  \isamarkuptrue%
    6.28  %
     7.1 --- a/doc-src/ProgProve/Thys/document/Isar.tex	Mon Apr 02 21:26:46 2012 +0100
     7.2 +++ b/doc-src/ProgProve/Thys/document/Isar.tex	Tue Apr 03 08:55:06 2012 +0200
     7.3 @@ -269,7 +269,7 @@
     7.4  \subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
     7.5  
     7.6  Lemmas can also be stated in a more structured fashion. To demonstrate this
     7.7 -feature with Cantor's theorem, we rephrase \noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ surj\ f{\isaliteral{22}{\isachardoublequote}}}}
     7.8 +feature with Cantor's theorem, we rephrase \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ surj\ f}
     7.9  a little:%
    7.10  \end{isamarkuptext}%
    7.11  \isamarkuptrue%
    7.12 @@ -288,7 +288,8 @@
    7.13  The optional \isacom{fixes} part allows you to state the types of
    7.14  variables up front rather than by decorating one of their occurrences in the
    7.15  formula with a type constraint. The key advantage of the structured format is
    7.16 -the \isacom{assumes} part that allows you to name each assumption. The
    7.17 +the \isacom{assumes} part that allows you to name each assumption; multiple
    7.18 +assumptions can be separated by \isacom{and}. The
    7.19  \isacom{shows} part gives the goal. The actual theorem that will come out of
    7.20  the proof is \isa{surj\ f\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False}, but during the proof the assumption
    7.21  \isa{surj\ f} is available under the name \isa{s} like any other fact.%
    7.22 @@ -672,7 +673,8 @@
    7.23  \endisadelimproof
    7.24  %
    7.25  \begin{isamarkuptext}%
    7.26 -How to prove set equality and subset relationship:
    7.27 +
    7.28 +Finally, how to prove set equality and subset relationship:
    7.29  \end{isamarkuptext}%
    7.30  \begin{tabular}{@ {}ll@ {}}
    7.31  \begin{minipage}[t]{.4\textwidth}
    7.32 @@ -942,7 +944,7 @@
    7.33  
    7.34  \subsection{Raw proof blocks}
    7.35  
    7.36 -Sometimes one would like to prove some lemma locally with in a proof.
    7.37 +Sometimes one would like to prove some lemma locally within a proof.
    7.38  A lemma that shares the current context of assumptions but that
    7.39  has its own assumptions and is generalised over its locally fixed
    7.40  variables at the end. This is what a \concept{raw proof block} does:
    7.41 @@ -1307,7 +1309,7 @@
    7.42  \begin{quote}
    7.43  \isacom{fix} \isa{n}\\
    7.44  \isacom{assume} \isa{Suc{\isaliteral{3A}{\isacharcolon}}}
    7.45 -  \begin{tabular}[t]{l}\isa{A{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}}\\\isa{A{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}}\end{tabular}\\
    7.46 +  \begin{tabular}[t]{l}\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\end{tabular}\\
    7.47  \isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}P{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
    7.48  \end{quote}
    7.49  The list of assumptions \isa{Suc} is actually subdivided
    7.50 @@ -1399,8 +1401,8 @@
    7.51  ~\\
    7.52  \isacom{fix} \isa{n}\\
    7.53  \isacom{assume} \isa{evSS{\isaliteral{3A}{\isacharcolon}}}
    7.54 -  \begin{tabular}[t]{l} \isa{ev\ n}\\\isa{even\ n}\end{tabular}\\
    7.55 -\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ even{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}\\
    7.56 +  \begin{tabular}[t]{l} \isa{{\isaliteral{22}{\isachardoublequote}}ev\ n{\isaliteral{22}{\isachardoublequote}}}\\\isa{{\isaliteral{22}{\isachardoublequote}}even\ n{\isaliteral{22}{\isachardoublequote}}}\end{tabular}\\
    7.57 +\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}even{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
    7.58  \end{minipage}
    7.59  \end{tabular}
    7.60  \medskip
     8.1 --- a/doc-src/ProgProve/Thys/document/Logic.tex	Mon Apr 02 21:26:46 2012 +0100
     8.2 +++ b/doc-src/ProgProve/Thys/document/Logic.tex	Tue Apr 03 08:55:06 2012 +0200
     8.3 @@ -570,7 +570,7 @@
     8.4  \ ev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
     8.5  ev{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}ev\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
     8.6  evSS{\isaliteral{3A}{\isacharcolon}}\ \ %
     8.7 -\isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}
     8.8 +\isa{{\isaliteral{22}{\isachardoublequote}}ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
     8.9  %
    8.10  \begin{isamarkuptext}%
    8.11  To get used to inductive definitions, we will first prove a few
     9.1 --- a/doc-src/ProgProve/Thys/document/Types_and_funs.tex	Mon Apr 02 21:26:46 2012 +0100
     9.2 +++ b/doc-src/ProgProve/Thys/document/Types_and_funs.tex	Tue Apr 03 08:55:06 2012 +0200
     9.3 @@ -68,7 +68,7 @@
     9.4  \end{isamarkuptext}%
     9.5  \isamarkuptrue%
     9.6  \isacommand{datatype}\isamarkupfalse%
     9.7 -\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Tip\ {\isaliteral{7C}{\isacharbar}}\ Node\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
     9.8 +\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Tip\ {\isaliteral{7C}{\isacharbar}}\ Node\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{27}{\isacharprime}}a\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}%
     9.9  \begin{isamarkuptext}%
    9.10  with a mirror function:%
    9.11  \end{isamarkuptext}%
    9.12 @@ -122,8 +122,8 @@
    9.13  \endisadelimproof
    9.14  \isacommand{fun}\isamarkupfalse%
    9.15  \ lookup\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
    9.16 -{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ None{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
    9.17 -{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ ps{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{27}{\isacharprime}}\ then\ Some\ y\ else\ lookup\ ps\ x{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
    9.18 +{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ None{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
    9.19 +{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ ps{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ a\ {\isaliteral{3D}{\isacharequal}}\ x\ then\ Some\ b\ else\ lookup\ ps\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
    9.20  \begin{isamarkuptext}%
    9.21  Note that \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} is the type of pairs, also written \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.
    9.22