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