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
```