19757

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 
begin

0

12 

17248

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

0

14 

17248

15 
subsection {* Natural Deduction Rules for LCF *}


16 


17 
classes cpo < "term"


18 
defaultsort cpo


19 


20 
typedecl tr


21 
typedecl void


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


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

0

24 

283

25 
arities

17248

26 
fun :: (cpo, cpo) cpo


27 
"*" :: (cpo, cpo) cpo


28 
"+" :: (cpo, cpo) cpo


29 
tr :: cpo


30 
void :: cpo

0

31 


32 
consts

1474

33 
UU :: "'a"

17248

34 
TT :: "tr"


35 
FF :: "tr"

1474

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


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


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

0

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


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


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

1474

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


43 
VOID :: "void" ("'(')")


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


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


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

17248

47 


48 
axioms

0

49 
(** DOMAIN THEORY **)


50 

17248

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

0

52 

17248

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

0

54 

17248

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

0

56 

17248

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

0

58 

17248

59 
minimal: "UU << x"

0

60 

17248

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

0

62 


63 
(** TR **)


64 

17248

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

0

66 

17248

67 
not_TT_less_FF: "~ TT << FF"


68 
not_FF_less_TT: "~ FF << TT"


69 
not_TT_less_UU: "~ TT << UU"


70 
not_FF_less_UU: "~ FF << UU"

0

71 

17248

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


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


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

0

75 


76 
(** PAIRS **)


77 

17248

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

0

79 

17248

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


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

0

82 


83 
(*** STRICT SUM ***)


84 

17248

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


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

0

87 

17248

88 
INL_STRICT: "INL(UU) = UU"


89 
INR_STRICT: "INR(UU) = UU"

0

90 

17248

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


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


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

0

94 

17248

95 
SUM_EXHAUSTION:

0

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


97 


98 
(** VOID **)


99 

17248

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

0

101 


102 
(** INDUCTION **)


103 

17248

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

0

105 


106 
(** Admissibility / Chain Completeness **)


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


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


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


110 

17248

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


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


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


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


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


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


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


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


119 

19757

120 


121 
lemma eq_imp_less1: "x = y ==> x << y"


122 
by (simp add: eq_def)


123 


124 
lemma eq_imp_less2: "x = y ==> y << x"


125 
by (simp add: eq_def)


126 


127 
lemma less_refl [simp]: "x << x"


128 
apply (rule eq_imp_less1)


129 
apply (rule refl)


130 
done


131 


132 
lemma less_anti_sym: "[ x << y; y << x ] ==> x=y"


133 
by (simp add: eq_def)


134 


135 
lemma ext: "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))"


136 
apply (rule less_anti_sym)


137 
apply (rule less_ext)


138 
apply simp


139 
apply simp


140 
done


141 


142 
lemma cong: "[ f=g; x=y ] ==> f(x)=g(y)"


143 
by simp


144 


145 
lemma less_ap_term: "x << y ==> f(x) << f(y)"


146 
by (rule less_refl [THEN mono])


147 


148 
lemma less_ap_thm: "f << g ==> f(x) << g(x)"


149 
by (rule less_refl [THEN [2] mono])


150 


151 
lemma ap_term: "(x::'a::cpo) = y ==> (f(x)::'b::cpo) = f(y)"


152 
apply (rule cong [OF refl])


153 
apply simp


154 
done


155 


156 
lemma ap_thm: "f = g ==> f(x) = g(x)"


157 
apply (erule cong)


158 
apply (rule refl)


159 
done


160 


161 


162 
lemma UU_abs: "(%x::'a::cpo. UU) = UU"


163 
apply (rule less_anti_sym)


164 
prefer 2


165 
apply (rule minimal)


166 
apply (rule less_ext)


167 
apply (rule allI)


168 
apply (rule minimal)


169 
done


170 


171 
lemma UU_app: "UU(x) = UU"


172 
by (rule UU_abs [symmetric, THEN ap_thm])


173 


174 
lemma less_UU: "x << UU ==> x=UU"


175 
apply (rule less_anti_sym)


176 
apply assumption


177 
apply (rule minimal)


178 
done

17248

179 

19757

180 
lemma tr_induct: "[ P(UU); P(TT); P(FF) ] ==> ALL b. P(b)"


181 
apply (rule allI)


182 
apply (rule mp)


183 
apply (rule_tac [2] p = b in tr_cases)


184 
apply blast


185 
done


186 


187 
lemma Contrapos: "~ B ==> (A ==> B) ==> ~A"


188 
by blast


