--- a/NEWS Tue Sep 12 19:03:13 2000 +0200
+++ b/NEWS Tue Sep 12 22:13:23 2000 +0200
@@ -52,8 +52,8 @@
* ZF: new treatment of arithmetic (nat & int) may break some old proofs;
-* Isar/Provers: intro/elim/dest attributes: changed
-intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one
+* Isar/Provers: intro/elim/dest attributes changed; renamed
+intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one
should have to change intro!! to intro? only); replaced "delrule" by
"rule del";
@@ -61,7 +61,7 @@
* Isar: renamed 'RS' attribute to 'THEN';
-* Isar: renamed some attributes (rulify -> rulified, elimify -> elimified, ...);
+* Isar: renamed some attributes (rulify -> rule_format, elimify -> elim_format, ...);
* Isar/HOL: renamed "intrs" to "intros" in inductive definitions;
@@ -192,9 +192,10 @@
'inductive_cases' command and 'ind_cases' method; NOTE: use (cases
(simplified)) method in proper proofs;
-* Provers: intro/elim/dest attributes: changed intro/intro!/intro!!
-flags to intro!/intro/intro? (in most cases, one should have to change
-intro!! to intro? only); replaced "delrule" by "rule del";
+* Provers: intro/elim/dest attributes changed; renamed
+intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in
+most cases, one should have to change intro!! to intro? only);
+replaced "delrule" by "rule del";
* names of theorems etc. may be natural numbers as well;
@@ -336,6 +337,9 @@
*** General ***
+* Provers: delrules now handles destruct rules as well (no longer need
+explicit make_elim);
+
* Provers: blast(_tac) now handles actual object-logic rules as
assumptions; note that auto(_tac) uses blast(_tac) internally as well;
--- a/doc-src/IsarRef/generic.tex Tue Sep 12 19:03:13 2000 +0200
+++ b/doc-src/IsarRef/generic.tex Tue Sep 12 22:13:23 2000 +0200
@@ -305,7 +305,7 @@
\indexisaratt{standard}
-\indexisaratt{elimified}
+\indexisaratt{elim-format}
\indexisaratt{no-vars}
\indexisaratt{THEN}\indexisaratt{COMP}
@@ -320,7 +320,7 @@
unfolded & : & \isaratt \\
folded & : & \isaratt \\[0.5ex]
standard & : & \isaratt \\
- elimified & : & \isaratt \\
+ elim_format & : & \isaratt \\
no_vars^* & : & \isaratt \\
exported^* & : & \isaratt \\
\end{matharray}
@@ -356,8 +356,8 @@
given meta-level definitions throughout a rule.
\item [$standard$] puts a theorem into the standard form of object-rules, just
as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
-\item [$elimified$] turns an destruction rule into an elimination, just as the
- ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
+\item [$elim_format$] turns a destruction rule into elimination rule format;
+ see also the ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
\item [$no_vars$] replaces schematic variables by free ones; this is mainly
for tuning output of pretty printed theorems.
\item [$exported$] lifts a local result out of the current proof context,
--- a/doc-src/IsarRef/hol.tex Tue Sep 12 19:03:13 2000 +0200
+++ b/doc-src/IsarRef/hol.tex Tue Sep 12 22:13:23 2000 +0200
@@ -3,21 +3,24 @@
\section{Miscellaneous attributes}
-\indexisaratt{rulified}
+\indexisaratt{rule-format}
\begin{matharray}{rcl}
- rulified & : & \isaratt \\
+ rule_format & : & \isaratt \\
\end{matharray}
+\railalias{ruleformat}{rule\_format}
+\railterm{ruleformat}
+
\begin{rail}
- 'rulified' ('(' noasm ')')?
+ ruleformat ('(' noasm ')')?
;
\end{rail}
\begin{descr}
-\item [$rulified$] causes a theorem to be put into standard object-rule form,
- replacing implication and (bounded) universal quantification of HOL by the
- corresponding meta-logical connectives. By default, the result is fully
+\item [$rule_format$] causes a theorem to be put into standard object-rule
+ form, replacing implication and (bounded) universal quantification of HOL by
+ the corresponding meta-logical connectives. By default, the result is fully
normalized, including assumptions and conclusions at any depth. The
$no_asm$ option restricts the transformation to the conclusion of a rule.
\end{descr}
--- a/doc-src/IsarRef/refcard.tex Tue Sep 12 19:03:13 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex Tue Sep 12 22:13:23 2000 +0200
@@ -118,8 +118,8 @@
$of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
$symmetric$ & resolution with symmetry of equality \\
$THEN~b$ & resolution with other rule \\
- $rulified$ & result put into standard rule form \\
- $elimified$ & destruct rule turned into elimination rule \\
+ $rule_format$ & result put into standard rule format \\
+ $elim_format$ & destruct rule turned into elimination rule format \\
$standard$ & result put into standard form \\[1ex]
\multicolumn{2}{l}{\textbf{Declarations}} \\[0.5ex]
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Sep 12 22:13:23 2000 +0200
@@ -94,10 +94,10 @@
text{*\noindent
or the wholesale stripping of @{text"\<forall>"} and
-@{text"\<longrightarrow>"} in the conclusion via @{text"rulified"}
+@{text"\<longrightarrow>"} in the conclusion via @{text"rule_format"}
*};
-lemmas myrule = simple[rulified];
+lemmas myrule = simple[rule_format];
text{*\noindent
yielding @{thm"myrule"[no_vars]}.
@@ -105,7 +105,7 @@
statement of your original lemma, thus avoiding the intermediate step:
*};
-lemma myrule[rulified]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma myrule[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
(*<*)
by blast;
(*>*)
@@ -206,14 +206,14 @@
We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}:
*};
-lemmas f_incr = f_incr_lem[rulified, OF refl];
+lemmas f_incr = f_incr_lem[rule_format, OF refl];
text{*\noindent
The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. Again,
we could have included this derivation in the original statement of the lemma:
*};
-lemma f_incr[rulified, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
+lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
(*<*)oops;(*>*)
text{*
--- a/src/HOL/Induct/Acc.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Induct/Acc.thy Tue Sep 12 22:13:23 2000 +0200
@@ -18,7 +18,7 @@
inductive "acc r"
intros
- accI [rulified]:
+ accI [rule_format]:
"\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r"
syntax
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Tue Sep 12 22:13:23 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 [rulified]);
+ proof (rule tiling_Un [rule_format]);
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 Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy Tue Sep 12 22:13:23 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 [rulified]);
+ hence "f (Suc n) <= f (f n)"; by (rule mono [rule_format]);
also; have "... < f (Suc n)"; by (rule f_ax);
finally; have "... < ..."; .; thus False; ..;
qed;
--- a/src/HOL/Lambda/Eta.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/Eta.thy Tue Sep 12 22:13:23 2000 +0200
@@ -45,7 +45,7 @@
subsection "Properties of eta, subst and free"
-lemma subst_not_free [rulified, simp]:
+lemma subst_not_free [rule_format, 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 [rulified]:
+lemma free_eta [rule_format]:
"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 [rulified, simp]:
+lemma eta_subst [rule_format, 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 [rulified]:
+lemma free_beta [rule_format]:
"s -> t ==> \<forall>i. free t i --> free s i"
apply (erule beta.induct)
apply simp_all
done
-lemma beta_subst [rulified, intro]:
+lemma beta_subst [rule_format, 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 [rulified, simp]:
+lemma eta_lift [rule_format, 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 [rulified]:
+lemma rtrancl_eta_subst [rule_format]:
"\<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 [rulified]:
+lemma not_free_iff_lifted [rule_format]:
"\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
apply (induct_tac s)
apply simp
--- a/src/HOL/Lambda/InductTermi.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/InductTermi.thy Tue Sep 12 22:13:23 2000 +0200
@@ -26,7 +26,7 @@
subsection {* Every term in IT terminates *}
-lemma double_induction_lemma [rulified]:
+lemma double_induction_lemma [rule_format]:
"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 Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/Lambda.thy Tue Sep 12 22:13:23 2000 +0200
@@ -120,7 +120,7 @@
apply (simp add: subst_Var)
done
-lemma lift_lift [rulified]:
+lemma lift_lift [rule_format]:
"\<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 [rulified]:
+lemma subst_subst [rule_format]:
"\<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 [rulified, simp]:
+theorem subst_preserves_beta [rule_format, 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 [rulified, simp]:
+theorem lift_preserves_beta [rule_format, simp]:
"r -> s ==> \<forall>i. lift r i -> lift s i"
apply (erule beta.induct)
apply auto
done
-theorem subst_preserves_beta2 [rulified, simp]:
+theorem subst_preserves_beta2 [rule_format, 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 Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.thy Tue Sep 12 22:13:23 2000 +0200
@@ -18,13 +18,13 @@
apply auto
done
-lemma Var_eq_apps_conv [rulified, iff]:
+lemma Var_eq_apps_conv [rule_format, 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 [rulified, iff]:
+lemma Var_apps_eq_Var_apps_conv [rule_format, 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 [rulified, iff]:
+lemma Var_apps_neq_Abs_apps [rule_format, 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 [rulified (no_asm)]:
+lemma lem [rule_format (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 Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/ListBeta.thy Tue Sep 12 22:13:23 2000 +0200
@@ -96,7 +96,7 @@
apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
done
-lemma apps_preserves_betas [rulified, simp]:
+lemma apps_preserves_betas [rule_format, simp]:
"\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
apply (induct_tac rs rule: rev_induct)
apply simp
--- a/src/HOL/Lambda/ListOrder.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/ListOrder.thy Tue Sep 12 22:13:23 2000 +0200
@@ -64,7 +64,7 @@
apply (blast intro: append_eq_appendI)
done
-lemma Cons_step1E [rulified, elim!]:
+lemma Cons_step1E [rule_format, 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 [rulified, intro!]:
+lemma Cons_acc_step1I [rule_format, 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 Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/ParRed.thy Tue Sep 12 22:13:23 2000 +0200
@@ -70,13 +70,13 @@
subsection {* Misc properties of par-beta *}
-lemma par_beta_lift [rulified, simp]:
+lemma par_beta_lift [rule_format, simp]:
"\<forall>t' n. t => t' --> lift t n => lift t' n"
apply (induct_tac t)
apply fastsimp+
done
-lemma par_beta_subst [rulified]:
+lemma par_beta_subst [rule_format]:
"\<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 [rulified]:
+lemma par_beta_cd [rule_format]:
"\<forall>t. s => t --> t => cd s"
apply (induct_tac s rule: cd.induct)
apply auto
--- a/src/HOL/Lambda/Type.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Lambda/Type.thy Tue Sep 12 22:13:23 2000 +0200
@@ -74,7 +74,7 @@
text {* Iterated function types *}
-lemma list_app_typeD [rulified]:
+lemma list_app_typeD [rule_format]:
"\<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 [rulified]:
+lemma list_app_typeI [rule_format]:
"\<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 [rulified]:
+lemma lists_types [rule_format]:
"\<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 [rulified, simp]:
+lemma lift_map [rule_format, 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 [rulified, simp]:
+lemma subst_map [rule_format, 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 [rulified, intro!]:
+lemma lift_IT [rule_format, 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 [rulified]:
+lemma lifts_IT [rule_format]:
"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' [rulified]:
+lemma lift_type' [rule_format]:
"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 [rulified]:
+lemma lift_types [rule_format]:
"\<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 [rulified]:
+lemma subst_lemma [rule_format]:
"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 [rulified]:
+lemma substs_lemma [rule_format]:
"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 [rulified]:
+lemma subject_reduction [rule_format]:
"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 [rulified]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
+lemma subst_Var_IT [rule_format]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
apply (erule IT.induct)
txt {* Case @{term Var}: *}
apply (intro strip)
@@ -347,7 +347,7 @@
subsection {* Well-typed substitution preserves termination *}
-lemma subst_type_IT [rulified]:
+lemma subst_type_IT [rule_format]:
"\<forall>t. t \<in> IT --> (\<forall>e T u i.
(\<lambda>j. if j < i then e j
else if j = i then U
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Sep 12 22:13:23 2000 +0200
@@ -587,7 +587,7 @@
by (auto simp add: correct_state_def Let_def)
-lemma BV_correct_1 [rulified]:
+lemma BV_correct_1 [rule_format]:
"\<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 [rulified]:
+theorem BV_correct [rule_format]:
"\<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 Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy Tue Sep 12 22:13:23 2000 +0200
@@ -383,7 +383,7 @@
qed
-theorem sup_loc_update [rulified]:
+theorem sup_loc_update [rule_format]:
"\<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 [rulified] dest!: sup_loc_length)
+ by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length)
qed
--- a/src/HOL/MicroJava/BV/Correct.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Tue Sep 12 22:13:23 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 [rulified]:
+lemma approx_val_imp_approx_val_assConvertible [rule_format]:
"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 [rulified]:
+lemma approx_val_imp_approx_val_sup_heap [rule_format]:
"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 [rulified]:
+lemma approx_val_imp_approx_val_sup [rule_format]:
"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 [rulified]:
+lemma assConv_approx_stk_imp_approx_loc [rule_format]:
"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 [rulified]:
+lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
"\<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 [rulified]:
+lemma approx_loc_imp_approx_loc_sup [rule_format]:
"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 [rulified]:
+lemma approx_loc_imp_approx_loc_subst [rule_format]:
"\<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 [rulified]:
+lemma approx_loc_append [rule_format]:
"\<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 [rulified]:
+lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
"\<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 [rulified]:
+lemma approx_stk_imp_approx_stk_sup [rule_format]:
"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 [rulified]:
+lemma oconf_imp_oconf_field_update [rule_format]:
"\<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 [rulified]:
+lemma oconf_imp_oconf_heap_newref [rule_format]:
"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 [rulified]:
+lemma oconf_imp_oconf_heap_update [rule_format]:
"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 [rulified]:
+lemma hconf_imp_hconf_newref [rule_format]:
"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 [rulified]:
+lemma hconf_imp_hconf_field_update [rule_format]:
"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 [rulified]:
+lemma correct_frames_imp_correct_frames_field_update [rule_format]:
"\<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 [rulified]:
+lemma correct_frames_imp_correct_frames_newref [rule_format]:
"\<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 Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Tue Sep 12 22:13:23 2000 +0200
@@ -161,7 +161,7 @@
case None
with wtl fits
show ?thesis
- by - (rule wtl_inst_mono [elimified], (simp add: wtl_cert_def)+)
+ by - (rule wtl_inst_mono [elim_format], (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 [rulified, elimified], auto simp add: wt_start_def)
+ (rule wt_imp_wtl_inst_list [rule_format, elim_format], 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 [elimified], clarsimp)
+ proof (rule bspec [elim_format], 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 [elimified], clarsimp)
+ proof (rule bspec [elim_format], 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 [elimified], assumption+,
+ by - (rule wtl_method_complete [elim_format], assumption+,
simp add: make_Cert_def unique_epsilon)
qed
qed
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Tue Sep 12 22:13:23 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 [elimified]) blast
+ by (rule exists_phi [elim_format]) blast
with wtl
have allpc:
--- a/src/HOL/MicroJava/BV/StepMono.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy Tue Sep 12 22:13:23 2000 +0200
@@ -13,7 +13,7 @@
by (auto elim: widen.elims)
-lemma sup_loc_some [rulified]:
+lemma sup_loc_some [rule_format]:
"\<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 [rulified]:
+lemma append_length_n [rule_format]:
"\<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 [rulified])
+ hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format])
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 [rulified])
+ by (rule rev_append_cons [rule_format])
thus ?thesis
by - (cases s2, elim exE conjE, simp, rule that)
qed
--- a/src/HOL/Real/HahnBanach/Aux.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy Tue Sep 12 22:13:23 2000 +0200
@@ -12,7 +12,7 @@
lemmas [intro?] = isLub_isUb
lemmas [intro?] = chainD
-lemmas chainE2 = chainD2 [elimified]
+lemmas chainE2 = chainD2 [elim_format, standard]
text_raw {* \medskip *}
text{* Lemmas about sets. *}
--- a/src/HOL/Real/HahnBanach/Subspace.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Tue Sep 12 22:13:23 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, elimified, standard]
+lemmas vs_sumE = vs_sumD [THEN iffD1, elim_format, standard]
lemma vs_sumI [intro?]:
"[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V"
--- a/src/HOL/ex/Primes.thy Tue Sep 12 19:03:13 2000 +0200
+++ b/src/HOL/ex/Primes.thy Tue Sep 12 22:13:23 2000 +0200
@@ -71,7 +71,7 @@
(*Maximality: for all m,n,k naturals,
if k divides m and k divides n then k divides gcd(m,n)*)
-lemma gcd_greatest [rulified]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
+lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
apply (induct_tac m n rule: gcd_induct)
apply (simp_all add: gcd_non_0 dvd_mod);
done;
--- a/src/Provers/classical.ML Tue Sep 12 19:03:13 2000 +0200
+++ b/src/Provers/classical.ML Tue Sep 12 22:13:23 2000 +0200
@@ -1046,10 +1046,11 @@
(* setup_attrs *)
-fun elimified x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x;
+fun elim_format x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x;
val setup_attrs = Attrib.add_attributes
- [("elimified", (elimified, elimified), "destruct rule turned into elimination rule (classical)"),
+ [("elim_format", (elim_format, elim_format),
+ "destruct rule turned into elimination rule format (classical)"),
(destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declaration of destruction rule"),
(elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declaration of elimination rule"),
(introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declaration of introduction rule"),
--- a/src/Provers/rulify.ML Tue Sep 12 19:03:13 2000 +0200
+++ b/src/Provers/rulify.ML Tue Sep 12 22:13:23 2000 +0200
@@ -19,8 +19,8 @@
signature RULIFY =
sig
include BASIC_RULIFY
- val rulified: 'a attribute
- val rulified_no_asm: 'a attribute
+ val rule_format: 'a attribute
+ val rule_format_no_asm: 'a attribute
val setup: (theory -> theory) list
end;
@@ -38,11 +38,11 @@
(* attributes *)
-fun rulified x = Drule.rule_attribute (fn _ => rulify) x;
-fun rulified_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
+fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;
+fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;
-fun rulified_att x = Attrib.syntax
- (Scan.lift (Args.parens (Args.$$$ "no_asm") >> K rulified_no_asm || Scan.succeed rulified)) x;
+fun rule_format_att x = Attrib.syntax
+ (Scan.lift (Args.parens (Args.$$$ "no_asm") >> K rule_format_no_asm || Scan.succeed rule_format)) x;
(* qed commands *)
@@ -60,6 +60,6 @@
val setup =
[Attrib.add_attributes
- [("rulified", (rulified_att, rulified_att), "result put into standard rule form")]];
+ [("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")]];
end;
--- a/src/Pure/Isar/attrib.ML Tue Sep 12 19:03:13 2000 +0200
+++ b/src/Pure/Isar/attrib.ML Tue Sep 12 22:13:23 2000 +0200
@@ -269,7 +269,7 @@
(* misc rules *)
fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
-fun elimified x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
+fun elim_format x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x;
fun exported_global x = no_args (Drule.rule_attribute (Proof.export_thm o ProofContext.init)) x;
@@ -292,7 +292,7 @@
("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"),
("folded", (folded_global, folded_local), "folded definitions"),
("standard", (standard, standard), "result put into standard form"),
- ("elimified", (elimified, elimified), "destruct rule turned into elimination rule"),
+ ("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"),
("no_vars", (no_vars, no_vars), "frozen schematic vars"),
("case_names", (case_names, case_names), "named rule cases"),
("params", (params, params), "named rule parameters"),