isabelle: src/HOL/IMP/Star.thy@96f60533ec1d (annotated)

43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	1	theory Star imports Main
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	2	begin
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	3
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	4	inductive
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	5	star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	6	for r where
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	7	refl: "star r x x" \|
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	8	step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	9
67443 3abf6a722518 standardized towards new-style formal comments: isabelle update_comments; wenzelm parents: 67406 diff changeset	10	hide_fact (open) refl step \<comment> \<open>names too generic\<close>
45265 521508e85c0d tuned names to avoid shadowing nipkow parents: 45015 diff changeset	11
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	12	lemma star_trans:
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	13	"star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
45015 fdac1e9880eb Updated IMP to use new induction method nipkow parents: 43141 diff changeset	14	proof(induction rule: star.induct)
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	15	case refl thus ?case .
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	16	next
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	17	case step thus ?case by (metis star.step)
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	18	qed
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	19
50054 6da283e4497b tuned layout nipkow parents: 45265 diff changeset	20	lemmas star_induct =
6da283e4497b tuned layout nipkow parents: 45265 diff changeset	21	star.induct[of "r:: 'a'b \<Rightarrow> 'a'b \<Rightarrow> bool", split_format(complete)]
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	22
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	23	declare star.refl[simp,intro]
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	24
45265 521508e85c0d tuned names to avoid shadowing nipkow parents: 45015 diff changeset	25	lemma star_step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
521508e85c0d tuned names to avoid shadowing nipkow parents: 45015 diff changeset	26	by(metis star.refl star.step)
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	27
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	28	code_pred star .
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	29
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: diff changeset	30	end

author	wenzelm
	Fri, 26 Apr 2024 13:25:44 +0200
changeset 80150	96f60533ec1d
parent 67443	3abf6a722518
permissions	-rw-r--r--