Proof: Difference between revisions
Content added Content deleted
(added Raku programming solution (Incomplete)) |
No edit summary |
||
Line 750: | Line 750: | ||
</lang> |
</lang> |
||
=={{header|Isabelle}}== |
|||
<lang Isabelle>theory Proof |
|||
imports Main |
|||
begin |
|||
section‹Using the Standard Library› |
|||
text‹ |
|||
All natural numbers: |
|||
The \<^const>‹UNIV› with the type annotation \<^typ>‹nat set› represents all natural numbers. |
|||
In general, \<^term>‹UNIV :: 'a set› is the set of all elements of type \<^typ>‹'a›. |
|||
› |
|||
lemma "{0, 1, 2, 3, 4} ⊆ (UNIV :: nat set)" by simp |
|||
text‹The set of all even numbers.› |
|||
lemma "{0, 2, 4, 6, 8} ⊆ {n. even n}" by simp |
|||
lemma "3 ∉ {n. even n}" by simp |
|||
text‹The set of all odd numbers.› |
|||
lemma "{1, 3, 5, 7, 9} ⊆ {n. odd n}" by simp |
|||
lemma "2 ∉ {n. odd n}" by simp |
|||
lemma "2+2 = 4" by simp |
|||
text‹Prove that the addition of any two even numbers is even.› |
|||
lemma "even n ⟹ even m ⟹ even (n+m)" by simp |
|||
text‹Prove that the addition is always associative.› |
|||
lemma fixes a::nat shows "(a+b)+c = a+(b+c)" by simp |
|||
text‹Prove that the addition is always commutative.› |
|||
lemma fixes a::nat shows "a+b = b+a" by simp |
|||
text‹Try to prove that the addition of any two even numbers is odd (it should be rejected).› |
|||
lemma "even n ⟹ even m ⟹ odd (n+m) ⟹ False" by simp |
|||
section‹Implementing our Own Natural Numbers› |
|||
datatype mynat = Z | S mynat |
|||
fun add :: "mynat ⇒ mynat ⇒ mynat" where |
|||
"add a Z = a" |
|||
| "add a (S b) = S (add a b)" |
|||
inductive myeven :: "mynat ⇒ bool" where |
|||
"myeven Z" |
|||
| "myeven a ⟹ myeven (S (S a))" |
|||
text‹All \<^typ>‹mynat›s. Since \<^const>‹S› and \<^const>‹Z› are unique, we don't need a type annotation.› |
|||
lemma "{Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z)))} ⊆ UNIV" by simp |
|||
text‹The set of all even numbers.› |
|||
lemma "{Z, S (S Z), S (S (S (S Z))), S (S (S (S (S (S Z)))))} ⊆ {n. myeven n}" by (auto intro: myeven.intros) |
|||
lemma "S (S (S Z)) ∉ {n. myeven n}" using myeven.cases by auto |
|||
text‹The set of all odd numbers.› |
|||
lemma "{S Z, S (S (S Z)), S (S (S (S (S Z)))), S (S (S (S (S (S (S Z))))))} ⊆ {n. ¬myeven n}" |
|||
apply (auto intro: myeven.intros) |
|||
by (metis myeven.cases mynat.distinct(1) mynat.inject)+ |
|||
lemma "S (S Z) ∉ {n. ¬myeven n}" by (auto intro: myeven.intros) |
|||
lemma "add (S (S Z)) (S (S Z)) = S (S (S (S Z)))" by simp |
|||
text‹Prove that the addition of any two even numbers is even.› |
|||
lemma "myeven m ⟹ myeven n ⟹ myeven (add n m)" |
|||
apply(induction m rule: myeven.induct) |
|||
apply(simp) |
|||
by (auto intro: myeven.intros) |
|||
text‹Prove that the addition is always associative.› |
|||
lemma "add (add a b) c = add a (add b c)" by(induction c) (simp)+ |
|||
text‹Prove that the addition is always commutative.› |
|||
lemma add_zero[simp]: "add Z b = b" by(induction b) (simp)+ |
|||
lemma add_fst: "add (S a) b = S (add a b)" by(induction b) (simp)+ |
|||
lemma "add a b = add b a" |
|||
apply(induction a arbitrary:b ) |
|||
apply(simp) |
|||
apply(simp add: add_fst) |
|||
done |
|||
text‹Try to prove that the addition of any two even numbers is odd (it should be rejected).› |
|||
lemma "myeven n ⟹ myeven m ⟹ ¬myeven (add n m) ⟹ False" |
|||
apply(induction n rule: myeven.induct) |
|||
apply(simp) |
|||
apply(simp add: add_fst) |
|||
by(auto intro: myeven.intros) |
|||
end</lang> |
|||
=={{header|J}}== |
=={{header|J}}== |