equal
deleted
inserted
replaced
77 wf_measure |
77 wf_measure |
78 wf_pred_nat |
78 wf_pred_nat |
79 wf_same_fst |
79 wf_same_fst |
80 wf_empty |
80 wf_empty |
81 |
81 |
|
82 (* The following should really go into Datatype or Finite_Set, but |
|
83 each one lacks the other theory as a parent . . . *) |
|
84 |
|
85 lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV" |
|
86 by (rule set_ext, case_tac x, auto) |
|
87 |
|
88 instance option :: (finite) finite |
|
89 proof |
|
90 have "finite (UNIV :: 'a set)" by (rule finite) |
|
91 hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp |
|
92 also have "insert None (Some ` (UNIV :: 'a set)) = UNIV" |
|
93 by (rule insert_None_conv_UNIV) |
|
94 finally show "finite (UNIV :: 'a option set)" . |
|
95 qed |
|
96 |
82 end |
97 end |