src/CTT/ex/Typechecking.thy
author wenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 39159 0dec18004e75
parent 36319 8feb2c4bef1a
child 58889 5b7a9633cfa8
permissions -rw-r--r--
more antiquotations;
wenzelm@19761
     1
(*  Title:      CTT/ex/Typechecking.thy
wenzelm@19761
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@19761
     3
    Copyright   1991  University of Cambridge
wenzelm@19761
     4
*)
wenzelm@19761
     5
wenzelm@19761
     6
header "Easy examples: type checking and type deduction"
wenzelm@19761
     7
wenzelm@19761
     8
theory Typechecking
wenzelm@19761
     9
imports CTT
wenzelm@19761
    10
begin
wenzelm@19761
    11
wenzelm@19761
    12
subsection {* Single-step proofs: verifying that a type is well-formed *}
wenzelm@19761
    13
wenzelm@36319
    14
schematic_lemma "?A type"
wenzelm@19761
    15
apply (rule form_rls)
wenzelm@19761
    16
done
wenzelm@19761
    17
wenzelm@36319
    18
schematic_lemma "?A type"
wenzelm@19761
    19
apply (rule form_rls)
wenzelm@19761
    20
back
wenzelm@19761
    21
apply (rule form_rls)
wenzelm@19761
    22
apply (rule form_rls)
wenzelm@19761
    23
done
wenzelm@19761
    24
wenzelm@36319
    25
schematic_lemma "PROD z:?A . N + ?B(z) type"
wenzelm@19761
    26
apply (rule form_rls)
wenzelm@19761
    27
apply (rule form_rls)
wenzelm@19761
    28
apply (rule form_rls)
wenzelm@19761
    29
apply (rule form_rls)
wenzelm@19761
    30
apply (rule form_rls)
wenzelm@19761
    31
done
wenzelm@19761
    32
wenzelm@19761
    33
wenzelm@19761
    34
subsection {* Multi-step proofs: Type inference *}
wenzelm@19761
    35
wenzelm@19761
    36
lemma "PROD w:N. N + N type"
wenzelm@19761
    37
apply (tactic form_tac)
wenzelm@19761
    38
done
wenzelm@19761
    39
wenzelm@36319
    40
schematic_lemma "<0, succ(0)> : ?A"
wenzelm@19761
    41
apply (tactic "intr_tac []")
wenzelm@19761
    42
done
wenzelm@19761
    43
wenzelm@36319
    44
schematic_lemma "PROD w:N . Eq(?A,w,w) type"
wenzelm@19761
    45
apply (tactic "typechk_tac []")
wenzelm@19761
    46
done
wenzelm@19761
    47
wenzelm@36319
    48
schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
wenzelm@19761
    49
apply (tactic "typechk_tac []")
wenzelm@19761
    50
done
wenzelm@19761
    51
wenzelm@19761
    52
text "typechecking an application of fst"
wenzelm@36319
    53
schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
wenzelm@19761
    54
apply (tactic "typechk_tac []")
wenzelm@19761
    55
done
wenzelm@19761
    56
wenzelm@19761
    57
text "typechecking the predecessor function"
wenzelm@36319
    58
schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A"
wenzelm@19761
    59
apply (tactic "typechk_tac []")
wenzelm@19761
    60
done
wenzelm@19761
    61
wenzelm@19761
    62
text "typechecking the addition function"
wenzelm@36319
    63
schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
wenzelm@19761
    64
apply (tactic "typechk_tac []")
wenzelm@19761
    65
done
wenzelm@19761
    66
wenzelm@19761
    67
(*Proofs involving arbitrary types.
wenzelm@19761
    68
  For concreteness, every type variable left over is forced to be N*)
wenzelm@39159
    69
ML {* val N_tac = TRYALL (rtac @{thm NF}) *}
wenzelm@19761
    70
wenzelm@36319
    71
schematic_lemma "lam w. <w,w> : ?A"
wenzelm@19761
    72
apply (tactic "typechk_tac []")
wenzelm@19761
    73
apply (tactic N_tac)
wenzelm@19761
    74
done
wenzelm@19761
    75
wenzelm@36319
    76
schematic_lemma "lam x. lam y. x : ?A"
wenzelm@19761
    77
apply (tactic "typechk_tac []")
wenzelm@19761
    78
apply (tactic N_tac)
wenzelm@19761
    79
done
wenzelm@19761
    80
wenzelm@19761
    81
text "typechecking fst (as a function object)"
wenzelm@36319
    82
schematic_lemma "lam i. split(i, %j k. j) : ?A"
wenzelm@19761
    83
apply (tactic "typechk_tac []")
wenzelm@19761
    84
apply (tactic N_tac)
wenzelm@19761
    85
done
wenzelm@19761
    86
wenzelm@19761
    87
end