src/Pure/Proof/proof_checker.ML
author wenzelm
Fri Oct 07 21:16:48 2016 +0200 (2016-10-07)
changeset 64092 95469c544b82
parent 60642 48dd1cefb4ae
child 70412 64ead6de6212
permissions -rw-r--r--
accept obscure timezone used in 2011;
wenzelm@45007
     1
(*  Title:      Pure/Proof/proof_checker.ML
wenzelm@11539
     2
    Author:     Stefan Berghofer, TU Muenchen
berghofe@11522
     3
berghofe@11522
     4
Simple proof checker based only on the core inference rules
berghofe@11522
     5
of Isabelle/Pure.
berghofe@11522
     6
*)
berghofe@11522
     7
berghofe@11522
     8
signature PROOF_CHECKER =
berghofe@11522
     9
sig
berghofe@11522
    10
  val thm_of_proof : theory -> Proofterm.proof -> thm
berghofe@11522
    11
end;
berghofe@11522
    12
wenzelm@44057
    13
structure Proof_Checker : PROOF_CHECKER =
berghofe@11522
    14
struct
berghofe@11522
    15
berghofe@11522
    16
(***** construct a theorem out of a proof term *****)
berghofe@11522
    17
berghofe@11522
    18
fun lookup_thm thy =
wenzelm@56161
    19
  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy true) Symtab.empty in
wenzelm@44057
    20
    fn s =>
wenzelm@44057
    21
      (case Symtab.lookup tab s of
wenzelm@44057
    22
        NONE => error ("Unknown theorem " ^ quote s)
wenzelm@44057
    23
      | SOME thm => thm)
berghofe@11522
    24
  end;
berghofe@11522
    25
berghofe@13733
    26
val beta_eta_convert =
wenzelm@22910
    27
  Conv.fconv_rule Drule.beta_eta_conversion;
berghofe@11522
    28
berghofe@37229
    29
(* equality modulo renaming of type variables *)
berghofe@37229
    30
fun is_equal t t' =
berghofe@37229
    31
  let
berghofe@37229
    32
    val atoms = fold_types (fold_atyps (insert (op =))) t [];
berghofe@37229
    33
    val atoms' = fold_types (fold_atyps (insert (op =))) t' []
berghofe@37229
    34
  in
berghofe@37229
    35
    length atoms = length atoms' andalso
berghofe@37229
    36
    map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
berghofe@37229
    37
  end;
berghofe@37229
    38
berghofe@37229
    39
fun pretty_prf thy vs Hs prf =
wenzelm@37310
    40
  let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
wenzelm@59582
    41
    Proofterm.prf_subst_pbounds (map (Hyp o Thm.prop_of) Hs)
berghofe@37229
    42
  in
