author | wenzelm |
Fri, 06 Mar 2015 15:58:56 +0100 | |
changeset 59621 | 291934bac95e |
parent 59582 | 0fbed69ff081 |
child 60642 | 48dd1cefb4ae |
permissions | -rw-r--r-- |
45007 | 1 |
(* Title: Pure/Proof/proof_checker.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 = |
|
56161 | 19 |
let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy true) Symtab.empty in |
44057 | 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) |> |
59582 | 41 |
Proofterm.prf_subst_pbounds (map (Hyp o Thm.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 |
|
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
71 |
fun thm_of_proof thy = |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
72 |
let val lookup = lookup_thm thy in |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
73 |
fn prf => |
13670 | 74 |
let |
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
75 |
val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context; |
13670 | 76 |
|
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
77 |
fun thm_of_atom thm Ts = |
11522 | 78 |
let |
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
79 |
val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev; |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
80 |
val (fmap, thm') = Thm.varifyT_global' [] thm; |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59582
diff
changeset
|
81 |
val ctye = map (apply2 (Thm.global_ctyp_of thy)) |
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
82 |
(map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) |
11522 | 83 |
in |
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
84 |
Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm')) |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
85 |
end; |
11522 | 86 |
|
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
87 |
fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) = |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
88 |
let |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
89 |
val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name)); |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
90 |
val prop = Thm.prop_of thm; |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
91 |
val _ = |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
92 |
if is_equal prop prop' then () |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
93 |
else |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
94 |
error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^ |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
95 |
Syntax.string_of_term_global thy prop ^ "\n\n" ^ |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
96 |
Syntax.string_of_term_global thy prop'); |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
97 |
in thm_of_atom thm Ts end |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
98 |
|
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
99 |
| thm_of _ _ (PAxm (name, _, SOME Ts)) = |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
100 |
thm_of_atom (Thm.axiom thy name) Ts |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
101 |
|
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
102 |
| thm_of _ Hs (PBound i) = nth Hs i |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
103 |
|
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
104 |
| thm_of (vs, names) Hs (Abst (s, SOME T, prf)) = |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
105 |
let |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
106 |
val (x, names') = Name.variant s names; |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
107 |
val thm = thm_of ((x, T) :: vs, names') Hs prf |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
108 |
in |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59582
diff
changeset
|
109 |
Thm.forall_intr (Thm.global_cterm_of thy (Free (x, T))) thm |
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
110 |
end |
11522 | 111 |
|
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
112 |
| thm_of (vs, names) Hs (prf % SOME t) = |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
113 |
let |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
114 |
val thm = thm_of (vs, names) Hs prf; |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59582
diff
changeset
|
115 |
val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t)); |
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
116 |
in |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
117 |
Thm.forall_elim ct thm |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
118 |
handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
119 |
end |
11522 | 120 |
|
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
121 |
| thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) = |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
122 |
let |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59582
diff
changeset
|
123 |
val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t)); |
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
124 |
val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf; |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
125 |
in |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
126 |
Thm.implies_intr ct thm |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
127 |
end |
11522 | 128 |
|
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
129 |
| thm_of vars Hs (prf %% prf') = |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
130 |
let |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
131 |
val thm = beta_eta_convert (thm_of vars Hs prf); |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
132 |
val thm' = beta_eta_convert (thm_of vars Hs prf'); |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
133 |
in |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
134 |
Thm.implies_elim thm thm' |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
135 |
handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf' |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
136 |
end |
11522 | 137 |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59582
diff
changeset
|
138 |
| thm_of _ _ (Hyp t) = Thm.assume (Thm.global_cterm_of thy t) |
11522 | 139 |
|
44061
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
140 |
| thm_of _ _ _ = error "thm_of_proof: partial proof term"; |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
141 |
|
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
142 |
in beta_eta_convert (thm_of ([], prf_names) [] prf) end |
9f17ede679e9
tuned thm_of_proof: build lookup table within closure;
wenzelm
parents:
44058
diff
changeset
|
143 |
end; |
11522 | 144 |
|
145 |
end; |