summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Recdef.thy

changeset 17040 | 6682c93b7d9f |

parent 16417 | 9bc16273c2d4 |

child 18336 | 1a2e30b37ed3 |

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