1600
+ − 1
theory ExLet
1773
+ − 2
imports "../Parser" "../../Attic/Prove"
1600
+ − 3
begin
+ − 4
+ − 5
text {* example 3 or example 5 from Terms.thy *}
+ − 6
+ − 7
atom_decl name
+ − 8
1757
+ − 9
ML {* val _ = recursive := false *}
1685
+ − 10
ML {* val _ = alpha_type := AlphaLst *}
1600
+ − 11
nominal_datatype trm =
+ − 12
Vr "name"
+ − 13
| Ap "trm" "trm"
+ − 14
| Lm x::"name" t::"trm" bind x in t
1602
+ − 15
| Lt a::"lts" t::"trm" bind "bn a" in t
1731
+ − 16
(*| L a::"lts" t1::"trm" t2::"trm" bind "bn a" in t1, bind "bn a" in t2*)
1600
+ − 17
and lts =
1602
+ − 18
Lnil
+ − 19
| Lcons "name" "trm" "lts"
1600
+ − 20
binder
+ − 21
bn
+ − 22
where
1685
+ − 23
"bn Lnil = []"
+ − 24
| "bn (Lcons x t l) = (atom x) # (bn l)"
1600
+ − 25
1731
+ − 26
+ − 27
thm alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros
+ − 28
1600
+ − 29
thm trm_lts.fv
+ − 30
thm trm_lts.eq_iff
+ − 31
thm trm_lts.bn
+ − 32
thm trm_lts.perm
1638
+ − 33
thm trm_lts.induct[no_vars]
+ − 34
thm trm_lts.inducts[no_vars]
1600
+ − 35
thm trm_lts.distinct
1731
+ − 36
(*thm trm_lts.supp*)
1685
+ − 37
thm trm_lts.fv[simplified trm_lts.supp(1-2)]
1600
+ − 38
1739
+ − 39
1644
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 40
primrec
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 41
permute_bn_raw
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 42
where
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 43
"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
+ − 44
| "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
+ − 45
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 46
quotient_definition
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 47
"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
+ − 48
is
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 49
"permute_bn_raw"
1639
+ − 50
1644
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 51
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
+ − 52
apply simp
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 53
apply clarify
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 54
apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts)
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 55
apply simp_all
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 56
apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 57
apply simp
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 58
apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 59
apply simp
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 60
done
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 61
0e705352bcef
Properly defined permute_bn. No more sorry's in Let strong induction.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 62
lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
1639
+ − 63
1642
+ − 64
lemma permute_bn_zero:
+ − 65
"permute_bn 0 a = a"
+ − 66
apply(induct a rule: trm_lts.inducts(2))
+ − 67
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
+ − 68
apply(simp_all add:permute_bn eqvts)
1642
+ − 69
done
+ − 70
1640
+ − 71
lemma permute_bn_add:
+ − 72
"permute_bn (p + q) a = permute_bn p (permute_bn q a)"
+ − 73
oops
+ − 74
1643
+ − 75
lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
+ − 76
apply(induct lts rule: trm_lts.inducts(2))
+ − 77
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
+ − 78
apply(simp_all add:permute_bn eqvts trm_lts.eq_iff)
1643
+ − 79
done
1641
+ − 80
1642
+ − 81
lemma perm_bn:
+ − 82
"p \<bullet> bn l = bn(permute_bn p l)"
+ − 83
apply(induct l rule: trm_lts.inducts(2))
+ − 84
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
+ − 85
apply(simp_all add:permute_bn eqvts)
1642
+ − 86
done
+ − 87
1757
+ − 88
lemma fv_perm_bn:
+ − 89
"fv_bn l = fv_bn (permute_bn p l)"
+ − 90
apply(induct l rule: trm_lts.inducts(2))
+ − 91
apply(rule TrueI)
+ − 92
apply(simp_all add:permute_bn eqvts)
+ − 93
done
+ − 94
1759
+ − 95
lemma fv_fv_bn:
+ − 96
"fv_bn l - set (bn l) = fv_lts l - set (bn l)"
+ − 97
apply(induct l rule: trm_lts.inducts(2))
+ − 98
apply(rule TrueI)
+ − 99
apply(simp_all add:permute_bn eqvts)
+ − 100
by blast
+ − 101
1643
+ − 102
lemma Lt_subst:
1685
+ − 103
"supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
1643
+ − 104
apply (simp only: trm_lts.eq_iff)
+ − 105
apply (rule_tac x="q" in exI)
+ − 106
apply (simp add: alphas)
+ − 107
apply (simp add: permute_bn_alpha_bn)
+ − 108
apply (simp add: perm_bn[symmetric])
+ − 109
apply (simp add: eqvts[symmetric])
1658
+ − 110
apply (simp add: supp_abs)
1643
+ − 111
apply (simp add: trm_lts.supp)
+ − 112
apply (rule supp_perm_eq[symmetric])
+ − 113
apply (subst supp_finite_atom_set)
+ − 114
apply (rule finite_Diff)
+ − 115
apply (simp add: finite_supp)
+ − 116
apply (assumption)
+ − 117
done
+ − 118
+ − 119
1642
+ − 120
lemma fin_bn:
1685
+ − 121
"finite (set (bn l))"
1642
+ − 122
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
+ − 123
apply(simp_all add:permute_bn eqvts)
1642
+ − 124
done
+ − 125
1765
+ − 126
thm trm_lts.inducts[no_vars]
+ − 127
1638
+ − 128
lemma
+ − 129
fixes t::trm
+ − 130
and l::lts
+ − 131
and c::"'a::fs"
1640
+ − 132
assumes a1: "\<And>name c. P1 c (Vr name)"
1638
+ − 133
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
+ − 134
and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
1685
+ − 135
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
+ − 136
and a5: "\<And>c. P2 c Lnil"
+ − 137
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)"
+ − 138
shows "P1 c t" and "P2 c l"
+ − 139
proof -
+ − 140
have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and
1642
+ − 141
b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))"
1638
+ − 142
apply(induct rule: trm_lts.inducts)
+ − 143
apply(simp)
+ − 144
apply(rule a1)
+ − 145
apply(simp)
+ − 146
apply(rule a2)
+ − 147
apply(simp)
+ − 148
apply(simp)
+ − 149
apply(simp)
+ − 150
apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
+ − 151
apply(erule exE)
+ − 152
apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)"
+ − 153
and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst)
+ − 154
apply(rule supp_perm_eq)
+ − 155
apply(simp)
+ − 156
apply(simp)
+ − 157
apply(rule a3)
+ − 158
apply(simp add: atom_eqvt)
+ − 159
apply(subst permute_plus[symmetric])
+ − 160
apply(blast)
+ − 161
apply(rule at_set_avoiding2_atom)
+ − 162
apply(simp add: finite_supp)
+ − 163
apply(simp add: finite_supp)
+ − 164
apply(simp add: fresh_def)
+ − 165
apply(simp add: trm_lts.fv[simplified trm_lts.supp])
+ − 166
apply(simp)
1685
+ − 167
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
+ − 168
apply(erule exE)
1641
+ − 169
apply(erule conjE)
1774
+ − 170
thm Lt_subst
1641
+ − 171
apply(subst Lt_subst)
+ − 172
apply assumption
1638
+ − 173
apply(rule a4)
1685
+ − 174
apply(simp add:perm_bn[symmetric])
+ − 175
apply(simp add: eqvts)
1641
+ − 176
apply (simp add: fresh_star_def fresh_def)
1640
+ − 177
apply(rotate_tac 1)
+ − 178
apply(drule_tac x="q + p" in meta_spec)
+ − 179
apply(simp)
1642
+ − 180
apply(rule at_set_avoiding2)
+ − 181
apply(rule fin_bn)
1641
+ − 182
apply(simp add: finite_supp)
+ − 183
apply(simp add: finite_supp)
1658
+ − 184
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
+ − 185
apply(simp add: eqvts permute_bn)
1640
+ − 186
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
+ − 187
apply(simp add: permute_bn)
1640
+ − 188
apply(rule a6)
+ − 189
apply simp
+ − 190
apply simp
1642
+ − 191
done
+ − 192
then have a: "P1 c (0 \<bullet> t)" by blast
+ − 193
have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
+ − 194
then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
+ − 195
qed
+ − 196
1638
+ − 197
+ − 198
1602
+ − 199
lemma lets_bla:
+ − 200
"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))"
+ − 201
by (simp add: trm_lts.eq_iff)
+ − 202
+ − 203
lemma lets_ok:
+ − 204
"(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
+ − 205
apply (simp add: trm_lts.eq_iff)
+ − 206
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 207
apply (simp_all add: alphas)
+ − 208
apply (simp add: fresh_star_def eqvts)
+ − 209
done
+ − 210
+ − 211
lemma lets_ok3:
+ − 212
"x \<noteq> y \<Longrightarrow>
+ − 213
(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ − 214
(Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
+ − 215
apply (simp add: alphas trm_lts.eq_iff)
+ − 216
done
+ − 217
+ − 218
+ − 219
lemma lets_not_ok1:
1685
+ − 220
"x \<noteq> y \<Longrightarrow>
+ − 221
(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
1602
+ − 222
(Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
1685
+ − 223
apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts)
1602
+ − 224
done
+ − 225
+ − 226
lemma lets_nok:
+ − 227
"x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ − 228
(Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ − 229
(Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
+ − 230
apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
+ − 231
done
+ − 232
+ − 233
1600
+ − 234
end
+ − 235
+ − 236
+ − 237