--- a/src/HOLCF/cfun1.thy Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(* Title: HOLCF/cfun1.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Definition of the type -> of continuous functions
-
-*)
-
-Cfun1 = Cont +
-
-
-(* new type of continuous functions *)
-
-types "->" 2 (infixr 5)
-
-arities "->" :: (pcpo,pcpo)term (* No properties for ->'s range *)
-
-consts
- Cfun :: "('a => 'b)set"
- fapp :: "('a -> 'b)=>('a => 'b)" ("(_[_])" [11,0] 1000)
- (* usually Rep_Cfun *)
- (* application *)
-
- fabs :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10)
- (* usually Abs_Cfun *)
- (* abstraction *)
-
- less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
-
-rules
-
- Cfun_def "Cfun == {f. contX(f)}"
-
- (*faking a type definition... *)
- (* -> is isomorphic to Cfun *)
-
- Rep_Cfun "fapp(fo):Cfun"
- Rep_Cfun_inverse "fabs(fapp(fo)) = fo"
- Abs_Cfun_inverse "f:Cfun ==> fapp(fabs(f))=f"
-
- (*defining the abstract constants*)
- less_cfun_def "less_cfun(fo1,fo2) == ( fapp(fo1) << fapp(fo2) )"
-
-end
--- a/src/HOLCF/cfun2.ML Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,276 +0,0 @@
-(* Title: HOLCF/cfun2.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Lemmas for cfun2.thy
-*)
-
-open Cfun2;
-
-(* ------------------------------------------------------------------------ *)
-(* access to less_cfun in class po *)
-(* ------------------------------------------------------------------------ *)
-
-val less_cfun = prove_goal Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
-(fn prems =>
- [
- (rtac (inst_cfun_po RS ssubst) 1),
- (fold_goals_tac [less_cfun_def]),
- (rtac refl 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* Type 'a ->'b is pointed *)
-(* ------------------------------------------------------------------------ *)
-
-val minimal_cfun = prove_goalw Cfun2.thy [UU_cfun_def] "UU_cfun << f"
-(fn prems =>
- [
- (rtac (less_cfun RS ssubst) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
- (rtac contX_const 1),
- (fold_goals_tac [UU_fun_def]),
- (rtac minimal_fun 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* fapp yields continuous functions in 'a => 'b *)
-(* this is continuity of fapp in its 'second' argument *)
-(* contX_fapp2 ==> monofun_fapp2 & contlub_fapp2 *)
-(* ------------------------------------------------------------------------ *)
-
-val contX_fapp2 = prove_goal Cfun2.thy "contX(fapp(fo))"
-(fn prems =>
- [
- (res_inst_tac [("P","contX")] CollectD 1),
- (fold_goals_tac [Cfun_def]),
- (rtac Rep_Cfun 1)
- ]);
-
-val monofun_fapp2 = contX_fapp2 RS contX2mono;
-(* monofun(fapp(?fo1)) *)
-
-
-val contlub_fapp2 = contX_fapp2 RS contX2contlub;
-(* contlub(fapp(?fo1)) *)
-
-(* ------------------------------------------------------------------------ *)
-(* expanded thms contX_fapp2, contlub_fapp2 *)
-(* looks nice with mixfix syntac _[_] *)
-(* ------------------------------------------------------------------------ *)
-
-val contX_cfun_arg = (contX_fapp2 RS contXE RS spec RS mp);
-(* is_chain(?x1) ==> range(%i. ?fo3[?x1(i)]) <<| ?fo3[lub(range(?x1))] *)
-
-val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp);
-(* is_chain(?x1) ==> ?fo4[lub(range(?x1))] = lub(range(%i. ?fo4[?x1(i)])) *)
-
-
-
-(* ------------------------------------------------------------------------ *)
-(* fapp is monotone in its 'first' argument *)
-(* ------------------------------------------------------------------------ *)
-
-val monofun_fapp1 = prove_goalw Cfun2.thy [monofun] "monofun(fapp)"
-(fn prems =>
- [
- (strip_tac 1),
- (etac (less_cfun RS subst) 1)
- ]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* monotonicity of application fapp in mixfix syntax [_]_ *)
-(* ------------------------------------------------------------------------ *)
-
-val monofun_cfun_fun = prove_goal Cfun2.thy "f1 << f2 ==> f1[x] << f2[x]"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("x","x")] spec 1),
- (rtac (less_fun RS subst) 1),
- (etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1)
- ]);
-
-
-val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
-(* ?x2 << ?x1 ==> ?fo5[?x2] << ?fo5[?x1] *)
-
-(* ------------------------------------------------------------------------ *)
-(* monotonicity of fapp in both arguments in mixfix syntax [_]_ *)
-(* ------------------------------------------------------------------------ *)
-
-val monofun_cfun = prove_goal Cfun2.thy
- "[|f1<<f2;x1<<x2|] ==> f1[x1] << f2[x2]"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac trans_less 1),
- (etac monofun_cfun_arg 1),
- (etac monofun_cfun_fun 1)
- ]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* ch2ch - rules for the type 'a -> 'b *)
-(* use MF2 lemmas from Cont.ML *)
-(* ------------------------------------------------------------------------ *)
-
-val ch2ch_fappR = prove_goal Cfun2.thy
- "is_chain(Y) ==> is_chain(%i. f[Y(i)])"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac (monofun_fapp2 RS ch2ch_MF2R) 1)
- ]);
-
-
-val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
-(* is_chain(?F) ==> is_chain(%i. ?F(i)[?x]) *)
-
-
-(* ------------------------------------------------------------------------ *)
-(* the lub of a chain of continous functions is monotone *)
-(* use MF2 lemmas from Cont.ML *)
-(* ------------------------------------------------------------------------ *)
-
-val lub_cfun_mono = prove_goal Cfun2.thy
- "is_chain(F) ==> monofun(% x.lub(range(% j.F(j)[x])))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac lub_MF2_mono 1),
- (rtac monofun_fapp1 1),
- (rtac (monofun_fapp2 RS allI) 1),
- (atac 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* a lemma about the exchange of lubs for type 'a -> 'b *)
-(* use MF2 lemmas from Cont.ML *)
-(* ------------------------------------------------------------------------ *)
-
-val ex_lubcfun = prove_goal Cfun2.thy
- "[| is_chain(F); is_chain(Y) |] ==>\
-\ lub(range(%j. lub(range(%i. F(j)[Y(i)])))) =\
-\ lub(range(%i. lub(range(%j. F(j)[Y(i)]))))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac ex_lubMF2 1),
- (rtac monofun_fapp1 1),
- (rtac (monofun_fapp2 RS allI) 1),
- (atac 1),
- (atac 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* the lub of a chain of cont. functions is continuous *)
-(* ------------------------------------------------------------------------ *)
-
-val contX_lubcfun = prove_goal Cfun2.thy
- "is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac monocontlub2contX 1),
- (etac lub_cfun_mono 1),
- (rtac contlubI 1),
- (strip_tac 1),
- (rtac (contlub_cfun_arg RS ext RS ssubst) 1),
- (atac 1),
- (etac ex_lubcfun 1),
- (atac 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* type 'a -> 'b is chain complete *)
-(* ------------------------------------------------------------------------ *)
-
-val lub_cfun = prove_goal Cfun2.thy
- "is_chain(CCF) ==> range(CCF) <<| fabs(% x.lub(range(% i.CCF(i)[x])))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac is_lubI 1),
- (rtac conjI 1),
- (rtac ub_rangeI 1),
- (rtac allI 1),
- (rtac (less_cfun RS ssubst) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
- (etac contX_lubcfun 1),
- (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
- (etac (monofun_fapp1 RS ch2ch_monofun) 1),
- (strip_tac 1),
- (rtac (less_cfun RS ssubst) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
- (etac contX_lubcfun 1),
- (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
- (etac (monofun_fapp1 RS ch2ch_monofun) 1),
- (etac (monofun_fapp1 RS ub2ub_monofun) 1)
- ]);
-
-val thelub_cfun = (lub_cfun RS thelubI);
-(*
-is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
-*)
-
-val cpo_cfun = prove_goal Cfun2.thy
- "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac exI 1),
- (etac lub_cfun 1)
- ]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* Extensionality in 'a -> 'b *)
-(* ------------------------------------------------------------------------ *)
-
-val ext_cfun = prove_goal Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
- (fn prems =>
- [
- (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
- (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
- (res_inst_tac [("f","fabs")] arg_cong 1),
- (rtac ext 1),
- (resolve_tac prems 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* Monotonicity of fabs *)
-(* ------------------------------------------------------------------------ *)
-
-val semi_monofun_fabs = prove_goal Cfun2.thy
- "[|contX(f);contX(g);f<<g|]==>fabs(f)<<fabs(g)"
- (fn prems =>
- [
- (rtac (less_cfun RS iffD2) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
- (resolve_tac prems 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
-(* Extenionality wrt. << in 'a -> 'b *)
-(* ------------------------------------------------------------------------ *)
-
-val less_cfun2 = prove_goal Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
- (fn prems =>
- [
- (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
- (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
- (rtac semi_monofun_fabs 1),
- (rtac contX_fapp2 1),
- (rtac contX_fapp2 1),
- (rtac (less_fun RS iffD2) 1),
- (rtac allI 1),
- (resolve_tac prems 1)
- ]);
-
-
--- a/src/HOLCF/cfun2.thy Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(* Title: HOLCF/cfun2.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Class Instance ->::(pcpo,pcpo)po
-
-*)
-
-Cfun2 = Cfun1 +
-
-(* Witness for the above arity axiom is cfun1.ML *)
-arities "->" :: (pcpo,pcpo)po
-
-consts
- UU_cfun :: "'a->'b"
-
-rules
-
-(* instance of << for type ['a -> 'b] *)
-
-inst_cfun_po "(op <<)::['a->'b,'a->'b]=>bool = less_cfun"
-
-(* definitions *)
-(* The least element in type 'a->'b *)
-
-UU_cfun_def "UU_cfun == fabs(% x.UU)"
-
-end
-
-ML
-
-(* ----------------------------------------------------------------------*)
-(* unique setup of print translation for fapp *)
-(* ----------------------------------------------------------------------*)
-
-val print_translation = [("fapp",fapptr')];
-
-
--- a/src/HOLCF/ex/coind.ML Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,140 +0,0 @@
-(* Title: HOLCF/coind.ML
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-*)
-
-open Coind;
-
-(* ------------------------------------------------------------------------- *)
-(* expand fixed point properties *)
-(* ------------------------------------------------------------------------- *)
-
-
-val nats_def2 = fix_prover Coind.thy nats_def
- "nats = scons[dzero][smap[dsucc][nats]]";
-
-val from_def2 = fix_prover Coind.thy from_def
- "from = (LAM n.scons[n][from[dsucc[n]]])";
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* recursive properties *)
-(* ------------------------------------------------------------------------- *)
-
-
-val from = prove_goal Coind.thy "from[n] = scons[n][from[dsucc[n]]]"
- (fn prems =>
- [
- (rtac trans 1),
- (rtac (from_def2 RS ssubst) 1),
- (simp_tac HOLCF_ss 1),
- (rtac refl 1)
- ]);
-
-
-val from1 = prove_goal Coind.thy "from[UU] = UU"
- (fn prems =>
- [
- (rtac trans 1),
- (rtac (from RS ssubst) 1),
- (resolve_tac stream_constrdef 1),
- (rtac refl 1)
- ]);
-
-val coind_rews =
- [iterator1, iterator2, iterator3, smap1, smap2,from1];
-
-
-(* ------------------------------------------------------------------------- *)
-(* the example *)
-(* prove: nats = from[dzero] *)
-(* ------------------------------------------------------------------------- *)
-
-
-val coind_lemma1 = prove_goal Coind.thy "iterator[n][smap[dsucc]][nats] =\
-\ scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
- (fn prems =>
- [
- (res_inst_tac [("s","n")] dnat_ind 1),
- (simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
- (simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
- (rtac trans 1),
- (rtac nats_def2 1),
- (simp_tac (HOLCF_ss addsimps (coind_rews @ dnat_rews)) 1),
- (rtac trans 1),
- (etac iterator3 1),
- (rtac trans 1),
- (asm_simp_tac HOLCF_ss 1),
- (rtac trans 1),
- (etac smap2 1),
- (rtac cfun_arg_cong 1),
- (asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat_rews)) 1)
- ]);
-
-
-val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
- (fn prems =>
- [
- (res_inst_tac [("R",
-"% p q.? n. p = iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
- (res_inst_tac [("x","dzero")] exI 2),
- (asm_simp_tac (HOLCF_ss addsimps coind_rews) 2),
- (rewrite_goals_tac [stream_bisim_def]),
- (strip_tac 1),
- (etac exE 1),
- (res_inst_tac [("Q","n=UU")] classical2 1),
- (rtac disjI1 1),
- (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
- (rtac disjI2 1),
- (etac conjE 1),
- (hyp_subst_tac 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("x","n")] exI 1),
- (res_inst_tac [("x","iterator[dsucc[n]][smap[dsucc]][nats]")] exI 1),
- (res_inst_tac [("x","from[dsucc[n]]")] exI 1),
- (etac conjI 1),
- (rtac conjI 1),
- (rtac coind_lemma1 1),
- (rtac conjI 1),
- (rtac from 1),
- (res_inst_tac [("x","dsucc[n]")] exI 1),
- (fast_tac HOL_cs 1)
- ]);
-
-(* another proof using stream_coind_lemma2 *)
-
-val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
- (fn prems =>
- [
- (res_inst_tac [("R","% p q.? n. p = \
-\ iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
- (rtac stream_coind_lemma2 1),
- (strip_tac 1),
- (etac exE 1),
- (res_inst_tac [("Q","n=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
- (res_inst_tac [("x","UU::dnat")] exI 1),
- (simp_tac (HOLCF_ss addsimps coind_rews addsimps stream_rews) 1),
- (etac conjE 1),
- (hyp_subst_tac 1),
- (hyp_subst_tac 1),
- (rtac conjI 1),
- (rtac (coind_lemma1 RS ssubst) 1),
- (rtac (from RS ssubst) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (res_inst_tac [("x","dsucc[n]")] exI 1),
- (rtac conjI 1),
- (rtac trans 1),
- (rtac (coind_lemma1 RS ssubst) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (rtac refl 1),
- (rtac trans 1),
- (rtac (from RS ssubst) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (rtac refl 1),
- (res_inst_tac [("x","dzero")] exI 1),
- (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1)
- ]);
-
--- a/src/LCF/lcf.ML Sat Apr 05 16:24:20 2003 +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 => [rewrite_goals_tac[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, rewrite_goals_tac [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 Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-(* Title: LCF/lcf.thy
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1992 University of Cambridge
-
-Natural Deduction Rules for LCF
-*)
-
-LCF = FOL +
-
-classes cpo < term
-
-default cpo
-
-types
- tr
- void
- ('a,'b) "*" (infixl 6)
- ('a,'b) "+" (infixl 5)
-
-arities
- fun, "*", "+" :: (cpo,cpo)cpo
- tr,void :: cpo
-
-consts
- UU :: "'a"
- TT,FF :: "tr"
- FIX :: "('a => 'a) => 'a"
- FST :: "'a*'b => 'a"
- SND :: "'a*'b => 'b"
- INL :: "'a => 'a+'b"
- INR :: "'b => 'a+'b"
- WHEN :: "['a=>'c, 'b=>'c, 'a+'b] => 'c"
- adm :: "('a => o) => o"
- VOID :: "void" ("()")
- PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100)
- COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60)
- "<<" :: "['a,'a] => o" (infixl 50)
-rules
- (** DOMAIN THEORY **)
-
- eq_def "x=y == x << y & y << x"
-
- less_trans "[| x << y; y << z |] ==> x << z"
-
- less_ext "(ALL x. f(x) << g(x)) ==> f << g"
-
- mono "[| f << g; x << y |] ==> f(x) << g(y)"
-
- minimal "UU << x"
-
- FIX_eq "f(FIX(f)) = FIX(f)"
-
- (** TR **)
-
- 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"
-
- 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"
-
- 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_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)"
-
- SUM_EXHAUSTION
- "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))"
-
- (** VOID **)
-
- void_cases "(x::void) = UU"
-
- (** INDUCTION **)
-
- 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))"
-end
--- a/src/LK/ex/hard-quant.ML Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,277 +0,0 @@
-(* Title: LK/ex/hard-quant
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
-
-Hard examples with quantifiers. Can be read to test the LK system.
-From F. J. Pelletier,
- Seventy-Five Problems for Testing Automatic Theorem Provers,
- J. Automated Reasoning 2 (1986), 191-216.
- Errata, JAR 4 (1988), 236-236.
-
-Uses pc_tac rather than fast_tac when the former is significantly faster.
-*)
-
-writeln"File LK/ex/hard-quant.";
-
-goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
-by (fast_tac LK_pack 1);
-result();
-
-goal LK.thy "|- (EX x. P-->Q(x)) <-> (P --> (EX x.Q(x)))";
-by (fast_tac LK_pack 1);
-result();
-
-goal LK.thy "|- (EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q";
-by (fast_tac LK_pack 1);
-result();
-
-goal LK.thy "|- (ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problems requiring quantifier duplication";
-
-(*Not provable by fast_tac LK_pack: needs multiple instantiation of ALL*)
-goal LK.thy "|- (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))";
-by (best_tac LK_dup_pack 1);
-result();
-
-(*Needs double instantiation of the quantifier*)
-goal LK.thy "|- EX x. P(x) --> P(a) & P(b)";
-by (fast_tac LK_dup_pack 1);
-result();
-
-goal LK.thy "|- EX z. P(z) --> (ALL x. P(x))";
-by (best_tac LK_dup_pack 1);
-result();
-
-writeln"Hard examples with quantifiers";
-
-writeln"Problem 18";
-goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
-by (best_tac LK_dup_pack 1);
-result();
-
-writeln"Problem 19";
-goal LK.thy "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
-by (best_tac LK_dup_pack 1);
-result();
-
-writeln"Problem 20";
-goal LK.thy "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) \
-\ --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 21";
-goal LK.thy "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
-by (best_tac LK_dup_pack 1);
-result();
-
-writeln"Problem 22";
-goal LK.thy "|- (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 23";
-goal LK.thy "|- (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))";
-by (best_tac LK_pack 1);
-result();
-
-writeln"Problem 24";
-goal LK.thy "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \
-\ ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x)) \
-\ --> (EX x. P(x)&R(x))";
-by (pc_tac LK_pack 1);
-result();
-
-writeln"Problem 25";
-goal LK.thy "|- (EX x. P(x)) & \
-\ (ALL x. L(x) --> ~ (M(x) & R(x))) & \
-\ (ALL x. P(x) --> (M(x) & L(x))) & \
-\ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) \
-\ --> (EX x. Q(x)&P(x))";
-by (best_tac LK_pack 1);
-result();
-
-writeln"Problem 26";
-goal LK.thy "|- ((EX x. p(x)) <-> (EX x. q(x))) & \
-\ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \
-\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
-by (pc_tac LK_pack 1);
-result();
-
-writeln"Problem 27";
-goal LK.thy "|- (EX x. P(x) & ~Q(x)) & \
-\ (ALL x. P(x) --> R(x)) & \
-\ (ALL x. M(x) & L(x) --> P(x)) & \
-\ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \
-\ --> (ALL x. M(x) --> ~L(x))";
-by (pc_tac LK_pack 1);
-result();
-
-writeln"Problem 28. AMENDED";
-goal LK.thy "|- (ALL x. P(x) --> (ALL x. Q(x))) & \
-\ ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \
-\ ((EX x.S(x)) --> (ALL x. L(x) --> M(x))) \
-\ --> (ALL x. P(x) & L(x) --> M(x))";
-by (pc_tac LK_pack 1);
-result();
-
-writeln"Problem 29. Essentially the same as Principia Mathematica *11.71";
-goal LK.thy "|- (EX x. P(x)) & (EX y. Q(y)) \
-\ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> \
-\ (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
-by (pc_tac LK_pack 1);
-result();
-
-writeln"Problem 30";
-goal LK.thy "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \
-\ (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \
-\ --> (ALL x. S(x))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 31";
-goal LK.thy "|- ~(EX x.P(x) & (Q(x) | R(x))) & \
-\ (EX x. L(x) & P(x)) & \
-\ (ALL x. ~ R(x) --> M(x)) \
-\ --> (EX x. L(x) & M(x))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 32";
-goal LK.thy "|- (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
-\ (ALL x. S(x) & R(x) --> L(x)) & \
-\ (ALL x. M(x) --> R(x)) \
-\ --> (ALL x. P(x) & M(x) --> L(x))";
-by (best_tac LK_pack 1);
-result();
-
-writeln"Problem 33";
-goal LK.thy "|- (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> \
-\ (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 34 AMENDED (TWICE!!) NOT PROVED AUTOMATICALLY";
-(*Andrews's challenge*)
-goal LK.thy "|- ((EX x. ALL y. p(x) <-> p(y)) <-> \
-\ ((EX x. q(x)) <-> (ALL y. p(y)))) <-> \
-\ ((EX x. ALL y. q(x) <-> q(y)) <-> \
-\ ((EX x. p(x)) <-> (ALL y. q(y))))";
-by (safe_goal_tac LK_pack 1); (*53 secs*) (*13 secs*)
-by (TRYALL (fast_tac LK_pack)); (*165 secs*) (*117 secs*) (*138 secs*)
-(*for some reason, pc_tac leaves 14 subgoals instead of 6*)
-by (TRYALL (best_tac LK_dup_pack)); (*55 secs*) (*29 secs*) (*54 secs*)
-result();
-
-
-writeln"Problem 35";
-goal LK.thy "|- EX x y. P(x,y) --> (ALL u v. P(u,v))";
-by (best_tac LK_dup_pack 1); (*27 secs??*)
-result();
-
-writeln"Problem 36";
-goal LK.thy "|- (ALL x. EX y. J(x,y)) & \
-\ (ALL x. EX y. G(x,y)) & \
-\ (ALL x y. J(x,y) | G(x,y) --> \
-\ (ALL z. J(y,z) | G(y,z) --> H(x,z))) \
-\ --> (ALL x. EX y. H(x,y))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 37";
-goal LK.thy "|- (ALL z. EX w. ALL x. EX y. \
-\ (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
-\ (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
-\ ((EX x y. Q(x,y)) --> (ALL x. R(x,x))) \
-\ --> (ALL x. EX y. R(x,y))";
-by (pc_tac LK_pack 1); (*slow*)
-by flexflex_tac;
-result();
-
-writeln"Problem 38. NOT PROVED";
-goal LK.thy
- "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) --> \
-\ (EX z. EX w. p(z) & r(x,w) & r(w,z))) <-> \
-\ (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) & \
-\ (~p(a) | ~(EX y. p(y) & r(x,y)) | \
-\ (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
-
-writeln"Problem 39";
-goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 40. AMENDED";
-goal LK.thy "|- (EX y. ALL x. F(x,y) <-> F(x,x)) --> \
-\ ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 41";
-goal LK.thy "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) \
-\ --> ~ (EX z. ALL x. f(x,z))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 42";
-goal LK.thy "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))";
-
-writeln"Problem 43 NOT PROVED AUTOMATICALLY";
-goal LK.thy "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \
-\ --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))";
-
-writeln"Problem 44";
-goal LK.thy "|- (ALL x. f(x) --> \
-\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
-\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \
-\ --> (EX x. j(x) & ~f(x))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 45";
-goal LK.thy "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y)) \
-\ --> (ALL y. g(y) & h(x,y) --> k(y))) & \
-\ ~ (EX y. l(y) & k(y)) & \
-\ (EX x. f(x) & (ALL y. h(x,y) --> l(y)) \
-\ & (ALL y. g(y) & h(x,y) --> j(x,y))) \
-\ --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
-by (best_tac LK_pack 1);
-result();
-
-
-writeln"Problem 50";
-goal LK.thy
- "|- (ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))";
-by (best_tac LK_dup_pack 1);
-result();
-
-writeln"Problem 57";
-goal LK.thy
- "|- P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
-\ (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 59";
-(*Unification works poorly here -- the abstraction %sobj prevents efficient
- operation of the occurs check*)
-Unify.trace_bound := !Unify.search_bound - 1;
-goal LK.thy "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
-by (best_tac LK_dup_pack 1);
-result();
-
-writeln"Problem 60";
-goal LK.thy
- "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Reached end of file.";
-
-(*18 June 92: loaded in 372 secs*)
-(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
-(*29 June 92: loaded in 370 secs*)
--- a/src/LK/lk.ML Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,237 +0,0 @@
-(* Title: LK/lk.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
-
-Tactics and lemmas for lk.thy (thanks also to Philippe de Groote)
-*)
-
-open LK;
-
-(*Higher precedence than := facilitates use of references*)
-infix 4 add_safes add_unsafes;
-
-signature LK_RESOLVE =
- sig
- datatype pack = Pack of thm list * thm list
- val add_safes: pack * thm list -> pack
- val add_unsafes: pack * thm list -> pack
- val allL_thin: thm
- val best_tac: pack -> int -> tactic
- val could_res: term * term -> bool
- val could_resolve_seq: term * term -> bool
- val cutL_tac: string -> int -> tactic
- val cutR_tac: string -> int -> tactic
- val conL: thm
- val conR: thm
- val empty_pack: pack
- val exR_thin: thm
- val fast_tac: pack -> int -> tactic
- val filseq_resolve_tac: thm list -> int -> int -> tactic
- val forms_of_seq: term -> term list
- val has_prems: int -> thm -> bool
- val iffL: thm
- val iffR: thm
- val less: thm * thm -> bool
- val LK_dup_pack: pack
- val LK_pack: pack
- val pc_tac: pack -> int -> tactic
- val prop_pack: pack
- val repeat_goal_tac: pack -> int -> tactic
- val reresolve_tac: thm list -> int -> tactic
- val RESOLVE_THEN: thm list -> (int -> tactic) -> int -> tactic
- val safe_goal_tac: pack -> int -> tactic
- val step_tac: pack -> int -> tactic
- val symL: thm
- val TrueR: thm
- end;
-
-
-structure LK_Resolve : LK_RESOLVE =
-struct
-
-(*Cut and thin, replacing the right-side formula*)
-fun cutR_tac (sP: string) i =
- res_inst_tac [ ("P",sP) ] cut i THEN rtac thinR i;
-
-(*Cut and thin, replacing the left-side formula*)
-fun cutL_tac (sP: string) i =
- res_inst_tac [ ("P",sP) ] cut i THEN rtac thinL (i+1);
-
-
-(** If-and-only-if rules **)
-val iffR = prove_goalw LK.thy [iff_def]
- "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
- (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
-
-val iffL = prove_goalw LK.thy [iff_def]
- "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
- (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);
-
-val TrueR = prove_goalw LK.thy [True_def]
- "$H |- $E, True, $F"
- (fn _=> [ rtac impR 1, rtac basic 1 ]);
-
-
-(** Weakened quantifier rules. Incomplete, they let the search terminate.**)
-
-val allL_thin = prove_goal LK.thy
- "$H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E"
- (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);
-
-val exR_thin = prove_goal LK.thy
- "$H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F"
- (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);
-
-(* Symmetry of equality in hypotheses *)
-val symL = prove_goal LK.thy
- "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E"
- (fn prems=>
- [ (rtac cut 1),
- (rtac thinL 2),
- (resolve_tac prems 2),
- (resolve_tac [basic RS sym] 1) ]);
-
-
-(**** Theorem Packs ****)
-
-datatype pack = Pack of thm list * thm list;
-
-(*A theorem pack has the form (safe rules, unsafe rules)
- An unsafe rule is incomplete or introduces variables in subgoals,
- and is tried only when the safe rules are not applicable. *)
-
-fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);
-
-val empty_pack = Pack([],[]);
-
-fun (Pack(safes,unsafes)) add_safes ths =
- Pack(sort less (ths@safes), unsafes);
-
-fun (Pack(safes,unsafes)) add_unsafes ths =
- Pack(safes, sort less (ths@unsafes));
-
-(*The rules of LK*)
-val prop_pack = empty_pack add_safes
- [basic, refl, conjL, conjR, disjL, disjR, impL, impR,
- notL, notR, iffL, iffR];
-
-val LK_pack = prop_pack add_safes [allR, exL]
- add_unsafes [allL_thin, exR_thin];
-
-val LK_dup_pack = prop_pack add_safes [allR, exL]
- add_unsafes [allL, exR];
-
-
-
-(*Returns the list of all formulas in the sequent*)
-fun forms_of_seq (Const("Seqof",_) $ P $ u) = P :: forms_of_seq u
- | forms_of_seq (H $ u) = forms_of_seq u
- | forms_of_seq _ = [];
-
-(*Tests whether two sequences (left or right sides) could be resolved.
- seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
- Assumes each formula in seqc is surrounded by sequence variables
- -- checks that each concl formula looks like some subgoal formula.
- It SHOULD check order as well, using recursion rather than forall/exists*)
-fun could_res (seqp,seqc) =
- forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc))
- (forms_of_seq seqp))
- (forms_of_seq seqc);
-
-(*Tests whether two sequents G|-H could be resolved, comparing each side.*)
-fun could_resolve_seq (prem,conc) =
- case (prem,conc) of
- (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
- _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
- could_res (leftp,leftc) andalso could_res (rightp,rightc)
- | _ => false;
-
-
-(*Like filt_resolve_tac, using could_resolve_seq
- Much faster than resolve_tac when there are many rules.
- Resolve subgoal i using the rules, unless more than maxr are compatible. *)
-fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
- let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
- in if length rls > maxr then no_tac else resolve_tac rls i
- end);
-
-
-(*Predicate: does the rule have n premises? *)
-fun has_prems n rule = (nprems_of rule = n);
-
-(*Continuation-style tactical for resolution.
- The list of rules is partitioned into 0, 1, 2 premises.
- The resulting tactic, gtac, tries to resolve with rules.
- If successful, it recursively applies nextac to the new subgoals only.
- Else fails. (Treatment of goals due to Ph. de Groote)
- Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)
-
-(*Takes rule lists separated in to 0, 1, 2, >2 premises.
- The abstraction over state prevents needless divergence in recursion.
- The 9999 should be a parameter, to delay treatment of flexible goals. *)
-fun RESOLVE_THEN rules =
- let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
- fun tac nextac i = STATE (fn state =>
- filseq_resolve_tac rls0 9999 i
- ORELSE
- (DETERM(filseq_resolve_tac rls1 9999 i) THEN TRY(nextac i))
- ORELSE
- (DETERM(filseq_resolve_tac rls2 9999 i) THEN TRY(nextac(i+1))
- THEN TRY(nextac i)) )
- in tac end;
-
-
-(*repeated resolution applied to the designated goal*)
-fun reresolve_tac rules =
- let val restac = RESOLVE_THEN rules; (*preprocessing done now*)
- fun gtac i = restac gtac i
- in gtac end;
-
-(*tries the safe rules repeatedly before the unsafe rules. *)
-fun repeat_goal_tac (Pack(safes,unsafes)) =
- let val restac = RESOLVE_THEN safes
- and lastrestac = RESOLVE_THEN unsafes;
- fun gtac i = restac gtac i ORELSE lastrestac gtac i
- in gtac end;
-
-
-(*Tries safe rules only*)
-fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;
-
-(*Tries a safe rule or else a unsafe rule. Single-step for tracing. *)
-fun step_tac (thm_pack as Pack(safes,unsafes)) =
- safe_goal_tac thm_pack ORELSE'
- filseq_resolve_tac unsafes 9999;
-
-
-(* Tactic for reducing a goal, using Predicate Calculus rules.
- A decision procedure for Propositional Calculus, it is incomplete
- for Predicate-Calculus because of allL_thin and exR_thin.
- Fails if it can do nothing. *)
-fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1));
-
-(*The following two tactics are analogous to those provided by
- Provers/classical. In fact, pc_tac is usually FASTER than fast_tac!*)
-fun fast_tac thm_pack =
- SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1));
-
-fun best_tac thm_pack =
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm)
- (step_tac thm_pack 1));
-
-(** Contraction. Useful since some rules are not complete. **)
-
-val conR = prove_goal LK.thy
- "$H |- $E, P, $F, P ==> $H |- $E, P, $F"
- (fn prems=>
- [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
-
-val conL = prove_goal LK.thy
- "$H, P, $G, P |- $E ==> $H, P, $G |- $E"
- (fn prems=>
- [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
-
-end;
-
-open LK_Resolve;
--- a/src/LK/lk.thy Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-(* Title: LK/lk.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Classical First-Order Sequent Calculus
-*)
-
-LK = Pure +
-
-classes term < logic
-
-default term
-
-types
- o sequence seqobj seqcont sequ sobj
-
-arities
- o :: logic
-
-consts
- True,False :: "o"
- "=" :: "['a,'a] => o" (infixl 50)
- "Not" :: "o => o" ("~ _" [40] 40)
- "&" :: "[o,o] => o" (infixr 35)
- "|" :: "[o,o] => o" (infixr 30)
- "-->","<->" :: "[o,o] => o" (infixr 25)
- The :: "('a => o) => 'a" (binder "THE " 10)
- All :: "('a => o) => o" (binder "ALL " 10)
- Ex :: "('a => o) => o" (binder "EX " 10)
-
- (*Representation of sequents*)
- Trueprop :: "[sobj=>sobj,sobj=>sobj] => prop"
- Seqof :: "o => sobj=>sobj"
- "@Trueprop" :: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5)
- "@MtSeq" :: "sequence" ("" [] 1000)
- "@NmtSeq" :: "[seqobj,seqcont] => sequence" ("__" [] 1000)
- "@MtSeqCont" :: "seqcont" ("" [] 1000)
- "@SeqCont" :: "[seqobj,seqcont] => seqcont" (",/ __" [] 1000)
- "" :: "o => seqobj" ("_" [] 1000)
- "@SeqId" :: "id => seqobj" ("$_" [] 1000)
- "@SeqVar" :: "var => seqobj" ("$_")
-
-rules
- (*Structural rules*)
-
- basic "$H, P, $G |- $E, P, $F"
-
- thinR "$H |- $E, $F ==> $H |- $E, P, $F"
- thinL "$H, $G |- $E ==> $H, P, $G |- $E"
-
- cut "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E"
-
- (*Propositional rules*)
-
- conjR "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
- conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
-
- disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
- disjL "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
-
- impR "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
- impL "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
-
- notR "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
- notL "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
-
- FalseL "$H, False, $G |- $E"
-
- True_def "True == False-->False"
- iff_def "P<->Q == (P-->Q) & (Q-->P)"
-
- (*Quantifiers*)
-
- allR "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
- allL "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
-
- exR "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
- exL "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
-
- (*Equality*)
-
- refl "$H |- $E, a=a, $F"
- sym "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F"
- trans "[| $H|- $E, a=b, $F; $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F"
-
-
- (*Descriptions*)
-
- The "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> \
-\ $H |- $E, P(THE x.P(x)), $F"
-end
-
-ML
-
-(*Abstract over "sobj" -- representation of a sequence of formulae *)
-fun abs_sobj t = Abs("sobj", Type("sobj",[]), t);
-
-(*Representation of empty sequence*)
-val Sempty = abs_sobj (Bound 0);
-
-fun seq_obj_tr(Const("@SeqId",_)$id) = id |
- seq_obj_tr(Const("@SeqVar",_)$id) = id |
- seq_obj_tr(fm) = Const("Seqof",dummyT)$fm;
-
-fun seq_tr(_$obj$seq) = seq_obj_tr(obj)$seq_tr(seq) |
- seq_tr(_) = Bound 0;
-
-fun seq_tr1(Const("@MtSeq",_)) = Sempty |
- seq_tr1(seq) = abs_sobj(seq_tr seq);
-
-fun true_tr[s1,s2] = Const("Trueprop",dummyT)$seq_tr1 s1$seq_tr1 s2;
-
-fun seq_obj_tr'(Const("Seqof",_)$fm) = fm |
- seq_obj_tr'(id) = Const("@SeqId",dummyT)$id;
-
-fun seq_tr'(obj$sq,C) =
- let val sq' = case sq of
- Bound 0 => Const("@MtSeqCont",dummyT) |
- _ => seq_tr'(sq,Const("@SeqCont",dummyT))
- in C $ seq_obj_tr' obj $ sq' end;
-
-fun seq_tr1'(Bound 0) = Const("@MtSeq",dummyT) |
- seq_tr1' s = seq_tr'(s,Const("@NmtSeq",dummyT));
-
-fun true_tr'[Abs(_,_,s1),Abs(_,_,s2)] =
- Const("@Trueprop",dummyT)$seq_tr1' s1$seq_tr1' s2;
-
-val parse_translation = [("@Trueprop",true_tr)];
-val print_translation = [("Trueprop",true_tr')];
--- a/src/Modal/modal0.thy Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(* Title: 91/Modal/modal0
- ID: $Id$
- Author: Martin Coen
- Copyright 1991 University of Cambridge
-*)
-
-Modal0 = LK +
-
-consts
- box :: "o=>o" ("[]_" [50] 50)
- dia :: "o=>o" ("<>_" [50] 50)
- "--<",">-<" :: "[o,o]=>o" (infixr 25)
- "@Lstar" :: "[sequence,sequence]=>prop" ("(_)|L>(_)" [6,6] 5)
- "@Rstar" :: "[sequence,sequence]=>prop" ("(_)|R>(_)" [6,6] 5)
- Lstar,Rstar :: "[sobj=>sobj,sobj=>sobj]=>prop"
-
-rules
- (* Definitions *)
-
- strimp_def "P --< Q == [](P --> Q)"
- streqv_def "P >-< Q == (P --< Q) & (Q --< P)"
-end
-
-ML
-
-local
-
- val Lstar = "Lstar";
- val Rstar = "Rstar";
- val SLstar = "@Lstar";
- val SRstar = "@Rstar";
-
- fun star_tr c [s1,s2] = Const(c,dummyT)$LK.seq_tr1 s1$LK.seq_tr1 s2;
- fun star_tr' c [Abs(_,_,s1),Abs(_,_,s2)] =
- Const(c,dummyT) $ LK.seq_tr1' s1 $ LK.seq_tr1' s2;
-in
-val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
-val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
-end;
--- a/src/Modal/s4.thy Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(* Title: 91/Modal/S4
- ID: $Id$
- Author: Martin Coen
- Copyright 1991 University of Cambridge
-*)
-
-S4 = Modal0 +
-rules
-(* Definition of the star operation using a set of Horn clauses *)
-(* For system S4: gamma * == {[]P | []P : gamma} *)
-(* delta * == {<>P | <>P : delta} *)
-
- lstar0 "|L>"
- lstar1 "$G |L> $H ==> []P, $G |L> []P, $H"
- lstar2 "$G |L> $H ==> P, $G |L> $H"
- rstar0 "|R>"
- rstar1 "$G |R> $H ==> <>P, $G |R> <>P, $H"
- rstar2 "$G |R> $H ==> P, $G |R> $H"
-
-(* Rules for [] and <> *)
-
- boxR
- "[| $E |L> $E'; $F |R> $F'; $G |R> $G'; \
-\ $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G"
- boxL "$E,P,$F,[]P |- $G ==> $E, []P, $F |- $G"
-
- diaR "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G"
- diaL
- "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; \
-\ $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G"
-end
--- a/src/Modal/s43.thy Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-(* Title: 91/Modal/S43
- ID: $Id$
- Author: Martin Coen
- Copyright 1991 University of Cambridge
-
-This implements Rajeev Gore's sequent calculus for S43.
-*)
-
-S43 = Modal0 +
-
-consts
- S43pi :: "[sobj=>sobj, sobj=>sobj, sobj=>sobj,\
-\ sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop"
- "@S43pi" :: "[sequence, sequence, sequence, sequence, sequence,\
-\ sequence] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
-
-rules
-(* Definition of the star operation using a set of Horn clauses *)
-(* For system S43: gamma * == {[]P | []P : gamma} *)
-(* delta * == {<>P | <>P : delta} *)
-
- lstar0 "|L>"
- lstar1 "$G |L> $H ==> []P, $G |L> []P, $H"
- lstar2 "$G |L> $H ==> P, $G |L> $H"
- rstar0 "|R>"
- rstar1 "$G |R> $H ==> <>P, $G |R> <>P, $H"
- rstar2 "$G |R> $H ==> P, $G |R> $H"
-
-(* Set of Horn clauses to generate the antecedents for the S43 pi rule *)
-(* ie *)
-(* S1...Sk,Sk+1...Sk+m *)
-(* ---------------------------------- *)
-(* <>P1...<>Pk, $G |- $H, []Q1...[]Qm *)
-(* *)
-(* where Si == <>P1...<>Pi-1,<>Pi+1,..<>Pk,Pi, $G * |- $H *, []Q1...[]Qm *)
-(* and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj *)
-(* and 1<=i<=k and k<j<=k+m *)
-
- S43pi0 "S43pi $L;; $R;; $Lbox; $Rdia"
- S43pi1
- "[| (S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia |] ==> \
-\ S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia"
- S43pi2
- "[| (S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia |] ==> \
-\ S43pi $L';; $R'; []P,$R; $Lbox;$Rdia"
-
-(* Rules for [] and <> for S43 *)
-
- boxL "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
- diaR "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
- pi1
- "[| $L1,<>P,$L2 |L> $Lbox; $L1,<>P,$L2 |R> $Ldia; $R |L> $Rbox; $R |R> $Rdia; \
-\ S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> \
-\ $L1, <>P, $L2 |- $R"
- pi2
- "[| $L |L> $Lbox; $L |R> $Ldia; $R1,[]P,$R2 |L> $Rbox; $R1,[]P,$R2 |R> $Rdia; \
-\ S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> \
-\ $L |- $R1, []P, $R2"
-end
-
-ML
-
-local
-
- val S43pi = "S43pi";
- val SS43pi = "@S43pi";
-
- val tr = LK.seq_tr1;
- val tr' = LK.seq_tr1';
-
- fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
- Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
- fun s43pi_tr'[Abs(_,_,s1),Abs(_,_,s2),Abs(_,_,s3),
- Abs(_,_,s4),Abs(_,_,s5),Abs(_,_,s6)] =
- Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
-in
-val parse_translation = [(SS43pi,s43pi_tr)];
-val print_translation = [(S43pi,s43pi_tr')]
-end
--- a/src/Modal/t.thy Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: 91/Modal/T
- ID: $Id$
- Author: Martin Coen
- Copyright 1991 University of Cambridge
-*)
-
-T = Modal0 +
-rules
-(* Definition of the star operation using a set of Horn clauses *)
-(* For system T: gamma * == {P | []P : gamma} *)
-(* delta * == {P | <>P : delta} *)
-
- lstar0 "|L>"
- lstar1 "$G |L> $H ==> []P, $G |L> P, $H"
- lstar2 "$G |L> $H ==> P, $G |L> $H"
- rstar0 "|R>"
- rstar1 "$G |R> $H ==> <>P, $G |R> P, $H"
- rstar2 "$G |R> $H ==> P, $G |R> $H"
-
-(* Rules for [] and <> *)
-
- boxR
- "[| $E |L> $E'; $F |R> $F'; $G |R> $G'; \
-\ $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G"
- boxL "$E, P, $F |- $G ==> $E, []P, $F |- $G"
- diaR "$E |- $F, P, $G ==> $E |- $F, <>P, $G"
- diaL
- "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; \
-\ $E', P, $F'|- $G'|] ==> $E, <>P, $F |- $G"
-end