189 


190 
lemma not_less_imp_not_eq1: "~ x << y \<Longrightarrow> x \<noteq> y"


191 
apply (erule Contrapos)


192 
apply simp


193 
done


194 


195 
lemma not_less_imp_not_eq2: "~ y << x \<Longrightarrow> x \<noteq> y"


196 
apply (erule Contrapos)


197 
apply simp


198 
done


199 


200 
lemma not_UU_eq_TT: "UU \<noteq> TT"


201 
by (rule not_less_imp_not_eq2) (rule not_TT_less_UU)


202 
lemma not_UU_eq_FF: "UU \<noteq> FF"


203 
by (rule not_less_imp_not_eq2) (rule not_FF_less_UU)


204 
lemma not_TT_eq_UU: "TT \<noteq> UU"


205 
by (rule not_less_imp_not_eq1) (rule not_TT_less_UU)


206 
lemma not_TT_eq_FF: "TT \<noteq> FF"


207 
by (rule not_less_imp_not_eq1) (rule not_TT_less_FF)


208 
lemma not_FF_eq_UU: "FF \<noteq> UU"


209 
by (rule not_less_imp_not_eq1) (rule not_FF_less_UU)


210 
lemma not_FF_eq_TT: "FF \<noteq> TT"


211 
by (rule not_less_imp_not_eq1) (rule not_FF_less_TT)


212 


213 


214 
lemma COND_cases_iff [rule_format]:


215 
"ALL b. P(b=>xy) <> (b=UU>P(UU)) & (b=TT>P(x)) & (b=FF>P(y))"


216 
apply (insert not_UU_eq_TT not_UU_eq_FF not_TT_eq_UU


217 
not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT)


218 
apply (rule tr_induct)


219 
apply (simplesubst COND_UU)


220 
apply blast


221 
apply (simplesubst COND_TT)


222 
apply blast


223 
apply (simplesubst COND_FF)


224 
apply blast


225 
done


226 


227 
lemma COND_cases:


228 
"[ x = UU > P(UU); x = TT > P(xa); x = FF > P(y) ] ==> P(x => xa  y)"


229 
apply (rule COND_cases_iff [THEN iffD2])


230 
apply blast


231 
done


232 


233 
lemmas [simp] =


234 
minimal


235 
UU_app


236 
UU_app [THEN ap_thm]


237 
UU_app [THEN ap_thm, THEN ap_thm]


238 
not_TT_less_FF not_FF_less_TT not_TT_less_UU not_FF_less_UU not_UU_eq_TT


239 
not_UU_eq_FF not_TT_eq_UU not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT


240 
COND_UU COND_TT COND_FF


241 
surj_pairing FST SND

17248

242 


243 


244 
subsection {* Ordered pairs and products *}


245 

19757

246 
lemma expand_all_PROD: "(ALL p. P(p)) <> (ALL x y. P(<x,y>))"


247 
apply (rule iffI)


248 
apply blast


249 
apply (rule allI)


250 
apply (rule surj_pairing [THEN subst])


251 
apply blast


252 
done


253 


254 
lemma PROD_less: "(p::'a*'b) << q <> FST(p) << FST(q) & SND(p) << SND(q)"


255 
apply (rule iffI)


256 
apply (rule conjI)


257 
apply (erule less_ap_term)


258 
apply (erule less_ap_term)


259 
apply (erule conjE)


260 
apply (rule surj_pairing [of p, THEN subst])


261 
apply (rule surj_pairing [of q, THEN subst])


262 
apply (rule mono, erule less_ap_term, assumption)


263 
done


264 


265 
lemma PROD_eq: "p=q <> FST(p)=FST(q) & SND(p)=SND(q)"


266 
apply (rule iffI)


267 
apply simp


268 
apply (unfold eq_def)


269 
apply (simp add: PROD_less)


270 
done


271 


272 
lemma PAIR_less [simp]: "<a,b> << <c,d> <> a<<c & b<<d"


273 
by (simp add: PROD_less)


274 


275 
lemma PAIR_eq [simp]: "<a,b> = <c,d> <> a=c & b=d"


276 
by (simp add: PROD_eq)


277 


278 
lemma UU_is_UU_UU [simp]: "<UU,UU> = UU"


279 
by (rule less_UU) (simp add: PROD_less)


280 


281 
lemma FST_STRICT [simp]: "FST(UU) = UU"


282 
apply (rule subst [OF UU_is_UU_UU])


283 
apply (simp del: UU_is_UU_UU)


284 
done


