author | wenzelm |
Mon, 10 Nov 2014 21:49:48 +0100 | |
changeset 58963 | 26bf09b95dda |
parent 58889 | 5b7a9633cfa8 |
child 58972 | 5b026cfc5f04 |
permissions | -rw-r--r-- |
19761 | 1 |
(* Title: CTT/ex/Typechecking.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
Copyright 1991 University of Cambridge |
|
4 |
*) |
|
5 |
||
58889 | 6 |
section "Easy examples: type checking and type deduction" |
19761 | 7 |
|
8 |
theory Typechecking |
|
9 |
imports CTT |
|
10 |
begin |
|
11 |
||
12 |
subsection {* Single-step proofs: verifying that a type is well-formed *} |
|
13 |
||
36319 | 14 |
schematic_lemma "?A type" |
19761 | 15 |
apply (rule form_rls) |
16 |
done |
|
17 |
||
36319 | 18 |
schematic_lemma "?A type" |
19761 | 19 |
apply (rule form_rls) |
20 |
back |
|
21 |
apply (rule form_rls) |
|
22 |
apply (rule form_rls) |
|
23 |
done |
|
24 |
||
36319 | 25 |
schematic_lemma "PROD z:?A . N + ?B(z) type" |
19761 | 26 |
apply (rule form_rls) |
27 |
apply (rule form_rls) |
|
28 |
apply (rule form_rls) |
|
29 |
apply (rule form_rls) |
|
30 |
apply (rule form_rls) |
|
31 |
done |
|
32 |
||
33 |
||
34 |
subsection {* Multi-step proofs: Type inference *} |
|
35 |
||
36 |
lemma "PROD w:N. N + N type" |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
37 |
apply (tactic "form_tac @{context}") |
19761 | 38 |
done |
39 |
||
36319 | 40 |
schematic_lemma "<0, succ(0)> : ?A" |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
41 |
apply (tactic "intr_tac @{context} []") |
19761 | 42 |
done |
43 |
||
36319 | 44 |
schematic_lemma "PROD w:N . Eq(?A,w,w) type" |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
45 |
apply (tactic "typechk_tac @{context} []") |
19761 | 46 |
done |
47 |
||
36319 | 48 |
schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type" |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
49 |
apply (tactic "typechk_tac @{context} []") |
19761 | 50 |
done |
51 |
||
52 |
text "typechecking an application of fst" |
|
36319 | 53 |
schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A" |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
54 |
apply (tactic "typechk_tac @{context} []") |
19761 | 55 |
done |
56 |
||
57 |
text "typechecking the predecessor function" |
|
36319 | 58 |
schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A" |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
59 |
apply (tactic "typechk_tac @{context} []") |
19761 | 60 |
done |
61 |
||
62 |
text "typechecking the addition function" |
|
36319 | 63 |
schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A" |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
64 |
apply (tactic "typechk_tac @{context} []") |
19761 | 65 |
done |
66 |
||
67 |
(*Proofs involving arbitrary types. |
|
68 |
For concreteness, every type variable left over is forced to be N*) |
|
39159 | 69 |
ML {* val N_tac = TRYALL (rtac @{thm NF}) *} |
19761 | 70 |
|
36319 | 71 |
schematic_lemma "lam w. <w,w> : ?A" |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
72 |
apply (tactic "typechk_tac @{context} []") |
19761 | 73 |
apply (tactic N_tac) |
74 |
done |
|
75 |
||
36319 | 76 |
schematic_lemma "lam x. lam y. x : ?A" |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
77 |
apply (tactic "typechk_tac @{context} []") |
19761 | 78 |
apply (tactic N_tac) |
79 |
done |
|
80 |
||
81 |
text "typechecking fst (as a function object)" |
|
36319 | 82 |
schematic_lemma "lam i. split(i, %j k. j) : ?A" |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
83 |
apply (tactic "typechk_tac @{context} []") |
19761 | 84 |
apply (tactic N_tac) |
85 |
done |
|
86 |
||
87 |
end |