Installation of new simplfier. Previously appeared to set up the old
simplifier to rewrite with the partial ordering [=, something not possible
with the new simplifier. But such rewriting appears not to have actually
been used, and there were few complications. In terms.ML setloop was used
to avoid infinite rewriting with the letrec rule. Congruence rules were
deleted, and an occasional SIMP_TAC had to become asm_simp_tac.
--- a/src/CCL/CCL.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/CCL.ML Mon Sep 20 17:02:11 1993 +0200
@@ -10,30 +10,10 @@
val ccl_data_defs = [apply_def,fix_def];
-(*** Simplifier for pre-order and equality ***)
-
-structure CCL_SimpData : SIMP_DATA =
- struct
- val refl_thms = [refl, po_refl, iff_refl]
- val trans_thms = [trans, iff_trans, po_trans]
- val red1 = iffD1
- val red2 = iffD2
- val mk_rew_rules = mk_rew_rules
- val case_splits = [] (*NO IF'S!*)
- val norm_thms = norm_thms
- val subst_thms = [subst];
- val dest_red = dest_red
- end;
-
-structure CCL_Simp = SimpFun(CCL_SimpData);
-open CCL_Simp;
-
-val auto_ss = empty_ss setauto (fn hyps => ares_tac (TrueI::hyps));
-
val po_refl_iff_T = make_iff_T po_refl;
-val CCL_ss = auto_ss addcongs (FOL_congs @ set_congs)
- addrews ([po_refl_iff_T] @ FOL_rews @ mem_rews);
+val CCL_ss = FOL_ss addcongs set_congs
+ addsimps ([po_refl_iff_T] @ mem_rews);
(*** Congruence Rules ***)
@@ -46,7 +26,7 @@
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
goal CCL.thy "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
-by (SIMP_TAC (CCL_ss addrews [eq_iff]) 1);
+by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
by (fast_tac (set_cs addIs [po_abstractn]) 1);
val abstractn = standard (allI RS (result() RS mp));
@@ -61,11 +41,6 @@
in do_prems 1 (prems_of thm) thm
end;
-fun ccl_mk_congs thy cs = map abs_prems (mk_congs thy cs);
-
-val ccl_congs = ccl_mk_congs CCL.thy
- ["op [=","SIM","POgen","EQgen","pair","lambda","case","op `","fix"];
-
val caseBs = [caseBtrue,caseBfalse,caseBpair,caseBlam,caseBbot];
(*** Termination and Divergence ***)
@@ -85,17 +60,16 @@
by (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals]))));
val eq_lemma = result();
-fun mk_inj_rl thy rews congs s =
+fun mk_inj_rl thy rews s =
let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]);
val inj_lemmas = flat (map mk_inj_lemmas rews);
val tac = REPEAT (ares_tac [iffI,allI,conjI] 1 ORELSE
eresolve_tac inj_lemmas 1 ORELSE
- ASM_SIMP_TAC (CCL_ss addrews rews
- addcongs congs) 1)
+ asm_simp_tac (CCL_ss addsimps rews) 1)
in prove_goal thy s (fn _ => [tac])
end;
-val ccl_injs = map (mk_inj_rl CCL.thy caseBs ccl_congs)
+val ccl_injs = map (mk_inj_rl CCL.thy caseBs)
["<a,b> = <a',b'> <-> (a=a' & b=b')",
"(lam x.b(x) = lam x.b'(x)) <-> ((ALL z.b(z)=b'(z)))"];
@@ -124,7 +98,7 @@
fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b");
val lemma = prove_goal CCL.thy "t=t' --> case(t,b,c,d,e) = case(t',b,c,d,e)"
- (fn _ => [SIMP_TAC (CCL_ss addcongs ccl_congs) 1]) RS mp;
+ (fn _ => [simp_tac CCL_ss 1]) RS mp;
fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL
[distinctness RS notE,sym RS (distinctness RS notE)];
in
@@ -143,7 +117,7 @@
fun mk_dstnct_thms thy defs inj_rls xs =
let fun mk_dstnct_thm rls s = prove_goalw thy defs s
- (fn _ => [SIMP_TAC (CCL_ss addrews (rls@inj_rls)) 1])
+ (fn _ => [simp_tac (CCL_ss addsimps (rls@inj_rls)) 1])
in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end;
fun mkall_dstnct_thms thy defs i_rls xss = flat (map (mk_dstnct_thms thy defs i_rls) xss);
@@ -158,7 +132,7 @@
val XH_to_Es = map XH_to_E;
val ccl_rews = caseBs @ ccl_injs @ ccl_dstncts;
-val ccl_ss = CCL_ss addrews ccl_rews addcongs ccl_congs;
+val ccl_ss = CCL_ss addsimps ccl_rews;
val ccl_cs = set_cs addSEs (pair_inject::(ccl_dstncts RL [notE]))
addSDs (XH_to_Ds ccl_injs);
@@ -179,7 +153,7 @@
br monoI 1;
by (safe_tac ccl_cs);
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
-by (ALLGOALS (SIMP_TAC ccl_ss));
+by (ALLGOALS (simp_tac ccl_ss));
by (ALLGOALS (fast_tac set_cs));
val POgen_mono = result();
@@ -194,7 +168,7 @@
"t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & a [= a' & b [= b') | \
\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.f(x) [= f'(x)))";
-by (SIMP_TAC (ccl_ss addrews [PO_iff]) 1);
+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;
@@ -202,27 +176,27 @@
goal CCL.thy "bot [= b";
br (poXH RS iffD2) 1;
-by (SIMP_TAC ccl_ss 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 (SIMP_TAC ccl_ss 1);
+by (simp_tac ccl_ss 1);
val bot_poleast = result() RS mp;
goal CCL.thy "<a,b> [= <a',b'> <-> a [= a' & b [= b'";
br (poXH RS iff_trans) 1;
-by (SIMP_TAC ccl_ss 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 (SIMP_TAC ccl_ss 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);
+by (asm_simp_tac ccl_ss 1);
by (fast_tac ccl_cs 1);
val po_lam = result();
@@ -275,7 +249,7 @@
fun mk_thm s = prove_goal CCL.thy s (fn _ =>
[rtac notI 1,dtac case_pocong 1,etac rev_mp 5,
- ALLGOALS (SIMP_TAC ccl_ss),
+ ALLGOALS (simp_tac ccl_ss),
REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]);
val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm
@@ -300,7 +274,7 @@
br monoI 1;
by (safe_tac set_cs);
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
-by (ALLGOALS (SIMP_TAC ccl_ss));
+by (ALLGOALS (simp_tac ccl_ss));
by (ALLGOALS (fast_tac set_cs));
val EQgen_mono = result();
@@ -321,7 +295,7 @@
\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : EQ & <b,b'> : EQ) | \
\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : EQ))" 1);
be rev_mp 1;
-by (SIMP_TAC (CCL_ss addrews [EQ_iff RS iff_sym]) 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;
@@ -345,7 +319,7 @@
goalw CCL.thy [apply_def] "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
by (safe_tac ccl_cs);
-by (SIMP_TAC ccl_ss 1);
+by (simp_tac ccl_ss 1);
val cond_eta = result() RS mp;
goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";
--- a/src/CCL/Fix.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/Fix.ML Mon Sep 20 17:02:11 1993 +0200
@@ -8,20 +8,13 @@
open Fix;
-val prems = goalw Fix.thy [INCL_def]
- "[| !!x.P(x) <-> Q(x) |] ==> INCL(%x.P(x)) <-> INCL(%x.Q(x))";
-by (REPEAT (ares_tac ([refl] @ FOL_congs @ set_congs @ prems) 1));
-val INCL_cong = result();
-
-val fix_congs = [INCL_cong] @ ccl_mk_congs Fix.thy ["napply"];
-
(*** Fixed Point Induction ***)
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 (Nat_ind RS ballI) 1 THEN atac 1);
-by (ALLGOALS (SIMP_TAC term_ss));
+by (ALLGOALS (simp_tac term_ss));
by (REPEAT (ares_tac [base,step] 1));
val fix_ind = result();
@@ -48,7 +41,6 @@
by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1);
val inclE = result();
-val fix_ss = term_ss addcongs fix_congs;
(*** Lemmas for Inclusive Predicates ***)
@@ -76,7 +68,7 @@
val ball_INCL = result();
goal Fix.thy "INCL(%x.a(x) = b(x)::'a::prog)";
-by (SIMP_TAC (fix_ss addrews [eq_iff]) 1);
+by (simp_tac (term_ss addsimps [eq_iff]) 1);
by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
val eq_INCL = result();
@@ -89,9 +81,9 @@
val fix_idgenfp = result();
goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x";
-by (SIMP_TAC term_ss 1);
+by (simp_tac term_ss 1);
br (term_case RS allI) 1;
-by (ALLGOALS (SIMP_TAC term_ss));
+by (ALLGOALS (simp_tac term_ss));
val id_idgenfp = result();
(* All fixed points are lam-expressions *)
@@ -106,12 +98,12 @@
val prems = goalw Fix.thy [idgen_def]
"[| a = b; a ` t = u |] ==> b ` t = u";
-by (SIMP_TAC (term_ss addrews (prems RL [sym])) 1);
+by (simp_tac (term_ss addsimps (prems RL [sym])) 1);
val l_lemma= result();
val idgen_lemmas =
let fun mk_thm s = prove_goalw Fix.thy [idgen_def] s
- (fn [prem] => [rtac (prem RS l_lemma) 1,SIMP_TAC term_ss 1])
+ (fn [prem] => [rtac (prem RS l_lemma) 1,simp_tac term_ss 1])
in map mk_thm
[ "idgen(d) = d ==> d ` bot = bot",
"idgen(d) = d ==> d ` true = true",
@@ -141,7 +133,7 @@
\ POgen({p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t & b = d ` t)})";
by (REPEAT (step_tac term_cs 1));
by (term_case_tac "t" 1);
-by (ALLGOALS (SIMP_TAC (term_ss addrews (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
+by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
by (ALLGOALS (fast_tac set_cs));
val lemma1 = result();
@@ -157,7 +149,7 @@
\ {p.EX a b.p=<a,b> & b = d ` a} <= POgen({p.EX a b.p=<a,b> & b = d ` a})";
by (REPEAT (step_tac term_cs 1));
by (term_case_tac "a" 1);
-by (ALLGOALS (SIMP_TAC (term_ss addrews (POgenXH::([prem] RL idgen_lemmas)))));
+by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas)))));
by (ALLGOALS (fast_tac set_cs));
val lemma2 = result();
@@ -165,7 +157,7 @@
"idgen(d) = d ==> lam x.x [= d";
br (allI RS po_eta) 1;
br (lemma2 RSN(2,po_coinduct)) 1;
-by (SIMP_TAC term_ss 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();
@@ -196,7 +188,7 @@
brs prems 1;
br (applyB RS ssubst )1;
by (res_inst_tac [("t","xa")] term_case 1);
-by (ALLGOALS (SIMP_TAC term_ss));
+by (ALLGOALS (simp_tac term_ss));
by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems))));
val term_ind = result();
--- a/src/CCL/Hered.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/Hered.ML Mon Sep 20 17:02:11 1993 +0200
@@ -10,8 +10,6 @@
fun type_of_terms (Const("Trueprop",_) $ (Const("op =",(Type ("fun", [t,_])))$_$_)) = t;
-val cong_rls = ccl_mk_congs Hered.thy ["HTTgen"];
-
(*** Hereditary Termination ***)
goalw Hered.thy [HTTgen_def] "mono(%X.HTTgen(X))";
@@ -54,16 +52,16 @@
goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
br (HTTXH RS iff_trans) 1;
-by (SIMP_TAC term_ss 1);
+by (simp_tac term_ss 1);
by (safe_tac term_cs);
-by (ASM_SIMP_TAC term_ss 1);
+by (asm_simp_tac term_ss 1);
by (fast_tac term_cs 1);
val HTT_lam = result();
local
val raw_HTTrews = [HTT_bot,HTT_true,HTT_false,HTT_pair,HTT_lam];
fun mk_thm s = prove_goalw Hered.thy data_defs s (fn _ =>
- [SIMP_TAC (term_ss addrews raw_HTTrews) 1]);
+ [simp_tac (term_ss addsimps raw_HTTrews) 1]);
in
val HTT_rews = raw_HTTrews @
map mk_thm ["one : HTT",
@@ -115,22 +113,22 @@
(*** Formation Rules for Types ***)
goal Hered.thy "Unit <= HTT";
-by (SIMP_TAC (CCL_ss addrews ([subsetXH,UnitXH] @ HTT_rews)) 1);
+by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1);
val UnitF = result();
goal Hered.thy "Bool <= HTT";
-by (SIMP_TAC (CCL_ss addrews ([subsetXH,BoolXH] @ HTT_rews)) 1);
+by (simp_tac (CCL_ss addsimps ([subsetXH,BoolXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
val BoolF = result();
val prems = goal Hered.thy "[| A <= HTT; B <= HTT |] ==> A + B <= HTT";
-by (SIMP_TAC (CCL_ss addrews ([subsetXH,PlusXH] @ HTT_rews)) 1);
+by (simp_tac (CCL_ss addsimps ([subsetXH,PlusXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
val PlusF = result();
val prems = goal Hered.thy
"[| A <= HTT; !!x.x:A ==> B(x) <= HTT |] ==> SUM x:A.B(x) <= HTT";
-by (SIMP_TAC (CCL_ss addrews ([subsetXH,SgXH] @ HTT_rews)) 1);
+by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
val SigmaF = result();
@@ -139,7 +137,7 @@
(*Proof by induction - needs induction rule for type*)
goal Hered.thy "Nat <= HTT";
-by (SIMP_TAC (term_ss addrews [subsetXH]) 1);
+by (simp_tac (term_ss addsimps [subsetXH]) 1);
by (safe_tac set_cs);
be Nat_ind 1;
by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD]))));
@@ -186,7 +184,7 @@
bd (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 addrews HTT_rews)));
+by (ALLGOALS (simp_tac (term_ss addsimps HTT_rews)));
by (ALLGOALS (fast_tac ccl_cs));
val HTT_po_op = result();
--- a/src/CCL/Set.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/Set.ML Mon Sep 20 17:02:11 1993 +0200
@@ -22,18 +22,13 @@
by (resolve_tac (prems RL [mem_Collect_iff RS iffD1]) 1);
val CollectD = result();
+val CollectE = make_elim CollectD;
+
val [prem] = goal Set.thy "[| !!x. x:A <-> x:B |] ==> A = B";
by (rtac (set_extension RS iffD2) 1);
by (rtac (prem RS allI) 1);
val set_ext = result();
-val prems = goal Set.thy "[| !!x. P(x) <-> Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
-by (REPEAT (ares_tac [set_ext,iffI,CollectI] 1 ORELSE
- eresolve_tac ([CollectD] RL (prems RL [iffD1,iffD2])) 1));
-val Collect_cong = result();
-
-val CollectE = make_elim CollectD;
-
(*** Bounded quantifiers ***)
val prems = goalw Set.thy [Ball_def]
--- a/src/CCL/Term.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/Term.ML Mon Sep 20 17:02:11 1993 +0200
@@ -19,15 +19,11 @@
val data_defs = simp_defs @ ind_defs @ [napply_def];
val genrec_defs = [letrec_def,letrec2_def,letrec3_def];
-val term_congs = ccl_mk_congs Term.thy
- ["inl","inr","succ","op .","split","if","when","ncase","nrec","lcase","lrec",
- "fst","snd","thd","let","letrec","letrec2","letrec3","napply"];
-
(*** Beta Rules, including strictness ***)
goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
by (res_inst_tac [("t","t")] term_case 1);
-by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
+by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
val letB = result() RS mp;
goalw Term.thy [let_def] "let x be bot in f(x) = bot";
@@ -36,11 +32,11 @@
goalw Term.thy [let_def] "let x be t in bot = bot";
brs ([caseBbot] RL [term_case]) 1;
-by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
+by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
val letBbbot = result();
goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)";
-by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
+by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
val applyB = result();
goalw Term.thy [apply_def] "bot ` a = bot";
@@ -57,10 +53,16 @@
resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1);
val letrecB = result();
-val rawBs = caseBs @ [applyB,applyBbot,letrecB];
+val rawBs = caseBs @ [applyB,applyBbot];
fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
- (fn _ => [SIMP_TAC (CCL_ss addrews rawBs addcongs term_congs) 1]);
+ (fn _ => [rtac (letrecB RS ssubst) 1,
+ simp_tac (CCL_ss addsimps rawBs) 1]);
+fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
+
+fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
+ (fn _ => [simp_tac (CCL_ss addsimps rawBs
+ setloop (rtac (letrecB RS ssubst))) 1]);
fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
val ifBtrue = mk_beta_rl "if true then t else u = t";
@@ -114,8 +116,7 @@
(*** Constructors are injective ***)
val term_injs = map (mk_inj_rl Term.thy
- [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons]
- (ccl_congs @ term_congs))
+ [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons])
["(inl(a) = inl(a')) <-> (a=a')",
"(inr(a) = inr(a')) <-> (a=a')",
"(succ(a) = succ(a')) <-> (a=a')",
@@ -130,7 +131,7 @@
local
fun mk_thm s = prove_goalw Term.thy data_defs s (fn _ =>
- [SIMP_TAC (ccl_ss addrews (ccl_porews)) 1]);
+ [simp_tac (ccl_ss addsimps (ccl_porews)) 1]);
in
val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
"inr(b) [= inr(b') <-> b [= b'",
@@ -141,6 +142,7 @@
(*** Rewriting and Proving ***)
val term_rews = termBs @ term_injs @ term_dstncts @ ccl_porews @ term_porews;
-val term_ss = ccl_ss addrews term_rews addcongs term_congs;
+val term_ss = ccl_ss addsimps term_rews;
-val term_cs = ccl_cs addSEs (term_dstncts RL [notE]) addSDs (XH_to_Ds term_injs);
+val term_cs = ccl_cs addSEs (term_dstncts RL [notE])
+ addSDs (XH_to_Ds term_injs);
--- a/src/CCL/Type.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/Type.ML Mon Sep 20 17:02:11 1993 +0200
@@ -65,7 +65,7 @@
fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s
(fn major::prems => [(resolve_tac ([major] RL top_crls) 1),
(REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
- (ALLGOALS (ASM_SIMP_TAC term_ss)),
+ (ALLGOALS (asm_simp_tac term_ss)),
(ALLGOALS (ares_tac (prems RL [lemma]) ORELSE'
eresolve_tac [bspec])),
(safe_tac (ccl_cs addSIs prems))]);
@@ -239,7 +239,7 @@
fun mk_prec_tac inds s = prove_goal Type.thy s
(fn major::prems => [resolve_tac ([major] RL inds) 1,
- ALLGOALS (SIMP_TAC term_ss THEN'
+ ALLGOALS (simp_tac term_ss THEN'
fast_tac (set_cs addSIs prems))]);
val prec_tac = mk_prec_tac inds;
--- a/src/CCL/Wfd.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/Wfd.ML Mon Sep 20 17:02:11 1993 +0200
@@ -14,10 +14,6 @@
(***********)
-val wfd_congs = mk_congs Wfd.thy ["Wfd","wf","op **","wmap","ListPR"];
-
-(***********)
-
val [major,prem] = goalw Wfd.thy [Wfd_def]
"[| Wfd(R); \
\ !!x.[| ALL y. <y,x>: R --> P(y) |] ==> P(x) |] ==> \
@@ -149,17 +145,17 @@
val prems = goal Wfd.thy "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
br wmapI 1;
-by (SIMP_TAC (term_ss addrews prems) 1);
+by (simp_tac (term_ss addsimps prems) 1);
val wfstI = result();
val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
br wmapI 1;
-by (SIMP_TAC (term_ss addrews prems) 1);
+by (simp_tac (term_ss addsimps prems) 1);
val wsndI = result();
val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)";
br wmapI 1;
-by (SIMP_TAC (term_ss addrews prems) 1);
+by (simp_tac (term_ss addsimps prems) 1);
val wthdI = result();
(*** Ground well-founded relations ***)
@@ -175,7 +171,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 addcongs wfd_congs)));
+by (ALLGOALS (asm_simp_tac CCL_ss));
br Empty_wf 1;
val wf_wf = result();
--- a/src/CCL/ccl.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/ccl.ML Mon Sep 20 17:02:11 1993 +0200
@@ -10,30 +10,10 @@
val ccl_data_defs = [apply_def,fix_def];
-(*** Simplifier for pre-order and equality ***)
-
-structure CCL_SimpData : SIMP_DATA =
- struct
- val refl_thms = [refl, po_refl, iff_refl]
- val trans_thms = [trans, iff_trans, po_trans]
- val red1 = iffD1
- val red2 = iffD2
- val mk_rew_rules = mk_rew_rules
- val case_splits = [] (*NO IF'S!*)
- val norm_thms = norm_thms
- val subst_thms = [subst];
- val dest_red = dest_red
- end;
-
-structure CCL_Simp = SimpFun(CCL_SimpData);
-open CCL_Simp;
-
-val auto_ss = empty_ss setauto (fn hyps => ares_tac (TrueI::hyps));
-
val po_refl_iff_T = make_iff_T po_refl;
-val CCL_ss = auto_ss addcongs (FOL_congs @ set_congs)
- addrews ([po_refl_iff_T] @ FOL_rews @ mem_rews);
+val CCL_ss = FOL_ss addcongs set_congs
+ addsimps ([po_refl_iff_T] @ mem_rews);
(*** Congruence Rules ***)
@@ -46,7 +26,7 @@
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
goal CCL.thy "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
-by (SIMP_TAC (CCL_ss addrews [eq_iff]) 1);
+by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
by (fast_tac (set_cs addIs [po_abstractn]) 1);
val abstractn = standard (allI RS (result() RS mp));
@@ -61,11 +41,6 @@
in do_prems 1 (prems_of thm) thm
end;
-fun ccl_mk_congs thy cs = map abs_prems (mk_congs thy cs);
-
-val ccl_congs = ccl_mk_congs CCL.thy
- ["op [=","SIM","POgen","EQgen","pair","lambda","case","op `","fix"];
-
val caseBs = [caseBtrue,caseBfalse,caseBpair,caseBlam,caseBbot];
(*** Termination and Divergence ***)
@@ -85,17 +60,16 @@
by (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals]))));
val eq_lemma = result();
-fun mk_inj_rl thy rews congs s =
+fun mk_inj_rl thy rews s =
let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]);
val inj_lemmas = flat (map mk_inj_lemmas rews);
val tac = REPEAT (ares_tac [iffI,allI,conjI] 1 ORELSE
eresolve_tac inj_lemmas 1 ORELSE
- ASM_SIMP_TAC (CCL_ss addrews rews
- addcongs congs) 1)
+ asm_simp_tac (CCL_ss addsimps rews) 1)
in prove_goal thy s (fn _ => [tac])
end;
-val ccl_injs = map (mk_inj_rl CCL.thy caseBs ccl_congs)
+val ccl_injs = map (mk_inj_rl CCL.thy caseBs)
["<a,b> = <a',b'> <-> (a=a' & b=b')",
"(lam x.b(x) = lam x.b'(x)) <-> ((ALL z.b(z)=b'(z)))"];
@@ -124,7 +98,7 @@
fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b");
val lemma = prove_goal CCL.thy "t=t' --> case(t,b,c,d,e) = case(t',b,c,d,e)"
- (fn _ => [SIMP_TAC (CCL_ss addcongs ccl_congs) 1]) RS mp;
+ (fn _ => [simp_tac CCL_ss 1]) RS mp;
fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL
[distinctness RS notE,sym RS (distinctness RS notE)];
in
@@ -143,7 +117,7 @@
fun mk_dstnct_thms thy defs inj_rls xs =
let fun mk_dstnct_thm rls s = prove_goalw thy defs s
- (fn _ => [SIMP_TAC (CCL_ss addrews (rls@inj_rls)) 1])
+ (fn _ => [simp_tac (CCL_ss addsimps (rls@inj_rls)) 1])
in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end;
fun mkall_dstnct_thms thy defs i_rls xss = flat (map (mk_dstnct_thms thy defs i_rls) xss);
@@ -158,7 +132,7 @@
val XH_to_Es = map XH_to_E;
val ccl_rews = caseBs @ ccl_injs @ ccl_dstncts;
-val ccl_ss = CCL_ss addrews ccl_rews addcongs ccl_congs;
+val ccl_ss = CCL_ss addsimps ccl_rews;
val ccl_cs = set_cs addSEs (pair_inject::(ccl_dstncts RL [notE]))
addSDs (XH_to_Ds ccl_injs);
@@ -179,7 +153,7 @@
br monoI 1;
by (safe_tac ccl_cs);
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
-by (ALLGOALS (SIMP_TAC ccl_ss));
+by (ALLGOALS (simp_tac ccl_ss));
by (ALLGOALS (fast_tac set_cs));
val POgen_mono = result();
@@ -194,7 +168,7 @@
"t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & a [= a' & b [= b') | \
\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.f(x) [= f'(x)))";
-by (SIMP_TAC (ccl_ss addrews [PO_iff]) 1);
+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;
@@ -202,27 +176,27 @@
goal CCL.thy "bot [= b";
br (poXH RS iffD2) 1;
-by (SIMP_TAC ccl_ss 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 (SIMP_TAC ccl_ss 1);
+by (simp_tac ccl_ss 1);
val bot_poleast = result() RS mp;
goal CCL.thy "<a,b> [= <a',b'> <-> a [= a' & b [= b'";
br (poXH RS iff_trans) 1;
-by (SIMP_TAC ccl_ss 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 (SIMP_TAC ccl_ss 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);
+by (asm_simp_tac ccl_ss 1);
by (fast_tac ccl_cs 1);
val po_lam = result();
@@ -275,7 +249,7 @@
fun mk_thm s = prove_goal CCL.thy s (fn _ =>
[rtac notI 1,dtac case_pocong 1,etac rev_mp 5,
- ALLGOALS (SIMP_TAC ccl_ss),
+ ALLGOALS (simp_tac ccl_ss),
REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]);
val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm
@@ -300,7 +274,7 @@
br monoI 1;
by (safe_tac set_cs);
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
-by (ALLGOALS (SIMP_TAC ccl_ss));
+by (ALLGOALS (simp_tac ccl_ss));
by (ALLGOALS (fast_tac set_cs));
val EQgen_mono = result();
@@ -321,7 +295,7 @@
\ (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : EQ & <b,b'> : EQ) | \
\ (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : EQ))" 1);
be rev_mp 1;
-by (SIMP_TAC (CCL_ss addrews [EQ_iff RS iff_sym]) 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;
@@ -345,7 +319,7 @@
goalw CCL.thy [apply_def] "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
by (safe_tac ccl_cs);
-by (SIMP_TAC ccl_ss 1);
+by (simp_tac ccl_ss 1);
val cond_eta = result() RS mp;
goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";
--- a/src/CCL/coinduction.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/coinduction.ML Mon Sep 20 17:02:11 1993 +0200
@@ -12,11 +12,11 @@
val lfpI = result();
val prems = goal CCL.thy "[| a=a'; a' : A |] ==> a : A";
-by (SIMP_TAC (term_ss addrews prems) 1);
+by (simp_tac (term_ss addsimps prems) 1);
val ssubst_single = result();
val prems = goal CCL.thy "[| a=a'; b=b'; <a',b'> : A |] ==> <a,b> : A";
-by (SIMP_TAC (term_ss addrews prems) 1);
+by (simp_tac (term_ss addsimps prems) 1);
val ssubst_pair = result();
(***)
@@ -33,7 +33,7 @@
fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
(fn prems => [rtac (genXH RS iffD2) 1,
- (SIMP_TAC term_ss 1),
+ (simp_tac term_ss 1),
TRY (fast_tac (term_cs addIs
([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
@ prems)) 1)]);
@@ -75,20 +75,20 @@
val EQ_refl = result();
val EQgenIs = map (mk_genIs Term.thy data_defs EQgenXH EQgen_mono)
- ["<true,true> : EQgen(R)",
- "<false,false> : EQgen(R)",
- "[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
- "[|!!x. <b(x),b'(x)> : R |] ==> <lam x.b(x),lam x.b'(x)> : EQgen(R)",
- "<one,one> : EQgen(R)",
- "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
-\ <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
- "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
-\ <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
- "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
- "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
-\ <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
- "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
- "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); \
+["<true,true> : EQgen(R)",
+ "<false,false> : EQgen(R)",
+ "[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
+ "[|!!x. <b(x),b'(x)> : R |] ==> <lam x.b(x),lam x.b'(x)> : EQgen(R)",
+ "<one,one> : EQgen(R)",
+ "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
+\ <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
+ "<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
+\ <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
+ "<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
+ "<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
+\ <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
+ "<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
+ "[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); \
\ <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |] ==> \
\ <h.t,h'.t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"];
@@ -101,7 +101,8 @@
(* rews are rewrite rules that would cause looping in the simpifier *)
fun EQgen_tac simp_set rews i =
- SELECT_GOAL (TRY (safe_tac ccl_cs) THEN
- resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [ssubst_pair])) i THEN
- ALLGOALS (SIMP_TAC simp_set) THEN
- ALLGOALS EQgen_raw_tac) i;
+ SELECT_GOAL
+ (TRY (safe_tac ccl_cs) THEN
+ resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [ssubst_pair])) i THEN
+ ALLGOALS (simp_tac simp_set) THEN
+ ALLGOALS EQgen_raw_tac) i;
--- a/src/CCL/ex/List.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/ex/List.ML Mon Sep 20 17:02:11 1993 +0200
@@ -13,7 +13,7 @@
(****)
-val listBs = map (fn s=>prove_goalw List.thy list_defs s (fn _ => [SIMP_TAC term_ss 1]))
+val listBs = map (fn s=>prove_goalw List.thy list_defs s (fn _ => [simp_tac term_ss 1]))
["(f o g) = (%a.f(g(a)))",
"(f o g)(a) = f(g(a))",
"map(f,[]) = []",
@@ -27,20 +27,18 @@
"insert(f,a,[]) = a.[]",
"insert(f,a,x.xs) = if f`a`x then a.x.xs else x.insert(f,a,xs)"];
-val list_congs = ccl_mk_congs List.thy ["map","op @","filter","flat","insert","napply"];
-
-val list_ss = nat_ss addrews listBs addcongs list_congs;
+val list_ss = nat_ss addsimps listBs;
(****)
val [prem] = goal List.thy "n:Nat ==> map(f) ^ n ` [] = []";
br (prem RS Nat_ind) 1;
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val nmapBnil = result();
val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x.xs) = f^n`x.map(f)^n`xs";
br (prem RS Nat_ind) 1;
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val nmapBcons = result();
(***)
--- a/src/CCL/ex/Nat.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/ex/Nat.ML Mon Sep 20 17:02:11 1993 +0200
@@ -10,7 +10,7 @@
val nat_defs = [not_def,add_def,mult_def,sub_def,le_def,lt_def,ack_def,napply_def];
-val natBs = map (fn s=>prove_goalw Nat.thy nat_defs s (fn _ => [SIMP_TAC term_ss 1]))
+val natBs = map (fn s=>prove_goalw Nat.thy nat_defs s (fn _ => [simp_tac term_ss 1]))
["not(true) = false",
"not(false) = true",
"zero #+ n = n",
@@ -20,16 +20,13 @@
"f^zero`a = a",
"f^succ(n)`a = f(f^n`a)"];
-val nat_congs = ccl_mk_congs Nat.thy ["not","op #+","op #*","op #-","op ##",
- "op #<","op #<=","ackermann","napply"];
-
-val nat_ss = term_ss addrews natBs addcongs nat_congs;
+val nat_ss = term_ss addsimps natBs;
(*** Lemma for napply ***)
val [prem] = goal Nat.thy "n:Nat ==> f^n`f(a) = f^succ(n)`a";
br (prem RS Nat_ind) 1;
-by (ALLGOALS (ASM_SIMP_TAC (nat_ss addcongs [read_instantiate [("f","f")] arg_cong])));
+by (ALLGOALS (asm_simp_tac nat_ss));
val napply_f = result();
(****)
--- a/src/CCL/ex/Stream.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/ex/Stream.ML Mon Sep 20 17:02:11 1993 +0200
@@ -21,7 +21,7 @@
by (safe_tac type_cs);
be (XH_to_E ListsXH) 1;
by (EQgen_tac list_ss [] 1);
-by (SIMP_TAC list_ss 1);
+by (simp_tac list_ss 1);
by (fast_tac ccl_cs 1);
val map_comp = result();
@@ -87,7 +87,7 @@
goalw Stream.thy [iter1_def] "iter1(f,a) = a.iter1(f,f(a))";
br (letrecB RS trans) 1;
-by (SIMP_TAC term_ss 1);
+by (simp_tac term_ss 1);
val iter1B = result();
goalw Stream.thy [iter2_def] "iter2(f,a) = a . map(f,iter2(f,a))";
@@ -98,14 +98,17 @@
val [prem] =goal Stream.thy
"n:Nat ==> map(f) ^ n ` iter2(f,a) = f ^ n ` a . map(f) ^ n ` map(f,iter2(f,a))";
br (iter2B RS ssubst) 1;back();back();
-by (SIMP_TAC (list_ss addrews [prem RS nmapBcons]) 1);
+by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
val iter2Blemma = result();
goal Stream.thy "iter1(f,a) = iter2(f,a)";
by (eq_coinduct3_tac
- "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}" 1);
-by (fast_tac (type_cs addSIs [napplyBzero RS sym,napplyBzero RS sym RS arg_cong]) 1);
+ "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
+ 1);
+by (fast_tac (type_cs addSIs [napplyBzero RS sym,
+ napplyBzero RS sym RS arg_cong]) 1);
by (EQgen_tac list_ss [iter1B,iter2Blemma] 1);
+by (assume_tac 1); (*should EQgen_tac call asm_simp_tac?*)
by (rtac (napply_f RS ssubst) 1 THEN atac 1);
by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1);
by (fast_tac type_cs 1);
--- a/src/CCL/ex/list.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/ex/list.ML Mon Sep 20 17:02:11 1993 +0200
@@ -13,7 +13,7 @@
(****)
-val listBs = map (fn s=>prove_goalw List.thy list_defs s (fn _ => [SIMP_TAC term_ss 1]))
+val listBs = map (fn s=>prove_goalw List.thy list_defs s (fn _ => [simp_tac term_ss 1]))
["(f o g) = (%a.f(g(a)))",
"(f o g)(a) = f(g(a))",
"map(f,[]) = []",
@@ -27,20 +27,18 @@
"insert(f,a,[]) = a.[]",
"insert(f,a,x.xs) = if f`a`x then a.x.xs else x.insert(f,a,xs)"];
-val list_congs = ccl_mk_congs List.thy ["map","op @","filter","flat","insert","napply"];
-
-val list_ss = nat_ss addrews listBs addcongs list_congs;
+val list_ss = nat_ss addsimps listBs;
(****)
val [prem] = goal List.thy "n:Nat ==> map(f) ^ n ` [] = []";
br (prem RS Nat_ind) 1;
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val nmapBnil = result();
val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x.xs) = f^n`x.map(f)^n`xs";
br (prem RS Nat_ind) 1;
-by (ALLGOALS (ASM_SIMP_TAC list_ss));
+by (ALLGOALS (asm_simp_tac list_ss));
val nmapBcons = result();
(***)
--- a/src/CCL/ex/nat.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/ex/nat.ML Mon Sep 20 17:02:11 1993 +0200
@@ -10,7 +10,7 @@
val nat_defs = [not_def,add_def,mult_def,sub_def,le_def,lt_def,ack_def,napply_def];
-val natBs = map (fn s=>prove_goalw Nat.thy nat_defs s (fn _ => [SIMP_TAC term_ss 1]))
+val natBs = map (fn s=>prove_goalw Nat.thy nat_defs s (fn _ => [simp_tac term_ss 1]))
["not(true) = false",
"not(false) = true",
"zero #+ n = n",
@@ -20,16 +20,13 @@
"f^zero`a = a",
"f^succ(n)`a = f(f^n`a)"];
-val nat_congs = ccl_mk_congs Nat.thy ["not","op #+","op #*","op #-","op ##",
- "op #<","op #<=","ackermann","napply"];
-
-val nat_ss = term_ss addrews natBs addcongs nat_congs;
+val nat_ss = term_ss addsimps natBs;
(*** Lemma for napply ***)
val [prem] = goal Nat.thy "n:Nat ==> f^n`f(a) = f^succ(n)`a";
br (prem RS Nat_ind) 1;
-by (ALLGOALS (ASM_SIMP_TAC (nat_ss addcongs [read_instantiate [("f","f")] arg_cong])));
+by (ALLGOALS (asm_simp_tac nat_ss));
val napply_f = result();
(****)
--- a/src/CCL/ex/stream.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/ex/stream.ML Mon Sep 20 17:02:11 1993 +0200
@@ -21,7 +21,7 @@
by (safe_tac type_cs);
be (XH_to_E ListsXH) 1;
by (EQgen_tac list_ss [] 1);
-by (SIMP_TAC list_ss 1);
+by (simp_tac list_ss 1);
by (fast_tac ccl_cs 1);
val map_comp = result();
@@ -87,7 +87,7 @@
goalw Stream.thy [iter1_def] "iter1(f,a) = a.iter1(f,f(a))";
br (letrecB RS trans) 1;
-by (SIMP_TAC term_ss 1);
+by (simp_tac term_ss 1);
val iter1B = result();
goalw Stream.thy [iter2_def] "iter2(f,a) = a . map(f,iter2(f,a))";
@@ -98,14 +98,17 @@
val [prem] =goal Stream.thy
"n:Nat ==> map(f) ^ n ` iter2(f,a) = f ^ n ` a . map(f) ^ n ` map(f,iter2(f,a))";
br (iter2B RS ssubst) 1;back();back();
-by (SIMP_TAC (list_ss addrews [prem RS nmapBcons]) 1);
+by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
val iter2Blemma = result();
goal Stream.thy "iter1(f,a) = iter2(f,a)";
by (eq_coinduct3_tac
- "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}" 1);
-by (fast_tac (type_cs addSIs [napplyBzero RS sym,napplyBzero RS sym RS arg_cong]) 1);
+ "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
+ 1);
+by (fast_tac (type_cs addSIs [napplyBzero RS sym,
+ napplyBzero RS sym RS arg_cong]) 1);
by (EQgen_tac list_ss [iter1B,iter2Blemma] 1);
+by (assume_tac 1); (*should EQgen_tac call asm_simp_tac?*)
by (rtac (napply_f RS ssubst) 1 THEN atac 1);
by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1);
by (fast_tac type_cs 1);
--- a/src/CCL/fix.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/fix.ML Mon Sep 20 17:02:11 1993 +0200
@@ -8,20 +8,13 @@
open Fix;
-val prems = goalw Fix.thy [INCL_def]
- "[| !!x.P(x) <-> Q(x) |] ==> INCL(%x.P(x)) <-> INCL(%x.Q(x))";
-by (REPEAT (ares_tac ([refl] @ FOL_congs @ set_congs @ prems) 1));
-val INCL_cong = result();
-
-val fix_congs = [INCL_cong] @ ccl_mk_congs Fix.thy ["napply"];
-
(*** Fixed Point Induction ***)
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 (Nat_ind RS ballI) 1 THEN atac 1);
-by (ALLGOALS (SIMP_TAC term_ss));
+by (ALLGOALS (simp_tac term_ss));
by (REPEAT (ares_tac [base,step] 1));
val fix_ind = result();
@@ -48,7 +41,6 @@
by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1);
val inclE = result();
-val fix_ss = term_ss addcongs fix_congs;
(*** Lemmas for Inclusive Predicates ***)
@@ -76,7 +68,7 @@
val ball_INCL = result();
goal Fix.thy "INCL(%x.a(x) = b(x)::'a::prog)";
-by (SIMP_TAC (fix_ss addrews [eq_iff]) 1);
+by (simp_tac (term_ss addsimps [eq_iff]) 1);
by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
val eq_INCL = result();
@@ -89,9 +81,9 @@
val fix_idgenfp = result();
goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x";
-by (SIMP_TAC term_ss 1);
+by (simp_tac term_ss 1);
br (term_case RS allI) 1;
-by (ALLGOALS (SIMP_TAC term_ss));
+by (ALLGOALS (simp_tac term_ss));
val id_idgenfp = result();
(* All fixed points are lam-expressions *)
@@ -106,12 +98,12 @@
val prems = goalw Fix.thy [idgen_def]
"[| a = b; a ` t = u |] ==> b ` t = u";
-by (SIMP_TAC (term_ss addrews (prems RL [sym])) 1);
+by (simp_tac (term_ss addsimps (prems RL [sym])) 1);
val l_lemma= result();
val idgen_lemmas =
let fun mk_thm s = prove_goalw Fix.thy [idgen_def] s
- (fn [prem] => [rtac (prem RS l_lemma) 1,SIMP_TAC term_ss 1])
+ (fn [prem] => [rtac (prem RS l_lemma) 1,simp_tac term_ss 1])
in map mk_thm
[ "idgen(d) = d ==> d ` bot = bot",
"idgen(d) = d ==> d ` true = true",
@@ -141,7 +133,7 @@
\ POgen({p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t & b = d ` t)})";
by (REPEAT (step_tac term_cs 1));
by (term_case_tac "t" 1);
-by (ALLGOALS (SIMP_TAC (term_ss addrews (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
+by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
by (ALLGOALS (fast_tac set_cs));
val lemma1 = result();
@@ -157,7 +149,7 @@
\ {p.EX a b.p=<a,b> & b = d ` a} <= POgen({p.EX a b.p=<a,b> & b = d ` a})";
by (REPEAT (step_tac term_cs 1));
by (term_case_tac "a" 1);
-by (ALLGOALS (SIMP_TAC (term_ss addrews (POgenXH::([prem] RL idgen_lemmas)))));
+by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas)))));
by (ALLGOALS (fast_tac set_cs));
val lemma2 = result();
@@ -165,7 +157,7 @@
"idgen(d) = d ==> lam x.x [= d";
br (allI RS po_eta) 1;
br (lemma2 RSN(2,po_coinduct)) 1;
-by (SIMP_TAC term_ss 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();
@@ -196,7 +188,7 @@
brs prems 1;
br (applyB RS ssubst )1;
by (res_inst_tac [("t","xa")] term_case 1);
-by (ALLGOALS (SIMP_TAC term_ss));
+by (ALLGOALS (simp_tac term_ss));
by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems))));
val term_ind = result();
--- a/src/CCL/hered.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/hered.ML Mon Sep 20 17:02:11 1993 +0200
@@ -10,8 +10,6 @@
fun type_of_terms (Const("Trueprop",_) $ (Const("op =",(Type ("fun", [t,_])))$_$_)) = t;
-val cong_rls = ccl_mk_congs Hered.thy ["HTTgen"];
-
(*** Hereditary Termination ***)
goalw Hered.thy [HTTgen_def] "mono(%X.HTTgen(X))";
@@ -54,16 +52,16 @@
goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
br (HTTXH RS iff_trans) 1;
-by (SIMP_TAC term_ss 1);
+by (simp_tac term_ss 1);
by (safe_tac term_cs);
-by (ASM_SIMP_TAC term_ss 1);
+by (asm_simp_tac term_ss 1);
by (fast_tac term_cs 1);
val HTT_lam = result();
local
val raw_HTTrews = [HTT_bot,HTT_true,HTT_false,HTT_pair,HTT_lam];
fun mk_thm s = prove_goalw Hered.thy data_defs s (fn _ =>
- [SIMP_TAC (term_ss addrews raw_HTTrews) 1]);
+ [simp_tac (term_ss addsimps raw_HTTrews) 1]);
in
val HTT_rews = raw_HTTrews @
map mk_thm ["one : HTT",
@@ -115,22 +113,22 @@
(*** Formation Rules for Types ***)
goal Hered.thy "Unit <= HTT";
-by (SIMP_TAC (CCL_ss addrews ([subsetXH,UnitXH] @ HTT_rews)) 1);
+by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1);
val UnitF = result();
goal Hered.thy "Bool <= HTT";
-by (SIMP_TAC (CCL_ss addrews ([subsetXH,BoolXH] @ HTT_rews)) 1);
+by (simp_tac (CCL_ss addsimps ([subsetXH,BoolXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
val BoolF = result();
val prems = goal Hered.thy "[| A <= HTT; B <= HTT |] ==> A + B <= HTT";
-by (SIMP_TAC (CCL_ss addrews ([subsetXH,PlusXH] @ HTT_rews)) 1);
+by (simp_tac (CCL_ss addsimps ([subsetXH,PlusXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
val PlusF = result();
val prems = goal Hered.thy
"[| A <= HTT; !!x.x:A ==> B(x) <= HTT |] ==> SUM x:A.B(x) <= HTT";
-by (SIMP_TAC (CCL_ss addrews ([subsetXH,SgXH] @ HTT_rews)) 1);
+by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
val SigmaF = result();
@@ -139,7 +137,7 @@
(*Proof by induction - needs induction rule for type*)
goal Hered.thy "Nat <= HTT";
-by (SIMP_TAC (term_ss addrews [subsetXH]) 1);
+by (simp_tac (term_ss addsimps [subsetXH]) 1);
by (safe_tac set_cs);
be Nat_ind 1;
by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD]))));
@@ -186,7 +184,7 @@
bd (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 addrews HTT_rews)));
+by (ALLGOALS (simp_tac (term_ss addsimps HTT_rews)));
by (ALLGOALS (fast_tac ccl_cs));
val HTT_po_op = result();
--- a/src/CCL/set.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/set.ML Mon Sep 20 17:02:11 1993 +0200
@@ -22,18 +22,13 @@
by (resolve_tac (prems RL [mem_Collect_iff RS iffD1]) 1);
val CollectD = result();
+val CollectE = make_elim CollectD;
+
val [prem] = goal Set.thy "[| !!x. x:A <-> x:B |] ==> A = B";
by (rtac (set_extension RS iffD2) 1);
by (rtac (prem RS allI) 1);
val set_ext = result();
-val prems = goal Set.thy "[| !!x. P(x) <-> Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
-by (REPEAT (ares_tac [set_ext,iffI,CollectI] 1 ORELSE
- eresolve_tac ([CollectD] RL (prems RL [iffD1,iffD2])) 1));
-val Collect_cong = result();
-
-val CollectE = make_elim CollectD;
-
(*** Bounded quantifiers ***)
val prems = goalw Set.thy [Ball_def]
--- a/src/CCL/subset.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/subset.ML Mon Sep 20 17:02:11 1993 +0200
@@ -83,10 +83,6 @@
by (rtac minor 1);
val monoD = result();
-val [prem] = goalw Set.thy [mono_def] "(!!x.f(x) = g(x)) ==> mono(f) <-> mono(g)";
-by (REPEAT (resolve_tac (iff_refl::FOL_congs @ [prem RS subst]) 1));
-val mono_cong = result();
-
val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
by (rtac Un_least 1);
by (rtac (Un_upper1 RS (prem RS monoD)) 1);
@@ -121,9 +117,6 @@
"(a : {}) <-> False",
"(a : {x.P(x)}) <-> P(a)" ]);
-val set_congs =
- [Collect_cong, ball_cong, bex_cong, INT_cong, UN_cong, mono_cong] @
- mk_congs Set.thy ["Compl", "op Int", "op Un", "Union", "Inter",
- "op :", "op <=", "singleton"];
+val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong];
-val set_ss = FOL_ss addcongs set_congs addrews mem_rews;
+val set_ss = FOL_ss addcongs set_congs addsimps mem_rews;
--- a/src/CCL/term.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/term.ML Mon Sep 20 17:02:11 1993 +0200
@@ -19,15 +19,11 @@
val data_defs = simp_defs @ ind_defs @ [napply_def];
val genrec_defs = [letrec_def,letrec2_def,letrec3_def];
-val term_congs = ccl_mk_congs Term.thy
- ["inl","inr","succ","op .","split","if","when","ncase","nrec","lcase","lrec",
- "fst","snd","thd","let","letrec","letrec2","letrec3","napply"];
-
(*** Beta Rules, including strictness ***)
goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
by (res_inst_tac [("t","t")] term_case 1);
-by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
+by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
val letB = result() RS mp;
goalw Term.thy [let_def] "let x be bot in f(x) = bot";
@@ -36,11 +32,11 @@
goalw Term.thy [let_def] "let x be t in bot = bot";
brs ([caseBbot] RL [term_case]) 1;
-by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
+by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
val letBbbot = result();
goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)";
-by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
+by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
val applyB = result();
goalw Term.thy [apply_def] "bot ` a = bot";
@@ -57,10 +53,16 @@
resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1);
val letrecB = result();
-val rawBs = caseBs @ [applyB,applyBbot,letrecB];
+val rawBs = caseBs @ [applyB,applyBbot];
fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
- (fn _ => [SIMP_TAC (CCL_ss addrews rawBs addcongs term_congs) 1]);
+ (fn _ => [rtac (letrecB RS ssubst) 1,
+ simp_tac (CCL_ss addsimps rawBs) 1]);
+fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
+
+fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
+ (fn _ => [simp_tac (CCL_ss addsimps rawBs
+ setloop (rtac (letrecB RS ssubst))) 1]);
fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
val ifBtrue = mk_beta_rl "if true then t else u = t";
@@ -114,8 +116,7 @@
(*** Constructors are injective ***)
val term_injs = map (mk_inj_rl Term.thy
- [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons]
- (ccl_congs @ term_congs))
+ [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons])
["(inl(a) = inl(a')) <-> (a=a')",
"(inr(a) = inr(a')) <-> (a=a')",
"(succ(a) = succ(a')) <-> (a=a')",
@@ -130,7 +131,7 @@
local
fun mk_thm s = prove_goalw Term.thy data_defs s (fn _ =>
- [SIMP_TAC (ccl_ss addrews (ccl_porews)) 1]);
+ [simp_tac (ccl_ss addsimps (ccl_porews)) 1]);
in
val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
"inr(b) [= inr(b') <-> b [= b'",
@@ -141,6 +142,7 @@
(*** Rewriting and Proving ***)
val term_rews = termBs @ term_injs @ term_dstncts @ ccl_porews @ term_porews;
-val term_ss = ccl_ss addrews term_rews addcongs term_congs;
+val term_ss = ccl_ss addsimps term_rews;
-val term_cs = ccl_cs addSEs (term_dstncts RL [notE]) addSDs (XH_to_Ds term_injs);
+val term_cs = ccl_cs addSEs (term_dstncts RL [notE])
+ addSDs (XH_to_Ds term_injs);
--- a/src/CCL/terms.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/terms.ML Mon Sep 20 17:02:11 1993 +0200
@@ -19,15 +19,11 @@
val data_defs = simp_defs @ ind_defs @ [napply_def];
val genrec_defs = [letrec_def,letrec2_def,letrec3_def];
-val term_congs = ccl_mk_congs Term.thy
- ["inl","inr","succ","op .","split","if","when","ncase","nrec","lcase","lrec",
- "fst","snd","thd","let","letrec","letrec2","letrec3","napply"];
-
(*** Beta Rules, including strictness ***)
goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
by (res_inst_tac [("t","t")] term_case 1);
-by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
+by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
val letB = result() RS mp;
goalw Term.thy [let_def] "let x be bot in f(x) = bot";
@@ -36,11 +32,11 @@
goalw Term.thy [let_def] "let x be t in bot = bot";
brs ([caseBbot] RL [term_case]) 1;
-by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
+by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
val letBbbot = result();
goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)";
-by (ALLGOALS(SIMP_TAC(CCL_ss addrews [caseBtrue,caseBfalse,caseBpair,caseBlam])));
+by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
val applyB = result();
goalw Term.thy [apply_def] "bot ` a = bot";
@@ -57,10 +53,16 @@
resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1);
val letrecB = result();
-val rawBs = caseBs @ [applyB,applyBbot,letrecB];
+val rawBs = caseBs @ [applyB,applyBbot];
fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
- (fn _ => [SIMP_TAC (CCL_ss addrews rawBs addcongs term_congs) 1]);
+ (fn _ => [rtac (letrecB RS ssubst) 1,
+ simp_tac (CCL_ss addsimps rawBs) 1]);
+fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
+
+fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
+ (fn _ => [simp_tac (CCL_ss addsimps rawBs
+ setloop (rtac (letrecB RS ssubst))) 1]);
fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
val ifBtrue = mk_beta_rl "if true then t else u = t";
@@ -114,8 +116,7 @@
(*** Constructors are injective ***)
val term_injs = map (mk_inj_rl Term.thy
- [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons]
- (ccl_congs @ term_congs))
+ [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons])
["(inl(a) = inl(a')) <-> (a=a')",
"(inr(a) = inr(a')) <-> (a=a')",
"(succ(a) = succ(a')) <-> (a=a')",
@@ -130,7 +131,7 @@
local
fun mk_thm s = prove_goalw Term.thy data_defs s (fn _ =>
- [SIMP_TAC (ccl_ss addrews (ccl_porews)) 1]);
+ [simp_tac (ccl_ss addsimps (ccl_porews)) 1]);
in
val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
"inr(b) [= inr(b') <-> b [= b'",
@@ -141,6 +142,7 @@
(*** Rewriting and Proving ***)
val term_rews = termBs @ term_injs @ term_dstncts @ ccl_porews @ term_porews;
-val term_ss = ccl_ss addrews term_rews addcongs term_congs;
+val term_ss = ccl_ss addsimps term_rews;
-val term_cs = ccl_cs addSEs (term_dstncts RL [notE]) addSDs (XH_to_Ds term_injs);
+val term_cs = ccl_cs addSEs (term_dstncts RL [notE])
+ addSDs (XH_to_Ds term_injs);
--- a/src/CCL/type.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/type.ML Mon Sep 20 17:02:11 1993 +0200
@@ -65,7 +65,7 @@
fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s
(fn major::prems => [(resolve_tac ([major] RL top_crls) 1),
(REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
- (ALLGOALS (ASM_SIMP_TAC term_ss)),
+ (ALLGOALS (asm_simp_tac term_ss)),
(ALLGOALS (ares_tac (prems RL [lemma]) ORELSE'
eresolve_tac [bspec])),
(safe_tac (ccl_cs addSIs prems))]);
@@ -239,7 +239,7 @@
fun mk_prec_tac inds s = prove_goal Type.thy s
(fn major::prems => [resolve_tac ([major] RL inds) 1,
- ALLGOALS (SIMP_TAC term_ss THEN'
+ ALLGOALS (simp_tac term_ss THEN'
fast_tac (set_cs addSIs prems))]);
val prec_tac = mk_prec_tac inds;
--- a/src/CCL/wfd.ML Fri Sep 17 16:52:10 1993 +0200
+++ b/src/CCL/wfd.ML Mon Sep 20 17:02:11 1993 +0200
@@ -14,10 +14,6 @@
(***********)
-val wfd_congs = mk_congs Wfd.thy ["Wfd","wf","op **","wmap","ListPR"];
-
-(***********)
-
val [major,prem] = goalw Wfd.thy [Wfd_def]
"[| Wfd(R); \
\ !!x.[| ALL y. <y,x>: R --> P(y) |] ==> P(x) |] ==> \
@@ -149,17 +145,17 @@
val prems = goal Wfd.thy "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
br wmapI 1;
-by (SIMP_TAC (term_ss addrews prems) 1);
+by (simp_tac (term_ss addsimps prems) 1);
val wfstI = result();
val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
br wmapI 1;
-by (SIMP_TAC (term_ss addrews prems) 1);
+by (simp_tac (term_ss addsimps prems) 1);
val wsndI = result();
val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)";
br wmapI 1;
-by (SIMP_TAC (term_ss addrews prems) 1);
+by (simp_tac (term_ss addsimps prems) 1);
val wthdI = result();
(*** Ground well-founded relations ***)
@@ -175,7 +171,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 addcongs wfd_congs)));
+by (ALLGOALS (asm_simp_tac CCL_ss));
br Empty_wf 1;
val wf_wf = result();