src/HOL/ex/veriT_Preprocessing.thy
author fleury <Mathias.Fleury@mpi-inf.mpg.de>
Tue Feb 14 18:32:53 2017 +0100 (21 months ago)
changeset 65029 00731700e54f
parent 65016 c0ab0824ccb5
child 69217 a8c707352ccc
permissions -rw-r--r--
cancellation simprocs generalising the multiset simprocs
     1 (*  Title:      HOL/ex/veriT_Preprocessing.thy
     2     Author:     Jasmin Christian Blanchette, Inria, LORIA, MPII
     3 *)
     4 
     5 section \<open>Proof Reconstruction for veriT's Preprocessing\<close>
     6 
     7 theory veriT_Preprocessing
     8 imports Main
     9 begin
    10 
    11 declare [[eta_contract = false]]
    12 
    13 lemma
    14   some_All_iffI: "p (SOME x. \<not> p x) = q \<Longrightarrow> (\<forall>x. p x) = q" and
    15   some_Ex_iffI: "p (SOME x. p x) = q \<Longrightarrow> (\<exists>x. p x) = q"
    16   by (metis (full_types) someI_ex)+
    17 
    18 ML \<open>
    19 fun mk_prod1 bound_Ts (t, u) =
    20   HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
    21 
    22 fun mk_tuple1 bound_Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 bound_Ts));
    23 
    24 fun mk_arg_congN 0 = refl
    25   | mk_arg_congN 1 = arg_cong
    26   | mk_arg_congN 2 = @{thm arg_cong2}
    27   | mk_arg_congN n = arg_cong RS funpow (n - 2) (fn th => @{thm cong} RS th) @{thm cong};
    28 
    29 fun mk_let_iffNI ctxt n =
    30   let
    31     val ((As, [B]), _) = ctxt
    32       |> Ctr_Sugar_Util.mk_TFrees n
    33       ||>> Ctr_Sugar_Util.mk_TFrees 1;
    34 
    35     val ((((ts, us), [p]), [q]), _) = ctxt
    36       |> Ctr_Sugar_Util.mk_Frees "t" As
    37       ||>> Ctr_Sugar_Util.mk_Frees "u" As
    38       ||>> Ctr_Sugar_Util.mk_Frees "p" [As ---> B]
    39       ||>> Ctr_Sugar_Util.mk_Frees "q" [B];
    40 
    41     val tuple_t = HOLogic.mk_tuple ts;
    42     val tuple_T = fastype_of tuple_t;
    43 
    44     val lambda_t = HOLogic.tupled_lambda tuple_t (list_comb (p, ts));
    45     val lambda_T = fastype_of lambda_t;
    46 
    47     val left_prems = map2 (curry Ctr_Sugar_Util.mk_Trueprop_eq) ts us;
    48     val right_prem = Ctr_Sugar_Util.mk_Trueprop_eq (list_comb (p, us), q);
    49     val concl = Ctr_Sugar_Util.mk_Trueprop_eq
    50       (Const (@{const_name Let}, tuple_T --> lambda_T --> B) $ tuple_t $ lambda_t, q);
    51 
    52     val goal = Logic.list_implies (left_prems @ [right_prem], concl);
    53     val vars = Variable.add_free_names ctxt goal [];
    54   in
    55     Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} =>
    56       HEADGOAL (hyp_subst_tac ctxt) THEN
    57       Local_Defs.unfold0_tac ctxt @{thms Let_def prod.case} THEN
    58       HEADGOAL (resolve_tac ctxt [refl]))
    59   end;
    60 
    61 datatype rule_name =
    62   Refl
    63 | Taut of thm
    64 | Trans of term
    65 | Cong
    66 | Bind
    67 | Sko_Ex
    68 | Sko_All
    69 | Let of term list;
    70 
    71 fun str_of_rule_name Refl = "Refl"
    72   | str_of_rule_name (Taut th) = "Taut[" ^ @{make_string} th ^ "]"
    73   | str_of_rule_name (Trans t) = "Trans[" ^ Syntax.string_of_term @{context} t ^ "]"
    74   | str_of_rule_name Cong = "Cong"
    75   | str_of_rule_name Bind = "Bind"
    76   | str_of_rule_name Sko_Ex = "Sko_Ex"
    77   | str_of_rule_name Sko_All = "Sko_All"
    78   | str_of_rule_name (Let ts) =
    79     "Let[" ^ commas (map (Syntax.string_of_term @{context}) ts) ^ "]";
    80 
    81 datatype node = N of rule_name * node list;
    82 
    83 fun lambda_count (Abs (_, _, t)) = lambda_count t + 1
    84   | lambda_count ((t as Abs _) $ _) = lambda_count t - 1
    85   | lambda_count ((t as Const (@{const_name case_prod}, _) $ _) $ _) = lambda_count t - 1
    86   | lambda_count (Const (@{const_name case_prod}, _) $ t) = lambda_count t - 1
    87   | lambda_count _ = 0;
    88 
    89 fun zoom apply =
    90   let
    91     fun zo 0 bound_Ts (Abs (r, T, t), Abs (s, U, u)) =
    92         let val (t', u') = zo 0 (T :: bound_Ts) (t, u) in
    93           (lambda (Free (r, T)) t', lambda (Free (s, U)) u')
    94         end
    95       | zo 0 bound_Ts ((t as Abs (_, T, _)) $ arg, u) =
    96         let val (t', u') = zo 1 (T :: bound_Ts) (t, u) in
    97           (t' $ arg, u')
    98         end
    99       | zo 0 bound_Ts ((t as Const (@{const_name case_prod}, _) $ _) $ arg, u) =
   100         let val (t', u') = zo 1 bound_Ts (t, u) in
   101           (t' $ arg, u')
   102         end
   103       | zo 0 bound_Ts tu = apply bound_Ts tu
   104       | zo n bound_Ts (Const (@{const_name case_prod},
   105           Type (@{type_name fun}, [Type (@{type_name fun}, [A, Type (@{type_name fun}, [B, _])]),
   106             Type (@{type_name fun}, [AB, _])])) $ t, u) =
   107         let
   108           val (t', u') = zo (n + 1) bound_Ts (t, u);
   109           val C = range_type (range_type (fastype_of t'));
   110         in
   111           (Const (@{const_name case_prod}, (A --> B --> C) --> AB --> C) $ t', u')
   112         end
   113       | zo n bound_Ts (Abs (s, T, t), u) =
   114         let val (t', u') = zo (n - 1) (T :: bound_Ts) (t, u) in
   115           (Abs (s, T, t'), u')
   116         end
   117       | zo _ _ (t, u) = raise TERM ("zoom", [t, u]);
   118   in
   119     zo 0 []
   120   end;
   121 
   122 fun apply_Trans_left t (lhs, _) = (lhs, t);
   123 fun apply_Trans_right t (_, rhs) = (t, rhs);
   124 
   125 fun apply_Cong ary j (lhs, rhs) =
   126   (case apply2 strip_comb (lhs, rhs) of
   127     ((c, ts), (d, us)) =>
   128     if c aconv d andalso length ts = ary andalso length us = ary then (nth ts j, nth us j)
   129     else raise TERM ("apply_Cong", [lhs, rhs]));
   130 
   131 fun apply_Bind (lhs, rhs) =
   132   (case (lhs, rhs) of
   133     (Const (@{const_name All}, _) $ Abs (_, T, t), Const (@{const_name All}, _) $ Abs (s, U, u)) =>
   134     (Abs (s, T, t), Abs (s, U, u))
   135   | (Const (@{const_name Ex}, _) $ t, Const (@{const_name Ex}, _) $ u) => (t, u)
   136   | _ => raise TERM ("apply_Bind", [lhs, rhs]));
   137 
   138 fun apply_Sko_Ex (lhs, rhs) =
   139   (case lhs of
   140     Const (@{const_name Ex}, _) $ (t as Abs (_, T, _)) =>
   141     (t $ (HOLogic.choice_const T $ t), rhs)
   142   | _ => raise TERM ("apply_Sko_Ex", [lhs]));
   143 
   144 fun apply_Sko_All (lhs, rhs) =
   145   (case lhs of
   146     Const (@{const_name All}, _) $ (t as Abs (s, T, body)) =>
   147     (t $ (HOLogic.choice_const T $ Abs (s, T, HOLogic.mk_not body)), rhs)
   148   | _ => raise TERM ("apply_Sko_All", [lhs]));
   149 
   150 fun apply_Let_left ts j (lhs, _) =
   151   (case lhs of
   152     Const (@{const_name Let}, _) $ t $ _ =>
   153     let val ts0 = HOLogic.strip_tuple t in
   154       (nth ts0 j, nth ts j)
   155     end
   156   | _ => raise TERM ("apply_Let_left", [lhs]));
   157 
   158 fun apply_Let_right ts bound_Ts (lhs, rhs) =
   159   let val t' = mk_tuple1 bound_Ts ts in
   160     (case lhs of
   161       Const (@{const_name Let}, _) $ _ $ u => (u $ t', rhs)
   162     | _ => raise TERM ("apply_Let_right", [lhs, rhs]))
   163   end;
   164 
   165 fun reconstruct_proof ctxt (lrhs as (_, rhs), N (rule_name, prems)) =
   166   let
   167     val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq lrhs);
   168     val ary = length prems;
   169 
   170     val _ = warning (Syntax.string_of_term @{context} goal);
   171     val _ = warning (str_of_rule_name rule_name);
   172 
   173     val parents =
   174       (case (rule_name, prems) of
   175         (Refl, []) => []
   176       | (Taut _, []) => []
   177       | (Trans t, [left_prem, right_prem]) =>
   178         [reconstruct_proof ctxt (zoom (K (apply_Trans_left t)) lrhs, left_prem),
   179          reconstruct_proof ctxt (zoom (K (apply_Trans_right t)) (rhs, rhs), right_prem)]
   180       | (Cong, _) =>
   181         map_index (fn (j, prem) => reconstruct_proof ctxt (zoom (K (apply_Cong ary j)) lrhs, prem))
   182           prems
   183       | (Bind, [prem]) => [reconstruct_proof ctxt (zoom (K apply_Bind) lrhs, prem)]
   184       | (Sko_Ex, [prem]) => [reconstruct_proof ctxt (zoom (K apply_Sko_Ex) lrhs, prem)]
   185       | (Sko_All, [prem]) => [reconstruct_proof ctxt (zoom (K apply_Sko_All) lrhs, prem)]
   186       | (Let ts, prems) =>
   187         let val (left_prems, right_prem) = split_last prems in
   188           map2 (fn j => fn prem =>
   189               reconstruct_proof ctxt (zoom (K (apply_Let_left ts j)) lrhs, prem))
   190             (0 upto length left_prems - 1) left_prems @
   191           [reconstruct_proof ctxt (zoom (apply_Let_right ts) lrhs, right_prem)]
   192         end
   193       | _ => raise Fail ("Invalid rule: " ^ str_of_rule_name rule_name ^ "/" ^
   194           string_of_int (length prems)));
   195 
   196     val rule_thms =
   197       (case rule_name of
   198         Refl => [refl]
   199       | Taut th => [th]
   200       | Trans _ => [trans]
   201       | Cong => [mk_arg_congN ary]
   202       | Bind => @{thms arg_cong[of _ _ All] arg_cong[of _ _ Ex]}
   203       | Sko_Ex => [@{thm some_Ex_iffI}]
   204       | Sko_All => [@{thm some_All_iffI}]
   205       | Let ts => [mk_let_iffNI ctxt (length ts)]);
   206 
   207     val num_lams = lambda_count rhs;
   208     val conged_parents = map (funpow num_lams (fn th => th RS fun_cong)
   209       #> Local_Defs.unfold0 ctxt @{thms prod.case}) parents;
   210   in
   211     Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, ...} =>
   212       Local_Defs.unfold0_tac ctxt @{thms prod.case} THEN
   213       HEADGOAL (REPEAT_DETERM_N num_lams o resolve_tac ctxt [ext] THEN'
   214       resolve_tac ctxt rule_thms THEN'
   215       K (Local_Defs.unfold0_tac ctxt @{thms prod.case}) THEN'
   216       EVERY' (map (resolve_tac ctxt o single) conged_parents)))
   217   end;
   218 \<close>
   219 
   220 ML \<open>
   221 val proof0 =
   222   ((@{term "\<exists>x :: nat. p x"},
   223     @{term "p (SOME x :: nat. p x)"}),
   224    N (Sko_Ex, [N (Refl, [])]));
   225 
   226 reconstruct_proof @{context} proof0;
   227 \<close>
   228 
   229 ML \<open>
   230 val proof1 =
   231   ((@{term "\<not> (\<forall>x :: nat. \<exists>y :: nat. p x y)"},
   232     @{term "\<not> (\<exists>y :: nat. p (SOME x :: nat. \<not> (\<exists>y :: nat. p x y)) y)"}),
   233    N (Cong, [N (Sko_All, [N (Bind, [N (Refl, [])])])]));
   234 
   235 reconstruct_proof @{context} proof1;
   236 \<close>
   237 
   238 ML \<open>
   239 val proof2 =
   240   ((@{term "\<forall>x :: nat. \<exists>y :: nat. \<exists>z :: nat. p x y z"},
   241     @{term "\<forall>x :: nat. p x (SOME y :: nat. \<exists>z :: nat. p x y z)
   242         (SOME z :: nat. p x (SOME y :: nat. \<exists>z :: nat. p x y z) z)"}),
   243    N (Bind, [N (Sko_Ex, [N (Sko_Ex, [N (Refl, [])])])]));
   244 
   245 reconstruct_proof @{context} proof2
   246 \<close>
   247 
   248 ML \<open>
   249 val proof3 =
   250   ((@{term "\<forall>x :: nat. \<exists>x :: nat. \<exists>x :: nat. p x x x"},
   251     @{term "\<forall>x :: nat. p (SOME x :: nat. p x x x) (SOME x. p x x x) (SOME x. p x x x)"}),
   252    N (Bind, [N (Sko_Ex, [N (Sko_Ex, [N (Refl, [])])])]));
   253 
   254 reconstruct_proof @{context} proof3
   255 \<close>
   256 
   257 ML \<open>
   258 val proof4 =
   259   ((@{term "\<forall>x :: nat. \<exists>x :: nat. \<exists>x :: nat. p x x x"},
   260     @{term "\<forall>x :: nat. \<exists>x :: nat. p (SOME x :: nat. p x x x) (SOME x. p x x x) (SOME x. p x x x)"}),
   261    N (Bind, [N (Bind, [N (Sko_Ex, [N (Refl, [])])])]));
   262 
   263 reconstruct_proof @{context} proof4
   264 \<close>
   265 
   266 ML \<open>
   267 val proof5 =
   268   ((@{term "\<forall>x :: nat. q \<and> (\<exists>x :: nat. \<exists>x :: nat. p x x x)"},
   269     @{term "\<forall>x :: nat. q \<and>
   270         (\<exists>x :: nat. p (SOME x :: nat. p x x x) (SOME x. p x x x) (SOME x. p x x x))"}),
   271    N (Bind, [N (Cong, [N (Refl, []), N (Bind, [N (Sko_Ex, [N (Refl, [])])])])]));
   272 
   273 reconstruct_proof @{context} proof5
   274 \<close>
   275 
   276 ML \<open>
   277 val proof6 =
   278   ((@{term "\<not> (\<forall>x :: nat. p \<and> (\<exists>x :: nat. \<forall>x :: nat. q x x))"},
   279     @{term "\<not> (\<forall>x :: nat. p \<and>
   280         (\<exists>x :: nat. q (SOME x :: nat. \<not> q x x) (SOME x. \<not> q x x)))"}),
   281    N (Cong, [N (Bind, [N (Cong, [N (Refl, []), N (Bind, [N (Sko_All, [N (Refl, [])])])])])]));
   282 
   283 reconstruct_proof @{context} proof6
   284 \<close>
   285 
   286 ML \<open>
   287 val proof7 =
   288   ((@{term "\<not> \<not> (\<exists>x. p x)"},
   289     @{term "\<not> \<not> p (SOME x. p x)"}),
   290    N (Cong, [N (Cong, [N (Sko_Ex, [N (Refl, [])])])]));
   291 
   292 reconstruct_proof @{context} proof7
   293 \<close>
   294 
   295 ML \<open>
   296 val proof8 =
   297   ((@{term "\<not> \<not> (let x = Suc x in x = 0)"},
   298     @{term "\<not> \<not> Suc x = 0"}),
   299    N (Cong, [N (Cong, [N (Let [@{term "Suc x"}], [N (Refl, []), N (Refl, [])])])]));
   300 
   301 reconstruct_proof @{context} proof8
   302 \<close>
   303 
   304 ML \<open>
   305 val proof9 =
   306   ((@{term "\<not> (let x = Suc x in x = 0)"},
   307     @{term "\<not> Suc x = 0"}),
   308    N (Cong, [N (Let [@{term "Suc x"}], [N (Refl, []), N (Refl, [])])]));
   309 
   310 reconstruct_proof @{context} proof9
   311 \<close>
   312 
   313 ML \<open>
   314 val proof10 =
   315   ((@{term "\<exists>x :: nat. p (x + 0)"},
   316     @{term "\<exists>x :: nat. p x"}),
   317    N (Bind, [N (Cong, [N (Taut @{thm add_0_right}, [])])]));
   318 
   319 reconstruct_proof @{context} proof10;
   320 \<close>
   321 
   322 ML \<open>
   323 val proof11 =
   324   ((@{term "\<not> (let (x, y) = (Suc y, Suc x) in y = 0)"},
   325     @{term "\<not> Suc x = 0"}),
   326    N (Cong, [N (Let [@{term "Suc y"}, @{term "Suc x"}], [N (Refl, []), N (Refl, []),
   327      N (Refl, [])])]));
   328 
   329 reconstruct_proof @{context} proof11
   330 \<close>
   331 
   332 ML \<open>
   333 val proof12 =
   334   ((@{term "\<not> (let (x, y) = (Suc y, Suc x); (u, v, w) = (y, x, y) in w = 0)"},
   335     @{term "\<not> Suc x = 0"}),
   336    N (Cong, [N (Let [@{term "Suc y"}, @{term "Suc x"}], [N (Refl, []), N (Refl, []),
   337      N (Let [@{term "Suc x"}, @{term "Suc y"}, @{term "Suc x"}],
   338        [N (Refl, []), N (Refl, []), N (Refl, []), N (Refl, [])])])]));
   339 
   340 reconstruct_proof @{context} proof12
   341 \<close>
   342 
   343 ML \<open>
   344 val proof13 =
   345   ((@{term "\<not> \<not> (let x = Suc x in x = 0)"},
   346     @{term "\<not> \<not> Suc x = 0"}),
   347    N (Cong, [N (Cong, [N (Let [@{term "Suc x"}], [N (Refl, []), N (Refl, [])])])]));
   348 
   349 reconstruct_proof @{context} proof13
   350 \<close>
   351 
   352 ML \<open>
   353 val proof14 =
   354   ((@{term "let (x, y) = (f (a :: nat), b :: nat) in x > a"},
   355     @{term "f (a :: nat) > a"}),
   356    N (Let [@{term "f (a :: nat) :: nat"}, @{term "b :: nat"}],
   357      [N (Cong, [N (Refl, [])]), N (Refl, []), N (Refl, [])]));
   358 
   359 reconstruct_proof @{context} proof14
   360 \<close>
   361 
   362 ML \<open>
   363 val proof15 =
   364   ((@{term "let x = (let y = g (z :: nat) in f (y :: nat)) in x = Suc 0"},
   365     @{term "f (g (z :: nat) :: nat) = Suc 0"}),
   366    N (Let [@{term "f (g (z :: nat) :: nat) :: nat"}],
   367      [N (Let [@{term "g (z :: nat) :: nat"}], [N (Refl, []), N (Refl, [])]), N (Refl, [])]));
   368 
   369 reconstruct_proof @{context} proof15
   370 \<close>
   371 
   372 ML \<open>
   373 val proof16 =
   374   ((@{term "a > Suc b"},
   375     @{term "a > Suc b"}),
   376    N (Trans @{term "a > Suc b"}, [N (Refl, []), N (Refl, [])]));
   377 
   378 reconstruct_proof @{context} proof16
   379 \<close>
   380 
   381 thm Suc_1
   382 thm numeral_2_eq_2
   383 thm One_nat_def
   384 
   385 ML \<open>
   386 val proof17 =
   387   ((@{term "2 :: nat"},
   388     @{term "Suc (Suc 0) :: nat"}),
   389    N (Trans @{term "Suc 1"}, [N (Taut @{thm Suc_1[symmetric]}, []), N (Cong,
   390      [N (Taut @{thm One_nat_def}, [])])]));
   391 
   392 reconstruct_proof @{context} proof17
   393 \<close>
   394 
   395 ML \<open>
   396 val proof18 =
   397   ((@{term "let x = a in let y = b in Suc x + y"},
   398     @{term "Suc a + b"}),
   399    N (Trans @{term "let y = b in Suc a + y"},
   400      [N (Let [@{term "a :: nat"}], [N (Refl, []), N (Refl, [])]),
   401       N (Let [@{term "b :: nat"}], [N (Refl, []), N (Refl, [])])]));
   402 
   403 reconstruct_proof @{context} proof18
   404 \<close>
   405 
   406 ML \<open>
   407 val proof19 =
   408   ((@{term "\<forall>x. let x = f (x :: nat) :: nat in g x"},
   409     @{term "\<forall>x. g (f (x :: nat) :: nat)"}),
   410    N (Bind, [N (Let [@{term "f :: nat \<Rightarrow> nat"} $ Bound 0],
   411      [N (Refl, []), N (Refl, [])])]));
   412 
   413 reconstruct_proof @{context} proof19
   414 \<close>
   415 
   416 ML \<open>
   417 val proof20 =
   418   ((@{term "\<forall>x. let y = Suc 0 in let x = f (x :: nat) :: nat in g x"},
   419     @{term "\<forall>x. g (f (x :: nat) :: nat)"}),
   420    N (Bind, [N (Let [@{term "Suc 0"}], [N (Refl, []), N (Let [@{term "f (x :: nat) :: nat"}],
   421      [N (Refl, []), N (Refl, [])])])]));
   422 
   423 reconstruct_proof @{context} proof20
   424 \<close>
   425 
   426 ML \<open>
   427 val proof21 =
   428   ((@{term "\<forall>x :: nat. let x = f x :: nat in let y = x in p y"},
   429     @{term "\<forall>z :: nat. p (f z :: nat)"}),
   430    N (Bind, [N (Let [@{term "f (z :: nat) :: nat"}],
   431      [N (Refl, []), N (Let [@{term "f (z :: nat) :: nat"}],
   432        [N (Refl, []), N (Refl, [])])])]));
   433 
   434 reconstruct_proof @{context} proof21
   435 \<close>
   436 
   437 ML \<open>
   438 val proof22 =
   439   ((@{term "\<forall>x :: nat. let x = f x :: nat in let y = x in p y"},
   440     @{term "\<forall>x :: nat. p (f x :: nat)"}),
   441    N (Bind, [N (Let [@{term "f (x :: nat) :: nat"}],
   442      [N (Refl, []), N (Let [@{term "f (x :: nat) :: nat"}],
   443        [N (Refl, []), N (Refl, [])])])]));
   444 
   445 reconstruct_proof @{context} proof22
   446 \<close>
   447 
   448 ML \<open>
   449 val proof23 =
   450   ((@{term "\<forall>x :: nat. let (x, a) = (f x :: nat, 0 ::nat) in let y = x in p y"},
   451     @{term "\<forall>z :: nat. p (f z :: nat)"}),
   452    N (Bind, [N (Let [@{term "f (z :: nat) :: nat"}, @{term "0 :: nat"}],
   453      [N (Refl, []), N (Refl, []), N (Let [@{term "f (z :: nat) :: nat"}],
   454        [N (Refl, []), N (Refl, [])])])]));
   455 
   456 reconstruct_proof @{context} proof23
   457 \<close>
   458 
   459 ML \<open>
   460 val proof24 =
   461   ((@{term "\<forall>x :: nat. let (x, a) = (f x :: nat, 0 ::nat) in let y = x in p y"},
   462     @{term "\<forall>x :: nat. p (f x :: nat)"}),
   463    N (Bind, [N (Let [@{term "f (x :: nat) :: nat"}, @{term "0 :: nat"}],
   464      [N (Refl, []), N (Refl, []), N (Let [@{term "f (x :: nat) :: nat"}],
   465        [N (Refl, []), N (Refl, [])])])]));
   466 
   467 reconstruct_proof @{context} proof24
   468 \<close>
   469 
   470 end