--- 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;
-
--- 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 "<FST(z),SND(z)> = z"
+ surj_pairing: "<FST(z),SND(z)> = z"
- FST "FST(<x,y>) = x"
- SND "SND(<x,y>) = y"
+ FST: "FST(<x,y>) = x"
+ SND: "SND(<x,y>) = 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
--- /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];
--- 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);
--- 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
--- 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
--- 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";
-
--- 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
--- 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);
--- 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
--- 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(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(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;
--- 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
--- 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(<x,y>))"
(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,b> << <c,d> <-> a<<c & b<<d"
+val PAIR_less = prove_goal (the_context ()) "<a,b> << <c,d> <-> a<<c & b<<d"
(fn _ => [simp_tac (LCF_ss addsimps [PROD_less])1]);
-val PAIR_eq = prove_goal LCF.thy "<a,b> = <c,d> <-> a=c & b=d"
+val PAIR_eq = prove_goal (the_context ()) "<a,b> = <c,d> <-> a=c & b=d"
(fn _ => [simp_tac (LCF_ss addsimps [PROD_eq])1]);
-val UU_is_UU_UU = prove_goal LCF.thy "<UU,UU> << UU"
+val UU_is_UU_UU = prove_goal (the_context ()) "<UU,UU> << UU"
(fn _ => [simp_tac (LCF_ss addsimps [PROD_less]) 1])
RS less_UU RS sym;
--- 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
--- 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];