src/HOL/Prod.ML
author nipkow
Mon Feb 19 18:04:41 1996 +0100 (1996-02-19)
changeset 1515 4ed79ebab64d
parent 1485 240cc98b94a7
child 1552 6f71b5d46700
permissions -rw-r--r--
Introduced normalize_thm into HOL.ML

Corrected some dependencies among Sum, Prod and mono.

Extended RelPow
clasohm@1465
     1
(*  Title:      HOL/prod
clasohm@923
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1991  University of Cambridge
clasohm@923
     5
clasohm@923
     6
For prod.thy.  Ordered Pairs, the Cartesian product type, the unit type
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
open Prod;
clasohm@923
    10
clasohm@923
    11
(*This counts as a non-emptiness result for admitting 'a * 'b as a type*)
clasohm@923
    12
goalw Prod.thy [Prod_def] "Pair_Rep a b : Prod";
clasohm@923
    13
by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
clasohm@923
    14
qed "ProdI";
clasohm@923
    15
clasohm@923
    16
val [major] = goalw Prod.thy [Pair_Rep_def]
clasohm@923
    17
    "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
clasohm@923
    18
by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), 
clasohm@1465
    19
            rtac conjI, rtac refl, rtac refl]);
clasohm@923
    20
qed "Pair_Rep_inject";
clasohm@923
    21
clasohm@923
    22
goal Prod.thy "inj_onto Abs_Prod Prod";
clasohm@923
    23
by (rtac inj_onto_inverseI 1);
clasohm@923
    24
by (etac Abs_Prod_inverse 1);
clasohm@923
    25
qed "inj_onto_Abs_Prod";
clasohm@923
    26
clasohm@923
    27
val prems = goalw Prod.thy [Pair_def]
clasohm@972
    28
    "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
clasohm@923
    29
by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1);
clasohm@923
    30
by (REPEAT (ares_tac (prems@[ProdI]) 1));
clasohm@923
    31
qed "Pair_inject";
clasohm@923
    32
clasohm@972
    33
goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
clasohm@923
    34
by (fast_tac (set_cs addIs [Pair_inject]) 1);
clasohm@923
    35
qed "Pair_eq";
clasohm@923
    36
clasohm@972
    37
goalw Prod.thy [fst_def] "fst((a,b)) = a";
clasohm@923
    38
by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1);
clasohm@923
    39
qed "fst_conv";
clasohm@923
    40
clasohm@972
    41
goalw Prod.thy [snd_def] "snd((a,b)) = b";
clasohm@923
    42
by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1);
clasohm@923
    43
qed "snd_conv";
clasohm@923
    44
clasohm@972
    45
goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
clasohm@923
    46
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
clasohm@923
    47
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
clasohm@1465
    48
           rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
clasohm@923
    49
qed "PairE_lemma";
clasohm@923
    50
clasohm@972
    51
val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
clasohm@923
    52
by (rtac (PairE_lemma RS exE) 1);
clasohm@923
    53
by (REPEAT (eresolve_tac [prem,exE] 1));
clasohm@923
    54
qed "PairE";
clasohm@923
    55
nipkow@1301
    56
(* replace parameters of product type by individual component parameters *)
nipkow@1301
    57
local
nipkow@1301
    58
fun is_pair (_,Type("*",_)) = true
nipkow@1301
    59
  | is_pair _ = false;
nipkow@1301
    60
nipkow@1301
    61
fun find_pair_param t =
nipkow@1301
    62
  let val params = Logic.strip_params t
nipkow@1301
    63
  in if exists is_pair params
nipkow@1301
    64
     then let val params = rev(rename_wrt_term t params)
nipkow@1301
    65
                           (*as they are printed*)
nipkow@1301
    66
          in apsome fst (find_first is_pair params) end
nipkow@1301
    67
     else None
nipkow@1301
    68
  end;
nipkow@1301
    69
nipkow@1301
    70
in
nipkow@1301
    71
nipkow@1301
    72
