src/HOL/Product_Type.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10999 b044cf3500a2
permissions -rw-r--r--
improved theory reference in comment
nipkow@10213
     1
(*  Title:      HOL/Product_Type.ML
nipkow@10213
     2
    ID:         $Id$
nipkow@10213
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
nipkow@10213
     4
    Copyright   1991  University of Cambridge
nipkow@10213
     5
nipkow@10213
     6
Ordered Pairs, the Cartesian product type, the unit type
nipkow@10213
     7
*)
nipkow@10213
     8
nipkow@10213
     9
(** unit **)
nipkow@10213
    10
nipkow@10213
    11
Goalw [Unity_def]
nipkow@10213
    12
    "u = ()";
nipkow@10213
    13
by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1);
nipkow@10213
    14
by (rtac (Rep_unit_inverse RS sym) 1);
nipkow@10213
    15
qed "unit_eq";
nipkow@10213
    16
nipkow@10213
    17
(*simplification procedure for unit_eq.
nipkow@10213
    18
  Cannot use this rule directly -- it loops!*)
nipkow@10213
    19
local
nipkow@10213
    20
  val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT));
nipkow@10213
    21
  val unit_meta_eq = standard (mk_meta_eq unit_eq);
nipkow@10213
    22
  fun proc _ _ t =
nipkow@10213
    23
    if HOLogic.is_unit t then None
nipkow@10213
    24
    else Some unit_meta_eq;
nipkow@10213
    25
in
nipkow@10213
    26
  val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc;
nipkow@10213
    27
end;
nipkow@10213
    28
nipkow@10213
    29
Addsimprocs [unit_eq_proc];
nipkow@10213
    30
nipkow@10213
    31
Goal "(!!x::unit. PROP P x) == PROP P ()";
nipkow@10213
    32
by (Simp_tac 1);
nipkow@10213
    33
qed "unit_all_eq1";
nipkow@10213
    34
nipkow@10213
    35
Goal "(!!x::unit. PROP P) == PROP P";
nipkow@10213
    36
by (rtac triv_forall_equality 1);
nipkow@10213
    37
qed "unit_all_eq2";
nipkow@10213
    38
nipkow@10213
    39
Goal "P () ==> P x";
nipkow@10213
    40
by (Simp_tac 1);
nipkow@10213
    41
qed "unit_induct";
nipkow@10213
    42
nipkow@10213
    43
(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u),
nipkow@10213
    44
  replacing it by f rather than by %u.f(). *)
nipkow@10213
    45
Goal "(%u::unit. f()) = f";
nipkow@10213
    46
by (rtac ext 1);
nipkow@10213
    47
by (Simp_tac 1);
nipkow@10213
    48
qed "unit_abs_eta_conv";
nipkow@10213
    49
Addsimps [unit_abs_eta_conv];
nipkow@10213
    50
nipkow@10213
    51
nipkow@10213
    52
(** prod **)
nipkow@10213
    53
nipkow@10213
    54
Goalw [Prod_def] "Pair_Rep a b : Prod";
nipkow@10213
    55
by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
nipkow@10213
    56
qed "ProdI";
nipkow@10213
    57
nipkow@10213
    58
Goalw [Pair_Rep_def] "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
nipkow@10213
    59
by (dtac (fun_cong RS fun_cong) 1);
nipkow@10213
    60
by (Blast_tac 1);
nipkow@10213
    61
qed "Pair_Rep_inject";
nipkow@10213
    62
nipkow@10213
    63
Goal "inj_on Abs_Prod Prod";
nipkow@10213
    64
by (rtac inj_on_inverseI 1);
nipkow@10213
    65
by (etac Abs_Prod_inverse 1);
nipkow@10213
    66
qed "inj_on_Abs_Prod";
nipkow@10213
    67
nipkow@10213
    68
val prems = Goalw [Pair_def]
nipkow@10213
    69
    "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
nipkow@10213
    70
by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
nipkow@10213
    71
by (REPEAT (ares_tac (prems@[ProdI]) 1));
nipkow@10213
    72
qed "Pair_inject";
nipkow@10213
    73
nipkow@10213
    74
Goal "((a,b) = (a',b')) = (a=a' & b=b')";
nipkow@10213
    75
by (blast_tac (claset() addSEs [Pair_inject]) 1);
nipkow@10213
    76
qed "Pair_eq";
nipkow@10213
    77
AddIffs [Pair_eq];
nipkow@10213
    78
nipkow@10213
    79
Goalw [fst_def] "fst (a,b) = a";
nipkow@10213
    80
by (Blast_tac 1);
nipkow@10213
    81
qed "fst_conv";
nipkow@10213
    82
