src/HOLCF/Sprod.thy
changeset 27310 d0229bc6c461
parent 26962 c8b20f615d6c
child 29063 7619f0561cd7
     1.1 --- a/src/HOLCF/Sprod.thy	Fri Jun 20 22:51:50 2008 +0200
     1.2 +++ b/src/HOLCF/Sprod.thy	Fri Jun 20 23:01:09 2008 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4    Rep_Sprod_inject [symmetric] less_Sprod_def
     1.5    Rep_Sprod_strict Rep_Sprod_spair
     1.6  
     1.7 -lemma Exh_Sprod2:
     1.8 +lemma Exh_Sprod:
     1.9    "z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)"
    1.10  apply (insert Rep_Sprod [of z])
    1.11  apply (simp add: Rep_Sprod_simps eq_cprod)
    1.12 @@ -85,7 +85,7 @@
    1.13  
    1.14  lemma sprodE [cases type: **]:
    1.15    "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    1.16 -by (cut_tac z=p in Exh_Sprod2, auto)
    1.17 +by (cut_tac z=p in Exh_Sprod, auto)
    1.18  
    1.19  lemma sprod_induct [induct type: **]:
    1.20    "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
    1.21 @@ -222,11 +222,14 @@
    1.22  subsection {* Strict product preserves flatness *}
    1.23  
    1.24  instance "**" :: (flat, flat) flat
    1.25 -apply (intro_classes, clarify)
    1.26 -apply (rule_tac p=x in sprodE, simp)
    1.27 -apply (rule_tac p=y in sprodE, simp)
    1.28 -apply (simp add: flat_less_iff spair_less)
    1.29 -done
    1.30 +proof
    1.31 +  fix x y :: "'a \<otimes> 'b"
    1.32 +  assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
    1.33 +    apply (induct x, simp)
    1.34 +    apply (induct y, simp)
    1.35 +    apply (simp add: spair_less_iff flat_less_iff)
    1.36 +    done
    1.37 +qed
    1.38  
    1.39  subsection {* Strict product is a bifinite domain *}
    1.40  
    1.41 @@ -239,7 +242,7 @@
    1.42  
    1.43  instance proof
    1.44    fix i :: nat and x :: "'a \<otimes> 'b"
    1.45 -  show "chain (\<lambda>i. approx i\<cdot>x)"
    1.46 +  show "chain (approx :: nat \<Rightarrow> 'a \<otimes> 'b \<rightarrow> 'a \<otimes> 'b)"
    1.47      unfolding approx_sprod_def by simp
    1.48    show "(\<Squnion>i. approx i\<cdot>x) = x"
    1.49      unfolding approx_sprod_def
    1.50 @@ -249,7 +252,7 @@
    1.51      by (simp add: ssplit_def strictify_conv_if)
    1.52    have "Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x} \<subseteq> {x. approx i\<cdot>x = x}"
    1.53      unfolding approx_sprod_def
    1.54 -    apply (clarify, rule_tac p=x in sprodE)
    1.55 +    apply (clarify, case_tac x)
    1.56       apply (simp add: Rep_Sprod_strict)
    1.57      apply (simp add: Rep_Sprod_spair spair_eq_iff)
    1.58      done