haftmann@31596: (* Author: Florian Haftmann, TU Muenchen *) haftmann@26348: haftmann@26348: header {* Finite types as explicit enumerations *} haftmann@26348: haftmann@26348: theory Enum haftmann@49972: imports Map haftmann@26348: begin haftmann@26348: haftmann@26348: subsection {* Class @{text enum} *} haftmann@26348: haftmann@29797: class enum = haftmann@26348: fixes enum :: "'a list" bulwahn@41078: fixes enum_all :: "('a \ bool) \ bool" haftmann@49950: fixes enum_ex :: "('a \ bool) \ bool" haftmann@33635: assumes UNIV_enum: "UNIV = set enum" haftmann@26444: and enum_distinct: "distinct enum" haftmann@49950: assumes enum_all_UNIV: "enum_all P \ Ball UNIV P" haftmann@49950: assumes enum_ex_UNIV: "enum_ex P \ Bex UNIV P" haftmann@49950: -- {* tailored towards simple instantiation *} haftmann@26348: begin haftmann@26348: haftmann@29797: subclass finite proof haftmann@29797: qed (simp add: UNIV_enum) haftmann@26444: haftmann@49950: lemma enum_UNIV: haftmann@49950: "set enum = UNIV" haftmann@49950: by (simp only: UNIV_enum) haftmann@26444: bulwahn@40683: lemma in_enum: "x \ set enum" haftmann@49950: by (simp add: enum_UNIV) haftmann@26348: haftmann@26348: lemma enum_eq_I: haftmann@26348: assumes "\x. x \ set xs" haftmann@26348: shows "set enum = set xs" haftmann@26348: proof - haftmann@26348: from assms UNIV_eq_I have "UNIV = set xs" by auto bulwahn@41078: with enum_UNIV show ?thesis by simp haftmann@26348: qed haftmann@26348: haftmann@49972: lemma card_UNIV_length_enum: haftmann@49972: "card (UNIV :: 'a set) = length enum" haftmann@49972: by (simp add: UNIV_enum distinct_card enum_distinct) haftmann@49972: haftmann@49950: lemma enum_all [simp]: haftmann@49950: "enum_all = HOL.All" haftmann@49950: by (simp add: fun_eq_iff enum_all_UNIV) haftmann@49950: haftmann@49950: lemma enum_ex [simp]: haftmann@49950: "enum_ex = HOL.Ex" haftmann@49950: by (simp add: fun_eq_iff enum_ex_UNIV) haftmann@49950: haftmann@26348: end haftmann@26348: haftmann@26348: haftmann@49949: subsection {* Implementations using @{class enum} *} haftmann@49949: haftmann@49949: subsubsection {* Unbounded operations and quantifiers *} haftmann@49949: haftmann@49949: lemma Collect_code [code]: haftmann@49949: "Collect P = set (filter P enum)" haftmann@49950: by (simp add: enum_UNIV) haftmann@49949: bulwahn@50567: lemma vimage_code [code]: bulwahn@50567: "f -` B = set (filter (%x. f x : B) enum_class.enum)" bulwahn@50567: unfolding vimage_def Collect_code .. bulwahn@50567: haftmann@49949: definition card_UNIV :: "'a itself \ nat" haftmann@49949: where haftmann@49949: [code del]: "card_UNIV TYPE('a) = card (UNIV :: 'a set)" haftmann@49949: haftmann@49949: lemma [code]: haftmann@49949: "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))" haftmann@49949: by (simp only: card_UNIV_def enum_UNIV) haftmann@49949: haftmann@49949: lemma all_code [code]: "(\x. P x) \ enum_all P" haftmann@49950: by simp haftmann@49949: haftmann@49949: lemma exists_code [code]: "(\x. P x) \ enum_ex P" haftmann@49950: by simp haftmann@49949: haftmann@49949: lemma exists1_code [code]: "(\!x. P x) \ list_ex1 P enum" haftmann@49950: by (auto simp add: list_ex1_iff enum_UNIV) haftmann@49949: haftmann@49949: haftmann@49949: subsubsection {* An executable choice operator *} haftmann@49949: haftmann@49949: definition haftmann@49949: [code del]: "enum_the = The" haftmann@49949: haftmann@49949: lemma [code]: haftmann@49949: "The P = (case filter P enum of [x] => x | _ => enum_the P)" haftmann@49949: proof - haftmann@49949: { haftmann@49949: fix a haftmann@49949: assume filter_enum: "filter P enum = [a]" haftmann@49949: have "The P = a" haftmann@49949: proof (rule the_equality) haftmann@49949: fix x haftmann@49949: assume "P x" haftmann@49949: show "x = a" haftmann@49949: proof (rule ccontr) haftmann@49949: assume "x \ a" haftmann@49949: from filter_enum obtain us vs haftmann@49949: where enum_eq: "enum = us @ [a] @ vs" haftmann@49949: and "\ x \ set us. \ P x" haftmann@49949: and "\ x \ set vs. \ P x" haftmann@49949: and "P a" haftmann@49949: by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric]) haftmann@49949: with `P x` in_enum[of x, unfolded enum_eq] `x \ a` show "False" by auto haftmann@49949: qed haftmann@49949: next haftmann@49949: from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff) haftmann@49949: qed haftmann@49949: } haftmann@49949: from this show ?thesis haftmann@49949: unfolding enum_the_def by (auto split: list.split) haftmann@49949: qed haftmann@49949: haftmann@54890: declare [[code abort: enum_the]] haftmann@52435: haftmann@52435: code_printing haftmann@52435: constant enum_the \ (Eval) "(fn '_ => raise Match)" haftmann@49949: haftmann@49949: haftmann@49949: subsubsection {* Equality and order on functions *} haftmann@26348: haftmann@38857: instantiation "fun" :: (enum, equal) equal haftmann@26513: begin haftmann@26348: haftmann@26513: definition haftmann@38857: "HOL.equal f g \ (\x \ set enum. f x = g x)" haftmann@26513: haftmann@31464: instance proof haftmann@49950: qed (simp_all add: equal_fun_def fun_eq_iff enum_UNIV) haftmann@26513: haftmann@26513: end haftmann@26348: bulwahn@40898: lemma [code]: bulwahn@41078: "HOL.equal f g \ enum_all (%x. f x = g x)" haftmann@49950: by (auto simp add: equal fun_eq_iff) bulwahn@40898: haftmann@38857: lemma [code nbe]: haftmann@38857: "HOL.equal (f :: _ \ _) f \ True" haftmann@38857: by (fact equal_refl) haftmann@38857: haftmann@28562: lemma order_fun [code]: haftmann@26348: fixes f g :: "'a\enum \ 'b\order" bulwahn@41078: shows "f \ g \ enum_all (\x. f x \ g x)" bulwahn@41078: and "f < g \ f \ g \ enum_ex (\x. f x \ g x)" haftmann@49950: by (simp_all add: fun_eq_iff le_fun_def order_less_le) haftmann@26968: haftmann@26968: haftmann@49949: subsubsection {* Operations on relations *} haftmann@49949: haftmann@49949: lemma [code]: haftmann@49949: "Id = image (\x. (x, x)) (set Enum.enum)" haftmann@49949: by (auto intro: imageI in_enum) haftmann@26968: blanchet@54148: lemma tranclp_unfold [code]: haftmann@49949: "tranclp r a b \ (a, b) \ trancl {(x, y). r x y}" haftmann@49949: by (simp add: trancl_def) haftmann@49949: blanchet@54148: lemma rtranclp_rtrancl_eq [code]: haftmann@49949: "rtranclp r x y \ (x, y) \ rtrancl {(x, y). r x y}" haftmann@49949: by (simp add: rtrancl_def) haftmann@26968: haftmann@49949: lemma max_ext_eq [code]: haftmann@49949: "max_ext R = {(X, Y). finite X \ finite Y \ Y \ {} \ (\x. x \ X \ (\xa \ Y. (x, xa) \ R))}" haftmann@49949: by (auto simp add: max_ext.simps) haftmann@49949: haftmann@49949: lemma max_extp_eq [code]: haftmann@49949: "max_extp r x y \ (x, y) \ max_ext {(x, y). r x y}" haftmann@49949: by (simp add: max_ext_def) haftmann@26348: haftmann@49949: lemma mlex_eq [code]: haftmann@49949: "f <*mlex*> R = {(x, y). f x < f y \ (f x \ f y \ (x, y) \ R)}" haftmann@49949: by (auto simp add: mlex_prod_def) haftmann@49949: blanchet@55088: blanchet@55088: subsubsection {* Bounded accessible part *} blanchet@55088: blanchet@55088: primrec bacc :: "('a \ 'a) set \ nat \ 'a set" blanchet@55088: where blanchet@55088: "bacc r 0 = {x. \ y. (y, x) \ r}" blanchet@55088: | "bacc r (Suc n) = (bacc r n \ {x. \y. (y, x) \ r \ y \ bacc r n})" blanchet@55088: blanchet@55088: lemma bacc_subseteq_acc: blanchet@55088: "bacc r n \ Wellfounded.acc r" blanchet@55088: by (induct n) (auto intro: acc.intros) blanchet@55088: blanchet@55088: lemma bacc_mono: blanchet@55088: "n \ m \ bacc r n \ bacc r m" blanchet@55088: by (induct rule: dec_induct) auto blanchet@55088: blanchet@55088: lemma bacc_upper_bound: blanchet@55088: "bacc (r :: ('a \ 'a) set) (card (UNIV :: 'a::finite set)) = (\n. bacc r n)" blanchet@55088: proof - blanchet@55088: have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono) blanchet@55088: moreover have "\n. bacc r n = bacc r (Suc n) \ bacc r (Suc n) = bacc r (Suc (Suc n))" by auto blanchet@55088: moreover have "finite (range (bacc r))" by auto blanchet@55088: ultimately show ?thesis blanchet@55088: by (intro finite_mono_strict_prefix_implies_finite_fixpoint) blanchet@55088: (auto intro: finite_mono_remains_stable_implies_strict_prefix) blanchet@55088: qed blanchet@55088: blanchet@55088: lemma acc_subseteq_bacc: blanchet@55088: assumes "finite r" blanchet@55088: shows "Wellfounded.acc r \ (\n. bacc r n)" blanchet@55088: proof blanchet@55088: fix x blanchet@55088: assume "x : Wellfounded.acc r" blanchet@55088: then have "\ n. x : bacc r n" blanchet@55088: proof (induct x arbitrary: rule: acc.induct) blanchet@55088: case (accI x) blanchet@55088: then have "\y. \ n. (y, x) \ r --> y : bacc r n" by simp blanchet@55088: from choice[OF this] obtain n where n: "\y. (y, x) \ r \ y \ bacc r (n y)" .. blanchet@55088: obtain n where "\y. (y, x) : r \ y : bacc r n" blanchet@55088: proof blanchet@55088: fix y assume y: "(y, x) : r" blanchet@55088: with n have "y : bacc r (n y)" by auto blanchet@55088: moreover have "n y <= Max ((%(y, x). n y) ` r)" blanchet@55088: using y `finite r` by (auto intro!: Max_ge) blanchet@55088: note bacc_mono[OF this, of r] blanchet@55088: ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto blanchet@55088: qed blanchet@55088: then show ?case blanchet@55088: by (auto simp add: Let_def intro!: exI[of _ "Suc n"]) blanchet@55088: qed blanchet@55088: then show "x : (UN n. bacc r n)" by auto blanchet@55088: qed blanchet@55088: blanchet@55088: lemma acc_bacc_eq: blanchet@55088: fixes A :: "('a :: finite \ 'a) set" blanchet@55088: assumes "finite A" blanchet@55088: shows "Wellfounded.acc A = bacc A (card (UNIV :: 'a set))" blanchet@55088: using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff) blanchet@55088: haftmann@49949: lemma [code]: haftmann@49949: fixes xs :: "('a::finite \ 'a) list" haftmann@54295: shows "Wellfounded.acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))" haftmann@49949: by (simp add: card_UNIV_def acc_bacc_eq) haftmann@49949: haftmann@26348: haftmann@49949: subsection {* Default instances for @{class enum} *} haftmann@26348: haftmann@26444: lemma map_of_zip_enum_is_Some: haftmann@26444: assumes "length ys = length (enum \ 'a\enum list)" haftmann@26444: shows "\y. map_of (zip (enum \ 'a\enum list) ys) x = Some y" haftmann@26444: proof - haftmann@26444: from assms have "x \ set (enum \ 'a\enum list) \ haftmann@26444: (\y. map_of (zip (enum \ 'a\enum list) ys) x = Some y)" haftmann@26444: by (auto intro!: map_of_zip_is_Some) bulwahn@41078: then show ?thesis using enum_UNIV by auto haftmann@26444: qed haftmann@26444: haftmann@26444: lemma map_of_zip_enum_inject: haftmann@26444: fixes xs ys :: "'b\enum list" haftmann@26444: assumes length: "length xs = length (enum \ 'a\enum list)" haftmann@26444: "length ys = length (enum \ 'a\enum list)" haftmann@26444: and map_of: "the \ map_of (zip (enum \ 'a\enum list) xs) = the \ map_of (zip (enum \ 'a\enum list) ys)" haftmann@26444: shows "xs = ys" haftmann@26444: proof - haftmann@26444: have "map_of (zip (enum \ 'a list) xs) = map_of (zip (enum \ 'a list) ys)" haftmann@26444: proof haftmann@26444: fix x :: 'a haftmann@26444: from length map_of_zip_enum_is_Some obtain y1 y2 haftmann@26444: where "map_of (zip (enum \ 'a list) xs) x = Some y1" haftmann@26444: and "map_of (zip (enum \ 'a list) ys) x = Some y2" by blast wenzelm@47230: moreover from map_of wenzelm@47230: have "the (map_of (zip (enum \ 'a\enum list) xs) x) = the (map_of (zip (enum \ 'a\enum list) ys) x)" haftmann@26444: by (auto dest: fun_cong) haftmann@26444: ultimately show "map_of (zip (enum \ 'a\enum list) xs) x = map_of (zip (enum \ 'a\enum list) ys) x" haftmann@26444: by simp haftmann@26444: qed haftmann@26444: with length enum_distinct show "xs = ys" by (rule map_of_zip_inject) haftmann@26444: qed haftmann@26444: haftmann@49950: definition all_n_lists :: "(('a :: enum) list \ bool) \ nat \ bool" bulwahn@41078: where haftmann@49950: "all_n_lists P n \ (\xs \ set (List.n_lists n enum). P xs)" bulwahn@41078: bulwahn@41078: lemma [code]: haftmann@49950: "all_n_lists P n \ (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))" haftmann@49950: unfolding all_n_lists_def enum_all haftmann@49950: by (cases n) (auto simp add: enum_UNIV) bulwahn@41078: haftmann@49950: definition ex_n_lists :: "(('a :: enum) list \ bool) \ nat \ bool" bulwahn@41078: where haftmann@49950: "ex_n_lists P n \ (\xs \ set (List.n_lists n enum). P xs)" bulwahn@41078: bulwahn@41078: lemma [code]: haftmann@49950: "ex_n_lists P n \ (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))" haftmann@49950: unfolding ex_n_lists_def enum_ex haftmann@49950: by (cases n) (auto simp add: enum_UNIV) bulwahn@41078: haftmann@26444: instantiation "fun" :: (enum, enum) enum haftmann@26444: begin haftmann@26444: haftmann@26444: definition haftmann@49948: "enum = map (\ys. the o map_of (zip (enum\'a list) ys)) (List.n_lists (length (enum\'a\enum list)) enum)" haftmann@26444: bulwahn@41078: definition bulwahn@41078: "enum_all P = all_n_lists (\bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))" bulwahn@41078: bulwahn@41078: definition bulwahn@41078: "enum_ex P = ex_n_lists (\bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))" bulwahn@41078: haftmann@26444: instance proof haftmann@26444: show "UNIV = set (enum \ ('a \ 'b) list)" haftmann@26444: proof (rule UNIV_eq_I) haftmann@26444: fix f :: "'a \ 'b" haftmann@26444: have "f = the \ map_of (zip (enum \ 'a\enum list) (map f enum))" bulwahn@40683: by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) haftmann@26444: then show "f \ set enum" bulwahn@40683: by (auto simp add: enum_fun_def set_n_lists intro: in_enum) haftmann@26444: qed haftmann@26444: next haftmann@26444: from map_of_zip_enum_inject haftmann@26444: show "distinct (enum \ ('a \ 'b) list)" haftmann@26444: by (auto intro!: inj_onI simp add: enum_fun_def haftmann@49950: distinct_map distinct_n_lists enum_distinct set_n_lists) bulwahn@41078: next bulwahn@41078: fix P haftmann@49950: show "enum_all (P :: ('a \ 'b) \ bool) = Ball UNIV P" bulwahn@41078: proof bulwahn@41078: assume "enum_all P" haftmann@49950: show "Ball UNIV P" bulwahn@41078: proof bulwahn@41078: fix f :: "'a \ 'b" bulwahn@41078: have f: "f = the \ map_of (zip (enum \ 'a\enum list) (map f enum))" bulwahn@41078: by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) bulwahn@41078: from `enum_all P` have "P (the \ map_of (zip enum (map f enum)))" bulwahn@41078: unfolding enum_all_fun_def all_n_lists_def bulwahn@41078: apply (simp add: set_n_lists) bulwahn@41078: apply (erule_tac x="map f enum" in allE) bulwahn@41078: apply (auto intro!: in_enum) bulwahn@41078: done bulwahn@41078: from this f show "P f" by auto bulwahn@41078: qed bulwahn@41078: next haftmann@49950: assume "Ball UNIV P" bulwahn@41078: from this show "enum_all P" bulwahn@41078: unfolding enum_all_fun_def all_n_lists_def by auto bulwahn@41078: qed bulwahn@41078: next bulwahn@41078: fix P haftmann@49950: show "enum_ex (P :: ('a \ 'b) \ bool) = Bex UNIV P" bulwahn@41078: proof bulwahn@41078: assume "enum_ex P" haftmann@49950: from this show "Bex UNIV P" bulwahn@41078: unfolding enum_ex_fun_def ex_n_lists_def by auto bulwahn@41078: next haftmann@49950: assume "Bex UNIV P" bulwahn@41078: from this obtain f where "P f" .. bulwahn@41078: have f: "f = the \ map_of (zip (enum \ 'a\enum list) (map f enum))" bulwahn@41078: by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) bulwahn@41078: from `P f` this have "P (the \ map_of (zip (enum \ 'a\enum list) (map f enum)))" bulwahn@41078: by auto bulwahn@41078: from this show "enum_ex P" bulwahn@41078: unfolding enum_ex_fun_def ex_n_lists_def bulwahn@41078: apply (auto simp add: set_n_lists) bulwahn@41078: apply (rule_tac x="map f enum" in exI) bulwahn@41078: apply (auto intro!: in_enum) bulwahn@41078: done bulwahn@41078: qed haftmann@26444: qed haftmann@26444: haftmann@26444: end haftmann@26444: haftmann@38857: lemma enum_fun_code [code]: "enum = (let enum_a = (enum \ 'a\{enum, equal} list) haftmann@49948: in map (\ys. the o map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))" haftmann@28245: by (simp add: enum_fun_def Let_def) haftmann@26444: bulwahn@41078: lemma enum_all_fun_code [code]: bulwahn@41078: "enum_all P = (let enum_a = (enum :: 'a::{enum, equal} list) bulwahn@41078: in all_n_lists (\bs. P (the o map_of (zip enum_a bs))) (length enum_a))" haftmann@49950: by (simp only: enum_all_fun_def Let_def) bulwahn@41078: bulwahn@41078: lemma enum_ex_fun_code [code]: bulwahn@41078: "enum_ex P = (let enum_a = (enum :: 'a::{enum, equal} list) bulwahn@41078: in ex_n_lists (\bs. P (the o map_of (zip enum_a bs))) (length enum_a))" haftmann@49950: by (simp only: enum_ex_fun_def Let_def) haftmann@45963: haftmann@45963: instantiation set :: (enum) enum haftmann@45963: begin haftmann@45963: haftmann@45963: definition haftmann@45963: "enum = map set (sublists enum)" haftmann@45963: haftmann@45963: definition haftmann@45963: "enum_all P \ (\A\set enum. P (A::'a set))" haftmann@45963: haftmann@45963: definition haftmann@45963: "enum_ex P \ (\A\set enum. P (A::'a set))" haftmann@45963: haftmann@45963: instance proof haftmann@45963: qed (simp_all add: enum_set_def enum_all_set_def enum_ex_set_def sublists_powset distinct_set_sublists haftmann@45963: enum_distinct enum_UNIV) huffman@29024: huffman@29024: end huffman@29024: haftmann@49950: instantiation unit :: enum haftmann@49950: begin haftmann@49950: haftmann@49950: definition haftmann@49950: "enum = [()]" haftmann@49950: haftmann@49950: definition haftmann@49950: "enum_all P = P ()" haftmann@49950: haftmann@49950: definition haftmann@49950: "enum_ex P = P ()" haftmann@49950: haftmann@49950: instance proof haftmann@49950: qed (auto simp add: enum_unit_def enum_all_unit_def enum_ex_unit_def) haftmann@49950: haftmann@49950: end haftmann@49950: haftmann@49950: instantiation bool :: enum haftmann@49950: begin haftmann@49950: haftmann@49950: definition haftmann@49950: "enum = [False, True]" haftmann@49950: haftmann@49950: definition haftmann@49950: "enum_all P \ P False \ P True" haftmann@49950: haftmann@49950: definition haftmann@49950: "enum_ex P \ P False \ P True" haftmann@49950: haftmann@49950: instance proof haftmann@49950: qed (simp_all only: enum_bool_def enum_all_bool_def enum_ex_bool_def UNIV_bool, simp_all) haftmann@49950: haftmann@49950: end haftmann@49950: haftmann@49950: instantiation prod :: (enum, enum) enum haftmann@49950: begin haftmann@49950: haftmann@49950: definition haftmann@49950: "enum = List.product enum enum" haftmann@49950: haftmann@49950: definition haftmann@49950: "enum_all P = enum_all (%x. enum_all (%y. P (x, y)))" haftmann@49950: haftmann@49950: definition haftmann@49950: "enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))" haftmann@49950: haftmann@49950: haftmann@49950: instance by default nipkow@57247: (simp_all add: enum_prod_def distinct_product haftmann@49950: enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def) haftmann@49950: haftmann@49950: end haftmann@49950: haftmann@49950: instantiation sum :: (enum, enum) enum haftmann@49950: begin haftmann@49950: haftmann@49950: definition haftmann@49950: "enum = map Inl enum @ map Inr enum" haftmann@49950: haftmann@49950: definition haftmann@49950: "enum_all P \ enum_all (\x. P (Inl x)) \ enum_all (\x. P (Inr x))" haftmann@49950: haftmann@49950: definition haftmann@49950: "enum_ex P \ enum_ex (\x. P (Inl x)) \ enum_ex (\x. P (Inr x))" haftmann@49950: haftmann@49950: instance proof haftmann@49950: qed (simp_all only: enum_sum_def enum_all_sum_def enum_ex_sum_def UNIV_sum, haftmann@49950: auto simp add: enum_UNIV distinct_map enum_distinct) haftmann@49950: haftmann@49950: end haftmann@49950: haftmann@49950: instantiation option :: (enum) enum haftmann@49950: begin haftmann@49950: haftmann@49950: definition haftmann@49950: "enum = None # map Some enum" haftmann@49950: haftmann@49950: definition haftmann@49950: "enum_all P \ P None \ enum_all (\x. P (Some x))" haftmann@49950: haftmann@49950: definition haftmann@49950: "enum_ex P \ P None \ enum_ex (\x. P (Some x))" haftmann@49950: haftmann@49950: instance proof haftmann@49950: qed (simp_all only: enum_option_def enum_all_option_def enum_ex_option_def UNIV_option_conv, haftmann@49950: auto simp add: distinct_map enum_UNIV enum_distinct) haftmann@49950: haftmann@49950: end haftmann@49950: haftmann@45963: bulwahn@40647: subsection {* Small finite types *} bulwahn@40647: bulwahn@40647: text {* We define small finite types for the use in Quickcheck *} bulwahn@40647: wenzelm@53015: datatype finite_1 = a\<^sub>1 bulwahn@40647: wenzelm@53015: notation (output) a\<^sub>1 ("a\<^sub>1") bulwahn@40900: haftmann@49950: lemma UNIV_finite_1: wenzelm@53015: "UNIV = {a\<^sub>1}" haftmann@49950: by (auto intro: finite_1.exhaust) haftmann@49950: bulwahn@40647: instantiation finite_1 :: enum bulwahn@40647: begin bulwahn@40647: bulwahn@40647: definition wenzelm@53015: "enum = [a\<^sub>1]" bulwahn@40647: bulwahn@41078: definition wenzelm@53015: "enum_all P = P a\<^sub>1" bulwahn@41078: bulwahn@41078: definition wenzelm@53015: "enum_ex P = P a\<^sub>1" bulwahn@41078: bulwahn@40647: instance proof haftmann@49950: qed (simp_all only: enum_finite_1_def enum_all_finite_1_def enum_ex_finite_1_def UNIV_finite_1, simp_all) bulwahn@40647: huffman@29024: end bulwahn@40647: bulwahn@40651: instantiation finite_1 :: linorder bulwahn@40651: begin bulwahn@40651: haftmann@49950: definition less_finite_1 :: "finite_1 \ finite_1 \ bool" haftmann@49950: where haftmann@49950: "x < (y :: finite_1) \ False" haftmann@49950: bulwahn@40651: definition less_eq_finite_1 :: "finite_1 \ finite_1 \ bool" bulwahn@40651: where haftmann@49950: "x \ (y :: finite_1) \ True" bulwahn@40651: bulwahn@40651: instance bulwahn@40651: apply (intro_classes) bulwahn@40651: apply (auto simp add: less_finite_1_def less_eq_finite_1_def) bulwahn@40651: apply (metis finite_1.exhaust) bulwahn@40651: done bulwahn@40651: bulwahn@40651: end bulwahn@40651: wenzelm@53015: hide_const (open) a\<^sub>1 bulwahn@40657: wenzelm@53015: datatype finite_2 = a\<^sub>1 | a\<^sub>2 bulwahn@40647: wenzelm@53015: notation (output) a\<^sub>1 ("a\<^sub>1") wenzelm@53015: notation (output) a\<^sub>2 ("a\<^sub>2") bulwahn@40900: haftmann@49950: lemma UNIV_finite_2: wenzelm@53015: "UNIV = {a\<^sub>1, a\<^sub>2}" haftmann@49950: by (auto intro: finite_2.exhaust) haftmann@49950: bulwahn@40647: instantiation finite_2 :: enum bulwahn@40647: begin bulwahn@40647: bulwahn@40647: definition wenzelm@53015: "enum = [a\<^sub>1, a\<^sub>2]" bulwahn@40647: bulwahn@41078: definition wenzelm@53015: "enum_all P \ P a\<^sub>1 \ P a\<^sub>2" bulwahn@41078: bulwahn@41078: definition wenzelm@53015: "enum_ex P \ P a\<^sub>1 \ P a\<^sub>2" bulwahn@41078: bulwahn@40647: instance proof haftmann@49950: qed (simp_all only: enum_finite_2_def enum_all_finite_2_def enum_ex_finite_2_def UNIV_finite_2, simp_all) bulwahn@40647: bulwahn@40647: end bulwahn@40647: bulwahn@40651: instantiation finite_2 :: linorder bulwahn@40651: begin bulwahn@40651: bulwahn@40651: definition less_finite_2 :: "finite_2 \ finite_2 \ bool" bulwahn@40651: where wenzelm@53015: "x < y \ x = a\<^sub>1 \ y = a\<^sub>2" bulwahn@40651: bulwahn@40651: definition less_eq_finite_2 :: "finite_2 \ finite_2 \ bool" bulwahn@40651: where haftmann@49950: "x \ y \ x = y \ x < (y :: finite_2)" bulwahn@40651: bulwahn@40651: instance bulwahn@40651: apply (intro_classes) bulwahn@40651: apply (auto simp add: less_finite_2_def less_eq_finite_2_def) haftmann@49950: apply (metis finite_2.nchotomy)+ bulwahn@40651: done bulwahn@40651: bulwahn@40651: end bulwahn@40651: wenzelm@53015: hide_const (open) a\<^sub>1 a\<^sub>2 bulwahn@40657: wenzelm@53015: datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 bulwahn@40647: wenzelm@53015: notation (output) a\<^sub>1 ("a\<^sub>1") wenzelm@53015: notation (output) a\<^sub>2 ("a\<^sub>2") wenzelm@53015: notation (output) a\<^sub>3 ("a\<^sub>3") bulwahn@40900: haftmann@49950: lemma UNIV_finite_3: wenzelm@53015: "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3}" haftmann@49950: by (auto intro: finite_3.exhaust) haftmann@49950: bulwahn@40647: instantiation finite_3 :: enum bulwahn@40647: begin bulwahn@40647: bulwahn@40647: definition wenzelm@53015: "enum = [a\<^sub>1, a\<^sub>2, a\<^sub>3]" bulwahn@40647: bulwahn@41078: definition wenzelm@53015: "enum_all P \ P a\<^sub>1 \ P a\<^sub>2 \ P a\<^sub>3" bulwahn@41078: bulwahn@41078: definition wenzelm@53015: "enum_ex P \ P a\<^sub>1 \ P a\<^sub>2 \ P a\<^sub>3" bulwahn@41078: bulwahn@40647: instance proof haftmann@49950: qed (simp_all only: enum_finite_3_def enum_all_finite_3_def enum_ex_finite_3_def UNIV_finite_3, simp_all) bulwahn@40647: bulwahn@40647: end bulwahn@40647: bulwahn@40651: instantiation finite_3 :: linorder bulwahn@40651: begin bulwahn@40651: bulwahn@40651: definition less_finite_3 :: "finite_3 \ finite_3 \ bool" bulwahn@40651: where wenzelm@53015: "x < y = (case x of a\<^sub>1 \ y \ a\<^sub>1 | a\<^sub>2 \ y = a\<^sub>3 | a\<^sub>3 \ False)" bulwahn@40651: bulwahn@40651: definition less_eq_finite_3 :: "finite_3 \ finite_3 \ bool" bulwahn@40651: where haftmann@49950: "x \ y \ x = y \ x < (y :: finite_3)" bulwahn@40651: bulwahn@40651: instance proof (intro_classes) bulwahn@40651: qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm) bulwahn@40651: bulwahn@40651: end bulwahn@40651: wenzelm@53015: hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 bulwahn@40657: wenzelm@53015: datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 bulwahn@40647: wenzelm@53015: notation (output) a\<^sub>1 ("a\<^sub>1") wenzelm@53015: notation (output) a\<^sub>2 ("a\<^sub>2") wenzelm@53015: notation (output) a\<^sub>3 ("a\<^sub>3") wenzelm@53015: notation (output) a\<^sub>4 ("a\<^sub>4") bulwahn@40900: haftmann@49950: lemma UNIV_finite_4: wenzelm@53015: "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4}" haftmann@49950: by (auto intro: finite_4.exhaust) haftmann@49950: bulwahn@40647: instantiation finite_4 :: enum bulwahn@40647: begin bulwahn@40647: bulwahn@40647: definition wenzelm@53015: "enum = [a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4]" bulwahn@40647: bulwahn@41078: definition wenzelm@53015: "enum_all P \ P a\<^sub>1 \ P a\<^sub>2 \ P a\<^sub>3 \ P a\<^sub>4" bulwahn@41078: bulwahn@41078: definition wenzelm@53015: "enum_ex P \ P a\<^sub>1 \ P a\<^sub>2 \ P a\<^sub>3 \ P a\<^sub>4" bulwahn@41078: bulwahn@40647: instance proof haftmann@49950: qed (simp_all only: enum_finite_4_def enum_all_finite_4_def enum_ex_finite_4_def UNIV_finite_4, simp_all) bulwahn@40647: bulwahn@40647: end bulwahn@40647: wenzelm@53015: hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 bulwahn@40651: bulwahn@40651: wenzelm@53015: datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5 bulwahn@40647: wenzelm@53015: notation (output) a\<^sub>1 ("a\<^sub>1") wenzelm@53015: notation (output) a\<^sub>2 ("a\<^sub>2") wenzelm@53015: notation (output) a\<^sub>3 ("a\<^sub>3") wenzelm@53015: notation (output) a\<^sub>4 ("a\<^sub>4") wenzelm@53015: notation (output) a\<^sub>5 ("a\<^sub>5") bulwahn@40900: haftmann@49950: lemma UNIV_finite_5: wenzelm@53015: "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4, a\<^sub>5}" haftmann@49950: by (auto intro: finite_5.exhaust) haftmann@49950: bulwahn@40647: instantiation finite_5 :: enum bulwahn@40647: begin bulwahn@40647: bulwahn@40647: definition wenzelm@53015: "enum = [a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4, a\<^sub>5]" bulwahn@40647: bulwahn@41078: definition wenzelm@53015: "enum_all P \ P a\<^sub>1 \ P a\<^sub>2 \ P a\<^sub>3 \ P a\<^sub>4 \ P a\<^sub>5" bulwahn@41078: bulwahn@41078: definition wenzelm@53015: "enum_ex P \ P a\<^sub>1 \ P a\<^sub>2 \ P a\<^sub>3 \ P a\<^sub>4 \ P a\<^sub>5" bulwahn@41078: bulwahn@40647: instance proof haftmann@49950: qed (simp_all only: enum_finite_5_def enum_all_finite_5_def enum_ex_finite_5_def UNIV_finite_5, simp_all) bulwahn@40647: bulwahn@40647: end bulwahn@40647: wenzelm@53015: hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 a\<^sub>5 bulwahn@46352: haftmann@49948: bulwahn@46352: subsection {* Closing up *} bulwahn@40657: bulwahn@41085: hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5 haftmann@49948: hide_const (open) enum enum_all enum_ex all_n_lists ex_n_lists ntrancl bulwahn@40647: bulwahn@40647: end