src/HOL/Datatype.thy
changeset 35216 7641e8d831d2
parent 33968 f94fb13ecbb3
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/Datatype.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/Datatype.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -144,11 +144,10 @@
     1.4  (** Scons vs Atom **)
     1.5  
     1.6  lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)"
     1.7 -apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def)
     1.8 -apply (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
     1.9 +unfolding Atom_def Scons_def Push_Node_def One_nat_def
    1.10 +by (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
    1.11           dest!: Abs_Node_inj 
    1.12           elim!: apfst_convE sym [THEN Push_neq_K0])  
    1.13 -done
    1.14  
    1.15  lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard]
    1.16  
    1.17 @@ -199,14 +198,12 @@
    1.18  (** Injectiveness of Scons **)
    1.19  
    1.20  lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'"
    1.21 -apply (simp add: Scons_def One_nat_def)
    1.22 -apply (blast dest!: Push_Node_inject)
    1.23 -done
    1.24 +unfolding Scons_def One_nat_def
    1.25 +by (blast dest!: Push_Node_inject)
    1.26  
    1.27  lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'"
    1.28 -apply (simp add: Scons_def One_nat_def)
    1.29 -apply (blast dest!: Push_Node_inject)
    1.30 -done
    1.31 +unfolding Scons_def One_nat_def
    1.32 +by (blast dest!: Push_Node_inject)
    1.33  
    1.34  lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
    1.35  apply (erule equalityE)
    1.36 @@ -230,14 +227,14 @@
    1.37  (** Scons vs Leaf **)
    1.38  
    1.39  lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
    1.40 -by (simp add: Leaf_def o_def Scons_not_Atom)
    1.41 +unfolding Leaf_def o_def by (rule Scons_not_Atom)
    1.42  
    1.43  lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym, standard]
    1.44  
    1.45  (** Scons vs Numb **)
    1.46  
    1.47  lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
    1.48 -by (simp add: Numb_def o_def Scons_not_Atom)
    1.49 +unfolding Numb_def o_def by (rule Scons_not_Atom)
    1.50  
    1.51  lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard]
    1.52  
    1.53 @@ -281,14 +278,15 @@
    1.54  by (auto simp add: Atom_def ntrunc_def ndepth_K0)
    1.55  
    1.56  lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)"
    1.57 -by (simp add: Leaf_def o_def ntrunc_Atom)
    1.58 +unfolding Leaf_def o_def by (rule ntrunc_Atom)
    1.59  
    1.60  lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)"
    1.61 -by (simp add: Numb_def o_def ntrunc_Atom)
    1.62 +unfolding Numb_def o_def by (rule ntrunc_Atom)
    1.63  
    1.64  lemma ntrunc_Scons [simp]: 
    1.65      "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"
    1.66 -by (auto simp add: Scons_def ntrunc_def One_nat_def ndepth_Push_Node) 
    1.67 +unfolding Scons_def ntrunc_def One_nat_def
    1.68 +by (auto simp add: ndepth_Push_Node)
    1.69  
    1.70  
    1.71  
    1.72 @@ -351,7 +349,7 @@
    1.73  (** Injection **)
    1.74  
    1.75  lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
    1.76 -by (auto simp add: In0_def In1_def One_nat_def)
    1.77 +unfolding In0_def In1_def One_nat_def by auto
    1.78  
    1.79  lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard]
    1.80  
    1.81 @@ -417,10 +415,10 @@
    1.82  by (simp add: Scons_def, blast)
    1.83  
    1.84  lemma In0_mono: "M<=N ==> In0(M) <= In0(N)"
    1.85 -by (simp add: In0_def subset_refl Scons_mono)
    1.86 +by (simp add: In0_def Scons_mono)
    1.87  
    1.88  lemma In1_mono: "M<=N ==> In1(M) <= In1(N)"
    1.89 -by (simp add: In1_def subset_refl Scons_mono)
    1.90 +by (simp add: In1_def Scons_mono)
    1.91  
    1.92  
    1.93  (*** Split and Case ***)