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  {*
```