--- a/src/HOL/Lambda/Commutation.thy Fri Dec 23 18:36:27 2005 +0100
+++ b/src/HOL/Lambda/Commutation.thy Fri Dec 23 20:02:30 2005 +0100
@@ -196,7 +196,7 @@
and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
\<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
- \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
+ \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
using wf
proof induct
case (less x b c)
--- a/src/HOL/Lambda/InductTermi.thy Fri Dec 23 18:36:27 2005 +0100
+++ b/src/HOL/Lambda/InductTermi.thy Fri Dec 23 20:02:30 2005 +0100
@@ -30,9 +30,9 @@
"s : termi beta ==> \<forall>t. t : termi beta -->
(\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> Abs r \<degree> s \<degree>\<degree> ss : termi beta)"
apply (erule acc_induct)
- apply (erule thin_rl)
apply (rule allI)
apply (rule impI)
+ apply (erule thin_rl)
apply (erule acc_induct)
apply clarify
apply (rule accI)
--- a/src/HOL/Lambda/ListBeta.thy Fri Dec 23 18:36:27 2005 +0100
+++ b/src/HOL/Lambda/ListBeta.thy Fri Dec 23 20:02:30 2005 +0100
@@ -17,65 +17,54 @@
translations
"rs => ss" == "(rs, ss) : step1 beta"
-lemma head_Var_reduction_aux:
- "v -> v' ==> (\<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss))"
- apply (induct set: beta)
+lemma head_Var_reduction:
+ "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
+ apply (induct u == "Var n \<degree>\<degree> rs" v fixing: rs set: beta)
apply simp
- apply (rule allI)
apply (rule_tac xs = rs in rev_exhaust)
apply simp
- apply (force intro: append_step1I)
- apply (rule allI)
+ apply (atomize, force intro: append_step1I)
apply (rule_tac xs = rs in rev_exhaust)
apply simp
apply (auto 0 3 intro: disjI2 [THEN append_step1I])
done
-lemma head_Var_reduction:
- "Var n \<degree>\<degree> rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss)"
- by (drule head_Var_reduction_aux) blast
-
-lemma apps_betasE_aux:
- "u -> u' ==> \<forall>r rs. u = r \<degree>\<degree> rs -->
- ((\<exists>r'. r -> r' \<and> u' = r' \<degree>\<degree> rs) \<or>
- (\<exists>rs'. rs => rs' \<and> u' = r \<degree>\<degree> rs') \<or>
- (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] \<degree>\<degree> ts))"
- apply (induct set: beta)
- apply (clarify del: disjCI)
- apply (case_tac r)
+lemma apps_betasE [elim!]:
+ assumes major: "r \<degree>\<degree> rs -> s"
+ and cases: "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
+ "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
+ "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
+ shows R
+proof -
+ from major have
+ "(\<exists>r'. r -> r' \<and> s = r' \<degree>\<degree> rs) \<or>
+ (\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
+ (\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
+ apply (induct u == "r \<degree>\<degree> rs" s fixing: r rs set: beta)
+ apply (case_tac r)
+ apply simp
+ apply (simp add: App_eq_foldl_conv)
+ apply (split split_if_asm)
+ apply simp
+ apply blast
+ apply simp
+ apply (simp add: App_eq_foldl_conv)
+ apply (split split_if_asm)
+ apply simp
apply simp
- apply (simp add: App_eq_foldl_conv)
+ apply (drule App_eq_foldl_conv [THEN iffD1])
apply (split split_if_asm)
apply simp
apply blast
- apply simp
- apply (simp add: App_eq_foldl_conv)
+ apply (force intro!: disjI1 [THEN append_step1I])
+ apply (drule App_eq_foldl_conv [THEN iffD1])
apply (split split_if_asm)
apply simp
- apply simp
- apply (clarify del: disjCI)
- apply (drule App_eq_foldl_conv [THEN iffD1])
- apply (split split_if_asm)
- apply simp
- apply blast
- apply (force intro!: disjI1 [THEN append_step1I])
- apply (clarify del: disjCI)
- apply (drule App_eq_foldl_conv [THEN iffD1])
- apply (split split_if_asm)
- apply simp
- apply blast
- apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
- done
-
-lemma apps_betasE [elim!]:
- assumes major: "r \<degree>\<degree> rs -> s"
- and "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
- and "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
- and "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
- shows R
- apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
- apply (assumption | rule refl | erule prems exE conjE impE disjE)+
- done
+ apply blast
+ apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
+ done
+ with cases show ?thesis by blast
+qed
lemma apps_preserves_beta [simp]:
"r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
--- a/src/HOL/Lambda/WeakNorm.thy Fri Dec 23 18:36:27 2005 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy Fri Dec 23 20:02:30 2005 +0100
@@ -109,9 +109,9 @@
done
lemma subst_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
- listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow>
- listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
- by (induct ts) simp+
+ listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow>
+ listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
+ by (induct ts) simp_all
lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"
apply (induct fixing: i j set: NF)
@@ -151,8 +151,8 @@
done
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)"
+ 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_all
lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
@@ -383,8 +383,9 @@
done
-theorem type_NF: assumes T: "e \<turnstile>\<^sub>R t : T"
- shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using T
+theorem type_NF:
+ assumes "e \<turnstile>\<^sub>R t : T"
+ shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using prems
proof induct
case Var
show ?case by (iprover intro: Var_NF)