Searched refs:to (Results 126 - 150 of 1836) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/datatype/record/
H A DRecordType.sig18 an augmented tyinfo and a string corresponding to an ML expression
22 [update_tyinfo ths] transforms a tyinfo by adding the ths to it as
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DGenPolyCanon.sig34 it to allow normalisation of "polynomials" over that type, collecting up
40 modes literals are shunted to the right end of the term.
44 left-associated, but possibly prepended by a literal to
59 coefficients. The result will be subjected to
61 postnorm : conversion to normalise certain coeff-term pairs. Must
73 To handle literals, get non_coeff to return a base of 1 for them, and then
76 [update_mode m g] returns a g' that is identical to g except that
77 the assoc_mode field of the record has been updated to have value m.
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/
H A DconstrFamiliesLib.sig22 corresponding to [constr]. For the arguments
59 to each other and injective. *)
138 This functions combines all the contents of a db to
141 (* This tries to find the family used by a call to
148 (* This tries to find an nchotony theorem for the given column. *)
152 (* This tries to destruct a term as a destructor. It looks
153 up in the given DB all possible constructors and tries to
158 (* add a compile fun to a db *)
162 (* add an nchotomy fun to
[all...]
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/
H A DquantHeuristicsLibFunRemove.sig11 (* very simple for to state that some function can be remove.
18 thm list is a list of rewrite theorems used carefully to bring every(!)
/seL4-l4v-10.1.1/HOL4/src/ring/src/
H A DnumRingScript.sml33 (* Hack to avoid (semi_ring 0 1 $+ $* ) to be confused with an end
/seL4-l4v-10.1.1/HOL4/tools/
H A Dbuild.sml13 Magic to ensure that interruptions (SIGINTs) are actually seen by the
53 else die ("Unable to link file "^quote s1^" to file "^quote s2^".")
69 Transport a compiled directory to another location. The
77 (print ("Uploading files to "^target^"\n");
88 For each element in SRCDIRS, build it, then upload it to SIGOBJ.
89 This allows us to have the build process only occur w.r.t. SIGOBJ
90 (thus requiring only a single place to look for things).
/seL4-l4v-10.1.1/graph-refine/seL4-example/
H A Dconfigure_default.sh5 # * This software may be distributed and modified according to the terms of
21 echo Will not be able to build seL4 C models.
45 # check if HOL4 is built, and if it is up to date
73 # setup graph-refine to use CVC4 from Isabelle
82 echo and adjust $SVFL to succeed.
89 echo Configured graph-refine to use CVC4 SMT solver.
96 echo and adjust $SVFL to succeed.
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dmake_imported_acl2_theory.ml30 (* not using map to guarantee hd-to-tl application order *)
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A Dsexp.ml5 (* Print an ACL2 DEFUN (entered as a preterm) to a file defun.tmp.lisp, *)
6 (* then run a2ml, then read in generated mlsexp, convert to a term and *)
H A Dacl2encodeLib.sig2 (* Information and trouble shooting guide for encoding to ACL2. *)
9 (* flatten_recognizers is used to do this. *)
15 (* The two common reasons for the encoding process to fail are: *)
51 (* Recursive calls are characterised by the limit being applied to *)
64 (* Prints all definitions, up until the definition given, to a file. *)
70 (* is occasionally unable to prove termination / verify guards. This will *)
80 (* Set the destructors for a given type to the theorems given. *)
93 (* Initialises a type so that functions over it can be translated to ACL2 *)
108 (* This function should be used to encode types added via hol_datatype. *)
109 (* Failure to d
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/
H A Dppc_closure.S7 Permission is hereby granted, free of charge, to any person obtaining
9 ``Software''), to deal in the Software without restriction, including
10 without limitation the rights to use, copy, modify, merge, publish,
11 distribute, sublicense, and/or sell copies of the Software, and to
12 permit persons to whom the Software is furnished to do so, subject to
44 # we want to build up an areas for the parameters passed
47 # so first save gpr 3 to gpr 10 (aligned to
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DSignal.sml18 License along with this library; if not, write to the Free Software
55 (* This call to the RTS returns either a pair of a signal
57 has been set to NONE. These aren't logically related but
58 it's convenient to use a single thread for both. *)
61 (* When we get a WeakMarker message we need to broadcast
75 to avoid waiting and being unable to handle any signals
84 (Thread.fork(sigThread, []); ()) handle Thread _ => print "Unable to create signal thread\n"
H A DThread.sml16 License along with this library; if not, write to the Free Software
34 (* Does this thread accept a broadcast interrupt? The default is not to
37 (* How to handle interrupts. The default is to handle interrupts synchronously. *)
53 is delivered asynchronously after which the interrupt state is changed to
54 InterruptSynch. It allows a thread to tidy up and if necessary indicate
75 (* Send an Interrupt exception to a specific thread. When and indeed whether
78 so an exception handler should be used unless the thread is known to
81 (* Send an interrupt exception to every thread which is set to accep
[all...]
H A DTextIO.sml15 License along with this library; if not, write to the Free Software
90 writer to map any exception other than Io into Io. *)
141 (* Reread all up to and including the newline
151 temporary end-of-stream to be cleared). *)
183 output1 function is likely to be more efficient. *)
215 (* We have to declare doIo separately depending on the
216 types of the arguments. It's possible to get round this
217 but that would result in an extra call to run_call3 for
265 (* Look at the stream to see what kind of buffering to us
[all...]
/seL4-l4v-10.1.1/HOL4/src/IndDef/Manual/
H A Dpaper.tex15 to appear in the Proceedings of the 1991 International Tutorial
46 definitional\/} approach to using higher order logic. That is, the syntax of
47 the logic is extended with new notation not simply by postulating axioms to
48 give meaning to it, but rather by defining it in terms of existing expressions
50 approach, as opposed to the axiomatic method, is that each of the primitive
52 constant specification, and type definition---is guaranteed to preserve
59 The {\small ML} metalanguage allows users to implement derived inference rules
74 introduction to the class of inductive definitions handled by the package and
84 closure of $R$ can be defined to be the least relation $R^{*} \subseteq A
103 therefore simply be {\it defined\/} to b
[all...]
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/
H A DMutRecDef.sml9 (* MODIFIED : 93.12.28 Fixed to handle polymorphism. ELG. *)
89 constructors to find the information necessary to prove the existence
103 witnesses were found then we need to start a new pass looking at all the
104 types that still don't have witnesses. Otherwise, we need to abort.
120 General Case: We need to try to find a witness for a type being defined.
121 We need to ask of each of it's constructors, whether there are witnesses
125 seen_new_witness_this_pass to true. If none of the constructors are closed
126 yet, we move that type over to no_witness_this_pas
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_LAMBDA_LIFT.sml15 License along with this library; if not, write to the Free Software
20 Lambda-lifting. If every call point to a function can be identified we can
31 empty closures have been code-generated to constants.
53 by setting the "use" or any bindings or recursive uses that require a closure to
57 (* An entry for each local binding. Set to true if we find a non-call reference. *)
69 (* A call of a function. We don't need to mark the function as needing a closure. *)
77 (* We want to add [UseGeneral] to bindings that require closures. To do that
78 we have to process the bindings in reverse order. *)
173 (* If this has been lifted we have to ad
[all...]
/seL4-l4v-10.1.1/HOL4/examples/muddy/
H A Dbdd.sig147 (* Structure bdd provide an interface to J��rn Linds <jl@it.dtu.dk>
156 for small test examples and up to 1000000 nodes for large examples.
157 A cache size of 10000 seems to work good even for large examples,
167 [setvarnum num] is used to define the number of variables used in
168 the bdd package. It may be called more than one time, but only to
169 increase the number of variables. num is the number of variables to
173 package to its initial state.
218 [toSet_ r] converts the bdd r to a varSet; no checks are performed
219 to check that r really represents a varSet therefore it should be
243 [appex x y opr varset] equivalent to 'exis
[all...]
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/
H A Drules.tex10 detailed, low-level proof steps. Later, we shall see how to automate such
15 transformed to yield another.
26 \textbf{Natural deduction} is an attempt to formalize logic in a way
30 The introduction rules allow us to infer this symbol (say, to
31 infer conjunctions). The elimination rules allow us to deduce
35 have to refer to other symbols as well. It is best not to be dogmatic.
39 Natural deduction generally deserves its name. It is easy to us
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/
H A Drules.tex10 detailed, low-level proof steps. Later, we shall see how to automate such
15 transformed to yield another.
26 \textbf{Natural deduction} is an attempt to formalize logic in a way
30 The introduction rules allow us to infer this symbol (say, to
31 infer conjunctions). The elimination rules allow us to deduce
35 have to refer to other symbols as well. It is best not to be dogmatic.
39 Natural deduction generally deserves its name. It is easy to us
[all...]
/seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/
H A DOpentheory.sig17 [define_tyop r] will be called when the article wants to define a type. [r]
18 consists of the name of the type operator to be defined, the type axiom, a list
26 [define_const name rhs] will be called when the article wants to define a new
30 [axiom thms (h,c)] will be called when the article wants to retrieve an
35 [const_name n] and [tyop_name n] will be called to translate OpenTheory names
36 to HOL4 names. The following functions can be used to simply look the names up in the global OpenTheory map.
43 An axiom function for readers that tries to find the desired theorem in the
54 define_tyop and define_const functions for readers that try to produce the
57 current theory. The first argument to [define_const_in_th
[all...]
/seL4-l4v-10.1.1/isabelle/src/Doc/Intro/document/
H A Droot.tex4 %% run bibtex intro to prepare bibliography
5 %% run ../sedindex intro to prepare index file
9 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Introduction to Isabelle}
36 syntax and shows how to conduct proofs using the
52 prover. It has been instantiated to support reasoning in several
56 \item higher-order logic, similar to that of Gordon's {\sc
68 which can be applied to object-logics.
72 The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some
75 if you are prepared to writing \ML{}
76 code, you can get Isabelle to d
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Intro/document/
H A Droot.tex4 %% run bibtex intro to prepare bibliography
5 %% run ../sedindex intro to prepare index file
9 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Introduction to Isabelle}
36 syntax and shows how to conduct proofs using the
52 prover. It has been instantiated to support reasoning in several
56 \item higher-order logic, similar to that of Gordon's {\sc
68 which can be applied to object-logics.
72 The Isabelle/HOL \emph{Tutorial}~\cite{isa-tutorial} describes how to get started. Advanced Isabelle users will benefit from some
75 if you are prepared to writing \ML{}
76 code, you can get Isabelle to d
[all...]
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A DHolSat.tex49 The purpose of {\tt{HolSatLib}} is to provide a platform for experimenting with combinations of theorem proving and SAT solvers. Only black box functionality is provided at the moment; an incremental interface is not available.
51 {\tt{HolSatLib}} provides a function {\tt SAT\_PROVE} \index{HolSatLib!SAT\_PROVE@\ml{SAT\_PROVE}} for propositional satisfiability testing and for proving propositional tautologies. It uses an external SAT solver (currently MiniSat 1.14p) to find an unsatisfiability proof or satisfying assignment, and then reconstructs the proof or checks the assignment deductively in \HOL.
53 Alternatively, the function {\tt SAT\_ORACLE} \index{HolSatLib!SAT\_ORACLE@\ml{SAT\_ORACLE}} has the same behaviour as {\tt SAT\_PROVE} but asserts the result of the solver without proof. The theorem thus asserted is tagged with ``{\tt{HolSatLib}}'' to indicate that it is unchecked. Since proof reconstruction can be expensive, the oracle facility can be useful during prototyping, or if proof is not required.
81 Setting \t{show\_tags} to \t{true} makes the \HOL{} top-level print theorem tags. The \t{DISK\_THM} oracle tag has nothing to do with \t{HolSatLib}. It just indicates the use of theorems from \HOL{} libraries read in from permanent storage.
85 The next example illustrates using {\tt{HolSatLib}} for satisfiability testing. The idea is to negate the target term before passing it to {\tt{HolSatLib}}.
102 {\tt{HolSatLib}} can only handle purely propositional terms (atoms must be propositional variables or constants) involving the usual propositional connectives as well as Boolean-valued conditionals. If you wish to prove tautologies that are instantiations of propositional terms, use {\tt{tautLib}} (see \S\ref{tautlib} below).
104 If MiniSat failed to build when \HOL{} was built, or proof replay fails for some other reason, \t{SAT\_PROVE} falls back to
[all...]
/seL4-l4v-10.1.1/HOL4/src/TeX/
H A Dholindex-demo.tex25 \item run \texttt{mkmunge.exe theories} to generate \texttt{munge.exe}
27 \item run latex on jobname.tex to generate jobname.hix
28 \item run \texttt{munge.exe -index jobname} to create jobname.tde and jobname.tid
29 \item rerun latex to use jobname.tid and jobname.tde
31 \item if using emacs with AucTex you might want to add to your \texttt{.emacs}
34 '(add-to-list 'TeX-command-list
55 - you want to use one theorem with different formating options
56 - you want to add a theorem several times to th
[all...]

Completed in 262 milliseconds

1234567891011>>