# HG changeset patch # User wenzelm # Date 934920803 -7200 # Node ID 36e58620ffc8352b5cbd12023624f9ec29bf4f18 # Parent 2919daadba912f8887681cf0432720d848512c3e replaced HOL_quantifiers flag by "HOL" print mode; simplified HOL basic syntax (more orthogonal); diff -r 2919daadba91 -r 36e58620ffc8 NEWS --- 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 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 "\\\\" 25) "op o" :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl "\\" 55) "op ~=" :: ['a, 'a] => bool (infixl "\\" 50) - "@Eps" :: [pttrn, bool] => 'a ("(3\\_./ _)" [0, 10] 10) - "! " :: [idts, bool] => bool ("(3\\_./ _)" [0, 10] 10) - "? " :: [idts, bool] => bool ("(3\\_./ _)" [0, 10] 10) - "?! " :: [idts, bool] => bool ("(3\\!_./ _)" [0, 10] 10) + "_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) "@case1" :: ['a, 'b] => case_syn ("(2_ \\/ _)" 10) (*"@case2" :: [case_syn, cases_syn] => cases_syn ("_/ \\ _")*) syntax (symbols output) "op ~=" :: ['a, 'a] => bool ("(_ \\/ _)" [51, 51] 50) - "*All" :: [idts, bool] => bool ("(3\\_./ _)" [0, 10] 10) - "*Ex" :: [idts, bool] => bool ("(3\\_./ _)" [0, 10] 10) - "*Ex1" :: [idts, bool] => bool ("(3\\!_./ _)" [0, 10] 10) syntax (xsymbols) "op -->" :: [bool, bool] => bool (infixr "\\" 25) @@ -146,6 +133,13 @@ syntax (HTML output) Not :: bool => bool ("\\ _" [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")]; diff -r 2919daadba91 -r 36e58620ffc8 src/HOL/Ord.thy --- 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\\_<_./ _)" [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) + +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 "! x. x < y --> P" - "! x<=y. P" => "! x. x <= y --> P" - "? x "? x. x < y & P" - "? x<=y. P" => "? x. x <= y & P" + "ALL x "ALL x. x < y --> P" + "EX x "EX x. x < y & P" + "ALL x<=y. P" => "ALL x. x <= y --> P" + "EX x<=y. P" => "EX x. x <= y & P" + end diff -r 2919daadba91 -r 36e58620ffc8 src/HOL/Set.thy --- 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\\ _\\_./ _)" 10) Union :: (('a set) set) => 'a set ("\\ _" [90] 90) Inter :: (('a set) set) => 'a set ("\\ _" [90] 90) - "@Ball" :: [pttrn, 'a set, bool] => bool ("(3\\ _\\_./ _)" [0, 0, 10] 10) - "@Bex" :: [pttrn, 'a set, bool] => bool ("(3\\ _\\_./ _)" [0, 0, 10] 10) - -syntax (symbols output) - "*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 ("(3\\ _\\_./ _)" [0, 0, 10] 10) + "_Bex" :: [pttrn, 'a set, bool] => bool ("(3\\ _\\_./ _)" [0, 0, 10] 10) translations "op \\" => "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;