# HG changeset patch
# User nipkow
# Date 822684339 -3600
# Node ID d0266c81a85e08f76860fa376a8b209924b4a5fb
# Parent  a4896058a47e4857d6be24e9662854b14d9f5728
Streamlined defs in Relation and added new intro/elim rules to do with
pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...

diff -r a4896058a47e -r d0266c81a85e src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Jan 26 13:43:36 1996 +0100
+++ b/src/HOL/Prod.ML	Fri Jan 26 20:25:39 1996 +0100
@@ -122,6 +122,11 @@
 (*These rules are for use with fast_tac.
   Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
 
+goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
+by(split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "splitI2";
+
 goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
 by (Asm_simp_tac 1);
 qed "splitI";
@@ -139,6 +144,11 @@
 by (Asm_simp_tac 1);
 qed "mem_splitI";
 
+goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
+by(split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "mem_splitI2";
+
 val prems = goalw Prod.thy [split_def]
     "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
@@ -258,8 +268,8 @@
 by (rtac (Rep_Unit_inverse RS sym) 1);
 qed "unit_eq";
 
-val prod_cs = set_cs addSIs [SigmaI, mem_splitI] 
+val prod_cs = set_cs addSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2] 
                      addIs  [fst_imageI, snd_imageI, prod_fun_imageI]
-                     addSEs [SigmaE2, SigmaE, mem_splitE, 
+                     addSEs [SigmaE2, SigmaE, splitE, mem_splitE, 
 			     fst_imageE, snd_imageE, prod_fun_imageE,
 			     Pair_inject];
diff -r a4896058a47e -r d0266c81a85e src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Fri Jan 26 13:43:36 1996 +0100
+++ b/src/HOL/Prod.thy	Fri Jan 26 20:25:39 1996 +0100
@@ -50,8 +50,6 @@
 
   "%(x,y,zs).b"   == "split(%x (y,zs).b)"
   "%(x,y).b"      == "split(%x y.b)"
-(* The <= direction fails if split has more than one argument because
-   ast-matching fails. Otherwise it would work fine *)
 
 defs
   Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
@@ -61,8 +59,6 @@
   prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
   Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
 
-
-
 (** Unit **)
 
 subtype (Unit)
@@ -78,31 +74,3 @@
 (* end 8bit 1 *)
 
 end
-(*
-ML
-
-local open Syntax
-
-fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t;
-fun pttrns s t = const"@pttrns" $ s $ t;
-
-fun split2(Abs(x,T,t)) =
-      let val (pats,u) = split1 t
-      in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end
-  | split2(Const("split",_) $ r) =
-      let val (pats,s) = split2(r)
-          val (pats2,t) = split1(s)
-      in (pttrns (pttrn pats) pats2, t) end
-and split1(Abs(x,T,t)) =  (Free(x,T), subst_bounds([free x],t))
-  | split1(Const("split",_)$t) = split2(t);
-
-fun split_tr'(t::args) =
-  let val (pats,ft) = split2(t)
-  in list_comb(const"_lambda" $ pttrn pats $ ft, args) end;
-
-in
-
-val print_translation = [("split", split_tr')];
-
-end;
-*)
diff -r a4896058a47e -r d0266c81a85e src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Fri Jan 26 13:43:36 1996 +0100
+++ b/src/HOL/Relation.ML	Fri Jan 26 20:25:39 1996 +0100
@@ -35,7 +35,7 @@
 
 val prems = goalw Relation.thy [comp_def]
     "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
-by (fast_tac (set_cs addIs prems) 1);
+by (fast_tac (prod_cs addIs prems) 1);
 qed "compI";
 
 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
@@ -44,7 +44,7 @@
 \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
 \    |] ==> P";
 by (cut_facts_tac prems 1);
-by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
+by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 ORELSE ares_tac prems 1));
 qed "compE";
 
 val prems = goal Relation.thy
@@ -84,7 +84,6 @@
 
 goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
 by (Simp_tac 1);
-by (fast_tac set_cs 1);
 qed "converseI";
 
 goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
@@ -97,8 +96,7 @@
 \    |] ==> P"
  (fn [major,minor]=>
   [ (rtac (major RS CollectE) 1),
-    (REPEAT (eresolve_tac [bexE,exE, conjE, minor] 1)),
-    (hyp_subst_tac 1),
+    (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
     (assume_tac 1) ]);
 
 val converse_cs = comp_cs addSIs [converseI] 
diff -r a4896058a47e -r d0266c81a85e src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Jan 26 13:43:36 1996 +0100
+++ b/src/HOL/Relation.thy	Fri Jan 26 20:25:39 1996 +0100
@@ -11,17 +11,16 @@
     id	        :: "('a * 'a)set"               (*the identity relation*)
     O	        :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
     trans       :: "('a * 'a)set => bool" 	(*transitivity predicate*)
-    converse    :: "('a*'a) set => ('a*'a) set"
-    "^^"        :: "[('a*'a) set,'a set] => 'a set" (infixl 90)
-    Domain      :: "('a*'a) set => 'a set"
-    Range       :: "('a*'a) set => 'a set"
+    converse    :: "('a * 'b)set => ('b * 'a)set"
+    "^^"        :: "[('a * 'b) set, 'a set] => 'b set" (infixl 90)
+    Domain      :: "('a * 'b) set => 'a set"
+    Range       :: "('a * 'b) set => 'b set"
 defs
     id_def	"id == {p. ? x. p = (x,x)}"
-    comp_def	(*composition of relations*)
-		"r O s == {xz. ? x y z. xz = (x,z) & (x,y):s & (y,z):r}"
+    comp_def	"r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
     trans_def	  "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
-    converse_def  "converse(r) == {z. (? w:r. ? x y. w=(x,y) & z=(y,x))}"
-    Domain_def    "Domain(r) == {z. ! x. (z=x --> (? y. (x,y):r))}"
+    converse_def  "converse(r) == {(y,x). (x,y):r}"
+    Domain_def    "Domain(r) == {x. ? y. (x,y):r}"
     Range_def     "Range(r) == Domain(converse(r))"
     Image_def     "r ^^ s == {y. y:Range(r) &  (? x:s. (x,y):r)}"
 end