Changes of HOLCF from Oscar Slotosch:
1. axclass instead of class
* less instead of
less_fun,
less_cfun,
less_sprod,
less_cprod,
less_ssum,
less_up,
less_lift
* @x.!y.x<<y instead of UUU instead of
UU_fun, UU_cfun, ...
* no witness type void needed (eliminated Void.thy.Void.ML)
* inst_<typ>_<class> derived as theorems
2. improved some proves on less_sprod and less_cprod
* eliminated the following theorems
Sprod1.ML: less_sprod1a
Sprod1.ML: less_sprod1b
Sprod1.ML: less_sprod2a
Sprod1.ML: less_sprod2b
Sprod1.ML: less_sprod2c
Sprod2.ML: less_sprod3a
Sprod2.ML: less_sprod3b
Sprod2.ML: less_sprod4b
Sprod2.ML: less_sprod4c
Sprod3.ML: less_sprod5b
Sprod3.ML: less_sprod5c
Cprod1.ML: less_cprod1b
Cprod1.ML: less_cprod2a
Cprod1.ML: less_cprod2b
Cprod1.ML: less_cprod2c
Cprod2.ML: less_cprod3a
Cprod2.ML: less_cprod3b
3. new classes:
* cpo<po,
* chfin<pcpo,
* flat<pcpo,
* derived: flat<chfin
to do: show instances for lift
4. Data Type One
* Used lift for the definition: one = unit lift
* Changed the constant one into ONE
5. Data Type Tr
* Used lift for the definition: tr = bool lift
* adopted definitions of if,andalso,orelse,neg
* only one theory Tr.thy,Tr.ML instead of
Tr1.thy,Tr1.ML, Tr2.thy,Tr2.ML
* reintroduced ceils for =TT,=FF
6. typedef
* Using typedef instead of faking type definitions
to do: change fapp, fabs from Cfun1 to Rep_Cfun, Abs_Cfun
7. adopted examples and domain construct to theses changes
These changes eliminated all rules and arities from HOLCF
--- a/src/HOLCF/Cfun1.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cfun1.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,37 +1,48 @@
-(* Title: HOLCF/cfun1.ML
+(* Title: HOLCF/Cfun1.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for cfun1.thy
+Lemmas for Cfun1.thy
*)
open Cfun1;
(* ------------------------------------------------------------------------ *)
-(* A non-emptyness result for Cfun *)
+(* derive old type definition rules for fabs & fapp *)
+(* fapp and fabs should be replaced by Rep_Cfun anf Abs_Cfun in future *)
(* ------------------------------------------------------------------------ *)
-
-qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun"
- (fn prems =>
+qed_goalw "Rep_Cfun" thy [fapp_def] "fapp fo : CFun"
+(fn prems =>
[
- (stac mem_Collect_eq 1),
- (rtac cont_id 1)
+ (rtac Rep_CFun 1)
]);
+qed_goalw "Rep_Cfun_inverse" thy [fapp_def,fabs_def] "fabs (fapp fo) = fo"
+(fn prems =>
+ [
+ (rtac Rep_CFun_inverse 1)
+ ]);
+
+qed_goalw "Abs_Cfun_inverse" thy [fapp_def,fabs_def] "f:CFun==>fapp(fabs f)=f"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac Abs_CFun_inverse 1)
+ ]);
(* ------------------------------------------------------------------------ *)
(* less_cfun is a partial order on type 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "refl_less_cfun" Cfun1.thy [less_cfun_def] "less_cfun f f"
+qed_goalw "refl_less_cfun" thy [less_cfun_def] "less(f::'a::pcpo->'b::pcpo) f"
(fn prems =>
[
(rtac refl_less 1)
]);
-qed_goalw "antisym_less_cfun" Cfun1.thy [less_cfun_def]
- "[|less_cfun f1 f2; less_cfun f2 f1|] ==> f1 = f2"
+qed_goalw "antisym_less_cfun" thy [less_cfun_def]
+ "[|less (f1::'a::pcpo->'b::pcpo) f2; less f2 f1|] ==> f1 = f2"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -43,8 +54,8 @@
(rtac Rep_Cfun_inverse 1)
]);
-qed_goalw "trans_less_cfun" Cfun1.thy [less_cfun_def]
- "[|less_cfun f1 f2; less_cfun f2 f3|] ==> less_cfun f1 f3"
+qed_goalw "trans_less_cfun" thy [less_cfun_def]
+ "[|less (f1::'a::pcpo->'b::pcpo) f2; less f2 f3|] ==> less f1 f3"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -56,7 +67,7 @@
(* lemmas about application of continuous functions *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cfun_cong" Cfun1.thy
+qed_goal "cfun_cong" thy
"[| f=g; x=y |] ==> f`x = g`y"
(fn prems =>
[
@@ -64,7 +75,7 @@
(fast_tac HOL_cs 1)
]);
-qed_goal "cfun_fun_cong" Cfun1.thy "f=g ==> f`x = g`x"
+qed_goal "cfun_fun_cong" thy "f=g ==> f`x = g`x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -72,7 +83,7 @@
(rtac refl 1)
]);
-qed_goal "cfun_arg_cong" Cfun1.thy "x=y ==> f`x = f`y"
+qed_goal "cfun_arg_cong" thy "x=y ==> f`x = f`y"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -86,12 +97,12 @@
(* additional lemma about the isomorphism between -> and Cfun *)
(* ------------------------------------------------------------------------ *)
-qed_goal "Abs_Cfun_inverse2" Cfun1.thy "cont(f) ==> fapp(fabs(f)) = f"
+qed_goal "Abs_Cfun_inverse2" thy "cont f ==> fapp (fabs f) = f"
(fn prems =>
[
(cut_facts_tac prems 1),
(rtac Abs_Cfun_inverse 1),
- (rewtac Cfun_def),
+ (rewtac CFun_def),
(etac (mem_Collect_eq RS ssubst) 1)
]);
@@ -99,8 +110,7 @@
(* simplification of application *)
(* ------------------------------------------------------------------------ *)
-qed_goal "Cfunapp2" Cfun1.thy
- "cont(f) ==> (fabs f)`x = f x"
+qed_goal "Cfunapp2" thy "cont f ==> (fabs f)`x = f x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -111,7 +121,7 @@
(* beta - equality for continuous functions *)
(* ------------------------------------------------------------------------ *)
-qed_goal "beta_cfun" Cfun1.thy
+qed_goal "beta_cfun" thy
"cont(c1) ==> (LAM x .c1 x)`u = c1 u"
(fn prems =>
[
--- a/src/HOLCF/Cfun1.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cfun1.thy Mon Feb 17 10:57:11 1997 +0100
@@ -9,49 +9,28 @@
Cfun1 = Cont +
-
-(* new type of continuous functions *)
-
-types "->" 2 (infixr 5)
-
-arities "->" :: (pcpo,pcpo)term (* No properties for ->'s range *)
+typedef (CFun) ('a, 'b) "->" (infixr 0) = "{f. cont f}" (CfunI)
consts
- Cfun :: "('a => 'b)set"
- fapp :: "('a -> 'b)=>('a => 'b)" (* usually Rep_Cfun *)
+ fapp :: "('a -> 'b)=>('a => 'b)" (* usually Rep_Cfun *)
(* application *)
-
- fabs :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10)
+ fabs :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10)
(* usually Abs_Cfun *)
(* abstraction *)
-
less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
-syntax "@fapp" :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
+syntax "@fapp" :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
translations "f`x" == "fapp f x"
syntax (symbols)
-
- "->" :: [type, type] => type ("(_ \\<rightarrow>/ _)" [6,5]5)
+ "->" :: [type, type] => type ("(_ \\<rightarrow>/ _)" [6,5]5)
"LAM " :: "[idts, 'a => 'b] => ('a -> 'b)"
("(3\\<Lambda>_./ _)" [0, 10] 10)
-
defs
-
- Cfun_def "Cfun == {f. cont(f)}"
-
-rules
+ fabs_def "fabs==Abs_CFun"
+ fapp_def "fapp==Rep_CFun"
- (*faking a type definition... *)
- (* -> is isomorphic to Cfun *)
-
- Rep_Cfun "fapp fo : Cfun"
- Rep_Cfun_inverse "fabs (fapp fo) = fo"
- Abs_Cfun_inverse "f:Cfun ==> fapp(fabs f) = f"
-
-defs
- (*defining the abstract constants*)
- less_cfun_def "less_cfun fo1 fo2 == ( fapp fo1 << fapp fo2 )"
+ less_cfun_def "less == (% fo1 fo2. fapp fo1 << fapp fo2 )"
end
--- a/src/HOLCF/Cfun2.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cfun2.ML Mon Feb 17 10:57:11 1997 +0100
@@ -8,43 +8,57 @@
open Cfun2;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2.fapp f1 << fapp f2)"
+ (fn prems =>
+ [
+ (fold_goals_tac [po_def,less_cfun_def]),
+ (rtac refl 1)
+ ]);
+
(* ------------------------------------------------------------------------ *)
(* access to less_cfun in class po *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
+qed_goal "less_cfun" thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
(fn prems =>
[
- (stac inst_cfun_po 1),
- (fold_goals_tac [less_cfun_def]),
- (rtac refl 1)
+ (simp_tac (!simpset addsimps [inst_cfun_po]) 1)
]);
(* ------------------------------------------------------------------------ *)
(* Type 'a ->'b is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
+qed_goal "minimal_cfun" thy "fabs(% x.UU) << f"
(fn prems =>
[
(stac less_cfun 1),
(stac Abs_Cfun_inverse2 1),
(rtac cont_const 1),
- (fold_goals_tac [UU_fun_def]),
(rtac minimal_fun 1)
]);
+bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
+
+qed_goal "least_cfun" thy "? x::'a->'b.!y.x<<y"
+(fn prems =>
+ [
+ (res_inst_tac [("x","fabs(% x.UU)")] exI 1),
+ (rtac (minimal_cfun RS allI) 1)
+ ]);
+
(* ------------------------------------------------------------------------ *)
(* fapp yields continuous functions in 'a => 'b *)
(* this is continuity of fapp in its 'second' argument *)
(* cont_fapp2 ==> monofun_fapp2 & contlub_fapp2 *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cont_fapp2" Cfun2.thy "cont(fapp(fo))"
+qed_goal "cont_fapp2" thy "cont(fapp(fo))"
(fn prems =>
[
(res_inst_tac [("P","cont")] CollectD 1),
- (fold_goals_tac [Cfun_def]),
+ (fold_goals_tac [CFun_def]),
(rtac Rep_Cfun 1)
]);
@@ -71,7 +85,7 @@
(* fapp is monotone in its 'first' argument *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_fapp1" Cfun2.thy [monofun] "monofun(fapp)"
+qed_goalw "monofun_fapp1" thy [monofun] "monofun(fapp)"
(fn prems =>
[
(strip_tac 1),
@@ -83,7 +97,7 @@
(* monotonicity of application fapp in mixfix syntax [_]_ *)
(* ------------------------------------------------------------------------ *)
-qed_goal "monofun_cfun_fun" Cfun2.thy "f1 << f2 ==> f1`x << f2`x"
+qed_goal "monofun_cfun_fun" thy "f1 << f2 ==> f1`x << f2`x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -100,7 +114,7 @@
(* monotonicity of fapp in both arguments in mixfix syntax [_]_ *)
(* ------------------------------------------------------------------------ *)
-qed_goal "monofun_cfun" Cfun2.thy
+qed_goal "monofun_cfun" thy
"[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2"
(fn prems =>
[
@@ -111,7 +125,7 @@
]);
-qed_goal "strictI" Cfun2.thy "f`x = UU ==> f`UU = UU" (fn prems => [
+qed_goal "strictI" thy "f`x = UU ==> f`UU = UU" (fn prems => [
cut_facts_tac prems 1,
rtac (eq_UU_iff RS iffD2) 1,
etac subst 1,
@@ -123,7 +137,7 @@
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ch2ch_fappR" Cfun2.thy
+qed_goal "ch2ch_fappR" thy
"is_chain(Y) ==> is_chain(%i. f`(Y i))"
(fn prems =>
[
@@ -141,7 +155,7 @@
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_cfun_mono" Cfun2.thy
+qed_goal "lub_cfun_mono" thy
"is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))"
(fn prems =>
[
@@ -157,7 +171,7 @@
(* use MF2 lemmas from Cont.ML *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ex_lubcfun" Cfun2.thy
+qed_goal "ex_lubcfun" thy
"[| is_chain(F); is_chain(Y) |] ==>\
\ lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\
\ lub(range(%i. lub(range(%j. F(j)`(Y i)))))"
@@ -175,7 +189,7 @@
(* the lub of a chain of cont. functions is continuous *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cont_lubcfun" Cfun2.thy
+qed_goal "cont_lubcfun" thy
"is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))"
(fn prems =>
[
@@ -194,7 +208,7 @@
(* type 'a -> 'b is chain complete *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_cfun" Cfun2.thy
+qed_goal "lub_cfun" thy
"is_chain(CCF) ==> range(CCF) <<| (LAM x.lub(range(% i.CCF(i)`x)))"
(fn prems =>
[
@@ -222,7 +236,7 @@
is_chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
*)
-qed_goal "cpo_cfun" Cfun2.thy
+qed_goal "cpo_cfun" thy
"is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
(fn prems =>
[
@@ -250,7 +264,7 @@
(* Monotonicity of fabs *)
(* ------------------------------------------------------------------------ *)
-qed_goal "semi_monofun_fabs" Cfun2.thy
+qed_goal "semi_monofun_fabs" thy
"[|cont(f);cont(g);f<<g|]==>fabs(f)<<fabs(g)"
(fn prems =>
[
@@ -266,7 +280,7 @@
(* Extenionality wrt. << in 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_cfun2" Cfun2.thy "(!!x. f`x << g`x) ==> f << g"
+qed_goal "less_cfun2" thy "(!!x. f`x << g`x) ==> f << g"
(fn prems =>
[
(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
--- a/src/HOLCF/Cfun2.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cfun2.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/cfun2.thy
+(* Title: HOLCF/Cfun2.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -9,22 +9,6 @@
Cfun2 = Cfun1 +
-(* Witness for the above arity axiom is cfun1.ML *)
-arities "->" :: (pcpo,pcpo)po
-
-consts
- UU_cfun :: "'a->'b"
-
-rules
-
-(* instance of << for type ['a -> 'b] *)
-
-inst_cfun_po "((op <<)::['a->'b,'a->'b]=>bool) = less_cfun"
-
-defs
-(* The least element in type 'a->'b *)
-
-UU_cfun_def "UU_cfun == fabs(% x.UU)"
+instance "->"::(pcpo,pcpo)po (refl_less_cfun,antisym_less_cfun,trans_less_cfun)
end
-
--- a/src/HOLCF/Cfun3.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cfun3.ML Mon Feb 17 10:57:11 1997 +0100
@@ -6,11 +6,18 @@
open Cfun3;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_cfun_pcpo" thy "UU = fabs(%x.UU)"
+ (fn prems =>
+ [
+ (simp_tac (HOL_ss addsimps [UU_def,UU_cfun_def]) 1)
+ ]);
+
(* ------------------------------------------------------------------------ *)
(* the contlub property for fapp its 'first' argument *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_fapp1" Cfun3.thy "contlub(fapp)"
+qed_goal "contlub_fapp1" thy "contlub(fapp)"
(fn prems =>
[
(rtac contlubI 1),
@@ -31,7 +38,7 @@
(* the cont property for fapp in its first argument *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cont_fapp1" Cfun3.thy "cont(fapp)"
+qed_goal "cont_fapp1" thy "cont(fapp)"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -44,7 +51,7 @@
(* contlub, cont properties of fapp in its first argument in mixfix _[_] *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_cfun_fun" Cfun3.thy
+qed_goal "contlub_cfun_fun" thy
"is_chain(FY) ==>\
\ lub(range FY)`x = lub(range (%i.FY(i)`x))"
(fn prems =>
@@ -58,7 +65,7 @@
]);
-qed_goal "cont_cfun_fun" Cfun3.thy
+qed_goal "cont_cfun_fun" thy
"is_chain(FY) ==>\
\ range(%i.FY(i)`x) <<| lub(range FY)`x"
(fn prems =>
@@ -74,7 +81,7 @@
(* contlub, cont properties of fapp in both argument in mixfix _[_] *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_cfun" Cfun3.thy
+qed_goal "contlub_cfun" thy
"[|is_chain(FY);is_chain(TY)|] ==>\
\ (lub(range FY))`(lub(range TY)) = lub(range(%i.FY(i)`(TY i)))"
(fn prems =>
@@ -88,7 +95,7 @@
(atac 1)
]);
-qed_goal "cont_cfun" Cfun3.thy
+qed_goal "cont_cfun" thy
"[|is_chain(FY);is_chain(TY)|] ==>\
\ range(%i.(FY i)`(TY i)) <<| (lub (range FY))`(lub(range TY))"
(fn prems =>
@@ -109,7 +116,7 @@
(* cont2cont lemma for fapp *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cont2cont_fapp" Cfun3.thy
+qed_goal "cont2cont_fapp" thy
"[|cont(%x.ft x);cont(%x.tt x)|] ==> cont(%x. (ft x)`(tt x))"
(fn prems =>
[
@@ -129,7 +136,7 @@
(* cont2mono Lemma for %x. LAM y. c1(x)(y) *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cont2mono_LAM" Cfun3.thy
+qed_goal "cont2mono_LAM" thy
"[|!x.cont(c1 x); !y.monofun(%x.c1 x y)|] ==>\
\ monofun(%x. LAM y. c1 x y)"
(fn prems =>
@@ -151,7 +158,7 @@
(* cont2cont Lemma for %x. LAM y. c1 x y) *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cont2cont_LAM" Cfun3.thy
+qed_goal "cont2cont_LAM" thy
"[| !x.cont(c1 x); !y.cont(%x.c1 x y) |] ==> cont(%x. LAM y. c1 x y)"
(fn prems =>
[
@@ -207,11 +214,10 @@
(* function application _[_] is strict in its first arguments *)
(* ------------------------------------------------------------------------ *)
-qed_goal "strict_fapp1" Cfun3.thy "(UU::'a->'b)`x = (UU::'b)"
+qed_goal "strict_fapp1" thy "(UU::'a->'b)`x = (UU::'b)"
(fn prems =>
[
(stac inst_cfun_pcpo 1),
- (rewtac UU_cfun_def),
(stac beta_cfun 1),
(Simp_tac 1),
(rtac refl 1)
@@ -222,14 +228,14 @@
(* results about strictify *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "Istrictify1" Cfun3.thy [Istrictify_def]
+qed_goalw "Istrictify1" thy [Istrictify_def]
"Istrictify(f)(UU)= (UU)"
(fn prems =>
[
(Simp_tac 1)
]);
-qed_goalw "Istrictify2" Cfun3.thy [Istrictify_def]
+qed_goalw "Istrictify2" thy [Istrictify_def]
"~x=UU ==> Istrictify(f)(x)=f`x"
(fn prems =>
[
@@ -237,7 +243,7 @@
(Asm_simp_tac 1)
]);
-qed_goal "monofun_Istrictify1" Cfun3.thy "monofun(Istrictify)"
+qed_goal "monofun_Istrictify1" thy "monofun(Istrictify)"
(fn prems =>
[
(rtac monofunI 1),
@@ -257,7 +263,7 @@
(rtac refl_less 1)
]);
-qed_goal "monofun_Istrictify2" Cfun3.thy "monofun(Istrictify(f))"
+qed_goal "monofun_Istrictify2" thy "monofun(Istrictify(f))"
(fn prems =>
[
(rtac monofunI 1),
@@ -276,7 +282,7 @@
]);
-qed_goal "contlub_Istrictify1" Cfun3.thy "contlub(Istrictify)"
+qed_goal "contlub_Istrictify1" thy "contlub(Istrictify)"
(fn prems =>
[
(rtac contlubI 1),
@@ -303,7 +309,7 @@
(rtac (refl RS allI) 1)
]);
-qed_goal "contlub_Istrictify2" Cfun3.thy "contlub(Istrictify(f::'a -> 'b))"
+qed_goal "contlub_Istrictify2" thy "contlub(Istrictify(f::'a -> 'b))"
(fn prems =>
[
(rtac contlubI 1),
@@ -352,7 +358,7 @@
(monofun_Istrictify2 RS monocontlub2cont));
-qed_goalw "strictify1" Cfun3.thy [strictify_def] "strictify`f`UU=UU" (fn _ => [
+qed_goalw "strictify1" thy [strictify_def] "strictify`f`UU=UU" (fn _ => [
(stac beta_cfun 1),
(simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1,
cont2cont_CF1L]) 1),
@@ -361,7 +367,7 @@
(rtac Istrictify1 1)
]);
-qed_goalw "strictify2" Cfun3.thy [strictify_def]
+qed_goalw "strictify2" thy [strictify_def]
"~x=UU ==> strictify`f`x=f`x" (fn prems => [
(stac beta_cfun 1),
(simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1,
--- a/src/HOLCF/Cfun3.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cfun3.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/cfun3.thy
+(* Title: HOLCF/Cfun3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -9,21 +9,14 @@
Cfun3 = Cfun2 +
-arities "->" :: (pcpo,pcpo)pcpo (* Witness cfun2.ML *)
+instance "->" :: (pcpo,pcpo)pcpo (least_cfun,cpo_cfun)
consts
Istrictify :: "('a->'b)=>'a=>'b"
strictify :: "('a->'b)->'a->'b"
-
-rules
-
-inst_cfun_pcpo "(UU::'a->'b) = UU_cfun"
-
defs
Istrictify_def "Istrictify f x == if x=UU then UU else f`x"
-
strictify_def "strictify == (LAM f x.Istrictify f x)"
end
-
--- a/src/HOLCF/Cont.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cont.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,9 +1,9 @@
-(* Title: HOLCF/cont.ML
+(* Title: HOLCF/Cont.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for cont.thy
+Lemmas for Cont.thy
*)
open Cont;
@@ -12,7 +12,7 @@
(* access to definition *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "contlubI" Cont.thy [contlub]
+qed_goalw "contlubI" thy [contlub]
"! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==>\
\ contlub(f)"
(fn prems =>
@@ -21,7 +21,7 @@
(atac 1)
]);
-qed_goalw "contlubE" Cont.thy [contlub]
+qed_goalw "contlubE" thy [contlub]
" contlub(f)==>\
\ ! Y. is_chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))"
(fn prems =>
@@ -31,7 +31,7 @@
]);
-qed_goalw "contI" Cont.thy [cont]
+qed_goalw "contI" thy [cont]
"! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
(fn prems =>
[
@@ -39,7 +39,7 @@
(atac 1)
]);
-qed_goalw "contE" Cont.thy [cont]
+qed_goalw "contE" thy [cont]
"cont(f) ==> ! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y)))"
(fn prems =>
[
@@ -48,7 +48,7 @@
]);
-qed_goalw "monofunI" Cont.thy [monofun]
+qed_goalw "monofunI" thy [monofun]
"! x y. x << y --> f(x) << f(y) ==> monofun(f)"
(fn prems =>
[
@@ -56,7 +56,7 @@
(atac 1)
]);
-qed_goalw "monofunE" Cont.thy [monofun]
+qed_goalw "monofunE" thy [monofun]
"monofun(f) ==> ! x y. x << y --> f(x) << f(y)"
(fn prems =>
[
@@ -73,7 +73,7 @@
(* monotone functions map chains to chains *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ch2ch_monofun" Cont.thy
+qed_goal "ch2ch_monofun" thy
"[| monofun(f); is_chain(Y) |] ==> is_chain(%i. f(Y(i)))"
(fn prems =>
[
@@ -88,7 +88,7 @@
(* monotone functions map upper bound to upper bounds *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ub2ub_monofun" Cont.thy
+qed_goal "ub2ub_monofun" thy
"[| monofun(f); range(Y) <| u|] ==> range(%i.f(Y(i))) <| f(u)"
(fn prems =>
[
@@ -103,7 +103,7 @@
(* left to right: monofun(f) & contlub(f) ==> cont(f) *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monocontlub2cont" Cont.thy [cont]
+qed_goalw "monocontlub2cont" thy [cont]
"[|monofun(f);contlub(f)|] ==> cont(f)"
(fn prems =>
[
@@ -120,7 +120,7 @@
(* first a lemma about binary chains *)
(* ------------------------------------------------------------------------ *)
-qed_goal "binchain_cont" Cont.thy
+qed_goal "binchain_cont" thy
"[| cont(f); x << y |] ==> range(%i. f(if i = 0 then x else y)) <<| f(y)"
(fn prems =>
[
@@ -137,7 +137,7 @@
(* part1: cont(f) ==> monofun(f *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "cont2mono" Cont.thy [monofun]
+qed_goalw "cont2mono" thy [monofun]
"cont(f) ==> monofun(f)"
(fn prems =>
[
@@ -155,7 +155,7 @@
(* part2: cont(f) ==> contlub(f) *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "cont2contlub" Cont.thy [contlub]
+qed_goalw "cont2contlub" thy [contlub]
"cont(f) ==> contlub(f)"
(fn prems =>
[
@@ -170,7 +170,7 @@
(* monotone functions map finite chains to finite chains *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_finch2finch" Cont.thy [finite_chain_def]
+qed_goalw "monofun_finch2finch" thy [finite_chain_def]
"[| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))"
(fn prems =>
[
@@ -193,7 +193,7 @@
(* in both arguments *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ch2ch_MF2L" Cont.thy
+qed_goal "ch2ch_MF2L" thy
"[|monofun(MF2); is_chain(F)|] ==> is_chain(%i. MF2 (F i) x)"
(fn prems =>
[
@@ -203,7 +203,7 @@
]);
-qed_goal "ch2ch_MF2R" Cont.thy
+qed_goal "ch2ch_MF2R" thy
"[|monofun(MF2(f)); is_chain(Y)|] ==> is_chain(%i. MF2 f (Y i))"
(fn prems =>
[
@@ -212,7 +212,7 @@
(atac 1)
]);
-qed_goal "ch2ch_MF2LR" Cont.thy
+qed_goal "ch2ch_MF2LR" thy
"[|monofun(MF2); !f.monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
\ is_chain(%i. MF2(F(i))(Y(i)))"
(fn prems =>
@@ -228,7 +228,7 @@
]);
-qed_goal "ch2ch_lubMF2R" Cont.thy
+qed_goal "ch2ch_lubMF2R" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F);is_chain(Y)|] ==> \
@@ -248,7 +248,7 @@
]);
-qed_goal "ch2ch_lubMF2L" Cont.thy
+qed_goal "ch2ch_lubMF2L" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F);is_chain(Y)|] ==> \
@@ -268,7 +268,7 @@
]);
-qed_goal "lub_MF2_mono" Cont.thy
+qed_goal "lub_MF2_mono" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F)|] ==> \
@@ -288,7 +288,7 @@
(atac 1)
]);
-qed_goal "ex_lubMF2" Cont.thy
+qed_goal "ex_lubMF2" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(F); is_chain(Y)|] ==> \
@@ -327,7 +327,7 @@
]);
-qed_goal "diag_lubMF2_1" Cont.thy
+qed_goal "diag_lubMF2_1" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(FY);is_chain(TY)|] ==>\
@@ -371,7 +371,7 @@
(atac 1)
]);
-qed_goal "diag_lubMF2_2" Cont.thy
+qed_goal "diag_lubMF2_2" thy
"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
\ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
\ is_chain(FY);is_chain(TY)|] ==>\
@@ -395,7 +395,7 @@
(* in both arguments *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_CF2" Cont.thy
+qed_goal "contlub_CF2" thy
"[|cont(CF2);!f.cont(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
\ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))"
(fn prems =>
@@ -421,7 +421,7 @@
(* The following results are about application for functions in 'a=>'b *)
(* ------------------------------------------------------------------------ *)
-qed_goal "monofun_fun_fun" Cont.thy
+qed_goal "monofun_fun_fun" thy
"f1 << f2 ==> f1(x) << f2(x)"
(fn prems =>
[
@@ -429,7 +429,7 @@
(etac (less_fun RS iffD1 RS spec) 1)
]);
-qed_goal "monofun_fun_arg" Cont.thy
+qed_goal "monofun_fun_arg" thy
"[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)"
(fn prems =>
[
@@ -438,7 +438,7 @@
(atac 1)
]);
-qed_goal "monofun_fun" Cont.thy
+qed_goal "monofun_fun" thy
"[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)"
(fn prems =>
[
@@ -455,7 +455,7 @@
(* continuity *)
(* ------------------------------------------------------------------------ *)
-qed_goal "mono2mono_MF1L" Cont.thy
+qed_goal "mono2mono_MF1L" thy
"[|monofun(c1)|] ==> monofun(%x. c1 x y)"
(fn prems =>
[
@@ -466,7 +466,7 @@
(atac 1)
]);
-qed_goal "cont2cont_CF1L" Cont.thy
+qed_goal "cont2cont_CF1L" thy
"[|cont(c1)|] ==> cont(%x. c1 x y)"
(fn prems =>
[
@@ -487,7 +487,7 @@
(********* Note "(%x.%y.c1 x y) = c1" ***********)
-qed_goal "mono2mono_MF1L_rev" Cont.thy
+qed_goal "mono2mono_MF1L_rev" thy
"!y.monofun(%x.c1 x y) ==> monofun(c1)"
(fn prems =>
[
@@ -500,7 +500,7 @@
(atac 1)
]);
-qed_goal "cont2cont_CF1L_rev" Cont.thy
+qed_goal "cont2cont_CF1L_rev" thy
"!y.cont(%x.c1 x y) ==> cont(c1)"
(fn prems =>
[
@@ -526,7 +526,7 @@
(* never used here *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_abstraction" Cont.thy
+qed_goal "contlub_abstraction" thy
"[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a=>'b=>'c) x y)|] ==>\
\ (%y.lub(range(%i.c (Y i) y))) = (lub(range(%i.%y.c (Y i) y)))"
(fn prems =>
@@ -543,7 +543,7 @@
]);
-qed_goal "mono2mono_app" Cont.thy
+qed_goal "mono2mono_app" thy
"[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\
\ monofun(%x.(ft(x))(tt(x)))"
(fn prems =>
@@ -561,7 +561,7 @@
]);
-qed_goal "cont2contlub_app" Cont.thy
+qed_goal "cont2contlub_app" thy
"[|cont(ft);!x.cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
(fn prems =>
[
@@ -578,7 +578,7 @@
]);
-qed_goal "cont2cont_app" Cont.thy
+qed_goal "cont2cont_app" thy
"[|cont(ft);!x.cont(ft(x));cont(tt)|] ==>\
\ cont(%x.(ft(x))(tt(x)))"
(fn prems =>
@@ -609,7 +609,7 @@
(* The identity function is continuous *)
(* ------------------------------------------------------------------------ *)
-qed_goal "cont_id" Cont.thy "cont(% x.x)"
+qed_goal "cont_id" thy "cont(% x.x)"
(fn prems =>
[
(rtac contI 1),
@@ -618,13 +618,11 @@
(rtac refl 1)
]);
-
-
(* ------------------------------------------------------------------------ *)
(* constant functions are continuous *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "cont_const" Cont.thy [cont] "cont(%x.c)"
+qed_goalw "cont_const" thy [cont] "cont(%x.c)"
(fn prems =>
[
(strip_tac 1),
@@ -639,7 +637,7 @@
]);
-qed_goal "cont2cont_app3" Cont.thy
+qed_goal "cont2cont_app3" thy
"[|cont(f);cont(t) |] ==> cont(%x. f(t(x)))"
(fn prems =>
[
@@ -650,3 +648,13 @@
(atac 1)
]);
+(* ------------------------------------------------------------------------ *)
+(* A non-emptyness result for Cfun *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "CfunI" thy "?x:Collect cont"
+ (fn prems =>
+ [
+ (rtac CollectI 1),
+ (rtac cont_const 1)
+ ]);
--- a/src/HOLCF/Cprod1.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cprod1.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,113 +1,48 @@
-(* Title: HOLCF/cprod1.ML
+(* Title: HOLCF/Cprod1.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for theory cprod1.thy
+Lemmas for theory Cprod1.thy
*)
open Cprod1;
-qed_goalw "less_cprod1b" Cprod1.thy [less_cprod_def]
- "less_cprod p1 p2 = ( fst(p1) << fst(p2) & snd(p1) << snd(p2))"
- (fn prems =>
- [
- (rtac refl 1)
- ]);
-
-qed_goalw "less_cprod2a" Cprod1.thy [less_cprod_def]
- "less_cprod (x,y) (UU,UU) ==> x = UU & y = UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac conjE 1),
- (dtac (fst_conv RS subst) 1),
- (dtac (fst_conv RS subst) 1),
- (dtac (fst_conv RS subst) 1),
- (dtac (snd_conv RS subst) 1),
- (dtac (snd_conv RS subst) 1),
- (dtac (snd_conv RS subst) 1),
- (rtac conjI 1),
- (etac UU_I 1),
- (etac UU_I 1)
- ]);
-
-qed_goal "less_cprod2b" Cprod1.thy
- "less_cprod p (UU,UU) ==> p = (UU,UU)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("p","p")] PairE 1),
- (hyp_subst_tac 1),
- (dtac less_cprod2a 1),
- (Asm_simp_tac 1)
- ]);
-
-qed_goalw "less_cprod2c" Cprod1.thy [less_cprod_def]
- "less_cprod (x1,y1) (x2,y2) ==> x1 << x2 & y1 << y2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac conjE 1),
- (dtac (fst_conv RS subst) 1),
- (dtac (fst_conv RS subst) 1),
- (dtac (fst_conv RS subst) 1),
- (dtac (snd_conv RS subst) 1),
- (dtac (snd_conv RS subst) 1),
- (dtac (snd_conv RS subst) 1),
- (rtac conjI 1),
- (atac 1),
- (atac 1)
- ]);
(* ------------------------------------------------------------------------ *)
(* less_cprod is a partial order on 'a * 'b *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less_cprod p p"
- (fn prems => [Simp_tac 1]);
-
-qed_goal "antisym_less_cprod" Cprod1.thy
- "[|less_cprod p1 p2;less_cprod p2 p1|] ==> p1=p2"
- (fn prems =>
+qed_goal "Sel_injective_cprod" Prod.thy
+ "[|fst x = fst y; snd x = snd y|] ==> x = y"
+(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("p","p1")] PairE 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p2")] PairE 1),
- (hyp_subst_tac 1),
- (dtac less_cprod2c 1),
- (dtac less_cprod2c 1),
- (etac conjE 1),
- (etac conjE 1),
- (stac Pair_eq 1),
- (fast_tac (HOL_cs addSIs [antisym_less]) 1)
+ (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1),
+ (rotate_tac ~1 1),
+ (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1),
+ (Asm_simp_tac 1)
]);
+qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less (p::'a*'b) p"
+ (fn prems => [Simp_tac 1]);
-qed_goal "trans_less_cprod" Cprod1.thy
- "[|less_cprod p1 p2;less_cprod p2 p3|] ==> less_cprod p1 p3"
- (fn prems =>
+qed_goalw "antisym_less_cprod" thy [less_cprod_def]
+ "[|less (p1::'a * 'b) p2;less p2 p1|] ==> p1=p2"
+(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("p","p1")] PairE 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p3")] PairE 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p2")] PairE 1),
- (hyp_subst_tac 1),
- (dtac less_cprod2c 1),
- (dtac less_cprod2c 1),
- (stac less_cprod1b 1),
- (Simp_tac 1),
- (etac conjE 1),
- (etac conjE 1),
- (rtac conjI 1),
- (etac trans_less 1),
- (atac 1),
- (etac trans_less 1),
- (atac 1)
+ (rtac Sel_injective_cprod 1),
+ (fast_tac (HOL_cs addIs [antisym_less]) 1),
+ (fast_tac (HOL_cs addIs [antisym_less]) 1)
]);
-
-
+qed_goalw "trans_less_cprod" thy [less_cprod_def]
+ "[|less (p1::'a*'b) p2;less p2 p3|] ==> less p1 p3"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac conjI 1),
+ (fast_tac (HOL_cs addIs [trans_less]) 1),
+ (fast_tac (HOL_cs addIs [trans_less]) 1)
+ ]);
--- a/src/HOLCF/Cprod1.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cprod1.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/cprod1.thy
+(* Title: HOLCF/Cprod1.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -10,14 +10,8 @@
Cprod1 = Cfun3 +
-
-consts
- less_cprod :: "[('a::pcpo * 'b::pcpo),('a * 'b)] => bool"
-
defs
- less_cprod_def "less_cprod p1 p2 == ( fst(p1) << fst(p2) &
- snd(p1) << snd(p2))"
+ less_cprod_def "less p1 p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
end
-
--- a/src/HOLCF/Cprod2.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cprod2.ML Mon Feb 17 10:57:11 1997 +0100
@@ -8,88 +8,70 @@
open Cprod2;
-qed_goal "less_cprod3a" Cprod2.thy
- "p1=(UU,UU) ==> p1 << p2"
+(* for compatibility with old HOLCF-Version *)
+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]),
+ (rtac refl 1)
+ ]);
+
+qed_goalw "less_cprod4c" thy [inst_cprod_po RS eq_reflection]
+ "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2"
(fn prems =>
[
(cut_facts_tac prems 1),
- (stac inst_cprod_po 1),
- (stac less_cprod1b 1),
- (hyp_subst_tac 1),
- (Asm_simp_tac 1)
- ]);
-
-qed_goal "less_cprod3b" Cprod2.thy
- "(p1 << p2) = (fst(p1)<<fst(p2) & snd(p1)<<snd(p2))"
- (fn prems =>
- [
- (stac inst_cprod_po 1),
- (rtac less_cprod1b 1)
- ]);
-
-qed_goal "less_cprod4a" Cprod2.thy
- "(x1,x2) << (UU,UU) ==> x1=UU & x2=UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac less_cprod2a 1),
- (etac (inst_cprod_po RS subst) 1)
- ]);
-
-qed_goal "less_cprod4b" Cprod2.thy
- "p << (UU,UU) ==> p = (UU,UU)"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac less_cprod2b 1),
- (etac (inst_cprod_po RS subst) 1)
- ]);
-
-qed_goal "less_cprod4c" Cprod2.thy
- " (xa,ya) << (x,y) ==> xa<<x & ya << y"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac less_cprod2c 1),
- (etac (inst_cprod_po RS subst) 1),
- (REPEAT (atac 1))
+ (etac conjE 1),
+ (dtac (fst_conv RS subst) 1),
+ (dtac (fst_conv RS subst) 1),
+ (dtac (fst_conv RS subst) 1),
+ (dtac (snd_conv RS subst) 1),
+ (dtac (snd_conv RS subst) 1),
+ (dtac (snd_conv RS subst) 1),
+ (rtac conjI 1),
+ (atac 1),
+ (atac 1)
]);
(* ------------------------------------------------------------------------ *)
(* type cprod is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goal "minimal_cprod" Cprod2.thy "(UU,UU)<<p"
+qed_goal "minimal_cprod" thy "(UU,UU)<<p"
(fn prems =>
[
- (rtac less_cprod3a 1),
- (rtac refl 1)
+ (simp_tac(!simpset addsimps[inst_cprod_po])1)
+ ]);
+
+bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym);
+
+qed_goal "least_cprod" thy "? x::'a*'b.!y.x<<y"
+(fn prems =>
+ [
+ (res_inst_tac [("x","(UU,UU)")] exI 1),
+ (rtac (minimal_cprod RS allI) 1)
]);
(* ------------------------------------------------------------------------ *)
(* Pair <_,_> is monotone in both arguments *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_pair1" Cprod2.thy [monofun] "monofun(Pair)"
+qed_goalw "monofun_pair1" thy [monofun] "monofun Pair"
(fn prems =>
[
(strip_tac 1),
(rtac (less_fun RS iffD2) 1),
(strip_tac 1),
- (rtac (less_cprod3b RS iffD2) 1),
- (Simp_tac 1)
+ (asm_simp_tac (!simpset addsimps [inst_cprod_po]) 1)
]);
-qed_goalw "monofun_pair2" Cprod2.thy [monofun] "monofun(Pair(x))"
+qed_goalw "monofun_pair2" thy [monofun] "monofun(Pair x)"
(fn prems =>
[
- (strip_tac 1),
- (rtac (less_cprod3b RS iffD2) 1),
- (Simp_tac 1)
+ (asm_simp_tac (!simpset addsimps [inst_cprod_po]) 1)
]);
-qed_goal "monofun_pair" Cprod2.thy
- "[|x1<<x2; y1<<y2|] ==> (x1,y1) << (x2,y2)"
+qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1,y1) << (x2,y2)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -105,7 +87,7 @@
(* fst and snd are monotone *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_fst" Cprod2.thy [monofun] "monofun(fst)"
+qed_goalw "monofun_fst" thy [monofun] "monofun fst"
(fn prems =>
[
(strip_tac 1),
@@ -117,7 +99,7 @@
(etac (less_cprod4c RS conjunct1) 1)
]);
-qed_goalw "monofun_snd" Cprod2.thy [monofun] "monofun(snd)"
+qed_goalw "monofun_snd" thy [monofun] "monofun snd"
(fn prems =>
[
(strip_tac 1),
@@ -133,17 +115,14 @@
(* the type 'a * 'b is a cpo *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_cprod" Cprod2.thy
-" is_chain(S) ==> range(S) <<| \
-\ (lub(range(%i.fst(S i))),lub(range(%i.snd(S i)))) "
+qed_goal "lub_cprod" thy
+"is_chain S ==> range S<<|(lub(range(%i.fst(S i))),lub(range(%i.snd(S i))))"
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac is_lubI 1),
- (rtac conjI 1),
- (rtac ub_rangeI 1),
- (rtac allI 1),
- (res_inst_tac [("t","S(i)")] (surjective_pairing RS ssubst) 1),
+ (rtac (conjI RS is_lubI) 1),
+ (rtac (allI RS ub_rangeI) 1),
+ (res_inst_tac [("t","S i")] (surjective_pairing RS ssubst) 1),
(rtac monofun_pair 1),
(rtac is_ub_thelub 1),
(etac (monofun_fst RS ch2ch_monofun) 1),
@@ -168,8 +147,7 @@
*)
-qed_goal "cpo_cprod" Cprod2.thy
- "is_chain(S::nat=>'a*'b)==>? x.range(S)<<| x"
+qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a*'b)==>? x.range S<<| x"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Cprod2.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cprod2.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/cprod2.thy
+(* Title: HOLCF/Cprod2.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -9,16 +9,8 @@
Cprod2 = Cprod1 +
-(* Witness for the above arity axiom is cprod1.ML *)
-
-arities "*" :: (pcpo,pcpo)po
-
-rules
-
-(* instance of << for type ['a * 'b] *)
-
-inst_cprod_po "((op <<)::['a * 'b,'a * 'b]=>bool) = less_cprod"
-
+instance "*"::(pcpo,pcpo)po
+ (refl_less_cprod,antisym_less_cprod,trans_less_cprod)
end
--- a/src/HOLCF/Cprod3.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cprod3.ML Mon Feb 17 10:57:11 1997 +0100
@@ -8,6 +8,13 @@
open Cprod3;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_cprod_pcpo" thy "UU = (UU,UU)"
+ (fn prems =>
+ [
+ (simp_tac (HOL_ss addsimps [UU_def,UU_cprod_def]) 1)
+ ]);
+
(* ------------------------------------------------------------------------ *)
(* continuity of (_,_) , fst, snd *)
(* ------------------------------------------------------------------------ *)
@@ -226,9 +233,9 @@
]);
qed_goal "cfst_strict" Cprod3.thy "cfst`UU = UU" (fn _ => [
- (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1)]);
+ (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1)]);
qed_goal "csnd_strict" Cprod3.thy "csnd`UU = UU" (fn _ => [
- (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1)]);
+ (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1)]);
qed_goalw "surjective_pairing_Cprod2" Cprod3.thy
[cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p"
@@ -242,22 +249,6 @@
(rtac (surjective_pairing RS sym) 1)
]);
-
-qed_goalw "less_cprod5b" Cprod3.thy [cfst_def,csnd_def,cpair_def]
- " (p1 << p2) = (cfst`p1 << cfst`p2 & csnd`p1 << csnd`p2)"
- (fn prems =>
- [
- (stac beta_cfun 1),
- (rtac cont_snd 1),
- (stac beta_cfun 1),
- (rtac cont_snd 1),
- (stac beta_cfun 1),
- (rtac cont_fst 1),
- (stac beta_cfun 1),
- (rtac cont_fst 1),
- (rtac less_cprod3b 1)
- ]);
-
qed_goalw "less_cprod5c" Cprod3.thy [cfst_def,csnd_def,cpair_def]
"<xa,ya> << <x,y> ==> xa<<x & ya << y"
(fn prems =>
@@ -269,7 +260,6 @@
(atac 1)
]);
-
qed_goalw "lub_cprod2" Cprod3.thy [cfst_def,csnd_def,cpair_def]
"[|is_chain(S)|] ==> range(S) <<| \
\ <(lub(range(%i.cfst`(S i)))) , lub(range(%i.csnd`(S i)))>"
--- a/src/HOLCF/Cprod3.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Cprod3.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,16 +1,15 @@
-(* Title: HOLCF/cprod3.thy
+(* Title: HOLCF/Cprod3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-
Class instance of * for class pcpo
*)
Cprod3 = Cprod2 +
-arities "*" :: (pcpo,pcpo)pcpo (* Witness cprod2.ML *)
+instance "*" :: (pcpo,pcpo)pcpo (least_cprod,cpo_cprod)
consts
cpair :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)
@@ -21,15 +20,10 @@
syntax
"@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)")
-
translations
"<x, y, z>" == "<x, <y, z>>"
"<x, y>" == "cpair`x`y"
-rules
-
-inst_cprod_pcpo "(UU::'a*'b) = (UU,UU)"
-
defs
cpair_def "cpair == (LAM x y.(x,y))"
cfst_def "cfst == (LAM p.fst(p))"
@@ -70,7 +64,6 @@
(* Misc Definitions *)
CLet_def "CLet == LAM s. LAM f.f`s"
-
syntax
(* syntax for LAM <x,y,z>.E *)
"@Cpttrn" :: "[pttrn,pttrns] => pttrn" ("<_,/_>")
--- a/src/HOLCF/Fix.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fix.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,9 +1,9 @@
-(* Title: HOLCF/fix.ML
+(* Title: HOLCF/Fix.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for fix.thy
+Lemmas for Fix.thy
*)
open Fix;
@@ -12,13 +12,13 @@
(* derive inductive properties of iterate from primitive recursion *)
(* ------------------------------------------------------------------------ *)
-qed_goal "iterate_0" Fix.thy "iterate 0 F x = x"
+qed_goal "iterate_0" thy "iterate 0 F x = x"
(fn prems =>
[
(resolve_tac (nat_recs iterate_def) 1)
]);
-qed_goal "iterate_Suc" Fix.thy "iterate (Suc n) F x = F`(iterate n F x)"
+qed_goal "iterate_Suc" thy "iterate (Suc n) F x = F`(iterate n F x)"
(fn prems =>
[
(resolve_tac (nat_recs iterate_def) 1)
@@ -26,7 +26,7 @@
Addsimps [iterate_0, iterate_Suc];
-qed_goal "iterate_Suc2" Fix.thy "iterate (Suc n) F x = iterate n F (F`x)"
+qed_goal "iterate_Suc2" thy "iterate (Suc n) F x = iterate n F (F`x)"
(fn prems =>
[
(nat_ind_tac "n" 1),
@@ -42,7 +42,7 @@
(* This property is essential since monotonicity of iterate makes no sense *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "is_chain_iterate2" Fix.thy [is_chain]
+qed_goalw "is_chain_iterate2" thy [is_chain]
" x << F`x ==> is_chain (%i.iterate i F x)"
(fn prems =>
[
@@ -56,7 +56,7 @@
]);
-qed_goal "is_chain_iterate" Fix.thy
+qed_goal "is_chain_iterate" thy
"is_chain (%i.iterate i F UU)"
(fn prems =>
[
@@ -71,7 +71,7 @@
(* ------------------------------------------------------------------------ *)
-qed_goalw "Ifix_eq" Fix.thy [Ifix_def] "Ifix F =F`(Ifix F)"
+qed_goalw "Ifix_eq" thy [Ifix_def] "Ifix F =F`(Ifix F)"
(fn prems =>
[
(stac contlub_cfun_arg 1),
@@ -95,7 +95,7 @@
]);
-qed_goalw "Ifix_least" Fix.thy [Ifix_def] "F`x=x ==> Ifix(F) << x"
+qed_goalw "Ifix_least" thy [Ifix_def] "F`x=x ==> Ifix(F) << x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -116,7 +116,7 @@
(* monotonicity and continuity of iterate *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_iterate" Fix.thy [monofun] "monofun(iterate(i))"
+qed_goalw "monofun_iterate" thy [monofun] "monofun(iterate(i))"
(fn prems =>
[
(strip_tac 1),
@@ -137,7 +137,7 @@
(* In this special case it is the application function fapp *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "contlub_iterate" Fix.thy [contlub] "contlub(iterate(i))"
+qed_goalw "contlub_iterate" thy [contlub] "contlub(iterate(i))"
(fn prems =>
[
(strip_tac 1),
@@ -168,7 +168,7 @@
]);
-qed_goal "cont_iterate" Fix.thy "cont(iterate(i))"
+qed_goal "cont_iterate" thy "cont(iterate(i))"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -180,7 +180,7 @@
(* a lemma about continuity of iterate in its third argument *)
(* ------------------------------------------------------------------------ *)
-qed_goal "monofun_iterate2" Fix.thy "monofun(iterate n F)"
+qed_goal "monofun_iterate2" thy "monofun(iterate n F)"
(fn prems =>
[
(rtac monofunI 1),
@@ -191,7 +191,7 @@
(etac monofun_cfun_arg 1)
]);
-qed_goal "contlub_iterate2" Fix.thy "contlub(iterate n F)"
+qed_goal "contlub_iterate2" thy "contlub(iterate n F)"
(fn prems =>
[
(rtac contlubI 1),
@@ -206,7 +206,7 @@
(etac (monofun_iterate2 RS ch2ch_monofun) 1)
]);
-qed_goal "cont_iterate2" Fix.thy "cont (iterate n F)"
+qed_goal "cont_iterate2" thy "cont (iterate n F)"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -218,7 +218,7 @@
(* monotonicity and continuity of Ifix *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_Ifix" Fix.thy [monofun,Ifix_def] "monofun(Ifix)"
+qed_goalw "monofun_Ifix" thy [monofun,Ifix_def] "monofun(Ifix)"
(fn prems =>
[
(strip_tac 1),
@@ -235,7 +235,7 @@
(* be derived for lubs in this argument *)
(* ------------------------------------------------------------------------ *)
-qed_goal "is_chain_iterate_lub" Fix.thy
+qed_goal "is_chain_iterate_lub" thy
"is_chain(Y) ==> is_chain(%i. lub(range(%ia. iterate ia (Y i) UU)))"
(fn prems =>
[
@@ -256,7 +256,7 @@
(* chains is the essential argument which is usually derived from monot. *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_Ifix_lemma1" Fix.thy
+qed_goal "contlub_Ifix_lemma1" thy
"is_chain(Y) ==>iterate n (lub(range Y)) y = lub(range(%i. iterate n (Y i) y))"
(fn prems =>
[
@@ -271,7 +271,7 @@
]);
-qed_goal "ex_lub_iterate" Fix.thy "is_chain(Y) ==>\
+qed_goal "ex_lub_iterate" thy "is_chain(Y) ==>\
\ lub(range(%i. lub(range(%ia. iterate i (Y ia) UU)))) =\
\ lub(range(%i. lub(range(%ia. iterate ia (Y i) UU))))"
(fn prems =>
@@ -305,7 +305,7 @@
]);
-qed_goalw "contlub_Ifix" Fix.thy [contlub,Ifix_def] "contlub(Ifix)"
+qed_goalw "contlub_Ifix" thy [contlub,Ifix_def] "contlub(Ifix)"
(fn prems =>
[
(strip_tac 1),
@@ -315,7 +315,7 @@
]);
-qed_goal "cont_Ifix" Fix.thy "cont(Ifix)"
+qed_goal "cont_Ifix" thy "cont(Ifix)"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -327,14 +327,14 @@
(* propagate properties of Ifix to its continuous counterpart *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "fix_eq" Fix.thy [fix_def] "fix`F = F`(fix`F)"
+qed_goalw "fix_eq" thy [fix_def] "fix`F = F`(fix`F)"
(fn prems =>
[
(asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
(rtac Ifix_eq 1)
]);
-qed_goalw "fix_least" Fix.thy [fix_def] "F`x = x ==> fix`F << x"
+qed_goalw "fix_least" thy [fix_def] "F`x = x ==> fix`F << x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -343,7 +343,7 @@
]);
-qed_goal "fix_eqI" Fix.thy
+qed_goal "fix_eqI" thy
"[| F`x = x; !z. F`z = z --> x << z |] ==> x = fix`F"
(fn prems =>
[
@@ -356,14 +356,14 @@
]);
-qed_goal "fix_eq2" Fix.thy "f == fix`F ==> f = F`f"
+qed_goal "fix_eq2" thy "f == fix`F ==> f = F`f"
(fn prems =>
[
(rewrite_goals_tac prems),
(rtac fix_eq 1)
]);
-qed_goal "fix_eq3" Fix.thy "f == fix`F ==> f`x = F`f`x"
+qed_goal "fix_eq3" thy "f == fix`F ==> f`x = F`f`x"
(fn prems =>
[
(rtac trans 1),
@@ -373,7 +373,7 @@
fun fix_tac3 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i));
-qed_goal "fix_eq4" Fix.thy "f = fix`F ==> f = F`f"
+qed_goal "fix_eq4" thy "f = fix`F ==> f = F`f"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -381,7 +381,7 @@
(rtac fix_eq 1)
]);
-qed_goal "fix_eq5" Fix.thy "f = fix`F ==> f`x = F`f`x"
+qed_goal "fix_eq5" thy "f = fix`F ==> f`x = F`f`x"
(fn prems =>
[
(rtac trans 1),
@@ -418,7 +418,7 @@
(* ------------------------------------------------------------------------ *)
-qed_goal "Ifix_def2" Fix.thy "Ifix=(%x. lub(range(%i. iterate i x UU)))"
+qed_goal "Ifix_def2" thy "Ifix=(%x. lub(range(%i. iterate i x UU)))"
(fn prems =>
[
(rtac ext 1),
@@ -430,7 +430,7 @@
(* direct connection between fix and iteration without Ifix *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "fix_def2" Fix.thy [fix_def]
+qed_goalw "fix_def2" thy [fix_def]
"fix`F = lub(range(%i. iterate i F UU))"
(fn prems =>
[
@@ -447,14 +447,14 @@
(* access to definitions *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "adm_def2" Fix.thy [adm_def]
+qed_goalw "adm_def2" thy [adm_def]
"adm(P) = (!Y. is_chain(Y) --> (!i.P(Y(i))) --> P(lub(range(Y))))"
(fn prems =>
[
(rtac refl 1)
]);
-qed_goalw "admw_def2" Fix.thy [admw_def]
+qed_goalw "admw_def2" thy [admw_def]
"admw(P) = (!F.(!n.P(iterate n F UU)) -->\
\ P (lub(range(%i.iterate i F UU))))"
(fn prems =>
@@ -466,7 +466,7 @@
(* an admissible formula is also weak admissible *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "adm_impl_admw" Fix.thy [admw_def] "adm(P)==>admw(P)"
+qed_goalw "adm_impl_admw" thy [admw_def] "adm(P)==>admw(P)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -481,7 +481,7 @@
(* fixed point induction *)
(* ------------------------------------------------------------------------ *)
-qed_goal "fix_ind" Fix.thy
+qed_goal "fix_ind" thy
"[| adm(P);P(UU);!!x. P(x) ==> P(F`x)|] ==> P(fix`F)"
(fn prems =>
[
@@ -499,7 +499,7 @@
(atac 1)
]);
-qed_goal "def_fix_ind" Fix.thy "[| f == fix`F; adm(P); \
+qed_goal "def_fix_ind" thy "[| f == fix`F; adm(P); \
\ P(UU);!!x. P(x) ==> P(F`x)|] ==> P f" (fn prems => [
(cut_facts_tac prems 1),
(asm_simp_tac HOL_ss 1),
@@ -511,7 +511,7 @@
(* computational induction for weak admissible formulae *)
(* ------------------------------------------------------------------------ *)
-qed_goal "wfix_ind" Fix.thy
+qed_goal "wfix_ind" thy
"[| admw(P); !n. P(iterate n F UU)|] ==> P(fix`F)"
(fn prems =>
[
@@ -523,7 +523,7 @@
(etac spec 1)
]);
-qed_goal "def_wfix_ind" Fix.thy "[| f == fix`F; admw(P); \
+qed_goal "def_wfix_ind" thy "[| f == fix`F; admw(P); \
\ !n. P(iterate n F UU) |] ==> P f" (fn prems => [
(cut_facts_tac prems 1),
(asm_simp_tac HOL_ss 1),
@@ -534,7 +534,7 @@
(* for chain-finite (easy) types every formula is admissible *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "adm_max_in_chain" Fix.thy [adm_def]
+qed_goalw "adm_max_in_chain" thy [adm_def]
"!Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain n Y) ==> adm(P::'a=>bool)"
(fn prems =>
[
@@ -550,7 +550,7 @@
(etac spec 1)
]);
-qed_goalw "adm_chain_finite" Fix.thy [chain_finite_def]
+qed_goalw "adm_chain_finite" thy [chain_finite_def]
"chain_finite(x::'a) ==> adm(P::'a=>bool)"
(fn prems =>
[
@@ -562,7 +562,7 @@
(* flat types are chain_finite *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "flat_imp_chain_finite" Fix.thy [flat_def,chain_finite_def]
+qed_goalw "flat_imp_chain_finite" thy [flat_def,chain_finite_def]
"flat(x::'a)==>chain_finite(x::'a)"
(fn prems =>
[
@@ -606,7 +606,16 @@
(* some properties of flat *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "flatdom2monofun" Fix.thy [flat_def]
+qed_goalw "flatI" thy [flat_def] "!x y::'a.x<<y-->x=UU|x=y==>flat(x::'a)"
+(fn prems => [rtac (hd(prems)) 1]);
+
+qed_goalw "flatE" thy [flat_def] "flat(x::'a)==>!x y::'a.x<<y-->x=UU|x=y"
+(fn prems => [rtac (hd(prems)) 1]);
+
+qed_goalw "flat_flat" thy [flat_def] "flat(x::'a::flat)"
+(fn prems => [rtac ax_flat 1]);
+
+qed_goalw "flatdom2monofun" thy [flat_def]
"[| flat(x::'a::pcpo); f UU = UU |] ==> monofun (f::'a=>'b::pcpo)"
(fn prems =>
[
@@ -615,15 +624,7 @@
]);
-qed_goalw "flat_void" Fix.thy [flat_def] "flat(UU::void)"
- (fn prems =>
- [
- (strip_tac 1),
- (rtac disjI1 1),
- (rtac unique_void2 1)
- ]);
-
-qed_goalw "flat_eq" Fix.thy [flat_def]
+qed_goalw "flat_eq" 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)]);
@@ -633,8 +634,19 @@
(* some lemmata for functions with flat/chain_finite domain/range types *)
(* ------------------------------------------------------------------------ *)
-qed_goal "chfin2finch" Fix.thy
- "[| is_chain (Y::nat=>'a); chain_finite (x::'a) |] ==> finite_chain Y"
+qed_goalw "chfinI" thy [chain_finite_def]
+ "!Y::nat=>'a.is_chain Y-->(? n.max_in_chain n Y)==>chain_finite(x::'a)"
+(fn prems => [rtac (hd(prems)) 1]);
+
+qed_goalw "chfinE" Fix.thy [chain_finite_def]
+ "chain_finite(x::'a)==>!Y::nat=>'a.is_chain Y-->(? n.max_in_chain n Y)"
+(fn prems => [rtac (hd(prems)) 1]);
+
+qed_goalw "chfin_chfin" thy [chain_finite_def] "chain_finite(x::'a::chfin)"
+(fn prems => [rtac ax_chfin 1]);
+
+qed_goal "chfin2finch" thy
+ "[| is_chain (Y::nat=>'a); chain_finite(x::'a) |] ==> finite_chain Y"
(fn prems =>
[
cut_facts_tac prems 1,
@@ -642,7 +654,9 @@
(!simpset addsimps [chain_finite_def,finite_chain_def])) 1
]);
-qed_goal "chfindom_monofun2cont" Fix.thy
+bind_thm("flat_subclass_chfin",flat_flat RS flat_imp_chain_finite RS chfinE);
+
+qed_goal "chfindom_monofun2cont" thy
"[| chain_finite(x::'a::pcpo); monofun f |] ==> cont (f::'a=>'b::pcpo)"
(fn prems =>
[
@@ -666,7 +680,7 @@
bind_thm("flatdom_monofun2cont",flat_imp_chain_finite RS chfindom_monofun2cont);
(* [| flat ?x; monofun ?f |] ==> cont ?f *)
-qed_goal "flatdom_strict2cont" Fix.thy
+qed_goal "flatdom_strict2cont" thy
"[| flat(x::'a::pcpo); f UU = UU |] ==> cont (f::'a=>'b::pcpo)"
(fn prems =>
[
@@ -675,7 +689,7 @@
flat_imp_chain_finite RS chfindom_monofun2cont])) 1
]);
-qed_goal "chfin_fappR" Fix.thy
+qed_goal "chfin_fappR" thy
"[| is_chain (Y::nat => 'a->'b); chain_finite(x::'b) |] ==> \
\ !s. ? n. lub(range(Y))`s = Y n`s"
(fn prems =>
@@ -687,7 +701,7 @@
fast_tac (HOL_cs addSIs [thelubI,lub_finch2,chfin2finch,ch2ch_fappL])1
]);
-qed_goalw "adm_chfindom" Fix.thy [adm_def]
+qed_goalw "adm_chfindom" thy [adm_def]
"chain_finite (x::'b) ==> adm (%(u::'a->'b). P(u`s))" (fn prems => [
cut_facts_tac prems 1,
strip_tac 1,
@@ -731,7 +745,7 @@
fast_tac (HOL_cs addDs [le_imp_less_or_eq]
addEs [chain_mono RS mp]) 1]);
-qed_goalw "admI" Fix.thy [adm_def]
+qed_goalw "admI" thy [adm_def]
"(!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
\ ==> P(lub (range Y))) ==> adm P"
(fn prems => [
@@ -745,7 +759,7 @@
(* a prove for embedding projection pairs is similar *)
(* ------------------------------------------------------------------------ *)
-qed_goal "iso_strict" Fix.thy
+qed_goal "iso_strict" thy
"!!f g.[|!y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
\ ==> f`UU=UU & g`UU=UU"
(fn prems =>
@@ -762,7 +776,7 @@
]);
-qed_goal "isorep_defined" Fix.thy
+qed_goal "isorep_defined" thy
"[|!x.rep`(abs`x)=x;!y.abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
(fn prems =>
[
@@ -776,7 +790,7 @@
(atac 1)
]);
-qed_goal "isoabs_defined" Fix.thy
+qed_goal "isoabs_defined" thy
"[|!x.rep`(abs`x) = x;!y.abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
(fn prems =>
[
@@ -794,7 +808,7 @@
(* propagation of flatness and chainfiniteness by continuous isomorphisms *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "chfin2chfin" Fix.thy [chain_finite_def]
+qed_goalw "chfin2chfin" thy [chain_finite_def]
"!!f g.[|chain_finite(x::'a); !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
\ ==> chain_finite(y::'b)"
(fn prems =>
@@ -817,7 +831,7 @@
(atac 1)
]);
-qed_goalw "flat2flat" Fix.thy [flat_def]
+qed_goalw "flat2flat" 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 =>
@@ -848,7 +862,7 @@
(* a result about functions with flat codomain *)
(* ------------------------------------------------------------------------- *)
-qed_goalw "flat_codom" Fix.thy [flat_def]
+qed_goalw "flat_codom" thy [flat_def]
"[|flat(y::'b);f`(x::'a)=(c::'b)|] ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
(fn prems =>
[
@@ -885,7 +899,7 @@
(* admissibility of special formulae and propagation *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "adm_less" Fix.thy [adm_def]
+qed_goalw "adm_less" thy [adm_def]
"[|cont u;cont v|]==> adm(%x.u x << v x)"
(fn prems =>
[
@@ -905,7 +919,7 @@
(atac 1)
]);
-qed_goal "adm_conj" Fix.thy
+qed_goal "adm_conj" thy
"[| adm P; adm Q |] ==> adm(%x. P x & Q x)"
(fn prems =>
[
@@ -923,7 +937,7 @@
(fast_tac HOL_cs 1)
]);
-qed_goal "adm_cong" Fix.thy
+qed_goal "adm_cong" thy
"(!x. P x = Q x) ==> adm P = adm Q "
(fn prems =>
[
@@ -934,13 +948,13 @@
(etac spec 1)
]);
-qed_goalw "adm_not_free" Fix.thy [adm_def] "adm(%x.t)"
+qed_goalw "adm_not_free" thy [adm_def] "adm(%x.t)"
(fn prems =>
[
(fast_tac HOL_cs 1)
]);
-qed_goalw "adm_not_less" Fix.thy [adm_def]
+qed_goalw "adm_not_less" thy [adm_def]
"cont t ==> adm(%x.~ (t x) << u)"
(fn prems =>
[
@@ -955,7 +969,7 @@
(atac 1)
]);
-qed_goal "adm_all" Fix.thy
+qed_goal "adm_all" thy
" !y.adm(P y) ==> adm(%x.!y.P y x)"
(fn prems =>
[
@@ -972,7 +986,7 @@
bind_thm ("adm_all2", allI RS adm_all);
-qed_goal "adm_subst" Fix.thy
+qed_goal "adm_subst" thy
"[|cont t; adm P|] ==> adm(%x. P (t x))"
(fn prems =>
[
@@ -990,7 +1004,7 @@
(atac 1)
]);
-qed_goal "adm_UU_not_less" Fix.thy "adm(%x.~ UU << t(x))"
+qed_goal "adm_UU_not_less" thy "adm(%x.~ UU << t(x))"
(fn prems =>
[
(res_inst_tac [("P2","%x.False")] (adm_cong RS iffD1) 1),
@@ -998,7 +1012,7 @@
(rtac adm_not_free 1)
]);
-qed_goalw "adm_not_UU" Fix.thy [adm_def]
+qed_goalw "adm_not_UU" thy [adm_def]
"cont(t)==> adm(%x.~ (t x) = UU)"
(fn prems =>
[
@@ -1016,7 +1030,7 @@
(atac 1)
]);
-qed_goal "adm_eq" Fix.thy
+qed_goal "adm_eq" thy
"[|cont u ; cont v|]==> adm(%x. u x = v x)"
(fn prems =>
[
@@ -1052,13 +1066,13 @@
(fast_tac HOL_cs 1)
]);
- val adm_disj_lemma2 = prove_goal Fix.thy
+ val adm_disj_lemma2 = prove_goal thy
"!!Q. [| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
\ lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
(fn _ => [fast_tac (!claset addEs [adm_def2 RS iffD1 RS spec RS mp RS mp]
addss !simpset) 1]);
- val adm_disj_lemma3 = prove_goalw Fix.thy [is_chain]
+ val adm_disj_lemma3 = prove_goalw thy [is_chain]
"!!Q. is_chain(Y) ==> is_chain(%m. if m < Suc i then Y(Suc i) else Y m)"
(fn _ =>
[
@@ -1080,7 +1094,7 @@
trans_tac 1
]);
- val adm_disj_lemma5 = prove_goal Fix.thy
+ val adm_disj_lemma5 = prove_goal thy
"!!Y::nat=>'a. [| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
\ lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
(fn prems =>
@@ -1093,7 +1107,7 @@
trans_tac 1
]);
- val adm_disj_lemma6 = prove_goal Fix.thy
+ val adm_disj_lemma6 = prove_goal thy
"[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
\ ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
(fn prems =>
@@ -1112,7 +1126,7 @@
(atac 1)
]);
- val adm_disj_lemma7 = prove_goal Fix.thy
+ val adm_disj_lemma7 = prove_goal thy
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ is_chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
(fn prems =>
@@ -1135,7 +1149,7 @@
(atac 1)
]);
- val adm_disj_lemma8 = prove_goal Fix.thy
+ val adm_disj_lemma8 = prove_goal thy
"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(LEAST j::nat. m<j & P(Y(j))))"
(fn prems =>
[
@@ -1146,7 +1160,7 @@
(etac (LeastI RS conjunct2) 1)
]);
- val adm_disj_lemma9 = prove_goal Fix.thy
+ val adm_disj_lemma9 = prove_goal thy
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
(fn prems =>
@@ -1177,7 +1191,7 @@
(rtac lessI 1)
]);
- val adm_disj_lemma10 = prove_goal Fix.thy
+ val adm_disj_lemma10 = prove_goal thy
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
(fn prems =>
@@ -1196,7 +1210,7 @@
(atac 1)
]);
- val adm_disj_lemma12 = prove_goal Fix.thy
+ val adm_disj_lemma12 = prove_goal thy
"[| adm(P); is_chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
(fn prems =>
[
@@ -1208,7 +1222,7 @@
in
-val adm_lemma11 = prove_goal Fix.thy
+val adm_lemma11 = prove_goal thy
"[| adm(P); is_chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
(fn prems =>
[
@@ -1218,7 +1232,7 @@
(atac 1)
]);
-val adm_disj = prove_goal Fix.thy
+val adm_disj = prove_goal thy
"[| adm P; adm Q |] ==> adm(%x.P x | Q x)"
(fn prems =>
[
@@ -1242,7 +1256,7 @@
bind_thm("adm_lemma11",adm_lemma11);
bind_thm("adm_disj",adm_disj);
-qed_goal "adm_imp" Fix.thy
+qed_goal "adm_imp" thy
"[| adm(%x.~(P x)); adm Q |] ==> adm(%x.P x --> Q x)"
(fn prems =>
[
@@ -1254,7 +1268,7 @@
(atac 1)
]);
-qed_goal "adm_not_conj" Fix.thy
+qed_goal "adm_not_conj" thy
"[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"(fn prems=>[
cut_facts_tac prems 1,
subgoal_tac
--- a/src/HOLCF/Fix.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fix.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/fix.thy
+(* Title: HOLCF/Fix.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -37,5 +37,15 @@
flat_def "flat (x::'a) == ! x y. (x::'a) << y --> (x = UU) | (x=y)"
+(* further useful class for HOLCF *)
+
+axclass chfin<pcpo
+
+ax_chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)"
+
+axclass flat<pcpo
+
+ax_flat "! x y.x << y --> (x = UU) | (x=y)"
+
end
--- a/src/HOLCF/Fun1.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fun1.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/fun1.ML
+(* Title: HOLCF/Fun1.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -12,14 +12,14 @@
(* less_fun is a partial order on 'a => 'b *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "refl_less_fun" Fun1.thy [less_fun_def] "less_fun f f"
+qed_goalw "refl_less_fun" thy [less_fun_def] "less(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_fun f1 f2; less_fun f2 f1|] ==> f1 = f2"
+ "[|less (f1::'a::term =>'b::po) f2; less 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_fun f1 f2; less_fun f2 f3 |] ==> less_fun f1 f3"
+ "[|less (f1::'a::term =>'b::po) f2; less f2 f3 |] ==> less f1 f3"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -38,12 +38,3 @@
(atac 1),
((etac allE 1) THEN (atac 1))
]);
-
-(*
- --------------------------------------------------------------------------
- Since less_fun :: "['a::term=>'b::po,'a::term=>'b::po] => bool" the
- lemmas refl_less_fun, antisym_less_fun, trans_less_fun justify
- the class arity fun::(term,po)po !!
- --------------------------------------------------------------------------
-*)
-
--- a/src/HOLCF/Fun1.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fun1.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/fun1.thy
+(* Title: HOLCF/Fun1.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -14,14 +14,11 @@
(* default class is still term *)
-consts
- less_fun :: "['a=>'b::po,'a=>'b] => bool"
-
defs
(* definition of the ordering less_fun *)
(* in fun1.ML it is proved that less_fun is a po *)
- less_fun_def "less_fun f1 f2 == ! x. f1(x) << f2(x)"
+ less_fun_def "less == (%f1 f2.!x. f1 x << f2 x)"
end
--- a/src/HOLCF/Fun2.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fun2.ML Mon Feb 17 10:57:11 1997 +0100
@@ -8,23 +8,38 @@
open Fun2;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x.f x << g x)"
+ (fn prems =>
+ [
+ (fold_goals_tac [po_def,less_fun_def]),
+ (rtac refl 1)
+ ]);
+
(* ------------------------------------------------------------------------ *)
(* Type 'a::term => 'b::pcpo is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "minimal_fun" Fun2.thy [UU_fun_def] "UU_fun << f"
+qed_goal "minimal_fun" thy "(%z.UU) << x"
(fn prems =>
[
- (stac inst_fun_po 1),
- (rewtac less_fun_def),
- (fast_tac (HOL_cs addSIs [minimal]) 1)
+ (simp_tac (!simpset addsimps [inst_fun_po,minimal]) 1)
+ ]);
+
+bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym);
+
+qed_goal "least_fun" thy "? x::'a=>'b::pcpo.!y.x<<y"
+(fn prems =>
+ [
+ (res_inst_tac [("x","(%z.UU)")] exI 1),
+ (rtac (minimal_fun RS allI) 1)
]);
(* ------------------------------------------------------------------------ *)
(* make the symbol << accessible for type fun *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_fun" Fun2.thy "(f1 << f2) = (! x. f1(x) << f2(x))"
+qed_goal "less_fun" thy "(f1 << f2) = (! x. f1(x) << f2(x))"
(fn prems =>
[
(stac inst_fun_po 1),
@@ -36,8 +51,8 @@
(* chains of functions yield chains in the po range *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ch2ch_fun" Fun2.thy
- "is_chain(S::nat=>('a::term => 'b::po)) ==> is_chain(% i.S(i)(x))"
+qed_goal "ch2ch_fun" thy
+ "is_chain(S::nat=>('a=>'b::po)) ==> is_chain(% i.S(i)(x))"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -103,4 +118,3 @@
(rtac exI 1),
(etac lub_fun 1)
]);
-
--- a/src/HOLCF/Fun2.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fun2.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,34 +1,16 @@
-(* Title: HOLCF/fun2.thy
+(* Title: HOLCF/Fun2.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class Instance =>::(term,po)po
-Definiton of least element
*)
Fun2 = Fun1 +
(* default class is still term !*)
-(* Witness for the above arity axiom is fun1.ML *)
-
-arities fun :: (term,po)po
-
-consts
- UU_fun :: "'a::term => 'b::pcpo"
-
-rules
-
-(* instance of << for type ['a::term => 'b::po] *)
-
-inst_fun_po "((op <<)::['a=>'b::po,'a=>'b::po ]=>bool) = less_fun"
-
-defs
-
-(* The least element in type 'a::term => 'b::pcpo *)
-
-UU_fun_def "UU_fun == (% x.UU)"
+instance fun :: (term,po)po (refl_less_fun,antisym_less_fun,trans_less_fun)
end
--- a/src/HOLCF/Fun3.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fun3.ML Mon Feb 17 10:57:11 1997 +0100
@@ -5,3 +5,10 @@
*)
open Fun3;
+
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_fun_pcpo" thy "UU = (%x.UU)"
+ (fn prems =>
+ [
+ (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1)
+ ]);
--- a/src/HOLCF/Fun3.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fun3.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/fun3.thy
+(* Title: HOLCF/Fun3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -11,13 +11,7 @@
(* default class is still term *)
-arities fun :: (term,pcpo)pcpo (* Witness fun2.ML *)
-
-rules
-
-inst_fun_pcpo "(UU::'a=>'b::pcpo) = UU_fun"
+instance fun :: (term,pcpo)pcpo (least_fun,cpo_fun)
end
-
-
--- a/src/HOLCF/HOLCF.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/HOLCF.thy Mon Feb 17 10:57:11 1997 +0100
@@ -8,9 +8,5 @@
*)
-HOLCF = Lift3 +
+HOLCF = One + Tr
-default pcpo
-
-end
-
--- a/src/HOLCF/IsaMakefile Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/IsaMakefile Mon Feb 17 10:57:11 1997 +0100
@@ -8,16 +8,19 @@
OUT = $(ISABELLE_OUTPUT_DIR)
-THYS = Void.thy Porder.thy Pcpo.thy \
+THYS = Porder.thy Porder0.thy Pcpo.thy \
Fun1.thy Fun2.thy Fun3.thy \
Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
Cprod1.thy Cprod2.thy Cprod3.thy \
Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
- Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy One.thy \
- Tr1.thy Tr2.thy Lift1.thy Lift2.thy Lift2.thy HOLCF.thy
+ Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
+ One.thy Tr.thy\
+ Lift1.thy Lift2.thy Lift3.thy HOLCF.thy
-FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML)
+ONLYTHYS = Lift.thy
+
+FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML)
$(OUT)/HOLCF: $(OUT)/HOL $(FILES)
@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/HOL HOLCF
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Lift.thy Mon Feb 17 10:57:11 1997 +0100
@@ -0,0 +1,16 @@
+(* Title: HOLCF/Lift.thy
+ ID: $Id$
+ Author: Oscar Slotosch
+ Copyright 1997 Technische Universitaet Muenchen
+*)
+
+Lift = Lift3 +
+
+instance lift :: (term)flat (ax_flat_lift)
+
+default pcpo
+
+end
+
+
+
--- a/src/HOLCF/Lift1.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Lift1.ML Mon Feb 17 10:57:11 1997 +0100
@@ -13,16 +13,18 @@
(* less_lift is a partial order on type 'a -> 'b *)
(* ------------------------------------------------------------------------ *)
-goalw Lift1.thy [less_lift_def] "less_lift x x";
+goalw thy [less_lift_def] "less (x::'a lift) x";
by (fast_tac HOL_cs 1);
qed"refl_less_lift";
-goalw Lift1.thy [less_lift_def]
- "less_lift x1 x2 & less_lift x2 x1 --> x1 = x2";
+val prems = goalw thy [less_lift_def]
+ "[|less (x1::'a lift) x2; less x2 x1|] ==> x1 = x2";
+by (cut_facts_tac prems 1);
by (fast_tac HOL_cs 1);
qed"antisym_less_lift";
-goalw Lift1.thy [less_lift_def]
- "less_lift x1 x2 & less_lift x2 x3 --> less_lift x1 x3";
+val prems = goalw Lift1.thy [less_lift_def]
+ "[|less (x1::'a lift) x2; less x2 x3|] ==> less x1 x3";
+by (cut_facts_tac prems 1);
by (fast_tac HOL_cs 1);
qed"trans_less_lift";
--- a/src/HOLCF/Lift1.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Lift1.thy Mon Feb 17 10:57:11 1997 +0100
@@ -6,21 +6,14 @@
Lifting types of class term to flat pcpo's
*)
-Lift1 = Tr2 +
+Lift1 = ccc1 +
default term
datatype 'a lift = Undef | Def 'a
-arities "lift" :: (term)term
-
-consts less_lift :: "['a lift, 'a lift] => bool"
- UU_lift :: "'a lift"
-
defs
- less_lift_def "less_lift x y == (x=y | x=Undef)"
-
+ less_lift_def "less x y == (x=y | x=Undef)"
end
-
--- a/src/HOLCF/Lift2.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Lift2.ML Mon Feb 17 10:57:11 1997 +0100
@@ -6,20 +6,32 @@
Theorems for Lift2.thy
*)
+open Lift2;
-open Lift2;
-Addsimps [less_lift_def];
-
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_lift_po" thy "(op <<)=(%x y.x=y|x=Undef)"
+ (fn prems =>
+ [
+ (fold_goals_tac [po_def,less_lift_def]),
+ (rtac refl 1)
+ ]);
(* -------------------------------------------------------------------------*)
(* type ('a)lift is pointed *)
(* ------------------------------------------------------------------------ *)
-
goal Lift2.thy "Undef << x";
by (simp_tac (!simpset addsimps [inst_lift_po]) 1);
qed"minimal_lift";
+bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
+
+qed_goal "least_lift" thy "? x::'a lift.!y.x<<y"
+(fn prems =>
+ [
+ (res_inst_tac [("x","Undef")] exI 1),
+ (rtac (minimal_lift RS allI) 1)
+ ]);
(* ------------------------------------------------------------------------ *)
(* ('a)lift is a cpo *)
--- a/src/HOLCF/Lift2.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Lift2.thy Mon Feb 17 10:57:11 1997 +0100
@@ -8,13 +8,8 @@
Lift2 = Lift1 +
-default term
-
-arities "lift" :: (term)po
-
-rules
-
- inst_lift_po "((op <<)::['a lift,'a lift]=>bool) = less_lift"
+instance "lift" :: (term)po (refl_less_lift,antisym_less_lift,trans_less_lift)
end
+
--- a/src/HOLCF/Lift3.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Lift3.ML Mon Feb 17 10:57:11 1997 +0100
@@ -9,6 +9,13 @@
open Lift3;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_lift_pcpo" thy "UU = Undef"
+ (fn prems =>
+ [
+ (simp_tac (HOL_ss addsimps [UU_def,UU_lift_def]) 1)
+ ]);
+
(* ----------------------------------------------------------- *)
(* From Undef to UU *)
(* ----------------------------------------------------------- *)
@@ -117,8 +124,6 @@
by (fast_tac (HOL_cs addSDs [DefE]) 1);
val DefE2 = result();
-
-
(* ---------------------------------------------------------- *)
(* Lift is flat *)
(* ---------------------------------------------------------- *)
@@ -127,7 +132,7 @@
by (simp_tac (!simpset addsimps [less_lift]) 1);
val flat_lift = result();
-
+bind_thm("ax_flat_lift",flat_lift RS flatE);
(* ---------------------------------------------------------- *)
@@ -237,89 +242,4 @@
fun cont_tacR i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN
REPEAT (cont_tac i);
-(* --------------------------------------------------------- *)
-(* Admissibility tactic and tricks *)
-(* --------------------------------------------------------- *)
-
-
-goal Lift3.thy "x~=FF = (x=TT|x=UU)";
-by (res_inst_tac [("p","x")] trE 1);
- by (TRYALL (Asm_full_simp_tac));
-qed"adm_trick_1";
-
-goal Lift3.thy "x~=TT = (x=FF|x=UU)";
-by (res_inst_tac [("p","x")] trE 1);
- by (TRYALL (Asm_full_simp_tac));
-qed"adm_trick_2";
-
-
-val adm_tricks = [adm_trick_1,adm_trick_2];
-
-(*val adm_tac = (fn i => ((resolve_tac adm_lemmas i)));*)
-(*val adm_tacR = (fn i => (REPEAT (adm_tac i)));*)
-(*val adm_cont_tac = (fn i => ((adm_tacR i) THEN (cont_tacR i)));*)
-
-(* ----------------------------------------------------------------- *)
-(* Relations between domains and terms using lift constructs *)
-(* ----------------------------------------------------------------- *)
-
-goal Lift3.thy
-"!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
-by (rtac iffI 1);
-(* 1 *)
-by (res_inst_tac [("p","t")] trE 1);
-by (fast_tac HOL_cs 1);
-by (res_inst_tac [("p","s")] trE 1);
-by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "(t andalso s) = FF" 1);
-by (fast_tac HOL_cs 1);
-by (Asm_full_simp_tac 1);
-by (res_inst_tac [("p","s")] trE 1);
-by (subgoal_tac "(t andalso s) = FF" 1);
-by (fast_tac HOL_cs 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "(t andalso s) = FF" 1);
-by (fast_tac HOL_cs 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "(t andalso s) = FF" 1);
-by (fast_tac HOL_cs 1);
-by (Asm_full_simp_tac 1);
-(* 2*)
-by (res_inst_tac [("p","t")] trE 1);
-by (fast_tac HOL_cs 1);
-by (Asm_full_simp_tac 1);
-by (fast_tac HOL_cs 1);
-qed"andalso_and";
-
-
-goal Lift3.thy "blift x ~=UU";
-by (simp_tac (!simpset addsimps [blift_def])1);
-by (case_tac "x" 1);
- by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-qed"blift_not_UU";
-
-goal Lift3.thy "(blift x ~=FF)= x";
-by (simp_tac (!simpset addsimps [blift_def]) 1);
-by (case_tac "x" 1);
- by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-qed"blift_and_bool";
-
-goal Lift3.thy "plift P`(Def y) = blift (P y)";
-by (simp_tac (!simpset addsimps [plift_def,flift1_def]) 1);
-qed"plift2blift";
-
-goal Lift3.thy
- "(If blift P then A else B fi)= (if P then A else B)";
-by (simp_tac (!simpset addsimps [blift_def]) 1);
-by (res_inst_tac [("P","P"),("Q","P")] impCE 1);
-by (fast_tac HOL_cs 1);
-by (REPEAT (Asm_full_simp_tac 1));
-qed"If_and_if";
-
-
-Addsimps [plift2blift,If_and_if,blift_not_UU,blift_and_bool];
-
-simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));
\ No newline at end of file
+simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));
--- a/src/HOLCF/Lift3.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Lift3.thy Mon Feb 17 10:57:11 1997 +0100
@@ -8,40 +8,24 @@
Lift3 = Lift2 +
-default term
-
-arities
- "lift" :: (term)pcpo
+instance lift :: (term)pcpo (cpo_lift,least_lift)
consts
flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)"
- blift :: "bool => tr"
- plift :: "('a => bool) => 'a lift -> tr"
flift2 :: "('a => 'b) => ('a lift -> 'b lift)"
translations
"UU" <= "Undef"
defs
- blift_def
- "blift b == (if b then TT else FF)"
-
flift1_def
"flift1 f == (LAM x. (case x of
Undef => UU
| Def y => (f y)))"
-
flift2_def
"flift2 f == (LAM x. (case x of
Undef => Undef
| Def y => Def (f y)))"
- plift_def
- "plift p == (LAM x. flift1 (%a. blift (p a))`x)"
-
-
-rules
- inst_lift_pcpo "(UU::'a lift) = Undef"
-
end
--- a/src/HOLCF/Makefile Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Makefile Mon Feb 17 10:57:11 1997 +0100
@@ -21,16 +21,19 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-THYS = Void.thy Porder.thy Pcpo.thy \
+THYS = Porder.thy Porder0.thy Pcpo.thy \
Fun1.thy Fun2.thy Fun3.thy \
Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
Cprod1.thy Cprod2.thy Cprod3.thy \
Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
- Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy One.thy \
- Tr1.thy Tr2.thy Lift1.thy Lift2.thy Lift2.thy HOLCF.thy
+ Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
+ One.thy Tr.thy \
+ Lift1.thy Lift2.thy Lift3.thy HOLCF.thy
-FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML)
+ONLYTHYS = Lift.thy
+
+FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML)
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/HOLCF: $(BIN)/HOL $(FILES)
--- a/src/HOLCF/One.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/One.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/One.ML
ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ Author: Oscar Slotosch
+ Copyright 1997 Technische Universitaet Muenchen
-Lemmas for One.thy
+Lemmas for One.thy
*)
open One;
@@ -12,24 +12,17 @@
(* Exhaustion and Elimination for type one *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "Exh_one" One.thy [one_def] "z=UU | z = one"
+qed_goalw "Exh_one" thy [ONE_def] "t=UU | t = ONE"
(fn prems =>
[
- (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),
- (rtac (abs_one_iso RS subst) 1),
- (etac cfun_arg_cong 1),
- (rtac disjI2 1),
- (rtac (abs_one_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (rtac (unique_void2 RS subst) 1),
- (atac 1)
- ]);
+ (lift.induct_tac "t" 1),
+ (fast_tac HOL_cs 1),
+ (Simp_tac 1),
+ (rtac unit_eq 1)
+ ]);
-qed_goal "oneE" One.thy
- "[| p=UU ==> Q; p = one ==>Q|] ==>Q"
+qed_goal "oneE" thy
+ "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q"
(fn prems =>
[
(rtac (Exh_one RS disjE) 1),
@@ -37,53 +30,22 @@
(eresolve_tac prems 1)
]);
+(* ------------------------------------------------------------------------ *)
+(* tactic for one-thms *)
+(* ------------------------------------------------------------------------ *)
+
+fun prover t = prove_goalw thy [ONE_def] t
+ (fn prems =>
+ [
+ (asm_simp_tac (!simpset addsimps [inst_lift_po]) 1)
+ ]);
+
(* ------------------------------------------------------------------------ *)
(* distinctness for type one : stored in a list *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "dist_less_one" One.thy [one_def] "~one << UU" (fn prems => [
- (rtac classical2 1),
- (rtac less_up4b 1),
- (rtac (rep_one_iso RS subst) 1),
- (rtac (rep_one_iso RS subst) 1),
- (rtac monofun_cfun_arg 1),
- (etac ((abs_one_iso RS allI) RS ((rep_one_iso RS allI) RS iso_strict )
- RS conjunct2 RS ssubst) 1)]);
-
-qed_goal "dist_eq_one" One.thy "one~=UU" (fn prems => [
- (rtac not_less2not_eq 1),
- (rtac dist_less_one 1)]);
-
-(* ------------------------------------------------------------------------ *)
-(* one is flat *)
-(* ------------------------------------------------------------------------ *)
+val dist_less_one = map prover ["~ONE << UU"];
-qed_goalw "flat_one" One.thy [flat_def] "flat one"
- (fn prems =>
- [
- (rtac allI 1),
- (rtac allI 1),
- (res_inst_tac [("p","x")] oneE 1),
- (Asm_simp_tac 1),
- (res_inst_tac [("p","y")] oneE 1),
- (asm_simp_tac (!simpset addsimps [dist_less_one]) 1),
- (Asm_simp_tac 1)
- ]);
-
+val dist_eq_one = map prover ["ONE~=UU","UU~=ONE"];
-(* ------------------------------------------------------------------------ *)
-(* properties of one_when *)
-(* here I tried a generic prove procedure *)
-(* ------------------------------------------------------------------------ *)
-
-fun prover s = prove_goalw One.thy [one_when_def,one_def] s
- (fn prems =>
- [
- (simp_tac (!simpset addsimps [(rep_one_iso ),
- (abs_one_iso RS allI) RS ((rep_one_iso RS allI)
- RS iso_strict) RS conjunct1] )1)
- ]);
-
-val one_when = map prover ["one_when`x`UU = UU","one_when`x`one = x"];
-
-Addsimps (dist_less_one::dist_eq_one::one_when);
+Addsimps (dist_less_one@dist_eq_one);
--- a/src/HOLCF/One.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/One.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,47 +1,21 @@
-(* Title: HOLCF/one.thy
+(* Title: HOLCF/One.thy
ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Introduce atomic type one = (void)u
-
-The type is axiomatized as the least solution of a domain equation.
-The functor term that specifies the domain equation is:
-
- FT = <U,K_{void}>
-
-For details see chapter 5 of:
-
-[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
- Dissertation, Technische Universit"at M"unchen, 1994
-
+ Author: Oscar Slotosch
+ Copyright 1997 Technische Universitaet Muenchen
*)
-One = ccc1+
+One = Lift +
-types one 0
-arities one :: pcpo
+types one = "unit lift"
consts
- abs_one :: "(void)u -> one"
- rep_one :: "one -> (void)u"
- one :: "one"
- one_when :: "'c -> one -> 'c"
+ ONE :: "one"
+
+translations
+ "one" == (type) "unit lift"
rules
- abs_one_iso "abs_one`(rep_one`u) = u"
- rep_one_iso "rep_one`(abs_one`x) = x"
-
-defs
- one_def "one == abs_one`(up`UU)"
- 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"
-
+ ONE_def "ONE == Def()"
end
-
-
-
--- a/src/HOLCF/Pcpo.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Pcpo.ML Mon Feb 17 10:57:11 1997 +0100
@@ -8,11 +8,23 @@
open Pcpo;
+
+(* ------------------------------------------------------------------------ *)
+(* derive the old rule minimal *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goalw "UU_least" thy [ UU_def ] "!z.UU << z"
+(fn prems => [
+ (rtac (select_eq_Ex RS iffD2) 1),
+ (rtac least 1)]);
+
+bind_thm("minimal",UU_least RS spec);
+
(* ------------------------------------------------------------------------ *)
(* in pcpo's everthing equal to THE lub has lub properties for every chain *)
(* ------------------------------------------------------------------------ *)
-qed_goal "thelubE" Pcpo.thy
+qed_goal "thelubE" thy
"[| is_chain(S);lub(range(S)) = (l::'a::pcpo)|] ==> range(S) <<| l "
(fn prems =>
[
@@ -33,7 +45,7 @@
bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub);
(* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1 *)
-qed_goal "maxinch_is_thelub" Pcpo.thy "is_chain Y ==> \
+qed_goal "maxinch_is_thelub" thy "is_chain Y ==> \
\ max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::pcpo))"
(fn prems =>
[
@@ -52,7 +64,7 @@
(* the << relation between two chains is preserved by their lubs *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_mono" Pcpo.thy
+qed_goal "lub_mono" thy
"[|is_chain(C1::(nat=>'a::pcpo));is_chain(C2); ! k. C1(k) << C2(k)|]\
\ ==> lub(range(C1)) << lub(range(C2))"
(fn prems =>
@@ -70,7 +82,7 @@
(* the = relation between two chains is preserved by their lubs *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_equal" Pcpo.thy
+qed_goal "lub_equal" thy
"[| is_chain(C1::(nat=>'a::pcpo));is_chain(C2);!k.C1(k)=C2(k)|]\
\ ==> lub(range(C1))=lub(range(C2))"
(fn prems =>
@@ -95,7 +107,7 @@
(* more results about mono and = of lubs of chains *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_mono2" Pcpo.thy
+qed_goal "lub_mono2" thy
"[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\
\ ==> lub(range(X))<<lub(range(Y))"
(fn prems =>
@@ -124,7 +136,7 @@
(resolve_tac prems 1)
]);
-qed_goal "lub_equal2" Pcpo.thy
+qed_goal "lub_equal2" thy
"[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\
\ ==> lub(range(X))=lub(range(Y))"
(fn prems =>
@@ -141,7 +153,7 @@
(fast_tac HOL_cs 1)
]);
-qed_goal "lub_mono3" Pcpo.thy "[|is_chain(Y::nat=>'a::pcpo);is_chain(X);\
+qed_goal "lub_mono3" thy "[|is_chain(Y::nat=>'a::pcpo);is_chain(X);\
\! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))"
(fn prems =>
[
@@ -162,10 +174,10 @@
(* usefull lemmas about UU *)
(* ------------------------------------------------------------------------ *)
-val eq_UU_sym = prove_goal Pcpo.thy "(UU = x) = (x = UU)" (fn _ => [
+val eq_UU_sym = prove_goal thy "(UU = x) = (x = UU)" (fn _ => [
fast_tac HOL_cs 1]);
-qed_goal "eq_UU_iff" Pcpo.thy "(x=UU)=(x<<UU)"
+qed_goal "eq_UU_iff" thy "(x=UU)=(x<<UU)"
(fn prems =>
[
(rtac iffI 1),
@@ -176,14 +188,14 @@
(rtac minimal 1)
]);
-qed_goal "UU_I" Pcpo.thy "x << UU ==> x = UU"
+qed_goal "UU_I" thy "x << UU ==> x = UU"
(fn prems =>
[
(stac eq_UU_iff 1),
(resolve_tac prems 1)
]);
-qed_goal "not_less2not_eq" Pcpo.thy "~x<<y ==> ~x=y"
+qed_goal "not_less2not_eq" thy "~x<<y ==> ~x=y"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -193,7 +205,7 @@
(rtac refl_less 1)
]);
-qed_goal "chain_UU_I" Pcpo.thy
+qed_goal "chain_UU_I" thy
"[|is_chain(Y);lub(range(Y))=UU|] ==> ! i.Y(i)=UU"
(fn prems =>
[
@@ -206,7 +218,7 @@
]);
-qed_goal "chain_UU_I_inverse" Pcpo.thy
+qed_goal "chain_UU_I_inverse" thy
"!i.Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU"
(fn prems =>
[
@@ -219,7 +231,7 @@
(etac spec 1)
]);
-qed_goal "chain_UU_I_inverse2" Pcpo.thy
+qed_goal "chain_UU_I_inverse2" thy
"~lub(range(Y::(nat=>'a::pcpo)))=UU ==> ? i.~ Y(i)=UU"
(fn prems =>
[
@@ -232,7 +244,7 @@
]);
-qed_goal "notUU_I" Pcpo.thy "[| x<<y; ~x=UU |] ==> ~y=UU"
+qed_goal "notUU_I" thy "[| x<<y; ~x=UU |] ==> ~y=UU"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -243,7 +255,7 @@
]);
-qed_goal "chain_mono2" Pcpo.thy
+qed_goal "chain_mono2" thy
"[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\
\ ==> ? j.!i.j<i-->~Y(i)=UU"
(fn prems =>
@@ -257,25 +269,3 @@
(etac (chain_mono RS mp) 1),
(atac 1)
]);
-
-
-
-
-(* ------------------------------------------------------------------------ *)
-(* uniqueness in void *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "unique_void2" Pcpo.thy "(x::void)=UU"
- (fn prems =>
- [
- (stac inst_void_pcpo 1),
- (rtac (Rep_Void_inverse RS subst) 1),
- (rtac (Rep_Void_inverse RS subst) 1),
- (rtac arg_cong 1),
- (rtac box_equals 1),
- (rtac refl 1),
- (rtac (unique_void RS sym) 1),
- (rtac (unique_void RS sym) 1)
- ]);
-
-
--- a/src/HOLCF/Pcpo.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Pcpo.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,22 +1,31 @@
+(* Title: HOLCF/Pcpo.thy
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
+
+introduction of the classes cpo and pcpo
+*)
Pcpo = Porder +
-classes pcpo < po
+(* The class cpo of chain complete partial orders *)
+(* ********************************************** *)
+axclass cpo < po
+ (* class axiom: *)
+ cpo "is_chain S ==> ? x. range(S) <<| (x::'a::po)"
-arities void :: pcpo
+(* The class pcpo of pointed cpos *)
+(* ****************************** *)
+axclass pcpo < cpo
+
+ least "? x.!y.x<<y"
consts
-
- UU :: "'a::pcpo"
+ UU :: "'a::pcpo"
syntax (symbols)
-
- UU :: "'a::pcpo" ("\\<bottom>")
-
-rules
+ UU :: "'a::pcpo" ("\\<bottom>")
- minimal "UU << x"
- cpo "is_chain S ==> ? x. range(S) <<| (x::'a::pcpo)"
-
-inst_void_pcpo "(UU::void) = UU_void"
+defs
+ UU_def "UU == @x.!y.x<<y"
end
--- a/src/HOLCF/Porder.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Porder.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,20 +1,18 @@
-(* Title: HOLCF/porder.thy
+(* Title: HOLCF/Porder.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for theory porder.thy
+Lemmas for theory Porder.thy
*)
-open Porder0;
open Porder;
-
(* ------------------------------------------------------------------------ *)
(* the reverse law of anti--symmetrie of << *)
(* ------------------------------------------------------------------------ *)
-qed_goal "antisym_less_inverse" Porder.thy "x=y ==> x << y & y << x"
+qed_goal "antisym_less_inverse" thy "x=y ==> x << y & y << x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -24,7 +22,7 @@
]);
-qed_goal "box_less" Porder.thy
+qed_goal "box_less" thy
"[| a << b; c << a; b << d|] ==> c << d"
(fn prems =>
[
@@ -38,7 +36,7 @@
(* lubs are unique *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "unique_lub " Porder.thy [is_lub, is_ub]
+qed_goalw "unique_lub "thy [is_lub, is_ub]
"[| S <<| x ; S <<| y |] ==> x=y"
( fn prems =>
[
@@ -54,8 +52,7 @@
(* chains are monotone functions *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "chain_mono" Porder.thy [is_chain]
- " is_chain(F) ==> x<y --> F(x)<<F(y)"
+qed_goalw "chain_mono" thy [is_chain] "is_chain F ==> x<y --> F x<<F y"
( fn prems =>
[
(cut_facts_tac prems 1),
@@ -74,8 +71,7 @@
(atac 1)
]);
-qed_goal "chain_mono3" Porder.thy
- "[| is_chain(F); x <= y |] ==> F(x) << F(y)"
+qed_goal "chain_mono3" thy "[| is_chain F; x <= y |] ==> F x << F y"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -92,7 +88,7 @@
(* The range of a chain is a totaly ordered << *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "chain_is_tord" Porder.thy [is_tord]
+qed_goalw "chain_is_tord" thy [is_tord]
"!!F. is_chain(F) ==> is_tord(range(F))"
(fn _ =>
[
@@ -103,8 +99,9 @@
(* ------------------------------------------------------------------------ *)
(* technical lemmas about lub and is_lub *)
(* ------------------------------------------------------------------------ *)
+bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
-qed_goal "lubI" Porder.thy "(? x. M <<| x) ==> M <<| lub(M)"
+qed_goal "lubI" thy "? x. M <<| x ==> M <<| lub(M)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -112,15 +109,14 @@
(etac (select_eq_Ex RS iffD2) 1)
]);
-qed_goal "lubE" Porder.thy " M <<| lub(M) ==> ? x. M <<| x"
+qed_goal "lubE" thy "M <<| lub(M) ==> ? x. M <<| x"
(fn prems =>
[
(cut_facts_tac prems 1),
(etac exI 1)
]);
-qed_goal "lub_eq" Porder.thy
- "(? x. M <<| x) = M <<| lub(M)"
+qed_goal "lub_eq" thy "(? x. M <<| x) = M <<| lub(M)"
(fn prems =>
[
(stac lub 1),
@@ -129,7 +125,7 @@
]);
-qed_goal "thelubI" Porder.thy " M <<| l ==> lub(M) = l"
+qed_goal "thelubI" thy "M <<| l ==> lub(M) = l"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -144,7 +140,7 @@
(* access to some definition as inference rule *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "is_lubE" Porder.thy [is_lub]
+qed_goalw "is_lubE" thy [is_lub]
"S <<| x ==> S <| x & (! u. S <| u --> x << u)"
(fn prems =>
[
@@ -152,7 +148,7 @@
(atac 1)
]);
-qed_goalw "is_lubI" Porder.thy [is_lub]
+qed_goalw "is_lubI" thy [is_lub]
"S <| x & (! u. S <| u --> x << u) ==> S <<| x"
(fn prems =>
[
@@ -160,15 +156,13 @@
(atac 1)
]);
-qed_goalw "is_chainE" Porder.thy [is_chain]
- "is_chain(F) ==> ! i. F(i) << F(Suc(i))"
+qed_goalw "is_chainE" thy [is_chain] "is_chain F ==> !i. F(i) << F(Suc(i))"
(fn prems =>
[
(cut_facts_tac prems 1),
(atac 1)]);
-qed_goalw "is_chainI" Porder.thy [is_chain]
- "! i. F(i) << F(Suc(i)) ==> is_chain(F) "
+qed_goalw "is_chainI" thy [is_chain] "!i. F i << F(Suc i) ==> is_chain F"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -178,8 +172,7 @@
(* technical lemmas about (least) upper bounds of chains *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "ub_rangeE" Porder.thy [is_ub]
- "range(S) <| x ==> ! i. S(i) << x"
+qed_goalw "ub_rangeE" thy [is_ub] "range S <| x ==> !i. S(i) << x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -189,8 +182,7 @@
(rtac rangeI 1)
]);
-qed_goalw "ub_rangeI" Porder.thy [is_ub]
- "! i. S(i) << x ==> range(S) <| x"
+qed_goalw "ub_rangeI" thy [is_ub] "!i. S i << x ==> range S <| x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -207,85 +199,11 @@
(* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1 *)
(* ------------------------------------------------------------------------ *)
-(* Prototype lemmas for class pcpo *)
-(* ------------------------------------------------------------------------ *)
-
-(* ------------------------------------------------------------------------ *)
-(* a technical argument about << on void *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "less_void" Porder.thy "((u1::void) << u2) = (u1 = u2)"
-(fn prems =>
- [
- (stac inst_void_po 1),
- (rewtac less_void_def),
- (rtac iffI 1),
- (rtac injD 1),
- (atac 2),
- (rtac inj_inverseI 1),
- (rtac Rep_Void_inverse 1),
- (etac arg_cong 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* void is pointed. The least element is UU_void *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "minimal_void" Porder.thy "UU_void << x"
-(fn prems =>
- [
- (stac inst_void_po 1),
- (rewtac less_void_def),
- (simp_tac (!simpset addsimps [unique_void]) 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* UU_void is the trivial lub of all chains in void *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "lub_void" Porder.thy [is_lub] "M <<| UU_void"
-(fn prems =>
- [
- (rtac conjI 1),
- (rewtac is_ub),
- (strip_tac 1),
- (stac inst_void_po 1),
- (rewtac less_void_def),
- (simp_tac (!simpset addsimps [unique_void]) 1),
- (strip_tac 1),
- (rtac minimal_void 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* lub(?M) = UU_void *)
-(* ------------------------------------------------------------------------ *)
-
-bind_thm ("thelub_void", lub_void RS thelubI);
-
-(* ------------------------------------------------------------------------ *)
-(* void is a cpo wrt. countable chains *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "cpo_void" Porder.thy
- "is_chain((S::nat=>void)) ==> ? x. range(S) <<| x "
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("x","UU_void")] exI 1),
- (rtac lub_void 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* end of prototype lemmas for class pcpo *)
-(* ------------------------------------------------------------------------ *)
-
-
-(* ------------------------------------------------------------------------ *)
(* results about finite chains *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "lub_finch1" Porder.thy [max_in_chain_def]
- "[| is_chain(C) ; max_in_chain i C|] ==> range(C) <<| C(i)"
+qed_goalw "lub_finch1" thy [max_in_chain_def]
+ "[| is_chain C; max_in_chain i C|] ==> range C <<| C i"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -306,7 +224,7 @@
(etac (ub_rangeE RS spec) 1)
]);
-qed_goalw "lub_finch2" Porder.thy [finite_chain_def]
+qed_goalw "lub_finch2" thy [finite_chain_def]
"finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)"
(fn prems=>
[
@@ -318,7 +236,7 @@
]);
-qed_goal "bin_chain" Porder.thy "x<<y ==> is_chain (%i. if i=0 then x else y)"
+qed_goal "bin_chain" thy "x<<y ==> is_chain (%i. if i=0 then x else y)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -330,7 +248,7 @@
(rtac refl_less 1)
]);
-qed_goalw "bin_chainmax" Porder.thy [max_in_chain_def,le_def]
+qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def]
"x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)"
(fn prems =>
[
@@ -341,7 +259,7 @@
(Asm_simp_tac 1)
]);
-qed_goal "lub_bin_chain" Porder.thy
+qed_goal "lub_bin_chain" thy
"x << y ==> range(%i. if (i=0) then x else y) <<| y"
(fn prems=>
[ (cut_facts_tac prems 1),
@@ -356,8 +274,8 @@
(* the maximal element in a chain is its lub *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_chain_maxelem" Porder.thy
-"[|? i.Y(i)=c;!i.Y(i)<<c|] ==> lub(range(Y)) = c"
+qed_goal "lub_chain_maxelem" thy
+"[|? i.Y i=c;!i.Y i<<c|] ==> lub(range Y) = c"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -375,7 +293,7 @@
(* the lub of a constant chain is the constant *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_const" Porder.thy "range(%x.c) <<| c"
+qed_goal "lub_const" thy "range(%x.c) <<| c"
(fn prems =>
[
(rtac is_lubI 1),
--- a/src/HOLCF/Porder.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Porder.thy Mon Feb 17 10:57:11 1997 +0100
@@ -33,11 +33,9 @@
defs
(* class definitions *)
-
is_ub "S <| x == ! y.y:S --> y<<x"
is_lub "S <<| x == S <| x & (! u. S <| u --> x << u)"
-
(* Arbitrary chains are total orders *)
is_tord "is_tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
@@ -45,14 +43,10 @@
is_chain "is_chain F == (! i.F(i) << F(Suc(i)))"
(* finite chains, needed for monotony of continouous functions *)
-
max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)"
-
finite_chain_def "finite_chain C == is_chain(C) & (? i. max_in_chain i C)"
-rules
-
-lub "lub S = (@x. S <<| x)"
+lub_def "lub S == (@x. S <<| x)"
end
--- a/src/HOLCF/Porder0.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Porder0.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,53 +1,33 @@
-(* Title: HOLCF/porder0.thy
+(* Title: HOLCF/Porder0.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Definition of class porder (partial order)
-The prototype theory for this class is void.thy
-
*)
-Porder0 = Void +
+Porder0 = Nat +
-(* Introduction of new class. The witness is type void. *)
-
-classes po < term
+(* first the global constant for HOLCF type classes *)
+consts
+ "less" :: "['a,'a] => bool" (infixl "\\<sqsubseteq>\\<sqsubseteq>" 55)
-(* default type is still term ! *)
-(* void is the prototype in po *)
-
-arities void :: po
-
+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 *)
consts
-
- "<<" :: "['a,'a::po] => bool" (infixl 55)
+ "<<" :: "['a,'a::po] => bool" (infixl 55)
syntax (symbols)
-
- "op <<" :: "['a,'a::po] => bool" (infixl "\\<sqsubseteq>" 55)
-
-rules
-
-(* class axioms: justification is theory Void *)
-
-refl_less "x<<x"
- (* witness refl_less_void *)
+ "op <<" :: "['a,'a::po] => bool" (infixl "\\<sqsubseteq>" 55)
-antisym_less "[|x<<y ; y<<x |] ==> x = y"
- (* witness antisym_less_void *)
-
-trans_less "[|x<<y ; y<<z |] ==> x<<z"
- (* witness trans_less_void *)
-
-(* instance of << for the prototype void *)
-
-inst_void_po "((op <<)::[void,void]=>bool) = less_void"
-
+defs
+po_def "(op <<) == less"
end
-
-
-
--- a/src/HOLCF/Sprod0.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Sprod0.ML Mon Feb 17 10:57:11 1997 +0100
@@ -19,7 +19,6 @@
(EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl])
]);
-
qed_goal "inj_onto_Abs_Sprod" Sprod0.thy
"inj_onto Abs_Sprod Sprod"
(fn prems =>
@@ -28,12 +27,10 @@
(etac Abs_Sprod_inverse 1)
]);
-
(* ------------------------------------------------------------------------ *)
(* Strictness and definedness of Spair_Rep *)
(* ------------------------------------------------------------------------ *)
-
qed_goalw "strict_Spair_Rep" Sprod0.thy [Spair_Rep_def]
"(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
(fn prems =>
@@ -374,3 +371,13 @@
(asm_simp_tac Sprod0_ss 1)
]);
+qed_goal "Sel_injective_Sprod" thy
+ "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1),
+ (rotate_tac ~1 1),
+ (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1),
+ (Asm_simp_tac 1)
+ ]);
--- a/src/HOLCF/Sprod0.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Sprod0.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,57 +1,36 @@
-(* Title: HOLCF/sprod0.thy
+(* Title: HOLCF/Sprod0.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Strict product
+Strict product with typedef
*)
Sprod0 = Cfun3 +
-(* new type for strict product *)
+constdefs
+ Spair_Rep :: ['a,'b] => ['a,'b] => bool
+ "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a & y=b ))"
-types "**" 2 (infixr 20)
-
-arities "**" :: (pcpo,pcpo)term
+typedef (Sprod) ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep a b}"
syntax (symbols)
-
- "**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20)
+ "**" :: [type, type] => type ("(_ \\<otimes>/ _)" [21,20] 20)
consts
- Sprod :: "('a => 'b => bool)set"
- Spair_Rep :: "['a,'b] => ['a,'b] => bool"
- Rep_Sprod :: "('a ** 'b) => ('a => 'b => bool)"
- Abs_Sprod :: "('a => 'b => bool) => ('a ** 'b)"
Ispair :: "['a,'b] => ('a ** 'b)"
Isfst :: "('a ** 'b) => 'a"
Issnd :: "('a ** 'b) => 'b"
defs
- Spair_Rep_def "Spair_Rep == (%a b. %x y.
- (~a=UU & ~b=UU --> x=a & y=b ))"
-
- Sprod_def "Sprod == {f. ? a b. f = Spair_Rep a b}"
-
-rules
- (*faking a type definition... *)
- (* "**" is isomorphic to Sprod *)
-
- Rep_Sprod "Rep_Sprod(p):Sprod"
- Rep_Sprod_inverse "Abs_Sprod(Rep_Sprod(p)) = p"
- Abs_Sprod_inverse "f:Sprod ==> Rep_Sprod(Abs_Sprod(f)) = f"
-
-defs
(*defining the abstract constants*)
Ispair_def "Ispair a b == Abs_Sprod(Spair_Rep a b)"
- Isfst_def "Isfst(p) == @z.
- (p=Ispair UU UU --> z=UU)
+ Isfst_def "Isfst(p) == @z. (p=Ispair UU UU --> z=UU)
&(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=a)"
- Issnd_def "Issnd(p) == @z.
- (p=Ispair UU UU --> z=UU)
+ Issnd_def "Issnd(p) == @z. (p=Ispair UU UU --> z=UU)
&(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)"
--- a/src/HOLCF/Sprod1.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Sprod1.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,183 +1,36 @@
-(* Title: HOLCF/sprod1.ML
+(* Title: HOLCF/Sprod1.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for theory sprod1.thy
+Lemmas for theory Sprod1.thy
*)
open Sprod1;
(* ------------------------------------------------------------------------ *)
-(* reduction properties for less_sprod *)
-(* ------------------------------------------------------------------------ *)
-
-
-qed_goalw "less_sprod1a" Sprod1.thy [less_sprod_def]
- "p1=Ispair UU UU ==> less_sprod p1 p2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac HOL_ss 1)
- ]);
-
-qed_goalw "less_sprod1b" Sprod1.thy [less_sprod_def]
- "p1~=Ispair UU UU ==> \
-\ less_sprod p1 p2 = ( Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac HOL_ss 1)
- ]);
-
-qed_goal "less_sprod2a" Sprod1.thy
- "less_sprod(Ispair x y)(Ispair UU UU) ==> x = UU | y = UU"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac (excluded_middle RS disjE) 1),
- (atac 2),
- (rtac disjI1 1),
- (rtac antisym_less 1),
- (rtac minimal 2),
- (res_inst_tac [("s","Isfst(Ispair x y)"),("t","x")] subst 1),
- (rtac Isfst 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1),
- (res_inst_tac [("s","Isfst(Ispair UU UU)"),("t","UU")] subst 1),
- (simp_tac Sprod0_ss 1),
- (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1),
- (REPEAT (fast_tac HOL_cs 1))
- ]);
-
-qed_goal "less_sprod2b" Sprod1.thy
- "less_sprod p (Ispair UU UU) ==> p = Ispair UU UU"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("p","p")] IsprodE 1),
- (atac 1),
- (hyp_subst_tac 1),
- (rtac strict_Ispair 1),
- (etac less_sprod2a 1)
- ]);
-
-qed_goal "less_sprod2c" Sprod1.thy
- "[|less_sprod(Ispair xa ya)(Ispair x y);\
-\ xa ~= UU ; ya ~= UU; x ~= UU ; y ~= UU |] ==> xa << x & ya << y"
-(fn prems =>
- [
- (rtac conjI 1),
- (res_inst_tac [("s","Isfst(Ispair xa ya)"),("t","xa")] subst 1),
- (simp_tac (Sprod0_ss addsimps prems)1),
- (res_inst_tac [("s","Isfst(Ispair x y)"),("t","x")] subst 1),
- (simp_tac (Sprod0_ss addsimps prems)1),
- (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1),
- (simp_tac (Sprod0_ss addsimps prems)1),
- (res_inst_tac [("s","Issnd(Ispair xa ya)"),("t","ya")] subst 1),
- (simp_tac (Sprod0_ss addsimps prems)1),
- (res_inst_tac [("s","Issnd(Ispair x y)"),("t","y")] subst 1),
- (simp_tac (Sprod0_ss addsimps prems)1),
- (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct2) 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1),
- (simp_tac (Sprod0_ss addsimps prems)1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
(* less_sprod is a partial order on Sprod *)
(* ------------------------------------------------------------------------ *)
-qed_goal "refl_less_sprod" Sprod1.thy "less_sprod p p"
-(fn prems =>
- [
- (res_inst_tac [("p","p")] IsprodE 1),
- (etac less_sprod1a 1),
- (hyp_subst_tac 1),
- (stac less_sprod1b 1),
- (rtac defined_Ispair 1),
- (REPEAT (fast_tac (HOL_cs addIs [refl_less]) 1))
- ]);
-
+qed_goalw "refl_less_sprod" thy [less_sprod_def]"less (p::'a ** 'b) p"
+(fn prems => [(fast_tac (HOL_cs addIs [refl_less]) 1)]);
-qed_goal "antisym_less_sprod" Sprod1.thy
- "[|less_sprod p1 p2;less_sprod p2 p1|] ==> p1=p2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("p","p1")] IsprodE 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p2")] IsprodE 1),
- (hyp_subst_tac 1),
- (rtac refl 1),
- (hyp_subst_tac 1),
- (rtac (strict_Ispair RS sym) 1),
- (etac less_sprod2a 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p2")] IsprodE 1),
- (hyp_subst_tac 1),
- (rtac (strict_Ispair) 1),
- (etac less_sprod2a 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("x1","x"),("y1","xa"),("x","y"),("y","ya")] (arg_cong RS cong) 1),
- (rtac antisym_less 1),
- (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1),
- (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1),
- (rtac antisym_less 1),
- (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1),
- (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1)
- ]);
-
-qed_goal "trans_less_sprod" Sprod1.thy
- "[|less_sprod (p1::'a**'b) p2;less_sprod p2 p3|] ==> less_sprod p1 p3"
- (fn prems =>
+qed_goalw "antisym_less_sprod" thy [less_sprod_def]
+ "[|less (p1::'a ** 'b) p2;less p2 p1|] ==> p1=p2"
+(fn prems =>
[
(cut_facts_tac prems 1),
- (res_inst_tac [("p","p1")] IsprodE 1),
- (etac less_sprod1a 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","p3")] IsprodE 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("s","p2"),("t","Ispair (UU::'a)(UU::'b)")] subst 1),
- (etac less_sprod2b 1),
- (atac 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("Q","p2=Ispair(UU::'a)(UU::'b)")]
- (excluded_middle RS disjE) 1),
- (stac (defined_Ispair RS less_sprod1b) 1),
- (REPEAT (atac 1)),
- (rtac conjI 1),
- (res_inst_tac [("y","Isfst(p2)")] trans_less 1),
- (rtac conjunct1 1),
- (rtac (less_sprod1b RS subst) 1),
- (rtac defined_Ispair 1),
- (REPEAT (atac 1)),
- (rtac conjunct1 1),
- (rtac (less_sprod1b RS subst) 1),
- (REPEAT (atac 1)),
- (res_inst_tac [("y","Issnd(p2)")] trans_less 1),
- (rtac conjunct2 1),
- (rtac (less_sprod1b RS subst) 1),
- (rtac defined_Ispair 1),
- (REPEAT (atac 1)),
- (rtac conjunct2 1),
- (rtac (less_sprod1b RS subst) 1),
- (REPEAT (atac 1)),
- (hyp_subst_tac 1),
- (res_inst_tac [("s","Ispair(UU::'a)(UU::'b)"),("t","Ispair x y")]
- subst 1),
- (etac (less_sprod2b RS sym) 1),
- (atac 1)
+ (rtac Sel_injective_Sprod 1),
+ (fast_tac (HOL_cs addIs [antisym_less]) 1),
+ (fast_tac (HOL_cs addIs [antisym_less]) 1)
]);
-
-
-
-
-
-
-
-
-
+qed_goalw "trans_less_sprod" thy [less_sprod_def]
+ "[|less (p1::'a**'b) p2;less p2 p3|] ==> less p1 p3"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac conjI 1),
+ (fast_tac (HOL_cs addIs [trans_less]) 1),
+ (fast_tac (HOL_cs addIs [trans_less]) 1)
+ ]);
--- a/src/HOLCF/Sprod1.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Sprod1.thy Mon Feb 17 10:57:11 1997 +0100
@@ -8,13 +8,7 @@
Sprod1 = Sprod0 +
-consts
- less_sprod :: "[('a ** 'b),('a ** 'b)] => bool"
-
defs
- less_sprod_def "less_sprod p1 p2 ==
- if p1 = Ispair UU UU
- then True
- else Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
+ less_sprod_def "less p1 p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
end
--- a/src/HOLCF/Sprod2.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Sprod2.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,70 +1,38 @@
-(* Title: HOLCF/sprod2.ML
+(* Title: HOLCF/Sprod2.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for sprod2.thy
+Lemmas for Sprod2.thy
*)
-
open Sprod2;
-(* ------------------------------------------------------------------------ *)
-(* access to less_sprod in class po *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "less_sprod3a" Sprod2.thy
- "p1=Ispair UU UU ==> p1 << p2"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (stac inst_sprod_po 1),
- (etac less_sprod1a 1)
- ]);
-
-
-qed_goal "less_sprod3b" Sprod2.thy
- "p1~=Ispair UU UU ==>\
-\ (p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))"
-(fn prems =>
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_sprod_po" thy "(op <<)=(%x y.Isfst x<<Isfst y&Issnd x<<Issnd y)"
+ (fn prems =>
[
- (cut_facts_tac prems 1),
- (stac inst_sprod_po 1),
- (etac less_sprod1b 1)
- ]);
-
-qed_goal "less_sprod4b" Sprod2.thy
- "p << Ispair UU UU ==> p = Ispair UU UU"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac less_sprod2b 1),
- (etac (inst_sprod_po RS subst) 1)
- ]);
-
-bind_thm ("less_sprod4a", less_sprod4b RS defined_Ispair_rev);
-(* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *)
-
-qed_goal "less_sprod4c" Sprod2.thy
- "[|Ispair xa ya << Ispair x y; xa~=UU; ya~=UU; x~=UU; y~=UU|] ==>\
-\ xa<<x & ya << y"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac less_sprod2c 1),
- (etac (inst_sprod_po RS subst) 1),
- (REPEAT (atac 1))
+ (fold_goals_tac [po_def,less_sprod_def]),
+ (rtac refl 1)
]);
(* ------------------------------------------------------------------------ *)
(* type sprod is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goal "minimal_sprod" Sprod2.thy "Ispair UU UU << p"
+qed_goal "minimal_sprod" thy "Ispair UU UU << p"
(fn prems =>
[
- (rtac less_sprod3a 1),
- (rtac refl 1)
+ (simp_tac(Sprod0_ss addsimps[inst_sprod_po,minimal])1)
+ ]);
+
+bind_thm ("UU_sprod_def",minimal_sprod RS minimal2UU RS sym);
+
+qed_goal "least_sprod" thy "? x::'a**'b.!y.x<<y"
+(fn prems =>
+ [
+ (res_inst_tac [("x","Ispair UU UU")] exI 1),
+ (rtac (minimal_sprod RS allI) 1)
]);
(* ------------------------------------------------------------------------ *)
@@ -77,77 +45,27 @@
(strip_tac 1),
(rtac (less_fun RS iffD2) 1),
(strip_tac 1),
- (res_inst_tac [("Q",
- " Ispair y xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
- (res_inst_tac [("Q",
- " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
- (rtac (less_sprod3b RS iffD2) 1),
- (atac 1),
- (rtac conjI 1),
- (stac Isfst 1),
- (etac (strict_Ispair_rev RS conjunct1) 1),
- (etac (strict_Ispair_rev RS conjunct2) 1),
- (stac Isfst 1),
- (etac (strict_Ispair_rev RS conjunct1) 1),
- (etac (strict_Ispair_rev RS conjunct2) 1),
+ (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
+ (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
+ (forward_tac [notUU_I] 1),
(atac 1),
- (stac Issnd 1),
- (etac (strict_Ispair_rev RS conjunct1) 1),
- (etac (strict_Ispair_rev RS conjunct2) 1),
- (stac Issnd 1),
- (etac (strict_Ispair_rev RS conjunct1) 1),
- (etac (strict_Ispair_rev RS conjunct2) 1),
- (rtac refl_less 1),
- (etac less_sprod3a 1),
- (res_inst_tac [("Q",
- " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
- (etac less_sprod3a 2),
- (res_inst_tac [("P","Ispair y xa = Ispair UU UU")] notE 1),
- (atac 2),
- (rtac defined_Ispair 1),
- (etac notUU_I 1),
- (etac (strict_Ispair_rev RS conjunct1) 1),
- (etac (strict_Ispair_rev RS conjunct2) 1)
+ (REPEAT(asm_simp_tac(Sprod0_ss
+ addsimps[inst_sprod_po,refl_less,minimal]) 1))
]);
-
qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))"
(fn prems =>
[
(strip_tac 1),
- (res_inst_tac [("Q",
- " Ispair x y = Ispair UU UU")] (excluded_middle RS disjE) 1),
- (res_inst_tac [("Q",
- " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
- (rtac (less_sprod3b RS iffD2) 1),
+ (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
+ (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
+ (forward_tac [notUU_I] 1),
(atac 1),
- (rtac conjI 1),
- (stac Isfst 1),
- (etac (strict_Ispair_rev RS conjunct1) 1),
- (etac (strict_Ispair_rev RS conjunct2) 1),
- (stac Isfst 1),
- (etac (strict_Ispair_rev RS conjunct1) 1),
- (etac (strict_Ispair_rev RS conjunct2) 1),
- (rtac refl_less 1),
- (stac Issnd 1),
- (etac (strict_Ispair_rev RS conjunct1) 1),
- (etac (strict_Ispair_rev RS conjunct2) 1),
- (stac Issnd 1),
- (etac (strict_Ispair_rev RS conjunct1) 1),
- (etac (strict_Ispair_rev RS conjunct2) 1),
- (atac 1),
- (etac less_sprod3a 1),
- (res_inst_tac [("Q",
- " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
- (etac less_sprod3a 2),
- (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
- (atac 2),
- (rtac defined_Ispair 1),
- (etac (strict_Ispair_rev RS conjunct1) 1),
- (etac notUU_I 1),
- (etac (strict_Ispair_rev RS conjunct2) 1)
+ (REPEAT(asm_simp_tac(Sprod0_ss
+ addsimps[inst_sprod_po,refl_less,minimal]) 1))
]);
+
qed_goal " monofun_Ispair" Sprod2.thy
"[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
(fn prems =>
@@ -166,60 +84,11 @@
(* Isfst and Issnd are monotone *)
(* ------------------------------------------------------------------------ *)
-qed_goalw " monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
-(fn prems =>
- [
- (strip_tac 1),
- (res_inst_tac [("p","x")] IsprodE 1),
- (hyp_subst_tac 1),
- (rtac trans_less 1),
- (rtac minimal 2),
- (stac strict_Isfst1 1),
- (rtac refl_less 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","y")] IsprodE 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("t","Isfst(Ispair xa ya)")] subst 1),
- (rtac refl_less 2),
- (etac (less_sprod4b RS sym RS arg_cong) 1),
- (hyp_subst_tac 1),
- (stac Isfst 1),
- (atac 1),
- (atac 1),
- (stac Isfst 1),
- (atac 1),
- (atac 1),
- (etac (less_sprod4c RS conjunct1) 1),
- (REPEAT (atac 1))
- ]);
+qed_goalw "monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
+(fn prems => [(simp_tac (HOL_ss addsimps [inst_sprod_po]) 1)]);
qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)"
-(fn prems =>
- [
- (strip_tac 1),
- (res_inst_tac [("p","x")] IsprodE 1),
- (hyp_subst_tac 1),
- (rtac trans_less 1),
- (rtac minimal 2),
- (stac strict_Issnd1 1),
- (rtac refl_less 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("p","y")] IsprodE 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("t","Issnd(Ispair xa ya)")] subst 1),
- (rtac refl_less 2),
- (etac (less_sprod4b RS sym RS arg_cong) 1),
- (hyp_subst_tac 1),
- (stac Issnd 1),
- (atac 1),
- (atac 1),
- (stac Issnd 1),
- (atac 1),
- (atac 1),
- (etac (less_sprod4c RS conjunct2) 1),
- (REPEAT (atac 1))
- ]);
-
+(fn prems => [(simp_tac (HOL_ss addsimps [inst_sprod_po]) 1)]);
(* ------------------------------------------------------------------------ *)
(* the type 'a ** 'b is a cpo *)
@@ -231,10 +100,8 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac is_lubI 1),
- (rtac conjI 1),
- (rtac ub_rangeI 1),
- (rtac allI 1),
+ (rtac (conjI RS is_lubI) 1),
+ (rtac (allI RS ub_rangeI) 1),
(res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1),
(rtac monofun_Ispair 1),
(rtac is_ub_thelub 1),
--- a/src/HOLCF/Sprod2.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Sprod2.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/sprod2.thy
+(* Title: HOLCF/Sprod2.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -8,17 +8,8 @@
Sprod2 = Sprod1 +
-arities "**" :: (pcpo,pcpo)po
-
-(* Witness for the above arity axiom is sprod1.ML *)
-
-rules
-
-(* instance of << for type ['a ** 'b] *)
-
-inst_sprod_po "((op <<)::['a ** 'b,'a ** 'b]=>bool) = less_sprod"
-
+instance "**"::(pcpo,pcpo)po
+ (refl_less_sprod, antisym_less_sprod, trans_less_sprod)
end
-
--- a/src/HOLCF/Sprod3.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Sprod3.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,18 +1,24 @@
-(* Title: HOLCF/sprod3.thy
+(* Title: HOLCF/Sprod3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for Sprod3.thy
+Lemmas for Sprod.thy
*)
open Sprod3;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_sprod_pcpo" thy "UU = Ispair UU UU"
+ (fn prems =>
+ [
+ (simp_tac (HOL_ss addsimps [UU_def,UU_sprod_def]) 1)
+ ]);
(* ------------------------------------------------------------------------ *)
(* continuity of Ispair, Isfst, Issnd *)
(* ------------------------------------------------------------------------ *)
-qed_goal "sprod3_lemma1" Sprod3.thy
+qed_goal "sprod3_lemma1" thy
"[| is_chain(Y); x~= UU; lub(range(Y))~= UU |] ==>\
\ Ispair (lub(range Y)) x =\
\ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \
@@ -49,7 +55,7 @@
(rtac minimal 1)
]);
-qed_goal "sprod3_lemma2" Sprod3.thy
+qed_goal "sprod3_lemma2" thy
"[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
\ Ispair (lub(range Y)) x =\
\ Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\
@@ -71,7 +77,7 @@
]);
-qed_goal "sprod3_lemma3" Sprod3.thy
+qed_goal "sprod3_lemma3" thy
"[| is_chain(Y); x = UU |] ==>\
\ Ispair (lub(range Y)) x =\
\ Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\
@@ -91,7 +97,7 @@
]);
-qed_goal "contlub_Ispair1" Sprod3.thy "contlub(Ispair)"
+qed_goal "contlub_Ispair1" thy "contlub(Ispair)"
(fn prems =>
[
(rtac contlubI 1),
@@ -117,7 +123,7 @@
(atac 1)
]);
-qed_goal "sprod3_lemma4" Sprod3.thy
+qed_goal "sprod3_lemma4" thy
"[| is_chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
\ Ispair x (lub(range Y)) =\
\ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
@@ -153,7 +159,7 @@
(asm_simp_tac Sprod0_ss 1)
]);
-qed_goal "sprod3_lemma5" Sprod3.thy
+qed_goal "sprod3_lemma5" thy
"[| is_chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
\ Ispair x (lub(range Y)) =\
\ Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\
@@ -174,7 +180,7 @@
(atac 1)
]);
-qed_goal "sprod3_lemma6" Sprod3.thy
+qed_goal "sprod3_lemma6" thy
"[| is_chain(Y); x = UU |] ==>\
\ Ispair x (lub(range Y)) =\
\ Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
@@ -193,7 +199,7 @@
(simp_tac Sprod0_ss 1)
]);
-qed_goal "contlub_Ispair2" Sprod3.thy "contlub(Ispair(x))"
+qed_goal "contlub_Ispair2" thy "contlub(Ispair(x))"
(fn prems =>
[
(rtac contlubI 1),
@@ -215,7 +221,7 @@
]);
-qed_goal "cont_Ispair1" Sprod3.thy "cont(Ispair)"
+qed_goal "cont_Ispair1" thy "cont(Ispair)"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -224,7 +230,7 @@
]);
-qed_goal "cont_Ispair2" Sprod3.thy "cont(Ispair(x))"
+qed_goal "cont_Ispair2" thy "cont(Ispair(x))"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -232,7 +238,7 @@
(rtac contlub_Ispair2 1)
]);
-qed_goal "contlub_Isfst" Sprod3.thy "contlub(Isfst)"
+qed_goal "contlub_Isfst" thy "contlub(Isfst)"
(fn prems =>
[
(rtac contlubI 1),
@@ -257,7 +263,7 @@
chain_UU_I RS spec]) 1)
]);
-qed_goal "contlub_Issnd" Sprod3.thy "contlub(Issnd)"
+qed_goal "contlub_Issnd" thy "contlub(Issnd)"
(fn prems =>
[
(rtac contlubI 1),
@@ -281,7 +287,7 @@
chain_UU_I RS spec]) 1)
]);
-qed_goal "cont_Isfst" Sprod3.thy "cont(Isfst)"
+qed_goal "cont_Isfst" thy "cont(Isfst)"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -289,7 +295,7 @@
(rtac contlub_Isfst 1)
]);
-qed_goal "cont_Issnd" Sprod3.thy "cont(Issnd)"
+qed_goal "cont_Issnd" thy "cont(Issnd)"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -297,14 +303,7 @@
(rtac contlub_Issnd 1)
]);
-(*
- --------------------------------------------------------------------------
- more lemmas for Sprod3.thy
-
- --------------------------------------------------------------------------
-*)
-
-qed_goal "spair_eq" Sprod3.thy "[|x1=x2;y1=y2|] ==> (|x1,y1|) = (|x2,y2|)"
+qed_goal "spair_eq" thy "[|x1=x2;y1=y2|] ==> (|x1,y1|) = (|x2,y2|)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -315,7 +314,7 @@
(* convert all lemmas to the continuous versions *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "beta_cfun_sprod" Sprod3.thy [spair_def]
+qed_goalw "beta_cfun_sprod" thy [spair_def]
"(LAM x y.Ispair x y)`a`b = Ispair a b"
(fn prems =>
[
@@ -327,7 +326,7 @@
(rtac refl 1)
]);
-qed_goalw "inject_spair" Sprod3.thy [spair_def]
+qed_goalw "inject_spair" thy [spair_def]
"[| aa~=UU ; ba~=UU ; (|a,b|)=(|aa,ba|) |] ==> a=aa & b=ba"
(fn prems =>
[
@@ -339,7 +338,7 @@
(rtac beta_cfun_sprod 1)
]);
-qed_goalw "inst_sprod_pcpo2" Sprod3.thy [spair_def] "UU = (|UU,UU|)"
+qed_goalw "inst_sprod_pcpo2" thy [spair_def] "UU = (|UU,UU|)"
(fn prems =>
[
(rtac sym 1),
@@ -349,7 +348,7 @@
(rtac inst_sprod_pcpo 1)
]);
-qed_goalw "strict_spair" Sprod3.thy [spair_def]
+qed_goalw "strict_spair" thy [spair_def]
"(a=UU | b=UU) ==> (|a,b|)=UU"
(fn prems =>
[
@@ -361,7 +360,7 @@
(etac strict_Ispair 1)
]);
-qed_goalw "strict_spair1" Sprod3.thy [spair_def] "(|UU,b|) = UU"
+qed_goalw "strict_spair1" thy [spair_def] "(|UU,b|) = UU"
(fn prems =>
[
(stac beta_cfun_sprod 1),
@@ -370,7 +369,7 @@
(rtac strict_Ispair1 1)
]);
-qed_goalw "strict_spair2" Sprod3.thy [spair_def] "(|a,UU|) = UU"
+qed_goalw "strict_spair2" thy [spair_def] "(|a,UU|) = UU"
(fn prems =>
[
(stac beta_cfun_sprod 1),
@@ -379,7 +378,7 @@
(rtac strict_Ispair2 1)
]);
-qed_goalw "strict_spair_rev" Sprod3.thy [spair_def]
+qed_goalw "strict_spair_rev" thy [spair_def]
"(|x,y|)~=UU ==> ~x=UU & ~y=UU"
(fn prems =>
[
@@ -390,7 +389,7 @@
(atac 1)
]);
-qed_goalw "defined_spair_rev" Sprod3.thy [spair_def]
+qed_goalw "defined_spair_rev" thy [spair_def]
"(|a,b|) = UU ==> (a = UU | b = UU)"
(fn prems =>
[
@@ -401,7 +400,7 @@
(atac 1)
]);
-qed_goalw "defined_spair" Sprod3.thy [spair_def]
+qed_goalw "defined_spair" thy [spair_def]
"[|a~=UU; b~=UU|] ==> (|a,b|) ~= UU"
(fn prems =>
[
@@ -412,7 +411,7 @@
(atac 1)
]);
-qed_goalw "Exh_Sprod2" Sprod3.thy [spair_def]
+qed_goalw "Exh_Sprod2" thy [spair_def]
"z=UU | (? a b. z=(|a,b|) & a~=UU & b~=UU)"
(fn prems =>
[
@@ -432,7 +431,7 @@
]);
-qed_goalw "sprodE" Sprod3.thy [spair_def]
+qed_goalw "sprodE" thy [spair_def]
"[|p=UU ==> Q;!!x y. [|p=(|x,y|);x~=UU ; y~=UU|] ==> Q|] ==> Q"
(fn prems =>
[
@@ -448,7 +447,7 @@
]);
-qed_goalw "strict_sfst" Sprod3.thy [sfst_def]
+qed_goalw "strict_sfst" thy [sfst_def]
"p=UU==>sfst`p=UU"
(fn prems =>
[
@@ -460,7 +459,7 @@
(atac 1)
]);
-qed_goalw "strict_sfst1" Sprod3.thy [sfst_def,spair_def]
+qed_goalw "strict_sfst1" thy [sfst_def,spair_def]
"sfst`(|UU,y|) = UU"
(fn prems =>
[
@@ -470,7 +469,7 @@
(rtac strict_Isfst1 1)
]);
-qed_goalw "strict_sfst2" Sprod3.thy [sfst_def,spair_def]
+qed_goalw "strict_sfst2" thy [sfst_def,spair_def]
"sfst`(|x,UU|) = UU"
(fn prems =>
[
@@ -480,7 +479,7 @@
(rtac strict_Isfst2 1)
]);
-qed_goalw "strict_ssnd" Sprod3.thy [ssnd_def]
+qed_goalw "strict_ssnd" thy [ssnd_def]
"p=UU==>ssnd`p=UU"
(fn prems =>
[
@@ -492,7 +491,7 @@
(atac 1)
]);
-qed_goalw "strict_ssnd1" Sprod3.thy [ssnd_def,spair_def]
+qed_goalw "strict_ssnd1" thy [ssnd_def,spair_def]
"ssnd`(|UU,y|) = UU"
(fn prems =>
[
@@ -502,7 +501,7 @@
(rtac strict_Issnd1 1)
]);
-qed_goalw "strict_ssnd2" Sprod3.thy [ssnd_def,spair_def]
+qed_goalw "strict_ssnd2" thy [ssnd_def,spair_def]
"ssnd`(|x,UU|) = UU"
(fn prems =>
[
@@ -512,7 +511,7 @@
(rtac strict_Issnd2 1)
]);
-qed_goalw "sfst2" Sprod3.thy [sfst_def,spair_def]
+qed_goalw "sfst2" thy [sfst_def,spair_def]
"y~=UU ==>sfst`(|x,y|)=x"
(fn prems =>
[
@@ -523,7 +522,7 @@
(etac Isfst2 1)
]);
-qed_goalw "ssnd2" Sprod3.thy [ssnd_def,spair_def]
+qed_goalw "ssnd2" thy [ssnd_def,spair_def]
"x~=UU ==>ssnd`(|x,y|)=y"
(fn prems =>
[
@@ -535,7 +534,7 @@
]);
-qed_goalw "defined_sfstssnd" Sprod3.thy [sfst_def,ssnd_def,spair_def]
+qed_goalw "defined_sfstssnd" thy [sfst_def,ssnd_def,spair_def]
"p~=UU ==> sfst`p ~=UU & ssnd`p ~=UU"
(fn prems =>
[
@@ -550,7 +549,7 @@
]);
-qed_goalw "surjective_pairing_Sprod2" Sprod3.thy
+qed_goalw "surjective_pairing_Sprod2" thy
[sfst_def,ssnd_def,spair_def] "(|sfst`p , ssnd`p|) = p"
(fn prems =>
[
@@ -563,38 +562,7 @@
]);
-qed_goalw "less_sprod5b" Sprod3.thy [sfst_def,ssnd_def,spair_def]
- "p1~=UU ==> (p1<<p2) = (sfst`p1<<sfst`p2 & ssnd`p1<<ssnd`p2)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (stac beta_cfun 1),
- (rtac cont_Issnd 1),
- (stac beta_cfun 1),
- (rtac cont_Issnd 1),
- (stac beta_cfun 1),
- (rtac cont_Isfst 1),
- (stac beta_cfun 1),
- (rtac cont_Isfst 1),
- (rtac less_sprod3b 1),
- (rtac (inst_sprod_pcpo RS subst) 1),
- (atac 1)
- ]);
-
-
-qed_goalw "less_sprod5c" Sprod3.thy [sfst_def,ssnd_def,spair_def]
- "[|(|xa,ya|) << (|x,y|);xa~=UU;ya~=UU;x~=UU;y~=UU|] ==>xa<<x & ya << y"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac less_sprod4c 1),
- (REPEAT (atac 2)),
- (rtac (beta_cfun_sprod RS subst) 1),
- (rtac (beta_cfun_sprod RS subst) 1),
- (atac 1)
- ]);
-
-qed_goalw "lub_sprod2" Sprod3.thy [sfst_def,ssnd_def,spair_def]
+qed_goalw "lub_sprod2" thy [sfst_def,ssnd_def,spair_def]
"[|is_chain(S)|] ==> range(S) <<| \
\ (| lub(range(%i.sfst`(S i))), lub(range(%i.ssnd`(S i))) |)"
(fn prems =>
@@ -617,7 +585,7 @@
(|lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i)))|)" : thm
*)
-qed_goalw "ssplit1" Sprod3.thy [ssplit_def]
+qed_goalw "ssplit1" thy [ssplit_def]
"ssplit`f`UU=UU"
(fn prems =>
[
@@ -627,7 +595,7 @@
(rtac refl 1)
]);
-qed_goalw "ssplit2" Sprod3.thy [ssplit_def]
+qed_goalw "ssplit2" thy [ssplit_def]
"[|x~=UU;y~=UU|] ==> ssplit`f`(|x,y|)= f`x`y"
(fn prems =>
[
@@ -647,7 +615,7 @@
]);
-qed_goalw "ssplit3" Sprod3.thy [ssplit_def]
+qed_goalw "ssplit3" thy [ssplit_def]
"ssplit`spair`z=z"
(fn prems =>
[
@@ -664,7 +632,6 @@
(rtac surjective_pairing_Sprod2 1)
]);
-
(* ------------------------------------------------------------------------ *)
(* install simplifier for Sprod *)
(* ------------------------------------------------------------------------ *)
@@ -672,7 +639,5 @@
val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair,
ssplit1,ssplit2];
+Addsimps Sprod_rews;
-Addsimps [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
- strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair,
- ssplit1,ssplit2];
--- a/src/HOLCF/Sprod3.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Sprod3.thy Mon Feb 17 10:57:11 1997 +0100
@@ -8,7 +8,7 @@
Sprod3 = Sprod2 +
-arities "**" :: (pcpo,pcpo)pcpo (* Witness sprod2.ML *)
+instance "**" :: (pcpo,pcpo)pcpo (least_sprod,cpo_sprod)
consts
spair :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
@@ -17,18 +17,14 @@
ssplit :: "('a->'b->'c)->('a**'b)->'c"
syntax
- "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(|_,/ _|'))")
+ "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(|_,/ _|'))")
translations
"(|x, y, z|)" == "(|x, (|y, z|)|)"
"(|x, y|)" == "spair`x`y"
syntax (symbols)
- "@stuple" :: "['a, args] => 'a ** 'b" ("(1\\<lparr>_,/ _\\<rparr>)")
-
-rules
-
-inst_sprod_pcpo "(UU::'a**'b) = Ispair UU UU"
+ "@stuple" :: "['a, args] => 'a ** 'b" ("(1\\<lparr>_,/ _\\<rparr>)")
defs
spair_def "spair == (LAM x y.Ispair x y)"
@@ -36,7 +32,6 @@
ssnd_def "ssnd == (LAM p.Issnd p)"
ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
-
end
--- a/src/HOLCF/Ssum0.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Ssum0.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,51 +1,30 @@
-(* Title: HOLCF/ssum0.thy
+(* Title: HOLCF/Ssum0.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Strict sum
+Strict sum with typedef
*)
Ssum0 = Cfun3 +
-(* new type for strict sum *)
+constdefs
+ Sinl_Rep :: ['a,'a,'b,bool]=>bool
+ "Sinl_Rep == (%a.%x y p. (a~=UU --> x=a & p))"
+ Sinr_Rep :: ['b,'a,'b,bool]=>bool
+ "Sinr_Rep == (%b.%x y p.(b~=UU --> y=b & ~p))"
-types "++" 2 (infixr 10)
-
-arities "++" :: (pcpo,pcpo)term
+typedef (Ssum) ('a, 'b) "++" (infixr 10) =
+ "{f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
syntax (symbols)
-
- "++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20)
+ "++" :: [type, type] => type ("(_ \\<oplus>/ _)" [21, 20] 20)
consts
- Ssum :: "(['a,'b,bool]=>bool)set"
- Sinl_Rep :: "['a,'a,'b,bool]=>bool"
- Sinr_Rep :: "['b,'a,'b,bool]=>bool"
- Rep_Ssum :: "('a ++ 'b) => (['a,'b,bool]=>bool)"
- Abs_Ssum :: "(['a,'b,bool]=>bool) => ('a ++ 'b)"
Isinl :: "'a => ('a ++ 'b)"
Isinr :: "'b => ('a ++ 'b)"
Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
-defs
-
- Sinl_Rep_def "Sinl_Rep == (%a.%x y p.
- (a~=UU --> x=a & p))"
-
- Sinr_Rep_def "Sinr_Rep == (%b.%x y p.
- (b~=UU --> y=b & ~p))"
-
- Ssum_def "Ssum =={f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
-
-rules
- (*faking a type definition... *)
- (* "++" is isomorphic to Ssum *)
-
- Rep_Ssum "Rep_Ssum(p):Ssum"
- Rep_Ssum_inverse "Abs_Ssum(Rep_Ssum(p)) = p"
- Abs_Ssum_inverse "f:Ssum ==> Rep_Ssum(Abs_Ssum(f)) = f"
-
defs (*defining the abstract constants*)
Isinl_def "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
Isinr_def "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
--- a/src/HOLCF/Ssum1.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Ssum1.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,9 +1,9 @@
-(* Title: HOLCF/ssum1.ML
+(* Title: HOLCF/Ssum1.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for theory ssum1.thy
+Lemmas for theory Ssum1.thy
*)
open Ssum1;
@@ -40,8 +40,8 @@
in
-val less_ssum1a = prove_goalw Ssum1.thy [less_ssum_def]
-"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less_ssum s1 s2 = (x << y)"
+val less_ssum1a = prove_goalw thy [less_ssum_def]
+"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less s1 s2 = (x << y)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -81,8 +81,8 @@
]);
-val less_ssum1b = prove_goalw Ssum1.thy [less_ssum_def]
-"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less_ssum s1 s2 = (x << y)"
+val less_ssum1b = prove_goalw thy [less_ssum_def]
+"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less s1 s2 = (x << y)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -123,8 +123,8 @@
]);
-val less_ssum1c = prove_goalw Ssum1.thy [less_ssum_def]
-"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less_ssum s1 s2 = ((x::'a) = UU)"
+val less_ssum1c = prove_goalw thy [less_ssum_def]
+"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less s1 s2 = ((x::'a) = UU)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -165,8 +165,8 @@
]);
-val less_ssum1d = prove_goalw Ssum1.thy [less_ssum_def]
-"[|s1=Isinr(x); s2=Isinl(y)|] ==> less_ssum s1 s2 = (x = UU)"
+val less_ssum1d = prove_goalw thy [less_ssum_def]
+"[|s1=Isinr(x); s2=Isinl(y)|] ==> less s1 s2 = (x = UU)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -212,8 +212,8 @@
(* optimize lemmas about less_ssum *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_ssum2a" Ssum1.thy
- "less_ssum (Isinl x) (Isinl y) = (x << y)"
+qed_goal "less_ssum2a" thy
+ "less (Isinl x) (Isinl y) = (x << y)"
(fn prems =>
[
(rtac less_ssum1a 1),
@@ -221,8 +221,8 @@
(rtac refl 1)
]);
-qed_goal "less_ssum2b" Ssum1.thy
- "less_ssum (Isinr x) (Isinr y) = (x << y)"
+qed_goal "less_ssum2b" thy
+ "less (Isinr x) (Isinr y) = (x << y)"
(fn prems =>
[
(rtac less_ssum1b 1),
@@ -230,8 +230,8 @@
(rtac refl 1)
]);
-qed_goal "less_ssum2c" Ssum1.thy
- "less_ssum (Isinl x) (Isinr y) = (x = UU)"
+qed_goal "less_ssum2c" thy
+ "less (Isinl x) (Isinr y) = (x = UU)"
(fn prems =>
[
(rtac less_ssum1c 1),
@@ -239,8 +239,8 @@
(rtac refl 1)
]);
-qed_goal "less_ssum2d" Ssum1.thy
- "less_ssum (Isinr x) (Isinl y) = (x = UU)"
+qed_goal "less_ssum2d" thy
+ "less (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" Ssum1.thy "less_ssum p p"
+qed_goal "refl_less_ssum" thy "less (p::'a++'b) p"
(fn prems =>
[
(res_inst_tac [("p","p")] IssumE2 1),
@@ -265,8 +265,8 @@
(rtac refl_less 1)
]);
-qed_goal "antisym_less_ssum" Ssum1.thy
- "[|less_ssum p1 p2; less_ssum p2 p1|] ==> p1=p2"
+qed_goal "antisym_less_ssum" thy
+ "[|less (p1::'a++'b) p2; less p2 p1|] ==> p1=p2"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -295,8 +295,8 @@
(etac (less_ssum2b RS iffD1) 1)
]);
-qed_goal "trans_less_ssum" Ssum1.thy
- "[|less_ssum p1 p2; less_ssum p2 p3|] ==> less_ssum p1 p3"
+qed_goal "trans_less_ssum" thy
+ "[|less (p1::'a++'b) p2; less p2 p3|] ==> less p1 p3"
(fn prems =>
[
(cut_facts_tac prems 1),
--- a/src/HOLCF/Ssum1.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Ssum1.thy Mon Feb 17 10:57:11 1997 +0100
@@ -1,4 +1,4 @@
-(* Title: HOLCF/ssum1.thy
+(* Title: HOLCF/Ssum1.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -8,17 +8,12 @@
Ssum1 = Ssum0 +
-consts
-
- less_ssum :: "[('a ++ 'b),('a ++ 'b)] => bool"
-
-rules
-
- less_ssum_def "less_ssum 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))
- &(! v x.s1=Isinr(v) & s2=Isinl(x) --> z = (v = UU)))"
+defs
+ less_ssum_def "less == (%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))
+ &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
end
--- a/src/HOLCF/Ssum2.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Ssum2.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,55 +1,58 @@
-(* Title: HOLCF/ssum2.ML
+(* Title: HOLCF/Ssum2.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for ssum2.thy
+Lemmas for Ssum2.thy
*)
open Ssum2;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_ssum_po" thy "(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))\
+\ &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
+ (fn prems =>
+ [
+ (fold_goals_tac [po_def,less_ssum_def]),
+ (rtac refl 1)
+ ]);
+
(* ------------------------------------------------------------------------ *)
(* access to less_ssum in class po *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_ssum3a" Ssum2.thy
- "(Isinl(x) << Isinl(y)) = (x << y)"
+qed_goal "less_ssum3a" thy "Isinl x << Isinl y = x << y"
(fn prems =>
[
- (stac inst_ssum_po 1),
- (rtac less_ssum2a 1)
+ (simp_tac (!simpset addsimps [po_def,less_ssum2a]) 1)
]);
-qed_goal "less_ssum3b" Ssum2.thy
- "(Isinr(x) << Isinr(y)) = (x << y)"
+qed_goal "less_ssum3b" thy "Isinr x << Isinr y = x << y"
(fn prems =>
[
- (stac inst_ssum_po 1),
- (rtac less_ssum2b 1)
+ (simp_tac (!simpset addsimps [po_def,less_ssum2b]) 1)
]);
-qed_goal "less_ssum3c" Ssum2.thy
- "(Isinl(x) << Isinr(y)) = (x = UU)"
+qed_goal "less_ssum3c" thy "Isinl x << Isinr y = (x = UU)"
(fn prems =>
[
- (stac inst_ssum_po 1),
- (rtac less_ssum2c 1)
+ (simp_tac (!simpset addsimps [po_def,less_ssum2c]) 1)
]);
-qed_goal "less_ssum3d" Ssum2.thy
- "(Isinr(x) << Isinl(y)) = (x = UU)"
+qed_goal "less_ssum3d" thy "Isinr x << Isinl y = (x = UU)"
(fn prems =>
[
- (stac inst_ssum_po 1),
- (rtac less_ssum2d 1)
+ (simp_tac (!simpset addsimps [po_def,less_ssum2d]) 1)
]);
-
(* ------------------------------------------------------------------------ *)
(* type ssum ++ is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goal "minimal_ssum" Ssum2.thy "Isinl(UU) << s"
+qed_goal "minimal_ssum" thy "Isinl UU << s"
(fn prems =>
[
(res_inst_tac [("p","s")] IssumE2 1),
@@ -62,19 +65,27 @@
(rtac minimal 1)
]);
+bind_thm ("UU_ssum_def",minimal_ssum RS minimal2UU RS sym);
+
+qed_goal "least_ssum" thy "? x::'a++'b.!y.x<<y"
+(fn prems =>
+ [
+ (res_inst_tac [("x","Isinl UU")] exI 1),
+ (rtac (minimal_ssum RS allI) 1)
+ ]);
(* ------------------------------------------------------------------------ *)
(* Isinl, Isinr are monotone *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_Isinl" Ssum2.thy [monofun] "monofun(Isinl)"
+qed_goalw "monofun_Isinl" thy [monofun] "monofun(Isinl)"
(fn prems =>
[
(strip_tac 1),
(etac (less_ssum3a RS iffD2) 1)
]);
-qed_goalw "monofun_Isinr" Ssum2.thy [monofun] "monofun(Isinr)"
+qed_goalw "monofun_Isinr" thy [monofun] "monofun(Isinr)"
(fn prems =>
[
(strip_tac 1),
@@ -87,7 +98,7 @@
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_Iwhen1" Ssum2.thy [monofun] "monofun(Iwhen)"
+qed_goalw "monofun_Iwhen1" thy [monofun] "monofun(Iwhen)"
(fn prems =>
[
(strip_tac 1),
@@ -103,7 +114,7 @@
(asm_simp_tac Ssum0_ss 1)
]);
-qed_goalw "monofun_Iwhen2" Ssum2.thy [monofun] "monofun(Iwhen(f))"
+qed_goalw "monofun_Iwhen2" thy [monofun] "monofun(Iwhen(f))"
(fn prems =>
[
(strip_tac 1),
@@ -117,7 +128,7 @@
(etac monofun_cfun_fun 1)
]);
-qed_goalw "monofun_Iwhen3" Ssum2.thy [monofun] "monofun(Iwhen(f)(g))"
+qed_goalw "monofun_Iwhen3" thy [monofun] "monofun(Iwhen(f)(g))"
(fn prems =>
[
(strip_tac 1),
@@ -158,14 +169,11 @@
]);
-
-
(* ------------------------------------------------------------------------ *)
(* some kind of exhaustion rules for chains in 'a ++ 'b *)
(* ------------------------------------------------------------------------ *)
-
-qed_goal "ssum_lemma1" Ssum2.thy
+qed_goal "ssum_lemma1" thy
"[|~(!i.? x.Y(i::nat)=Isinl(x))|] ==> (? i.! x.Y(i)~=Isinl(x))"
(fn prems =>
[
@@ -173,7 +181,7 @@
(fast_tac HOL_cs 1)
]);
-qed_goal "ssum_lemma2" Ssum2.thy
+qed_goal "ssum_lemma2" thy
"[|(? i.!x.(Y::nat => 'a++'b)(i::nat)~=Isinl(x::'a))|] ==>\
\ (? i y. (Y::nat => 'a++'b)(i::nat)=Isinr(y::'b) & y~=UU)"
(fn prems =>
@@ -189,7 +197,7 @@
]);
-qed_goal "ssum_lemma3" Ssum2.thy
+qed_goal "ssum_lemma3" thy
"[|is_chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
\ (!i.? y.Y(i)=Isinr(y))"
(fn prems =>
@@ -222,7 +230,7 @@
(atac 1)
]);
-qed_goal "ssum_lemma4" Ssum2.thy
+qed_goal "ssum_lemma4" thy
"is_chain(Y) ==> (!i.? x.Y(i)=Isinl(x))|(!i.? y.Y(i)=Isinr(y))"
(fn prems =>
[
@@ -240,7 +248,7 @@
(* restricted surjectivity of Isinl *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ssum_lemma5" Ssum2.thy
+qed_goal "ssum_lemma5" thy
"z=Isinl(x)==> Isinl((Iwhen (LAM x.x) (LAM y.UU))(z)) = z"
(fn prems =>
[
@@ -255,7 +263,7 @@
(* restricted surjectivity of Isinr *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ssum_lemma6" Ssum2.thy
+qed_goal "ssum_lemma6" thy
"z=Isinr(x)==> Isinr((Iwhen (LAM y.UU) (LAM x.x))(z)) = z"
(fn prems =>
[
@@ -270,7 +278,7 @@
(* technical lemmas *)
(* ------------------------------------------------------------------------ *)
-qed_goal "ssum_lemma7" Ssum2.thy
+qed_goal "ssum_lemma7" thy
"[|Isinl(x) << z; x~=UU|] ==> ? y.z=Isinl(y) & y~=UU"
(fn prems =>
[
@@ -288,7 +296,7 @@
(atac 1)
]);
-qed_goal "ssum_lemma8" Ssum2.thy
+qed_goal "ssum_lemma8" thy
"[|Isinr(x) << z; x~=UU|] ==> ? y.z=Isinr(y) & y~=UU"
(fn prems =>
[
@@ -308,7 +316,7 @@
(* the type 'a ++ 'b is a cpo in three steps *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_ssum1a" Ssum2.thy
+qed_goal "lub_ssum1a" thy
"[|is_chain(Y);(!i.? x.Y(i)=Isinl(x))|] ==>\
\ range(Y) <<|\
\ Isinl(lub(range(%i.(Iwhen (LAM x.x) (LAM y.UU))(Y i))))"
@@ -349,7 +357,7 @@
]);
-qed_goal "lub_ssum1b" Ssum2.thy
+qed_goal "lub_ssum1b" thy
"[|is_chain(Y);(!i.? x.Y(i)=Isinr(x))|] ==>\
\ range(Y) <<|\
\ Isinr(lub(range(%i.(Iwhen (LAM y.UU) (LAM x.x))(Y i))))"
@@ -404,7 +412,7 @@
(lub (range (%i. Iwhen (LAM y. UU) (LAM x. x) (?Y1 i))))
*)
-qed_goal "cpo_ssum" Ssum2.thy
+qed_goal "cpo_ssum" thy
"is_chain(Y::nat=>'a ++'b) ==> ? x.range(Y) <<|x"
(fn prems =>
[
--- a/src/HOLCF/Ssum2.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Ssum2.thy Mon Feb 17 10:57:11 1997 +0100
@@ -8,14 +8,7 @@
Ssum2 = Ssum1 +
-arities "++" :: (pcpo,pcpo)po
-(* Witness for the above arity axiom is ssum1.ML *)
-
-rules
-
-(* instance of << for type ['a ++ 'b] *)
-
-inst_ssum_po "((op <<)::['a ++ 'b,'a ++ 'b]=>bool) = less_ssum"
+instance "++"::(pcpo,pcpo)po (refl_less_ssum,antisym_less_ssum,trans_less_ssum)
end
--- a/src/HOLCF/Ssum3.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Ssum3.ML Mon Feb 17 10:57:11 1997 +0100
@@ -8,11 +8,17 @@
open Ssum3;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_ssum_pcpo" thy "UU = Isinl UU"
+ (fn prems =>
+ [
+ (simp_tac (HOL_ss addsimps [UU_def,UU_ssum_def]) 1)
+ ]);
+
(* ------------------------------------------------------------------------ *)
(* continuity for Isinl and Isinr *)
(* ------------------------------------------------------------------------ *)
-
qed_goal "contlub_Isinl" Ssum3.thy "contlub(Isinl)"
(fn prems =>
[
--- a/src/HOLCF/Ssum3.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Ssum3.thy Mon Feb 17 10:57:11 1997 +0100
@@ -8,18 +8,13 @@
Ssum3 = Ssum2 +
-arities "++" :: (pcpo,pcpo)pcpo (* Witness ssum2.ML *)
+instance "++" :: (pcpo,pcpo)pcpo (least_ssum,cpo_ssum)
consts
sinl :: "'a -> ('a++'b)"
sinr :: "'b -> ('a++'b)"
sswhen :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
-rules
-
-inst_ssum_pcpo "(UU::'a++'b) = Isinl(UU)"
-
-
defs
sinl_def "sinl == (LAM x.Isinl(x))"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tr.ML Mon Feb 17 10:57:11 1997 +0100
@@ -0,0 +1,187 @@
+(* Title: HOLCF/Tr.ML
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
+
+Lemmas for Tr.thy
+*)
+
+open Tr;
+
+(* ------------------------------------------------------------------------ *)
+(* Exhaustion and Elimination for type one *)
+(* ------------------------------------------------------------------------ *)
+qed_goalw "Exh_tr" thy [FF_def,TT_def] "t=UU | t = TT | t = FF"
+ (fn prems =>
+ [
+ (lift.induct_tac "t" 1),
+ (fast_tac HOL_cs 1),
+ (fast_tac (HOL_cs addss !simpset) 1)
+ ]);
+
+qed_goal "trE" thy
+ "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
+ (fn prems =>
+ [
+ (rtac (Exh_tr RS disjE) 1),
+ (eresolve_tac prems 1),
+ (etac disjE 1),
+ (eresolve_tac prems 1),
+ (eresolve_tac prems 1)
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* tactic for tr-thms with case split *)
+(* ------------------------------------------------------------------------ *)
+
+val tr_defs = [andalso_def,orelse_def,neg_def,ifte_def,TT_def,FF_def];
+
+fun prover t = prove_goal thy t
+ (fn prems =>
+ [
+ (res_inst_tac [("p","y")] trE 1),
+ (REPEAT(asm_simp_tac (!simpset addsimps
+ [o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* distinctness for type tr *)
+(* ------------------------------------------------------------------------ *)
+
+val dist_less_tr = map prover [
+ "~TT << UU",
+ "~FF << UU",
+ "~TT << FF",
+ "~FF << TT"
+ ];
+
+val dist_eq_tr = map prover ["TT~=UU","FF~=UU","TT~=FF"];
+val dist_eq_tr = dist_eq_tr @ (map (fn thm => (thm RS not_sym)) dist_eq_tr);
+
+(* ------------------------------------------------------------------------ *)
+(* lemmas about andalso, orelse, neg and if *)
+(* ------------------------------------------------------------------------ *)
+
+val andalso_thms = map prover [
+ "(TT andalso y) = y",
+ "(FF andalso y) = FF",
+ "(UU andalso y) = UU",
+ "(y andalso TT) = y",
+ "(y andalso y) = y"
+ ];
+
+val orelse_thms = map prover [
+ "(TT orelse y) = TT",
+ "(FF orelse y) = y",
+ "(UU orelse y) = UU",
+ "(y orelse FF) = y",
+ "(y orelse y) = y"];
+
+val neg_thms = map prover [
+ "neg`TT = FF",
+ "neg`FF = TT",
+ "neg`UU = UU"
+ ];
+
+val ifte_thms = map prover [
+ "If UU then e1 else e2 fi = UU",
+ "If FF then e1 else e2 fi = e2",
+ "If TT then e1 else e2 fi = e1"];
+
+Addsimps (dist_less_tr @ dist_eq_tr @ andalso_thms @
+ orelse_thms @ neg_thms @ ifte_thms);
+
+
+
+(* --------------------------------------------------------- *)
+(* Theroems for the liftings *)
+(* --------------------------------------------------------- *)
+
+
+(* --------------------------------------------------------- *)
+(* Admissibility tactic and tricks *)
+(* --------------------------------------------------------- *)
+
+
+goal thy "x~=FF = (x=TT|x=UU)";
+by (res_inst_tac [("p","x")] trE 1);
+ by (TRYALL (Asm_full_simp_tac));
+qed"adm_trick_1";
+
+goal thy "x~=TT = (x=FF|x=UU)";
+by (res_inst_tac [("p","x")] trE 1);
+ by (TRYALL (Asm_full_simp_tac));
+qed"adm_trick_2";
+
+val adm_tricks = [adm_trick_1,adm_trick_2];
+
+(*val adm_tac = (fn i => ((resolve_tac adm_lemmas i)));*)
+(*val adm_tacR = (fn i => (REPEAT (adm_tac i)));*)
+(*val adm_cont_tac = (fn i => ((adm_tacR i) THEN (cont_tacR i)));*)
+
+(* ----------------------------------------------------------------- *)
+(* Relations between domains and terms using lift constructs *)
+(* ----------------------------------------------------------------- *)
+
+goal thy "!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
+by (rtac iffI 1);
+(* 1 *)
+by (res_inst_tac [("p","t")] trE 1);
+by (fast_tac HOL_cs 1);
+by (res_inst_tac [("p","s")] trE 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "(t andalso s) = FF" 1);
+by (fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+by (res_inst_tac [("p","s")] trE 1);
+by (subgoal_tac "(t andalso s) = FF" 1);
+by (fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "(t andalso s) = FF" 1);
+by (fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "(t andalso s) = FF" 1);
+by (fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+(* 2*)
+by (res_inst_tac [("p","t")] trE 1);
+by (fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac HOL_cs 1);
+qed"andalso_and";
+
+goal thy "Def x ~=UU";
+by (Simp_tac 1);
+qed"blift_not_UU";
+
+goal thy "(Def x ~=FF)= x";
+by (simp_tac (!simpset addsimps [FF_def]) 1);
+qed"blift_and_bool";
+
+goal thy "(Def x = TT) = x";
+by (simp_tac (!simpset addsimps [TT_def]) 1);
+qed"blift_and_bool2";
+
+goal thy "(Def x = FF) = (~x)";
+by (simp_tac (!simpset addsimps [FF_def]) 1);
+by (fast_tac HOL_cs 1);
+qed"blift_and_bool3";
+
+goal thy "plift P`(Def y) = Def (P y)";
+by (simp_tac (!simpset addsimps [plift_def,flift1_def]) 1);
+qed"plift2blift";
+
+goal thy
+ "(If Def P then A else B fi)= (if P then A else B)";
+by (res_inst_tac [("p","Def P")] trE 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps tr_defs@[flift1_def,o_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps tr_defs@[flift1_def,o_def]) 1);
+qed"If_and_if";
+
+Addsimps [plift2blift,If_and_if,blift_not_UU,
+ blift_and_bool,blift_and_bool2,blift_and_bool3];
+
+simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tr.thy Mon Feb 17 10:57:11 1997 +0100
@@ -0,0 +1,54 @@
+(* Title: HOLCF/Tr.thy
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
+
+Introduce infix if_then_else_fi and boolean connectives andalso, orelse
+*)
+
+Tr = Lift +
+
+types tr = "bool lift"
+
+consts
+ TT,FF :: "tr"
+ Icifte :: "tr -> 'c -> 'c -> 'c"
+ trand :: "tr -> tr -> tr"
+ tror :: "tr -> tr -> tr"
+ neg :: "tr -> tr"
+ plift :: "('a => bool) => 'a lift -> tr"
+
+syntax "@cifte" :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
+ "@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
+ "@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30)
+
+translations
+ "tr" ==(type) "bool lift"
+ "x andalso y" == "trand`x`y"
+ "x orelse y" == "tror`x`y"
+ "If b then e1 else e2 fi" == "Icifte`b`e1`e2"
+defs
+ TT_def "TT==Def True"
+ FF_def "FF==Def False"
+ neg_def "neg == flift2 not"
+ ifte_def "Icifte == (LAM b t e.flift1(%b.if b then t else e)`b)"
+ andalso_def "trand == (LAM x y.If x then y else FF fi)"
+ orelse_def "tror == (LAM x y.If x then TT else y fi)"
+(* andalso, orelse are different from strict functions
+ andalso_def "trand == flift1(flift2 o (op &))"
+ orelse_def "tror == flift1(flift2 o (op |))"
+*)
+ plift_def "plift p == (LAM x. flift1(%a.Def(p a))`x)"
+
+(* start 8bit 1 *)
+syntax
+ "GeqTT" :: "tr => bool" ("(\\<lceil>_\\<rceil>)")
+ "GeqFF" :: "tr => bool" ("(\\<lfloor>_\\<rfloor>)")
+
+translations
+ "\\<lceil>x\\<rceil>" == "x = TT"
+ "\\<lfloor>x\\<rfloor>" == "x = FF"
+(* end 8bit 1 *)
+
+end
+
--- a/src/HOLCF/Tr1.ML Sat Feb 15 18:24:05 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,159 +0,0 @@
-(* Title: HOLCF/tr1.ML
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Lemmas for tr1.thy
-*)
-
-open Tr1;
-
-(* -------------------------------------------------------------------------- *)
-(* distinctness for type tr *)
-(* -------------------------------------------------------------------------- *)
-
-val dist_less_tr = [
-prove_goalw Tr1.thy [TT_def] "~TT << UU"
- (fn prems =>
- [
- (rtac classical2 1),
- (rtac defined_sinl 1),
- (rtac not_less2not_eq 1),
- (rtac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2) 1),
- (etac (eq_UU_iff RS ssubst) 1)
- ]),
-prove_goalw Tr1.thy [FF_def] "~FF << UU"
- (fn prems =>
- [
- (rtac classical2 1),
- (rtac defined_sinr 1),
- (rtac not_less2not_eq 1),
- (rtac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2) 1),
- (etac (eq_UU_iff RS ssubst) 1)
- ]),
-prove_goalw Tr1.thy [FF_def,TT_def] "~TT << FF"
- (fn prems =>
- [
- (rtac classical2 1),
- (rtac (less_ssum4c RS iffD1) 2),
- (rtac not_less2not_eq 1),
- (rtac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (etac monofun_cfun_arg 1)
- ]),
-prove_goalw Tr1.thy [FF_def,TT_def] "~FF << TT"
- (fn prems =>
- [
- (rtac classical2 1),
- (rtac (less_ssum4d RS iffD1) 2),
- (rtac not_less2not_eq 1),
- (rtac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (etac monofun_cfun_arg 1)
- ])
-];
-
-fun prover s = prove_goal Tr1.thy s
- (fn prems =>
- [
- (rtac not_less2not_eq 1),
- (resolve_tac dist_less_tr 1)
- ]);
-
-val dist_eq_tr = map prover ["TT~=UU","FF~=UU","TT~=FF"];
-val dist_eq_tr = dist_eq_tr @ (map (fn thm => (thm RS not_sym)) dist_eq_tr);
-
-(* ------------------------------------------------------------------------ *)
-(* Exhaustion and elimination for type tr *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "Exh_tr" Tr1.thy [FF_def,TT_def] "t=UU | t = TT | t = FF"
- (fn prems =>
- [
- (res_inst_tac [("p","rep_tr`t")] ssumE 1),
- (rtac disjI1 1),
- (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict )
- RS conjunct2 RS subst) 1),
- (rtac (abs_tr_iso RS subst) 1),
- (etac cfun_arg_cong 1),
- (rtac disjI2 1),
- (rtac disjI1 1),
- (rtac (abs_tr_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (etac trans 1),
- (rtac cfun_arg_cong 1),
- (rtac (Exh_one RS disjE) 1),
- (contr_tac 1),
- (atac 1),
- (rtac disjI2 1),
- (rtac disjI2 1),
- (rtac (abs_tr_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (etac trans 1),
- (rtac cfun_arg_cong 1),
- (rtac (Exh_one RS disjE) 1),
- (contr_tac 1),
- (atac 1)
- ]);
-
-
-qed_goal "trE" Tr1.thy
- "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
- (fn prems =>
- [
- (rtac (Exh_tr RS disjE) 1),
- (eresolve_tac prems 1),
- (etac disjE 1),
- (eresolve_tac prems 1),
- (eresolve_tac prems 1)
- ]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* type tr is flat *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "flat_tr" Tr1.thy [flat_def] "flat TT"
- (fn prems =>
- [
- (rtac allI 1),
- (rtac allI 1),
- (res_inst_tac [("p","x")] trE 1),
- (Asm_simp_tac 1),
- (res_inst_tac [("p","y")] trE 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
- (res_inst_tac [("p","y")] trE 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1)
- ]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* properties of tr_when *)
-(* ------------------------------------------------------------------------ *)
-
-fun prover s = prove_goalw Tr1.thy [tr_when_def,TT_def,FF_def] s (fn prems => [
- (Simp_tac 1),
- (simp_tac (!simpset addsimps [rep_tr_iso,
- (abs_tr_iso RS allI) RS ((rep_tr_iso RS allI)
- RS iso_strict) RS conjunct1]) 1)]);
-
-val tr_when = map prover [
- "tr_when`x`y`UU = UU",
- "tr_when`x`y`TT = x",
- "tr_when`x`y`FF = y"
- ];
-
--- a/src/HOLCF/Tr1.thy Sat Feb 15 18:24:05 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(* Title: HOLCF/tr1.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Introduce the domain of truth values tr = one ++ one
-
-The type is axiomatized as the least solution of a domain equation.
-The functor term that specifies the domain equation is:
-
- FT = <++,K_{one},K_{one}>
-
-For details see chapter 5 of:
-
-[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
- Dissertation, Technische Universit"at M"unchen, 1994
-
-*)
-
-Tr1 = One +
-
-types tr 0
-arities tr :: pcpo
-
-consts
- abs_tr :: "one ++ one -> tr"
- rep_tr :: "tr -> one ++ one"
- TT :: "tr"
- FF :: "tr"
- tr_when :: "'c -> 'c -> tr -> 'c"
-
-rules
-
- abs_tr_iso "abs_tr`(rep_tr`u) = u"
- rep_tr_iso "rep_tr`(abs_tr`x) = x"
-
-defs
-
- TT_def "TT == abs_tr`(sinl`one)"
- FF_def "FF == abs_tr`(sinr`one)"
-
- tr_when_def "tr_when ==
- (LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))"
-
-end
--- a/src/HOLCF/Tr2.ML Sat Feb 15 18:24:05 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(* Title: HOLCF/tr2.ML
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Lemmas for Tr2.thy
-*)
-
-open Tr2;
-
-(* ------------------------------------------------------------------------ *)
-(* lemmas about andalso *)
-(* ------------------------------------------------------------------------ *)
-
-fun prover s = prove_goalw Tr2.thy [andalso_def] s
- (fn prems =>
- [
- (simp_tac (!simpset addsimps tr_when) 1)
- ]);
-
-val andalso_thms = map prover [
- "(TT andalso y) = y",
- "(FF andalso y) = FF",
- "(UU andalso y) = UU"
- ];
-
-val andalso_thms = andalso_thms @
- [prove_goalw Tr2.thy [andalso_def] "(x andalso TT) = x"
- (fn prems =>
- [
- (res_inst_tac [("p","x")] trE 1),
- (asm_simp_tac (!simpset addsimps tr_when) 1),
- (asm_simp_tac (!simpset addsimps tr_when) 1),
- (asm_simp_tac (!simpset addsimps tr_when) 1)
- ])];
-
-(* ------------------------------------------------------------------------ *)
-(* lemmas about orelse *)
-(* ------------------------------------------------------------------------ *)
-
-fun prover s = prove_goalw Tr2.thy [orelse_def] s
- (fn prems =>
- [
- (simp_tac (!simpset addsimps tr_when) 1)
- ]);
-
-val orelse_thms = map prover [
- "(TT orelse y) = TT",
- "(FF orelse y) = y",
- "(UU orelse y) = UU"
- ];
-
-val orelse_thms = orelse_thms @
- [prove_goalw Tr2.thy [orelse_def] "(x orelse FF) = x"
- (fn prems =>
- [
- (res_inst_tac [("p","x")] trE 1),
- (asm_simp_tac (!simpset addsimps tr_when) 1),
- (asm_simp_tac (!simpset addsimps tr_when) 1),
- (asm_simp_tac (!simpset addsimps tr_when) 1)
- ])];
-
-
-(* ------------------------------------------------------------------------ *)
-(* lemmas about neg *)
-(* ------------------------------------------------------------------------ *)
-
-fun prover s = prove_goalw Tr2.thy [neg_def] s
- (fn prems =>
- [
- (simp_tac (!simpset addsimps tr_when) 1)
- ]);
-
-val neg_thms = map prover [
- "neg`TT = FF",
- "neg`FF = TT",
- "neg`UU = UU"
- ];
-
-(* ------------------------------------------------------------------------ *)
-(* lemmas about If_then_else_fi *)
-(* ------------------------------------------------------------------------ *)
-
-fun prover s = prove_goalw Tr2.thy [ifte_def] s
- (fn prems =>
- [
- (simp_tac (!simpset addsimps tr_when) 1)
- ]);
-
-val ifte_thms = map prover [
- "If UU then e1 else e2 fi = UU",
- "If FF then e1 else e2 fi = e2",
- "If TT then e1 else e2 fi = e1"];
-
-Addsimps (dist_less_tr @ dist_eq_tr @ tr_when @ andalso_thms @
- orelse_thms @ neg_thms @ ifte_thms);
-
-
-
--- a/src/HOLCF/Tr2.thy Sat Feb 15 18:24:05 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: HOLCF/tr2.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Introduce infix if_then_else_fi and boolean connectives andalso, orelse
-*)
-
-Tr2 = Tr1 +
-
-consts
- Icifte :: "tr -> 'c -> 'c -> 'c"
- trand :: "tr -> tr -> tr"
- tror :: "tr -> tr -> tr"
- neg :: "tr -> tr"
-
-syntax "@cifte" :: "tr=>'c=>'c=>'c"
- ("(3If _/ (then _/ else _) fi)" 60)
- "@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
- "@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30)
-
-translations "x andalso y" == "trand`x`y"
- "x orelse y" == "tror`x`y"
- "If b then e1 else e2 fi" == "Icifte`b`e1`e2"
-
-defs
-
- ifte_def "Icifte == (LAM t e1 e2.tr_when`e1`e2`t)"
- andalso_def "trand == (LAM t1 t2.tr_when`t2`FF`t1)"
- orelse_def "tror == (LAM t1 t2.tr_when`TT`t2`t1)"
- neg_def "neg == (LAM t. tr_when`FF`TT`t)"
-
-end
--- 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),
--- a/src/HOLCF/Up1.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Up1.thy Mon Feb 17 10:57:11 1997 +0100
@@ -12,40 +12,17 @@
(* new type for lifting *)
-types "u" 1
-
-arities "u" :: (pcpo)term
+typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
consts
-
- Rep_Up :: "('a)u => (void + 'a)"
- Abs_Up :: "(void + 'a) => ('a)u"
-
Iup :: "'a => ('a)u"
- UU_up :: "('a)u"
Ifup :: "('a->'b)=>('a)u => 'b"
- less_up :: "('a)u => ('a)u => bool"
-
-rules
-
- (*faking a type definition... *)
- (* ('a)u is isomorphic to void + 'a *)
-
- Rep_Up_inverse "Abs_Up(Rep_Up(p)) = p"
- Abs_Up_inverse "Rep_Up(Abs_Up(p)) = p"
-
- (*defining the abstract constants*)
defs
-
- UU_up_def "UU_up == Abs_Up(Inl(UU))"
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_up(x1)(x2) == (case Rep_Up(x1) of
+ less_up_def "less == (%x1 x2.case Rep_Up(x1) of
Inl(y1) => True
| Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False
| Inr(z2) => y2<<z2))"
-
end
--- a/src/HOLCF/Up2.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Up2.ML Mon Feb 17 10:57:11 1997 +0100
@@ -3,52 +3,69 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for up2.thy
+Lemmas for Up2.thy
*)
open Up2;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_up_po" thy "(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))"
+ (fn prems =>
+ [
+ (fold_goals_tac [po_def,less_up_def]),
+ (rtac refl 1)
+ ]);
+
(* -------------------------------------------------------------------------*)
(* type ('a)u is pointed *)
(* ------------------------------------------------------------------------ *)
-qed_goal "minimal_up" Up2.thy "UU_up << z"
+qed_goal "minimal_up" thy "Abs_Up(Inl ()) << z"
(fn prems =>
[
- (stac inst_up_po 1),
- (rtac less_up1a 1)
+ (simp_tac (!simpset addsimps [po_def,less_up1a]) 1)
+ ]);
+
+bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
+
+qed_goal "least_up" thy "? x::'a u.!y.x<<y"
+(fn prems =>
+ [
+ (res_inst_tac [("x","Abs_Up(Inl ())")] exI 1),
+ (rtac (minimal_up RS allI) 1)
]);
(* -------------------------------------------------------------------------*)
(* access to less_up in class po *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_up2b" Up2.thy "~ Iup(x) << UU_up"
+qed_goal "less_up2b" thy "~ Iup(x) << Abs_Up(Inl ())"
(fn prems =>
[
- (stac inst_up_po 1),
- (rtac less_up1b 1)
+ (simp_tac (!simpset addsimps [po_def,less_up1b]) 1)
]);
-qed_goal "less_up2c" Up2.thy "(Iup(x)<<Iup(y)) = (x<<y)"
+qed_goal "less_up2c" thy "(Iup(x)<<Iup(y)) = (x<<y)"
(fn prems =>
[
- (stac inst_up_po 1),
- (rtac less_up1c 1)
+ (simp_tac (!simpset addsimps [po_def,less_up1c]) 1)
]);
(* ------------------------------------------------------------------------ *)
(* Iup and Ifup are monotone *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_Iup" Up2.thy [monofun] "monofun(Iup)"
+qed_goalw "monofun_Iup" thy [monofun] "monofun(Iup)"
(fn prems =>
[
(strip_tac 1),
(etac (less_up2c RS iffD2) 1)
]);
-qed_goalw "monofun_Ifup1" Up2.thy [monofun] "monofun(Ifup)"
+qed_goalw "monofun_Ifup1" thy [monofun] "monofun(Ifup)"
(fn prems =>
[
(strip_tac 1),
@@ -60,7 +77,7 @@
(etac monofun_cfun_fun 1)
]);
-qed_goalw "monofun_Ifup2" Up2.thy [monofun] "monofun(Ifup(f))"
+qed_goalw "monofun_Ifup2" thy [monofun] "monofun(Ifup(f))"
(fn prems =>
[
(strip_tac 1),
@@ -82,8 +99,7 @@
(* Some kind of surjectivity lemma *)
(* ------------------------------------------------------------------------ *)
-
-qed_goal "up_lemma1" Up2.thy "z=Iup(x) ==> Iup(Ifup(LAM x.x)(z)) = z"
+qed_goal "up_lemma1" thy "z=Iup(x) ==> Iup(Ifup(LAM x.x)(z)) = z"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -94,7 +110,7 @@
(* ('a)u is a cpo *)
(* ------------------------------------------------------------------------ *)
-qed_goal "lub_up1a" Up2.thy
+qed_goal "lub_up1a" thy
"[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\
\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x.x) (Y(i))))))"
(fn prems =>
@@ -105,7 +121,7 @@
(rtac ub_rangeI 1),
(rtac allI 1),
(res_inst_tac [("p","Y(i)")] upE 1),
- (res_inst_tac [("s","UU_up"),("t","Y(i)")] subst 1),
+ (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] subst 1),
(etac sym 1),
(rtac minimal_up 1),
(res_inst_tac [("t","Y(i)")] (up_lemma1 RS subst) 1),
@@ -117,7 +133,7 @@
(res_inst_tac [("p","u")] upE 1),
(etac exE 1),
(etac exE 1),
- (res_inst_tac [("P","Y(i)<<UU_up")] notE 1),
+ (res_inst_tac [("P","Y(i)<<Abs_Up (Inl ())")] notE 1),
(res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
(atac 1),
(rtac less_up2b 1),
@@ -131,9 +147,9 @@
(etac (monofun_Ifup2 RS ub2ub_monofun) 1)
]);
-qed_goal "lub_up1b" Up2.thy
+qed_goal "lub_up1b" thy
"[|is_chain(Y);!i x. Y(i)~=Iup(x)|] ==>\
-\ range(Y) <<| UU_up"
+\ range(Y) <<| Abs_Up (Inl ())"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -142,7 +158,7 @@
(rtac ub_rangeI 1),
(rtac allI 1),
(res_inst_tac [("p","Y(i)")] upE 1),
- (res_inst_tac [("s","UU_up"),("t","Y(i)")] ssubst 1),
+ (res_inst_tac [("s","Abs_Up (Inl ())"),("t","Y(i)")] ssubst 1),
(atac 1),
(rtac refl_less 1),
(rtac notE 1),
@@ -166,7 +182,7 @@
lub (range ?Y1) = UU_up
*)
-qed_goal "cpo_up" Up2.thy
+qed_goal "cpo_up" thy
"is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x"
(fn prems =>
[
--- a/src/HOLCF/Up2.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Up2.thy Mon Feb 17 10:57:11 1997 +0100
@@ -9,15 +9,7 @@
Up2 = Up1 +
-(* Witness for the above arity axiom is up1.ML *)
-
-arities "u" :: (pcpo)po
-
-rules
-
-(* instance of << for type ('a)u *)
-
-inst_up_po "((op <<)::[('a)u,('a)u]=>bool) = less_up"
+instance u :: (pcpo)po (refl_less_up,antisym_less_up,trans_less_up)
end
--- a/src/HOLCF/Up3.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Up3.ML Mon Feb 17 10:57:11 1997 +0100
@@ -8,18 +8,25 @@
open Up3;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_up_pcpo" thy "UU = Abs_Up(Inl ())"
+ (fn prems =>
+ [
+ (simp_tac (HOL_ss addsimps [UU_def,UU_up_def]) 1)
+ ]);
+
(* -------------------------------------------------------------------------*)
(* some lemmas restated for class pcpo *)
(* ------------------------------------------------------------------------ *)
-qed_goal "less_up3b" Up3.thy "~ Iup(x) << UU"
+qed_goal "less_up3b" thy "~ Iup(x) << UU"
(fn prems =>
[
(stac inst_up_pcpo 1),
(rtac less_up2b 1)
]);
-qed_goal "defined_Iup2" Up3.thy "Iup(x) ~= UU"
+qed_goal "defined_Iup2" thy "Iup(x) ~= UU"
(fn prems =>
[
(stac inst_up_pcpo 1),
@@ -30,7 +37,7 @@
(* continuity for Iup *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_Iup" Up3.thy "contlub(Iup)"
+qed_goal "contlub_Iup" thy "contlub(Iup)"
(fn prems =>
[
(rtac contlubI 1),
@@ -47,7 +54,7 @@
(asm_simp_tac Up0_ss 1)
]);
-qed_goal "cont_Iup" Up3.thy "cont(Iup)"
+qed_goal "cont_Iup" thy "cont(Iup)"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -60,7 +67,7 @@
(* continuity for Ifup *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_Ifup1" Up3.thy "contlub(Ifup)"
+qed_goal "contlub_Ifup1" thy "contlub(Ifup)"
(fn prems =>
[
(rtac contlubI 1),
@@ -77,7 +84,7 @@
]);
-qed_goal "contlub_Ifup2" Up3.thy "contlub(Ifup(f))"
+qed_goal "contlub_Ifup2" thy "contlub(Ifup(f))"
(fn prems =>
[
(rtac contlubI 1),
@@ -124,7 +131,7 @@
(atac 1)
]);
-qed_goal "cont_Ifup1" Up3.thy "cont(Ifup)"
+qed_goal "cont_Ifup1" thy "cont(Ifup)"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -132,7 +139,7 @@
(rtac contlub_Ifup1 1)
]);
-qed_goal "cont_Ifup2" Up3.thy "cont(Ifup(f))"
+qed_goal "cont_Ifup2" thy "cont(Ifup(f))"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -145,7 +152,7 @@
(* continuous versions of lemmas for ('a)u *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "Exh_Up1" Up3.thy [up_def] "z = UU | (? x. z = up`x)"
+qed_goalw "Exh_Up1" thy [up_def] "z = UU | (? x. z = up`x)"
(fn prems =>
[
(simp_tac (Up0_ss addsimps [cont_Iup]) 1),
@@ -153,7 +160,7 @@
(rtac Exh_Up 1)
]);
-qed_goalw "inject_up" Up3.thy [up_def] "up`x=up`y ==> x=y"
+qed_goalw "inject_up" thy [up_def] "up`x=up`y ==> x=y"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -163,14 +170,14 @@
(simp_tac (Up0_ss addsimps [cont_Iup]) 1)
]);
-qed_goalw "defined_up" Up3.thy [up_def] " up`x ~= UU"
+qed_goalw "defined_up" thy [up_def] " up`x ~= UU"
(fn prems =>
[
(simp_tac (Up0_ss addsimps [cont_Iup]) 1),
(rtac defined_Iup2 1)
]);
-qed_goalw "upE1" Up3.thy [up_def]
+qed_goalw "upE1" thy [up_def]
"[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q"
(fn prems =>
[
@@ -184,7 +191,7 @@
val tac = (simp_tac (!simpset addsimps [cont_Iup,cont_Ifup1,
cont_Ifup2,cont2cont_CF1L]) 1);
-qed_goalw "fup1" Up3.thy [up_def,fup_def] "fup`f`UU=UU"
+qed_goalw "fup1" thy [up_def,fup_def] "fup`f`UU=UU"
(fn prems =>
[
(stac inst_up_pcpo 1),
@@ -195,7 +202,7 @@
(simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1)
]);
-qed_goalw "fup2" Up3.thy [up_def,fup_def] "fup`f`(up`x)=f`x"
+qed_goalw "fup2" thy [up_def,fup_def] "fup`f`(up`x)=f`x"
(fn prems =>
[
(stac beta_cfun 1),
@@ -207,14 +214,14 @@
(simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1)
]);
-qed_goalw "less_up4b" Up3.thy [up_def,fup_def] "~ up`x << UU"
+qed_goalw "less_up4b" thy [up_def,fup_def] "~ up`x << UU"
(fn prems =>
[
(simp_tac (Up0_ss addsimps [cont_Iup]) 1),
(rtac less_up3b 1)
]);
-qed_goalw "less_up4c" Up3.thy [up_def,fup_def]
+qed_goalw "less_up4c" thy [up_def,fup_def]
"(up`x << up`y) = (x<<y)"
(fn prems =>
[
@@ -222,7 +229,7 @@
(rtac less_up2c 1)
]);
-qed_goalw "thelub_up2a" Up3.thy [up_def,fup_def]
+qed_goalw "thelub_up2a" thy [up_def,fup_def]
"[| is_chain(Y); ? i x. Y(i) = up`x |] ==>\
\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
(fn prems =>
@@ -247,7 +254,7 @@
-qed_goalw "thelub_up2b" Up3.thy [up_def,fup_def]
+qed_goalw "thelub_up2b" thy [up_def,fup_def]
"[| is_chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"
(fn prems =>
[
@@ -267,7 +274,7 @@
]);
-qed_goal "up_lemma2" Up3.thy " (? x.z = up`x) = (z~=UU)"
+qed_goal "up_lemma2" thy " (? x.z = up`x) = (z~=UU)"
(fn prems =>
[
(rtac iffI 1),
@@ -281,7 +288,7 @@
]);
-qed_goal "thelub_up2a_rev" Up3.thy
+qed_goal "thelub_up2a_rev" thy
"[| is_chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x"
(fn prems =>
[
@@ -295,7 +302,7 @@
(atac 1)
]);
-qed_goal "thelub_up2b_rev" Up3.thy
+qed_goal "thelub_up2b_rev" thy
"[| is_chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x"
(fn prems =>
[
@@ -308,7 +315,7 @@
]);
-qed_goal "thelub_up3" Up3.thy
+qed_goal "thelub_up3" thy
"is_chain(Y) ==> lub(range(Y)) = UU |\
\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x.x)`(Y i))))"
(fn prems =>
@@ -326,7 +333,7 @@
(fast_tac HOL_cs 1)
]);
-qed_goal "fup3" Up3.thy "fup`up`x=x"
+qed_goal "fup3" thy "fup`up`x=x"
(fn prems =>
[
(res_inst_tac [("p","x")] upE1 1),
--- a/src/HOLCF/Up3.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Up3.thy Mon Feb 17 10:57:11 1997 +0100
@@ -10,22 +10,15 @@
Up3 = Up2 +
-arities "u" :: (pcpo)pcpo (* Witness up2.ML *)
-
-consts
- up :: "'a -> ('a)u"
- fup :: "('a->'c)-> ('a)u -> 'c"
+instance u :: (pcpo)pcpo (least_up,cpo_up)
-rules
-
- inst_up_pcpo "(UU::('a)u) = UU_up"
-
-defs
- up_def "up == (LAM x.Iup(x))"
- fup_def "fup == (LAM f p.Ifup(f)(p))"
+constdefs
+ up :: "'a -> ('a)u"
+ "up == (LAM x.Iup(x))"
+ fup :: "('a->'c)-> ('a)u -> 'c"
+ "fup == (LAM f p.Ifup(f)(p))"
translations
-
"case l of up`x => t1" == "fup`(LAM x.t1)`l"
end
--- a/src/HOLCF/Void.ML Sat Feb 15 18:24:05 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(* Title: HOLCF/void.ML
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Lemmas for void.thy.
-
-These lemmas are prototype lemmas for class porder
-see class theory porder.thy
-*)
-
-open Void;
-
-(* ------------------------------------------------------------------------ *)
-(* A non-emptyness result for Void *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "VoidI" Void.thy [UU_void_Rep_def,Void_def]
- " UU_void_Rep : Void"
-(fn prems =>
- [
- (stac mem_Collect_eq 1),
- (rtac refl 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* less_void is a partial ordering on void *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "refl_less_void" Void.thy [ less_void_def ] "less_void x x"
-(fn prems =>
- [
- (fast_tac HOL_cs 1)
- ]);
-
-qed_goalw "antisym_less_void" Void.thy [ less_void_def ]
- "[|less_void x y; less_void y x|] ==> x = y"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac (Rep_Void_inverse RS subst) 1),
- (etac subst 1),
- (rtac (Rep_Void_inverse RS sym) 1)
- ]);
-
-qed_goalw "trans_less_void" Void.thy [ less_void_def ]
- "[|less_void x y; less_void y z|] ==> less_void x z"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (fast_tac HOL_cs 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* a technical lemma about void: *)
-(* every element in void is represented by UU_void_Rep *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "unique_void" Void.thy "Rep_Void(x) = UU_void_Rep"
-(fn prems =>
- [
- (rtac (mem_Collect_eq RS subst) 1),
- (fold_goals_tac [Void_def]),
- (rtac Rep_Void 1)
- ]);
-
-
-
-
--- a/src/HOLCF/Void.thy Sat Feb 15 18:24:05 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-(* Title: HOLCF/void.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Definition of type void with partial order. Void is the prototype for
-all types in class 'po'
-
-Type void is defined as a set Void over type bool.
-*)
-
-Void = Nat +
-
-types void 0
-
-arities void :: term
-
-consts
- Void :: "bool set"
- UU_void_Rep :: "bool"
- Rep_Void :: "void => bool"
- Abs_Void :: "bool => void"
- UU_void :: "void"
- less_void :: "[void,void] => bool"
-
-defs
-
- (* The unique element in Void is False:bool *)
-
- UU_void_Rep_def "UU_void_Rep == False"
- Void_def "Void == {x. x = UU_void_Rep}"
-
- (*defining the abstract constants*)
-
- UU_void_def "UU_void == Abs_Void(UU_void_Rep)"
- less_void_def "less_void x y == (Rep_Void x = Rep_Void y)"
-
-rules
-
- (*faking a type definition... *)
- (* void is isomorphic to Void *)
-
- Rep_Void "Rep_Void(x):Void"
- Rep_Void_inverse "Abs_Void(Rep_Void(x)) = x"
- Abs_Void_inverse "y:Void ==> Rep_Void(Abs_Void(y)) = y"
-
-end
-
-
-
-
--- a/src/HOLCF/ccc1.thy Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/ccc1.thy Mon Feb 17 10:57:11 1997 +0100
@@ -7,7 +7,9 @@
define constants for categorical reasoning
*)
-ccc1 = Cprod3 + Sprod3 + Ssum3 + Up3 + Fix +
+ccc1 = Cprod3 + Sprod3 + Ssum3 + Up3 + Fix +
+
+instance flat<chfin (flat_subclass_chfin)
consts
ID :: "'a -> 'a"