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