isabelle: src/HOL/Hoare/Hoare_Tac.thy@a8e47bd31965 (annotated)

72985 9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	1	(* Title: HOL/Hoare/Hoare_Tac.thy
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	2	Author: Leonor Prensa Nieto & Tobias Nipkow
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	3	Author: Walter Guttmann (extension to total-correctness proofs)
72990 db8f94656024 tuned document, notably authors and sections; wenzelm parents: 72985 diff changeset	4	*)
72985 9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	5
72990 db8f94656024 tuned document, notably authors and sections; wenzelm parents: 72985 diff changeset	6	section \<open>Hoare logic VCG tactic\<close>
72985 9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	7
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	8	theory Hoare_Tac
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	9	imports Main
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	10	begin
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	11
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	12	context
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	13	begin
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	14
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	15	qualified named_theorems BasicRule
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	16	qualified named_theorems SkipRule
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	17	qualified named_theorems AbortRule
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	18	qualified named_theorems SeqRule
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	19	qualified named_theorems CondRule
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	20	qualified named_theorems WhileRule
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	21
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	22	qualified named_theorems BasicRuleTC
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	23	qualified named_theorems SkipRuleTC
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	24	qualified named_theorems SeqRuleTC
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	25	qualified named_theorems CondRuleTC
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	26	qualified named_theorems WhileRuleTC
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	27
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	28	lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	29	by blast
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	30
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	31	ML_file \<open>hoare_tac.ML\<close>
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	32
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	33	end
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	34
9cc431444435 clarified modules: avoid multiple uses of the same ML file; wenzelm parents: diff changeset	35	end

author	wenzelm
	Tue, 22 Jul 2025 12:02:53 +0200
changeset 82894	a8e47bd31965
parent 72990	db8f94656024
permissions	-rw-r--r--