cleaned up instance proofs
authorhuffman
Mon Jan 14 20:45:10 2008 +0100 (2008-01-14)
changeset 25908d8ce142f7e6e
parent 25907 695a9d88d697
child 25909 6b96b9392873
cleaned up instance proofs
src/HOLCF/Cprod.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Mon Jan 14 20:35:52 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Mon Jan 14 20:45:10 2008 +0100
     1.3 @@ -44,16 +44,13 @@
     1.4  
     1.5  subsection {* Product type is a partial order *}
     1.6  
     1.7 -instantiation "*" :: (sq_ord, sq_ord) sq_ord
     1.8 +instantiation "*" :: (po, po) po
     1.9  begin
    1.10  
    1.11  definition
    1.12    less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
    1.13  
    1.14 -instance ..
    1.15 -end
    1.16 -
    1.17 -instance "*" :: (po, po) po
    1.18 +instance
    1.19  proof
    1.20    fix x :: "'a \<times> 'b"
    1.21    show "x \<sqsubseteq> x"
    1.22 @@ -70,6 +67,7 @@
    1.23      by (fast intro: trans_less)
    1.24  qed
    1.25  
    1.26 +end
    1.27  
    1.28  subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    1.29  
    1.30 @@ -138,16 +136,10 @@
    1.31  lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
    1.32  by (simp add: less_cprod_def)
    1.33  
    1.34 -lemma least_cprod: "EX x::'a::pcpo * 'b::pcpo. ALL y. x \<sqsubseteq> y"
    1.35 -apply (rule_tac x = "(\<bottom>, \<bottom>)" in exI)
    1.36 -apply (rule minimal_cprod [THEN allI])
    1.37 -done
    1.38 +instance "*" :: (pcpo, pcpo) pcpo
    1.39 +by intro_classes (fast intro: minimal_cprod)
    1.40  
    1.41 -instance "*" :: (pcpo, pcpo) pcpo
    1.42 -by intro_classes (rule least_cprod)
    1.43 -
    1.44 -text {* for compatibility with old HOLCF-Version *}
    1.45 -lemma inst_cprod_pcpo: "UU = (UU,UU)"
    1.46 +lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
    1.47  by (rule minimal_cprod [THEN UU_I, symmetric])
    1.48  
    1.49