10365
|
1 |
%
|
11173
|
2 |
\begin{isabelle}
|
|
3 |
\def\isabellecontext{Advanced}
|
10365
|
4 |
\isanewline
|
11173
|
5 |
\isacommand{theory}\ Advanced\ =\ Even:\isanewline
|
10469
|
6 |
\isanewline
|
|
7 |
\isanewline
|
11173
|
8 |
\isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list"\isanewline
|
10469
|
9 |
\isanewline
|
11173
|
10 |
\isacommand{datatype}\ integer_op\ =\ Number\ int\ |\ UnaryMinus\ |\ Plus\isanewline
|
10469
|
11 |
\isanewline
|
11173
|
12 |
\isacommand{consts}\ gterms\ ::\ "'f\ set\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
|
|
13 |
\isacommand{inductive}\ "gterms\ F"\isanewline
|
10469
|
14 |
\isakeyword{intros}\isanewline
|
11173
|
15 |
step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ gterms\ F;\ \ f\ \isasymin \ F\isasymrbrakk \isanewline
|
|
16 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ gterms\ F"\isanewline
|
10469
|
17 |
\isanewline
|
11173
|
18 |
\isacommand{lemma}\ gterms_mono:\ "F\isasymsubseteq G\ \isasymLongrightarrow \ gterms\ F\ \isasymsubseteq \ gterms\ G"\isanewline
|
10469
|
19 |
\isacommand{apply}\ clarify\isanewline
|
11173
|
20 |
\isacommand{apply}\ (erule\ gterms.induct)
|
|
21 |
\begin{isamarkuptxt}
|
|
22 |
\begin{isabelle}
|
|
23 |
\ 1.\ \isasymAnd x\ args\ f.\isanewline
|
|
24 |
\isaindent{\ 1.\ \ \ \ }\isasymlbrakk F\ \isasymsubseteq \ G;\ \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F\ \isasymand \ t\ \isasymin \ gterms\ G;\ f\ \isasymin \ F\isasymrbrakk \isanewline
|
|
25 |
\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G%
|
|
26 |
\end{isabelle}
|
|
27 |
\end{isamarkuptxt}
|
10469
|
28 |
\isacommand{apply}\ blast\isanewline
|
11173
|
29 |
\isacommand{done}
|
|
30 |
\begin{isamarkuptext}
|
|
31 |
\begin{isabelle}
|
|
32 |
\ \ \ \ \ \isasymlbrakk a\ \isasymin \ even;\ a\ =\ 0\ \isasymLongrightarrow \ P;\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc\ (Suc\ n);\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
|
|
33 |
\rulename{even.cases}
|
10469
|
34 |
\end{isabelle}
|
|
35 |
|
|
36 |
Just as a demo I include
|
|
37 |
the two forms that Markus has made available. First the one for binding the
|
|
38 |
result to a name%
|
11173
|
39 |
\end{isamarkuptext}
|
|
40 |
\isacommand{inductive_cases}\ Suc_Suc_cases\ [elim!]:\isanewline
|
|
41 |
\ \ "Suc(Suc\ n)\ \isasymin \ even"\isanewline
|
10365
|
42 |
\isanewline
|
11173
|
43 |
\isacommand{thm}\ Suc_Suc_cases%
|
|
44 |
\begin{isamarkuptext}
|
|
45 |
\begin{isabelle}
|
|
46 |
\ \ \ \ \ \isasymlbrakk Suc\ (Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\ \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
|
|
47 |
\rulename{Suc_Suc_cases}
|
10469
|
48 |
\end{isabelle}
|
|
49 |
|
10457
|
50 |
and now the one for local usage:%
|
11173
|
51 |
\end{isamarkuptext}
|
|
52 |
\isacommand{lemma}\ "Suc(Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ P\ n"\isanewline
|
|
53 |
\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")\isanewline
|
10469
|
54 |
\isacommand{oops}\isanewline
|
|
55 |
\isanewline
|
11173
|
56 |
\isacommand{inductive_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\ \isasymin \ gterms\ F"
|
|
57 |
\begin{isamarkuptext}
|
10469
|
58 |
this is what we get:
|
10457
|
59 |
|
11173
|
60 |
\begin{isabelle}
|
|
61 |
\ \ \ \ \ \isasymlbrakk Apply\ f\ args\ \isasymin \ gterms\ F;\ \isasymlbrakk \isasymforall t\isasymin set\ args.\ t\ \isasymin \ gterms\ F;\ f\ \isasymin \ F\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
|
|
62 |
\rulename{gterm_Apply_elim}
|
10469
|
63 |
\end{isabelle}
|
11173
|
64 |
\end{isamarkuptext}
|
|
65 |
\isacommand{lemma}\ gterms_IntI\ [rule_format,\ intro!]:\isanewline
|
|
66 |
\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter G)"\isanewline
|
|
67 |
\isacommand{apply}\ (erule\ gterms.induct)
|
|
68 |
\begin{isamarkuptxt}
|
|
69 |
\begin{isabelle}
|
|
70 |
\ 1.\ \isasymAnd args\ f.\isanewline
|
|
71 |
\isaindent{\ 1.\ \ \ \ }\isasymlbrakk \isasymforall t\isasymin set\ args.\isanewline
|
|
72 |
\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ gterms\ F\ \isasymand \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline
|
|
73 |
\isaindent{\ 1.\ \ \ \ \ \ \ }f\ \isasymin \ F\isasymrbrakk \isanewline
|
|
74 |
\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \isanewline
|
|
75 |
\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G)
|
|
76 |
\end{isabelle}
|
|
77 |
\end{isamarkuptxt}
|
10469
|
78 |
\isacommand{apply}\ blast\isanewline
|
11173
|
79 |
\isacommand{done}
|
|
80 |
\begin{isamarkuptext}
|
|
81 |
\begin{isabelle}
|
|
82 |
\ \ \ \ \ mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \ f\ A\ \isasyminter \ f\ B%
|
|
83 |
\rulename{mono_Int}
|
10469
|
84 |
\end{isabelle}
|
11173
|
85 |
\end{isamarkuptext}
|
|
86 |
\isacommand{lemma}\ gterms_Int_eq\ [simp]:\isanewline
|
|
87 |
\ \ \ \ \ "gterms\ (F\isasyminter G)\ =\ gterms\ F\ \isasyminter \ gterms\ G"\isanewline
|
|
88 |
\isacommand{by}\ (blast\ intro!:\ mono_Int\ monoI\ gterms_mono)\isanewline
|
10469
|
89 |
\isanewline
|
|
90 |
\isanewline
|
11173
|
91 |
\isacommand{consts}\ integer_arity\ ::\ "integer_op\ \isasymRightarrow \ nat"\isanewline
|
10469
|
92 |
\isacommand{primrec}\isanewline
|
11173
|
93 |
"integer_arity\ (Number\ n)\ \ \ \ \ \ \ \ =\ \#0"\isanewline
|
|
94 |
"integer_arity\ UnaryMinus\ \ \ \ \ \ \ \ =\ \#1"\isanewline
|
|
95 |
"integer_arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ =\ \#2"\isanewline
|
10469
|
96 |
\isanewline
|
11173
|
97 |
\isacommand{consts}\ well_formed_gterm\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
|
|
98 |
\isacommand{inductive}\ "well_formed_gterm\ arity"\isanewline
|
10365
|
99 |
\isakeyword{intros}\isanewline
|
11173
|
100 |
step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ well_formed_gterm\ arity;\ \ \isanewline
|
|
101 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
|
|
102 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm\ arity"\isanewline
|
10365
|
103 |
\isanewline
|
|
104 |
\isanewline
|
11173
|
105 |
\isacommand{consts}\ well_formed_gterm'\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
|
|
106 |
\isacommand{inductive}\ "well_formed_gterm'\ arity"\isanewline
|
10365
|
107 |
\isakeyword{intros}\isanewline
|
11173
|
108 |
step[intro!]:\ "\isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity);\ \ \isanewline
|
|
109 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
|
|
110 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm'\ arity"\isanewline
|
|
111 |
\isakeyword{monos}\ lists_mono\isanewline
|
10469
|
112 |
\isanewline
|
11173
|
113 |
\isacommand{lemma}\ "well_formed_gterm\ arity\ \isasymsubseteq \ well_formed_gterm'\ arity"\isanewline
|
10878
|
114 |
\isacommand{apply}\ clarify%
|
11173
|
115 |
\begin{isamarkuptxt}
|
10878
|
116 |
The situation after clarify
|
11173
|
117 |
\begin{isabelle}
|
|
118 |
\ 1.\ \isasymAnd x.\ x\ \isasymin \ well_formed_gterm\ arity\ \isasymLongrightarrow \isanewline
|
|
119 |
\isaindent{\ 1.\ \isasymAnd x.\ }x\ \isasymin \ well_formed_gterm'\ arity%
|
|
120 |
\end{isabelle}
|
|
121 |
\end{isamarkuptxt}
|
|
122 |
\isacommand{apply}\ (erule\ well_formed_gterm.induct)
|
|
123 |
\begin{isamarkuptxt}
|
10878
|
124 |
note the induction hypothesis!
|
11173
|
125 |
\begin{isabelle}
|
|
126 |
\ 1.\ \isasymAnd x\ args\ f.\isanewline
|
|
127 |
\isaindent{\ 1.\ \ \ \ }\isasymlbrakk \isasymforall t\isasymin set\ args.\isanewline
|
|
128 |
\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ well_formed_gterm\ arity\ \isasymand \isanewline
|
|
129 |
\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ well_formed_gterm'\ arity;\isanewline
|
|
130 |
\isaindent{\ 1.\ \ \ \ \ \ \ }length\ args\ =\ arity\ f\isasymrbrakk \isanewline
|
|
131 |
\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm'\ arity%
|
|
132 |
\end{isabelle}
|
|
133 |
\end{isamarkuptxt}
|
10878
|
134 |
\isacommand{apply}\ auto\isanewline
|
|
135 |
\isacommand{done}\isanewline
|
|
136 |
\isanewline
|
|
137 |
\isanewline
|
|
138 |
\isanewline
|
11173
|
139 |
\isacommand{lemma}\ "well_formed_gterm'\ arity\ \isasymsubseteq \ well_formed_gterm\ arity"\isanewline
|
10878
|
140 |
\isacommand{apply}\ clarify%
|
11173
|
141 |
\begin{isamarkuptxt}
|
10878
|
142 |
The situation after clarify
|
11173
|
143 |
\begin{isabelle}
|
|
144 |
\ 1.\ \isasymAnd x.\ x\ \isasymin \ well_formed_gterm'\ arity\ \isasymLongrightarrow \isanewline
|
|
145 |
\isaindent{\ 1.\ \isasymAnd x.\ }x\ \isasymin \ well_formed_gterm\ arity%
|
|
146 |
\end{isabelle}
|
|
147 |
\end{isamarkuptxt}
|
|
148 |
\isacommand{apply}\ (erule\ well_formed_gterm'.induct)
|
|
149 |
\begin{isamarkuptxt}
|
10878
|
150 |
note the induction hypothesis!
|
11173
|
151 |
\begin{isabelle}
|
|
152 |
\ 1.\ \isasymAnd x\ args\ f.\isanewline
|
|
153 |
\isaindent{\ 1.\ \ \ \ }\isasymlbrakk args\isanewline
|
|
154 |
\isaindent{\ 1.\ \ \ \ \isasymlbrakk }\isasymin \ lists\isanewline
|
|
155 |
\isaindent{\ 1.\ \ \ \ \isasymlbrakk \isasymin \ \ }(well_formed_gterm'\ arity\ \isasyminter \isanewline
|
|
156 |
\isaindent{\ 1.\ \ \ \ \isasymlbrakk \isasymin \ \ (}\isacharbraceleft x.\ x\ \isasymin \ well_formed_gterm\ arity\isacharbraceright );\isanewline
|
|
157 |
\isaindent{\ 1.\ \ \ \ \ \ \ }length\ args\ =\ arity\ f\isasymrbrakk \isanewline
|
|
158 |
\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm\ arity%
|
|
159 |
\end{isabelle}
|
|
160 |
\end{isamarkuptxt}
|
10469
|
161 |
\isacommand{apply}\ auto\isanewline
|
11173
|
162 |
\isacommand{done}
|
|
163 |
\begin{isamarkuptext}
|
|
164 |
\begin{isabelle}
|
|
165 |
\ \ \ \ \ lists\ (A\ \isasyminter \ B)\ =\ lists\ A\ \isasyminter \ lists\ B%
|
|
166 |
\end{isabelle}
|
|
167 |
\end{isamarkuptext}
|
10469
|
168 |
%
|
11173
|
169 |
\begin{isamarkuptext}
|
10469
|
170 |
the rest isn't used: too complicated. OK for an exercise though.%
|
11173
|
171 |
\end{isamarkuptext}
|
|
172 |
\isacommand{consts}\ integer_signature\ ::\ "(integer_op\ *\ (unit\ list\ *\ unit))\ set"\isanewline
|
|
173 |
\isacommand{inductive}\ "integer_signature"\isanewline
|
10365
|
174 |
\isakeyword{intros}\isanewline
|
11173
|
175 |
Number:\ \ \ \ \ "(Number\ n,\ \ \ ([],\ ()))\ \isasymin \ integer_signature"\isanewline
|
|
176 |
UnaryMinus:\ "(UnaryMinus,\ ([()],\ ()))\ \isasymin \ integer_signature"\isanewline
|
|
177 |
Plus:\ \ \ \ \ \ \ "(Plus,\ \ \ \ \ \ \ ([(),()],\ ()))\ \isasymin \ integer_signature"\isanewline
|
10469
|
178 |
\isanewline
|
|
179 |
\isanewline
|
11173
|
180 |
\isacommand{consts}\ well_typed_gterm\ ::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline
|
|
181 |
\isacommand{inductive}\ "well_typed_gterm\ sig"\isanewline
|
10469
|
182 |
\isakeyword{intros}\isanewline
|
11173
|
183 |
step[intro!]:\ \isanewline
|
|
184 |
\ \ \ \ "\isasymlbrakk \isasymforall pair\ \isasymin \ set\ args.\ pair\ \isasymin \ well_typed_gterm\ sig;\ \isanewline
|
|
185 |
\ \ \ \ \ \ sig\ f\ =\ (map\ snd\ args,\ rtype)\isasymrbrakk \isanewline
|
|
186 |
\ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ (map\ fst\ args),\ rtype)\ \isanewline
|
|
187 |
\ \ \ \ \ \ \ \ \ \isasymin \ well_typed_gterm\ sig"\isanewline
|
10469
|
188 |
\isanewline
|
11173
|
189 |
\isacommand{consts}\ well_typed_gterm'\ ::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline
|
|
190 |
\isacommand{inductive}\ "well_typed_gterm'\ sig"\isanewline
|
10469
|
191 |
\isakeyword{intros}\isanewline
|
11173
|
192 |
step[intro!]:\ \isanewline
|
|
193 |
\ \ \ \ "\isasymlbrakk args\ \isasymin \ lists(well_typed_gterm'\ sig);\ \isanewline
|
|
194 |
\ \ \ \ \ \ sig\ f\ =\ (map\ snd\ args,\ rtype)\isasymrbrakk \isanewline
|
|
195 |
\ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ (map\ fst\ args),\ rtype)\ \isanewline
|
|
196 |
\ \ \ \ \ \ \ \ \ \isasymin \ well_typed_gterm'\ sig"\isanewline
|
|
197 |
\isakeyword{monos}\ lists_mono\isanewline
|
10365
|
198 |
\isanewline
|
|
199 |
\isanewline
|
11173
|
200 |
\isacommand{lemma}\ "well_typed_gterm\ sig\ \isasymsubseteq \ well_typed_gterm'\ sig"\isanewline
|
10365
|
201 |
\isacommand{apply}\ clarify\isanewline
|
11173
|
202 |
\isacommand{apply}\ (erule\ well_typed_gterm.induct)\isanewline
|
10365
|
203 |
\isacommand{apply}\ auto\isanewline
|
|
204 |
\isacommand{done}\isanewline
|
|
205 |
\isanewline
|
11173
|
206 |
\isacommand{lemma}\ "well_typed_gterm'\ sig\ \isasymsubseteq \ well_typed_gterm\ sig"\isanewline
|
10365
|
207 |
\isacommand{apply}\ clarify\isanewline
|
11173
|
208 |
\isacommand{apply}\ (erule\ well_typed_gterm'.induct)\isanewline
|
10365
|
209 |
\isacommand{apply}\ auto\isanewline
|
|
210 |
\isacommand{done}\isanewline
|
|
211 |
\isanewline
|
10469
|
212 |
\isanewline
|
10365
|
213 |
\isacommand{end}\isanewline
|
|
214 |
\isanewline
|
11173
|
215 |
\end{isabelle}
|
10365
|
216 |
%%% Local Variables:
|
|
217 |
%%% mode: latex
|
|
218 |
%%% TeX-master: "root"
|
|
219 |
%%% End:
|