Merge pull request #111 from jargh/master

Enable more descriptive names for quantifiers and logical constants

Help/set_verbose_symbols.hlp

@@ -0,0 +1,61 @@
+\DOC set_verbose_symbols
+
+\TYPE {set_verbose_symbols : unit -> unit}
+
+\SYNOPSIS
+Enables more verbose descriptive names for quantifiers and logical constants
+
+\DESCRIBE
+A call to {set_verbose_symbols()} enables a more verbose syntax for the logical
+quantifiers and constants. These are all just interface mappings, the
+underlying constant names in the abstract syntax of the logic being unchanged.
+But the more descriptive names are applied by default when printing and
+are accepted when parsing terms as synonyms of the symbolic names. The new
+names are:
+
+\begin{{itemize}}
+
+\item The universal quantifier `{!}' is now parsed and printed as `{forall}'
+
+\item The existential quantifier `{?}' is now parsed and printed as `{exists}'
+
+\item The exists-unique quantifier `{?!}' is now parsed and printed as
+`{existsunique}'
+
+\item The logical constant `{T}' is now parsed and printed as `{true}'
+
+\item The logical constant `{F}' is now parsed and printed as `{false}'
+
+\end{{itemize}}
+
+The effect can be reverse by a call to the dual function
+{unset_verbose_symbols()}.
+
+\EXAMPLE
+Notice how the printing of theorems changes from using the symbolic names for
+quantifiers
+{
+  # unset_verbose_symbols();;
+  val it : unit = ()
+  # num_Axiom;;
+  val it : thm = |- !e f. ?!fn. fn 0 = e /\ (!n. fn (SUC n) = f (fn n) n)
+}
+\noindent to the more verbose and descriptive names:
+{
+  # set_verbose_symbols();;
+  val it : unit = ()
+  # num_Axiom;;
+  val it : thm =
+    |- forall e f.
+           existsunique fn. fn 0 = e /\ (forall n. fn (SUC n) = f (fn n) n)
+}
+
+\FAILURE
+Only fails if some of the names have already been used for incompatible
+constants.
+
+\SEEALSO
+overload_interface, override_interface, remove_interface,
+the_interface, unset_verbose_symbols.
+
+\ENDDOC

Help/unset_verbose_symbols.hlp

@@ -0,0 +1,38 @@
+\DOC unset_verbose_symbols
+
+\TYPE {unset_verbose_symbols : unit -> unit}
+
+\SYNOPSIS
+Disables more verbose descriptive names for quantifiers and logical constants
+
+\DESCRIBE
+A call to {unset_verbose_symbols()} disables the more verbose syntax for the
+logical quantifiers and constants that is set up by default and can be
+explicitly enabled by the dual function {set_verbose_symbols()}.
+
+\EXAMPLE
+Notice how the printing of theorems changes from using the verbose descriptive
+names for quantifiers by default:
+{
+  # num_Axiom;;
+  val it : thm =
+    |- forall e f.
+           existsunique fn. fn 0 = e /\ (forall n. fn (SUC n) = f (fn n) n)
+}
+\noindent to using the more concise symbolic names
+{
+  # unset_verbose_symbols();;
+  val it : unit = ()
+  # num_Axiom;;
+  val it : thm = |- !e f. ?!fn. fn 0 = e /\ (!n. fn (SUC n) = f (fn n) n)
+}
+
+\FAILURE
+Only fails if some of the names have already been used for incompatible
+constants.
+
+\SEEALSO
+overload_interface, override_interface, remove_interface, set_verbose_symbols,
+the_interface.
+
+\ENDDOC

bool.ml

@@ -482,3 +482,23 @@ let EXISTENCE =
         let ty = snd(dest_var(bndvar abs)) in
         MP (PINST [ty,aty] [abs,P] pth) th
     with Failure _ -> failwith "EXISTENCE";;
+
+(* ------------------------------------------------------------------------- *)
+(* Optionally select more verbose syntax for quantifiers, as well            *)
+(* as the logical constants T (true) and F (false). Enabled by default.      *)
+(* ------------------------------------------------------------------------- *)
+
+let set_verbose_symbols() =
+ (do_list parse_as_binder ["forall"; "exists"; "existsunique"];
+  override_interface("true",`T`);
+  override_interface("false",`F`);
+  override_interface("forall",`(!):(A->bool)->bool`);
+  override_interface("exists",`(?):(A->bool)->bool`);
+  override_interface("existsunique",`(?!):(A->bool)->bool`));;
+
+let unset_verbose_symbols() =
+ (do_list unparse_as_binder ["forall"; "exists"; "existsunique"];
+  do_list remove_interface
+    ["true"; "false"; "forall"; "exists"; "existsunique"]);;
+
+set_verbose_symbols();;