equal
deleted
inserted
replaced
39 into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of |
39 into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of |
40 \isa{ordrel}:% |
40 \isa{ordrel}:% |
41 \end{isamarkuptext}% |
41 \end{isamarkuptext}% |
42 \isamarkuptrue% |
42 \isamarkuptrue% |
43 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel\isamarkupfalse% |
43 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel\isamarkupfalse% |
44 % |
|
45 \begin{isamarkuptxt}% |
|
46 \noindent |
|
47 Command \isacommand{instance} actually starts a proof, namely that |
|
48 \isa{bool} satisfies all axioms of \isa{ordrel}. |
|
49 There are none, but we still need to finish that proof, which we do |
|
50 by invoking the \methdx{intro_classes} method:% |
|
51 \end{isamarkuptxt}% |
|
52 \isamarkuptrue% |
44 \isamarkuptrue% |
53 \isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse% |
45 \isamarkupfalse% |
54 % |
46 % |
55 \begin{isamarkuptext}% |
47 \begin{isamarkuptext}% |
56 \noindent |
48 \noindent |
57 More interesting \isacommand{instance} proofs will arise below |
49 More interesting \isacommand{instance} proofs will arise below |
58 in the context of proper axiomatic type classes. |
50 in the context of proper axiomatic type classes. |
70 Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable:% |
62 Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable:% |
71 \end{isamarkuptext}% |
63 \end{isamarkuptext}% |
72 \isamarkuptrue% |
64 \isamarkuptrue% |
73 \isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequote}\isanewline |
65 \isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequote}\isanewline |
74 \isamarkupfalse% |
66 \isamarkupfalse% |
75 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
67 \isamarkupfalse% |
76 % |
68 % |
77 \begin{isamarkuptext}% |
69 \begin{isamarkuptext}% |
78 \noindent |
70 \noindent |
79 At this point, \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed. |
71 At this point, \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed. |
80 To make it well-typed, |
72 To make it well-typed, |