src/HOL/Univ.thy
changeset 1531 e5eb247ad13c
parent 1475 7f5a4cd08209
child 1562 e98c7f6165c9
equal deleted inserted replaced
1530:63fed88fe8e6 1531:e5eb247ad13c
    20 
    20 
    21 types
    21 types
    22   'a item = 'a node set
    22   'a item = 'a node set
    23 
    23 
    24 consts
    24 consts
    25   Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
       
    26 
       
    27   apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
    25   apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
    28   Push      :: [nat, nat=>nat] => (nat=>nat)
    26   Push      :: [nat, nat=>nat] => (nat=>nat)
    29 
    27 
    30   Push_Node :: [nat, 'a node] => 'a node
    28   Push_Node :: [nat, 'a node] => 'a node
    31   ndepth    :: 'a node => nat
    29   ndepth    :: 'a node => nat
    49            => ('a item * 'a item)set" (infixr 80)
    47            => ('a item * 'a item)set" (infixr 80)
    50   "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
    48   "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
    51            => ('a item * 'a item)set" (infixr 70)
    49            => ('a item * 'a item)set" (infixr 70)
    52 
    50 
    53 defs
    51 defs
    54 
       
    55   (*least number operator*)
       
    56   Least_def      "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
       
    57 
    52 
    58   Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    53   Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    59 
    54 
    60   (*crude "lists" of nats -- needed for the constructions*)
    55   (*crude "lists" of nats -- needed for the constructions*)
    61   apfst_def  "apfst == (%f (x,y). (f(x),y))"
    56   apfst_def  "apfst == (%f (x,y). (f(x),y))"