4 |
4 |
5 declare One_nat_def[simp del] |
5 declare One_nat_def[simp del] |
6 |
6 |
7 fun oddfactor :: "nat \<Rightarrow> nat" where |
7 fun oddfactor :: "nat \<Rightarrow> nat" where |
8 [simp del]: "oddfactor n = (if n = 0 then 0 |
8 [simp del]: "oddfactor n = (if n = 0 then 0 |
9 else if even n then oddfactor (n div 2) else n)" |
9 else if even n then oddfactor (n div 2) else ((n - 1) div 2))" |
10 |
10 |
11 fun evenfactor :: "nat \<Rightarrow> nat" where |
11 fun evenfactor :: "nat \<Rightarrow> nat" where |
12 [simp del]: "evenfactor n = (if n = 0 then 0 |
12 [simp del]: "evenfactor n = (if n = 0 then 0 |
13 else if even n then 2 * evenfactor (n div 2) else 1)" |
13 else if even n then 2 * evenfactor (n div 2) else 1)" |
14 |
14 |
15 lemma oddfactor[simp]: |
15 lemma oddfactor [simp]: |
16 "oddfactor 0 = 0" |
16 "oddfactor 0 = 0" |
17 "odd n \<Longrightarrow> oddfactor n = n" |
17 "odd n \<Longrightarrow> oddfactor n = (n - 1) div 2" |
18 "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)" |
18 "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)" |
19 by (simp_all add: oddfactor.simps) |
19 by (simp_all add: oddfactor.simps) |
|
20 |
|
21 lemma evenfactor [simp]: |
|
22 "evenfactor 0 = 0" |
|
23 "odd n \<Longrightarrow> evenfactor n = 1" |
|
24 "even n \<Longrightarrow> evenfactor n = 2 * evenfactor (n div 2)" |
|
25 apply(simp_all add: evenfactor.simps) |
|
26 apply(case_tac n) |
|
27 apply(simp_all) |
|
28 done |
|
29 |
|
30 fun penc :: "(nat \<times> nat) \<Rightarrow> nat" where |
|
31 "penc (m, n) = (2 ^ m) * (2 * n + 1) - 1" |
|
32 |
|
33 fun pdec :: "nat \<Rightarrow> nat \<times> nat" where |
|
34 "pdec z = (Discrete.log (evenfactor (Suc z)), oddfactor (Suc z))" |
|
35 |
|
36 lemma q2: "pdec (penc m) = m" |
|
37 apply(case_tac m) |
|
38 apply(simp) |
|
39 apply(simp only: penc.simps pdec.simps) |
|
40 apply(case_tac m) |
|
41 apply(simp only: penc.simps pdec.simps) |
|
42 apply(subst y1) |
|
43 apply(subst y2) |
|
44 apply(simp) |
|
45 done |
20 |
46 |
21 |
47 |
22 lemma oddfactor_odd: |
48 lemma oddfactor_odd: |
23 "oddfactor n = 0 \<or> odd (oddfactor n)" |
49 "oddfactor n = 0 \<or> odd (oddfactor n)" |
24 apply(induct n rule: nat_less_induct) |
50 apply(induct n rule: nat_less_induct) |