adding an executable THE operator on finite types
authorbulwahn
Mon Dec 13 08:51:52 2010 +0100 (2010-12-13)
changeset 411152c362ff5daf4
parent 41114 f9ae7c2abf7e
child 41116 7230a7c379dc
adding an executable THE operator on finite types
src/HOL/Enum.thy
     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