src/HOL/Univ.thy
author nipkow
Sat Apr 22 13:25:31 1995 +0200 (1995-04-22)
changeset 1068 e0f2dffab506
parent 972 e61b058d58d2
child 1151 c820b3cc3df0
permissions -rw-r--r--
HOL.thy:

"@" is no longer introduced as a "binder" but has its own explicit
translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further
translation rules for abstractions with patterns take care of the rest. This
is very modular and avoids problems with "binders" such as "!" mentioned
below.

let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u)


Set.thy:

UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@"
above, except that "@" was a "binder" originally.


Prod.thy:

Added new syntax for pttrn which allows arbitrarily nested tuples. Two
translation rules take care of %pttrn. Unfortunately they cannot be
reversed. Hence a little ML-code is used as well.

Note that now "! (x,y). ..." is syntactically valid but leads to a
translation error. This is because "!" is introduced as a "binder" which
means that its translation into lambda-terms is not done by a rewrite rule
(aka macro) but by some fixed ML-code which comes after the rewriting stage
and does not know how to handle patterns. This looks like a minor blemish
since patterns in unbounded quantifiers are not that useful (well, except
maybe in unique existence ...). Ideally, there should be two syntactic
categories:

idts, as we know and love it, which does not admit patterns.
patterns, which is what idts has become now.

There is one more point where patterns are now allowed but don't make sense:

{e | idts . P}

where idts is the list of local variables.


Univ.thy: converted the defs for <++> and <**> into pattern form. It worked
perfectly.
clasohm@923
     1
(*  Title:      HOL/Univ.thy
clasohm@923
     2
    ID:         $Id$
clasohm@923
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1993  University of Cambridge
clasohm@923
     5
clasohm@923
     6
Move LEAST to Nat.thy???  Could it be defined for all types 'a::ord?
clasohm@923
     7
clasohm@923
     8
Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat)
clasohm@923
     9
clasohm@923
    10
Defines "Cartesian Product" and "Disjoint Sum" as set operations.
clasohm@923
    11
Could <*> be generalized to a general summation (Sigma)?
clasohm@923
    12
*)
clasohm@923
    13
clasohm@923
    14
Univ = Arith + Sum +
clasohm@923
    15
clasohm@923
    16
(** lists, trees will be sets of nodes **)
clasohm@923
    17
clasohm@923
    18
subtype (Node)
clasohm@972
    19
  'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
clasohm@923
    20
clasohm@923
    21
types
clasohm@923
    22
  'a item = "'a node set"
clasohm@923
    23
clasohm@923
    24
consts
clasohm@923
    25
  Least     :: "(nat=>bool) => nat"    (binder "LEAST " 10)
clasohm@923
    26
clasohm@923
    27
  apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
clasohm@923
    28
  Push      :: "[nat, nat=>nat] => (nat=>nat)"
clasohm@923
    29
clasohm@923
    30
  Push_Node :: "[nat, 'a node] => 'a node"
clasohm@923
    31
  ndepth    :: "'a node => nat"
clasohm@923
    32
clasohm@923
    33
  Atom      :: "('a+nat) => 'a item"
clasohm@923
    34
  Leaf      :: "'a => 'a item"
clasohm@923
    35
  Numb      :: "nat => 'a item"
clasohm@923
    36
  "$"       :: "['a item, 'a item]=> 'a item"   (infixr 60)
clasohm@923
    37
  In0,In1   :: "'a item => 'a item"
clasohm@923
    38
clasohm@923
    39
  ntrunc    :: "[nat, 'a item] => 'a item"
clasohm@923
    40
clasohm@923
    41
  "<*>"  :: "['a item set, 'a item set]=> 'a item set" (infixr 80)
clasohm@923
    42
  "<+>"  :: "['a item set, 'a item set]=> 'a item set" (infixr 70)
clasohm@923
    43
clasohm@923
    44
  Split  :: "[['a item, 'a item]=>'b, 'a item] => 'b"
clasohm@923
    45
  Case   :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b"
clasohm@923
    46
clasohm@923
    47
  diag   :: "'a set => ('a * 'a)set"
clasohm@923
    48
  "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
clasohm@923
    49
\           => ('a item * 'a item)set" (infixr 80)
clasohm@923
    50
  "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
clasohm@923
    51
\           => ('a item * 'a item)set" (infixr 70)
clasohm@923
    52
clasohm@923
    53
defs
clasohm@923
    54
clasohm@923
    55
  (*least number operator*)
clasohm@923
    56
  Least_def      "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
clasohm@923
    57
clasohm@923
    58
  Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
clasohm@923
    59
clasohm@923
    60
  (*crude "lists" of nats -- needed for the constructions*)
clasohm@972
    61
  apfst_def  "apfst == (%f. split(%x y. (f(x),y)))"
clasohm@923
    62
  Push_def   "Push == (%b h. nat_case (Suc b) h)"
clasohm@923
    63
clasohm@923
    64
  (** operations on S-expressions -- sets of nodes **)
clasohm@923
    65
clasohm@923
    66
  (*S-expression constructors*)
clasohm@972
    67
  Atom_def   "Atom == (%x. {Abs_Node((%k.0, x))})"
clasohm@923
    68
  Scons_def  "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
clasohm@923
    69
clasohm@923
    70
  (*Leaf nodes, with arbitrary or nat labels*)
clasohm@923
    71
  Leaf_def   "Leaf == Atom o Inl"
clasohm@923
    72
  Numb_def   "Numb == Atom o Inr"
clasohm@923
    73
clasohm@923
    74
  (*Injections of the "disjoint sum"*)
clasohm@923
    75
  In0_def    "In0(M) == Numb(0) $ M"
clasohm@923
    76
  In1_def    "In1(M) == Numb(Suc(0)) $ M"
clasohm@923
    77
clasohm@923
    78
  (*the set of nodes with depth less than k*)
nipkow@1068
    79
  ndepth_def "ndepth(n) == (%(f,x). LEAST k. f(k)=0) (Rep_Node n)"
clasohm@923
    80
  ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}"
clasohm@923
    81
clasohm@923
    82
  (*products and sums for the "universe"*)
clasohm@923
    83
  uprod_def  "A<*>B == UN x:A. UN y:B. { (x$y) }"
clasohm@923
    84
  usum_def   "A<+>B == In0``A Un In1``B"
clasohm@923
    85
clasohm@923
    86
  (*the corresponding eliminators*)
clasohm@923
    87
  Split_def  "Split c M == @u. ? x y. M = x$y & u = c x y"
clasohm@923
    88
clasohm@923
    89
  Case_def   "Case c d M == @u.  (? x . M = In0(x) & u = c(x)) \
clasohm@923
    90
\                              | (? y . M = In1(y) & u = d(y))"
clasohm@923
    91
clasohm@923
    92
clasohm@923
    93
  (** diagonal sets and equality for the "universe" **)
clasohm@923
    94
clasohm@972
    95
  diag_def   "diag(A) == UN x:A. {(x,x)}"
clasohm@923
    96
nipkow@1068
    97
  dprod_def  "r<**>s == UN (x,x'):r. UN (y,y'):s. {(x$y,x'$y')}"
clasohm@923
    98
nipkow@1068
    99
  dsum_def   "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un \
nipkow@1068
   100
\                       (UN (y,y'):s. {(In1(y),In1(y'))})"
clasohm@923
   101
clasohm@923
   102
end