1 theory SigmaEx |
|
2 imports Nominal "../Quotient" "../Quotient_List" "../Quotient_Product" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 datatype robj = |
|
8 rVar "name" |
|
9 | rObj "(string \<times> rmethod) list" |
|
10 | rInv "robj" "string" |
|
11 | rUpd "robj" "string" "rmethod" |
|
12 and rmethod = |
|
13 rSig "name" "robj" |
|
14 |
|
15 inductive |
|
16 alpha_obj :: "robj \<Rightarrow> robj \<Rightarrow> bool" ("_ \<approx>o _" [100, 100] 100) |
|
17 and alpha_method :: "rmethod \<Rightarrow> rmethod \<Rightarrow> bool" ("_ \<approx>m _" [100, 100] 100) |
|
18 where |
|
19 a1: "a = b \<Longrightarrow> (rVar a) \<approx>o (rVar b)" |
|
20 | a2: "rObj [] \<approx>o rObj []" |
|
21 | a3: "rObj t1 \<approx>o rObj t2 \<Longrightarrow> m1 \<approx>m r2 \<Longrightarrow> rObj ((l1, m1) # t1) \<approx>o rObj ((l2, m2) # t2)" |
|
22 | a4: "x \<approx>o y \<Longrightarrow> rInv x l1 \<approx>o rInv y l2" |
|
23 | a5: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>o s \<and> (pi \<bullet> a) = b) |
|
24 \<Longrightarrow> rSig a t \<approx>m rSig b s" |
|
25 |
|
26 lemma alpha_equivps: |
|
27 shows "equivp alpha_obj" |
|
28 and "equivp alpha_method" |
|
29 sorry |
|
30 |
|
31 quotient_type |
|
32 obj = robj / alpha_obj |
|
33 and method = rmethod / alpha_method |
|
34 by (auto intro: alpha_equivps) |
|
35 |
|
36 quotient_definition |
|
37 "Var :: name \<Rightarrow> obj" |
|
38 is |
|
39 "rVar" |
|
40 |
|
41 quotient_definition |
|
42 "Obj :: (string \<times> method) list \<Rightarrow> obj" |
|
43 is |
|
44 "rObj" |
|
45 |
|
46 quotient_definition |
|
47 "Inv :: obj \<Rightarrow> string \<Rightarrow> obj" |
|
48 is |
|
49 "rInv" |
|
50 |
|
51 quotient_definition |
|
52 "Upd :: obj \<Rightarrow> string \<Rightarrow> method \<Rightarrow> obj" |
|
53 is |
|
54 "rUpd" |
|
55 |
|
56 quotient_definition |
|
57 "Sig :: name \<Rightarrow> obj \<Rightarrow> method" |
|
58 is |
|
59 "rSig" |
|
60 |
|
61 overloading |
|
62 perm_obj \<equiv> "perm :: 'x prm \<Rightarrow> obj \<Rightarrow> obj" (unchecked) |
|
63 perm_method \<equiv> "perm :: 'x prm \<Rightarrow> method \<Rightarrow> method" (unchecked) |
|
64 begin |
|
65 |
|
66 quotient_definition |
|
67 "perm_obj :: 'x prm \<Rightarrow> obj \<Rightarrow> obj" |
|
68 is |
|
69 "(perm::'x prm \<Rightarrow> robj \<Rightarrow> robj)" |
|
70 |
|
71 quotient_definition |
|
72 "perm_method :: 'x prm \<Rightarrow> method \<Rightarrow> method" |
|
73 is |
|
74 "(perm::'x prm \<Rightarrow> rmethod \<Rightarrow> rmethod)" |
|
75 |
|
76 end |
|
77 |
|
78 |
|
79 |
|
80 lemma tolift: |
|
81 "\<forall> fvar. |
|
82 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
83 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =). |
|
84 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =). |
|
85 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
86 \<forall> fnil. |
|
87 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
|
88 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
|
89 |
|
90 Ex1 (\<lambda>x. |
|
91 (x \<in> (Respects (prod_rel (alpha_obj ===> op =) |
|
92 (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) |
|
93 (prod_rel ((prod_rel (op =) alpha_method) ===> op =) |
|
94 (alpha_method ===> op =) |
|
95 ) |
|
96 )))) \<and> |
|
97 (\<lambda> (hom_o\<Colon>robj \<Rightarrow> 'a, hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b, hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c, hom_m\<Colon>rmethod \<Rightarrow> 'd). |
|
98 |
|
99 ((\<forall>x. hom_o (rVar x) = fvar x) \<and> |
|
100 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
|
101 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
|
102 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
103 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
104 (hom_d [] = fnil) \<and> |
|
105 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
106 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
107 )) x) " |
|
108 sorry |
|
109 |
|
110 lemma test_to: "Ex1 (\<lambda>x. (x \<in> (Respects alpha_obj)) \<and> P x)" |
|
111 ML_prf {* prop_of (#goal (Isar.goal ())) *} |
|
112 sorry |
|
113 lemma test_tod: "Ex1 (P :: obj \<Rightarrow> bool)" |
|
114 apply (lifting test_to) |
|
115 done |
|
116 |
|
117 |
|
118 |
|
119 |
|
120 (*syntax |
|
121 "_expttrn" :: "pttrn => bool => bool" ("(3\<exists>\<exists> _./ _)" [0, 10] 10) |
|
122 |
|
123 translations |
|
124 "\<exists>\<exists> x. P" == "Ex (%x. P)" |
|
125 *) |
|
126 |
|
127 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar" |
|
128 by (simp add: a1) |
|
129 |
|
130 lemma robj_rsp[quot_respect]: "(list_rel (prod_rel op = alpha_method) ===> alpha_obj) rObj rObj" |
|
131 sorry |
|
132 lemma rinv_rsp[quot_respect]: "(alpha_obj ===> op = ===> alpha_obj) rInv rInv" |
|
133 sorry |
|
134 lemma rupd_rsp[quot_respect]: "(alpha_obj ===> op = ===> alpha_method ===> alpha_obj) rUpd rUpd" |
|
135 sorry |
|
136 lemma rsig_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_method) rSig rSig" |
|
137 sorry |
|
138 lemma operm_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_obj) op \<bullet> op \<bullet>" |
|
139 sorry |
|
140 |
|
141 |
|
142 lemma bex1_bex1reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))" |
|
143 apply (simp add: Ex1_def Bex1_rel_def in_respects) |
|
144 apply clarify |
|
145 apply auto |
|
146 apply (rule bexI) |
|
147 apply assumption |
|
148 apply (simp add: in_respects) |
|
149 apply (simp add: in_respects) |
|
150 apply auto |
|
151 done |
|
152 |
|
153 lemma liftd: " |
|
154 Ex1 (\<lambda>(hom_o, hom_d, hom_e, hom_m). |
|
155 |
|
156 (\<forall>x. hom_o (Var x) = fvar x) \<and> |
|
157 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and> |
|
158 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and> |
|
159 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
160 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
161 (hom_d [] = fnil) \<and> |
|
162 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
163 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
164 )" |
|
165 apply (lifting tolift) |
|
166 done |
|
167 |
|
168 lemma tolift': |
|
169 "\<forall> fvar. |
|
170 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
171 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =). |
|
172 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =). |
|
173 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
174 \<forall> fnil. |
|
175 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
|
176 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
|
177 |
|
178 \<exists> hom_o\<Colon>robj \<Rightarrow> 'a \<in> Respects (alpha_obj ===> op =). |
|
179 \<exists> hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b \<in> Respects (list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
180 \<exists> hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c \<in> Respects ((prod_rel (op =) alpha_method) ===> op =). |
|
181 \<exists> hom_m\<Colon>rmethod \<Rightarrow> 'd \<in> Respects (alpha_method ===> op =). |
|
182 ( |
|
183 (\<forall>x. hom_o (rVar x) = fvar x) \<and> |
|
184 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
|
185 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
|
186 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
187 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
188 (hom_d [] = fnil) \<and> |
|
189 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
190 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
191 )" |
|
192 sorry |
|
193 |
|
194 lemma liftd': " |
|
195 \<exists>hom_o. \<exists>hom_d. \<exists>hom_e. \<exists>hom_m. |
|
196 ( |
|
197 (\<forall>x. hom_o (Var x) = fvar x) \<and> |
|
198 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and> |
|
199 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and> |
|
200 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
201 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
202 (hom_d [] = fnil) \<and> |
|
203 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
204 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
205 )" |
|
206 apply (lifting tolift') |
|
207 done |
|
208 |
|
209 lemma tolift'': |
|
210 "\<forall> fvar. |
|
211 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
212 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =). |
|
213 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =). |
|
214 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
215 \<forall> fnil. |
|
216 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
|
217 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
|
218 |
|
219 Bex1_rel (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a . |
|
220 Bex1_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b. |
|
221 Bex1_rel ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c. |
|
222 Bex1_rel (alpha_method ===> op =) (\<lambda>hom_m\<Colon>rmethod \<Rightarrow> 'd. |
|
223 ( |
|
224 (\<forall>x. hom_o (rVar x) = fvar x) \<and> |
|
225 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
|
226 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
|
227 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
228 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
229 (hom_d [] = fnil) \<and> |
|
230 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
231 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
232 ) |
|
233 ))))" |
|
234 sorry |
|
235 |
|
236 lemma liftd'': " |
|
237 \<exists>!hom_o. \<exists>!hom_d. \<exists>!hom_e. \<exists>!hom_m. |
|
238 ( |
|
239 (\<forall>x. hom_o (Var x) = fvar x) \<and> |
|
240 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and> |
|
241 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and> |
|
242 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
243 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
244 (hom_d [] = fnil) \<and> |
|
245 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
246 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
247 )" |
|
248 apply (lifting tolift'') |
|
249 done |
|
250 |
|
251 |
|
252 end |
|
253 |
|