src/CTT/ex/Typechecking.thy
author wenzelm
Wed, 17 May 2017 13:47:19 +0200
changeset 65851 c103358a5559
parent 61391 2332d9be352b
permissions -rw-r--r--
tuned signature;
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
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     3
    Copyright   1991  University of Cambridge
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     4
*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     5
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 39159
diff changeset
     6
section "Easy examples: type checking and type deduction"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     7
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     8
theory Typechecking
58974
cbc2ac19d783 simplifie sessions;
wenzelm
parents: 58972
diff changeset
     9
imports "../CTT"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    10
begin
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    11
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59498
diff changeset
    12
subsection \<open>Single-step proofs: verifying that a type is well-formed\<close>
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    13
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    14
schematic_goal "?A type"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    15
apply (rule form_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    16
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    17
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    18
schematic_goal "?A type"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    19
apply (rule form_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    20
back
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    21
apply (rule form_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    22
apply (rule form_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    23
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    24
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    25
schematic_goal "\<Prod>z:?A . N + ?B(z) type"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    26
apply (rule form_rls)
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
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    32
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    33
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59498
diff changeset
    34
subsection \<open>Multi-step proofs: Type inference\<close>
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    35
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    36
lemma "\<Prod>w:N. N + N type"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    37
apply form
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    38
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    39
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 60770
diff changeset
    40
schematic_goal "<0, succ(0)> : ?A"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    41
apply intr
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    42
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    43
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    44
schematic_goal "\<Prod>w:N . Eq(?A,w,w) type"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    45
apply typechk
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    46
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    47
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    48
schematic_goal "\<Prod>x:N . \<Prod>y:N . Eq(?A,x,y) type"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    49
apply typechk
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    50
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    51
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    52
text "typechecking an application of fst"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    53
schematic_goal "(\<^bold>\<lambda>u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    54
apply typechk
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    55
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    56
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    57
text "typechecking the predecessor function"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    58
schematic_goal "\<^bold>\<lambda>n. rec(n, 0, \<lambda>x y. x) : ?A"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    59
apply typechk
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    60
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    61
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    62
text "typechecking the addition function"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    63
schematic_goal "\<^bold>\<lambda>n. \<^bold>\<lambda>m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    64
apply typechk
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    65
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    66
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    67
(*Proofs involving arbitrary types.
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    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
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59498
diff changeset
    70
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))\<close>
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    71
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    72
schematic_goal "\<^bold>\<lambda>w. <w,w> : ?A"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    73
apply typechk
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    74
apply N
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    75
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    76
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    77
schematic_goal "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : ?A"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    78
apply typechk
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    79
apply N
19761
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)"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    83
schematic_goal "\<^bold>\<lambda>i. split(i, \<lambda>j k. j) : ?A"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    84
apply typechk
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    85
apply N
19761
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