equal
deleted
inserted
replaced
491 |
491 |
492 subsection {* Small finite types *} |
492 subsection {* Small finite types *} |
493 |
493 |
494 text {* We define small finite types for use in Quickcheck *} |
494 text {* We define small finite types for use in Quickcheck *} |
495 |
495 |
496 datatype (plugins only: code "quickcheck*" extraction) finite_1 = |
496 datatype (plugins only: code "quickcheck" extraction) finite_1 = |
497 a\<^sub>1 |
497 a\<^sub>1 |
498 |
498 |
499 notation (output) a\<^sub>1 ("a\<^sub>1") |
499 notation (output) a\<^sub>1 ("a\<^sub>1") |
500 |
500 |
501 lemma UNIV_finite_1: |
501 lemma UNIV_finite_1: |
594 end |
594 end |
595 |
595 |
596 declare [[simproc del: finite_1_eq]] |
596 declare [[simproc del: finite_1_eq]] |
597 hide_const (open) a\<^sub>1 |
597 hide_const (open) a\<^sub>1 |
598 |
598 |
599 datatype (plugins only: code "quickcheck*" extraction) finite_2 = |
599 datatype (plugins only: code "quickcheck" extraction) finite_2 = |
600 a\<^sub>1 | a\<^sub>2 |
600 a\<^sub>1 | a\<^sub>2 |
601 |
601 |
602 notation (output) a\<^sub>1 ("a\<^sub>1") |
602 notation (output) a\<^sub>1 ("a\<^sub>1") |
603 notation (output) a\<^sub>2 ("a\<^sub>2") |
603 notation (output) a\<^sub>2 ("a\<^sub>2") |
604 |
604 |
709 by intro_classes (simp_all add: mod_finite_2_def split: finite_2.splits) |
709 by intro_classes (simp_all add: mod_finite_2_def split: finite_2.splits) |
710 |
710 |
711 |
711 |
712 hide_const (open) a\<^sub>1 a\<^sub>2 |
712 hide_const (open) a\<^sub>1 a\<^sub>2 |
713 |
713 |
714 datatype (plugins only: code "quickcheck*" extraction) finite_3 = |
714 datatype (plugins only: code "quickcheck" extraction) finite_3 = |
715 a\<^sub>1 | a\<^sub>2 | a\<^sub>3 |
715 a\<^sub>1 | a\<^sub>2 | a\<^sub>3 |
716 |
716 |
717 notation (output) a\<^sub>1 ("a\<^sub>1") |
717 notation (output) a\<^sub>1 ("a\<^sub>1") |
718 notation (output) a\<^sub>2 ("a\<^sub>2") |
718 notation (output) a\<^sub>2 ("a\<^sub>2") |
719 notation (output) a\<^sub>3 ("a\<^sub>3") |
719 notation (output) a\<^sub>3 ("a\<^sub>3") |
836 |
836 |
837 |
837 |
838 |
838 |
839 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 |
839 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 |
840 |
840 |
841 datatype (plugins only: code "quickcheck*" extraction) finite_4 = |
841 datatype (plugins only: code "quickcheck" extraction) finite_4 = |
842 a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 |
842 a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 |
843 |
843 |
844 notation (output) a\<^sub>1 ("a\<^sub>1") |
844 notation (output) a\<^sub>1 ("a\<^sub>1") |
845 notation (output) a\<^sub>2 ("a\<^sub>2") |
845 notation (output) a\<^sub>2 ("a\<^sub>2") |
846 notation (output) a\<^sub>3 ("a\<^sub>3") |
846 notation (output) a\<^sub>3 ("a\<^sub>3") |
938 (simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def split: finite_4.splits) |
938 (simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def split: finite_4.splits) |
939 end |
939 end |
940 |
940 |
941 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 |
941 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 |
942 |
942 |
943 datatype (plugins only: code "quickcheck*" extraction) finite_5 = |
943 datatype (plugins only: code "quickcheck" extraction) finite_5 = |
944 a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5 |
944 a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5 |
945 |
945 |
946 notation (output) a\<^sub>1 ("a\<^sub>1") |
946 notation (output) a\<^sub>1 ("a\<^sub>1") |
947 notation (output) a\<^sub>2 ("a\<^sub>2") |
947 notation (output) a\<^sub>2 ("a\<^sub>2") |
948 notation (output) a\<^sub>3 ("a\<^sub>3") |
948 notation (output) a\<^sub>3 ("a\<^sub>3") |