# HG changeset patch
# User oheimb
# Date 849266133 -3600
# Node ID dbce3dce821a441480ebb4cc3a2140cf3faafde3
# Parent  1b1b46adc9b34a0808f058d2c92ecad9133d26a6
renamed is_flat to flat,
moved Lift*.* to Up*.*, renaming of all constans and theorems concerned,
                        (*lift* to *up*, except Ilift to Ifup, lift to fup)

diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/Cfun1.thy
--- a/src/HOLCF/Cfun1.thy	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/Cfun1.thy	Fri Nov 29 12:15:33 1996 +0100
@@ -48,6 +48,17 @@
   less_cfun_def         "less_cfun fo1 fo2 == ( fapp fo1 << fapp fo2 )"
 
 (* start 8bit 1 *)
+types
+
+('a, 'b) "è"          (infixr 5)
+
+syntax
+	Gfabs	:: "('a => 'b)=>('a -> 'b)"	(binder "¤" 10)
+
+translations
+
+(type)  "x è y"	== (type) "x -> y" 
+
 (* end 8bit 1 *)
 
 
diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/Fix.ML	Fri Nov 29 12:15:33 1996 +0100
@@ -549,8 +549,8 @@
 (* flat types are chain_finite                                              *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "flat_imp_chain_finite"  Fix.thy  [is_flat_def,chain_finite_def]
-        "is_flat(x::'a)==>chain_finite(x::'a)"
+qed_goalw "flat_imp_chain_finite"  Fix.thy  [flat_def,chain_finite_def]
+        "flat(x::'a)==>chain_finite(x::'a)"
  (fn prems =>
         [
         (rewtac max_in_chain_def),
@@ -587,9 +587,9 @@
 
 
 bind_thm ("adm_flat", flat_imp_chain_finite RS adm_chain_finite);
-(* is_flat(?x::?'a) ==> adm(?P::?'a => bool) *)
+(* flat(?x::?'a) ==> adm(?P::?'a => bool) *)
 
-qed_goalw "flat_void" Fix.thy [is_flat_def] "is_flat(UU::void)"
+qed_goalw "flat_void" Fix.thy [flat_def] "flat(UU::void)"
  (fn prems =>
         [
         (strip_tac 1),
@@ -597,8 +597,8 @@
         (rtac unique_void2 1)
         ]);
 
-qed_goalw "flat_eq" Fix.thy [is_flat_def] 
-        "[| is_flat (x::'a); (a::'a) ~= UU |] ==> a << b = (a = b)" (fn prems=>[
+qed_goalw "flat_eq" Fix.thy [flat_def] 
+        "[| flat (x::'a); (a::'a) ~= UU |] ==> a << b = (a = b)" (fn prems=>[
         (cut_facts_tac prems 1),
         (fast_tac (HOL_cs addIs [refl_less]) 1)]);
 
@@ -719,9 +719,9 @@
         (atac 1)
         ]);
 
-qed_goalw "flat2flat"  Fix.thy  [is_flat_def]
-"!!f g.[|is_flat(x::'a); !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
-\ ==> is_flat(y::'b)"
+qed_goalw "flat2flat"  Fix.thy  [flat_def]
+"!!f g.[|flat(x::'a); !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
+\ ==> flat(y::'b)"
  (fn prems =>
         [
         (strip_tac 1),
@@ -750,8 +750,8 @@
 (* a result about functions with flat codomain                               *)
 (* ------------------------------------------------------------------------- *)
 
-qed_goalw "flat_codom" Fix.thy [is_flat_def]
-"[|is_flat(y::'b);f`(x::'a)=(c::'b)|] ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
+qed_goalw "flat_codom" Fix.thy [flat_def]
+"[|flat(y::'b);f`(x::'a)=(c::'b)|] ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/Fix.thy	Fri Nov 29 12:15:33 1996 +0100
@@ -18,7 +18,7 @@
 adm		:: "('a=>bool)=>bool"
 admw		:: "('a=>bool)=>bool"
 chain_finite	:: "'a=>bool"
-is_flat		:: "'a=>bool" (* should be called flat, for consistency *)
+flat		:: "'a=>bool" (* should be called flat, for consistency *)
 
 defs
 
@@ -35,8 +35,7 @@
 chain_finite_def  "chain_finite (x::'a)==
                         !Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)"
 
-is_flat_def          "is_flat (x::'a) ==
-                        ! x y. (x::'a) << y --> (x = UU) | (x=y)"
+flat_def	  "flat (x::'a) == ! x y. (x::'a) << y --> (x = UU) | (x=y)"
 
 end
 
diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/Holcfb.ML
--- a/src/HOLCF/Holcfb.ML	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/Holcfb.ML	Fri Nov 29 12:15:33 1996 +0100
@@ -13,32 +13,5 @@
 (* ------------------------------------------------------------------------ *)
 
 
-(* val de_morgan1 = de_Morgan_disj RS sym;   "(~a & ~b)=(~(a | b))" *)
-
-(* val de_morgan2 = de_Morgan_conj RS sym;   "(~a | ~b)=(~(a & b))" *)
-
-
-(* val notall2ex = not_all                   "(~ (!x.P(x))) = (? x.~P(x))" *)
-
-(* val notex2all = not_ex                    "(~ (? x.P(x))) = (!x.~P(x))" *)
-
-
-(* val selectI3 =  select_eq_Ex RS iffD2   "(? x. P(x)) ==> P(@ x.P(x))" *)
-
-(* val selectE =   select_eq_Ex RS iffD1   "P(@ x.P(x)) ==> (? x. P(x))" *)
-
-
-(*
-qed_goal "notnotI" HOL.thy "P ==> ~~P"
-(fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (fast_tac HOL_cs 1)
-        ]);
-*)
-
-(* val classical2 = case_split_thm;        "[|Q ==> R; ~Q ==> R|]==>R" *)
-
-(* fun case_tac s = res_inst_tac [("Q",s)] classical2; *)
 
 val classical3 = (notE RS notI); (* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *)
diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/Makefile	Fri Nov 29 12:15:33 1996 +0100
@@ -27,7 +27,7 @@
        Cprod1.thy Cprod2.thy Cprod3.thy \
        Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
        Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
-       Lift1.thy Lift2.thy Lift3.thy Fix.thy ccc1.thy One.thy \
+       Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy One.thy \
        Tr1.thy Tr2.thy HOLCF.thy 
 
 FILES = ROOT.ML Porder0.thy  $(THYS) $(THYS:.thy=.ML)
diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/One.ML
--- a/src/HOLCF/One.ML	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/One.ML	Fri Nov 29 12:15:33 1996 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/one.thy
+(*  Title:      HOLCF/One.ML
     ID:         $Id$
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
@@ -15,7 +15,7 @@
 qed_goalw "Exh_one" One.thy [one_def] "z=UU | z = one"
  (fn prems =>
         [
-        (res_inst_tac [("p","rep_one`z")] liftE1 1),
+        (res_inst_tac [("p","rep_one`z")] upE1 1),
         (rtac disjI1 1),
         (rtac ((abs_one_iso RS allI) RS ((rep_one_iso RS allI) RS iso_strict )
                 RS conjunct2 RS subst) 1),
@@ -46,7 +46,7 @@
  (fn prems =>
         [
         (rtac classical3 1),
-        (rtac less_lift4b 1),
+        (rtac less_up4b 1),
         (rtac (rep_one_iso RS subst) 1),
         (rtac (rep_one_iso RS subst) 1),
         (rtac monofun_cfun_arg 1),
@@ -68,7 +68,7 @@
 (* one is flat                                                              *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "flat_one" One.thy [is_flat_def] "is_flat(one)"
+qed_goalw "flat_one" One.thy [flat_def] "flat one"
  (fn prems =>
         [
         (rtac allI 1),
diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/One.thy	Fri Nov 29 12:15:33 1996 +0100
@@ -34,7 +34,7 @@
 
 defs
   one_def       "one == abs_one`(up`UU)"
-  one_when_def "one_when == (LAM c u.lift`(LAM x.c)`(rep_one`u))"
+  one_when_def "one_when == (LAM c u.fup`(LAM x.c)`(rep_one`u))"
 
 translations
   "case l of one => t1" == "one_when`t1`l"
diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/Pcpo.ML	Fri Nov 29 12:15:33 1996 +0100
@@ -148,6 +148,9 @@
 (* usefull lemmas about UU                                                  *)
 (* ------------------------------------------------------------------------ *)
 
+val eq_UU_sym = prove_goal Pcpo.thy "(UU = x) = (x = UU)" (fn _ => [
+	fast_tac HOL_cs 1]);
+
 qed_goal "eq_UU_iff" Pcpo.thy "(x=UU)=(x<<UU)"
  (fn prems =>
         [
diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/ROOT.ML	Fri Nov 29 12:15:33 1996 +0100
@@ -11,8 +11,6 @@
 init_thy_reader();
 
 (* start 8bit 1 *)
-val banner = 
-        "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
 (* end 8bit 1 *)
 
 writeln banner;
diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/Tr1.ML
--- a/src/HOLCF/Tr1.ML	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/Tr1.ML	Fri Nov 29 12:15:33 1996 +0100
@@ -123,7 +123,7 @@
 (* type tr is flat                                                          *) 
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "flat_tr" Tr1.thy [is_flat_def] "is_flat(TT)"
+qed_goalw "flat_tr" Tr1.thy [flat_def] "flat TT"
  (fn prems =>
         [
         (rtac allI 1),
diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/ccc1.ML
--- a/src/HOLCF/ccc1.ML	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/ccc1.ML	Fri Nov 29 12:15:33 1996 +0100
@@ -87,7 +87,7 @@
 (* Merge the different rewrite rules for the simplifier                     *)
 (* ------------------------------------------------------------------------ *)
 
-Addsimps (lift_rews @ [ID1,ID2,ID3,cfcomp2]);
+Addsimps (up_rews @ [ID1,ID2,ID3,cfcomp2]);
 
 
 
diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/ccc1.thy
--- a/src/HOLCF/ccc1.thy	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/ccc1.thy	Fri Nov 29 12:15:33 1996 +0100
@@ -3,11 +3,11 @@
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Merge Theories Cprof, Sprod, Ssum, Lift, Fix and
+Merge Theories Cprof, Sprod, Ssum, Up, Fix and
 define constants for categorical reasoning
 *)
 
-ccc1 = Cprod3 + Sprod3 + Ssum3 + Lift3 + Fix +
+ccc1 = Cprod3 + Sprod3 + Ssum3 + Up3 + Fix +
 
 consts
         ID      :: "'a -> 'a"