--- a/src/HOL/IMP/Hoare.ML Tue May 07 18:17:52 1996 +0200
+++ b/src/HOL/IMP/Hoare.ML Tue May 07 18:19:13 1996 +0200
@@ -9,8 +9,8 @@
open Hoare;
-goalw Hoare.thy [hoare_valid_def] "!P c Q. |- {P}c{Q} --> |= {P}c{Q}";
-by (rtac hoare.mutual_induct 1);
+goalw Hoare.thy [hoare_valid_def] "!!P c Q. |- {P}c{Q} ==> |= {P}c{Q}";
+by (etac hoare.induct 1);
by(ALLGOALS Asm_simp_tac);
by(fast_tac rel_cs 1);
by(fast_tac HOL_cs 1);
@@ -23,7 +23,7 @@
by(eres_inst_tac [("x","a")] allE 1);
by (safe_tac comp_cs);
by(ALLGOALS Asm_full_simp_tac);
-qed_spec_mp "hoare_sound";
+qed "hoare_sound";
goalw Hoare.thy [swp_def] "swp SKIP Q = Q";
by(Simp_tac 1);
--- a/src/HOL/IMP/Natural.ML Tue May 07 18:17:52 1996 +0200
+++ b/src/HOL/IMP/Natural.ML Tue May 07 18:19:13 1996 +0200
@@ -16,8 +16,8 @@
addEs [evalc_WHILE_case];
(* evaluation of com is deterministic *)
-goal Natural.thy "!c s t. <c,s> -c-> t --> (!u. <c,s> -c-> u --> u=t)";
-by (rtac evalc.mutual_induct 1);
+goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
+by (etac evalc.induct 1);
by (eres_inst_tac [("V", "<?c,s2> -c-> s1")] thin_rl 7);
by (ALLGOALS (deepen_tac evalc_cs 4));
qed_spec_mp "com_det";
--- a/src/HOL/IMP/Transition.ML Tue May 07 18:17:52 1996 +0200
+++ b/src/HOL/IMP/Transition.ML Tue May 07 18:19:13 1996 +0200
@@ -42,8 +42,8 @@
qed_spec_mp "lemma1";
-goal Transition.thy "!c s s1. <c,s> -c-> s1 --> (c,s) -*-> (SKIP,s1)";
-br evalc.mutual_induct 1;
+goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
+be evalc.induct 1;
(* SKIP *)
br rtrancl_refl 1;
@@ -63,7 +63,7 @@
by (fast_tac (evalc1_cs addDs [rtrancl_imp_UN_rel_pow]
addIs [rtrancl_into_rtrancl2,lemma1]) 1);
-qed_spec_mp "evalc_impl_evalc1";
+qed "evalc_impl_evalc1";
goal Transition.thy
@@ -136,8 +136,8 @@
qed_spec_mp "my_lemma1";
-goal Transition.thy "!c s s1. <c,s> -c-> s1 --> (c,s) -*-> (SKIP,s1)";
-br evalc.mutual_induct 1;
+goal Transition.thy "!!c s s1. <c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
+be evalc.induct 1;
(* SKIP *)
br rtrancl_refl 1;
@@ -156,7 +156,7 @@
by (fast_tac (evalc1_cs addSIs [r_into_rtrancl]) 1);
by (fast_tac (evalc1_cs addIs [rtrancl_into_rtrancl2,my_lemma1]) 1);
-qed_spec_mp "evalc_impl_evalc1";
+qed "evalc_impl_evalc1";
(* The opposite direction is based on a Coq proof done by Ranan Fraer and
Yves Bertot. The following sketch is from an email by Ranan Fraer.
@@ -193,18 +193,12 @@
*)
-goal Transition.thy "!cs c' s'. (cs -1-> (c',s')) --> (!c s. cs = (c,s) \
-\ --> (!t. <c',s'> -c-> t --> <c,s> -c-> t))";
-br evalc1.mutual_induct 1;
+goal Transition.thy
+ "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
+be evalc1.induct 1;
by(ALLGOALS(fast_tac (evalc1_cs addEs (evalc_elim_cases@evalc1_elim_cases)
addss !simpset)));
-val lemma = result();
-
-val prems = goal Transition.thy
- "[| ((c,s) -1-> (c',s')); <c',s'> -c-> t |] ==> <c,s> -c-> t";
-by(cut_facts_tac (lemma::prems) 1);
-by(fast_tac HOL_cs 1);
-qed "FB_lemma3";
+qed_spec_mp "FB_lemma3";
val [major] = goal Transition.thy
"(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
--- a/src/HOL/Lambda/Eta.ML Tue May 07 18:17:52 1996 +0200
+++ b/src/HOL/Lambda/Eta.ML Tue May 07 18:19:13 1996 +0200
@@ -87,7 +87,7 @@
Addsimps [free_subst];
goal Eta.thy "!!s. s -e> t ==> !i. free t i = free s i";
-by (etac (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1);
+by (etac eta.induct 1);
by(ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong])));
qed_spec_mp "free_eta";
@@ -107,7 +107,7 @@
qed "subst_decr";
goal Eta.thy "!!s. s -e> t ==> !u i. s[u/i] -e> t[u/i]";
-by (etac (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1);
+by (etac eta.induct 1);
by(ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def])));
by(asm_simp_tac (!simpset addsimps [subst_decr]) 1);
qed_spec_mp "eta_subst";
@@ -120,7 +120,8 @@
(*** Confluence of eta ***)
goalw Eta.thy [square_def,id_def] "square eta eta (eta^=) (eta^=)";
-by (rtac eta.mutual_induct 1);
+by (rtac (impI RS allI RS allI) 1);
+by (etac eta.induct 1);
by(ALLGOALS(fast_tac (eta_cs addSEs [eta_decr,not_free_eta] addss !simpset)));
val lemma = result();
@@ -152,13 +153,13 @@
(*** Commutation of beta and eta ***)
-goal Eta.thy "!s t. s -> t --> (!i. free t i --> free s i)";
-by (rtac beta.mutual_induct 1);
+goal Eta.thy "!!s t. s -> t ==> (!i. free t i --> free s i)";
+by (etac beta.induct 1);
by(ALLGOALS(Asm_full_simp_tac));
qed_spec_mp "free_beta";
-goalw Eta.thy [decr_def] "!s t. s -> t --> (!i. decr s i -> decr t i)";
-by (rtac beta.mutual_induct 1);
+goalw Eta.thy [decr_def] "!!s t. s -> t ==> (!i. decr s i -> decr t i)";
+by (etac beta.induct 1);
by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym])));
qed_spec_mp "beta_decr";
@@ -185,8 +186,8 @@
qed "decr_not_free";
Addsimps [decr_not_free];
-goal Eta.thy "!s t. s -e> t --> (!i. lift s i -e> lift t i)";
-by (rtac eta.mutual_induct 1);
+goal Eta.thy "!!s t. s -e> t ==> (!i. lift s i -e> lift t i)";
+by (etac eta.induct 1);
by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def])));
by(asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1);
qed_spec_mp "eta_lift";
@@ -201,7 +202,8 @@
qed_spec_mp "rtrancl_eta_subst";
goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)";
-by (rtac beta.mutual_induct 1);
+by (rtac (impI RS allI RS allI) 1);
+by (etac beta.induct 1);
by(strip_tac 1);
by (eresolve_tac eta_cases 1);
by (eresolve_tac eta_cases 1);
--- a/src/HOL/Lambda/ParRed.ML Tue May 07 18:17:52 1996 +0200
+++ b/src/HOL/Lambda/ParRed.ML Tue May 07 18:19:13 1996 +0200
@@ -33,17 +33,19 @@
goal ParRed.thy "beta <= par_beta";
by (rtac subsetI 1);
by (split_all_tac 1);
-by (etac (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1);
+by (etac beta.induct 1);
by (ALLGOALS(fast_tac (parred_cs addSIs [par_beta_refl])));
qed "beta_subset_par_beta";
goal ParRed.thy "par_beta <= beta^*";
by (rtac subsetI 1);
by (split_all_tac 1);
-by (etac (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1);
-by (ALLGOALS(fast_tac (parred_cs addIs
- [rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl,
- rtrancl_into_rtrancl] addEs [rtrancl_trans])));
+by (etac par_beta.induct 1);
+by (ALLGOALS
+ (fast_tac (parred_cs addIs
+ [rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl,
+ rtrancl_into_rtrancl]
+ addEs [rtrancl_trans])));
qed "par_beta_subset_beta";
(*** => ***)
@@ -69,7 +71,8 @@
(*** Confluence (directly) ***)
goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
-by (rtac par_beta.mutual_induct 1);
+by (rtac (impI RS allI RS allI) 1);
+by (etac par_beta.induct 1);
by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst])));
qed "diamond_par_beta";
--- a/src/HOL/ex/Comb.ML Tue May 07 18:17:52 1996 +0200
+++ b/src/HOL/ex/Comb.ML Tue May 07 18:19:13 1996 +0200
@@ -103,9 +103,6 @@
(*** Results about Parallel Contraction ***)
-bind_thm ("parcontract_induct",
- (parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp)));
-
(*Derive a case for each combinator constructor*)
val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z";
val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
@@ -136,7 +133,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";
@@ -146,6 +143,7 @@
goal Comb.thy "contract <= parcontract";
by (rtac subsetI 1);
+by (split_all_tac 1);
by (etac contract.induct 1);
by (ALLGOALS (fast_tac (parcontract_cs)));
qed "contract_subset_parcontract";
@@ -164,6 +162,7 @@
goal Comb.thy "parcontract <= contract^*";
by (rtac subsetI 1);
+by (split_all_tac 1);
by (etac parcontract.induct 1);
by (ALLGOALS (deepen_tac reduce_cs 0));
qed "parcontract_subset_reduce";
--- a/src/HOL/ex/Perm.ML Tue May 07 18:17:52 1996 +0200
+++ b/src/HOL/ex/Perm.ML Tue May 07 18:19:13 1996 +0200
@@ -18,30 +18,28 @@
by (REPEAT (ares_tac perm.intrs 1));
qed "perm_refl";
-val perm_induct = standard (perm.mutual_induct RS spec RS spec RSN (2,rev_mp));
-
(** Some examples of rule induction on permutations **)
(*The form of the premise lets the induction bind xs and ys.*)
goal Perm.thy "!!xs. xs <~~> ys ==> xs=[] --> ys=[]";
-by (etac perm_induct 1);
+by (etac perm.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "perm_Nil_lemma";
(*A more general version is actually easier to understand!*)
goal Perm.thy "!!xs. xs <~~> ys ==> length(xs) = length(ys)";
-by (etac perm_induct 1);
+by (etac perm.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "perm_length";
goal Perm.thy "!!xs. xs <~~> ys ==> ys <~~> xs";
-by (etac perm_induct 1);
+by (etac perm.induct 1);
by (REPEAT (ares_tac perm.intrs 1));
qed "perm_sym";
goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
-by (etac perm_induct 1);
+by (etac perm.induct 1);
by (fast_tac HOL_cs 4);
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
val perm_mem_lemma = result();