src/HOL/Nitpick_Examples/Manual_Nits.thy
 author wenzelm Thu Feb 11 23:00:22 2010 +0100 (2010-02-11) changeset 35115 446c5063e4fd parent 35078 6fd1052fe463 child 35180 c57dba973391 permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
```     1 (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
```
```     2     Author:     Jasmin Blanchette, TU Muenchen
```
```     3     Copyright   2009, 2010
```
```     4
```
```     5 Examples from the Nitpick manual.
```
```     6 *)
```
```     7
```
```     8 header {* Examples from the Nitpick Manual *}
```
```     9
```
```    10 theory Manual_Nits
```
```    11 imports Main Coinductive_List RealDef
```
```    12 begin
```
```    13
```
```    14 chapter {* 3. First Steps *}
```
```    15
```
```    16 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
```
```    17
```
```    18 subsection {* 3.1. Propositional Logic *}
```
```    19
```
```    20 lemma "P \<longleftrightarrow> Q"
```
```    21 nitpick
```
```    22 apply auto
```
```    23 nitpick 1
```
```    24 nitpick 2
```
```    25 oops
```
```    26
```
```    27 subsection {* 3.2. Type Variables *}
```
```    28
```
```    29 lemma "P x \<Longrightarrow> P (THE y. P y)"
```
```    30 nitpick [verbose]
```
```    31 oops
```
```    32
```
```    33 subsection {* 3.3. Constants *}
```
```    34
```
```    35 lemma "P x \<Longrightarrow> P (THE y. P y)"
```
```    36 nitpick [show_consts]
```
```    37 nitpick [full_descrs, show_consts]
```
```    38 nitpick [dont_specialize, full_descrs, show_consts]
```
```    39 oops
```
```    40
```
```    41 lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
```
```    42 nitpick
```
```    43 nitpick [card 'a = 1-50]
```
```    44 (* sledgehammer *)
```
```    45 apply (metis the_equality)
```
```    46 done
```
```    47
```
```    48 subsection {* 3.4. Skolemization *}
```
```    49
```
```    50 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
```
```    51 nitpick
```
```    52 oops
```
```    53
```
```    54 lemma "\<exists>x. \<forall>f. f x = x"
```
```    55 nitpick
```
```    56 oops
```
```    57
```
```    58 lemma "refl r \<Longrightarrow> sym r"
```
```    59 nitpick
```
```    60 oops
```
```    61
```
```    62 subsection {* 3.5. Natural Numbers and Integers *}
```
```    63
```
```    64 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
```
```    65 nitpick
```
```    66 oops
```
```    67
```
```    68 lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
```
```    69 nitpick [card nat = 100, check_potential]
```
```    70 oops
```
```    71
```
```    72 lemma "P Suc"
```
```    73 nitpick [card = 1-6]
```
```    74 oops
```
```    75
```
```    76 lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
```
```    77 nitpick [card nat = 1]
```
```    78 nitpick [card nat = 2]
```
```    79 oops
```
```    80
```
```    81 subsection {* 3.6. Inductive Datatypes *}
```
```    82
```
```    83 lemma "hd (xs @ [y, y]) = hd xs"
```
```    84 nitpick
```
```    85 nitpick [show_consts, show_datatypes]
```
```    86 oops
```
```    87
```
```    88 lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
```
```    89 nitpick [show_datatypes]
```
```    90 oops
```
```    91
```
```    92 subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
```
```    93
```
```    94 typedef three = "{0\<Colon>nat, 1, 2}"
```
```    95 by blast
```
```    96
```
```    97 definition A :: three where "A \<equiv> Abs_three 0"
```
```    98 definition B :: three where "B \<equiv> Abs_three 1"
```
```    99 definition C :: three where "C \<equiv> Abs_three 2"
```
```   100
```
```   101 lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
```
```   102 nitpick [show_datatypes]
```
```   103 oops
```
```   104
```
```   105 record point =
```
```   106   Xcoord :: int
```
```   107   Ycoord :: int
```
```   108
```
```   109 lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
```
```   110 nitpick [show_datatypes]
```
```   111 oops
```
```   112
```
```   113 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
```
```   114 nitpick [show_datatypes]
```
```   115 oops
```
```   116
```
```   117 subsection {* 3.8. Inductive and Coinductive Predicates *}
```
```   118
```
```   119 inductive even where
```
```   120 "even 0" |
```
```   121 "even n \<Longrightarrow> even (Suc (Suc n))"
```
```   122
```
```   123 lemma "\<exists>n. even n \<and> even (Suc n)"
```
```   124 nitpick [card nat = 100, unary_ints, verbose]
```
```   125 oops
```
```   126
```
```   127 lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
```
```   128 nitpick [card nat = 100, unary_ints, verbose]
```
```   129 oops
```
```   130
```
```   131 inductive even' where
```
```   132 "even' (0\<Colon>nat)" |
```
```   133 "even' 2" |
```
```   134 "\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
```
```   135
```
```   136 lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
```
```   137 nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
```
```   138 oops
```
```   139
```
```   140 lemma "even' (n - 2) \<Longrightarrow> even' n"
```
```   141 nitpick [card nat = 10, show_consts]
```
```   142 oops
```
```   143
```
```   144 coinductive nats where
```
```   145 "nats (x\<Colon>nat) \<Longrightarrow> nats x"
```
```   146
```
```   147 lemma "nats = {0, 1, 2, 3, 4}"
```
```   148 nitpick [card nat = 10, show_consts]
```
```   149 oops
```
```   150
```
```   151 inductive odd where
```
```   152 "odd 1" |
```
```   153 "\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
```
```   154
```
```   155 lemma "odd n \<Longrightarrow> odd (n - 2)"
```
```   156 nitpick [card nat = 10, show_consts]
```
```   157 oops
```
```   158
```
```   159 subsection {* 3.9. Coinductive Datatypes *}
```
```   160
```
```   161 lemma "xs \<noteq> LCons a xs"
```
```   162 nitpick
```
```   163 oops
```
```   164
```
```   165 lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
```
```   166 nitpick [verbose]
```
```   167 nitpick [bisim_depth = -1, verbose]
```
```   168 oops
```
```   169
```
```   170 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
```
```   171 nitpick [bisim_depth = -1, show_datatypes]
```
```   172 nitpick
```
```   173 sorry
```
```   174
```
```   175 subsection {* 3.10. Boxing *}
```
```   176
```
```   177 datatype tm = Var nat | Lam tm | App tm tm
```
```   178
```
```   179 primrec lift where
```
```   180 "lift (Var j) k = Var (if j < k then j else j + 1)" |
```
```   181 "lift (Lam t) k = Lam (lift t (k + 1))" |
```
```   182 "lift (App t u) k = App (lift t k) (lift u k)"
```
```   183
```
```   184 primrec loose where
```
```   185 "loose (Var j) k = (j \<ge> k)" |
```
```   186 "loose (Lam t) k = loose t (Suc k)" |
```
```   187 "loose (App t u) k = (loose t k \<or> loose u k)"
```
```   188
```
```   189 primrec subst\<^isub>1 where
```
```   190 "subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
```
```   191 "subst\<^isub>1 \<sigma> (Lam t) =
```
```   192  Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
```
```   193 "subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
```
```   194
```
```   195 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
```
```   196 nitpick [verbose]
```
```   197 nitpick [eval = "subst\<^isub>1 \<sigma> t"]
```
```   198 nitpick [dont_box]
```
```   199 oops
```
```   200
```
```   201 primrec subst\<^isub>2 where
```
```   202 "subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
```
```   203 "subst\<^isub>2 \<sigma> (Lam t) =
```
```   204  Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
```
```   205 "subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
```
```   206
```
```   207 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
```
```   208 nitpick
```
```   209 sorry
```
```   210
```
```   211 subsection {* 3.11. Scope Monotonicity *}
```
```   212
```
```   213 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
```
```   214 nitpick [verbose]
```
```   215 nitpick [card = 8, verbose]
```
```   216 oops
```
```   217
```
```   218 lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
```
```   219 nitpick [mono]
```
```   220 nitpick
```
```   221 oops
```
```   222
```
```   223 subsection {* 3.12. Inductive Properties *}
```
```   224
```
```   225 inductive_set reach where
```
```   226 "(4\<Colon>nat) \<in> reach" |
```
```   227 "n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
```
```   228 "n \<in> reach \<Longrightarrow> n + 2 \<in> reach"
```
```   229
```
```   230 lemma "n \<in> reach \<Longrightarrow> 2 dvd n"
```
```   231 nitpick
```
```   232 apply (induct set: reach)
```
```   233   apply auto
```
```   234  nitpick
```
```   235  apply (thin_tac "n \<in> reach")
```
```   236  nitpick
```
```   237 oops
```
```   238
```
```   239 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<noteq> 0"
```
```   240 nitpick
```
```   241 apply (induct set: reach)
```
```   242   apply auto
```
```   243  nitpick
```
```   244  apply (thin_tac "n \<in> reach")
```
```   245  nitpick
```
```   246 oops
```
```   247
```
```   248 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
```
```   249 by (induct set: reach) arith+
```
```   250
```
```   251 datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
```
```   252
```
```   253 primrec labels where
```
```   254 "labels (Leaf a) = {a}" |
```
```   255 "labels (Branch t u) = labels t \<union> labels u"
```
```   256
```
```   257 primrec swap where
```
```   258 "swap (Leaf c) a b =
```
```   259  (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
```
```   260 "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
```
```   261
```
```   262 lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t"
```
```   263 nitpick
```
```   264 proof (induct t)
```
```   265   case Leaf thus ?case by simp
```
```   266 next
```
```   267   case (Branch t u) thus ?case
```
```   268   nitpick
```
```   269   nitpick [non_std "'a bin_tree", show_consts]
```
```   270 oops
```
```   271
```
```   272 lemma "labels (swap t a b) =
```
```   273        (if a \<in> labels t then
```
```   274           if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
```
```   275         else
```
```   276           if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
```
```   277 nitpick
```
```   278 proof (induct t)
```
```   279   case Leaf thus ?case by simp
```
```   280 next
```
```   281   case (Branch t u) thus ?case
```
```   282   nitpick [non_std "'a bin_tree", show_consts]
```
```   283   by auto
```
```   284 qed
```
```   285
```
```   286 section {* 4. Case Studies *}
```
```   287
```
```   288 nitpick_params [max_potential = 0, max_threads = 2]
```
```   289
```
```   290 subsection {* 4.1. A Context-Free Grammar *}
```
```   291
```
```   292 datatype alphabet = a | b
```
```   293
```
```   294 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
```
```   295   "[] \<in> S\<^isub>1"
```
```   296 | "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
```
```   297 | "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
```
```   298 | "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
```
```   299 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
```
```   300 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
```
```   301
```
```   302 theorem S\<^isub>1_sound:
```
```   303 "w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
```
```   304 nitpick
```
```   305 oops
```
```   306
```
```   307 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
```
```   308   "[] \<in> S\<^isub>2"
```
```   309 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
```
```   310 | "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
```
```   311 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
```
```   312 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
```
```   313 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
```
```   314
```
```   315 theorem S\<^isub>2_sound:
```
```   316 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
```
```   317 nitpick
```
```   318 oops
```
```   319
```
```   320 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
```
```   321   "[] \<in> S\<^isub>3"
```
```   322 | "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
```
```   323 | "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
```
```   324 | "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
```
```   325 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
```
```   326 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
```
```   327
```
```   328 theorem S\<^isub>3_sound:
```
```   329 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
```
```   330 nitpick
```
```   331 sorry
```
```   332
```
```   333 theorem S\<^isub>3_complete:
```
```   334 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
```
```   335 nitpick
```
```   336 oops
```
```   337
```
```   338 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
```
```   339   "[] \<in> S\<^isub>4"
```
```   340 | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
```
```   341 | "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
```
```   342 | "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
```
```   343 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
```
```   344 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
```
```   345 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
```
```   346
```
```   347 theorem S\<^isub>4_sound:
```
```   348 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
```
```   349 nitpick
```
```   350 sorry
```
```   351
```
```   352 theorem S\<^isub>4_complete:
```
```   353 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
```
```   354 nitpick
```
```   355 sorry
```
```   356
```
```   357 theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
```
```   358 "w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
```
```   359 "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
```
```   360 "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
```
```   361 nitpick
```
```   362 sorry
```
```   363
```
```   364 subsection {* 4.2. AA Trees *}
```
```   365
```
```   366 datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
```
```   367
```
```   368 primrec data where
```
```   369 "data \<Lambda> = undefined" |
```
```   370 "data (N x _ _ _) = x"
```
```   371
```
```   372 primrec dataset where
```
```   373 "dataset \<Lambda> = {}" |
```
```   374 "dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
```
```   375
```
```   376 primrec level where
```
```   377 "level \<Lambda> = 0" |
```
```   378 "level (N _ k _ _) = k"
```
```   379
```
```   380 primrec left where
```
```   381 "left \<Lambda> = \<Lambda>" |
```
```   382 "left (N _ _ t\<^isub>1 _) = t\<^isub>1"
```
```   383
```
```   384 primrec right where
```
```   385 "right \<Lambda> = \<Lambda>" |
```
```   386 "right (N _ _ _ t\<^isub>2) = t\<^isub>2"
```
```   387
```
```   388 fun wf where
```
```   389 "wf \<Lambda> = True" |
```
```   390 "wf (N _ k t u) =
```
```   391  (if t = \<Lambda> then
```
```   392     k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
```
```   393   else
```
```   394     wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
```
```   395
```
```   396 fun skew where
```
```   397 "skew \<Lambda> = \<Lambda>" |
```
```   398 "skew (N x k t u) =
```
```   399  (if t \<noteq> \<Lambda> \<and> k = level t then
```
```   400     N (data t) k (left t) (N x k (right t) u)
```
```   401   else
```
```   402     N x k t u)"
```
```   403
```
```   404 fun split where
```
```   405 "split \<Lambda> = \<Lambda>" |
```
```   406 "split (N x k t u) =
```
```   407  (if u \<noteq> \<Lambda> \<and> k = level (right u) then
```
```   408     N (data u) (Suc k) (N x k t (left u)) (right u)
```
```   409   else
```
```   410     N x k t u)"
```
```   411
```
```   412 theorem dataset_skew_split:
```
```   413 "dataset (skew t) = dataset t"
```
```   414 "dataset (split t) = dataset t"
```
```   415 nitpick
```
```   416 sorry
```
```   417
```
```   418 theorem wf_skew_split:
```
```   419 "wf t \<Longrightarrow> skew t = t"
```
```   420 "wf t \<Longrightarrow> split t = t"
```
```   421 nitpick
```
```   422 sorry
```
```   423
```
```   424 primrec insort\<^isub>1 where
```
```   425 "insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
```
```   426 "insort\<^isub>1 (N y k t u) x =
```
```   427  (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
```
```   428                              (if x > y then insort\<^isub>1 u x else u))"
```
```   429
```
```   430 theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
```
```   431 nitpick
```
```   432 oops
```
```   433
```
```   434 theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
```
```   435 nitpick [eval = "insort\<^isub>1 t x"]
```
```   436 oops
```
```   437
```
```   438 primrec insort\<^isub>2 where
```
```   439 "insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
```
```   440 "insort\<^isub>2 (N y k t u) x =
```
```   441  (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
```
```   442                        (if x > y then insort\<^isub>2 u x else u))"
```
```   443
```
```   444 theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
```
```   445 nitpick
```
```   446 sorry
```
```   447
```
```   448 theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
```
```   449 nitpick
```
```   450 sorry
```
```   451
```
```   452 end
```