val split_all_tac = REPEAT o SUBGOAL (fn (t,_) =>
nipkow@1301
    73
  case find_pair_param t of
nipkow@1301
    74
    None => no_tac
nipkow@1301
    75
  | Some x => EVERY[res_inst_tac[("p",x)] PairE 1,
nipkow@1301
    76
                    REPEAT(hyp_subst_tac 1), prune_params_tac]);
nipkow@1301
    77
nipkow@1301
    78
end;
nipkow@1301
    79
nipkow@1301
    80
goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
nipkow@1301
    81
by(fast_tac (HOL_cs addbefore split_all_tac 1) 1);
nipkow@1301
    82
qed "split_paired_All";
nipkow@1301
    83
clasohm@972
    84
goalw Prod.thy [split_def] "split c (a,b) = c a b";
nipkow@1485
    85
by (EVERY1[stac fst_conv, stac snd_conv]);
clasohm@923
    86
by (rtac refl 1);
clasohm@923
    87
qed "split";
clasohm@923
    88
nipkow@1301
    89
Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq];
clasohm@923
    90
clasohm@923
    91
goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
clasohm@923
    92
by (res_inst_tac[("p","s")] PairE 1);
clasohm@923
    93
by (res_inst_tac[("p","t")] PairE 1);
clasohm@1264
    94
by (Asm_simp_tac 1);
clasohm@923
    95
qed "Pair_fst_snd_eq";
clasohm@923
    96
clasohm@923
    97
(*Prevents simplification of c: much faster*)
clasohm@923
    98
qed_goal "split_weak_cong" Prod.thy
clasohm@923
    99
  "p=q ==> split c p = split c q"
clasohm@923
   100
  (fn [prem] => [rtac (prem RS arg_cong) 1]);
clasohm@923
   101
clasohm@923
   102
(* Do not add as rewrite rule: invalidates some proofs in IMP *)
clasohm@972
   103
goal Prod.thy "p = (fst(p),snd(p))";
clasohm@923
   104
by (res_inst_tac [("p","p")] PairE 1);
clasohm@1264
   105
by (Asm_simp_tac 1);
clasohm@923
   106
qed "surjective_pairing";
clasohm@923
   107
clasohm@972
   108
goal Prod.thy "p = split (%x y.(x,y)) p";
clasohm@923
   109
by (res_inst_tac [("p","p")] PairE 1);
clasohm@1264
   110
by (Asm_simp_tac 1);
clasohm@923
   111
qed "surjective_pairing2";
clasohm@923
   112
clasohm@923
   113
(*For use with split_tac and the simplifier*)
clasohm@972
   114
goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
clasohm@923
   115
by (stac surjective_pairing 1);
clasohm@923
   116
by (stac split 1);
clasohm@923
   117
by (fast_tac (HOL_cs addSEs [Pair_inject]) 1);
clasohm@923
   118
qed "expand_split";
clasohm@923
   119
clasohm@923
   120
(** split used as a logical connective or set former **)
clasohm@923
   121
clasohm@923
   122
(*These rules are for use with fast_tac.
clasohm@923
   123
  Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
clasohm@923
   124
nipkow@1454
   125
goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
nipkow@1454
   126
by(split_all_tac 1);
nipkow@1454
   127
by (Asm_simp_tac 1);
nipkow@1454
   128
qed "splitI2";
nipkow@1454
   129
clasohm@972
   130
goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
clasohm@1264
   131
by (Asm_simp_tac 1);
clasohm@923
   132
qed "splitI";
clasohm@923
   133
clasohm@923
   134
val prems = goalw Prod.thy [split_def]
clasohm@972
   135
    "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
clasohm@923
   136
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
clasohm@923
   137
qed "splitE";
clasohm@923
   138
clasohm@972
   139
goal Prod.thy "!!R a b. split R (a,b) ==> R a b";
clasohm@923
   140
by (etac (split RS iffD1) 1);
clasohm@923
   141
qed "splitD";
clasohm@923
   142
clasohm@972
   143
goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)";
clasohm@1264
   144
by (Asm_simp_tac 1);
clasohm@923
   145
