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