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