34 adm :: "('a => o) => o" |
43 adm :: "('a => o) => o" |
35 VOID :: "void" ("'(')") |
44 VOID :: "void" ("'(')") |
36 PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100) |
45 PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100) |
37 COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60) |
46 COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60) |
38 "<<" :: "['a,'a] => o" (infixl 50) |
47 "<<" :: "['a,'a] => o" (infixl 50) |
39 rules |
48 |
|
49 axioms |
40 (** DOMAIN THEORY **) |
50 (** DOMAIN THEORY **) |
41 |
51 |
42 eq_def "x=y == x << y & y << x" |
52 eq_def: "x=y == x << y & y << x" |
43 |
53 |
44 less_trans "[| x << y; y << z |] ==> x << z" |
54 less_trans: "[| x << y; y << z |] ==> x << z" |
45 |
55 |
46 less_ext "(ALL x. f(x) << g(x)) ==> f << g" |
56 less_ext: "(ALL x. f(x) << g(x)) ==> f << g" |
47 |
57 |
48 mono "[| f << g; x << y |] ==> f(x) << g(y)" |
58 mono: "[| f << g; x << y |] ==> f(x) << g(y)" |
49 |
59 |
50 minimal "UU << x" |
60 minimal: "UU << x" |
51 |
61 |
52 FIX_eq "f(FIX(f)) = FIX(f)" |
62 FIX_eq: "f(FIX(f)) = FIX(f)" |
53 |
63 |
54 (** TR **) |
64 (** TR **) |
55 |
65 |
56 tr_cases "p=UU | p=TT | p=FF" |
66 tr_cases: "p=UU | p=TT | p=FF" |
57 |
67 |
58 not_TT_less_FF "~ TT << FF" |
68 not_TT_less_FF: "~ TT << FF" |
59 not_FF_less_TT "~ FF << TT" |
69 not_FF_less_TT: "~ FF << TT" |
60 not_TT_less_UU "~ TT << UU" |
70 not_TT_less_UU: "~ TT << UU" |
61 not_FF_less_UU "~ FF << UU" |
71 not_FF_less_UU: "~ FF << UU" |
62 |
72 |
63 COND_UU "UU => x | y = UU" |
73 COND_UU: "UU => x | y = UU" |
64 COND_TT "TT => x | y = x" |
74 COND_TT: "TT => x | y = x" |
65 COND_FF "FF => x | y = y" |
75 COND_FF: "FF => x | y = y" |
66 |
76 |
67 (** PAIRS **) |
77 (** PAIRS **) |
68 |
78 |
69 surj_pairing "<FST(z),SND(z)> = z" |
79 surj_pairing: "<FST(z),SND(z)> = z" |
70 |
80 |
71 FST "FST(<x,y>) = x" |
81 FST: "FST(<x,y>) = x" |
72 SND "SND(<x,y>) = y" |
82 SND: "SND(<x,y>) = y" |
73 |
83 |
74 (*** STRICT SUM ***) |
84 (*** STRICT SUM ***) |
75 |
85 |
76 INL_DEF "~x=UU ==> ~INL(x)=UU" |
86 INL_DEF: "~x=UU ==> ~INL(x)=UU" |
77 INR_DEF "~x=UU ==> ~INR(x)=UU" |
87 INR_DEF: "~x=UU ==> ~INR(x)=UU" |
78 |
88 |
79 INL_STRICT "INL(UU) = UU" |
89 INL_STRICT: "INL(UU) = UU" |
80 INR_STRICT "INR(UU) = UU" |
90 INR_STRICT: "INR(UU) = UU" |
81 |
91 |
82 WHEN_UU "WHEN(f,g,UU) = UU" |
92 WHEN_UU: "WHEN(f,g,UU) = UU" |
83 WHEN_INL "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" |
93 WHEN_INL: "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" |
84 WHEN_INR "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" |
94 WHEN_INR: "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" |
85 |
95 |
86 SUM_EXHAUSTION |
96 SUM_EXHAUSTION: |
87 "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))" |
97 "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))" |
88 |
98 |
89 (** VOID **) |
99 (** VOID **) |
90 |
100 |
91 void_cases "(x::void) = UU" |
101 void_cases: "(x::void) = UU" |
92 |
102 |
93 (** INDUCTION **) |
103 (** INDUCTION **) |
94 |
104 |
95 induct "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))" |
105 induct: "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))" |
96 |
106 |
97 (** Admissibility / Chain Completeness **) |
107 (** Admissibility / Chain Completeness **) |
98 (* All rules can be found on pages 199--200 of Larry's LCF book. |
108 (* All rules can be found on pages 199--200 of Larry's LCF book. |
99 Note that "easiness" of types is not taken into account |
109 Note that "easiness" of types is not taken into account |
100 because it cannot be expressed schematically; flatness could be. *) |
110 because it cannot be expressed schematically; flatness could be. *) |
101 |
111 |
102 adm_less "adm(%x. t(x) << u(x))" |
112 adm_less: "adm(%x. t(x) << u(x))" |
103 adm_not_less "adm(%x.~ t(x) << u)" |
113 adm_not_less: "adm(%x.~ t(x) << u)" |
104 adm_not_free "adm(%x. A)" |
114 adm_not_free: "adm(%x. A)" |
105 adm_subst "adm(P) ==> adm(%x. P(t(x)))" |
115 adm_subst: "adm(P) ==> adm(%x. P(t(x)))" |
106 adm_conj "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))" |
116 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))" |
117 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))" |
118 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))" |
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 |
110 end |
135 end |