Theory Typechecking

(*  Title:      CTT/ex/Typechecking.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge
*)

section "Easy examples: type checking and type deduction"

theory Typechecking
imports "../CTT"
begin

subsection Single-step proofs: verifying that a type is well-formed

schematic_goal "?A type"
apply (rule form_rls)
done

schematic_goal "?A type"
apply (rule form_rls)
back
apply (rule form_rls)
apply (rule form_rls)
done

schematic_goal "z:?A . N + ?B(z) type"
apply (rule form_rls)
apply (rule form_rls)
apply (rule form_rls)
apply (rule form_rls)
apply (rule form_rls)
done


subsection Multi-step proofs: Type inference

lemma "w:N. N + N type"
apply form
done

schematic_goal "<0, succ(0)> : ?A"
apply intr
done

schematic_goal "w:N . Eq(?A,w,w) type"
apply typechk
done

schematic_goal "x:N . y:N . Eq(?A,x,y) type"
apply typechk
done

text "typechecking an application of fst"
schematic_goal "(λu. split(u, λv w. v)) ` <0, succ(0)> : ?A"
apply typechk
done

text "typechecking the predecessor function"
schematic_goal "λn. rec(n, 0, λx y. x) : ?A"
apply typechk
done

text "typechecking the addition function"
schematic_goal "λn. λm. rec(n, m, λx y. succ(y)) : ?A"
apply typechk
done

(*Proofs involving arbitrary types.
  For concreteness, every type variable left over is forced to be N*)
method_setup N =
  Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))

schematic_goal "λw. <w,w> : ?A"
apply typechk
apply N
done

schematic_goal "λx. λy. x : ?A"
apply typechk
apply N
done

text "typechecking fst (as a function object)"
schematic_goal "λi. split(i, λj k. j) : ?A"
apply typechk
apply N
done

end