src/HOL/Prod.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6016 797c76d6ff04
child 6394 3d9fd50fcc43
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
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
paulson@5810
     6
Ordered Pairs, the Cartesian product type, the unit type
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
(*This counts as a non-emptiness result for admitting 'a * 'b as a type*)
wenzelm@5069
    10
Goalw [Prod_def] "Pair_Rep a b : Prod";
clasohm@923
    11
by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
clasohm@923
    12
qed "ProdI";
clasohm@923
    13
clasohm@923
    14
val [major] = goalw Prod.thy [Pair_Rep_def]
clasohm@923
    15
    "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
clasohm@923
    16
by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), 
clasohm@1465
    17
            rtac conjI, rtac refl, rtac refl]);
clasohm@923
    18
qed "Pair_Rep_inject";
clasohm@923
    19
wenzelm@5069
    20
Goal "inj_on Abs_Prod Prod";
nipkow@4830
    21
by (rtac inj_on_inverseI 1);
clasohm@923
    22
by (etac Abs_Prod_inverse 1);
nipkow@4830
    23
qed "inj_on_Abs_Prod";
clasohm@923
    24
paulson@5316
    25
val prems = Goalw [Pair_def]
clasohm@972
    26
    "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
nipkow@4830
    27
by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
clasohm@923
    28
by (REPEAT (ares_tac (prems@[ProdI]) 1));
clasohm@923
    29
qed "Pair_inject";
clasohm@923
    30
wenzelm@5069
    31
Goal "((a,b) = (a',b')) = (a=a' & b=b')";
wenzelm@4089
    32
by (blast_tac (claset() addSEs [Pair_inject]) 1);
clasohm@923
    33
qed "Pair_eq";
nipkow@3429
    34
AddIffs [Pair_eq];
clasohm@923
    35
wenzelm@5069
    36
Goalw [fst_def] "fst((a,b)) = a";
oheimb@4534
    37
by (Blast_tac 1);
clasohm@923
    38
qed "fst_conv";
wenzelm@5069
    39
Goalw [snd_def] "snd((a,b)) = b";
oheimb@4534
    40
by (Blast_tac 1);
clasohm@923
    41
qed "snd_conv";
oheimb@4534
    42
Addsimps [fst_conv, snd_conv];
clasohm@923
    43
wenzelm@5069
    44
Goalw [Pair_def] "? x y. p = (x,y)";
clasohm@923
    45
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
clasohm@923
    46
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
clasohm@1465
    47
           rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
clasohm@923
    48
qed "PairE_lemma";
clasohm@923
    49
paulson@5316
    50
val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
clasohm@923
    51
by (rtac (PairE_lemma RS exE) 1);
clasohm@923
    52
by (REPEAT (eresolve_tac [prem,exE] 1));
clasohm@923
    53
qed "PairE";
clasohm@923
    54
oheimb@4819
    55
fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac,
oheimb@4819
    56
			 K prune_params_tac];
oheimb@4134
    57
oheimb@4828
    58
(* Do not add as rewrite rule: invalidates some proofs in IMP *)
wenzelm@5069
    59
Goal "p = (fst(p),snd(p))";
oheimb@4828
    60
by (pair_tac "p" 1);
oheimb@4828
    61
by (Asm_simp_tac 1);
oheimb@4828
    62
qed "surjective_pairing";
oheimb@4828
    63
oheimb@4828
    64
val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (K [
oheimb@4828
    65
	rtac exI 1, rtac exI 1, rtac surjective_pairing 1]);
oheimb@4828
    66
Addsimps [surj_pair];
oheimb@4828
    67
oheimb@4828
    68
wenzelm@5699
    69
