# HG changeset patch
# User nipkow
# Date 798549931 -7200
# Node ID e0f2dffab5067d3fc87819e2c50e575821d0c76a
# Parent  00ed040f66e17018622a0a88797713a4037be14b
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.

diff -r 00ed040f66e1 -r e0f2dffab506 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Apr 22 12:21:41 1995 +0200
+++ b/src/HOL/HOL.thy	Sat Apr 22 13:25:31 1995 +0200
@@ -43,7 +43,7 @@
 
   (* Binders *)
 
-  Eps           :: "('a => bool) => 'a"               (binder "@" 10)
+  Eps           :: "('a => bool) => 'a"
   All           :: "('a => bool) => bool"             (binder "! " 10)
   Ex            :: "('a => bool) => bool"             (binder "? " 10)
   Ex1           :: "('a => bool) => bool"             (binder "?! " 10)
@@ -53,7 +53,6 @@
 
   o             :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixr 50)
   "="           :: "['a, 'a] => bool"                 (infixl 50)
-(*"~="          :: "['a, 'a] => bool"                 (infixl 50)*)
   "&"           :: "[bool, bool] => bool"             (infixr 35)
   "|"           :: "[bool, bool] => bool"             (infixr 30)
   "-->"         :: "[bool, bool] => bool"             (infixr 25)
@@ -73,6 +72,8 @@
 
   "~="          :: "['a, 'a] => bool"                 (infixl 50)
 
+  "@Eps"        :: "[pttrn,bool] => 'a"               ("(3@ _./ _)" 10)
+
   (* Alternative Quantifiers *)
 
   "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
@@ -81,7 +82,7 @@
 
   (* Let expressions *)
 
-  "_bind"       :: "[idt, 'a] => letbind"             ("(2_ =/ _)" 10)
+  "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
   ""            :: "letbind => letbinds"              ("_")
   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
@@ -95,6 +96,7 @@
 
 translations
   "x ~= y"      == "~ (x = y)"
+  "@ x.b"       == "Eps(%x.b)"
   "ALL xs. P"   => "! xs. P"
   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
diff -r 00ed040f66e1 -r e0f2dffab506 src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Sat Apr 22 12:21:41 1995 +0200
+++ b/src/HOL/Prod.thy	Sat Apr 22 13:25:31 1995 +0200
@@ -34,13 +34,25 @@
   Pair          :: "['a, 'b] => 'a * 'b"
   Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
 
+(** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
+types pttrns
+
 syntax
   "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
 
+  "@pttrn"  :: "pttrns => pttrn"            ("'(_')")
+  ""        :: " pttrn           => pttrns" ("_")
+  "@pttrns" :: "[pttrn,pttrns]   => pttrns" ("_,/_")
+
 translations
   "(x, y, z)"   == "(x, (y, z))"
   "(x, y)"      == "Pair x y"
 
+  "%(x,y,zs).b"   => "split(%x (y,zs).b)"
+  "%(x,y).b"      => "split(%x y.b)"
+(* The <= direction fails if split has more than one argument because
+   ast-matching fails. Otherwise it would work fine *)
+
 defs
   Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
   fst_def       "fst(p) == @a. ? b. p = (a, b)"
@@ -63,3 +75,34 @@
   Unity_def     "() == Abs_Unit(True)"
 
 end
+
+ML
+
+local open Syntax
+
+fun pttrn s = const"@pttrn" $ s;
+fun pttrns s t = const"@pttrns" $ s $ t;
+
+fun split2(Abs(x,T,t)) =
+      let val (pats,u) = split1 t
+      in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end
+  | split2(Const("split",_) $ r) =
+      let val (pats,s) = split2(r)
+          val (pats2,t) = split1(s)
+      in (pttrns (pttrn pats) pats2, t) end
+and split1(Abs(x,T,t)) =  (Free(x,T), subst_bounds([free x],t))
+  | split1(Const("split",_)$t) = split2(t);
+
+fun split_tr'(t::args) =
+  let val (pats,ft) = split2(t)
+  in case args of
+       [] => const"_abs" $ pttrn pats $ ft
+     | arg::rest =>
+         list_comb(const"_Let"$(const"_bind"$(pttrn pats)$arg)$ft, rest)
+  end
+
+in
+
+val print_translation = [("split", split_tr')];
+
+end;
diff -r 00ed040f66e1 -r e0f2dffab506 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Apr 22 12:21:41 1995 +0200
+++ b/src/HOL/Set.thy	Sat Apr 22 13:25:31 1995 +0200
@@ -41,20 +41,20 @@
 
   "@Finset"     :: "args => 'a set"                   ("{(_)}")
 
-  "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})")
+  "@Coll"       :: "[pttrn, bool] => 'a set"          ("(1{_./ _})")
   "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("(1{_ |/_./ _})")
 
   (* Big Intersection / Union *)
 
-  "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"  ("(3INT _:_./ _)" 10)
-  "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"  ("(3UN _:_./ _)" 10)
+  "@INTER"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3INT _:_./ _)" 10)
+  "@UNION"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3UN _:_./ _)" 10)
 
   (* Bounded Quantifiers *)
 
-  "@Ball"       :: "[idt, 'a set, bool] => bool"      ("(3! _:_./ _)" 10)
-  "@Bex"        :: "[idt, 'a set, bool] => bool"      ("(3? _:_./ _)" 10)
-  "*Ball"       :: "[idt, 'a set, bool] => bool"      ("(3ALL _:_./ _)" 10)
-  "*Bex"        :: "[idt, 'a set, bool] => bool"      ("(3EX _:_./ _)" 10)
+  "@Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3! _:_./ _)" 10)
+  "@Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3? _:_./ _)" 10)
+  "*Ball"       :: "[pttrn, 'a set, bool] => bool"      ("(3ALL _:_./ _)" 10)
+  "*Bex"        :: "[pttrn, 'a set, bool] => bool"      ("(3EX _:_./ _)" 10)
 
 translations
   "x ~: y"      == "~ (x : y)"
diff -r 00ed040f66e1 -r e0f2dffab506 src/HOL/Univ.thy
--- a/src/HOL/Univ.thy	Sat Apr 22 12:21:41 1995 +0200
+++ b/src/HOL/Univ.thy	Sat Apr 22 13:25:31 1995 +0200
@@ -76,7 +76,7 @@
   In1_def    "In1(M) == Numb(Suc(0)) $ M"
 
   (*the set of nodes with depth less than k*)
-  ndepth_def "ndepth(n) == split (%f x. LEAST k. f(k)=0) (Rep_Node n)"
+  ndepth_def "ndepth(n) == (%(f,x). LEAST k. f(k)=0) (Rep_Node n)"
   ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}"
 
   (*products and sums for the "universe"*)
@@ -94,10 +94,9 @@
 
   diag_def   "diag(A) == UN x:A. {(x,x)}"
 
-  dprod_def  "r<**>s == UN u:r. split (%x x'. \
-\                       UN v:s. split (%y y'. {(x$y,x'$y')}) v) u"
+  dprod_def  "r<**>s == UN (x,x'):r. UN (y,y'):s. {(x$y,x'$y')}"
 
-  dsum_def   "r<++>s == (UN u:r. split (%x x'. {(In0(x),In0(x'))}) u) Un \
-\                       (UN v:s. split (%y y'. {(In1(y),In1(y'))}) v)"
+  dsum_def   "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un \
+\                       (UN (y,y'):s. {(In1(y),In1(y'))})"
 
 end