src/HOL/Enum.thy
 changeset 41115 2c362ff5daf4 parent 41085 a549ff1d4070 child 45117 3911cf09899a
equal inserted replaced
41114:f9ae7c2abf7e 41115:2c362ff5daf4
`   722     by (auto, case_tac x) auto`
`   722     by (auto, case_tac x) auto`
`   723 qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)`
`   723 qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)`
`   724 `
`   724 `
`   725 end`
`   725 end`
`   726 `
`   726 `
`       `
`   727 subsection {* An executable THE operator on finite types *}`
`       `
`   728 `
`       `
`   729 definition`
`       `
`   730   [code del]: "enum_the P = The P"`
`       `
`   731 `
`       `
`   732 lemma [code]:`
`       `
`   733   "The P = (case filter P enum of [x] => x | _ => enum_the P)"`
`       `
`   734 proof -`
`       `
`   735   {`
`       `
`   736     fix a`
`       `
`   737     assume filter_enum: "filter P enum = [a]"`
`       `
`   738     have "The P = a"`
`       `
`   739     proof (rule the_equality)`
`       `
`   740       fix x`
`       `
`   741       assume "P x"`
`       `
`   742       show "x = a"`
`       `
`   743       proof (rule ccontr)`
`       `
`   744         assume "x \<noteq> a"`
`       `
`   745         from filter_enum obtain us vs`
`       `
`   746           where enum_eq: "enum = us @ [a] @ vs"`
`       `
`   747           and "\<forall> x \<in> set us. \<not> P x"`
`       `
`   748           and "\<forall> x \<in> set vs. \<not> P x"`
`       `
`   749           and "P a"`
`       `
`   750           by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric])`
`       `
`   751         with `P x` in_enum[of x, unfolded enum_eq] `x \<noteq> a` show "False" by auto`
`       `
`   752       qed`
`       `
`   753     next`
`       `
`   754       from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff)`
`       `
`   755     qed`
`       `
`   756   }`
`       `
`   757   from this show ?thesis`
`       `
`   758     unfolding enum_the_def by (auto split: list.split)`
`       `
`   759 qed`
`       `
`   760 `
`       `
`   761 code_abort enum_the`
`       `
`   762 `
`   727 hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5`
`   763 hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5`
`   728 `
`   764 `
`   729 `
`   765 `
`   730 hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5`
`   766 hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5`
`   731 hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product`
`   767 hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product`