# HG changeset patch # User wenzelm # Date 1125762850 -7200 # Node ID 81bf91654e73246c8e92d4231a9a2edb4321f786 # Parent 6927a62c77dc3e805b0230df5e83d09b748911f1 converted to Isar theory format; diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/LCF.ML --- a/src/LCF/LCF.ML Sat Sep 03 17:54:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,129 +0,0 @@ -(* Title: LCF/lcf.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1992 University of Cambridge - -For lcf.thy. Basic lemmas about LCF -*) - -open LCF; - -signature LCF_LEMMAS = -sig - val ap_term: thm - val ap_thm: thm - val COND_cases: thm - val COND_cases_iff: thm - val Contrapos: thm - val cong: thm - val ext: thm - val eq_imp_less1: thm - val eq_imp_less2: thm - val less_anti_sym: thm - val less_ap_term: thm - val less_ap_thm: thm - val less_refl: thm - val less_UU: thm - val not_UU_eq_TT: thm - val not_UU_eq_FF: thm - val not_TT_eq_UU: thm - val not_TT_eq_FF: thm - val not_FF_eq_UU: thm - val not_FF_eq_TT: thm - val rstac: thm list -> int -> tactic - val stac: thm -> int -> tactic - val sstac: thm list -> int -> tactic - val strip_tac: int -> tactic - val tr_induct: thm - val UU_abs: thm - val UU_app: thm -end; - - -structure LCF_Lemmas : LCF_LEMMAS = - -struct - -(* Standard abbreviations *) - -val rstac = resolve_tac; -fun stac th = rtac(th RS sym RS subst); -fun sstac ths = EVERY' (map stac ths); - -fun strip_tac i = REPEAT(rstac [impI,allI] i); - -val eq_imp_less1 = prove_goal thy "x=y ==> x << y" - (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]); - -val eq_imp_less2 = prove_goal thy "x=y ==> y << x" - (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]); - -val less_refl = refl RS eq_imp_less1; - -val less_anti_sym = prove_goal thy "[| x << y; y << x |] ==> x=y" - (fn prems => [rewtac eq_def, - REPEAT(rstac(conjI::prems)1)]); - -val ext = prove_goal thy - "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))" - (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI, - prem RS eq_imp_less1, - prem RS eq_imp_less2]1)]); - -val cong = prove_goal thy "[| f=g; x=y |] ==> f(x)=g(y)" - (fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1, - rtac refl 1]); - -val less_ap_term = less_refl RS mono; -val less_ap_thm = less_refl RSN (2,mono); -val ap_term = refl RS cong; -val ap_thm = refl RSN (2,cong); - -val UU_abs = prove_goal thy "(%x::'a::cpo. UU) = UU" - (fn _ => [rtac less_anti_sym 1, rtac minimal 2, - rtac less_ext 1, rtac allI 1, rtac minimal 1]); - -val UU_app = UU_abs RS sym RS ap_thm; - -val less_UU = prove_goal thy "x << UU ==> x=UU" - (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]); - - -val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)" - (fn prems => [rtac allI 1, rtac mp 1, - res_inst_tac[("p","b")]tr_cases 2, - fast_tac (FOL_cs addIs prems) 1]); - - -val Contrapos = prove_goal thy "(A ==> B) ==> (~B ==> ~A)" - (fn prems => [rtac notI 1, rtac notE 1, rstac prems 1, - rstac prems 1, atac 1]); - -val not_less_imp_not_eq1 = eq_imp_less1 COMP Contrapos; -val not_less_imp_not_eq2 = eq_imp_less2 COMP Contrapos; - -val not_UU_eq_TT = not_TT_less_UU RS not_less_imp_not_eq2; -val not_UU_eq_FF = not_FF_less_UU RS not_less_imp_not_eq2; -val not_TT_eq_UU = not_TT_less_UU RS not_less_imp_not_eq1; -val not_TT_eq_FF = not_TT_less_FF RS not_less_imp_not_eq1; -val not_FF_eq_UU = not_FF_less_UU RS not_less_imp_not_eq1; -val not_FF_eq_TT = not_FF_less_TT RS not_less_imp_not_eq1; - - -val COND_cases_iff = (prove_goal thy - "ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))" - (fn _ => [cut_facts_tac [not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU, - not_TT_eq_FF,not_FF_eq_UU,not_FF_eq_TT]1, - rtac tr_induct 1, stac COND_UU 1, stac COND_TT 2, - stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)])) RS spec; - -val lemma = prove_goal thy "A<->B ==> B ==> A" - (fn prems => [cut_facts_tac prems 1, rewtac iff_def, - fast_tac FOL_cs 1]); - -val COND_cases = conjI RSN (2,conjI RS (COND_cases_iff RS lemma)); - -end; - -open LCF_Lemmas; - diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/LCF.thy --- a/src/LCF/LCF.thy Sat Sep 03 17:54:07 2005 +0200 +++ b/src/LCF/LCF.thy Sat Sep 03 17:54:10 2005 +0200 @@ -2,29 +2,38 @@ ID: $Id$ Author: Tobias Nipkow Copyright 1992 University of Cambridge - -Natural Deduction Rules for LCF *) -LCF = FOL + +header {* LCF on top of First-Order Logic *} -classes cpo < term +theory LCF +imports FOL +uses ("pair.ML") ("fix.ML") +begin -default cpo +text {* This theory is based on Lawrence Paulson's book Logic and Computation. *} -types - tr - void - ('a,'b) "*" (infixl 6) - ('a,'b) "+" (infixl 5) +subsection {* Natural Deduction Rules for LCF *} + +classes cpo < "term" +defaultsort cpo + +typedecl tr +typedecl void +typedecl ('a,'b) "*" (infixl 6) +typedecl ('a,'b) "+" (infixl 5) arities - fun, "*", "+" :: (cpo,cpo)cpo - tr,void :: cpo + fun :: (cpo, cpo) cpo + "*" :: (cpo, cpo) cpo + "+" :: (cpo, cpo) cpo + tr :: cpo + void :: cpo consts UU :: "'a" - TT,FF :: "tr" + TT :: "tr" + FF :: "tr" FIX :: "('a => 'a) => 'a" FST :: "'a*'b => 'a" SND :: "'a*'b => 'b" @@ -36,75 +45,91 @@ PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100) COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60) "<<" :: "['a,'a] => o" (infixl 50) -rules + +axioms (** DOMAIN THEORY **) - eq_def "x=y == x << y & y << x" + eq_def: "x=y == x << y & y << x" - less_trans "[| x << y; y << z |] ==> x << z" + less_trans: "[| x << y; y << z |] ==> x << z" - less_ext "(ALL x. f(x) << g(x)) ==> f << g" + less_ext: "(ALL x. f(x) << g(x)) ==> f << g" - mono "[| f << g; x << y |] ==> f(x) << g(y)" + mono: "[| f << g; x << y |] ==> f(x) << g(y)" - minimal "UU << x" + minimal: "UU << x" - FIX_eq "f(FIX(f)) = FIX(f)" + FIX_eq: "f(FIX(f)) = FIX(f)" (** TR **) - tr_cases "p=UU | p=TT | p=FF" + tr_cases: "p=UU | p=TT | p=FF" - not_TT_less_FF "~ TT << FF" - not_FF_less_TT "~ FF << TT" - not_TT_less_UU "~ TT << UU" - not_FF_less_UU "~ FF << UU" + not_TT_less_FF: "~ TT << FF" + not_FF_less_TT: "~ FF << TT" + not_TT_less_UU: "~ TT << UU" + not_FF_less_UU: "~ FF << UU" - COND_UU "UU => x | y = UU" - COND_TT "TT => x | y = x" - COND_FF "FF => x | y = y" + COND_UU: "UU => x | y = UU" + COND_TT: "TT => x | y = x" + COND_FF: "FF => x | y = y" (** PAIRS **) - surj_pairing " = z" + surj_pairing: " = z" - FST "FST() = x" - SND "SND() = y" + FST: "FST() = x" + SND: "SND() = y" (*** STRICT SUM ***) - INL_DEF "~x=UU ==> ~INL(x)=UU" - INR_DEF "~x=UU ==> ~INR(x)=UU" + INL_DEF: "~x=UU ==> ~INL(x)=UU" + INR_DEF: "~x=UU ==> ~INR(x)=UU" - INL_STRICT "INL(UU) = UU" - INR_STRICT "INR(UU) = UU" + INL_STRICT: "INL(UU) = UU" + INR_STRICT: "INR(UU) = UU" - WHEN_UU "WHEN(f,g,UU) = UU" - WHEN_INL "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" - WHEN_INR "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" + WHEN_UU: "WHEN(f,g,UU) = UU" + WHEN_INL: "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" + WHEN_INR: "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" - SUM_EXHAUSTION + SUM_EXHAUSTION: "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))" (** VOID **) - void_cases "(x::void) = UU" + void_cases: "(x::void) = UU" (** INDUCTION **) - induct "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))" + induct: "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))" (** Admissibility / Chain Completeness **) (* All rules can be found on pages 199--200 of Larry's LCF book. Note that "easiness" of types is not taken into account because it cannot be expressed schematically; flatness could be. *) - adm_less "adm(%x. t(x) << u(x))" - adm_not_less "adm(%x.~ t(x) << u)" - adm_not_free "adm(%x. A)" - adm_subst "adm(P) ==> adm(%x. P(t(x)))" - adm_conj "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))" - adm_disj "[| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))" - adm_imp "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))" - adm_all "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))" + adm_less: "adm(%x. t(x) << u(x))" + adm_not_less: "adm(%x.~ t(x) << u)" + adm_not_free: "adm(%x. A)" + adm_subst: "adm(P) ==> adm(%x. P(t(x)))" + adm_conj: "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))" + adm_disj: "[| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))" + adm_imp: "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))" + adm_all: "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))" + +ML {* use_legacy_bindings (the_context ()) *} + +use "LCF_lemmas.ML" + + +subsection {* Ordered pairs and products *} + +use "pair.ML" + + +subsection {* Fixedpoint theory *} + +use "fix.ML" + end diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/LCF_lemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LCF/LCF_lemmas.ML Sat Sep 03 17:54:10 2005 +0200 @@ -0,0 +1,94 @@ +(* Title: LCF/lcf.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1992 University of Cambridge +*) + +(* Standard abbreviations *) + +val rstac = resolve_tac; +fun stac th = rtac(th RS sym RS subst); +fun sstac ths = EVERY' (map stac ths); + +fun strip_tac i = REPEAT(rstac [impI,allI] i); + +val eq_imp_less1 = prove_goal (the_context ()) "x=y ==> x << y" + (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]); + +val eq_imp_less2 = prove_goal (the_context ()) "x=y ==> y << x" + (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]); + +val less_refl = refl RS eq_imp_less1; + +val less_anti_sym = prove_goal (the_context ()) "[| x << y; y << x |] ==> x=y" + (fn prems => [rewtac eq_def, + REPEAT(rstac(conjI::prems)1)]); + +val ext = prove_goal (the_context ()) + "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))" + (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI, + prem RS eq_imp_less1, + prem RS eq_imp_less2]1)]); + +val cong = prove_goal (the_context ()) "[| f=g; x=y |] ==> f(x)=g(y)" + (fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1, + rtac refl 1]); + +val less_ap_term = less_refl RS mono; +val less_ap_thm = less_refl RSN (2,mono); +val ap_term = refl RS cong; +val ap_thm = refl RSN (2,cong); + +val UU_abs = prove_goal (the_context ()) "(%x::'a::cpo. UU) = UU" + (fn _ => [rtac less_anti_sym 1, rtac minimal 2, + rtac less_ext 1, rtac allI 1, rtac minimal 1]); + +val UU_app = UU_abs RS sym RS ap_thm; + +val less_UU = prove_goal (the_context ()) "x << UU ==> x=UU" + (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]); + + +val tr_induct = prove_goal (the_context ()) "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)" + (fn prems => [rtac allI 1, rtac mp 1, + res_inst_tac[("p","b")]tr_cases 2, + fast_tac (FOL_cs addIs prems) 1]); + + +val Contrapos = prove_goal (the_context ()) "(A ==> B) ==> (~B ==> ~A)" + (fn prems => [rtac notI 1, rtac notE 1, rstac prems 1, + rstac prems 1, atac 1]); + +val not_less_imp_not_eq1 = eq_imp_less1 COMP Contrapos; +val not_less_imp_not_eq2 = eq_imp_less2 COMP Contrapos; + +val not_UU_eq_TT = not_TT_less_UU RS not_less_imp_not_eq2; +val not_UU_eq_FF = not_FF_less_UU RS not_less_imp_not_eq2; +val not_TT_eq_UU = not_TT_less_UU RS not_less_imp_not_eq1; +val not_TT_eq_FF = not_TT_less_FF RS not_less_imp_not_eq1; +val not_FF_eq_UU = not_FF_less_UU RS not_less_imp_not_eq1; +val not_FF_eq_TT = not_FF_less_TT RS not_less_imp_not_eq1; + + +val COND_cases_iff = (prove_goal (the_context ()) + "ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))" + (fn _ => [cut_facts_tac [not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU, + not_TT_eq_FF,not_FF_eq_UU,not_FF_eq_TT]1, + rtac tr_induct 1, stac COND_UU 1, stac COND_TT 2, + stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)])) RS spec; + +val lemma = prove_goal (the_context ()) "A<->B ==> B ==> A" + (fn prems => [cut_facts_tac prems 1, rewtac iff_def, + fast_tac FOL_cs 1]); + +val COND_cases = conjI RSN (2,conjI RS (COND_cases_iff RS lemma)); + + +val LCF_ss = FOL_ss addsimps + [minimal, + UU_app, UU_app RS ap_thm, UU_app RS ap_thm RS ap_thm, + not_TT_less_FF,not_FF_less_TT,not_TT_less_UU,not_FF_less_UU, + not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,not_TT_eq_FF, + not_FF_eq_UU,not_FF_eq_TT, + COND_UU,COND_TT,COND_FF, + surj_pairing,FST,SND]; diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/ex/Ex1.ML --- a/src/LCF/ex/Ex1.ML Sat Sep 03 17:54:07 2005 +0200 +++ b/src/LCF/ex/Ex1.ML Sat Sep 03 17:54:10 2005 +0200 @@ -3,13 +3,13 @@ Addsimps [P_strict,K]; -val H_unfold = prove_goal thy "H = K(H)" +val H_unfold = prove_goal (the_context ()) "H = K(H)" (fn _ => [stac H 1, rtac (FIX_eq RS sym) 1]); bind_thm ("H_unfold", H_unfold); -val H_strict = prove_goal thy "H(UU)=UU" +val H_strict = prove_goal (the_context ()) "H(UU)=UU" (fn _ => [stac H_unfold 1, Simp_tac 1]); bind_thm ("H_strict", H_strict); diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/ex/Ex1.thy --- a/src/LCF/ex/Ex1.thy Sat Sep 03 17:54:07 2005 +0200 +++ b/src/LCF/ex/Ex1.thy Sat Sep 03 17:54:10 2005 +0200 @@ -1,17 +1,23 @@ -(*** Section 10.4 ***) +(* $Id$ *) + +header {* Section 10.4 *} -Ex1 = LCF + +theory Ex1 +imports LCF +begin consts - P :: "'a => tr" - G :: "'a => 'a" - H :: "'a => 'a" - K :: "('a => 'a) => ('a => 'a)" + P :: "'a => tr" + G :: "'a => 'a" + H :: "'a => 'a" + K :: "('a => 'a) => ('a => 'a)" -rules - P_strict "P(UU) = UU" - K "K = (%h x. P(x) => x | h(h(G(x))))" - H "H = FIX(K)" +axioms + P_strict: "P(UU) = UU" + K: "K = (%h x. P(x) => x | h(h(G(x))))" + H: "H = FIX(K)" + +ML {* use_legacy_bindings (the_context ()) *} end diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/ex/Ex2.thy --- a/src/LCF/ex/Ex2.thy Sat Sep 03 17:54:07 2005 +0200 +++ b/src/LCF/ex/Ex2.thy Sat Sep 03 17:54:10 2005 +0200 @@ -1,18 +1,24 @@ -(*** Example 3.8 ***) +(* $Id$ *) + +header {* Example 3.8 *} -Ex2 = LCF + +theory Ex2 +imports LCF +begin consts - P :: "'a => tr" - F :: "'a => 'a" - G :: "'a => 'a" - H :: "'a => 'b => 'b" - K :: "('a => 'b => 'b) => ('a => 'b => 'b)" + P :: "'a => tr" + F :: "'a => 'a" + G :: "'a => 'a" + H :: "'a => 'b => 'b" + K :: "('a => 'b => 'b) => ('a => 'b => 'b)" -rules - F_strict "F(UU) = UU" - K "K = (%h x y. P(x) => y | F(h(G(x),y)))" - H "H = FIX(K)" +axioms + F_strict: "F(UU) = UU" + K: "K = (%h x y. P(x) => y | F(h(G(x),y)))" + H: "H = FIX(K)" + +ML {* use_legacy_bindings (the_context ()) *} end diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/ex/Ex3.ML --- a/src/LCF/ex/Ex3.ML Sat Sep 03 17:54:07 2005 +0200 +++ b/src/LCF/ex/Ex3.ML Sat Sep 03 17:54:10 2005 +0200 @@ -8,4 +8,3 @@ by (Simp_tac 1); by (Simp_tac 1); qed "example"; - diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/ex/Ex3.thy --- a/src/LCF/ex/Ex3.thy Sat Sep 03 17:54:07 2005 +0200 +++ b/src/LCF/ex/Ex3.thy Sat Sep 03 17:54:10 2005 +0200 @@ -1,14 +1,20 @@ -(*** Addition with fixpoint of successor ***) +(* $Id$ *) + +header {* Addition with fixpoint of successor *} -Ex3 = LCF + +theory Ex3 +imports LCF +begin consts - s :: "'a => 'a" - p :: "'a => 'a => 'a" + s :: "'a => 'a" + p :: "'a => 'a => 'a" -rules - p_strict "p(UU) = UU" - p_s "p(s(x),y) = s(p(x,y))" +axioms + p_strict: "p(UU) = UU" + p_s: "p(s(x),y) = s(p(x,y))" + +ML {* use_legacy_bindings (the_context ()) *} end diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/ex/Ex4.ML --- a/src/LCF/ex/Ex4.ML Sat Sep 03 17:54:07 2005 +0200 +++ b/src/LCF/ex/Ex4.ML Sat Sep 03 17:54:10 2005 +0200 @@ -1,5 +1,5 @@ -val asms = goal thy "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p"; +val asms = goal (the_context ()) "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p"; by (rewtac eq_def); by (rtac conjI 1); by (induct_tac "f" 1); diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/ex/Ex4.thy --- a/src/LCF/ex/Ex4.thy Sat Sep 03 17:54:07 2005 +0200 +++ b/src/LCF/ex/Ex4.thy Sat Sep 03 17:54:10 2005 +0200 @@ -1,4 +1,8 @@ -(*** Prefixpoints ***) +header {* Prefixpoints *} -Ex4 = LCF +theory Ex4 +imports LCF +begin + +end diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/fix.ML --- a/src/LCF/fix.ML Sat Sep 03 17:54:07 2005 +0200 +++ b/src/LCF/fix.ML Sat Sep 03 17:54:10 2005 +0200 @@ -2,46 +2,28 @@ ID: $Id$ Author: Tobias Nipkow Copyright 1992 University of Cambridge - -Fixedpoint theory *) -signature FIX = -sig - val adm_eq: thm - val adm_not_eq_tr: thm - val adm_not_not: thm - val not_eq_TT: thm - val not_eq_FF: thm - val not_eq_UU: thm - val induct2: thm - val induct_tac: string -> int -> tactic - val induct2_tac: string*string -> int -> tactic -end; - -structure Fix:FIX = -struct - -val adm_eq = prove_goal LCF.thy "adm(%x. t(x)=(u(x)::'a::cpo))" +val adm_eq = prove_goal (the_context ()) "adm(%x. t(x)=(u(x)::'a::cpo))" (fn _ => [rewtac eq_def, REPEAT(rstac[adm_conj,adm_less]1)]); -val adm_not_not = prove_goal LCF.thy "adm(P) ==> adm(%x.~~P(x))" +val adm_not_not = prove_goal (the_context ()) "adm(P) ==> adm(%x.~~P(x))" (fn prems => [simp_tac (LCF_ss addsimps prems) 1]); -val tac = rtac tr_induct 1 THEN REPEAT(simp_tac LCF_ss 1); +val tac = rtac tr_induct 1 THEN ALLGOALS (simp_tac LCF_ss); -val not_eq_TT = prove_goal LCF.thy "ALL p. ~p=TT <-> (p=FF | p=UU)" +val not_eq_TT = prove_goal (the_context ()) "ALL p. ~p=TT <-> (p=FF | p=UU)" (fn _ => [tac]) RS spec; -val not_eq_FF = prove_goal LCF.thy "ALL p. ~p=FF <-> (p=TT | p=UU)" +val not_eq_FF = prove_goal (the_context ()) "ALL p. ~p=FF <-> (p=TT | p=UU)" (fn _ => [tac]) RS spec; -val not_eq_UU = prove_goal LCF.thy "ALL p. ~p=UU <-> (p=TT | p=FF)" +val not_eq_UU = prove_goal (the_context ()) "ALL p. ~p=UU <-> (p=TT | p=FF)" (fn _ => [tac]) RS spec; -val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr. adm(%x. ~t(x)=p)" +val adm_not_eq_tr = prove_goal (the_context ()) "ALL p::tr. adm(%x. ~t(x)=p)" (fn _ => [rtac tr_induct 1, REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec; @@ -53,11 +35,11 @@ REPEAT(rstac adm_lemmas i); -val least_FIX = prove_goal LCF.thy "f(p) = p ==> FIX(f) << p" +val least_FIX = prove_goal (the_context ()) "f(p) = p ==> FIX(f) << p" (fn [prem] => [induct_tac "f" 1, rtac minimal 1, strip_tac 1, stac (prem RS sym) 1, etac less_ap_term 1]); -val lfp_is_FIX = prove_goal LCF.thy +val lfp_is_FIX = prove_goal (the_context ()) "[| f(p) = p; ALL q. f(q)=q --> p << q |] ==> p = FIX(f)" (fn [prem1,prem2] => [rtac less_anti_sym 1, rtac (prem2 RS spec RS mp) 1, rtac FIX_eq 1, @@ -67,7 +49,7 @@ val gfix = read_instantiate [("f","g::?'a=>?'a")] FIX_eq; val ss = LCF_ss addsimps [ffix,gfix]; -val FIX_pair = prove_goal LCF.thy +val FIX_pair = prove_goal (the_context ()) " = FIX(%p.)" (fn _ => [rtac lfp_is_FIX 1, simp_tac ss 1, strip_tac 1, simp_tac (LCF_ss addsimps [PROD_less]) 1, @@ -79,7 +61,7 @@ val FIX1 = FIX_pair_conj RS conjunct1; val FIX2 = FIX_pair_conj RS conjunct2; -val induct2 = prove_goal LCF.thy +val induct2 = prove_goal (the_context ()) "[| adm(%p. P(FST(p),SND(p))); P(UU::'a,UU::'b);\ \ ALL x y. P(x,y) --> P(f(x),g(y)) |] ==> P(FIX(f),FIX(g))" (fn prems => [EVERY1 @@ -91,7 +73,3 @@ fun induct2_tac (f,g) i = res_inst_tac[("f",f),("g",g)] induct2 i THEN REPEAT(rstac adm_lemmas i); - -end; - -open Fix; diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/fix.thy --- a/src/LCF/fix.thy Sat Sep 03 17:54:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ - -fix = LCF diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/pair.ML --- a/src/LCF/pair.ML Sat Sep 03 17:54:07 2005 +0200 +++ b/src/LCF/pair.ML Sat Sep 03 17:54:10 2005 +0200 @@ -2,11 +2,9 @@ ID: $Id$ Author: Tobias Nipkow Copyright 1992 University of Cambridge - -Theory of ordered pairs and products *) -val expand_all_PROD = prove_goal LCF.thy +val expand_all_PROD = prove_goal (the_context ()) "(ALL p. P(p)) <-> (ALL x y. P())" (fn _ => [rtac iffI 1, fast_tac FOL_cs 1, rtac allI 1, rtac (surj_pairing RS subst) 1, fast_tac FOL_cs 1]); @@ -15,7 +13,7 @@ val ppair = read_instantiate [("z","p::'a*'b")] surj_pairing; val qpair = read_instantiate [("z","q::'a*'b")] surj_pairing; in -val PROD_less = prove_goal LCF.thy +val PROD_less = prove_goal (the_context ()) "(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)" (fn _ => [EVERY1[rtac iffI, rtac conjI, etac less_ap_term, etac less_ap_term, @@ -23,18 +21,18 @@ etac conjE, rtac mono, etac less_ap_term, atac]]); end; -val PROD_eq = prove_goal LCF.thy "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)" +val PROD_eq = prove_goal (the_context ()) "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)" (fn _ => [rtac iffI 1, asm_simp_tac LCF_ss 1, rewtac eq_def, asm_simp_tac (LCF_ss addsimps [PROD_less]) 1]); -val PAIR_less = prove_goal LCF.thy " << <-> a< << <-> a< [simp_tac (LCF_ss addsimps [PROD_less])1]); -val PAIR_eq = prove_goal LCF.thy " = <-> a=c & b=d" +val PAIR_eq = prove_goal (the_context ()) " = <-> a=c & b=d" (fn _ => [simp_tac (LCF_ss addsimps [PROD_eq])1]); -val UU_is_UU_UU = prove_goal LCF.thy " << UU" +val UU_is_UU_UU = prove_goal (the_context ()) " << UU" (fn _ => [simp_tac (LCF_ss addsimps [PROD_less]) 1]) RS less_UU RS sym; diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/pair.thy --- a/src/LCF/pair.thy Sat Sep 03 17:54:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ - -pair = LCF diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/simpdata.ML --- a/src/LCF/simpdata.ML Sat Sep 03 17:54:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -(* Title: LCF/simpdata - ID: $Id$ - Author: Tobias Nipkow, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Simplification data for LCF -*) - -val LCF_ss = FOL_ss addsimps - [minimal, - UU_app, UU_app RS ap_thm, UU_app RS ap_thm RS ap_thm, - not_TT_less_FF,not_FF_less_TT,not_TT_less_UU,not_FF_less_UU, - not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,not_TT_eq_FF, - not_FF_eq_UU,not_FF_eq_TT, - COND_UU,COND_TT,COND_FF, - surj_pairing,FST,SND];