tuned proofs;
authorwenzelm
Fri Dec 23 20:02:30 2005 +0100 (2005-12-23)
changeset 18513791b53bf4073
parent 18512 f8df49d4af35
child 18514 0cec730b3942
tuned proofs;
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/InductTermi.thy
src/HOL/Lambda/ListBeta.thy
src/HOL/Lambda/WeakNorm.thy
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Fri Dec 23 18:36:27 2005 +0100
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Fri Dec 23 20:02:30 2005 +0100
     1.3 @@ -196,7 +196,7 @@
     1.4    and lc: "\<And>a b c. (a, b) \<in> R \<Longrightarrow> (a, c) \<in> R \<Longrightarrow>
     1.5      \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
     1.6    shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
     1.7 -               \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
     1.8 +    \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
     1.9    using wf
    1.10  proof induct
    1.11    case (less x b c)
     2.1 --- a/src/HOL/Lambda/InductTermi.thy	Fri Dec 23 18:36:27 2005 +0100
     2.2 +++ b/src/HOL/Lambda/InductTermi.thy	Fri Dec 23 20:02:30 2005 +0100
     2.3 @@ -30,9 +30,9 @@
     2.4    "s : termi beta ==> \<forall>t. t : termi beta -->
     2.5      (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> Abs r \<degree> s \<degree>\<degree> ss : termi beta)"
     2.6    apply (erule acc_induct)
     2.7 -  apply (erule thin_rl)
     2.8    apply (rule allI)
     2.9    apply (rule impI)
    2.10 +  apply (erule thin_rl)
    2.11    apply (erule acc_induct)
    2.12    apply clarify
    2.13    apply (rule accI)
     3.1 --- a/src/HOL/Lambda/ListBeta.thy	Fri Dec 23 18:36:27 2005 +0100
     3.2 +++ b/src/HOL/Lambda/ListBeta.thy	Fri Dec 23 20:02:30 2005 +0100
     3.3 @@ -17,65 +17,54 @@
     3.4  translations
     3.5    "rs => ss" == "(rs, ss) : step1 beta"
     3.6  
     3.7 -lemma head_Var_reduction_aux:
     3.8 -  "v -> v' ==> (\<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss))"
     3.9 -  apply (induct set: beta)
    3.10 +lemma head_Var_reduction:
    3.11 +  "Var n \<degree>\<degree> rs -> v \<Longrightarrow> \<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss"
    3.12 +  apply (induct u == "Var n \<degree>\<degree> rs" v fixing: rs set: beta)
    3.13       apply simp
    3.14 -    apply (rule allI)
    3.15      apply (rule_tac xs = rs in rev_exhaust)
    3.16       apply simp
    3.17 -    apply (force intro: append_step1I)
    3.18 -   apply (rule allI)
    3.19 +    apply (atomize, force intro: append_step1I)
    3.20     apply (rule_tac xs = rs in rev_exhaust)
    3.21      apply simp
    3.22      apply (auto 0 3 intro: disjI2 [THEN append_step1I])
    3.23    done
    3.24  
    3.25 -lemma head_Var_reduction:
    3.26 -  "Var n \<degree>\<degree> rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss)"
    3.27 -  by (drule head_Var_reduction_aux) blast
    3.28 -
    3.29 -lemma apps_betasE_aux:
    3.30 -  "u -> u' ==> \<forall>r rs. u = r \<degree>\<degree> rs -->
    3.31 -    ((\<exists>r'. r -> r' \<and> u' = r' \<degree>\<degree> rs) \<or>
    3.32 -     (\<exists>rs'. rs => rs' \<and> u' = r \<degree>\<degree> rs') \<or>
    3.33 -     (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] \<degree>\<degree> ts))"
    3.34 -  apply (induct set: beta)
    3.35 -     apply (clarify del: disjCI)
    3.36 -     apply (case_tac r)
    3.37 +lemma apps_betasE [elim!]:
    3.38 +  assumes major: "r \<degree>\<degree> rs -> s"
    3.39 +    and cases: "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
    3.40 +      "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
    3.41 +      "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
    3.42 +  shows R
    3.43 +proof -
    3.44 +  from major have
    3.45 +   "(\<exists>r'. r -> r' \<and> s = r' \<degree>\<degree> rs) \<or>
    3.46 +    (\<exists>rs'. rs => rs' \<and> s = r \<degree>\<degree> rs') \<or>
    3.47 +    (\<exists>t u us. r = Abs t \<and> rs = u # us \<and> s = t[u/0] \<degree>\<degree> us)"
    3.48 +    apply (induct u == "r \<degree>\<degree> rs" s fixing: r rs set: beta)
    3.49 +       apply (case_tac r)
    3.50 +         apply simp
    3.51 +        apply (simp add: App_eq_foldl_conv)
    3.52 +        apply (split split_if_asm)
    3.53 +         apply simp
    3.54 +         apply blast
    3.55 +        apply simp
    3.56 +       apply (simp add: App_eq_foldl_conv)
    3.57 +       apply (split split_if_asm)
    3.58 +        apply simp
    3.59         apply simp
    3.60 -      apply (simp add: App_eq_foldl_conv)
    3.61 +      apply (drule App_eq_foldl_conv [THEN iffD1])
    3.62        apply (split split_if_asm)
    3.63         apply simp
    3.64         apply blast
    3.65 -      apply simp
    3.66 -     apply (simp add: App_eq_foldl_conv)
    3.67 +      apply (force intro!: disjI1 [THEN append_step1I])
    3.68 +     apply (drule App_eq_foldl_conv [THEN iffD1])
    3.69       apply (split split_if_asm)
    3.70        apply simp
    3.71 -     apply simp
    3.72 -    apply (clarify del: disjCI)
    3.73 -    apply (drule App_eq_foldl_conv [THEN iffD1])
    3.74 -    apply (split split_if_asm)
    3.75 -     apply simp
    3.76 -     apply blast
    3.77 -    apply (force intro!: disjI1 [THEN append_step1I])
    3.78 -   apply (clarify del: disjCI)
    3.79 -   apply (drule App_eq_foldl_conv [THEN iffD1])
    3.80 -   apply (split split_if_asm)
    3.81 -    apply simp
    3.82 -    apply blast
    3.83 -   apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
    3.84 -  done
    3.85 -
    3.86 -lemma apps_betasE [elim!]:
    3.87 -  assumes major: "r \<degree>\<degree> rs -> s"
    3.88 -    and "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
    3.89 -    and "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
    3.90 -    and "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
    3.91 -  shows R
    3.92 -  apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
    3.93 -  apply (assumption | rule refl | erule prems exE conjE impE disjE)+
    3.94 -  done
    3.95 +      apply blast
    3.96 +     apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
    3.97 +    done
    3.98 +  with cases show ?thesis by blast
    3.99 +qed
   3.100  
   3.101  lemma apps_preserves_beta [simp]:
   3.102      "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
     4.1 --- a/src/HOL/Lambda/WeakNorm.thy	Fri Dec 23 18:36:27 2005 +0100
     4.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Fri Dec 23 20:02:30 2005 +0100
     4.3 @@ -109,9 +109,9 @@
     4.4    done
     4.5  
     4.6  lemma subst_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
     4.7 -  listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow>
     4.8 -  listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
     4.9 -  by (induct ts) simp+
    4.10 +    listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow>
    4.11 +    listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
    4.12 +  by (induct ts) simp_all
    4.13  
    4.14  lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"
    4.15    apply (induct fixing: i j set: NF)
    4.16 @@ -151,8 +151,8 @@
    4.17    done
    4.18  
    4.19  lemma lift_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
    4.20 -  listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow>
    4.21 -  listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)"
    4.22 +    listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow>
    4.23 +    listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)"
    4.24    by (induct ts) simp_all
    4.25  
    4.26  lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
    4.27 @@ -383,8 +383,9 @@
    4.28    done
    4.29  
    4.30  
    4.31 -theorem type_NF: assumes T: "e \<turnstile>\<^sub>R t : T"
    4.32 -  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using T
    4.33 +theorem type_NF:
    4.34 +  assumes "e \<turnstile>\<^sub>R t : T"
    4.35 +  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using prems
    4.36  proof induct
    4.37    case Var
    4.38    show ?case by (iprover intro: Var_NF)