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