bind_thm ("split_paired_all",
wenzelm@5699
    70
  SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
oheimb@4828
    71
(*
oheimb@4828
    72
Addsimps [split_paired_all] does not work with simplifier 
oheimb@4828
    73
because it also affects premises in congrence rules, 
oheimb@4828
    74
where is can lead to premises of the form !!a b. ... = ?P(a,b)
oheimb@4828
    75
which cannot be solved by reflexivity.
oheimb@4828
    76
*)
oheimb@4828
    77
nipkow@1301
    78
(* replace parameters of product type by individual component parameters *)
nipkow@1301
    79
local
oheimb@4819
    80
  fun is_pair (_,Type("*",_)) = true
oheimb@4819
    81
    | is_pair  _              = false;
oheimb@4828
    82
  fun exists_paired_all prem  = exists is_pair (Logic.strip_params prem);
oheimb@4828
    83
  val split_tac = full_simp_tac (HOL_basic_ss addsimps [split_paired_all]);
nipkow@1301
    84
in
oheimb@4828
    85
val split_all_tac = SUBGOAL (fn (prem,i) => 
oheimb@4828
    86
    if exists_paired_all prem then split_tac i else no_tac);  
nipkow@1301
    87
end;
nipkow@1301
    88
oheimb@4828
    89
claset_ref() := claset() addSWrapper ("split_all_tac", 
oheimb@4828
    90
				      fn tac2 => split_all_tac ORELSE' tac2);
nipkow@3568
    91
wenzelm@5069
    92
Goal "(!x. P x) = (!a b. P(a,b))";
oheimb@4650
    93
by (Fast_tac 1);
nipkow@1301
    94
qed "split_paired_All";
nipkow@3568
    95
Addsimps [split_paired_All];
nipkow@3568
    96
(* AddIffs is not a good idea because it makes Blast_tac loop *)
nipkow@3568
    97
berghofe@5715
    98
bind_thm ("prod_induct",
berghofe@5715
    99
  allI RS (allI RS (split_paired_All RS iffD2)) RS spec);
berghofe@5715
   100
wenzelm@5069
   101
Goal "(? x. P x) = (? a b. P(a,b))";
oheimb@4650
   102
by (Fast_tac 1);
nipkow@3568
   103
qed "split_paired_Ex";
oheimb@4534
   104
Addsimps [split_paired_Ex];
nipkow@1301
   105
wenzelm@5069
   106
Goalw [split_def] "split c (a,b) = c a b";
oheimb@4534
   107
by (Simp_tac 1);
clasohm@923
   108
qed "split";
oheimb@4534
   109
Addsimps [split];
clasohm@923
   110
wenzelm@5069
   111
Goal "split Pair p = p";
oheimb@4828
   112
by (pair_tac "p" 1);
oheimb@4828
   113
by (Simp_tac 1);
oheimb@4828
   114
qed "split_Pair";
oheimb@4828
   115
(*unused: val surjective_pairing2 = split_Pair RS sym;*)
oheimb@4828
   116
wenzelm@5069
   117
Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
oheimb@4828
   118
by (split_all_tac 1);
clasohm@1264
   119
by (Asm_simp_tac 1);
clasohm@923
   120
qed "Pair_fst_snd_eq";
clasohm@923
   121
clasohm@923
   122
(*Prevents simplification of c: much faster*)
clasohm@923
   123
qed_goal "split_weak_cong" Prod.thy
clasohm@923
   124
  "p=q ==> split c p = split c q"
clasohm@923
   125
  (fn [prem] => [rtac (prem RS arg_cong) 1]);
clasohm@923
   126
nipkow@1655
   127
qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
oheimb@4534
   128
  (K [rtac ext 1, split_all_tac 1, rtac split 1]);
nipkow@1655
   129
oheimb@4989
   130
qed_goal "cond_split_eta" Prod.thy 
oheimb@4989
   131
	"!!f. (!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g"
oheimb@4989
   132
  (K [asm_simp_tac (simpset() addsimps [split_eta]) 1]);
oheimb@5294
   133
oheimb@5294
   134
oheimb@5294
   135
(*simplification procedure for cond_split_eta. 
oheimb@5294
   136
  using split_eta a rewrite rule is not general enough, and using 
oheimb@5294
   137
  cond_split_eta directly would render some existing proofs very inefficient*)
oheimb@5294
   138
local
oheimb@5294
   139
  val split_eta_pat = Thm.read_cterm (sign_of thy) 
oheimb@5294
   140
		("split (%x. split (%y. f x y))", HOLogic.termTVar);
oheimb@5553
   141
  val split_eta_meta_eq = standard (mk_meta_eq cond_split_eta);
oheimb@5294
   142
  fun  Pair_pat 0      (Bound 0) = true
oheimb@5294
   143
  |    Pair_pat k      (Const ("Pair",  _) $ Bound m $ t) = 
oheimb@5294
   144
			m = k andalso Pair_pat (k-1) t
oheimb@5294
   145
  |    Pair_pat _ _ = false;
oheimb@5294
   146
  fun split_pat k (Abs  (_, _, f $ 
oheimb@5294
   147
			(Const ("Pair",_) $ Bound m $ 
oheimb@5294
   148
			(Const ("Pair",_) $ Bound n $ t)))) =
oheimb@5294
   149
			if m = k andalso n = k-1 andalso Pair_pat (k-2) t
oheimb@5294
   150
			then Some f else None
oheimb@5294
   151
  |   split_pat k (Const ("split", _) $ Abs (_, _, t)) = split_pat (k+1) t
oheimb@5294
   152
  |   split_pat k _ = None;
oheimb@5361
   153
  fun proc sg _	(s as
oheimb@5294
   154
	(Const ("split", _) $ Abs (_, _, 
oheimb@5294
   155
	(Const ("split", _) $ Abs (_, _, t))))) = (case split_pat 2 t of
oheimb@5294
   156
	  Some f => (let val fvar = Free ("f", fastype_of f);
oheimb@5294
   157
			 fun atom_fun t = if t = f then fvar else atom t
oheimb@5294
   158
			 and atom     (Abs (x, T, t)) = Abs (x, T,atom_fun t)
oheimb@5294
   159
			   | atom     (t $ u)         = atom_fun t $ atom_fun u
oheimb@5294
   160
			   | atom     x               = x;
oheimb@5361
   161
			 val ct   = cterm_of sg (HOLogic.mk_Trueprop
oheimb@5294
   162
				   (HOLogic.mk_eq (atom_fun s,fvar)));
oheimb@5294
   163
			 val ss   = HOL_basic_ss addsimps [cond_split_eta];
oheimb@5553
   164
         in Some (mk_meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end)
oheimb@5294
   165
	| None => None)
oheimb@5294
   166
  |   proc _ _ _ = None;
oheimb@5294
   167
oheimb@5294
   168
in
oheimb@5294
   169
  val split_eta_proc = Simplifier.mk_simproc "split_eta" [split_eta_pat] proc;
oheimb@5294
   170
end;
oheimb@5294
   171
oheimb@5294
   172
Addsimprocs [split_eta_proc];
oheimb@5294
   173
oheimb@4989
   174
oheimb@4819
   175
qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
oheimb@4534
   176
	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);
oheimb@4134
   177
clasohm@923
   178
(*For use with split_tac and the simplifier*)
wenzelm@5069
   179
Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
clasohm@923
   180
by (stac surjective_pairing 1);
clasohm@923
   181
by (stac split 1);
paulson@2935
   182
by (Blast_tac 1);
nipkow@4830
   183
qed "split_split";
clasohm@923
   184
nipkow@3568
   185
(* could be done after split_tac has been speeded up significantly:
nipkow@4830
   186
simpset_ref() := simpset() addsplits [split_split];
nipkow@3568
   187
   precompute the constants involved and don't do anything unless
nipkow@3568
   188
   the current goal contains one of those constants
nipkow@3568
   189
*)
nipkow@3568
   190
wenzelm@5069
   191
Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
nipkow@4830
   192
by (stac split_split 1);
oheimb@4435
   193
by (Simp_tac 1);
oheimb@4435
   194
qed "expand_split_asm";
oheimb@4435
   195
clasohm@923
   196
(** split used as a logical connective or set former **)
clasohm@923
   197
paulson@2935
   198
(*These rules are for use with blast_tac.
clasohm@923
   199
  Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
clasohm@923
   200
wenzelm@5069
   201
Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
paulson@1552
   202
by (split_all_tac 1);
nipkow@1454
   203
by (Asm_simp_tac 1);
nipkow@1454
   204
qed "splitI2";
nipkow@1454
   205
paulson@5143
   206
Goal "c a b ==> split c (a,b)";
clasohm@1264
   207
by (Asm_simp_tac 1);
clasohm@923
   208
qed "splitI";
clasohm@923
   209
paulson@5316
   210
val prems = Goalw [split_def]
clasohm@972
   211
    "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
clasohm@923
   212
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
clasohm@923
   213
qed "splitE";
clasohm@923
   214
oheimb@4134
   215
val splitE2 = prove_goal Prod.thy 
oheimb@4134
   216
"[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
oheimb@4134
   217
	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
oheimb@4134
   218
	rtac (split_beta RS subst) 1,
oheimb@4134
   219
	rtac (hd prems) 1]);
oheimb@4134
   220
paulson@5143
   221
Goal "split R (a,b) ==> R a b";
clasohm@923
   222
by (etac (split RS iffD1) 1);
clasohm@923
   223
qed "splitD";
clasohm@923
   224
paulson@5143
   225
Goal "z: c a b ==> z: split c (a,b)";
clasohm@1264
   226
by (Asm_simp_tac 1);
clasohm@923
   227
qed "mem_splitI";
clasohm@923
   228
wenzelm@5069
   229
Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
paulson@1552
   230
by (split_all_tac 1);
nipkow@1454
   231
by (Asm_simp_tac 1);
nipkow@1454
   232
qed "mem_splitI2";
nipkow@1454
   233
paulson@5316
   234
val prems = Goalw [split_def]
clasohm@972
   235
    "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
clasohm@923
   236
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
clasohm@923
   237
qed "mem_splitE";
clasohm@923
   238
paulson@2856
   239
AddSIs [splitI, splitI2, mem_splitI, mem_splitI2];
paulson@2856
   240
AddSEs [splitE, mem_splitE];
paulson@2856
   241
oheimb@4534
   242
(* allows simplifications of nested splits in case of independent predicates *)
wenzelm@5069
   243
Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";
oheimb@4534
   244
by (rtac ext 1);
oheimb@4534
   245
by (Blast_tac 1);
oheimb@4534
   246
qed "split_part";
oheimb@4534
   247
Addsimps [split_part];
oheimb@4534
   248
wenzelm@5069
   249
Goal "(@(x',y'). x = x' & y = y') = (x,y)";
oheimb@4534
   250
by (Blast_tac 1);
oheimb@4534
   251
qed "Eps_split_eq";
oheimb@4534
   252
Addsimps [Eps_split_eq];
oheimb@4534
   253
(*
oheimb@4534
   254
the following  would be slightly more general, 
oheimb@4534
   255
but cannot be used as rewrite rule:
oheimb@4534
   256
### Cannot add premise as rewrite rule because it contains (type) unknowns:
oheimb@4534
   257
### ?y = .x
paulson@5143
   258
Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
oheimb@4534
   259
by (rtac select_equality 1);
oheimb@4534
   260
by ( Simp_tac 1);
oheimb@4534
   261
by (split_all_tac 1);
oheimb@4534
   262
by (Asm_full_simp_tac 1);
oheimb@4534
   263
qed "Eps_split_eq";
oheimb@4534
   264
*)
oheimb@4534
   265
clasohm@923
   266
(*** prod_fun -- action of the product functor upon functions ***)
clasohm@923
   267
wenzelm@5069
   268
Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
clasohm@923
   269
by (rtac split 1);
clasohm@923
   270
qed "prod_fun";
paulson@4521
   271
Addsimps [prod_fun];
clasohm@923
   272
paulson@5278
   273
Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
clasohm@923
   274
by (rtac ext 1);
oheimb@4828
   275
by (pair_tac "x" 1);
paulson@4521
   276
by (Asm_simp_tac 1);
clasohm@923
   277
qed "prod_fun_compose";
clasohm@923
   278
wenzelm@5069
   279
Goal "prod_fun (%x. x) (%y. y) = (%z. z)";
clasohm@923
   280
by (rtac ext 1);
oheimb@4828
   281
by (pair_tac "z" 1);
paulson@4521
   282
by (Asm_simp_tac 1);
clasohm@923
   283
qed "prod_fun_ident";
paulson@4521
   284
Addsimps [prod_fun_ident];
clasohm@923
   285
paulson@5316
   286
Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
clasohm@923
   287
by (rtac image_eqI 1);
clasohm@923
   288
by (rtac (prod_fun RS sym) 1);
paulson@5316
   289
by (assume_tac 1);
clasohm@923
   290
qed "prod_fun_imageI";
clasohm@923
   291
paulson@5316
   292
val major::prems = Goal
clasohm@972
   293
    "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
clasohm@923
   294
\    |] ==> P";
clasohm@923
   295
