1.1 --- a/NEWS	Sun Nov 10 10:02:34 2013 +0100
     1.2 +++ b/NEWS	Sun Nov 10 15:05:06 2013 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Qualified constant names Wellfounded.acc, Wellfounded.accp.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * Fact generalization and consolidation:
    1.11      neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
    1.12  INCOMPATIBILITY.

     2.1 --- a/src/Doc/Functions/Functions.thy	Sun Nov 10 10:02:34 2013 +0100
     2.2 +++ b/src/Doc/Functions/Functions.thy	Sun Nov 10 15:05:06 2013 +0100
     2.3 @@ -1003,13 +1003,13 @@
     2.4    recursive calls. In general, there is one introduction rule for each
     2.5    recursive call.
     2.6  
     2.7 -  The predicate @{term "accp findzero_rel"} is the accessible part of
     2.8 +  The predicate @{term "Wellfounded.accp findzero_rel"} is the accessible part of
     2.9    that relation. An argument belongs to the accessible part, if it can
    2.10    be reached in a finite number of steps (cf.~its definition in @{text
    2.11    "Wellfounded.thy"}).
    2.12  
    2.13    Since the domain predicate is just an abbreviation, you can use
    2.14 -  lemmas for @{const accp} and @{const findzero_rel} directly. Some
    2.15 +  lemmas for @{const Wellfounded.accp} and @{const findzero_rel} directly. Some
    2.16    lemmas which are occasionally useful are @{thm [source] accpI}, @{thm [source]
    2.17    accp_downward}, and of course the introduction and elimination rules
    2.18    for the recursion relation @{thm [source] "findzero_rel.intros"} and @{thm

     3.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sun Nov 10 10:02:34 2013 +0100
     3.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sun Nov 10 15:05:06 2013 +0100
     3.3 @@ -26,7 +26,7 @@
     3.4    "pred_of_set = pred_of_set" ..
     3.5  
     3.6  lemma [code, code del]:
     3.7 -  "acc = acc" ..
     3.8 +  "Wellfounded.acc = Wellfounded.acc" ..
     3.9  
    3.10  lemma [code, code del]:
    3.11    "Cardinality.card' = Cardinality.card'" ..

     4.1 --- a/src/HOL/Enum.thy	Sun Nov 10 10:02:34 2013 +0100
     4.2 +++ b/src/HOL/Enum.thy	Sun Nov 10 15:05:06 2013 +0100
     4.3 @@ -178,13 +178,9 @@
     4.4  
     4.5  lemma [code]:
     4.6    fixes xs :: "('a::finite \<times> 'a) list"
     4.7 -  shows "acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
     4.8 +  shows "Wellfounded.acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
     4.9    by (simp add: card_UNIV_def acc_bacc_eq)
    4.10  
    4.11 -lemma [code]:
    4.12 -  "accp r = (\<lambda>x. x \<in> acc {(x, y). r x y})"
    4.13 -  by (simp add: acc_def)
    4.14 -
    4.15  
    4.16  subsection {* Default instances for @{class enum} *}
    4.17  

     5.1 --- a/src/HOL/Hilbert_Choice.thy	Sun Nov 10 10:02:34 2013 +0100
     5.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Nov 10 15:05:06 2013 +0100
     5.3 @@ -741,7 +741,7 @@
     5.4  | "bacc r (Suc n) = (bacc r n \<union> {x. \<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r n})"
     5.5  
     5.6  lemma bacc_subseteq_acc:
     5.7 -  "bacc r n \<subseteq> acc r"
     5.8 +  "bacc r n \<subseteq> Wellfounded.acc r"
     5.9    by (induct n) (auto intro: acc.intros)
    5.10  
    5.11  lemma bacc_mono:
    5.12 @@ -761,10 +761,10 @@
    5.13  
    5.14  lemma acc_subseteq_bacc:
    5.15    assumes "finite r"
    5.16 -  shows "acc r \<subseteq> (\<Union>n. bacc r n)"
    5.17 +  shows "Wellfounded.acc r \<subseteq> (\<Union>n. bacc r n)"
    5.18  proof
    5.19    fix x
    5.20 -  assume "x : acc r"
    5.21 +  assume "x : Wellfounded.acc r"
    5.22    then have "\<exists> n. x : bacc r n"
    5.23    proof (induct x arbitrary: rule: acc.induct)
    5.24      case (accI x)
    5.25 @@ -788,7 +788,7 @@
    5.26  lemma acc_bacc_eq:
    5.27    fixes A :: "('a :: finite \<times> 'a) set"
    5.28    assumes "finite A"
    5.29 -  shows "acc A = bacc A (card (UNIV :: 'a set))"
    5.30 +  shows "Wellfounded.acc A = bacc A (card (UNIV :: 'a set))"
    5.31    using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
    5.32  
    5.33  

     6.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy	Sun Nov 10 10:02:34 2013 +0100
     6.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy	Sun Nov 10 15:05:06 2013 +0100
     6.3 @@ -135,8 +135,6 @@
     6.4  
     6.5  subsubsection "Ascending Chain Condition"
     6.6  
     6.7 -hide_const (open) acc
     6.8 -
     6.9  abbreviation "strict r == r \<inter> -(r^-1)"
    6.10  abbreviation "acc r == wf((strict r)^-1)"
    6.11  

     7.1 --- a/src/HOL/Library/Multiset.thy	Sun Nov 10 10:02:34 2013 +0100
     7.2 +++ b/src/HOL/Library/Multiset.thy	Sun Nov 10 15:05:06 2013 +0100
     7.3 @@ -1533,10 +1533,10 @@
     7.4    qed
     7.5  qed
     7.6  
     7.7 -lemma all_accessible: "wf r ==> \<forall>M. M \<in> acc (mult1 r)"
     7.8 +lemma all_accessible: "wf r ==> \<forall>M. M \<in> Wellfounded.acc (mult1 r)"
     7.9  proof
    7.10    let ?R = "mult1 r"
    7.11 -  let ?W = "acc ?R"
    7.12 +  let ?W = "Wellfounded.acc ?R"
    7.13    {
    7.14      fix M M0 a
    7.15      assume M0: "M0 \<in> ?W"

     8.1 --- a/src/HOL/List.thy	Sun Nov 10 10:02:34 2013 +0100
     8.2 +++ b/src/HOL/List.thy	Sun Nov 10 15:05:06 2013 +0100
     8.3 @@ -5514,15 +5514,15 @@
     8.4  text{* Accessible part and wellfoundedness: *}
     8.5  
     8.6  lemma Cons_acc_listrel1I [intro!]:
     8.7 -  "x \<in> acc r \<Longrightarrow> xs \<in> acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> acc (listrel1 r)"
     8.8 -apply (induct arbitrary: xs set: acc)
     8.9 +  "x \<in> Wellfounded.acc r \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> Wellfounded.acc (listrel1 r)"
    8.10 +apply (induct arbitrary: xs set: Wellfounded.acc)
    8.11  apply (erule thin_rl)
    8.12  apply (erule acc_induct)
    8.13  apply (rule accI)
    8.14  apply (blast)
    8.15  done
    8.16  
    8.17 -lemma lists_accD: "xs \<in> lists (acc r) \<Longrightarrow> xs \<in> acc (listrel1 r)"
    8.18 +lemma lists_accD: "xs \<in> lists (Wellfounded.acc r) \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r)"
    8.19  apply (induct set: lists)
    8.20   apply (rule accI)
    8.21   apply simp
    8.22 @@ -5530,8 +5530,8 @@
    8.23  apply (fast dest: acc_downward)
    8.24  done
    8.25  
    8.26 -lemma lists_accI: "xs \<in> acc (listrel1 r) \<Longrightarrow> xs \<in> lists (acc r)"
    8.27 -apply (induct set: acc)
    8.28 +lemma lists_accI: "xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> xs \<in> lists (Wellfounded.acc r)"
    8.29 +apply (induct set: Wellfounded.acc)
    8.30  apply clarify
    8.31  apply (rule accI)
    8.32  apply (fastforce dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)

     9.1 --- a/src/HOL/Proofs/Lambda/ListOrder.thy	Sun Nov 10 10:02:34 2013 +0100
     9.2 +++ b/src/HOL/Proofs/Lambda/ListOrder.thy	Sun Nov 10 15:05:06 2013 +0100
     9.3 @@ -89,15 +89,15 @@
     9.4    done
     9.5  
     9.6  lemma Cons_acc_step1I [intro!]:
     9.7 -    "accp r x ==> accp (step1 r) xs \<Longrightarrow> accp (step1 r) (x # xs)"
     9.8 -  apply (induct arbitrary: xs set: accp)
     9.9 +    "Wellfounded.accp r x ==> Wellfounded.accp (step1 r) xs \<Longrightarrow> Wellfounded.accp (step1 r) (x # xs)"
    9.10 +  apply (induct arbitrary: xs set: Wellfounded.accp)
    9.11    apply (erule thin_rl)
    9.12    apply (erule accp_induct)
    9.13    apply (rule accp.accI)
    9.14    apply blast
    9.15    done
    9.16  
    9.17 -lemma lists_accD: "listsp (accp r) xs ==> accp (step1 r) xs"
    9.18 +lemma lists_accD: "listsp (Wellfounded.accp r) xs ==> Wellfounded.accp (step1 r) xs"
    9.19    apply (induct set: listsp)
    9.20     apply (rule accp.accI)
    9.21     apply simp
    9.22 @@ -113,8 +113,8 @@
    9.23    apply force
    9.24    done
    9.25  
    9.26 -lemma lists_accI: "accp (step1 r) xs ==> listsp (accp r) xs"
    9.27 -  apply (induct set: accp)
    9.28 +lemma lists_accI: "Wellfounded.accp (step1 r) xs ==> listsp (Wellfounded.accp r) xs"
    9.29 +  apply (induct set: Wellfounded.accp)
    9.30    apply clarify
    9.31    apply (rule accp.accI)
    9.32    apply (drule_tac r=r in ex_step1I, assumption)

    10.1 --- a/src/HOL/Tools/Function/function_common.ML	Sun Nov 10 10:02:34 2013 +0100
    10.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sun Nov 10 15:05:06 2013 +0100
    10.3 @@ -119,7 +119,7 @@
    10.4  
    10.5  fun PROFILE msg = if !profile then timeap_msg msg else I
    10.6  
    10.7 -val acc_const_name = @{const_name accp}
    10.8 +val acc_const_name = @{const_name Wellfounded.accp}
    10.9  fun mk_acc domT R =
   10.10    Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
   10.11  

    11.1 --- a/src/HOL/Wellfounded.thy	Sun Nov 10 10:02:34 2013 +0100
    11.2 +++ b/src/HOL/Wellfounded.thy	Sun Nov 10 15:05:06 2013 +0100
    11.3 @@ -482,6 +482,11 @@
    11.4  
    11.5  lemmas accpI = accp.accI
    11.6  
    11.7 +lemma accp_eq_acc [code]:
    11.8 +  "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})"
    11.9 +  by (simp add: acc_def)
   11.10 +
   11.11 +
   11.12  text {* Induction rules *}
   11.13  
   11.14  theorem accp_induct:
   11.15 @@ -855,4 +860,7 @@
   11.16  
   11.17  declare "prod.size" [no_atp]
   11.18  
   11.19 +
   11.20 +hide_const (open) acc accp
   11.21 +
   11.22  end