1(*  Title:      CTT/ex/Typechecking.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1991  University of Cambridge
4*)
5
6section "Easy examples: type checking and type deduction"
7
8theory Typechecking
9imports "../CTT"
10begin
11
12subsection \<open>Single-step proofs: verifying that a type is well-formed\<close>
13
14schematic_goal "?A type"
15apply (rule form_rls)
16done
17
18schematic_goal "?A type"
19apply (rule form_rls)
20back
21apply (rule form_rls)
22apply (rule form_rls)
23done
24
25schematic_goal "\<Prod>z:?A . N + ?B(z) type"
26apply (rule form_rls)
27apply (rule form_rls)
28apply (rule form_rls)
29apply (rule form_rls)
30apply (rule form_rls)
31done
32
33
34subsection \<open>Multi-step proofs: Type inference\<close>
35
36lemma "\<Prod>w:N. N + N type"
37apply form
38done
39
40schematic_goal "<0, succ(0)> : ?A"
41apply intr
42done
43
44schematic_goal "\<Prod>w:N . Eq(?A,w,w) type"
45apply typechk
46done
47
48schematic_goal "\<Prod>x:N . \<Prod>y:N . Eq(?A,x,y) type"
49apply typechk
50done
51
52text "typechecking an application of fst"
53schematic_goal "(\<^bold>\<lambda>u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
54apply typechk
55done
56
57text "typechecking the predecessor function"
58schematic_goal "\<^bold>\<lambda>n. rec(n, 0, \<lambda>x y. x) : ?A"
59apply typechk
60done
61
62text "typechecking the addition function"
63schematic_goal "\<^bold>\<lambda>n. \<^bold>\<lambda>m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
64apply typechk
65done
66
67(*Proofs involving arbitrary types.
68  For concreteness, every type variable left over is forced to be N*)
69method_setup N =
70  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))\<close>
71
72schematic_goal "\<^bold>\<lambda>w. <w,w> : ?A"
73apply typechk
74apply N
75done
76
77schematic_goal "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : ?A"
78apply typechk
79apply N
80done
81
82text "typechecking fst (as a function object)"
83schematic_goal "\<^bold>\<lambda>i. split(i, \<lambda>j k. j) : ?A"
84apply typechk
85apply N
86done
87
88end
89