equal
deleted
inserted
replaced
3 *) |
3 *) |
4 theory QuotOption |
4 theory QuotOption |
5 imports QuotMain |
5 imports QuotMain |
6 begin |
6 begin |
7 |
7 |
8 section {* Quotient infrastructure for option type *} |
8 section {* Quotient infrastructure for the option type. *} |
9 |
9 |
10 fun |
10 fun |
11 option_rel |
11 option_rel |
12 where |
12 where |
13 "option_rel R None None = True" |
13 "option_rel R None None = True" |
18 declare [[map option = (Option.map, option_rel)]] |
18 declare [[map option = (Option.map, option_rel)]] |
19 |
19 |
20 text {* should probably be in Option.thy *} |
20 text {* should probably be in Option.thy *} |
21 lemma split_option_all: |
21 lemma split_option_all: |
22 shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))" |
22 shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))" |
23 apply(auto) |
23 apply(auto) |
24 apply(case_tac x) |
24 apply(case_tac x) |
25 apply(simp_all) |
25 apply(simp_all) |
26 done |
26 done |
27 |
27 |
28 lemma option_quotient[quot_thm]: |
28 lemma option_quotient[quot_thm]: |
29 assumes q: "Quotient R Abs Rep" |
29 assumes q: "Quotient R Abs Rep" |
30 shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" |
30 shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" |
31 unfolding Quotient_def |
31 unfolding Quotient_def |