|
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 199--200 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 |