| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/HOLCF/IMP/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle HoareEx.thySprache: Isabelle |
|||||||||||||||
|
(* Title: HOL/HOLCF/IMP/HoareEx.thy Author: Tobias Nipkow, TUM Copyright 1997 TUM *) section "Correctness of Hoare by Fixpoint Reasoning" theory HoareEx imports Denotational begin text ‹ An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch cite‹MuellerNvOS99›. It demonstrates fixpoint reasoning by showing the correctness of the Hoare rule for while-loops. › type_synonym assn = "state → bool" definition hoare_valid :: "[assn, com, assn] → bool" (‹|= {(1_)}/ (_)/ {(1_)}› 50) where "|= {P} c {Q} = (∀s t. P s ∧ D c⋅(Discr s) = Def t ⟶ Q t)" lemma WHILE_rule_sound: "|= {A} c {A} ==> |= {A} WHILE b DO c {λs. A s ∧ ¬ bval b s}" apply (unfold hoare_valid_def) apply (simp (no_asm)) apply (rule fix_ind) apply (simp (no_asm)) ― ‹simplifier with enhanced ‹adm›-tactic› apply (simp (no_asm)) apply (simp (no_asm)) apply blast done end
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09