added subsection headings, cleaned up some proofs
authorhuffman
Tue Mar 08 00:15:01 2005 +0100 (2005-03-08)
changeset 1559017f4f5afcd5f
parent 15589 69bea57212ef
child 15591 50c3384ca6c4
added subsection headings, cleaned up some proofs
src/HOLCF/Discrete.thy
     1.1 --- a/src/HOLCF/Discrete.thy	Tue Mar 08 00:11:49 2005 +0100
     1.2 +++ b/src/HOLCF/Discrete.thy	Tue Mar 08 00:15:01 2005 +0100
     1.3 @@ -14,6 +14,8 @@
     1.4  
     1.5  datatype 'a discr = Discr "'a :: type"
     1.6  
     1.7 +subsection {* Type @{typ "'a discr"} is a partial order *}
     1.8 +
     1.9  instance discr :: (type) sq_ord ..
    1.10  
    1.11  defs (overloaded)
    1.12 @@ -32,6 +34,8 @@
    1.13    { assume "x << y" and "y << z" thus "x << z" by simp }
    1.14  qed
    1.15  
    1.16 +subsection {* Type @{typ "'a discr"} is a cpo *}
    1.17 +
    1.18  lemma discr_chain0: 
    1.19   "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
    1.20  apply (unfold chain_def)
    1.21 @@ -54,26 +58,25 @@
    1.22  apply (simp (no_asm_simp))
    1.23  done
    1.24  
    1.25 -instance discr :: (type)cpo
    1.26 -by (intro_classes, rule discr_cpo)
    1.27 +instance discr :: (type) cpo
    1.28 +by intro_classes (rule discr_cpo)
    1.29 +
    1.30 +subsection {* @{term undiscr} *}
    1.31  
    1.32  constdefs
    1.33     undiscr :: "('a::type)discr => 'a"
    1.34    "undiscr x == (case x of Discr y => y)"
    1.35  
    1.36  lemma undiscr_Discr [simp]: "undiscr(Discr x) = x"
    1.37 -apply (unfold undiscr_def)
    1.38 -apply (simp (no_asm))
    1.39 -done
    1.40 +by (simp add: undiscr_def)
    1.41  
    1.42  lemma discr_chain_f_range0:
    1.43   "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
    1.44 -apply (fast dest: discr_chain0 elim: arg_cong)
    1.45 -done
    1.46 +by (fast dest: discr_chain0 elim: arg_cong)
    1.47  
    1.48  lemma cont_discr [iff]: "cont(%x::('a::type)discr. f x)"
    1.49  apply (unfold cont is_lub_def is_ub_def)
    1.50 -apply (simp (no_asm) add: discr_chain_f_range0)
    1.51 +apply (simp add: discr_chain_f_range0)
    1.52  done
    1.53  
    1.54  end