equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Datatype option *} |
5 header {* Datatype option *} |
6 |
6 |
7 theory Option |
7 theory Option |
8 imports Datatype |
8 imports Datatype Finite_Set |
9 begin |
9 begin |
10 |
10 |
11 datatype 'a option = None | Some 'a |
11 datatype 'a option = None | Some 'a |
12 |
12 |
13 lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" |
13 lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" |
27 | (Some) y where "x = Some y" and "Q y" |
27 | (Some) y where "x = Some y" and "Q y" |
28 using c by (cases x) simp_all |
28 using c by (cases x) simp_all |
29 |
29 |
30 lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV" |
30 lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV" |
31 by (rule set_ext, case_tac x) auto |
31 by (rule set_ext, case_tac x) auto |
|
32 |
|
33 instance option :: (finite) finite proof |
|
34 qed (simp add: insert_None_conv_UNIV [symmetric]) |
32 |
35 |
33 lemma inj_Some [simp]: "inj_on Some A" |
36 lemma inj_Some [simp]: "inj_on Some A" |
34 by (rule inj_onI) simp |
37 by (rule inj_onI) simp |
35 |
38 |
36 |
39 |