--- a/Arith.thy Fri Sep 16 15:48:20 1994 +0200
+++ b/Arith.thy Wed Sep 21 15:40:41 1994 +0200
@@ -1,24 +1,26 @@
-(* Title: HOL/arith.thy
+(* Title: HOL/Arith.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Arithmetic operators and their definitions
*)
Arith = Nat +
-arities nat::plus
- nat::minus
- nat::times
+
+instance
+ nat :: {plus, minus, times}
+
consts
- pred :: "nat => nat"
- div,mod :: "[nat,nat]=>nat" (infixl 70)
-rules
+ pred :: "nat => nat"
+ div, mod :: "[nat, nat] => nat" (infixl 70)
+
+defs
pred_def "pred(m) == nat_rec(m, 0, %n r.n)"
- add_def "m+n == nat_rec(m, n, %u v. Suc(v))"
- diff_def "m-n == nat_rec(n, m, %u v. pred(v))"
- mult_def "m*n == nat_rec(m, 0, %u v. n + v)"
- mod_def "m mod n == wfrec(trancl(pred_nat), m, %j f. if(j<n, j, f(j-n)))"
+ add_def "m+n == nat_rec(m, n, %u v. Suc(v))"
+ diff_def "m-n == nat_rec(n, m, %u v. pred(v))"
+ mult_def "m*n == nat_rec(m, 0, %u v. n + v)"
+ mod_def "m mod n == wfrec(trancl(pred_nat), m, %j f. if(j<n, j, f(j-n)))"
div_def "m div n == wfrec(trancl(pred_nat), m, %j f. if(j<n, 0, Suc(f(j-n))))"
end
@@ -26,3 +28,4 @@
There are no negative numbers; we have
m - n = 0 iff m<=n and m - n = Suc(k) iff m>n.
Also, nat_rec(m, 0, %z w.z) is pred(m). *)
+
--- a/HOL.thy Fri Sep 16 15:48:20 1994 +0200
+++ b/HOL.thy Wed Sep 21 15:40:41 1994 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/hol.thy
+(* Title: HOL/HOL.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 1993 University of Cambridge
@@ -10,8 +10,14 @@
classes
term < logic
+
+axclass
plus < term
+
+axclass
minus < term
+
+axclass
times < term
default
@@ -19,8 +25,6 @@
types
bool
- letbinds letbind
- case_syn cases_syn
arities
fun :: (term, term) term
@@ -43,31 +47,13 @@
All :: "('a => bool) => bool" (binder "! " 10)
Ex :: "('a => bool) => bool" (binder "? " 10)
Ex1 :: "('a => bool) => bool" (binder "?! " 10)
-
Let :: "['a, 'a => 'b] => 'b"
- "_bind" :: "[idt, 'a] => letbind" ("(2_ =/ _)" 10)
- "" :: "letbind => letbinds" ("_")
- "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
- "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
-
- (* Case expressions *)
-
- "@case" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
- "@case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10)
- "" :: "case_syn => cases_syn" ("_")
- "@case2" :: "[case_syn,cases_syn] => cases_syn" ("_/ | _")
-
- (* Alternative Quantifiers *)
-
- "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10)
- "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10)
- "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10)
(* Infixes *)
o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50)
"=" :: "['a, 'a] => bool" (infixl 50)
- "~=" :: "['a, 'a] => bool" ("(_ ~=/ _)" [50, 51] 50)
+(*"~=" :: "['a, 'a] => bool" (infixl 50)*)
"&" :: "[bool, bool] => bool" (infixr 35)
"|" :: "[bool, bool] => bool" (infixr 30)
"-->" :: "[bool, bool] => bool" (infixr 25)
@@ -79,13 +65,42 @@
"*" :: "['a::times, 'a] => 'a" (infixl 70)
+types
+ letbinds letbind
+ case_syn cases_syn
+
+syntax
+
+ "~=" :: "['a, 'a] => bool" (infixl 50)
+
+ (* Alternative Quantifiers *)
+
+ "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10)
+ "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10)
+ "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10)
+
+ (* Let expressions *)
+
+ "_bind" :: "[idt, 'a] => letbind" ("(2_ =/ _)" 10)
+ "" :: "letbind => letbinds" ("_")
+ "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
+ "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
+
+ (* Case expressions *)
+
+ "@case" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
+ "@case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10)
+ "" :: "case_syn => cases_syn" ("_")
+ "@case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
+
translations
+ "x ~= y" == "~ (x = y)"
"ALL xs. P" => "! xs. P"
"EX xs. P" => "? xs. P"
"EX! xs. P" => "?! xs. P"
- "x ~= y" == "~ (x = y)"
- "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
- "let x = a in e" == "Let(a, %x. e)"
+ "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
+ "let x = a in e" == "Let(a, %x. e)"
+
rules
@@ -103,15 +118,15 @@
(* Definitions *)
- True_def "True == ((%x::bool.x)=(%x.x))"
- All_def "All(P) == (P = (%x.True))"
- Ex_def "Ex(P) == P(@x.P(x))"
- False_def "False == (!P.P)"
- not_def "~ P == P-->False"
- and_def "P & Q == !R. (P-->Q-->R) --> R"
- or_def "P | Q == !R. (P-->R) --> (Q-->R) --> R"
- Ex1_def "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)"
- Let_def "Let(s,f) == f(s)"
+ True_def "True == ((%x::bool.x)=(%x.x))"
+ All_def "All(P) == (P = (%x.True))"
+ Ex_def "Ex(P) == P(@x.P(x))"
+ False_def "False == (!P.P)"
+ not_def "~ P == P-->False"
+ and_def "P & Q == !R. (P-->Q-->R) --> R"
+ or_def "P | Q == !R. (P-->R) --> (Q-->R) --> R"
+ Ex1_def "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)"
+ Let_def "Let(s, f) == f(s)"
(* Axioms *)
--- a/Nat.thy Fri Sep 16 15:48:20 1994 +0200
+++ b/Nat.thy Wed Sep 21 15:40:41 1994 +0200
@@ -1,6 +1,6 @@
-(* Title: HOL/nat
+(* Title: HOL/Nat.thy
ID: $Id$
- Author: Tobias Nipkow, Cambridge University Computer Laboratory
+ Author: Tobias Nipkow, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Definition of types ind and nat.
@@ -15,45 +15,48 @@
nat
arities
- ind,nat :: term
- nat :: ord
+ ind, nat :: term
+
+instance
+ nat :: ord
consts
- Zero_Rep :: "ind"
- Suc_Rep :: "ind => ind"
- Nat :: "ind set"
- Rep_Nat :: "nat => ind"
- Abs_Nat :: "ind => nat"
- Suc :: "nat => nat"
- nat_case :: "['a, nat=>'a, nat] =>'a"
- pred_nat :: "(nat*nat) set"
- nat_rec :: "[nat, 'a, [nat, 'a]=>'a] => 'a"
- "0" :: "nat" ("0")
+ Zero_Rep :: "ind"
+ Suc_Rep :: "ind => ind"
+ Nat :: "ind set"
+ Rep_Nat :: "nat => ind"
+ Abs_Nat :: "ind => nat"
+ Suc :: "nat => nat"
+ nat_case :: "['a, nat=>'a, nat] =>'a"
+ pred_nat :: "(nat * nat) set"
+ nat_rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
+ "0" :: "nat" ("0")
translations
"case p of 0 => a | Suc(y) => b" == "nat_case(a, %y.b, p)"
rules
(*the axiom of infinity in 2 parts*)
- inj_Suc_Rep "inj(Suc_Rep)"
- Suc_Rep_not_Zero_Rep "~(Suc_Rep(x) = Zero_Rep)"
- Nat_def "Nat == lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"
+ inj_Suc_Rep "inj(Suc_Rep)"
+ Suc_Rep_not_Zero_Rep "~(Suc_Rep(x) = Zero_Rep)"
+ Nat_def "Nat == lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"
(*faking a type definition...*)
- Rep_Nat "Rep_Nat(n): Nat"
- Rep_Nat_inverse "Abs_Nat(Rep_Nat(n)) = n"
- Abs_Nat_inverse "i: Nat ==> Rep_Nat(Abs_Nat(i)) = i"
+ Rep_Nat "Rep_Nat(n): Nat"
+ Rep_Nat_inverse "Abs_Nat(Rep_Nat(n)) = n"
+ Abs_Nat_inverse "i: Nat ==> Rep_Nat(Abs_Nat(i)) = i"
(*defining the abstract constants*)
- Zero_def "0 == Abs_Nat(Zero_Rep)"
- Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
+ Zero_def "0 == Abs_Nat(Zero_Rep)"
+ Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
(*nat operations and recursion*)
- nat_case_def "nat_case(a,f,n) == @z. (n=0 --> z=a) \
+ nat_case_def "nat_case(a,f,n) == @z. (n=0 --> z=a) \
\ & (!x. n=Suc(x) --> z=f(x))"
- pred_nat_def "pred_nat == {p. ? n. p = <n, Suc(n)>}"
+ pred_nat_def "pred_nat == {p. ? n. p = <n, Suc(n)>}"
less_def "m<n == <m,n>:trancl(pred_nat)"
le_def "m<=(n::nat) == ~(n<m)"
- nat_rec_def "nat_rec(n,c,d) == wfrec(pred_nat, n, \
+ nat_rec_def "nat_rec(n,c,d) == wfrec(pred_nat, n, \
\ nat_case(%g.c, %m g. d(m,g(m))))"
end
+
--- a/Ord.thy Fri Sep 16 15:48:20 1994 +0200
+++ b/Ord.thy Wed Sep 21 15:40:41 1994 +0200
@@ -1,23 +1,25 @@
-(* Title: HOL/Ord.thy
+(* Title: HOL/Ord.thy
ID: $Id$
- Author: Tobias Nipkow, Cambridge University Computer Laboratory
+ Author: Tobias Nipkow, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-The type class for ordered types
+The type class for ordered types (* FIXME improve comment *)
*)
Ord = HOL +
-classes
+
+axclass
ord < term
+
consts
"<", "<=" :: "['a::ord, 'a] => bool" (infixl 50)
- mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*)
- min,max :: "['a::ord,'a] => 'a"
+ mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*)
+ min, max :: "['a::ord, 'a] => 'a"
-rules
-
-mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
-min_def "min(a,b) == if(a <= b, a, b)"
-max_def "max(a,b) == if(a <= b, b, a)"
+defs
+ mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
+ min_def "min(a, b) == if(a <= b, a, b)"
+ max_def "max(a, b) == if(a <= b, b, a)"
end
+
--- a/Set.thy Fri Sep 16 15:48:20 1994 +0200
+++ b/Set.thy Wed Sep 21 15:40:41 1994 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/set.thy
+(* Title: HOL/Set.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 1993 University of Cambridge
@@ -11,14 +11,13 @@
arities
set :: (term) term
- set :: (term) ord
- set :: (term) minus
+instance
+ set :: (term) {ord, minus}
consts
-
- (* Constants *)
-
+ "{}" :: "'a set" ("{}")
+ insert :: "['a, 'a set] => 'a set"
Collect :: "('a => bool) => 'a set" (*comprehension*)
Compl :: "('a set) => 'a set" (*complement*)
Int :: "['a set, 'a set] => 'a set" (infixl 70)
@@ -27,23 +26,20 @@
UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10)
INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10)
Union, Inter :: "(('a set)set) => 'a set" (*of a set*)
- Pow :: "'a set => 'a set set" (*powerset*)
+ Pow :: "'a set => 'a set set" (*powerset*)
range :: "('a => 'b) => 'b set" (*of function*)
Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*)
inj, surj :: "('a => 'b) => bool" (*inj/surjective*)
inj_onto :: "['a => 'b, 'a set] => bool"
"``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90)
":" :: "['a, 'a set] => bool" (infixl 50) (*membership*)
- "~:" :: "['a, 'a set] => bool" ("(_ ~:/ _)" [50, 51] 50)
-
- (* Finite Sets *)
-
- insert :: "['a, 'a set] => 'a set"
- "{}" :: "'a set" ("{}")
- "@Finset" :: "args => 'a set" ("{(_)}")
- (** Binding Constants **)
+syntax
+
+ "~:" :: "['a, 'a set] => bool" (infixl 50)
+
+ "@Finset" :: "args => 'a set" ("{(_)}")
"@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})")
"@SetCompr" :: "['a, idts, bool] => 'a set" ("(1{_ |/_./ _})")
@@ -60,7 +56,6 @@
"*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10)
"*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10)
-
translations
"x ~: y" == "~ (x : y)"
"{x, xs}" == "insert(x, {xs})"
@@ -89,14 +84,14 @@
Compl_def "Compl(A) == {x. ~x:A}"
Un_def "A Un B == {x.x:A | x:B}"
Int_def "A Int B == {x.x:A & x:B}"
- set_diff_def "A-B == {x. x:A & ~x:B}"
+ set_diff_def "A - B == {x. x:A & ~x:B}"
INTER_def "INTER(A, B) == {y. ! x:A. y: B(x)}"
UNION_def "UNION(A, B) == {y. ? x:A. y: B(x)}"
INTER1_def "INTER1(B) == INTER({x.True}, B)"
UNION1_def "UNION1(B) == UNION({x.True}, B)"
Inter_def "Inter(S) == (INT x:S. x)"
Union_def "Union(S) == (UN x:S. x)"
- Pow_def "Pow(A) == {B. B <= A}"
+ Pow_def "Pow(A) == {B. B <= A}"
empty_def "{} == {x. False}"
insert_def "insert(a, B) == {x.x=a} Un B"
range_def "range(f) == {y. ? x. y=f(x)}"
@@ -113,18 +108,16 @@
(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *)
-fun dummyC(s) = Const(s,dummyT);
-
val ex_tr = snd(mk_binder_tr("? ","Ex"));
fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
| nvars(_) = 1;
fun setcompr_tr[e,idts,b] =
- let val eq = dummyC("op =") $ Bound(nvars(idts)) $ e
- val P = dummyC("op &") $ eq $ b
+ let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
+ val P = Syntax.const("op &") $ eq $ b
val exP = ex_tr [idts,P]
- in dummyC("Collect") $ Abs("",dummyT,exP) end;
+ in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
@@ -135,14 +128,13 @@
fun tr'(_ $ abs) =
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
- in dummyC("@SetCompr") $ e $ idts $ Q end
+ in Syntax.const("@SetCompr") $ e $ idts $ Q end
in ok(P,0); tr'(P) end;
in
-val parse_translation = [("@SetCompr",setcompr_tr)];
-val print_translation = [("Collect",setcompr_tr')];
-
+val parse_translation = [("@SetCompr", setcompr_tr)];
+val print_translation = [("Collect", setcompr_tr')];
val print_ast_translation =
map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];