src/HOL/Datatype.thy
changeset 26356 2312df2efa12
parent 26339 7825c83c9eff
child 26748 4d51ddd6aa5c
     1.1 --- a/src/HOL/Datatype.thy	Thu Mar 20 12:02:51 2008 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Thu Mar 20 12:02:52 2008 +0100
     1.3 @@ -28,7 +28,6 @@
     1.4        ('a, 'b) dtree = "('a, 'b) node set"
     1.5  
     1.6  consts
     1.7 -  apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
     1.8    Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
     1.9  
    1.10    Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
    1.11 @@ -61,7 +60,6 @@
    1.12    Push_Node_def:  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    1.13  
    1.14    (*crude "lists" of nats -- needed for the constructions*)
    1.15 -  apfst_def:  "apfst == (%f (x,y). (f(x),y))"
    1.16    Push_def:   "Push == (%b h. nat_case b h)"
    1.17  
    1.18    (** operations on S-expressions -- sets of nodes **)
    1.19 @@ -105,12 +103,6 @@
    1.20  
    1.21  
    1.22  
    1.23 -(** apfst -- can be used in similar type definitions **)
    1.24 -
    1.25 -lemma apfst_conv [simp, code]: "apfst f (a, b) = (f a, b)"
    1.26 -by (simp add: apfst_def)
    1.27 -
    1.28 -
    1.29  lemma apfst_convE: 
    1.30      "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R  
    1.31       |] ==> R"