src/HOL/Library/Option_ord.thy
changeset 56166 9a241bc276cd
parent 52729 412c9e0381a1
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Option_ord.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Library/Option_ord.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -292,11 +292,11 @@
     1.4  
     1.5  lemma Some_INF:
     1.6    "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
     1.7 -  by (simp add: INF_def Some_Inf image_image)
     1.8 +  using Some_Inf [of "f ` A"] by (simp add: comp_def)
     1.9  
    1.10  lemma Some_SUP:
    1.11    "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
    1.12 -  by (simp add: SUP_def Some_Sup image_image)
    1.13 +  using Some_Sup [of "f ` A"] by (simp add: comp_def)
    1.14  
    1.15  instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
    1.16  begin
    1.17 @@ -319,7 +319,7 @@
    1.18        case False then have B: "{x \<in> B. \<exists>y. x = Some y} = B" by auto (metis not_Some_eq)
    1.19        from sup_Inf have "Some c \<squnion> Some (\<Sqinter>Option.these B) = Some (\<Sqinter>b\<in>Option.these B. c \<squnion> b)" by simp
    1.20        then have "Some c \<squnion> \<Sqinter>(Some ` Option.these B) = (\<Sqinter>x\<in>Some ` Option.these B. Some c \<squnion> x)"
    1.21 -        by (simp add: Some_INF Some_Inf)
    1.22 +        by (simp add: Some_INF Some_Inf comp_def)
    1.23        with Some B show ?thesis by (simp add: Some_image_these_eq)
    1.24      qed
    1.25    qed
    1.26 @@ -332,7 +332,7 @@
    1.27      show ?thesis
    1.28      proof (cases "B = {} \<or> B = {None}")
    1.29        case True
    1.30 -      then show ?thesis by (auto simp add: SUP_def)
    1.31 +      then show ?thesis by auto
    1.32      next
    1.33        have B: "B = {x \<in> B. \<exists>y. x = Some y} \<union> {x \<in> B. x = None}"
    1.34          by auto
    1.35 @@ -347,7 +347,7 @@
    1.36        moreover from inf_Sup have "Some c \<sqinter> Some (\<Squnion>Option.these B) = Some (\<Squnion>b\<in>Option.these B. c \<sqinter> b)"
    1.37          by simp
    1.38        ultimately have "Some c \<sqinter> \<Squnion>(Some ` Option.these B) = (\<Squnion>x\<in>Some ` Option.these B. Some c \<sqinter> x)"
    1.39 -        by (simp add: Some_SUP Some_Sup)
    1.40 +        by (simp add: Some_SUP Some_Sup comp_def)
    1.41        with Some show ?thesis
    1.42          by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib)
    1.43      qed