by (rtac (major RS imageE) 1);
clasohm@923
   296
by (res_inst_tac [("p","x")] PairE 1);
clasohm@923
   297
by (resolve_tac prems 1);
paulson@2935
   298
by (Blast_tac 2);
wenzelm@4089
   299
by (blast_tac (claset() addIs [prod_fun]) 1);
clasohm@923
   300
qed "prod_fun_imageE";
clasohm@923
   301
paulson@5788
   302
AddIs  [prod_fun_imageI];
paulson@5788
   303
AddSEs [prod_fun_imageE];
paulson@5788
   304
paulson@4521
   305
clasohm@923
   306
(*** Disjoint union of a family of sets - Sigma ***)
clasohm@923
   307
clasohm@923
   308
qed_goalw "SigmaI" Prod.thy [Sigma_def]
clasohm@972
   309
    "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
clasohm@923
   310
 (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
clasohm@923
   311
paulson@2856
   312
AddSIs [SigmaI];
paulson@2856
   313
clasohm@923
   314
(*The general elimination rule*)
clasohm@923
   315
qed_goalw "SigmaE" Prod.thy [Sigma_def]
clasohm@923
   316
    "[| c: Sigma A B;  \
clasohm@972
   317
\       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
clasohm@923
   318
\    |] ==> P"
clasohm@923
   319
 (fn major::prems=>
clasohm@923
   320
  [ (cut_facts_tac [major] 1),
clasohm@923
   321
    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
clasohm@923
   322
clasohm@972
   323
(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
clasohm@972
   324
qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A"
clasohm@923
   325
 (fn [major]=>
clasohm@923
   326
  [ (rtac (major RS SigmaE) 1),
clasohm@923
   327
    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
clasohm@923
   328
clasohm@972
   329
qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)"
clasohm@923
   330
 (fn [major]=>
clasohm@923
   331
  [ (rtac (major RS SigmaE) 1),
clasohm@923
   332
    (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
clasohm@923
   333
clasohm@923
   334
qed_goal "SigmaE2" Prod.thy
clasohm@972
   335
    "[| (a,b) : Sigma A B;    \
clasohm@923
   336
\       [| a:A;  b:B(a) |] ==> P   \
clasohm@923
   337
\    |] ==> P"
clasohm@923
   338
 (fn [major,minor]=>
clasohm@923
   339
  [ (rtac minor 1),
clasohm@923
   340
    (rtac (major RS SigmaD1) 1),
clasohm@923
   341
    (rtac (major RS SigmaD2) 1) ]);
clasohm@923
   342
paulson@2856
   343
AddSEs [SigmaE2, SigmaE];
paulson@2856
   344
paulson@5316
   345
val prems = Goal
paulson@1642
   346
    "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
nipkow@1515
   347
by (cut_facts_tac prems 1);
wenzelm@4089
   348
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
nipkow@1515
   349
qed "Sigma_mono";
nipkow@1515
   350
paulson@1618
   351
qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
paulson@2935
   352
 (fn _ => [ (Blast_tac 1) ]);
paulson@1618
   353
paulson@1642
   354
qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
paulson@2935
   355
 (fn _ => [ (Blast_tac 1) ]);
paulson@1618
   356
paulson@1618
   357
Addsimps [Sigma_empty1,Sigma_empty2]; 
paulson@1618
   358
wenzelm@5069
   359
Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
paulson@2935
   360
by (Blast_tac 1);
paulson@1618
   361
qed "mem_Sigma_iff";
nipkow@3568
   362
AddIffs [mem_Sigma_iff]; 
paulson@1618
   363
paulson@6016
   364
Goal "x:C ==> (A Times C <= B Times C) = (A <= B)";
paulson@6016
   365
by (Blast_tac 1);
paulson@6016
   366
qed "Times_subset_cancel2";
paulson@6016
   367
paulson@6016
   368
Goal "x:C ==> (A Times C = B Times C) = (A = B)";
paulson@6016
   369
by (blast_tac (claset() addEs [equalityE]) 1);
paulson@6016
   370
qed "Times_eq_cancel2";
paulson@6016
   371
paulson@5810
   372
paulson@5810
   373
(*** Complex rules for Sigma ***)
paulson@5810
   374
oheimb@4534
   375
val Collect_split = prove_goal Prod.thy 
oheimb@4134
   376
	"{(a,b). P a & Q b} = Collect P Times Collect Q" (K [Blast_tac 1]);
oheimb@4534
   377
Addsimps [Collect_split];
nipkow@1515
   378
paulson@2856
   379
(*Suggested by Pierre Chartier*)
paulson@5278
   380
Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)";
paulson@2935
   381
by (Blast_tac 1);
paulson@2856
   382
qed "UNION_Times_distrib";
paulson@2856
   383
paulson@6016
   384
Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))";
paulson@5810
   385
by (Fast_tac 1);
paulson@6016
   386
qed "split_paired_Ball_Sigma";
paulson@6016
   387
Addsimps [split_paired_Ball_Sigma];
paulson@5810
   388
paulson@6016
   389
Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))";
paulson@5810
   390
by (Fast_tac 1);
paulson@6016
   391
qed "split_paired_Bex_Sigma";
paulson@6016
   392
Addsimps [split_paired_Bex_Sigma];
paulson@5810
   393
paulson@5810
   394
Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))";
paulson@5810
   395