qed "mem_splitI";
clasohm@923
   146
nipkow@1454
   147
goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
nipkow@1454
   148
by(split_all_tac 1);
nipkow@1454
   149
by (Asm_simp_tac 1);
nipkow@1454
   150
qed "mem_splitI2";
nipkow@1454
   151
clasohm@923
   152
val prems = goalw Prod.thy [split_def]
clasohm@972
   153
    "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
clasohm@923
   154
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
clasohm@923
   155
qed "mem_splitE";
clasohm@923
   156
clasohm@923
   157
(*** prod_fun -- action of the product functor upon functions ***)
clasohm@923
   158
clasohm@972
   159
goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
clasohm@923
   160
by (rtac split 1);
clasohm@923
   161
qed "prod_fun";
clasohm@923
   162
clasohm@923
   163
goal Prod.thy 
clasohm@923
   164
    "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
clasohm@923
   165
by (rtac ext 1);
clasohm@923
   166
by (res_inst_tac [("p","x")] PairE 1);
clasohm@1264
   167
by (asm_simp_tac (!simpset addsimps [prod_fun,o_def]) 1);
clasohm@923
   168
qed "prod_fun_compose";
clasohm@923
   169
clasohm@923
   170
goal Prod.thy "prod_fun (%x.x) (%y.y) = (%z.z)";
clasohm@923
   171
by (rtac ext 1);
clasohm@923
   172
by (res_inst_tac [("p","z")] PairE 1);
clasohm@1264
   173
by (asm_simp_tac (!simpset addsimps [prod_fun]) 1);
clasohm@923
   174
qed "prod_fun_ident";
clasohm@923
   175
clasohm@972
   176
val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
clasohm@923
   177
by (rtac image_eqI 1);
clasohm@923
   178
by (rtac (prod_fun RS sym) 1);
clasohm@923
   179
by (resolve_tac prems 1);
clasohm@923
   180
qed "prod_fun_imageI";
clasohm@923
   181
clasohm@923
   182
val major::prems = goal Prod.thy
clasohm@972
   183
    "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
clasohm@923
   184
\    |] ==> P";
clasohm@923
   185
by (rtac (major RS imageE) 1);
clasohm@923
   186
by (res_inst_tac [("p","x")] PairE 1);
clasohm@923
   187
by (resolve_tac prems 1);
clasohm@923
   188
by (fast_tac HOL_cs 2);
clasohm@923
   189
by (fast_tac (HOL_cs addIs [prod_fun]) 1);
clasohm@923
   190
qed "prod_fun_imageE";
clasohm@923
   191
clasohm@923
   192
(*** Disjoint union of a family of sets - Sigma ***)
clasohm@923
   193
clasohm@923
   194
qed_goalw "SigmaI" Prod.thy [Sigma_def]
clasohm@972
   195
    "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
