905
+ − 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 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)"
914
+ − 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"
905
+ − 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 as
+ − 39 "rVar"
+ − 40
+ − 41 quotient_definition
+ − 42 "Obj :: (string \<times> method) list \<Rightarrow> obj"
+ − 43 as
+ − 44 "rObj"
+ − 45
+ − 46 quotient_definition
+ − 47 "Inv :: obj \<Rightarrow> string \<Rightarrow> obj"
+ − 48 as
+ − 49 "rInv"
+ − 50
+ − 51 quotient_definition
+ − 52 "Upd :: obj \<Rightarrow> string \<Rightarrow> method \<Rightarrow> obj"
+ − 53 as
+ − 54 "rUpd"
+ − 55
+ − 56 quotient_definition
+ − 57 "Sig :: name \<Rightarrow> obj \<Rightarrow> method"
+ − 58 as
+ − 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 as
+ − 69 "(perm::'x prm \<Rightarrow> robj \<Rightarrow> robj)"
+ − 70
+ − 71 quotient_definition
+ − 72 "perm_method :: 'x prm \<Rightarrow> method \<Rightarrow> method"
+ − 73 as
+ − 74 "(perm::'x prm \<Rightarrow> rmethod \<Rightarrow> rmethod)"
+ − 75
+ − 76 end
+ − 77
+ − 78 lemma tolift:
+ − 79 "\<forall> fvar.
+ − 80 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
+ − 81 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =).
+ − 82 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =).
+ − 83 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
+ − 84 \<forall> fnil.
+ − 85 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
+ − 86 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).
+ − 87
+ − 88 \<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)
+ − 89 \<in> Respects
+ − 90 (prod_rel (alpha_obj ===> op =)
+ − 91 (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =)
+ − 92 (prod_rel ((prod_rel (op =) alpha_method) ===> op =)
+ − 93 (alpha_method ===> op =)
+ − 94 )
+ − 95 )
+ − 96 ).
+ − 97
+ − 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 )"
+ − 108 sorry
+ − 109
+ − 110 syntax
+ − 111 "_expttrn" :: "pttrn => bool => bool" ("(3\<exists>\<exists> _./ _)" [0, 10] 10)
+ − 112
+ − 113 translations
+ − 114 "\<exists>\<exists> x. P" == "Ex (%x. P)"
+ − 115
+ − 116 lemma split_rsp[quot_respect]: "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split"
+ − 117 by auto
+ − 118
+ − 119 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar"
+ − 120 by (simp add: a1)
+ − 121
+ − 122 lemma robj_rsp[quot_respect]: "(list_rel (prod_rel op = alpha_method) ===> alpha_obj) rObj rObj"
+ − 123 sorry
+ − 124 lemma rinv_rsp[quot_respect]: "(alpha_obj ===> op = ===> alpha_obj) rInv rInv"
+ − 125 sorry
+ − 126 lemma rupd_rsp[quot_respect]: "(alpha_obj ===> op = ===> alpha_method ===> alpha_obj) rUpd rUpd"
+ − 127 sorry
+ − 128 lemma rsig_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_method) rSig rSig"
+ − 129 sorry
+ − 130 lemma operm_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_obj) op \<bullet> op \<bullet>"
+ − 131 sorry
+ − 132
+ − 133 lemma liftd: "
+ − 134 \<exists>\<exists>(hom_o, (hom_d, (hom_e, hom_m))).
+ − 135 (
+ − 136 (\<forall>x. hom_o (Var x) = fvar x) \<and>
+ − 137 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and>
+ − 138 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and>
+ − 139 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
+ − 140 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
+ − 141 (hom_d [] = fnil) \<and>
+ − 142 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
+ − 143 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
+ − 144 )"
+ − 145 apply (lifting tolift)
+ − 146 apply (regularize)
908
+ − 147 apply (simp)
905
+ − 148 prefer 2
+ − 149 apply cleaning
+ − 150 apply simp
+ − 151 sorry
+ − 152
+ − 153 lemma tolift':
+ − 154 "\<forall> fvar.
+ − 155 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
+ − 156 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =).
+ − 157 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =).
+ − 158 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
+ − 159 \<forall> fnil.
+ − 160 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
+ − 161 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).
+ − 162
+ − 163 \<exists> hom_o\<Colon>robj \<Rightarrow> 'a \<in> Respects (alpha_obj ===> op =).
+ − 164 \<exists> hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b \<in> Respects (list_rel (prod_rel (op =) alpha_method) ===> op =).
+ − 165 \<exists> hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c \<in> Respects ((prod_rel (op =) alpha_method) ===> op =).
+ − 166 \<exists> hom_m\<Colon>rmethod \<Rightarrow> 'd \<in> Respects (alpha_method ===> op =).
+ − 167 (
+ − 168 (\<forall>x. hom_o (rVar x) = fvar x) \<and>
+ − 169 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and>
+ − 170 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and>
+ − 171 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
+ − 172 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
+ − 173 (hom_d [] = fnil) \<and>
+ − 174 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
+ − 175 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
+ − 176 )"
+ − 177 sorry
+ − 178
+ − 179 lemma liftd': "
+ − 180 \<exists>hom_o. \<exists>hom_d. \<exists>hom_e. \<exists>hom_m.
+ − 181 (
+ − 182 (\<forall>x. hom_o (Var x) = fvar x) \<and>
+ − 183 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and>
+ − 184 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and>
+ − 185 (\<forall>a l m. hom_o (Upd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
+ − 186 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
+ − 187 (hom_d [] = fnil) \<and>
+ − 188 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
+ − 189 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
+ − 190 )"
+ − 191 apply (lifting tolift')
+ − 192 done
+ − 193
912
+ − 194 lemma tolift'':
+ − 195 "\<forall> fvar.
+ − 196 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
+ − 197 \<forall> fnvk\<in>Respects (op = ===> alpha_obj ===> op =).
+ − 198 \<forall> fupd\<in>Respects (op = ===> op = ===> alpha_obj ===> op = ===> alpha_method ===> op =).
+ − 199 \<forall> fcns\<in>Respects (op = ===> op = ===> prod_rel (op =) alpha_method ===> list_rel (prod_rel (op =) alpha_method) ===> op =).
+ − 200 \<forall> fnil.
+ − 201 \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
+ − 202 \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).
+ − 203
+ − 204 Bexeq (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a .
+ − 205 Bexeq (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b.
+ − 206 Bexeq ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c.
+ − 207 Bexeq (alpha_method ===> op =) (\<lambda>hom_m\<Colon>rmethod \<Rightarrow> 'd.
+ − 208 (
+ − 209 (\<forall>x. hom_o (rVar x) = fvar x) \<and>
+ − 210 (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and>
+ − 211 (\<forall>a l. hom_o (rInv a l) = fnvk (hom_o a) a l) \<and>
+ − 212 (\<forall>a l m. hom_o (rUpd a l m) = fupd (hom_o a) (hom_m m) a l m) \<and>
+ − 213 (\<forall>e d. hom_d (e # d) = fcns (hom_e e) (hom_d d) e d) \<and>
+ − 214 (hom_d [] = fnil) \<and>
+ − 215 (\<forall>l m. hom_e (l, m) = fpar (hom_m m) l m) \<and>
+ − 216 (\<forall>x a. hom_m (rSig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
+ − 217 )
+ − 218 ))))"
+ − 219 sorry
+ − 220
+ − 221 lemma liftd'': "
+ − 222 \<exists>!hom_o. \<exists>!hom_d. \<exists>!hom_e. \<exists>!hom_m.
+ − 223 (
+ − 224 (\<forall>x. hom_o (Var x) = fvar x) \<and>
+ − 225 (\<forall>d. hom_o (Obj d) = fobj (hom_d d) d) \<and>
+ − 226 (\<forall>a l. hom_o (Inv a l) = fnvk (hom_o a) a l) \<and>
+ − 227 (\<forall>a l m. hom_o (Upd 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 (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a))
+ − 232 )"
+ − 233 apply (lifting tolift'')
+ − 234 done
+ − 235
+ − 236
905
+ − 237 end
+ − 238