src/HOL/Enum.thy
 changeset 41115 2c362ff5daf4 parent 41085 a549ff1d4070 child 45117 3911cf09899a
```     1.1 --- a/src/HOL/Enum.thy	Sun Dec 12 21:41:01 2010 +0100
1.2 +++ b/src/HOL/Enum.thy	Mon Dec 13 08:51:52 2010 +0100
1.3 @@ -724,6 +724,42 @@
1.4
1.5  end
1.6
1.7 +subsection {* An executable THE operator on finite types *}
1.8 +
1.9 +definition
1.10 +  [code del]: "enum_the P = The P"
1.11 +
1.12 +lemma [code]:
1.13 +  "The P = (case filter P enum of [x] => x | _ => enum_the P)"
1.14 +proof -
1.15 +  {
1.16 +    fix a
1.17 +    assume filter_enum: "filter P enum = [a]"
1.18 +    have "The P = a"
1.19 +    proof (rule the_equality)
1.20 +      fix x
1.21 +      assume "P x"
1.22 +      show "x = a"
1.23 +      proof (rule ccontr)
1.24 +        assume "x \<noteq> a"
1.25 +        from filter_enum obtain us vs
1.26 +          where enum_eq: "enum = us @ [a] @ vs"
1.27 +          and "\<forall> x \<in> set us. \<not> P x"
1.28 +          and "\<forall> x \<in> set vs. \<not> P x"
1.29 +          and "P a"
1.30 +          by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric])
1.31 +        with `P x` in_enum[of x, unfolded enum_eq] `x \<noteq> a` show "False" by auto
1.32 +      qed
1.33 +    next
1.34 +      from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff)
1.35 +    qed
1.36 +  }
1.37 +  from this show ?thesis
1.38 +    unfolding enum_the_def by (auto split: list.split)
1.39 +qed
1.40 +
1.41 +code_abort enum_the
1.42 +
1.43  hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
1.44
1.45
```