src/HOL/Datatype.thy
changeset 22782 8bc6fbbe1d0f
parent 22744 5cbe966d67a2
child 22886 cdff6ef76009
     1.1 --- a/src/HOL/Datatype.thy	Tue Apr 24 15:17:22 2007 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Tue Apr 24 15:18:09 2007 +0200
     1.3 @@ -553,6 +553,26 @@
     1.4    inject Pair_eq
     1.5    induction prod_induct
     1.6  
     1.7 +lemmas prod_caseI = prod.cases [THEN iffD2, standard]
     1.8 +
     1.9 +lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
    1.10 +  by auto
    1.11 +
    1.12 +lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x"
    1.13 +  by (auto simp: split_tupled_all)
    1.14 +
    1.15 +lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
    1.16 +  by (induct p) auto
    1.17 +
    1.18 +lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
    1.19 +  by (induct p) auto
    1.20 +
    1.21 +lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
    1.22 +  by (simp add: expand_fun_eq)
    1.23 +
    1.24 +declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
    1.25 +declare prod_caseE' [elim!] prod_caseE [elim!]
    1.26 +
    1.27  rep_datatype sum
    1.28    distinct Inl_not_Inr Inr_not_Inl
    1.29    inject Inl_eq Inr_eq