Editing Isabelle (proof assistant) (section)

==Example proof==
Isabelle allows proofs to be written in two different styles, the [[procedural programming|procedural]] and the [[declarative programming|declarative]]. Procedural proofs specify a series of [[Tactic (computer science)|tactics]] (theorem proving [[Subroutine|functions/procedures]]) to apply. While reflecting the procedure that a human mathematician might apply to proving a result, they are typically hard to read as they do not describe the outcome of these steps. Declarative proofs (supported by Isabelle's proof language, Isar), on the other hand, specify the actual mathematical operations to be performed, and are therefore more easily read and checked by humans.

The procedural style has been deprecated in recent versions of Isabelle.<ref>{{cite web|url=https://isabelle.in.tum.de/doc/isar-ref.pdf|title=The Isabelle/Isar Reference Manual|first=Makarius|last=Wenzel|date=March 13, 2025|access-date=2025-05-10}} Page 148: "Arbitrary goal refinement via tactics is considered harmful". See also section 7.3, "Tactics: improper proof methods", pp. 172–175.</ref>

For example, a declarative [[proof by contradiction]] in Isar that [[Square root of 2#Proof by infinite descent|the square root of two is not rational]] can be written as follows.
<div style="font-family: monospace, monospace;"> 
 {{color|darkblue|theorem}} sqrt2_not_rational:
   {{olive|"sqrt 2 ∉ {{mathbb|Q}}"}}
 {{color|darkblue|proof}}
   {{color|darkblue|let}} ?x = {{olive|"sqrt 2"}}
   {{blue|assume}} {{olive|"?x ∈ {{mathbb|Q}}"}}
   {{color|darkblue|then}} {{blue|obtain}} m n :: nat {{green|where}}
     sqrt_rat: {{olive|"¦?x¦ {{=}} m / n"}} {{green|and}} lowest_terms: {{olive|"coprime m n"}}
     {{color|darkblue|by}} (rule Rats_abs_nat_div_natE)
   {{color|darkblue|hence}} {{olive|"m^2 {{=}} ?x^2 * n^2"}} {{color|darkblue|by}} (auto simp add: power2_eq_square)
   {{color|darkblue|hence}} eq: {{olive|"m^2 {{=}} 2 * n^2"}} {{color|darkblue|using}} of_nat_eq_iff power2_eq_square {{color|darkblue|by}} fastforce
   {{color|darkblue|hence}} {{olive|"2 dvd m^2"}} {{color|darkblue|by}} simp
   {{color|darkblue|hence}} {{olive|"2 dvd m"}} {{color|darkblue|by}} simp
   {{color|darkblue|have}} {{olive|"2 dvd n"}} {{color|darkblue|proof}} -
     {{color|darkblue|from}} {{olive|‹2 dvd m›}} {{blue|obtain}} k {{green|where}} {{color|olive|"m {{=}} 2 * k"}} ..<!--The two dots refer to a complete proof of this claim-->
     {{color|darkblue|with}} eq {{color|darkblue|have}} {{olive|"2 * n^2 {{=}} 2^2 * k^2"}} {{color|darkblue|by}} simp
     {{color|darkblue|hence}} {{olive|"2 dvd n^2"}} {{color|darkblue|by}} simp
     {{blue|thus}} {{olive|"2 dvd n"}} {{color|darkblue|by}} simp
   {{color|darkblue|qed}}
   {{color|darkblue|with}} {{olive|‹2 dvd m›}} {{color|darkblue|have}} {{olive|"2 dvd gcd m n"}} {{color|darkblue|by}} (rule gcd_greatest)
   {{color|darkblue|with}} lowest_terms {{color|darkblue|have}} {{olive|"2 dvd 1"}} {{color|darkblue|by}} simp
   {{blue|thus}} False {{color|darkblue|using}} odd_one {{color|darkblue|by}} blast
 {{color|darkblue|qed}}
</div>