1.1 --- a/src/LCF/IsaMakefile Thu Jun 01 21:14:54 2006 +0200
1.2 +++ b/src/LCF/IsaMakefile Thu Jun 01 23:07:51 2006 +0200
1.3 @@ -26,7 +26,7 @@
1.4 FOL:
1.5 @cd $(SRC)/FOL; $(ISATOOL) make FOL
1.6
1.7 -$(OUT)/LCF: $(OUT)/FOL LCF_lemmas.ML LCF.thy ROOT.ML fix.ML pair.ML
1.8 +$(OUT)/LCF: $(OUT)/FOL LCF.thy ROOT.ML
1.9 @$(ISATOOL) usedir -b -r $(OUT)/FOL LCF
1.10
1.11
2.1 --- a/src/LCF/LCF.thy Thu Jun 01 21:14:54 2006 +0200
2.2 +++ b/src/LCF/LCF.thy Thu Jun 01 23:07:51 2006 +0200
2.3 @@ -1,4 +1,4 @@
2.4 -(* Title: LCF/lcf.thy
2.5 +(* Title: LCF/LCF.thy
2.6 ID: $Id$
2.7 Author: Tobias Nipkow
2.8 Copyright 1992 University of Cambridge
2.9 @@ -8,7 +8,6 @@
2.10
2.11 theory LCF
2.12 imports FOL
2.13 -uses ("LCF_lemmas.ML") ("pair.ML") ("fix.ML")
2.14 begin
2.15
2.16 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *}
2.17 @@ -118,18 +117,277 @@
2.18 adm_imp: "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))"
2.19 adm_all: "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))"
2.20
2.21 -ML {* use_legacy_bindings (the_context ()) *}
2.22
2.23 -use "LCF_lemmas.ML"
2.24 +lemma eq_imp_less1: "x = y ==> x << y"
2.25 + by (simp add: eq_def)
2.26 +
2.27 +lemma eq_imp_less2: "x = y ==> y << x"
2.28 + by (simp add: eq_def)
2.29 +
2.30 +lemma less_refl [simp]: "x << x"
2.31 + apply (rule eq_imp_less1)
2.32 + apply (rule refl)
2.33 + done
2.34 +
2.35 +lemma less_anti_sym: "[| x << y; y << x |] ==> x=y"
2.36 + by (simp add: eq_def)
2.37 +
2.38 +lemma ext: "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))"
2.39 + apply (rule less_anti_sym)
2.40 + apply (rule less_ext)
2.41 + apply simp
2.42 + apply simp
2.43 + done
2.44 +
2.45 +lemma cong: "[| f=g; x=y |] ==> f(x)=g(y)"
2.46 + by simp
2.47 +
2.48 +lemma less_ap_term: "x << y ==> f(x) << f(y)"
2.49 + by (rule less_refl [THEN mono])
2.50 +
2.51 +lemma less_ap_thm: "f << g ==> f(x) << g(x)"
2.52 + by (rule less_refl [THEN [2] mono])
2.53 +
2.54 +lemma ap_term: "(x::'a::cpo) = y ==> (f(x)::'b::cpo) = f(y)"
2.55 + apply (rule cong [OF refl])
2.56 + apply simp
2.57 + done
2.58 +
2.59 +lemma ap_thm: "f = g ==> f(x) = g(x)"
2.60 + apply (erule cong)
2.61 + apply (rule refl)
2.62 + done
2.63 +
2.64 +
2.65 +lemma UU_abs: "(%x::'a::cpo. UU) = UU"
2.66 + apply (rule less_anti_sym)
2.67 + prefer 2
2.68 + apply (rule minimal)
2.69 + apply (rule less_ext)
2.70 + apply (rule allI)
2.71 + apply (rule minimal)
2.72 + done
2.73 +
2.74 +lemma UU_app: "UU(x) = UU"
2.75 + by (rule UU_abs [symmetric, THEN ap_thm])
2.76 +
2.77 +lemma less_UU: "x << UU ==> x=UU"
2.78 + apply (rule less_anti_sym)
2.79 + apply assumption
2.80 + apply (rule minimal)
2.81 + done
2.82 +
2.83 +lemma tr_induct: "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)"
2.84 + apply (rule allI)
2.85 + apply (rule mp)
2.86 + apply (rule_tac [2] p = b in tr_cases)
2.87 + apply blast
2.88 + done
2.89 +
2.90 +lemma Contrapos: "~ B ==> (A ==> B) ==> ~A"
2.91 + by blast
2.92 +
2.93 +lemma not_less_imp_not_eq1: "~ x << y \<Longrightarrow> x \<noteq> y"
2.94 + apply (erule Contrapos)
2.95 + apply simp
2.96 + done
2.97 +
2.98 +lemma not_less_imp_not_eq2: "~ y << x \<Longrightarrow> x \<noteq> y"
2.99 + apply (erule Contrapos)
2.100 + apply simp
2.101 + done
2.102 +
2.103 +lemma not_UU_eq_TT: "UU \<noteq> TT"
2.104 + by (rule not_less_imp_not_eq2) (rule not_TT_less_UU)
2.105 +lemma not_UU_eq_FF: "UU \<noteq> FF"
2.106 + by (rule not_less_imp_not_eq2) (rule not_FF_less_UU)
2.107 +lemma not_TT_eq_UU: "TT \<noteq> UU"
2.108 + by (rule not_less_imp_not_eq1) (rule not_TT_less_UU)
2.109 +lemma not_TT_eq_FF: "TT \<noteq> FF"
2.110 + by (rule not_less_imp_not_eq1) (rule not_TT_less_FF)
2.111 +lemma not_FF_eq_UU: "FF \<noteq> UU"
2.112 + by (rule not_less_imp_not_eq1) (rule not_FF_less_UU)
2.113 +lemma not_FF_eq_TT: "FF \<noteq> TT"
2.114 + by (rule not_less_imp_not_eq1) (rule not_FF_less_TT)
2.115 +
2.116 +
2.117 +lemma COND_cases_iff [rule_format]:
2.118 + "ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))"
2.119 + apply (insert not_UU_eq_TT not_UU_eq_FF not_TT_eq_UU
2.120 + not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT)
2.121 + apply (rule tr_induct)
2.122 + apply (simplesubst COND_UU)
2.123 + apply blast
2.124 + apply (simplesubst COND_TT)
2.125 + apply blast
2.126 + apply (simplesubst COND_FF)
2.127 + apply blast
2.128 + done
2.129 +
2.130 +lemma COND_cases:
2.131 + "[| x = UU --> P(UU); x = TT --> P(xa); x = FF --> P(y) |] ==> P(x => xa | y)"
2.132 + apply (rule COND_cases_iff [THEN iffD2])
2.133 + apply blast
2.134 + done
2.135 +
2.136 +lemmas [simp] =
2.137 + minimal
2.138 + UU_app
2.139 + UU_app [THEN ap_thm]
2.140 + UU_app [THEN ap_thm, THEN ap_thm]
2.141 + not_TT_less_FF not_FF_less_TT not_TT_less_UU not_FF_less_UU not_UU_eq_TT
2.142 + not_UU_eq_FF not_TT_eq_UU not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT
2.143 + COND_UU COND_TT COND_FF
2.144 + surj_pairing FST SND
2.145
2.146
2.147 subsection {* Ordered pairs and products *}
2.148
2.149 -use "pair.ML"
2.150 +lemma expand_all_PROD: "(ALL p. P(p)) <-> (ALL x y. P(<x,y>))"
2.151 + apply (rule iffI)
2.152 + apply blast
2.153 + apply (rule allI)
2.154 + apply (rule surj_pairing [THEN subst])
2.155 + apply blast
2.156 + done
2.157 +
2.158 +lemma PROD_less: "(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)"
2.159 + apply (rule iffI)
2.160 + apply (rule conjI)
2.161 + apply (erule less_ap_term)
2.162 + apply (erule less_ap_term)
2.163 + apply (erule conjE)
2.164 + apply (rule surj_pairing [of p, THEN subst])
2.165 + apply (rule surj_pairing [of q, THEN subst])
2.166 + apply (rule mono, erule less_ap_term, assumption)
2.167 + done
2.168 +
2.169 +lemma PROD_eq: "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)"
2.170 + apply (rule iffI)
2.171 + apply simp
2.172 + apply (unfold eq_def)
2.173 + apply (simp add: PROD_less)
2.174 + done
2.175 +
2.176 +lemma PAIR_less [simp]: "<a,b> << <c,d> <-> a<<c & b<<d"
2.177 + by (simp add: PROD_less)
2.178 +
2.179 +lemma PAIR_eq [simp]: "<a,b> = <c,d> <-> a=c & b=d"
2.180 + by (simp add: PROD_eq)
2.181 +
2.182 +lemma UU_is_UU_UU [simp]: "<UU,UU> = UU"
2.183 + by (rule less_UU) (simp add: PROD_less)
2.184 +
2.185 +lemma FST_STRICT [simp]: "FST(UU) = UU"
2.186 + apply (rule subst [OF UU_is_UU_UU])
2.187 + apply (simp del: UU_is_UU_UU)
2.188 + done
2.189 +
2.190 +lemma SND_STRICT [simp]: "SND(UU) = UU"
2.191 + apply (rule subst [OF UU_is_UU_UU])
2.192 + apply (simp del: UU_is_UU_UU)
2.193 + done
2.194
2.195
2.196 subsection {* Fixedpoint theory *}
2.197
2.198 -use "fix.ML"
2.199 +lemma adm_eq: "adm(%x. t(x)=(u(x)::'a::cpo))"
2.200 + apply (unfold eq_def)
2.201 + apply (rule adm_conj adm_less)+
2.202 + done
2.203 +
2.204 +lemma adm_not_not: "adm(P) ==> adm(%x.~~P(x))"
2.205 + by simp
2.206 +
2.207 +lemma not_eq_TT: "ALL p. ~p=TT <-> (p=FF | p=UU)"
2.208 + and not_eq_FF: "ALL p. ~p=FF <-> (p=TT | p=UU)"
2.209 + and not_eq_UU: "ALL p. ~p=UU <-> (p=TT | p=FF)"
2.210 + by (rule tr_induct, simp_all)+
2.211 +
2.212 +lemma adm_not_eq_tr: "ALL p::tr. adm(%x. ~t(x)=p)"
2.213 + apply (rule tr_induct)
2.214 + apply (simp_all add: not_eq_TT not_eq_FF not_eq_UU)
2.215 + apply (rule adm_disj adm_eq)+
2.216 + done
2.217 +
2.218 +lemmas adm_lemmas =
2.219 + adm_not_free adm_eq adm_less adm_not_less
2.220 + adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
2.221 +
2.222 +
2.223 +ML {*
2.224 +local
2.225 + val adm_lemmas = thms "adm_lemmas"
2.226 + val induct = thm "induct"
2.227 +in
2.228 + fun induct_tac v i =
2.229 + res_inst_tac[("f",v)] induct i THEN REPEAT (resolve_tac adm_lemmas i)
2.230 +end
2.231 +*}
2.232 +
2.233 +lemma least_FIX: "f(p) = p ==> FIX(f) << p"
2.234 + apply (tactic {* induct_tac "f" 1 *})
2.235 + apply (rule minimal)
2.236 + apply (intro strip)
2.237 + apply (erule subst)
2.238 + apply (erule less_ap_term)
2.239 + done
2.240 +
2.241 +lemma lfp_is_FIX:
2.242 + assumes 1: "f(p) = p"
2.243 + and 2: "ALL q. f(q)=q --> p << q"
2.244 + shows "p = FIX(f)"
2.245 + apply (rule less_anti_sym)
2.246 + apply (rule 2 [THEN spec, THEN mp])
2.247 + apply (rule FIX_eq)
2.248 + apply (rule least_FIX)
2.249 + apply (rule 1)
2.250 + done
2.251 +
2.252 +
2.253 +lemma FIX_pair: "<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)"
2.254 + apply (rule lfp_is_FIX)
2.255 + apply (simp add: FIX_eq [of f] FIX_eq [of g])
2.256 + apply (intro strip)
2.257 + apply (simp add: PROD_less)
2.258 + apply (rule conjI)
2.259 + apply (rule least_FIX)
2.260 + apply (erule subst, rule FST [symmetric])
2.261 + apply (rule least_FIX)
2.262 + apply (erule subst, rule SND [symmetric])
2.263 + done
2.264 +
2.265 +lemma FIX1: "FIX(f) = FST(FIX(%p. <f(FST(p)),g(SND(p))>))"
2.266 + by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct1])
2.267 +
2.268 +lemma FIX2: "FIX(g) = SND(FIX(%p. <f(FST(p)),g(SND(p))>))"
2.269 + by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct2])
2.270 +
2.271 +lemma induct2:
2.272 + assumes 1: "adm(%p. P(FST(p),SND(p)))"
2.273 + and 2: "P(UU::'a,UU::'b)"
2.274 + and 3: "ALL x y. P(x,y) --> P(f(x),g(y))"
2.275 + shows "P(FIX(f),FIX(g))"
2.276 + apply (rule FIX1 [THEN ssubst, of _ f g])
2.277 + apply (rule FIX2 [THEN ssubst, of _ f g])
2.278 + apply (rule induct [OF 1, where ?f = "%x. <f(FST(x)),g(SND(x))>"])
2.279 + apply simp
2.280 + apply (rule 2)
2.281 + apply (simp add: expand_all_PROD)
2.282 + apply (rule 3)
2.283 + done
2.284 +
2.285 +ML {*
2.286 +local
2.287 + val induct2 = thm "induct2"
2.288 + val adm_lemmas = thms "adm_lemmas"
2.289 +in
2.290 +
2.291 +fun induct2_tac (f,g) i =
2.292 + res_inst_tac[("f",f),("g",g)] induct2 i THEN
2.293 + REPEAT(resolve_tac adm_lemmas i)
2.294
2.295 end
2.296 +*}
2.297 +
2.298 +end
3.1 --- a/src/LCF/LCF_lemmas.ML Thu Jun 01 21:14:54 2006 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,96 +0,0 @@
3.4 -(* Title: LCF/lcf.ML
3.5 - ID: $Id$
3.6 - Author: Tobias Nipkow
3.7 - Copyright 1992 University of Cambridge
3.8 -*)
3.9 -
3.10 -(* Standard abbreviations *)
3.11 -
3.12 -val rstac = resolve_tac;
3.13 -fun stac th = rtac(th RS sym RS subst);
3.14 -fun sstac ths = EVERY' (map stac ths);
3.15 -
3.16 -fun strip_tac i = REPEAT(rstac [impI,allI] i);
3.17 -
3.18 -bind_thm ("eq_imp_less1", prove_goal (the_context ()) "x=y ==> x << y"
3.19 - (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]));
3.20 -
3.21 -bind_thm ("eq_imp_less2", prove_goal (the_context ()) "x=y ==> y << x"
3.22 - (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]));
3.23 -
3.24 -bind_thm ("less_refl", refl RS eq_imp_less1);
3.25 -
3.26 -bind_thm ("less_anti_sym", prove_goal (the_context ()) "[| x << y; y << x |] ==> x=y"
3.27 - (fn prems => [rewtac eq_def,
3.28 - REPEAT(rstac(conjI::prems)1)]));
3.29 -
3.30 -bind_thm ("ext", prove_goal (the_context ())
3.31 - "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))"
3.32 - (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
3.33 - prem RS eq_imp_less1,
3.34 - prem RS eq_imp_less2]1)]));
3.35 -
3.36 -bind_thm ("cong", prove_goal (the_context ()) "[| f=g; x=y |] ==> f(x)=g(y)"
3.37 - (fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1,
3.38 - rtac refl 1]));
3.39 -
3.40 -bind_thm ("less_ap_term", less_refl RS mono);
3.41 -bind_thm ("less_ap_thm", less_refl RSN (2,mono));
3.42 -bind_thm ("ap_term", refl RS cong);
3.43 -bind_thm ("ap_thm", refl RSN (2,cong));
3.44 -
3.45 -bind_thm ("UU_abs", prove_goal (the_context ()) "(%x::'a::cpo. UU) = UU"
3.46 - (fn _ => [rtac less_anti_sym 1, rtac minimal 2,
3.47 - rtac less_ext 1, rtac allI 1, rtac minimal 1]));
3.48 -
3.49 -bind_thm ("UU_app", UU_abs RS sym RS ap_thm);
3.50 -
3.51 -bind_thm ("less_UU", prove_goal (the_context ()) "x << UU ==> x=UU"
3.52 - (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]));
3.53 -
3.54 -
3.55 -bind_thm ("tr_induct", prove_goal (the_context ()) "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)"
3.56 - (fn prems => [rtac allI 1, rtac mp 1,
3.57 - res_inst_tac[("p","b")]tr_cases 2,
3.58 - fast_tac (FOL_cs addIs prems) 1]));
3.59 -
3.60 -
3.61 -bind_thm ("Contrapos", prove_goal (the_context ()) "(A ==> B) ==> (~B ==> ~A)"
3.62 - (fn prems => [rtac notI 1, rtac notE 1, rstac prems 1,
3.63 - rstac prems 1, atac 1]));
3.64 -
3.65 -bind_thm ("not_less_imp_not_eq1", eq_imp_less1 COMP Contrapos);
3.66 -bind_thm ("not_less_imp_not_eq2", eq_imp_less2 COMP Contrapos);
3.67 -
3.68 -bind_thm ("not_UU_eq_TT", not_TT_less_UU RS not_less_imp_not_eq2);
3.69 -bind_thm ("not_UU_eq_FF", not_FF_less_UU RS not_less_imp_not_eq2);
3.70 -bind_thm ("not_TT_eq_UU", not_TT_less_UU RS not_less_imp_not_eq1);
3.71 -bind_thm ("not_TT_eq_FF", not_TT_less_FF RS not_less_imp_not_eq1);
3.72 -bind_thm ("not_FF_eq_UU", not_FF_less_UU RS not_less_imp_not_eq1);
3.73 -bind_thm ("not_FF_eq_TT", not_FF_less_TT RS not_less_imp_not_eq1);
3.74 -
3.75 -
3.76 -bind_thm ("COND_cases_iff", (prove_goal (the_context ())
3.77 - "ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))"
3.78 - (fn _ => [cut_facts_tac [not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,
3.79 - not_TT_eq_FF,not_FF_eq_UU,not_FF_eq_TT]1,
3.80 - rtac tr_induct 1, stac COND_UU 1, stac COND_TT 2,
3.81 - stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)])) RS spec);
3.82 -
3.83 -val lemma = prove_goal (the_context ()) "A<->B ==> B ==> A"
3.84 - (fn prems => [cut_facts_tac prems 1, rewtac iff_def,
3.85 - fast_tac FOL_cs 1]);
3.86 -
3.87 -bind_thm ("COND_cases", conjI RSN (2,conjI RS (COND_cases_iff RS lemma)));
3.88 -
3.89 -
3.90 -val LCF_ss = FOL_ss addsimps
3.91 - [minimal,
3.92 - UU_app, UU_app RS ap_thm, UU_app RS ap_thm RS ap_thm,
3.93 - not_TT_less_FF,not_FF_less_TT,not_TT_less_UU,not_FF_less_UU,
3.94 - not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,not_TT_eq_FF,
3.95 - not_FF_eq_UU,not_FF_eq_TT,
3.96 - COND_UU,COND_TT,COND_FF,
3.97 - surj_pairing,FST,SND];
3.98 -
3.99 -change_simpset (fn _ => LCF_ss);
4.1 --- a/src/LCF/fix.ML Thu Jun 01 21:14:54 2006 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,75 +0,0 @@
4.4 -(* Title: LCF/fix
4.5 - ID: $Id$
4.6 - Author: Tobias Nipkow
4.7 - Copyright 1992 University of Cambridge
4.8 -*)
4.9 -
4.10 -val adm_eq = prove_goal (the_context ()) "adm(%x. t(x)=(u(x)::'a::cpo))"
4.11 - (fn _ => [rewtac eq_def,
4.12 - REPEAT(rstac[adm_conj,adm_less]1)]);
4.13 -
4.14 -val adm_not_not = prove_goal (the_context ()) "adm(P) ==> adm(%x.~~P(x))"
4.15 - (fn prems => [simp_tac (LCF_ss addsimps prems) 1]);
4.16 -
4.17 -
4.18 -val tac = rtac tr_induct 1 THEN ALLGOALS (simp_tac LCF_ss);
4.19 -
4.20 -val not_eq_TT = prove_goal (the_context ()) "ALL p. ~p=TT <-> (p=FF | p=UU)"
4.21 - (fn _ => [tac]) RS spec;
4.22 -
4.23 -val not_eq_FF = prove_goal (the_context ()) "ALL p. ~p=FF <-> (p=TT | p=UU)"
4.24 - (fn _ => [tac]) RS spec;
4.25 -
4.26 -val not_eq_UU = prove_goal (the_context ()) "ALL p. ~p=UU <-> (p=TT | p=FF)"
4.27 - (fn _ => [tac]) RS spec;
4.28 -
4.29 -val adm_not_eq_tr = prove_goal (the_context ()) "ALL p::tr. adm(%x. ~t(x)=p)"
4.30 - (fn _ => [rtac tr_induct 1,
4.31 - REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN
4.32 - REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec;
4.33 -
4.34 -val adm_lemmas = [adm_not_free,adm_eq,adm_less,adm_not_less,adm_not_eq_tr,
4.35 - adm_conj,adm_disj,adm_imp,adm_all];
4.36 -
4.37 -fun induct_tac v i = res_inst_tac[("f",v)] induct i THEN
4.38 - REPEAT(rstac adm_lemmas i);
4.39 -
4.40 -
4.41 -val least_FIX = prove_goal (the_context ()) "f(p) = p ==> FIX(f) << p"
4.42 - (fn [prem] => [induct_tac "f" 1, rtac minimal 1, strip_tac 1,
4.43 - stac (prem RS sym) 1, etac less_ap_term 1]);
4.44 -
4.45 -val lfp_is_FIX = prove_goal (the_context ())
4.46 - "[| f(p) = p; ALL q. f(q)=q --> p << q |] ==> p = FIX(f)"
4.47 - (fn [prem1,prem2] => [rtac less_anti_sym 1,
4.48 - rtac (prem2 RS spec RS mp) 1, rtac FIX_eq 1,
4.49 - rtac least_FIX 1, rtac prem1 1]);
4.50 -
4.51 -val ffix = read_instantiate [("f","f::?'a=>?'a")] FIX_eq;
4.52 -val gfix = read_instantiate [("f","g::?'a=>?'a")] FIX_eq;
4.53 -val ss = LCF_ss addsimps [ffix,gfix];
4.54 -
4.55 -val FIX_pair = prove_goal (the_context ())
4.56 - "<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)"
4.57 - (fn _ => [rtac lfp_is_FIX 1, simp_tac ss 1,
4.58 - strip_tac 1, simp_tac (LCF_ss addsimps [PROD_less]) 1,
4.59 - rtac conjI 1, rtac least_FIX 1, etac subst 1, rtac (FST RS sym) 1,
4.60 - rtac least_FIX 1, etac subst 1, rtac (SND RS sym) 1]);
4.61 -
4.62 -val FIX_pair_conj = rewrite_rule (map mk_meta_eq [PROD_eq,FST,SND]) FIX_pair;
4.63 -
4.64 -val FIX1 = FIX_pair_conj RS conjunct1;
4.65 -val FIX2 = FIX_pair_conj RS conjunct2;
4.66 -
4.67 -val induct2 = prove_goal (the_context ())
4.68 - "[| adm(%p. P(FST(p),SND(p))); P(UU::'a,UU::'b);\
4.69 -\ ALL x y. P(x,y) --> P(f(x),g(y)) |] ==> P(FIX(f),FIX(g))"
4.70 - (fn prems => [EVERY1
4.71 - [res_inst_tac [("f","f"),("g","g")] (standard(FIX1 RS ssubst)),
4.72 - res_inst_tac [("f","f"),("g","g")] (standard(FIX2 RS ssubst)),
4.73 - res_inst_tac [("f","%x. <f(FST(x)),g(SND(x))>")] induct,
4.74 - rstac prems, simp_tac ss, rstac prems,
4.75 - simp_tac (LCF_ss addsimps [expand_all_PROD]), rstac prems]]);
4.76 -
4.77 -fun induct2_tac (f,g) i = res_inst_tac[("f",f),("g",g)] induct2 i THEN
4.78 - REPEAT(rstac adm_lemmas i);
5.1 --- a/src/LCF/pair.ML Thu Jun 01 21:14:54 2006 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,39 +0,0 @@
5.4 -(* Title: LCF/pair
5.5 - ID: $Id$
5.6 - Author: Tobias Nipkow
5.7 - Copyright 1992 University of Cambridge
5.8 -*)
5.9 -
5.10 -val expand_all_PROD = prove_goal (the_context ())
5.11 - "(ALL p. P(p)) <-> (ALL x y. P(<x,y>))"
5.12 - (fn _ => [rtac iffI 1, fast_tac FOL_cs 1, rtac allI 1,
5.13 - rtac (surj_pairing RS subst) 1, fast_tac FOL_cs 1]);
5.14 -
5.15 -local
5.16 -val ppair = read_instantiate [("z","p::'a*'b")] surj_pairing;
5.17 -val qpair = read_instantiate [("z","q::'a*'b")] surj_pairing;
5.18 -in
5.19 -val PROD_less = prove_goal (the_context ())
5.20 - "(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)"
5.21 - (fn _ => [EVERY1[rtac iffI,
5.22 - rtac conjI, etac less_ap_term, etac less_ap_term,
5.23 - rtac (ppair RS subst), rtac (qpair RS subst),
5.24 - etac conjE, rtac mono, etac less_ap_term, atac]]);
5.25 -end;
5.26 -
5.27 -val PROD_eq = prove_goal (the_context ()) "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)"
5.28 - (fn _ => [rtac iffI 1, asm_simp_tac LCF_ss 1,
5.29 - rewtac eq_def,
5.30 - asm_simp_tac (LCF_ss addsimps [PROD_less]) 1]);
5.31 -
5.32 -val PAIR_less = prove_goal (the_context ()) "<a,b> << <c,d> <-> a<<c & b<<d"
5.33 - (fn _ => [simp_tac (LCF_ss addsimps [PROD_less])1]);
5.34 -
5.35 -val PAIR_eq = prove_goal (the_context ()) "<a,b> = <c,d> <-> a=c & b=d"
5.36 - (fn _ => [simp_tac (LCF_ss addsimps [PROD_eq])1]);
5.37 -
5.38 -val UU_is_UU_UU = prove_goal (the_context ()) "<UU,UU> << UU"
5.39 - (fn _ => [simp_tac (LCF_ss addsimps [PROD_less]) 1])
5.40 - RS less_UU RS sym;
5.41 -
5.42 -val LCF_ss = LCF_ss addsimps [PAIR_less,PAIR_eq,UU_is_UU_UU];