2436
+ − 1
theory Let
2454
+ − 2
imports "../Nominal2"
1600
+ − 3
begin
+ − 4
+ − 5
atom_decl name
+ − 6
+ − 7
nominal_datatype trm =
2436
+ − 8
Var "name"
+ − 9
| App "trm" "trm"
+ − 10
| Lam x::"name" t::"trm" bind x in t
2490
+ − 11
| Let as::"assn" t::"trm" bind "bn as" in t
+ − 12
and assn =
+ − 13
ANil
+ − 14
| ACons "name" "trm" "assn"
1600
+ − 15
binder
+ − 16
bn
+ − 17
where
2490
+ − 18
"bn ANil = []"
+ − 19
| "bn (ACons x t as) = (atom x) # (bn as)"
+ − 20
2494
+ − 21
thm at_set_avoiding2
2490
+ − 22
thm trm_assn.fv_defs
2492
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23
thm trm_assn.eq_iff
2490
+ − 24
thm trm_assn.bn_defs
+ − 25
thm trm_assn.perm_simps
2492
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 26
thm trm_assn.induct
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 27
thm trm_assn.inducts
2490
+ − 28
thm trm_assn.distinct
+ − 29
thm trm_assn.supp
2493
+ − 30
thm trm_assn.fresh
2490
+ − 31
+ − 32
+ − 33
lemma fin_bn:
+ − 34
shows "finite (set (bn l))"
+ − 35
apply(induct l rule: trm_assn.inducts(2))
+ − 36
apply(simp_all)
+ − 37
done
+ − 38
2494
+ − 39
primrec
+ − 40
permute_bn_raw
+ − 41
where
+ − 42
"permute_bn_raw p (ANil_raw) = ANil_raw"
+ − 43
| "permute_bn_raw p (ACons_raw a t l) = ACons_raw (p \<bullet> a) t (permute_bn_raw p l)"
+ − 44
+ − 45
quotient_definition
+ − 46
"permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn"
+ − 47
is
+ − 48
"permute_bn_raw"
+ − 49
+ − 50
lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw"
+ − 51
apply simp
+ − 52
apply clarify
+ − 53
apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts)
+ − 54
apply (rule TrueI)+
+ − 55
apply simp_all
+ − 56
apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros)
+ − 57
apply simp_all
+ − 58
done
+ − 59
+ − 60
lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
+ − 61
+ − 62
lemma uu:
+ − 63
shows "alpha_bn (permute_bn p as) as"
+ − 64
apply(induct as rule: trm_assn.inducts(2))
+ − 65
apply(auto)[4]
+ − 66
apply(simp add: permute_bn)
+ − 67
apply(simp add: trm_assn.eq_iff)
+ − 68
apply(simp add: permute_bn)
+ − 69
apply(simp add: trm_assn.eq_iff)
+ − 70
done
+ − 71
+ − 72
lemma tt:
+ − 73
shows "(p \<bullet> bn as) = bn (permute_bn p as)"
+ − 74
apply(induct as rule: trm_assn.inducts(2))
+ − 75
apply(auto)[4]
+ − 76
apply(simp add: permute_bn trm_assn.bn_defs)
+ − 77
apply(simp add: permute_bn trm_assn.bn_defs)
+ − 78
apply(simp add: atom_eqvt)
+ − 79
done
+ − 80
+ − 81
thm trm_assn.supp
+ − 82
+ − 83
lemma "as \<sharp>* x \<longleftrightarrow> (\<forall>a\<in>as. a \<sharp> x)"
+ − 84
apply(simp add: fresh_def)
+ − 85
apply(simp add: fresh_star_def)
+ − 86
oops
2490
+ − 87
+ − 88
inductive
+ − 89
test_trm :: "trm \<Rightarrow> bool"
+ − 90
and test_assn :: "assn \<Rightarrow> bool"
+ − 91
where
+ − 92
"test_trm (Var x)"
+ − 93
| "\<lbrakk>test_trm t1; test_trm t2\<rbrakk> \<Longrightarrow> test_trm (App t1 t2)"
+ − 94
| "\<lbrakk>test_trm t; {atom x} \<sharp>* Lam x t\<rbrakk> \<Longrightarrow> test_trm (Lam x t)"
+ − 95
| "\<lbrakk>test_assn as; test_trm t; set (bn as) \<sharp>* Let as t\<rbrakk> \<Longrightarrow> test_trm (Let as t)"
+ − 96
| "test_assn ANil"
+ − 97
| "\<lbrakk>test_trm t; test_assn as\<rbrakk> \<Longrightarrow> test_assn (ACons x t as)"
+ − 98
+ − 99
declare trm_assn.fv_bn_eqvt[eqvt]
+ − 100
equivariance test_trm
+ − 101
+ − 102
lemma
+ − 103
fixes p::"perm"
+ − 104
shows "test_trm (p \<bullet> t)" and "test_assn (p \<bullet> as)"
+ − 105
apply(induct t and as arbitrary: p and p rule: trm_assn.inducts)
+ − 106
apply(simp)
+ − 107
apply(rule test_trm_test_assn.intros)
+ − 108
apply(simp)
+ − 109
apply(rule test_trm_test_assn.intros)
+ − 110
apply(assumption)
+ − 111
apply(assumption)
+ − 112
apply(simp)
+ − 113
apply(rule test_trm_test_assn.intros)
+ − 114
apply(assumption)
2493
+ − 115
apply(simp add: trm_assn.fresh fresh_star_def)
2490
+ − 116
apply(simp)
+ − 117
defer
+ − 118
apply(simp)
+ − 119
apply(rule test_trm_test_assn.intros)
+ − 120
apply(simp)
+ − 121
apply(rule test_trm_test_assn.intros)
+ − 122
apply(assumption)
+ − 123
apply(assumption)
2494
+ − 124
apply(subgoal_tac "finite (set (bn (p \<bullet> assn)))")
+ − 125
apply(subgoal_tac "set (bn (p \<bullet> assn)) \<sharp>* (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm))")
+ − 126
apply(drule_tac c="()" in at_set_avoiding2)
+ − 127
apply(simp add: supp_Unit)
+ − 128
prefer 2
+ − 129
apply(assumption)
+ − 130
apply(simp add: finite_supp)
+ − 131
apply(erule exE)
+ − 132
apply(erule conjE)
+ − 133
apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" and
+ − 134
s = "Let (permute_bn pa (p \<bullet> assn)) (pa \<bullet> (p \<bullet> trm))" in subst)
2493
+ − 135
apply(rule trm_assn.eq_iff(4)[THEN iffD2])
2494
+ − 136
apply(simp add: uu)
+ − 137
apply(drule supp_perm_eq)
+ − 138
apply(simp add: tt)
+ − 139
apply(rule test_trm_test_assn.intros(4))
2490
+ − 140
defer
2494
+ − 141
apply(subst permute_plus[symmetric])
+ − 142
apply(blast)
+ − 143
oops
2490
+ − 144
+ − 145
2494
+ − 146
(*
2490
+ − 147
lemma
+ − 148
fixes t::trm
+ − 149
and as::assn
+ − 150
and c::"'a::fs"
+ − 151
assumes a1: "\<And>x c. P1 c (Var x)"
+ − 152
and a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"
+ − 153
and a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"
+ − 154
and a4: "\<And>as t c. \<lbrakk>set (bn as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let as t)"
+ − 155
and a5: "\<And>c. P2 c ANil"
+ − 156
and a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)"
+ − 157
shows "P1 c t" and "P2 c as"
+ − 158
proof -
+ − 159
have x: "\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t)"
+ − 160
and y: "\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> as)"
+ − 161
apply(induct rule: trm_assn.inducts)
+ − 162
apply(simp)
+ − 163
apply(rule a1)
+ − 164
apply(simp)
+ − 165
apply(rule a2)
+ − 166
apply(assumption)
+ − 167
apply(assumption)
+ − 168
-- "lam case"
+ − 169
apply(simp)
+ − 170
apply(subgoal_tac "\<exists>q. (q \<bullet> {atom (p \<bullet> name)}) \<sharp>* c \<and> supp (Lam (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
+ − 171
apply(erule exE)
+ − 172
apply(erule conjE)
+ − 173
apply(drule supp_perm_eq[symmetric])
+ − 174
apply(simp)
+ − 175
apply(thin_tac "?X = ?Y")
+ − 176
apply(rule a3)
+ − 177
apply(simp add: atom_eqvt permute_set_eq)
+ − 178
apply(simp only: permute_plus[symmetric])
+ − 179
apply(rule at_set_avoiding2)
+ − 180
apply(simp add: finite_supp)
+ − 181
apply(simp add: finite_supp)
+ − 182
apply(simp add: finite_supp)
+ − 183
apply(simp add: freshs fresh_star_def)
+ − 184
--"let case"
+ − 185
apply(simp)
+ − 186
thm trm_assn.eq_iff
+ − 187
thm eq_iffs
+ − 188
apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> assn))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm)) \<sharp>* q")
+ − 189
apply(erule exE)
+ − 190
apply(erule conjE)
+ − 191
prefer 2
+ − 192
apply(rule at_set_avoiding2)
+ − 193
apply(rule fin_bn)
+ − 194
apply(simp add: finite_supp)
+ − 195
apply(simp add: finite_supp)
+ − 196
apply(simp add: abs_fresh)
+ − 197
apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)
+ − 198
prefer 2
+ − 199
apply(rule a4)
+ − 200
prefer 4
+ − 201
apply(simp add: eq_iffs)
+ − 202
apply(rule conjI)
+ − 203
prefer 2
+ − 204
apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)
+ − 205
apply(subst permute_plus[symmetric])
+ − 206
apply(blast)
+ − 207
prefer 2
+ − 208
apply(simp add: eq_iffs)
+ − 209
thm eq_iffs
+ − 210
apply(subst permute_plus[symmetric])
+ − 211
apply(blast)
+ − 212
apply(simp add: supps)
+ − 213
apply(simp add: fresh_star_def freshs)
+ − 214
apply(drule supp_perm_eq[symmetric])
+ − 215
apply(simp)
+ − 216
apply(simp add: eq_iffs)
+ − 217
apply(simp)
+ − 218
apply(thin_tac "?X = ?Y")
+ − 219
apply(rule a4)
+ − 220
apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)
+ − 221
apply(subst permute_plus[symmetric])
+ − 222
apply(blast)
+ − 223
apply(subst permute_plus[symmetric])
+ − 224
apply(blast)
+ − 225
apply(simp add: supps)
+ − 226
thm at_set_avoiding2
+ − 227
--"HERE"
+ − 228
apply(rule at_set_avoiding2)
+ − 229
apply(rule fin_bn)
+ − 230
apply(simp add: finite_supp)
+ − 231
apply(simp add: finite_supp)
+ − 232
apply(simp add: fresh_star_def freshs)
+ − 233
apply(rule ballI)
+ − 234
apply(simp add: eqvts permute_bn)
+ − 235
apply(rule a5)
+ − 236
apply(simp add: permute_bn)
+ − 237
apply(rule a6)
+ − 238
apply simp
+ − 239
apply simp
+ − 240
done
+ − 241
then have a: "P1 c (0 \<bullet> t)" by blast
+ − 242
have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
+ − 243
then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
+ − 244
qed
+ − 245
*)
1600
+ − 246
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 247
text {* *}
1731
+ − 248
2436
+ − 249
(*
1731
+ − 250
1644
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 251
primrec
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 252
permute_bn_raw
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 253
where
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 254
"permute_bn_raw pi (Lnil_raw) = Lnil_raw"
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 255
| "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)"
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 256
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 257
quotient_definition
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 258
"permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts"
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 259
is
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 260
"permute_bn_raw"
1639
+ − 261
1644
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 262
lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw"
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 263
apply simp
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 264
apply clarify
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 265
apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts)
2039
+ − 266
apply (rule TrueI)+
1644
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 267
apply simp_all
2039
+ − 268
apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
+ − 269
apply simp_all
1644
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 270
done
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 271
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 272
lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
1639
+ − 273
1642
+ − 274
lemma permute_bn_zero:
+ − 275
"permute_bn 0 a = a"
+ − 276
apply(induct a rule: trm_lts.inducts(2))
2039
+ − 277
apply(rule TrueI)+
+ − 278
apply(simp_all add:permute_bn)
1642
+ − 279
done
+ − 280
1640
+ − 281
lemma permute_bn_add:
+ − 282
"permute_bn (p + q) a = permute_bn p (permute_bn q a)"
+ − 283
oops
+ − 284
1643
+ − 285
lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
+ − 286
apply(induct lts rule: trm_lts.inducts(2))
2039
+ − 287
apply(rule TrueI)+
1644
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 288
apply(simp_all add:permute_bn eqvts trm_lts.eq_iff)
1643
+ − 289
done
1641
+ − 290
1642
+ − 291
lemma perm_bn:
+ − 292
"p \<bullet> bn l = bn(permute_bn p l)"
+ − 293
apply(induct l rule: trm_lts.inducts(2))
2039
+ − 294
apply(rule TrueI)+
1644
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 295
apply(simp_all add:permute_bn eqvts)
1642
+ − 296
done
+ − 297
1757
+ − 298
lemma fv_perm_bn:
+ − 299
"fv_bn l = fv_bn (permute_bn p l)"
+ − 300
apply(induct l rule: trm_lts.inducts(2))
2039
+ − 301
apply(rule TrueI)+
1757
+ − 302
apply(simp_all add:permute_bn eqvts)
+ − 303
done
+ − 304
1643
+ − 305
lemma Lt_subst:
1685
+ − 306
"supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
2039
+ − 307
apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn)
1643
+ − 308
apply (rule_tac x="q" in exI)
+ − 309
apply (simp add: alphas)
+ − 310
apply (simp add: perm_bn[symmetric])
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 311
apply(rule conjI)
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 312
apply(drule supp_perm_eq)
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 313
apply(simp add: abs_eq_iff)
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 314
apply(simp add: alphas_abs alphas)
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 315
apply(drule conjunct1)
1643
+ − 316
apply (simp add: trm_lts.supp)
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 317
apply(simp add: supp_abs)
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 318
apply (simp add: trm_lts.supp)
1643
+ − 319
done
+ − 320
+ − 321
1642
+ − 322
lemma fin_bn:
1685
+ − 323
"finite (set (bn l))"
1642
+ − 324
apply(induct l rule: trm_lts.inducts(2))
1644
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 325
apply(simp_all add:permute_bn eqvts)
1642
+ − 326
done
+ − 327
1765
+ − 328
thm trm_lts.inducts[no_vars]
+ − 329
1638
+ − 330
lemma
+ − 331
fixes t::trm
+ − 332
and l::lts
+ − 333
and c::"'a::fs"
1640
+ − 334
assumes a1: "\<And>name c. P1 c (Vr name)"
1638
+ − 335
and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
1640
+ − 336
and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
1685
+ − 337
and a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
1638
+ − 338
and a5: "\<And>c. P2 c Lnil"
+ − 339
and a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
+ − 340
shows "P1 c t" and "P2 c l"
+ − 341
proof -
+ − 342
have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
1642
+ − 343
b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))"
1638
+ − 344
apply(induct rule: trm_lts.inducts)
+ − 345
apply(simp)
+ − 346
apply(rule a1)
+ − 347
apply(simp)
+ − 348
apply(rule a2)
+ − 349
apply(simp)
+ − 350
apply(simp)
+ − 351
apply(simp)
+ − 352
apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
+ − 353
apply(erule exE)
+ − 354
apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)"
+ − 355
and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst)
+ − 356
apply(rule supp_perm_eq)
+ − 357
apply(simp)
+ − 358
apply(simp)
+ − 359
apply(rule a3)
+ − 360
apply(simp add: atom_eqvt)
+ − 361
apply(subst permute_plus[symmetric])
+ − 362
apply(blast)
+ − 363
apply(rule at_set_avoiding2_atom)
+ − 364
apply(simp add: finite_supp)
+ − 365
apply(simp add: finite_supp)
+ − 366
apply(simp add: fresh_def)
+ − 367
apply(simp add: trm_lts.fv[simplified trm_lts.supp])
+ − 368
apply(simp)
1685
+ − 369
apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
1638
+ − 370
apply(erule exE)
1641
+ − 371
apply(erule conjE)
1774
+ − 372
thm Lt_subst
1641
+ − 373
apply(subst Lt_subst)
+ − 374
apply assumption
1638
+ − 375
apply(rule a4)
1685
+ − 376
apply(simp add:perm_bn[symmetric])
+ − 377
apply(simp add: eqvts)
1641
+ − 378
apply (simp add: fresh_star_def fresh_def)
1640
+ − 379
apply(rotate_tac 1)
+ − 380
apply(drule_tac x="q + p" in meta_spec)
+ − 381
apply(simp)
1642
+ − 382
apply(rule at_set_avoiding2)
+ − 383
apply(rule fin_bn)
1641
+ − 384
apply(simp add: finite_supp)
+ − 385
apply(simp add: finite_supp)
1658
+ − 386
apply(simp add: fresh_star_def fresh_def supp_abs)
1644
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 387
apply(simp add: eqvts permute_bn)
1640
+ − 388
apply(rule a5)
1644
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 389
apply(simp add: permute_bn)
1640
+ − 390
apply(rule a6)
+ − 391
apply simp
+ − 392
apply simp
1642
+ − 393
done
+ − 394
then have a: "P1 c (0 \<bullet> t)" by blast
+ − 395
have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
+ − 396
then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
+ − 397
qed
+ − 398
1638
+ − 399
+ − 400
1602
+ − 401
lemma lets_bla:
+ − 402
"x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
+ − 403
by (simp add: trm_lts.eq_iff)
+ − 404
+ − 405
lemma lets_ok:
+ − 406
"(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
+ − 407
apply (simp add: trm_lts.eq_iff)
+ − 408
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
2039
+ − 409
apply (simp_all add: alphas eqvts supp_at_base fresh_star_def)
1602
+ − 410
done
+ − 411
+ − 412
lemma lets_ok3:
+ − 413
"x \<noteq> y \<Longrightarrow>
+ − 414
(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ − 415
(Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
+ − 416
apply (simp add: alphas trm_lts.eq_iff)
+ − 417
done
+ − 418
+ − 419
+ − 420
lemma lets_not_ok1:
1685
+ − 421
"x \<noteq> y \<Longrightarrow>
+ − 422
(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
1602
+ − 423
(Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
1685
+ − 424
apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts)
1602
+ − 425
done
+ − 426
+ − 427
lemma lets_nok:
+ − 428
"x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ − 429
(Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ − 430
(Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
+ − 431
apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
+ − 432
done
2436
+ − 433
*)
1602
+ − 434
1600
+ − 435
end
+ − 436
+ − 437
+ − 438