blob: a5e77ecc371024ca9618fc8ae2bee7f0b351174f (
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
74
75
76
77
78
|
(* Title: HoTT/ex/Synthesis.thy
Author: Josh Chen
Examples of synthesis.
*)
theory Synthesis
imports "../HoTT"
begin
section ‹Synthesis of the predecessor function›
text "
In this example we construct, with the help of Isabelle, a predecessor function for the natural numbers.
This is also done in ‹CTT.thy›; there the work is easier as the equality type is extensional, and also the methods are set up a little more nicely.
"
text "First we show that the property we want is well-defined."
lemma pred_welltyped: "∑pred:ℕ→ℕ . ((pred`0) =⇩ℕ 0) × (∏n:ℕ. (pred`(succ n)) =⇩ℕ n): U(O)"
by routine
text "
Now we look for an inhabitant of this type.
Observe that we're looking for a lambda term ‹pred› satisfying ‹(pred`0) =⇩ℕ 0› and ‹∏n:ℕ. (pred`(succ n)) =⇩ℕ n›.
What if we require **definitional** equality instead of just propositional equality?
"
schematic_goal "?p`0 ≡ 0" and "⋀n. n: ℕ ⟹ (?p`(succ n)) ≡ n"
apply compute
prefer 4 apply compute
prefer 3 apply compute
apply (rule Nat_routine Nat_elim | compute | assumption)+
done
text "
The above proof finds a candidate, namely ‹❙λn. ind⇩ℕ (λa b. a) 0 n›.
We prove this has the required type and properties.
"
definition pred :: Term where "pred ≡ ❙λn. ind⇩ℕ (λa b. a) 0 n"
lemma pred_type: "pred: ℕ → ℕ" unfolding pred_def by routine
lemma pred_props: "<refl(0), ❙λn. refl(n)>: ((pred`0) =⇩ℕ 0) × (∏n:ℕ. (pred`(succ n)) =⇩ℕ n)"
proof (routine lems: pred_type)
have *: "pred`0 ≡ 0" unfolding pred_def
proof compute
show "⋀n. n: ℕ ⟹ ind⇩ℕ (λa b. a) 0 n: ℕ" by routine
show "ind⇩ℕ (λa b. a) 0 0 ≡ 0"
proof compute
show "ℕ: U(O)" ..
qed routine
qed rule
then show "refl(0): (pred`0) =⇩ℕ 0" by (subst *) routine
show "❙λn. refl(n): ∏n:ℕ. (pred`(succ(n))) =⇩ℕ n"
unfolding pred_def proof
show "⋀n. n: ℕ ⟹ refl(n): ((❙λn. ind⇩ℕ (λa b. a) 0 n)`succ(n)) =⇩ℕ n"
proof compute
show "⋀n. n: ℕ ⟹ ind⇩ℕ (λa b. a) 0 n: ℕ" by routine
show "⋀n. n: ℕ ⟹ refl(n): ind⇩ℕ (λa b. a) 0 (succ n) =⇩ℕ n"
proof compute
show "ℕ: U(O)" ..
qed routine
qed rule
qed rule
qed
theorem
"<pred, <refl(0), ❙λn. refl(n)>>: ∑pred:ℕ→ℕ . ((pred`0) =⇩ℕ 0) × (∏n:ℕ. (pred`(succ n)) =⇩ℕ n)"
by (routine lems: pred_welltyped pred_type pred_props)
end
|
