# HG changeset patch
# User desharna
# Date 1718021395 -7200
# Node ID b10f7c981df6c1ed52c3a841f721ef8d60ea7646
# Parent  31b9dfbe534c85184833a8233f4d181050dde0bb
renamed theorems

diff -r 31b9dfbe534c -r b10f7c981df6 NEWS
--- a/NEWS	Mon Jun 10 13:44:46 2024 +0200
+++ b/NEWS	Mon Jun 10 14:09:55 2024 +0200
@@ -11,9 +11,22 @@
   - Renamed lemmas. Minor INCOMPATIBILITY.
       accp_wfPD ~> accp_wfpD
       accp_wfPI ~> accp_wfpI
+      wfPUNIVI ~> wfpUNIVI
+      wfP_SUP ~> wfp_SUP
       wfP_accp_iff ~> wfp_accp_iff
+      wfP_acyclicP ~> wfp_acyclicP
+      wfP_def ~> wfp_def
+      wfP_empty ~> wfp_empty
+      wfP_eq_minimal ~> wfp_eq_minimal
       wfP_if_convertible_to_nat ~> wfp_if_convertible_to_nat
       wfP_if_convertible_to_wfP ~> wfp_if_convertible_to_wfp
+      wfP_imp_asymp ~> wfp_imp_asymp
+      wfP_imp_irreflp ~> wfp_imp_irreflp
+      wfP_induct ~> wfp_induct
+      wfP_induct_rule ~> wfp_induct_rule
+      wfP_subset ~> wfp_subset
+      wfP_trancl ~> wfp_tranclp
+      wfP_wf_eq ~> wfp_wf_eq
       wf_acc_iff ~> wf_iff_acc
 
 
diff -r 31b9dfbe534c -r b10f7c981df6 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Mon Jun 10 13:44:46 2024 +0200
+++ b/src/HOL/Fun_Def.thy	Mon Jun 10 14:09:55 2024 +0200
@@ -68,8 +68,8 @@
 
 definition in_rel_def[simp]: "in_rel R x y \<equiv> (x, y) \<in> R"
 
-lemma wf_in_rel: "wf R \<Longrightarrow> wfP (in_rel R)"
-  by (simp add: wfP_def)
+lemma wf_in_rel: "wf R \<Longrightarrow> wfp (in_rel R)"
+  by (simp add: wfp_def)
 
 ML_file \<open>Tools/Function/function_core.ML\<close>
 ML_file \<open>Tools/Function/mutual.ML\<close>
diff -r 31b9dfbe534c -r b10f7c981df6 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Jun 10 13:44:46 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Jun 10 14:09:55 2024 +0200
@@ -1548,7 +1548,7 @@
 text \<open>Well-foundedness of strict subset relation\<close>
 
 lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
-  using mset_subset_size wfP_def wfp_if_convertible_to_nat by blast
+  using mset_subset_size wfp_def wfp_if_convertible_to_nat by blast
 
 lemma wfP_subset_mset[simp]: "wfP (\<subset>#)"
   by (rule wf_subset_mset_rel[to_pred])
@@ -3246,7 +3246,7 @@
   unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
 
 lemma wfP_multp: "wfP r \<Longrightarrow> wfP (multp r)"
-  unfolding multp_def wfP_def
+  unfolding multp_def wfp_def
   by (simp add: wf_mult)
 
 
diff -r 31b9dfbe534c -r b10f7c981df6 src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Mon Jun 10 13:44:46 2024 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Mon Jun 10 14:09:55 2024 +0200
@@ -399,7 +399,7 @@
 \<comment> \<open>Well-foundedness of the termination relation:\<close>
 apply (rule wf_lex_prod)
  apply (insert orderI [THEN acc_le_listI])
- apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric])
+ apply (simp add: acc_def lesssub_def wfp_wf_eq [symmetric])
 apply (rule wf_finite_psubset) 
 
 \<comment> \<open>Loop decreases along termination relation:\<close>
diff -r 31b9dfbe534c -r b10f7c981df6 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Mon Jun 10 13:44:46 2024 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Mon Jun 10 14:09:55 2024 +0200
@@ -715,7 +715,7 @@
 
 (** Termination rule **)
 
-val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
+val wf_induct_rule = @{thm Wellfounded.wfp_induct_rule}
 val wf_in_rel = @{thm Fun_Def.wf_in_rel}
 val in_rel_def = @{thm Fun_Def.in_rel_def}
 
diff -r 31b9dfbe534c -r b10f7c981df6 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Jun 10 13:44:46 2024 +0200
+++ b/src/HOL/Wellfounded.thy	Mon Jun 10 14:09:55 2024 +0200
@@ -41,10 +41,10 @@
 lemma wf_def: "wf r \<longleftrightarrow> (\<forall>P. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x. P x))"
   unfolding wf_on_def by simp
 
-lemma wfP_def: "wfP r \<longleftrightarrow> wf {(x, y). r x y}"
+lemma wfp_def: "wfp r \<longleftrightarrow> wf {(x, y). r x y}"
   unfolding wf_def wfp_on_def by simp
 
-lemma wfP_wf_eq: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
+lemma wfp_wf_eq: "wfp (\<lambda>x y. (x, y) \<in> r) = wf r"
   using wfp_on_wf_on_eq .
 
 
@@ -66,11 +66,11 @@
   shows "P a"
   using assms by (auto intro: wf_on_induct[of UNIV])
 
-lemmas wfP_induct = wf_induct [to_pred]
+lemmas wfp_induct = wf_induct [to_pred]
 
 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
 
-lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
+lemmas wfp_induct_rule = wf_induct_rule [to_pred, induct set: wfp]
 
 lemma wf_on_iff_wf: "wf_on A r \<longleftrightarrow> wf {(x, y) \<in> r. x \<in> A \<and> y \<in> A}"
 proof (rule iffI)
@@ -129,7 +129,7 @@
 lemma wfUNIVI: "(\<And>P x. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<Longrightarrow> P x) \<Longrightarrow> wf r"
   unfolding wf_def by blast
 
-lemmas wfPUNIVI = wfUNIVI [to_pred]
+lemmas wfpUNIVI = wfUNIVI [to_pred]
 
 text \<open>Restriction to domain \<open>A\<close> and range \<open>B\<close>.
   If \<open>r\<close> is well-founded over their intersection, then \<open>wf r\<close>.\<close>
@@ -153,7 +153,7 @@
 lemma wf_imp_asym: "wf r \<Longrightarrow> asym r"
   by (auto intro: asymI elim: wf_asym)
 
-lemma wfP_imp_asymp: "wfP r \<Longrightarrow> asymp r"
+lemma wfp_imp_asymp: "wfp r \<Longrightarrow> asymp r"
   by (rule wf_imp_asym[to_pred])
 
 lemma wf_not_refl [simp]: "wf r \<Longrightarrow> (a, a) \<notin> r"
@@ -168,7 +168,7 @@
   assumes "wf r" shows "irrefl r" 
   using wf_irrefl [OF assms] by (auto simp add: irrefl_def)
 
-lemma wfP_imp_irreflp: "wfP r \<Longrightarrow> irreflp r"
+lemma wfp_imp_irreflp: "wfp r \<Longrightarrow> irreflp r"
   by (rule wf_imp_irrefl[to_pred])
 
 lemma wf_wellorderI:
@@ -182,8 +182,8 @@
 lemma (in wellorder) wf: "wf {(x, y). x < y}"
   unfolding wf_def by (blast intro: less_induct)
 
-lemma (in wellorder) wfP_less[simp]: "wfP (<)"
-  by (simp add: wf wfP_def)
+lemma (in wellorder) wfP_less[simp]: "wfp (<)"
+  by (simp add: wf wfp_def)
 
 lemma (in wellorder) wfp_on_less[simp]: "wfp_on A (<)"
   unfolding wfp_on_def
@@ -307,7 +307,7 @@
 lemma wf_eq_minimal: "wf r \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q))"
   unfolding wf_iff_ex_minimal by blast
 
-lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
+lemmas wfp_eq_minimal = wf_eq_minimal [to_pred]
 
 
 subsubsection \<open>Antimonotonicity\<close>
@@ -376,7 +376,7 @@
   then show ?thesis unfolding wf_def by blast
 qed
 
-lemmas wfP_trancl = wf_trancl [to_pred]
+lemmas wfp_tranclp = wf_trancl [to_pred]
 
 lemma wf_converse_trancl: "wf (r\<inverse>) \<Longrightarrow> wf ((r\<^sup>+)\<inverse>)"
   apply (subst trancl_converse [symmetric])
@@ -388,16 +388,16 @@
 lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p"
   by (simp add: wf_eq_minimal) fast
 
-lemmas wfP_subset = wf_subset [to_pred]
+lemmas wfp_subset = wf_subset [to_pred]
 
 text \<open>Well-foundedness of the empty relation\<close>
 
 lemma wf_empty [iff]: "wf {}"
   by (simp add: wf_def)
 
-lemma wfP_empty [iff]: "wfP (\<lambda>x y. False)"
+lemma wfp_empty [iff]: "wfp (\<lambda>x y. False)"
 proof -
-  have "wfP bot"
+  have "wfp bot"
     by (fact wf_empty[to_pred bot_empty_eq2])
   then show ?thesis
     by (simp add: bot_fun_def)
@@ -602,9 +602,9 @@
   qed
 qed
 
-lemma wfP_SUP:
-  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow>
-    wfP (\<Squnion>(range r))"
+lemma wfp_SUP:
+  "\<forall>i. wfp (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow>
+    wfp (\<Squnion>(range r))"
   by (rule wf_UN[to_pred]) simp_all
 
 lemma wf_Union:
@@ -757,7 +757,7 @@
 lemma wf_acyclic: "wf r \<Longrightarrow> acyclic r"
   by (simp add: acyclic_def) (blast elim: wf_trancl [THEN wf_irrefl])
 
-lemmas wfP_acyclicP = wf_acyclic [to_pred]
+lemmas wfp_acyclicP = wf_acyclic [to_pred]
 
 
 subsubsection \<open>Wellfoundedness of finite acyclic relations\<close>
@@ -922,7 +922,7 @@
   by (blast dest: accp_downwards_aux)
 
 theorem accp_wfpI: "\<forall>x. accp r x \<Longrightarrow> wfp r"
-proof (rule wfPUNIVI)
+proof (rule wfpUNIVI)
   fix P x
   assume "\<forall>x. accp r x" "\<forall>x. (\<forall>y. r y x \<longrightarrow> P y) \<longrightarrow> P x"
   then show "P x"
@@ -930,7 +930,7 @@
 qed
 
 theorem accp_wfpD: "wfp r \<Longrightarrow> accp r x"
-  apply (erule wfP_induct_rule)
+  apply (erule wfp_induct_rule)
   apply (rule accp.accI)
   apply blast
   done