isabelle: src/HOL/HOLCF/IOA/NTP/Lemmas.thy@64b47495676d (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
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	11	lemma neg_flip: "(X = (~ Y)) = ((~X) = Y)"
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:
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	18	"f(x) : (UN x. {f(x)})"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	19	"f x y : (UN x y. {f x y})"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	20	"!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})"
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 17244 diff changeset	21	"!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"
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
	Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787	64b47495676d
parent 63648	f9f3006a5579
child 67613	ce654b0e6d69
permissions	-rw-r--r--