berghofe@37229
    43
    (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
berghofe@37229
    44
     Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
berghofe@37229
    45
  end;
berghofe@37229
    46
berghofe@37229
    47
fun pretty_term thy vs _ t =
berghofe@37229
    48
  let val t' = subst_bounds (map Free vs, t)
berghofe@37229
    49
  in
berghofe@37229
    50
    (Syntax.pretty_term_global thy t',
berghofe@37229
    51
     Syntax.pretty_typ_global thy (fastype_of t'))
berghofe@37229
    52
  end;
berghofe@37229
    53
berghofe@37229
    54
fun appl_error thy prt vs Hs s f a =
berghofe@37229
    55
  let
berghofe@37229
    56
    val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
berghofe@37229
    57
    val (pp_a, pp_aT) = prt thy vs Hs a
berghofe@37229
    58
  in
berghofe@37229
    59
    error (cat_lines
berghofe@37229
    60
      [s,
berghofe@37229
    61
       "",
berghofe@37229
    62
       Pretty.string_of (Pretty.block
berghofe@37229
    63
         [Pretty.str "Operator:", Pretty.brk 2, pp_f,
berghofe@37229
    64
           Pretty.str " ::", Pretty.brk 1, pp_fT]),
berghofe@37229
    65
       Pretty.string_of (Pretty.block
berghofe@37229
    66
         [Pretty.str "Operand:", Pretty.brk 3, pp_a,
berghofe@37229
    67
           Pretty.str " ::", Pretty.brk 1, pp_aT]),
berghofe@37229
    68
       ""])
berghofe@37229
    69
  end;
berghofe@37229
    70
wenzelm@44061
    71
fun thm_of_proof thy =
wenzelm@44061
    72
  let val lookup = lookup_thm thy in
wenzelm@44061
    73
    fn prf =>
berghofe@13670
    74
      let
wenzelm@44061
    75
        val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
berghofe@13670
    76
wenzelm@44061
    77
        fun thm_of_atom thm Ts =
berghofe@11522
    78
          let
wenzelm@44061
    79
            val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
wenzelm@44061
    80
            val (fmap, thm') = Thm.varifyT_global' [] thm;
wenzelm@60642
    81
            val ctye =
wenzelm@60642
    82
              (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
berghofe@11522
    83
          in
wenzelm@44061
    84
            Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
wenzelm@44061
    85
          end;
berghofe@11522
    86
wenzelm@44061
    87
        fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
wenzelm@44061
    88
              let
wenzelm@44061
    89
                val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
wenzelm@44061
    90
                val prop = Thm.prop_of thm;
wenzelm@44061
    91
                val _ =
wenzelm@44061
    92
                  if is_equal prop prop' then ()
wenzelm@44061
    93
                  else
wenzelm@44061
    94
                    error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
wenzelm@44061
    95
                      Syntax.string_of_term_global thy prop ^ "\n\n" ^
wenzelm@44061
    96
                      Syntax.string_of_term_global thy prop');
wenzelm@44061
    97
              in thm_of_atom thm Ts end
wenzelm@44061
    98
wenzelm@44061
    99
          | thm_of _ _ (PAxm (name, _, SOME Ts)) =
wenzelm@44061
   100
              thm_of_atom (Thm.axiom thy name) Ts
wenzelm@44061
   101
wenzelm@44061
   102
          | thm_of _ Hs (PBound i) = nth Hs i
wenzelm@44061
   103
wenzelm@44061
   104
          | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
wenzelm@44061
   105
              let
wenzelm@44061
   106
                val (x, names') = Name.variant s names;
wenzelm@44061
   107
                val thm = thm_of ((x, T) :: vs, names') Hs prf
wenzelm@44061
   108
              in
wenzelm@59621
   109
                Thm.forall_intr (Thm.global_cterm_of thy (Free (x, T))) thm
wenzelm@44061
   110
              end
berghofe@11522
   111
wenzelm@44061
   112
          | thm_of (vs, names) Hs (prf % SOME t) =
wenzelm@44061
   113
              let
wenzelm@44061
   114
                val thm = thm_of (vs, names) Hs prf;
wenzelm@59621
   115
                val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t));
wenzelm@44061
   116
              in
wenzelm@44061
   117
                Thm.forall_elim ct thm
wenzelm@44061
   118
                handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
wenzelm@44061
   119
              end
berghofe@11522
   120
wenzelm@60642
   121
          | thm_of (vs, names) Hs (AbsP (_, SOME t, prf)) =
wenzelm@44061
   122
              let
wenzelm@59621
   123
                val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t));
wenzelm@44061
   124
                val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
wenzelm@44061
   125
              in
wenzelm@44061
   126
                Thm.implies_intr ct thm
wenzelm@44061
   127
              end
berghofe@11522
   128
wenzelm@44061
   129
          | thm_of vars Hs (prf %% prf') =
wenzelm@44061
   130
              let
wenzelm@44061
   131
                val thm = beta_eta_convert (thm_of vars Hs prf);
wenzelm@44061
   132
                val thm' = beta_eta_convert (thm_of vars Hs prf');
wenzelm@44061
   133
              in
wenzelm@44061
   134
                Thm.implies_elim thm thm'
wenzelm@44061
   135
                handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
wenzelm@44061
   136
              end
berghofe@11522
   137
wenzelm@59621
   138
          | thm_of _ _ (Hyp t) = Thm.assume (Thm.global_cterm_of thy t)
berghofe@11522
   139
wenzelm@44061
   140
          | thm_of _ _ _ = error "thm_of_proof: partial proof term";
wenzelm@44061
   141
wenzelm@44061
   142
      in beta_eta_convert (thm_of ([], prf_names) [] prf) end
wenzelm@44061
   143
  end;
berghofe@11522
   144
berghofe@11522
   145
end;