1(* Title: LCF/LCF.thy 2 Author: Tobias Nipkow 3 Copyright 1992 University of Cambridge 4*) 5 6section \<open>LCF on top of First-Order Logic\<close> 7 8theory LCF 9imports FOL 10begin 11 12text \<open>This theory is based on Lawrence Paulson's book Logic and Computation.\<close> 13 14subsection \<open>Natural Deduction Rules for LCF\<close> 15 16class cpo = "term" 17default_sort cpo 18 19typedecl tr 20typedecl void 21typedecl ('a,'b) prod (infixl "*" 6) 22typedecl ('a,'b) sum (infixl "+" 5) 23 24instance "fun" :: (cpo, cpo) cpo .. 25instance prod :: (cpo, cpo) cpo .. 26instance sum :: (cpo, cpo) cpo .. 27instance tr :: cpo .. 28instance void :: cpo .. 29 30consts 31 UU :: "'a" 32 TT :: "tr" 33 FF :: "tr" 34 FIX :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" 35 FST :: "'a*'b \<Rightarrow> 'a" 36 SND :: "'a*'b \<Rightarrow> 'b" 37 INL :: "'a \<Rightarrow> 'a+'b" 38 INR :: "'b \<Rightarrow> 'a+'b" 39 WHEN :: "['a\<Rightarrow>'c, 'b\<Rightarrow>'c, 'a+'b] \<Rightarrow> 'c" 40 adm :: "('a \<Rightarrow> o) \<Rightarrow> o" 41 VOID :: "void" ("'(')") 42 PAIR :: "['a,'b] \<Rightarrow> 'a*'b" ("(1<_,/_>)" [0,0] 100) 43 COND :: "[tr,'a,'a] \<Rightarrow> 'a" ("(_ \<Rightarrow>/ (_ |/ _))" [60,60,60] 60) 44 less :: "['a,'a] \<Rightarrow> o" (infixl "<<" 50) 45 46axiomatization where 47 (** DOMAIN THEORY **) 48 49 eq_def: "x=y == x << y \<and> y << x" and 50 51 less_trans: "\<lbrakk>x << y; y << z\<rbrakk> \<Longrightarrow> x << z" and 52 53 less_ext: "(\<forall>x. f(x) << g(x)) \<Longrightarrow> f << g" and 54 55 mono: "\<lbrakk>f << g; x << y\<rbrakk> \<Longrightarrow> f(x) << g(y)" and 56 57 minimal: "UU << x" and 58 59 FIX_eq: "\<And>f. f(FIX(f)) = FIX(f)" 60 61axiomatization where 62 (** TR **) 63 64 tr_cases: "p=UU \<or> p=TT \<or> p=FF" and 65 66 not_TT_less_FF: "\<not> TT << FF" and 67 not_FF_less_TT: "\<not> FF << TT" and 68 not_TT_less_UU: "\<not> TT << UU" and 69 not_FF_less_UU: "\<not> FF << UU" and 70 71 COND_UU: "UU \<Rightarrow> x | y = UU" and 72 COND_TT: "TT \<Rightarrow> x | y = x" and 73 COND_FF: "FF \<Rightarrow> x | y = y" 74 75axiomatization where 76 (** PAIRS **) 77 78 surj_pairing: "<FST(z),SND(z)> = z" and 79 80 FST: "FST(<x,y>) = x" and 81 SND: "SND(<x,y>) = y" 82 83axiomatization where 84 (*** STRICT SUM ***) 85 86 INL_DEF: "\<not>x=UU \<Longrightarrow> \<not>INL(x)=UU" and 87 INR_DEF: "\<not>x=UU \<Longrightarrow> \<not>INR(x)=UU" and 88 89 INL_STRICT: "INL(UU) = UU" and 90 INR_STRICT: "INR(UU) = UU" and 91 92 WHEN_UU: "WHEN(f,g,UU) = UU" and 93 WHEN_INL: "\<not>x=UU \<Longrightarrow> WHEN(f,g,INL(x)) = f(x)" and 94 WHEN_INR: "\<not>x=UU \<Longrightarrow> WHEN(f,g,INR(x)) = g(x)" and 95 96 SUM_EXHAUSTION: 97 "z = UU \<or> (\<exists>x. \<not>x=UU \<and> z = INL(x)) \<or> (\<exists>y. \<not>y=UU \<and> z = INR(y))" 98 99axiomatization where 100 (** VOID **) 101 102 void_cases: "(x::void) = UU" 103 104 (** INDUCTION **) 105 106axiomatization where 107 induct: "\<lbrakk>adm(P); P(UU); \<forall>x. P(x) \<longrightarrow> P(f(x))\<rbrakk> \<Longrightarrow> P(FIX(f))" 108 109axiomatization where 110 (** Admissibility / Chain Completeness **) 111 (* All rules can be found on pages 199--200 of Larry's LCF book. 112 Note that "easiness" of types is not taken into account 113 because it cannot be expressed schematically; flatness could be. *) 114 115 adm_less: "\<And>t u. adm(\<lambda>x. t(x) << u(x))" and 116 adm_not_less: "\<And>t u. adm(\<lambda>x.\<not> t(x) << u)" and 117 adm_not_free: "\<And>A. adm(\<lambda>x. A)" and 118 adm_subst: "\<And>P t. adm(P) \<Longrightarrow> adm(\<lambda>x. P(t(x)))" and 119 adm_conj: "\<And>P Q. \<lbrakk>adm(P); adm(Q)\<rbrakk> \<Longrightarrow> adm(\<lambda>x. P(x)\<and>Q(x))" and 120 adm_disj: "\<And>P Q. \<lbrakk>adm(P); adm(Q)\<rbrakk> \<Longrightarrow> adm(\<lambda>x. P(x)\<or>Q(x))" and 121 adm_imp: "\<And>P Q. \<lbrakk>adm(\<lambda>x.\<not>P(x)); adm(Q)\<rbrakk> \<Longrightarrow> adm(\<lambda>x. P(x)\<longrightarrow>Q(x))" and 122 adm_all: "\<And>P. (\<And>y. adm(P(y))) \<Longrightarrow> adm(\<lambda>x. \<forall>y. P(y,x))" 123 124 125lemma eq_imp_less1: "x = y \<Longrightarrow> x << y" 126 by (simp add: eq_def) 127 128lemma eq_imp_less2: "x = y \<Longrightarrow> y << x" 129 by (simp add: eq_def) 130 131lemma less_refl [simp]: "x << x" 132 apply (rule eq_imp_less1) 133 apply (rule refl) 134 done 135 136lemma less_anti_sym: "\<lbrakk>x << y; y << x\<rbrakk> \<Longrightarrow> x=y" 137 by (simp add: eq_def) 138 139lemma ext: "(\<And>x::'a::cpo. f(x)=(g(x)::'b::cpo)) \<Longrightarrow> (\<lambda>x. f(x))=(\<lambda>x. g(x))" 140 apply (rule less_anti_sym) 141 apply (rule less_ext) 142 apply simp 143 apply simp 144 done 145 146lemma cong: "\<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> f(x)=g(y)" 147 by simp 148 149lemma less_ap_term: "x << y \<Longrightarrow> f(x) << f(y)" 150 by (rule less_refl [THEN mono]) 151 152lemma less_ap_thm: "f << g \<Longrightarrow> f(x) << g(x)" 153 by (rule less_refl [THEN [2] mono]) 154 155lemma ap_term: "(x::'a::cpo) = y \<Longrightarrow> (f(x)::'b::cpo) = f(y)" 156 apply (rule cong [OF refl]) 157 apply simp 158 done 159 160lemma ap_thm: "f = g \<Longrightarrow> f(x) = g(x)" 161 apply (erule cong) 162 apply (rule refl) 163 done 164 165 166lemma UU_abs: "(\<lambda>x::'a::cpo. UU) = UU" 167 apply (rule less_anti_sym) 168 prefer 2 169 apply (rule minimal) 170 apply (rule less_ext) 171 apply (rule allI) 172 apply (rule minimal) 173 done 174 175lemma UU_app: "UU(x) = UU" 176 by (rule UU_abs [symmetric, THEN ap_thm]) 177 178lemma less_UU: "x << UU \<Longrightarrow> x=UU" 179 apply (rule less_anti_sym) 180 apply assumption 181 apply (rule minimal) 182 done 183 184lemma tr_induct: "\<lbrakk>P(UU); P(TT); P(FF)\<rbrakk> \<Longrightarrow> \<forall>b. P(b)" 185 apply (rule allI) 186 apply (rule mp) 187 apply (rule_tac [2] p = b in tr_cases) 188 apply blast 189 done 190 191lemma Contrapos: "\<not> B \<Longrightarrow> (A \<Longrightarrow> B) \<Longrightarrow> \<not>A" 192 by blast 193 194lemma not_less_imp_not_eq1: "\<not> x << y \<Longrightarrow> x \<noteq> y" 195 apply (erule Contrapos) 196 apply simp 197 done 198 199lemma not_less_imp_not_eq2: "\<not> y << x \<Longrightarrow> x \<noteq> y" 200 apply (erule Contrapos) 201 apply simp 202 done 203 204lemma not_UU_eq_TT: "UU \<noteq> TT" 205 by (rule not_less_imp_not_eq2) (rule not_TT_less_UU) 206lemma not_UU_eq_FF: "UU \<noteq> FF" 207 by (rule not_less_imp_not_eq2) (rule not_FF_less_UU) 208lemma not_TT_eq_UU: "TT \<noteq> UU" 209 by (rule not_less_imp_not_eq1) (rule not_TT_less_UU) 210lemma not_TT_eq_FF: "TT \<noteq> FF" 211 by (rule not_less_imp_not_eq1) (rule not_TT_less_FF) 212lemma not_FF_eq_UU: "FF \<noteq> UU" 213 by (rule not_less_imp_not_eq1) (rule not_FF_less_UU) 214lemma not_FF_eq_TT: "FF \<noteq> TT" 215 by (rule not_less_imp_not_eq1) (rule not_FF_less_TT) 216 217 218lemma COND_cases_iff [rule_format]: 219 "\<forall>b. P(b\<Rightarrow>x|y) \<longleftrightarrow> (b=UU\<longrightarrow>P(UU)) \<and> (b=TT\<longrightarrow>P(x)) \<and> (b=FF\<longrightarrow>P(y))" 220 apply (insert not_UU_eq_TT not_UU_eq_FF not_TT_eq_UU 221 not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT) 222 apply (rule tr_induct) 223 apply (simplesubst COND_UU) 224 apply blast 225 apply (simplesubst COND_TT) 226 apply blast 227 apply (simplesubst COND_FF) 228 apply blast 229 done 230 231lemma COND_cases: 232 "\<lbrakk>x = UU \<longrightarrow> P(UU); x = TT \<longrightarrow> P(xa); x = FF \<longrightarrow> P(y)\<rbrakk> \<Longrightarrow> P(x \<Rightarrow> xa | y)" 233 apply (rule COND_cases_iff [THEN iffD2]) 234 apply blast 235 done 236 237lemmas [simp] = 238 minimal 239 UU_app 240 UU_app [THEN ap_thm] 241 UU_app [THEN ap_thm, THEN ap_thm] 242 not_TT_less_FF not_FF_less_TT not_TT_less_UU not_FF_less_UU not_UU_eq_TT 243 not_UU_eq_FF not_TT_eq_UU not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT 244 COND_UU COND_TT COND_FF 245 surj_pairing FST SND 246 247 248subsection \<open>Ordered pairs and products\<close> 249 250lemma expand_all_PROD: "(\<forall>p. P(p)) \<longleftrightarrow> (\<forall>x y. P(<x,y>))" 251 apply (rule iffI) 252 apply blast 253 apply (rule allI) 254 apply (rule surj_pairing [THEN subst]) 255 apply blast 256 done 257 258lemma PROD_less: "(p::'a*'b) << q \<longleftrightarrow> FST(p) << FST(q) \<and> SND(p) << SND(q)" 259 apply (rule iffI) 260 apply (rule conjI) 261 apply (erule less_ap_term) 262 apply (erule less_ap_term) 263 apply (erule conjE) 264 apply (rule surj_pairing [of p, THEN subst]) 265 apply (rule surj_pairing [of q, THEN subst]) 266 apply (rule mono, erule less_ap_term, assumption) 267 done 268 269lemma PROD_eq: "p=q \<longleftrightarrow> FST(p)=FST(q) \<and> SND(p)=SND(q)" 270 apply (rule iffI) 271 apply simp 272 apply (unfold eq_def) 273 apply (simp add: PROD_less) 274 done 275 276lemma PAIR_less [simp]: "<a,b> << <c,d> \<longleftrightarrow> a<<c \<and> b<<d" 277 by (simp add: PROD_less) 278 279lemma PAIR_eq [simp]: "<a,b> = <c,d> \<longleftrightarrow> a=c \<and> b=d" 280 by (simp add: PROD_eq) 281 282lemma UU_is_UU_UU [simp]: "<UU,UU> = UU" 283 by (rule less_UU) (simp add: PROD_less) 284 285lemma FST_STRICT [simp]: "FST(UU) = UU" 286 apply (rule subst [OF UU_is_UU_UU]) 287 apply (simp del: UU_is_UU_UU) 288 done 289 290lemma SND_STRICT [simp]: "SND(UU) = UU" 291 apply (rule subst [OF UU_is_UU_UU]) 292 apply (simp del: UU_is_UU_UU) 293 done 294 295 296subsection \<open>Fixedpoint theory\<close> 297 298lemma adm_eq: "adm(\<lambda>x. t(x)=(u(x)::'a::cpo))" 299 apply (unfold eq_def) 300 apply (rule adm_conj adm_less)+ 301 done 302 303lemma adm_not_not: "adm(P) \<Longrightarrow> adm(\<lambda>x. \<not> \<not> P(x))" 304 by simp 305 306lemma not_eq_TT: "\<forall>p. \<not>p=TT \<longleftrightarrow> (p=FF \<or> p=UU)" 307 and not_eq_FF: "\<forall>p. \<not>p=FF \<longleftrightarrow> (p=TT \<or> p=UU)" 308 and not_eq_UU: "\<forall>p. \<not>p=UU \<longleftrightarrow> (p=TT \<or> p=FF)" 309 by (rule tr_induct, simp_all)+ 310 311lemma adm_not_eq_tr: "\<forall>p::tr. adm(\<lambda>x. \<not>t(x)=p)" 312 apply (rule tr_induct) 313 apply (simp_all add: not_eq_TT not_eq_FF not_eq_UU) 314 apply (rule adm_disj adm_eq)+ 315 done 316 317lemmas adm_lemmas = 318 adm_not_free adm_eq adm_less adm_not_less 319 adm_not_eq_tr adm_conj adm_disj adm_imp adm_all 320 321method_setup induct = \<open> 322 Scan.lift Args.embedded_inner_syntax >> (fn v => fn ctxt => 323 SIMPLE_METHOD' (fn i => 324 Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] [] @{thm induct} i THEN 325 REPEAT (resolve_tac ctxt @{thms adm_lemmas} i))) 326\<close> 327 328lemma least_FIX: "f(p) = p \<Longrightarrow> FIX(f) << p" 329 apply (induct f) 330 apply (rule minimal) 331 apply (intro strip) 332 apply (erule subst) 333 apply (erule less_ap_term) 334 done 335 336lemma lfp_is_FIX: 337 assumes 1: "f(p) = p" 338 and 2: "\<forall>q. f(q)=q \<longrightarrow> 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 348lemma FIX_pair: "<FIX(f),FIX(g)> = FIX(\<lambda>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 360lemma FIX1: "FIX(f) = FST(FIX(\<lambda>p. <f(FST(p)),g(SND(p))>))" 361 by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct1]) 362 363lemma FIX2: "FIX(g) = SND(FIX(\<lambda>p. <f(FST(p)),g(SND(p))>))" 364 by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct2]) 365 366lemma induct2: 367 assumes 1: "adm(\<lambda>p. P(FST(p),SND(p)))" 368 and 2: "P(UU::'a,UU::'b)" 369 and 3: "\<forall>x y. P(x,y) \<longrightarrow> 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]) 373 apply (rule induct [where ?f = "\<lambda>x. <f(FST(x)),g(SND(x))>"]) 374 apply (rule 1) 375 apply simp 376 apply (rule 2) 377 apply (simp add: expand_all_PROD) 378 apply (rule 3) 379 done 380 381ML \<open> 382fun induct2_tac ctxt (f, g) i = 383 Rule_Insts.res_inst_tac ctxt 384 [((("f", 0), Position.none), f), ((("g", 0), Position.none), g)] [] @{thm induct2} i THEN 385 REPEAT(resolve_tac ctxt @{thms adm_lemmas} i) 386\<close> 387 388end 389