2083
+ − 1
theory CoreHaskell
2044
+ − 2
imports "../NewParser"
1601
+ − 3
begin
+ − 4
2308
+ − 5
(* Core Haskell *)
2100
+ − 6
1601
+ − 7
atom_decl var
1698
+ − 8
atom_decl cvar
1601
+ − 9
atom_decl tvar
+ − 10
2400
+ − 11
declare [[STEPS = 20]]
2308
+ − 12
1601
+ − 13
nominal_datatype tkind =
+ − 14
KStar
+ − 15
| KFun "tkind" "tkind"
+ − 16
and ckind =
+ − 17
CKEq "ty" "ty"
+ − 18
and ty =
+ − 19
TVar "tvar"
1684
+ − 20
| TC "string"
1601
+ − 21
| TApp "ty" "ty"
1684
+ − 22
| TFun "string" "ty_lst"
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23
| TAll tv::"tvar" "tkind" T::"ty" bind (set) tv in T
1698
+ − 24
| TEq "ckind" "ty"
1606
+ − 25
and ty_lst =
+ − 26
TsNil
+ − 27
| TsCons "ty" "ty_lst"
1601
+ − 28
and co =
1699
+ − 29
CVar "cvar"
1698
+ − 30
| CConst "string"
1601
+ − 31
| CApp "co" "co"
1684
+ − 32
| CFun "string" "co_lst"
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33
| CAll cv::"cvar" "ckind" C::"co" bind (set) cv in C
1698
+ − 34
| CEq "ckind" "co"
+ − 35
| CRefl "ty"
1601
+ − 36
| CSym "co"
1698
+ − 37
| CCir "co" "co"
+ − 38
| CAt "co" "ty"
1601
+ − 39
| CLeft "co"
+ − 40
| CRight "co"
1698
+ − 41
| CSim "co" "co"
1601
+ − 42
| CRightc "co"
+ − 43
| CLeftc "co"
+ − 44
| CCoe "co" "co"
1606
+ − 45
and co_lst =
+ − 46
CsNil
+ − 47
| CsCons "co" "co_lst"
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 48
and trm =
1601
+ − 49
Var "var"
1699
+ − 50
| K "string"
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 51
| LAMT tv::"tvar" "tkind" t::"trm" bind (set) tv in t
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 52
| LAMC cv::"cvar" "ckind" t::"trm" bind (set) cv in t
1698
+ − 53
| AppT "trm" "ty"
+ − 54
| AppC "trm" "co"
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
| Lam v::"var" "ty" t::"trm" bind (set) v in t
1601
+ − 56
| App "trm" "trm"
2424
621ebd8b13c4
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 57
| Let x::"var" "ty" "trm" t::"trm" bind (set) x in t
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 58
| Case "trm" "assoc_lst"
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 59
| Cast "trm" "ty" --"ty is supposed to be a coercion type only"
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 60
and assoc_lst =
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 61
ANil
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 62
| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
1601
+ − 63
and pat =
1700
+ − 64
Kpat "string" "tvars" "cvars" "vars"
+ − 65
and vars =
+ − 66
VsNil
+ − 67
| VsCons "var" "ty" "vars"
+ − 68
and tvars =
+ − 69
TvsNil
+ − 70
| TvsCons "tvar" "tkind" "tvars"
+ − 71
and cvars =
+ − 72
CvsNil
+ − 73
| CvsCons "cvar" "ckind" "cvars"
1601
+ − 74
binder
1695
+ − 75
bv :: "pat \<Rightarrow> atom list"
1700
+ − 76
and bv_vs :: "vars \<Rightarrow> atom list"
+ − 77
and bv_tvs :: "tvars \<Rightarrow> atom list"
+ − 78
and bv_cvs :: "cvars \<Rightarrow> atom list"
1601
+ − 79
where
1700
+ − 80
"bv (Kpat s tvts tvcs vs) = append (bv_tvs tvts) (append (bv_cvs tvcs) (bv_vs vs))"
+ − 81
| "bv_vs VsNil = []"
+ − 82
| "bv_vs (VsCons v k t) = (atom v) # bv_vs t"
+ − 83
| "bv_tvs TvsNil = []"
+ − 84
| "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
+ − 85
| "bv_cvs CvsNil = []"
2213
+ − 86
| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
+ − 87
2400
+ − 88
(* can lift *)
2410
2bbdb9c427b5
improved runtime slightly, by constructing an explicit size measure for the function definitions
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 89
2393
d9a0cf26a88c
added a function that transforms the helper-rsp lemmas into real rsp lemmas
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 90
thm distinct
2400
+ − 91
thm fv_defs
2404
+ − 92
thm alpha_bn_imps alpha_equivp
2339
+ − 93
2400
+ − 94
thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts
+ − 95
thm perm_simps
+ − 96
thm perm_laws
+ − 97
thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)
+ − 98
+ − 99
thm eq_iff
+ − 100
thm eq_iff_simps
+ − 101
+ − 102
ML {*
+ − 103
val qtys = [@{typ tkind}, @{typ ckind}, @{typ ty}, @{typ ty_lst}, @{typ co},
+ − 104
@{typ co_lst}, @{typ trm}, @{typ assoc_lst}, @{typ pat}, @{typ vars},
+ − 105
@{typ tvars}, @{typ cvars}]
+ − 106
*}
+ − 107
+ − 108
ML {*
+ − 109
val thms_d = map (lift_thm qtys @{context}) @{thms distinct}
+ − 110
*}
+ − 111
+ − 112
ML {*
+ − 113
val thms_i = map (lift_thm qtys @{context}) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts}
+ − 114
*}
+ − 115
+ − 116
ML {*
+ − 117
val thms_f = map (lift_thm qtys @{context}) @{thms fv_defs}
+ − 118
*}
+ − 119
+ − 120
ML {*
+ − 121
val thms_i = map (lift_thm qtys @{context}) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)}
+ − 122
*}
+ − 123
+ − 124
ML {*
+ − 125
val thms_p = map (lift_thm qtys @{context}) @{thms perm_simps}
+ − 126
*}
+ − 127
+ − 128
ML {*
+ − 129
val thms_f = map (lift_thm qtys @{context}) @{thms perm_laws}
+ − 130
*}
+ − 131
2404
+ − 132
ML {*
+ − 133
val thms_e = map (lift_thm qtys @{context})
+ − 134
@{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+ − 135
prod.cases]}
+ − 136
*}
2339
+ − 137
2405
+ − 138
ML {*
+ − 139
val thms_f = map (lift_thm qtys @{context}) @{thms bn_defs}
+ − 140
*}
+ − 141
2406
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 142
ML {*
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 143
val thms_f = map (lift_thm qtys @{context}) @{thms bn_eqvt}
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 144
*}
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 145
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 146
ML {*
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 147
val thms_f = map (lift_thm qtys @{context}) @{thms fv_eqvt}
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 148
*}
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 149
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 150
ML {*
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 151
val thms_f = map (lift_thm qtys @{context}) @{thms size_eqvt}
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 152
*}
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 154
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 155
2339
+ − 156
1700
+ − 157
lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
+ − 158
lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
+ − 159
lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm
+ − 160
lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff
+ − 161
lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts
1634
+ − 162
1700
+ − 163
lemmas alpha_inducts=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts
+ − 164
lemmas alpha_intros=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros
1647
+ − 165
1634
+ − 166
lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
+ − 167
unfolding fresh_star_def Ball_def
+ − 168
by auto (simp_all add: fresh_minus_perm)
1615
0ea578c6dae3
Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 169
1700
+ − 170
primrec permute_bv_vs_raw
+ − 171
where "permute_bv_vs_raw p VsNil_raw = VsNil_raw"
+ − 172
| "permute_bv_vs_raw p (VsCons_raw v t l) = VsCons_raw (p \<bullet> v) t (permute_bv_vs_raw p l)"
+ − 173
primrec permute_bv_cvs_raw
+ − 174
where "permute_bv_cvs_raw p CvsNil_raw = CvsNil_raw"
+ − 175
| "permute_bv_cvs_raw p (CvsCons_raw v t l) = CvsCons_raw (p \<bullet> v) t (permute_bv_cvs_raw p l)"
+ − 176
primrec permute_bv_tvs_raw
+ − 177
where "permute_bv_tvs_raw p TvsNil_raw = TvsNil_raw"
+ − 178
| "permute_bv_tvs_raw p (TvsCons_raw v t l) = TvsCons_raw (p \<bullet> v) t (permute_bv_tvs_raw p l)"
1647
+ − 179
primrec permute_bv_raw
1700
+ − 180
where "permute_bv_raw p (Kpat_raw c l1 l2 l3) =
+ − 181
Kpat_raw c (permute_bv_tvs_raw p l1) (permute_bv_cvs_raw p l2) (permute_bv_vs_raw p l3)"
1647
+ − 182
1700
+ − 183
quotient_definition "permute_bv_vs :: perm \<Rightarrow> vars \<Rightarrow> vars"
+ − 184
is "permute_bv_vs_raw"
+ − 185
quotient_definition "permute_bv_cvs :: perm \<Rightarrow> cvars \<Rightarrow> cvars"
+ − 186
is "permute_bv_cvs_raw"
+ − 187
quotient_definition "permute_bv_tvs :: perm \<Rightarrow> tvars \<Rightarrow> tvars"
+ − 188
is "permute_bv_tvs_raw"
1647
+ − 189
quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"
+ − 190
is "permute_bv_raw"
+ − 191
+ − 192
lemma rsp_pre:
1700
+ − 193
"alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)"
+ − 194
"alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)"
+ − 195
"alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)"
1647
+ − 196
apply (erule_tac [!] alpha_inducts)
2044
+ − 197
apply (simp_all only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps)
1647
+ − 198
done
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 199
1647
+ − 200
lemma [quot_respect]:
+ − 201
"(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw"
1700
+ − 202
"(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw"
+ − 203
"(op = ===> alpha_cvars_raw ===> alpha_cvars_raw) permute_bv_cvs_raw permute_bv_cvs_raw"
+ − 204
"(op = ===> alpha_vars_raw ===> alpha_vars_raw) permute_bv_vs_raw permute_bv_vs_raw"
1647
+ − 205
apply (simp_all add: rsp_pre)
+ − 206
apply clarify
+ − 207
apply (erule_tac alpha_inducts)
+ − 208
apply (simp_all)
+ − 209
apply (rule alpha_intros)
+ − 210
apply (simp_all add: rsp_pre)
+ − 211
done
+ − 212
1684
+ − 213
thm permute_bv_raw.simps[no_vars]
1700
+ − 214
permute_bv_vs_raw.simps[quot_lifted]
+ − 215
permute_bv_cvs_raw.simps[quot_lifted]
+ − 216
permute_bv_tvs_raw.simps[quot_lifted]
1684
+ − 217
+ − 218
lemma permute_bv_pre:
1700
+ − 219
"permute_bv p (Kpat c l1 l2 l3) =
+ − 220
Kpat c (permute_bv_tvs p l1) (permute_bv_cvs p l2) (permute_bv_vs p l3)"
1684
+ − 221
by (lifting permute_bv_raw.simps)
+ − 222
+ − 223
lemmas permute_bv[simp] =
+ − 224
permute_bv_pre
1700
+ − 225
permute_bv_vs_raw.simps[quot_lifted]
+ − 226
permute_bv_cvs_raw.simps[quot_lifted]
+ − 227
permute_bv_tvs_raw.simps[quot_lifted]
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 228
1647
+ − 229
lemma perm_bv1:
1700
+ − 230
"p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)"
+ − 231
"p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)"
+ − 232
"p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)"
1647
+ − 233
apply(induct b rule: inducts(12))
+ − 234
apply(simp_all add:permute_bv eqvts)
+ − 235
apply(induct c rule: inducts(11))
+ − 236
apply(simp_all add:permute_bv eqvts)
+ − 237
apply(induct d rule: inducts(10))
+ − 238
apply(simp_all add:permute_bv eqvts)
+ − 239
done
+ − 240
+ − 241
lemma perm_bv2:
+ − 242
"p \<bullet> bv l = bv (permute_bv p l)"
+ − 243
apply(induct l rule: inducts(9))
+ − 244
apply(simp_all add:permute_bv)
+ − 245
apply(simp add: perm_bv1[symmetric])
+ − 246
apply(simp add: eqvts)
+ − 247
done
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 248
1648
+ − 249
lemma alpha_perm_bn1:
2044
+ − 250
"alpha_bv_tvs tvars (permute_bv_tvs q tvars)"
1700
+ − 251
"alpha_bv_cvs cvars (permute_bv_cvs q cvars)"
+ − 252
"alpha_bv_vs vars (permute_bv_vs q vars)"
+ − 253
apply(induct tvars rule: inducts(11))
1648
+ − 254
apply(simp_all add:permute_bv eqvts eq_iff)
1700
+ − 255
apply(induct cvars rule: inducts(12))
1648
+ − 256
apply(simp_all add:permute_bv eqvts eq_iff)
1700
+ − 257
apply(induct vars rule: inducts(10))
1648
+ − 258
apply(simp_all add:permute_bv eqvts eq_iff)
+ − 259
done
+ − 260
+ − 261
lemma alpha_perm_bn:
2142
c39d4fe31100
moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 262
"alpha_bv pt (permute_bv q pt)"
c39d4fe31100
moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 263
apply(induct pt rule: inducts(9))
1648
+ − 264
apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
+ − 265
done
+ − 266
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 267
lemma ACons_subst:
2142
c39d4fe31100
moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 268
"supp (Abs_lst (bv pt) trm) \<sharp>* q \<Longrightarrow> (ACons pt trm al) = ACons (permute_bv q pt) (q \<bullet> trm) al"
1648
+ − 269
apply (simp only: eq_iff)
2044
+ − 270
apply (simp add: alpha_perm_bn)
1648
+ − 271
apply (rule_tac x="q" in exI)
+ − 272
apply (simp add: alphas)
+ − 273
apply (simp add: perm_bv2[symmetric])
1658
+ − 274
apply (simp add: supp_abs)
1648
+ − 275
apply (simp add: fv_supp)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 276
apply (simp add: supp_eqvt[symmetric] set_eqvt[symmetric] Diff_eqvt[symmetric])
1648
+ − 277
apply (rule supp_perm_eq[symmetric])
+ − 278
apply (subst supp_finite_atom_set)
+ − 279
apply (rule finite_Diff)
+ − 280
apply (simp add: finite_supp)
+ − 281
apply (assumption)
+ − 282
done
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 283
1647
+ − 284
lemma permute_bv_zero1:
1700
+ − 285
"permute_bv_cvs 0 b = b"
+ − 286
"permute_bv_tvs 0 c = c"
+ − 287
"permute_bv_vs 0 d = d"
1647
+ − 288
apply(induct b rule: inducts(12))
+ − 289
apply(simp_all add:permute_bv eqvts)
+ − 290
apply(induct c rule: inducts(11))
+ − 291
apply(simp_all add:permute_bv eqvts)
+ − 292
apply(induct d rule: inducts(10))
+ − 293
apply(simp_all add:permute_bv eqvts)
+ − 294
done
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 295
1647
+ − 296
lemma permute_bv_zero2:
+ − 297
"permute_bv 0 a = a"
+ − 298
apply(induct a rule: inducts(9))
+ − 299
apply(simp_all add:permute_bv eqvts permute_bv_zero1)
+ − 300
done
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 301
1700
+ − 302
lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x"
2044
+ − 303
apply (induct x rule: inducts(11))
+ − 304
apply (simp_all add: eq_iff fresh_star_union)
+ − 305
done
1635
+ − 306
1700
+ − 307
lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x"
1635
+ − 308
apply (induct x rule: inducts(12))
2044
+ − 309
apply (rule TrueI)+
1635
+ − 310
apply (simp_all add: eq_iff fresh_star_union)
+ − 311
apply (subst supp_perm_eq)
+ − 312
apply (simp_all add: fv_supp)
+ − 313
done
+ − 314
1700
+ − 315
lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x"
1635
+ − 316
apply (induct x rule: inducts(10))
2044
+ − 317
apply (rule TrueI)+
+ − 318
apply (simp_all add: fresh_star_union eq_iff)
1635
+ − 319
apply (subst supp_perm_eq)
+ − 320
apply (simp_all add: fv_supp)
+ − 321
done
+ − 322
+ − 323
lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x"
+ − 324
apply (induct x rule: inducts(9))
2044
+ − 325
apply (rule TrueI)+
1635
+ − 326
apply (simp_all add: eq_iff fresh_star_union)
+ − 327
apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
2044
+ − 328
apply (subst supp_perm_eq)
+ − 329
apply (simp_all add: fv_supp)
1635
+ − 330
done
+ − 331
1700
+ − 332
lemma fin1: "finite (fv_bv_tvs x)"
1635
+ − 333
apply (induct x rule: inducts(11))
+ − 334
apply (simp_all add: fv_supp finite_supp)
+ − 335
done
+ − 336
1700
+ − 337
lemma fin2: "finite (fv_bv_cvs x)"
1635
+ − 338
apply (induct x rule: inducts(12))
+ − 339
apply (simp_all add: fv_supp finite_supp)
+ − 340
done
+ − 341
1700
+ − 342
lemma fin3: "finite (fv_bv_vs x)"
1635
+ − 343
apply (induct x rule: inducts(10))
+ − 344
apply (simp_all add: fv_supp finite_supp)
+ − 345
done
+ − 346
+ − 347
lemma fin_fv_bv: "finite (fv_bv x)"
+ − 348
apply (induct x rule: inducts(9))
2044
+ − 349
apply (rule TrueI)+
+ − 350
defer
+ − 351
apply (rule TrueI)+
1635
+ − 352
apply (simp add: fin1 fin2 fin3)
2044
+ − 353
apply (rule finite_supp)
1635
+ − 354
done
+ − 355
1700
+ − 356
lemma finb1: "finite (set (bv_tvs x))"
1635
+ − 357
apply (induct x rule: inducts(11))
+ − 358
apply (simp_all add: fv_supp finite_supp)
+ − 359
done
+ − 360
1700
+ − 361
lemma finb2: "finite (set (bv_cvs x))"
1635
+ − 362
apply (induct x rule: inducts(12))
+ − 363
apply (simp_all add: fv_supp finite_supp)
+ − 364
done
+ − 365
1700
+ − 366
lemma finb3: "finite (set (bv_vs x))"
1635
+ − 367
apply (induct x rule: inducts(10))
+ − 368
apply (simp_all add: fv_supp finite_supp)
+ − 369
done
+ − 370
1695
+ − 371
lemma fin_bv: "finite (set (bv x))"
1635
+ − 372
apply (induct x rule: inducts(9))
2044
+ − 373
apply (simp_all add: finb1 finb2 finb3)
1635
+ − 374
done
+ − 375
1701
+ − 376
lemma strong_induction_principle:
1631
+ − 377
assumes a01: "\<And>b. P1 b KStar"
+ − 378
and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
+ − 379
and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
+ − 380
and a04: "\<And>tvar b. P3 b (TVar tvar)"
1684
+ − 381
and a05: "\<And>string b. P3 b (TC string)"
1631
+ − 382
and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
1684
+ − 383
and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)"
1632
+ − 384
and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
+ − 385
\<Longrightarrow> P3 b (TAll tvar tkind ty)"
1701
+ − 386
and a09: "\<And>ck ty b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TEq ck ty)"
+ − 387
and a10: "\<And>b. P4 b TsNil"
+ − 388
and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)"
+ − 389
and a12: "\<And>string b. P5 b (CVar string)"
+ − 390
and a12a:"\<And>str b. P5 b (CConst str)"
1631
+ − 391
and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
1684
+ − 392
and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)"
1632
+ − 393
and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
+ − 394
\<Longrightarrow> P5 b (CAll tvar ckind co)"
1701
+ − 395
and a16: "\<And>ck co b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CEq ck co)"
+ − 396
and a17: "\<And>ty b. \<lbrakk>\<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CRefl ty)"
+ − 397
and a17a: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"
1631
+ − 398
and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"
1701
+ − 399
and a18a:"\<And>co ty b. \<lbrakk>\<And>c. P5 c co; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CAt co ty)"
1631
+ − 400
and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)"
+ − 401
and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)"
1701
+ − 402
and a21: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CSim co1 co2)"
1631
+ − 403
and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)"
+ − 404
and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"
+ − 405
and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"
+ − 406
and a25: "\<And>b. P6 b CsNil"
+ − 407
and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)"
+ − 408
and a27: "\<And>var b. P7 b (Var var)"
1701
+ − 409
and a28: "\<And>string b. P7 b (K string)"
1632
+ − 410
and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
+ − 411
\<Longrightarrow> P7 b (LAMT tvar tkind trm)"
+ − 412
and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
+ − 413
\<Longrightarrow> P7 b (LAMC tvar ckind trm)"
1701
+ − 414
and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (AppT trm ty)"
+ − 415
and a31a:"\<And>trm co b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P7 b (AppC trm co)"
1632
+ − 416
and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)"
1631
+ − 417
and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)"
1632
+ − 418
and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk>
1631
+ − 419
\<Longrightarrow> P7 b (Let var ty trm1 trm2)"
+ − 420
and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)"
+ − 421
and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
+ − 422
and a37: "\<And>b. P8 b ANil"
2142
c39d4fe31100
moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 423
and a38: "\<And>pt trm assoc_lst b. \<lbrakk>\<And>c. P9 c pt; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pt)) \<sharp>* b\<rbrakk>
c39d4fe31100
moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 424
\<Longrightarrow> P8 b (ACons pt trm assoc_lst)"
1700
+ − 425
and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk>
1701
+ − 426
\<Longrightarrow> P9 b (Kpat string tvars cvars vars)"
1700
+ − 427
and a40: "\<And>b. P10 b VsNil"
+ − 428
and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)"
+ − 429
and a42: "\<And>b. P11 b TvsNil"
+ − 430
and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk>
+ − 431
\<Longrightarrow> P11 b (TvsCons tvar tkind tvars)"
+ − 432
and a44: "\<And>b. P12 b CvsNil"
+ − 433
and a45: "\<And>tvar ckind cvars b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c cvars\<rbrakk>
+ − 434
\<Longrightarrow> P12 b (CvsCons tvar ckind cvars)"
1632
+ − 435
shows "P1 (a :: 'a :: pt) tkind \<and>
1631
+ − 436
P2 (b :: 'b :: pt) ckind \<and>
1634
+ − 437
P3 (c :: 'c :: {pt,fs}) ty \<and>
1631
+ − 438
P4 (d :: 'd :: pt) ty_lst \<and>
1635
+ − 439
P5 (e :: 'e :: {pt,fs}) co \<and>
1631
+ − 440
P6 (f :: 'f :: pt) co_lst \<and>
1645
+ − 441
P7 (g :: 'g :: {pt,fs}) trm \<and>
1635
+ − 442
P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>
2142
c39d4fe31100
moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 443
P9 (i :: 'i :: pt) pt \<and>
1700
+ − 444
P10 (j :: 'j :: pt) vars \<and>
+ − 445
P11 (k :: 'k :: pt) tvars \<and>
+ − 446
P12 (l :: 'l :: pt) cvars"
1631
+ − 447
proof -
2142
c39d4fe31100
moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 448
have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pt)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"
1700
+ − 449
apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts)
1632
+ − 450
apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
+ − 451
apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
1635
+ − 452
+ − 453
(* GOAL1 *)
+ − 454
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>
+ − 455
supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")
+ − 456
apply clarify
+ − 457
apply (simp only: perm)
+ − 458
apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)"
+ − 459
and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
2044
+ − 460
apply (simp add: eq_iff)
1635
+ − 461
apply (rule_tac x="-pa" in exI)
1658
+ − 462
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
1635
+ − 463
apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
+ − 464
and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
+ − 465
apply (simp add: eqvts)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 466
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
1635
+ − 467
apply (rule conjI)
+ − 468
apply (rule supp_perm_eq)
+ − 469
apply (simp add: eqvts)
+ − 470
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 471
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1635
+ − 472
apply (simp add: eqvts)
+ − 473
apply (subst supp_perm_eq)
+ − 474
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 475
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1635
+ − 476
apply assumption
+ − 477
apply (simp add: fresh_star_minus_perm)
+ − 478
apply (rule a08)
+ − 479
apply simp
+ − 480
apply(rotate_tac 1)
+ − 481
apply(erule_tac x="(pa + p)" in allE)
+ − 482
apply simp
+ − 483
apply (simp add: eqvts eqvts_raw)
1634
+ − 484
apply (rule at_set_avoiding2_atom)
+ − 485
apply (simp add: finite_supp)
+ − 486
apply (simp add: finite_supp)
+ − 487
apply (simp add: fresh_def)
1658
+ − 488
apply (simp only: supp_abs eqvts)
1634
+ − 489
apply blast
1635
+ − 490
+ − 491
(* GOAL2 *)
1701
+ − 492
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and>
+ − 493
supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)")
1634
+ − 494
apply clarify
+ − 495
apply (simp only: perm)
1701
+ − 496
apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)"
+ − 497
and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
2044
+ − 498
apply (simp add: eq_iff)
1634
+ − 499
apply (rule_tac x="-pa" in exI)
1658
+ − 500
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
1701
+ − 501
apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
+ − 502
and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst)
1635
+ − 503
apply (simp add: eqvts)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 504
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
1634
+ − 505
apply (rule conjI)
+ − 506
apply (rule supp_perm_eq)
+ − 507
apply (simp add: eqvts)
+ − 508
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 509
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1634
+ − 510
apply (simp add: eqvts)
+ − 511
apply (subst supp_perm_eq)
+ − 512
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 513
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1634
+ − 514
apply assumption
+ − 515
apply (simp add: fresh_star_minus_perm)
1635
+ − 516
apply (rule a15)
+ − 517
apply simp
+ − 518
apply(rotate_tac 1)
+ − 519
apply(erule_tac x="(pa + p)" in allE)
+ − 520
apply simp
+ − 521
apply (simp add: eqvts eqvts_raw)
+ − 522
apply (rule at_set_avoiding2_atom)
+ − 523
apply (simp add: finite_supp)
+ − 524
apply (simp add: finite_supp)
+ − 525
apply (simp add: fresh_def)
1658
+ − 526
apply (simp only: supp_abs eqvts)
1635
+ − 527
apply blast
+ − 528
1645
+ − 529
+ − 530
(* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *)
+ − 531
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
+ − 532
supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
+ − 533
apply clarify
+ − 534
apply (simp only: perm)
+ − 535
apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)"
+ − 536
and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)
2044
+ − 537
apply (simp add: eq_iff)
1645
+ − 538
apply (rule_tac x="-pa" in exI)
1658
+ − 539
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
1645
+ − 540
apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
+ − 541
and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
+ − 542
apply (simp add: eqvts)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 543
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
1645
+ − 544
apply (rule conjI)
+ − 545
apply (rule supp_perm_eq)
+ − 546
apply (simp add: eqvts)
+ − 547
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 548
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1645
+ − 549
apply (simp add: eqvts)
+ − 550
apply (subst supp_perm_eq)
+ − 551
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 552
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1645
+ − 553
apply assumption
+ − 554
apply (simp add: fresh_star_minus_perm)
+ − 555
apply (rule a29)
+ − 556
apply simp
+ − 557
apply(rotate_tac 1)
+ − 558
apply(erule_tac x="(pa + p)" in allE)
+ − 559
apply simp
+ − 560
apply (simp add: eqvts eqvts_raw)
+ − 561
apply (rule at_set_avoiding2_atom)
+ − 562
apply (simp add: finite_supp)
+ − 563
apply (simp add: finite_supp)
+ − 564
apply (simp add: fresh_def)
1658
+ − 565
apply (simp only: supp_abs eqvts)
1645
+ − 566
apply blast
+ − 567
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 568
(* GOAL4 a copy-and-paste *)
1701
+ − 569
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and>
+ − 570
supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)")
1635
+ − 571
apply clarify
+ − 572
apply (simp only: perm)
1701
+ − 573
apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)"
+ − 574
and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
2044
+ − 575
apply (simp add: eq_iff)
1635
+ − 576
apply (rule_tac x="-pa" in exI)
1658
+ − 577
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
1701
+ − 578
apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
+ − 579
and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst)
1635
+ − 580
apply (simp add: eqvts)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 581
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
1635
+ − 582
apply (rule conjI)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 583
apply (rule supp_perm_eq)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 584
apply (simp add: eqvts)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 585
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 586
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 587
apply (simp add: eqvts)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 588
apply (subst supp_perm_eq)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 589
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 590
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 591
apply assumption
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 592
apply (simp add: fresh_star_minus_perm)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 593
apply (rule a30)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 594
apply simp
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 595
apply(rotate_tac 1)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 596
apply(erule_tac x="(pa + p)" in allE)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 597
apply simp
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 598
apply (simp add: eqvts eqvts_raw)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 599
apply (rule at_set_avoiding2_atom)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 600
apply (simp add: finite_supp)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 601
apply (simp add: finite_supp)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 602
apply (simp add: fresh_def)
1658
+ − 603
apply (simp only: supp_abs eqvts)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 604
apply blast
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 605
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 606
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 607
(* GOAL5 a copy-and-paste *)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 608
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 609
supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)")
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 610
apply clarify
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 611
apply (simp only: perm)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 612
apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 613
and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
2044
+ − 614
apply (simp add: eq_iff)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 615
apply (rule_tac x="-pa" in exI)
1658
+ − 616
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 617
apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 618
and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 619
apply (simp add: eqvts)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 620
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
1635
+ − 621
apply (rule conjI)
+ − 622
apply (rule supp_perm_eq)
+ − 623
apply (simp add: eqvts)
+ − 624
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 625
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1635
+ − 626
apply (simp add: eqvts)
+ − 627
apply (subst supp_perm_eq)
+ − 628
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 629
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1635
+ − 630
apply assumption
+ − 631
apply (simp add: fresh_star_minus_perm)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 632
apply (rule a32)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 633
apply simp
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 634
apply(rotate_tac 1)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 635
apply(erule_tac x="(pa + p)" in allE)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 636
apply simp
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 637
apply (simp add: eqvts eqvts_raw)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 638
apply (rule at_set_avoiding2_atom)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 639
apply (simp add: finite_supp)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 640
apply (simp add: finite_supp)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 641
apply (simp add: fresh_def)
1658
+ − 642
apply (simp only: supp_abs eqvts)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 643
apply blast
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 644
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 645
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 646
(* GOAL6 a copy-and-paste *)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 647
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 648
supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)")
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 649
apply clarify
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 650
apply (simp only: perm)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 651
apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 652
and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
2044
+ − 653
apply (simp add: eq_iff)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 654
apply (rule_tac x="-pa" in exI)
1658
+ − 655
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 656
apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 657
and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 658
apply (simp add: eqvts)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 659
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 660
apply (rule conjI)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 661
apply (rule supp_perm_eq)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 662
apply (simp add: eqvts)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 663
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 664
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 665
apply (simp add: eqvts)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 666
apply (subst supp_perm_eq)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 667
apply (subst supp_finite_atom_set)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 668
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 669
apply assumption
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 670
apply (simp add: fresh_star_minus_perm)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 671
apply (rule a34)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 672
apply simp
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 673
apply simp
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 674
apply(rotate_tac 2)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 675
apply(erule_tac x="(pa + p)" in allE)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 676
apply simp
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 677
apply (simp add: eqvts eqvts_raw)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 678
apply (rule at_set_avoiding2_atom)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 679
apply (simp add: finite_supp)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 680
apply (simp add: finite_supp)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 681
apply (simp add: fresh_def)
1658
+ − 682
apply (simp only: supp_abs eqvts)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 683
apply blast
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 684
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 685
(* MAIN ACons Goal *)
1695
+ − 686
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and>
+ − 687
supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 688
apply clarify
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 689
apply (simp only: perm eqvts)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 690
apply (subst ACons_subst)
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 691
apply assumption
1635
+ − 692
apply (rule a38)
+ − 693
apply simp
+ − 694
apply(rotate_tac 1)
+ − 695
apply(erule_tac x="(pa + p)" in allE)
+ − 696
apply simp
+ − 697
apply simp
1647
+ − 698
apply (simp add: perm_bv2[symmetric])
1635
+ − 699
apply (simp add: eqvts eqvts_raw)
+ − 700
apply (rule at_set_avoiding2)
+ − 701
apply (simp add: fin_bv)
+ − 702
apply (simp add: finite_supp)
1658
+ − 703
apply (simp add: supp_abs)
1646
733bac87d5bf
Solved all boring subgoals, and looking at properly defning permute_bv
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 704
apply (simp add: finite_supp)
1658
+ − 705
apply (simp add: fresh_star_def fresh_def supp_abs eqvts)
1647
+ − 706
done
+ − 707
then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+)
2142
c39d4fe31100
moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 708
moreover have "P9 i (permute_bv 0 (0 \<bullet> pt))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
1647
+ − 709
ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
1631
+ − 710
qed
1615
0ea578c6dae3
Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 711
1868
26c0c35641cb
equivariance for alpha_raw in CoreHaskell is automatically derived
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 712
section {* test about equivariance for alpha *}
26c0c35641cb
equivariance for alpha_raw in CoreHaskell is automatically derived
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 713
2044
+ − 714
(* this should not be an equivariance rule *)
+ − 715
(* for the moment, we force it to be *)
+ − 716
+ − 717
(*declare permute_pure[eqvt]*)
2104
2205b572bc9b
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 718
(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} *)
2044
+ − 719
1868
26c0c35641cb
equivariance for alpha_raw in CoreHaskell is automatically derived
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 720
thm eqvts
26c0c35641cb
equivariance for alpha_raw in CoreHaskell is automatically derived
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 721
thm eqvts_raw
26c0c35641cb
equivariance for alpha_raw in CoreHaskell is automatically derived
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 722
26c0c35641cb
equivariance for alpha_raw in CoreHaskell is automatically derived
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 723
1601
+ − 724
end
+ − 725