src/HOL/Lambda/Type.thy
author wenzelm
Sat Apr 08 22:51:06 2006 +0200 (2006-04-08)
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
child 19380 b808efaa5828
permissions -rw-r--r--
refined 'abbreviation';
     1 (*  Title:      HOL/Lambda/Type.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer
     4     Copyright   2000 TU Muenchen
     5 *)
     6 
     7 header {* Simply-typed lambda terms *}
     8 
     9 theory Type imports ListApplication begin
    10 
    11 
    12 subsection {* Environments *}
    13 
    14 definition
    15   shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
    16   "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
    17 
    18 abbreviation (xsymbols)
    19   shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    20   "e\<langle>i:a\<rangle> == e<i:a>"
    21 
    22 abbreviation (HTML output)
    23   shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
    24   "shift == xsymbols.shift"
    25 
    26 lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
    27   by (simp add: shift_def)
    28 
    29 lemma shift_gt [simp]: "j < i \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e j"
    30   by (simp add: shift_def)
    31 
    32 lemma shift_lt [simp]: "i < j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = e (j - 1)"
    33   by (simp add: shift_def)
    34 
    35 lemma shift_commute [simp]: "e\<langle>i:U\<rangle>\<langle>0:T\<rangle> = e\<langle>0:T\<rangle>\<langle>Suc i:U\<rangle>"
    36   apply (rule ext)
    37   apply (case_tac x)
    38    apply simp
    39   apply (case_tac nat)
    40    apply (simp_all add: shift_def)
    41   done
    42 
    43 
    44 subsection {* Types and typing rules *}
    45 
    46 datatype type =
    47     Atom nat
    48   | Fun type type    (infixr "\<Rightarrow>" 200)
    49 
    50 consts
    51   typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
    52   typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    53 
    54 abbreviation
    55   funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "=>>" 200)
    56   "Ts =>> T == foldr Fun Ts T"
    57 
    58   typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |- _ : _" [50, 50, 50] 50)
    59   "env |- t : T == (env, t, T) \<in> typing"
    60 
    61   typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    62     ("_ ||- _ : _" [50, 50, 50] 50)
    63   "env ||- ts : Ts == typings env ts Ts"
    64 
    65 abbreviation (xsymbols)
    66   typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
    67   "env \<turnstile> t : T == env |- t : T"
    68 
    69 abbreviation (latex)
    70   funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
    71   "op \<Rrightarrow> == op =>>"
    72   typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
    73     ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
    74   "env \<tturnstile> ts : Ts == env ||- ts : Ts"
    75 
    76 inductive typing
    77   intros
    78     Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
    79     Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)"
    80     App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
    81 
    82 inductive_cases typing_elims [elim!]:
    83   "e \<turnstile> Var i : T"
    84   "e \<turnstile> t \<degree> u : T"
    85   "e \<turnstile> Abs t : T"
    86 
    87 primrec
    88   "(e \<tturnstile> [] : Ts) = (Ts = [])"
    89   "(e \<tturnstile> (t # ts) : Ts) =
    90     (case Ts of
    91       [] \<Rightarrow> False
    92     | T # Ts \<Rightarrow> e \<turnstile> t : T \<and> e \<tturnstile> ts : Ts)"
    93 
    94 
    95 subsection {* Some examples *}
    96 
    97 lemma "e \<turnstile> Abs (Abs (Abs (Var 1 \<degree> (Var 2 \<degree> Var 1 \<degree> Var 0)))) : ?T"
    98   by force
    99 
   100 lemma "e \<turnstile> Abs (Abs (Abs (Var 2 \<degree> Var 0 \<degree> (Var 1 \<degree> Var 0)))) : ?T"
   101   by force
   102 
   103 
   104 subsection {* Lists of types *}
   105 
   106 lemma lists_typings:
   107     "e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
   108   apply (induct ts fixing: Ts)
   109    apply (case_tac Ts)
   110      apply simp
   111      apply (rule lists.Nil)
   112     apply simp
   113   apply (case_tac Ts)
   114    apply simp
   115   apply simp
   116   apply (rule lists.Cons)
   117    apply blast
   118   apply blast
   119   done
   120 
   121 lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]"
   122   apply (induct ts fixing: Ts)
   123   apply simp
   124   apply (case_tac Ts)
   125   apply simp+
   126   done
   127 
   128 lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] =
   129   (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)"
   130   apply (induct ts fixing: Ts)
   131   apply (case_tac Ts)
   132   apply simp+
   133   apply (case_tac Ts)
   134   apply (case_tac "ts @ [t]")
   135   apply simp+
   136   done
   137 
   138 lemma rev_exhaust2 [case_names Nil snoc, extraction_expand]:
   139   "(xs = [] \<Longrightarrow> P) \<Longrightarrow> (\<And>ys y. xs = ys @ [y] \<Longrightarrow> P) \<Longrightarrow> P"
   140   -- {* Cannot use @{text rev_exhaust} from the @{text List}
   141     theory, since it is not constructive *}
   142   apply (subgoal_tac "\<forall>ys. xs = rev ys \<longrightarrow> P")
   143   apply (erule_tac x="rev xs" in allE)
   144   apply simp
   145   apply (rule allI)
   146   apply (rule impI)
   147   apply (case_tac ys)
   148   apply simp
   149   apply simp
   150   apply atomize
   151   apply (erule allE)+
   152   apply (erule mp, rule conjI)
   153   apply (rule refl)+
   154   done
   155 
   156 lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts \<Longrightarrow>
   157   (\<And>Us U. Ts = Us @ [U] \<Longrightarrow> e \<tturnstile> ts : Us \<Longrightarrow> e \<turnstile> t : U \<Longrightarrow> P) \<Longrightarrow> P"
   158   apply (cases Ts rule: rev_exhaust2)
   159   apply simp
   160   apply (case_tac "ts @ [t]")
   161   apply (simp add: types_snoc_eq)+
   162   apply iprover
   163   done
   164 
   165 
   166 subsection {* n-ary function types *}
   167 
   168 lemma list_app_typeD:
   169     "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
   170   apply (induct ts fixing: t T)
   171    apply simp
   172   apply atomize
   173   apply simp
   174   apply (erule_tac x = "t \<degree> a" in allE)
   175   apply (erule_tac x = T in allE)
   176   apply (erule impE)
   177    apply assumption
   178   apply (elim exE conjE)
   179   apply (ind_cases "e \<turnstile> t \<degree> u : T")
   180   apply (rule_tac x = "Ta # Ts" in exI)
   181   apply simp
   182   done
   183 
   184 lemma list_app_typeE:
   185   "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C"
   186   by (insert list_app_typeD) fast
   187 
   188 lemma list_app_typeI:
   189     "e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
   190   apply (induct ts fixing: t T Ts)
   191    apply simp
   192   apply atomize
   193   apply (case_tac Ts)
   194    apply simp
   195   apply simp
   196   apply (erule_tac x = "t \<degree> a" in allE)
   197   apply (erule_tac x = T in allE)
   198   apply (erule_tac x = list in allE)
   199   apply (erule impE)
   200    apply (erule conjE)
   201    apply (erule typing.App)
   202    apply assumption
   203   apply blast
   204   done
   205 
   206 text {*
   207 For the specific case where the head of the term is a variable,
   208 the following theorems allow to infer the types of the arguments
   209 without analyzing the typing derivation. This is crucial
   210 for program extraction.
   211 *}
   212 
   213 theorem var_app_type_eq:
   214   "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
   215   apply (induct ts fixing: T U rule: rev_induct)
   216   apply simp
   217   apply (ind_cases "e \<turnstile> Var i : T")
   218   apply (ind_cases "e \<turnstile> Var i : T")
   219   apply simp
   220   apply simp
   221   apply (ind_cases "e \<turnstile> t \<degree> u : T")
   222   apply (ind_cases "e \<turnstile> t \<degree> u : T")
   223   apply atomize
   224   apply (erule_tac x="Ta \<Rightarrow> T" in allE)
   225   apply (erule_tac x="Tb \<Rightarrow> U" in allE)
   226   apply (erule impE)
   227   apply assumption
   228   apply (erule impE)
   229   apply assumption
   230   apply simp
   231   done
   232 
   233 lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow>
   234   e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us"
   235   apply (induct us fixing: ts Ts U)
   236   apply simp
   237   apply (erule var_app_type_eq)
   238   apply assumption
   239   apply simp
   240   apply atomize
   241   apply (case_tac U)
   242   apply (rule FalseE)
   243   apply simp
   244   apply (erule list_app_typeE)
   245   apply (ind_cases "e \<turnstile> t \<degree> u : T")
   246   apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   247   apply assumption
   248   apply simp
   249   apply (erule_tac x="ts @ [a]" in allE)
   250   apply (erule_tac x="Ts @ [type1]" in allE)
   251   apply (erule_tac x="type2" in allE)
   252   apply simp
   253   apply (erule impE)
   254   apply (rule types_snoc)
   255   apply assumption
   256   apply (erule list_app_typeE)
   257   apply (ind_cases "e \<turnstile> t \<degree> u : T")
   258   apply (drule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   259   apply assumption
   260   apply simp
   261   apply (erule impE)
   262   apply (rule typing.App)
   263   apply assumption
   264   apply (erule list_app_typeE)
   265   apply (ind_cases "e \<turnstile> t \<degree> u : T")
   266   apply (frule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   267   apply assumption
   268   apply simp
   269   apply (erule exE)
   270   apply (rule_tac x="type1 # Us" in exI)
   271   apply simp
   272   apply (erule list_app_typeE)
   273   apply (ind_cases "e \<turnstile> t \<degree> u : T")
   274   apply (frule_tac T="type1 \<Rightarrow> Us \<Rrightarrow> T" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   275   apply assumption
   276   apply simp
   277   done
   278 
   279 lemma var_app_typesE: "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow>
   280   (\<And>Ts. e \<turnstile> Var i : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> P) \<Longrightarrow> P"
   281   apply (drule var_app_types [of _ _ "[]", simplified])
   282   apply (iprover intro: typing.Var)+
   283   done
   284 
   285 lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P"
   286   apply (cases T)
   287   apply (rule FalseE)
   288   apply (erule typing.elims)
   289   apply simp_all
   290   apply atomize
   291   apply (erule_tac x="type1" in allE)
   292   apply (erule_tac x="type2" in allE)
   293   apply (erule mp)
   294   apply (erule typing.elims)
   295   apply simp_all
   296   done
   297 
   298 
   299 subsection {* Lifting preserves well-typedness *}
   300 
   301 lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
   302   by (induct fixing: i U set: typing) auto
   303 
   304 lemma lift_types:
   305   "e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
   306   apply (induct ts fixing: Ts)
   307    apply simp
   308   apply (case_tac Ts)
   309    apply auto
   310   done
   311 
   312 
   313 subsection {* Substitution lemmas *}
   314 
   315 lemma subst_lemma:
   316     "e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T"
   317   apply (induct fixing: e' i U u set: typing)
   318     apply (rule_tac x = x and y = i in linorder_cases)
   319       apply auto
   320   apply blast
   321   done
   322 
   323 lemma substs_lemma:
   324   "e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
   325      e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
   326   apply (induct ts fixing: Ts)
   327    apply (case_tac Ts)
   328     apply simp
   329    apply simp
   330   apply atomize
   331   apply (case_tac Ts)
   332    apply simp
   333   apply simp
   334   apply (erule conjE)
   335   apply (erule (1) subst_lemma)
   336   apply (rule refl)
   337   done
   338 
   339 
   340 subsection {* Subject reduction *}
   341 
   342 lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t -> t' \<Longrightarrow> e \<turnstile> t' : T"
   343   apply (induct fixing: t' set: typing)
   344     apply blast
   345    apply blast
   346   apply atomize
   347   apply (ind_cases "s \<degree> t -> t'")
   348     apply hypsubst
   349     apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U")
   350     apply (rule subst_lemma)
   351       apply assumption
   352      apply assumption
   353     apply (rule ext)
   354     apply (case_tac x)
   355      apply auto
   356   done
   357 
   358 theorem subject_reduction': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<turnstile> t' : T"
   359   by (induct set: rtrancl) (iprover intro: subject_reduction)+
   360 
   361 
   362 subsection {* Alternative induction rule for types *}
   363 
   364 lemma type_induct [induct type]:
   365   assumes
   366   "(\<And>T. (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow>
   367     (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T)"
   368   shows "P T"
   369 proof (induct T)
   370   case Atom
   371   show ?case by (rule prems) simp_all
   372 next
   373   case Fun
   374   show ?case  by (rule prems) (insert Fun, simp_all)
   375 qed
   376 
   377 end