10 begin |
10 begin |
11 |
11 |
12 named_theorems partial_function_mono "monotonicity rules for partial function definitions" |
12 named_theorems partial_function_mono "monotonicity rules for partial function definitions" |
13 ML_file "Tools/Function/partial_function.ML" |
13 ML_file "Tools/Function/partial_function.ML" |
14 |
14 |
|
15 lemma (in ccpo) in_chain_finite: |
|
16 assumes "Complete_Partial_Order.chain op \<le> A" "finite A" "A \<noteq> {}" |
|
17 shows "\<Squnion>A \<in> A" |
|
18 using assms(2,1,3) |
|
19 proof induction |
|
20 case empty thus ?case by simp |
|
21 next |
|
22 case (insert x A) |
|
23 note chain = `Complete_Partial_Order.chain op \<le> (insert x A)` |
|
24 show ?case |
|
25 proof(cases "A = {}") |
|
26 case True thus ?thesis by simp |
|
27 next |
|
28 case False |
|
29 from chain have chain': "Complete_Partial_Order.chain op \<le> A" |
|
30 by(rule chain_subset) blast |
|
31 hence "\<Squnion>A \<in> A" using False by(rule insert.IH) |
|
32 show ?thesis |
|
33 proof(cases "x \<le> \<Squnion>A") |
|
34 case True |
|
35 have "\<Squnion>insert x A \<le> \<Squnion>A" using chain |
|
36 by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain']) |
|
37 hence "\<Squnion>insert x A = \<Squnion>A" |
|
38 by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain']) |
|
39 with `\<Squnion>A \<in> A` show ?thesis by simp |
|
40 next |
|
41 case False |
|
42 with chainD[OF chain, of x "\<Squnion>A"] `\<Squnion>A \<in> A` |
|
43 have "\<Squnion>insert x A = x" |
|
44 by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain]) |
|
45 thus ?thesis by simp |
|
46 qed |
|
47 qed |
|
48 qed |
15 |
49 |
16 subsection {* Axiomatic setup *} |
50 subsection {* Axiomatic setup *} |
17 |
51 |
18 text {* This techical locale constains the requirements for function |
52 text {* This techical locale constains the requirements for function |
19 definitions with ccpo fixed points. *} |
53 definitions with ccpo fixed points. *} |