# HG changeset patch
# User nipkow
# Date 1555561170 -7200
# Node ID 93516cb6cd3080cbe184ee01855d5d5f85c80c77
# Parent  269dcea7426c6a12b1576990a7de8abf80e35d04# Parent  5beca7396282821b03b411060d2fa42ed818f6ea
merged

diff -r 269dcea7426c -r 93516cb6cd30 src/HOL/Order_Relation.thy
--- a/src/HOL/Order_Relation.thy	Wed Apr 17 21:53:45 2019 +0100
+++ b/src/HOL/Order_Relation.thy	Thu Apr 18 06:19:30 2019 +0200
@@ -52,6 +52,14 @@
   by (simp add: linear_order_on_def)
 
 
+lemma partial_order_on_acyclic:
+  "partial_order_on A r \<Longrightarrow> acyclic (r - Id)"
+  by (simp add: acyclic_irrefl partial_order_on_def preorder_on_def trans_diff_Id)
+
+lemma partial_order_on_well_order_on:               
+  "finite r \<Longrightarrow> partial_order_on A r \<Longrightarrow> wf (r - Id)" 
+  by (simp add: finite_acyclic_wf partial_order_on_acyclic) 
+
 lemma strict_linear_order_on_diff_Id: "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r - Id)"
   by (simp add: order_on_defs trans_diff_Id)
 
@@ -360,6 +368,23 @@
     using assms order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
 qed
 
+lemma finite_Partial_order_induct[consumes 3, case_names step]:
+  assumes "Partial_order r"
+    and "x \<in> Field r"
+    and "finite r"
+    and step: "\<And>x. x \<in> Field r \<Longrightarrow> (\<And>y. y \<in> aboveS r x \<Longrightarrow> P y) \<Longrightarrow> P x"
+  shows "P x"
+  using assms(2)
+proof (induct rule: wf_induct[of "r\<inverse> - Id"])
+  case 1
+  from assms(1,3) show "wf (r\<inverse> - Id)"
+    using partial_order_on_well_order_on partial_order_on_converse by blast
+next
+  case prems: (2 x)
+  show ?case
+    by (rule step) (use prems in \<open>auto simp: aboveS_def intro: FieldI2\<close>)
+qed
+
 lemma finite_Linear_order_induct[consumes 3, case_names step]:
   assumes "Linear_order r"
     and "x \<in> Field r"