replaced HOL_quantifiers flag by "HOL" print mode;
simplified HOL basic syntax (more orthogonal);
--- a/NEWS Tue Aug 17 22:11:05 1999 +0200
+++ b/NEWS Tue Aug 17 22:13:23 1999 +0200
@@ -147,18 +147,15 @@
** HOL misc **
-* HOL/datatype: Now also handles arbitrarily branching datatypes
- (using function types) such as
-
- datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
-
* HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
-- avoids syntactic ambiguities and treats state, transition, and
temporal levels more uniformly; introduces INCOMPATIBILITIES due to
changed syntax and (many) tactics;
-* New bounded quantifier syntax (input only):
- ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P
+* HOL/datatype: Now also handles arbitrarily branching datatypes
+ (using function types) such as
+
+ datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
* HOL/typedef: fixed type inference for representing set; type
arguments now have to occur explicitly on the rhs as type constraints;
@@ -170,6 +167,17 @@
INCOMPATIBILITY: while [] and infix # syntax is still there, of
course, ML tools referring to List.list.op # etc. have to be adapted;
+* HOL_quantifiers flag superseded by "HOL" print mode, which is
+disabled by default; run isabelle with option -m HOL to get back to
+the original Gordon/HOL-style output;
+
+* HOL/Ord.thy: new bounded quantifier syntax (input only): ALL x<y. P,
+ALL x<=y. P, EX x<y. P, EX x<=y. P;
+
+* HOL basic syntax simplified (more orthogonal): all variants of
+All/Ex now support plain / symbolic / HOL notation; plain syntax for
+Eps operator is provided as well: "SOME x. P[x]";
+
*** LK ***
--- a/src/HOL/HOL.thy Tue Aug 17 22:11:05 1999 +0200
+++ b/src/HOL/HOL.thy Tue Aug 17 22:13:23 1999 +0200
@@ -40,9 +40,9 @@
(* Binders *)
Eps :: ('a => bool) => 'a
- All :: ('a => bool) => bool (binder "! " 10)
- Ex :: ('a => bool) => bool (binder "? " 10)
- Ex1 :: ('a => bool) => bool (binder "?! " 10)
+ All :: ('a => bool) => bool (binder "ALL " 10)
+ Ex :: ('a => bool) => bool (binder "EX " 10)
+ Ex1 :: ('a => bool) => bool (binder "EX! " 10)
Let :: ['a, 'a => 'b] => 'b
(* Infixes *)
@@ -75,6 +75,7 @@
(*See Nat.thy for "^"*)
+
(** Additional concrete syntax **)
nonterminals
@@ -82,16 +83,8 @@
case_syn cases_syn
syntax
-
"~=" :: ['a, 'a] => bool (infixl 50)
-
- "@Eps" :: [pttrn, bool] => 'a ("(3@ _./ _)" [0, 10] 10)
-
- (* Alternative Quantifiers *)
-
- "*All" :: [idts, bool] => bool ("(3ALL _./ _)" [0, 10] 10)
- "*Ex" :: [idts, bool] => bool ("(3EX _./ _)" [0, 10] 10)
- "*Ex1" :: [idts, bool] => bool ("(3EX! _./ _)" [0, 10] 10)
+ "_Eps" :: [pttrn, bool] => 'a ("(3SOME _./ _)" [0, 10] 10)
(* Let expressions *)
@@ -108,11 +101,8 @@
"@case2" :: [case_syn, cases_syn] => cases_syn ("_/ | _")
translations
- "x ~= y" == "~ (x = y)"
- "@ x. b" == "Eps (%x. b)"
- "ALL xs. P" => "! xs. P"
- "EX xs. P" => "? xs. P"
- "EX! xs. P" => "?! xs. P"
+ "x ~= y" == "~ (x = y)"
+ "SOME x. P" == "Eps (%x. P)"
"_Let (_binds b bs) e" == "_Let b (_Let bs e)"
"let x = a in e" == "Let a (%x. e)"
@@ -127,18 +117,15 @@
"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>_./ _)" [0, 10] 10)
- "! " :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10)
- "? " :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10)
- "?! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10)
+ "_Eps" :: [pttrn, bool] => 'a ("(3\\<epsilon>_./ _)" [0, 10] 10)
+ "ALL " :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10)
+ "EX " :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10)
+ "EX! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10)
"@case1" :: ['a, 'b] => case_syn ("(2_ \\<Rightarrow>/ _)" 10)
(*"@case2" :: [case_syn, cases_syn] => cases_syn ("_/ \\<orelse> _")*)
syntax (symbols output)
"op ~=" :: ['a, 'a] => bool ("(_ \\<noteq>/ _)" [51, 51] 50)
- "*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10)
- "*Ex" :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10)
- "*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10)
syntax (xsymbols)
"op -->" :: [bool, bool] => bool (infixr "\\<longrightarrow>" 25)
@@ -146,6 +133,13 @@
syntax (HTML output)
Not :: bool => bool ("\\<not> _" [40] 40)
+syntax (HOL)
+ "_Eps" :: [pttrn, bool] => 'a ("(3@ _./ _)" [0, 10] 10)
+ "ALL " :: [idts, bool] => bool ("(3! _./ _)" [0, 10] 10)
+ "EX " :: [idts, bool] => bool ("(3? _./ _)" [0, 10] 10)
+ "EX! " :: [idts, bool] => bool ("(3?! _./ _)" [0, 10] 10)
+
+
(** Rules and definitions **)
@@ -205,24 +199,3 @@
end
-
-
-ML
-
-
-(** Choice between the HOL and Isabelle style of quantifiers **)
-
-val HOL_quantifiers = ref true;
-
-fun alt_ast_tr' (name, alt_name) =
- let
- fun ast_tr' (*name*) args =
- if ! HOL_quantifiers then raise Match
- else Syntax.mk_appl (Syntax.Constant alt_name) args;
- in
- (name, ast_tr')
- end;
-
-
-val print_ast_translation =
- map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
--- a/src/HOL/Ord.thy Tue Aug 17 22:11:05 1999 +0200
+++ b/src/HOL/Ord.thy Tue Aug 17 22:13:23 1999 +0200
@@ -56,16 +56,32 @@
axclass linorder < order
linorder_linear "x <= y | y <= x"
-(*bounded quantifiers*)
+
+(* bounded quantifiers *)
+
syntax
- "@lessAll" :: [idt, 'a, bool] => bool ("(3! _<_./ _)" [0, 0, 10] 10)
- "@lessEx" :: [idt, 'a, bool] => bool ("(3? _<_./ _)" [0, 0, 10] 10)
- "@leAll" :: [idt, 'a, bool] => bool ("(3! _<=_./ _)" [0, 0, 10] 10)
- "@leEx" :: [idt, 'a, bool] => bool ("(3? _<=_./ _)" [0, 0, 10] 10)
+ "_lessAll" :: [idt, 'a, bool] => bool ("(3ALL _<_./ _)" [0, 0, 10] 10)
+ "_lessEx" :: [idt, 'a, bool] => bool ("(3EX _<_./ _)" [0, 0, 10] 10)
+ "_leAll" :: [idt, 'a, bool] => bool ("(3ALL _<=_./ _)" [0, 0, 10] 10)
+ "_leEx" :: [idt, 'a, bool] => bool ("(3EX _<=_./ _)" [0, 0, 10] 10)
+
+syntax (symbols)
+ "_lessAll" :: [idt, 'a, bool] => bool ("(3\\<forall>_<_./ _)" [0, 0, 10] 10)
+ "_lessEx" :: [idt, 'a, bool] => bool ("(3\\<exists>_<_./ _)" [0, 0, 10] 10)
+ "_leAll" :: [idt, 'a, bool] => bool ("(3\\<forall>_<=_./ _)" [0, 0, 10] 10)
+ "_leEx" :: [idt, 'a, bool] => bool ("(3\\<exists>_<=_./ _)" [0, 0, 10] 10)
+
+syntax (HOL)
+ "_lessAll" :: [idt, 'a, bool] => bool ("(3! _<_./ _)" [0, 0, 10] 10)
+ "_lessEx" :: [idt, 'a, bool] => bool ("(3? _<_./ _)" [0, 0, 10] 10)
+ "_leAll" :: [idt, 'a, bool] => bool ("(3! _<=_./ _)" [0, 0, 10] 10)
+ "_leEx" :: [idt, 'a, bool] => bool ("(3? _<=_./ _)" [0, 0, 10] 10)
+
translations
- "! x<y. P" => "! x. x < y --> P"
- "! x<=y. P" => "! x. x <= y --> P"
- "? x<y. P" => "? x. x < y & P"
- "? x<=y. P" => "? x. x <= y & P"
+ "ALL x<y. P" => "ALL x. x < y --> P"
+ "EX x<y. P" => "EX x. x < y & P"
+ "ALL x<=y. P" => "ALL x. x <= y --> P"
+ "EX x<=y. P" => "EX x. x <= y & P"
+
end
--- a/src/HOL/Set.thy Tue Aug 17 22:11:05 1999 +0200
+++ b/src/HOL/Set.thy Tue Aug 17 22:13:23 1999 +0200
@@ -44,14 +44,13 @@
syntax
-
(* Infix syntax for non-membership *)
"op ~:" :: ['a, 'a set] => bool ("op ~:")
"op ~:" :: ['a, 'a set] => bool ("(_/ ~: _)" [50, 51] 50)
+
"@Finset" :: args => 'a set ("{(_)}")
-
"@Coll" :: [pttrn, bool] => 'a set ("(1{_./ _})")
"@SetCompr" :: ['a, idts, bool] => 'a set ("(1{_ |/_./ _})")
@@ -64,11 +63,12 @@
"@UNION" :: [pttrn, 'a set, 'b set] => 'b set ("(3UN _:_./ _)" 10)
(* Bounded Quantifiers *)
+ "_Ball" :: [pttrn, 'a set, bool] => bool ("(3ALL _:_./ _)" [0, 0, 10] 10)
+ "_Bex" :: [pttrn, 'a set, bool] => bool ("(3EX _:_./ _)" [0, 0, 10] 10)
- "@Ball" :: [pttrn, 'a set, bool] => bool ("(3! _:_./ _)" [0, 0, 10] 10)
- "@Bex" :: [pttrn, 'a set, bool] => bool ("(3? _:_./ _)" [0, 0, 10] 10)
- "*Ball" :: [pttrn, 'a set, bool] => bool ("(3ALL _:_./ _)" [0, 0, 10] 10)
- "*Bex" :: [pttrn, 'a set, bool] => bool ("(3EX _:_./ _)" [0, 0, 10] 10)
+syntax (HOL)
+ "_Ball" :: [pttrn, 'a set, bool] => bool ("(3! _:_./ _)" [0, 0, 10] 10)
+ "_Bex" :: [pttrn, 'a set, bool] => bool ("(3? _:_./ _)" [0, 0, 10] 10)
translations
"range f" == "f``UNIV"
@@ -78,14 +78,12 @@
"{x. P}" == "Collect (%x. P)"
"UN x y. B" == "UN x. UN y. B"
"UN x. B" == "UNION UNIV (%x. B)"
- "INT x y. B" == "INT x. INT y. B"
+ "INT x y. B" == "INT x. INT y. B"
"INT x. B" == "INTER UNIV (%x. B)"
"UN x:A. B" == "UNION A (%x. B)"
"INT x:A. B" == "INTER A (%x. B)"
- "! x:A. P" == "Ball A (%x. P)"
- "? x:A. P" == "Bex A (%x. P)"
- "ALL x:A. P" => "Ball A (%x. P)"
- "EX x:A. P" => "Bex A (%x. P)"
+ "ALL x:A. P" == "Ball A (%x. P)"
+ "EX x:A. P" == "Bex A (%x. P)"
syntax ("" output)
"_setle" :: ['a set, 'a set] => bool ("op <=")
@@ -112,12 +110,8 @@
"@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Inter> _\\<in>_./ _)" 10)
Union :: (('a set) set) => 'a set ("\\<Union> _" [90] 90)
Inter :: (('a set) set) => 'a set ("\\<Inter> _" [90] 90)
- "@Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
- "@Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
-
-syntax (symbols output)
- "*Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
- "*Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
+ "_Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
+ "_Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
translations
"op \\<subseteq>" => "op <= :: [_ set, _ set] => bool"
@@ -138,7 +132,6 @@
defs
-
Ball_def "Ball A P == ! x. x:A --> P(x)"
Bex_def "Bex A P == ? x. x:A & P(x)"
subset_def "A <= B == ! x:A. x:B"
@@ -157,6 +150,7 @@
insert_def "insert a B == {x. x=a} Un B"
image_def "f``A == {y. ? x:A. y=f(x)}"
+
end
@@ -178,7 +172,7 @@
(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *)
(* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
-val ex_tr = snd(mk_binder_tr("? ","Ex"));
+val ex_tr = snd(mk_binder_tr("EX ","Ex"));
fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
| nvars(_) = 1;
@@ -208,7 +202,6 @@
val parse_translation = [("@SetCompr", setcompr_tr)];
val print_translation = [("Collect", setcompr_tr')];
val typed_print_translation = [("op <=", le_tr'), ("op <", less_tr')];
-val print_ast_translation =
- map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
+
end;