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