Goalw [snd_def] "snd (a,b) = b";
nipkow@10213
    83
by (Blast_tac 1);
nipkow@10213
    84
qed "snd_conv";
nipkow@10213
    85
Addsimps [fst_conv, snd_conv];
nipkow@10213
    86
nipkow@10213
    87
Goal "fst (x, y) = a ==> x = a";
nipkow@10213
    88
by (Asm_full_simp_tac 1);
nipkow@10213
    89
qed "fst_eqD";
nipkow@10213
    90
Goal "snd (x, y) = a ==> y = a";
nipkow@10213
    91
by (Asm_full_simp_tac 1);
nipkow@10213
    92
qed "snd_eqD";
nipkow@10213
    93
nipkow@10213
    94
Goalw [Pair_def] "? x y. p = (x,y)";
nipkow@10213
    95
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
nipkow@10213
    96
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
nipkow@10213
    97
           rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
nipkow@10213
    98
qed "PairE_lemma";
nipkow@10213
    99
nipkow@10213
   100
val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
nipkow@10213
   101
by (rtac (PairE_lemma RS exE) 1);
nipkow@10213
   102
by (REPEAT (eresolve_tac [prem,exE] 1));
nipkow@10213
   103
qed "PairE";
nipkow@10213
   104
nipkow@10213
   105
fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac,
nipkow@10213
   106
                         K prune_params_tac];
nipkow@10213
   107
nipkow@10213
   108
(* Do not add as rewrite rule: invalidates some proofs in IMP *)
nipkow@10213
   109
Goal "p = (fst(p),snd(p))";
nipkow@10213
   110
by (pair_tac "p" 1);
nipkow@10213
   111
by (Asm_simp_tac 1);
nipkow@10213
   112
qed "surjective_pairing";
nipkow@10213
   113
Addsimps [surjective_pairing RS sym];
nipkow@10213
   114
nipkow@10213
   115
Goal "? x y. z = (x, y)";
nipkow@10213
   116
by (rtac exI 1);
nipkow@10213
   117
by (rtac exI 1);
nipkow@10213
   118
by (rtac surjective_pairing 1);
nipkow@10213
   119
qed "surj_pair";
nipkow@10213
   120
Addsimps [surj_pair];
nipkow@10213
   121
nipkow@10213
   122
nipkow@10213
   123
bind_thm ("split_paired_all",
nipkow@10213
   124
  SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
nipkow@10213
   125
bind_thms ("split_tupled_all", [split_paired_all, unit_all_eq2]);
nipkow@10213
   126
nipkow@10213
   127
(*
nipkow@10213
   128
Addsimps [split_paired_all] does not work with simplifier
nipkow@10213
   129
because it also affects premises in congrence rules,
nipkow@10213
   130
where is can lead to premises of the form !!a b. ... = ?P(a,b)
nipkow@10213
   131
which cannot be solved by reflexivity.
nipkow@10213
   132
*)
nipkow@10213
   133
nipkow@10213
   134
(* replace parameters of product type by individual component parameters *)
nipkow@10213
   135
local
wenzelm@10813
   136
  fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) =
wenzelm@10813
   137
        can HOLogic.dest_prodT T orelse exists_paired_all t
wenzelm@10813
   138
    | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u
wenzelm@10813
   139
    | exists_paired_all (Abs (_, _, t)) = exists_paired_all t
wenzelm@10813
   140
    | exists_paired_all _ = false;
wenzelm@10829
   141
  val ss = HOL_basic_ss
wenzelm@10829
   142
    addsimps [split_paired_all, unit_all_eq2, unit_abs_eta_conv]
wenzelm@10829
   143
    addsimprocs [unit_eq_proc];
nipkow@10213
   144
in
wenzelm@10813
   145
  val split_all_tac = SUBGOAL (fn (t, i) =>
wenzelm@10829
   146
    if exists_paired_all t then full_simp_tac ss i else no_tac);
wenzelm@10829
   147
  fun split_all th =
wenzelm@10829
   148
    if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
nipkow@10213
   149
end;
nipkow@10213
   150
nipkow@10213
   151
