--- a/src/HOL/Lambda/T.thy Thu Aug 17 10:40:31 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,484 +0,0 @@
-(* Title: HOL/Lambda/Type.thy
- ID: $Id$
- Author: Stefan Berghofer
- Copyright 2000 TU Muenchen
-
-Simply-typed lambda terms. Subject reduction and strong normalization
-of simply-typed lambda terms. Partly based on a paper proof by Ralph
-Matthes.
-*)
-
-theory Type = InductTermi:
-
-datatype "typ" =
- Atom nat
- | Fun "typ" "typ" (infixr "=>" 200)
-
-consts
- typing :: "((nat => typ) * dB * typ) set"
-
-syntax
- "_typing" :: "[nat => typ, dB, typ] => bool" ("_ |- _ : _" [50,50,50] 50)
- "_funs" :: "[typ list, typ] => typ" (infixl "=>>" 150)
-
-translations
- "env |- t : T" == "(env, t, T) : typing"
- "Ts =>> T" == "foldr Fun Ts T"
-
-lemmas [intro!] = IT.BetaI IT.LambdaI IT.VarI
-
-(* FIXME
-declare IT.intros [intro!]
-*)
-
-inductive typing
-intros (* FIXME [intro!] *)
- Var: "env x = T ==> env |- Var x : T"
- Abs: "(nat_case T env) |- t : U ==> env |- (Abs t) : (T => U)"
- App: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"
-
-lemmas [intro!] = App Abs Var
-
-consts
- "types" :: "[nat => typ, dB list, typ list] => bool"
-primrec
- "types e [] Ts = (Ts = [])"
- "types e (t # ts) Ts =
- (case Ts of
- [] => False
- | T # Ts => e |- t : T & types e ts Ts)"
-
-(* FIXME order *)
-inductive_cases [elim!]:
- "e |- Abs t : T"
- "e |- t $ u : T"
- "e |- Var i : T"
-
-inductive_cases [elim!]:
- "x # xs : lists S"
-
-
-text {* Some tests. *}
-
-lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : T \<and> U = T"
- apply (intro exI conjI)
- apply force
- apply (rule refl)
- done
-
-lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : T \<and> U = T";
- apply (intro exI conjI)
- apply force
- apply (rule refl)
- done
-
-
-text {* n-ary function types *}
-
-lemma list_app_typeD [rulify]:
- "\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)"
- apply (induct_tac ts)
- apply simp
- apply (intro strip)
- apply simp
- apply (erule_tac x = "t $ a" in allE)
- apply (erule_tac x = T in allE)
- apply (erule impE)
- apply assumption
- apply (elim exE conjE)
- apply (ind_cases "e |- t $ u : T")
- apply (rule_tac x = "Ta # Ts" in exI)
- apply simp
- done
-
-lemma list_app_typeI [rulify]:
- "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
- apply (induct_tac ts)
- apply (intro strip)
- apply simp
- apply (intro strip)
- apply (case_tac Ts)
- apply simp
- apply simp
- apply (erule_tac x = "t $ a" in allE)
- apply (erule_tac x = T in allE)
- apply (erule_tac x = lista in allE)
- apply (erule impE)
- apply (erule conjE)
- apply (erule typing.App)
- apply assumption
- apply blast
- done
-
-lemma lists_types [rulify]:
- "\<forall>Ts. types e ts Ts --> ts : lists {t. \<exists>T. e |- t : T}"
- apply (induct_tac ts)
- apply (intro strip)
- apply (case_tac Ts)
- apply simp
- apply (rule lists.Nil)
- apply simp
- apply (intro strip)
- apply (case_tac Ts)
- apply simp
- apply simp
- apply (rule lists.Cons)
- apply blast
- apply blast
- done
-
-
-text {* lifting preserves termination and well-typedness *}
-
-lemma lift_map [rulify, simp]:
- "\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
- apply (induct_tac ts)
- apply simp_all
- done
-
-lemma subst_map [rulify, simp]:
- "\<forall>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts"
- apply (induct_tac ts)
- apply simp_all
- done
-
-lemma lift_IT [rulify, intro!]:
- "t : IT ==> \<forall>i. lift t i : IT"
- apply (erule IT.induct)
- apply (rule allI)
- apply (simp (no_asm))
- apply (rule conjI)
- apply
- (rule impI,
- rule IT.VarI,
- erule lists.induct,
- simp (no_asm),
- rule lists.Nil,
- simp (no_asm),
- erule IntE,
- rule lists.Cons,
- blast,
- assumption)+
- apply auto
- done
-
-lemma lifts_IT [rulify]:
- "ts : lists IT --> map (\<lambda>t. lift t 0) ts : lists IT"
- apply (induct_tac ts)
- apply auto
- done
-
-
-lemma shift_env [simp]:
- "nat_case T
- (\<lambda>j. if j < i then e j else if j = i then Ua else e (j - 1)) =
- (\<lambda>j. if j < Suc i then nat_case T e j else if j = Suc i then Ua
- else nat_case T e (j - 1))"
- apply (rule ext)
- apply (case_tac j)
- apply simp
- apply (case_tac nat)
- apply simp_all
- done
-
-lemma lift_type' [rulify]:
- "e |- t : T ==> \<forall>i U.
- (\<lambda>j. if j < i then e j
- else if j = i then U
- else e (j - 1)) |- lift t i : T"
- apply (erule typing.induct)
- apply auto
- done
-
-
-lemma lift_type [intro!]:
- "e |- t : T ==> nat_case U e |- lift t 0 : T"
- apply (subgoal_tac
- "nat_case U e =
- (\<lambda>j. if j < 0 then e j
- else if j = 0 then U else e (j - 1))")
- apply (erule ssubst)
- apply (erule lift_type')
- apply (rule ext)
- apply (case_tac j)
- apply simp_all
- done
-
-lemma lift_types [rulify]:
- "\<forall>Ts. types e ts Ts -->
- types (\<lambda>j. if j < i then e j
- else if j = i then U
- else e (j - 1)) (map (\<lambda>t. lift t i) ts) Ts"
- apply (induct_tac ts)
- apply simp
- apply (intro strip)
- apply (case_tac Ts)
- apply simp_all
- apply (rule lift_type')
- apply (erule conjunct1)
- done
-
-
-text {* substitution lemma *}
-
-lemma subst_lemma [rulify]:
- "e |- t : T ==> \<forall>e' i U u.
- e = (\<lambda>j. if j < i then e' j
- else if j = i then U
- else e' (j-1)) -->
- e' |- u : U --> e' |- t[u/i] : T"
- apply (erule typing.induct)
- apply (intro strip)
- apply (case_tac "x = i")
- apply simp
- apply (frule linorder_neq_iff [THEN iffD1])
- apply (erule disjE)
- apply simp
- apply (rule typing.Var)
- apply assumption
- apply (frule order_less_not_sym)
- apply (simp only: subst_gt split: split_if add: if_False)
- apply (rule typing.Var)
- apply assumption
- apply fastsimp
- apply fastsimp
- done
-
-lemma substs_lemma [rulify]:
- "e |- u : T ==>
- \<forall>Ts. types (\<lambda>j. if j < i then e j
- else if j = i then T else e (j - 1)) ts Ts -->
- types e (map (%t. t[u/i]) ts) Ts"
- apply (induct_tac ts)
- apply (intro strip)
- apply (case_tac Ts)
- apply simp
- apply simp
- apply (intro strip)
- apply (case_tac Ts)
- apply simp
- apply simp
- apply (erule conjE)
- apply (erule subst_lemma)
- apply (rule refl)
- apply assumption
- done
-
-
-text {* subject reduction *}
-
-lemma subject_reduction [rulify]:
- "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T"
- apply (erule typing.induct)
- apply blast
- apply blast
- apply (intro strip)
- apply (ind_cases "s $ t -> t'")
- apply hypsubst
- apply (ind_cases "env |- Abs t : T => U")
- apply (rule subst_lemma)
- apply assumption
- prefer 2
- apply assumption
- apply (rule ext)
- apply (case_tac j)
-
- apply simp
- apply simp
- apply fast
- apply fast
- (* FIXME apply auto *)
- done
-
-text {* additional lemmas *}
-
-lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])"
- apply simp
- done
-
-
-lemma subst_Var_IT [rulify]: "r : IT ==> \<forall>i j. r[Var i/j] : IT"
- apply (erule IT.induct)
- txt {* Var *}
- apply (intro strip)
- apply (simp (no_asm) add: subst_Var)
- apply
- ((rule conjI impI)+,
- rule IT.VarI,
- erule lists.induct,
- simp (no_asm),
- rule lists.Nil,
- simp (no_asm),
- erule IntE,
- erule CollectE,
- rule lists.Cons,
- fast,
- assumption)+
- txt {* Lambda *}
- apply (intro strip)
- apply simp
- apply (rule IT.LambdaI)
- apply fast
- txt {* Beta *}
- apply (intro strip)
- apply (simp (no_asm_use) add: subst_subst [symmetric])
- apply (rule IT.BetaI)
- apply auto
- done
-
-lemma Var_IT: "Var n \<in> IT"
- apply (subgoal_tac "Var n $$ [] \<in> IT")
- apply simp
- apply (rule IT.VarI)
- apply (rule lists.Nil)
- done
-
-lemma app_Var_IT: "t : IT ==> t $ Var i : IT"
- apply (erule IT.induct)
- apply (subst app_last)
- apply (rule IT.VarI)
- apply simp
- apply (rule lists.Cons)
- apply (rule Var_IT)
- apply (rule lists.Nil)
- apply (rule IT.BetaI [where ?ss = "[]", unfold foldl_Nil [THEN eq_reflection]])
- apply (erule subst_Var_IT)
- apply (rule Var_IT)
- apply (subst app_last)
- apply (rule IT.BetaI)
- apply (subst app_last [symmetric])
- apply assumption
- apply assumption
- done
-
-
-text {* Well-typed substitution preserves termination. *}
-
-lemma subst_type_IT [rulify]:
- "\<forall>t. t : IT --> (\<forall>e T u i.
- (\<lambda>j. if j < i then e j
- else if j = i then U
- else e (j - 1)) |- t : T -->
- u : IT --> e |- u : U --> t[u/i] : IT)"
- apply (rule_tac f = size and a = U in measure_induct)
- apply (rule allI)
- apply (rule impI)
- apply (erule IT.induct)
- txt {* Var *}
- apply (intro strip)
- apply (case_tac "n = i")
- txt {* n=i *}
- apply (case_tac rs)
- apply simp
- apply simp
- apply (drule list_app_typeD)
- apply (elim exE conjE)
- apply (ind_cases "e |- t $ u : T")
- apply (ind_cases "e |- Var i : T")
- apply (drule_tac s = "(?T::typ) => ?U" in sym)
- apply simp
- apply (subgoal_tac "lift u 0 $ Var 0 : IT")
- prefer 2
- apply (rule app_Var_IT)
- apply (erule lift_IT)
- apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] : IT")
- apply (simp (no_asm_use))
- apply (subgoal_tac "(Var 0 $$ map (%t. lift t 0)
- (map (%t. t[u/i]) list))[(u $ a[u/i])/0] : IT")
- apply (simp (no_asm_use) del: map_compose add: map_compose [symmetric] o_def)
- apply (erule_tac x = "Ts =>> T" in allE)
- apply (erule impE)
- apply simp
- apply (erule_tac x = "Var 0 $$
- map (%t. lift t 0) (map (%t. t[u/i]) list)" in allE)
- apply (erule impE)
- apply (rule IT.VarI)
- apply (rule lifts_IT)
- apply (drule lists_types)
- apply
- (ind_cases "x # xs : lists (Collect P)",
- erule lists_IntI [THEN lists.induct],
- assumption)
- apply fastsimp
- apply fastsimp
- apply (erule_tac x = e in allE)
- apply (erule_tac x = T in allE)
- apply (erule_tac x = "u $ a[u/i]" in allE)
- apply (erule_tac x = 0 in allE)
- apply (fastsimp intro!: list_app_typeI lift_types subst_lemma substs_lemma)
-
-(* FIXME
- apply (tactic { * fast_tac (claset()
- addSIs [thm "list_app_typeI", thm "lift_types", thm "subst_lemma", thm "substs_lemma"]
- addss simpset()) 1 * }) *)
-
- apply (erule_tac x = Ta in allE)
- apply (erule impE)
- apply simp
- apply (erule_tac x = "lift u 0 $ Var 0" in allE)
- apply (erule impE)
- apply assumption
- apply (erule_tac x = e in allE)
- apply (erule_tac x = "Ts =>> T" in allE)
- apply (erule_tac x = "a[u/i]" in allE)
- apply (erule_tac x = 0 in allE)
- apply (erule impE)
- apply (rule typing.App)
- apply (erule lift_type')
- apply (rule typing.Var)
- apply simp
- apply (fast intro!: subst_lemma)
- txt {* n~=i *}
- apply (drule list_app_typeD)
- apply (erule exE)
- apply (erule conjE)
- apply (drule lists_types)
- apply (subgoal_tac "map (%x. x[u/i]) rs : lists IT")
- apply (simp add: subst_Var)
- apply fast
- apply (erule lists_IntI [THEN lists.induct])
- apply assumption
- apply fastsimp
- apply fastsimp
- txt {* Lambda *}
- apply fastsimp
- txt {* Beta *}
- apply (intro strip)
- apply (simp (no_asm))
- apply (rule IT.BetaI)
- apply (simp (no_asm) del: subst_map add: subst_subst subst_map [symmetric])
- apply (drule subject_reduction)
- apply (rule apps_preserves_beta)
- apply (rule beta.beta)
- apply fast
- apply (drule list_app_typeD)
- apply fast
- done
-
-
-text {* main theorem: well-typed terms are strongly normalizing *}
-
-lemma type_implies_IT: "e |- t : T ==> t : IT"
- apply (erule typing.induct)
- apply (rule Var_IT)
- apply (erule IT.LambdaI)
- apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT")
- apply simp
- apply (rule subst_type_IT)
- apply (rule lists.Nil [THEN 2 lists.Cons [THEN IT.VarI], unfold foldl_Nil [THEN eq_reflection]
- foldl_Cons [THEN eq_reflection]])
- apply (erule lift_IT)
- apply (rule typing.App)
- apply (rule typing.Var)
- apply simp
- apply (erule lift_type')
- apply assumption
- apply assumption
- done
-
-theorem type_implies_termi: "e |- t : T ==> t : termi beta"
- apply (rule IT_implies_termi)
- apply (erule type_implies_IT)
- done
-
-end