src/quantHeuristics/quantHeuristicsLibSimple.sml

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