src/ZF/Rel.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 2469 b50b8c0eec01
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 760
diff changeset
     1
(*  Title:      ZF/Rel.ML
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 760
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     5
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     6
For Rel.thy.  Relations in Zermelo-Fraenkel Set Theory 
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     7
*)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     8
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     9
open Rel;
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    10
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    11
(*** Some properties of relations -- useful? ***)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    12
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    13
(* irreflexivity *)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    14
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    15
val prems = goalw Rel.thy [irrefl_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    16
    "[| !!x. x:A ==> <x,x> ~: r |] ==> irrefl(A,r)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    17
by (REPEAT (ares_tac (prems @ [ballI]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 435
diff changeset
    18
qed "irreflI";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    19
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    20
val prems = goalw Rel.thy [irrefl_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    21
    "[| irrefl(A,r);  x:A |] ==>  <x,x> ~: r";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    22
by (rtac (prems MRS bspec) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 435
diff changeset
    23
qed "irreflE";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    24
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    25
(* symmetry *)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    26
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    27
val prems = goalw Rel.thy [sym_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    28
     "[| !!x y.<x,y>: r ==> <y,x>: r |] ==> sym(r)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    29
by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 435
diff changeset
    30
qed "symI";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    31
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    32
goalw Rel.thy [sym_def] "!!r. [| sym(r); <x,y>: r |]  ==>  <y,x>: r";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    33
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 435
diff changeset
    34
qed "symE";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    35
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    36
(* antisymmetry *)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    37
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    38
val prems = goalw Rel.thy [antisym_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    39
     "[| !!x y.[| <x,y>: r;  <y,x>: r |] ==> x=y |] ==> \
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    40
\     antisym(r)";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    41
by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 435
diff changeset
    42
qed "antisymI";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    43
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    44
val prems = goalw Rel.thy [antisym_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    45
     "!!r. [| antisym(r); <x,y>: r;  <y,x>: r |]  ==>  x=y";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    46
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 435
diff changeset
    47
qed "antisymE";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    48
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    49
(* transitivity *)
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    50
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    51
goalw Rel.thy [trans_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    52
    "!!r. [| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    53
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 435
diff changeset
    54
qed "transD";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    55
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    56
goalw Rel.thy [trans_on_def]
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    57
    "!!r. [| trans[A](r);  <a,b>:r;  <b,c>:r;  a:A;  b:A;  c:A |] ==> <a,c>:r";
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    58
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 435
diff changeset
    59
qed "trans_onD";
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    60