src/HOL/Sum.ML
changeset 7014 11ee650edcd2
parent 5316 7a8975451a89
child 7031 972b5f62f476
     1.1 --- a/src/HOL/Sum.ML	Fri Jul 16 12:02:06 1999 +0200
     1.2 +++ b/src/HOL/Sum.ML	Fri Jul 16 12:09:48 1999 +0200
     1.3 @@ -167,6 +167,17 @@
     1.4    "s=t ==> sum_case f g s = sum_case f g t"
     1.5    (fn [prem] => [rtac (prem RS arg_cong) 1]);
     1.6  
     1.7 +val [p1,p2] = Goal "[| sum_case f1 f2 = sum_case g1 g2;  \
     1.8 +  \  [| f1 = g1; f2 = g2 |] ==> P |] ==> P";
     1.9 +by (cut_facts_tac [p1] 1);
    1.10 +br p2 1;
    1.11 +br ext 1;
    1.12 +by (dres_inst_tac [("x","Inl x")] fun_cong 1);
    1.13 +by (Asm_full_simp_tac 1);
    1.14 +br ext 1;
    1.15 +by (dres_inst_tac [("x","Inr x")] fun_cong 1);
    1.16 +by (Asm_full_simp_tac 1);
    1.17 +qed "sum_case_inject";
    1.18  
    1.19  
    1.20  (** Rules for the Part primitive **)