author | wenzelm |
Sat, 13 Dec 2008 15:00:39 +0100 | |
changeset 29091 | b81fe045e799 |
parent 28808 | 7925199a0226 |
child 29270 | 0eade173f77e |
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 = |
22910 | 30 |
Conv.fconv_rule Drule.beta_eta_conversion; |
11522 | 31 |
|
32 |
fun thm_of_proof thy prf = |
|
33 |
let |
|
20164 | 34 |
val prf_names = Proofterm.fold_proof_terms |
35 |
(fold_aterms (fn Free (x, _) => Name.declare x | _ => I)) (K I) prf Name.context; |
|
11522 | 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; |
20151 | 42 |
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
|
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 |
||
28808 | 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" ^ |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
22910
diff
changeset
|
54 |
Syntax.string_of_term_global thy prop ^ "\n\n" ^ |
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
22910
diff
changeset
|
55 |
Syntax.string_of_term_global thy prop'); |
13670 | 56 |
in thm_of_atom thm Ts end |
11522 | 57 |
|
15531 | 58 |
| thm_of _ _ (PAxm (name, _, SOME Ts)) = |
28674 | 59 |
thm_of_atom (Thm.axiom thy name) Ts |
11522 | 60 |
|
15570 | 61 |
| thm_of _ Hs (PBound i) = List.nth (Hs, i) |
11522 | 62 |
|
20164 | 63 |
| thm_of (vs, names) Hs (Abst (s, SOME T, prf)) = |
11522 | 64 |
let |
20164 | 65 |
val ([x], names') = Name.variants [s] names; |
66 |
val thm = thm_of ((x, T) :: vs, names') Hs prf |
|
11522 | 67 |
in |
20151 | 68 |
Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm |
11522 | 69 |
end |
70 |
||
20164 | 71 |
| thm_of (vs, names) Hs (prf % SOME t) = |
11522 | 72 |
let |
20164 | 73 |
val thm = thm_of (vs, names) Hs prf; |
74 |
val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t)); |
|
11522 | 75 |
in Thm.forall_elim ct thm end |
76 |
||
20164 | 77 |
| thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) = |
11522 | 78 |
let |
20151 | 79 |
val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t)); |
20164 | 80 |
val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf; |
11522 | 81 |
in |
82 |
Thm.implies_intr ct thm |
|
83 |
end |
|
84 |
||
20164 | 85 |
| thm_of vars Hs (prf %% prf') = |
20151 | 86 |
let |
20164 | 87 |
val thm = beta_eta_convert (thm_of vars Hs prf); |
88 |
val thm' = beta_eta_convert (thm_of vars Hs prf'); |
|
11522 | 89 |
in |
90 |
Thm.implies_elim thm thm' |
|
91 |
end |
|
92 |
||
20151 | 93 |
| thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t) |
11522 | 94 |
|
95 |
| thm_of _ _ _ = error "thm_of_proof: partial proof term"; |
|
96 |
||
20164 | 97 |
in beta_eta_convert (thm_of ([], prf_names) [] prf) end; |
11522 | 98 |
|
99 |
end; |