src/HOL/Datatype_Universe.ML
changeset 11464 ddea204de5bc
parent 10908 a7cfffb5d7dc
child 11470 d3a3be6660f9
     1.1 --- a/src/HOL/Datatype_Universe.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Datatype_Universe.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -80,7 +80,8 @@
     1.4  
     1.5  (** Scons vs Atom **)
     1.6  
     1.7 -Goalw [Atom_def,Scons_def,Push_Node_def] "Scons M N ~= Atom(a)";
     1.8 +Goalw [Atom_def,Scons_def,Push_Node_def,One_def]
     1.9 + "Scons M N ~= Atom(a)";
    1.10  by (rtac notI 1);
    1.11  by (etac (equalityD2 RS subsetD RS UnE) 1);
    1.12  by (rtac singletonI 1);
    1.13 @@ -140,11 +141,11 @@
    1.14  
    1.15  (** Injectiveness of Scons **)
    1.16  
    1.17 -Goalw [Scons_def] "Scons M N <= Scons M' N' ==> M<=M'";
    1.18 +Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> M<=M'";
    1.19  by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
    1.20  qed "Scons_inject_lemma1";
    1.21  
    1.22 -Goalw [Scons_def] "Scons M N <= Scons M' N' ==> N<=N'";
    1.23 +Goalw [Scons_def,One_def] "Scons M N <= Scons M' N' ==> N<=N'";
    1.24  by (blast_tac (claset() addSDs [Push_Node_inject]) 1);
    1.25  qed "Scons_inject_lemma2";
    1.26  
    1.27 @@ -251,7 +252,7 @@
    1.28  by (rtac ntrunc_Atom 1);
    1.29  qed "ntrunc_Numb";
    1.30  
    1.31 -Goalw [Scons_def,ntrunc_def]
    1.32 +Goalw [Scons_def,ntrunc_def,One_def]
    1.33      "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)";
    1.34  by (safe_tac (claset() addSIs [imageI]));
    1.35  by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
    1.36 @@ -265,7 +266,7 @@
    1.37  
    1.38  (** Injection nodes **)
    1.39  
    1.40 -Goalw [In0_def] "ntrunc 1 (In0 M) = {}";
    1.41 +Goalw [In0_def] "ntrunc 1' (In0 M) = {}";
    1.42  by (Simp_tac 1);
    1.43  by (rewtac Scons_def);
    1.44  by (Blast_tac 1);
    1.45 @@ -276,7 +277,7 @@
    1.46  by (Simp_tac 1);
    1.47  qed "ntrunc_In0";
    1.48  
    1.49 -Goalw [In1_def] "ntrunc 1 (In1 M) = {}";
    1.50 +Goalw [In1_def] "ntrunc 1' (In1 M) = {}";
    1.51  by (Simp_tac 1);
    1.52  by (rewtac Scons_def);
    1.53  by (Blast_tac 1);
    1.54 @@ -338,7 +339,7 @@
    1.55  
    1.56  (** Injection **)
    1.57  
    1.58 -Goalw [In0_def,In1_def] "In0(M) ~= In1(N)";
    1.59 +Goalw [In0_def,In1_def,One_def] "In0(M) ~= In1(N)";
    1.60  by (rtac notI 1);
    1.61  by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1);
    1.62  qed "In0_not_In1";