equal
deleted
inserted
replaced
436 *} |
436 *} |
437 |
437 |
438 inductive ev :: "nat \<Rightarrow> bool" where |
438 inductive ev :: "nat \<Rightarrow> bool" where |
439 ev0: "ev 0" | |
439 ev0: "ev 0" | |
440 evSS: (*<*)"ev n \<Longrightarrow> ev (Suc(Suc n))"(*>*) |
440 evSS: (*<*)"ev n \<Longrightarrow> ev (Suc(Suc n))"(*>*) |
441 text_raw{* @{prop"ev n \<Longrightarrow> ev (n + 2)"} *} |
441 text_raw{* @{prop[source]"ev n \<Longrightarrow> ev (n + 2)"} *} |
442 |
442 |
443 text{* To get used to inductive definitions, we will first prove a few |
443 text{* To get used to inductive definitions, we will first prove a few |
444 properties of @{const ev} informally before we descend to the Isabelle level. |
444 properties of @{const ev} informally before we descend to the Isabelle level. |
445 |
445 |
446 How do we prove that some number is even, e.g.\ @{prop "ev 4"}? Simply by combining the defining rules for @{const ev}: |
446 How do we prove that some number is even, e.g.\ @{prop "ev 4"}? Simply by combining the defining rules for @{const ev}: |