Searched refs:rule (Results 1 - 25 of 318) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DRule.sig104 (* A rule takes one theorem and either deduces another or raises an Error *)
108 type rule = Thm.thm -> Thm.thm type
110 val allRule : rule
112 val noRule : rule
114 val thenRule : rule -> rule -> rule
116 val orelseRule : rule -> rule -> rule
[all...]
H A DRewrite.sig68 rewrite -> reductionOrder -> LiteralSet.set -> Rule.rule
70 val rewriteRule : rewrite -> reductionOrder -> Rule.rule
77 rewrite -> reductionOrder -> equationId -> LiteralSet.set -> Rule.rule
79 val rewriteIdRule : rewrite -> reductionOrder -> equationId -> Rule.rule
92 (* Rewriting as a derived rule. *)
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DRule.sig104 (* A rule takes one theorem and either deduces another or raises an Error *)
108 type rule = Thm.thm -> Thm.thm type
110 val allRule : rule
112 val noRule : rule
114 val thenRule : rule -> rule -> rule
116 val orelseRule : rule -> rule -> rule
[all...]
H A DRewrite.sig68 rewrite -> reductionOrder -> LiteralSet.set -> Rule.rule
70 val rewriteRule : rewrite -> reductionOrder -> Rule.rule
77 rewrite -> reductionOrder -> equationId -> LiteralSet.set -> Rule.rule
79 val rewriteIdRule : rewrite -> reductionOrder -> equationId -> Rule.rule
92 (* Rewriting as a derived rule. *)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/
H A DhelperLib.sig21 val RW : thm list -> rule
22 val RW1 : thm list -> rule
91 val BASIC_SEP_REWRITE_RULE : thm -> rule
92 val EXISTS_PRE : term frag list -> rule
93 val EXISTS_SEP_REWRITE_RULE : thm -> rule
94 val HIDE_POST_RULE : term -> rule
95 val HIDE_PRE_RULE : term -> rule
96 val HIDE_PRE_STATUS_RULE : thm -> rule
97 val HIDE_STATUS_RULE : bool -> thm -> rule
98 val INST_SPEC : thm -> rule
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/prog/
H A Dm0_progLib.sig7 val m0_introduction: Drule.rule
11 val memory_introduction: Drule.rule
13 val register_introduction: Drule.rule
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DutilsLib.sig8 val ALL_HYP_CONV_RULE: conv -> rule
9 val ALL_HYP_RULE: rule -> rule
13 val ELIM_UNDISCH: rule
16 val HYP_CANON_RULE: rule
17 val HYP_CONV_RULE: conv -> term -> rule
18 val HYP_RULE: (thm -> thm) -> term -> rule
21 val INST_REWRITE_RULE: thm list -> rule
22 val LIST_DISCH: term list -> rule
23 val MATCH_HYP_CONV_RULE: conv -> term -> rule
[all...]
H A DstateLib.sig6 val chunks_intro: bool -> thm -> rule
7 val chunks_intro_pre_process: thm -> rule
18 val introduce_triple_definition: bool * thm -> rule
19 val introduce_map_definition: thm * conv -> rule
28 val pick_endian_rule: (term -> bool) * rule * rule -> rule
38 val sep_array_intro: bool -> thm -> thm list -> rule
62 val MOVE_COND_RULE: term -> rule
H A Dspec_databaseLib.sig7 (''a -> ''a -> Drule.rule) -> (Thm.thm -> Term.term) ->
/seL4-l4v-10.1.1/HOL4/src/n-bit/
H A DblastLib.sig6 val BBLAST_RULE : Conv.rule
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/
H A Dcore.sml29 { rule : rule,
34 val eqItem = fn (ITEM{rule=RULE{num=n,...},dot=d,...},
35 ITEM{rule=RULE{num=m,...},dot=e,...}) =>
38 val gtItem = fn (ITEM{rule=RULE{num=n,...},dot=d,...},
39 ITEM{rule=RULE{num=m,...},dot=e,...}) =>
68 in fn (ITEM {rule=RULE {lhs,rhs,rulenum,num,...},
72 of nil => (print " (reduce by rule ";
H A Dlalr.sml114 (* look_pos: position in the rhs of a rule at which we should start placing
123 (* rule_pos: calculate place in the rhs of a rule at which we should start
133 rule has proven to be nullable so far.
155 val check_rule = fn (rule as RULE {num,...}) =>
156 let val pos = rule_pos rule
158 prRule rule;
162 update(positions,num,rule_pos rule))
171 fn (ITEM{rule,dot, rhsAfter=NONTERM _ :: _}) =>
172 dot >= (look_pos rule)
189 map (fn rule
[all...]
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/
H A DformalizeUseful.sig204 type rule = thm -> thm type
298 val THENR : rule * rule -> rule
299 val REPEATR : rule -> rule
300 val ORELSER : rule * rule -> rule
301 val TRYR : rule
[all...]
H A DsubtypeUseful.sig205 type rule = thm -> thm type
299 val THENR : rule * rule -> rule
300 val REPEATR : rule -> rule
301 val ORELSER : rule * rule -> rule
302 val TRYR : rule
[all...]
/seL4-l4v-10.1.1/HOL4/examples/miller/useful/
H A DHurdUseful.sig201 type rule = thm -> thm type
294 val THENR : rule * rule -> rule
295 val REPEATR : rule -> rule
296 val ORELSER : rule * rule -> rule
297 val TRYR : rule
[all...]
/seL4-l4v-10.1.1/HOL4/src/floating-point/
H A Dlift_machine_ieeeScript.sml16 val rule = value
133 rule fp16_float_add_relative)
136 rule fp16_float_sub_relative)
139 rule fp16_float_mul_relative)
142 rule fp16_float_mul_add_relative)
145 rule fp16_float_mul_sub_relative)
148 rule fp16_float_div_relative)
151 rule fp16_float_sqrt_relative)
237 rule fp32_float_add_relative)
240 rule fp32_float_sub_relativ
[all...]
/seL4-l4v-10.1.1/HOL4/src/list/src/
H A DnumposrepLib.sml17 val rule = simpLib.SIMP_RULE numLib.std_ss [] value
19 fun l2n_pow2 i = rule (Thm.SPEC (f i) thm)
20 fun n2l_pow2 i = rule (Thm.SPEC (f i) n2l_pow2_compute)
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/
H A Dres_quanLib.sig59 val RESQ_HALF_SPEC : term -> rule
60 val RESQ_HALF_SPECL : term list -> rule
61 val RESQ_SPEC : term -> rule
62 val RESQ_SPECL : term list -> rule
106 val Q_RESQ_HALF_SPEC : term quotation -> rule
107 val Q_RESQ_HALF_SPECL : term quotation list -> rule
108 val Q_RESQ_SPEC : term quotation -> rule
109 val Q_RESQ_SPECL : term quotation list -> rule
110 val Q_RESQ_HALF_ISPEC : term quotation -> rule
111 val Q_RESQ_HALF_ISPECL : term quotation list -> rule
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A DpatternMatch.sml44 | Leaf of rule_type list (* a single rule *)
67 fun relevant_indices(test_set, rule) =
72 (index = fst rule) andalso
73 not (match_constr (List.nth(snd rule, index), name))) test_list
95 (* Eliminate redundant rules in a rule list. *)
130 (* Modify the rule by instantializing it with constructor information. *)
133 fun inst_rule (rule : rule_type, index, subterm) =
134 (#1(rule), List.take(#2 rule, index) @ [subterm] @ List.drop(#2 rule, inde
[all...]
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/
H A Dind_rel.sig1 (* Subject: Mutually recursive rule induction *)
11 Term.term list (* each term corresponds to a quantified rule *)
/seL4-l4v-10.1.1/HOL4/examples/MLsyntax/
H A DMLScript.sml39 * match ::= <rule> *
40 * | <rule> "|" <match> *
42 * rule ::= <pat> "=>" <exp> *
85 match = match rule
86 | matchl rule match ;
88 rule = rule pat exp ;
119 (ruleV (rule p e) = (patV p) UNION (expV e))
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/prog/
H A Darm_progLib.sig10 val change_config_rule: Drule.rule
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/
H A DarmLib.sig17 val UNABBREV_RULE : term frag list -> rule
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A DarmLib.sig15 val UNABBREV_RULE : term frag list -> rule
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/examples/
H A Dvar_example.sml29 [{name = "match", arg_info = [being_defined "rule"]},
30 {name = "match_list", arg_info = [being_defined "rule",
32 {type_name = "rule",
34 [{name = "rule", arg_info = [being_defined "pat",
90 (ruleV (rule p e) = (patV p) UNION (expV e))

Completed in 94 milliseconds

1234567891011>>