Searched refs:clause (Results 76 - 100 of 130) sorted by relevance

123456

/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DRule.sig270 val factor' : Thm.clause -> Subst.subst list
H A DTptp.sml781 type clause = literal list; type
817 fun clauseFromThm th = clauseFromLiteralSet (Thm.clause th);
1848 | CnfGoal of (formulaName * clause) list
1923 fun addCnf role ((name,clause),(norm,cnf)) =
1924 if List.exists (equalBooleanLiteral true) clause then (norm,cnf)
1927 val cl = List.mapPartial (total destLiteral) clause
1930 val src = CnfClauseSource (name,clause)
2395 val cls = List.map Thm.clause (Proof.parents inference)
2445 val cl = Thm.clause th
H A DRewrite.sml169 literalsReducible order known id (Thm.clause th);
335 val (neq,_) = mkNeqConvs order (Thm.clause th)
397 rewriteIdLiteralsRule' order known redexes id (Thm.clause th) th;
H A Dproblems.sml216 (lit ==> clause) ==> (lit \/ clause <=> clause)`},
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DRule.sig270 val factor' : Thm.clause -> Subst.subst list
H A DTptp.sml781 type clause = literal list; type
817 fun clauseFromThm th = clauseFromLiteralSet (Thm.clause th);
1848 | CnfGoal of (formulaName * clause) list
1923 fun addCnf role ((name,clause),(norm,cnf)) =
1924 if List.exists (equalBooleanLiteral true) clause then (norm,cnf)
1927 val cl = List.mapPartial (total destLiteral) clause
1930 val src = CnfClauseSource (name,clause)
2395 val cls = List.map Thm.clause (Proof.parents inference)
2445 val cl = Thm.clause th
H A DRewrite.sml169 literalsReducible order known id (Thm.clause th);
335 val (neq,_) = mkNeqConvs order (Thm.clause th)
397 rewriteIdLiteralsRule' order known redexes id (Thm.clause th) th;
H A Dproblems.sml216 (lit ==> clause) ==> (lit \/ clause <=> clause)`},
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DBASE_PARSE_TREE.sml220 patterns in each clause. It checks that they are the same in each
221 clause. *)
H A DBaseParseTreeSig.sml223 patterns in each clause. It checks that they are the same in each
224 clause. *)
H A DTYPECHECK_PARSETREE.sml1643 may be more than one clause in a function binding but each
1652 (* Just look at the first clause for the moment. *)
1698 fun processClause (clause as FValClause {dec, exp, line, ...}) =
1723 (* This clause as a parsetree object for error messages. *)
1724 mkFunDeclaration([mkClausal([clause], line)], explicit, implicit, line)
1731 name ^ " has already been bound in this clause.");
1806 assigns the result type for each clause in the fun but
1809 (* The type of this clause is a function type. *)
1816 typeMismatch("Type of clause does not match the type of previous clauses.",
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DInduction.sml377 (if is_imp(concl thm') (* recursive calls in this clause *)
458 (* A clause of the case_thm can have one of the following forms: *)
464 (* the clause. The reason for this is that "proved_cases" needs to align *)
471 fun match_clause pat clause =
473 val (V,tm) = strip_exists clause
479 of ([],[]) => clause
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sml808 (* derive assum clause *)
822 val clause = case ind of value
824 val clause = prove(forall_goal, value
829 in clause end
833 val clause = prove(i |> concl |> rand, value
842 in clause end
845 val _ = add_assum_clause clause
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DfolMapping.sml429 val prettify_thm = (mlibThm.AXIOM o map prettify_formula o mlibThm.clause);
724 val hol_lits = map (fol_literal_to_hol parm) (clause fol_th)
737 val (sub, hol_lits') = f [] [] (zip (clause fol_th) hol_lits)
753 val (a, b) = partition (equal fl o fst) (zip (clause fth) hls)
785 val n = mlibUseful.index (equal fol_lit) (clause fol_th)
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DZ3_ProofReplay.sml88 The input clause (including "t") is really treated as a set of
91 its disjuncts may even be spread throughout the input clause).
93 in the input clause.
145 val clause = Thm.concl (List.hd thms) value
146 val clause_imp_t = prove_from_disj dict clause
148 Thm.MP (Thm.DISCH clause clause_imp_t) (List.hd thms)
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/
H A Dho_proverTools.sml65 datatype clause = CLAUSE of vars * literal list; type
67 datatype fact = FACT of clause * thm susp;
72 type clause_rule = clause -> (substitution * clause * rule) list;
79 (* Literal and clause operations. *)
256 (* Replace clause variables in a fact with fresh ones. *)
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DpolytypicLib.sml705 of SOME (var_list,clause) => raise (dexn ("The variables; " ^ xlist_to_string term_to_string var_list ^
706 " are free in the clause: " ^ term_to_string clause))
881 (* a) there can be no free variables in any clause except fni *)
889 (* a) there can be no free variables in any clause except fni *)
1016 fun conv clause =
1019 (op:: (strip_comb (rand (lhs (snd (strip_forall clause))))))
1023 clause
1189 fun is_double_term_target (scheme:translation_scheme) funcs clause term =
1199 (is_single_constructor scheme clause orels
[all...]
H A Dacl2encodeLib.sig120 (* a) Convert to clause form, using *)
H A DfunctionEncodeLib.sml1544 (* Returns a list of clause * thm where if: *)
1546 (* clause(i) = ``f (Ci x y z) a b c *)
1571 (* Converts a function defined using clause structure to use case *)
1588 (* The algorithm terminates if this clause does not have a free variable *)
1593 (* reflection of this clause and adds it to the list of missing calls. *)
2993 (* Converts a missing clause to a limit *)
3012 ("Missing clause: " ^ term_to_string missing ^
3020 (* Calculates the nested theorems required for a missing clause limit: *)
3179 (* Limit theorems: |- destructed clause ==> full clause *)
[all...]
/seL4-l4v-10.1.1/HOL4/src/meson/src/
H A DmesonLib.sml429 (* Insert new goal's negation in ancestor clause, given refinement. *)
609 (* Creation of tagged contrapositives from a HOL clause. *)
927 (* time if there is a proof based on the first support clause with similar *)
928 (* size. It would be easy to separate out the support-clause trying (and *)
/seL4-l4v-10.1.1/HOL4/src/1/
H A DPrim_rec.sml90 message = ("Failed to match LHSes in clause "^Int.toString cnum)}
437 fun clause (a,c) = mk_eq(list_mk_comb(v,c::arg_list), function
440 list_mk_conj (ListPair.map clause (arg_list, clist))
1285 fun mk_clause clause =
1286 let val (lhs,rhs) = (dest_eq o #2 o strip_forall) clause
1791 fun clause n = let
1800 val clauses = sepby " | " (List.tabulate(n, clause))
H A DPmatch.sml61 * clause in a function definition.
751 val clause_s = if new_rows = 1 then " clause " else " clauses "
/seL4-l4v-10.1.1/HOL4/src/pfl/
H A Dindex.sml435 let fun fn_of clause = fst(strip_comb(lhs(snd(strip_forall clause))))
/seL4-l4v-10.1.1/isabelle/src/Doc/
H A Dpreface.tex32 An inference rule in Isabelle is a generalized Horn clause. Rules are
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/
H A Dpreface.tex32 An inference rule in Isabelle is a generalized Horn clause. Rules are

Completed in 232 milliseconds

123456