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';
--- 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")];
--- 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")];
--- 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")];
--- 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")];