# HG changeset patch # User wenzelm # Date 749745834 -3600 # Node ID d199410f1db12ee077193c8fff64b0e14da55798 # Parent a910a65478be8d986c2f4a3f8bfe5c4b08c38483 HOL/hol.thy renamed mk_alt_ast_tr' to alt_ast_tr'; added alternative quantifier THE; replaced Ast by Syntax; HOL/set.thy replaced HOL.mk_alt_ast_tr' by HOL.alt_ast_tr'; diff -r a910a65478be -r d199410f1db1 HOL.thy --- a/HOL.thy Tue Sep 28 14:27:31 1993 +0100 +++ b/HOL.thy Mon Oct 04 15:43:54 1993 +0100 @@ -28,41 +28,42 @@ (* Constants *) - Trueprop :: "bool => prop" ("(_)" [0] 5) - not :: "bool => bool" ("~ _" [40] 40) + Trueprop :: "bool => prop" ("(_)" 5) + not :: "bool => bool" ("~ _" [40] 40) True, False :: "bool" if :: "[bool, 'a, 'a] => 'a" Inv :: "('a => 'b) => ('b => 'a)" (* Binders *) - Eps :: "('a => bool) => 'a" (binder "@" 10) - All :: "('a => bool) => bool" (binder "! " 10) - Ex :: "('a => bool) => bool" (binder "? " 10) - Ex1 :: "('a => bool) => bool" (binder "?! " 10) + Eps :: "('a => bool) => 'a" (binder "@" 10) + All :: "('a => bool) => bool" (binder "! " 10) + Ex :: "('a => bool) => bool" (binder "? " 10) + Ex1 :: "('a => bool) => bool" (binder "?! " 10) - Let :: "['a, 'a=>'b] => 'b" - "@let" :: "[idt,'a,'b] => 'b" ("(let _ = (2_)/ in (2_))" 10) + Let :: "['a, 'a => 'b] => 'b" + "@Let" :: "[idt, 'a, 'b] => 'b" ("(let _ = (2_)/ in (2_))" 10) (* Alternative Quantifiers *) - "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" [0,0] 10) - "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" [0,0] 10) - "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" [0,0] 10) + "*The" :: "[idts, bool] => 'a" ("(3THE _./ _)" 10) + "*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) - "&" :: "[bool, bool] => bool" (infixr 35) - "|" :: "[bool, bool] => bool" (infixr 30) - "-->" :: "[bool, bool] => bool" (infixr 25) + o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) + "=" :: "['a, 'a] => bool" (infixl 50) + "&" :: "[bool, bool] => bool" (infixr 35) + "|" :: "[bool, bool] => bool" (infixr 30) + "-->" :: "[bool, bool] => bool" (infixr 25) (* Overloaded Constants *) - "+" :: "['a::plus, 'a] => 'a" (infixl 65) - "-" :: "['a::minus, 'a] => 'a" (infixl 65) - "*" :: "['a::times, 'a] => 'a" (infixl 70) + "+" :: "['a::plus, 'a] => 'a" (infixl 65) + "-" :: "['a::minus, 'a] => 'a" (infixl 65) + "*" :: "['a::times, 'a] => 'a" (infixl 70) (* Rewriting Gadget *) @@ -70,11 +71,12 @@ translations + "THE xs. P" => "@ xs. P" "ALL xs. P" => "! xs. P" "EX xs. P" => "? xs. P" "EX! xs. P" => "?! xs. P" - "let x = s in t" == "Let(s,%x.t)" + "let x = s in t" == "Let(s, %x. t)" rules @@ -100,7 +102,7 @@ and_def "op & = (%P Q. !R. (P-->Q-->R) --> R)" or_def "op | = (%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)" + Let_def "Let(s, f) = f(s)" (* Axioms *) @@ -127,16 +129,16 @@ val HOL_quantifiers = ref true; -fun mk_alt_ast_tr' (name, alt_name) = +fun alt_ast_tr' (name, alt_name) = let fun ast_tr' (*name*) args = if ! HOL_quantifiers then raise Match - else Ast.mk_appl (Ast.Constant alt_name) args; + else Syntax.mk_appl (Syntax.Constant alt_name) args; in (name, ast_tr') end; val print_ast_translation = - map mk_alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")]; + map alt_ast_tr' [("@", "*The"), ("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")]; diff -r a910a65478be -r d199410f1db1 Set.thy --- a/Set.thy Tue Sep 28 14:27:31 1993 +0100 +++ b/Set.thy Mon Oct 04 15:43:54 1993 +0100 @@ -19,43 +19,43 @@ (* Constants *) - Collect :: "('a => bool) => 'a set" (*comprehension*) - Compl :: "('a set) => 'a set" (*complement*) - Int :: "['a set, 'a set] => 'a set" (infixl 70) - Un :: "['a set, 'a set] => 'a set" (infixl 65) - UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) - 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*) - range :: "('a => 'b) => 'b set" (*of function*) - Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*) - inj, surj :: "('a => 'b) => bool" (*injective/surjective*) + Collect :: "('a => bool) => 'a set" (*comprehension*) + Compl :: "('a set) => 'a set" (*complement*) + Int :: "['a set, 'a set] => 'a set" (infixl 70) + Un :: "['a set, 'a set] => 'a set" (infixl 65) + UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) + 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*) + range :: "('a => 'b) => 'b set" (*of function*) + Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*) + inj, surj :: "('a => 'b) => bool" (*injective/surjective*) inj_onto :: "['a => 'b, 'a set] => bool" - "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90) - ":" :: "['a, 'a set] => bool" (infixl 50) (*membership*) + "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90) + ":" :: "['a, 'a set] => bool" (infixl 50) (*membership*) (* Finite Sets *) insert :: "['a, 'a set] => 'a set" - "{}" :: "'a set" ("{}") - "@Finset" :: "args => 'a set" ("{(_)}") + "{}" :: "'a set" ("{}") + "@Finset" :: "args => 'a set" ("{(_)}") (** Binding Constants **) - "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*) + "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*) (* Big Intersection / Union *) - "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(3INT _:_./ _)" 10) - "@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(3UN _:_./ _)" 10) + "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(3INT _:_./ _)" 10) + "@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(3UN _:_./ _)" 10) (* Bounded Quantifiers *) - "@Ball" :: "[idt, 'a set, bool] => bool" ("(3! _:_./ _)" 10) - "@Bex" :: "[idt, 'a set, bool] => bool" ("(3? _:_./ _)" 10) - "*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10) - "*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10) + "@Ball" :: "[idt, 'a set, bool] => bool" ("(3! _:_./ _)" 10) + "@Bex" :: "[idt, 'a set, bool] => bool" ("(3? _:_./ _)" 10) + "*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10) + "*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10) translations @@ -107,5 +107,5 @@ ML val print_ast_translation = - map HOL.mk_alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")]; + map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")]; diff -r a910a65478be -r d199410f1db1 hol.thy --- a/hol.thy Tue Sep 28 14:27:31 1993 +0100 +++ b/hol.thy Mon Oct 04 15:43:54 1993 +0100 @@ -28,41 +28,42 @@ (* Constants *) - Trueprop :: "bool => prop" ("(_)" [0] 5) - not :: "bool => bool" ("~ _" [40] 40) + Trueprop :: "bool => prop" ("(_)" 5) + not :: "bool => bool" ("~ _" [40] 40) True, False :: "bool" if :: "[bool, 'a, 'a] => 'a" Inv :: "('a => 'b) => ('b => 'a)" (* Binders *) - Eps :: "('a => bool) => 'a" (binder "@" 10) - All :: "('a => bool) => bool" (binder "! " 10) - Ex :: "('a => bool) => bool" (binder "? " 10) - Ex1 :: "('a => bool) => bool" (binder "?! " 10) + Eps :: "('a => bool) => 'a" (binder "@" 10) + All :: "('a => bool) => bool" (binder "! " 10) + Ex :: "('a => bool) => bool" (binder "? " 10) + Ex1 :: "('a => bool) => bool" (binder "?! " 10) - Let :: "['a, 'a=>'b] => 'b" - "@let" :: "[idt,'a,'b] => 'b" ("(let _ = (2_)/ in (2_))" 10) + Let :: "['a, 'a => 'b] => 'b" + "@Let" :: "[idt, 'a, 'b] => 'b" ("(let _ = (2_)/ in (2_))" 10) (* Alternative Quantifiers *) - "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" [0,0] 10) - "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" [0,0] 10) - "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" [0,0] 10) + "*The" :: "[idts, bool] => 'a" ("(3THE _./ _)" 10) + "*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) - "&" :: "[bool, bool] => bool" (infixr 35) - "|" :: "[bool, bool] => bool" (infixr 30) - "-->" :: "[bool, bool] => bool" (infixr 25) + o :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixr 50) + "=" :: "['a, 'a] => bool" (infixl 50) + "&" :: "[bool, bool] => bool" (infixr 35) + "|" :: "[bool, bool] => bool" (infixr 30) + "-->" :: "[bool, bool] => bool" (infixr 25) (* Overloaded Constants *) - "+" :: "['a::plus, 'a] => 'a" (infixl 65) - "-" :: "['a::minus, 'a] => 'a" (infixl 65) - "*" :: "['a::times, 'a] => 'a" (infixl 70) + "+" :: "['a::plus, 'a] => 'a" (infixl 65) + "-" :: "['a::minus, 'a] => 'a" (infixl 65) + "*" :: "['a::times, 'a] => 'a" (infixl 70) (* Rewriting Gadget *) @@ -70,11 +71,12 @@ translations + "THE xs. P" => "@ xs. P" "ALL xs. P" => "! xs. P" "EX xs. P" => "? xs. P" "EX! xs. P" => "?! xs. P" - "let x = s in t" == "Let(s,%x.t)" + "let x = s in t" == "Let(s, %x. t)" rules @@ -100,7 +102,7 @@ and_def "op & = (%P Q. !R. (P-->Q-->R) --> R)" or_def "op | = (%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)" + Let_def "Let(s, f) = f(s)" (* Axioms *) @@ -127,16 +129,16 @@ val HOL_quantifiers = ref true; -fun mk_alt_ast_tr' (name, alt_name) = +fun alt_ast_tr' (name, alt_name) = let fun ast_tr' (*name*) args = if ! HOL_quantifiers then raise Match - else Ast.mk_appl (Ast.Constant alt_name) args; + else Syntax.mk_appl (Syntax.Constant alt_name) args; in (name, ast_tr') end; val print_ast_translation = - map mk_alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")]; + map alt_ast_tr' [("@", "*The"), ("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")]; diff -r a910a65478be -r d199410f1db1 set.thy --- a/set.thy Tue Sep 28 14:27:31 1993 +0100 +++ b/set.thy Mon Oct 04 15:43:54 1993 +0100 @@ -19,43 +19,43 @@ (* Constants *) - Collect :: "('a => bool) => 'a set" (*comprehension*) - Compl :: "('a set) => 'a set" (*complement*) - Int :: "['a set, 'a set] => 'a set" (infixl 70) - Un :: "['a set, 'a set] => 'a set" (infixl 65) - UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) - 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*) - range :: "('a => 'b) => 'b set" (*of function*) - Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*) - inj, surj :: "('a => 'b) => bool" (*injective/surjective*) + Collect :: "('a => bool) => 'a set" (*comprehension*) + Compl :: "('a set) => 'a set" (*complement*) + Int :: "['a set, 'a set] => 'a set" (infixl 70) + Un :: "['a set, 'a set] => 'a set" (infixl 65) + UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) + 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*) + range :: "('a => 'b) => 'b set" (*of function*) + Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*) + inj, surj :: "('a => 'b) => bool" (*injective/surjective*) inj_onto :: "['a => 'b, 'a set] => bool" - "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90) - ":" :: "['a, 'a set] => bool" (infixl 50) (*membership*) + "``" :: "['a => 'b, 'a set] => ('b set)" (infixl 90) + ":" :: "['a, 'a set] => bool" (infixl 50) (*membership*) (* Finite Sets *) insert :: "['a, 'a set] => 'a set" - "{}" :: "'a set" ("{}") - "@Finset" :: "args => 'a set" ("{(_)}") + "{}" :: "'a set" ("{}") + "@Finset" :: "args => 'a set" ("{(_)}") (** Binding Constants **) - "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*) + "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*) (* Big Intersection / Union *) - "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(3INT _:_./ _)" 10) - "@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(3UN _:_./ _)" 10) + "@INTER" :: "[idt, 'a set, 'b set] => 'b set" ("(3INT _:_./ _)" 10) + "@UNION" :: "[idt, 'a set, 'b set] => 'b set" ("(3UN _:_./ _)" 10) (* Bounded Quantifiers *) - "@Ball" :: "[idt, 'a set, bool] => bool" ("(3! _:_./ _)" 10) - "@Bex" :: "[idt, 'a set, bool] => bool" ("(3? _:_./ _)" 10) - "*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10) - "*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10) + "@Ball" :: "[idt, 'a set, bool] => bool" ("(3! _:_./ _)" 10) + "@Bex" :: "[idt, 'a set, bool] => bool" ("(3? _:_./ _)" 10) + "*Ball" :: "[idt, 'a set, bool] => bool" ("(3ALL _:_./ _)" 10) + "*Bex" :: "[idt, 'a set, bool] => bool" ("(3EX _:_./ _)" 10) translations @@ -107,5 +107,5 @@ ML val print_ast_translation = - map HOL.mk_alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")]; + map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];