clasohm@923
   196
 (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
clasohm@923
   197
clasohm@923
   198
(*The general elimination rule*)
clasohm@923
   199
qed_goalw "SigmaE" Prod.thy [Sigma_def]
clasohm@923
   200
    "[| c: Sigma A B;  \
clasohm@972
   201
\       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
clasohm@923
   202
\    |] ==> P"
clasohm@923
   203
 (fn major::prems=>
clasohm@923
   204
  [ (cut_facts_tac [major] 1),
clasohm@923
   205
    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
clasohm@923
   206
clasohm@972
   207
(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
clasohm@972
   208
qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A"
clasohm@923
   209
 (fn [major]=>
clasohm@923
   210
  [ (rtac (major RS SigmaE) 1),
clasohm@923
   211
    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
clasohm@923
   212
clasohm@972
   213
qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)"
clasohm@923
   214
 (fn [major]=>
clasohm@923
   215
  [ (rtac (major RS SigmaE) 1),
clasohm@923
   216
    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
clasohm@923
   217
clasohm@923
   218
qed_goal "SigmaE2" Prod.thy
clasohm@972
   219
    "[| (a,b) : Sigma A B;    \
clasohm@923
   220
\       [| a:A;  b:B(a) |] ==> P   \
clasohm@923
   221
\    |] ==> P"
clasohm@923
   222
 (fn [major,minor]=>
clasohm@923
   223
  [ (rtac minor 1),
clasohm@923
   224
    (rtac (major RS SigmaD1) 1),
clasohm@923
   225
    (rtac (major RS SigmaD2) 1) ]);
clasohm@923
   226
nipkow@1515
   227
val prems = goal Prod.thy
nipkow@1515
   228
    "[| A<=C;  !!x. x:A ==> B<=D |] ==> Sigma A (%x.B) <= Sigma C (%x.D)";
nipkow@1515
   229
by (cut_facts_tac prems 1);
nipkow@1515
   230
by (fast_tac (set_cs addIs (prems RL [subsetD]) 
nipkow@1515
   231
                     addSIs [SigmaI] 
nipkow@1515
   232
                     addSEs [SigmaE]) 1);
nipkow@1515
   233
qed "Sigma_mono";
nipkow@1515
   234
nipkow@1515
   235
clasohm@923
   236
(*** Domain of a relation ***)
clasohm@923
   237
clasohm@972
   238
val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";
clasohm@923
   239
by (rtac CollectI 1);
clasohm@923
   240
by (rtac bexI 1);
clasohm@923
   241
by (rtac (fst_conv RS sym) 1);
clasohm@923
   242
by (resolve_tac prems 1);
clasohm@923
   243
qed "fst_imageI";
clasohm@923
   244
clasohm@923
   245
val major::prems = goal Prod.thy
clasohm@972
   246
    "[| a : fst``r;  !!y.[| (a,y) : r |] ==> P |] ==> P"; 
clasohm@923
   247
by (rtac (major RS imageE) 1);
clasohm@923
   248
by (resolve_tac prems 1);
clasohm@923
   249
by (etac ssubst 1);
clasohm@923
   250
by (rtac (surjective_pairing RS subst) 1);
clasohm@923
   251
by (assume_tac 1);
clasohm@923
   252
qed "fst_imageE";
clasohm@923
   253
clasohm@923
   254
(*** Range of a relation ***)
clasohm@923
   255
clasohm@972
   256
val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r";
clasohm@923
   257
by (rtac CollectI 1);
clasohm@923
   258
by (rtac bexI 1);
clasohm@923
   259
by (rtac (snd_conv RS sym) 1);
clasohm@923
   260
by (resolve_tac prems 1);
clasohm@923
   261
qed "snd_imageI";
clasohm@923
   262
clasohm@923
   263
val major::prems = goal Prod.thy
clasohm@972
   264
    "[| a : snd``r;  !!y.[| (y,a) : r |] ==> P |] ==> P"; 
clasohm@923
   265
by (rtac (major RS imageE) 1);
clasohm@923
   266
by (resolve_tac prems 1);
clasohm@923
   267
by (etac ssubst 1);
clasohm@923
   268
by (rtac (surjective_pairing RS subst) 1);
clasohm@923
   269
by (assume_tac 1);
clasohm@923
   270
qed "snd_imageE";
clasohm@923
   271
clasohm@923
   272
(** Exhaustion rule for unit -- a degenerate form of induction **)
clasohm@923
   273
clasohm@923
   274
goalw Prod.thy [Unity_def]
clasohm@972
   275
    "u = ()";
clasohm@923
   276
by (stac (rewrite_rule [Unit_def] Rep_Unit RS CollectD RS sym) 1);
clasohm@923
   277
by (rtac (Rep_Unit_inverse RS sym) 1);
clasohm@923
   278
qed "unit_eq";
clasohm@923
   279
nipkow@1454
   280
val prod_cs = set_cs addSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2] 
clasohm@923
   281
                     addIs  [fst_imageI, snd_imageI, prod_fun_imageI]
nipkow@1454
   282
                     addSEs [SigmaE2, SigmaE, splitE, mem_splitE, 
clasohm@1465
   283
                             fst_imageE, snd_imageE, prod_fun_imageE,
clasohm@1465
   284
                             Pair_inject];