src/HOL/Sum_Type.thy
changeset 33961 03f2ab6a4ea6
parent 31080 21ffc770ebc0
child 33962 abf9fa17452a
     1.1 --- a/src/HOL/Sum_Type.thy	Wed Nov 25 11:16:57 2009 +0100
     1.2 +++ b/src/HOL/Sum_Type.thy	Wed Nov 25 11:16:58 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header{*The Disjoint Sum of Two Types*}
     1.5  
     1.6  theory Sum_Type
     1.7 -imports Typedef Fun
     1.8 +imports Typedef Inductive Fun
     1.9  begin
    1.10  
    1.11  text{*The representations of the two injections*}
    1.12 @@ -191,6 +191,74 @@
    1.13  lemma Part_Collect: "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}"
    1.14  by blast
    1.15  
    1.16 +subsection {* Representing sums *}
    1.17 +
    1.18 +rep_datatype (sum) Inl Inr
    1.19 +proof -
    1.20 +  fix P
    1.21 +  fix s :: "'a + 'b"
    1.22 +  assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
    1.23 +  then show "P s" by (auto intro: sumE [of s])
    1.24 +qed simp_all
    1.25 +
    1.26 +lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
    1.27 +  by (rule ext) (simp split: sum.split)
    1.28 +
    1.29 +lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
    1.30 +  apply (rule_tac s = s in sumE)
    1.31 +   apply (erule ssubst)
    1.32 +   apply (rule sum.cases(1))
    1.33 +  apply (erule ssubst)
    1.34 +  apply (rule sum.cases(2))
    1.35 +  done
    1.36 +
    1.37 +lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
    1.38 +  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
    1.39 +  by simp
    1.40 +
    1.41 +lemma sum_case_inject:
    1.42 +  "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
    1.43 +proof -
    1.44 +  assume a: "sum_case f1 f2 = sum_case g1 g2"
    1.45 +  assume r: "f1 = g1 ==> f2 = g2 ==> P"
    1.46 +  show P
    1.47 +    apply (rule r)
    1.48 +     apply (rule ext)
    1.49 +     apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
    1.50 +    apply (rule ext)
    1.51 +    apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
    1.52 +    done
    1.53 +qed
    1.54 +
    1.55 +constdefs
    1.56 +  Suml :: "('a => 'c) => 'a + 'b => 'c"
    1.57 +  "Suml == (%f. sum_case f undefined)"
    1.58 +
    1.59 +  Sumr :: "('b => 'c) => 'a + 'b => 'c"
    1.60 +  "Sumr == sum_case undefined"
    1.61 +
    1.62 +lemma [code]:
    1.63 +  "Suml f (Inl x) = f x"
    1.64 +  by (simp add: Suml_def)
    1.65 +
    1.66 +lemma [code]:
    1.67 +  "Sumr f (Inr x) = f x"
    1.68 +  by (simp add: Sumr_def)
    1.69 +
    1.70 +lemma Suml_inject: "Suml f = Suml g ==> f = g"
    1.71 +  by (unfold Suml_def) (erule sum_case_inject)
    1.72 +
    1.73 +lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
    1.74 +  by (unfold Sumr_def) (erule sum_case_inject)
    1.75 +
    1.76 +primrec Projl :: "'a + 'b => 'a"
    1.77 +where Projl_Inl: "Projl (Inl x) = x"
    1.78 +
    1.79 +primrec Projr :: "'a + 'b => 'b"
    1.80 +where Projr_Inr: "Projr (Inr x) = x"
    1.81 +
    1.82 +hide (open) const Suml Sumr Projl Projr
    1.83 +
    1.84  
    1.85  ML
    1.86  {*