equal
deleted
inserted
replaced
119 |
119 |
120 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
120 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
121 by (simp add: permute_pure) |
121 by (simp add: permute_pure) |
122 |
122 |
123 (* TODO: should be provided by nominal *) |
123 (* TODO: should be provided by nominal *) |
124 lemma [eqvt]: "p \<bullet> bn a = bn (p \<bullet> a)" |
124 lemmas [eqvt] = trm_assn.fv_bn_eqvt |
125 by descending (rule eqvts) |
|
126 |
125 |
127 (* PROBLEM: the proof needs induction on alpha_bn inside which is not possible... *) |
126 (* PROBLEM: the proof needs induction on alpha_bn inside which is not possible... *) |
128 nominal_primrec |
127 nominal_primrec |
129 height_trm :: "trm \<Rightarrow> nat" |
128 height_trm :: "trm \<Rightarrow> nat" |
130 and height_assn :: "assn \<Rightarrow> nat" |
129 and height_assn :: "assn \<Rightarrow> nat" |
149 apply (simp_all add: pure_fresh) |
148 apply (simp_all add: pure_fresh) |
150 apply (simp add: eqvt_at_def) |
149 apply (simp add: eqvt_at_def) |
151 apply (erule Abs_lst_fcb) |
150 apply (erule Abs_lst_fcb) |
152 apply (simp_all add: pure_fresh) |
151 apply (simp_all add: pure_fresh) |
153 apply (simp_all add: eqvt_at_def eqvts) |
152 apply (simp_all add: eqvt_at_def eqvts) |
|
153 apply (rule arg_cong) back |
154 oops |
154 oops |
155 |
155 |
156 nominal_primrec |
156 nominal_primrec |
157 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
157 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
158 and substa :: "name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn" |
158 and substa :: "name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn" |