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
2924
+ − 21
print_theorems
+ − 22
+ − 23
thm alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros
+ − 24
thm bn_raw.simps
+ − 25
thm permute_bn_raw.simps
+ − 26
thm trm_assn.perm_bn_alpha
+ − 27
thm trm_assn.permute_bn
+ − 28
2490
+ − 29
thm trm_assn.fv_defs
2924
+ − 30
thm trm_assn.eq_iff
2490
+ − 31
thm trm_assn.bn_defs
2922
+ − 32
thm trm_assn.bn_inducts
2490
+ − 33
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
+ − 34
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
+ − 35
thm trm_assn.inducts
2490
+ − 36
thm trm_assn.distinct
+ − 37
thm trm_assn.supp
2493
+ − 38
thm trm_assn.fresh
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39
thm trm_assn.exhaust
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 40
thm trm_assn.strong_exhaust
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 41
thm trm_assn.perm_bn_simps
2494
+ − 42
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 43
lemma alpha_bn_inducts_raw[consumes 1]:
2923
+ − 44
"\<lbrakk>alpha_bn_raw a b; P3 ANil_raw ANil_raw;
+ − 45
\<And>trm_raw trm_rawa assn_raw assn_rawa name namea.
+ − 46
\<lbrakk>alpha_trm_raw trm_raw trm_rawa; alpha_bn_raw assn_raw assn_rawa;
+ − 47
P3 assn_raw assn_rawa\<rbrakk>
+ − 48
\<Longrightarrow> P3 (ACons_raw name trm_raw assn_raw)
+ − 49
(ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b"
+ − 50
by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto
+ − 51
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 52
lemmas alpha_bn_inducts[consumes 1] = alpha_bn_inducts_raw[quot_lifted]
2923
+ − 53
+ − 54
+ − 55
+ − 56
lemma alpha_bn_refl: "alpha_bn x x"
+ − 57
by (induct x rule: trm_assn.inducts(2))
+ − 58
(rule TrueI, auto simp add: trm_assn.eq_iff)
+ − 59
lemma alpha_bn_sym: "alpha_bn x y \<Longrightarrow> alpha_bn y x"
+ − 60
sorry
+ − 61
lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z"
+ − 62
sorry
2922
+ − 63
2923
+ − 64
lemma bn_inj[rule_format]:
+ − 65
assumes a: "alpha_bn x y"
+ − 66
shows "bn x = bn y \<longrightarrow> x = y"
+ − 67
by (rule alpha_bn_inducts[OF a]) (simp_all add: trm_assn.bn_defs)
+ − 68
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 69
lemma bn_inj2:
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 70
assumes a: "alpha_bn x y"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 71
shows "\<And>q r. (q \<bullet> bn x) = (r \<bullet> bn y) \<Longrightarrow> permute_bn q x = permute_bn r y"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 72
using a
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 73
apply(induct rule: alpha_bn_inducts)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 74
apply(simp add: trm_assn.perm_bn_simps)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 75
apply(simp add: trm_assn.perm_bn_simps)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 76
apply(simp add: trm_assn.bn_defs)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 77
apply(simp add: atom_eqvt)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 78
done
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 79
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 80
lemma Abs_lst_fcb2:
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 81
fixes as bs :: "atom list"
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 82
and x y :: "'b :: fs"
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 83
and c::"'c::fs"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 84
assumes eq: "[as]lst. x = [bs]lst. y"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 85
and fcb1: "(set as) \<sharp>* c \<Longrightarrow> (set as) \<sharp>* f as x c"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 86
and fresh1: "set as \<sharp>* c"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 87
and fresh2: "set bs \<sharp>* c"
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 88
and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 89
and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 90
shows "f as x c = f bs y c"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 91
proof -
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 92
have "supp (as, x, c) supports (f as x c)"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 93
unfolding supports_def fresh_def[symmetric]
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 94
by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh)
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 95
then have fin1: "finite (supp (f as x c))"
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 96
by (auto intro: supports_finite simp add: finite_supp)
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 97
have "supp (bs, y, c) supports (f bs y c)"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 98
unfolding supports_def fresh_def[symmetric]
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 99
by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh)
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 100
then have fin2: "finite (supp (f bs y c))"
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 101
by (auto intro: supports_finite simp add: finite_supp)
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 102
obtain q::"perm" where
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 103
fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 104
fr2: "supp q \<sharp>* Abs_lst as x" and
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 105
inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 106
using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"]
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 107
fin1 fin2
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 108
by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 109
have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 110
also have "\<dots> = Abs_lst as x"
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 111
by (simp only: fr2 perm_supp_eq)
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 112
finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 113
then obtain r::perm where
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 114
qq1: "q \<bullet> x = r \<bullet> y" and
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 115
qq2: "q \<bullet> as = r \<bullet> bs" and
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 116
qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs"
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 117
apply(drule_tac sym)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 118
apply(simp only: Abs_eq_iff2 alphas)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 119
apply(erule exE)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 120
apply(erule conjE)+
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 121
apply(drule_tac x="p" in meta_spec)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 122
apply(simp add: set_eqvt)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 123
apply(blast)
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 124
done
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 125
have "(set as) \<sharp>* f as x c"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 126
apply(rule fcb1)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 127
apply(rule fresh1)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 128
done
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 129
then have "q \<bullet> ((set as) \<sharp>* f as x c)"
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 130
by (simp add: permute_bool_def)
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 131
then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 132
apply(simp add: fresh_star_eqvt set_eqvt)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 133
apply(subst (asm) perm1)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 134
using inc fresh1 fr1
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 135
apply(auto simp add: fresh_star_def fresh_Pair)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 136
done
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 137
then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 138
then have "r \<bullet> ((set bs) \<sharp>* f bs y c)"
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 139
apply(simp add: fresh_star_eqvt set_eqvt)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 140
apply(subst (asm) perm2[symmetric])
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 141
using qq3 fresh2 fr1
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 142
apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 143
done
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 144
then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def)
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 145
have "f as x c = q \<bullet> (f as x c)"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 146
apply(rule perm_supp_eq[symmetric])
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 147
using inc fcb1[OF fresh1] fr1 by (auto simp add: fresh_star_def)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 148
also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c"
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 149
apply(rule perm1)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 150
using inc fresh1 fr1 by (auto simp add: fresh_star_def)
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 151
also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 152
also have "\<dots> = r \<bullet> (f bs y c)"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
apply(rule perm2[symmetric])
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 154
using qq3 fresh2 fr1 by (auto simp add: fresh_star_def)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 155
also have "... = f bs y c"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 156
apply(rule perm_supp_eq)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 157
using qq3 fr1 fcb2 by (auto simp add: fresh_star_def)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 158
finally show ?thesis by simp
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 159
qed
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 160
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 161
lemma Abs_lst1_fcb2:
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 162
fixes a b :: "atom"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 163
and x y :: "'b :: fs"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 164
and c::"'c :: fs"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 165
assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 166
and fcb1: "a \<sharp> c \<Longrightarrow> a \<sharp> f a x c"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 167
and fresh: "{a, b} \<sharp>* c"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 168
and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 169
and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 170
shows "f a x c = f b y c"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 171
using e
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 172
apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"])
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 173
apply(simp_all)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 174
using fcb1 fresh perm1 perm2
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 175
apply(simp_all add: fresh_star_def)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 176
done
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 177
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 178
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 179
lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 180
by (simp add: permute_pure)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 181
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 182
function
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 183
apply_assn :: "(trm \<Rightarrow> nat) \<Rightarrow> assn \<Rightarrow> nat"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 184
where
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 185
"apply_assn f ANil = (0 :: nat)"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 186
| "apply_assn f (ACons x t as) = max (f t) (apply_assn f as)"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 187
apply(case_tac x)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 188
apply(case_tac b rule: trm_assn.exhaust(2))
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 189
apply(simp_all)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 190
apply(blast)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 191
done
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 192
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 193
termination by lexicographic_order
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 194
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 195
lemma [eqvt]:
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 196
"p \<bullet> (apply_assn f a) = apply_assn (p \<bullet> f) (p \<bullet> a)"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 197
apply(induct f a rule: apply_assn.induct)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 198
apply simp_all
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 199
apply(perm_simp)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 200
apply rule
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 201
apply(perm_simp)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 202
apply simp
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 203
done
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 204
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 205
lemma alpha_bn_apply_assn:
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 206
assumes "alpha_bn as bs"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 207
shows "apply_assn f as = apply_assn f bs"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 208
using assms
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 209
apply (induct rule: alpha_bn_inducts)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 210
apply simp_all
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 211
done
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 212
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 213
nominal_primrec
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 214
height_trm :: "trm \<Rightarrow> nat"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 215
where
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 216
"height_trm (Var x) = 1"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 217
| "height_trm (App l r) = max (height_trm l) (height_trm r)"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 218
| "height_trm (Lam v b) = 1 + (height_trm b)"
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 219
| "height_trm (Let as b) = max (apply_assn height_trm as) (height_trm b)"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 220
apply (simp only: eqvt_def height_trm_graph_def)
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 221
apply (rule, perm_simp, rule, rule TrueI)
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 222
apply (case_tac x rule: trm_assn.exhaust(1))
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 223
apply (auto)[4]
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 224
apply (drule_tac x="assn" in meta_spec)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 225
apply (drule_tac x="trm" in meta_spec)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 226
apply (simp add: alpha_bn_refl)
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 227
apply(simp_all)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 228
apply (erule_tac c="()" in Abs_lst1_fcb2)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 229
apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)[4]
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 230
apply (erule conjE)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 231
apply (subst alpha_bn_apply_assn)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 232
apply assumption
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 233
apply (rule arg_cong) back
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 234
apply (erule_tac c="()" in Abs_lst_fcb2)
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 235
apply (simp_all add: pure_fresh fresh_star_def)[3]
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 236
apply (simp_all add: eqvt_at_def)[2]
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 237
done
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 238
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 239
definition "height_assn = apply_assn height_trm"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 240
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 241
function
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 242
apply_assn2 :: "(trm \<Rightarrow> trm) \<Rightarrow> assn \<Rightarrow> assn"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 243
where
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 244
"apply_assn2 f ANil = ANil"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 245
| "apply_assn2 f (ACons x t as) = ACons x (f t) (apply_assn2 f as)"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 246
apply(case_tac x)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 247
apply(case_tac b rule: trm_assn.exhaust(2))
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 248
apply(simp_all)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 249
apply(blast)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 250
done
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 251
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 252
termination by lexicographic_order
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 253
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 254
lemma [eqvt]:
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 255
"p \<bullet> (apply_assn2 f a) = apply_assn2 (p \<bullet> f) (p \<bullet> a)"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 256
apply(induct f a rule: apply_assn2.induct)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 257
apply simp_all
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 258
apply(perm_simp)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 259
apply rule
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 260
done
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 261
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 262
lemma bn_apply_assn2: "bn (apply_assn2 f as) = bn as"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 263
apply (induct as rule: trm_assn.inducts(2))
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 264
apply (rule TrueI)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 265
apply (simp_all add: trm_assn.bn_defs)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 266
done
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 267
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 268
nominal_primrec
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 269
subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 270
where
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 271
"subst s t (Var x) = (if (s = x) then t else (Var x))"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 272
| "subst s t (App l r) = App (subst s t l) (subst s t r)"
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 273
| "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)"
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 274
| "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (apply_assn2 (subst s t) as) (subst s t b)"
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 275
apply (simp only: eqvt_def subst_graph_def)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 276
apply (rule, perm_simp, rule)
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 277
apply (rule TrueI)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 278
apply (case_tac x)
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 279
apply (rule_tac y="c" and c="(a,b)" in trm_assn.strong_exhaust(1))
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 280
apply (auto simp add: fresh_star_def)[3]
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 281
apply (drule_tac x="assn" in meta_spec)
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 282
apply (simp add: Abs1_eq_iff alpha_bn_refl)
2938
+ − 283
apply simp_all[7]
+ − 284
prefer 2
+ − 285
apply(simp)
+ − 286
apply(simp)
+ − 287
apply(erule conjE)+
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 288
apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 289
apply (simp add: Abs_fresh_iff)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 290
apply (simp add: fresh_star_def)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 291
apply (simp_all add: fresh_star_Pair_elim perm_supp_eq eqvt_at_def)[2]
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 292
apply (simp add: bn_apply_assn2)
2938
+ − 293
apply(erule conjE)+
+ − 294
apply(rule conjI)
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 295
apply (erule_tac c="(sa, ta)" in Abs_lst_fcb2)
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 296
apply (simp add: fresh_star_def Abs_fresh_iff)
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 297
apply assumption+
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 298
apply (simp_all add: fresh_star_Pair_elim perm_supp_eq eqvt_at_def trm_assn.fv_bn_eqvt)[2]
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 299
apply (erule alpha_bn_inducts)
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 300
apply simp_all
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 301
done
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 302
1602
+ − 303
lemma lets_bla:
2670
+ − 304
"x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Let (ACons x (Var y) ANil) (Var x)) \<noteq> (Let (ACons x (Var z) ANil) (Var x))"
+ − 305
by (simp add: trm_assn.eq_iff)
+ − 306
1602
+ − 307
lemma lets_ok:
2670
+ − 308
"(Let (ACons x (Var y) ANil) (Var x)) = (Let (ACons y (Var y) ANil) (Var y))"
+ − 309
apply (simp add: trm_assn.eq_iff Abs_eq_iff )
1602
+ − 310
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
2670
+ − 311
apply (simp_all add: alphas atom_eqvt supp_at_base fresh_star_def trm_assn.bn_defs trm_assn.supp)
1602
+ − 312
done
+ − 313
+ − 314
lemma lets_ok3:
+ − 315
"x \<noteq> y \<Longrightarrow>
2670
+ − 316
(Let (ACons x (App (Var y) (Var x)) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq>
+ − 317
(Let (ACons y (App (Var x) (Var y)) (ACons x (Var x) ANil)) (App (Var x) (Var y)))"
+ − 318
apply (simp add: trm_assn.eq_iff)
1602
+ − 319
done
+ − 320
+ − 321
lemma lets_not_ok1:
1685
+ − 322
"x \<noteq> y \<Longrightarrow>
2670
+ − 323
(Let (ACons x (Var x) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq>
+ − 324
(Let (ACons y (Var x) (ACons x (Var y) ANil)) (App (Var x) (Var y)))"
+ − 325
apply (simp add: alphas trm_assn.eq_iff trm_assn.supp fresh_star_def atom_eqvt Abs_eq_iff trm_assn.bn_defs)
1602
+ − 326
done
+ − 327
+ − 328
lemma lets_nok:
+ − 329
"x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
2670
+ − 330
(Let (ACons x (App (Var z) (Var z)) (ACons y (Var z) ANil)) (App (Var x) (Var y))) \<noteq>
+ − 331
(Let (ACons y (Var z) (ACons x (App (Var z) (Var z)) ANil)) (App (Var x) (Var y)))"
+ − 332
apply (simp add: alphas trm_assn.eq_iff fresh_star_def trm_assn.bn_defs Abs_eq_iff trm_assn.supp trm_assn.distinct)
1602
+ − 333
done
2670
+ − 334
+ − 335
lemma
+ − 336
fixes a b c :: name
+ − 337
assumes x: "a \<noteq> c" and y: "b \<noteq> c"
+ − 338
shows "\<exists>p.([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c)"
+ − 339
apply (rule_tac x="(a \<leftrightarrow> b)" in exI)
+ − 340
apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt)
+ − 341
by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y)
+ − 342
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 343
end