isabelle: src/HOLCF/IOA/NTP/Lemmas.ML@ae1daa601638 (annotated)

3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOL/IOA/NTP/Lemmas.ML
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
12218 6597093b77e7 GPLed; wenzelm parents: 11701 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	6
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7	(* Logic *)
4532 006e5572aca8 * empty log message * oheimb parents: 4423 diff changeset	8
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	9	goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10	by (Fast_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11	qed "fork_lemma";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13	goal HOL.thy "((A --> B) & (C --> B)) = ((A \| C) --> B)";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14	by (Fast_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	15	qed "imp_or_lem";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17	goal HOL.thy "(X = (~ Y)) = ((~X) = Y)";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18	by (Fast_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19	qed "neg_flip";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	20
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	21
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	22	(* Sets *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	23	val set_lemmas =
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	24	map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	25	["f(x) : (UN x. {f(x)})",
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	26	"f x y : (UN x y. {f x y})",
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	27	"!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	28	"!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	29
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30
4377 2cba48b0f1c4 Cleaned up arithmetic mess. nipkow parents: 4372 diff changeset	31	(* Arithmetic *)
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	32
11701 3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, wenzelm parents: 10215 diff changeset	33	goal NatArith.thy "!!x. 0<x ==> (x - 1 = y) = (x = Suc(y))";
5192 704dd3a6d47d Adapted to new datatype package. berghofe parents: 4833 diff changeset	34	by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	35	qed "pred_suc";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	36
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	37
4377 2cba48b0f1c4 Cleaned up arithmetic mess. nipkow parents: 4372 diff changeset	38	Addsimps (hd_append :: set_lemmas);

author	aspinall
	Thu, 10 Jun 2004 18:46:35 +0200
changeset 14916	ae1daa601638
parent 13524	604d0f3622d6
child 14981	e73f8140af78
permissions	-rw-r--r--