--- a/src/HOL/ex/rel.ML Wed Jun 10 18:07:07 1998 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(* Title: HOL/ex/rel
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Domain, range of a relation or function -- NOT YET WORKING
-*)
-
-structure Rel =
-struct
-val thy = extend_theory Univ.thy "Rel"
-([], [], [], [],
- [
- (["domain"], "('a * 'b)set => 'a set"),
- (["range2"], "('a * 'b)set => 'b set"),
- (["field"], "('a * 'a)set => 'a set")
- ],
- None)
- [
- ("domain_def", "domain(r) == {a. ? b. (a,b) : r}" ),
- ("range2_def", "range2(r) == {b. ? a. (a,b) : r}" ),
- ("field_def", "field(r) == domain(r) Un range2(r)" )
- ];
-end;
-
-local val ax = get_axiom Rel.thy
-in
-val domain_def = ax"domain_def";
-val range2_def = ax"range2_def";
-val field_def = ax"field_def";
-end;
-
-
-(*** domain ***)
-
-val [prem] = goalw Rel.thy [domain_def,Pair_def] "(a,b): r ==> a : domain(r)";
-by (fast_tac (claset() addIs [prem]) 1);
-qed "domainI";
-
-val major::prems = goalw Rel.thy [domain_def]
- "[| a : domain(r); !!y. (a,y): r ==> P |] ==> P";
-by (rtac (major RS CollectE) 1);
-by (etac exE 1);
-by (REPEAT (ares_tac prems 1));
-qed "domainE";
-
-
-(*** range2 ***)
-
-val [prem] = goalw Rel.thy [range2_def,Pair_def] "(a,b): r ==> b : range2(r)";
-by (fast_tac (claset() addIs [prem]) 1);
-qed "range2I";
-
-val major::prems = goalw Rel.thy [range2_def]
- "[| b : range2(r); !!x. (x,b): r ==> P |] ==> P";
-by (rtac (major RS CollectE) 1);
-by (etac exE 1);
-by (REPEAT (ares_tac prems 1));
-qed "range2E";
-
-
-(*** field ***)
-
-val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> a : field(r)";
-by (rtac (prem RS domainI RS UnI1) 1);
-qed "fieldI1";
-
-val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> b : field(r)";
-by (rtac (prem RS range2I RS UnI2) 1);
-qed "fieldI2";
-
-val [prem] = goalw Rel.thy [field_def]
- "(~ (c,a):r ==> (a,b): r) ==> a : field(r)";
-by (rtac (prem RS domainI RS UnCI) 1);
-by (swap_res_tac [range2I] 1);
-by (etac notnotD 1);
-qed "fieldCI";
-
-val major::prems = goalw Rel.thy [field_def]
- "[| a : field(r); \
-\ !!x. (a,x): r ==> P; \
-\ !!x. (x,a): r ==> P |] ==> P";
-by (rtac (major RS UnE) 1);
-by (REPEAT (eresolve_tac (prems@[domainE,range2E]) 1));
-qed "fieldE";
-
-goalw Rel.thy [field_def] "domain(r) <= field(r)";
-by (rtac Un_upper1 1);
-qed "domain_in_field";
-
-goalw Rel.thy [field_def] "range2(r) <= field(r)";
-by (rtac Un_upper2 1);
-qed "range2_in_field";
-
-
-????????????????????????????????????????????????????????????????;
-
-(*If r allows well-founded induction then wf(r)*)
-val [prem1,prem2] = goalw Rel.thy [wf_def]
- "[| field(r)<=A; \
-\ !!P u. ! x:A. (! y. (y,x): r --> P(y)) --> P(x) ==> P(u) |] \
-\ ==> wf(r)";
-by (rtac (prem1 RS wfI) 1);
-by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);
-by (Fast_tac 3);
-by (Fast_tac 2);
-by (Fast_tac 1);
-qed "wfI2";
-