claset_ref() := claset()
nipkow@10213
   152
  addSWrapper ("split_all_tac", fn tac2 => split_all_tac ORELSE' tac2);
nipkow@10213
   153
nipkow@10213
   154
Goal "(!x. P x) = (!a b. P(a,b))";
nipkow@10213
   155
by (Fast_tac 1);
nipkow@10213
   156
qed "split_paired_All";
nipkow@10213
   157
Addsimps [split_paired_All];
nipkow@10213
   158
(* AddIffs is not a good idea because it makes Blast_tac loop *)
nipkow@10213
   159
nipkow@10213
   160
bind_thm ("prod_induct",
nipkow@10213
   161
  allI RS (allI RS (split_paired_All RS iffD2)) RS spec);
nipkow@10213
   162
nipkow@10213
   163
Goal "(? x. P x) = (? a b. P(a,b))";
nipkow@10213
   164
by (Fast_tac 1);
nipkow@10213
   165
qed "split_paired_Ex";
nipkow@10213
   166
Addsimps [split_paired_Ex];
nipkow@10213
   167
nipkow@10213
   168
Goalw [split_def] "split c (a,b) = c a b";
nipkow@10213
   169
by (Simp_tac 1);
wenzelm@10918
   170
qed "split_conv";
wenzelm@10918
   171
Addsimps [split_conv];
wenzelm@10918
   172
(*bind_thm ("split", split_conv);                  (*for compatibility*)*)
nipkow@10213
   173
nipkow@10213
   174
(*Subsumes the old split_Pair when f is the identity function*)
nipkow@10213
   175
Goal "split (%x y. f(x,y)) = f";
nipkow@10213
   176
by (rtac ext 1);
nipkow@10213
   177
by (pair_tac "x" 1);
nipkow@10213
   178
by (Simp_tac 1);
nipkow@10213
   179
qed "split_Pair_apply";
nipkow@10213
   180
nipkow@10213
   181
(*Can't be added to simpset: loops!*)
nipkow@10213
   182
Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
nipkow@10213
   183
by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
nipkow@10213
   184
qed "split_paired_Eps";
nipkow@10213
   185
nipkow@10213
   186
Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
nipkow@10213
   187
by (split_all_tac 1);
nipkow@10213
   188
by (Asm_simp_tac 1);
nipkow@10213
   189
qed "Pair_fst_snd_eq";
nipkow@10213
   190
nipkow@10213
   191
Goal "fst p = fst q ==> snd p = snd q ==> p = q";
nipkow@10213
   192
by (asm_simp_tac (simpset() addsimps [Pair_fst_snd_eq]) 1);
nipkow@10213
   193
qed "prod_eqI";
nipkow@10213
   194
AddXIs [prod_eqI];
nipkow@10213
   195
nipkow@10213
   196
(*Prevents simplification of c: much faster*)
nipkow@10213
   197
Goal "p=q ==> split c p = split c q";
nipkow@10213
   198
by (etac arg_cong 1);
nipkow@10213
   199
qed "split_weak_cong";
nipkow@10213
   200
nipkow@10213
   201
Goal "(%(x,y). f(x,y)) = f";
nipkow@10213
   202
by (rtac ext 1);
nipkow@10213
   203
by (split_all_tac 1);
wenzelm@10918
   204
by (rtac split_conv 1);
nipkow@10213
   205
qed "split_eta";
nipkow@10213
   206
nipkow@10213
   207
val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
nipkow@10213
   208
by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1);
nipkow@10213
   209
qed "cond_split_eta";
nipkow@10213
   210
nipkow@10213
   211
(*simplification procedure for cond_split_eta.
nipkow@10213
   212
  using split_eta a rewrite rule is not general enough, and using
nipkow@10213
   213
  cond_split_eta directly would render some existing proofs very inefficient.
nipkow@10213
   214
  similarly for split_beta. *)
nipkow@10213
   215
local
nipkow@10213
   216
  fun  Pair_pat k 0 (Bound m) = (m = k)
nipkow@10213
   217
  |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
nipkow@10213
   218
                        m = k+i andalso Pair_pat k (i-1) t
nipkow@10213
   219
  |    Pair_pat _ _ _ = false;
nipkow@10213
   220
  fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
nipkow@10213
   221
  |   no_args k i (t $ u) = no_args k i t andalso no_args k i u
nipkow@10213
   222
  |   no_args k i (Bound m) = m < k orelse m > k+i
nipkow@10213
   223
  |   no_args _ _ _ = true;
nipkow@10213
   224
  fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then Some (i,t) else None
nipkow@10213
   225
  |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
nipkow@10213
   226
  |   split_pat tp i _ = None;
nipkow@10213
   227
  fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
nipkow@10213
   228
        (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
nipkow@10213
   229
        (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
nipkow@10213
   230
  val sign = sign_of (the_context ());
nipkow@10213
   231
  fun simproc name patstr = Simplifier.mk_simproc name
nipkow@10213
   232
                [Thm.read_cterm sign (patstr, HOLogic.termT)];
nipkow@10213
   233
nipkow@10213
   234
  val beta_patstr = "split f z";
nipkow@10213
   235
  val  eta_patstr = "split f";
nipkow@10213
   236
  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
nipkow@10213
   237
  |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
nipkow@10213
   238
                        (beta_term_pat k i t andalso beta_term_pat k i u)
nipkow@10213
   239
  |   beta_term_pat k i t = no_args k i t;
nipkow@10213
   240
  fun  eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
nipkow@10213
   241
  |    eta_term_pat _ _ _ = false;
nipkow@10213
   242
  fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
nipkow@10213
   243
  |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
nipkow@10213
   244
                              else (subst arg k i t $ subst arg k i u)
nipkow@10213
   245
  |   subst arg k i t = t;
nipkow@10213
   246
  fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
nipkow@10213
   247
        (case split_pat beta_term_pat 1 t of
nipkow@10213
   248
        Some (i,f) => Some (metaeq sg s (subst arg 0 i f))
nipkow@10213
   249
        | None => None)
nipkow@10213
   250
  |   beta_proc _ _ _ = None;
nipkow@10213
   251
  fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) =
nipkow@10213
   252
        (case split_pat eta_term_pat 1 t of
nipkow@10213
   253
          Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end))
nipkow@10213
   254
        | None => None)
