--- a/src/HOL/Lambda/Type.thy Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/Type.thy Wed Feb 07 17:44:07 2007 +0100
@@ -45,8 +45,18 @@
Atom nat
| Fun type type (infixr "\<Rightarrow>" 200)
+inductive2 typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+ where
+ Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
+ | Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)"
+ | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
+
+inductive_cases2 typing_elims [elim!]:
+ "e \<turnstile> Var i : T"
+ "e \<turnstile> t \<degree> u : T"
+ "e \<turnstile> Abs t : T"
+
consts
- typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
abbreviation
@@ -54,32 +64,14 @@
"Ts =>> T == foldr Fun Ts T"
abbreviation
- typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool" ("_ |- _ : _" [50, 50, 50] 50) where
- "env |- t : T == (env, t, T) \<in> typing"
-
-abbreviation
typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
("_ ||- _ : _" [50, 50, 50] 50) where
"env ||- ts : Ts == typings env ts Ts"
-notation (xsymbols)
- typing_rel ("_ \<turnstile> _ : _" [50, 50, 50] 50)
-
notation (latex)
funs (infixr "\<Rrightarrow>" 200) and
typings_rel ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
-inductive typing
- intros
- Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
- Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)"
- App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
-
-inductive_cases typing_elims [elim!]:
- "e \<turnstile> Var i : T"
- "e \<turnstile> t \<degree> u : T"
- "e \<turnstile> Abs t : T"
-
primrec
"(e \<tturnstile> [] : Ts) = (Ts = [])"
"(e \<tturnstile> (t # ts) : Ts) =
@@ -100,16 +92,16 @@
subsection {* Lists of types *}
lemma lists_typings:
- "e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
+ "e \<tturnstile> ts : Ts \<Longrightarrow> listsp (\<lambda>t. \<exists>T. e \<turnstile> t : T) ts"
apply (induct ts arbitrary: Ts)
apply (case_tac Ts)
apply simp
- apply (rule lists.Nil)
+ apply (rule listsp.Nil)
apply simp
apply (case_tac Ts)
apply simp
apply simp
- apply (rule lists.Cons)
+ apply (rule listsp.Cons)
apply blast
apply blast
done
@@ -172,7 +164,7 @@
apply (erule impE)
apply assumption
apply (elim exE conjE)
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply (rule_tac x = "Ta # Ts" in exI)
apply simp
done
@@ -210,12 +202,12 @@
"e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
apply (induct ts arbitrary: T U rule: rev_induct)
apply simp
- apply (ind_cases "e \<turnstile> Var i : T")
- apply (ind_cases "e \<turnstile> Var i : T")
+ apply (ind_cases2 "e \<turnstile> Var i : T" for T)
+ apply (ind_cases2 "e \<turnstile> Var i : T" for T)
apply simp
apply simp
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply atomize
apply (erule_tac x="Ta \<Rightarrow> T" in allE)
apply (erule_tac x="Tb \<Rightarrow> U" in allE)
@@ -238,7 +230,7 @@
apply (rule FalseE)
apply simp
apply (erule list_app_typeE)
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
apply assumption
apply simp
@@ -250,7 +242,7 @@
apply (rule types_snoc)
apply assumption
apply (erule list_app_typeE)
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply (drule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
apply assumption
apply simp
@@ -258,7 +250,7 @@
apply (rule typing.App)
apply assumption
apply (erule list_app_typeE)
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply (frule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
apply assumption
apply simp
@@ -266,7 +258,7 @@
apply (rule_tac x="type1 # Us" in exI)
apply simp
apply (erule list_app_typeE)
- apply (ind_cases "e \<turnstile> t \<degree> u : T")
+ apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
apply (frule_tac T="type1 \<Rightarrow> Us \<Rrightarrow> T" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
apply assumption
apply simp
@@ -281,13 +273,13 @@
lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P"
apply (cases T)
apply (rule FalseE)
- apply (erule typing.elims)
+ apply (erule typing.cases)
apply simp_all
apply atomize
apply (erule_tac x="type1" in allE)
apply (erule_tac x="type2" in allE)
apply (erule mp)
- apply (erule typing.elims)
+ apply (erule typing.cases)
apply simp_all
done
@@ -335,14 +327,14 @@
subsection {* Subject reduction *}
-lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t -> t' \<Longrightarrow> e \<turnstile> t' : T"
+lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> e \<turnstile> t' : T"
apply (induct arbitrary: t' set: typing)
apply blast
apply blast
apply atomize
- apply (ind_cases "s \<degree> t -> t'")
+ apply (ind_cases2 "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t')
apply hypsubst
- apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U")
+ apply (ind_cases2 "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U)
apply (rule subst_lemma)
apply assumption
apply assumption