src/HOL/Prod.ML
author nipkow
Thu Apr 03 19:29:53 1997 +0200 (1997-04-03)
changeset 2886 fd5645efa43d
parent 2880 a0fde30aa126
child 2935 998cb95fdd43
permissions -rw-r--r--
Now: unit = {True}
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
paulson@2856
    33
AddSEs [Pair_inject];
paulson@2856
    34
clasohm@972
    35
goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
paulson@2856
    36
by (Fast_tac 1);
clasohm@923
    37
qed "Pair_eq";
clasohm@923
    38
clasohm@972
    39
goalw Prod.thy [fst_def] "fst((a,b)) = a";
paulson@2856
    40
by (fast_tac (!claset addIs [select_equality]) 1);
clasohm@923
    41
qed "fst_conv";
clasohm@923
    42
clasohm@972
    43
goalw Prod.thy [snd_def] "snd((a,b)) = b";
paulson@2856
    44
by (fast_tac (!claset addIs [select_equality]) 1);
clasohm@923
    45
qed "snd_conv";
clasohm@923
    46
clasohm@972
    47
goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
clasohm@923
    48
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
clasohm@923
    49
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
clasohm@1465
    50
           rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
clasohm@923
    51
qed "PairE_lemma";
clasohm@923
    52
clasohm@972
    53
val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
clasohm@923
    54
by (rtac (PairE_lemma RS exE) 1);
clasohm@923
    55
by (REPEAT (eresolve_tac [prem,exE] 1));
clasohm@923
    56
qed "PairE";
clasohm@923
    57
nipkow@1301
    58
(* replace parameters of product type by individual component parameters *)
nipkow@1301
    59
local
nipkow@1301
    60
fun is_pair (_,Type("*",_)) = true
nipkow@1301
    61
  | is_pair _ = false;
nipkow@1301
    62
paulson@1727
    63
fun find_pair_param prem =
paulson@1727
    64
  let val params = Logic.strip_params prem
nipkow@1301
    65
  in if exists is_pair params
paulson@1727
    66
     then let val params = rev(rename_wrt_term prem params)
nipkow@1301
    67
                           (*as they are printed*)
nipkow@1301
    68
          in apsome fst (find_first is_pair params) end
nipkow@1301
    69
     else None
nipkow@1301
    70
  end;
nipkow@1301
    71
nipkow@1301
    72
in
nipkow@1301
    73
paulson@1727
    74
val split_all_tac = REPEAT o SUBGOAL (fn (prem,i) =>
paulson@1727
    75
  case find_pair_param prem of
nipkow@1301
    76
    None => no_tac
paulson@1727
    77
  | Some x => EVERY[res_inst_tac[("p",x)] PairE i,
paulson@1727
    78
                    REPEAT(hyp_subst_tac i), prune_params_tac]);
nipkow@1301
    79
nipkow@1301
    80
end;
nipkow@1301
    81
nipkow@1301
    82
goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
oheimb@2637
    83
by (fast_tac (!claset addbefore split_all_tac) 1);
nipkow@1301
    84
qed "split_paired_All";
nipkow@1301
    85
clasohm@972
    86
goalw Prod.thy [split_def] "split c (a,b) = c a b";
nipkow@1485
    87
by (EVERY1[stac fst_conv, stac snd_conv]);
clasohm@923
    88
by (rtac refl 1);
clasohm@923
    89
qed "split";
clasohm@923
    90
nipkow@1301
    91
Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq];
clasohm@923
    92
clasohm@923
    93
goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
clasohm@923
    94
by (res_inst_tac[("p","s")] PairE 1);
clasohm@923
    95
by (res_inst_tac[("p","t")] PairE 1);
clasohm@1264
    96
by (Asm_simp_tac 1);
clasohm@923
    97
qed "Pair_fst_snd_eq";
clasohm@923
    98
clasohm@923
    99
(*Prevents simplification of c: much faster*)
clasohm@923
   100
qed_goal "split_weak_cong" Prod.thy
clasohm@923
   101
  "p=q ==> split c p = split c q"
clasohm@923
   102
  (fn [prem] => [rtac (prem RS arg_cong) 1]);
clasohm@923
   103
clasohm@923
   104
(* Do not add as rewrite rule: invalidates some proofs in IMP *)
clasohm@972
   105
goal Prod.thy "p = (fst(p),snd(p))";
clasohm@923
   106
by (res_inst_tac [("p","p")] PairE 1);
clasohm@1264
   107
by (Asm_simp_tac 1);
clasohm@923
   108
qed "surjective_pairing";
clasohm@923
   109
clasohm@972
   110
goal Prod.thy "p = split (%x y.(x,y)) p";
clasohm@923
   111
by (res_inst_tac [("p","p")] PairE 1);
clasohm@1264
   112
