--- a/src/HOL/Induct/Acc.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Induct/Acc.thy Thu Sep 07 21:10:11 2000 +0200
@@ -18,7 +18,7 @@
inductive "acc r"
intros
- accI [rulify_prems]:
+ accI [rulified]:
"\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
syntax
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Thu Sep 07 21:10:11 2000 +0200
@@ -154,7 +154,7 @@
have "?B (Suc m) = ?t Un ?B m"; by (simp add: Sigma_Suc);
also; have "... : ?T";
- proof (rule tiling_Un [rulify]);
+ proof (rule tiling_Un [rulified]);
show "?t : ?T"; by (rule dominoes_tile_row);
from hyp; show "?B m : ?T"; .;
show "?t Int ?B m = {}"; by blast;
--- a/src/HOL/Isar_examples/Puzzle.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy Thu Sep 07 21:10:11 2000 +0200
@@ -118,7 +118,7 @@
proof;
assume "n < f n";
hence "Suc n <= f n"; by (rule Suc_leI);
- hence "f (Suc n) <= f (f n)"; by (rule mono [rulify]);
+ hence "f (Suc n) <= f (f n)"; by (rule mono [rulified]);
also; have "... < f (Suc n)"; by (rule f_ax);
finally; have "... < ..."; .; thus False; ..;
qed;
--- a/src/HOL/Lambda/Eta.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/Eta.thy Thu Sep 07 21:10:11 2000 +0200
@@ -45,7 +45,7 @@
subsection "Properties of eta, subst and free"
-lemma subst_not_free [rulify, simp]:
+lemma subst_not_free [rulified, simp]:
"\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]"
apply (induct_tac s)
apply (simp_all add: subst_Var)
@@ -74,7 +74,7 @@
apply simp_all
done
-lemma free_eta [rulify]:
+lemma free_eta [rulified]:
"s -e> t ==> \<forall>i. free t i = free s i"
apply (erule eta.induct)
apply (simp_all cong: conj_cong)
@@ -85,7 +85,7 @@
apply (simp add: free_eta)
done
-lemma eta_subst [rulify, simp]:
+lemma eta_subst [rulified, simp]:
"s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]"
apply (erule eta.induct)
apply (simp_all add: subst_subst [symmetric])
@@ -136,13 +136,13 @@
subsection "Commutation of beta and eta"
-lemma free_beta [rulify]:
+lemma free_beta [rulified]:
"s -> t ==> \<forall>i. free t i --> free s i"
apply (erule beta.induct)
apply simp_all
done
-lemma beta_subst [rulify, intro]:
+lemma beta_subst [rulified, intro]:
"s -> t ==> \<forall>u i. s[u/i] -> t[u/i]"
apply (erule beta.induct)
apply (simp_all add: subst_subst [symmetric])
@@ -153,13 +153,13 @@
apply (auto elim!: linorder_neqE simp: subst_Var)
done
-lemma eta_lift [rulify, simp]:
+lemma eta_lift [rulified, simp]:
"s -e> t ==> \<forall>i. lift s i -e> lift t i"
apply (erule eta.induct)
apply simp_all
done
-lemma rtrancl_eta_subst [rulify]:
+lemma rtrancl_eta_subst [rulified]:
"\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
apply (induct_tac u)
apply (simp_all add: subst_Var)
@@ -190,7 +190,7 @@
text {* @{term "Abs (lift s 0 $ Var 0) -e> s"} *}
-lemma not_free_iff_lifted [rulify]:
+lemma not_free_iff_lifted [rulified]:
"\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
apply (induct_tac s)
apply simp
--- a/src/HOL/Lambda/InductTermi.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/InductTermi.thy Thu Sep 07 21:10:11 2000 +0200
@@ -26,7 +26,7 @@
subsection {* Every term in IT terminates *}
-lemma double_induction_lemma [rulify]:
+lemma double_induction_lemma [rulified]:
"s : termi beta ==> \<forall>t. t : termi beta -->
(\<forall>r ss. t = r[s/0] $$ ss --> Abs r $ s $$ ss : termi beta)"
apply (erule acc_induct)
--- a/src/HOL/Lambda/Lambda.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/Lambda.thy Thu Sep 07 21:10:11 2000 +0200
@@ -120,7 +120,7 @@
apply (simp add: subst_Var)
done
-lemma lift_lift [rulify]:
+lemma lift_lift [rulified]:
"\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
apply (induct_tac t)
apply auto
@@ -144,7 +144,7 @@
apply simp_all
done
-lemma subst_subst [rulify]:
+lemma subst_subst [rulified]:
"\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
apply (induct_tac t)
apply (simp_all
@@ -183,19 +183,19 @@
text {* Not used in Church-Rosser proof, but in Strong
Normalization. \medskip *}
-theorem subst_preserves_beta [rulify, simp]:
+theorem subst_preserves_beta [rulified, simp]:
"r -> s ==> \<forall>t i. r[t/i] -> s[t/i]"
apply (erule beta.induct)
apply (simp_all add: subst_subst [symmetric])
done
-theorem lift_preserves_beta [rulify, simp]:
+theorem lift_preserves_beta [rulified, simp]:
"r -> s ==> \<forall>i. lift r i -> lift s i"
apply (erule beta.induct)
apply auto
done
-theorem subst_preserves_beta2 [rulify, simp]:
+theorem subst_preserves_beta2 [rulified, simp]:
"\<forall>r s i. r -> s --> t[r/i] ->> t[s/i]"
apply (induct_tac t)
apply (simp add: subst_Var r_into_rtrancl)
--- a/src/HOL/Lambda/ListApplication.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.thy Thu Sep 07 21:10:11 2000 +0200
@@ -18,13 +18,13 @@
apply auto
done
-lemma Var_eq_apps_conv [rulify, iff]:
+lemma Var_eq_apps_conv [rulified, iff]:
"\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
apply (induct_tac ss)
apply auto
done
-lemma Var_apps_eq_Var_apps_conv [rulify, iff]:
+lemma Var_apps_eq_Var_apps_conv [rulified, iff]:
"\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
apply (induct_tac rs rule: rev_induct)
apply simp
@@ -69,7 +69,7 @@
apply auto
done
-lemma Var_apps_neq_Abs_apps [rulify, iff]:
+lemma Var_apps_neq_Abs_apps [rulified, iff]:
"\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
apply (induct_tac ss rule: rev_induct)
apply simp
@@ -103,7 +103,7 @@
text {* \medskip A customized induction schema for @{text "$$"}. *}
-lemma lem [rulify]:
+lemma lem [rulified (no_asm)]:
"[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
|] ==> \<forall>t. size t = n --> P t"
--- a/src/HOL/Lambda/ListBeta.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/ListBeta.thy Thu Sep 07 21:10:11 2000 +0200
@@ -96,7 +96,7 @@
apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
done
-lemma apps_preserves_betas [rulify, simp]:
+lemma apps_preserves_betas [rulified, simp]:
"\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
apply (induct_tac rs rule: rev_induct)
apply simp
--- a/src/HOL/Lambda/ListOrder.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/ListOrder.thy Thu Sep 07 21:10:11 2000 +0200
@@ -64,7 +64,7 @@
apply (blast intro: append_eq_appendI)
done
-lemma Cons_step1E [rulify_prems, elim!]:
+lemma Cons_step1E [rulified, elim!]:
"[| (ys, x # xs) \<in> step1 r;
\<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
\<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R
@@ -87,7 +87,7 @@
apply blast
done
-lemma Cons_acc_step1I [rulify, intro!]:
+lemma Cons_acc_step1I [rulified, intro!]:
"x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
apply (erule acc_induct)
apply (erule thin_rl)
--- a/src/HOL/Lambda/ParRed.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/ParRed.thy Thu Sep 07 21:10:11 2000 +0200
@@ -70,13 +70,13 @@
subsection {* Misc properties of par-beta *}
-lemma par_beta_lift [rulify, simp]:
+lemma par_beta_lift [rulified, simp]:
"\<forall>t' n. t => t' --> lift t n => lift t' n"
apply (induct_tac t)
apply fastsimp+
done
-lemma par_beta_subst [rulify]:
+lemma par_beta_subst [rulified]:
"\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
apply (induct_tac t)
apply (simp add: subst_Var)
@@ -110,7 +110,7 @@
"cd (Abs u $ t) = (cd u)[cd t/0]"
"cd (Abs s) = Abs (cd s)"
-lemma par_beta_cd [rulify]:
+lemma par_beta_cd [rulified]:
"\<forall>t. s => t --> t => cd s"
apply (induct_tac s rule: cd.induct)
apply auto
--- a/src/HOL/Lambda/Type.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Lambda/Type.thy Thu Sep 07 21:10:11 2000 +0200
@@ -74,7 +74,7 @@
text {* Iterated function types *}
-lemma list_app_typeD [rulify]:
+lemma list_app_typeD [rulified]:
"\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)"
apply (induct_tac ts)
apply simp
@@ -90,7 +90,7 @@
apply simp
done
-lemma list_app_typeI [rulify]:
+lemma list_app_typeI [rulified]:
"\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
apply (induct_tac ts)
apply (intro strip)
@@ -109,7 +109,7 @@
apply blast
done
-lemma lists_types [rulify]:
+lemma lists_types [rulified]:
"\<forall>Ts. types e ts Ts --> ts \<in> lists {t. \<exists>T. e |- t : T}"
apply (induct_tac ts)
apply (intro strip)
@@ -129,19 +129,19 @@
subsection {* Lifting preserves termination and well-typedness *}
-lemma lift_map [rulify, simp]:
+lemma lift_map [rulified, simp]:
"\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
apply (induct_tac ts)
apply simp_all
done
-lemma subst_map [rulify, simp]:
+lemma subst_map [rulified, simp]:
"\<forall>t. subst (t $$ ts) u i = subst t u i $$ map (\<lambda>t. subst t u i) ts"
apply (induct_tac ts)
apply simp_all
done
-lemma lift_IT [rulify, intro!]:
+lemma lift_IT [rulified, intro!]:
"t \<in> IT ==> \<forall>i. lift t i \<in> IT"
apply (erule IT.induct)
apply (rule allI)
@@ -161,7 +161,7 @@
apply auto
done
-lemma lifts_IT [rulify]:
+lemma lifts_IT [rulified]:
"ts \<in> lists IT --> map (\<lambda>t. lift t 0) ts \<in> lists IT"
apply (induct_tac ts)
apply auto
@@ -180,7 +180,7 @@
apply simp_all
done
-lemma lift_type' [rulify]:
+lemma lift_type' [rulified]:
"e |- t : T ==> \<forall>i U.
(\<lambda>j. if j < i then e j
else if j = i then U
@@ -202,7 +202,7 @@
apply simp_all
done
-lemma lift_types [rulify]:
+lemma lift_types [rulified]:
"\<forall>Ts. types e ts Ts -->
types (\<lambda>j. if j < i then e j
else if j = i then U
@@ -219,7 +219,7 @@
subsection {* Substitution lemmas *}
-lemma subst_lemma [rulify]:
+lemma subst_lemma [rulified]:
"e |- t : T ==> \<forall>e' i U u.
e = (\<lambda>j. if j < i then e' j
else if j = i then U
@@ -242,7 +242,7 @@
apply fastsimp
done
-lemma substs_lemma [rulify]:
+lemma substs_lemma [rulified]:
"e |- u : T ==>
\<forall>Ts. types (\<lambda>j. if j < i then e j
else if j = i then T else e (j - 1)) ts Ts -->
@@ -265,7 +265,7 @@
subsection {* Subject reduction *}
-lemma subject_reduction [rulify]:
+lemma subject_reduction [rulified]:
"e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T"
apply (erule typing.induct)
apply blast
@@ -290,7 +290,7 @@
apply simp
done
-lemma subst_Var_IT [rulify]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
+lemma subst_Var_IT [rulified]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
apply (erule IT.induct)
txt {* Case @{term Var}: *}
apply (intro strip)
@@ -334,7 +334,7 @@
apply (rule lists.Cons)
apply (rule Var_IT)
apply (rule lists.Nil)
- apply (rule IT.Beta [where ?ss = "[]", unfold foldl_Nil [THEN eq_reflection]])
+ apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]])
apply (erule subst_Var_IT)
apply (rule Var_IT)
apply (subst app_last)
@@ -347,7 +347,7 @@
subsection {* Well-typed substitution preserves termination *}
-lemma subst_type_IT [rulify]:
+lemma subst_type_IT [rulified]:
"\<forall>t. t \<in> IT --> (\<forall>e T u i.
(\<lambda>j. if j < i then e j
else if j = i then U
@@ -454,7 +454,7 @@
apply simp
apply (rule subst_type_IT)
apply (rule lists.Nil
- [THEN 2 lists.Cons [THEN IT.Var], unfold foldl_Nil [THEN eq_reflection]
+ [THEN 2 lists.Cons [THEN IT.Var], unfolded foldl_Nil [THEN eq_reflection]
foldl_Cons [THEN eq_reflection]])
apply (erule lift_IT)
apply (rule typing.App)
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Sep 07 21:10:11 2000 +0200
@@ -587,7 +587,7 @@
by (auto simp add: correct_state_def Let_def)
-lemma BV_correct_1 [rulify]:
+lemma BV_correct_1 [rulified]:
"\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk>
\<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (simp only: split_tupled_all)
@@ -617,7 +617,7 @@
done
-theorem BV_correct [rulify]:
+theorem BV_correct [rulified]:
"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
apply (unfold exec_all_def)
apply (erule rtrancl_induct)
--- a/src/HOL/MicroJava/BV/Convert.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy Thu Sep 07 21:10:11 2000 +0200
@@ -383,7 +383,7 @@
qed
-theorem sup_loc_update [rulify]:
+theorem sup_loc_update [rulified]:
"\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow>
(G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
proof (induct x)
@@ -485,7 +485,7 @@
with G
show ?thesis
- by (auto intro!: all_nth_sup_loc [rulify] dest!: sup_loc_length)
+ by (auto intro!: all_nth_sup_loc [rulified] dest!: sup_loc_length)
qed
--- a/src/HOL/MicroJava/BV/Correct.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Thu Sep 07 21:10:11 2000 +0200
@@ -92,11 +92,11 @@
"approx_val G hp Null (Ok (RefT x))"
by (auto intro: null simp add: approx_val_def)
-lemma approx_val_imp_approx_val_assConvertible [rulify]:
+lemma approx_val_imp_approx_val_assConvertible [rulified]:
"wf_prog wt G \<Longrightarrow> approx_val G hp v (Ok T) \<longrightarrow> G\<turnstile> T\<preceq>T' \<longrightarrow> approx_val G hp v (Ok T')"
by (cases T) (auto intro: conf_widen simp add: approx_val_def)
-lemma approx_val_imp_approx_val_sup_heap [rulify]:
+lemma approx_val_imp_approx_val_sup_heap [rulified]:
"approx_val G hp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' v at"
apply (simp add: approx_val_def split: err.split)
apply (blast intro: conf_hext)
@@ -107,7 +107,7 @@
\<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T"
by (cases v, auto simp add: obj_ty_def conf_def)
-lemma approx_val_imp_approx_val_sup [rulify]:
+lemma approx_val_imp_approx_val_sup [rulified]:
"wf_prog wt G \<Longrightarrow> (approx_val G h v us) \<longrightarrow> (G \<turnstile> us <=o us') \<longrightarrow> (approx_val G h v us')"
apply (simp add: sup_PTS_eq approx_val_def split: err.split)
apply (blast intro: conf_widen)
@@ -128,7 +128,7 @@
"approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)"
by (simp add: approx_loc_def)
-lemma assConv_approx_stk_imp_approx_loc [rulify]:
+lemma assConv_approx_stk_imp_approx_loc [rulified]:
"wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G)
\<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow>
approx_loc G hp s (map Ok ts)"
@@ -139,7 +139,7 @@
.
-lemma approx_loc_imp_approx_loc_sup_heap [rulify]:
+lemma approx_loc_imp_approx_loc_sup_heap [rulified]:
"\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_loc G hp' lvars lt"
apply (unfold approx_loc_def list_all2_def)
apply (cases lt)
@@ -149,7 +149,7 @@
apply auto
.
-lemma approx_loc_imp_approx_loc_sup [rulify]:
+lemma approx_loc_imp_approx_loc_sup [rulified]:
"wf_prog wt G \<Longrightarrow> approx_loc G hp lvars lt \<longrightarrow> G \<turnstile> lt <=l lt' \<longrightarrow> approx_loc G hp lvars lt'"
apply (unfold sup_loc_def approx_loc_def list_all2_def)
apply (auto simp add: all_set_conv_all_nth)
@@ -157,7 +157,7 @@
.
-lemma approx_loc_imp_approx_loc_subst [rulify]:
+lemma approx_loc_imp_approx_loc_subst [rulified]:
"\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X)
\<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
apply (unfold approx_loc_def list_all2_def)
@@ -167,7 +167,7 @@
lemmas [cong] = conj_cong
-lemma approx_loc_append [rulify]:
+lemma approx_loc_append [rulified]:
"\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow>
approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
apply (unfold approx_loc_def list_all2_def)
@@ -191,11 +191,11 @@
by (auto intro: subst [OF approx_stk_rev_lem])
-lemma approx_stk_imp_approx_stk_sup_heap [rulify]:
+lemma approx_stk_imp_approx_stk_sup_heap [rulified]:
"\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_stk G hp' lvars lt"
by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
-lemma approx_stk_imp_approx_stk_sup [rulify]:
+lemma approx_stk_imp_approx_stk_sup [rulified]:
"wf_prog wt G \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st'))
\<longrightarrow> approx_stk G hp lvars st'"
by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
@@ -232,13 +232,13 @@
.
-lemma oconf_imp_oconf_field_update [rulify]:
+lemma oconf_imp_oconf_field_update [rulified]:
"\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
\<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
by (simp add: oconf_def lconf_def)
-lemma oconf_imp_oconf_heap_newref [rulify]:
+lemma oconf_imp_oconf_heap_newref [rulified]:
"hp x = None \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G,hp\<turnstile>obj'\<surd> \<longrightarrow> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
apply (unfold oconf_def lconf_def)
apply simp
@@ -246,7 +246,7 @@
.
-lemma oconf_imp_oconf_heap_update [rulify]:
+lemma oconf_imp_oconf_heap_update [rulified]:
"hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd>
\<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
apply (unfold oconf_def lconf_def)
@@ -258,13 +258,13 @@
(** hconf **)
-lemma hconf_imp_hconf_newref [rulify]:
+lemma hconf_imp_hconf_newref [rulified]:
"hp x = None \<longrightarrow> G\<turnstile>h hp\<surd> \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
apply (simp add: hconf_def)
apply (fast intro: oconf_imp_oconf_heap_newref)
.
-lemma hconf_imp_hconf_field_update [rulify]:
+lemma hconf_imp_hconf_field_update [rulified]:
"map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and>
G,hp\<turnstile>v\<Colon>\<preceq>T \<and> G\<turnstile>h hp\<surd> \<longrightarrow> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
apply (simp add: hconf_def)
@@ -276,7 +276,7 @@
lemmas [simp del] = fun_upd_apply
-lemma correct_frames_imp_correct_frames_field_update [rulify]:
+lemma correct_frames_imp_correct_frames_field_update [rulified]:
"\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow>
hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow>
G,hp\<turnstile>v\<Colon>\<preceq>fd
@@ -299,7 +299,7 @@
apply simp
.
-lemma correct_frames_imp_correct_frames_newref [rulify]:
+lemma correct_frames_imp_correct_frames_newref [rulified]:
"\<forall>rT C sig. hp x = None \<longrightarrow> correct_frames G hp phi rT sig frs \<and> oconf G hp obj
\<longrightarrow> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
apply (induct frs)
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Thu Sep 07 21:10:11 2000 +0200
@@ -161,7 +161,7 @@
case None
with wtl fits
show ?thesis
- by - (rule wtl_inst_mono [elimify], (simp add: wtl_cert_def)+)
+ by - (rule wtl_inst_mono [elimified], (simp add: wtl_cert_def)+)
next
case Some
with wtl fits
@@ -406,7 +406,7 @@
"[| wt_method G C pTs rT mxl ins phi; fits ins cert phi |] ==>
wtl_method G C pTs rT mxl ins cert"
by (simp add: wt_method_def wtl_method_def)
- (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def)
+ (rule wt_imp_wtl_inst_list [rulified, elimified], auto simp add: wt_start_def)
lemma wtl_method_complete:
@@ -462,17 +462,17 @@
from 1
show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"
- proof (rule bspec [elimify], clarsimp)
+ proof (rule bspec [elimified], clarsimp)
assume ub : "unique b"
assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and>
(\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb"
from m b
show ?thesis
- proof (rule bspec [elimify], clarsimp)
+ proof (rule bspec [elimified], clarsimp)
assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"
with wfprog uG ub b 1
show ?thesis
- by - (rule wtl_method_complete [elimify], assumption+,
+ by - (rule wtl_method_complete [elimified], assumption+,
simp add: make_Cert_def unique_epsilon)
qed
qed
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Sep 07 21:10:11 2000 +0200
@@ -264,7 +264,7 @@
assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err"
obtain phi where fits: "fits phi ins G rT ?s0 cert"
- by (rule exists_phi [elimify]) blast
+ by (rule exists_phi [elimified]) blast
with wtl
have allpc:
--- a/src/HOL/MicroJava/BV/StepMono.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy Thu Sep 07 21:10:11 2000 +0200
@@ -13,7 +13,7 @@
by (auto elim: widen.elims)
-lemma sup_loc_some [rulify]:
+lemma sup_loc_some [rulified]:
"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Ok t \<longrightarrow>
(\<exists>t. b!n = Ok t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
proof (induct (open) ?P b)
@@ -59,7 +59,7 @@
qed
-lemma append_length_n [rulify]:
+lemma append_length_n [rulified]:
"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
proof (induct (open) ?P x)
show "?P []" by simp
@@ -78,7 +78,7 @@
fix "n'" assume s: "n = Suc n'"
with l
have "n' \<le> length ls" by simp
- hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rulify])
+ hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rulified])
thus ?thesis
proof elim
fix a b
@@ -254,7 +254,7 @@
have "length list < length (fst s2)"
by (simp add: sup_state_length)
hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
- by (rule rev_append_cons [rulify])
+ by (rule rev_append_cons [rulified])
thus ?thesis
by - (cases s2, elim exE conjE, simp, rule that)
qed
--- a/src/HOL/Real/HahnBanach/Aux.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Thu Sep 07 21:10:11 2000 +0200
@@ -12,7 +12,7 @@
lemmas [intro?] = isLub_isUb
lemmas [intro?] = chainD
-lemmas chainE2 = chainD2 [elimify]
+lemmas chainE2 = chainD2 [elimified]
text_raw {* \medskip *}
text{* Lemmas about sets. *}
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Sep 07 21:10:11 2000 +0200
@@ -273,7 +273,7 @@
by case analysis on $a$. *};
also; have "... <= p (y + a \<cdot> x0)";
- proof (rule linorder_less_split);
+ proof (rule linorder_cases);
assume z: "a = #0";
with vs y a; show ?thesis; by simp;
--- a/src/HOL/Real/HahnBanach/Subspace.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Thu Sep 07 21:10:11 2000 +0200
@@ -227,7 +227,7 @@
"x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
by (unfold vs_sum_def) fast
-lemmas vs_sumE = vs_sumD [THEN iffD1, elimify, standard]
+lemmas vs_sumE = vs_sumD [THEN iffD1, elimified, standard]
lemma vs_sumI [intro?]:
"[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
--- a/src/HOL/ex/Primes.thy Thu Sep 07 21:06:55 2000 +0200
+++ b/src/HOL/ex/Primes.thy Thu Sep 07 21:10:11 2000 +0200
@@ -71,7 +71,7 @@
(*Maximality: for all m,n,f naturals,
if f divides m and f divides n then f divides gcd(m,n)*)
-lemma gcd_greatest [rulify]: "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"
+lemma gcd_greatest [rulified]: "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"
apply (induct_tac m n rule: gcd_induct)
apply (simp_all add: gcd_non_0 dvd_mod);
done;