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
+ − 21
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
+ − 22
thm trm_assn.eq_iff
2490
+ − 23
thm trm_assn.bn_defs
+ − 24
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
+ − 25
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
+ − 26
thm trm_assn.inducts
2490
+ − 27
thm trm_assn.distinct
+ − 28
thm trm_assn.supp
2493
+ − 29
thm trm_assn.fresh
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 30
thm trm_assn.exhaust
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 31
thm trm_assn.strong_exhaust
2494
+ − 32
2670
+ − 33
1602
+ − 34
lemma lets_bla:
2670
+ − 35
"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))"
+ − 36
by (simp add: trm_assn.eq_iff)
+ − 37
1602
+ − 38
+ − 39
lemma lets_ok:
2670
+ − 40
"(Let (ACons x (Var y) ANil) (Var x)) = (Let (ACons y (Var y) ANil) (Var y))"
+ − 41
apply (simp add: trm_assn.eq_iff Abs_eq_iff )
1602
+ − 42
apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
2670
+ − 43
apply (simp_all add: alphas atom_eqvt supp_at_base fresh_star_def trm_assn.bn_defs trm_assn.supp)
1602
+ − 44
done
+ − 45
+ − 46
lemma lets_ok3:
+ − 47
"x \<noteq> y \<Longrightarrow>
2670
+ − 48
(Let (ACons x (App (Var y) (Var x)) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq>
+ − 49
(Let (ACons y (App (Var x) (Var y)) (ACons x (Var x) ANil)) (App (Var x) (Var y)))"
+ − 50
apply (simp add: trm_assn.eq_iff)
1602
+ − 51
done
+ − 52
+ − 53
+ − 54
lemma lets_not_ok1:
1685
+ − 55
"x \<noteq> y \<Longrightarrow>
2670
+ − 56
(Let (ACons x (Var x) (ACons y (Var y) ANil)) (App (Var x) (Var y))) \<noteq>
+ − 57
(Let (ACons y (Var x) (ACons x (Var y) ANil)) (App (Var x) (Var y)))"
+ − 58
apply (simp add: alphas trm_assn.eq_iff trm_assn.supp fresh_star_def atom_eqvt Abs_eq_iff trm_assn.bn_defs)
1602
+ − 59
done
+ − 60
+ − 61
lemma lets_nok:
+ − 62
"x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
2670
+ − 63
(Let (ACons x (App (Var z) (Var z)) (ACons y (Var z) ANil)) (App (Var x) (Var y))) \<noteq>
+ − 64
(Let (ACons y (Var z) (ACons x (App (Var z) (Var z)) ANil)) (App (Var x) (Var y)))"
+ − 65
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
+ − 66
done
2670
+ − 67
+ − 68
lemma
+ − 69
fixes a b c :: name
+ − 70
assumes x: "a \<noteq> c" and y: "b \<noteq> c"
+ − 71
shows "\<exists>p.([atom a], Var c) \<approx>lst (op =) supp p ([atom b], Var c)"
+ − 72
apply (rule_tac x="(a \<leftrightarrow> b)" in exI)
+ − 73
apply (simp add: alphas trm_assn.supp supp_at_base x y fresh_star_def atom_eqvt)
+ − 74
by (metis Rep_name_inverse atom_name_def flip_fresh_fresh fresh_atom fresh_perm x y)
+ − 75
2720
+ − 76
lemma alpha_bn_refl: "alpha_bn x x"
+ − 77
apply (induct x rule: trm_assn.inducts(2))
+ − 78
apply (rule TrueI)
+ − 79
apply (auto simp add: trm_assn.eq_iff)
+ − 80
done
+ − 81
+ − 82
lemma alpha_bn_inducts_raw:
+ − 83
"\<lbrakk>alpha_bn_raw a b; P3 ANil_raw ANil_raw;
+ − 84
\<And>trm_raw trm_rawa assn_raw assn_rawa name namea.
+ − 85
\<lbrakk>alpha_trm_raw trm_raw trm_rawa; alpha_bn_raw assn_raw assn_rawa;
+ − 86
P3 assn_raw assn_rawa\<rbrakk>
+ − 87
\<Longrightarrow> P3 (ACons_raw name trm_raw assn_raw)
+ − 88
(ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b"
+ − 89
by (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts(3)[of _ _ "\<lambda>x y. True" _ "\<lambda>x y. True", simplified]) auto
+ − 90
+ − 91
lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted]
+ − 92
2854
+ − 93
lemma Abs_lst_fcb:
+ − 94
fixes xs ys :: "'a :: fs"
+ − 95
and S T :: "'b :: fs"
+ − 96
assumes e: "(Abs_lst (ba xs) T) = (Abs_lst (ba ys) S)"
+ − 97
and f1: "\<And>x. x \<in> set (ba xs) \<Longrightarrow> x \<sharp> f xs T"
+ − 98
and f2: "\<And>x. supp T - set (ba xs) = supp S - set (ba ys) \<Longrightarrow> x \<in> set (ba ys) \<Longrightarrow> x \<sharp> f xs T"
+ − 99
and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> p \<bullet> ba xs = ba ys \<Longrightarrow> supp p \<subseteq> set (ba xs) \<union> set (ba ys) \<Longrightarrow> p \<bullet> (f xs T) = f ys S"
+ − 100
shows "f xs T = f ys S"
+ − 101
using e apply -
+ − 102
apply(subst (asm) Abs_eq_iff2)
+ − 103
apply(simp add: alphas)
+ − 104
apply(elim exE conjE)
+ − 105
apply(rule trans)
+ − 106
apply(rule_tac p="p" in supp_perm_eq[symmetric])
+ − 107
apply(rule fresh_star_supp_conv)
+ − 108
apply(drule fresh_star_perm_set_conv)
+ − 109
apply(rule finite_Diff)
+ − 110
apply(rule finite_supp)
+ − 111
apply(subgoal_tac "(set (ba xs) \<union> set (ba ys)) \<sharp>* f xs T")
+ − 112
apply(metis Un_absorb2 fresh_star_Un)
+ − 113
apply(subst fresh_star_Un)
+ − 114
apply(rule conjI)
+ − 115
apply(simp add: fresh_star_def f1)
+ − 116
apply(simp add: fresh_star_def f2)
+ − 117
apply(simp add: eqv)
+ − 118
done
+ − 119
+ − 120
lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
+ − 121
by (simp add: permute_pure)
+ − 122
+ − 123
(* TODO: should be provided by nominal *)
+ − 124
lemma [eqvt]: "p \<bullet> bn a = bn (p \<bullet> a)"
+ − 125
by descending (rule eqvts)
+ − 126
+ − 127
(* PROBLEM: the proof needs induction on alpha_bn inside which is not possible... *)
+ − 128
nominal_primrec
+ − 129
height_trm :: "trm \<Rightarrow> nat"
+ − 130
and height_assn :: "assn \<Rightarrow> nat"
+ − 131
where
+ − 132
"height_trm (Var x) = 1"
+ − 133
| "height_trm (App l r) = max (height_trm l) (height_trm r)"
+ − 134
| "height_trm (Lam v b) = 1 + (height_trm b)"
+ − 135
| "height_trm (Let as b) = max (height_assn as) (height_trm b)"
+ − 136
| "height_assn ANil = 0"
+ − 137
| "height_assn (ACons v t as) = max (height_trm t) (height_assn as)"
+ − 138
apply (simp only: eqvt_def height_trm_height_assn_graph_def)
+ − 139
apply (rule, perm_simp, rule, rule TrueI)
+ − 140
apply (case_tac x)
+ − 141
apply (case_tac a rule: trm_assn.exhaust(1))
+ − 142
apply (auto)[4]
+ − 143
apply (drule_tac x="assn" in meta_spec)
+ − 144
apply (drule_tac x="trm" in meta_spec)
+ − 145
apply (simp add: alpha_bn_refl)
+ − 146
apply (case_tac b rule: trm_assn.exhaust(2))
+ − 147
apply (auto)
+ − 148
apply (erule Abs_lst1_fcb)
+ − 149
apply (simp_all add: pure_fresh)
+ − 150
apply (simp add: eqvt_at_def)
+ − 151
apply (erule Abs_lst_fcb)
+ − 152
apply (simp_all add: pure_fresh)
+ − 153
apply (simp_all add: eqvt_at_def eqvts)
+ − 154
oops
+ − 155
2720
+ − 156
nominal_primrec
+ − 157
subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
+ − 158
and substa :: "name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn"
+ − 159
where
+ − 160
"subst s t (Var x) = (if (s = x) then t else (Var x))"
+ − 161
| "subst s t (App l r) = App (subst s t l) (subst s t r)"
+ − 162
| "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)"
+ − 163
| "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (substa s t as) (subst s t b)"
+ − 164
| "substa s t ANil = ANil"
+ − 165
| "substa s t (ACons v t' as) = ACons v (subst v t t') as"
2842
+ − 166
(*unfolding eqvt_def subst_substa_graph_def
+ − 167
apply (rule, perm_simp)*)
+ − 168
defer
+ − 169
apply (rule TrueI)
+ − 170
apply (case_tac x)
+ − 171
apply (case_tac a)
+ − 172
apply (rule_tac y="c" and c="(aa,b)" in trm_assn.strong_exhaust(1))
+ − 173
apply (auto simp add: fresh_star_def)[3]
+ − 174
apply (drule_tac x="assn" in meta_spec)
+ − 175
apply (simp add: Abs1_eq_iff alpha_bn_refl)
+ − 176
apply (case_tac b)
+ − 177
apply (case_tac c rule: trm_assn.exhaust(2))
+ − 178
apply (auto)[2]
+ − 179
apply blast
+ − 180
apply blast
+ − 181
apply auto
+ − 182
apply (simp_all add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
+ − 183
apply (simp_all add: meta_eq_to_obj_eq[OF substa_def, symmetric, unfolded fun_eq_iff])
2854
+ − 184
(*apply (erule Abs_lst1_fcb)*)
2842
+ − 185
prefer 3
+ − 186
apply (erule alpha_bn_inducts)
+ − 187
apply (simp add: alpha_bn_refl)
+ − 188
(* Needs an invariant *)
+ − 189
oops
2720
+ − 190
1600
+ − 191
end
+ − 192
+ − 193
+ − 194