Streamlined defs in Relation and added new intro/elim rules to do with
authornipkow
Fri Jan 26 20:25:39 1996 +0100 (1996-01-26)
changeset 1454d0266c81a85e
parent 1453 a4896058a47e
child 1455 52a0271621f3
Streamlined defs in Relation and added new intro/elim rules to do with
pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...
src/HOL/Prod.ML
src/HOL/Prod.thy
src/HOL/Relation.ML
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Prod.ML	Fri Jan 26 13:43:36 1996 +0100
     1.2 +++ b/src/HOL/Prod.ML	Fri Jan 26 20:25:39 1996 +0100
     1.3 @@ -122,6 +122,11 @@
     1.4  (*These rules are for use with fast_tac.
     1.5    Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
     1.6  
     1.7 +goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
     1.8 +by(split_all_tac 1);
     1.9 +by (Asm_simp_tac 1);
    1.10 +qed "splitI2";
    1.11 +
    1.12  goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
    1.13  by (Asm_simp_tac 1);
    1.14  qed "splitI";
    1.15 @@ -139,6 +144,11 @@
    1.16  by (Asm_simp_tac 1);
    1.17  qed "mem_splitI";
    1.18  
    1.19 +goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
    1.20 +by(split_all_tac 1);
    1.21 +by (Asm_simp_tac 1);
    1.22 +qed "mem_splitI2";
    1.23 +
    1.24  val prems = goalw Prod.thy [split_def]
    1.25      "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
    1.26  by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
    1.27 @@ -258,8 +268,8 @@
    1.28  by (rtac (Rep_Unit_inverse RS sym) 1);
    1.29  qed "unit_eq";
    1.30  
    1.31 -val prod_cs = set_cs addSIs [SigmaI, mem_splitI] 
    1.32 +val prod_cs = set_cs addSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2] 
    1.33                       addIs  [fst_imageI, snd_imageI, prod_fun_imageI]
    1.34 -                     addSEs [SigmaE2, SigmaE, mem_splitE, 
    1.35 +                     addSEs [SigmaE2, SigmaE, splitE, mem_splitE, 
    1.36  			     fst_imageE, snd_imageE, prod_fun_imageE,
    1.37  			     Pair_inject];
     2.1 --- a/src/HOL/Prod.thy	Fri Jan 26 13:43:36 1996 +0100
     2.2 +++ b/src/HOL/Prod.thy	Fri Jan 26 20:25:39 1996 +0100
     2.3 @@ -50,8 +50,6 @@
     2.4  
     2.5    "%(x,y,zs).b"   == "split(%x (y,zs).b)"
     2.6    "%(x,y).b"      == "split(%x y.b)"
     2.7 -(* The <= direction fails if split has more than one argument because
     2.8 -   ast-matching fails. Otherwise it would work fine *)
     2.9  
    2.10  defs
    2.11    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    2.12 @@ -61,8 +59,6 @@
    2.13    prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
    2.14    Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    2.15  
    2.16 -
    2.17 -
    2.18  (** Unit **)
    2.19  
    2.20  subtype (Unit)
    2.21 @@ -78,31 +74,3 @@
    2.22  (* end 8bit 1 *)
    2.23  
    2.24  end
    2.25 -(*
    2.26 -ML
    2.27 -
    2.28 -local open Syntax
    2.29 -
    2.30 -fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t;
    2.31 -fun pttrns s t = const"@pttrns" $ s $ t;
    2.32 -
    2.33 -fun split2(Abs(x,T,t)) =
    2.34 -      let val (pats,u) = split1 t
    2.35 -      in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end
    2.36 -  | split2(Const("split",_) $ r) =
    2.37 -      let val (pats,s) = split2(r)
    2.38 -          val (pats2,t) = split1(s)
    2.39 -      in (pttrns (pttrn pats) pats2, t) end
    2.40 -and split1(Abs(x,T,t)) =  (Free(x,T), subst_bounds([free x],t))
    2.41 -  | split1(Const("split",_)$t) = split2(t);
    2.42 -
    2.43 -fun split_tr'(t::args) =
    2.44 -  let val (pats,ft) = split2(t)
    2.45 -  in list_comb(const"_lambda" $ pttrn pats $ ft, args) end;
    2.46 -
    2.47 -in
    2.48 -
    2.49 -val print_translation = [("split", split_tr')];
    2.50 -
    2.51 -end;
    2.52 -*)
     3.1 --- a/src/HOL/Relation.ML	Fri Jan 26 13:43:36 1996 +0100
     3.2 +++ b/src/HOL/Relation.ML	Fri Jan 26 20:25:39 1996 +0100
     3.3 @@ -35,7 +35,7 @@
     3.4  
     3.5  val prems = goalw Relation.thy [comp_def]
     3.6      "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
     3.7 -by (fast_tac (set_cs addIs prems) 1);
     3.8 +by (fast_tac (prod_cs addIs prems) 1);
     3.9  qed "compI";
    3.10  
    3.11  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    3.12 @@ -44,7 +44,7 @@
    3.13  \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
    3.14  \    |] ==> P";
    3.15  by (cut_facts_tac prems 1);
    3.16 -by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
    3.17 +by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 ORELSE ares_tac prems 1));
    3.18  qed "compE";
    3.19  
    3.20  val prems = goal Relation.thy
    3.21 @@ -84,7 +84,6 @@
    3.22  
    3.23  goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
    3.24  by (Simp_tac 1);
    3.25 -by (fast_tac set_cs 1);
    3.26  qed "converseI";
    3.27  
    3.28  goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
    3.29 @@ -97,8 +96,7 @@
    3.30  \    |] ==> P"
    3.31   (fn [major,minor]=>
    3.32    [ (rtac (major RS CollectE) 1),
    3.33 -    (REPEAT (eresolve_tac [bexE,exE, conjE, minor] 1)),
    3.34 -    (hyp_subst_tac 1),
    3.35 +    (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
    3.36      (assume_tac 1) ]);
    3.37  
    3.38  val converse_cs = comp_cs addSIs [converseI] 
     4.1 --- a/src/HOL/Relation.thy	Fri Jan 26 13:43:36 1996 +0100
     4.2 +++ b/src/HOL/Relation.thy	Fri Jan 26 20:25:39 1996 +0100
     4.3 @@ -11,17 +11,16 @@
     4.4      id	        :: "('a * 'a)set"               (*the identity relation*)
     4.5      O	        :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
     4.6      trans       :: "('a * 'a)set => bool" 	(*transitivity predicate*)
     4.7 -    converse    :: "('a*'a) set => ('a*'a) set"
     4.8 -    "^^"        :: "[('a*'a) set,'a set] => 'a set" (infixl 90)
     4.9 -    Domain      :: "('a*'a) set => 'a set"
    4.10 -    Range       :: "('a*'a) set => 'a set"
    4.11 +    converse    :: "('a * 'b)set => ('b * 'a)set"
    4.12 +    "^^"        :: "[('a * 'b) set, 'a set] => 'b set" (infixl 90)
    4.13 +    Domain      :: "('a * 'b) set => 'a set"
    4.14 +    Range       :: "('a * 'b) set => 'b set"
    4.15  defs
    4.16      id_def	"id == {p. ? x. p = (x,x)}"
    4.17 -    comp_def	(*composition of relations*)
    4.18 -		"r O s == {xz. ? x y z. xz = (x,z) & (x,y):s & (y,z):r}"
    4.19 +    comp_def	"r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    4.20      trans_def	  "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
    4.21 -    converse_def  "converse(r) == {z. (? w:r. ? x y. w=(x,y) & z=(y,x))}"
    4.22 -    Domain_def    "Domain(r) == {z. ! x. (z=x --> (? y. (x,y):r))}"
    4.23 +    converse_def  "converse(r) == {(y,x). (x,y):r}"
    4.24 +    Domain_def    "Domain(r) == {x. ? y. (x,y):r}"
    4.25      Range_def     "Range(r) == Domain(converse(r))"
    4.26      Image_def     "r ^^ s == {y. y:Range(r) &  (? x:s. (x,y):r)}"
    4.27  end