equal
deleted
inserted
replaced
1077 \end{warn} |
1077 \end{warn} |
1078 |
1078 |
1079 |
1079 |
1080 \subsection{Exercises} |
1080 \subsection{Exercises} |
1081 |
1081 |
|
1082 |
|
1083 \exercise |
|
1084 Give a structured proof of @{prop "ev(Suc(Suc n)) \<Longrightarrow> ev n"} |
|
1085 by rule inversion: |
|
1086 *} |
|
1087 |
|
1088 lemma assumes a: "ev(Suc(Suc n))" shows "ev n" |
|
1089 (*<*)oops(*>*) |
|
1090 |
|
1091 text{* |
|
1092 \endexercise |
|
1093 |
1082 \begin{exercise} |
1094 \begin{exercise} |
1083 Give a structured proof of @{prop "\<not> ev(Suc(Suc(Suc 0)))"}. |
1095 Give a structured proof of @{prop "\<not> ev(Suc(Suc(Suc 0)))"} |
1084 Rule inversion is sufficient. If there are no cases to be proved you can close |
1096 by rule inversions. If there are no cases to be proved you can close |
1085 a proof immediateley with \isacom{qed}. |
1097 a proof immediateley with \isacom{qed}. |
1086 \end{exercise} |
1098 \end{exercise} |
1087 |
1099 |
1088 \begin{exercise} |
1100 \begin{exercise} |
1089 Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"} |
1101 Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"} |