src/Pure/Proof/proofchecker.ML
author wenzelm
Tue May 31 11:53:40 2005 +0200 (2005-05-31)
changeset 16149 d8cac577493c
parent 15798 016f3be5a5ec
child 16351 561b9f8be72e
permissions -rw-r--r--
Theory.restore_naming;
tuned fold;
     1 (*  Title:      Pure/Proof/proofchecker.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4 
     5 Simple proof checker based only on the core inference rules
     6 of Isabelle/Pure.
     7 *)
     8 
     9 signature PROOF_CHECKER =
    10 sig
    11   val thm_of_proof : theory -> Proofterm.proof -> thm
    12 end;
    13 
    14 structure ProofChecker : PROOF_CHECKER =
    15 struct
    16 
    17 open Proofterm;
    18 
    19 (***** construct a theorem out of a proof term *****)
    20 
    21 fun lookup_thm thy =
    22   let val tab = foldr Symtab.update Symtab.empty
    23     (List.concat (map thms_of (thy :: Theory.ancestors_of thy)))
    24   in
    25     (fn s => case Symtab.lookup (tab, s) of
    26        NONE => error ("Unknown theorem " ^ quote s)
    27      | SOME thm => thm)
    28   end;
    29 
    30 val beta_eta_convert =
    31   Drule.fconv_rule Drule.beta_eta_conversion;
    32 
    33 fun thm_of_proof thy prf =
    34   let
    35     val names = add_prf_names ([], prf);
    36     val sg = sign_of thy;
    37     val lookup = lookup_thm thy;
    38 
    39     fun thm_of_atom thm Ts =
    40       let
    41         val tvars = term_tvars (prop_of thm);
    42         val (thm', fmap) = Thm.varifyT' [] thm;
    43         val ctye = map (pairself (Thm.ctyp_of sg))
    44           (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
    45       in
    46         Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
    47       end;
    48 
    49     fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) =
    50           let
    51             val thm = Thm.implies_intr_hyps (lookup name);
    52             val {prop, ...} = rep_thm thm;
    53             val _ = if prop aconv prop' then () else
    54               error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
    55                 Sign.string_of_term sg prop ^ "\n\n" ^
    56                 Sign.string_of_term sg prop');
    57           in thm_of_atom thm Ts end
    58 
    59       | thm_of _ _ (PAxm (name, _, SOME Ts)) =
    60           thm_of_atom (get_axiom thy name) Ts
    61 
    62       | thm_of _ Hs (PBound i) = List.nth (Hs, i)
    63 
    64       | thm_of vs Hs (Abst (s, SOME T, prf)) =
    65           let
    66             val x = variant (names @ map fst vs) s;
    67             val thm = thm_of ((x, T) :: vs) Hs prf
    68           in
    69             Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm
    70           end
    71 
    72       | thm_of vs Hs (prf % SOME t) =
    73           let
    74             val thm = thm_of vs Hs prf
    75             val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t))
    76           in Thm.forall_elim ct thm end
    77 
    78       | thm_of vs Hs (AbsP (s, SOME t, prf)) =
    79           let
    80             val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t));
    81             val thm = thm_of vs (Thm.assume ct :: Hs) prf
    82           in
    83             Thm.implies_intr ct thm
    84           end
    85 
    86       | thm_of vs Hs (prf %% prf') =
    87           let 
    88             val thm = beta_eta_convert (thm_of vs Hs prf);
    89             val thm' = beta_eta_convert (thm_of vs Hs prf')
    90           in
    91             Thm.implies_elim thm thm'
    92           end
    93 
    94       | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of sg t)
    95 
    96       | thm_of _ _ _ = error "thm_of_proof: partial proof term";
    97 
    98   in beta_eta_convert (thm_of [] [] prf) end;
    99 
   100 end;