--- a/src/ZF/Resid/Confluence.ML Wed May 08 16:10:32 1996 +0200
+++ b/src/ZF/Resid/Confluence.ML Wed May 08 17:43:23 1996 +0200
@@ -27,7 +27,7 @@
goalw Confluence.thy [confluence_def,strip_def]
"!!u.[|confluence(Spar_red1)|]==> strip";
by (resolve_tac [impI RS allI RS allI] 1);
-by (etac par_red_induct 1);
+by (etac Spar_red.induct 1);
by (fast_tac reduc_cs 1);
by (fast_tac (ZF_cs addIs [Spar_red.trans]) 1);
val strip_lemma_r = result();
@@ -36,7 +36,7 @@
goalw Confluence.thy [confluence_def,strip_def]
"!!u.strip==> confluence(Spar_red)";
by (resolve_tac [impI RS allI RS allI] 1);
-by (etac par_red_induct 1);
+by (etac Spar_red.induct 1);
by (fast_tac reduc_cs 1);
by (step_tac ZF_cs 1);
by (dres_inst_tac [("x1","z")] (spec RS mp) 1);
--- a/src/ZF/Resid/Conversion.ML Wed May 08 16:10:32 1996 +0200
+++ b/src/ZF/Resid/Conversion.ML Wed May 08 17:43:23 1996 +0200
@@ -9,13 +9,10 @@
val conv_ss = reduc_ss addsimps (Sconv1.intrs@[Sconv.one_step,Sconv.refl]);
-val conv1_induct = Sconv1.mutual_induct RS spec RS spec RSN (2,rev_mp);
-val conv_induct = Sconv.mutual_induct RS spec RS spec RSN (2,rev_mp);
-
goal Conversion.thy
"!!u.m<--->n ==> n<--->m";
-by (etac conv_induct 1);
-by (etac conv1_induct 1);
+by (etac Sconv.induct 1);
+by (etac Sconv1.induct 1);
by (resolve_tac [Sconv.trans] 4);
by (ALLGOALS(asm_simp_tac (conv_ss) ));
val conv_sym = result();
@@ -26,8 +23,8 @@
goal Conversion.thy
"!!u.m<--->n ==> EX p.(m --->p) & (n ---> p)";
-by (etac conv_induct 1);
-by (etac conv1_induct 1);
+by (etac Sconv.induct 1);
+by (etac Sconv1.induct 1);
by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1);
by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1);
by (fast_tac (reduc_cs addIs [red1D1,redD2]) 1);
--- a/src/ZF/Resid/Cube.ML Wed May 08 16:10:32 1996 +0200
+++ b/src/ZF/Resid/Cube.ML Wed May 08 17:43:23 1996 +0200
@@ -21,7 +21,7 @@
"!!u.v<==u ==> \
\ regular(u)-->(ALL w.w~v-->w~u--> \
\ w |> u = (w|>v) |> (u|>v))";
-by (etac sub_induct 1);
+by (etac Ssub.induct 1);
by (asm_simp_tac (prism_ss) 1);
by (asm_simp_tac (prism_ss ) 1);
by (asm_simp_tac (prism_ss ) 1);
--- a/src/ZF/Resid/Reduction.ML Wed May 08 16:10:32 1996 +0200
+++ b/src/ZF/Resid/Reduction.ML Wed May 08 17:43:23 1996 +0200
@@ -35,31 +35,26 @@
val reducL_ss = reduc_ss setloop (SELECT_GOAL (safe_tac reduc_cs));
-val red1_induct = Sred1.mutual_induct RS spec RS spec RSN (2,rev_mp);
-val red_induct = Sred.mutual_induct RS spec RS spec RSN (2,rev_mp);
-val par_red1_induct = Spar_red1.mutual_induct RS spec RS spec RSN (2,rev_mp);
-val par_red_induct = Spar_red.mutual_induct RS spec RS spec RSN (2,rev_mp);
-
(* ------------------------------------------------------------------------- *)
(* Lemmas for reduction *)
(* ------------------------------------------------------------------------- *)
goal Reduction.thy "!!u. m--->n ==> Fun(m) ---> Fun(n)";
-by (etac red_induct 1);
+by (etac Sred.induct 1);
by (resolve_tac [Sred.trans] 3);
by (ALLGOALS (asm_simp_tac reduc_ss ));
val red_Fun = result();
goal Reduction.thy
"!!u.[|n:lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)";
-by (etac red_induct 1);
+by (etac Sred.induct 1);
by (resolve_tac [Sred.trans] 3);
by (ALLGOALS (asm_simp_tac reduc_ss ));
val red_Apll = result();
goal Reduction.thy
"!!u.[|n:lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')";
-by (etac red_induct 1);
+by (etac Sred.induct 1);
by (resolve_tac [Sred.trans] 3);
by (ALLGOALS (asm_simp_tac reduc_ss ));
val red_Aplr = result();
@@ -89,19 +84,19 @@
val refl_par_red1 = result();
goal Reduction.thy "!!u.m-1->n ==> m=1=>n";
-by (etac red1_induct 1);
+by (etac Sred1.induct 1);
by (ALLGOALS (asm_simp_tac (reduc_ss addsimps [refl_par_red1]) ));
val red1_par_red1 = result();
goal Reduction.thy "!!u.m--->n ==> m===>n";
-by (etac red_induct 1);
+by (etac Sred.induct 1);
by (resolve_tac [Spar_red.trans] 3);
by (ALLGOALS (asm_simp_tac (reduc_ss addsimps [refl_par_red1,red1_par_red1]) ));
val red_par_red = result();
goal Reduction.thy "!!u.m===>n ==> m--->n";
-by (etac par_red_induct 1);
-by (etac par_red1_induct 1);
+by (etac Spar_red.induct 1);
+by (etac Spar_red1.induct 1);
by (resolve_tac [Sred.trans] 5);
by (ALLGOALS (asm_simp_tac (reduc_ss addsimps [red_Fun,red_beta,red_Apl]) ));
val par_red_red = result();
@@ -113,7 +108,7 @@
goal Reduction.thy
"!!u.m=1=>n ==> EX v. m|>v = n & m~v & regular(v)";
-by (etac par_red1_induct 1);
+by (etac Spar_red1.induct 1);
by (step_tac ZF_cs 1);
by (ALLGOALS (REPEAT o (resolve_tac [exI,conjI])));
by (TRYALL(resolve_tac [res_redex,res_App,res_Fun,res_Var]));
@@ -147,7 +142,7 @@
goal Reduction.thy
"!!u.u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (ALLGOALS (asm_full_simp_tac (reducL_ss addsimps [unmmark_subst_rec]) ));
by (dres_inst_tac [("psi", "Fun(?u) =1=> ?w")] asm_rl 1);
by (asm_full_simp_tac reducL_ss 1);
--- a/src/ZF/Resid/Residuals.ML Wed May 08 16:10:32 1996 +0200
+++ b/src/ZF/Resid/Residuals.ML Wed May 08 17:43:23 1996 +0200
@@ -11,31 +11,28 @@
(* Setting up rule lists *)
(* ------------------------------------------------------------------------- *)
-val residuals_induct = standard
- (Sres.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp));
-
val res_cs = union_cs
addIs (Sres.intrs@redexes.intrs@Sreg.intrs@
[subst_type]@nat_typechecks)
- addSEs (redexes.free_SEs@
- [Sres.mk_cases redexes.con_defs "residuals(Var(n),Var(n),v)",
- Sres.mk_cases redexes.con_defs "residuals(Fun(t),Fun(u),v)",
- Sres.mk_cases redexes.con_defs
- "residuals(App(b, u1, u2), App(0, v1, v2),v)",
- Sres.mk_cases redexes.con_defs
- "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)",
- Sres.mk_cases redexes.con_defs "residuals(Var(n),u,v)",
- Sres.mk_cases redexes.con_defs "residuals(Fun(t),u,v)",
- Sres.mk_cases redexes.con_defs "residuals(App(b, u1, u2), w,v)",
- Sres.mk_cases redexes.con_defs "residuals(u,Var(n),v)",
- Sres.mk_cases redexes.con_defs "residuals(u,Fun(t),v)",
- Sres.mk_cases redexes.con_defs "residuals(w,App(b, u1, u2),v)",
- Ssub.mk_cases redexes.con_defs "Var(n) <== u",
- Ssub.mk_cases redexes.con_defs "Fun(n) <== u",
- Ssub.mk_cases redexes.con_defs "u <== Fun(n)",
- Ssub.mk_cases redexes.con_defs "App(1,Fun(t),a) <== u",
- Ssub.mk_cases redexes.con_defs "App(0,t,a) <== u",
- redexes.mk_cases redexes.con_defs "Fun(t):redexes"]);
+ addSEs (redexes.free_SEs @
+ (map (Sres.mk_cases redexes.con_defs)
+ ["residuals(Var(n),Var(n),v)",
+ "residuals(Fun(t),Fun(u),v)",
+ "residuals(App(b, u1, u2), App(0, v1, v2),v)",
+ "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)",
+ "residuals(Var(n),u,v)",
+ "residuals(Fun(t),u,v)",
+ "residuals(App(b, u1, u2), w,v)",
+ "residuals(u,Var(n),v)",
+ "residuals(u,Fun(t),v)",
+ "residuals(w,App(b, u1, u2),v)"]) @
+ (map (Ssub.mk_cases redexes.con_defs)
+ ["Var(n) <== u",
+ "Fun(n) <== u",
+ "u <== Fun(n)",
+ "App(1,Fun(t),a) <== u",
+ "App(0,t,a) <== u"]) @
+ [redexes.mk_cases redexes.con_defs "Fun(t):redexes"]);
val res_ss = subst_ss addsimps (Sres.intrs);
val resD1 =Sres.dom_subset RS subsetD RS SigmaD1;
@@ -49,14 +46,14 @@
goal Residuals.thy
"!!u.residuals(u,v,w) ==> ALL w1.residuals(u,v,w1) --> w1 = w";
-by (etac residuals_induct 1);
+by (etac Sres.induct 1);
by (ALLGOALS (fast_tac res_cs ));
val residuals_function = result();
val res_is_func = residuals_function RS spec RS mp;
goal Residuals.thy
"!!u.u~v ==> regular(v) --> (EX w.residuals(u,v,w))";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (ALLGOALS (fast_tac res_cs));
val residuals_intro = result();
@@ -102,7 +99,7 @@
goal Residuals.thy
"!!n.[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (ALLGOALS (asm_full_simp_tac
(res_ss addsimps [res_Var,res_Fun,res_App,res_redex]
setloop (SELECT_GOAL (safe_tac res_cs)))));
@@ -125,20 +122,20 @@
goal Residuals.thy
"!!u.u<==v ==> u~v";
-by (etac sub_induct 1);
+by (etac Ssub.induct 1);
by (ALLGOALS (asm_simp_tac res1_ss));
val sub_comp = result();
goal Residuals.thy
"!!u.u<==v ==> regular(v) --> regular(u)";
-by (etac sub_induct 1);
+by (etac Ssub.induct 1);
by (ALLGOALS (asm_simp_tac res1L_ss));
val sub_preserve_reg = result();
goal Residuals.thy
"!!u.[|u~v; k:nat|]==> regular(v)--> (ALL n:nat. \
\ lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (step_tac res_cs 1);
by (ALLGOALS (asm_full_simp_tac ((addsplit res1_ss) addsimps [lift_subst])));
by (dres_inst_tac [("psi", "ALL x:nat.Fun(?u(x)) |> ?v(x) = ?w(x)")] asm_rl 1);
@@ -149,7 +146,7 @@
"!!u.u1~u2 ==> ALL v1 v2.v1~v2 --> regular(v2) --> regular(u2) -->\
\ (ALL n:nat.subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
\ subst_rec(v1 |> v2, u1 |> u2,n))";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (step_tac (res_cs) 1);
by (ALLGOALS
(asm_full_simp_tac ((addsplit res1_ss) addsimps ([residuals_lift_rec]))));
@@ -170,7 +167,7 @@
goal Residuals.thy
"!!u.u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (ALLGOALS (asm_simp_tac (res1L_ss )));
by (dresolve_tac [spec RS mp RS mp RS mp] 1
THEN resolve_tac Scomp.intrs 1 THEN resolve_tac Scomp.intrs 2
@@ -182,7 +179,7 @@
goal Residuals.thy
"!!u.u~v ==> regular(u) --> regular(v) --> regular(u|>v)";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (safe_tac res_cs);
by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl));
by (ALLGOALS (asm_full_simp_tac res1L_ss));
@@ -194,13 +191,13 @@
goal Residuals.thy
"!!u.u~v ==> v ~ (u un v)";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (ALLGOALS (asm_full_simp_tac res_ss));
val union_preserve_comp = result();
goal Residuals.thy
"!!u.u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (safe_tac res_cs);
by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3);
by (ALLGOALS (asm_full_simp_tac (res1L_ss addsimps
--- a/src/ZF/Resid/SubUnion.ML Wed May 08 16:10:32 1996 +0200
+++ b/src/ZF/Resid/SubUnion.ML Wed May 08 17:43:23 1996 +0200
@@ -12,9 +12,6 @@
(* Specialisation of comp-rules *)
(* ------------------------------------------------------------------------- *)
-val comp_induct = standard
- (Scomp.mutual_induct RS spec RS spec RSN (2,rev_mp));
-
val compD1 =Scomp.dom_subset RS subsetD RS SigmaD1;
val compD2 =Scomp.dom_subset RS subsetD RS SigmaD2;
@@ -76,7 +73,7 @@
goal SubUnion.thy
"!!u.u ~ v ==> v ~ u";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (ALLGOALS(fast_tac union_cs));
val comp_sym = result();
@@ -88,7 +85,7 @@
goal SubUnion.thy
"!!u.u ~ v ==> ALL w.v ~ w-->u ~ w";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (ALLGOALS(fast_tac union_cs));
val comp_trans1 = result();
@@ -98,26 +95,23 @@
(* union proofs *)
(* ------------------------------------------------------------------------- *)
-val sub_induct = standard
- (Ssub.mutual_induct RS spec RS spec RSN (2,rev_mp));
-
goal SubUnion.thy
"!!u.u ~ v ==> u <== (u un v)";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (etac boolE 3);
by (ALLGOALS(asm_full_simp_tac union_ss));
val union_l = result();
goal SubUnion.thy
"!!u.u ~ v ==> v <== (u un v)";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (eres_inst_tac [("c","b2")] boolE 3);
by (ALLGOALS(asm_full_simp_tac union_ss));
val union_r = result();
goal SubUnion.thy
"!!u.u ~ v ==> u un v = v un u";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (ALLGOALS(asm_simp_tac (union_ss addsimps [or_commute])));
val union_sym = result();
@@ -127,7 +121,7 @@
goal SubUnion.thy
"!!u.u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (ALLGOALS(asm_full_simp_tac
(union_ss setloop(SELECT_GOAL (safe_tac union_cs)))));
by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
--- a/src/ZF/Resid/Substitution.ML Wed May 08 16:10:32 1996 +0200
+++ b/src/ZF/Resid/Substitution.ML Wed May 08 17:43:23 1996 +0200
@@ -267,14 +267,14 @@
goal Substitution.thy
"!!n.[|n:nat; u ~ v|]==> ALL m:nat.lift_rec(u,m) ~ lift_rec(v,m)";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (ALLGOALS(asm_simp_tac (subst_ss addsimps [comp_refl])));
val lift_rec_preserve_comp = result();
goal Substitution.thy
"!!n.u2 ~ v2 ==> ALL m:nat.ALL u1:redexes.ALL v1:redexes.\
\ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)";
-by (etac comp_induct 1);
+by (etac Scomp.induct 1);
by (ALLGOALS(asm_full_simp_tac ((addsplit subst_ss) addsimps
([lift_rec_preserve_comp,comp_refl]))));
val subst_rec_preserve_comp = result();
--- a/src/ZF/ex/Comb.ML Wed May 08 16:10:32 1996 +0200
+++ b/src/ZF/ex/Comb.ML Wed May 08 17:43:23 1996 +0200
@@ -23,9 +23,6 @@
(*** Results about Contraction ***)
-bind_thm ("contract_induct",
- (contract.mutual_induct RS spec RS spec RSN (2,rev_mp)));
-
(*For type checking: replaces a-1->b by a,b:comb *)
val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2;
val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1;
@@ -119,9 +116,6 @@
(*** Results about Parallel Contraction ***)
-bind_thm ("parcontract_induct",
- (parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp)));
-
(*For type checking: replaces a=1=>b by a,b:comb *)
val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2;
val parcontract_combD1 = parcontract.dom_subset RS subsetD RS SigmaD1;
@@ -163,7 +157,7 @@
(*Church-Rosser property for parallel contraction*)
goalw Comb.thy [diamond_def] "diamond(parcontract)";
by (rtac (impI RS allI RS allI) 1);
-by (etac parcontract_induct 1);
+by (etac parcontract.induct 1);
by (ALLGOALS
(fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
qed "diamond_parcontract";
@@ -192,7 +186,7 @@
(*** Equivalence of p--->q and p===>q ***)
goal Comb.thy "!!p q. p-1->q ==> p=1=>q";
-by (etac contract_induct 1);
+by (etac contract.induct 1);
by (ALLGOALS (fast_tac (parcontract_cs)));
qed "contract_imp_parcontract";
@@ -207,7 +201,7 @@
goal Comb.thy "!!p q. p=1=>q ==> p--->q";
-by (etac parcontract_induct 1);
+by (etac parcontract.induct 1);
by (fast_tac (contract_cs addIs reduction_rls) 1);
by (fast_tac (contract_cs addIs reduction_rls) 1);
by (fast_tac (contract_cs addIs reduction_rls) 1);
--- a/src/ZF/ex/ListN.ML Wed May 08 16:10:32 1996 +0200
+++ b/src/ZF/ex/ListN.ML Wed May 08 17:43:23 1996 +0200
@@ -11,9 +11,6 @@
open ListN;
-val listn_induct = standard
- (listn.mutual_induct RS spec RS spec RSN (2,rev_mp));
-
goal ListN.thy "!!l. l:list(A) ==> <length(l),l> : listn(A)";
by (etac list.induct 1);
by (ALLGOALS (asm_simp_tac list_ss));
@@ -22,7 +19,7 @@
goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
by (rtac iffI 1);
-by (etac listn_induct 1);
+by (etac listn.induct 1);
by (safe_tac (ZF_cs addSIs (list_typechecks @
[length_Nil, length_Cons, list_into_listn])));
qed "listn_iff";
@@ -41,7 +38,7 @@
goal ListN.thy
"!!n l. [| <n,l> : listn(A); <n',l'> : listn(A) |] ==> \
\ <n#+n', l@l'> : listn(A)";
-by (etac listn_induct 1);
+by (etac listn.induct 1);
by (ALLGOALS (asm_simp_tac (list_ss addsimps listn.intrs)));
qed "listn_append";
--- a/src/ZF/ex/Rmap.ML Wed May 08 16:10:32 1996 +0200
+++ b/src/ZF/ex/Rmap.ML Wed May 08 17:43:23 1996 +0200
@@ -15,9 +15,6 @@
basic_monos) 1));
qed "rmap_mono";
-bind_thm ("rmap_induct",
- (rmap.mutual_induct RS spec RS spec RSN (2,rev_mp)));
-
val Nil_rmap_case = rmap.mk_cases list.con_defs "<Nil,zs> : rmap(r)"
and Cons_rmap_case = rmap.mk_cases list.con_defs "<Cons(x,xs),zs> : rmap(r)";
@@ -39,7 +36,7 @@
goalw Rmap.thy [function_def] "!!r. function(r) ==> function(rmap(r))";
by (rtac (impI RS allI RS allI) 1);
-by (etac rmap_induct 1);
+by (etac rmap.induct 1);
by (ALLGOALS (fast_tac rmap_cs));
qed "rmap_functional";