summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 09 Aug 2005 11:44:38 +0200 | |

changeset 17040 | 6682c93b7d9f |

parent 17039 | 78159411623f |

child 17041 | dee6f7047cae |

added finite(option) to Recdef.thy

--- a/src/HOL/Recdef.thy Tue Aug 09 11:00:44 2005 +0200 +++ b/src/HOL/Recdef.thy Tue Aug 09 11:44:38 2005 +0200 @@ -79,4 +79,19 @@ wf_same_fst wf_empty +(* The following should really go into Datatype or Finite_Set, but +each one lacks the other theory as a parent . . . *) + +lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV" +by (rule set_ext, case_tac x, auto) + +instance option :: (finite) finite +proof + have "finite (UNIV :: 'a set)" by (rule finite) + hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp + also have "insert None (Some ` (UNIV :: 'a set)) = UNIV" + by (rule insert_None_conv_UNIV) + finally show "finite (UNIV :: 'a option set)" . +qed + end