32 thm single_let.eq_iff |
32 thm single_let.eq_iff |
33 thm single_let.fv_bn_eqvt |
33 thm single_let.fv_bn_eqvt |
34 thm single_let.size_eqvt |
34 thm single_let.size_eqvt |
35 thm single_let.supports |
35 thm single_let.supports |
36 thm single_let.fsupp |
36 thm single_let.fsupp |
|
37 thm single_let.supp |
37 |
38 |
38 lemma test2: |
39 lemma test2: |
39 assumes "fv_trm t = supp t" |
40 assumes "fv_trm t = supp t" |
40 shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)" |
41 shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)" |
41 apply(rule allI) |
42 apply(rule allI) |
42 apply(rule_tac p="-p" in permute_boolE) |
43 apply(rule_tac p="-p" in permute_boolE) |
43 apply(perm_simp add: single_let.fv_bn_eqvt permute_minus_cancel) |
44 apply(perm_simp add: single_let.fv_bn_eqvt permute_minus_cancel) |
44 apply(rule assms) |
45 apply(rule assms) |
45 done |
46 done |
46 |
47 |
47 |
|
48 lemma supp_fv: |
48 lemma supp_fv: |
49 "fv_trm t = supp t" "fv_assg as = supp as" "fv_bn as = supp_rel alpha_bn as" |
49 "fv_trm x = supp x" |
50 apply(induct t and as rule: single_let.inducts) |
50 "fv_assg xa = supp xa" |
|
51 "fv_bn xa = supp_rel alpha_bn xa" |
|
52 apply(induct rule: single_let.inducts) |
51 -- " 0A " |
53 -- " 0A " |
52 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
54 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
53 apply(simp only: supp_abs(3)[symmetric])? |
|
54 apply(simp (no_asm) only: supp_def) |
55 apply(simp (no_asm) only: supp_def) |
55 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
56 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
56 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
57 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
57 -- " 0B" |
58 -- " 0B" |
58 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
59 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
59 apply(simp only: supp_abs(3)[symmetric])? |
|
60 apply(simp (no_asm) only: supp_def) |
60 apply(simp (no_asm) only: supp_def) |
61 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
61 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
62 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
62 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
63 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
63 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
64 --" 1 " |
64 --" 1 " |
65 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
65 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
66 apply(simp only: supp_abs(3)[symmetric]) |
66 apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *}) |
67 apply(simp (no_asm) only: supp_def) |
67 apply(simp (no_asm) only: supp_def) |
68 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
68 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
69 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
69 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
70 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
70 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
71 apply(drule test2) |
71 apply(drule test2) |
72 apply(simp only:) |
72 apply(simp only:) |
73 -- " 2 " |
73 -- " 2 " |
74 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
74 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
75 apply(simp only: supp_abs(3)[symmetric]) |
75 apply(subst supp_abs(3)[symmetric]) |
76 apply(simp (no_asm) only: supp_def supp_rel_def) |
76 apply(simp (no_asm) only: supp_def supp_rel_def) |
77 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
77 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
78 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
78 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
79 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
79 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
80 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
80 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
81 apply(drule test2) |
81 apply(drule test2) |
82 apply(simp only:) |
82 apply(simp only:) |
83 -- " 3 " |
83 -- " 3 " |
84 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
84 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
85 apply(simp only: supp_abs(1)[symmetric]) |
85 apply(subst supp_abs(1)[symmetric]) |
86 apply(simp (no_asm) only: supp_def supp_rel_def) |
86 apply(simp (no_asm) only: supp_def supp_rel_def) |
87 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
87 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
88 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
88 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
89 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
89 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
90 apply(drule test2)+ |
90 apply(drule test2)+ |
91 apply(simp only: supp_Pair Un_assoc conj_assoc) |
91 apply(simp only: supp_Pair Un_assoc conj_assoc) |
92 -- " Bar " |
92 -- " Bar " |
93 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
93 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
94 apply(simp only: supp_abs(3)[symmetric]) |
94 apply(subst supp_abs(3)[symmetric]) |
95 apply(simp (no_asm) only: supp_def) |
95 apply(simp (no_asm) only: supp_def) |
96 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
96 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
97 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
97 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
98 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
98 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
99 apply(drule test2)+ |
99 apply(drule test2)+ |
100 apply(simp only: supp_Pair Un_assoc conj_assoc) |
100 apply(simp only: supp_Pair Un_assoc conj_assoc) |
101 -- " Baz " |
101 -- " Baz " |
102 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
102 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
103 apply(simp only: supp_abs(3)[symmetric]) |
103 apply(subst supp_abs(1)[symmetric]) |
|
104 apply(subst supp_abs(1)[symmetric]) |
104 apply(simp (no_asm) only: supp_def) |
105 apply(simp (no_asm) only: supp_def) |
105 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
106 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
106 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
107 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
107 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
108 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
108 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
109 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
109 apply(drule test2)+ |
110 apply(drule test2)+ |
110 apply(simp only: supp_Pair Un_assoc conj_assoc) |
111 apply(simp only: supp_Pair Un_assoc conj_assoc) |
111 -- "last" |
112 -- "last" |
112 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
113 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
113 apply(simp only: supp_abs(3)[symmetric]) |
114 apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *}) |
114 apply(simp (no_asm) only: supp_def supp_rel_def) |
115 apply(simp (no_asm) only: supp_def supp_rel_def) |
115 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
116 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
116 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
117 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
117 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
118 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
118 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
119 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |