src/HOL/Sum_Type.thy
changeset 37388 793618618f78
parent 36176 3fe7e97ccca8
child 37678 0040bafffdef
     1.1 --- a/src/HOL/Sum_Type.thy	Tue Jun 08 16:37:19 2010 +0200
     1.2 +++ b/src/HOL/Sum_Type.thy	Tue Jun 08 16:37:22 2010 +0200
     1.3 @@ -17,21 +17,17 @@
     1.4  definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
     1.5    "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
     1.6  
     1.7 -global
     1.8 -
     1.9 -typedef (Sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
    1.10 +typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
    1.11    by auto
    1.12  
    1.13 -local
    1.14 -
    1.15 -lemma Inl_RepI: "Inl_Rep a \<in> Sum"
    1.16 -  by (auto simp add: Sum_def)
    1.17 +lemma Inl_RepI: "Inl_Rep a \<in> sum"
    1.18 +  by (auto simp add: sum_def)
    1.19  
    1.20 -lemma Inr_RepI: "Inr_Rep b \<in> Sum"
    1.21 -  by (auto simp add: Sum_def)
    1.22 +lemma Inr_RepI: "Inr_Rep b \<in> sum"
    1.23 +  by (auto simp add: sum_def)
    1.24  
    1.25 -lemma inj_on_Abs_Sum: "A \<subseteq> Sum \<Longrightarrow> inj_on Abs_Sum A"
    1.26 -  by (rule inj_on_inverseI, rule Abs_Sum_inverse) auto
    1.27 +lemma inj_on_Abs_sum: "A \<subseteq> sum \<Longrightarrow> inj_on Abs_sum A"
    1.28 +  by (rule inj_on_inverseI, rule Abs_sum_inverse) auto
    1.29  
    1.30  lemma Inl_Rep_inject: "inj_on Inl_Rep A"
    1.31  proof (rule inj_onI)
    1.32 @@ -49,28 +45,28 @@
    1.33    by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq)
    1.34  
    1.35  definition Inl :: "'a \<Rightarrow> 'a + 'b" where
    1.36 -  "Inl = Abs_Sum \<circ> Inl_Rep"
    1.37 +  "Inl = Abs_sum \<circ> Inl_Rep"
    1.38  
    1.39  definition Inr :: "'b \<Rightarrow> 'a + 'b" where
    1.40 -  "Inr = Abs_Sum \<circ> Inr_Rep"
    1.41 +  "Inr = Abs_sum \<circ> Inr_Rep"
    1.42  
    1.43  lemma inj_Inl [simp]: "inj_on Inl A"
    1.44 -by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_Sum Inl_RepI)
    1.45 +by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
    1.46  
    1.47  lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
    1.48  using inj_Inl by (rule injD)
    1.49  
    1.50  lemma inj_Inr [simp]: "inj_on Inr A"
    1.51 -by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_Sum Inr_RepI)
    1.52 +by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
    1.53  
    1.54  lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
    1.55  using inj_Inr by (rule injD)
    1.56  
    1.57  lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
    1.58  proof -
    1.59 -  from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> Sum" by auto
    1.60 -  with inj_on_Abs_Sum have "inj_on Abs_Sum {Inl_Rep a, Inr_Rep b}" .
    1.61 -  with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_Sum (Inl_Rep a) \<noteq> Abs_Sum (Inr_Rep b)" by auto
    1.62 +  from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" by auto
    1.63 +  with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
    1.64 +  with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)" by auto
    1.65    then show ?thesis by (simp add: Inl_def Inr_def)
    1.66  qed
    1.67  
    1.68 @@ -81,10 +77,10 @@
    1.69    assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
    1.70      and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
    1.71    shows P
    1.72 -proof (rule Abs_Sum_cases [of s])
    1.73 +proof (rule Abs_sum_cases [of s])
    1.74    fix f 
    1.75 -  assume "s = Abs_Sum f" and "f \<in> Sum"
    1.76 -  with assms show P by (auto simp add: Sum_def Inl_def Inr_def)
    1.77 +  assume "s = Abs_sum f" and "f \<in> sum"
    1.78 +  with assms show P by (auto simp add: sum_def Inl_def Inr_def)
    1.79  qed
    1.80  
    1.81  rep_datatype (sum) Inl Inr