by (Asm_simp_tac 1);
clasohm@923
   113
qed "surjective_pairing2";
clasohm@923
   114
nipkow@1655
   115
qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
nipkow@1655
   116
  (fn _ => [rtac ext 1, split_all_tac 1, rtac split 1]);
nipkow@1655
   117
clasohm@923
   118
(*For use with split_tac and the simplifier*)
clasohm@972
   119
goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
clasohm@923
   120
by (stac surjective_pairing 1);
clasohm@923
   121
by (stac split 1);
paulson@2856
   122
by (Fast_tac 1);
clasohm@923
   123
qed "expand_split";
clasohm@923
   124
clasohm@923
   125
(** split used as a logical connective or set former **)
clasohm@923
   126
clasohm@923
   127
(*These rules are for use with fast_tac.
clasohm@923
   128
  Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
clasohm@923
   129
nipkow@1454
   130
goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
paulson@1552
   131
by (split_all_tac 1);
nipkow@1454
   132
by (Asm_simp_tac 1);
nipkow@1454
   133
qed "splitI2";
nipkow@1454
   134
clasohm@972
   135
goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
clasohm@1264
   136
by (Asm_simp_tac 1);
clasohm@923
   137
qed "splitI";
clasohm@923
   138
clasohm@923
   139
val prems = goalw Prod.thy [split_def]
clasohm@972
   140
    "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
clasohm@923
   141
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
clasohm@923
   142
qed "splitE";
clasohm@923
   143
clasohm@972
   144
goal Prod.thy "!!R a b. split R (a,b) ==> R a b";
clasohm@923
   145
by (etac (split RS iffD1) 1);
clasohm@923
   146
qed "splitD";
clasohm@923
   147
clasohm@972
   148
goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)";
clasohm@1264
   149
by (Asm_simp_tac 1);
clasohm@923
   150
qed "mem_splitI";
clasohm@923
   151
nipkow@1454
   152
goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
paulson@1552
   153
by (split_all_tac 1);
nipkow@1454
   154
by (Asm_simp_tac 1);
nipkow@1454
   155
qed "mem_splitI2";
nipkow@1454
   156
clasohm@923
   157
val prems = goalw Prod.thy [split_def]
clasohm@972
   158
    "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
clasohm@923
   159
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
clasohm@923
   160
qed "mem_splitE";
clasohm@923
   161
paulson@2856
   162
AddSIs [splitI, splitI2, mem_splitI, mem_splitI2];
paulson@2856
   163
AddSEs [splitE, mem_splitE];
paulson@2856
   164
clasohm@923
   165
(*** prod_fun -- action of the product functor upon functions ***)
clasohm@923
   166
clasohm@972
   167
goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
clasohm@923
   168
by (rtac split 1);
clasohm@923
   169
qed "prod_fun";
clasohm@923
   170
clasohm@923
   171
goal Prod.thy 
clasohm@923
   172
    "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
clasohm@923
   173
by (rtac ext 1);
clasohm@923
   174
by (res_inst_tac [("p","x")] PairE 1);
clasohm@1264
   175
by (asm_simp_tac (!simpset addsimps [prod_fun,o_def]) 1);
clasohm@923
   176
qed "prod_fun_compose";
clasohm@923
   177
clasohm@923
   178
goal Prod.thy "prod_fun (%x.x) (%y.y) = (%z.z)";
clasohm@923
   179
by (rtac ext 1);
clasohm@923
   180
by (res_inst_tac [("p","z")] PairE 1);
clasohm@1264
   181
by (asm_simp_tac (!simpset addsimps [prod_fun]) 1);
clasohm@923
   182
qed "prod_fun_ident";
clasohm@923
   183
clasohm@972
   184
val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
clasohm@923
   185
by (rtac image_eqI 1);
clasohm@923
   186
by (rtac (prod_fun RS sym) 1);
clasohm@923
   187
by (resolve_tac prems 1);
clasohm@923
   188
qed "prod_fun_imageI";
clasohm@923
   189
clasohm@923
   190
val major::prems = goal Prod.thy
clasohm@972
   191
    "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
clasohm@923
   192
\    |] ==> P";
clasohm@923
   193
by (rtac (major RS imageE) 1);
clasohm@923
   194
by (res_inst_tac [("p","x")] PairE 1);
clasohm@923
   195
by (resolve_tac prems 1);
berghofe@1754
   196
by (Fast_tac 2);
berghofe@1754
   197
by (fast_tac (!claset addIs [prod_fun]) 1);
clasohm@923
   198
qed "prod_fun_imageE";
clasohm@923
   199
clasohm@923
   200
(*** Disjoint union of a family of sets - Sigma ***)
clasohm@923
   201
clasohm@923
   202
