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 ‹Maybe type›
theory Maybe
imports More_Types
begin
text ‹Defined as a sum.›
definition "Maybe A ≡ A ∨ ⊤"
definition "none A ≡ inr A ⊤ tt"
definition "some A a ≡ inl A ⊤ a"
lemma
MaybeF: "A: U i ⟹ Maybe A: U i" and
Maybe_none: "A: U i ⟹ none A: Maybe A" and
Maybe_some: "a: A ⟹ some A a: Maybe A"
unfolding Maybe_def none_def some_def by typechk+
Definition MaybeInd:
assumes
"A: U i"
"⋀m. m: Maybe A ⟹ C m: U i"
"c⇩0: C (none A)"
"⋀a. a: A ⟹ f a: C (some A a)"
"m: Maybe A"
shows "C m"
supply assms[unfolded Maybe_def none_def some_def]
apply (elim m)
» unfolding Maybe_def .
» by (rule ‹_ ⟹ _: C (inl _ _ _)›)
» by elim (rule ‹_: C (inr _ _ _)›)
done
Lemma Maybe_comp_none:
assumes
"A: U i"
"c⇩0: C (none A)"
"⋀a. a: A ⟹ f a: C (some A a)"
"⋀m. m: Maybe A ⟹ C m: U i"
shows "MaybeInd A C c⇩0 f (none A) ≡ c⇩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⇩0: C (none A)"
"⋀a. a: A ⟹ f a: C (some A a)"
"⋀m. m: Maybe A ⟹ C m: U i"
shows "MaybeInd A C c⇩0 f (some A a) ≡ 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 ≡ MaybeInd A (K C)"
definition none_i ("none") where [implicit]: "none ≡ Maybe.none ?"
definition some_i ("some") where [implicit]: "some a ≡ Maybe.some ? a"
translations
"none" ↽ "CONST Maybe.none A"
"some a" ↽ "CONST Maybe.some A a"
end
|
