--- a/src/HOL/HOL.thy Wed Nov 27 16:48:19 1996 +0100
+++ b/src/HOL/HOL.thy Wed Nov 27 16:51:15 1996 +0100
@@ -3,23 +3,17 @@
Author: Tobias Nipkow
Copyright 1993 University of Cambridge
-Higher-Order Logic
+Higher-Order Logic.
*)
HOL = CPure +
+
+(** Core syntax **)
+
classes
term < logic
-axclass
- plus < term
-
-axclass
- minus < term
-
-axclass
- times < term
-
default
term
@@ -57,13 +51,27 @@
"|" :: [bool, bool] => bool (infixr 30)
"-->" :: [bool, bool] => bool (infixr 25)
- (* Overloaded Constants *)
+
+(* Overloaded Constants *)
+
+axclass
+ plus < term
+axclass
+ minus < term
+
+axclass
+ times < term
+
+consts
"+" :: ['a::plus, 'a] => 'a (infixl 65)
"-" :: ['a::minus, 'a] => 'a (infixl 65)
"*" :: ['a::times, 'a] => 'a (infixl 70)
+
+(** Additional concrete syntax **)
+
types
letbinds letbind
case_syn cases_syn
@@ -72,7 +80,7 @@
"~=" :: ['a, 'a] => bool (infixl 50)
- "@Eps" :: [pttrn,bool] => 'a ("(3@ _./ _)" 10)
+ "@Eps" :: [pttrn, bool] => 'a ("(3@ _./ _)" 10)
(* Alternative Quantifiers *)
@@ -96,13 +104,34 @@
translations
"x ~= y" == "~ (x = y)"
- "@ x.b" == "Eps(%x.b)"
+ "@ x.b" == "Eps (%x. b)"
"ALL xs. P" => "! xs. P"
"EX xs. P" => "? xs. P"
"EX! xs. P" => "?! xs. P"
"_Let (_binds b bs) e" == "_Let b (_Let bs e)"
"let x = a in e" == "Let a (%x. e)"
+
+syntax (symbols)
+ not :: bool => bool ("\\<not> _" [40] 40)
+ "op &" :: [bool, bool] => bool (infixr "\\<and>" 35)
+ "op |" :: [bool, bool] => bool (infixr "\\<or>" 30)
+ "op -->" :: [bool, bool] => bool (infixr "\\<midarrow>\\<rightarrow>" 25)
+ "op o" :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl "\\<circ>" 55)
+ "op ~=" :: ['a, 'a] => bool (infixl "\\<noteq>" 50)
+ "@Eps" :: [pttrn, bool] => 'a ("(3\\<epsilon>_./ _)" 10)
+ "! " :: [idts, bool] => bool ("(3\\<forall>_./ _)" 10)
+ "? " :: [idts, bool] => bool ("(3\\<exists>_./ _)" 10)
+ "?! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" 10)
+ "*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" 10)
+ "*Ex" :: [idts, bool] => bool ("(3\\<exists>_./ _)" 10)
+ "*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" 10)
+ "@case1" :: ['a, 'b] => case_syn ("(2_ \\<mapsto>/ _)" 10)
+
+
+
+(** Rules and definitions **)
+
rules
eq_reflection "(x=y) ==> (x==y)"
@@ -147,6 +176,7 @@
end
+
ML
(** Choice between the HOL and Isabelle style of quantifiers **)
@@ -168,6 +198,3 @@
(* start 8bit 2 *)
(* end 8bit 2 *)
-
-
-
--- a/src/HOL/Prod.thy Wed Nov 27 16:48:19 1996 +0100
+++ b/src/HOL/Prod.thy Wed Nov 27 16:51:15 1996 +0100
@@ -9,7 +9,8 @@
Prod = Fun + equalities +
-(** Products **)
+
+(** products **)
(* type definition *)
@@ -21,6 +22,9 @@
('a, 'b) "*" (infixr 20)
= "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
+syntax (symbols)
+ "*" :: [type, type] => type ("(_ \\<times>/ _)" [21, 20] 20)
+
(* abstract constants and syntax *)
@@ -32,30 +36,37 @@
Pair :: "['a, 'b] => 'a * 'b"
Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set"
-(** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
+
+(* patterns -- extends pre-defined type "pttrn" used in abstractions *)
+
types pttrns
syntax
- "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))")
+ "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))")
- "@pttrn" :: [pttrn,pttrns] => pttrn ("'(_,/_')")
- "" :: pttrn => pttrns ("_")
- "@pttrns" :: [pttrn,pttrns] => pttrns ("_,/_")
+ "@pttrn" :: [pttrn, pttrns] => pttrn ("'(_,/_')")
+ "" :: pttrn => pttrns ("_")
+ "@pttrns" :: [pttrn, pttrns] => pttrns ("_,/_")
- "@Sigma" :: "[idt,'a set,'b set] => ('a * 'b)set"
- ("(3SIGMA _:_./ _)" 10)
- "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set"
- ("_ Times _" [81,80] 80)
+ "@Sigma" :: "[idt, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
+ "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ Times _" [81, 80] 80)
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)"
+ "%(x,y,zs).b" == "split(%x (y,zs).b)"
+ "%(x,y).b" == "split(%x y.b)"
+
+ "SIGMA x:A.B" => "Sigma A (%x.B)"
+ "A Times B" => "Sigma A (_K B)"
- "SIGMA x:A. B" => "Sigma A (%x.B)"
- "A Times B" => "Sigma A (_K B)"
+syntax (symbols)
+ "@Sigma" :: "[idt, 'a set, 'b set] => ('a * 'b) set" ("(3\\<Sigma> _\\<in>_./ _)" 10)
+ "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \\<times> _" [81, 80] 80)
+
+
+(* definitions *)
defs
Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)"
@@ -65,7 +76,9 @@
prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))"
Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
-(** Unit **)
+
+
+(** unit **)
typedef (Unit)
unit = "{p. p = True}"