src/Pure/Proof/proofchecker.ML
author berghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797 a63605582573
parent 15574 b1d1b5bfc464
child 15798 016f3be5a5ec
permissions -rw-r--r--
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
     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 fst tvars @ map snd fmap ~~ map (Thm.ctyp_of sg) Ts
    44       in
    45         Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
    46       end;
    47 
    48     fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) =
    49           let
    50             val thm = Thm.implies_intr_hyps (lookup name);
    51             val {prop, ...} = rep_thm thm;
    52             val _ = if prop aconv prop' then () else
    53               error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
    54                 Sign.string_of_term sg prop ^ "\n\n" ^
    55                 Sign.string_of_term sg prop');
    56           in thm_of_atom thm Ts end
    57 
    58       | thm_of _ _ (PAxm (name, _, SOME Ts)) =
    59           thm_of_atom (get_axiom thy name) Ts
    60 
    61       | thm_of _ Hs (PBound i) = List.nth (Hs, i)
    62 
    63       | thm_of vs Hs (Abst (s, SOME T, prf)) =
    64           let
    65             val x = variant (names @ map fst vs) s;
    66             val thm = thm_of ((x, T) :: vs) Hs prf
    67           in
    68             Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm
    69           end
    70 
    71       | thm_of vs Hs (prf % SOME t) =
    72           let
    73             val thm = thm_of vs Hs prf
    74             val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t))
    75           in Thm.forall_elim ct thm end
    76 
    77       | thm_of vs Hs (AbsP (s, SOME t, prf)) =
    78           let
    79             val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t));
    80             val thm = thm_of vs (Thm.assume ct :: Hs) prf
    81           in
    82             Thm.implies_intr ct thm
    83           end
    84 
    85       | thm_of vs Hs (prf %% prf') =
    86           let 
    87             val thm = beta_eta_convert (thm_of vs Hs prf);
    88             val thm' = beta_eta_convert (thm_of vs Hs prf')
    89           in
    90             Thm.implies_elim thm thm'
    91           end
    92 
    93       | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of sg t)
    94 
    95       | thm_of _ _ _ = error "thm_of_proof: partial proof term";
    96 
    97   in beta_eta_convert (thm_of [] [] prf) end;
    98 
    99 end;