author | nipkow |

Tue Aug 09 11:44:38 2005 +0200 (2005-08-09) | |

changeset 17040 | 6682c93b7d9f |

parent 17039 | 78159411623f |

child 17041 | dee6f7047cae |

added finite(option) to Recdef.thy

1.1 --- a/src/HOL/Recdef.thy Tue Aug 09 11:00:44 2005 +0200 1.2 +++ b/src/HOL/Recdef.thy Tue Aug 09 11:44:38 2005 +0200 1.3 @@ -79,4 +79,19 @@ 1.4 wf_same_fst 1.5 wf_empty 1.6 1.7 +(* The following should really go into Datatype or Finite_Set, but 1.8 +each one lacks the other theory as a parent . . . *) 1.9 + 1.10 +lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV" 1.11 +by (rule set_ext, case_tac x, auto) 1.12 + 1.13 +instance option :: (finite) finite 1.14 +proof 1.15 + have "finite (UNIV :: 'a set)" by (rule finite) 1.16 + hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp 1.17 + also have "insert None (Some ` (UNIV :: 'a set)) = UNIV" 1.18 + by (rule insert_None_conv_UNIV) 1.19 + finally show "finite (UNIV :: 'a option set)" . 1.20 +qed 1.21 + 1.22 end