# HOL-Theorem-Prover/HOL

### Subversion checkout URL

You can clone with
or
.

# Comparing changes

Choose two branches to see what's changed or to start a new pull request. If you need to, you can also compare across forks.

# Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
...
• 7 commits
• 7 files changed
• 2 contributors
Commits on Oct 07, 2011
 mn200 Make point in Tutorial that structures may need to be opened. In response to a comment from a user. f83d69f mn200 Remove some trailing whitespace. fca9a25
Commits on Oct 09, 2011
 mn200 Document GEN_ABS. Closes #3. 30fca47
Commits on Oct 10, 2011
 mn200 Remove trailing whitespace in src/num/termination/TotalDefn.sml 9ee0a82
Commits on Oct 11, 2011
 mn200 Document RESORT_{FORALL,EXISTS}_CONV. Closes #5. ec954cf xrchz remove a bash-ism from HolQbfLib When /bin/sh is dash (e.g. on Ubuntu I think) HolQbfLib's system call to squolem2 won't work ("Syntax error: Bad fd number"). This should fix it. d24a68e xrchz Merge branch 'master' into logging 965f2c1
12 Manual/Tutorial/logic.tex
 @@ -151,7 +151,7 @@ \chapter{The HOL Logic}\label{HOLlogic} \end{session} The constructors {\small\verb|mk_conj|} and {\small\verb|mk_imp|} construct -conjunctions and implications respectively. A large collection of +conjunctions and implications respectively. A large collection of term constructors and destructors is available for the core theories in \HOL. @@ -228,7 +228,7 @@ \chapter{The HOL Logic}\label{HOLlogic} \paragraph{Function application types} -An application $(t_1\ t_2)$ is well-typed if $t_1$ is a function +An application $(t_1\ t_2)$ is well-typed if $t_1$ is a function with type $\tau_1 \to \tau_2$ and $t_2$ has type $\tau_1$. Contrarily, an application $(t_1\ t_2)$ is badly typed if $t_1$ is not a function: @@ -262,7 +262,7 @@ \chapter{The HOL Logic}\label{HOLlogic} unification failure message: unify failed ! Uncaught exception: -! HOL_ERR +! HOL_ERR \end{verbatim}\end{session} The dollar symbol in front of {\small\verb|~|} indicates that the @@ -564,14 +564,14 @@ \section{Forward proof} - val Th5 = ASSUME t1; <> ! Uncaught exception: -! HOL_ERR +! HOL_ERR - val Th5 = ASSUME t1 handle e => Raise e; <> Exception raised at Thm.ASSUME: not a proposition ! Uncaught exception: -! HOL_ERR +! HOL_ERR - val Th5 = ASSUME t1:bool; > val Th5 = [.] |- t1 : thm @@ -1032,7 +1032,7 @@ \section{Goal Oriented Proof: Tactics and Tacticals} are propagated unchanged to the two subgoals is indicated by the absence of assumptions in the notation. -Another example is {\small\verb|numLib.INDUCT_TAC|}, the tactic for +Another example is \ml{numLib.INDUCT_TAC},\footnote{Later, we will write \ml{INDUCT_TAC} on its own, without first prefixing it with \ml{numLib}. To allow this we must issue the command \ml{open~numLib}.} the tactic for doing mathematical induction on the natural numbers: \begin{center}
1  Manual/Tutorial/tutorial.tex
 @@ -27,6 +27,7 @@ %\includeonly{Studies/int_mod/mod_arith_study/tutorial} %\includeonly{binomial} %\includeonly{parity} +\usepackage[strings]{underscore} \begin{document}
38 help/Docfiles/Conv.RESORT_EXISTS_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
38 help/Docfiles/Conv.RESORT_FORALL_CONV.doc
 @@ -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
59 help/Docfiles/Thm.GEN_ABS.doc
 @@ -0,0 +1,59 @@ +\DOC + +\TYPE {GEN_ABS : term option -> term list -> thm -> thm} + +\SYNOPSIS +Rule of inference for building binder-equations. + +\KEYWORDS + +\DESCRIBE +The {GEN_ABS} function is, semantically at least, a derived rule that +combines applications of the primitive rules {ABS} and {MK_COMB}. +When the first argument, a term option, is the value {NONE}, the +effect is an iterated application of the rule {ABS} (as per {List.foldl}. Thus, +{ + G |- x = y + -------------------------------------------- GEN_ABS NONE [v1,v2,...,vn] + G |- (\v1 v2 .. vn. x) = (\v1 v2 .. vn. y) +} +If the first argument is {SOME b} for some term {b}, this term {b} is +to be a binder, usually of polymorphic type {:('a -> bool) -> bool}. +Then the effect is to interleave the effect of {ABS} and a call to +{AP_TERM}. For every variable {v} in the list, the following theorem +transformation will occur +{ + G |- x = y + ------------------------ ABS v + G |- (\v. x) = (\v. y) + ---------------------------- AP_TERM b' + G |- b (\v. x) = b (\v. x) +} +where {b'} is a version of {b} that has been instantiated to match the +type of the term to which it is applied ({AP_TERM} doesn't do this). + +\EXAMPLE +{ +- val th = REWRITE_CONV [] t /\ u /\ u +> val th = |- t /\ u /\ u = t /\ u : thm + +- GEN_ABS (SOME \$!) [t:bool, u:bool] th; +> val it = |- (!t u. t /\ u /\ u) <=> (!t u. t /\ u) : thm +} + +\FAILURE +Fails if the theorem argument is not an equality. Fails if the second +argument (the list of terms) does not consist of variables. Fails if +any of the variables in the list appears in the hypotheses of the +theorem. Fails if the first argument is {SOME b} and the type of {b} +is either not of type {:('a -> bool) -> bool}, or some +{:(ty -> bool) -> bool} where all the variables have type {ty}. + +\COMMENTS +Though semantically a derived rule, a HOL kernel may implement this as +part of its core for reasons of efficiency. + +\SEEALSO +Thm.ABS, Thm.AP_TERM, Thm.MK_COMB. + +\ENDDOC
2  src/HolQbf/HolQbfLib.sml
 @@ -9,7 +9,7 @@ structure HolQbfLib :> HolQbfLib = struct val path = FileSys.tmpName () val dict = QDimacs.write_qdimacs_file path t (* the actual system call to Squolem *) - val cmd = "squolem2 -c " ^ path ^ " >& /dev/null" + val cmd = "squolem2 -c " ^ path ^ " >/dev/null 2>&1" val _ = if !QbfTrace.trace > 1 then Feedback.HOL_MESG ("HolQbfLib: calling external command '" ^ cmd ^ "'") else ()
8 src/num/termination/TotalDefn.sml
 @@ -113,18 +113,18 @@ fun mk_lex_reln argvars sizedlist arrangement = (* x.fld is a proper subterm of x. *) (*---------------------------------------------------------------------------*) -fun is_recd_proj tm1 tm2 = +fun is_recd_proj tm1 tm2 = let val (proj,a) = dest_comb tm1 val aty = type_of a - val projlist = mapfilter + val projlist = mapfilter (fst o dest_comb o boolSyntax.lhs o snd o strip_forall o concl) (TypeBase.accessors_of aty) in TypeBase.is_record_type aty andalso mem proj projlist end handle HOL_ERR _ => false; - + fun proper_subterm tm1 tm2 = - not(aconv tm1 tm2) + not(aconv tm1 tm2) andalso (Lib.can (find_term (aconv tm1)) tm2 orelse is_recd_proj tm1 tm2);

### No commit comments for this range

Something went wrong with that request. Please try again.