0

1 
(* Title: LCF/lcf.thy


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1992 University of Cambridge


5 


6 
Natural Deduction Rules for LCF


7 
*)


8 


9 
LCF = FOL +


10 


11 
classes cpo < term


12 


13 
default cpo


14 


15 
types tr,void 0


16 
"*" 2 (infixl 6)


17 
"+" 2 (infixl 5)


18 


19 
arities fun, "*", "+" :: (cpo,cpo)cpo


20 
tr,void :: cpo


21 


22 
consts


23 
UU :: "'a"


24 
TT,FF :: "tr"


25 
FIX :: "('a => 'a) => 'a"


26 
FST :: "'a*'b => 'a"


27 
SND :: "'a*'b => 'b"


28 
INL :: "'a => 'a+'b"


29 
INR :: "'b => 'a+'b"


30 
WHEN :: "['a=>'c, 'b=>'c, 'a+'b] => 'c"


31 
adm :: "('a => o) => o"


32 
VOID :: "void" ("()")


33 
PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100)


34 
COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ / _))" [60,60,60] 60)


35 
"<<" :: "['a,'a] => o" (infixl 50)


36 
rules


37 
(** DOMAIN THEORY **)


38 


39 
eq_def "x=y == x << y & y << x"


40 


41 
less_trans "[ x << y; y << z ] ==> x << z"


42 


43 
less_ext "(ALL x. f(x) << g(x)) ==> f << g"


44 


45 
mono "[ f << g; x << y ] ==> f(x) << g(y)"


46 


47 
minimal "UU << x"


48 


49 
FIX_eq "f(FIX(f)) = FIX(f)"


50 


51 
(** TR **)


52 


53 
tr_cases "p=UU  p=TT  p=FF"


54 


55 
not_TT_less_FF "~ TT << FF"


56 
not_FF_less_TT "~ FF << TT"


57 
not_TT_less_UU "~ TT << UU"


58 
not_FF_less_UU "~ FF << UU"


59 


60 
COND_UU "UU => x  y = UU"


61 
COND_TT "TT => x  y = x"


62 
COND_FF "FF => x  y = y"


63 


64 
(** PAIRS **)


65 


66 
surj_pairing "<FST(z),SND(z)> = z"


67 


68 
FST "FST(<x,y>) = x"


69 
SND "SND(<x,y>) = y"


70 


71 
(*** STRICT SUM ***)


72 


73 
INL_DEF "~x=UU ==> ~INL(x)=UU"


74 
INR_DEF "~x=UU ==> ~INR(x)=UU"


75 


76 
INL_STRICT "INL(UU) = UU"


77 
INR_STRICT "INR(UU) = UU"


78 


79 
WHEN_UU "WHEN(f,g,UU) = UU"


80 
WHEN_INL "~x=UU ==> WHEN(f,g,INL(x)) = f(x)"


81 
WHEN_INR "~x=UU ==> WHEN(f,g,INR(x)) = g(x)"


82 


83 
SUM_EXHAUSTION


84 
"z = UU  (EX x. ~x=UU & z = INL(x))  (EX y. ~y=UU & z = INR(y))"


85 


86 
(** VOID **)


87 


88 
void_cases "(x::void) = UU"


89 


90 
(** INDUCTION **)


91 


92 
induct "[ adm(P); P(UU); ALL x. P(x) > P(f(x)) ] ==> P(FIX(f))"


93 


94 
(** Admissibility / Chain Completeness **)


95 
(* All rules can be found on pages 199200 of Larry's LCF book.


96 
Note that "easiness" of types is not taken into account


97 
because it cannot be expressed schematically; flatness could be. *)


98 


99 
adm_less "adm(%x.t(x) << u(x))"


100 
adm_not_less "adm(%x.~ t(x) << u)"


101 
adm_not_free "adm(%x.A)"


102 
adm_subst "adm(P) ==> adm(%x.P(t(x)))"


103 
adm_conj "[ adm(P); adm(Q) ] ==> adm(%x.P(x)&Q(x))"


104 
adm_disj "[ adm(P); adm(Q) ] ==> adm(%x.P(x)Q(x))"


105 
adm_imp "[ adm(%x.~P(x)); adm(Q) ] ==> adm(%x.P(x)>Q(x))"


106 
adm_all "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"


107 
end
