--- a/NEWS Tue Sep 04 17:31:18 2001 +0200
+++ b/NEWS Tue Sep 04 21:10:57 2001 +0200
@@ -5,6 +5,11 @@
New in Isabelle2001 (?? 2001)
-----------------------------
+*** Isar ***
+
+* renamed "antecedent" case to "rule_context";
+
+
*** HOL ***
* HOL: added "The" definite description operator;
--- a/doc-src/IsarRef/conversion.tex Tue Sep 04 17:31:18 2001 +0200
+++ b/doc-src/IsarRef/conversion.tex Tue Sep 04 21:10:57 2001 +0200
@@ -223,9 +223,9 @@
Note that the above scheme repeats the text of premises $\phi@1$, \dots, while
the conclusion $\psi$ is referenced via the automatic text abbreviation
$\Var{thesis}$. The assumption context may be invoked in a less verbose
-manner as well, using ``$\CASE{antecedent}$'' instead of
+manner as well, using ``$\CASE{rule_context}$'' instead of
``$\ASSUME{prem@1}{\phi@1}~\AND~\dots$'' above. Then the list of \emph{all}
-premises is bound to the name $antecedent$; Isar does not provide a way to
+premises is bound to the name $rule_context$; Isar does not provide a way to
destruct lists into single items, though.
\medskip In practice, actual rules are often rather direct consequences of
--- a/doc-src/IsarRef/pure.tex Tue Sep 04 17:31:18 2001 +0200
+++ b/doc-src/IsarRef/pure.tex Tue Sep 04 21:10:57 2001 +0200
@@ -761,8 +761,8 @@
Any goal statement causes some term abbreviations (such as $\Var{thesis}$,
$\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}.
-Furthermore, the local context of a (non-atomic) goal is provided via the case
-name $antecedent$\indexisarcase{antecedent}, see also \S\ref{sec:cases}.
+Furthermore, the local context of a (non-atomic) goal is provided via the
+$rule_context$\indexisarcase{rule-context} case, see also \S\ref{sec:cases}.
\medskip
--- a/src/HOL/Induct/Term.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Induct/Term.thy Tue Sep 04 21:10:57 2001 +0200
@@ -48,11 +48,11 @@
(!!f ts. list_all P ts ==> P (App f ts))
==> P t"
proof -
- case antecedent
+ case rule_context
have "P t \<and> list_all P ts"
apply (induct t and ts rule: term.induct)
- apply (rule antecedent)
- apply (rule antecedent)
+ apply (rule rule_context)
+ apply (rule rule_context)
apply assumption
apply simp_all
done
--- a/src/HOL/Lambda/ListApplication.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Lambda/ListApplication.thy Tue Sep 04 21:10:57 2001 +0200
@@ -108,7 +108,7 @@
!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
|] ==> \<forall>t. size t = n --> P t"
proof -
- case antecedent
+ case rule_context
show ?thesis
apply (induct_tac n rule: nat_less_induct)
apply (rule allI)
@@ -150,7 +150,7 @@
!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
|] ==> P t"
proof -
- case antecedent
+ case rule_context
show ?thesis
apply (rule_tac t = t in lem)
prefer 3
--- a/src/HOL/Lambda/ListBeta.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Lambda/ListBeta.thy Tue Sep 04 21:10:57 2001 +0200
@@ -76,7 +76,7 @@
==> R"
proof -
assume major: "r $$ rs -> s"
- case antecedent
+ case rule_context
show ?thesis
apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
apply (assumption | rule refl | erule prems exE conjE impE disjE)+
--- a/src/HOL/Library/Multiset.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Sep 04 21:10:57 2001 +0200
@@ -331,8 +331,8 @@
"P (\<lambda>a. 0) ==> (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1')))
==> \<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
proof -
- case antecedent
- note prems = this [unfolded multiset_def]
+ case rule_context
+ note premises = this [unfolded multiset_def]
show ?thesis
apply (unfold multiset_def)
apply (induct_tac n)
@@ -340,7 +340,7 @@
apply clarify
apply (subgoal_tac "f = (\<lambda>a.0)")
apply simp
- apply (rule prems)
+ apply (rule premises)
apply (rule ext)
apply force
apply clarify
@@ -358,7 +358,7 @@
prefer 2
apply (rule ext)
apply (simp (no_asm_simp))
- apply (erule ssubst, rule prems)
+ apply (erule ssubst, rule premises)
apply blast
apply (erule allE, erule impE, erule_tac [2] mp)
apply blast
--- a/src/HOL/Library/Quotient.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Library/Quotient.thy Tue Sep 04 21:10:57 2001 +0200
@@ -203,7 +203,7 @@
(!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
proof -
- case antecedent from this TrueI
+ case rule_context from this TrueI
show ?thesis by (rule quot_cond_function)
qed
--- a/src/HOL/Library/Rational_Numbers.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Library/Rational_Numbers.thy Tue Sep 04 21:10:57 2001 +0200
@@ -360,7 +360,7 @@
g (fract a b) (fract c d) = g (fract a' b') (fract c' d')) ==>
f (Fract a b) (Fract c d) = g (fract a b) (fract c d)"
proof -
- case antecedent from this TrueI
+ case rule_context from this TrueI
show ?thesis by (rule rat_cond_function)
qed
--- a/src/HOL/Library/While_Combinator.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Library/While_Combinator.thy Tue Sep 04 21:10:57 2001 +0200
@@ -79,14 +79,14 @@
wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
P s --> Q (while b c s)"
proof -
- case antecedent
+ case rule_context
assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
show ?thesis
apply (induct s rule: wf [THEN wf_induct])
apply simp
apply clarify
apply (subst while_unfold)
- apply (simp add: antecedent)
+ apply (simp add: rule_context)
done
qed
--- a/src/HOL/MicroJava/BV/Err.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/MicroJava/BV/Err.thy Tue Sep 04 21:10:57 2001 +0200
@@ -257,7 +257,7 @@
[| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |]
==> x <=_r z \<and> y <=_r z"
by (rule plus_le_conv [THEN iffD1])
- case antecedent
+ case rule_context
thus ?thesis
apply (rule_tac iffI)
apply clarify
--- a/src/HOL/MicroJava/BV/Kildall.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy Tue Sep 04 21:10:57 2001 +0200
@@ -165,7 +165,7 @@
done
} note this [dest]
- case antecedent
+ case rule_context
thus ?thesis by blast
qed
--- a/src/HOL/MicroJava/BV/Product.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/MicroJava/BV/Product.thy Tue Sep 04 21:10:57 2001 +0200
@@ -79,7 +79,7 @@
"!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z"
by (rule plus_le_conv [THEN iffD1])
- case antecedent
+ case rule_context
thus ?thesis
apply (rule_tac iffI)
apply clarify
--- a/src/HOL/NumberTheory/BijectionRel.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/NumberTheory/BijectionRel.thy Tue Sep 04 21:10:57 2001 +0200
@@ -67,13 +67,13 @@
(!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F))
==> P F"
proof -
- case antecedent
+ case rule_context
assume major: "finite F"
and subs: "F \<subseteq> A"
show ?thesis
apply (rule subs [THEN rev_mp])
apply (rule major [THEN finite_induct])
- apply (blast intro: antecedent)+
+ apply (blast intro: rule_context)+
done
qed
--- a/src/HOL/NumberTheory/EulerFermat.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy Tue Sep 04 21:10:57 2001 +0200
@@ -71,14 +71,14 @@
==> P (BnorRset(a,m)) a m)
==> P (BnorRset(u,v)) u v"
proof -
- case antecedent
+ case rule_context
show ?thesis
apply (rule BnorRset.induct)
apply safe
apply (case_tac [2] "#0 < a")
- apply (rule_tac [2] antecedent)
+ apply (rule_tac [2] rule_context)
apply simp_all
- apply (simp_all add: BnorRset.simps antecedent)
+ apply (simp_all add: BnorRset.simps rule_context)
done
qed
--- a/src/HOL/NumberTheory/IntFact.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/NumberTheory/IntFact.thy Tue Sep 04 21:10:57 2001 +0200
@@ -58,14 +58,14 @@
==> P (d22set a) a)
==> P (d22set u) u"
proof -
- case antecedent
+ case rule_context
show ?thesis
apply (rule d22set.induct)
apply safe
apply (case_tac [2] "#1 < a")
- apply (rule_tac [2] antecedent)
+ apply (rule_tac [2] rule_context)
apply (simp_all (no_asm_simp))
- apply (simp_all (no_asm_simp) add: d22set.simps antecedent)
+ apply (simp_all (no_asm_simp) add: d22set.simps rule_context)
done
qed
--- a/src/HOL/NumberTheory/WilsonRuss.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Tue Sep 04 21:10:57 2001 +0200
@@ -184,14 +184,14 @@
==> P (wset (a, p)) a p)
==> P (wset (u, v)) u v"
proof -
- case antecedent
+ case rule_context
show ?thesis
apply (rule wset.induct)
apply safe
apply (case_tac [2] "#1 < a")
- apply (rule_tac [2] antecedent)
+ apply (rule_tac [2] rule_context)
apply simp_all
- apply (simp_all add: wset.simps antecedent)
+ apply (simp_all add: wset.simps rule_context)
done
qed
--- a/src/HOL/Unix/Unix.thy Tue Sep 04 17:31:18 2001 +0200
+++ b/src/HOL/Unix/Unix.thy Tue Sep 04 21:10:57 2001 +0200
@@ -618,7 +618,7 @@
"root =xs\<Rightarrow> root' \<Longrightarrow> \<exists>att dir. root = Env att dir
\<Longrightarrow> \<exists>att dir. root' = Env att dir"
proof -
- case antecedent
+ case rule_context
with transition_type_safe show ?thesis
proof (rule transitions_invariant)
show "\<forall>x \<in> set xs. True" by blast
@@ -957,7 +957,7 @@
lemma init_invariant: "init users =bogus\<Rightarrow> root \<Longrightarrow> invariant root bogus_path"
proof -
note eval = "setup" access_def init_def
- case antecedent thus ?thesis
+ case rule_context thus ?thesis
apply (unfold bogus_def bogus_path_def)
apply (drule transitions_consD, rule transition.intros,
(force simp add: eval)+, (simp add: eval)?)+
@@ -1126,7 +1126,7 @@
\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user1) \<and>
can_exec root (xs @ [Rmdir user1 [user1, name1]]))"
proof -
- case antecedent
+ case rule_context
with cannot_rmdir init_invariant preserve_invariant
show ?thesis by (rule general_procedure)
qed
--- a/src/Pure/Isar/proof.ML Tue Sep 04 17:31:18 2001 +0200
+++ b/src/Pure/Isar/proof.ML Tue Sep 04 21:10:57 2001 +0200
@@ -580,7 +580,7 @@
(* setup goals *)
-val antN = "antecedent";
+val rule_contextN = "rule_context";
fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
let
@@ -604,7 +604,7 @@
commas (map (Sign.string_of_term (sign_of state)) vars));
state'
|> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds))
- |> map_context (ProofContext.add_cases (RuleCases.make true goal [antN]))
+ |> map_context (ProofContext.add_cases (RuleCases.make true goal [rule_contextN]))
|> auto_bind_goal prop
|> (if is_chain state then use_facts else reset_facts)
|> new_block