src/Pure/Proof/proofchecker.ML
author wenzelm
Fri Aug 31 18:46:48 2001 +0200 (2001-08-31)
changeset 11539 0f17da240450
parent 11522 42fbb6abed5a
child 11612 ae8450657bf0
permissions -rw-r--r--
tuned headers;
berghofe@11522
     1
(*  Title:      Pure/Proof/proofchecker.ML
berghofe@11522
     2
    ID:         $Id$
wenzelm@11539
     3
    Author:     Stefan Berghofer, TU Muenchen
wenzelm@11539
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
berghofe@11522
     5
berghofe@11522
     6
Simple proof checker based only on the core inference rules
berghofe@11522
     7
of Isabelle/Pure.
berghofe@11522
     8
*)
berghofe@11522
     9
berghofe@11522
    10
signature PROOF_CHECKER =
berghofe@11522
    11
sig
berghofe@11522
    12
  val thm_of_proof : theory -> Proofterm.proof -> thm
berghofe@11522
    13
end;
berghofe@11522
    14
berghofe@11522
    15
structure ProofChecker =
berghofe@11522
    16
struct
berghofe@11522
    17
berghofe@11522
    18
open Proofterm;
berghofe@11522
    19
berghofe@11522
    20
(***** construct a theorem out of a proof term *****)
berghofe@11522
    21
berghofe@11522
    22
fun lookup_thm thy =
berghofe@11522
    23
  let val tab = foldr Symtab.update
berghofe@11522
    24
    (flat (map thms_of (thy :: Theory.ancestors_of thy)), Symtab.empty)
berghofe@11522
    25
  in
berghofe@11522
    26
    (fn s => case Symtab.lookup (tab, s) of
berghofe@11522
    27
       None => error ("Unknown theorem " ^ quote s)
berghofe@11522
    28
     | Some thm => thm)
berghofe@11522
    29
  end;
berghofe@11522
    30
berghofe@11522
    31
fun beta_eta_convert thm =
berghofe@11522
    32
  let
berghofe@11522
    33
    val beta_thm = beta_conversion true (cprop_of thm);
berghofe@11522
    34
    val (_, rhs) = Drule.dest_equals (cprop_of beta_thm);
berghofe@11522
    35
  in Thm.equal_elim (Thm.transitive beta_thm (eta_conversion rhs)) thm end;
berghofe@11522
    36
berghofe@11522
    37
fun thm_of_proof thy prf =
berghofe@11522
    38
  let
berghofe@11522
    39
    val names = add_prf_names ([], prf);
berghofe@11522
    40
    val sg = sign_of thy;
berghofe@11522
    41
    val lookup = lookup_thm thy;
berghofe@11522
    42
berghofe@11522
    43
    fun thm_of _ _ (PThm ((name, _), _, prop', Some Ts)) =
berghofe@11522
    44
          let
berghofe@11522
    45
            val thm = lookup name;
berghofe@11522
    46
            val {prop, ...} = rep_thm thm;
berghofe@11522
    47
            val _ = if prop=prop' then () else
berghofe@11522
    48
              error ("Duplicate use of theorem name " ^ quote name);
berghofe@11522
    49
            val tvars = term_tvars prop;
berghofe@11522
    50
            val ctye = map fst tvars ~~ map (Thm.ctyp_of sg) Ts
berghofe@11522
    51
          in
berghofe@11522
    52
            Thm.instantiate (ctye, []) (forall_intr_vars thm)
berghofe@11522
    53
          end
berghofe@11522
    54
berghofe@11522
    55
      | thm_of _ _ (PAxm (name, _, Some Ts)) =
berghofe@11522
    56
          let
berghofe@11522
    57
            val thm = get_axiom thy name;
berghofe@11522
    58
            val {prop, ...} = rep_thm thm;
berghofe@11522
    59
            val tvars = term_tvars prop;
berghofe@11522
    60
            val ctye = map fst tvars ~~ map (Thm.ctyp_of sg) Ts
berghofe@11522
    61
          in
berghofe@11522
    62
            Thm.instantiate (ctye, []) (forall_intr_vars thm)
berghofe@11522
    63
          end
berghofe@11522
    64
berghofe@11522
    65
      | thm_of _ Hs (PBound i) = nth_elem (i, Hs)
berghofe@11522
    66
berghofe@11522
    67
      | thm_of vs Hs (Abst (s, Some T, prf)) =
berghofe@11522
    68
          let
berghofe@11522
    69
            val x = variant (names @ map fst vs) s;
berghofe@11522
    70
            val thm = thm_of ((x, T) :: vs) Hs prf
berghofe@11522
    71
          in
berghofe@11522
    72
            Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm
berghofe@11522
    73
          end
berghofe@11522
    74
berghofe@11522
    75
      | thm_of vs Hs (prf %% Some t) =
berghofe@11522
    76
          let
berghofe@11522
    77
            val thm = thm_of vs Hs prf
berghofe@11522
    78
            val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t))
berghofe@11522
    79
          in Thm.forall_elim ct thm end
berghofe@11522
    80
berghofe@11522
    81
      | thm_of vs Hs (AbsP (s, Some t, prf)) =
berghofe@11522
    82
          let
berghofe@11522
    83
            val ct = Thm.cterm_of sg (Term.subst_bounds (map Free vs, t));
berghofe@11522
    84
            val thm = thm_of vs (Thm.assume ct :: Hs) prf
berghofe@11522
    85
          in
berghofe@11522
    86
            Thm.implies_intr ct thm
berghofe@11522
    87
          end
berghofe@11522
    88
berghofe@11522
    89
      | thm_of vs Hs (prf % prf') =
berghofe@11522
    90
          let 
berghofe@11522
    91
            val thm = beta_eta_convert (thm_of vs Hs prf);
berghofe@11522
    92
            val thm' = beta_eta_convert (thm_of vs Hs prf')
berghofe@11522
    93
          in
berghofe@11522
    94
            Thm.implies_elim thm thm'
berghofe@11522
    95
          end
berghofe@11522
    96
berghofe@11522
    97
      | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of sg t)
berghofe@11522
    98
berghofe@11522
    99
      | thm_of _ _ _ = error "thm_of_proof: partial proof term";
berghofe@11522
   100
berghofe@11522
   101
  in thm_of [] [] prf end;
berghofe@11522
   102
berghofe@11522
   103
end;
berghofe@11522
   104