src/HOL/ex/veriT_Preprocessing.thy
 author blanchet Thu Nov 01 09:25:58 2018 +0100 (5 months ago) changeset 69217 a8c707352ccc parent 65017 d11249edc2c2 child 69220 c6b15fc78f78 permissions -rw-r--r--
```     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 ML \<open>
```
```   471 val proof25 =
```
```   472   ((@{term "let vr0 = vr1 in let vr1 = vr2 in vr0 + vr1 + vr2 :: nat"},
```
```   473     @{term "vr1 + vr2 + vr2 :: nat"}),
```
```   474    N (Trans @{term "let vr1a = vr2 in vr1 + vr1a + vr2 :: nat"},
```
```   475      [N (Let [@{term "vr1 :: nat"}], [N (Refl, []), N (Refl, [])]),
```
```   476       N (Let [@{term "vr2 :: nat"}], [N (Refl, []), N (Refl, [])])]));
```
```   477
```
```   478 reconstruct_proof @{context} proof18
```
```   479 \<close>
```
```   480
```
```   481 end
```