nipkow@10213
   255
  |   eta_proc _ _ _ = None;
nipkow@10213
   256
in
nipkow@10213
   257
  val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
nipkow@10213
   258
  val split_eta_proc  = simproc "split_eta"   eta_patstr  eta_proc;
nipkow@10213
   259
end;
nipkow@10213
   260
nipkow@10213
   261
Addsimprocs [split_beta_proc,split_eta_proc];
nipkow@10213
   262
nipkow@10213
   263
Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
wenzelm@10918
   264
by (stac surjective_pairing 1 THEN rtac split_conv 1);
nipkow@10213
   265
qed "split_beta";
nipkow@10213
   266
nipkow@10213
   267
(*For use with split_tac and the simplifier*)
nipkow@10213
   268
Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
nipkow@10213
   269
by (stac surjective_pairing 1);
wenzelm@10918
   270
by (stac split_conv 1);
nipkow@10213
   271
by (Blast_tac 1);
nipkow@10213
   272
qed "split_split";
nipkow@10213
   273
nipkow@10213
   274
(* could be done after split_tac has been speeded up significantly:
nipkow@10213
   275
simpset_ref() := simpset() addsplits [split_split];
nipkow@10213
   276
   precompute the constants involved and don't do anything unless
nipkow@10213
   277
   the current goal contains one of those constants
nipkow@10213
   278
*)
nipkow@10213
   279
nipkow@10213
   280
Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
nipkow@10213
   281
by (stac split_split 1);
nipkow@10213
   282
by (Simp_tac 1);
nipkow@10540
   283
qed "split_split_asm";
nipkow@10213
   284
nipkow@10213
   285
(** split used as a logical connective or set former **)
nipkow@10213
   286
nipkow@10213
   287
(*These rules are for use with blast_tac.
nipkow@10213
   288
  Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
nipkow@10213
   289
nipkow@10213
   290
Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
nipkow@10213
   291
by (split_all_tac 1);
nipkow@10213
   292
by (Asm_simp_tac 1);
nipkow@10213
   293
qed "splitI2";
nipkow@10213
   294
nipkow@10213
   295
Goal "!!p. [| !!a b. (a,b)=p ==> c a b x |] ==> split c p x";
nipkow@10213
   296
by (split_all_tac 1);
nipkow@10213
   297
by (Asm_simp_tac 1);
nipkow@10213
   298
qed "splitI2'";
nipkow@10213
   299
nipkow@10213
   300
Goal "c a b ==> split c (a,b)";
nipkow@10213
   301
by (Asm_simp_tac 1);
nipkow@10213
   302
qed "splitI";
nipkow@10213
   303
nipkow@10213
   304
val prems = Goalw [split_def]
nipkow@10213
   305
    "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
nipkow@10213
   306
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
nipkow@10213
   307
qed "splitE";
nipkow@10213
   308
nipkow@10213
   309
val prems = Goalw [split_def]
nipkow@10213
   310
    "[| split c p z;  !!x y. [| p = (x,y);  c x y z |] ==> Q |] ==> Q";
nipkow@10213
   311
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
nipkow@10213
   312
qed "splitE'";
nipkow@10213
   313
nipkow@10213
   314
val major::prems = Goal
nipkow@10213
   315
    "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R  \
nipkow@10213
   316
\    |] ==> R";
nipkow@10213
   317
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
nipkow@10213
   318
by (rtac (split_beta RS subst) 1 THEN rtac major 1);
nipkow@10213
   319
