# HG changeset patch # User haftmann # Date 1384092306 -3600 # Node ID 45a5523d4a63b9b7e34bdb288fcc8d57bc06cdfa # Parent 98826791a58869247d21f8f9134322e4dc4498c3 qualifed popular user space names diff -r 98826791a588 -r 45a5523d4a63 NEWS --- 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. diff -r 98826791a588 -r 45a5523d4a63 src/Doc/Functions/Functions.thy --- 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 diff -r 98826791a588 -r 45a5523d4a63 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy --- 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'" .. diff -r 98826791a588 -r 45a5523d4a63 src/HOL/Enum.thy --- 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 \ '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 = (\x. x \ acc {(x, y). r x y})" - by (simp add: acc_def) - subsection {* Default instances for @{class enum} *} diff -r 98826791a588 -r 45a5523d4a63 src/HOL/Hilbert_Choice.thy --- 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 \ {x. \y. (y, x) \ r \ y \ bacc r n})" lemma bacc_subseteq_acc: - "bacc r n \ acc r" + "bacc r n \ 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 \ (\n. bacc r n)" + shows "Wellfounded.acc r \ (\n. bacc r n)" proof fix x - assume "x : acc r" + assume "x : Wellfounded.acc r" then have "\ 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 \ '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) diff -r 98826791a588 -r 45a5523d4a63 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy --- 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 \ -(r^-1)" abbreviation "acc r == wf((strict r)^-1)" diff -r 98826791a588 -r 45a5523d4a63 src/HOL/Library/Multiset.thy --- 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 ==> \M. M \ acc (mult1 r)" +lemma all_accessible: "wf r ==> \M. M \ 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 \ ?W" diff -r 98826791a588 -r 45a5523d4a63 src/HOL/List.thy --- 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 \ acc r \ xs \ acc (listrel1 r) \ (x # xs) \ acc (listrel1 r)" -apply (induct arbitrary: xs set: acc) + "x \ Wellfounded.acc r \ xs \ Wellfounded.acc (listrel1 r) \ (x # xs) \ 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 \ lists (acc r) \ xs \ acc (listrel1 r)" +lemma lists_accD: "xs \ lists (Wellfounded.acc r) \ xs \ 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 \ acc (listrel1 r) \ xs \ lists (acc r)" -apply (induct set: acc) +lemma lists_accI: "xs \ Wellfounded.acc (listrel1 r) \ xs \ 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) diff -r 98826791a588 -r 45a5523d4a63 src/HOL/Proofs/Lambda/ListOrder.thy --- 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 \ accp (step1 r) (x # xs)" - apply (induct arbitrary: xs set: accp) + "Wellfounded.accp r x ==> Wellfounded.accp (step1 r) xs \ 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) diff -r 98826791a588 -r 45a5523d4a63 src/HOL/Tools/Function/function_common.ML --- 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 diff -r 98826791a588 -r 45a5523d4a63 src/HOL/Wellfounded.thy --- 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 = (\x. x \ 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