doc-src/TutorialI/Inductive/document/Advanced.tex

revisions in response to comments by Tobias

%
\begin{isabelle}
\def\isabellecontext{Advanced}
\isanewline
\isacommand{theory}\ Advanced\ =\ Even:\isanewline
\isanewline
\isanewline
\isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list"\isanewline
\isanewline
\isacommand{datatype}\ integer_op\ =\ Number\ int\ |\ UnaryMinus\ |\ Plus\isanewline
\isanewline
\isacommand{consts}\ gterms\ ::\ "'f\ set\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
\isacommand{inductive}\ "gterms\ F"\isanewline
\isakeyword{intros}\isanewline
step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ gterms\ F;\ \ f\ \isasymin \ F\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ gterms\ F"\isanewline
\isanewline
\isacommand{lemma}\ gterms_mono:\ "F\isasymsubseteq G\ \isasymLongrightarrow \ gterms\ F\ \isasymsubseteq \ gterms\ G"\isanewline
\isacommand{apply}\ clarify\isanewline
\isacommand{apply}\ (erule\ gterms.induct)
\begin{isamarkuptxt}
\begin{isabelle}
\ 1.\ \isasymAnd x\ args\ f.\isanewline
\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
\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G%
\end{isabelle}
\end{isamarkuptxt}
\isacommand{apply}\ blast\isanewline
\isacommand{done}
\begin{isamarkuptext}
\begin{isabelle}
\ \ \ \ \ \isasymlbrakk a\ \isasymin \ even;\ a\ =\ 0\ \isasymLongrightarrow \ P;\ \isasymAnd n.\ \isasymlbrakk a\ =\ Suc\ (Suc\ n);\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
\rulename{even.cases}
\end{isabelle}

Just as a demo I include
the two forms that Markus has made available. First the one for binding the
result to a name%
\end{isamarkuptext}
\isacommand{inductive_cases}\ Suc_Suc_cases\ [elim!]:\isanewline
\ \ "Suc(Suc\ n)\ \isasymin \ even"\isanewline
\isanewline
\isacommand{thm}\ Suc_Suc_cases%
\begin{isamarkuptext}
\begin{isabelle}
\ \ \ \ \ \isasymlbrakk Suc\ (Suc\ n)\ \isasymin \ even;\ n\ \isasymin \ even\ \isasymLongrightarrow \ P\isasymrbrakk \ \isasymLongrightarrow \ P%
\rulename{Suc_Suc_cases}
\end{isabelle}