by (Blast_tac 1);
paulson@5810
   396
qed "Sigma_Un_distrib1";
paulson@5810
   397
paulson@5810
   398
Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))";
paulson@5810
   399
by (Blast_tac 1);
paulson@5810
   400
qed "Sigma_Un_distrib2";
paulson@5810
   401
paulson@5810
   402
Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))";
paulson@5810
   403
by (Blast_tac 1);
paulson@5810
   404
qed "Sigma_Int_distrib1";
paulson@5810
   405
paulson@5810
   406
Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))";
paulson@5810
   407
by (Blast_tac 1);
paulson@5810
   408
qed "Sigma_Int_distrib2";
paulson@5810
   409
paulson@5810
   410
Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))";
paulson@5810
   411
by (Blast_tac 1);
paulson@5810
   412
qed "Sigma_Diff_distrib1";
paulson@5810
   413
paulson@5810
   414
Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))";
paulson@5810
   415
by (Blast_tac 1);
paulson@5810
   416
qed "Sigma_Diff_distrib2";
paulson@5810
   417
paulson@6016
   418
Goal "Sigma (Union X) B = (UN A:X. Sigma A B)";
paulson@6016
   419
by (Blast_tac 1);
paulson@6016
   420
qed "Sigma_Union";
paulson@6016
   421
paulson@5810
   422
