src/Pure/Proof/proofchecker.ML
author wenzelm
Thu Oct 23 15:28:01 2008 +0200 (2008-10-23)
changeset 28674 08a77c495dc1
parent 26939 1035c89b4c02
child 28808 7925199a0226
permissions -rw-r--r--
renamed Thm.get_axiom_i to Thm.axiom;
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 =
wenzelm@17412
    22
  let val tab = fold_rev Symtab.update (PureThy.all_thms_of thy) Symtab.empty
berghofe@11522
    23
  in
wenzelm@17412
    24
    (fn s => case Symtab.lookup tab s of
skalberg@15531
    25
       NONE => error ("Unknown theorem " ^ quote s)
skalberg@15531
    26
     | SOME thm => thm)
berghofe@11522
    27
  end;
berghofe@11522
    28
berghofe@13733
    29
val beta_eta_convert =
wenzelm@22910
    30
  Conv.fconv_rule Drule.beta_eta_conversion;
berghofe@11522
    31
berghofe@11522
    32
fun thm_of_proof thy prf =
berghofe@11522
    33
  let
wenzelm@20164
    34
    val prf_names = Proofterm.fold_proof_terms
wenzelm@20164
    35
      (fold_aterms (fn Free (x, _) => Name.declare x | _ => I)) (K I) prf Name.context;
berghofe@11522
    36
    val lookup = lookup_thm thy;
berghofe@11522
    37
berghofe@13670
    38
    fun thm_of_atom thm Ts =
berghofe@13670
    39
      let
wenzelm@16862
    40
        val tvars = term_tvars (Thm.full_prop_of thm);
wenzelm@18127
    41
        val (fmap, thm') = Thm.varifyT' [] thm;
wenzelm@20151
    42
        val ctye = map (pairself (Thm.ctyp_of thy))
berghofe@15798
    43
          (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
berghofe@13670
    44
      in
berghofe@13670
    45
        Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
berghofe@13670
    46
      end;
berghofe@13670
    47
wenzelm@21646
    48
    fun thm_of _ _ (PThm (name, _, prop', SOME Ts)) =
berghofe@11522
    49
          let
wenzelm@16608
    50
            val thm = Drule.implies_intr_hyps (lookup name);
berghofe@11522
    51
            val {prop, ...} = rep_thm thm;
berghofe@13733
    52
            val _ = if prop aconv prop' then () else
berghofe@12238
    53
              error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
wenzelm@26939
    54
                Syntax.string_of_term_global thy prop ^ "\n\n" ^
wenzelm@26939
    55
                Syntax.string_of_term_global thy prop');
berghofe@13670
    56
          in thm_of_atom thm Ts end
berghofe@11522
    57
skalberg@15531
    58
      | thm_of _ _ (PAxm (name, _, SOME Ts)) =
wenzelm@28674
    59
          thm_of_atom (Thm.axiom thy name) Ts
berghofe@11522
    60
skalberg@15570
    61
      | thm_of _ Hs (PBound i) = List.nth (Hs, i)
berghofe@11522
    62
wenzelm@20164
    63
      | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
berghofe@11522
    64
          let
wenzelm@20164
    65
            val ([x], names') = Name.variants [s] names;
wenzelm@20164
    66
            val thm = thm_of ((x, T) :: vs, names') Hs prf
berghofe@11522
    67
          in
wenzelm@20151
    68
            Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
berghofe@11522
    69
          end
berghofe@11522
    70
wenzelm@20164
    71
      | thm_of (vs, names) Hs (prf % SOME t) =
berghofe@11522
    72
          let
wenzelm@20164
    73
            val thm = thm_of (vs, names) Hs prf;
wenzelm@20164
    74
            val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
berghofe@11522
    75
          in Thm.forall_elim ct thm end
berghofe@11522
    76
wenzelm@20164
    77
      | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
berghofe@11522
    78
          let
wenzelm@20151
    79
            val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
wenzelm@20164
    80
            val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
berghofe@11522
    81
          in
berghofe@11522
    82
            Thm.implies_intr ct thm
berghofe@11522
    83
          end
berghofe@11522
    84
wenzelm@20164
    85
      | thm_of vars Hs (prf %% prf') =
wenzelm@20151
    86
          let
wenzelm@20164
    87
            val thm = beta_eta_convert (thm_of vars Hs prf);
wenzelm@20164
    88
            val thm' = beta_eta_convert (thm_of vars Hs prf');
berghofe@11522
    89
          in
berghofe@11522
    90
            Thm.implies_elim thm thm'
berghofe@11522
    91
          end
berghofe@11522
    92
wenzelm@20151
    93
      | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
berghofe@11522
    94
berghofe@11522
    95
      | thm_of _ _ _ = error "thm_of_proof: partial proof term";
berghofe@11522
    96
wenzelm@20164
    97
  in beta_eta_convert (thm_of ([], prf_names) [] prf) end;
berghofe@11522
    98
berghofe@11522
    99
end;