summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.

"@" 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.

1 (* Title: HOL/Univ.thy

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 1993 University of Cambridge

6 Move LEAST to Nat.thy??? Could it be defined for all types 'a::ord?

8 Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat)

10 Defines "Cartesian Product" and "Disjoint Sum" as set operations.

11 Could <*> be generalized to a general summation (Sigma)?

12 *)

14 Univ = Arith + Sum +

16 (** lists, trees will be sets of nodes **)

18 subtype (Node)

19 'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"

21 types

22 'a item = "'a node set"

24 consts

25 Least :: "(nat=>bool) => nat" (binder "LEAST " 10)

27 apfst :: "['a=>'c, 'a*'b] => 'c*'b"

28 Push :: "[nat, nat=>nat] => (nat=>nat)"

30 Push_Node :: "[nat, 'a node] => 'a node"

31 ndepth :: "'a node => nat"

33 Atom :: "('a+nat) => 'a item"

34 Leaf :: "'a => 'a item"

35 Numb :: "nat => 'a item"

36 "$" :: "['a item, 'a item]=> 'a item" (infixr 60)

37 In0,In1 :: "'a item => 'a item"

39 ntrunc :: "[nat, 'a item] => 'a item"

41 "<*>" :: "['a item set, 'a item set]=> 'a item set" (infixr 80)

42 "<+>" :: "['a item set, 'a item set]=> 'a item set" (infixr 70)

44 Split :: "[['a item, 'a item]=>'b, 'a item] => 'b"

45 Case :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b"

47 diag :: "'a set => ('a * 'a)set"

48 "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \

49 \ => ('a item * 'a item)set" (infixr 80)

50 "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \

51 \ => ('a item * 'a item)set" (infixr 70)

53 defs

55 (*least number operator*)

56 Least_def "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"

58 Push_Node_def "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"

60 (*crude "lists" of nats -- needed for the constructions*)

61 apfst_def "apfst == (%f. split(%x y. (f(x),y)))"

62 Push_def "Push == (%b h. nat_case (Suc b) h)"

64 (** operations on S-expressions -- sets of nodes **)

66 (*S-expression constructors*)

67 Atom_def "Atom == (%x. {Abs_Node((%k.0, x))})"

68 Scons_def "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"

70 (*Leaf nodes, with arbitrary or nat labels*)

71 Leaf_def "Leaf == Atom o Inl"

72 Numb_def "Numb == Atom o Inr"

74 (*Injections of the "disjoint sum"*)

75 In0_def "In0(M) == Numb(0) $ M"

76 In1_def "In1(M) == Numb(Suc(0)) $ M"

78 (*the set of nodes with depth less than k*)

79 ndepth_def "ndepth(n) == (%(f,x). LEAST k. f(k)=0) (Rep_Node n)"

80 ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}"

82 (*products and sums for the "universe"*)

83 uprod_def "A<*>B == UN x:A. UN y:B. { (x$y) }"

84 usum_def "A<+>B == In0``A Un In1``B"

86 (*the corresponding eliminators*)

87 Split_def "Split c M == @u. ? x y. M = x$y & u = c x y"

89 Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x)) \

90 \ | (? y . M = In1(y) & u = d(y))"

93 (** diagonal sets and equality for the "universe" **)

95 diag_def "diag(A) == UN x:A. {(x,x)}"

97 dprod_def "r<**>s == UN (x,x'):r. UN (y,y'):s. {(x$y,x'$y')}"

99 dsum_def "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un \

100 \ (UN (y,y'):s. {(In1(y),In1(y'))})"

102 end