clasohm@923
   423
(** Exhaustion rule for unit -- a degenerate form of induction **)
clasohm@923
   424
wenzelm@5069
   425
Goalw [Unity_def]
clasohm@972
   426
    "u = ()";
nipkow@2886
   427
by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
nipkow@2880
   428
by (rtac (Rep_unit_inverse RS sym) 1);
clasohm@923
   429
qed "unit_eq";
berghofe@1754
   430
 
paulson@5088
   431
(*simplification procedure for unit_eq.
paulson@5088
   432
  Cannot use this rule directly -- it loops!*)
wenzelm@5083
   433
local
wenzelm@5083
   434
  val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT));
oheimb@5553
   435
  val unit_meta_eq = standard (mk_meta_eq unit_eq);
wenzelm@5083
   436
  fun proc _ _ t =
wenzelm@5083
   437
    if HOLogic.is_unit t then None
wenzelm@5083
   438
    else Some unit_meta_eq;
wenzelm@5083
   439
in
wenzelm@5083
   440
  val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc;
wenzelm@5083
   441
end;
wenzelm@5083
   442
wenzelm@5083
   443
Addsimprocs [unit_eq_proc];
wenzelm@5083
   444
wenzelm@5083
   445
berghofe@5761
   446
Goal "P () ==> P x";
berghofe@5761
   447
