--- a/src/HOL/Lambda/Eta.thy Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/Eta.thy Fri Nov 25 19:09:44 2005 +0100
@@ -67,16 +67,16 @@
apply (simp add: diff_Suc subst_Var split: nat.split)
done
-lemma free_eta: "s -e> t ==> (!!i. free t i = free s i)"
- by (induct set: eta) (simp_all cong: conj_cong)
+lemma free_eta: "s -e> t ==> free t i = free s i"
+ by (induct fixing: i set: eta) (simp_all cong: conj_cong)
lemma not_free_eta:
"[| s -e> t; \<not> free s i |] ==> \<not> free t i"
by (simp add: free_eta)
lemma eta_subst [simp]:
- "s -e> t ==> (!!u i. s[u/i] -e> t[u/i])"
- by (induct set: eta) (simp_all add: subst_subst [symmetric])
+ "s -e> t ==> s[u/i] -e> t[u/i]"
+ by (induct fixing: u i set: eta) (simp_all add: subst_subst [symmetric])
theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
by (induct s fixing: i dummy) simp_all
@@ -122,17 +122,17 @@
subsection "Commutation of beta and eta"
lemma free_beta:
- "s -> t ==> (!!i. free t i \<Longrightarrow> free s i)"
- by (induct set: beta) auto
+ "s -> t ==> free t i \<Longrightarrow> free s i"
+ by (induct fixing: i set: beta) auto
-lemma beta_subst [intro]: "s -> t ==> (!!u i. s[u/i] -> t[u/i])"
- by (induct set: beta) (simp_all add: subst_subst [symmetric])
+lemma beta_subst [intro]: "s -> t ==> s[u/i] -> t[u/i]"
+ by (induct fixing: u i set: beta) (simp_all add: subst_subst [symmetric])
lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
by (induct t fixing: i) (auto elim!: linorder_neqE simp: subst_Var)
-lemma eta_lift [simp]: "s -e> t ==> (!!i. lift s i -e> lift t i)"
- by (induct set: eta) simp_all
+lemma eta_lift [simp]: "s -e> t ==> lift s i -e> lift t i"
+ by (induct fixing: i set: eta) simp_all
lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]"
apply (induct u fixing: s t i)
--- a/src/HOL/Lambda/Lambda.thy Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/Lambda.thy Fri Nov 25 19:09:44 2005 +0100
@@ -159,8 +159,8 @@
Normalization. \medskip *}
theorem subst_preserves_beta [simp]:
- "r \<rightarrow>\<^sub>\<beta> s ==> (\<And>t i. r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i])"
- by (induct set: beta) (simp_all add: subst_subst [symmetric])
+ "r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
+ by (induct fixing: t i set: beta) (simp_all add: subst_subst [symmetric])
theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
apply (induct set: rtrancl)
@@ -170,8 +170,8 @@
done
theorem lift_preserves_beta [simp]:
- "r \<rightarrow>\<^sub>\<beta> s ==> (\<And>i. lift r i \<rightarrow>\<^sub>\<beta> lift s i)"
- by (induct set: beta) auto
+ "r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
+ by (induct fixing: i set: beta) auto
theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
apply (induct set: rtrancl)
--- a/src/HOL/Lambda/ListApplication.thy Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/ListApplication.thy Fri Nov 25 19:09:44 2005 +0100
@@ -53,11 +53,11 @@
done
lemma Abs_App_neq_Var_apps [iff]:
- "Abs s \<degree> t ~= Var n \<degree>\<degree> ss"
+ "Abs s \<degree> t \<noteq> Var n \<degree>\<degree> ss"
by (induct ss fixing: s t rule: rev_induct) auto
lemma Var_apps_neq_Abs_apps [iff]:
- "Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
+ "Var n \<degree>\<degree> ts \<noteq> Abs r \<degree>\<degree> ss"
apply (induct ss fixing: ts rule: rev_induct)
apply simp
apply (induct_tac ts rule: rev_induct)
--- a/src/HOL/Lambda/ListOrder.thy Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/ListOrder.thy Fri Nov 25 19:09:44 2005 +0100
@@ -64,12 +64,13 @@
apply (blast intro: append_eq_appendI)
done
-lemma Cons_step1E [rule_format, elim!]:
- "[| (ys, x # xs) \<in> step1 r;
- \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
- \<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R
- |] ==> R"
- apply (case_tac ys)
+lemma Cons_step1E [elim!]:
+ assumes "(ys, x # xs) \<in> step1 r"
+ and "!!y. ys = y # xs \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> R"
+ and "!!zs. ys = x # zs \<Longrightarrow> (zs, xs) \<in> step1 r \<Longrightarrow> R"
+ shows R
+ using prems
+ apply (cases ys)
apply (simp add: step1_def)
apply blast
done
@@ -88,8 +89,8 @@
done
lemma Cons_acc_step1I [intro!]:
- "x \<in> acc r ==> (!!xs. xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r))"
- apply (induct set: acc)
+ "x \<in> acc r ==> xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r)"
+ apply (induct fixing: xs set: acc)
apply (erule thin_rl)
apply (erule acc_induct)
apply (rule accI)
--- a/src/HOL/Lambda/StrongNorm.thy Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/StrongNorm.thy Fri Nov 25 19:09:44 2005 +0100
@@ -16,8 +16,8 @@
subsection {* Properties of @{text IT} *}
-lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> (\<And>i. lift t i \<in> IT)"
- apply (induct set: IT)
+lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> lift t i \<in> IT"
+ apply (induct fixing: i set: IT)
apply (simp (no_asm))
apply (rule conjI)
apply
@@ -37,8 +37,8 @@
lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT"
by (induct ts) auto
-lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> (\<And>i j. r[Var i/j] \<in> IT)"
- apply (induct set: IT)
+lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> r[Var i/j] \<in> IT"
+ apply (induct fixing: i j set: IT)
txt {* Case @{term Var}: *}
apply (simp (no_asm) add: subst_Var)
apply
@@ -249,34 +249,33 @@
subsection {* Well-typed terms are strongly normalizing *}
-lemma type_implies_IT: "e \<turnstile> t : T \<Longrightarrow> t \<in> IT"
-proof -
- assume "e \<turnstile> t : T"
- thus ?thesis
- proof induct
- case Var
- show ?case by (rule Var_IT)
- next
- case Abs
- show ?case by (rule IT.Lambda)
- next
- case (App T U e s t)
- have "(Var 0 \<degree> lift t 0)[s/0] \<in> IT"
- proof (rule subst_type_IT)
- have "lift t 0 \<in> IT" by (rule lift_IT)
- hence "[lift t 0] \<in> lists IT" by (rule lists.Cons) (rule lists.Nil)
- hence "Var 0 \<degree>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
- also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
- finally show "\<dots> \<in> IT" .
- have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
- by (rule typing.Var) simp
- moreover have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
- by (rule lift_type)
- ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U"
- by (rule typing.App)
- qed
- thus ?case by simp
+lemma type_implies_IT:
+ assumes "e \<turnstile> t : T"
+ shows "t \<in> IT"
+ using prems
+proof induct
+ case Var
+ show ?case by (rule Var_IT)
+next
+ case Abs
+ show ?case by (rule IT.Lambda)
+next
+ case (App T U e s t)
+ have "(Var 0 \<degree> lift t 0)[s/0] \<in> IT"
+ proof (rule subst_type_IT)
+ have "lift t 0 \<in> IT" by (rule lift_IT)
+ hence "[lift t 0] \<in> lists IT" by (rule lists.Cons) (rule lists.Nil)
+ hence "Var 0 \<degree>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
+ also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
+ finally show "\<dots> \<in> IT" .
+ have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
+ by (rule typing.Var) simp
+ moreover have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
+ by (rule lift_type)
+ ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U"
+ by (rule typing.App)
qed
+ thus ?case by simp
qed
theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> t \<in> termi beta"
--- a/src/HOL/Lambda/Type.thy Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/Type.thy Fri Nov 25 19:09:44 2005 +0100
@@ -288,8 +288,8 @@
subsection {* Lifting preserves well-typedness *}
-lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> (\<And>i U. e\<langle>i:U\<rangle> \<turnstile> lift t i : T)"
- by (induct set: typing) auto
+lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
+ by (induct fixing: i U set: typing) auto
lemma lift_types:
"e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
@@ -303,8 +303,8 @@
subsection {* Substitution lemmas *}
lemma subst_lemma:
- "e \<turnstile> t : T \<Longrightarrow> (\<And>e' i U u. e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T)"
- apply (induct set: typing)
+ "e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T"
+ apply (induct fixing: e' i U u set: typing)
apply (rule_tac x = x and y = i in linorder_cases)
apply auto
apply blast
@@ -329,8 +329,8 @@
subsection {* Subject reduction *}
-lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> (\<And>t'. t -> t' \<Longrightarrow> e \<turnstile> t' : T)"
- apply (induct set: typing)
+lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t -> t' \<Longrightarrow> e \<turnstile> t' : T"
+ apply (induct fixing: t' set: typing)
apply blast
apply blast
apply atomize
--- a/src/HOL/Lambda/WeakNorm.thy Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy Fri Nov 25 19:09:44 2005 +0100
@@ -113,8 +113,8 @@
listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
by (induct ts) simp+
-lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> (\<And>i j. t[Var i/j] \<in> NF)"
- apply (induct set: NF)
+lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"
+ apply (induct fixing: i j set: NF)
apply simp
apply (frule listall_conj1)
apply (drule listall_conj2)
@@ -153,10 +153,10 @@
lemma lift_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow>
listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)"
- by (induct ts) simp+
+ by (induct ts) simp_all
-lemma lift_NF: "t \<in> NF \<Longrightarrow> (\<And>i. lift t i \<in> NF)"
- apply (induct set: NF)
+lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
+ apply (induct fixing: i set: NF)
apply (frule listall_conj1)
apply (drule listall_conj2)
apply (drule_tac i=i in lift_terms_NF)