# HG changeset patch
# User clasohm
# Date 826541345 -3600
# Node ID 9ba0906aa60d4b0dff8876a092ac5ca52ad818ed
# Parent  9c6ebfab4e05330a53fc14d58f5a635151da1e32
added constdefs section

diff -r 9c6ebfab4e05 -r 9ba0906aa60d src/HOL/Integ/Integ.thy
--- a/src/HOL/Integ/Integ.thy	Fri Mar 08 13:11:09 1996 +0100
+++ b/src/HOL/Integ/Integ.thy	Mon Mar 11 11:49:05 1996 +0100
@@ -9,12 +9,9 @@
 *)
 
 Integ = Equiv + Arith +
-consts
+constdefs
   intrel      :: "((nat * nat) * (nat * nat)) set"
-
-defs
-  intrel_def
-   "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
+  "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
 
 typedef (Integ)
   int = "{x::(nat*nat).True}/intrel"            (Equiv.quotient_def)
@@ -22,29 +19,43 @@
 instance
   int :: {ord, plus, times, minus}
 
-consts
+constdefs
+
   zNat        :: nat set
-  znat        :: nat => int        ("$# _" [80] 80)
-  zminus      :: int => int        ("$~ _" [80] 80)
+  "zNat == {x::nat. True}"
+
+  znat        :: nat => int                                  ("$# _" [80] 80)
+  "$# m == Abs_Integ(intrel ^^ {(m,0)})"
+
+  zminus      :: int => int                                  ("$~ _" [80] 80)
+  "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
+
   znegative   :: int => bool
+  "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
+
   zmagnitude  :: int => int
-  zdiv,zmod   :: [int,int]=>int  (infixl 70)
-  zpred,zsuc  :: int=>int
+  "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).
+                              split (%x y. intrel^^{((y-x) + (x-y),0)}) p)"
+
+  zdiv        :: [int,int]=>int                              (infixl 70)
+  "Z1 zdiv Z2 ==   
+      Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   
+          split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),   
+          (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)"
+
+  zmod        :: [int,int]=>int                              (infixl 70)
+  "Z1 zmod Z2 ==   
+      Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1.   
+          split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)),   
+          (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)"
+
+  zpred       :: int=>int
+  "zpred(Z) == Z - $# Suc(0)"
+
+  zsuc        :: int=>int
+  "zsuc(Z) == Z + $# Suc(0)"
 
 defs
-  zNat_def    "zNat == {x::nat. True}"
-
-  znat_def    "$# m == Abs_Integ(intrel ^^ {(m,0)})"
-
-  zminus_def
-        "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
-
-  znegative_def
-      "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
-
-  zmagnitude_def
-      "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{((y-x) + (x-y),0)}) p)"
-
   zadd_def
    "Z1 + Z2 == 
        Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2).   
@@ -61,19 +72,4 @@
        Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   
            split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
 
-  zdiv_def
-   "Z1 zdiv Z2 ==   
-       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   
-           split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),   
-           (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)"
-
-  zmod_def
-   "Z1 zmod Z2 ==   
-       Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1.   
-           split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)),   
-           (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)"
-
-  zsuc_def     "zsuc(Z) == Z + $# Suc(0)"
-
-  zpred_def    "zpred(Z) == Z - $# Suc(0)"
 end
diff -r 9c6ebfab4e05 -r 9ba0906aa60d src/HOL/Lex/Auto.thy
--- a/src/HOL/Lex/Auto.thy	Fri Mar 08 13:11:09 1996 +0100
+++ b/src/HOL/Lex/Auto.thy	Mon Mar 11 11:49:05 1996 +0100
@@ -16,23 +16,24 @@
 
 types ('a,'b)auto = "'b * ('b => 'a => 'b) * ('b => bool)"
 
-consts
+constdefs
+
   start :: ('a, 'b)auto => 'b
+  "start(A) == fst(A)"
+
   next  :: ('a, 'b)auto => ('b => 'a => 'b)
-  fin   :: ('a, 'b)auto => ('b => bool)
-  nexts :: ('a, 'b)auto => 'b => 'a list => 'b
-  accepts :: ('a,'b) auto => 'a list => bool  
-  acc_prefix :: ('a, 'b)auto => 'b => 'a list => bool
+  "next(A) == fst(snd(A))"
 
-defs
-  start_def "start(A) == fst(A)"
-  next_def  "next(A) == fst(snd(A))"
-  fin_def   "fin(A) == snd(snd(A))"
-  nexts_def "nexts(A) == foldl(next(A))"
+  fin   :: ('a, 'b)auto => ('b => bool)
+  "fin(A) == snd(snd(A))"
+
+  nexts :: ('a, 'b)auto => 'b => 'a list => 'b
+  "nexts(A) == foldl(next(A))"
 
-  accepts_def "accepts A xs == fin A (nexts A (start A) xs)"
+  accepts :: ('a,'b) auto => 'a list => bool
+  "accepts A xs == fin A (nexts A (start A) xs)"
 
-  acc_prefix_def
-    "acc_prefix A st xs == ? us. us <= xs & us~=[] & fin A (nexts A st us)"
+  acc_prefix :: ('a, 'b)auto => 'b => 'a list => bool
+  "acc_prefix A st xs == ? us. us <= xs & us~=[] & fin A (nexts A st us)"
 
 end
diff -r 9c6ebfab4e05 -r 9ba0906aa60d src/HOL/Lex/Chopper.thy
--- a/src/HOL/Lex/Chopper.thy	Fri Mar 08 13:11:09 1996 +0100
+++ b/src/HOL/Lex/Chopper.thy	Mon Mar 11 11:49:05 1996 +0100
@@ -19,16 +19,14 @@
 
 types   'a chopper = "'a list => 'a list list * 'a list"
 
-consts
+constdefs
   is_longest_prefix_chopper :: ['a list => bool, 'a chopper] => bool
+  "is_longest_prefix_chopper L chopper == !xs.
+       (!zs. chopper(xs) = ([],zs) -->
+             zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &
+       (!ys yss zs. chopper(xs) = (ys#yss,zs) -->
+          ys ~= [] & L(ys) & xs=ys@flat(yss)@zs &
+          chopper(flat(yss)@zs) = (yss,zs) &
+          (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
 
-defs
-  is_longest_prefix_chopper_def
-    "is_longest_prefix_chopper L chopper == !xs.   \
-\        (!zs. chopper(xs) = ([],zs) --> \
-\              zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &  \
-\        (!ys yss zs. chopper(xs) = (ys#yss,zs) -->                \
-\           ys ~= [] & L(ys) & xs=ys@flat(yss)@zs &   \
-\           chopper(flat(yss)@zs) = (yss,zs) &     \
-\           (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
 end