equal
deleted
inserted
replaced
14 An injective function from @{text "\<nat>\<twosuperior>"} to @{text \<nat>}. Definition |
14 An injective function from @{text "\<nat>\<twosuperior>"} to @{text \<nat>}. Definition |
15 and proofs are from \cite[page 85]{Oberschelp:1993}. |
15 and proofs are from \cite[page 85]{Oberschelp:1993}. |
16 *} |
16 *} |
17 |
17 |
18 definition |
18 definition |
19 nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" |
19 nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where |
20 "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)" |
20 "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)" |
21 |
21 |
22 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" |
22 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" |
23 proof (cases "2 dvd a") |
23 proof (cases "2 dvd a") |
24 case True |
24 case True |