--- a/NEWS Sun Nov 10 10:02:34 2013 +0100
+++ b/NEWS Sun Nov 10 15:05:06 2013 +0100
@@ -6,6 +6,9 @@
*** HOL ***
+* Qualified constant names Wellfounded.acc, Wellfounded.accp.
+INCOMPATIBILITY.
+
* Fact generalization and consolidation:
neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
INCOMPATIBILITY.
--- a/src/Doc/Functions/Functions.thy Sun Nov 10 10:02:34 2013 +0100
+++ b/src/Doc/Functions/Functions.thy Sun Nov 10 15:05:06 2013 +0100
@@ -1003,13 +1003,13 @@
recursive calls. In general, there is one introduction rule for each
recursive call.
- The predicate @{term "accp findzero_rel"} is the accessible part of
+ The predicate @{term "Wellfounded.accp findzero_rel"} is the accessible part of
that relation. An argument belongs to the accessible part, if it can
be reached in a finite number of steps (cf.~its definition in @{text
"Wellfounded.thy"}).
Since the domain predicate is just an abbreviation, you can use
- lemmas for @{const accp} and @{const findzero_rel} directly. Some
+ lemmas for @{const Wellfounded.accp} and @{const findzero_rel} directly. Some
lemmas which are occasionally useful are @{thm [source] accpI}, @{thm [source]
accp_downward}, and of course the introduction and elimination rules
for the recursion relation @{thm [source] "findzero_rel.intros"} and @{thm
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Sun Nov 10 10:02:34 2013 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Sun Nov 10 15:05:06 2013 +0100
@@ -26,7 +26,7 @@
"pred_of_set = pred_of_set" ..
lemma [code, code del]:
- "acc = acc" ..
+ "Wellfounded.acc = Wellfounded.acc" ..
lemma [code, code del]:
"Cardinality.card' = Cardinality.card'" ..
--- a/src/HOL/Enum.thy Sun Nov 10 10:02:34 2013 +0100
+++ b/src/HOL/Enum.thy Sun Nov 10 15:05:06 2013 +0100
@@ -178,13 +178,9 @@
lemma [code]:
fixes xs :: "('a::finite \<times> 'a) list"
- shows "acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
+ shows "Wellfounded.acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
by (simp add: card_UNIV_def acc_bacc_eq)
-lemma [code]:
- "accp r = (\<lambda>x. x \<in> acc {(x, y). r x y})"
- by (simp add: acc_def)
-
subsection {* Default instances for @{class enum} *}
--- a/src/HOL/Hilbert_Choice.thy Sun Nov 10 10:02:34 2013 +0100
+++ b/src/HOL/Hilbert_Choice.thy Sun Nov 10 15:05:06 2013 +0100
@@ -741,7 +741,7 @@
| "bacc r (Suc n) = (bacc r n \<union> {x. \<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r n})"
lemma bacc_subseteq_acc:
- "bacc r n \<subseteq> acc r"
+ "bacc r n \<subseteq> Wellfounded.acc r"
by (induct n) (auto intro: acc.intros)
lemma bacc_mono:
@@ -761,10 +761,10 @@
lemma acc_subseteq_bacc:
assumes "finite r"
- shows "acc r \<subseteq> (\<Union>n. bacc r n)"
+ shows "Wellfounded.acc r \<subseteq> (\<Union>n. bacc r n)"
proof
fix x
- assume "x : acc r"
+ assume "x : Wellfounded.acc r"
then have "\<exists> n. x : bacc r n"
proof (induct x arbitrary: rule: acc.induct)
case (accI x)
@@ -788,7 +788,7 @@
lemma acc_bacc_eq:
fixes A :: "('a :: finite \<times> 'a) set"
assumes "finite A"
- shows "acc A = bacc A (card (UNIV :: 'a set))"
+ shows "Wellfounded.acc A = bacc A (card (UNIV :: 'a set))"
using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy Sun Nov 10 10:02:34 2013 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy Sun Nov 10 15:05:06 2013 +0100
@@ -135,8 +135,6 @@
subsubsection "Ascending Chain Condition"
-hide_const (open) acc
-
abbreviation "strict r == r \<inter> -(r^-1)"
abbreviation "acc r == wf((strict r)^-1)"
--- a/src/HOL/Library/Multiset.thy Sun Nov 10 10:02:34 2013 +0100
+++ b/src/HOL/Library/Multiset.thy Sun Nov 10 15:05:06 2013 +0100
@@ -1533,10 +1533,10 @@
qed
qed
-lemma all_accessible: "wf r ==> \<forall>M. M \<in> acc (mult1 r)"
+lemma all_accessible: "wf r ==> \<forall>M. M \<in> Wellfounded.acc (mult1 r)"
proof
let ?R = "mult1 r"
- let ?W = "acc ?R"
+ let ?W = "Wellfounded.acc ?R"
{
fix M M0 a
assume M0: "M0 \<in> ?W"
--- a/src/HOL/List.thy Sun Nov 10 10:02:34 2013 +0100
+++ b/src/HOL/List.thy Sun Nov 10 15:05:06 2013 +0100
@@ -5514,15 +5514,15 @@
text{* Accessible part and wellfoundedness: *}
lemma Cons_acc_listrel1I [intro!]:
- "x \<in> acc r \<Longrightarrow> xs \<in> acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> acc (listrel1 r)"
-apply (induct arbitrary: xs set: acc)
+ "x \<in> Wellfounded.acc r \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> Wellfounded.acc (listrel1 r)"
+apply (induct arbitrary: xs set: Wellfounded.acc)
apply (erule thin_rl)
apply (erule acc_induct)
apply (rule accI)
apply (blast)
done
-lemma lists_accD: "xs \<in> lists (acc r) \<Longrightarrow> xs \<in> acc (listrel1 r)"
+lemma lists_accD: "xs \<in> lists (Wellfounded.acc r) \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r)"
apply (induct set: lists)
apply (rule accI)
apply simp
@@ -5530,8 +5530,8 @@
apply (fast dest: acc_downward)
done
-lemma lists_accI: "xs \<in> acc (listrel1 r) \<Longrightarrow> xs \<in> lists (acc r)"
-apply (induct set: acc)
+lemma lists_accI: "xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> xs \<in> lists (Wellfounded.acc r)"
+apply (induct set: Wellfounded.acc)
apply clarify
apply (rule accI)
apply (fastforce dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
--- a/src/HOL/Proofs/Lambda/ListOrder.thy Sun Nov 10 10:02:34 2013 +0100
+++ b/src/HOL/Proofs/Lambda/ListOrder.thy Sun Nov 10 15:05:06 2013 +0100
@@ -89,15 +89,15 @@
done
lemma Cons_acc_step1I [intro!]:
- "accp r x ==> accp (step1 r) xs \<Longrightarrow> accp (step1 r) (x # xs)"
- apply (induct arbitrary: xs set: accp)
+ "Wellfounded.accp r x ==> Wellfounded.accp (step1 r) xs \<Longrightarrow> Wellfounded.accp (step1 r) (x # xs)"
+ apply (induct arbitrary: xs set: Wellfounded.accp)
apply (erule thin_rl)
apply (erule accp_induct)
apply (rule accp.accI)
apply blast
done
-lemma lists_accD: "listsp (accp r) xs ==> accp (step1 r) xs"
+lemma lists_accD: "listsp (Wellfounded.accp r) xs ==> Wellfounded.accp (step1 r) xs"
apply (induct set: listsp)
apply (rule accp.accI)
apply simp
@@ -113,8 +113,8 @@
apply force
done
-lemma lists_accI: "accp (step1 r) xs ==> listsp (accp r) xs"
- apply (induct set: accp)
+lemma lists_accI: "Wellfounded.accp (step1 r) xs ==> listsp (Wellfounded.accp r) xs"
+ apply (induct set: Wellfounded.accp)
apply clarify
apply (rule accp.accI)
apply (drule_tac r=r in ex_step1I, assumption)
--- a/src/HOL/Tools/Function/function_common.ML Sun Nov 10 10:02:34 2013 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Sun Nov 10 15:05:06 2013 +0100
@@ -119,7 +119,7 @@
fun PROFILE msg = if !profile then timeap_msg msg else I
-val acc_const_name = @{const_name accp}
+val acc_const_name = @{const_name Wellfounded.accp}
fun mk_acc domT R =
Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R
--- a/src/HOL/Wellfounded.thy Sun Nov 10 10:02:34 2013 +0100
+++ b/src/HOL/Wellfounded.thy Sun Nov 10 15:05:06 2013 +0100
@@ -482,6 +482,11 @@
lemmas accpI = accp.accI
+lemma accp_eq_acc [code]:
+ "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})"
+ by (simp add: acc_def)
+
+
text {* Induction rules *}
theorem accp_induct:
@@ -855,4 +860,7 @@
declare "prod.size" [no_atp]
+
+hide_const (open) acc accp
+
end