blob: d8219206eeb3f3f8e1c4b68130c960e3d48c4eb7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
chapter \<open>Maybe type\<close>
theory Maybe
imports More_Types
begin
text \<open>Defined as a sum.\<close>
definition "Maybe A \<equiv> A \<or> \<top>"
definition "none A \<equiv> inr A \<top> tt"
definition "some A a \<equiv> inl A \<top> a"
lemma
MaybeF: "A: U i \<Longrightarrow> Maybe A: U i" and
Maybe_none: "A: U i \<Longrightarrow> none A: Maybe A" and
Maybe_some: "a: A \<Longrightarrow> some A a: Maybe A"
unfolding Maybe_def none_def some_def by typechk+
Definition MaybeInd:
assumes
"A: U i"
"\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
"c\<^sub>0: C (none A)"
"\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
"m: Maybe A"
shows "C m"
supply assms[unfolded Maybe_def none_def some_def]
apply (elim m)
\<guillemotright> unfolding Maybe_def .
\<guillemotright> by (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>)
\<guillemotright> by elim (rule \<open>_: C (inr _ _ _)\<close>)
done
Lemma Maybe_comp_none:
assumes
"A: U i"
"c\<^sub>0: C (none A)"
"\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
"\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
shows "MaybeInd A C c\<^sub>0 f (none A) \<equiv> c\<^sub>0"
supply assms[unfolded Maybe_def some_def none_def]
unfolding MaybeInd_def none_def by reduce
Lemma Maybe_comp_some:
assumes
"A: U i"
"a: A"
"c\<^sub>0: C (none A)"
"\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
"\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
shows "MaybeInd A C c\<^sub>0 f (some A a) \<equiv> f a"
supply assms[unfolded Maybe_def some_def none_def]
unfolding MaybeInd_def some_def by (reduce add: Maybe_def)
lemmas
[intros] = MaybeF Maybe_none Maybe_some and
[comps] = Maybe_comp_none Maybe_comp_some and
MaybeE [elims "?m"] = MaybeInd[rotated 4]
lemmas
Maybe_cases [cases] = MaybeE
abbreviation "MaybeRec A C \<equiv> MaybeInd A (K C)"
definition none_i ("none") where [implicit]: "none \<equiv> Maybe.none ?"
definition some_i ("some") where [implicit]: "some a \<equiv> Maybe.some ? a"
translations
"none" \<leftharpoondown> "CONST Maybe.none A"
"some a" \<leftharpoondown> "CONST Maybe.some A a"
end
|
