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