isabelle: src/HOL/HOLCF/IOA/NTP/Lemmas.thy@a37ed1aeb163 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40774 diff changeset	1	(* Title: HOL/HOLCF/IOA/NTP/Lemmas.thy
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	5	theory Lemmas
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	imports Main
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	begin
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 42151 diff changeset	9	subsubsection \<open>Logic\<close>
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	10
67613 ce654b0e6d69 more symbols; wenzelm parents: 63648 diff changeset	11	lemma neg_flip: "(X = (\<not> Y)) = ((\<not>X) = Y)"
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	12	by blast
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	13
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	14
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 42151 diff changeset	15	subsection \<open>Sets\<close>
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	16
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	17	lemma set_lemmas:
67613 ce654b0e6d69 more symbols; wenzelm parents: 63648 diff changeset	18	"f(x) \<in> (\<Union>x. {f(x)})"
ce654b0e6d69 more symbols; wenzelm parents: 63648 diff changeset	19	"f x y \<in> (\<Union>x y. {f x y})"
ce654b0e6d69 more symbols; wenzelm parents: 63648 diff changeset	20	"\<And>a. (\<forall>x. a \<noteq> f(x)) \<Longrightarrow> a \<notin> (\<Union>x. {f(x)})"
ce654b0e6d69 more symbols; wenzelm parents: 63648 diff changeset	21	"\<And>a. (\<forall>x y. a \<noteq> f x y) \<Longrightarrow> a \<notin> (\<Union>x y. {f x y})"
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	22	by auto
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	23
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	24
62002 f1599e98c4d0 isabelle update_cartouches -c -t; wenzelm parents: 42151 diff changeset	25	subsection \<open>Arithmetic\<close>
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	26
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	27	lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))"
63648 f9f3006a5579 "split add" -> "split" nipkow parents: 62002 diff changeset	28	by (simp add: diff_Suc split: nat.split)
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	29
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	30	lemmas [simp] = hd_append set_lemmas
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	31
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	32	end

author	wenzelm
	Sun, 22 Sep 2024 15:58:55 +0200
changeset 80921	a37ed1aeb163
parent 67613	ce654b0e6d69
permissions	-rw-r--r--