blob: aa576354a59637e74fd37dae765ed381de924802 (
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
|
theory More_List
imports
Spartan.List
Nat
begin
experiment begin
Lemma "map (\<lambda>n: Nat. suc n) [0, suc (suc 0), suc 0] \<equiv> ?xs"
unfolding map_def by (subst comps)+
end
section \<open>Length\<close>
definition [implicit]:
"len \<equiv> ListRec ? Nat 0 (\<lambda>_ _ n. suc n)"
experiment begin
Lemma "len [] \<equiv> 0" by reduce
Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comps)+
end
section \<open>Equality on lists\<close>
(*Hmmm.*)
end
|
