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