src/HOL/Tools/set_comprehension_pointfree.ML
changeset 50031 d12b3a270a62
parent 50030 349f651ec203
child 50032 a439a9d14ba3
equal deleted inserted replaced
50030:349f651ec203 50031:d12b3a270a62
   287     val conjs' = filter_out (fn t => eq = t) conjs
   287     val conjs' = filter_out (fn t => eq = t) conjs
   288     val unused_bounds = subtract (op =) (distinct (op =) (maps loose_bnos conjs'))
   288     val unused_bounds = subtract (op =) (distinct (op =) (maps loose_bnos conjs'))
   289       (0 upto (length vs - 1))
   289       (0 upto (length vs - 1))
   290     val (pats, fm) =
   290     val (pats, fm) =
   291       mk_formula ((x, T) :: vs) (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds))
   291       mk_formula ((x, T) :: vs) (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds))
   292     fun mk_set (Atom pt) = (case map (lookup pt) pats of [t'] => t' | ts => foldr1 mk_sigma ts)
   292     fun mk_set (Atom pt) = foldr1 mk_sigma (map (lookup pt) pats)
   293       | mk_set (Un (f1, f2)) = mk_sup (mk_set f1, mk_set f2)
   293       | mk_set (Un (f1, f2)) = mk_sup (mk_set f1, mk_set f2)
   294       | mk_set (Int (f1, f2)) = mk_inf (mk_set f1, mk_set f2)
   294       | mk_set (Int (f1, f2)) = mk_inf (mk_set f1, mk_set f2)
   295     val pat = foldr1 (mk_prod1 Ts) (map (term_of_pattern Ts) pats)
   295     val pat = foldr1 (mk_prod1 Ts) (map (term_of_pattern Ts) pats)
   296     val t = mk_split_abs (rev ((x, T) :: vs)) pat (reorder_bounds pats f)
   296     val t = mk_split_abs (rev ((x, T) :: vs)) pat (reorder_bounds pats f)
   297   in
   297   in