qed_goalw "SigmaI" Prod.thy [Sigma_def]
clasohm@972
   203
    "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
clasohm@923
   204
 (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
clasohm@923
   205
paulson@2856
   206
AddSIs [SigmaI];
paulson@2856
   207
clasohm@923
   208
(*The general elimination rule*)
clasohm@923
   209
qed_goalw "SigmaE" Prod.thy [Sigma_def]
clasohm@923
   210
    "[| c: Sigma A B;  \
clasohm@972
   211
\       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
clasohm@923
   212
\    |] ==> P"
clasohm@923
   213
 (fn major::prems=>
clasohm@923
   214
  [ (cut_facts_tac [major] 1),
clasohm@923
   215
    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
clasohm@923
   216
clasohm@972
   217
(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
clasohm@972
   218
qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A"
clasohm@923
   219
 (fn [major]=>
clasohm@923
   220
  [ (rtac (major RS SigmaE) 1),
clasohm@923
   221
    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
clasohm@923
   222
clasohm@972
   223
qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)"
clasohm@923
   224
 (fn [major]=>
clasohm@923
   225
  [ (rtac (major RS SigmaE) 1),
clasohm@923
   226
    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
clasohm@923
   227
clasohm@923
   228
qed_goal "SigmaE2" Prod.thy
clasohm@972
   229
    "[| (a,b) : Sigma A B;    \
clasohm@923
   230
\       [| a:A;  b:B(a) |] ==> P   \
clasohm@923
   231
\    |] ==> P"
clasohm@923
   232
 (fn [major,minor]=>
clasohm@923
   233
  [ (rtac minor 1),
clasohm@923
   234
    (rtac (major RS SigmaD1) 1),
clasohm@923
   235
    (rtac (major RS SigmaD2) 1) ]);
clasohm@923
   236
paulson@2856
   237
AddSEs [SigmaE2, SigmaE];
paulson@2856
   238
nipkow@1515
   239
val prems = goal Prod.thy
paulson@1642
   240
    "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
nipkow@1515
   241
by (cut_facts_tac prems 1);
paulson@2856
   242
by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
nipkow@1515
   243
qed "Sigma_mono";
nipkow@1515
   244
paulson@1618
   245
qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
paulson@2856
   246
 (fn _ => [ (Fast_tac 1) ]);
paulson@1618
   247
paulson@1642
   248
qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
paulson@2856
   249
 (fn _ => [ (Fast_tac 1) ]);
paulson@1618
   250
paulson@1618
   251
Addsimps [Sigma_empty1,Sigma_empty2]; 
paulson@1618
   252
paulson@1618
   253
goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
paulson@2856
   254
by (Fast_tac 1);
paulson@1618
   255
qed "mem_Sigma_iff";
paulson@1618
   256
Addsimps [mem_Sigma_iff]; 
paulson@1618
   257
nipkow@1515
   258
paulson@2856
   259
(*Suggested by Pierre Chartier*)
paulson@2856
   260
goal Prod.thy
paulson@2856
   261
     "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
paulson@2856
   262
by (Fast_tac 1);
paulson@2856
   263
qed "UNION_Times_distrib";
paulson@2856
   264
clasohm@923
   265
(*** Domain of a relation ***)
clasohm@923
   266
clasohm@972
   267
val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";
clasohm@923
   268
by (rtac CollectI 1);
clasohm@923
   269
by (rtac bexI 1);
clasohm@923
   270
by (rtac (fst_conv RS sym) 1);
clasohm@923
   271
by (resolve_tac prems 1);
clasohm@923
   272
qed "fst_imageI";
clasohm@923
   273
clasohm@923
   274
val major::prems = goal Prod.thy
clasohm@972
   275
    "[| a : fst``r;  !!y.[| (a,y) : r |] ==> P |] ==> P"; 
clasohm@923
   276
by (rtac (major RS imageE) 1);
clasohm@923
   277
by (resolve_tac prems 1);
clasohm@923
   278
by (etac ssubst 1);
clasohm@923
   279
by (rtac (surjective_pairing RS subst) 1);
clasohm@923
   280
by (assume_tac 1);
clasohm@923
   281
qed "fst_imageE";
clasohm@923
   282
clasohm@923
   283
(*** Range of a relation ***)
clasohm@923
   284
clasohm@972
   285
val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r";
clasohm@923
   286
by (rtac CollectI 1);
clasohm@923
   287
by (rtac bexI 1);
clasohm@923
   288
by (rtac (snd_conv RS sym) 1);
clasohm@923
   289
by (resolve_tac prems 1);
clasohm@923
   290
qed "snd_imageI";
clasohm@923
   291
clasohm@923
   292
val major::prems = goal Prod.thy
clasohm@972
   293
    "[| a : snd``r;  !!y.[| (y,a) : r |] ==> P |] ==> P"; 
clasohm@923
   294
by (rtac (major RS imageE) 1);
clasohm@923
   295
by (resolve_tac prems 1);
clasohm@923
   296
by (etac ssubst 1);
clasohm@923
   297
by (rtac (surjective_pairing RS subst) 1);
clasohm@923
   298
by (assume_tac 1);
clasohm@923
   299
qed "snd_imageE";
clasohm@923
   300
clasohm@923
   301
(** Exhaustion rule for unit -- a degenerate form of induction **)
clasohm@923
   302
clasohm@923
   303
goalw Prod.thy [Unity_def]
clasohm@972
   304
    "u = ()";
nipkow@2886
   305
by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
nipkow@2880
   306
by (rtac (Rep_unit_inverse RS sym) 1);
clasohm@923
   307
qed "unit_eq";
berghofe@1754
   308
 
berghofe@1754
   309
AddIs  [fst_imageI, snd_imageI, prod_fun_imageI];
paulson@2856
   310
AddSEs [fst_imageE, snd_imageE, prod_fun_imageE];
clasohm@923
   311
nipkow@1746
   312
structure Prod_Syntax =
nipkow@1746
   313
struct
nipkow@1746
   314
nipkow@1746
   315
val unitT = Type("unit",[]);
nipkow@1746
   316
nipkow@1746
   317
fun mk_prod (T1,T2) = Type("*", [T1,T2]);
nipkow@1746
   318
nipkow@1746
   319
(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
nipkow@1746
   320
fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
nipkow@1746
   321
  | factors T                    = [T];
nipkow@1746
   322
nipkow@1746
   323
(*Make a correctly typed ordered pair*)
nipkow@1746
   324
fun mk_Pair (t1,t2) = 
nipkow@1746
   325
  let val T1 = fastype_of t1
nipkow@1746
   326
      and T2 = fastype_of t2
nipkow@1746
   327
  in  Const("Pair", [T1, T2] ---> mk_prod(T1,T2)) $ t1 $ t2  end;
nipkow@1746
   328
   
nipkow@1746
   329
fun split_const(Ta,Tb,Tc) = 
nipkow@1746
   330
    Const("split", [[Ta,Tb]--->Tc, mk_prod(Ta,Tb)] ---> Tc);
nipkow@1746
   331
nipkow@1746
   332
(*In ap_split S T u, term u expects separate arguments for the factors of S,
nipkow@1746
   333
  with result type T.  The call creates a new term expecting one argument
nipkow@1746
   334
  of type S.*)
nipkow@1746
   335
fun ap_split (Type("*", [T1,T2])) T3 u = 
nipkow@1746
   336
      split_const(T1,T2,T3) $ 
nipkow@1746
   337
      Abs("v", T1, 
paulson@2031
   338
          ap_split T2 T3
paulson@2031
   339
             ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
paulson@2031
   340
              Bound 0))
nipkow@1746
   341
  | ap_split T T3 u = u;
nipkow@1746
   342
nipkow@1746
   343
(*Makes a nested tuple from a list, following the product type structure*)
nipkow@1746
   344
fun mk_tuple (Type("*", [T1,T2])) tms = 
nipkow@1746
   345
        mk_Pair (mk_tuple T1 tms, 
paulson@2031
   346
                 mk_tuple T2 (drop (length (factors T1), tms)))
nipkow@1746
   347
  | mk_tuple T (t::_) = t;
nipkow@1746
   348
nipkow@1746
   349
(*Attempts to remove occurrences of split, and pair-valued parameters*)
nipkow@1746
   350
val remove_split = rewrite_rule [split RS eq_reflection]  o  
paulson@2031
   351
                   rule_by_tactic (ALLGOALS split_all_tac);
nipkow@1746
   352
nipkow@1746
   353
(*Uncurries any Var of function type in the rule*)
nipkow@1746
   354
fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =
nipkow@1746
   355
      let val T' = factors T1 ---> T2
paulson@2031
   356
          val newt = ap_split T1 T2 (Var(v,T'))
paulson@2031
   357
          val cterm = Thm.cterm_of (#sign(rep_thm rl))
nipkow@1746
   358
      in
paulson@2031
   359
          remove_split (instantiate ([], [(cterm t, cterm newt)]) rl)
nipkow@1746
   360
      end
nipkow@1746
   361
  | split_rule_var (t,rl) = rl;
nipkow@1746
   362
nipkow@1746
   363
(*Uncurries ALL function variables occurring in a rule's conclusion*)
nipkow@1746
   364
fun split_rule rl = foldr split_rule_var (term_vars (concl_of rl), rl)
nipkow@1746
   365
                    |> standard;
nipkow@1746
   366
nipkow@1746
   367
end;