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