src/HOL/Sum.ML
changeset 7293 959e060f4a2f
parent 7254 fc7f95f293da
child 9108 9fff97d29837
     1.1 --- a/src/HOL/Sum.ML	Thu Aug 19 18:36:41 1999 +0200
     1.2 +++ b/src/HOL/Sum.ML	Thu Aug 19 19:00:42 1999 +0200
     1.3 @@ -114,18 +114,6 @@
     1.4  AddSEs [PlusE];
     1.5  
     1.6  
     1.7 -(** sum_case -- the selection operator for sums **)
     1.8 -
     1.9 -Goalw [sum_case_def] "basic_sum_case f g (Inl x) = f(x)";
    1.10 -by (Blast_tac 1);
    1.11 -qed "sum_case_Inl";
    1.12 -
    1.13 -Goalw [sum_case_def] "basic_sum_case f g (Inr x) = g(x)";
    1.14 -by (Blast_tac 1);
    1.15 -qed "sum_case_Inr";
    1.16 -
    1.17 -Addsimps [sum_case_Inl, sum_case_Inr];
    1.18 -
    1.19  (** Exhaustion rule for sums -- a degenerate form of induction **)
    1.20  
    1.21  val prems = Goalw [Inl_def,Inr_def]
    1.22 @@ -143,42 +131,6 @@
    1.23  by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
    1.24  qed "sum_induct";
    1.25  
    1.26 -Goal "basic_sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    1.27 -by (EVERY1 [res_inst_tac [("s","s")] sumE, 
    1.28 -            etac ssubst, rtac sum_case_Inl,
    1.29 -            etac ssubst, rtac sum_case_Inr]);
    1.30 -qed "surjective_sum";
    1.31 -
    1.32 -Goal "R(basic_sum_case f g s) = \
    1.33 -\             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
    1.34 -by (res_inst_tac [("s","s")] sumE 1);
    1.35 -by Auto_tac;
    1.36 -qed "split_sum_case";
    1.37 -
    1.38 -Goal "P (basic_sum_case f g s) = \
    1.39 -\     (~ ((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))";
    1.40 -by (stac split_sum_case 1);
    1.41 -by (Blast_tac 1);
    1.42 -qed "split_sum_case_asm";
    1.43 -
    1.44 -(*Prevents simplification of f and g: much faster*)
    1.45 -Goal "s=t ==> basic_sum_case f g s = basic_sum_case f g t";
    1.46 -by (etac arg_cong 1);
    1.47 -qed "sum_case_weak_cong";
    1.48 -
    1.49 -val [p1,p2] = Goal
    1.50 -  "[| basic_sum_case f1 f2 = basic_sum_case g1 g2;  \
    1.51 -\     [| f1 = g1; f2 = g2 |] ==> P |] \
    1.52 -\  ==> P";
    1.53 -by (rtac p2 1);
    1.54 -by (rtac ext 1);
    1.55 -by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
    1.56 -by (Asm_full_simp_tac 1);
    1.57 -by (rtac ext 1);
    1.58 -by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
    1.59 -by (Asm_full_simp_tac 1);
    1.60 -qed "sum_case_inject";
    1.61 -
    1.62  
    1.63  (** Rules for the Part primitive **)
    1.64  
    1.65 @@ -222,7 +174,6 @@
    1.66  by (Blast_tac 1);
    1.67  qed "Part_Int";
    1.68  
    1.69 -(*For inductive definitions*)
    1.70  Goal "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}";
    1.71  by (Blast_tac 1);
    1.72  qed "Part_Collect";