|
1 theory SigmaEx |
|
2 imports Nominal "../QuotMain" "../QuotList" "../QuotProd" |
|
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 (* Need to fix it, just 2 random rules *) |
|
16 inductive |
|
17 alpha_obj :: "robj \<Rightarrow> robj \<Rightarrow> bool" ("_ \<approx>o _" [100, 100] 100) |
|
18 and alpha_method :: "rmethod \<Rightarrow> rmethod \<Rightarrow> bool" ("_ \<approx>m _" [100, 100] 100) |
|
19 where |
|
20 a1: "a = b \<Longrightarrow> (rVar a) \<approx>o (rVar b)" |
|
21 | a2: "a = b \<and> c = d \<Longrightarrow> rSig a c \<approx>m rSig b d" |
|
22 |
|
23 lemma alpha_equivps: |
|
24 shows "equivp alpha_obj" |
|
25 and "equivp alpha_method" |
|
26 sorry |
|
27 |
|
28 quotient_type |
|
29 obj = robj / alpha_obj |
|
30 and method = rmethod / alpha_method |
|
31 by (auto intro: alpha_equivps) |
|
32 |
|
33 quotient_definition |
|
34 "Var :: name \<Rightarrow> obj" |
|
35 as |
|
36 "rVar" |
|
37 |
|
38 quotient_definition |
|
39 "Obj :: (string \<times> method) list \<Rightarrow> obj" |
|
40 as |
|
41 "rObj" |
|
42 |
|
43 quotient_definition |
|
44 "Inv :: obj \<Rightarrow> string \<Rightarrow> obj" |
|
45 as |
|
46 "rInv" |
|
47 |
|
48 quotient_definition |
|
49 "Upd :: obj \<Rightarrow> string \<Rightarrow> method \<Rightarrow> obj" |
|
50 as |
|
51 "rUpd" |
|
52 |
|
53 quotient_definition |
|
54 "Sig :: name \<Rightarrow> obj \<Rightarrow> method" |
|
55 as |
|
56 "rSig" |
|
57 |
|
58 overloading |
|
59 perm_obj \<equiv> "perm :: 'x prm \<Rightarrow> obj \<Rightarrow> obj" (unchecked) |
|
60 perm_method \<equiv> "perm :: 'x prm \<Rightarrow> method \<Rightarrow> method" (unchecked) |
|
61 begin |
|
62 |
|
63 quotient_definition |
|
64 "perm_obj :: 'x prm \<Rightarrow> obj \<Rightarrow> obj" |
|
65 as |
|
66 "(perm::'x prm \<Rightarrow> robj \<Rightarrow> robj)" |
|
67 |
|
68 quotient_definition |
|
69 "perm_method :: 'x prm \<Rightarrow> method \<Rightarrow> method" |
|
70 as |
|
71 "(perm::'x prm \<Rightarrow> rmethod \<Rightarrow> rmethod)" |
|
72 |
|
73 end |
|
74 |
|
75 lemma tolift: |
|
76 "\<forall> fvar. |
|
77 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
78 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =). |
|
79 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =). |
|
80 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
81 \<forall> fnil. |
|
82 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
|
83 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
|
84 |
|
85 \<exists> (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) |
|
86 \<in> Respects |
|
87 (prod_rel (alpha_obj ===> op =) |
|
88 (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) |
|
89 (prod_rel ((prod_rel (op =) alpha_method) ===> op =) |
|
90 (alpha_method ===> op =) |
|
91 ) |
|
92 ) |
|
93 ). |
|
94 |
|
95 ( |
|
96 (\<forall>x. hom_o (rVar x) = fvar x) \<and> |
|
97 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
|
98 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
|
99 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
100 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
101 (hom_d [] = fnil) \<and> |
|
102 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
103 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
104 )" |
|
105 sorry |
|
106 |
|
107 syntax |
|
108 "_expttrn" :: "pttrn => bool => bool" ("(3\<exists>\<exists> _./ _)" [0, 10] 10) |
|
109 |
|
110 translations |
|
111 "\<exists>\<exists> x. P" == "Ex (%x. P)" |
|
112 |
|
113 lemma split_rsp[quot_respect]: "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split" |
|
114 by auto |
|
115 |
|
116 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar" |
|
117 by (simp add: a1) |
|
118 |
|
119 lemma robj_rsp[quot_respect]: "(list_rel (prod_rel op = alpha_method) ===> alpha_obj) rObj rObj" |
|
120 sorry |
|
121 lemma rinv_rsp[quot_respect]: "(alpha_obj ===> op = ===> alpha_obj) rInv rInv" |
|
122 sorry |
|
123 lemma rupd_rsp[quot_respect]: "(alpha_obj ===> op = ===> alpha_method ===> alpha_obj) rUpd rUpd" |
|
124 sorry |
|
125 lemma rsig_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_method) rSig rSig" |
|
126 sorry |
|
127 lemma operm_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_obj) op \<bullet> op \<bullet>" |
|
128 sorry |
|
129 |
|
130 lemma liftd: " |
|
131 \<exists>\<exists>(hom_o, (hom_d, (hom_e, hom_m))). |
|
132 ( |
|
133 (\<forall>x. hom_o (Var x) = fvar x) \<and> |
|
134 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and> |
|
135 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and> |
|
136 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
137 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
138 (hom_d [] = fnil) \<and> |
|
139 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
140 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
141 )" |
|
142 apply (lifting tolift) |
|
143 apply (regularize) |
|
144 prefer 2 |
|
145 apply cleaning |
|
146 apply simp |
|
147 sorry |
|
148 |
|
149 lemma tolift': |
|
150 "\<forall> fvar. |
|
151 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
152 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =). |
|
153 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =). |
|
154 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
155 \<forall> fnil. |
|
156 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =). |
|
157 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =). |
|
158 |
|
159 \<exists> hom_o\<Colon>robj \<Rightarrow> 'a \<in> Respects (alpha_obj ===> op =). |
|
160 \<exists> hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b \<in> Respects (list_rel (prod_rel (op =) alpha_method) ===> op =). |
|
161 \<exists> hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c \<in> Respects ((prod_rel (op =) alpha_method) ===> op =). |
|
162 \<exists> hom_m\<Colon>rmethod \<Rightarrow> 'd \<in> Respects (alpha_method ===> op =). |
|
163 ( |
|
164 (\<forall>x. hom_o (rVar x) = fvar x) \<and> |
|
165 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and> |
|
166 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and> |
|
167 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
168 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
169 (hom_d [] = fnil) \<and> |
|
170 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
171 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
172 )" |
|
173 sorry |
|
174 |
|
175 lemma liftd': " |
|
176 \<exists>hom_o. \<exists>hom_d. \<exists>hom_e. \<exists>hom_m. |
|
177 ( |
|
178 (\<forall>x. hom_o (Var x) = fvar x) \<and> |
|
179 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and> |
|
180 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and> |
|
181 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and> |
|
182 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and> |
|
183 (hom_d [] = fnil) \<and> |
|
184 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and> |
|
185 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
|
186 )" |
|
187 apply (lifting tolift') |
|
188 done |
|
189 |
|
190 end |
|
191 |