src/HOL/Product_Type.thy

 lemma ProdI: "Pair_Rep a b : Prod"
   by (unfold Prod_def) blast
 
 lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' ==> a = a' & b = b'"
   apply (unfold Pair_Rep_def)
-  apply (drule fun_cong [THEN fun_cong])
-  apply blast
+  apply (drule fun_cong [THEN fun_cong], blast)
   done
 
 lemma inj_on_Abs_Prod: "inj_on Abs_Prod Prod"
   apply (rule inj_on_inverseI)
   apply (erule Abs_Prod_inverse)

 lemmas splitD = split_conv [THEN iffD1, standard]
 
 lemma split_Pair_apply: "split (%x y. f (x, y)) = f"
   -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
   apply (rule ext)
-  apply (tactic {* pair_tac "x" 1 *})
-  apply simp
+  apply (tactic {* pair_tac "x" 1 *}, simp)
   done
 
 lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))"
   -- {* Can't be added to simpset: loops! *}
   by (simp add: split_Pair_apply)
 
 lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
   by (simp add: split_def)
 
 lemma Pair_fst_snd_eq: "!!s t. (s = t) = (fst s = fst t & snd s = snd t)"
-  apply (simp only: split_tupled_all)
-  apply simp
-  done
+by (simp only: split_tupled_all, simp)
 
 lemma prod_eqI [intro?]: "fst p = fst q ==> snd p = snd q ==> p = q"
   by (simp add: Pair_fst_snd_eq)
 
 lemma split_weak_cong: "p = q ==> split c p = split c q"

   by (subst surjective_pairing, rule split_conv)
 
 lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))"
   -- {* For use with @{text split} and the Simplifier. *}
   apply (subst surjective_pairing)
-  apply (subst split_conv)
-  apply blast
+  apply (subst split_conv, blast)
   done
 
 text {*
   @{thm [source] split_split} could be declared as @{text "[split]"}
   done after the Splitter has been speeded up significantly;
   precompute the constants involved and don't do anything unless the
   current goal contains one of those constants.
 *}
 
 lemma split_split_asm: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
-  apply (subst split_split)
-  apply simp
-  done
+by (subst split_split, simp)
 
 
 text {*
   \medskip @{term split} used as a logical connective or set former.
 

 
 lemma mem_splitI: "z: c a b ==> z: split c (a, b)"
   by simp
 
 lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: split c p"
-  apply (simp only: split_tupled_all)
-  apply simp
-  done
+by (simp only: split_tupled_all, simp)
 
 lemma mem_splitE: "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"
 proof -
   case rule_context [unfolded split_def]
   show ?thesis by (rule rule_context surjective_pairing)+

    to quite time-consuming computations (in particular for nested tuples) *)
 claset_ref() := claset() addSbefore (\"split_conv_tac\", split_conv_tac);
 "
 
 lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
-  apply (rule ext)
-  apply fast
-  done
+by (rule ext, fast)
 
 lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
-  apply (rule ext)
-  apply fast
-  done
+by (rule ext, fast)
 
 lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
   -- {* Allows simplifications of nested splits in case of independent predicates. *}
-  apply (rule ext)
-  apply blast
+  apply (rule ext, blast)
   done
 
 lemma split_comp_eq [simp]: 
 "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
 by (rule ext, auto)

 the following  would be slightly more general,
 but cannot be used as rewrite rule:
 ### Cannot add premise as rewrite rule because it contains (type) unknowns:
 ### ?y = .x
 Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)"
-by (rtac some_equality 1);
-by ( Simp_tac 1);
-by (split_all_tac 1);
-by (Asm_full_simp_tac 1);
+by (rtac some_equality 1)
+by ( Simp_tac 1)
+by (split_all_tac 1)
+by (Asm_full_simp_tac 1)
 qed "The_split_eq";
 *)
 
 lemma injective_fst_snd: "!!x y. [|fst x = fst y; snd x = snd y|] ==> x = y"
   by auto

 lemma prod_fun [simp]: "prod_fun f g (a, b) = (f a, g b)"
   by (simp add: prod_fun_def)
 
 lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
   apply (rule ext)
-  apply (tactic {* pair_tac "x" 1 *})
-  apply simp
+  apply (tactic {* pair_tac "x" 1 *}, simp)
   done
 
 lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
   apply (rule ext)
-  apply (tactic {* pair_tac "z" 1 *})
-  apply simp
+  apply (tactic {* pair_tac "z" 1 *}, simp)
   done
 
 lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r"
   apply (rule image_eqI)
-  apply (rule prod_fun [symmetric])
-  apply assumption
+  apply (rule prod_fun [symmetric], assumption)
   done
 
 lemma prod_fun_imageE [elim!]:
   "[| c: (prod_fun f g)`r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P
     |] ==> P"

   Elimination of @{term "(a, b) : A \<times> B"} -- introduces no
   eigenvariables.
 *}
 
 lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
-  apply (erule SigmaE)
-  apply blast
-  done
+by (erule SigmaE, blast)
 
 lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
-  apply (erule SigmaE)
-  apply blast
-  done
+by (erule SigmaE, blast)
 
 lemma SigmaE2:
     "[| (a, b) : Sigma A B;
         [| a:A;  b:B(a) |] ==> P
      |] ==> P"