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