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