by (Simp_tac 1);
berghofe@5761
   448
qed "unit_induct";
berghofe@5761
   449
berghofe@5761
   450
paulson@5088
   451
(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u),
paulson@5088
   452
  replacing it by f rather than by %u.f(). *)
paulson@5088
   453
Goal "(%u::unit. f()) = f";
paulson@5088
   454
by (rtac ext 1);
paulson@5088
   455
by (Simp_tac 1);
paulson@5088
   456
qed "unit_abs_eta_conv";
paulson@5088
   457
Addsimps [unit_abs_eta_conv];
paulson@5088
   458
paulson@5088
   459
berghofe@5096
   460
(*Attempts to remove occurrences of split, and pair-valued parameters*)
berghofe@5096
   461
val remove_split = rewrite_rule [split RS eq_reflection] o  
berghofe@5096
   462
                   rule_by_tactic (TRYALL split_all_tac);
nipkow@1746
   463
berghofe@5096
   464
local
nipkow@1746
   465
nipkow@1746
   466
(*In ap_split S T u, term u expects separate arguments for the factors of S,
nipkow@1746
   467
  with result type T.  The call creates a new term expecting one argument
nipkow@1746
   468
  of type S.*)
berghofe@5096
   469
fun ap_split (Type ("*", [T1, T2])) T3 u = 
berghofe@5096
   470
      HOLogic.split_const (T1, T2, T3) $ 
