author  immler 
Sun, 27 Oct 2019 21:51:14 0400  
changeset 71035  6fe5a0e1fa8e 
parent 61391  2332d9be352b 
permissions  rwrr 
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 

58974  9 
imports "../CTT" 
19761  10 
begin 
11 

60770  12 
subsection \<open>Singlestep proofs: verifying that a type is wellformed\<close> 
19761  13 

61337  14 
schematic_goal "?A type" 
19761  15 
apply (rule form_rls) 
16 
done 

17 

61337  18 
schematic_goal "?A type" 
19761  19 
apply (rule form_rls) 
20 
back 

21 
apply (rule form_rls) 

22 
apply (rule form_rls) 

23 
done 

24 

61391  25 
schematic_goal "\<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 

60770  34 
subsection \<open>Multistep proofs: Type inference\<close> 
19761  35 

61391  36 
lemma "\<Prod>w:N. N + N type" 
58972  37 
apply form 
19761  38 
done 
39 

61337  40 
schematic_goal "<0, succ(0)> : ?A" 
58972  41 
apply intr 
19761  42 
done 
43 

61391  44 
schematic_goal "\<Prod>w:N . Eq(?A,w,w) type" 
58972  45 
apply typechk 
19761  46 
done 
47 

61391  48 
schematic_goal "\<Prod>x:N . \<Prod>y:N . Eq(?A,x,y) type" 
58972  49 
apply typechk 
19761  50 
done 
51 

52 
text "typechecking an application of fst" 

61391  53 
schematic_goal "(\<^bold>\<lambda>u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A" 
58972  54 
apply typechk 
19761  55 
done 
56 

57 
text "typechecking the predecessor function" 

61391  58 
schematic_goal "\<^bold>\<lambda>n. rec(n, 0, \<lambda>x y. x) : ?A" 
58972  59 
apply typechk 
19761  60 
done 
61 

62 
text "typechecking the addition function" 

61391  63 
schematic_goal "\<^bold>\<lambda>n. \<^bold>\<lambda>m. rec(n, m, \<lambda>x y. succ(y)) : ?A" 
58972  64 
apply typechk 
19761  65 
done 
66 

67 
(*Proofs involving arbitrary types. 

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

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58977
diff
changeset

69 
method_setup N = 
60770  70 
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))\<close> 
19761  71 

61391  72 
schematic_goal "\<^bold>\<lambda>w. <w,w> : ?A" 
58972  73 
apply typechk 
74 
apply N 

19761  75 
done 
76 

61391  77 
schematic_goal "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : ?A" 
58972  78 
apply typechk 
79 
apply N 

19761  80 
done 
81 

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

61391  83 
schematic_goal "\<^bold>\<lambda>i. split(i, \<lambda>j k. j) : ?A" 
58972  84 
apply typechk 
85 
apply N 

19761  86 
done 
87 

88 
end 