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