ord.ML
author convert-repo
Thu, 23 Jul 2009 14:03:20 +0000
changeset 255 435bf30c29a5
parent 0 7949f97df77a
permissions -rw-r--r--
update tags
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     1
open Ord;
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     2
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     3
val [prem] = goalw Ord.thy [mono_def]
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     4
    "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     5
by (REPEAT (ares_tac [allI, impI, prem] 1));
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     6
val monoI = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     7
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     8
val [major,minor] = goalw Ord.thy [mono_def]
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     9
    "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    10
by (rtac (major RS spec RS spec RS mp) 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    11
by (rtac minor 1);
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    12
val monoD = result();
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    13