src/HOLCF/Up1.ML

--- a/src/HOLCF/Up1.ML	Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Up1.ML	Mon Feb 17 10:57:11 1997 +0100
@@ -6,15 +6,21 @@
 
 open Up1;
 
-qed_goalw "Exh_Up" Up1.thy [UU_up_def,Iup_def ]
-        "z = UU_up | (? x. z = Iup(x))"
+qed_goal "Abs_Up_inverse2" thy "Rep_Up (Abs_Up y) = y"
+ (fn prems =>
+        [
+	(simp_tac (!simpset addsimps [Up_def,Abs_Up_inverse]) 1)
+	]);
+
+qed_goalw "Exh_Up" thy [Iup_def ]
+        "z = Abs_Up(Inl ()) | (? x. z = Iup x)"
  (fn prems =>
         [
         (rtac (Rep_Up_inverse RS subst) 1),
-        (res_inst_tac [("s","Rep_Up(z)")] sumE 1),
+        (res_inst_tac [("s","Rep_Up z")] sumE 1),
         (rtac disjI1 1),
         (res_inst_tac [("f","Abs_Up")] arg_cong 1),
-        (rtac (unique_void2 RS subst) 1),
+        (rtac (unit_eq RS subst) 1),
         (atac 1),
         (rtac disjI2 1),
         (rtac exI 1),
@@ -22,21 +28,21 @@
         (atac 1)
         ]);
 
-qed_goal "inj_Abs_Up" Up1.thy "inj(Abs_Up)"
+qed_goal "inj_Abs_Up" thy "inj(Abs_Up)"
  (fn prems =>
         [
         (rtac inj_inverseI 1),
-        (rtac Abs_Up_inverse 1)
+        (rtac Abs_Up_inverse2 1)
         ]);
 
-qed_goal "inj_Rep_Up" Up1.thy "inj(Rep_Up)"
+qed_goal "inj_Rep_Up" thy "inj(Rep_Up)"
  (fn prems =>
         [
         (rtac inj_inverseI 1),
         (rtac Rep_Up_inverse 1)
         ]);
 
-qed_goalw "inject_Iup" Up1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y"
+qed_goalw "inject_Iup" thy [Iup_def] "Iup x=Iup y ==> x=y"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -45,7 +51,7 @@
         (atac 1)
         ]);
 
-qed_goalw "defined_Iup" Up1.thy [Iup_def,UU_up_def] "Iup(x)~=UU_up"
+qed_goalw "defined_Iup" thy [Iup_def] "Iup x~=Abs_Up(Inl ())"
  (fn prems =>
         [
         (rtac notI 1),
@@ -56,8 +62,8 @@
         ]);
 
 
-qed_goal "upE"  Up1.thy
-        "[| p=UU_up ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
+qed_goal "upE"  thy
+        "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
  (fn prems =>
         [
         (rtac (Exh_Up RS disjE) 1),
@@ -66,62 +72,62 @@
         (eresolve_tac prems 1)
         ]);
 
-qed_goalw "Ifup1"  Up1.thy [Ifup_def,UU_up_def]
-        "Ifup(f)(UU_up)=UU"
+qed_goalw "Ifup1"  thy [Ifup_def]
+        "Ifup(f)(Abs_Up(Inl ()))=UU"
  (fn prems =>
         [
-        (stac Abs_Up_inverse 1),
+        (stac Abs_Up_inverse2 1),
         (stac sum_case_Inl 1),
         (rtac refl 1)
         ]);
 
-qed_goalw "Ifup2"  Up1.thy [Ifup_def,Iup_def]
+qed_goalw "Ifup2"  thy [Ifup_def,Iup_def]
         "Ifup(f)(Iup(x))=f`x"
  (fn prems =>
         [
-        (stac Abs_Up_inverse 1),
+        (stac Abs_Up_inverse2 1),
         (stac sum_case_Inr 1),
         (rtac refl 1)
         ]);
 
 val Up0_ss = (simpset_of "Cfun3") addsimps [Ifup1,Ifup2];
 
-qed_goalw "less_up1a"  Up1.thy [less_up_def,UU_up_def]
-        "less_up(UU_up)(z)"
+qed_goalw "less_up1a"  thy [less_up_def]
+        "less(Abs_Up(Inl ()))(z)"
  (fn prems =>
         [
-        (stac Abs_Up_inverse 1),
+        (stac Abs_Up_inverse2 1),
         (stac sum_case_Inl 1),
         (rtac TrueI 1)
         ]);
 
-qed_goalw "less_up1b"  Up1.thy [Iup_def,less_up_def,UU_up_def]
-        "~less_up (Iup x) UU_up"
+qed_goalw "less_up1b" thy [Iup_def,less_up_def]
+        "~less (Iup x) (Abs_Up(Inl ()))"
  (fn prems =>
         [
         (rtac notI 1),
         (rtac iffD1 1),
         (atac 2),
-        (stac Abs_Up_inverse 1),
-        (stac Abs_Up_inverse 1),
+        (stac Abs_Up_inverse2 1),
+        (stac Abs_Up_inverse2 1),
         (stac sum_case_Inr 1),
         (stac sum_case_Inl 1),
         (rtac refl 1)
         ]);
 
-qed_goalw "less_up1c"  Up1.thy [Iup_def,less_up_def,UU_up_def]
-        "less_up (Iup x) (Iup y)=(x<<y)"
+qed_goalw "less_up1c"  thy [Iup_def,less_up_def]
+        "less (Iup x) (Iup y)=(x<<y)"
  (fn prems =>
         [
-        (stac Abs_Up_inverse 1),
-        (stac Abs_Up_inverse 1),
+        (stac Abs_Up_inverse2 1),
+        (stac Abs_Up_inverse2 1),
         (stac sum_case_Inr 1),
         (stac sum_case_Inr 1),
         (rtac refl 1)
         ]);
 
 
-qed_goal "refl_less_up"  Up1.thy "less_up p p"
+qed_goal "refl_less_up"  thy "less (p::'a u) p"
  (fn prems =>
         [
         (res_inst_tac [("p","p")] upE 1),
@@ -132,8 +138,8 @@
         (rtac refl_less 1)
         ]);
 
-qed_goal "antisym_less_up"  Up1.thy 
-        "!!p1. [|less_up p1 p2;less_up p2 p1|] ==> p1=p2"
+qed_goal "antisym_less_up"  thy 
+        "!!p1.[|less(p1::'a u) p2;less p2 p1|] ==> p1=p2"
  (fn _ =>
         [
         (res_inst_tac [("p","p1")] upE 1),
@@ -141,13 +147,13 @@
         (res_inst_tac [("p","p2")] upE 1),
         (etac sym 1),
         (hyp_subst_tac 1),
-        (res_inst_tac [("P","less_up (Iup x) UU_up")] notE 1),
+        (res_inst_tac [("P","less (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_up (Iup x) UU_up")] notE 1),
+        (res_inst_tac [("P","less (Iup x) (Abs_Up(Inl ()))")] notE 1),
         (rtac less_up1b 1),
         (atac 1),
         (hyp_subst_tac 1),
@@ -157,8 +163,8 @@
         (etac (less_up1c RS iffD1) 1)
         ]);
 
-qed_goal "trans_less_up"  Up1.thy 
-        "[|less_up p1 p2;less_up p2 p3|] ==> less_up p1 p3"
+qed_goal "trans_less_up"  thy 
+        "[|less (p1::'a u) p2;less p2 p3|] ==> less p1 p3"
  (fn prems =>
         [
         (cut_facts_tac prems 1),