905
+ − 1
theory SigmaEx
1128
+ − 2
imports Nominal "../Quotient" "../Quotient_List" "../Quotient_Product"
905
+ − 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"
1139
+ − 38
is
905
+ − 39
"rVar"
+ − 40
+ − 41
quotient_definition
+ − 42
"Obj :: (string \<times> method) list \<Rightarrow> obj"
1139
+ − 43
is
905
+ − 44
"rObj"
+ − 45
+ − 46
quotient_definition
+ − 47
"Inv :: obj \<Rightarrow> string \<Rightarrow> obj"
1139
+ − 48
is
905
+ − 49
"rInv"
+ − 50
+ − 51
quotient_definition
+ − 52
"Upd :: obj \<Rightarrow> string \<Rightarrow> method \<Rightarrow> obj"
1139
+ − 53
is
905
+ − 54
"rUpd"
+ − 55
+ − 56
quotient_definition
+ − 57
"Sig :: name \<Rightarrow> obj \<Rightarrow> method"
1139
+ − 58
is
905
+ − 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"
1139
+ − 68
is
905
+ − 69
"(perm::'x prm \<Rightarrow> robj \<Rightarrow> robj)"
+ − 70
+ − 71
quotient_definition
+ − 72
"perm_method :: 'x prm \<Rightarrow> method \<Rightarrow> method"
1139
+ − 73
is
905
+ − 74
"(perm::'x prm \<Rightarrow> rmethod \<Rightarrow> rmethod)"
+ − 75
+ − 76
end
+ − 77
1074
+ − 78
+ − 79
905
+ − 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
1074
+ − 90
Ex1 (\<lambda>x.
+ − 91
(x \<in> (Respects (prod_rel (alpha_obj ===> op =)
905
+ − 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
)
1074
+ − 96
)))) \<and>
945
+ − 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).
905
+ − 98
1074
+ − 99
((\<forall>x. hom_o (rVar x) = fvar x) \<and>
905
+ − 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))
1074
+ − 107
)) x) "
905
+ − 108
sorry
+ − 109
1074
+ − 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
905
+ − 121
"_expttrn" :: "pttrn => bool => bool" ("(3\<exists>\<exists> _./ _)" [0, 10] 10)
+ − 122
+ − 123
translations
+ − 124
"\<exists>\<exists> x. P" == "Ex (%x. P)"
1074
+ − 125
*)
905
+ − 126
+ − 127
lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar"
938
+ − 128
by (simp add: a1)
905
+ − 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
918
+ − 141
980
+ − 142
lemma bex1_bex1reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
1074
+ − 143
apply (simp add: Ex1_def Bex1_rel_def in_respects)
946
+ − 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
918
+ − 152
905
+ − 153
lemma liftd: "
945
+ − 154
Ex1 (\<lambda>(hom_o, hom_d, hom_e, hom_m).
+ − 155
905
+ − 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)
944
6267ad688ea8
2 cases for regularize with split, lemmas with split now lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 166
done
905
+ − 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
912
+ − 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
980
+ − 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.
912
+ − 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
905
+ − 252
end
+ − 253