src/HOL/Enum.thy
changeset 41115 2c362ff5daf4
parent 41085 a549ff1d4070
child 45117 3911cf09899a
equal deleted 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