|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{AB}% |
|
4 \isacommand{theory}\ AB\ {\isacharequal}\ Main{\isacharcolon}\isanewline |
|
5 \isanewline |
|
6 \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b\isanewline |
|
7 \isanewline |
|
8 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isacharampersand}\ {\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline |
|
9 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharparenright}\isanewline |
|
10 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline |
|
11 \isanewline |
|
12 \isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline |
|
13 \ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline |
|
14 \ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline |
|
15 \isanewline |
|
16 \isacommand{inductive}\ S\ A\ B\isanewline |
|
17 \isakeyword{intros}\isanewline |
|
18 {\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}\ S{\isachardoublequote}\isanewline |
|
19 {\isachardoublequote}w\ {\isacharcolon}\ A\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}w\ {\isacharcolon}\ S{\isachardoublequote}\isanewline |
|
20 {\isachardoublequote}w\ {\isacharcolon}\ B\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}w\ {\isacharcolon}\ S{\isachardoublequote}\isanewline |
|
21 \isanewline |
|
22 {\isachardoublequote}w\ {\isacharcolon}\ S\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}w\ {\isacharcolon}\ A{\isachardoublequote}\isanewline |
|
23 {\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ v{\isacharcolon}A{\isacharsemicolon}\ w{\isacharcolon}A\ {\isacharbar}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}v{\isacharat}w\ {\isacharcolon}\ A{\isachardoublequote}\isanewline |
|
24 \isanewline |
|
25 {\isachardoublequote}w\ {\isacharcolon}\ S\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}w\ {\isacharcolon}\ B{\isachardoublequote}\isanewline |
|
26 {\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ v{\isacharcolon}B{\isacharsemicolon}\ w{\isacharcolon}B\ {\isacharbar}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}v{\isacharat}w\ {\isacharcolon}\ B{\isachardoublequote}\isanewline |
|
27 \isanewline |
|
28 \isacommand{thm}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharbrackleft}no{\isacharunderscore}vars{\isacharbrackright}\isanewline |
|
29 \isanewline |
|
30 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}w\ {\isacharcolon}\ S\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ {\isacharampersand}\isanewline |
|
31 \ \ \ \ \ \ \ {\isacharparenleft}w\ {\isacharcolon}\ A\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharampersand}\isanewline |
|
32 \ \ \ \ \ \ \ {\isacharparenleft}w\ {\isacharcolon}\ B\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
|
33 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline |
|
34 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline |
|
35 \isanewline |
|
36 \isacommand{lemma}\ intermed{\isacharunderscore}val{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline |
|
37 \ {\isachardoublequote}{\isacharparenleft}{\isacharbang}i{\isacharless}n{\isachardot}\ abs{\isacharparenleft}f{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isacharparenright}\ {\isacharminus}{\isacharminus}{\isachargreater}\ \isanewline |
|
38 \ \ f\ {\isadigit{0}}\ {\isacharless}{\isacharequal}\ k\ {\isacharampersand}\ k\ {\isacharless}{\isacharequal}\ f\ n\ {\isacharminus}{\isacharminus}{\isachargreater}\ {\isacharparenleft}{\isacharquery}\ i\ {\isacharless}{\isacharequal}\ n{\isachardot}\ f\ i\ {\isacharequal}\ {\isacharparenleft}k{\isacharcolon}{\isacharcolon}int{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
|
39 \isacommand{apply}{\isacharparenleft}induct\ n{\isacharparenright}\isanewline |
|
40 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
41 \ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline |
|
42 \isacommand{apply}{\isacharparenleft}rule{\isacharparenright}\isanewline |
|
43 \isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline |
|
44 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
45 \isacommand{apply}{\isacharparenleft}rule{\isacharparenright}\isanewline |
|
46 \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ n\ \isakeyword{in}\ allE{\isacharparenright}\isanewline |
|
47 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
48 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequote}k\ {\isacharequal}\ f{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline |
|
49 \ \isacommand{apply}{\isacharparenleft}force{\isacharparenright}\isanewline |
|
50 \isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline |
|
51 \ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ split{\isacharcolon}split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}\isanewline |
|
52 \ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline |
|
53 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}le{\isacharunderscore}SucI{\isacharparenright}\isanewline |
|
54 \isanewline |
|
55 \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}ALL\ i\ {\isacharless}\ size\ w{\isachardot}\isanewline |
|
56 \ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w\ {\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\ int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w\ {\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharminus}\isanewline |
|
57 \ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ i\ w\ {\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\ int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ i\ w\ {\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}\isanewline |
|
58 \isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline |
|
59 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
60 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline |
|
61 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline |
|
62 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline |
|
63 \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
64 \ \isacommand{apply}{\isacharparenleft}erule\ allE{\isacharparenright}\isanewline |
|
65 \ \isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline |
|
66 \ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline |
|
67 \ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline |
|
68 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
69 \isacommand{apply}{\isacharparenleft}erule\ allE{\isacharparenright}\isanewline |
|
70 \isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline |
|
71 \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline |
|
72 \isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline |
|
73 \isanewline |
|
74 \isanewline |
|
75 \isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline |
|
76 \ {\isachardoublequote}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ Suc{\isacharparenleft}Suc{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}{\isacharequal}{\isachargreater}\isanewline |
|
77 \ \ EX\ i{\isacharless}{\isacharequal}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ w{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline |
|
78 \isacommand{apply}{\isacharparenleft}insert\ intermed{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline |
|
79 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
80 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline |
|
81 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}i\ \isakeyword{in}\ exI{\isacharparenright}\isanewline |
|
82 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
83 \isacommand{apply}{\isacharparenleft}rule\ int{\isacharunderscore}int{\isacharunderscore}eq{\isacharbrackleft}THEN\ iffD{\isadigit{1}}{\isacharbrackright}{\isacharparenright}\isanewline |
|
84 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
85 \isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline |
|
86 \isanewline |
|
87 \isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline |
|
88 {\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs\ {\isacharat}\ drop\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs\ {\isacharat}\ drop\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline |
|
89 \ \ \ \ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}\ {\isacharbar}{\isacharbrackright}\isanewline |
|
90 \ {\isacharequal}{\isacharequal}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}drop\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}drop\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline |
|
91 \isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isanewline |
|
92 \isanewline |
|
93 \isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros\isanewline |
|
94 \isanewline |
|
95 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ S{\isacharparenright}\ {\isacharampersand}\isanewline |
|
96 \ \ \ \ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ A{\isacharparenright}\ {\isacharampersand}\isanewline |
|
97 \ \ \ \ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ B{\isacharparenright}{\isachardoublequote}\isanewline |
|
98 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isanewline |
|
99 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequote}xs{\isachardoublequote}{\isacharparenright}\isanewline |
|
100 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
101 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
102 \isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline |
|
103 \ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
104 \ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
|
105 \ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline |
|
106 \ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline |
|
107 \ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
|
108 \ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline |
|
109 \ \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}list\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline |
|
110 \ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline |
|
111 \ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
|
112 \ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline |
|
113 \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline |
|
114 \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
|
115 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline |
|
116 \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline |
|
117 \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline |
|
118 \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline |
|
119 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}list\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline |
|
120 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline |
|
121 \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline |
|
122 \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline |
|
123 \isanewline |
|
124 \isacommand{end}\isanewline |
|
125 \end{isabellebody}% |
|
126 %%% Local Variables: |
|
127 %%% mode: latex |
|
128 %%% TeX-master: "root" |
|
129 %%% End: |