isabelle: src/HOLCF/Porder0.ML@6e20cc79bde6 (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
2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	4
12030 46d57d0290a2 GPLed; wenzelm parents: 9969 diff changeset	5	derive the characteristic axioms for the characteristic constants
9245 428385c4bc50 removed most batch-style proofs paulson parents: 9169 diff changeset	6	*)
2644 2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	7
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2644 diff changeset	8	AddIffs [refl_less];
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2644 diff changeset	9
2644 2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	10	(* ------------------------------------------------------------------------ *)
2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	11	(* minimal fixes least element *)
2fa0f0c1c750 New file for theorems of Porder0 slotosch parents: diff changeset	12	(* ------------------------------------------------------------------------ *)
9245 428385c4bc50 removed most batch-style proofs paulson parents: 9169 diff changeset	13	Goal "!x::'a::po. uu<<x ==> uu=(@u.!y. u<<y)";
9969 4753185f1dd2 renamed (most of...) the select rules paulson parents: 9248 diff changeset	14	by (blast_tac (claset() addIs [someI2,antisym_less]) 1);
9245 428385c4bc50 removed most batch-style proofs paulson parents: 9169 diff changeset	15	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	16
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	(* 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	19	(* ------------------------------------------------------------------------ *)
7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	20
9169 85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	21	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	22	by (Blast_tac 1);
9169 85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	23	qed "antisym_less_inverse";
3026 7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	24
7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	25
9169 85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	26	Goal "[\| (a::'a::po) << b; c << a; b << d\|] ==> c << d";
85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	27	by (etac trans_less 1);
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 (atac 1);
85a47aa21f74 tidying and unbatchifying paulson parents: 5068 diff changeset	30	qed "box_less";
3026 7a5611f66b72 moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML slotosch parents: 2841 diff changeset	31
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4423 diff changeset	32	Goal "((x::'a::po)=y) = (x << y & y << x)";
4423 a129b817b58a expandshort; wenzelm parents: 3842 diff changeset	33	by (fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
3460 5d71eed16fbe Tuned Franz's proofs. nipkow parents: 3323 diff changeset	34	qed "po_eq_conv";

author	aspinall
	Thu, 21 Oct 2004 19:21:32 +0200
changeset 15253	6e20cc79bde6
parent 14981	e73f8140af78
child 15562	8455c9671494
permissions	-rw-r--r--