--- 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
--- 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
--- 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