19761

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


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1991 University of Cambridge


4 
*)


5 


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


7 


8 
theory Typechecking


9 
imports CTT


10 
begin


11 


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


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 {* Multistep proofs: Type inference *}


35 


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


37 
apply (tactic form_tac)


38 
done


39 

36319

40 
schematic_lemma "<0, succ(0)> : ?A"

19761

41 
apply (tactic "intr_tac []")


42 
done


43 

36319

44 
schematic_lemma "PROD w:N . Eq(?A,w,w) type"

19761

45 
apply (tactic "typechk_tac []")


46 
done


47 

36319

48 
schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"

19761

49 
apply (tactic "typechk_tac []")


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"

19761

54 
apply (tactic "typechk_tac []")


55 
done


56 


57 
text "typechecking the predecessor function"

36319

58 
schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A"

19761

59 
apply (tactic "typechk_tac []")


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"

19761

64 
apply (tactic "typechk_tac []")


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"

19761

72 
apply (tactic "typechk_tac []")


73 
apply (tactic N_tac)


74 
done


75 

36319

76 
schematic_lemma "lam x. lam y. x : ?A"

19761

77 
apply (tactic "typechk_tac []")


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"

19761

83 
apply (tactic "typechk_tac []")


84 
apply (tactic N_tac)


85 
done


86 


87 
end
