src/HOL/ex/rel.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      HOL/ex/rel
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Domain, range of a relation or function -- NOT YET WORKING
     7 *)
     8 
     9 structure Rel =
    10 struct
    11 val thy = extend_theory Univ.thy "Rel"
    12 ([], [], [], [],
    13  [ 
    14   (["domain"],  "('a * 'b)set => 'a set"),
    15   (["range2"],  "('a * 'b)set => 'b set"),
    16   (["field"],   "('a * 'a)set => 'a set")
    17  ],
    18  None)
    19  [
    20   ("domain_def",     "domain(r) == {a. ? b. (a,b) : r}" ),
    21   ("range2_def",     "range2(r) == {b. ? a. (a,b) : r}" ),
    22   ("field_def",      "field(r)  == domain(r) Un range2(r)" )
    23  ];
    24 end;
    25 
    26 local val ax = get_axiom Rel.thy
    27 in
    28 val domain_def = ax"domain_def";
    29 val range2_def = ax"range2_def";
    30 val field_def = ax"field_def";
    31 end;
    32 
    33 
    34 (*** domain ***)
    35 
    36 val [prem] = goalw Rel.thy [domain_def,Pair_def] "(a,b): r ==> a : domain(r)";
    37 by (fast_tac (claset() addIs [prem]) 1);
    38 qed "domainI";
    39 
    40 val major::prems = goalw Rel.thy [domain_def]
    41     "[| a : domain(r);  !!y. (a,y): r ==> P |] ==> P";
    42 by (rtac (major RS CollectE) 1);
    43 by (etac exE 1);
    44 by (REPEAT (ares_tac prems 1));
    45 qed "domainE";
    46 
    47 
    48 (*** range2 ***)
    49 
    50 val [prem] = goalw Rel.thy [range2_def,Pair_def] "(a,b): r ==> b : range2(r)";
    51 by (fast_tac (claset() addIs [prem]) 1);
    52 qed "range2I";
    53 
    54 val major::prems = goalw Rel.thy [range2_def]
    55     "[| b : range2(r);  !!x. (x,b): r ==> P |] ==> P";
    56 by (rtac (major RS CollectE) 1);
    57 by (etac exE 1);
    58 by (REPEAT (ares_tac prems 1));
    59 qed "range2E";
    60 
    61 
    62 (*** field ***)
    63 
    64 val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> a : field(r)";
    65 by (rtac (prem RS domainI RS UnI1) 1);
    66 qed "fieldI1";
    67 
    68 val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> b : field(r)";
    69 by (rtac (prem RS range2I RS UnI2) 1);
    70 qed "fieldI2";
    71 
    72 val [prem] = goalw Rel.thy [field_def]
    73     "(~ (c,a):r ==> (a,b): r) ==> a : field(r)";
    74 by (rtac (prem RS domainI RS UnCI) 1);
    75 by (swap_res_tac [range2I] 1);
    76 by (etac notnotD 1);
    77 qed "fieldCI";
    78 
    79 val major::prems = goalw Rel.thy [field_def]
    80      "[| a : field(r);  \
    81 \        !!x. (a,x): r ==> P;  \
    82 \        !!x. (x,a): r ==> P        |] ==> P";
    83 by (rtac (major RS UnE) 1);
    84 by (REPEAT (eresolve_tac (prems@[domainE,range2E]) 1));
    85 qed "fieldE";
    86 
    87 goalw Rel.thy [field_def] "domain(r) <= field(r)";
    88 by (rtac Un_upper1 1);
    89 qed "domain_in_field";
    90 
    91 goalw Rel.thy [field_def] "range2(r) <= field(r)";
    92 by (rtac Un_upper2 1);
    93 qed "range2_in_field";
    94 
    95 
    96 ????????????????????????????????????????????????????????????????;
    97 
    98 (*If r allows well-founded induction then wf(r)*)
    99 val [prem1,prem2] = goalw Rel.thy [wf_def] 
   100     "[| field(r)<=A;  \
   101 \       !!P u. ! x:A. (! y. (y,x): r --> P(y)) --> P(x) ==> P(u) |]  \
   102 \    ==>  wf(r)";
   103 by (rtac (prem1 RS wfI) 1);
   104 by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);
   105 by (Fast_tac 3);
   106 by (Fast_tac 2);
   107 by (Fast_tac 1);
   108 qed "wfI2";
   109