qed "splitE2";
nipkow@10213
   320
nipkow@10213
   321
Goal "split R (a,b) ==> R a b";
wenzelm@10918
   322
by (etac (split_conv RS iffD1) 1);
nipkow@10213
   323
qed "splitD";
nipkow@10213
   324
nipkow@10213
   325
Goal "z: c a b ==> z: split c (a,b)";
nipkow@10213
   326
by (Asm_simp_tac 1);
nipkow@10213
   327
qed "mem_splitI";
nipkow@10213
   328
nipkow@10213
   329
Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
nipkow@10213
   330
by (split_all_tac 1);
nipkow@10213
   331
by (Asm_simp_tac 1);
nipkow@10213
   332
qed "mem_splitI2";
nipkow@10213
   333
nipkow@10213
   334
val prems = Goalw [split_def]
nipkow@10213
   335
    "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
nipkow@10213
   336
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
nipkow@10213
   337
qed "mem_splitE";
nipkow@10213
   338
nipkow@10213
   339
AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2];
nipkow@10213
   340
AddSEs [splitE, splitE', mem_splitE];
nipkow@10213
   341
nipkow@10213
   342
Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P";
nipkow@10213
   343
by (rtac ext 1);
nipkow@10213
   344
by (Fast_tac 1);
nipkow@10213
   345
qed "split_eta_SetCompr";
nipkow@10213
   346
Addsimps [split_eta_SetCompr];
nipkow@10213
   347
nipkow@10213
   348
Goal "(%u. ? x y. u = (x, y) & P x y) = split P";
nipkow@10213
   349
br ext 1;
nipkow@10213
   350
by (Fast_tac 1);
nipkow@10213
   351
qed "split_eta_SetCompr2";
nipkow@10213
   352
Addsimps [split_eta_SetCompr2];
nipkow@10213
   353
nipkow@10213
   354
(* allows simplifications of nested splits in case of independent predicates *)
nipkow@10213
   355
Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";
nipkow@10213
   356
by (rtac ext 1);
nipkow@10213
   357
by (Blast_tac 1);
nipkow@10213
   358
qed "split_part";
nipkow@10213
   359
Addsimps [split_part];
nipkow@10213
   360
nipkow@10213
   361
Goal "(@(x',y'). x = x' & y = y') = (x,y)";
nipkow@10213
   362
by (Blast_tac 1);
nipkow@10213
   363
qed "Eps_split_eq";
nipkow@10213
   364
Addsimps [Eps_split_eq];
nipkow@10213
   365
(*
nipkow@10213
   366
the following  would be slightly more general,
nipkow@10213
   367
but cannot be used as rewrite rule:
nipkow@10213
   368
### Cannot add premise as rewrite rule because it contains (type) unknowns:
nipkow@10213
   369
### ?y = .x
nipkow@10213
   370
Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
nipkow@10213
   371
by (rtac some_equality 1);
nipkow@10213
   372
by ( Simp_tac 1);
nipkow@10213
   373
by (split_all_tac 1);
nipkow@10213
   374
by (Asm_full_simp_tac 1);
nipkow@10213
   375
qed "Eps_split_eq";
nipkow@10213
   376
*)
nipkow@10213
   377
nipkow@10213
   378
(*** prod_fun -- action of the product functor upon functions ***)
nipkow@10213
   379
nipkow@10213
   380
Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
wenzelm@10918
   381
by (rtac split_conv 1);
nipkow@10213
   382
qed "prod_fun";
nipkow@10213
   383
Addsimps [prod_fun];
nipkow@10213
   384
nipkow@10213
   385
Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
nipkow@10213
   386
by (rtac ext 1);
nipkow@10213
   387
by (pair_tac "x" 1);
nipkow@10213
   388
by (Asm_simp_tac 1);
nipkow@10213
   389
qed "prod_fun_compose";
nipkow@10213
   390
nipkow@10213
   391
Goal "prod_fun (%x. x) (%y. y) = (%z. z)";
nipkow@10213
   392
by (rtac ext 1);
nipkow@10213
   393
by (pair_tac "z" 1);
nipkow@10213
   394
by (Asm_simp_tac 1);
nipkow@10213
   395
qed "prod_fun_ident";
nipkow@10213
   396
Addsimps [prod_fun_ident];
nipkow@10213
   397
nipkow@10832
   398
Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)`r";
nipkow@10213
   399
by (rtac image_eqI 1);
nipkow@10213
   400
by (rtac (prod_fun RS sym) 1);
nipkow@10213
   401
by (assume_tac 1);
nipkow@10213
   402
qed "prod_fun_imageI";
nipkow@10213
   403
nipkow@10213
   404
val major::prems = Goal
nipkow@10832
   405
    "[| c: (prod_fun f g)`r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
