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