11 |
11 |
12 subsection {* Basis preorder *} |
12 subsection {* Basis preorder *} |
13 |
13 |
14 definition |
14 definition |
15 upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<sharp>" 50) where |
15 upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<sharp>" 50) where |
16 "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. compact_le x y)" |
16 "upper_le = (\<lambda>u v. \<forall>y\<in>Rep_pd_basis v. \<exists>x\<in>Rep_pd_basis u. x \<sqsubseteq> y)" |
17 |
17 |
18 lemma upper_le_refl [simp]: "t \<le>\<sharp> t" |
18 lemma upper_le_refl [simp]: "t \<le>\<sharp> t" |
19 unfolding upper_le_def by (fast intro: compact_le_refl) |
19 unfolding upper_le_def by fast |
20 |
20 |
21 lemma upper_le_trans: "\<lbrakk>t \<le>\<sharp> u; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> t \<le>\<sharp> v" |
21 lemma upper_le_trans: "\<lbrakk>t \<le>\<sharp> u; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> t \<le>\<sharp> v" |
22 unfolding upper_le_def |
22 unfolding upper_le_def |
23 apply (rule ballI) |
23 apply (rule ballI) |
24 apply (drule (1) bspec, erule bexE) |
24 apply (drule (1) bspec, erule bexE) |
25 apply (drule (1) bspec, erule bexE) |
25 apply (drule (1) bspec, erule bexE) |
26 apply (erule rev_bexI) |
26 apply (erule rev_bexI) |
27 apply (erule (1) compact_le_trans) |
27 apply (erule (1) trans_less) |
28 done |
28 done |
29 |
29 |
30 interpretation upper_le: preorder [upper_le] |
30 interpretation upper_le: preorder [upper_le] |
31 by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans) |
31 by (rule preorder.intro, rule upper_le_refl, rule upper_le_trans) |
32 |
32 |
33 lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t" |
33 lemma upper_le_minimal [simp]: "PDUnit compact_bot \<le>\<sharp> t" |
34 unfolding upper_le_def Rep_PDUnit by simp |
34 unfolding upper_le_def Rep_PDUnit by simp |
35 |
35 |
36 lemma PDUnit_upper_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<sharp> PDUnit y" |
36 lemma PDUnit_upper_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<sharp> PDUnit y" |
37 unfolding upper_le_def Rep_PDUnit by simp |
37 unfolding upper_le_def Rep_PDUnit by simp |
38 |
38 |
39 lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v" |
39 lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v" |
40 unfolding upper_le_def Rep_PDPlus by fast |
40 unfolding upper_le_def Rep_PDPlus by fast |
41 |
41 |
42 lemma PDPlus_upper_less: "PDPlus t u \<le>\<sharp> t" |
42 lemma PDPlus_upper_less: "PDPlus t u \<le>\<sharp> t" |
43 unfolding upper_le_def Rep_PDPlus by (fast intro: compact_le_refl) |
43 unfolding upper_le_def Rep_PDPlus by fast |
44 |
44 |
45 lemma upper_le_PDUnit_PDUnit_iff [simp]: |
45 lemma upper_le_PDUnit_PDUnit_iff [simp]: |
46 "(PDUnit a \<le>\<sharp> PDUnit b) = compact_le a b" |
46 "(PDUnit a \<le>\<sharp> PDUnit b) = a \<sqsubseteq> b" |
47 unfolding upper_le_def Rep_PDUnit by fast |
47 unfolding upper_le_def Rep_PDUnit by fast |
48 |
48 |
49 lemma upper_le_PDPlus_PDUnit_iff: |
49 lemma upper_le_PDPlus_PDUnit_iff: |
50 "(PDPlus t u \<le>\<sharp> PDUnit a) = (t \<le>\<sharp> PDUnit a \<or> u \<le>\<sharp> PDUnit a)" |
50 "(PDPlus t u \<le>\<sharp> PDUnit a) = (t \<le>\<sharp> PDUnit a \<or> u \<le>\<sharp> PDUnit a)" |
51 unfolding upper_le_def Rep_PDPlus Rep_PDUnit by fast |
51 unfolding upper_le_def Rep_PDPlus Rep_PDUnit by fast |
53 lemma upper_le_PDPlus_iff: "(t \<le>\<sharp> PDPlus u v) = (t \<le>\<sharp> u \<and> t \<le>\<sharp> v)" |
53 lemma upper_le_PDPlus_iff: "(t \<le>\<sharp> PDPlus u v) = (t \<le>\<sharp> u \<and> t \<le>\<sharp> v)" |
54 unfolding upper_le_def Rep_PDPlus by fast |
54 unfolding upper_le_def Rep_PDPlus by fast |
55 |
55 |
56 lemma upper_le_induct [induct set: upper_le]: |
56 lemma upper_le_induct [induct set: upper_le]: |
57 assumes le: "t \<le>\<sharp> u" |
57 assumes le: "t \<le>\<sharp> u" |
58 assumes 1: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)" |
58 assumes 1: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)" |
59 assumes 2: "\<And>t u a. P t (PDUnit a) \<Longrightarrow> P (PDPlus t u) (PDUnit a)" |
59 assumes 2: "\<And>t u a. P t (PDUnit a) \<Longrightarrow> P (PDPlus t u) (PDUnit a)" |
60 assumes 3: "\<And>t u v. \<lbrakk>P t u; P t v\<rbrakk> \<Longrightarrow> P t (PDPlus u v)" |
60 assumes 3: "\<And>t u v. \<lbrakk>P t u; P t v\<rbrakk> \<Longrightarrow> P t (PDPlus u v)" |
61 shows "P t u" |
61 shows "P t u" |
62 using le apply (induct u arbitrary: t rule: pd_basis_induct) |
62 using le apply (induct u arbitrary: t rule: pd_basis_induct) |
63 apply (erule rev_mp) |
63 apply (erule rev_mp) |
113 apply (rule Abs_upper_pd_inverse [simplified]) |
113 apply (rule Abs_upper_pd_inverse [simplified]) |
114 apply (rule upper_le.ideal_principal) |
114 apply (rule upper_le.ideal_principal) |
115 done |
115 done |
116 |
116 |
117 interpretation upper_pd: |
117 interpretation upper_pd: |
118 bifinite_basis [upper_le upper_principal Rep_upper_pd approx_pd] |
118 bifinite_basis [upper_le approx_pd upper_principal Rep_upper_pd] |
119 apply unfold_locales |
119 apply unfold_locales |
120 apply (rule ideal_Rep_upper_pd) |
|
121 apply (rule cont_Rep_upper_pd) |
|
122 apply (rule Rep_upper_principal) |
|
123 apply (simp only: less_upper_pd_def less_set_def) |
|
124 apply (rule approx_pd_upper_le) |
120 apply (rule approx_pd_upper_le) |
125 apply (rule approx_pd_idem) |
121 apply (rule approx_pd_idem) |
126 apply (erule approx_pd_upper_mono) |
122 apply (erule approx_pd_upper_mono) |
127 apply (rule approx_pd_upper_mono1, simp) |
123 apply (rule approx_pd_upper_mono1, simp) |
128 apply (rule finite_range_approx_pd) |
124 apply (rule finite_range_approx_pd) |
129 apply (rule ex_approx_pd_eq) |
125 apply (rule ex_approx_pd_eq) |
|
126 apply (rule ideal_Rep_upper_pd) |
|
127 apply (rule cont_Rep_upper_pd) |
|
128 apply (rule Rep_upper_principal) |
|
129 apply (simp only: less_upper_pd_def less_set_def) |
130 done |
130 done |
131 |
131 |
132 lemma upper_principal_less_iff [simp]: |
132 lemma upper_principal_less_iff [simp]: |
133 "(upper_principal t \<sqsubseteq> upper_principal u) = (t \<le>\<sharp> u)" |
133 "(upper_principal t \<sqsubseteq> upper_principal u) = (t \<le>\<sharp> u)" |
134 unfolding less_upper_pd_def Rep_upper_principal less_set_def |
134 unfolding less_upper_pd_def Rep_upper_principal less_set_def |