# HG changeset patch
# User slotosch
# Date 856182392 -3600
# Node ID 2fa0f0c1c750681669d9aa681b6cce1c7ed641d9
# Parent  a7f469c0ba592501c9c3f423e7a05fc52604b782
New file for theorems of Porder0
Dervie the prperties of partial orders from the axiomatic type class po

diff -r a7f469c0ba59 -r 2fa0f0c1c750 src/HOLCF/Porder0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Porder0.ML	Mon Feb 17 13:26:32 1997 +0100
@@ -0,0 +1,40 @@
+(*  Title:      HOLCF/Porder0.ML
+    ID:         $Id$
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
+
+    derive the characteristic axioms for the characteristic constants *)
+
+open Porder0;
+
+qed_goalw "refl_less" thy [ po_def ] "x << x"
+(fn prems =>
+        [
+        (fast_tac (HOL_cs addSIs [ax_refl_less]) 1)
+        ]);
+
+qed_goalw "antisym_less" thy [ po_def ] "[| x << y; y << x |] ==> x = y"
+(fn prems =>
+        [
+        (fast_tac (HOL_cs addSIs prems@[ax_antisym_less]) 1)
+        ]);
+
+qed_goalw "trans_less" thy [ po_def ] "[| x << y; y << z |] ==> x << z"
+(fn prems =>
+        [
+        (fast_tac (HOL_cs addIs prems@[ax_trans_less]) 1)
+        ]);
+
+(* ------------------------------------------------------------------------ *)
+(* minimal fixes least element                                              *)
+(* ------------------------------------------------------------------------ *)
+bind_thm("minimal2UU",allI RS (prove_goal thy "!x.uu<<x==>uu=(@u.!y.u<<y)"
+(fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (rtac antisym_less 1),
+        (etac spec 1),
+        (res_inst_tac [("a","uu")] selectI2 1),
+	(atac 1),
+	(etac spec 1)
+        ])));