Lines Matching defs:avoid
37 term set -> (* vars to avoid *)
53 fun not_uses_avoid_vars avoid tm = let
55 val s2 = HOLset.intersection (s1, avoid)
91 fun sgsfwc_eq_var sys avoid sgty_forall v tm = failwith "sgsfwc_eq_var: only works for exists"
92 | sgsfwc_eq_var sys avoid sgty_exists v tm = (
98 fun sgsfwc_eq (sys : simple_guess_search_fun) avoid sgty_forall v tm =
100 | sgsfwc_eq sys avoid sgty_exists v tm = let
102 if (aconv v tm1) andalso not_uses_avoid_vars avoid tm2 then
104 else if (aconv v tm2) andalso not_uses_avoid_vars avoid tm1 then
109 fun sgsfwc_neg (sys : simple_guess_search_fun) avoid sgty v tm =
115 val g = sys avoid sgty' v tm'
118 fun sgsfwc_and (sys : simple_guess_search_fun) avoid sgty_forall v tm =
120 | sgsfwc_and sys avoid sgty_exists v tm = let
123 val g1 = sys avoid sgty_exists v tm1
127 val g2 = sys avoid sgty_exists v tm2
132 fun sgsfwc_or (sys : simple_guess_search_fun) avoid sgty_exists v tm =
134 | sgsfwc_or sys avoid sgty_forall v tm = let
137 val g1 = sys avoid sgty_forall v tm1
141 val g2 = sys avoid sgty_forall v tm2
146 fun sgsfwc_imp (sys : simple_guess_search_fun) avoid sgty_exists v tm =
148 | sgsfwc_imp sys avoid sgty_forall v tm = let
151 val g1 = sys avoid sgty_exists v tm1
155 val g2 = sys avoid sgty_forall v tm2
160 fun sgsfwc_forall (sys : simple_guess_search_fun) avoid sgty v tm =
163 val avoid' = HOLset.add (avoid, v')
164 val g0 = sys avoid' sgty v tm'
173 fun sgsfwc_exists (sys : simple_guess_search_fun) avoid sgty v tm =
176 val avoid' = HOLset.add (avoid, v')
177 val g0 = sys avoid' sgty v tm'
187 fun sgsfwc_eq_fun_aux (sys : simple_guess_search_fun) avoid v (tm1, tm2) (f, cond, rewr) =
199 val g = sys avoid sgty_exists v tm''
205 fun sgsfwc_eq_fun l (sys : simple_guess_search_fun) avoid sgty_forall v tm =
207 | sgsfwc_eq_fun l (sys : simple_guess_search_fun) avoid sgty_exists v tm =
211 tryfind (sgsfwc_eq_fun_aux sys avoid v (tm1, tm2)) l
225 avoid ty v tm =
226 Lib.tryfind (fn wc => wc (combine_sgsfwcs wc_l) avoid ty v tm) wc_l
253 val avoid = HOLset.singleton Term.compare v
254 val guess = combine_sgsfwcs wcl avoid sgty_exists v b_tm
274 val avoid = HOLset.singleton Term.compare v
275 val guess = combine_sgsfwcs wcl avoid sgty_forall v b_tm
288 val avoid = HOLset.singleton Term.compare v
289 val guess = combine_sgsfwcs wcl avoid sgty_exists v b_tm
301 val avoid = HOLset.singleton Term.compare v
302 val guess = combine_sgsfwcs wcl avoid sgty_exists v b_tm
314 val avoid = HOLset.singleton Term.compare v
315 val guess = combine_sgsfwcs wcl avoid sgty_exists v b_tm