285 


286 
lemma SND_STRICT [simp]: "SND(UU) = UU"


287 
apply (rule subst [OF UU_is_UU_UU])


288 
apply (simp del: UU_is_UU_UU)


289 
done

17248

290 


291 


292 
subsection {* Fixedpoint theory *}


293 

19757

294 
lemma adm_eq: "adm(%x. t(x)=(u(x)::'a::cpo))"


295 
apply (unfold eq_def)


296 
apply (rule adm_conj adm_less)+


297 
done


298 


299 
lemma adm_not_not: "adm(P) ==> adm(%x.~~P(x))"


300 
by simp


301 


302 
lemma not_eq_TT: "ALL p. ~p=TT <> (p=FF  p=UU)"


303 
and not_eq_FF: "ALL p. ~p=FF <> (p=TT  p=UU)"


304 
and not_eq_UU: "ALL p. ~p=UU <> (p=TT  p=FF)"


305 
by (rule tr_induct, simp_all)+


306 


307 
lemma adm_not_eq_tr: "ALL p::tr. adm(%x. ~t(x)=p)"


308 
apply (rule tr_induct)


309 
apply (simp_all add: not_eq_TT not_eq_FF not_eq_UU)


310 
apply (rule adm_disj adm_eq)+


311 
done


312 


313 
lemmas adm_lemmas =


314 
adm_not_free adm_eq adm_less adm_not_less


315 
adm_not_eq_tr adm_conj adm_disj adm_imp adm_all


316 


317 


318 
ML {*


319 
local


320 
val adm_lemmas = thms "adm_lemmas"


321 
val induct = thm "induct"


322 
in


323 
fun induct_tac v i =


324 
res_inst_tac[("f",v)] induct i THEN REPEAT (resolve_tac adm_lemmas i)


325 
end


326 
*}


327 


328 
lemma least_FIX: "f(p) = p ==> FIX(f) << p"


329 
apply (tactic {* induct_tac "f" 1 *})


330 
apply (rule minimal)


331 
apply (intro strip)


332 
apply (erule subst)


333 
apply (erule less_ap_term)


334 
done


335 


336 
lemma lfp_is_FIX:


337 
assumes 1: "f(p) = p"


338 
and 2: "ALL q. f(q)=q > p << q"


339 
shows "p = FIX(f)"


340 
apply (rule less_anti_sym)


341 
apply (rule 2 [THEN spec, THEN mp])


342 
apply (rule FIX_eq)


343 
apply (rule least_FIX)


344 
apply (rule 1)


345 
done


346 


347 


348 
lemma FIX_pair: "<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)"


349 
apply (rule lfp_is_FIX)


350 
apply (simp add: FIX_eq [of f] FIX_eq [of g])


351 
apply (intro strip)


352 
apply (simp add: PROD_less)


353 
apply (rule conjI)


354 
apply (rule least_FIX)


355 
apply (erule subst, rule FST [symmetric])


356 
apply (rule least_FIX)


357 
apply (erule subst, rule SND [symmetric])


358 
done


359 


360 
lemma FIX1: "FIX(f) = FST(FIX(%p. <f(FST(p)),g(SND(p))>))"


361 
by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct1])


362 


363 
lemma FIX2: "FIX(g) = SND(FIX(%p. <f(FST(p)),g(SND(p))>))"


364 
by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct2])


365 


366 
lemma induct2:


367 
assumes 1: "adm(%p. P(FST(p),SND(p)))"


368 
and 2: "P(UU::'a,UU::'b)"


369 
and 3: "ALL x y. P(x,y) > P(f(x),g(y))"


370 
shows "P(FIX(f),FIX(g))"


371 
apply (rule FIX1 [THEN ssubst, of _ f g])


372 
apply (rule FIX2 [THEN ssubst, of _ f g])

19758

373 
apply (rule induct [where ?f = "%x. <f(FST(x)),g(SND(x))>"])


374 
apply (rule 1)

19757

375 
apply simp


376 
apply (rule 2)


377 
apply (simp add: expand_all_PROD)


378 
apply (rule 3)


379 
done


380 


381 
ML {*


382 
local


383 
val induct2 = thm "induct2"


384 
val adm_lemmas = thms "adm_lemmas"


385 
in


386 


387 
fun induct2_tac (f,g) i =


388 
res_inst_tac[("f",f),("g",g)] induct2 i THEN


389 
REPEAT(resolve_tac adm_lemmas i)

17248

390 

0

391 
end

19757

392 
*}


393 


394 
end
