74 map_filter |
74 map_filter |
75 (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty)))) |
75 (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty)))) |
76 | _ => NONE) cos; |
76 | _ => NONE) cos; |
77 fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) = |
77 fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) = |
78 trueprop $ (equiv $ mk_eq (t1, t2) $ rhs); |
78 trueprop $ (equiv $ mk_eq (t1, t2) $ rhs); |
79 val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index); |
79 val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr]) index); |
80 fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) = |
80 fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) = |
81 [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)]; |
81 [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)]; |
82 val distincts = |
82 val distincts = |
83 maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index)); |
83 maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr]) index)); |
84 val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty))); |
84 val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty))); |
85 val simpset = |
85 val simpset = |
86 Simplifier.global_context thy |
86 Simplifier.global_context thy |
87 (HOL_basic_ss addsimps |
87 (HOL_basic_ss addsimps |
88 (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms))); |
88 (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms))); |