# HG changeset patch # User paulson # Date 831570203 -7200 # Node ID 38776e927da8d78235b88be0da57418fada31b7e # Parent 2ad693c6cb134ce61dc393c9f685da3acde1e90d Updated for new form of induction rules diff -r 2ad693c6cb13 -r 38776e927da8 src/ZF/Resid/Confluence.ML --- 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); diff -r 2ad693c6cb13 -r 38776e927da8 src/ZF/Resid/Conversion.ML --- 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); diff -r 2ad693c6cb13 -r 38776e927da8 src/ZF/Resid/Cube.ML --- 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); diff -r 2ad693c6cb13 -r 38776e927da8 src/ZF/Resid/Reduction.ML --- 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); diff -r 2ad693c6cb13 -r 38776e927da8 src/ZF/Resid/Residuals.ML --- 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 diff -r 2ad693c6cb13 -r 38776e927da8 src/ZF/Resid/SubUnion.ML --- 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); diff -r 2ad693c6cb13 -r 38776e927da8 src/ZF/Resid/Substitution.ML --- 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(); diff -r 2ad693c6cb13 -r 38776e927da8 src/ZF/ex/Comb.ML --- 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); diff -r 2ad693c6cb13 -r 38776e927da8 src/ZF/ex/ListN.ML --- 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) ==> : listn(A)"; by (etac list.induct 1); by (ALLGOALS (asm_simp_tac list_ss)); @@ -22,7 +19,7 @@ goal ListN.thy " : 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. [| : listn(A); : listn(A) |] ==> \ \ : 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"; diff -r 2ad693c6cb13 -r 38776e927da8 src/ZF/ex/Rmap.ML --- 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 " : rmap(r)" and Cons_rmap_case = rmap.mk_cases list.con_defs " : 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";