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