author | wenzelm |
Mon, 08 Aug 2011 17:23:15 +0200 | |
changeset 44058 | ae85c5d64913 |
parent 44057 | fda143b5c2f5 |
child 44061 | 9f17ede679e9 |
permissions | -rw-r--r-- |
11522 | 1 |
(* Title: Pure/Proof/proofchecker.ML |
11539 | 2 |
Author: Stefan Berghofer, TU Muenchen |
11522 | 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 |
||
44057 | 13 |
structure Proof_Checker : PROOF_CHECKER = |
11522 | 14 |
struct |
15 |
||
16 |
(***** construct a theorem out of a proof term *****) |
|
17 |
||
18 |
fun lookup_thm thy = |
|
44057 | 19 |
let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in |
20 |
fn s => |
|
21 |
(case Symtab.lookup tab s of |
|
22 |
NONE => error ("Unknown theorem " ^ quote s) |
|
23 |
| SOME thm => thm) |
|
11522 | 24 |
end; |
25 |
||
13733 | 26 |
val beta_eta_convert = |
22910 | 27 |
Conv.fconv_rule Drule.beta_eta_conversion; |
11522 | 28 |
|
37229
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
29 |
(* equality modulo renaming of type variables *) |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
30 |
fun is_equal t t' = |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
31 |
let |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
32 |
val atoms = fold_types (fold_atyps (insert (op =))) t []; |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
33 |
val atoms' = fold_types (fold_atyps (insert (op =))) t' [] |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
34 |
in |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
35 |
length atoms = length atoms' andalso |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
36 |
map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t' |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
37 |
end; |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
38 |
|
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
39 |
fun pretty_prf thy vs Hs prf = |
37310 | 40 |
let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |> |
41 |
Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs) |
|
37229
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
42 |
in |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
43 |
(Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf', |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
44 |
Syntax.pretty_term_global thy (Reconstruct.prop_of prf')) |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
45 |
end; |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
46 |
|
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
47 |
fun pretty_term thy vs _ t = |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
48 |
let val t' = subst_bounds (map Free vs, t) |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
49 |
in |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
50 |
(Syntax.pretty_term_global thy t', |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
51 |
Syntax.pretty_typ_global thy (fastype_of t')) |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
52 |
end; |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
53 |
|
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
54 |
fun appl_error thy prt vs Hs s f a = |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
55 |
let |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
56 |
val (pp_f, pp_fT) = pretty_prf thy vs Hs f; |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
57 |
val (pp_a, pp_aT) = prt thy vs Hs a |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
58 |
in |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
59 |
error (cat_lines |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
60 |
[s, |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
61 |
"", |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
62 |
Pretty.string_of (Pretty.block |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
63 |
[Pretty.str "Operator:", Pretty.brk 2, pp_f, |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
64 |
Pretty.str " ::", Pretty.brk 1, pp_fT]), |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
65 |
Pretty.string_of (Pretty.block |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
66 |
[Pretty.str "Operand:", Pretty.brk 3, pp_a, |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
67 |
Pretty.str " ::", Pretty.brk 1, pp_aT]), |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
68 |
""]) |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
69 |
end; |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
70 |
|
11522 | 71 |
fun thm_of_proof thy prf = |
72 |
let |
|
29277 | 73 |
val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context; |
11522 | 74 |
val lookup = lookup_thm thy; |
75 |
||
13670 | 76 |
fun thm_of_atom thm Ts = |
77 |
let |
|
36042
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35985
diff
changeset
|
78 |
val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev; |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
30146
diff
changeset
|
79 |
val (fmap, thm') = Thm.varifyT_global' [] thm; |
20151 | 80 |
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
|
81 |
(map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) |
13670 | 82 |
in |
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35845
diff
changeset
|
83 |
Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm')) |
13670 | 84 |
end; |
85 |
||
28808 | 86 |
fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) = |
11522 | 87 |
let |
37229
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
88 |
val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name)); |
44058 | 89 |
val prop = Thm.prop_of thm; |
44057 | 90 |
val _ = |
91 |
if is_equal prop prop' then () |
|
92 |
else |
|
93 |
error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
|
94 |
Syntax.string_of_term_global thy prop ^ "\n\n" ^ |
|
95 |
Syntax.string_of_term_global thy prop'); |
|
13670 | 96 |
in thm_of_atom thm Ts end |
11522 | 97 |
|
15531 | 98 |
| thm_of _ _ (PAxm (name, _, SOME Ts)) = |
28674 | 99 |
thm_of_atom (Thm.axiom thy name) Ts |
11522 | 100 |
|
30146 | 101 |
| thm_of _ Hs (PBound i) = nth Hs i |
11522 | 102 |
|
20164 | 103 |
| thm_of (vs, names) Hs (Abst (s, SOME T, prf)) = |
11522 | 104 |
let |
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
39557
diff
changeset
|
105 |
val (x, names') = Name.variant s names; |
20164 | 106 |
val thm = thm_of ((x, T) :: vs, names') Hs prf |
11522 | 107 |
in |
20151 | 108 |
Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm |
11522 | 109 |
end |
110 |
||
20164 | 111 |
| thm_of (vs, names) Hs (prf % SOME t) = |
11522 | 112 |
let |
20164 | 113 |
val thm = thm_of (vs, names) Hs prf; |
114 |
val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t)); |
|
37229
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
115 |
in |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
116 |
Thm.forall_elim ct thm |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
117 |
handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t |
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
118 |
end |
11522 | 119 |
|
20164 | 120 |
| thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) = |
11522 | 121 |
let |
20151 | 122 |
val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t)); |
20164 | 123 |
val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf; |
11522 | 124 |
in |
125 |
Thm.implies_intr ct thm |
|
126 |
end |
|
127 |
||
20164 | 128 |
| thm_of vars Hs (prf %% prf') = |
20151 | 129 |
let |
20164 | 130 |
val thm = beta_eta_convert (thm_of vars Hs prf); |
131 |
val thm' = beta_eta_convert (thm_of vars Hs prf'); |
|
11522 | 132 |
in |
133 |
Thm.implies_elim thm thm' |
|
37229
47eb565796f4
- Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents:
36042
diff
changeset
|
134 |
handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf' |
11522 | 135 |
end |
136 |
||
20151 | 137 |
| thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t) |
11522 | 138 |
|
139 |
| thm_of _ _ _ = error "thm_of_proof: partial proof term"; |
|
140 |
||
20164 | 141 |
in beta_eta_convert (thm_of ([], prf_names) [] prf) end; |
11522 | 142 |
|
143 |
end; |