equal
deleted
inserted
replaced
34 lemma size_rsp: |
34 lemma size_rsp: |
35 "alpha_t_raw x y \<Longrightarrow> size x = size y" |
35 "alpha_t_raw x y \<Longrightarrow> size x = size y" |
36 "alpha_tyS_raw a b \<Longrightarrow> size a = size b" |
36 "alpha_tyS_raw a b \<Longrightarrow> size a = size b" |
37 apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts) |
37 apply (induct rule: alpha_t_raw_alpha_tyS_raw.inducts) |
38 apply (simp_all only: t_raw_tyS_raw.size) |
38 apply (simp_all only: t_raw_tyS_raw.size) |
39 apply (simp_all only: alpha_gen) |
39 apply (simp_all only: alphas) |
40 apply clarify |
40 apply clarify |
41 apply (simp_all only: size_eqvt_raw) |
41 apply (simp_all only: size_eqvt_raw) |
42 done |
42 done |
43 |
43 |
44 lemma [quot_respect]: |
44 lemma [quot_respect]: |
117 |
117 |
118 lemma |
118 lemma |
119 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
119 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
120 apply(simp add: t_tyS.eq_iff) |
120 apply(simp add: t_tyS.eq_iff) |
121 apply(rule_tac x="0::perm" in exI) |
121 apply(rule_tac x="0::perm" in exI) |
122 apply(simp add: alpha_gen) |
122 apply(simp add: alphas) |
123 apply(auto) |
123 apply(auto) |
124 apply(simp add: fresh_star_def fresh_zero_perm) |
124 apply(simp add: fresh_star_def fresh_zero_perm) |
125 done |
125 done |
126 |
126 |
127 lemma |
127 lemma |