|
paulson@10365
|
1 |
%
|
|
paulson@11187
|
2 |
\begin{isabellebody}%
|
|
paulson@11187
|
3 |
\def\isabellecontext{Advanced}%
|
|
paulson@10365
|
4 |
\isanewline
|
|
paulson@11187
|
5 |
\isacommand{theory}\ Advanced\ {\isacharequal}\ Even{\isacharcolon}\isanewline
|
|
paulson@10469
|
6 |
\isanewline
|
|
paulson@10469
|
7 |
\isanewline
|
|
wenzelm@11866
|
8 |
\isamarkupfalse%
|
|
paulson@11187
|
9 |
\isacommand{datatype}\ {\isacharprime}f\ gterm\ {\isacharequal}\ Apply\ {\isacharprime}f\ {\isachardoublequote}{\isacharprime}f\ gterm\ list{\isachardoublequote}\isanewline
|
|
paulson@10469
|
10 |
\isanewline
|
|
wenzelm@11866
|
11 |
\isamarkupfalse%
|
|
paulson@11187
|
12 |
\isacommand{datatype}\ integer{\isacharunderscore}op\ {\isacharequal}\ Number\ int\ {\isacharbar}\ UnaryMinus\ {\isacharbar}\ Plus\isanewline
|
|
paulson@10469
|
13 |
\isanewline
|
|
wenzelm@11866
|
14 |
\isamarkupfalse%
|
|
paulson@11187
|
15 |
\isacommand{consts}\ gterms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
16 |
\isamarkupfalse%
|
|
paulson@11187
|
17 |
\isacommand{inductive}\ {\isachardoublequote}gterms\ F{\isachardoublequote}\isanewline
|
|
paulson@10469
|
18 |
\isakeyword{intros}\isanewline
|
|
paulson@11187
|
19 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
|
|
paulson@11187
|
20 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ gterms\ F{\isachardoublequote}\isanewline
|
|
paulson@10469
|
21 |
\isanewline
|
|
wenzelm@11866
|
22 |
\isamarkupfalse%
|
|
paulson@11187
|
23 |
\isacommand{lemma}\ gterms{\isacharunderscore}mono{\isacharcolon}\ {\isachardoublequote}F{\isasymsubseteq}G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
24 |
\isamarkupfalse%
|
|
paulson@10469
|
25 |
\isacommand{apply}\ clarify\isanewline
|
|
wenzelm@11866
|
26 |
\isamarkupfalse%
|
|
wenzelm@11866
|
27 |
\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isamarkupfalse%
|
|
wenzelm@11866
|
28 |
%
|
|
paulson@11187
|
29 |
\begin{isamarkuptxt}%
|
|
paulson@11187
|
30 |
\begin{isabelle}%
|
|
paulson@11187
|
31 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
|
|
paulson@11187
|
32 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ t\ {\isasymin}\ gterms\ G{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
|
|
paulson@11187
|
33 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G%
|
|
paulson@11187
|
34 |
\end{isabelle}%
|
|
paulson@11187
|
35 |
\end{isamarkuptxt}%
|
|
wenzelm@11866
|
36 |
\isamarkuptrue%
|
|
paulson@11187
|
37 |
\isacommand{apply}\ blast\isanewline
|
|
wenzelm@11866
|
38 |
\isamarkupfalse%
|
|
wenzelm@11866
|
39 |
\isacommand{done}\isamarkupfalse%
|
|
wenzelm@11866
|
40 |
%
|
|
paulson@11187
|
41 |
\begin{isamarkuptext}%
|
|
paulson@11187
|
42 |
\begin{isabelle}%
|
|
paulson@11187
|
43 |
\ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
|
|
paulson@11173
|
44 |
\end{isabelle}
|
|
paulson@11173
|
45 |
\rulename{even.cases}
|
|
paulson@10469
|
46 |
|
|
paulson@10469
|
47 |
Just as a demo I include
|
|
paulson@10469
|
48 |
the two forms that Markus has made available. First the one for binding the
|
|
paulson@10469
|
49 |
result to a name%
|
|
paulson@11187
|
50 |
\end{isamarkuptext}%
|
|
wenzelm@11866
|
51 |
\isamarkuptrue%
|
|
paulson@11187
|
52 |
\isacommand{inductive{\isacharunderscore}cases}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline
|
|
paulson@11187
|
53 |
\ \ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}\isanewline
|
|
paulson@10365
|
54 |
\isanewline
|
|
wenzelm@11866
|
55 |
\isamarkupfalse%
|
|
wenzelm@11866
|
56 |
\isacommand{thm}\ Suc{\isacharunderscore}Suc{\isacharunderscore}cases\isamarkupfalse%
|
|
wenzelm@11866
|
57 |
%
|
|
paulson@11187
|
58 |
\begin{isamarkuptext}%
|
|
paulson@11187
|
59 |
\begin{isabelle}%
|
|
paulson@11187
|
60 |
\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
|
|
paulson@11187
|
61 |
\end{isabelle}
|
|
paulson@11173
|
62 |
\rulename{Suc_Suc_cases}
|
|
paulson@10469
|
63 |
|
|
wenzelm@10457
|
64 |
and now the one for local usage:%
|
|
paulson@11187
|
65 |
\end{isamarkuptext}%
|
|
wenzelm@11866
|
66 |
\isamarkuptrue%
|
|
paulson@11187
|
67 |
\isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
68 |
\isamarkupfalse%
|
|
paulson@11187
|
69 |
\isacommand{apply}\ {\isacharparenleft}ind{\isacharunderscore}cases\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}{\isacharparenright}\isanewline
|
|
wenzelm@11866
|
70 |
\isamarkupfalse%
|
|
paulson@10469
|
71 |
\isacommand{oops}\isanewline
|
|
paulson@10469
|
72 |
\isanewline
|
|
wenzelm@11866
|
73 |
\isamarkupfalse%
|
|
wenzelm@11866
|
74 |
\isacommand{inductive{\isacharunderscore}cases}\ gterm{\isacharunderscore}Apply{\isacharunderscore}elim\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isachardoublequote}\isamarkupfalse%
|
|
wenzelm@11866
|
75 |
%
|
|
paulson@11187
|
76 |
\begin{isamarkuptext}%
|
|
paulson@10469
|
77 |
this is what we get:
|
|
wenzelm@10457
|
78 |
|
|
paulson@11187
|
79 |
\begin{isabelle}%
|
|
paulson@11187
|
80 |
\ \ \ \ \ {\isasymlbrakk}Apply\ f\ args\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
|
|
paulson@10469
|
81 |
\end{isabelle}
|
|
paulson@11187
|
82 |
\rulename{gterm_Apply_elim}%
|
|
paulson@11187
|
83 |
\end{isamarkuptext}%
|
|
wenzelm@11866
|
84 |
\isamarkuptrue%
|
|
paulson@11187
|
85 |
\isacommand{lemma}\ gterms{\isacharunderscore}IntI\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline
|
|
paulson@11187
|
86 |
\ \ \ \ \ {\isachardoublequote}t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
87 |
\isamarkupfalse%
|
|
wenzelm@11866
|
88 |
\isacommand{apply}\ {\isacharparenleft}erule\ gterms{\isachardot}induct{\isacharparenright}\isamarkupfalse%
|
|
wenzelm@11866
|
89 |
%
|
|
paulson@11187
|
90 |
\begin{isamarkuptxt}%
|
|
paulson@11187
|
91 |
\begin{isabelle}%
|
|
paulson@11187
|
92 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline
|
|
paulson@11187
|
93 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
|
|
paulson@11187
|
94 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
|
|
paulson@14379
|
95 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
|
|
paulson@11187
|
96 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline
|
|
paulson@11187
|
97 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}%
|
|
paulson@11187
|
98 |
\end{isabelle}%
|
|
paulson@11187
|
99 |
\end{isamarkuptxt}%
|
|
wenzelm@11866
|
100 |
\isamarkuptrue%
|
|
paulson@11187
|
101 |
\isacommand{apply}\ blast\isanewline
|
|
wenzelm@11866
|
102 |
\isamarkupfalse%
|
|
wenzelm@11866
|
103 |
\isacommand{done}\isamarkupfalse%
|
|
wenzelm@11866
|
104 |
%
|
|
paulson@11187
|
105 |
\begin{isamarkuptext}%
|
|
paulson@11187
|
106 |
\begin{isabelle}%
|
|
paulson@11187
|
107 |
\ \ \ \ \ mono\ f\ {\isasymLongrightarrow}\ f\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isasymsubseteq}\ f\ A\ {\isasyminter}\ f\ B%
|
|
paulson@11173
|
108 |
\end{isabelle}
|
|
paulson@11187
|
109 |
\rulename{mono_Int}%
|
|
paulson@11187
|
110 |
\end{isamarkuptext}%
|
|
wenzelm@11866
|
111 |
\isamarkuptrue%
|
|
paulson@11187
|
112 |
\isacommand{lemma}\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
|
|
paulson@11187
|
113 |
\ \ \ \ \ {\isachardoublequote}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
114 |
\isamarkupfalse%
|
|
paulson@12156
|
115 |
\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isamarkupfalse%
|
|
paulson@12156
|
116 |
%
|
|
paulson@12156
|
117 |
\begin{isamarkuptext}%
|
|
paulson@12156
|
118 |
the following declaration isn't actually used%
|
|
paulson@12156
|
119 |
\end{isamarkuptext}%
|
|
paulson@12156
|
120 |
\isamarkuptrue%
|
|
paulson@11187
|
121 |
\isacommand{consts}\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
122 |
\isamarkupfalse%
|
|
paulson@10469
|
123 |
\isacommand{primrec}\isanewline
|
|
wenzelm@11708
|
124 |
{\isachardoublequote}integer{\isacharunderscore}arity\ {\isacharparenleft}Number\ n{\isacharparenright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
|
|
wenzelm@11708
|
125 |
{\isachardoublequote}integer{\isacharunderscore}arity\ UnaryMinus\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
|
|
wenzelm@11708
|
126 |
{\isachardoublequote}integer{\isacharunderscore}arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{2}}{\isachardoublequote}\isanewline
|
|
paulson@10469
|
127 |
\isanewline
|
|
wenzelm@11866
|
128 |
\isamarkupfalse%
|
|
paulson@11187
|
129 |
\isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
130 |
\isamarkupfalse%
|
|
paulson@11187
|
131 |
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
|
|
paulson@10365
|
132 |
\isakeyword{intros}\isanewline
|
|
paulson@11187
|
133 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharsemicolon}\ \ \isanewline
|
|
paulson@11187
|
134 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
|
|
paulson@11187
|
135 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
|
|
paulson@10365
|
136 |
\isanewline
|
|
paulson@10469
|
137 |
\isanewline
|
|
wenzelm@11866
|
138 |
\isamarkupfalse%
|
|
paulson@11187
|
139 |
\isacommand{consts}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
140 |
\isamarkupfalse%
|
|
paulson@11187
|
141 |
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
|
|
paulson@10365
|
142 |
\isakeyword{intros}\isanewline
|
|
paulson@11187
|
143 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}{\isacharsemicolon}\ \ \isanewline
|
|
paulson@11187
|
144 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
|
|
paulson@11187
|
145 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
|
|
paulson@11187
|
146 |
\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline
|
|
paulson@10365
|
147 |
\isanewline
|
|
wenzelm@11866
|
148 |
\isamarkupfalse%
|
|
paulson@11187
|
149 |
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
150 |
\isamarkupfalse%
|
|
wenzelm@11866
|
151 |
\isacommand{apply}\ clarify\isamarkupfalse%
|
|
wenzelm@11866
|
152 |
%
|
|
paulson@11187
|
153 |
\begin{isamarkuptxt}%
|
|
paulson@10878
|
154 |
The situation after clarify
|
|
paulson@11187
|
155 |
\begin{isabelle}%
|
|
paulson@11187
|
156 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymLongrightarrow}\isanewline
|
|
paulson@11187
|
157 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
|
|
paulson@11187
|
158 |
\end{isabelle}%
|
|
paulson@11187
|
159 |
\end{isamarkuptxt}%
|
|
wenzelm@11866
|
160 |
\isamarkuptrue%
|
|
wenzelm@11866
|
161 |
\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isamarkupfalse%
|
|
wenzelm@11866
|
162 |
%
|
|
paulson@11187
|
163 |
\begin{isamarkuptxt}%
|
|
paulson@10878
|
164 |
note the induction hypothesis!
|
|
paulson@11187
|
165 |
\begin{isabelle}%
|
|
paulson@11187
|
166 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
|
|
paulson@11187
|
167 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
|
|
paulson@11187
|
168 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\isanewline
|
|
paulson@11187
|
169 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
|
|
paulson@14379
|
170 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
|
|
paulson@11187
|
171 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity%
|
|
paulson@11187
|
172 |
\end{isabelle}%
|
|
paulson@11187
|
173 |
\end{isamarkuptxt}%
|
|
wenzelm@11866
|
174 |
\isamarkuptrue%
|
|
paulson@10878
|
175 |
\isacommand{apply}\ auto\isanewline
|
|
wenzelm@11866
|
176 |
\isamarkupfalse%
|
|
paulson@10878
|
177 |
\isacommand{done}\isanewline
|
|
paulson@10878
|
178 |
\isanewline
|
|
paulson@10878
|
179 |
\isanewline
|
|
paulson@10878
|
180 |
\isanewline
|
|
wenzelm@11866
|
181 |
\isamarkupfalse%
|
|
paulson@11187
|
182 |
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
183 |
\isamarkupfalse%
|
|
wenzelm@11866
|
184 |
\isacommand{apply}\ clarify\isamarkupfalse%
|
|
wenzelm@11866
|
185 |
%
|
|
paulson@11187
|
186 |
\begin{isamarkuptxt}%
|
|
paulson@10878
|
187 |
The situation after clarify
|
|
paulson@11187
|
188 |
\begin{isabelle}%
|
|
paulson@11187
|
189 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymLongrightarrow}\isanewline
|
|
paulson@11187
|
190 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
|
|
paulson@11187
|
191 |
\end{isabelle}%
|
|
paulson@11187
|
192 |
\end{isamarkuptxt}%
|
|
wenzelm@11866
|
193 |
\isamarkuptrue%
|
|
wenzelm@11866
|
194 |
\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isamarkupfalse%
|
|
wenzelm@11866
|
195 |
%
|
|
paulson@11187
|
196 |
\begin{isamarkuptxt}%
|
|
paulson@10878
|
197 |
note the induction hypothesis!
|
|
paulson@11187
|
198 |
\begin{isabelle}%
|
|
paulson@11187
|
199 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
|
|
paulson@11187
|
200 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline
|
|
paulson@11187
|
201 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline
|
|
paulson@11187
|
202 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline
|
|
paulson@11187
|
203 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline
|
|
paulson@14379
|
204 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
|
|
paulson@11187
|
205 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity%
|
|
paulson@11187
|
206 |
\end{isabelle}%
|
|
paulson@11187
|
207 |
\end{isamarkuptxt}%
|
|
wenzelm@11866
|
208 |
\isamarkuptrue%
|
|
paulson@10469
|
209 |
\isacommand{apply}\ auto\isanewline
|
|
wenzelm@11866
|
210 |
\isamarkupfalse%
|
|
wenzelm@11866
|
211 |
\isacommand{done}\isamarkupfalse%
|
|
wenzelm@11866
|
212 |
%
|
|
paulson@11187
|
213 |
\begin{isamarkuptext}%
|
|
paulson@11187
|
214 |
\begin{isabelle}%
|
|
paulson@11187
|
215 |
\ \ \ \ \ lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B%
|
|
paulson@11187
|
216 |
\end{isabelle}%
|
|
paulson@11187
|
217 |
\end{isamarkuptext}%
|
|
wenzelm@11866
|
218 |
\isamarkuptrue%
|
|
paulson@10469
|
219 |
%
|
|
paulson@11187
|
220 |
\begin{isamarkuptext}%
|
|
paulson@10469
|
221 |
the rest isn't used: too complicated. OK for an exercise though.%
|
|
paulson@11187
|
222 |
\end{isamarkuptext}%
|
|
wenzelm@11866
|
223 |
\isamarkuptrue%
|
|
paulson@11187
|
224 |
\isacommand{consts}\ integer{\isacharunderscore}signature\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}integer{\isacharunderscore}op\ {\isacharasterisk}\ {\isacharparenleft}unit\ list\ {\isacharasterisk}\ unit{\isacharparenright}{\isacharparenright}\ set{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
225 |
\isamarkupfalse%
|
|
paulson@11187
|
226 |
\isacommand{inductive}\ {\isachardoublequote}integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
|
|
paulson@10469
|
227 |
\isakeyword{intros}\isanewline
|
|
paulson@11187
|
228 |
Number{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isacharparenleft}Number\ n{\isacharcomma}\ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
|
|
paulson@11187
|
229 |
UnaryMinus{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}UnaryMinus{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
|
|
paulson@11187
|
230 |
Plus{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}Plus{\isacharcomma}\ \ \ \ \ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharcomma}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequote}\isanewline
|
|
paulson@10469
|
231 |
\isanewline
|
|
paulson@10469
|
232 |
\isanewline
|
|
wenzelm@11866
|
233 |
\isamarkupfalse%
|
|
paulson@11187
|
234 |
\isacommand{consts}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
235 |
\isamarkupfalse%
|
|
paulson@11187
|
236 |
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
|
|
paulson@10469
|
237 |
\isakeyword{intros}\isanewline
|
|
paulson@11187
|
238 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline
|
|
paulson@11187
|
239 |
\ \ \ \ {\isachardoublequote}{\isasymlbrakk}{\isasymforall}pair\ {\isasymin}\ set\ args{\isachardot}\ pair\ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isacharsemicolon}\ \isanewline
|
|
paulson@11187
|
240 |
\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline
|
|
paulson@11187
|
241 |
\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline
|
|
paulson@11187
|
242 |
\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
|
|
paulson@10469
|
243 |
\isanewline
|
|
wenzelm@11866
|
244 |
\isamarkupfalse%
|
|
paulson@11187
|
245 |
\isacommand{consts}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
246 |
\isamarkupfalse%
|
|
paulson@11187
|
247 |
\isacommand{inductive}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
|
|
paulson@10469
|
248 |
\isakeyword{intros}\isanewline
|
|
paulson@11187
|
249 |
step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline
|
|
paulson@11187
|
250 |
\ \ \ \ {\isachardoublequote}{\isasymlbrakk}args\ {\isasymin}\ lists{\isacharparenleft}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isacharparenright}{\isacharsemicolon}\ \isanewline
|
|
paulson@11187
|
251 |
\ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline
|
|
paulson@11187
|
252 |
\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline
|
|
paulson@11187
|
253 |
\ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
|
|
paulson@11187
|
254 |
\isakeyword{monos}\ lists{\isacharunderscore}mono\isanewline
|
|
paulson@10469
|
255 |
\isanewline
|
|
paulson@10469
|
256 |
\isanewline
|
|
wenzelm@11866
|
257 |
\isamarkupfalse%
|
|
paulson@11187
|
258 |
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
259 |
\isamarkupfalse%
|
|
paulson@10469
|
260 |
\isacommand{apply}\ clarify\isanewline
|
|
wenzelm@11866
|
261 |
\isamarkupfalse%
|
|
paulson@11187
|
262 |
\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isachardot}induct{\isacharparenright}\isanewline
|
|
wenzelm@11866
|
263 |
\isamarkupfalse%
|
|
paulson@10365
|
264 |
\isacommand{apply}\ auto\isanewline
|
|
wenzelm@11866
|
265 |
\isamarkupfalse%
|
|
paulson@10365
|
266 |
\isacommand{done}\isanewline
|
|
paulson@10365
|
267 |
\isanewline
|
|
wenzelm@11866
|
268 |
\isamarkupfalse%
|
|
paulson@11187
|
269 |
\isacommand{lemma}\ {\isachardoublequote}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig\ {\isasymsubseteq}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequote}\isanewline
|
|
wenzelm@11866
|
270 |
\isamarkupfalse%
|
|
paulson@10365
|
271 |
\isacommand{apply}\ clarify\isanewline
|
|
wenzelm@11866
|
272 |
\isamarkupfalse%
|
|
paulson@11187
|
273 |
\isacommand{apply}\ {\isacharparenleft}erule\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}{\isachardot}induct{\isacharparenright}\isanewline
|
|
wenzelm@11866
|
274 |
\isamarkupfalse%
|
|
paulson@10365
|
275 |
\isacommand{apply}\ auto\isanewline
|
|
wenzelm@11866
|
276 |
\isamarkupfalse%
|
|
paulson@10365
|
277 |
\isacommand{done}\isanewline
|
|
paulson@10365
|
278 |
\isanewline
|
|
paulson@10469
|
279 |
\isanewline
|
|
wenzelm@11866
|
280 |
\isamarkupfalse%
|
|
paulson@10365
|
281 |
\isacommand{end}\isanewline
|
|
paulson@10365
|
282 |
\isanewline
|
|
wenzelm@11866
|
283 |
\isamarkupfalse%
|
|
paulson@11187
|
284 |
\end{isabellebody}%
|
|
paulson@10365
|
285 |
%%% Local Variables:
|
|
paulson@10365
|
286 |
%%% mode: latex
|
|
paulson@10365
|
287 |
%%% TeX-master: "root"
|
|
paulson@10365
|
288 |
%%% End:
|