author | wenzelm |
Wed, 09 Nov 2005 16:26:41 +0100 | |
changeset 18127 | 9f03d8a9a81b |
parent 17412 | e26cb20ef0cc |
child 20071 | 8f3e1ddb50e6 |
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 |
|
34 |
val names = add_prf_names ([], prf); |
|
35 |
val sg = sign_of thy; |
|
36 |
val lookup = lookup_thm thy; |
|
37 |
||
13670 | 38 |
fun thm_of_atom thm Ts = |
39 |
let |
|
16862 | 40 |
val tvars = term_tvars (Thm.full_prop_of thm); |
18127 | 41 |
val (fmap, thm') = Thm.varifyT' [] thm; |
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset
|
42 |
val ctye = map (pairself (Thm.ctyp_of sg)) |
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15574
diff
changeset
|
43 |
(map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) |
13670 | 44 |
in |
45 |
Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) |
|
46 |
end; |
|
47 |
||
15531 | 48 |
fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) = |
11522 | 49 |
let |
16608 | 50 |
val thm = Drule.implies_intr_hyps (lookup name); |
11522 | 51 |
val {prop, ...} = rep_thm thm; |
13733 | 52 |
val _ = if prop aconv prop' then () else |
12238 | 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'); |
|
13670 | 56 |
in thm_of_atom thm Ts end |
11522 | 57 |
|
15531 | 58 |
| thm_of _ _ (PAxm (name, _, SOME Ts)) = |
13670 | 59 |
thm_of_atom (get_axiom thy name) Ts |
11522 | 60 |
|
15570 | 61 |
| thm_of _ Hs (PBound i) = List.nth (Hs, i) |
11522 | 62 |
|
15531 | 63 |
| thm_of vs Hs (Abst (s, SOME T, prf)) = |
11522 | 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 |
||
15531 | 71 |
| thm_of vs Hs (prf % SOME t) = |
11522 | 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 |
||
15531 | 77 |
| thm_of vs Hs (AbsP (s, SOME t, prf)) = |
11522 | 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 |
||
11612 | 85 |
| thm_of vs Hs (prf %% prf') = |
11522 | 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 |
||
13733 | 97 |
in beta_eta_convert (thm_of [] [] prf) end; |
11522 | 98 |
|
99 |
end; |