Anonymous user
Proof: Difference between revisions
no edit summary
(added Raku programming solution (Incomplete)) |
No edit summary |
||
Line 750:
</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}}==
| |||