--- a/src/HOL/Lambda/Lambda.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/Lambda.thy Wed Nov 23 22:26:13 2005 +0100
@@ -86,21 +86,15 @@
lemma rtrancl_beta_Abs [intro!]:
"s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
- apply (erule rtrancl_induct)
- apply (blast intro: rtrancl_into_rtrancl)+
- done
+ by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
lemma rtrancl_beta_AppL:
"s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
- apply (erule rtrancl_induct)
- apply (blast intro: rtrancl_into_rtrancl)+
- done
+ by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
lemma rtrancl_beta_AppR:
"t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
- apply (erule rtrancl_induct)
- apply (blast intro: rtrancl_into_rtrancl)+
- done
+ by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
lemma rtrancl_beta_App [intro]:
"[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
@@ -112,72 +106,51 @@
subsection {* Substitution-lemmas *}
lemma subst_eq [simp]: "(Var k)[u/k] = u"
- apply (simp add: subst_Var)
- done
+ by (simp add: subst_Var)
lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
- apply (simp add: subst_Var)
- done
+ by (simp add: subst_Var)
lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
- apply (simp add: subst_Var)
- done
+ by (simp add: subst_Var)
-lemma lift_lift [rule_format]:
- "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
- apply (induct_tac t)
- apply auto
- done
+lemma lift_lift:
+ "i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i"
+ by (induct t fixing: i k) auto
lemma lift_subst [simp]:
- "\<forall>i j s. j < i + 1 --> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
- apply (induct_tac t)
- apply (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
- done
+ "j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
+ by (induct t fixing: i j s)
+ (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
lemma lift_subst_lt:
- "\<forall>i j s. i < j + 1 --> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
- apply (induct_tac t)
- apply (simp_all add: subst_Var lift_lift)
- done
+ "i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
+ by (induct t fixing: i j s) (simp_all add: subst_Var lift_lift)
lemma subst_lift [simp]:
- "\<forall>k s. (lift t k)[s/k] = t"
- apply (induct_tac t)
- apply simp_all
- done
+ "(lift t k)[s/k] = t"
+ by (induct t fixing: k s) simp_all
-lemma subst_subst [rule_format]:
- "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
- apply (induct_tac t)
- apply (simp_all
- add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
+lemma subst_subst:
+ "i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
+ by (induct t fixing: i j u v)
+ (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
split: nat.split)
- done
subsection {* Equivalence proof for optimized substitution *}
-lemma liftn_0 [simp]: "\<forall>k. liftn 0 t k = t"
- apply (induct_tac t)
- apply (simp_all add: subst_Var)
- done
+lemma liftn_0 [simp]: "liftn 0 t k = t"
+ by (induct t fixing: k) (simp_all add: subst_Var)
-lemma liftn_lift [simp]:
- "\<forall>k. liftn (Suc n) t k = lift (liftn n t k) k"
- apply (induct_tac t)
- apply (simp_all add: subst_Var)
- done
+lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
+ by (induct t fixing: k) (simp_all add: subst_Var)
-lemma substn_subst_n [simp]:
- "\<forall>n. substn t s n = t[liftn n s 0 / n]"
- apply (induct_tac t)
- apply (simp_all add: subst_Var)
- done
+lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
+ by (induct t fixing: n) (simp_all add: subst_Var)
theorem substn_subst_0: "substn t s 0 = t[s/0]"
- apply simp
- done
+ by simp
subsection {* Preservation theorems *}
@@ -187,13 +160,11 @@
theorem subst_preserves_beta [simp]:
"r \<rightarrow>\<^sub>\<beta> s ==> (\<And>t i. r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i])"
- apply (induct set: beta)
- apply (simp_all add: subst_subst [symmetric])
- done
+ by (induct 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 (erule rtrancl.induct)
- apply (rule rtrancl_refl)
+ apply (induct set: rtrancl)
+ apply (rule rtrancl_refl)
apply (erule rtrancl_into_rtrancl)
apply (erule subst_preserves_beta)
done
@@ -203,23 +174,22 @@
by (induct set: beta) auto
theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
- apply (erule rtrancl.induct)
- apply (rule rtrancl_refl)
+ apply (induct set: rtrancl)
+ apply (rule rtrancl_refl)
apply (erule rtrancl_into_rtrancl)
apply (erule lift_preserves_beta)
done
-theorem subst_preserves_beta2 [simp]:
- "\<And>r s i. r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
- apply (induct t)
+theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
+ apply (induct t fixing: r s i)
apply (simp add: subst_Var r_into_rtrancl)
apply (simp add: rtrancl_beta_App)
apply (simp add: rtrancl_beta_Abs)
done
theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
- apply (erule rtrancl.induct)
- apply (rule rtrancl_refl)
+ apply (induct set: rtrancl)
+ apply (rule rtrancl_refl)
apply (erule rtrancl_trans)
apply (erule subst_preserves_beta2)
done