1474

1 
(* Title: LCF/lcf.thy

0

2 
ID: $Id$

1474

3 
Author: Tobias Nipkow

0

4 
Copyright 1992 University of Cambridge


5 
*)


6 

17248

7 
header {* LCF on top of FirstOrder Logic *}

0

8 

17248

9 
theory LCF


10 
imports FOL


11 
uses ("pair.ML") ("fix.ML")


12 
begin

0

13 

17248

14 
text {* This theory is based on Lawrence Paulson's book Logic and Computation. *}

0

15 

17248

16 
subsection {* Natural Deduction Rules for LCF *}


17 


18 
classes cpo < "term"


19 
defaultsort cpo


20 


21 
typedecl tr


22 
typedecl void


23 
typedecl ('a,'b) "*" (infixl 6)


24 
typedecl ('a,'b) "+" (infixl 5)

0

25 

283

26 
arities

17248

27 
fun :: (cpo, cpo) cpo


28 
"*" :: (cpo, cpo) cpo


29 
"+" :: (cpo, cpo) cpo


30 
tr :: cpo


31 
void :: cpo

0

32 


33 
consts

1474

34 
UU :: "'a"

17248

35 
TT :: "tr"


36 
FF :: "tr"

1474

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


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


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

0

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


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


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

1474

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


44 
VOID :: "void" ("'(')")


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


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


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

17248

48 


49 
axioms

0

50 
(** DOMAIN THEORY **)


51 

17248

52 
eq_def: "x=y == x << y & y << x"

0

53 

17248

54 
less_trans: "[ x << y; y << z ] ==> x << z"

0

55 

17248

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

0

57 

17248

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

0

59 

17248

60 
minimal: "UU << x"

0

61 

17248

62 
FIX_eq: "f(FIX(f)) = FIX(f)"

0

63 


64 
(** TR **)


65 

17248

66 
tr_cases: "p=UU  p=TT  p=FF"

0

67 

17248

68 
not_TT_less_FF: "~ TT << FF"


69 
not_FF_less_TT: "~ FF << TT"


70 
not_TT_less_UU: "~ TT << UU"


71 
not_FF_less_UU: "~ FF << UU"

0

72 

17248

73 
COND_UU: "UU => x  y = UU"


74 
COND_TT: "TT => x  y = x"


75 
COND_FF: "FF => x  y = y"

0

76 


77 
(** PAIRS **)


78 

17248

79 
surj_pairing: "<FST(z),SND(z)> = z"

0

80 

17248

81 
FST: "FST(<x,y>) = x"


82 
SND: "SND(<x,y>) = y"

0

83 


84 
(*** STRICT SUM ***)


85 

17248

86 
INL_DEF: "~x=UU ==> ~INL(x)=UU"


87 
INR_DEF: "~x=UU ==> ~INR(x)=UU"

0

88 

17248

89 
INL_STRICT: "INL(UU) = UU"


90 
INR_STRICT: "INR(UU) = UU"

0

91 

17248

92 
WHEN_UU: "WHEN(f,g,UU) = UU"


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


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

0

95 

17248

96 
SUM_EXHAUSTION:

0

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


98 


99 
(** VOID **)


100 

17248

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

0

102 


103 
(** INDUCTION **)


104 

17248

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

0

106 


107 
(** Admissibility / Chain Completeness **)


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


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


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


111 

17248

112 
adm_less: "adm(%x. t(x) << u(x))"


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


114 
adm_not_free: "adm(%x. A)"


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


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


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


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


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


120 


121 
ML {* use_legacy_bindings (the_context ()) *}


122 


123 
use "LCF_lemmas.ML"


124 


125 


126 
subsection {* Ordered pairs and products *}


127 


128 
use "pair.ML"


129 


130 


131 
subsection {* Fixedpoint theory *}


132 


133 
use "fix.ML"


134 

0

135 
end
