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

src/HOL/Recdef.thy

changeset 22399 | 80395c2c40cc |

parent 22264 | 6a65e9b2ae05 |

child 22622 | 25693088396b |

1.1 --- a/src/HOL/Recdef.thy Sat Mar 03 09:26:58 2007 +0100 1.2 +++ b/src/HOL/Recdef.thy Sat Mar 03 09:27:00 2007 +0100 1.3 @@ -82,20 +82,4 @@ 1.4 wf_implies_wfP 1.5 wfP_implies_wf 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 - 1.23 end