src/LCF/lcf.thy
changeset 0 a5a9c433f639
child 283 76caebd18756
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/LCF/lcf.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,107 @@
     1.4 +(*  Title: 	LCF/lcf.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Tobias Nipkow
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +Natural Deduction Rules for LCF
    1.10 +*)
    1.11 +
    1.12 +LCF = FOL +
    1.13 +
    1.14 +classes cpo < term
    1.15 +
    1.16 +default cpo
    1.17 +
    1.18 +types tr,void 0
    1.19 +      "*" 2 (infixl 6)
    1.20 +      "+" 2 (infixl 5)
    1.21 +
    1.22 +arities fun, "*", "+" :: (cpo,cpo)cpo
    1.23 +        tr,void :: cpo
    1.24 +
    1.25 +consts
    1.26 + UU	:: "'a"
    1.27 + TT,FF	:: "tr"
    1.28 + FIX	:: "('a => 'a) => 'a"
    1.29 + FST	:: "'a*'b => 'a"
    1.30 + SND	:: "'a*'b => 'b"
    1.31 + INL    :: "'a => 'a+'b"
    1.32 + INR    :: "'b => 'a+'b"
    1.33 + WHEN   :: "['a=>'c, 'b=>'c, 'a+'b] => 'c"
    1.34 + adm	:: "('a => o) => o"
    1.35 + VOID	:: "void"		("()")
    1.36 + PAIR	:: "['a,'b] => 'a*'b"	("(1<_,/_>)" [0,0] 100)
    1.37 + COND	:: "[tr,'a,'a] => 'a"	("(_ =>/ (_ |/ _))" [60,60,60] 60)
    1.38 + "<<"	:: "['a,'a] => o"	(infixl 50)
    1.39 +rules
    1.40 +  (** DOMAIN THEORY **)
    1.41 +
    1.42 +  eq_def	"x=y == x << y & y << x"
    1.43 +
    1.44 +  less_trans	"[| x << y; y << z |] ==> x << z"
    1.45 +
    1.46 +  less_ext	"(ALL x. f(x) << g(x)) ==> f << g"
    1.47 +
    1.48 +  mono		"[| f << g; x << y |] ==> f(x) << g(y)"
    1.49 +
    1.50 +  minimal	"UU << x"
    1.51 +
    1.52 +  FIX_eq	"f(FIX(f)) = FIX(f)"
    1.53 +
    1.54 +  (** TR **)
    1.55 +
    1.56 +  tr_cases	"p=UU | p=TT | p=FF"
    1.57 +
    1.58 +  not_TT_less_FF "~ TT << FF"
    1.59 +  not_FF_less_TT "~ FF << TT"
    1.60 +  not_TT_less_UU "~ TT << UU"
    1.61 +  not_FF_less_UU "~ FF << UU"
    1.62 +
    1.63 +  COND_UU	"UU => x | y  =  UU"
    1.64 +  COND_TT	"TT => x | y  =  x"
    1.65 +  COND_FF	"FF => x | y  =  y"
    1.66 +
    1.67 +  (** PAIRS **)
    1.68 +
    1.69 +  surj_pairing	"<FST(z),SND(z)> = z"
    1.70 +
    1.71 +  FST	"FST(<x,y>) = x"
    1.72 +  SND	"SND(<x,y>) = y"
    1.73 +
    1.74 +  (*** STRICT SUM ***)
    1.75 +
    1.76 +  INL_DEF "~x=UU ==> ~INL(x)=UU"
    1.77 +  INR_DEF "~x=UU ==> ~INR(x)=UU"
    1.78 +
    1.79 +  INL_STRICT "INL(UU) = UU"
    1.80 +  INR_STRICT "INR(UU) = UU"
    1.81 +
    1.82 +  WHEN_UU  "WHEN(f,g,UU) = UU"
    1.83 +  WHEN_INL "~x=UU ==> WHEN(f,g,INL(x)) = f(x)"
    1.84 +  WHEN_INR "~x=UU ==> WHEN(f,g,INR(x)) = g(x)"
    1.85 +
    1.86 +  SUM_EXHAUSTION
    1.87 +    "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))"
    1.88 +
    1.89 +  (** VOID **)
    1.90 +
    1.91 +  void_cases	"(x::void) = UU"
    1.92 +
    1.93 +  (** INDUCTION **)
    1.94 +
    1.95 +  induct	"[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))"
    1.96 +
    1.97 +  (** Admissibility / Chain Completeness **)
    1.98 +  (* All rules can be found on pages 199--200 of Larry's LCF book.
    1.99 +     Note that "easiness" of types is not taken into account
   1.100 +     because it cannot be expressed schematically; flatness could be. *)
   1.101 +
   1.102 +  adm_less	"adm(%x.t(x) << u(x))"
   1.103 +  adm_not_less	"adm(%x.~ t(x) << u)"
   1.104 +  adm_not_free  "adm(%x.A)"
   1.105 +  adm_subst	"adm(P) ==> adm(%x.P(t(x)))"
   1.106 +  adm_conj	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
   1.107 +  adm_disj	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
   1.108 +  adm_imp	"[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
   1.109 +  adm_all	"(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"
   1.110 +end