--- a/src/LCF/LCF.thy Mon Feb 05 13:44:28 1996 +0100
+++ b/src/LCF/LCF.thy Mon Feb 05 14:44:09 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: LCF/lcf.thy
+(* Title: LCF/lcf.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1992 University of Cambridge
Natural Deduction Rules for LCF
@@ -15,61 +15,61 @@
types
tr
void
- ('a,'b) "*" (infixl 6)
- ('a,'b) "+" (infixl 5)
+ ('a,'b) "*" (infixl 6)
+ ('a,'b) "+" (infixl 5)
arities
fun, "*", "+" :: (cpo,cpo)cpo
tr,void :: cpo
consts
- UU :: "'a"
- TT,FF :: "tr"
- FIX :: "('a => 'a) => 'a"
- FST :: "'a*'b => 'a"
- SND :: "'a*'b => 'b"
+ UU :: "'a"
+ TT,FF :: "tr"
+ FIX :: "('a => 'a) => 'a"
+ FST :: "'a*'b => 'a"
+ SND :: "'a*'b => 'b"
INL :: "'a => 'a+'b"
INR :: "'b => 'a+'b"
WHEN :: "['a=>'c, 'b=>'c, 'a+'b] => 'c"
- adm :: "('a => o) => o"
- VOID :: "void" ("'(')")
- PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100)
- COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60)
- "<<" :: "['a,'a] => o" (infixl 50)
+ adm :: "('a => o) => o"
+ VOID :: "void" ("'(')")
+ PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100)
+ COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60)
+ "<<" :: "['a,'a] => o" (infixl 50)
rules
(** DOMAIN THEORY **)
- eq_def "x=y == x << y & y << x"
+ eq_def "x=y == x << y & y << x"
- less_trans "[| x << y; y << z |] ==> x << z"
+ less_trans "[| x << y; y << z |] ==> x << z"
- less_ext "(ALL x. f(x) << g(x)) ==> f << g"
+ less_ext "(ALL x. f(x) << g(x)) ==> f << g"
- mono "[| f << g; x << y |] ==> f(x) << g(y)"
+ mono "[| f << g; x << y |] ==> f(x) << g(y)"
- minimal "UU << x"
+ minimal "UU << x"
- FIX_eq "f(FIX(f)) = FIX(f)"
+ FIX_eq "f(FIX(f)) = FIX(f)"
(** TR **)
- tr_cases "p=UU | p=TT | p=FF"
+ tr_cases "p=UU | p=TT | p=FF"
not_TT_less_FF "~ TT << FF"
not_FF_less_TT "~ FF << TT"
not_TT_less_UU "~ TT << UU"
not_FF_less_UU "~ FF << UU"
- COND_UU "UU => x | y = UU"
- COND_TT "TT => x | y = x"
- COND_FF "FF => x | y = y"
+ COND_UU "UU => x | y = UU"
+ COND_TT "TT => x | y = x"
+ COND_FF "FF => x | y = y"
(** PAIRS **)
- surj_pairing "<FST(z),SND(z)> = z"
+ surj_pairing "<FST(z),SND(z)> = z"
- FST "FST(<x,y>) = x"
- SND "SND(<x,y>) = y"
+ FST "FST(<x,y>) = x"
+ SND "SND(<x,y>) = y"
(*** STRICT SUM ***)
@@ -88,23 +88,23 @@
(** VOID **)
- void_cases "(x::void) = UU"
+ void_cases "(x::void) = UU"
(** INDUCTION **)
- induct "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))"
+ induct "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))"
(** Admissibility / Chain Completeness **)
(* All rules can be found on pages 199--200 of Larry's LCF book.
Note that "easiness" of types is not taken into account
because it cannot be expressed schematically; flatness could be. *)
- adm_less "adm(%x.t(x) << u(x))"
- adm_not_less "adm(%x.~ t(x) << u)"
+ adm_less "adm(%x.t(x) << u(x))"
+ adm_not_less "adm(%x.~ t(x) << u)"
adm_not_free "adm(%x.A)"
- adm_subst "adm(P) ==> adm(%x.P(t(x)))"
- adm_conj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
- adm_disj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
- adm_imp "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
- adm_all "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"
+ adm_subst "adm(P) ==> adm(%x.P(t(x)))"
+ adm_conj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
+ adm_disj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
+ adm_imp "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
+ adm_all "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"
end