author | wenzelm |
Tue, 29 Mar 2011 17:47:11 +0200 | |
changeset 42151 | 4da4fc77664b |
parent 41533 | 869b5ea478b0 |
child 58880 | 0baae4311a9f |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Library/Defl_Bifinite.thy |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
2 |
Author: Brian Huffman |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
3 |
*) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
4 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
5 |
header {* Algebraic deflations are a bifinite domain *} |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
6 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
7 |
theory Defl_Bifinite |
41477 | 8 |
imports HOLCF "~~/src/HOL/Library/Infinite_Set" |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
9 |
begin |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
10 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
11 |
subsection {* Lemmas about MOST *} |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
12 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
13 |
default_sort type |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
14 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
15 |
lemma MOST_INFM: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
16 |
assumes inf: "infinite (UNIV::'a set)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
17 |
shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
18 |
unfolding Alm_all_def Inf_many_def |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
19 |
apply (auto simp add: Collect_neg_eq) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
20 |
apply (drule (1) finite_UnI) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
21 |
apply (simp add: Compl_partition2 inf) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
22 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
23 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
24 |
lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
25 |
by (rule MOST_inj [OF _ inj_Suc]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
26 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
27 |
lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
28 |
unfolding MOST_nat |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
29 |
apply (clarify, rule_tac x="Suc m" in exI, clarify) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
30 |
apply (erule Suc_lessE, simp) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
31 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
32 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
33 |
lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
34 |
by (rule iffI [OF MOST_SucD MOST_SucI]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
35 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
36 |
lemma INFM_finite_Bex_distrib: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
37 |
"finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
38 |
by (induct set: finite, simp, simp add: INFM_disj_distrib) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
39 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
40 |
lemma MOST_finite_Ball_distrib: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
41 |
"finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
42 |
by (induct set: finite, simp, simp add: MOST_conj_distrib) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
43 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
44 |
lemma MOST_ge_nat: "MOST n::nat. m \<le> n" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
45 |
unfolding MOST_nat_le by fast |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
46 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
47 |
subsection {* Eventually constant sequences *} |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
48 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
49 |
definition |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
50 |
eventually_constant :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
51 |
where |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
52 |
"eventually_constant S = (\<exists>x. MOST i. S i = x)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
53 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
54 |
lemma eventually_constant_MOST_MOST: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
55 |
"eventually_constant S \<longleftrightarrow> (MOST m. MOST n. S n = S m)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
56 |
unfolding eventually_constant_def MOST_nat |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
57 |
apply safe |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
58 |
apply (rule_tac x=m in exI, clarify) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
59 |
apply (rule_tac x=m in exI, clarify) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
60 |
apply simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
61 |
apply fast |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
62 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
63 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
64 |
lemma eventually_constantI: "MOST i. S i = x \<Longrightarrow> eventually_constant S" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
65 |
unfolding eventually_constant_def by fast |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
66 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
67 |
lemma eventually_constant_comp: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
68 |
"eventually_constant (\<lambda>i. S i) \<Longrightarrow> eventually_constant (\<lambda>i. f (S i))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
69 |
unfolding eventually_constant_def |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
70 |
apply (erule exE, rule_tac x="f x" in exI) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
71 |
apply (erule MOST_mono, simp) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
72 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
73 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
74 |
lemma eventually_constant_Suc_iff: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
75 |
"eventually_constant (\<lambda>i. S (Suc i)) \<longleftrightarrow> eventually_constant (\<lambda>i. S i)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
76 |
unfolding eventually_constant_def |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
77 |
by (subst MOST_Suc_iff, rule refl) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
78 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
79 |
lemma eventually_constant_SucD: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
80 |
"eventually_constant (\<lambda>i. S (Suc i)) \<Longrightarrow> eventually_constant (\<lambda>i. S i)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
81 |
by (rule eventually_constant_Suc_iff [THEN iffD1]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
82 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
83 |
subsection {* Limits of eventually constant sequences *} |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
84 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
85 |
definition |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
86 |
eventual :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
87 |
"eventual S = (THE x. MOST i. S i = x)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
88 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
89 |
lemma eventual_eqI: "MOST i. S i = x \<Longrightarrow> eventual S = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
90 |
unfolding eventual_def |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
91 |
apply (rule the_equality, assumption) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
92 |
apply (rename_tac y) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
93 |
apply (subgoal_tac "MOST i::nat. y = x", simp) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
94 |
apply (erule MOST_rev_mp) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
95 |
apply (erule MOST_rev_mp) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
96 |
apply simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
97 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
98 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
99 |
lemma MOST_eq_eventual: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
100 |
"eventually_constant S \<Longrightarrow> MOST i. S i = eventual S" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
101 |
unfolding eventually_constant_def |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
102 |
by (erule exE, simp add: eventual_eqI) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
103 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
104 |
lemma eventual_mem_range: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
105 |
"eventually_constant S \<Longrightarrow> eventual S \<in> range S" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
106 |
apply (drule MOST_eq_eventual) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
107 |
apply (simp only: MOST_nat_le, clarify) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
108 |
apply (drule spec, drule mp, rule order_refl) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
109 |
apply (erule range_eqI [OF sym]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
110 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
111 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
112 |
lemma eventually_constant_MOST_iff: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
113 |
assumes S: "eventually_constant S" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
114 |
shows "(MOST n. P (S n)) \<longleftrightarrow> P (eventual S)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
115 |
apply (subgoal_tac "(MOST n. P (S n)) \<longleftrightarrow> (MOST n::nat. P (eventual S))") |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
116 |
apply simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
117 |
apply (rule iffI) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
118 |
apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
119 |
apply (erule MOST_mono, force) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
120 |
apply (rule MOST_rev_mp [OF MOST_eq_eventual [OF S]]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
121 |
apply (erule MOST_mono, simp) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
122 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
123 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
124 |
lemma MOST_eventual: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
125 |
"\<lbrakk>eventually_constant S; MOST n. P (S n)\<rbrakk> \<Longrightarrow> P (eventual S)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
126 |
proof - |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
127 |
assume "eventually_constant S" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
128 |
hence "MOST n. S n = eventual S" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
129 |
by (rule MOST_eq_eventual) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
130 |
moreover assume "MOST n. P (S n)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
131 |
ultimately have "MOST n. S n = eventual S \<and> P (S n)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
132 |
by (rule MOST_conj_distrib [THEN iffD2, OF conjI]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
133 |
hence "MOST n::nat. P (eventual S)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
134 |
by (rule MOST_mono) auto |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
135 |
thus ?thesis by simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
136 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
137 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
138 |
lemma eventually_constant_MOST_Suc_eq: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
139 |
"eventually_constant S \<Longrightarrow> MOST n. S (Suc n) = S n" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
140 |
apply (drule MOST_eq_eventual) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
141 |
apply (frule MOST_Suc_iff [THEN iffD2]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
142 |
apply (erule MOST_rev_mp) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
143 |
apply (erule MOST_rev_mp) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
144 |
apply simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
145 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
146 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
147 |
lemma eventual_comp: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
148 |
"eventually_constant S \<Longrightarrow> eventual (\<lambda>i. f (S i)) = f (eventual (\<lambda>i. S i))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
149 |
apply (rule eventual_eqI) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
150 |
apply (rule MOST_mono) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
151 |
apply (erule MOST_eq_eventual) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
152 |
apply simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
153 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
154 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
155 |
subsection {* Constructing finite deflations by iteration *} |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
156 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
157 |
default_sort cpo |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
158 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
159 |
lemma le_Suc_induct: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
160 |
assumes le: "i \<le> j" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
161 |
assumes step: "\<And>i. P i (Suc i)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
162 |
assumes refl: "\<And>i. P i i" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
163 |
assumes trans: "\<And>i j k. \<lbrakk>P i j; P j k\<rbrakk> \<Longrightarrow> P i k" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
164 |
shows "P i j" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
165 |
proof (cases "i = j") |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
166 |
assume "i = j" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
167 |
thus "P i j" by (simp add: refl) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
168 |
next |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
169 |
assume "i \<noteq> j" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
170 |
with le have "i < j" by simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
171 |
thus "P i j" using step trans by (rule less_Suc_induct) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
172 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
173 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
174 |
definition |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
175 |
eventual_iterate :: "('a \<rightarrow> 'a::cpo) \<Rightarrow> ('a \<rightarrow> 'a)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
176 |
where |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
177 |
"eventual_iterate f = eventual (\<lambda>n. iterate n\<cdot>f)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
178 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
179 |
text {* A pre-deflation is like a deflation, but not idempotent. *} |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
180 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
181 |
locale pre_deflation = |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
182 |
fixes f :: "'a \<rightarrow> 'a::cpo" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
183 |
assumes below: "\<And>x. f\<cdot>x \<sqsubseteq> x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
184 |
assumes finite_range: "finite (range (\<lambda>x. f\<cdot>x))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
185 |
begin |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
186 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
187 |
lemma iterate_below: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
188 |
by (induct i, simp_all add: below_trans [OF below]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
189 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
190 |
lemma iterate_fixed: "f\<cdot>x = x \<Longrightarrow> iterate i\<cdot>f\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
191 |
by (induct i, simp_all) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
192 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
193 |
lemma antichain_iterate_app: "i \<le> j \<Longrightarrow> iterate j\<cdot>f\<cdot>x \<sqsubseteq> iterate i\<cdot>f\<cdot>x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
194 |
apply (erule le_Suc_induct) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
195 |
apply (simp add: below) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
196 |
apply (rule below_refl) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
197 |
apply (erule (1) below_trans) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
198 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
199 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
200 |
lemma finite_range_iterate_app: "finite (range (\<lambda>i. iterate i\<cdot>f\<cdot>x))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
201 |
proof (rule finite_subset) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
202 |
show "range (\<lambda>i. iterate i\<cdot>f\<cdot>x) \<subseteq> insert x (range (\<lambda>x. f\<cdot>x))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
203 |
by (clarify, case_tac i, simp_all) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
204 |
show "finite (insert x (range (\<lambda>x. f\<cdot>x)))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
205 |
by (simp add: finite_range) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
206 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
207 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
208 |
lemma eventually_constant_iterate_app: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
209 |
"eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>x)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
210 |
unfolding eventually_constant_def MOST_nat_le |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
211 |
proof - |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
212 |
let ?Y = "\<lambda>i. iterate i\<cdot>f\<cdot>x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
213 |
have "\<exists>j. \<forall>k. ?Y j \<sqsubseteq> ?Y k" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
214 |
apply (rule finite_range_has_max) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
215 |
apply (erule antichain_iterate_app) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
216 |
apply (rule finite_range_iterate_app) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
217 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
218 |
then obtain j where j: "\<And>k. ?Y j \<sqsubseteq> ?Y k" by fast |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
219 |
show "\<exists>z m. \<forall>n\<ge>m. ?Y n = z" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
220 |
proof (intro exI allI impI) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
221 |
fix k |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
222 |
assume "j \<le> k" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
223 |
hence "?Y k \<sqsubseteq> ?Y j" by (rule antichain_iterate_app) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
224 |
also have "?Y j \<sqsubseteq> ?Y k" by (rule j) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
225 |
finally show "?Y k = ?Y j" . |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
226 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
227 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
228 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
229 |
lemma eventually_constant_iterate: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
230 |
"eventually_constant (\<lambda>n. iterate n\<cdot>f)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
231 |
proof - |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
232 |
have "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). eventually_constant (\<lambda>i. iterate i\<cdot>f\<cdot>y)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
233 |
by (simp add: eventually_constant_iterate_app) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
234 |
hence "\<forall>y\<in>range (\<lambda>x. f\<cdot>x). MOST i. MOST j. iterate j\<cdot>f\<cdot>y = iterate i\<cdot>f\<cdot>y" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
235 |
unfolding eventually_constant_MOST_MOST . |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
236 |
hence "MOST i. MOST j. \<forall>y\<in>range (\<lambda>x. f\<cdot>x). iterate j\<cdot>f\<cdot>y = iterate i\<cdot>f\<cdot>y" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
237 |
by (simp only: MOST_finite_Ball_distrib [OF finite_range]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
238 |
hence "MOST i. MOST j. \<forall>x. iterate j\<cdot>f\<cdot>(f\<cdot>x) = iterate i\<cdot>f\<cdot>(f\<cdot>x)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
239 |
by simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
240 |
hence "MOST i. MOST j. \<forall>x. iterate (Suc j)\<cdot>f\<cdot>x = iterate (Suc i)\<cdot>f\<cdot>x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
241 |
by (simp only: iterate_Suc2) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
242 |
hence "MOST i. MOST j. iterate (Suc j)\<cdot>f = iterate (Suc i)\<cdot>f" |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39999
diff
changeset
|
243 |
by (simp only: cfun_eq_iff) |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
244 |
hence "eventually_constant (\<lambda>i. iterate (Suc i)\<cdot>f)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
245 |
unfolding eventually_constant_MOST_MOST . |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
246 |
thus "eventually_constant (\<lambda>i. iterate i\<cdot>f)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
247 |
by (rule eventually_constant_SucD) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
248 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
249 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
250 |
abbreviation |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
251 |
d :: "'a \<rightarrow> 'a" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
252 |
where |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
253 |
"d \<equiv> eventual_iterate f" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
254 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
255 |
lemma MOST_d: "MOST n. P (iterate n\<cdot>f) \<Longrightarrow> P d" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
256 |
unfolding eventual_iterate_def |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
257 |
using eventually_constant_iterate by (rule MOST_eventual) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
258 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
259 |
lemma f_d: "f\<cdot>(d\<cdot>x) = d\<cdot>x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
260 |
apply (rule MOST_d) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
261 |
apply (subst iterate_Suc [symmetric]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
262 |
apply (rule eventually_constant_MOST_Suc_eq) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
263 |
apply (rule eventually_constant_iterate_app) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
264 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
265 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
266 |
lemma d_fixed_iff: "d\<cdot>x = x \<longleftrightarrow> f\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
267 |
proof |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
268 |
assume "d\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
269 |
with f_d [where x=x] |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
270 |
show "f\<cdot>x = x" by simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
271 |
next |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
272 |
assume f: "f\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
273 |
have "\<forall>n. iterate n\<cdot>f\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
274 |
by (rule allI, rule nat.induct, simp, simp add: f) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
275 |
hence "MOST n. iterate n\<cdot>f\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
276 |
by (rule ALL_MOST) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
277 |
thus "d\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
278 |
by (rule MOST_d) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
279 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
280 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
281 |
lemma finite_deflation_d: "finite_deflation d" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
282 |
proof |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
283 |
fix x :: 'a |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
284 |
have "d \<in> range (\<lambda>n. iterate n\<cdot>f)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
285 |
unfolding eventual_iterate_def |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
286 |
using eventually_constant_iterate |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
287 |
by (rule eventual_mem_range) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
288 |
then obtain n where n: "d = iterate n\<cdot>f" .. |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
289 |
have "iterate n\<cdot>f\<cdot>(d\<cdot>x) = d\<cdot>x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
290 |
using f_d by (rule iterate_fixed) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
291 |
thus "d\<cdot>(d\<cdot>x) = d\<cdot>x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
292 |
by (simp add: n) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
293 |
next |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
294 |
fix x :: 'a |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
295 |
show "d\<cdot>x \<sqsubseteq> x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
296 |
by (rule MOST_d, simp add: iterate_below) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
297 |
next |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
298 |
from finite_range |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
299 |
have "finite {x. f\<cdot>x = x}" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
300 |
by (rule finite_range_imp_finite_fixes) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
301 |
thus "finite {x. d\<cdot>x = x}" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
302 |
by (simp add: d_fixed_iff) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
303 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
304 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
305 |
lemma deflation_d: "deflation d" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
306 |
using finite_deflation_d |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
307 |
by (rule finite_deflation_imp_deflation) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
308 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
309 |
end |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
310 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
311 |
lemma finite_deflation_eventual_iterate: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
312 |
"pre_deflation d \<Longrightarrow> finite_deflation (eventual_iterate d)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
313 |
by (rule pre_deflation.finite_deflation_d) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
314 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
315 |
lemma pre_deflation_oo: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
316 |
assumes "finite_deflation d" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
317 |
assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
318 |
shows "pre_deflation (d oo f)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
319 |
proof |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
320 |
interpret d: finite_deflation d by fact |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
321 |
fix x |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
322 |
show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
323 |
by (simp, rule below_trans [OF d.below f]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
324 |
show "finite (range (\<lambda>x. (d oo f)\<cdot>x))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
325 |
by (rule finite_subset [OF _ d.finite_range], auto) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
326 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
327 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
328 |
lemma eventual_iterate_oo_fixed_iff: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
329 |
assumes "finite_deflation d" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
330 |
assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
331 |
shows "eventual_iterate (d oo f)\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
332 |
proof - |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
333 |
interpret d: finite_deflation d by fact |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
334 |
let ?e = "d oo f" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
335 |
interpret e: pre_deflation "d oo f" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
336 |
using `finite_deflation d` f |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
337 |
by (rule pre_deflation_oo) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
338 |
let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
339 |
show ?thesis |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
340 |
apply (subst e.d_fixed_iff) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
341 |
apply simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
342 |
apply safe |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
343 |
apply (erule subst) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
344 |
apply (rule d.idem) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
345 |
apply (rule below_antisym) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
346 |
apply (rule f) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
347 |
apply (erule subst, rule d.below) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
348 |
apply simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
349 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
350 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
351 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
352 |
lemma eventual_mono: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
353 |
assumes A: "eventually_constant A" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
354 |
assumes B: "eventually_constant B" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
355 |
assumes below: "\<And>n. A n \<sqsubseteq> B n" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
356 |
shows "eventual A \<sqsubseteq> eventual B" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
357 |
proof - |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
358 |
from A have "MOST n. A n = eventual A" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
359 |
by (rule MOST_eq_eventual) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
360 |
then have "MOST n. eventual A \<sqsubseteq> B n" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
361 |
by (rule MOST_mono) (erule subst, rule below) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
362 |
with B show "eventual A \<sqsubseteq> eventual B" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
363 |
by (rule MOST_eventual) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
364 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
365 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
366 |
lemma eventual_iterate_mono: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
367 |
assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \<sqsubseteq> g" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
368 |
shows "eventual_iterate f \<sqsubseteq> eventual_iterate g" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
369 |
unfolding eventual_iterate_def |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
370 |
apply (rule eventual_mono) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
371 |
apply (rule pre_deflation.eventually_constant_iterate [OF f]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
372 |
apply (rule pre_deflation.eventually_constant_iterate [OF g]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
373 |
apply (rule monofun_cfun_arg [OF `f \<sqsubseteq> g`]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
374 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
375 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
376 |
lemma cont2cont_eventual_iterate_oo: |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
377 |
assumes d: "finite_deflation d" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
378 |
assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
379 |
shows "cont (\<lambda>x. eventual_iterate (d oo f x))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
380 |
(is "cont ?e") |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
381 |
proof (rule contI2) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
382 |
show "monofun ?e" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
383 |
apply (rule monofunI) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
384 |
apply (rule eventual_iterate_mono) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
385 |
apply (rule pre_deflation_oo [OF d below]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
386 |
apply (rule pre_deflation_oo [OF d below]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
387 |
apply (rule monofun_cfun_arg) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
388 |
apply (erule cont2monofunE [OF cont]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
389 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
390 |
next |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
391 |
fix Y :: "nat \<Rightarrow> 'b" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
392 |
assume Y: "chain Y" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
393 |
with cont have fY: "chain (\<lambda>i. f (Y i))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
394 |
by (rule ch2ch_cont) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
395 |
assume eY: "chain (\<lambda>i. ?e (Y i))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
396 |
have lub_below: "\<And>x. f (\<Squnion>i. Y i)\<cdot>x \<sqsubseteq> x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
397 |
by (rule admD [OF _ Y], simp add: cont, rule below) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
398 |
have "deflation (?e (\<Squnion>i. Y i))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
399 |
apply (rule pre_deflation.deflation_d) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
400 |
apply (rule pre_deflation_oo [OF d lub_below]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
401 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
402 |
then show "?e (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. ?e (Y i))" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
403 |
proof (rule deflation.belowI) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
404 |
fix x :: 'a |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
405 |
assume "?e (\<Squnion>i. Y i)\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
406 |
hence "d\<cdot>x = x" and "f (\<Squnion>i. Y i)\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
407 |
by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
408 |
hence "(\<Squnion>i. f (Y i)\<cdot>x) = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
409 |
apply (simp only: cont2contlubE [OF cont Y]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
410 |
apply (simp only: contlub_cfun_fun [OF fY]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
411 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
412 |
have "compact (d\<cdot>x)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
413 |
using d by (rule finite_deflation.compact) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
414 |
then have "compact x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
415 |
using `d\<cdot>x = x` by simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
416 |
then have "compact (\<Squnion>i. f (Y i)\<cdot>x)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
417 |
using `(\<Squnion>i. f (Y i)\<cdot>x) = x` by simp |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
418 |
then have "\<exists>n. max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
419 |
by - (rule compact_imp_max_in_chain, simp add: fY, assumption) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
420 |
then obtain n where n: "max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" .. |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
421 |
then have "f (Y n)\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
422 |
using `(\<Squnion>i. f (Y i)\<cdot>x) = x` fY by (simp add: maxinch_is_thelub) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
423 |
with `d\<cdot>x = x` have "?e (Y n)\<cdot>x = x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
424 |
by (simp add: eventual_iterate_oo_fixed_iff [OF d below]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
425 |
moreover have "?e (Y n)\<cdot>x \<sqsubseteq> (\<Squnion>i. ?e (Y i)\<cdot>x)" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
426 |
by (rule is_ub_thelub, simp add: eY) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
427 |
ultimately have "x \<sqsubseteq> (\<Squnion>i. ?e (Y i))\<cdot>x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
428 |
by (simp add: contlub_cfun_fun eY) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
429 |
also have "(\<Squnion>i. ?e (Y i))\<cdot>x \<sqsubseteq> x" |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
430 |
apply (rule deflation.below) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
431 |
apply (rule admD [OF adm_deflation eY]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
432 |
apply (rule pre_deflation.deflation_d) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
433 |
apply (rule pre_deflation_oo [OF d below]) |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
434 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
435 |
finally show "(\<Squnion>i. ?e (Y i))\<cdot>x = x" .. |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
436 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
437 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
438 |
|
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
439 |
subsection {* Intersection of algebraic deflations *} |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
440 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
441 |
default_sort bifinite |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
442 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
443 |
definition meet_fin_defl :: "'a fin_defl \<Rightarrow> 'a fin_defl \<Rightarrow> 'a fin_defl" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
444 |
where "meet_fin_defl a b = |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
445 |
Abs_fin_defl (eventual_iterate (Rep_fin_defl a oo Rep_fin_defl b))" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
446 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
447 |
lemma Rep_meet_fin_defl: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
448 |
"Rep_fin_defl (meet_fin_defl a b) = |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
449 |
eventual_iterate (Rep_fin_defl a oo Rep_fin_defl b)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
450 |
unfolding meet_fin_defl_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
451 |
apply (rule Abs_fin_defl_inverse [simplified]) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
452 |
apply (rule finite_deflation_eventual_iterate) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
453 |
apply (rule pre_deflation_oo) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
454 |
apply (rule finite_deflation_Rep_fin_defl) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
455 |
apply (rule Rep_fin_defl.below) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
456 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
457 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
458 |
lemma Rep_meet_fin_defl_fixed_iff: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
459 |
"Rep_fin_defl (meet_fin_defl a b)\<cdot>x = x \<longleftrightarrow> |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
460 |
Rep_fin_defl a\<cdot>x = x \<and> Rep_fin_defl b\<cdot>x = x" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
461 |
unfolding Rep_meet_fin_defl |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
462 |
apply (rule eventual_iterate_oo_fixed_iff) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
463 |
apply (rule finite_deflation_Rep_fin_defl) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
464 |
apply (rule Rep_fin_defl.below) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
465 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
466 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
467 |
lemma meet_fin_defl_mono: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
468 |
"\<lbrakk>a \<sqsubseteq> b; c \<sqsubseteq> d\<rbrakk> \<Longrightarrow> meet_fin_defl a c \<sqsubseteq> meet_fin_defl b d" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
469 |
unfolding below_fin_defl_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
470 |
apply (rule Rep_fin_defl.belowI) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
471 |
apply (simp add: Rep_meet_fin_defl_fixed_iff Rep_fin_defl.belowD) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
472 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
473 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
474 |
lemma meet_fin_defl_below1: "meet_fin_defl a b \<sqsubseteq> a" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
475 |
unfolding below_fin_defl_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
476 |
apply (rule Rep_fin_defl.belowI) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
477 |
apply (simp add: Rep_meet_fin_defl_fixed_iff Rep_fin_defl.belowD) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
478 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
479 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
480 |
lemma meet_fin_defl_below2: "meet_fin_defl a b \<sqsubseteq> b" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
481 |
unfolding below_fin_defl_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
482 |
apply (rule Rep_fin_defl.belowI) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
483 |
apply (simp add: Rep_meet_fin_defl_fixed_iff Rep_fin_defl.belowD) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
484 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
485 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
486 |
lemma meet_fin_defl_greatest: "\<lbrakk>a \<sqsubseteq> b; a \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> meet_fin_defl b c" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
487 |
unfolding below_fin_defl_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
488 |
apply (rule Rep_fin_defl.belowI) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
489 |
apply (simp add: Rep_meet_fin_defl_fixed_iff Rep_fin_defl.belowD) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
490 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
491 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
492 |
definition meet_defl :: "'a defl \<rightarrow> 'a defl \<rightarrow> 'a defl" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
493 |
where "meet_defl = defl.extension (\<lambda>a. defl.extension (\<lambda>b. |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
494 |
defl_principal (meet_fin_defl a b)))" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
495 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
496 |
lemma meet_defl_principal: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
497 |
"meet_defl\<cdot>(defl_principal a)\<cdot>(defl_principal b) = |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
498 |
defl_principal (meet_fin_defl a b)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
499 |
unfolding meet_defl_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
500 |
by (simp add: defl.extension_principal defl.extension_mono meet_fin_defl_mono) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
501 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
502 |
lemma meet_defl_below1: "meet_defl\<cdot>a\<cdot>b \<sqsubseteq> a" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
503 |
apply (induct a rule: defl.principal_induct, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
504 |
apply (induct b rule: defl.principal_induct, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
505 |
apply (simp add: meet_defl_principal meet_fin_defl_below1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
506 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
507 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
508 |
lemma meet_defl_below2: "meet_defl\<cdot>a\<cdot>b \<sqsubseteq> b" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
509 |
apply (induct a rule: defl.principal_induct, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
510 |
apply (induct b rule: defl.principal_induct, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
511 |
apply (simp add: meet_defl_principal meet_fin_defl_below2) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
512 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
513 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
514 |
lemma meet_defl_greatest: "\<lbrakk>a \<sqsubseteq> b; a \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> meet_defl\<cdot>b\<cdot>c" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
515 |
apply (induct a rule: defl.principal_induct, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
516 |
apply (induct b rule: defl.principal_induct, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
517 |
apply (induct c rule: defl.principal_induct, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
518 |
apply (simp add: meet_defl_principal meet_fin_defl_greatest) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
519 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
520 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
521 |
lemma meet_defl_eq2: "b \<sqsubseteq> a \<Longrightarrow> meet_defl\<cdot>a\<cdot>b = b" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
522 |
by (fast intro: below_antisym meet_defl_below2 meet_defl_greatest) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
523 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
524 |
interpretation meet_defl: semilattice "\<lambda>a b. meet_defl\<cdot>a\<cdot>b" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
525 |
by default |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
526 |
(fast intro: below_antisym meet_defl_greatest |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
527 |
meet_defl_below1 [THEN below_trans] meet_defl_below2 [THEN below_trans])+ |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
528 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
529 |
lemma deflation_meet_defl: "deflation (meet_defl\<cdot>a)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
530 |
apply (rule deflation.intro) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
531 |
apply (rule meet_defl.left_idem) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
532 |
apply (rule meet_defl_below2) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
533 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
534 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
535 |
lemma finite_deflation_meet_defl: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
536 |
assumes "compact a" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
537 |
shows "finite_deflation (meet_defl\<cdot>a)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
538 |
proof (rule finite_deflation_intro) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
539 |
obtain d where a: "a = defl_principal d" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
540 |
using defl.compact_imp_principal [OF assms] .. |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
541 |
have "finite (defl_set -` Pow (defl_set a))" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
542 |
apply (rule finite_vimageI) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
543 |
apply (rule finite_Pow_iff [THEN iffD2]) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
544 |
apply (simp add: defl_set_def a cast_defl_principal Abs_fin_defl_inverse) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
545 |
apply (rule Rep_fin_defl.finite_fixes) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
546 |
apply (rule injI) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
547 |
apply (simp add: po_eq_conv defl_set_subset_iff [symmetric]) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
548 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
549 |
hence "finite (range (\<lambda>b. meet_defl\<cdot>a\<cdot>b))" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
550 |
apply (rule rev_finite_subset) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
551 |
apply (clarsimp, erule rev_subsetD) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
552 |
apply (simp add: defl_set_subset_iff meet_defl_below1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
553 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
554 |
thus "finite {b. meet_defl\<cdot>a\<cdot>b = b}" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
555 |
by (rule finite_range_imp_finite_fixes) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
556 |
qed (rule deflation_meet_defl) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
557 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
558 |
lemma compact_iff_finite_deflation_cast: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
559 |
"compact d \<longleftrightarrow> finite_deflation (cast\<cdot>d)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
560 |
apply (safe dest!: defl.compact_imp_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
561 |
apply (simp add: cast_defl_principal finite_deflation_Rep_fin_defl) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
562 |
apply (rule compact_cast_iff [THEN iffD1]) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
563 |
apply (erule finite_deflation_imp_compact) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
564 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
565 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
566 |
lemma compact_iff_finite_defl_set: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
567 |
"compact d \<longleftrightarrow> finite (defl_set d)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
568 |
by (simp add: compact_iff_finite_deflation_cast defl_set_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
569 |
finite_deflation_def deflation_cast finite_deflation_axioms_def) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
570 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
571 |
lemma compact_meet_defl1: "compact a \<Longrightarrow> compact (meet_defl\<cdot>a\<cdot>b)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
572 |
apply (simp add: compact_iff_finite_defl_set) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
573 |
apply (erule rev_finite_subset) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
574 |
apply (simp add: defl_set_subset_iff meet_defl_below1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
575 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
576 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
577 |
lemma compact_meet_defl2: "compact b \<Longrightarrow> compact (meet_defl\<cdot>a\<cdot>b)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
578 |
by (subst meet_defl.commute, rule compact_meet_defl1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
579 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
580 |
subsection {* Chain of approx functions on algebraic deflations *} |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
581 |
|
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
582 |
context bifinite_approx_chain |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
583 |
begin |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
584 |
|
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
585 |
definition defl_approx :: "nat \<Rightarrow> 'a defl \<rightarrow> 'a defl" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
586 |
where "defl_approx i = meet_defl\<cdot>(defl_principal (Abs_fin_defl (approx i)))" |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
587 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
588 |
lemma defl_approx: "approx_chain defl_approx" |
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
589 |
proof (rule approx_chain.intro) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
590 |
have chain1: "chain (\<lambda>i. defl_principal (Abs_fin_defl (approx i)))" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
591 |
apply (rule chainI) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
592 |
apply (rule defl.principal_mono) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
593 |
apply (simp add: below_fin_defl_def Abs_fin_defl_inverse) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
594 |
apply (rule chainE [OF chain_approx]) |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
595 |
done |
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
596 |
show chain: "chain (\<lambda>i. defl_approx i)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
597 |
unfolding defl_approx_def by (simp add: chain1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
598 |
have below: "\<And>i d. defl_approx i\<cdot>d \<sqsubseteq> d" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
599 |
unfolding defl_approx_def by (rule meet_defl_below2) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
600 |
show "(\<Squnion>i. defl_approx i) = ID" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
601 |
apply (rule cfun_eqI, rename_tac d, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
602 |
apply (rule below_antisym) |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
603 |
apply (simp add: contlub_cfun_fun chain) |
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
604 |
apply (simp add: lub_below chain below) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
605 |
apply (simp add: defl_approx_def) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
606 |
apply (simp add: lub_distribs chain1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
607 |
apply (rule meet_defl_greatest [OF _ below_refl]) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
608 |
apply (rule cast_below_imp_below) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
609 |
apply (simp add: contlub_cfun_arg chain1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
610 |
apply (simp add: cast_defl_principal Abs_fin_defl_inverse) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
611 |
apply (rule cast.below_ID) |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
612 |
done |
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
613 |
show "\<And>i. finite_deflation (defl_approx i)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
614 |
unfolding defl_approx_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
615 |
apply (rule finite_deflation_meet_defl) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
616 |
apply (rule defl.compact_principal) |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
617 |
done |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
618 |
qed |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
619 |
|
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
620 |
end |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
621 |
|
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
622 |
subsection {* Algebraic deflations are a bifinite domain *} |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
623 |
|
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
624 |
instance defl :: (bifinite) bifinite |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
625 |
proof |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
626 |
obtain a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where "approx_chain a" |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
627 |
using bifinite .. |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
628 |
hence "bifinite_approx_chain a" |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
629 |
unfolding bifinite_approx_chain_def . |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
630 |
thus "\<exists>(a::nat \<Rightarrow> 'a defl \<rightarrow> 'a defl). approx_chain a" |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
631 |
by (fast intro: bifinite_approx_chain.defl_approx) |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
632 |
qed |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
633 |
|
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
634 |
subsection {* Algebraic deflations are representable *} |
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
40774
diff
changeset
|
635 |
|
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
636 |
default_sort "domain" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
637 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
638 |
definition defl_emb :: "udom defl \<rightarrow> udom" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
639 |
where "defl_emb = udom_emb (bifinite_approx_chain.defl_approx udom_approx)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
640 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
641 |
definition defl_prj :: "udom \<rightarrow> udom defl" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
642 |
where "defl_prj = udom_prj (bifinite_approx_chain.defl_approx udom_approx)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
643 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
644 |
lemma ep_pair_defl: "ep_pair defl_emb defl_prj" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
645 |
unfolding defl_emb_def defl_prj_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
646 |
apply (rule ep_pair_udom) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
647 |
apply (rule bifinite_approx_chain.defl_approx) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
648 |
apply (simp add: bifinite_approx_chain_def) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
649 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
650 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
651 |
text "Deflation combinator for deflation type constructor" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
652 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
653 |
definition defl_defl :: "udom defl \<rightarrow> udom defl" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
654 |
where defl_deflation_def: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
655 |
"defl_defl = defl.extension (\<lambda>a. defl_principal |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
656 |
(Abs_fin_defl (defl_emb oo meet_defl\<cdot>(defl_principal a) oo defl_prj)))" |
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
657 |
|
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
658 |
lemma cast_defl_defl: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
659 |
"cast\<cdot>(defl_defl\<cdot>a) = defl_emb oo meet_defl\<cdot>a oo defl_prj" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
660 |
apply (induct a rule: defl.principal_induct, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
661 |
apply (subst defl_deflation_def) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
662 |
apply (subst defl.extension_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
663 |
apply (simp add: below_fin_defl_def Abs_fin_defl_inverse |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
664 |
ep_pair.finite_deflation_e_d_p ep_pair_defl |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
665 |
finite_deflation_meet_defl monofun_cfun) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
666 |
apply (simp add: cast_defl_principal |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
667 |
below_fin_defl_def Abs_fin_defl_inverse |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
668 |
ep_pair.finite_deflation_e_d_p ep_pair_defl |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
669 |
finite_deflation_meet_defl monofun_cfun) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
670 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
671 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
672 |
definition defl_map_emb :: "'a::domain defl \<rightarrow> udom defl" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
673 |
where "defl_map_emb = defl_fun1 emb prj ID" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
674 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
675 |
definition defl_map_prj :: "udom defl \<rightarrow> 'a::domain defl" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
676 |
where "defl_map_prj = defl.extension (\<lambda>a. defl_principal (Abs_fin_defl (prj oo cast\<cdot>(meet_defl\<cdot>DEFL('a)\<cdot>(defl_principal a)) oo emb)))" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
677 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
678 |
lemma defl_map_emb_principal: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
679 |
"defl_map_emb\<cdot>(defl_principal a) = |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
680 |
defl_principal (Abs_fin_defl (emb oo Rep_fin_defl a oo prj))" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
681 |
unfolding defl_map_emb_def defl_fun1_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
682 |
apply (subst defl.extension_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
683 |
apply (rule defl.principal_mono) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
684 |
apply (simp add: below_fin_defl_def Abs_fin_defl_inverse monofun_cfun |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
685 |
domain.finite_deflation_e_d_p finite_deflation_Rep_fin_defl) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
686 |
apply simp |
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
687 |
done |
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
688 |
|
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
689 |
lemma defl_map_prj_principal: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
690 |
"(defl_map_prj\<cdot>(defl_principal a) :: 'a::domain defl) = |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
691 |
defl_principal (Abs_fin_defl (prj oo cast\<cdot>(meet_defl\<cdot>DEFL('a)\<cdot>(defl_principal a)) oo emb))" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
692 |
unfolding defl_map_prj_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
693 |
apply (rule defl.extension_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
694 |
apply (rule defl.principal_mono) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
695 |
apply (simp add: below_fin_defl_def) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
696 |
apply (subst Abs_fin_defl_inverse, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
697 |
apply (rule domain.finite_deflation_p_d_e) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
698 |
apply (rule finite_deflation_cast) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
699 |
apply (simp add: compact_meet_defl2) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
700 |
apply (subst emb_prj) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
701 |
apply (intro monofun_cfun below_refl meet_defl_below1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
702 |
apply (subst Abs_fin_defl_inverse, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
703 |
apply (rule domain.finite_deflation_p_d_e) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
704 |
apply (rule finite_deflation_cast) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
705 |
apply (simp add: compact_meet_defl2) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
706 |
apply (subst emb_prj) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
707 |
apply (intro monofun_cfun below_refl meet_defl_below1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
708 |
apply (simp add: monofun_cfun below_fin_defl_def) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
709 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
710 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
711 |
lemma defl_map_prj_defl_map_emb: "defl_map_prj\<cdot>(defl_map_emb\<cdot>d) = d" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
712 |
apply (rule cast_eq_imp_eq) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
713 |
apply (induct_tac d rule: defl.principal_induct, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
714 |
apply (subst defl_map_emb_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
715 |
apply (subst defl_map_prj_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
716 |
apply (simp add: cast_defl_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
717 |
apply (subst Abs_fin_defl_inverse, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
718 |
apply (rule domain.finite_deflation_p_d_e) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
719 |
apply (rule finite_deflation_cast) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
720 |
apply (simp add: compact_meet_defl2) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
721 |
apply (subst emb_prj) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
722 |
apply (intro monofun_cfun below_refl meet_defl_below1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
723 |
apply (subst meet_defl_eq2) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
724 |
apply (rule cast_below_imp_below) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
725 |
apply (simp add: cast_DEFL) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
726 |
apply (simp add: cast_defl_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
727 |
apply (subst Abs_fin_defl_inverse, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
728 |
apply (rule domain.finite_deflation_e_d_p) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
729 |
apply (rule finite_deflation_Rep_fin_defl) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
730 |
apply (rule cfun_belowI, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
731 |
apply (rule Rep_fin_defl.below) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
732 |
apply (simp add: cast_defl_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
733 |
apply (subst Abs_fin_defl_inverse, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
734 |
apply (rule domain.finite_deflation_e_d_p) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
735 |
apply (rule finite_deflation_Rep_fin_defl) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
736 |
apply (simp add: cfun_eqI) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
737 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
738 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
739 |
lemma defl_map_emb_defl_map_prj: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
740 |
"defl_map_emb\<cdot>(defl_map_prj\<cdot>d :: 'a defl) = meet_defl\<cdot>DEFL('a)\<cdot>d" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
741 |
apply (induct_tac d rule: defl.principal_induct, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
742 |
apply (subst defl_map_prj_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
743 |
apply (subst defl_map_emb_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
744 |
apply (subst Abs_fin_defl_inverse, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
745 |
apply (rule domain.finite_deflation_p_d_e) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
746 |
apply (rule finite_deflation_cast) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
747 |
apply (simp add: compact_meet_defl2) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
748 |
apply (subst emb_prj) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
749 |
apply (intro monofun_cfun below_refl meet_defl_below1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
750 |
apply (rule cast_eq_imp_eq) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
751 |
apply (subst cast_defl_principal) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
752 |
apply (simp add: cfcomp1 emb_prj) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
753 |
apply (subst deflation_below_comp2 [OF deflation_cast deflation_cast]) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
754 |
apply (rule monofun_cfun_arg, rule meet_defl_below1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
755 |
apply (subst deflation_below_comp1 [OF deflation_cast deflation_cast]) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
756 |
apply (rule monofun_cfun_arg, rule meet_defl_below1) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
757 |
apply (simp add: eta_cfun) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
758 |
apply (rule Abs_fin_defl_inverse, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
759 |
apply (rule finite_deflation_cast) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
760 |
apply (rule compact_meet_defl2, simp) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
761 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
762 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
763 |
lemma ep_pair_defl_map_emb_defl_map_prj: |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
764 |
"ep_pair defl_map_emb defl_map_prj" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
765 |
apply (rule ep_pair.intro) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
766 |
apply (rule defl_map_prj_defl_map_emb) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
767 |
apply (simp add: defl_map_emb_defl_map_prj) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
768 |
apply (rule meet_defl_below2) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
769 |
done |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
770 |
|
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
771 |
instantiation defl :: ("domain") "domain" |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
772 |
begin |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
773 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
774 |
definition |
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
775 |
"emb = defl_emb oo defl_map_emb" |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
776 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
777 |
definition |
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
778 |
"prj = defl_map_prj oo defl_prj" |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
779 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
780 |
definition |
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
781 |
"defl (t::'a defl itself) = defl_defl\<cdot>DEFL('a)" |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
782 |
|
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40002
diff
changeset
|
783 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
784 |
"(liftemb :: 'a defl u \<rightarrow> udom u) = u_map\<cdot>emb" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40002
diff
changeset
|
785 |
|
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40002
diff
changeset
|
786 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
787 |
"(liftprj :: udom u \<rightarrow> 'a defl u) = u_map\<cdot>prj" |
40491
6de5839e2fb3
add 'predomain' class: unpointed version of bifinite
huffman
parents:
40002
diff
changeset
|
788 |
|
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
789 |
definition |
41436 | 790 |
"liftdefl (t::'a defl itself) = liftdefl_of\<cdot>DEFL('a defl)" |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
791 |
|
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
792 |
instance proof |
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
793 |
show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a defl)" |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
794 |
unfolding emb_defl_def prj_defl_def |
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
795 |
apply (rule ep_pair_comp [OF _ ep_pair_defl]) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
796 |
apply (rule ep_pair_defl_map_emb_defl_map_prj) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
797 |
done |
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
798 |
show "cast\<cdot>DEFL('a defl) = emb oo (prj :: udom \<rightarrow> 'a defl)" |
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
799 |
unfolding defl_defl_def emb_defl_def prj_defl_def |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
800 |
by (simp add: cast_defl_defl cfcomp1 defl_map_emb_defl_map_prj) |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41290
diff
changeset
|
801 |
qed (fact liftemb_defl_def liftprj_defl_def liftdefl_defl_def)+ |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
802 |
|
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
803 |
end |
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
804 |
|
41533
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
805 |
lemma DEFL_defl [domain_defl_simps]: "DEFL('a defl) = defl_defl\<cdot>DEFL('a)" |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
806 |
by (rule defl_defl_def) |
869b5ea478b0
proper 'domain' class instance for 'a defl, with deflation combinator
huffman
parents:
41477
diff
changeset
|
807 |
|
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
diff
changeset
|
808 |
end |