Permalink
Browse files

Document RESORT_{FORALL,EXISTS}_CONV. Closes #5.

  • Loading branch information...
1 parent 9ee0a82 commit ec954cf792574872095edc7037822dd5a8fb459f @mn200 mn200 committed Oct 11, 2011
Showing with 76 additions and 0 deletions.
  1. +38 −0 help/Docfiles/Conv.RESORT_EXISTS_CONV.doc
  2. +38 −0 help/Docfiles/Conv.RESORT_FORALL_CONV.doc
@@ -0,0 +1,38 @@
+\DOC
+
+\TYPE {RESORT_EXISTS_CONV : (term list -> term list) -> conv}
+
+\SYNOPSIS
+Reorders bound variables under existential quantifiers.
+
+\KEYWORDS
+
+\DESCRIBE
+
+A call to {RESORT_EXISTS_CONV f t} strips the outer
+existentially-quantified variables of {t}, giving a list {vs}, such that
+{t} is of the form {?vs. body}. The list {vs} is then passed to the
+function argument {f}. The result of the call {f vs} is expected to
+be a new list of variables {vs'}, and the result of the conversion is
+the theorem
+{
+ |- (?vs. body) <=> (?vs'. body)
+}
+The function {f} is generally expected to return a permutation of the
+variables appearing in the term {vs}, but may in fact introduce fresh
+variables that are fresh for {body}, and may also remove variables
+from {vs} that also don't appear in {body}.
+
+\FAILURE
+Given a term {t}, fails if {t} is not of boolean type. Fails if when
+applied to the outermost existentially quantified variables (permitted
+to be the empty list) the function {f} returns a list of terms that
+are not all variables. Also fails if either {f} returns a list that
+does not include variables from {vs} that appear in the body of {t},
+or if it includes variables that are in the body, but which were not
+originally bound.
+
+\SEEALSO
+Conv.RESORT_FORALL_CONV.
+
+\ENDDOC
@@ -0,0 +1,38 @@
+\DOC
+
+\TYPE {RESORT_FORALL_CONV : (term list -> term list) -> conv}
+
+\SYNOPSIS
+Reorders bound variables under universal quantifiers.
+
+\KEYWORDS
+
+\DESCRIBE
+
+A call to {RESORT_FORALL_CONV f t} strips the outer
+universally-quantified variables of {t}, giving a list {vs}, such that
+{t} is of the form {!vs. body}. The list {vs} is then passed to the
+function argument {f}. The result of the call {f vs} is expected to
+be a new list of variables {vs'}, and the result of the conversion is
+the theorem
+{
+ |- (!vs. body) <=> (!vs'. body)
+}
+The function {f} is generally expected to return a permutation of the
+variables appearing in the term {vs}, but may in fact introduce fresh
+variables that are fresh for {body}, and may also remove variables
+from {vs} that also don't appear in {body}.
+
+\FAILURE
+Given a term {t}, fails if {t} is not of boolean type. Fails if when
+applied to the outermost universally quantified variables (permitted
+to be the empty list) the function {f} returns a list of terms that
+are not all variables. Also fails if either {f} returns a list that
+does not include variables from {vs} that appear in the body of {t},
+or if it includes variables that are in the body, but which were not
+originally bound.
+
+\SEEALSO
+Conv.RESORT_EXISTS_CONV.
+
+\ENDDOC

0 comments on commit ec954cf

Please sign in to comment.