19761

1 
(* Title: CTT/ex/Typechecking.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 
*)


6 


7 
header "Easy examples: type checking and type deduction"


8 


9 
theory Typechecking


10 
imports CTT


11 
begin


12 


13 
subsection {* Singlestep proofs: verifying that a type is wellformed *}


14 


15 
lemma "?A type"


16 
apply (rule form_rls)


17 
done


18 


19 
lemma "?A type"


20 
apply (rule form_rls)


21 
back


22 
apply (rule form_rls)


23 
apply (rule form_rls)


24 
done


25 


26 
lemma "PROD z:?A . N + ?B(z) type"


27 
apply (rule form_rls)


28 
apply (rule form_rls)


29 
apply (rule form_rls)


30 
apply (rule form_rls)


31 
apply (rule form_rls)


32 
done


33 


34 


35 
subsection {* Multistep proofs: Type inference *}


36 


37 
lemma "PROD w:N. N + N type"


38 
apply (tactic form_tac)


39 
done


40 


41 
lemma "<0, succ(0)> : ?A"


42 
apply (tactic "intr_tac []")


43 
done


44 


45 
lemma "PROD w:N . Eq(?A,w,w) type"


46 
apply (tactic "typechk_tac []")


47 
done


48 


49 
lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"


50 
apply (tactic "typechk_tac []")


51 
done


52 


53 
text "typechecking an application of fst"


54 
lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"


55 
apply (tactic "typechk_tac []")


56 
done


57 


58 
text "typechecking the predecessor function"


59 
lemma "lam n. rec(n, 0, %x y. x) : ?A"


60 
apply (tactic "typechk_tac []")


61 
done


62 


63 
text "typechecking the addition function"


64 
lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"


65 
apply (tactic "typechk_tac []")


66 
done


67 


68 
(*Proofs involving arbitrary types.


69 
For concreteness, every type variable left over is forced to be N*)


70 
ML {* val N_tac = TRYALL (rtac (thm "NF")) *}


71 


72 
lemma "lam w. <w,w> : ?A"


73 
apply (tactic "typechk_tac []")


74 
apply (tactic N_tac)


75 
done


76 


77 
lemma "lam x. lam y. x : ?A"


78 
apply (tactic "typechk_tac []")


79 
apply (tactic N_tac)


80 
done


81 


82 
text "typechecking fst (as a function object)"


83 
lemma "lam i. split(i, %j k. j) : ?A"


84 
apply (tactic "typechk_tac []")


85 
apply (tactic N_tac)


86 
done


87 


88 
end
