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)
--- 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 *)
--- 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),
--- 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
--- 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 *)
--- 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)
--- 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),
--- 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"
--- 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 =>
[
--- 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;
--- 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),
--- 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]);
--- 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"