instance "*" :: (sq_ord, sq_ord) sq_ord
authorhuffman
Sat Feb 02 03:28:36 2008 +0100 (2008-02-02)
changeset 260359f8810c42604
parent 26034 97d00128072b
child 26036 f9e779f11949
instance "*" :: (sq_ord, sq_ord) sq_ord
src/HOLCF/Cprod.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Sat Feb 02 03:26:40 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Sat Feb 02 03:28:36 2008 +0100
     1.3 @@ -45,13 +45,16 @@
     1.4  
     1.5  subsection {* Product type is a partial order *}
     1.6  
     1.7 -instantiation "*" :: (po, po) po
     1.8 +instantiation "*" :: (sq_ord, sq_ord) sq_ord
     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 +instance ..
    1.16 +end
    1.17 +
    1.18 +instance "*" :: (po, po) po
    1.19  proof
    1.20    fix x :: "'a \<times> 'b"
    1.21    show "x \<sqsubseteq> x"
    1.22 @@ -68,8 +71,6 @@
    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  lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"