renamed "antecedent" case to "rule_context";
authorwenzelm
Tue Sep 04 21:10:57 2001 +0200 (2001-09-04)
changeset 11549e7265e70fd7c
parent 11548 0028bd06a19c
child 11550 915c5de6480f
renamed "antecedent" case to "rule_context";
NEWS
doc-src/IsarRef/conversion.tex
doc-src/IsarRef/pure.tex
src/HOL/Induct/Term.thy
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ListBeta.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/Rational_Numbers.thy
src/HOL/Library/While_Combinator.thy
src/HOL/MicroJava/BV/Err.thy
src/HOL/MicroJava/BV/Kildall.thy
src/HOL/MicroJava/BV/Product.thy
src/HOL/NumberTheory/BijectionRel.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/IntFact.thy
src/HOL/NumberTheory/WilsonRuss.thy
src/HOL/Unix/Unix.thy
src/Pure/Isar/proof.ML
     1.1 --- a/NEWS	Tue Sep 04 17:31:18 2001 +0200
     1.2 +++ b/NEWS	Tue Sep 04 21:10:57 2001 +0200
     1.3 @@ -5,6 +5,11 @@
     1.4  New in Isabelle2001 (?? 2001)
     1.5  -----------------------------
     1.6  
     1.7 +*** Isar ***
     1.8 +
     1.9 +* renamed "antecedent" case to "rule_context";
    1.10 +
    1.11 +
    1.12  *** HOL ***
    1.13  
    1.14  * HOL: added "The" definite description operator;
     2.1 --- a/doc-src/IsarRef/conversion.tex	Tue Sep 04 17:31:18 2001 +0200
     2.2 +++ b/doc-src/IsarRef/conversion.tex	Tue Sep 04 21:10:57 2001 +0200
     2.3 @@ -223,9 +223,9 @@
     2.4  Note that the above scheme repeats the text of premises $\phi@1$, \dots, while
     2.5  the conclusion $\psi$ is referenced via the automatic text abbreviation
     2.6  $\Var{thesis}$.  The assumption context may be invoked in a less verbose
     2.7 -manner as well, using ``$\CASE{antecedent}$'' instead of
     2.8 +manner as well, using ``$\CASE{rule_context}$'' instead of
     2.9  ``$\ASSUME{prem@1}{\phi@1}~\AND~\dots$'' above.  Then the list of \emph{all}
    2.10 -premises is bound to the name $antecedent$; Isar does not provide a way to
    2.11 +premises is bound to the name $rule_context$; Isar does not provide a way to
    2.12  destruct lists into single items, though.
    2.13  
    2.14  \medskip In practice, actual rules are often rather direct consequences of
     3.1 --- a/doc-src/IsarRef/pure.tex	Tue Sep 04 17:31:18 2001 +0200
     3.2 +++ b/doc-src/IsarRef/pure.tex	Tue Sep 04 21:10:57 2001 +0200
     3.3 @@ -761,8 +761,8 @@
     3.4  
     3.5  Any goal statement causes some term abbreviations (such as $\Var{thesis}$,
     3.6  $\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}.
     3.7 -Furthermore, the local context of a (non-atomic) goal is provided via the case
     3.8 -name $antecedent$\indexisarcase{antecedent}, see also \S\ref{sec:cases}.
     3.9 +Furthermore, the local context of a (non-atomic) goal is provided via the
    3.10 +$rule_context$\indexisarcase{rule-context} case, see also \S\ref{sec:cases}.
    3.11  
    3.12  \medskip
    3.13  
     4.1 --- a/src/HOL/Induct/Term.thy	Tue Sep 04 17:31:18 2001 +0200
     4.2 +++ b/src/HOL/Induct/Term.thy	Tue Sep 04 21:10:57 2001 +0200
     4.3 @@ -48,11 +48,11 @@
     4.4      (!!f ts. list_all P ts ==> P (App f ts))
     4.5    ==> P t"
     4.6  proof -
     4.7 -  case antecedent
     4.8 +  case rule_context
     4.9    have "P t \<and> list_all P ts"
    4.10      apply (induct t and ts rule: term.induct)
    4.11 -       apply (rule antecedent)
    4.12 -      apply (rule antecedent)
    4.13 +       apply (rule rule_context)
    4.14 +      apply (rule rule_context)
    4.15        apply assumption
    4.16       apply simp_all
    4.17      done
     5.1 --- a/src/HOL/Lambda/ListApplication.thy	Tue Sep 04 17:31:18 2001 +0200
     5.2 +++ b/src/HOL/Lambda/ListApplication.thy	Tue Sep 04 21:10:57 2001 +0200
     5.3 @@ -108,7 +108,7 @@
     5.4      !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
     5.5    |] ==> \<forall>t. size t = n --> P t"
     5.6  proof -
     5.7 -  case antecedent
     5.8 +  case rule_context
     5.9    show ?thesis
    5.10     apply (induct_tac n rule: nat_less_induct)
    5.11     apply (rule allI)
    5.12 @@ -150,7 +150,7 @@
    5.13      !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
    5.14    |] ==> P t"
    5.15  proof -
    5.16 -  case antecedent
    5.17 +  case rule_context
    5.18    show ?thesis
    5.19      apply (rule_tac t = t in lem)
    5.20        prefer 3
     6.1 --- a/src/HOL/Lambda/ListBeta.thy	Tue Sep 04 17:31:18 2001 +0200
     6.2 +++ b/src/HOL/Lambda/ListBeta.thy	Tue Sep 04 21:10:57 2001 +0200
     6.3 @@ -76,7 +76,7 @@
     6.4    ==> R"
     6.5  proof -
     6.6    assume major: "r $$ rs -> s"
     6.7 -  case antecedent
     6.8 +  case rule_context
     6.9    show ?thesis
    6.10      apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
    6.11      apply (assumption | rule refl | erule prems exE conjE impE disjE)+
     7.1 --- a/src/HOL/Library/Multiset.thy	Tue Sep 04 17:31:18 2001 +0200
     7.2 +++ b/src/HOL/Library/Multiset.thy	Tue Sep 04 21:10:57 2001 +0200
     7.3 @@ -331,8 +331,8 @@
     7.4    "P (\<lambda>a. 0) ==> (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1')))
     7.5      ==> \<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
     7.6  proof -
     7.7 -  case antecedent
     7.8 -  note prems = this [unfolded multiset_def]
     7.9 +  case rule_context
    7.10 +  note premises = this [unfolded multiset_def]
    7.11    show ?thesis
    7.12      apply (unfold multiset_def)
    7.13      apply (induct_tac n)
    7.14 @@ -340,7 +340,7 @@
    7.15       apply clarify
    7.16       apply (subgoal_tac "f = (\<lambda>a.0)")
    7.17        apply simp
    7.18 -      apply (rule prems)
    7.19 +      apply (rule premises)
    7.20       apply (rule ext)
    7.21       apply force
    7.22      apply clarify
    7.23 @@ -358,7 +358,7 @@
    7.24       prefer 2
    7.25       apply (rule ext)
    7.26       apply (simp (no_asm_simp))
    7.27 -     apply (erule ssubst, rule prems)
    7.28 +     apply (erule ssubst, rule premises)
    7.29       apply blast
    7.30      apply (erule allE, erule impE, erule_tac [2] mp)
    7.31       apply blast
     8.1 --- a/src/HOL/Library/Quotient.thy	Tue Sep 04 17:31:18 2001 +0200
     8.2 +++ b/src/HOL/Library/Quotient.thy	Tue Sep 04 21:10:57 2001 +0200
     8.3 @@ -203,7 +203,7 @@
     8.4      (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
     8.5      f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
     8.6  proof -
     8.7 -  case antecedent from this TrueI
     8.8 +  case rule_context from this TrueI
     8.9    show ?thesis by (rule quot_cond_function)
    8.10  qed
    8.11  
     9.1 --- a/src/HOL/Library/Rational_Numbers.thy	Tue Sep 04 17:31:18 2001 +0200
     9.2 +++ b/src/HOL/Library/Rational_Numbers.thy	Tue Sep 04 21:10:57 2001 +0200
     9.3 @@ -360,7 +360,7 @@
     9.4        g (fract a b) (fract c d) = g (fract a' b') (fract c' d')) ==>
     9.5      f (Fract a b) (Fract c d) = g (fract a b) (fract c d)"
     9.6  proof -
     9.7 -  case antecedent from this TrueI
     9.8 +  case rule_context from this TrueI
     9.9    show ?thesis by (rule rat_cond_function)
    9.10  qed
    9.11  
    10.1 --- a/src/HOL/Library/While_Combinator.thy	Tue Sep 04 17:31:18 2001 +0200
    10.2 +++ b/src/HOL/Library/While_Combinator.thy	Tue Sep 04 21:10:57 2001 +0200
    10.3 @@ -79,14 +79,14 @@
    10.4        wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
    10.5      P s --> Q (while b c s)"
    10.6  proof -
    10.7 -  case antecedent
    10.8 +  case rule_context
    10.9    assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
   10.10    show ?thesis
   10.11      apply (induct s rule: wf [THEN wf_induct])
   10.12      apply simp
   10.13      apply clarify
   10.14      apply (subst while_unfold)
   10.15 -    apply (simp add: antecedent)
   10.16 +    apply (simp add: rule_context)
   10.17      done
   10.18  qed
   10.19  
    11.1 --- a/src/HOL/MicroJava/BV/Err.thy	Tue Sep 04 17:31:18 2001 +0200
    11.2 +++ b/src/HOL/MicroJava/BV/Err.thy	Tue Sep 04 21:10:57 2001 +0200
    11.3 @@ -257,7 +257,7 @@
    11.4      [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |] 
    11.5      ==> x <=_r z \<and> y <=_r z"
    11.6      by (rule plus_le_conv [THEN iffD1])
    11.7 -  case antecedent
    11.8 +  case rule_context
    11.9    thus ?thesis
   11.10    apply (rule_tac iffI)
   11.11     apply clarify
    12.1 --- a/src/HOL/MicroJava/BV/Kildall.thy	Tue Sep 04 17:31:18 2001 +0200
    12.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Tue Sep 04 21:10:57 2001 +0200
    12.3 @@ -165,7 +165,7 @@
    12.4      done
    12.5    } note this [dest]
    12.6    
    12.7 -  case antecedent
    12.8 +  case rule_context
    12.9    thus ?thesis by blast
   12.10  qed
   12.11  
    13.1 --- a/src/HOL/MicroJava/BV/Product.thy	Tue Sep 04 17:31:18 2001 +0200
    13.2 +++ b/src/HOL/MicroJava/BV/Product.thy	Tue Sep 04 21:10:57 2001 +0200
    13.3 @@ -79,7 +79,7 @@
    13.4      "!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
    13.5                   OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z"
    13.6      by (rule plus_le_conv [THEN iffD1])
    13.7 -  case antecedent
    13.8 +  case rule_context
    13.9    thus ?thesis
   13.10    apply (rule_tac iffI)
   13.11     apply clarify
    14.1 --- a/src/HOL/NumberTheory/BijectionRel.thy	Tue Sep 04 17:31:18 2001 +0200
    14.2 +++ b/src/HOL/NumberTheory/BijectionRel.thy	Tue Sep 04 21:10:57 2001 +0200
    14.3 @@ -67,13 +67,13 @@
    14.4      (!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F))
    14.5    ==> P F"
    14.6  proof -
    14.7 -  case antecedent
    14.8 +  case rule_context
    14.9    assume major: "finite F"
   14.10      and subs: "F \<subseteq> A"
   14.11    show ?thesis
   14.12      apply (rule subs [THEN rev_mp])
   14.13      apply (rule major [THEN finite_induct])
   14.14 -     apply (blast intro: antecedent)+
   14.15 +     apply (blast intro: rule_context)+
   14.16      done
   14.17  qed
   14.18  
    15.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Tue Sep 04 17:31:18 2001 +0200
    15.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Tue Sep 04 21:10:57 2001 +0200
    15.3 @@ -71,14 +71,14 @@
    15.4        ==> P (BnorRset(a,m)) a m)
    15.5      ==> P (BnorRset(u,v)) u v"
    15.6  proof -
    15.7 -  case antecedent
    15.8 +  case rule_context
    15.9    show ?thesis
   15.10      apply (rule BnorRset.induct)
   15.11      apply safe
   15.12       apply (case_tac [2] "#0 < a")
   15.13 -      apply (rule_tac [2] antecedent)
   15.14 +      apply (rule_tac [2] rule_context)
   15.15         apply simp_all
   15.16 -     apply (simp_all add: BnorRset.simps antecedent)
   15.17 +     apply (simp_all add: BnorRset.simps rule_context)
   15.18    done
   15.19  qed
   15.20  
    16.1 --- a/src/HOL/NumberTheory/IntFact.thy	Tue Sep 04 17:31:18 2001 +0200
    16.2 +++ b/src/HOL/NumberTheory/IntFact.thy	Tue Sep 04 21:10:57 2001 +0200
    16.3 @@ -58,14 +58,14 @@
    16.4        ==> P (d22set a) a)
    16.5      ==> P (d22set u) u"
    16.6  proof -
    16.7 -  case antecedent
    16.8 +  case rule_context
    16.9    show ?thesis
   16.10      apply (rule d22set.induct)
   16.11      apply safe
   16.12       apply (case_tac [2] "#1 < a")
   16.13 -      apply (rule_tac [2] antecedent)
   16.14 +      apply (rule_tac [2] rule_context)
   16.15         apply (simp_all (no_asm_simp))
   16.16 -     apply (simp_all (no_asm_simp) add: d22set.simps antecedent)
   16.17 +     apply (simp_all (no_asm_simp) add: d22set.simps rule_context)
   16.18      done
   16.19  qed
   16.20  
    17.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Tue Sep 04 17:31:18 2001 +0200
    17.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Tue Sep 04 21:10:57 2001 +0200
    17.3 @@ -184,14 +184,14 @@
    17.4        ==> P (wset (a, p)) a p)
    17.5      ==> P (wset (u, v)) u v"
    17.6  proof -
    17.7 -  case antecedent
    17.8 +  case rule_context
    17.9    show ?thesis
   17.10      apply (rule wset.induct)
   17.11      apply safe
   17.12       apply (case_tac [2] "#1 < a")
   17.13 -      apply (rule_tac [2] antecedent)
   17.14 +      apply (rule_tac [2] rule_context)
   17.15          apply simp_all
   17.16 -      apply (simp_all add: wset.simps antecedent)
   17.17 +      apply (simp_all add: wset.simps rule_context)
   17.18      done
   17.19  qed
   17.20  
    18.1 --- a/src/HOL/Unix/Unix.thy	Tue Sep 04 17:31:18 2001 +0200
    18.2 +++ b/src/HOL/Unix/Unix.thy	Tue Sep 04 21:10:57 2001 +0200
    18.3 @@ -618,7 +618,7 @@
    18.4    "root =xs\<Rightarrow> root' \<Longrightarrow> \<exists>att dir. root = Env att dir
    18.5      \<Longrightarrow> \<exists>att dir. root' = Env att dir"
    18.6  proof -
    18.7 -  case antecedent
    18.8 +  case rule_context
    18.9    with transition_type_safe show ?thesis
   18.10    proof (rule transitions_invariant)
   18.11      show "\<forall>x \<in> set xs. True" by blast
   18.12 @@ -957,7 +957,7 @@
   18.13  lemma init_invariant: "init users =bogus\<Rightarrow> root \<Longrightarrow> invariant root bogus_path"
   18.14  proof -
   18.15    note eval = "setup" access_def init_def
   18.16 -  case antecedent thus ?thesis
   18.17 +  case rule_context thus ?thesis
   18.18      apply (unfold bogus_def bogus_path_def)
   18.19      apply (drule transitions_consD, rule transition.intros,
   18.20        (force simp add: eval)+, (simp add: eval)?)+
   18.21 @@ -1126,7 +1126,7 @@
   18.22    \<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user1) \<and>
   18.23        can_exec root (xs @ [Rmdir user1 [user1, name1]]))"
   18.24  proof -
   18.25 -  case antecedent
   18.26 +  case rule_context
   18.27    with cannot_rmdir init_invariant preserve_invariant
   18.28    show ?thesis by (rule general_procedure)
   18.29  qed
    19.1 --- a/src/Pure/Isar/proof.ML	Tue Sep 04 17:31:18 2001 +0200
    19.2 +++ b/src/Pure/Isar/proof.ML	Tue Sep 04 21:10:57 2001 +0200
    19.3 @@ -580,7 +580,7 @@
    19.4  
    19.5  (* setup goals *)
    19.6  
    19.7 -val antN = "antecedent";
    19.8 +val rule_contextN = "rule_context";
    19.9  
   19.10  fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
   19.11    let
   19.12 @@ -604,7 +604,7 @@
   19.13        commas (map (Sign.string_of_term (sign_of state)) vars));
   19.14      state'
   19.15      |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds))
   19.16 -    |> map_context (ProofContext.add_cases (RuleCases.make true goal [antN]))
   19.17 +    |> map_context (ProofContext.add_cases (RuleCases.make true goal [rule_contextN]))
   19.18      |> auto_bind_goal prop
   19.19      |> (if is_chain state then use_facts else reset_facts)
   19.20      |> new_block