equal
deleted
inserted
replaced
10 Var "name" |
10 Var "name" |
11 | Fun "t" "t" |
11 | Fun "t" "t" |
12 and tyS = |
12 and tyS = |
13 All xs::"name fset" ty::"t" bind xs in ty |
13 All xs::"name fset" ty::"t" bind xs in ty |
14 |
14 |
15 lemma t_tyS_supp_fv: "fv_t t = supp t \<and> fv_tyS tyS = supp tyS" |
15 lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp] |
16 apply (induct rule: t_tyS.induct) |
|
17 apply (simp_all only: t_tyS.fv) |
|
18 apply (simp_all only: supp_abs(2)[symmetric]) |
|
19 apply(simp_all (no_asm) only: supp_def) |
|
20 apply(simp_all only: t_tyS.perm permute_abs) |
|
21 apply(simp only: t_tyS.eq_iff supp_at_base[simplified supp_def]) |
|
22 apply(simp only: t_tyS.eq_iff Collect_disj_eq[symmetric] infinite_Un[symmetric]) |
|
23 apply simp |
|
24 apply(simp only: Abs_eq_iff t_tyS.eq_iff) |
|
25 apply (simp add: alphas) |
|
26 apply (simp add: eqvts[symmetric]) |
|
27 apply (simp add: eqvts eqvts_raw) |
|
28 done |
|
29 |
|
30 lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS_supp_fv] |
|
31 |
|
32 |
16 |
33 lemma size_eqvt_raw: |
17 lemma size_eqvt_raw: |
34 "size (pi \<bullet> t :: t_raw) = size t" |
18 "size (pi \<bullet> t :: t_raw) = size t" |
35 "size (pi \<bullet> ts :: tyS_raw) = size ts" |
19 "size (pi \<bullet> ts :: tyS_raw) = size ts" |
36 apply (induct rule: t_raw_tyS_raw.inducts) |
20 apply (induct rule: t_raw_tyS_raw.inducts) |