nipkow@1746
   471
      Abs("v", T1, 
paulson@2031
   472
          ap_split T2 T3
berghofe@5096
   473
             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ 
paulson@2031
   474
              Bound 0))
nipkow@1746
   475
  | ap_split T T3 u = u;
nipkow@1746
   476
berghofe@5096
   477
(*Curries any Var of function type in the rule*)
berghofe@5096
   478
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
berghofe@5096
   479
      let val T' = HOLogic.prodT_factors T1 ---> T2
berghofe@5096
   480
          val newt = ap_split T1 T2 (Var (v, T'))
berghofe@5096
   481
          val cterm = Thm.cterm_of (#sign (rep_thm rl))
berghofe@5096
   482
      in
berghofe@5096
   483
          instantiate ([], [(cterm t, cterm newt)]) rl
berghofe@5096
   484
      end
berghofe@5096
   485
  | split_rule_var' (t, rl) = rl;
nipkow@1746
   486
berghofe@5096
   487
in
nipkow@1746
   488
berghofe@5096
   489
val split_rule_var = standard o remove_split o split_rule_var';
berghofe@5096
   490
berghofe@5096
   491
(*Curries ALL function variables occurring in a rule's conclusion*)
berghofe@5096
   492
fun split_rule rl = remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl))
nipkow@1746
   493
                    |> standard;
nipkow@1746
   494
nipkow@1746
   495
end;
paulson@5810
   496
paulson@5810
   497