nipkow@10213
   406
\    |] ==> P";
nipkow@10213
   407
by (rtac (major RS imageE) 1);
nipkow@10213
   408
by (res_inst_tac [("p","x")] PairE 1);
nipkow@10213
   409
by (resolve_tac prems 1);
nipkow@10213
   410
by (Blast_tac 2);
nipkow@10213
   411
by (blast_tac (claset() addIs [prod_fun]) 1);
nipkow@10213
   412
qed "prod_fun_imageE";
nipkow@10213
   413
nipkow@10213
   414
AddIs  [prod_fun_imageI];
nipkow@10213
   415
AddSEs [prod_fun_imageE];
nipkow@10213
   416
nipkow@10213
   417
nipkow@10213
   418
(*** Disjoint union of a family of sets - Sigma ***)
nipkow@10213
   419
nipkow@10213
   420
Goalw [Sigma_def] "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B";
nipkow@10213
   421
by (REPEAT (ares_tac [singletonI,UN_I] 1));
nipkow@10213
   422
qed "SigmaI";
nipkow@10213
   423
nipkow@10213
   424
AddSIs [SigmaI];
nipkow@10213
   425
nipkow@10213
   426
(*The general elimination rule*)
nipkow@10213
   427
val major::prems = Goalw [Sigma_def]
nipkow@10213
   428
    "[| c: Sigma A B;  \
nipkow@10213
   429
\       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
nipkow@10213
   430
\    |] ==> P";
nipkow@10213
   431
by (cut_facts_tac [major] 1);
nipkow@10213
   432
by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
nipkow@10213
   433
qed "SigmaE";
nipkow@10213
   434
nipkow@10213
   435
(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
nipkow@10213
   436
nipkow@10213
   437
Goal "(a,b) : Sigma A B ==> a : A";
nipkow@10213
   438
by (etac SigmaE 1);
nipkow@10213
   439
by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
nipkow@10213
   440
qed "SigmaD1";
nipkow@10213
   441
nipkow@10213
   442
Goal "(a,b) : Sigma A B ==> b : B(a)";
nipkow@10213
   443
by (etac SigmaE 1);
nipkow@10213
   444
by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
nipkow@10213
   445
qed "SigmaD2";
nipkow@10213
   446
nipkow@10213
   447
val [major,minor]= Goal
nipkow@10213
   448
    "[| (a,b) : Sigma A B;    \
nipkow@10213
   449
\       [| a:A;  b:B(a) |] ==> P   \
nipkow@10213
   450
\    |] ==> P";
nipkow@10213
   451
by (rtac minor 1);
nipkow@10213
   452
by (rtac (major RS SigmaD1) 1);
nipkow@10213
   453
by (rtac (major RS SigmaD2) 1) ;
nipkow@10213
   454
qed "SigmaE2";
nipkow@10213
   455
nipkow@10213
   456
AddSEs [SigmaE2, SigmaE];
nipkow@10213
   457
nipkow@10213
   458
val prems = Goal
nipkow@10213
   459
    "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
nipkow@10213
   460
by (cut_facts_tac prems 1);
nipkow@10213
   461
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
nipkow@10213
   462
qed "Sigma_mono";
nipkow@10213
   463
nipkow@10213
   464
Goal "Sigma {} B = {}";
nipkow@10213
   465
by (Blast_tac 1) ;
nipkow@10213
   466
qed "Sigma_empty1";
nipkow@10213
   467
nipkow@10213
   468
Goal "A <*> {} = {}";
nipkow@10213
   469
by (Blast_tac 1) ;
nipkow@10213
   470
qed "Sigma_empty2";
nipkow@10213
   471
nipkow@10213
   472
Addsimps [Sigma_empty1,Sigma_empty2];
nipkow@10213
   473
nipkow@10213
   474
Goal "UNIV <*> UNIV = UNIV";
nipkow@10213
   475
by Auto_tac;
nipkow@10213
   476
qed "UNIV_Times_UNIV";
nipkow@10213
   477
Addsimps [UNIV_Times_UNIV];
nipkow@10213
   478
nipkow@10213
   479
Goal "- (UNIV <*> A) = UNIV <*> (-A)";
nipkow@10213
   480
by Auto_tac;
nipkow@10213
   481
qed "Compl_Times_UNIV1";
nipkow@10213
   482
nipkow@10213
   483
Goal "- (A <*> UNIV) = (-A) <*> UNIV";
nipkow@10213
   484
by Auto_tac;
nipkow@10213
   485