and now the one for local usage:%
\end{isamarkuptext}
\isacommand{lemma}\ "Suc(Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ P\ n"\isanewline
\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")\isanewline
\isacommand{oops}\isanewline
\isanewline
\isacommand{inductive_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\ \isasymin \ gterms\ F"
\begin{isamarkuptext}
this is what we get:

\begin{isabelle}
\ \ \ \ \ \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%
\rulename{gterm_Apply_elim}
\end{isabelle}
\end{isamarkuptext}
\isacommand{lemma}\ gterms_IntI\ [rule_format,\ intro!]:\isanewline
\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter G)"\isanewline
\isacommand{apply}\ (erule\ gterms.induct)
\begin{isamarkuptxt}
\begin{isabelle}
\ 1.\ \isasymAnd args\ f.\isanewline
\isaindent{\ 1.\ \ \ \ }\isasymlbrakk \isasymforall t\isasymin set\ args.\isanewline
\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ gterms\ F\ \isasymand \ (t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\ \isasyminter \ G));\isanewline
\isaindent{\ 1.\ \ \ \ \ \ \ }f\ \isasymin \ F\isasymrbrakk \isanewline
\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ gterms\ G\ \isasymlongrightarrow \isanewline
\isaindent{\ 1.\ \ \ \ \isasymLongrightarrow \ }Apply\ f\ args\ \isasymin \ gterms\ (F\ \isasyminter \ G)
\end{isabelle}
\end{isamarkuptxt}
\isacommand{apply}\ blast\isanewline
\isacommand{done}
\begin{isamarkuptext}
\begin{isabelle}
\ \ \ \ \ mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \ f\ A\ \isasyminter \ f\ B%
\rulename{mono_Int}
\end{isabelle}
\end{isamarkuptext}
\isacommand{lemma}\ gterms_Int_eq\ [simp]:\isanewline
\ \ \ \ \ "gterms\ (F\isasyminter G)\ =\ gterms\ F\ \isasyminter \ gterms\ G"\isanewline
\isacommand{by}\ (blast\ intro!:\ mono_Int\ monoI\ gterms_mono)\isanewline
\isanewline
\isanewline
\isacommand{consts}\ integer_arity\ ::\ "integer_op\ \isasymRightarrow \ nat"\isanewline
\isacommand{primrec}\isanewline
"integer_arity\ (Number\ n)\ \ \ \ \ \ \ \ =\ \#0"\isanewline
"integer_arity\ UnaryMinus\ \ \ \ \ \ \ \ =\ \#1"\isanewline
"integer_arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ =\ \#2"\isanewline
\isanewline
\isacommand{consts}\ well_formed_gterm\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
\isacommand{inductive}\ "well_formed_gterm\ arity"\isanewline
\isakeyword{intros}\isanewline
step[intro!]:\ "\isasymlbrakk \isasymforall t\ \isasymin \ set\ args.\ t\ \isasymin \ well_formed_gterm\ arity;\ \ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm\ arity"\isanewline
\isanewline
\isanewline
\isacommand{consts}\ well_formed_gterm'\ ::\ "('f\ \isasymRightarrow \ nat)\ \isasymRightarrow \ 'f\ gterm\ set"\isanewline
\isacommand{inductive}\ "well_formed_gterm'\ arity"\isanewline
\isakeyword{intros}\isanewline
step[intro!]:\ "\isasymlbrakk args\ \isasymin \ lists\ (well_formed_gterm'\ arity);\ \ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ =\ arity\ f\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ args)\ \isasymin \ well_formed_gterm'\ arity"\isanewline
\isakeyword{monos}\ lists_mono\isanewline
\isanewline
\isacommand{lemma}\ "well_formed_gterm\ arity\ \isasymsubseteq \ well_formed_gterm'\ arity"\isanewline
\isacommand{apply}\ clarify%
\begin{isamarkuptxt}
The situation after clarify
\begin{isabelle}
\ 1.\ \isasymAnd x.\ x\ \isasymin \ well_formed_gterm\ arity\ \isasymLongrightarrow \isanewline
\isaindent{\ 1.\ \isasymAnd x.\ }x\ \isasymin \ well_formed_gterm'\ arity%
\end{isabelle}
\end{isamarkuptxt}
\isacommand{apply}\ (erule\ well_formed_gterm.induct)
\begin{isamarkuptxt}
note the induction hypothesis!
\begin{isabelle}
\ 1.\ \isasymAnd x\ args\ f.\isanewline
\isaindent{\ 1.\ \ \ \ }\isasymlbrakk \isasymforall t\isasymin set\ args.\isanewline
\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ well_formed_gterm\ arity\ \isasymand \isanewline
\isaindent{\ 1.\ \ \ \ \isasymlbrakk \ \ \ }t\ \isasymin \ well_formed_gterm'\ arity;\isanewline
\isaindent{\ 1.\ \ \ \ \ \ \ }length\ args\ =\ arity\ f\isasymrbrakk \isanewline
\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm'\ arity%
\end{isabelle}
\end{isamarkuptxt}
\isacommand{apply}\ auto\isanewline
\isacommand{done}\isanewline
\isanewline
\isanewline
\isanewline
\isacommand{lemma}\ "well_formed_gterm'\ arity\ \isasymsubseteq \ well_formed_gterm\ arity"\isanewline
\isacommand{apply}\ clarify%
\begin{isamarkuptxt}
The situation after clarify
\begin{isabelle}
\ 1.\ \isasymAnd x.\ x\ \isasymin \ well_formed_gterm'\ arity\ \isasymLongrightarrow \isanewline
\isaindent{\ 1.\ \isasymAnd x.\ }x\ \isasymin \ well_formed_gterm\ arity%
\end{isabelle}
\end{isamarkuptxt}
\isacommand{apply}\ (erule\ well_formed_gterm'.induct)
\begin{isamarkuptxt}
note the induction hypothesis!
\begin{isabelle}
\ 1.\ \isasymAnd x\ args\ f.\isanewline
\isaindent{\ 1.\ \ \ \ }\isasymlbrakk args\isanewline
\isaindent{\ 1.\ \ \ \ \isasymlbrakk }\isasymin \ lists\isanewline
\isaindent{\ 1.\ \ \ \ \isasymlbrakk \isasymin \ \ }(well_formed_gterm'\ arity\ \isasyminter \isanewline
\isaindent{\ 1.\ \ \ \ \isasymlbrakk \isasymin \ \ (}\isacharbraceleft x.\ x\ \isasymin \ well_formed_gterm\ arity\isacharbraceright );\isanewline
\isaindent{\ 1.\ \ \ \ \ \ \ }length\ args\ =\ arity\ f\isasymrbrakk \isanewline
\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ Apply\ f\ args\ \isasymin \ well_formed_gterm\ arity%
\end{isabelle}
\end{isamarkuptxt}
\isacommand{apply}\ auto\isanewline
\isacommand{done}
\begin{isamarkuptext}
\begin{isabelle}
\ \ \ \ \ lists\ (A\ \isasyminter \ B)\ =\ lists\ A\ \isasyminter \ lists\ B%
\end{isabelle}
\end{isamarkuptext}
%
\begin{isamarkuptext}
the rest isn't used: too complicated.  OK for an exercise though.%
\end{isamarkuptext}
\isacommand{consts}\ integer_signature\ ::\ "(integer_op\ *\ (unit\ list\ *\ unit))\ set"\isanewline
\isacommand{inductive}\ "integer_signature"\isanewline
\isakeyword{intros}\isanewline
Number:\ \ \ \ \ "(Number\ n,\ \ \ ([],\ ()))\ \isasymin \ integer_signature"\isanewline
UnaryMinus:\ "(UnaryMinus,\ ([()],\ ()))\ \isasymin \ integer_signature"\isanewline
Plus:\ \ \ \ \ \ \ "(Plus,\ \ \ \ \ \ \ ([(),()],\ ()))\ \isasymin \ integer_signature"\isanewline
\isanewline
\isanewline
\isacommand{consts}\ well_typed_gterm\ ::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline
\isacommand{inductive}\ "well_typed_gterm\ sig"\isanewline
\isakeyword{intros}\isanewline
step[intro!]:\ \isanewline
\ \ \ \ "\isasymlbrakk \isasymforall pair\ \isasymin \ set\ args.\ pair\ \isasymin \ well_typed_gterm\ sig;\ \isanewline
\ \ \ \ \ \ sig\ f\ =\ (map\ snd\ args,\ rtype)\isasymrbrakk \isanewline
\ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ (map\ fst\ args),\ rtype)\ \isanewline
\ \ \ \ \ \ \ \ \ \isasymin \ well_typed_gterm\ sig"\isanewline
\isanewline
\isacommand{consts}\ well_typed_gterm'\ ::\ "('f\ \isasymRightarrow \ 't\ list\ *\ 't)\ \isasymRightarrow \ ('f\ gterm\ *\ 't)set"\isanewline
\isacommand{inductive}\ "well_typed_gterm'\ sig"\isanewline
\isakeyword{intros}\isanewline
step[intro!]:\ \isanewline
\ \ \ \ "\isasymlbrakk args\ \isasymin \ lists(well_typed_gterm'\ sig);\ \isanewline
\ \ \ \ \ \ sig\ f\ =\ (map\ snd\ args,\ rtype)\isasymrbrakk \isanewline
\ \ \ \ \ \isasymLongrightarrow \ (Apply\ f\ (map\ fst\ args),\ rtype)\ \isanewline
\ \ \ \ \ \ \ \ \ \isasymin \ well_typed_gterm'\ sig"\isanewline
\isakeyword{monos}\ lists_mono\isanewline
\isanewline
\isanewline
\isacommand{lemma}\ "well_typed_gterm\ sig\ \isasymsubseteq \ well_typed_gterm'\ sig"\isanewline
\isacommand{apply}\ clarify\isanewline
\isacommand{apply}\ (erule\ well_typed_gterm.induct)\isanewline
\isacommand{apply}\ auto\isanewline
\isacommand{done}\isanewline
\isanewline
\isacommand{lemma}\ "well_typed_gterm'\ sig\ \isasymsubseteq \ well_typed_gterm\ sig"\isanewline
\isacommand{apply}\ clarify\isanewline
\isacommand{apply}\ (erule\ well_typed_gterm'.induct)\isanewline
\isacommand{apply}\ auto\isanewline
\isacommand{done}\isanewline
\isanewline
\isanewline
\isacommand{end}\isanewline
\isanewline
\end{isabelle}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: