equal
deleted
inserted
replaced
28 have "\<And>(pi::name prm) x. P x (pi\<bullet>t)" |
28 have "\<And>(pi::name prm) x. P x (pi\<bullet>t)" |
29 proof (induct rule: lam.induct_weak) |
29 proof (induct rule: lam.induct_weak) |
30 case (Lam a t) |
30 case (Lam a t) |
31 have ih: "\<And>(pi::name prm) x. P x (pi\<bullet>t)" by fact |
31 have ih: "\<And>(pi::name prm) x. P x (pi\<bullet>t)" by fact |
32 show "\<And>(pi::name prm) x. P x (pi\<bullet>(Lam [a].t))" |
32 show "\<And>(pi::name prm) x. P x (pi\<bullet>(Lam [a].t))" |
33 proof (simp add: abs_perm) |
33 proof (simp) |
34 fix x::"'a" and pi::"name prm" |
34 fix x::"'a" and pi::"name prm" |
35 have "\<exists>c::name. c\<sharp>(f x,pi\<bullet>a,pi\<bullet>t)" |
35 have "\<exists>c::name. c\<sharp>(f x,pi\<bullet>a,pi\<bullet>t)" |
36 by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1 fs) |
36 by (rule at_exists_fresh[OF at_name_inst], simp add: supp_prod fs_name1 fs) |
37 then obtain c::"name" |
37 then obtain c::"name" |
38 where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(f x)" and f3: "c\<sharp>(pi\<bullet>t)" |
38 where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(f x)" and f3: "c\<sharp>(pi\<bullet>t)" |