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
--- a/src/HOLCF/Cfun1.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cfun1.ML Sun May 25 11:07:52 1997 +0200
@@ -35,14 +35,14 @@
(* less_cfun is a partial order on type 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "refl_less_cfun" thy [less_cfun_def] "less(f::'a->'b) f"
+qed_goalw "refl_less_cfun" thy [less_cfun_def] "(f::'a->'b) << f"
(fn prems =>
[
(rtac refl_less 1)
]);
qed_goalw "antisym_less_cfun" thy [less_cfun_def]
- "[|less (f1::'a->'b) f2; less f2 f1|] ==> f1 = f2"
+ "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -55,7 +55,7 @@
]);
qed_goalw "trans_less_cfun" thy [less_cfun_def]
- "[|less (f1::'a->'b) f2; less f2 f3|] ==> less f1 f3"
+ "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Cfun1.thy Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cfun1.thy Sun May 25 11:07:52 1997 +0200
@@ -13,6 +13,9 @@
typedef (CFun) ('a, 'b) "->" (infixr 0) = "{f. cont f}" (CfunI)
+(* to make << defineable *)
+instance "->" :: (cpo,cpo)sq_ord
+
consts
fapp :: "('a -> 'b)=>('a => 'b)" (* usually Rep_Cfun *)
(* application *)
@@ -33,6 +36,6 @@
fabs_def "fabs==Abs_CFun"
fapp_def "fapp==Rep_CFun"
- less_cfun_def "less == (% fo1 fo2. fapp fo1 << fapp fo2 )"
+ less_cfun_def "(op <<) == (% fo1 fo2. fapp fo1 << fapp fo2 )"
end
--- a/src/HOLCF/Cfun2.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cfun2.ML Sun May 25 11:07:52 1997 +0200
@@ -12,7 +12,7 @@
qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2.fapp f1 << fapp f2)"
(fn prems =>
[
- (fold_goals_tac [po_def,less_cfun_def]),
+ (fold_goals_tac [less_cfun_def]),
(rtac refl 1)
]);
--- a/src/HOLCF/Cont.thy Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cont.thy Sun May 25 11:07:52 1997 +0200
@@ -11,7 +11,7 @@
(*
Now we change the default class! Form now on all untyped typevariables are
- of default class pcpo
+ of default class po
*)
--- a/src/HOLCF/Cprod1.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cprod1.ML Sun May 25 11:07:52 1997 +0200
@@ -24,11 +24,11 @@
(Asm_simp_tac 1)
]);
-qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less (p::'a*'b) p"
+qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "(p::'a*'b) << p"
(fn prems => [Simp_tac 1]);
qed_goalw "antisym_less_cprod" thy [less_cprod_def]
- "[|less (p1::'a * 'b) p2;less p2 p1|] ==> p1=p2"
+ "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -38,7 +38,7 @@
]);
qed_goalw "trans_less_cprod" thy [less_cprod_def]
- "[|less (p1::'a*'b) p2;less p2 p3|] ==> less p1 p3"
+ "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Cprod1.thy Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cprod1.thy Sun May 25 11:07:52 1997 +0200
@@ -12,8 +12,10 @@
default cpo
+instance "*"::(sq_ord,sq_ord)sq_ord
+
defs
- less_cprod_def "less p1 p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
+ less_cprod_def "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
end
--- a/src/HOLCF/Cprod2.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cprod2.ML Sun May 25 11:07:52 1997 +0200
@@ -12,7 +12,7 @@
qed_goal "inst_cprod_po" thy "(op <<)=(%x y.fst x<<fst y & snd x<<snd y)"
(fn prems =>
[
- (fold_goals_tac [po_def,less_cprod_def]),
+ (fold_goals_tac [less_cprod_def]),
(rtac refl 1)
]);
@@ -71,7 +71,7 @@
(asm_simp_tac (!simpset addsimps [inst_cprod_po]) 1)
]);
-qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1,y1) << (x2,y2)"
+qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Discrete0.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Discrete0.ML Sun May 25 11:07:52 1997 +0200
@@ -6,17 +6,17 @@
Proves that 'a discr is a po
*)
-goalw thy [less_discr_def] "less (x::('a::term)discr) x";
+goalw thy [less_discr_def] "(x::('a::term)discr) << x";
by (rtac refl 1);
qed "less_discr_refl";
goalw thy [less_discr_def]
- "!!x. [| less (x::('a::term)discr) y; less y z |] ==> less x z";
+ "!!x. [| (x::('a::term)discr) << y; y << z |] ==> x << z";
by (etac trans 1);
by (assume_tac 1);
qed "less_discr_trans";
goalw thy [less_discr_def]
- "!!x. [| less (x::('a::term)discr) y; less y x |] ==> x=y";
+ "!!x. [| (x::('a::term)discr) << y; y << x |] ==> x=y";
by (assume_tac 1);
qed "less_discr_antisym";
--- a/src/HOLCF/Discrete0.thy Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Discrete0.thy Sun May 25 11:07:52 1997 +0200
@@ -10,7 +10,9 @@
datatype 'a discr = Discr 'a
+instance discr :: (term)sq_ord
+
defs
-less_discr_def "(less::('a::term)discr=>'a discr=>bool) == op ="
+less_discr_def "((op <<)::('a::term)discr=>'a discr=>bool) == op ="
end
--- a/src/HOLCF/Discrete1.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Discrete1.ML Sun May 25 11:07:52 1997 +0200
@@ -6,7 +6,7 @@
Proves that 'a discr is a cpo
*)
-goalw thy [po_def,less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
+goalw thy [less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
by (rtac refl 1);
qed "discr_less_eq";
AddIffs [discr_less_eq];
@@ -14,7 +14,7 @@
goalw thy [is_chain]
"!!S::nat=>('a::term)discr. is_chain S ==> S i = S 0";
by (nat_ind_tac "i" 1);
- by (rtac refl 1);
+by (rtac refl 1);
by (etac subst 1);
by (rtac sym 1);
by (Fast_tac 1);
--- a/src/HOLCF/Fun1.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Fun1.ML Sun May 25 11:07:52 1997 +0200
@@ -12,14 +12,14 @@
(* less_fun is a partial order on 'a => 'b *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "refl_less_fun" thy [less_fun_def] "less(f::'a::term =>'b::po) f"
+qed_goalw "refl_less_fun" thy [less_fun_def] "(f::'a::term =>'b::po) << f"
(fn prems =>
[
(fast_tac (HOL_cs addSIs [refl_less]) 1)
]);
qed_goalw "antisym_less_fun" Fun1.thy [less_fun_def]
- "[|less (f1::'a::term =>'b::po) f2; less f2 f1|] ==> f1 = f2"
+ "[|(f1::'a::term =>'b::po) << f2; f2 << f1|] ==> f1 = f2"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -28,7 +28,7 @@
]);
qed_goalw "trans_less_fun" Fun1.thy [less_fun_def]
- "[|less (f1::'a::term =>'b::po) f2; less f2 f3 |] ==> less f1 f3"
+ "[|(f1::'a::term =>'b::po) << f2; f2 << f3 |] ==> f1 << f3"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Fun1.thy Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Fun1.thy Sun May 25 11:07:52 1997 +0200
@@ -12,14 +12,11 @@
Fun1 = Pcpo +
-(* default class is still term *)
+(* to make << defineable: *)
+instance fun :: (term,sq_ord)sq_ord
defs
- (* definition of the ordering less_fun *)
- (* in fun1.ML it is proved that less_fun is a po *)
-
- less_fun_def "less == (%f1 f2.!x. f1 x << f2 x)"
-
+ less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)"
end
--- a/src/HOLCF/Fun2.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Fun2.ML Sun May 25 11:07:52 1997 +0200
@@ -12,7 +12,7 @@
qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x.f x << g x)"
(fn prems =>
[
- (fold_goals_tac [po_def,less_fun_def]),
+ (fold_goals_tac [less_fun_def]),
(rtac refl 1)
]);
--- a/src/HOLCF/Lift1.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Lift1.ML Sun May 25 11:07:52 1997 +0200
@@ -13,18 +13,18 @@
(* less_lift is a partial order on type 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-goalw thy [less_lift_def] "less (x::'a lift) x";
+goalw thy [less_lift_def] "(x::'a lift) << x";
by (fast_tac HOL_cs 1);
qed"refl_less_lift";
val prems = goalw thy [less_lift_def]
- "[|less (x1::'a lift) x2; less x2 x1|] ==> x1 = x2";
+ "[|(x1::'a lift) << x2; x2 << x1|] ==> x1 = x2";
by (cut_facts_tac prems 1);
by (fast_tac HOL_cs 1);
qed"antisym_less_lift";
val prems = goalw Lift1.thy [less_lift_def]
- "[|less (x1::'a lift) x2; less x2 x3|] ==> less x1 x3";
+ "[|(x1::'a lift) << x2; x2 << x3|] ==> x1 << x3";
by (cut_facts_tac prems 1);
by (fast_tac HOL_cs 1);
qed"trans_less_lift";
--- a/src/HOLCF/Lift1.thy Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Lift1.thy Sun May 25 11:07:52 1997 +0200
@@ -12,8 +12,9 @@
datatype 'a lift = Undef | Def 'a
+instance lift :: (term)sq_ord
defs
- less_lift_def "less x y == (x=y | x=Undef)"
+ less_lift_def "x << y == (x=y | x=Undef)"
end
--- a/src/HOLCF/Lift2.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Lift2.ML Sun May 25 11:07:52 1997 +0200
@@ -12,7 +12,7 @@
qed_goal "inst_lift_po" thy "(op <<)=(%x y.x=y|x=Undef)"
(fn prems =>
[
- (fold_goals_tac [po_def,less_lift_def]),
+ (fold_goals_tac [less_lift_def]),
(rtac refl 1)
]);
--- a/src/HOLCF/Pcpo.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Pcpo.ML Sun May 25 11:07:52 1997 +0200
@@ -195,7 +195,7 @@
(resolve_tac prems 1)
]);
-qed_goal "not_less2not_eq" thy "~x<<y ==> ~x=y"
+qed_goal "not_less2not_eq" thy "~(x::'a::po)<<y ==> ~x=y"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Porder0.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Porder0.ML Sun May 25 11:07:52 1997 +0200
@@ -7,30 +7,12 @@
open Porder0;
-qed_goalw "refl_less" thy [ po_def ] "x << x"
-(fn prems =>
- [
- (fast_tac (HOL_cs addSIs [ax_refl_less]) 1)
- ]);
-
AddIffs [refl_less];
-qed_goalw "antisym_less" thy [ po_def ] "[| x << y; y << x |] ==> x = y"
-(fn prems =>
- [
- (fast_tac (HOL_cs addSIs prems@[ax_antisym_less]) 1)
- ]);
-
-qed_goalw "trans_less" thy [ po_def ] "[| x << y; y << z |] ==> x << z"
-(fn prems =>
- [
- (fast_tac (HOL_cs addIs prems@[ax_trans_less]) 1)
- ]);
-
(* ------------------------------------------------------------------------ *)
(* minimal fixes least element *)
(* ------------------------------------------------------------------------ *)
-bind_thm("minimal2UU",allI RS (prove_goal thy "!x.uu<<x==>uu=(@u.!y.u<<y)"
+bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po.uu<<x==>uu=(@u.!y.u<<y)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -45,7 +27,7 @@
(* the reverse law of anti--symmetrie of << *)
(* ------------------------------------------------------------------------ *)
-qed_goal "antisym_less_inverse" thy "x=y ==> x << y & y << x"
+qed_goal "antisym_less_inverse" thy "(x::'a::po)=y ==> x << y & y << x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -56,7 +38,7 @@
qed_goal "box_less" thy
-"[| a << b; c << a; b << d|] ==> c << d"
+"[| (a::'a::po) << b; c << a; b << d|] ==> c << d"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Porder0.thy Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Porder0.thy Sun May 25 11:07:52 1997 +0200
@@ -9,25 +9,22 @@
Porder0 = Arith +
-(* first the global constant for HOLCF type classes *)
-consts
- less :: "['a,'a] => bool"
+ (* introduce a (syntactic) class for the constant << *)
+axclass sq_ord<term
-axclass po < term
- (* class axioms: *)
-ax_refl_less "less x x"
-ax_antisym_less "[|less x y; less y x |] ==> x = y"
-ax_trans_less "[|less x y; less y z |] ==> less x z"
-
- (* characteristic constant << on po *)
+ (* characteristic constant << for po *)
consts
- "<<" :: "['a,'a::po] => bool" (infixl 55)
+ "<<" :: "['a,'a::sq_ord] => bool" (infixl 55)
syntax (symbols)
- "op <<" :: "['a,'a::po] => bool" (infixl "\\<sqsubseteq>" 55)
+ "op <<" :: "['a,'a::sq_ord] => bool" (infixl "\\<sqsubseteq>" 55)
-defs
-po_def "(op <<) == less"
+axclass po < sq_ord
+ (* class axioms: *)
+refl_less "x << x"
+antisym_less "[|x << y; y << x |] ==> x = y"
+trans_less "[|x << y; y << z |] ==> x << z"
+
end
--- a/src/HOLCF/Sprod1.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Sprod1.ML Sun May 25 11:07:52 1997 +0200
@@ -12,11 +12,11 @@
(* less_sprod is a partial order on Sprod *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "refl_less_sprod" thy [less_sprod_def]"less (p::'a ** 'b) p"
+qed_goalw "refl_less_sprod" thy [less_sprod_def]"(p::'a ** 'b) << p"
(fn prems => [(fast_tac (HOL_cs addIs [refl_less]) 1)]);
qed_goalw "antisym_less_sprod" thy [less_sprod_def]
- "[|less (p1::'a ** 'b) p2;less p2 p1|] ==> p1=p2"
+ "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -26,7 +26,7 @@
]);
qed_goalw "trans_less_sprod" thy [less_sprod_def]
- "[|less (p1::'a**'b) p2;less p2 p3|] ==> less p1 p3"
+ "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Sprod1.thy Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Sprod1.thy Sun May 25 11:07:52 1997 +0200
@@ -8,7 +8,9 @@
Sprod1 = Sprod0 +
+instance "**"::(sq_ord,sq_ord)sq_ord
+
defs
- less_sprod_def "less p1 p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
+ less_sprod_def "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
end
--- a/src/HOLCF/Sprod2.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Sprod2.ML Sun May 25 11:07:52 1997 +0200
@@ -12,7 +12,7 @@
qed_goal "inst_sprod_po" thy "(op <<)=(%x y.Isfst x<<Isfst y&Issnd x<<Issnd y)"
(fn prems =>
[
- (fold_goals_tac [po_def,less_sprod_def]),
+ (fold_goals_tac [less_sprod_def]),
(rtac refl 1)
]);
--- a/src/HOLCF/Ssum1.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Ssum1.ML Sun May 25 11:07:52 1997 +0200
@@ -41,7 +41,7 @@
in
val less_ssum1a = prove_goalw thy [less_ssum_def]
-"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less s1 s2 = (x << y)"
+"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -82,7 +82,7 @@
val less_ssum1b = prove_goalw thy [less_ssum_def]
-"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less s1 s2 = (x << y)"
+"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -124,7 +124,7 @@
val less_ssum1c = prove_goalw thy [less_ssum_def]
-"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less s1 s2 = ((x::'a) = UU)"
+"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -166,7 +166,7 @@
val less_ssum1d = prove_goalw thy [less_ssum_def]
-"[|s1=Isinr(x); s2=Isinl(y)|] ==> less s1 s2 = (x = UU)"
+"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -213,7 +213,7 @@
(* ------------------------------------------------------------------------ *)
qed_goal "less_ssum2a" thy
- "less (Isinl x) (Isinl y) = (x << y)"
+ "(Isinl x) << (Isinl y) = (x << y)"
(fn prems =>
[
(rtac less_ssum1a 1),
@@ -222,7 +222,7 @@
]);
qed_goal "less_ssum2b" thy
- "less (Isinr x) (Isinr y) = (x << y)"
+ "(Isinr x) << (Isinr y) = (x << y)"
(fn prems =>
[
(rtac less_ssum1b 1),
@@ -231,7 +231,7 @@
]);
qed_goal "less_ssum2c" thy
- "less (Isinl x) (Isinr y) = (x = UU)"
+ "(Isinl x) << (Isinr y) = (x = UU)"
(fn prems =>
[
(rtac less_ssum1c 1),
@@ -240,7 +240,7 @@
]);
qed_goal "less_ssum2d" thy
- "less (Isinr x) (Isinl y) = (x = UU)"
+ "(Isinr x) << (Isinl y) = (x = UU)"
(fn prems =>
[
(rtac less_ssum1d 1),
@@ -253,7 +253,7 @@
(* less_ssum is a partial order on ++ *)
(* ------------------------------------------------------------------------ *)
-qed_goal "refl_less_ssum" thy "less (p::'a++'b) p"
+qed_goal "refl_less_ssum" thy "(p::'a++'b) << p"
(fn prems =>
[
(res_inst_tac [("p","p")] IssumE2 1),
@@ -266,7 +266,7 @@
]);
qed_goal "antisym_less_ssum" thy
- "[|less (p1::'a++'b) p2; less p2 p1|] ==> p1=p2"
+ "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -296,7 +296,7 @@
]);
qed_goal "trans_less_ssum" thy
- "[|less (p1::'a++'b) p2; less p2 p3|] ==> less p1 p3"
+ "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Ssum1.thy Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Ssum1.thy Sun May 25 11:07:52 1997 +0200
@@ -8,8 +8,10 @@
Ssum1 = Ssum0 +
+instance "++"::(pcpo,pcpo)sq_ord
+
defs
- less_ssum_def "less == (%s1 s2.@z.
+ less_ssum_def "(op <<) == (%s1 s2.@z.
(! u x.s1=Isinl u & s2=Isinl x --> z = u << x)
&(! v y.s1=Isinr v & s2=Isinr y --> z = v << y)
&(! u y.s1=Isinl u & s2=Isinr y --> z = (u = UU))
--- a/src/HOLCF/Ssum2.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Ssum2.ML Sun May 25 11:07:52 1997 +0200
@@ -16,7 +16,7 @@
\ &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
(fn prems =>
[
- (fold_goals_tac [po_def,less_ssum_def]),
+ (fold_goals_tac [less_ssum_def]),
(rtac refl 1)
]);
@@ -27,25 +27,25 @@
qed_goal "less_ssum3a" thy "Isinl x << Isinl y = x << y"
(fn prems =>
[
- (simp_tac (!simpset addsimps [po_def,less_ssum2a]) 1)
+ (simp_tac (!simpset addsimps [less_ssum2a]) 1)
]);
qed_goal "less_ssum3b" thy "Isinr x << Isinr y = x << y"
(fn prems =>
[
- (simp_tac (!simpset addsimps [po_def,less_ssum2b]) 1)
+ (simp_tac (!simpset addsimps [less_ssum2b]) 1)
]);
qed_goal "less_ssum3c" thy "Isinl x << Isinr y = (x = UU)"
(fn prems =>
[
- (simp_tac (!simpset addsimps [po_def,less_ssum2c]) 1)
+ (simp_tac (!simpset addsimps [less_ssum2c]) 1)
]);
qed_goal "less_ssum3d" thy "Isinr x << Isinl y = (x = UU)"
(fn prems =>
[
- (simp_tac (!simpset addsimps [po_def,less_ssum2d]) 1)
+ (simp_tac (!simpset addsimps [less_ssum2d]) 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Up1.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Up1.ML Sun May 25 11:07:52 1997 +0200
@@ -93,7 +93,7 @@
val Up0_ss = (simpset_of "Cfun3") addsimps [Ifup1,Ifup2];
qed_goalw "less_up1a" thy [less_up_def]
- "less(Abs_Up(Inl ()))(z)"
+ "Abs_Up(Inl ())<< z"
(fn prems =>
[
(stac Abs_Up_inverse2 1),
@@ -102,7 +102,7 @@
]);
qed_goalw "less_up1b" thy [Iup_def,less_up_def]
- "~less (Iup x) (Abs_Up(Inl ()))"
+ "~(Iup x) << (Abs_Up(Inl ()))"
(fn prems =>
[
(rtac notI 1),
@@ -116,7 +116,7 @@
]);
qed_goalw "less_up1c" thy [Iup_def,less_up_def]
- "less (Iup x) (Iup y)=(x<<y)"
+ " (Iup x) << (Iup y)=(x<<y)"
(fn prems =>
[
(stac Abs_Up_inverse2 1),
@@ -127,7 +127,7 @@
]);
-qed_goal "refl_less_up" thy "less (p::'a u) p"
+qed_goal "refl_less_up" thy "(p::'a u) << p"
(fn prems =>
[
(res_inst_tac [("p","p")] upE 1),
@@ -139,7 +139,7 @@
]);
qed_goal "antisym_less_up" thy
- "!!p1.[|less(p1::'a u) p2;less p2 p1|] ==> p1=p2"
+ "!!p1.[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2"
(fn _ =>
[
(res_inst_tac [("p","p1")] upE 1),
@@ -147,13 +147,13 @@
(res_inst_tac [("p","p2")] upE 1),
(etac sym 1),
(hyp_subst_tac 1),
- (res_inst_tac [("P","less (Iup x) (Abs_Up(Inl ()))")] notE 1),
+ (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
(rtac less_up1b 1),
(atac 1),
(hyp_subst_tac 1),
(res_inst_tac [("p","p2")] upE 1),
(hyp_subst_tac 1),
- (res_inst_tac [("P","less (Iup x) (Abs_Up(Inl ()))")] notE 1),
+ (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
(rtac less_up1b 1),
(atac 1),
(hyp_subst_tac 1),
@@ -164,7 +164,7 @@
]);
qed_goal "trans_less_up" thy
- "[|less (p1::'a u) p2;less p2 p3|] ==> less p1 p3"
+ "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Up1.thy Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Up1.thy Sun May 25 11:07:52 1997 +0200
@@ -14,6 +14,8 @@
typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
+instance u :: (sq_ord)sq_ord
+
consts
Iup :: "'a => ('a)u"
Ifup :: "('a->'b)=>('a)u => 'b"
@@ -21,7 +23,7 @@
defs
Iup_def "Iup x == Abs_Up(Inr(x))"
Ifup_def "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z"
- less_up_def "less == (%x1 x2.case Rep_Up(x1) of
+ less_up_def "(op <<) == (%x1 x2.case Rep_Up(x1) of
Inl(y1) => True
| Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False
| Inr(z2) => y2<<z2))"
--- a/src/HOLCF/Up2.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Up2.ML Sun May 25 11:07:52 1997 +0200
@@ -15,7 +15,7 @@
\ | Inr(z2) => y2<<z2))"
(fn prems =>
[
- (fold_goals_tac [po_def,less_up_def]),
+ (fold_goals_tac [less_up_def]),
(rtac refl 1)
]);
@@ -26,7 +26,7 @@
qed_goal "minimal_up" thy "Abs_Up(Inl ()) << z"
(fn prems =>
[
- (simp_tac (!simpset addsimps [po_def,less_up1a]) 1)
+ (simp_tac (!simpset addsimps [less_up1a]) 1)
]);
bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
@@ -45,13 +45,13 @@
qed_goal "less_up2b" thy "~ Iup(x) << Abs_Up(Inl ())"
(fn prems =>
[
- (simp_tac (!simpset addsimps [po_def,less_up1b]) 1)
+ (simp_tac (!simpset addsimps [less_up1b]) 1)
]);
qed_goal "less_up2c" thy "(Iup(x)<<Iup(y)) = (x<<y)"
(fn prems =>
[
- (simp_tac (!simpset addsimps [po_def,less_up1c]) 1)
+ (simp_tac (!simpset addsimps [less_up1c]) 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/domain/theorems.ML Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/domain/theorems.ML Sun May 25 11:07:52 1997 +0200
@@ -51,7 +51,7 @@
cut_facts_tac prems 1,
fast_tac HOL_cs 1]);
-val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [
+val dist_eqI = prove_goal Porder.thy "~(x::'a::po) << y ==> x ~= y" (fn prems => [
rtac rev_contrapos 1,
etac (antisym_less_inverse RS conjunct1) 1,
resolve_tac prems 1]);