qed "Compl_Times_UNIV2";
nipkow@10213
   486
nipkow@10213
   487
Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2];
nipkow@10213
   488
nipkow@10213
   489
Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
nipkow@10213
   490
by (Blast_tac 1);
nipkow@10213
   491
qed "mem_Sigma_iff";
nipkow@10213
   492
AddIffs [mem_Sigma_iff];
nipkow@10213
   493
nipkow@10213
   494
Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)";
nipkow@10213
   495
by (Blast_tac 1);
nipkow@10213
   496
qed "Times_subset_cancel2";
nipkow@10213
   497
nipkow@10213
   498
Goal "x:C ==> (A <*> C = B <*> C) = (A = B)";
nipkow@10213
   499
by (blast_tac (claset() addEs [equalityE]) 1);
nipkow@10213
   500
qed "Times_eq_cancel2";
nipkow@10213
   501
nipkow@10213
   502
Goal "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))";
nipkow@10213
   503
by (Fast_tac 1);
nipkow@10213
   504
qed "SetCompr_Sigma_eq";
nipkow@10213
   505
nipkow@10213
   506
(*** Complex rules for Sigma ***)
nipkow@10213
   507
nipkow@10213
   508
Goal "{(a,b). P a & Q b} = Collect P <*> Collect Q";
nipkow@10213
   509
by (Blast_tac 1);
nipkow@10213
   510
qed "Collect_split";
nipkow@10213
   511
nipkow@10213
   512
Addsimps [Collect_split];
nipkow@10213
   513
nipkow@10213
   514
(*Suggested by Pierre Chartier*)
nipkow@10213
   515
Goal "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)";
nipkow@10213
   516
by (Blast_tac 1);
nipkow@10213
   517
qed "UN_Times_distrib";
nipkow@10213
   518
nipkow@10213
   519
Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))";
nipkow@10213
   520
by (Fast_tac 1);
nipkow@10213
   521
qed "split_paired_Ball_Sigma";
nipkow@10213
   522
Addsimps [split_paired_Ball_Sigma];
nipkow@10213
   523
nipkow@10213
   524
Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))";
nipkow@10213
   525
by (Fast_tac 1);
nipkow@10213
   526
qed "split_paired_Bex_Sigma";
nipkow@10213
   527
Addsimps [split_paired_Bex_Sigma];
nipkow@10213
   528
nipkow@10213
   529
Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))";
nipkow@10213
   530
by (Blast_tac 1);
nipkow@10213
   531
qed "Sigma_Un_distrib1";
nipkow@10213
   532
nipkow@10213
   533
Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))";
nipkow@10213
   534
by (Blast_tac 1);
nipkow@10213
   535
qed "Sigma_Un_distrib2";
nipkow@10213
   536
nipkow@10213
   537
Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))";
nipkow@10213
   538
by (Blast_tac 1);
nipkow@10213
   539
qed "Sigma_Int_distrib1";
nipkow@10213
   540
nipkow@10213
   541
Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))";
nipkow@10213
   542
by (Blast_tac 1);
nipkow@10213
   543
qed "Sigma_Int_distrib2";
nipkow@10213
   544
nipkow@10213
   545
Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))";
nipkow@10213
   546
by (Blast_tac 1);
nipkow@10213
   547
qed "Sigma_Diff_distrib1";
nipkow@10213
   548
nipkow@10213
   549
Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))";
nipkow@10213
   550
by (Blast_tac 1);
nipkow@10213
   551
qed "Sigma_Diff_distrib2";
nipkow@10213
   552
nipkow@10213
   553
Goal "Sigma (Union X) B = (UN A:X. Sigma A B)";
nipkow@10213
   554
by (Blast_tac 1);
nipkow@10213
   555
qed "Sigma_Union";
nipkow@10213
   556
nipkow@10213
   557
(*Non-dependent versions are needed to avoid the need for higher-order
nipkow@10213
   558
  matching, especially when the rules are re-oriented*)
nipkow@10213
   559
Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)";
nipkow@10213
   560
by (Blast_tac 1);
nipkow@10213
   561
qed "Times_Un_distrib1";
nipkow@10213
   562
nipkow@10213
   563
Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)";
nipkow@10213
   564
by (Blast_tac 1);
nipkow@10213
   565
qed "Times_Int_distrib1";
nipkow@10213
   566
nipkow@10213
   567
Goal "(A - B) <*> C = (A <*> C) - (B <*> C)";
nipkow@10213
   568
by (Blast_tac 1);
nipkow@10213
   569
qed "Times_Diff_distrib1";
nipkow@10213
   570
nipkow@10213
   571
nipkow@10213
   572
