src/HOL/ex/veriT_Preprocessing.thy
 author blanchet Fri Feb 10 08:27:27 2017 +0100 (2017-02-10) changeset 65016 c0ab0824ccb5 parent 64978 5b9ba120d222 child 65017 d11249edc2c2 permissions -rw-r--r--
tuning
```     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 = Node 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), Node (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    Node (Sko_Ex, [Node (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    Node (Cong, [Node (Sko_All, [Node (Bind, [Node (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    Node (Bind, [Node (Sko_Ex, [Node (Sko_Ex, [Node (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    Node (Bind, [Node (Sko_Ex, [Node (Sko_Ex, [Node (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    Node (Bind, [Node (Bind, [Node (Sko_Ex, [Node (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    Node (Bind, [Node (Cong, [Node (Refl, []), Node (Bind, [Node (Sko_Ex,
```
```   272      [Node (Refl, [])])])])]));
```
```   273
```
```   274 reconstruct_proof @{context} proof5
```
```   275 \<close>
```
```   276
```
```   277 ML \<open>
```
```   278 val proof6 =
```
```   279   ((@{term "\<not> (\<forall>x :: nat. p \<and> (\<exists>x :: nat. \<forall>x :: nat. q x x))"},
```
```   280     @{term "\<not> (\<forall>x :: nat. p \<and>
```
```   281         (\<exists>x :: nat. q (SOME x :: nat. \<not> q x x) (SOME x. \<not> q x x)))"}),
```
```   282    Node (Cong, [Node (Bind, [Node (Cong, [Node (Refl, []), Node (Bind, [Node (Sko_All,
```
```   283      [Node (Refl, [])])])])])]));
```
```   284
```
```   285 reconstruct_proof @{context} proof6
```
```   286 \<close>
```
```   287
```
```   288 ML \<open>
```
```   289 val proof7 =
```
```   290   ((@{term "\<not> \<not> (\<exists>x. p x)"},
```
```   291     @{term "\<not> \<not> p (SOME x. p x)"}),
```
```   292    Node (Cong, [Node (Cong, [Node (Sko_Ex, [Node (Refl, [])])])]));
```
```   293
```
```   294 reconstruct_proof @{context} proof7
```
```   295 \<close>
```
```   296
```
```   297 ML \<open>
```
```   298 val proof8 =
```
```   299   ((@{term "\<not> \<not> (let x = Suc x in x = 0)"},
```
```   300     @{term "\<not> \<not> Suc x = 0"}),
```
```   301    Node (Cong, [Node (Cong, [Node (Let [@{term "Suc x"}],
```
```   302      [Node (Refl, []), Node (Refl, [])])])]));
```
```   303
```
```   304 reconstruct_proof @{context} proof8
```
```   305 \<close>
```
```   306
```
```   307 ML \<open>
```
```   308 val proof9 =
```
```   309   ((@{term "\<not> (let x = Suc x in x = 0)"},
```
```   310     @{term "\<not> Suc x = 0"}),
```
```   311    Node (Cong, [Node (Let [@{term "Suc x"}], [Node (Refl, []), Node (Refl, [])])]));
```
```   312
```
```   313 reconstruct_proof @{context} proof9
```
```   314 \<close>
```
```   315
```
```   316 ML \<open>
```
```   317 val proof10 =
```
```   318   ((@{term "\<exists>x :: nat. p (x + 0)"},
```
```   319     @{term "\<exists>x :: nat. p x"}),
```
```   320    Node (Bind, [Node (Cong, [Node (Taut @{thm add_0_right}, [])])]));
```
```   321
```
```   322 reconstruct_proof @{context} proof10;
```
```   323 \<close>
```
```   324
```
```   325 ML \<open>
```
```   326 val proof11 =
```
```   327   ((@{term "\<not> (let (x, y) = (Suc y, Suc x) in y = 0)"},
```
```   328     @{term "\<not> Suc x = 0"}),
```
```   329    Node (Cong, [Node (Let [@{term "Suc y"}, @{term "Suc x"}],
```
```   330      [Node (Refl, []), Node (Refl, []), Node (Refl, [])])]));
```
```   331
```
```   332 reconstruct_proof @{context} proof11
```
```   333 \<close>
```
```   334
```
```   335 ML \<open>
```
```   336 val proof12 =
```
```   337   ((@{term "\<not> (let (x, y) = (Suc y, Suc x); (u, v, w) = (y, x, y) in w = 0)"},
```
```   338     @{term "\<not> Suc x = 0"}),
```
```   339    Node (Cong, [Node (Let [@{term "Suc y"}, @{term "Suc x"}],
```
```   340      [Node (Refl, []), Node (Refl, []),
```
```   341        Node (Let [@{term "Suc x"}, @{term "Suc y"}, @{term "Suc x"}],
```
```   342          [Node (Refl, []), Node (Refl, []), Node (Refl, []), Node (Refl, [])])])]));
```
```   343
```
```   344 reconstruct_proof @{context} proof12
```
```   345 \<close>
```
```   346
```
```   347 ML \<open>
```
```   348 val proof13 =
```
```   349   ((@{term "\<not> \<not> (let x = Suc x in x = 0)"},
```
```   350     @{term "\<not> \<not> Suc x = 0"}),
```
```   351    Node (Cong, [Node (Cong, [Node (Let [@{term "Suc x"}],
```
```   352      [Node (Refl, []), Node (Refl, [])])])]));
```
```   353
```
```   354 reconstruct_proof @{context} proof13
```
```   355 \<close>
```
```   356
```
```   357 ML \<open>
```
```   358 val proof14 =
```
```   359   ((@{term "let (x, y) = (f (a :: nat), b :: nat) in x > a"},
```
```   360     @{term "f (a :: nat) > a"}),
```
```   361    Node (Let [@{term "f (a :: nat) :: nat"}, @{term "b :: nat"}],
```
```   362      [Node (Cong, [Node (Refl, [])]), Node (Refl, []), Node (Refl, [])]));
```
```   363
```
```   364 reconstruct_proof @{context} proof14
```
```   365 \<close>
```
```   366
```
```   367 ML \<open>
```
```   368 val proof15 =
```
```   369   ((@{term "let x = (let y = g (z :: nat) in f (y :: nat)) in x = Suc 0"},
```
```   370     @{term "f (g (z :: nat) :: nat) = Suc 0"}),
```
```   371    Node (Let [@{term "f (g (z :: nat) :: nat) :: nat"}],
```
```   372      [Node (Let [@{term "g (z :: nat) :: nat"}], [Node (Refl, []), Node (Refl, [])]),
```
```   373       Node (Refl, [])]));
```
```   374
```
```   375 reconstruct_proof @{context} proof15
```
```   376 \<close>
```
```   377
```
```   378 ML \<open>
```
```   379 val proof16 =
```
```   380   ((@{term "a > Suc b"},
```
```   381     @{term "a > Suc b"}),
```
```   382    Node (Trans @{term "a > Suc b"}, [Node (Refl, []), Node (Refl, [])]));
```
```   383
```
```   384 reconstruct_proof @{context} proof16
```
```   385 \<close>
```
```   386
```
```   387 thm Suc_1
```
```   388 thm numeral_2_eq_2
```
```   389 thm One_nat_def
```
```   390
```
```   391 ML \<open>
```
```   392 val proof17 =
```
```   393   ((@{term "2 :: nat"},
```
```   394     @{term "Suc (Suc 0) :: nat"}),
```
```   395    Node (Trans @{term "Suc 1"}, [Node (Taut @{thm Suc_1[symmetric]}, []),
```
```   396      Node (Cong, [Node (Taut @{thm One_nat_def}, [])])]));
```
```   397
```
```   398 reconstruct_proof @{context} proof17
```
```   399 \<close>
```
```   400
```
```   401 ML \<open>
```
```   402 val proof18 =
```
```   403   ((@{term "let x = a in let y = b in Suc x + y"},
```
```   404     @{term "Suc a + b"}),
```
```   405    Node (Trans @{term "let y = b in Suc a + y"},
```
```   406      [Node (Let [@{term "a :: nat"}], [Node (Refl, []), Node (Refl, [])]),
```
```   407       Node (Let [@{term "b :: nat"}], [Node (Refl, []), Node (Refl, [])])]));
```
```   408
```
```   409 reconstruct_proof @{context} proof18
```
```   410 \<close>
```
```   411
```
```   412 ML \<open>
```
```   413 val proof19 =
```
```   414   ((@{term "\<forall>x. let x = f (x :: nat) :: nat in g x"},
```
```   415     @{term "\<forall>x. g (f (x :: nat) :: nat)"}),
```
```   416    Node (Bind, [Node (Let [@{term "f :: nat \<Rightarrow> nat"} \$ Bound 0],
```
```   417      [Node (Refl, []), Node (Refl, [])])]));
```
```   418
```
```   419 reconstruct_proof @{context} proof19
```
```   420 \<close>
```
```   421
```
```   422 ML \<open>
```
```   423 val proof20 =
```
```   424   ((@{term "\<forall>x. let y = Suc 0 in let x = f (x :: nat) :: nat in g x"},
```
```   425     @{term "\<forall>x. g (f (x :: nat) :: nat)"}),
```
```   426    Node (Bind, [Node (Let [@{term "Suc 0"}],
```
```   427      [Node (Refl, []), Node (Let [@{term "f (x :: nat) :: nat"}],
```
```   428         [Node (Refl, []), Node (Refl, [])])])]));
```
```   429
```
```   430 reconstruct_proof @{context} proof20
```
```   431 \<close>
```
```   432
```
```   433 ML \<open>
```
```   434 val proof21 =
```
```   435   ((@{term "\<forall>x :: nat. let x = f x :: nat in let y = x in p y"},
```
```   436     @{term "\<forall>z :: nat. p (f z :: nat)"}),
```
```   437    Node (Bind, [Node (Let [@{term "f (z :: nat) :: nat"}],
```
```   438      [Node (Refl, []), Node (Let [@{term "f (z :: nat) :: nat"}],
```
```   439         [Node (Refl, []), Node (Refl, [])])])]));
```
```   440
```
```   441 reconstruct_proof @{context} proof21
```
```   442 \<close>
```
```   443
```
```   444 ML \<open>
```
```   445 val proof22 =
```
```   446   ((@{term "\<forall>x :: nat. let x = f x :: nat in let y = x in p y"},
```
```   447     @{term "\<forall>x :: nat. p (f x :: nat)"}),
```
```   448    Node (Bind, [Node (Let [@{term "f (x :: nat) :: nat"}],
```
```   449      [Node (Refl, []), Node (Let [@{term "f (x :: nat) :: nat"}],
```
```   450         [Node (Refl, []), Node (Refl, [])])])]));
```
```   451
```
```   452 reconstruct_proof @{context} proof22
```
```   453 \<close>
```
```   454
```
```   455 ML \<open>
```
```   456 val proof23 =
```
```   457   ((@{term "\<forall>x :: nat. let (x, a) = (f x :: nat, 0 ::nat) in let y = x in p y"},
```
```   458     @{term "\<forall>z :: nat. p (f z :: nat)"}),
```
```   459    Node (Bind, [Node (Let [@{term "f (z :: nat) :: nat"}, @{term "0 :: nat"}],
```
```   460      [Node (Refl, []), Node (Refl, []), Node (Let [@{term "f (z :: nat) :: nat"}],
```
```   461         [Node (Refl, []), Node (Refl, [])])])]));
```
```   462
```
```   463 reconstruct_proof @{context} proof23
```
```   464 \<close>
```
```   465
```
```   466 ML \<open>
```
```   467 val proof24 =
```
```   468   ((@{term "\<forall>x :: nat. let (x, a) = (f x :: nat, 0 ::nat) in let y = x in p y"},
```
```   469     @{term "\<forall>x :: nat. p (f x :: nat)"}),
```
```   470    Node (Bind, [Node (Let [@{term "f (x :: nat) :: nat"}, @{term "0 :: nat"}],
```
```   471      [Node (Refl, []), Node (Refl, []), Node (Let [@{term "f (x :: nat) :: nat"}],
```
```   472         [Node (Refl, []), Node (Refl, [])])])]));
```
```   473
```
```   474 reconstruct_proof @{context} proof24
```
```   475 \<close>
```
```   476
```
```   477 end
```