# HG changeset patch
# User Andreas Lochbihler
# Date 1429012645 -7200
# Node ID 4c5de5a860ee4677bd89d0945463f6298073a5ff
# Parent  279472fa0b1d6a79e3d0b091eb7cda94893214fb
move lemma from AFP/Coinductive

diff -r 279472fa0b1d -r 4c5de5a860ee src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Tue Apr 14 13:56:34 2015 +0200
+++ b/src/HOL/Partial_Function.thy	Tue Apr 14 13:57:25 2015 +0200
@@ -12,6 +12,40 @@
 named_theorems partial_function_mono "monotonicity rules for partial function definitions"
 ML_file "Tools/Function/partial_function.ML"
 
+lemma (in ccpo) in_chain_finite:
+  assumes "Complete_Partial_Order.chain op \<le> A" "finite A" "A \<noteq> {}"
+  shows "\<Squnion>A \<in> A"
+using assms(2,1,3)
+proof induction
+  case empty thus ?case by simp
+next
+  case (insert x A)
+  note chain = `Complete_Partial_Order.chain op \<le> (insert x A)`
+  show ?case
+  proof(cases "A = {}")
+    case True thus ?thesis by simp
+  next
+    case False
+    from chain have chain': "Complete_Partial_Order.chain op \<le> A"
+      by(rule chain_subset) blast
+    hence "\<Squnion>A \<in> A" using False by(rule insert.IH)
+    show ?thesis
+    proof(cases "x \<le> \<Squnion>A")
+      case True
+      have "\<Squnion>insert x A \<le> \<Squnion>A" using chain
+        by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain'])
+      hence "\<Squnion>insert x A = \<Squnion>A"
+        by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
+      with `\<Squnion>A \<in> A` show ?thesis by simp
+    next
+      case False
+      with chainD[OF chain, of x "\<Squnion>A"] `\<Squnion>A \<in> A`
+      have "\<Squnion>insert x A = x"
+        by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
+      thus ?thesis by simp
+    qed
+  qed
+qed
 
 subsection {* Axiomatic setup *}