equal
deleted
inserted
replaced
358 then have "P a (([]::name prm) \<bullet> lam)" by blast |
358 then have "P a (([]::name prm) \<bullet> lam)" by blast |
359 then show "P a lam" by simp |
359 then show "P a lam" by simp |
360 qed |
360 qed |
361 |
361 |
362 |
362 |
363 lemma var_supp: |
|
364 shows "supp (Var a) = ((supp a)::name set)" |
|
365 apply(simp add: supp_def) |
|
366 apply(simp add: pi_var2) |
|
367 apply(simp add: var_inject) |
|
368 done |
|
369 |
|
370 lemma var_fresh: |
363 lemma var_fresh: |
371 fixes a::"name" |
364 fixes a::"name" |
372 shows "(a \<sharp> (Var b)) = (a \<sharp> b)" |
365 shows "(a \<sharp> (Var b)) = (a \<sharp> b)" |
373 apply(simp add: fresh_def) |
366 apply(simp add: fresh_def) |
374 apply(simp add: var_supp) |
367 apply(simp add: var_supp1) |
375 done |
368 done |
376 |
369 |
377 end |
370 end |