(*Attempts to remove occurrences of split, and pair-valued parameters*)
wenzelm@10918
   573
val remove_split = rewrite_rule [split_conv RS eq_reflection] o split_all;
nipkow@10213
   574
nipkow@10213
   575
local
nipkow@10213
   576
nipkow@10213
   577
(*In ap_split S T u, term u expects separate arguments for the factors of S,
nipkow@10213
   578
  with result type T.  The call creates a new term expecting one argument
nipkow@10213
   579
  of type S.*)
nipkow@10213
   580
fun ap_split (Type ("*", [T1, T2])) T3 u =
nipkow@10213
   581
      HOLogic.split_const (T1, T2, T3) $
nipkow@10213
   582
      Abs("v", T1,
nipkow@10213
   583
          ap_split T2 T3
nipkow@10213
   584
             ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
nipkow@10213
   585
              Bound 0))
nipkow@10213
   586
  | ap_split T T3 u = u;
nipkow@10213
   587
nipkow@10213
   588
(*Curries any Var of function type in the rule*)
nipkow@10213
   589
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
nipkow@10213
   590
      let val T' = HOLogic.prodT_factors T1 ---> T2
nipkow@10213
   591
          val newt = ap_split T1 T2 (Var (v, T'))
nipkow@10213
   592
          val cterm = Thm.cterm_of (#sign (rep_thm rl))
nipkow@10213
   593
      in
nipkow@10213
   594
          instantiate ([], [(cterm t, cterm newt)]) rl
nipkow@10213
   595
      end
nipkow@10213
   596
  | split_rule_var' (t, rl) = rl;
nipkow@10213
   597
berghofe@10989
   598
(*** Complete splitting of partially splitted rules ***)
berghofe@10989
   599
berghofe@10989
   600
fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
berghofe@10989
   601
      (ap_split T (flat (map HOLogic.prodT_factors Ts) ---> U)
berghofe@10989
   602
        (incr_boundvars 1 u) $ Bound 0))
berghofe@10989
   603
  | ap_split' _ _ u = u;
berghofe@10989
   604
berghofe@10989
   605
fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
berghofe@10989
   606
      let
berghofe@10989
   607
        val cterm = Thm.cterm_of (#sign (rep_thm rl))
berghofe@10989
   608
        val (Us', U') = strip_type T;
berghofe@10989
   609
        val Us = take (length ts, Us');
berghofe@10989
   610
        val U = drop (length ts, Us') ---> U';
berghofe@10989
   611
        val T' = flat (map HOLogic.prodT_factors Us) ---> U;
berghofe@10999
   612
        fun mk_tuple ((xs, insts), v as Var ((a, _), T)) =
berghofe@10999
   613
              let
berghofe@10999
   614
                val Ts = HOLogic.prodT_factors T;
berghofe@10999
   615
                val ys = variantlist (replicate (length Ts) a, xs);
berghofe@10999
   616
              in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
berghofe@10999
   617
                (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
berghofe@10999
   618
              end
berghofe@10999
   619
          | mk_tuple (x, _) = x;
berghofe@10989
   620
        val newt = ap_split' Us U (Var (v, T'));
berghofe@10989
   621
        val cterm = Thm.cterm_of (#sign (rep_thm rl));
berghofe@10999
   622
        val (vs', insts) = foldl mk_tuple ((vs, []), ts);
berghofe@10989
   623
      in
berghofe@10989
   624
        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
berghofe@10989
   625
      end
berghofe@10989
   626
  | complete_split_rule_var (_, x) = x;
berghofe@10989
   627
berghofe@10989
   628
fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t)
berghofe@10989
   629
  | collect_vars (vs, t) = (case strip_comb t of
berghofe@10999
   630
        (v as Var _, ts) => (v, ts)::vs
berghofe@10989
   631
      | (t, ts) => foldl collect_vars (vs, ts));
berghofe@10989
   632
nipkow@10213
   633
in
nipkow@10213
   634
nipkow@10213
   635
val split_rule_var = standard o remove_split o split_rule_var';
nipkow@10213
   636
nipkow@10213
   637
(*Curries ALL function variables occurring in a rule's conclusion*)
wenzelm@10829
   638
fun split_rule rl = standard (remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl)));
nipkow@10213
   639
berghofe@10989
   640
fun complete_split_rule rl =
berghofe@10989
   641
  standard (remove_split (fst (foldr complete_split_rule_var
berghofe@10989
   642
    (collect_vars ([], concl_of rl),
berghofe@10989
   643
     (rl, map (fst o fst o dest_Var) (term_vars (#prop (rep_thm rl))))))));
berghofe@10989
   644
nipkow@10213
   645
end;