| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/SPARK/Examples/Sqrt/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 696 B |
|
Quelle Sqrt.thy Sprache: Isabelle |
|||||||||
|
(* Title: HOL/SPARK/Examples/Sqrt/Sqrt.thy
Author: Stefan Berghofer Copyright: secunet Security Networks AG *) theory Sqrt imports "HOL-SPARK.SPARK" begin spark_open \<open>sqrt/isqrt\<close> spark_vc function_isqrt_4 proof - from \<open>0 \<le> r\<close> have "(r = 0 \<or> r = 1 \<or> r = 2) \<or> 2 < r" by auto then show "2 * r \ proof assume "2 < r" then have "0 < r" by simp with \<open>2 < r\<close> have "2 * r < r * r" by (rule mult_strict_right_mono) with \<open>r * r \<le> n\<close> and \<open>n \<le> 2147483647\<close> show ?thesis by simp qed auto then show "2 * r \ qed spark_end end ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28