author | wenzelm |
Tue, 18 Jul 2006 20:01:47 +0200 | |
changeset 20151 | b22c14181eb7 |
parent 20071 | 8f3e1ddb50e6 |
child 20164 | 928c8dc07216 |
permissions | -rw-r--r-- |
11522 | 1 |
(* Title: Pure/Proof/proofchecker.ML |
2 |
ID: $Id$ |
|
11539 | 3 |
Author: Stefan Berghofer, TU Muenchen |
11522 | 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 |
||
11612 | 14 |
structure ProofChecker : PROOF_CHECKER = |
11522 | 15 |
struct |
16 |
||
17 |
open Proofterm; |
|
18 |
||
19 |
(***** construct a theorem out of a proof term *****) |
|
20 |
||
21 |
fun lookup_thm thy = |
|
17412 | 22 |
let val tab = fold_rev Symtab.update (PureThy.all_thms_of thy) Symtab.empty |
11522 | 23 |
in |
17412 | 24 |
(fn s => case Symtab.lookup tab s of |
15531 | 25 |
NONE => error ("Unknown theorem " ^ quote s) |
26 |
| SOME thm => thm) |
|
11522 | 27 |
end; |
28 |
||
13733 | 29 |
val beta_eta_convert = |
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14981
diff
changeset
|
30 |
Drule.fconv_rule Drule.beta_eta_conversion; |
11522 | 31 |
|
32 |
fun thm_of_proof thy prf = |
|
33 |
let |
|
20151 | 34 |
val names = Proofterm.fold_proof_terms Term.declare_term_names (K I) prf Name.context; |
11522 | 35 |
val lookup = lookup_thm thy; |
36 |
||
13670 | 37 |
fun thm_of_atom thm Ts = |
38 |
let |
|
16862 | 39 |
val tvars = term_tvars (Thm.full_prop_of thm); |
18127 | 40 |
val (fmap, thm') = Thm.varifyT' [] thm; |
20151 | 41 |
val ctye = map (pairself (Thm.ctyp_of thy)) |
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset
|
42 |
(map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) |
13670 | 43 |
in |
44 |
Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) |
|
45 |
end; |
|
46 |
||
15531 | 47 |
fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) = |
11522 | 48 |
let |
16608 | 49 |
val thm = Drule.implies_intr_hyps (lookup name); |
11522 | 50 |
val {prop, ...} = rep_thm thm; |
13733 | 51 |
val _ = if prop aconv prop' then () else |
12238 | 52 |
error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
20151 | 53 |
Sign.string_of_term thy prop ^ "\n\n" ^ |
54 |
Sign.string_of_term thy prop'); |
|
13670 | 55 |
in thm_of_atom thm Ts end |
11522 | 56 |
|
15531 | 57 |
| thm_of _ _ (PAxm (name, _, SOME Ts)) = |
13670 | 58 |
thm_of_atom (get_axiom thy name) Ts |
11522 | 59 |
|
15570 | 60 |
| thm_of _ Hs (PBound i) = List.nth (Hs, i) |
11522 | 61 |
|
15531 | 62 |
| thm_of vs Hs (Abst (s, SOME T, prf)) = |
11522 | 63 |
let |
20151 | 64 |
val ([x], _) = Name.variants [s] (fold (Name.declare o fst) vs names); |
11522 | 65 |
val thm = thm_of ((x, T) :: vs) Hs prf |
66 |
in |
|
20151 | 67 |
Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm |
11522 | 68 |
end |
69 |
||
15531 | 70 |
| thm_of vs Hs (prf % SOME t) = |
11522 | 71 |
let |
72 |
val thm = thm_of vs Hs prf |
|
20151 | 73 |
val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t)) |
11522 | 74 |
in Thm.forall_elim ct thm end |
75 |
||
15531 | 76 |
| thm_of vs Hs (AbsP (s, SOME t, prf)) = |
11522 | 77 |
let |
20151 | 78 |
val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t)); |
11522 | 79 |
val thm = thm_of vs (Thm.assume ct :: Hs) prf |
80 |
in |
|
81 |
Thm.implies_intr ct thm |
|
82 |
end |
|
83 |
||
11612 | 84 |
| thm_of vs Hs (prf %% prf') = |
20151 | 85 |
let |
11522 | 86 |
val thm = beta_eta_convert (thm_of vs Hs prf); |
87 |
val thm' = beta_eta_convert (thm_of vs Hs prf') |
|
88 |
in |
|
89 |
Thm.implies_elim thm thm' |
|
90 |
end |
|
91 |
||
20151 | 92 |
| thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t) |
11522 | 93 |
|
94 |
| thm_of _ _ _ = error "thm_of_proof: partial proof term"; |
|
95 |
||
13733 | 96 |
in beta_eta_convert (thm_of [] [] prf) end; |
11522 | 97 |
|
98 |
end; |