berghofe@11522
|
1 |
(* Title: Pure/Proof/proofchecker.ML
|
wenzelm@11539
|
2 |
Author: Stefan Berghofer, TU Muenchen
|
berghofe@11522
|
3 |
|
berghofe@11522
|
4 |
Simple proof checker based only on the core inference rules
|
berghofe@11522
|
5 |
of Isabelle/Pure.
|
berghofe@11522
|
6 |
*)
|
berghofe@11522
|
7 |
|
berghofe@11522
|
8 |
signature PROOF_CHECKER =
|
berghofe@11522
|
9 |
sig
|
berghofe@11522
|
10 |
val thm_of_proof : theory -> Proofterm.proof -> thm
|
berghofe@11522
|
11 |
end;
|
berghofe@11522
|
12 |
|
berghofe@11612
|
13 |
structure ProofChecker : PROOF_CHECKER =
|
berghofe@11522
|
14 |
struct
|
berghofe@11522
|
15 |
|
berghofe@11522
|
16 |
open Proofterm;
|
berghofe@11522
|
17 |
|
berghofe@11522
|
18 |
(***** construct a theorem out of a proof term *****)
|
berghofe@11522
|
19 |
|
berghofe@11522
|
20 |
fun lookup_thm thy =
|
wenzelm@17412
|
21 |
let val tab = fold_rev Symtab.update (PureThy.all_thms_of thy) Symtab.empty
|
berghofe@11522
|
22 |
in
|
wenzelm@17412
|
23 |
(fn s => case Symtab.lookup tab s of
|
skalberg@15531
|
24 |
NONE => error ("Unknown theorem " ^ quote s)
|
skalberg@15531
|
25 |
| SOME thm => thm)
|
berghofe@11522
|
26 |
end;
|
berghofe@11522
|
27 |
|
berghofe@13733
|
28 |
val beta_eta_convert =
|
wenzelm@22910
|
29 |
Conv.fconv_rule Drule.beta_eta_conversion;
|
berghofe@11522
|
30 |
|
berghofe@37229
|
31 |
(* equality modulo renaming of type variables *)
|
berghofe@37229
|
32 |
fun is_equal t t' =
|
berghofe@37229
|
33 |
let
|
berghofe@37229
|
34 |
val atoms = fold_types (fold_atyps (insert (op =))) t [];
|
berghofe@37229
|
35 |
val atoms' = fold_types (fold_atyps (insert (op =))) t' []
|
berghofe@37229
|
36 |
in
|
berghofe@37229
|
37 |
length atoms = length atoms' andalso
|
berghofe@37229
|
38 |
map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
|
berghofe@37229
|
39 |
end;
|
berghofe@37229
|
40 |
|
berghofe@37229
|
41 |
fun pretty_prf thy vs Hs prf =
|
berghofe@37229
|
42 |
let val prf' = prf |> prf_subst_bounds (map Free vs) |>
|
berghofe@37229
|
43 |
prf_subst_pbounds (map (Hyp o prop_of) Hs)
|
berghofe@37229
|
44 |
in
|
berghofe@37229
|
45 |
(Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
|
berghofe@37229
|
46 |
Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
|
berghofe@37229
|
47 |
end;
|
berghofe@37229
|
48 |
|
berghofe@37229
|
49 |
fun pretty_term thy vs _ t =
|
berghofe@37229
|
50 |
let val t' = subst_bounds (map Free vs, t)
|
berghofe@37229
|
51 |
in
|
berghofe@37229
|
52 |
(Syntax.pretty_term_global thy t',
|
berghofe@37229
|
53 |
Syntax.pretty_typ_global thy (fastype_of t'))
|
berghofe@37229
|
54 |
end;
|
berghofe@37229
|
55 |
|
berghofe@37229
|
56 |
fun appl_error thy prt vs Hs s f a =
|
berghofe@37229
|
57 |
let
|
berghofe@37229
|
58 |
val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
|
berghofe@37229
|
59 |
val (pp_a, pp_aT) = prt thy vs Hs a
|
berghofe@37229
|
60 |
in
|
berghofe@37229
|
61 |
error (cat_lines
|
berghofe@37229
|
62 |
[s,
|
berghofe@37229
|
63 |
"",
|
berghofe@37229
|
64 |
Pretty.string_of (Pretty.block
|
berghofe@37229
|
65 |
[Pretty.str "Operator:", Pretty.brk 2, pp_f,
|
berghofe@37229
|
66 |
Pretty.str " ::", Pretty.brk 1, pp_fT]),
|
berghofe@37229
|
67 |
Pretty.string_of (Pretty.block
|
berghofe@37229
|
68 |
[Pretty.str "Operand:", Pretty.brk 3, pp_a,
|
berghofe@37229
|
69 |
Pretty.str " ::", Pretty.brk 1, pp_aT]),
|
berghofe@37229
|
70 |
""])
|
berghofe@37229
|
71 |
end;
|
berghofe@37229
|
72 |
|
berghofe@11522
|
73 |
fun thm_of_proof thy prf =
|
berghofe@11522
|
74 |
let
|
wenzelm@29277
|
75 |
val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
|
berghofe@11522
|
76 |
val lookup = lookup_thm thy;
|
berghofe@11522
|
77 |
|
berghofe@13670
|
78 |
fun thm_of_atom thm Ts =
|
berghofe@13670
|
79 |
let
|
krauss@36042
|
80 |
val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
|
wenzelm@35845
|
81 |
val (fmap, thm') = Thm.varifyT_global' [] thm;
|
wenzelm@20151
|
82 |
val ctye = map (pairself (Thm.ctyp_of thy))
|
berghofe@15798
|
83 |
(map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
|
berghofe@13670
|
84 |
in
|
wenzelm@35986
|
85 |
Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
|
berghofe@13670
|
86 |
end;
|
berghofe@13670
|
87 |
|
wenzelm@28808
|
88 |
fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
|
berghofe@11522
|
89 |
let
|
berghofe@37229
|
90 |
val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
|
berghofe@11522
|
91 |
val {prop, ...} = rep_thm thm;
|
berghofe@37229
|
92 |
val _ = if is_equal prop prop' then () else
|
berghofe@12238
|
93 |
error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
|
wenzelm@26939
|
94 |
Syntax.string_of_term_global thy prop ^ "\n\n" ^
|
wenzelm@26939
|
95 |
Syntax.string_of_term_global thy prop');
|
berghofe@13670
|
96 |
in thm_of_atom thm Ts end
|
berghofe@11522
|
97 |
|
skalberg@15531
|
98 |
| thm_of _ _ (PAxm (name, _, SOME Ts)) =
|
wenzelm@28674
|
99 |
thm_of_atom (Thm.axiom thy name) Ts
|
berghofe@11522
|
100 |
|
wenzelm@30146
|
101 |
| thm_of _ Hs (PBound i) = nth Hs i
|
berghofe@11522
|
102 |
|
wenzelm@20164
|
103 |
| thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
|
berghofe@11522
|
104 |
let
|
wenzelm@20164
|
105 |
val ([x], names') = Name.variants [s] names;
|
wenzelm@20164
|
106 |
val thm = thm_of ((x, T) :: vs, names') Hs prf
|
berghofe@11522
|
107 |
in
|
wenzelm@20151
|
108 |
Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
|
berghofe@11522
|
109 |
end
|
berghofe@11522
|
110 |
|
wenzelm@20164
|
111 |
| thm_of (vs, names) Hs (prf % SOME t) =
|
berghofe@11522
|
112 |
let
|
wenzelm@20164
|
113 |
val thm = thm_of (vs, names) Hs prf;
|
wenzelm@20164
|
114 |
val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
|
berghofe@37229
|
115 |
in
|
berghofe@37229
|
116 |
Thm.forall_elim ct thm
|
berghofe@37229
|
117 |
handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
|
berghofe@37229
|
118 |
end
|
berghofe@11522
|
119 |
|
wenzelm@20164
|
120 |
| thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
|
berghofe@11522
|
121 |
let
|
wenzelm@20151
|
122 |
val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
|
wenzelm@20164
|
123 |
val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
|
berghofe@11522
|
124 |
in
|
berghofe@11522
|
125 |
Thm.implies_intr ct thm
|
berghofe@11522
|
126 |
end
|
berghofe@11522
|
127 |
|
wenzelm@20164
|
128 |
| thm_of vars Hs (prf %% prf') =
|
wenzelm@20151
|
129 |
let
|
wenzelm@20164
|
130 |
val thm = beta_eta_convert (thm_of vars Hs prf);
|
wenzelm@20164
|
131 |
val thm' = beta_eta_convert (thm_of vars Hs prf');
|
berghofe@11522
|
132 |
in
|
berghofe@11522
|
133 |
Thm.implies_elim thm thm'
|
berghofe@37229
|
134 |
handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
|
berghofe@11522
|
135 |
end
|
berghofe@11522
|
136 |
|
wenzelm@20151
|
137 |
| thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
|
berghofe@11522
|
138 |
|
berghofe@11522
|
139 |
| thm_of _ _ _ = error "thm_of_proof: partial proof term";
|
berghofe@11522
|
140 |
|
wenzelm@20164
|
141 |
in beta_eta_convert (thm_of ([], prf_names) [] prf) end;
|
berghofe@11522
|
142 |
|
berghofe@11522
|
143 |
end;
|