88 (ACons_raw namea trm_rawa assn_rawa)\<rbrakk> \<Longrightarrow> P3 a b" |
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 |
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 |
90 |
91 lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted] |
91 lemmas alpha_bn_inducts = alpha_bn_inducts_raw[quot_lifted] |
92 |
92 |
|
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 |
93 nominal_primrec |
156 nominal_primrec |
94 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
157 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
95 and substa :: "name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn" |
158 and substa :: "name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn" |
96 where |
159 where |
97 "subst s t (Var x) = (if (s = x) then t else (Var x))" |
160 "subst s t (Var x) = (if (s = x) then t else (Var x))" |
116 apply blast |
179 apply blast |
117 apply blast |
180 apply blast |
118 apply auto |
181 apply auto |
119 apply (simp_all add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) |
182 apply (simp_all add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) |
120 apply (simp_all add: meta_eq_to_obj_eq[OF substa_def, symmetric, unfolded fun_eq_iff]) |
183 apply (simp_all add: meta_eq_to_obj_eq[OF substa_def, symmetric, unfolded fun_eq_iff]) |
|
184 (*apply (erule Abs_lst1_fcb)*) |
121 prefer 3 |
185 prefer 3 |
122 apply (erule alpha_bn_inducts) |
186 apply (erule alpha_bn_inducts) |
123 apply (simp add: alpha_bn_refl) |
187 apply (simp add: alpha_bn_refl) |
124 (* Needs an invariant *) |
188 (* Needs an invariant *) |
125 oops |
189 oops |