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 

283

15 
types


16 
tr


17 
void


18 
('a,'b) "*" (infixl 6)


19 
('a,'b) "+" (infixl 5)

0

20 

283

21 
arities


22 
fun, "*", "+" :: (cpo,cpo)cpo


23 
tr,void :: cpo

0

24 


25 
consts


26 
UU :: "'a"


27 
TT,FF :: "tr"


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


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


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


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


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


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


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


35 
VOID :: "void" ("()")


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


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


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


39 
rules


40 
(** DOMAIN THEORY **)


41 


42 
eq_def "x=y == x << y & y << x"


43 


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


45 


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


47 


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


49 


50 
minimal "UU << x"


51 


52 
FIX_eq "f(FIX(f)) = FIX(f)"


53 


54 
(** TR **)


55 


56 
tr_cases "p=UU  p=TT  p=FF"


57 


58 
not_TT_less_FF "~ TT << FF"


59 
not_FF_less_TT "~ FF << TT"


60 
not_TT_less_UU "~ TT << UU"


61 
not_FF_less_UU "~ FF << UU"


62 


63 
COND_UU "UU => x  y = UU"


64 
COND_TT "TT => x  y = x"


65 
COND_FF "FF => x  y = y"


66 


67 
(** PAIRS **)


68 


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


70 


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


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


73 


74 
(*** STRICT SUM ***)


75 


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


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


78 


79 
INL_STRICT "INL(UU) = UU"


80 
INR_STRICT "INR(UU) = UU"


81 


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


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


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


85 


86 
SUM_EXHAUSTION


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


88 


89 
(** VOID **)


90 


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


92 


93 
(** INDUCTION **)


94 


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


96 


97 
(** Admissibility / Chain Completeness **)


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


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


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


101 


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


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


104 
adm_not_free "adm(%x.A)"


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


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


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


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


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


110 
end
