# HG changeset patch # User lcp # Date 782555036 -3600 # Node ID 0db578095e6a0a1966cac14a9b99ac87df9f6162 # Parent 49fc43cd6a35acc01694ef3bb9b5ba85f550ebea CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification CCL/CCL, Fix, Gfp, Hered, Set, Term, Trancl, Type, Wfd: expanded shorthands diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/CCL.ML --- a/src/CCL/CCL.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/CCL.ML Wed Oct 19 09:23:56 1994 +0100 @@ -44,11 +44,11 @@ (*** Termination and Divergence ***) goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot"; -br iff_refl 1; +by (rtac iff_refl 1); val Trm_iff = result(); goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <-> t = bot"; -br iff_refl 1; +by (rtac iff_refl 1); val Dvg_iff = result(); (*** Constructors are injective ***) @@ -138,7 +138,7 @@ (****** Facts from gfp Definition of [= and = ******) val major::prems = goal Set.thy "[| A=B; a:B <-> P |] ==> a:A <-> P"; -brs (prems RL [major RS ssubst]) 1; +by (resolve_tac (prems RL [major RS ssubst]) 1); val XHlemma1 = result(); goal CCL.thy "(P(t,t') <-> Q) --> ( : {p.EX t t'.p= & P(t,t')} <-> Q)"; @@ -148,7 +148,7 @@ (*** Pre-Order ***) goalw CCL.thy [POgen_def,SIM_def] "mono(%X.POgen(X))"; -br monoI 1; +by (rtac monoI 1); by (safe_tac ccl_cs); by (REPEAT_SOME (resolve_tac [exI,conjI,refl])); by (ALLGOALS (simp_tac ccl_ss)); @@ -159,7 +159,7 @@ " : POgen(R) <-> t= bot | (t=true & t'=true) | (t=false & t'=false) | \ \ (EX a a' b b'.t= & t'= & : R & : R) | \ \ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x. : R))"; -br (iff_refl RS XHlemma2) 1; +by (rtac (iff_refl RS XHlemma2) 1); val POgenXH = result(); goal CCL.thy @@ -169,29 +169,29 @@ by (simp_tac (ccl_ss addsimps [PO_iff]) 1); br (rewrite_rule [POgen_def,SIM_def] (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1; -br (iff_refl RS XHlemma2) 1; +by (rtac (iff_refl RS XHlemma2) 1); val poXH = result(); goal CCL.thy "bot [= b"; -br (poXH RS iffD2) 1; +by (rtac (poXH RS iffD2) 1); by (simp_tac ccl_ss 1); val po_bot = result(); goal CCL.thy "a [= bot --> a=bot"; -br impI 1; -bd (poXH RS iffD1) 1; -be rev_mp 1; +by (rtac impI 1); +by (dtac (poXH RS iffD1) 1); +by (etac rev_mp 1); by (simp_tac ccl_ss 1); val bot_poleast = result() RS mp; goal CCL.thy " [= <-> a [= a' & b [= b'"; -br (poXH RS iff_trans) 1; +by (rtac (poXH RS iff_trans) 1); by (simp_tac ccl_ss 1); by (fast_tac ccl_cs 1); val po_pair = result(); goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))"; -br (poXH RS iff_trans) 1; +by (rtac (poXH RS iff_trans) 1); by (simp_tac ccl_ss 1); by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1)); by (asm_simp_tac ccl_ss 1); @@ -203,13 +203,13 @@ val [p1,p2,p3,p4,p5] = goal CCL.thy "[| t [= t'; a [= a'; b [= b'; !!x y.c(x,y) [= c'(x,y); \ \ !!u.d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')"; -br (p1 RS po_cong RS po_trans) 1; -br (p2 RS po_cong RS po_trans) 1; -br (p3 RS po_cong RS po_trans) 1; -br (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1; +by (rtac (p1 RS po_cong RS po_trans) 1); +by (rtac (p2 RS po_cong RS po_trans) 1); +by (rtac (p3 RS po_cong RS po_trans) 1); +by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1); by (res_inst_tac [("f1","%d.case(t',a',b',c',d)")] (p5 RS po_abstractn RS po_cong RS po_trans) 1); -br po_refl 1; +by (rtac po_refl 1); val case_pocong = result(); val [p1,p2] = goalw CCL.thy ccl_data_defs @@ -219,29 +219,29 @@ val prems = goal CCL.thy "~ lam x.b(x) [= bot"; -br notI 1; -bd bot_poleast 1; -be (distinctness RS notE) 1; +by (rtac notI 1); +by (dtac bot_poleast 1); +by (etac (distinctness RS notE) 1); val npo_lam_bot = result(); val eq1::eq2::prems = goal CCL.thy "[| x=a; y=b; x[=y |] ==> a[=b"; -br (eq1 RS subst) 1; -br (eq2 RS subst) 1; -brs prems 1; +by (rtac (eq1 RS subst) 1); +by (rtac (eq2 RS subst) 1); +by (resolve_tac prems 1); val po_lemma = result(); goal CCL.thy "~ [= lam x.f(x)"; -br notI 1; -br (npo_lam_bot RS notE) 1; -be (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1; +by (rtac notI 1); +by (rtac (npo_lam_bot RS notE) 1); +by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1); by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)); val npo_pair_lam = result(); goal CCL.thy "~ lam x.f(x) [= "; -br notI 1; -br (npo_lam_bot RS notE) 1; -be (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1; +by (rtac notI 1); +by (rtac (npo_lam_bot RS notE) 1); +by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1); by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)); val npo_lam_pair = result(); @@ -260,7 +260,7 @@ (* Coinduction for [= *) val prems = goal CCL.thy "[| : R; R <= POgen(R) |] ==> t [= u"; -br (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1; +by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1); by (REPEAT (ares_tac prems 1)); val po_coinduct = result(); @@ -269,7 +269,7 @@ (*************** EQUALITY *******************) goalw CCL.thy [EQgen_def,SIM_def] "mono(%X.EQgen(X))"; -br monoI 1; +by (rtac monoI 1); by (safe_tac set_cs); by (REPEAT_SOME (resolve_tac [exI,conjI,refl])); by (ALLGOALS (simp_tac ccl_ss)); @@ -281,7 +281,7 @@ \ (t=false & t'=false) | \ \ (EX a a' b b'.t= & t'= & : R & : R) | \ \ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x. : R))"; -br (iff_refl RS XHlemma2) 1; +by (rtac (iff_refl RS XHlemma2) 1); val EQgenXH = result(); goal CCL.thy @@ -292,21 +292,21 @@ " : EQ <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | \ \ (EX a a' b b'.t= & t'= & : EQ & : EQ) | \ \ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x. : EQ))" 1); -be rev_mp 1; +by (etac rev_mp 1); by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1); br (rewrite_rule [EQgen_def,SIM_def] (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1; -br (iff_refl RS XHlemma2) 1; +by (rtac (iff_refl RS XHlemma2) 1); val eqXH = result(); val prems = goal CCL.thy "[| : R; R <= EQgen(R) |] ==> t = u"; -br (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1; +by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1); by (REPEAT (ares_tac prems 1)); val eq_coinduct = result(); val prems = goal CCL.thy "[| : R; R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u"; -br (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1; +by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1); by (REPEAT (ares_tac (EQgen_mono::prems) 1)); val eq_coinduct3 = result(); diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/Fix.ML --- a/src/CCL/Fix.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/Fix.ML Wed Oct 19 09:23:56 1994 +0100 @@ -12,7 +12,7 @@ val [base,step,incl] = goalw Fix.thy [INCL_def] "[| P(bot); !!x.P(x) ==> P(f(x)); INCL(P) |] ==> P(fix(f))"; -br (incl RS spec RS mp) 1; +by (rtac (incl RS spec RS mp) 1); by (rtac (Nat_ind RS ballI) 1 THEN atac 1); by (ALLGOALS (simp_tac term_ss)); by (REPEAT (ares_tac [base,step] 1)); @@ -22,7 +22,7 @@ val prems = goalw Fix.thy [INCL_def] "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))"; -br iff_refl 1; +by (rtac iff_refl 1); val inclXH = result(); val prems = goal Fix.thy @@ -45,13 +45,13 @@ (*** Lemmas for Inclusive Predicates ***) goal Fix.thy "INCL(%x.~ a(x) [= t)"; -br inclI 1; -bd bspec 1; -br zeroT 1; -be contrapos 1; -br po_trans 1; -ba 2; -br (napplyBzero RS ssubst) 1; +by (rtac inclI 1); +by (dtac bspec 1); +by (rtac zeroT 1); +by (etac contrapos 1); +by (rtac po_trans 1); +by (assume_tac 2); +by (rtac (napplyBzero RS ssubst) 1); by (rtac po_cong 1 THEN rtac po_bot 1); val npo_INCL = result(); @@ -77,21 +77,21 @@ (* Fixed points of idgen *) goal Fix.thy "idgen(fix(idgen)) = fix(idgen)"; -br (fixB RS sym) 1; +by (rtac (fixB RS sym) 1); val fix_idgenfp = result(); goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x"; by (simp_tac term_ss 1); -br (term_case RS allI) 1; +by (rtac (term_case RS allI) 1); by (ALLGOALS (simp_tac term_ss)); val id_idgenfp = result(); (* All fixed points are lam-expressions *) val [prem] = goal Fix.thy "idgen(d) = d ==> d = lam x.?f(x)"; -br (prem RS subst) 1; -bw idgen_def; -br refl 1; +by (rtac (prem RS subst) 1); +by (rewtac idgen_def); +by (rtac refl 1); val idgenfp_lam = result(); (* Lemmas for rewriting fixed points of idgen *) @@ -117,14 +117,14 @@ val [p1,p2,p3] = goal CCL.thy "[| ALL x.t ` x [= u ` x; EX f.t=lam x.f(x); EX f.u=lam x.f(x) |] ==> t [= u"; -br (p2 RS cond_eta RS ssubst) 1; -br (p3 RS cond_eta RS ssubst) 1; -br (p1 RS (po_lam RS iffD2)) 1; +by (rtac (p2 RS cond_eta RS ssubst) 1); +by (rtac (p3 RS cond_eta RS ssubst) 1); +by (rtac (p1 RS (po_lam RS iffD2)) 1); val po_eta = result(); val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)"; -br (prem RS subst) 1; -br refl 1; +by (rtac (prem RS subst) 1); +by (rtac refl 1); val po_eta_lemma = result(); val [prem] = goal Fix.thy @@ -139,8 +139,8 @@ val [prem] = goal Fix.thy "idgen(d) = d ==> fix(idgen) [= d"; -br (allI RS po_eta) 1; -br (lemma1 RSN(2,po_coinduct)) 1; +by (rtac (allI RS po_eta) 1); +by (rtac (lemma1 RSN(2,po_coinduct)) 1); by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp]))); val fix_least_idgen = result(); @@ -155,8 +155,8 @@ val [prem] = goal Fix.thy "idgen(d) = d ==> lam x.x [= d"; -br (allI RS po_eta) 1; -br (lemma2 RSN(2,po_coinduct)) 1; +by (rtac (allI RS po_eta) 1); +by (rtac (lemma2 RSN(2,po_coinduct)) 1); by (simp_tac term_ss 1); by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp]))); val id_least_idgen = result(); @@ -170,8 +170,8 @@ (********) val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t"; -br (prem RS sym RS subst) 1; -br applyB 1; +by (rtac (prem RS sym RS subst) 1); +by (rtac applyB 1); val id_apply = result(); val prems = goal Fix.thy @@ -179,13 +179,13 @@ \ !!x y.[| P(x); P(y) |] ==> P(); \ \ !!u.(!!x.P(u(x))) ==> P(lam x.u(x)); INCL(P) |] ==> \ \ P(t)"; -br (reachability RS id_apply RS subst) 1; +by (rtac (reachability RS id_apply RS subst) 1); by (res_inst_tac [("x","t")] spec 1); -br fix_ind 1; -bw idgen_def; +by (rtac fix_ind 1); +by (rewtac idgen_def); by (REPEAT_SOME (ares_tac [allI])); -br (applyBbot RS ssubst) 1; -brs prems 1; +by (rtac (applyBbot RS ssubst) 1); +by (resolve_tac prems 1); br (applyB RS ssubst )1; by (res_inst_tac [("t","xa")] term_case 1); by (ALLGOALS (simp_tac term_ss)); diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/Gfp.ML --- a/src/CCL/Gfp.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/Gfp.ML Wed Oct 19 09:23:56 1994 +0100 @@ -60,10 +60,11 @@ val coinduct2_lemma = result(); (*strong version, thanks to Martin Coen*) -val prems = goal Gfp.thy +val ainA::prems = goal Gfp.thy "[| a: A; A <= f(A) Un gfp(f); mono(f) |] ==> a : gfp(f)"; -by (rtac (coinduct2_lemma RSN (2,coinduct)) 1); -by (REPEAT (resolve_tac (prems@[UnI1]) 1)); +by (rtac coinduct 1); +by (rtac (prems MRS coinduct2_lemma) 2); +by (resolve_tac [ainA RS UnI1] 1); val coinduct2 = result(); (*** Even Stronger version of coinduct [by Martin Coen] @@ -78,22 +79,22 @@ "[| A <= f(lfp(%x.f(x) Un A Un gfp(f))); mono(f) |] ==> \ \ lfp(%x.f(x) Un A Un gfp(f)) <= f(lfp(%x.f(x) Un A Un gfp(f)))"; by (rtac subset_trans 1); -br (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1; +by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1); by (rtac (Un_least RS Un_least) 1); -br subset_refl 1; -br prem 1; -br (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1; +by (rtac subset_refl 1); +by (rtac prem 1); +by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1); by (rtac (mono RS monoD) 1); by (rtac (mono RS coinduct3_mono_lemma RS lfp_Tarski RS ssubst) 1); by (rtac Un_upper2 1); val coinduct3_lemma = result(); -val prems = goal Gfp.thy +val ainA::prems = goal Gfp.thy "[| a:A; A <= f(lfp(%x.f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)"; -by (rtac (coinduct3_lemma RSN (2,coinduct)) 1); -brs (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1; -br (UnI2 RS UnI1) 1; -by (REPEAT (resolve_tac prems 1)); +by (rtac coinduct 1); +by (rtac (prems MRS coinduct3_lemma) 2); +by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1); +by (rtac (ainA RS UnI2 RS UnI1) 1); val coinduct3 = result(); diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/Hered.ML --- a/src/CCL/Hered.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/Hered.ML Wed Oct 19 09:23:56 1994 +0100 @@ -13,7 +13,7 @@ (*** Hereditary Termination ***) goalw Hered.thy [HTTgen_def] "mono(%X.HTTgen(X))"; -br monoI 1; +by (rtac monoI 1); by (fast_tac set_cs 1); val HTTgen_mono = result(); @@ -46,12 +46,12 @@ val HTT_false = result(); goal Hered.thy " : HTT <-> a : HTT & b : HTT"; -br (HTTXH RS iff_trans) 1; +by (rtac (HTTXH RS iff_trans) 1); by (fast_tac term_cs 1); val HTT_pair = result(); goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)"; -br (HTTXH RS iff_trans) 1; +by (rtac (HTTXH RS iff_trans) 1); by (simp_tac term_ss 1); by (safe_tac term_cs); by (asm_simp_tac term_ss 1); @@ -78,7 +78,7 @@ (*** Coinduction for HTT ***) val prems = goal Hered.thy "[| t : R; R <= HTTgen(R) |] ==> t : HTT"; -br (HTT_def RS def_coinduct) 1; +by (rtac (HTT_def RS def_coinduct) 1); by (REPEAT (ares_tac prems 1)); val HTT_coinduct = result(); @@ -86,7 +86,7 @@ val prems = goal Hered.thy "[| t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT"; -br (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1; +by (rtac (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1); by (REPEAT (ares_tac prems 1)); val HTT_coinduct3 = result(); val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3; @@ -139,20 +139,20 @@ goal Hered.thy "Nat <= HTT"; by (simp_tac (term_ss addsimps [subsetXH]) 1); by (safe_tac set_cs); -be Nat_ind 1; +by (etac Nat_ind 1); by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])))); val NatF = result(); goal Hered.thy "Nat <= HTT"; by (safe_tac set_cs); -be HTT_coinduct3 1; +by (etac HTT_coinduct3 1); by (fast_tac (set_cs addIs HTTgenIs addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1); val NatF = result(); val [prem] = goal Hered.thy "A <= HTT ==> List(A) <= HTT"; by (safe_tac set_cs); -be HTT_coinduct3 1; +by (etac HTT_coinduct3 1); by (fast_tac (set_cs addSIs HTTgenIs addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] addEs [XH_to_E ListXH]) 1); @@ -160,7 +160,7 @@ val [prem] = goal Hered.thy "A <= HTT ==> Lists(A) <= HTT"; by (safe_tac set_cs); -be HTT_coinduct3 1; +by (etac HTT_coinduct3 1); by (fast_tac (set_cs addSIs HTTgenIs addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] addEs [XH_to_E ListsXH]) 1); @@ -168,7 +168,7 @@ val [prem] = goal Hered.thy "A <= HTT ==> ILists(A) <= HTT"; by (safe_tac set_cs); -be HTT_coinduct3 1; +by (etac HTT_coinduct3 1); by (fast_tac (set_cs addSIs HTTgenIs addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] addEs [XH_to_E IListsXH]) 1); @@ -181,7 +181,7 @@ by (po_coinduct_tac "{p. EX a b.p= & b : HTT & b [= a}" 1); by (fast_tac (ccl_cs addIs prems) 1); by (safe_tac ccl_cs); -bd (poXH RS iffD1) 1; +by (dtac (poXH RS iffD1) 1); by (safe_tac (set_cs addSEs [HTT_bot RS notE])); by (REPEAT_SOME (rtac (POgenXH RS iffD2) ORELSE' etac rev_mp)); by (ALLGOALS (simp_tac (term_ss addsimps HTT_rews))); diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/Set.ML --- a/src/CCL/Set.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/Set.ML Wed Oct 19 09:23:56 1994 +0100 @@ -117,7 +117,7 @@ (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]); goal Set.thy "!!A B C. [| A<=B; B<=C |] ==> A<=C"; -br subsetI 1; +by (rtac subsetI 1); by (REPEAT (eresolve_tac [asm_rl, subsetD] 1)); val subset_trans = result(); @@ -164,7 +164,7 @@ val setup_induction = result(); goal Set.thy "{x.x:A} = A"; -by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1 ORELSE eresolve_tac [CollectD] 1)); +by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1 ORELSE etac CollectD 1)); val trivial_set = result(); (*** Rules for binary union -- Un ***) @@ -235,7 +235,7 @@ (*** Empty sets ***) goalw Set.thy [empty_def] "{x.False} = {}"; -br refl 1; +by (rtac refl 1); val empty_eq = result(); val [prem] = goalw Set.thy [empty_def] "a : {} ==> P"; @@ -245,8 +245,8 @@ val emptyE = make_elim emptyD; val [prem] = goal Set.thy "~ A={} ==> (EX x.x:A)"; -br (prem RS swap) 1; -br equalityI 1; +by (rtac (prem RS swap) 1); +by (rtac equalityI 1); by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD]))); val not_emptyD = result(); diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/Term.ML --- a/src/CCL/Term.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/Term.ML Wed Oct 19 09:23:56 1994 +0100 @@ -27,11 +27,11 @@ val letB = result() RS mp; goalw Term.thy [let_def] "let x be bot in f(x) = bot"; -br caseBbot 1; +by (rtac caseBbot 1); val letBabot = result(); goalw Term.thy [let_def] "let x be t in bot = bot"; -brs ([caseBbot] RL [term_case]) 1; +by (resolve_tac ([caseBbot] RL [term_case]) 1); by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam]))); val letBbbot = result(); @@ -40,17 +40,17 @@ val applyB = result(); goalw Term.thy [apply_def] "bot ` a = bot"; -br caseBbot 1; +by (rtac caseBbot 1); val applyBbot = result(); goalw Term.thy [fix_def] "fix(f) = f(fix(f))"; -by (resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1); +by (resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1); val fixB = result(); goalw Term.thy [letrec_def] "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))"; by (resolve_tac [fixB RS ssubst] 1 THEN - resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1); + resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1); val letrecB = result(); val rawBs = caseBs @ [applyB,applyBbot]; diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/Trancl.ML --- a/src/CCL/Trancl.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/Trancl.ML Wed Oct 19 09:23:56 1994 +0100 @@ -86,14 +86,14 @@ (*Reflexivity of rtrancl*) goal Trancl.thy " : r^*"; -br (rtrancl_unfold RS ssubst) 1; +by (rtac (rtrancl_unfold RS ssubst) 1); by (fast_tac comp_cs 1); val rtrancl_refl = result(); (*Closure under composition with r*) val prems = goal Trancl.thy "[| : r^*; : r |] ==> : r^*"; -br (rtrancl_unfold RS ssubst) 1; +by (rtac (rtrancl_unfold RS ssubst) 1); by (fast_tac (comp_cs addIs prems) 1); val rtrancl_into_rtrancl = result(); diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/Type.ML --- a/src/CCL/Type.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/Type.ML Wed Oct 19 09:23:56 1994 +0100 @@ -67,7 +67,7 @@ (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))), (ALLGOALS (asm_simp_tac term_ss)), (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' - eresolve_tac [bspec])), + etac bspec )), (safe_tac (ccl_cs addSIs prems))]); end; @@ -118,13 +118,13 @@ val major::prems = goal Type.thy "mono(%X.A(X)) ==> mono(%X.[A(X)])"; -br (subsetI RS monoI) 1; -bd (LiftXH RS iffD1) 1; -be disjE 1; -be (disjI1 RS (LiftXH RS iffD2)) 1; -br (disjI2 RS (LiftXH RS iffD2)) 1; -be (major RS monoD RS subsetD) 1; -ba 1; +by (rtac (subsetI RS monoI) 1); +by (dtac (LiftXH RS iffD1) 1); +by (etac disjE 1); +by (etac (disjI1 RS (LiftXH RS iffD2)) 1); +by (rtac (disjI2 RS (LiftXH RS iffD2)) 1); +by (etac (major RS monoD RS subsetD) 1); +by (assume_tac 1); val LiftM = result(); val prems = goal Type.thy @@ -261,8 +261,8 @@ val [major,minor] = goal Type.thy "[| : Sigma(A,B); [| a:A; b:B(a) |] ==> P \ \ |] ==> P"; -br (major RS (XH_to_E SgXH)) 1; -br minor 1; +by (rtac (major RS (XH_to_E SgXH)) 1); +by (rtac minor 1); by (ALLGOALS (fast_tac term_cs)); val SgE2 = result(); @@ -277,15 +277,15 @@ (*** Infinite Data Types ***) val [mono] = goal Type.thy "mono(f) ==> lfp(f) <= gfp(f)"; -br (lfp_lowerbound RS subset_trans) 1; -br (mono RS gfp_lemma3) 1; -br subset_refl 1; +by (rtac (lfp_lowerbound RS subset_trans) 1); +by (rtac (mono RS gfp_lemma3) 1); +by (rtac subset_refl 1); val lfp_subset_gfp = result(); val prems = goal Type.thy "[| a:A; !!x X.[| x:A; ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \ \ t(a) : gfp(B)"; -br coinduct 1; +by (rtac coinduct 1); by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1); by (ALLGOALS (fast_tac (ccl_cs addSIs prems))); val gfpI = result(); @@ -302,7 +302,7 @@ val prems = goal Type.thy "letrec g x be zero$g(x) in g(bot) : Lists(Nat)"; by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1); -br (letrecB RS ssubst) 1; -bw cons_def; +by (rtac (letrecB RS ssubst) 1); +by (rewtac cons_def); by (fast_tac type_cs 1); result(); diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/Wfd.ML --- a/src/CCL/Wfd.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/Wfd.ML Wed Oct 19 09:23:56 1994 +0100 @@ -26,7 +26,7 @@ "[| !!x y. : R ==> Q(x); \ \ ALL x. (ALL y. : R --> y : P) --> x : P; \ \ !!x.Q(x) ==> x:P |] ==> a:P"; -br (p2 RS spec RS mp) 1; +by (rtac (p2 RS spec RS mp) 1); by (fast_tac (set_cs addSIs [p1 RS p3]) 1); val wfd_strengthen_lemma = result(); @@ -36,7 +36,7 @@ val wfd::prems = goal Wfd.thy "[| Wfd(r); :r; :r |] ==> P"; by (subgoal_tac "ALL x. :r --> :r --> P" 1); by (fast_tac (FOL_cs addIs prems) 1); -br (wfd RS wfd_induct) 1; +by (rtac (wfd RS wfd_induct) 1); by (ALLGOALS (fast_tac (ccl_cs addSIs prems))); val wf_anti_sym = result(); @@ -53,11 +53,11 @@ (*must retain the universal formula for later use!*) by (rtac allE 1 THEN assume_tac 1); by (etac mp 1); -br (prem RS wfd_induct) 1; +by (rtac (prem RS wfd_induct) 1); by (rtac (impI RS allI) 1); by (etac tranclE 1); by (fast_tac ccl_cs 1); -be (spec RS mp RS spec RS mp) 1; +by (etac (spec RS mp RS spec RS mp) 1); by (REPEAT (atac 1)); val trancl_wf = result(); @@ -83,27 +83,27 @@ \ !!a a' b b'.[| : ra; p=<,> |] ==> R; \ \ !!a b b'.[| : rb; p = <,> |] ==> R |] ==> \ \ R"; -br (major RS (lexXH RS iffD1) RS exE) 1; +by (rtac (major RS (lexXH RS iffD1) RS exE) 1); by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems))); by (ALLGOALS (fast_tac ccl_cs)); val lexE = result(); val [major,minor] = goal Wfd.thy "[| p : r**s; !!a a' b b'. p = <,> ==> P |] ==>P"; -br (major RS lexE) 1; +by (rtac (major RS lexE) 1); by (ALLGOALS (fast_tac (set_cs addSEs [minor]))); val lex_pair = result(); val [wfa,wfb] = goal Wfd.thy "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)"; -bw Wfd_def; +by (rewtac Wfd_def); by (safe_tac ccl_cs); by (wfd_strengthen_tac "%x.EX a b.x=" 1); by (fast_tac (term_cs addSEs [lex_pair]) 1); by (subgoal_tac "ALL a b.:P" 1); by (fast_tac ccl_cs 1); -br (wfa RS wfd_induct RS allI) 1; -br (wfb RS wfd_induct RS allI) 1;back(); +by (rtac (wfa RS wfd_induct RS allI) 1); +by (rtac (wfb RS wfd_induct RS allI) 1);back(); by (fast_tac (type_cs addSEs [lexE]) 1); val lex_wf = result(); @@ -121,40 +121,40 @@ val major::prems = goal Wfd.thy "[| p : wmap(f,r); !!a b.[| : r; p= |] ==> R |] ==> R"; -br (major RS (wmapXH RS iffD1) RS exE) 1; +by (rtac (major RS (wmapXH RS iffD1) RS exE) 1); by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems))); by (ALLGOALS (fast_tac ccl_cs)); val wmapE = result(); val [wf] = goal Wfd.thy "Wfd(r) ==> Wfd(wmap(f,r))"; -bw Wfd_def; +by (rewtac Wfd_def); by (safe_tac ccl_cs); by (subgoal_tac "ALL b.ALL a.f(a)=b-->a:P" 1); by (fast_tac ccl_cs 1); -br (wf RS wfd_induct RS allI) 1; +by (rtac (wf RS wfd_induct RS allI) 1); by (safe_tac ccl_cs); -be (spec RS mp) 1; +by (etac (spec RS mp) 1); by (safe_tac (ccl_cs addSEs [wmapE])); -be (spec RS mp RS spec RS mp) 1; -ba 1; -br refl 1; +by (etac (spec RS mp RS spec RS mp) 1); +by (assume_tac 1); +by (rtac refl 1); val wmap_wf = result(); (* Projections *) val prems = goal Wfd.thy " : r ==> <,> : wmap(fst,r)"; -br wmapI 1; +by (rtac wmapI 1); by (simp_tac (term_ss addsimps prems) 1); val wfstI = result(); val prems = goal Wfd.thy " : r ==> <,> : wmap(snd,r)"; -br wmapI 1; +by (rtac wmapI 1); by (simp_tac (term_ss addsimps prems) 1); val wsndI = result(); val prems = goal Wfd.thy " : r ==> <>,>> : wmap(thd,r)"; -br wmapI 1; +by (rtac wmapI 1); by (simp_tac (term_ss addsimps prems) 1); val wthdI = result(); @@ -172,7 +172,7 @@ val prems = goalw Wfd.thy [wf_def] "Wfd(wf(R))"; by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1); by (ALLGOALS (asm_simp_tac CCL_ss)); -br Empty_wf 1; +by (rtac Empty_wf 1); val wf_wf = result(); goalw Wfd.thy [NatPR_def] "p : NatPR <-> (EX x:Nat.p=)"; @@ -190,7 +190,7 @@ by (safe_tac set_cs); by (wfd_strengthen_tac "%x.x:Nat" 1); by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1); -be Nat_ind 1; +by (etac Nat_ind 1); by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH]))); val NatPR_wf = result(); @@ -198,7 +198,7 @@ by (safe_tac set_cs); by (wfd_strengthen_tac "%x.x:List(A)" 1); by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1); -be List_ind 1; +by (etac List_ind 1); by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH]))); val ListPR_wf = result(); diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/coinduction.ML --- a/src/CCL/coinduction.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/coinduction.ML Wed Oct 19 09:23:56 1994 +0100 @@ -7,8 +7,8 @@ *) val [mono,prem] = goal Lfp.thy "[| mono(f); a : f(lfp(f)) |] ==> a : lfp(f)"; -br ((mono RS lfp_Tarski) RS ssubst) 1; -br prem 1; +by (rtac ((mono RS lfp_Tarski) RS ssubst) 1); +by (rtac prem 1); val lfpI = result(); val prems = goal CCL.thy "[| a=a'; a' : A |] ==> a : A"; @@ -41,7 +41,7 @@ (** POgen **) goal Term.thy " : PO"; -br (po_refl RS (XH_to_D PO_iff)) 1; +by (rtac (po_refl RS (XH_to_D PO_iff)) 1); val PO_refl = result(); val POgenIs = map (mk_genIs Term.thy data_defs POgenXH POgen_mono) @@ -71,7 +71,7 @@ (** EQgen **) goal Term.thy " : EQ"; -br (refl RS (EQ_iff RS iffD1)) 1; +by (rtac (refl RS (EQ_iff RS iffD1)) 1); val EQ_refl = result(); val EQgenIs = map (mk_genIs Term.thy data_defs EQgenXH EQgen_mono) diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/eval.ML --- a/src/CCL/eval.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/eval.ML Wed Oct 19 09:23:56 1994 +0100 @@ -22,16 +22,16 @@ val major::prems = goalw thy [let_def] "[| t ---> a; f(a) ---> c |] ==> let x be t in f(x) ---> c"; -br (major RS canonical) 1; +by (rtac (major RS canonical) 1); by (REPEAT (DEPTH_SOLVE_1 (resolve_tac ([major]@prems@(!EVal_rls)) 1 ORELSE - eresolve_tac [substitute] 1))); + etac substitute 1))); val letV = result(); val prems = goalw thy [fix_def] "f(fix(f)) ---> c ==> fix(f) ---> c"; -br applyV 1; -br lamV 1; -brs prems 1; +by (rtac applyV 1); +by (rtac lamV 1); +by (resolve_tac prems 1); val fixV = result(); val prems = goalw thy [letrec_def] diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/genrec.ML --- a/src/CCL/genrec.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/genrec.ML Wed Oct 19 09:23:56 1994 +0100 @@ -12,18 +12,18 @@ \ !!p g.[| p:A; ALL x:{x: A. :wf(R)}. g(x) : D(x) |] ==>\ \ h(p,g) : D(p) |] ==> \ \ letrec g x be h(x,g) in g(a) : D(a)"; -br (major RS rev_mp) 1; -br (wf_wf RS wfd_induct) 1; -br (letrecB RS ssubst) 1; -br impI 1; -bes prems 1; -br ballI 1; -be (spec RS mp RS mp) 1; +by (rtac (major RS rev_mp) 1); +by (rtac (wf_wf RS wfd_induct) 1); +by (rtac (letrecB RS ssubst) 1); +by (rtac impI 1); +by (eresolve_tac prems 1); +by (rtac ballI 1); +by (etac (spec RS mp RS mp) 1); by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1)); val letrecT = result(); goalw Wfd.thy [SPLIT_def] "SPLIT(,B) = B(a,b)"; -br set_ext 1; +by (rtac set_ext 1); by (fast_tac ccl_cs 1); val SPLITB = result(); @@ -33,11 +33,11 @@ \ ALL x:A.ALL y:{y: B. <,>:wf(R)}. g(x,y) : D(x,y) |] ==>\ \ h(p,q,g) : D(p,q) |] ==> \ \ letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"; -br (SPLITB RS subst) 1; +by (rtac (SPLITB RS subst) 1); by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); -br (SPLITB RS ssubst) 1; +by (rtac (SPLITB RS ssubst) 1); by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); -br (SPLITB RS subst) 1; +by (rtac (SPLITB RS subst) 1); by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); val letrec2T = result(); @@ -53,11 +53,11 @@ \ g(x,y,z) : D(x,y,z) |] ==>\ \ h(p,q,r,g) : D(p,q,r) |] ==> \ \ letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"; -br (lemma RS subst) 1; +by (rtac (lemma RS subst) 1); by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); by (simp_tac (ccl_ss addsimps [SPLITB]) 1); by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); -br (lemma RS subst) 1; +by (rtac (lemma RS subst) 1); by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); val letrec3T = result(); @@ -99,9 +99,9 @@ \ ALL x:{x:A.:wf(R)}.g(x):D(x) ==> a:A; \ \ ALL x:{x:A.:wf(R)}.g(x):D(x) ==> :wf(R) |] ==> \ \ P"; -brs (prems RL prems) 1; -brs (prems RL [sym]) 1; -br rcallT 1; +by (resolve_tac (prems RL prems) 1); +by (resolve_tac (prems RL [sym]) 1); +by (rtac rcallT 1); by (REPEAT (ares_tac prems 1)); val hyprcallT = result(); @@ -109,9 +109,9 @@ "[| g(a) = b; ALL x:{x:A.:wf(R)}.g(x):D(x);\ \ [| b=g(a); g(a) : D(a) |] ==> P; a:A; :wf(R) |] ==> \ \ P"; -brs (prems) 1; -brs (prems RL [sym]) 1; -br rcallT 1; +by (resolve_tac (prems) 1); +by (resolve_tac (prems RL [sym]) 1); +by (rtac rcallT 1); by (REPEAT (ares_tac prems 1)); val hyprcallT = result(); @@ -120,9 +120,9 @@ \ [| c=g(a,b); g(a,b) : D(a,b) |] ==> P; \ \ a:A; b:B; <,>:wf(R) |] ==> \ \ P"; -brs (prems) 1; -brs (prems RL [sym]) 1; -br rcall2T 1; +by (resolve_tac (prems) 1); +by (resolve_tac (prems RL [sym]) 1); +by (rtac rcall2T 1); by (REPEAT (ares_tac prems 1)); val hyprcall2T = result(); @@ -132,9 +132,9 @@ \ [| d=g(a,b,c); g(a,b,c) : D(a,b,c) |] ==> P; \ \ a:A; b:B; c:C; <>,>> : wf(R) |] ==> \ \ P"; -brs (prems) 1; -brs (prems RL [sym]) 1; -br rcall3T 1; +by (resolve_tac (prems) 1); +by (resolve_tac (prems RL [sym]) 1); +by (rtac rcall3T 1); by (REPEAT (ares_tac prems 1)); val hyprcall3T = result(); diff -r 49fc43cd6a35 -r 0db578095e6a src/CCL/typecheck.ML --- a/src/CCL/typecheck.ML Wed Oct 12 16:38:58 1994 +0100 +++ b/src/CCL/typecheck.ML Wed Oct 19 09:23:56 1994 +0100 @@ -13,7 +13,7 @@ val Subtype_canTs = let fun tac prems = cut_facts_tac prems 1 THEN REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE - eresolve_tac [SubtypeE] 1) + etac SubtypeE 1) fun solve s = prove_goal Type.thy s (fn prems => [tac prems]) in map solve ["P(one) ==> one : {x:Unit.P(x)}", @@ -31,7 +31,7 @@ val Subtype_canTs = let fun tac prems = cut_facts_tac prems 1 THEN REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE - eresolve_tac [SubtypeE] 1) + etac SubtypeE 1) fun solve s = prove_goal Type.thy s (fn prems => [tac prems]) in map solve ["a : {x:A. b:{y:B(a).P()}} ==> : {x:Sigma(A,B).P(x)}", @@ -44,8 +44,8 @@ val prems = goal Type.thy "[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B"; by (cut_facts_tac prems 1); -be (letB RS ssubst) 1; -ba 1; +by (etac (letB RS ssubst) 1); +by (assume_tac 1); val letT = result(); val prems = goal Type.thy