eliminated the constant less by the introduction of the axclass sq_ord
authorslotosch
Sun May 25 11:07:52 1997 +0200 (1997-05-25)
changeset 3323194ae2e0c193
parent 3322 bc4d107fb6dd
child 3324 6b26b886ff69
eliminated the constant less by the introduction of the axclass sq_ord
added explicit type ::'a::po in the following theorems:
minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair
and dist_eqI (in domain-package)
added instances
instance fun :: (term,sq_ord)sq_ord
instance "->" :: (term,sq_ord)sq_ord
instance "**" :: (sq_ord,sq_ord)sq_ord
instance "*" :: (sq_ord,sq_ord)sq_ord
instance "++" :: (pcpo,pcpo)sq_ord
instance u :: (sq_ord)sq_ord
instance lift :: (term)sq_ord
instance discr :: (term)sq_ord
src/HOLCF/Cfun1.ML
src/HOLCF/Cfun1.thy
src/HOLCF/Cfun2.ML
src/HOLCF/Cont.thy
src/HOLCF/Cprod1.ML
src/HOLCF/Cprod1.thy
src/HOLCF/Cprod2.ML
src/HOLCF/Discrete0.ML
src/HOLCF/Discrete0.thy
src/HOLCF/Discrete1.ML
src/HOLCF/Fun1.ML
src/HOLCF/Fun1.thy
src/HOLCF/Fun2.ML
src/HOLCF/Lift1.ML
src/HOLCF/Lift1.thy
src/HOLCF/Lift2.ML
src/HOLCF/Pcpo.ML
src/HOLCF/Porder0.ML
src/HOLCF/Porder0.thy
src/HOLCF/Sprod1.ML
src/HOLCF/Sprod1.thy
src/HOLCF/Sprod2.ML
src/HOLCF/Ssum1.ML
src/HOLCF/Ssum1.thy
src/HOLCF/Ssum2.ML
src/HOLCF/Up1.ML
src/HOLCF/Up1.thy
src/HOLCF/Up2.ML
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/Cfun1.ML	Fri May 23 18:55:28 1997 +0200
     1.2 +++ b/src/HOLCF/Cfun1.ML	Sun May 25 11:07:52 1997 +0200
     1.3 @@ -35,14 +35,14 @@
     1.4  (* less_cfun is a partial order on type 'a -> 'b                            *)
     1.5  (* ------------------------------------------------------------------------ *)
     1.6  
     1.7 -qed_goalw "refl_less_cfun" thy [less_cfun_def] "less(f::'a->'b) f"
     1.8 +qed_goalw "refl_less_cfun" thy [less_cfun_def] "(f::'a->'b) << f"
     1.9  (fn prems =>
    1.10          [
    1.11          (rtac refl_less 1)
    1.12          ]);
    1.13  
    1.14  qed_goalw "antisym_less_cfun" thy [less_cfun_def] 
    1.15 -        "[|less (f1::'a->'b) f2; less f2 f1|] ==> f1 = f2"
    1.16 +        "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2"
    1.17  (fn prems =>
    1.18          [
    1.19          (cut_facts_tac prems 1),
    1.20 @@ -55,7 +55,7 @@
    1.21          ]);
    1.22  
    1.23  qed_goalw "trans_less_cfun" thy [less_cfun_def] 
    1.24 -        "[|less (f1::'a->'b) f2; less f2 f3|] ==> less f1 f3"
    1.25 +        "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3"
    1.26  (fn prems =>
    1.27          [
    1.28          (cut_facts_tac prems 1),
     2.1 --- a/src/HOLCF/Cfun1.thy	Fri May 23 18:55:28 1997 +0200
     2.2 +++ b/src/HOLCF/Cfun1.thy	Sun May 25 11:07:52 1997 +0200
     2.3 @@ -13,6 +13,9 @@
     2.4  
     2.5  typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f. cont f}" (CfunI)
     2.6  
     2.7 +(* to make << defineable *)
     2.8 +instance "->"  :: (cpo,cpo)sq_ord
     2.9 +
    2.10  consts  
    2.11          fapp      :: "('a -> 'b)=>('a => 'b)"   (* usually Rep_Cfun *)
    2.12                                                  (* application      *)
    2.13 @@ -33,6 +36,6 @@
    2.14    fabs_def	"fabs==Abs_CFun"
    2.15    fapp_def	"fapp==Rep_CFun"
    2.16  
    2.17 -  less_cfun_def "less == (% fo1 fo2. fapp fo1 << fapp fo2 )"
    2.18 +  less_cfun_def "(op <<) == (% fo1 fo2. fapp fo1 << fapp fo2 )"
    2.19  
    2.20  end
     3.1 --- a/src/HOLCF/Cfun2.ML	Fri May 23 18:55:28 1997 +0200
     3.2 +++ b/src/HOLCF/Cfun2.ML	Sun May 25 11:07:52 1997 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4  qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2.fapp f1 << fapp f2)"
     3.5   (fn prems => 
     3.6          [
     3.7 -	(fold_goals_tac [po_def,less_cfun_def]),
     3.8 +	(fold_goals_tac [less_cfun_def]),
     3.9  	(rtac refl 1)
    3.10          ]);
    3.11  
     4.1 --- a/src/HOLCF/Cont.thy	Fri May 23 18:55:28 1997 +0200
     4.2 +++ b/src/HOLCF/Cont.thy	Sun May 25 11:07:52 1997 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  (* 
     4.5  
     4.6     Now we change the default class! Form now on all untyped typevariables are
     4.7 -   of default class pcpo
     4.8 +   of default class po
     4.9  
    4.10  *)
    4.11  
     5.1 --- a/src/HOLCF/Cprod1.ML	Fri May 23 18:55:28 1997 +0200
     5.2 +++ b/src/HOLCF/Cprod1.ML	Sun May 25 11:07:52 1997 +0200
     5.3 @@ -24,11 +24,11 @@
     5.4          (Asm_simp_tac 1)
     5.5          ]);
     5.6  
     5.7 -qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less (p::'a*'b) p"
     5.8 +qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "(p::'a*'b) << p"
     5.9   (fn prems => [Simp_tac 1]);
    5.10  
    5.11  qed_goalw "antisym_less_cprod" thy [less_cprod_def]
    5.12 -        "[|less (p1::'a * 'b) p2;less p2 p1|] ==> p1=p2"
    5.13 +        "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"
    5.14  (fn prems =>
    5.15          [
    5.16          (cut_facts_tac prems 1),
    5.17 @@ -38,7 +38,7 @@
    5.18          ]);
    5.19  
    5.20  qed_goalw "trans_less_cprod" thy [less_cprod_def]
    5.21 -        "[|less (p1::'a*'b) p2;less p2 p3|] ==> less p1 p3"
    5.22 +        "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"
    5.23  (fn prems =>
    5.24          [
    5.25          (cut_facts_tac prems 1),
     6.1 --- a/src/HOLCF/Cprod1.thy	Fri May 23 18:55:28 1997 +0200
     6.2 +++ b/src/HOLCF/Cprod1.thy	Sun May 25 11:07:52 1997 +0200
     6.3 @@ -12,8 +12,10 @@
     6.4  
     6.5  default cpo
     6.6  
     6.7 +instance "*"::(sq_ord,sq_ord)sq_ord 
     6.8 +
     6.9  defs
    6.10  
    6.11 -  less_cprod_def "less p1 p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
    6.12 +  less_cprod_def "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
    6.13  
    6.14  end
     7.1 --- a/src/HOLCF/Cprod2.ML	Fri May 23 18:55:28 1997 +0200
     7.2 +++ b/src/HOLCF/Cprod2.ML	Sun May 25 11:07:52 1997 +0200
     7.3 @@ -12,7 +12,7 @@
     7.4  qed_goal "inst_cprod_po" thy "(op <<)=(%x y.fst x<<fst y & snd x<<snd y)"
     7.5   (fn prems => 
     7.6          [
     7.7 -        (fold_goals_tac [po_def,less_cprod_def]),
     7.8 +        (fold_goals_tac [less_cprod_def]),
     7.9          (rtac refl 1)
    7.10          ]);
    7.11  
    7.12 @@ -71,7 +71,7 @@
    7.13          (asm_simp_tac (!simpset addsimps [inst_cprod_po]) 1)
    7.14          ]);
    7.15  
    7.16 -qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1,y1) << (x2,y2)"
    7.17 +qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
    7.18   (fn prems =>
    7.19          [
    7.20          (cut_facts_tac prems 1),
     8.1 --- a/src/HOLCF/Discrete0.ML	Fri May 23 18:55:28 1997 +0200
     8.2 +++ b/src/HOLCF/Discrete0.ML	Sun May 25 11:07:52 1997 +0200
     8.3 @@ -6,17 +6,17 @@
     8.4  Proves that 'a discr is a po
     8.5  *)
     8.6  
     8.7 -goalw thy [less_discr_def] "less (x::('a::term)discr) x";
     8.8 +goalw thy [less_discr_def] "(x::('a::term)discr) << x";
     8.9  by (rtac refl 1);
    8.10  qed "less_discr_refl";
    8.11  
    8.12  goalw thy [less_discr_def]
    8.13 -  "!!x. [| less (x::('a::term)discr) y; less y z |] ==> less x z";
    8.14 +  "!!x. [| (x::('a::term)discr) << y; y << z |] ==> x <<  z";
    8.15  by (etac trans 1);
    8.16  by (assume_tac 1);
    8.17  qed "less_discr_trans";
    8.18  
    8.19  goalw thy [less_discr_def]
    8.20 -  "!!x. [| less (x::('a::term)discr) y; less y x |] ==> x=y";
    8.21 +  "!!x. [| (x::('a::term)discr) << y; y << x |] ==> x=y";
    8.22  by (assume_tac 1);
    8.23  qed "less_discr_antisym";
     9.1 --- a/src/HOLCF/Discrete0.thy	Fri May 23 18:55:28 1997 +0200
     9.2 +++ b/src/HOLCF/Discrete0.thy	Sun May 25 11:07:52 1997 +0200
     9.3 @@ -10,7 +10,9 @@
     9.4  
     9.5  datatype 'a discr = Discr 'a
     9.6  
     9.7 +instance discr :: (term)sq_ord
     9.8 +
     9.9  defs
    9.10 -less_discr_def "(less::('a::term)discr=>'a discr=>bool)  ==  op ="
    9.11 +less_discr_def "((op <<)::('a::term)discr=>'a discr=>bool)  ==  op ="
    9.12  
    9.13  end
    10.1 --- a/src/HOLCF/Discrete1.ML	Fri May 23 18:55:28 1997 +0200
    10.2 +++ b/src/HOLCF/Discrete1.ML	Sun May 25 11:07:52 1997 +0200
    10.3 @@ -6,7 +6,7 @@
    10.4  Proves that 'a discr is a cpo
    10.5  *)
    10.6  
    10.7 -goalw thy [po_def,less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
    10.8 +goalw thy [less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
    10.9  by (rtac refl 1);
   10.10  qed "discr_less_eq";
   10.11  AddIffs [discr_less_eq];
   10.12 @@ -14,7 +14,7 @@
   10.13  goalw thy [is_chain]
   10.14   "!!S::nat=>('a::term)discr. is_chain S ==> S i = S 0";
   10.15  by (nat_ind_tac "i" 1);
   10.16 - by (rtac refl 1);
   10.17 +by (rtac refl 1);
   10.18  by (etac subst 1);
   10.19  by (rtac sym 1);
   10.20  by (Fast_tac 1);
    11.1 --- a/src/HOLCF/Fun1.ML	Fri May 23 18:55:28 1997 +0200
    11.2 +++ b/src/HOLCF/Fun1.ML	Sun May 25 11:07:52 1997 +0200
    11.3 @@ -12,14 +12,14 @@
    11.4  (* less_fun is a partial order on 'a => 'b                                  *)
    11.5  (* ------------------------------------------------------------------------ *)
    11.6  
    11.7 -qed_goalw "refl_less_fun" thy [less_fun_def] "less(f::'a::term =>'b::po) f"
    11.8 +qed_goalw "refl_less_fun" thy [less_fun_def] "(f::'a::term =>'b::po) << f"
    11.9  (fn prems =>
   11.10          [
   11.11          (fast_tac (HOL_cs addSIs [refl_less]) 1)
   11.12          ]);
   11.13  
   11.14  qed_goalw "antisym_less_fun" Fun1.thy [less_fun_def] 
   11.15 -        "[|less (f1::'a::term =>'b::po) f2; less f2 f1|] ==> f1 = f2"
   11.16 +        "[|(f1::'a::term =>'b::po) << f2; f2 << f1|] ==> f1 = f2"
   11.17  (fn prems =>
   11.18          [
   11.19          (cut_facts_tac prems 1),
   11.20 @@ -28,7 +28,7 @@
   11.21          ]);
   11.22  
   11.23  qed_goalw "trans_less_fun" Fun1.thy [less_fun_def] 
   11.24 -        "[|less (f1::'a::term =>'b::po) f2; less f2 f3 |] ==> less f1 f3"
   11.25 +        "[|(f1::'a::term =>'b::po) << f2; f2 << f3 |] ==> f1 << f3"
   11.26  (fn prems =>
   11.27          [
   11.28          (cut_facts_tac prems 1),
    12.1 --- a/src/HOLCF/Fun1.thy	Fri May 23 18:55:28 1997 +0200
    12.2 +++ b/src/HOLCF/Fun1.thy	Sun May 25 11:07:52 1997 +0200
    12.3 @@ -12,14 +12,11 @@
    12.4  
    12.5  Fun1 = Pcpo +
    12.6  
    12.7 -(* default class is still term *)
    12.8 +(* to make << defineable: *)
    12.9 +instance fun  :: (term,sq_ord)sq_ord
   12.10  
   12.11  defs
   12.12 -   (* definition of the ordering less_fun            *)
   12.13 -   (* in fun1.ML it is proved that less_fun is a po *)
   12.14 -   
   12.15 -  less_fun_def "less == (%f1 f2.!x. f1 x << f2 x)"  
   12.16 -
   12.17 +  less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)"  
   12.18  end
   12.19  
   12.20  
    13.1 --- a/src/HOLCF/Fun2.ML	Fri May 23 18:55:28 1997 +0200
    13.2 +++ b/src/HOLCF/Fun2.ML	Sun May 25 11:07:52 1997 +0200
    13.3 @@ -12,7 +12,7 @@
    13.4  qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x.f x << g x)"
    13.5   (fn prems => 
    13.6          [
    13.7 -	(fold_goals_tac [po_def,less_fun_def]),
    13.8 +	(fold_goals_tac [less_fun_def]),
    13.9  	(rtac refl 1)
   13.10          ]);
   13.11  
    14.1 --- a/src/HOLCF/Lift1.ML	Fri May 23 18:55:28 1997 +0200
    14.2 +++ b/src/HOLCF/Lift1.ML	Sun May 25 11:07:52 1997 +0200
    14.3 @@ -13,18 +13,18 @@
    14.4  (* less_lift is a partial order on type 'a -> 'b                            *)
    14.5  (* ------------------------------------------------------------------------ *)
    14.6  
    14.7 -goalw thy [less_lift_def] "less (x::'a lift) x";
    14.8 +goalw thy [less_lift_def] "(x::'a lift) << x";
    14.9  by (fast_tac HOL_cs 1);
   14.10  qed"refl_less_lift";
   14.11  
   14.12  val prems = goalw thy [less_lift_def] 
   14.13 -  "[|less (x1::'a lift) x2; less x2 x1|] ==> x1 = x2";
   14.14 +  "[|(x1::'a lift) << x2; x2 << x1|] ==> x1 = x2";
   14.15  by (cut_facts_tac prems 1);
   14.16  by (fast_tac HOL_cs 1);
   14.17  qed"antisym_less_lift";
   14.18  
   14.19  val prems = goalw Lift1.thy [less_lift_def] 
   14.20 -  "[|less (x1::'a lift) x2; less x2 x3|] ==> less x1 x3";
   14.21 +  "[|(x1::'a lift) << x2; x2 << x3|] ==> x1 << x3";
   14.22  by (cut_facts_tac prems 1);
   14.23  by (fast_tac HOL_cs 1);
   14.24  qed"trans_less_lift";
    15.1 --- a/src/HOLCF/Lift1.thy	Fri May 23 18:55:28 1997 +0200
    15.2 +++ b/src/HOLCF/Lift1.thy	Sun May 25 11:07:52 1997 +0200
    15.3 @@ -12,8 +12,9 @@
    15.4  
    15.5  datatype 'a lift = Undef | Def 'a
    15.6  
    15.7 +instance lift :: (term)sq_ord
    15.8  defs 
    15.9   
   15.10 - less_lift_def  "less x y == (x=y | x=Undef)"
   15.11 + less_lift_def  "x << y == (x=y | x=Undef)"
   15.12  
   15.13  end
    16.1 --- a/src/HOLCF/Lift2.ML	Fri May 23 18:55:28 1997 +0200
    16.2 +++ b/src/HOLCF/Lift2.ML	Sun May 25 11:07:52 1997 +0200
    16.3 @@ -12,7 +12,7 @@
    16.4  qed_goal "inst_lift_po" thy "(op <<)=(%x y.x=y|x=Undef)"
    16.5   (fn prems => 
    16.6          [
    16.7 -        (fold_goals_tac [po_def,less_lift_def]),
    16.8 +        (fold_goals_tac [less_lift_def]),
    16.9          (rtac refl 1)
   16.10          ]);
   16.11  
    17.1 --- a/src/HOLCF/Pcpo.ML	Fri May 23 18:55:28 1997 +0200
    17.2 +++ b/src/HOLCF/Pcpo.ML	Sun May 25 11:07:52 1997 +0200
    17.3 @@ -195,7 +195,7 @@
    17.4          (resolve_tac prems 1)
    17.5          ]);
    17.6  
    17.7 -qed_goal "not_less2not_eq" thy "~x<<y ==> ~x=y"
    17.8 +qed_goal "not_less2not_eq" thy "~(x::'a::po)<<y ==> ~x=y"
    17.9   (fn prems =>
   17.10          [
   17.11          (cut_facts_tac prems 1),
    18.1 --- a/src/HOLCF/Porder0.ML	Fri May 23 18:55:28 1997 +0200
    18.2 +++ b/src/HOLCF/Porder0.ML	Sun May 25 11:07:52 1997 +0200
    18.3 @@ -7,30 +7,12 @@
    18.4  
    18.5  open Porder0;
    18.6  
    18.7 -qed_goalw "refl_less" thy [ po_def ] "x << x"
    18.8 -(fn prems =>
    18.9 -        [
   18.10 -        (fast_tac (HOL_cs addSIs [ax_refl_less]) 1)
   18.11 -        ]);
   18.12 -
   18.13  AddIffs [refl_less];
   18.14  
   18.15 -qed_goalw "antisym_less" thy [ po_def ] "[| x << y; y << x |] ==> x = y"
   18.16 -(fn prems =>
   18.17 -        [
   18.18 -        (fast_tac (HOL_cs addSIs prems@[ax_antisym_less]) 1)
   18.19 -        ]);
   18.20 -
   18.21 -qed_goalw "trans_less" thy [ po_def ] "[| x << y; y << z |] ==> x << z"
   18.22 -(fn prems =>
   18.23 -        [
   18.24 -        (fast_tac (HOL_cs addIs prems@[ax_trans_less]) 1)
   18.25 -        ]);
   18.26 -
   18.27  (* ------------------------------------------------------------------------ *)
   18.28  (* minimal fixes least element                                              *)
   18.29  (* ------------------------------------------------------------------------ *)
   18.30 -bind_thm("minimal2UU",allI RS (prove_goal thy "!x.uu<<x==>uu=(@u.!y.u<<y)"
   18.31 +bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po.uu<<x==>uu=(@u.!y.u<<y)"
   18.32  (fn prems =>
   18.33          [
   18.34          (cut_facts_tac prems 1),
   18.35 @@ -45,7 +27,7 @@
   18.36  (* the reverse law of anti--symmetrie of <<                                 *)
   18.37  (* ------------------------------------------------------------------------ *)
   18.38  
   18.39 -qed_goal "antisym_less_inverse" thy "x=y ==> x << y & y << x"
   18.40 +qed_goal "antisym_less_inverse" thy "(x::'a::po)=y ==> x << y & y << x"
   18.41  (fn prems =>
   18.42          [
   18.43          (cut_facts_tac prems 1),
   18.44 @@ -56,7 +38,7 @@
   18.45  
   18.46  
   18.47  qed_goal "box_less" thy
   18.48 -"[| a << b; c << a; b << d|] ==> c << d"
   18.49 +"[| (a::'a::po) << b; c << a; b << d|] ==> c << d"
   18.50   (fn prems =>
   18.51          [
   18.52          (cut_facts_tac prems 1),
    19.1 --- a/src/HOLCF/Porder0.thy	Fri May 23 18:55:28 1997 +0200
    19.2 +++ b/src/HOLCF/Porder0.thy	Sun May 25 11:07:52 1997 +0200
    19.3 @@ -9,25 +9,22 @@
    19.4  
    19.5  Porder0 = Arith +
    19.6  
    19.7 -(* first the global constant for HOLCF type classes *)
    19.8 -consts
    19.9 -  less        :: "['a,'a] => bool"
   19.10 +	(* introduce a (syntactic) class for the constant << *)
   19.11 +axclass sq_ord<term
   19.12  
   19.13 -axclass po < term
   19.14 -        (* class axioms: *)
   19.15 -ax_refl_less       "less x x"        
   19.16 -ax_antisym_less    "[|less x y; less y x |] ==> x = y"    
   19.17 -ax_trans_less      "[|less x y; less y z |] ==> less x z"
   19.18 - 
   19.19 -	(* characteristic constant << on po *)
   19.20 +	(* characteristic constant << for po *)
   19.21  consts
   19.22 -  "<<"          :: "['a,'a::po] => bool"        (infixl 55)
   19.23 +  "<<"          :: "['a,'a::sq_ord] => bool"        (infixl 55)
   19.24  
   19.25  syntax (symbols)
   19.26 -  "op <<"       :: "['a,'a::po] => bool"        (infixl "\\<sqsubseteq>" 55)
   19.27 +  "op <<"       :: "['a,'a::sq_ord] => bool"        (infixl "\\<sqsubseteq>" 55)
   19.28  
   19.29 -defs
   19.30 -po_def             "(op <<) == less"
   19.31 +axclass po < sq_ord
   19.32 +        (* class axioms: *)
   19.33 +refl_less       "x << x"        
   19.34 +antisym_less    "[|x << y; y << x |] ==> x = y"    
   19.35 +trans_less      "[|x << y; y << z |] ==> x << z"
   19.36 + 
   19.37  end 
   19.38  
   19.39  
    20.1 --- a/src/HOLCF/Sprod1.ML	Fri May 23 18:55:28 1997 +0200
    20.2 +++ b/src/HOLCF/Sprod1.ML	Sun May 25 11:07:52 1997 +0200
    20.3 @@ -12,11 +12,11 @@
    20.4  (* less_sprod is a partial order on Sprod                                   *)
    20.5  (* ------------------------------------------------------------------------ *)
    20.6  
    20.7 -qed_goalw "refl_less_sprod" thy [less_sprod_def]"less (p::'a ** 'b) p"
    20.8 +qed_goalw "refl_less_sprod" thy [less_sprod_def]"(p::'a ** 'b) << p"
    20.9  (fn prems => [(fast_tac (HOL_cs addIs [refl_less]) 1)]);
   20.10  
   20.11  qed_goalw "antisym_less_sprod" thy [less_sprod_def]
   20.12 -        "[|less (p1::'a ** 'b) p2;less p2 p1|] ==> p1=p2"
   20.13 +        "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2"
   20.14  (fn prems =>
   20.15          [
   20.16          (cut_facts_tac prems 1),
   20.17 @@ -26,7 +26,7 @@
   20.18          ]);
   20.19  
   20.20  qed_goalw "trans_less_sprod" thy [less_sprod_def]
   20.21 -        "[|less (p1::'a**'b) p2;less p2 p3|] ==> less p1 p3"
   20.22 +        "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
   20.23  (fn prems =>
   20.24          [
   20.25          (cut_facts_tac prems 1),
    21.1 --- a/src/HOLCF/Sprod1.thy	Fri May 23 18:55:28 1997 +0200
    21.2 +++ b/src/HOLCF/Sprod1.thy	Sun May 25 11:07:52 1997 +0200
    21.3 @@ -8,7 +8,9 @@
    21.4  
    21.5  Sprod1 = Sprod0 +
    21.6  
    21.7 +instance "**"::(sq_ord,sq_ord)sq_ord 
    21.8 +
    21.9  defs
   21.10 -  less_sprod_def "less p1 p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
   21.11 +  less_sprod_def "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
   21.12  
   21.13  end
    22.1 --- a/src/HOLCF/Sprod2.ML	Fri May 23 18:55:28 1997 +0200
    22.2 +++ b/src/HOLCF/Sprod2.ML	Sun May 25 11:07:52 1997 +0200
    22.3 @@ -12,7 +12,7 @@
    22.4  qed_goal "inst_sprod_po" thy "(op <<)=(%x y.Isfst x<<Isfst y&Issnd x<<Issnd y)"
    22.5   (fn prems => 
    22.6          [
    22.7 -	(fold_goals_tac [po_def,less_sprod_def]),
    22.8 +	(fold_goals_tac [less_sprod_def]),
    22.9  	(rtac refl 1)
   22.10          ]);
   22.11  
    23.1 --- a/src/HOLCF/Ssum1.ML	Fri May 23 18:55:28 1997 +0200
    23.2 +++ b/src/HOLCF/Ssum1.ML	Sun May 25 11:07:52 1997 +0200
    23.3 @@ -41,7 +41,7 @@
    23.4  in
    23.5  
    23.6  val less_ssum1a = prove_goalw thy [less_ssum_def]
    23.7 -"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less s1 s2 = (x << y)"
    23.8 +"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"
    23.9   (fn prems =>
   23.10          [
   23.11          (cut_facts_tac prems 1),
   23.12 @@ -82,7 +82,7 @@
   23.13  
   23.14  
   23.15  val less_ssum1b = prove_goalw thy [less_ssum_def]
   23.16 -"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less s1 s2 = (x << y)"
   23.17 +"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"
   23.18   (fn prems =>
   23.19          [
   23.20          (cut_facts_tac prems 1),
   23.21 @@ -124,7 +124,7 @@
   23.22  
   23.23  
   23.24  val less_ssum1c = prove_goalw thy [less_ssum_def]
   23.25 -"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less s1 s2 = ((x::'a) = UU)"
   23.26 +"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"
   23.27   (fn prems =>
   23.28          [
   23.29          (cut_facts_tac prems 1),
   23.30 @@ -166,7 +166,7 @@
   23.31  
   23.32  
   23.33  val less_ssum1d = prove_goalw thy [less_ssum_def]
   23.34 -"[|s1=Isinr(x); s2=Isinl(y)|] ==> less s1 s2 = (x = UU)"
   23.35 +"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"
   23.36   (fn prems =>
   23.37          [
   23.38          (cut_facts_tac prems 1),
   23.39 @@ -213,7 +213,7 @@
   23.40  (* ------------------------------------------------------------------------ *)
   23.41  
   23.42  qed_goal "less_ssum2a" thy 
   23.43 -        "less (Isinl x) (Isinl y) = (x << y)"
   23.44 +        "(Isinl x) << (Isinl y) = (x << y)"
   23.45   (fn prems =>
   23.46          [
   23.47          (rtac less_ssum1a 1),
   23.48 @@ -222,7 +222,7 @@
   23.49          ]);
   23.50  
   23.51  qed_goal "less_ssum2b" thy 
   23.52 -        "less (Isinr x) (Isinr y) = (x << y)"
   23.53 +        "(Isinr x) << (Isinr y) = (x << y)"
   23.54   (fn prems =>
   23.55          [
   23.56          (rtac less_ssum1b 1),
   23.57 @@ -231,7 +231,7 @@
   23.58          ]);
   23.59  
   23.60  qed_goal "less_ssum2c" thy 
   23.61 -        "less (Isinl x) (Isinr y) = (x = UU)"
   23.62 +        "(Isinl x) << (Isinr y) = (x = UU)"
   23.63   (fn prems =>
   23.64          [
   23.65          (rtac less_ssum1c 1),
   23.66 @@ -240,7 +240,7 @@
   23.67          ]);
   23.68  
   23.69  qed_goal "less_ssum2d" thy 
   23.70 -        "less (Isinr x) (Isinl y) = (x = UU)"
   23.71 +        "(Isinr x) << (Isinl y) = (x = UU)"
   23.72   (fn prems =>
   23.73          [
   23.74          (rtac less_ssum1d 1),
   23.75 @@ -253,7 +253,7 @@
   23.76  (* less_ssum is a partial order on ++                                     *)
   23.77  (* ------------------------------------------------------------------------ *)
   23.78  
   23.79 -qed_goal "refl_less_ssum" thy "less (p::'a++'b) p"
   23.80 +qed_goal "refl_less_ssum" thy "(p::'a++'b) << p"
   23.81   (fn prems =>
   23.82          [
   23.83          (res_inst_tac [("p","p")] IssumE2 1),
   23.84 @@ -266,7 +266,7 @@
   23.85          ]);
   23.86  
   23.87  qed_goal "antisym_less_ssum" thy 
   23.88 - "[|less (p1::'a++'b) p2; less p2 p1|] ==> p1=p2"
   23.89 + "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2"
   23.90   (fn prems =>
   23.91          [
   23.92          (cut_facts_tac prems 1),
   23.93 @@ -296,7 +296,7 @@
   23.94          ]);
   23.95  
   23.96  qed_goal "trans_less_ssum" thy 
   23.97 - "[|less (p1::'a++'b) p2; less p2 p3|] ==> less p1 p3"
   23.98 + "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3"
   23.99   (fn prems =>
  23.100          [
  23.101          (cut_facts_tac prems 1),
    24.1 --- a/src/HOLCF/Ssum1.thy	Fri May 23 18:55:28 1997 +0200
    24.2 +++ b/src/HOLCF/Ssum1.thy	Sun May 25 11:07:52 1997 +0200
    24.3 @@ -8,8 +8,10 @@
    24.4  
    24.5  Ssum1 = Ssum0 +
    24.6  
    24.7 +instance "++"::(pcpo,pcpo)sq_ord
    24.8 +
    24.9  defs
   24.10 -  less_ssum_def "less == (%s1 s2.@z.
   24.11 +  less_ssum_def "(op <<) == (%s1 s2.@z.
   24.12           (! u x.s1=Isinl u & s2=Isinl x --> z = u << x)
   24.13          &(! v y.s1=Isinr v & s2=Isinr y --> z = v << y)
   24.14          &(! u y.s1=Isinl u & s2=Isinr y --> z = (u = UU))
    25.1 --- a/src/HOLCF/Ssum2.ML	Fri May 23 18:55:28 1997 +0200
    25.2 +++ b/src/HOLCF/Ssum2.ML	Sun May 25 11:07:52 1997 +0200
    25.3 @@ -16,7 +16,7 @@
    25.4  \        &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
    25.5   (fn prems => 
    25.6          [
    25.7 -        (fold_goals_tac [po_def,less_ssum_def]),
    25.8 +        (fold_goals_tac [less_ssum_def]),
    25.9          (rtac refl 1)
   25.10          ]);
   25.11  
   25.12 @@ -27,25 +27,25 @@
   25.13  qed_goal "less_ssum3a" thy "Isinl x << Isinl y = x << y"
   25.14   (fn prems =>
   25.15          [
   25.16 -        (simp_tac (!simpset addsimps [po_def,less_ssum2a]) 1)
   25.17 +        (simp_tac (!simpset addsimps [less_ssum2a]) 1)
   25.18          ]);
   25.19  
   25.20  qed_goal "less_ssum3b" thy "Isinr x << Isinr y = x << y"
   25.21   (fn prems =>
   25.22          [
   25.23 -        (simp_tac (!simpset addsimps [po_def,less_ssum2b]) 1)
   25.24 +        (simp_tac (!simpset addsimps [less_ssum2b]) 1)
   25.25          ]);
   25.26  
   25.27  qed_goal "less_ssum3c" thy "Isinl x << Isinr y = (x = UU)"
   25.28   (fn prems =>
   25.29          [
   25.30 -        (simp_tac (!simpset addsimps [po_def,less_ssum2c]) 1)
   25.31 +        (simp_tac (!simpset addsimps [less_ssum2c]) 1)
   25.32          ]);
   25.33  
   25.34  qed_goal "less_ssum3d" thy "Isinr x << Isinl y = (x = UU)"
   25.35   (fn prems =>
   25.36          [
   25.37 -        (simp_tac (!simpset addsimps [po_def,less_ssum2d]) 1)
   25.38 +        (simp_tac (!simpset addsimps [less_ssum2d]) 1)
   25.39          ]);
   25.40  
   25.41  (* ------------------------------------------------------------------------ *)
    26.1 --- a/src/HOLCF/Up1.ML	Fri May 23 18:55:28 1997 +0200
    26.2 +++ b/src/HOLCF/Up1.ML	Sun May 25 11:07:52 1997 +0200
    26.3 @@ -93,7 +93,7 @@
    26.4  val Up0_ss = (simpset_of "Cfun3") addsimps [Ifup1,Ifup2];
    26.5  
    26.6  qed_goalw "less_up1a"  thy [less_up_def]
    26.7 -        "less(Abs_Up(Inl ()))(z)"
    26.8 +        "Abs_Up(Inl ())<< z"
    26.9   (fn prems =>
   26.10          [
   26.11          (stac Abs_Up_inverse2 1),
   26.12 @@ -102,7 +102,7 @@
   26.13          ]);
   26.14  
   26.15  qed_goalw "less_up1b" thy [Iup_def,less_up_def]
   26.16 -        "~less (Iup x) (Abs_Up(Inl ()))"
   26.17 +        "~(Iup x) << (Abs_Up(Inl ()))"
   26.18   (fn prems =>
   26.19          [
   26.20          (rtac notI 1),
   26.21 @@ -116,7 +116,7 @@
   26.22          ]);
   26.23  
   26.24  qed_goalw "less_up1c"  thy [Iup_def,less_up_def]
   26.25 -        "less (Iup x) (Iup y)=(x<<y)"
   26.26 +        " (Iup x) << (Iup y)=(x<<y)"
   26.27   (fn prems =>
   26.28          [
   26.29          (stac Abs_Up_inverse2 1),
   26.30 @@ -127,7 +127,7 @@
   26.31          ]);
   26.32  
   26.33  
   26.34 -qed_goal "refl_less_up"  thy "less (p::'a u) p"
   26.35 +qed_goal "refl_less_up"  thy "(p::'a u) << p"
   26.36   (fn prems =>
   26.37          [
   26.38          (res_inst_tac [("p","p")] upE 1),
   26.39 @@ -139,7 +139,7 @@
   26.40          ]);
   26.41  
   26.42  qed_goal "antisym_less_up"  thy 
   26.43 -        "!!p1.[|less(p1::'a u) p2;less p2 p1|] ==> p1=p2"
   26.44 +        "!!p1.[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2"
   26.45   (fn _ =>
   26.46          [
   26.47          (res_inst_tac [("p","p1")] upE 1),
   26.48 @@ -147,13 +147,13 @@
   26.49          (res_inst_tac [("p","p2")] upE 1),
   26.50          (etac sym 1),
   26.51          (hyp_subst_tac 1),
   26.52 -        (res_inst_tac [("P","less (Iup x) (Abs_Up(Inl ()))")] notE 1),
   26.53 +        (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
   26.54          (rtac less_up1b 1),
   26.55          (atac 1),
   26.56          (hyp_subst_tac 1),
   26.57          (res_inst_tac [("p","p2")] upE 1),
   26.58          (hyp_subst_tac 1),
   26.59 -        (res_inst_tac [("P","less (Iup x) (Abs_Up(Inl ()))")] notE 1),
   26.60 +        (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
   26.61          (rtac less_up1b 1),
   26.62          (atac 1),
   26.63          (hyp_subst_tac 1),
   26.64 @@ -164,7 +164,7 @@
   26.65          ]);
   26.66  
   26.67  qed_goal "trans_less_up"  thy 
   26.68 -        "[|less (p1::'a u) p2;less p2 p3|] ==> less p1 p3"
   26.69 +        "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3"
   26.70   (fn prems =>
   26.71          [
   26.72          (cut_facts_tac prems 1),
    27.1 --- a/src/HOLCF/Up1.thy	Fri May 23 18:55:28 1997 +0200
    27.2 +++ b/src/HOLCF/Up1.thy	Sun May 25 11:07:52 1997 +0200
    27.3 @@ -14,6 +14,8 @@
    27.4  
    27.5  typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
    27.6  
    27.7 +instance u :: (sq_ord)sq_ord
    27.8 +
    27.9  consts
   27.10    Iup         :: "'a => ('a)u"
   27.11    Ifup        :: "('a->'b)=>('a)u => 'b"
   27.12 @@ -21,7 +23,7 @@
   27.13  defs
   27.14    Iup_def     "Iup x == Abs_Up(Inr(x))"
   27.15    Ifup_def    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z"
   27.16 -  less_up_def "less == (%x1 x2.case Rep_Up(x1) of                 
   27.17 +  less_up_def "(op <<) == (%x1 x2.case Rep_Up(x1) of                 
   27.18                 Inl(y1) => True          
   27.19               | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
   27.20                                              | Inr(z2) => y2<<z2))"
    28.1 --- a/src/HOLCF/Up2.ML	Fri May 23 18:55:28 1997 +0200
    28.2 +++ b/src/HOLCF/Up2.ML	Sun May 25 11:07:52 1997 +0200
    28.3 @@ -15,7 +15,7 @@
    28.4  \                                            | Inr(z2) => y2<<z2))"
    28.5   (fn prems => 
    28.6          [
    28.7 -        (fold_goals_tac [po_def,less_up_def]),
    28.8 +        (fold_goals_tac [less_up_def]),
    28.9          (rtac refl 1)
   28.10          ]);
   28.11  
   28.12 @@ -26,7 +26,7 @@
   28.13  qed_goal "minimal_up" thy "Abs_Up(Inl ()) << z"
   28.14   (fn prems =>
   28.15          [
   28.16 -        (simp_tac (!simpset addsimps [po_def,less_up1a]) 1)
   28.17 +        (simp_tac (!simpset addsimps [less_up1a]) 1)
   28.18          ]);
   28.19  
   28.20  bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
   28.21 @@ -45,13 +45,13 @@
   28.22  qed_goal "less_up2b" thy "~ Iup(x) << Abs_Up(Inl ())"
   28.23   (fn prems =>
   28.24          [
   28.25 -        (simp_tac (!simpset addsimps [po_def,less_up1b]) 1)
   28.26 +        (simp_tac (!simpset addsimps [less_up1b]) 1)
   28.27          ]);
   28.28  
   28.29  qed_goal "less_up2c" thy "(Iup(x)<<Iup(y)) = (x<<y)"
   28.30   (fn prems =>
   28.31          [
   28.32 -        (simp_tac (!simpset addsimps [po_def,less_up1c]) 1)
   28.33 +        (simp_tac (!simpset addsimps [less_up1c]) 1)
   28.34          ]);
   28.35  
   28.36  (* ------------------------------------------------------------------------ *)
    29.1 --- a/src/HOLCF/domain/theorems.ML	Fri May 23 18:55:28 1997 +0200
    29.2 +++ b/src/HOLCF/domain/theorems.ML	Sun May 25 11:07:52 1997 +0200
    29.3 @@ -51,7 +51,7 @@
    29.4                                  cut_facts_tac prems 1,
    29.5                                  fast_tac HOL_cs 1]);
    29.6  
    29.7 -val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [
    29.8 +val dist_eqI = prove_goal Porder.thy "~(x::'a::po) << y ==> x ~= y" (fn prems => [
    29.9                                  rtac rev_contrapos 1,
   29.10                                  etac (antisym_less_inverse RS conjunct1) 1,
   29.11                                  resolve_tac prems 1]);