isabelle: src/HOLCF/Porder0.ML@4dff931b852f (annotated)

2644 2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	1	(* Title: HOLCF/Porder0.ML
2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	2	ID: $Id$
2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	3	Author: Oscar Slotosch
12030 46d57d0290a2 GPLed; wenzelm parents: 9969 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
2644 2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	5
12030 46d57d0290a2 GPLed; wenzelm parents: 9969 diff changeset	6	derive the characteristic axioms for the characteristic constants
9245 428385c4bc50 removed most batch-style proofs paulson parents: 9169 diff changeset	7	*)
2644 2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	8
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2644 diff changeset	9	AddIffs [refl_less];
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2644 diff changeset	10
2644 2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	11	(* ------------------------------------------------------------------------ *)
2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	12	(* minimal fixes least element *)
2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	13	(* ------------------------------------------------------------------------ *)
9245 428385c4bc50 removed most batch-style proofs paulson parents: 9169 diff changeset	14	Goal "!x::'a::po. uu<<x ==> uu=(@u.!y. u<<y)";
9969 4753185f1dd2 renamed (most of...) the select rules paulson parents: 9248 diff changeset	15	by (blast_tac (claset() addIs [someI2,antisym_less]) 1);
9245 428385c4bc50 removed most batch-style proofs paulson parents: 9169 diff changeset	16	bind_thm ("minimal2UU", allI RS result());
3026 7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	17
7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	18	(* ------------------------------------------------------------------------ *)
7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	19	(* the reverse law of anti--symmetrie of << *)
7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	20	(* ------------------------------------------------------------------------ *)
7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	21
9169 85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	22	Goal "(x::'a::po)=y ==> x << y & y << x";
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	23	by (Blast_tac 1);
9169 85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	24	qed "antisym_less_inverse";
3026 7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	25
7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	26
9169 85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	27	Goal "[\| (a::'a::po) << b; c << a; b << d\|] ==> c << d";
85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	28	by (etac trans_less 1);
85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	29	by (etac trans_less 1);
85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	30	by (atac 1);
85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	31	qed "box_less";
3026 7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	32
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4423 diff changeset	33	Goal "((x::'a::po)=y) = (x << y & y << x)";
4423 a129b817b58a expandshort; wenzelm parents: 3842 diff changeset	34	by (fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
3460 5d71eed16fbe Tuned Franz's proofs. nipkow parents: 3323 diff changeset	35	qed "po_eq_conv";

author	wenzelm
	Thu, 15 Nov 2001 18:20:13 +0100
changeset 12207	4dff931b852f
parent 12030	46d57d0290a2
child 14981	e73f8140af78
permissions	-rw-r--r--