equal
deleted
inserted
replaced
32 thm foo.inducts |
32 thm foo.inducts |
33 thm foo.exhaust |
33 thm foo.exhaust |
34 thm foo.fv_defs |
34 thm foo.fv_defs |
35 thm foo.bn_defs |
35 thm foo.bn_defs |
36 thm foo.perm_simps |
36 thm foo.perm_simps |
37 thm foo.eq_iff |
37 thm foo.eq_iff(5) |
38 thm foo.fv_bn_eqvt |
38 thm foo.fv_bn_eqvt |
39 thm foo.size_eqvt |
39 thm foo.size_eqvt |
40 thm foo.supports |
40 thm foo.supports |
41 thm foo.fsupp |
41 thm foo.fsupp |
42 thm foo.supp |
42 thm foo.supp |
72 apply(simp only: permute_Abs) |
72 apply(simp only: permute_Abs) |
73 apply(simp only: tt1) |
73 apply(simp only: tt1) |
74 apply(simp only: foo.eq_iff) |
74 apply(simp only: foo.eq_iff) |
75 apply(simp add: uu1) |
75 apply(simp add: uu1) |
76 done |
76 done |
|
77 |
|
78 lemma Let2_rename: |
|
79 assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(supp ([[atom y]]lst. t2)) \<sharp>* p" |
|
80 shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)" |
|
81 using assms |
|
82 apply - |
|
83 apply(drule supp_perm_eq[symmetric]) |
|
84 apply(drule supp_perm_eq[symmetric]) |
|
85 apply(simp only: foo.eq_iff) |
|
86 apply(simp only: eqvts) |
|
87 apply simp |
|
88 done |
77 |
89 |
78 lemma strong_exhaust1: |
90 lemma strong_exhaust1: |
79 fixes c::"'a::fs" |
91 fixes c::"'a::fs" |
80 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
92 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
81 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
93 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |