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 thm single_let.supp |
38 |
38 |
39 lemma test2: |
|
40 assumes "fv_trm t = supp t" |
|
41 shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)" |
|
42 apply(rule allI) |
|
43 apply(rule_tac p="-p" in permute_boolE) |
|
44 apply(perm_simp add: single_let.fv_bn_eqvt permute_minus_cancel) |
|
45 apply(rule assms) |
|
46 done |
|
47 |
39 |
48 lemma supp_fv: |
|
49 "fv_trm x = supp x" |
|
50 "fv_assg xa = supp xa" |
|
51 "fv_bn xa = supp_rel alpha_bn xa" |
|
52 apply(induct rule: single_let.inducts) |
|
53 -- " 0A " |
|
54 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
|
55 apply(simp (no_asm) only: supp_def) |
|
56 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
|
57 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
|
58 -- " 0B" |
|
59 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
|
60 apply(simp (no_asm) only: supp_def) |
|
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) |
|
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 " |
|
65 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
|
66 apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *}) |
|
67 apply(simp (no_asm) only: supp_def) |
|
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) |
|
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) |
|
72 apply(simp only:) |
|
73 -- " 2 " |
|
74 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
|
75 apply(subst supp_abs(3)[symmetric]) |
|
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) |
|
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) |
|
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) |
|
82 apply(simp only:) |
|
83 -- " 3 " |
|
84 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
|
85 apply(subst supp_abs(1)[symmetric]) |
|
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) |
|
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) |
|
90 apply(drule test2)+ |
|
91 apply(simp only: supp_Pair Un_assoc conj_assoc) |
|
92 -- " Bar " |
|
93 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
|
94 apply(subst supp_abs(3)[symmetric]) |
|
95 apply(simp (no_asm) only: supp_def) |
|
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) |
|
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)+ |
|
100 apply(simp only: supp_Pair Un_assoc conj_assoc) |
|
101 -- " Baz " |
|
102 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
|
103 apply(subst supp_abs(1)[symmetric]) |
|
104 apply(subst supp_abs(1)[symmetric]) |
|
105 apply(simp (no_asm) only: supp_def) |
|
106 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
|
107 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
|
108 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
|
109 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
|
110 apply(drule test2)+ |
|
111 apply(simp only: supp_Pair Un_assoc conj_assoc) |
|
112 -- "last" |
|
113 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
|
114 apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *}) |
|
115 apply(simp (no_asm) only: supp_def supp_rel_def) |
|
116 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
|
117 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
|
118 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
|
119 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
|
120 apply(drule test2)+ |
|
121 apply(simp only: supp_Pair Un_assoc conj_assoc) |
|
122 -- "other case" |
|
123 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
|
124 apply(simp only: supp_abs(3)[symmetric]) |
|
125 apply(simp (no_asm) only: supp_def supp_rel_def) |
|
126 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
|
127 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
|
128 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
|
129 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)? |
|
130 apply(drule test2)+ |
|
131 apply(simp only: supp_Pair Un_assoc conj_assoc) |
|
132 done |
|
133 |
|
134 |
|
135 |
|
136 |
|
137 |
|
138 text {* *} |
|
139 |
|
140 (* |
|
141 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm" |
|
142 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg" |
|
143 |
|
144 lemma y: |
|
145 "perm_bn_trm p (Var x) = (Var x)" |
|
146 "perm_bn_trm p (App t1 t2) = (App t1 t2)" |
|
147 "perm_bn_trm p (" |
|
148 |
|
149 |
|
150 |
|
151 typ trm |
|
152 typ assg |
|
153 |
|
154 thm trm_assg.fv |
|
155 thm trm_assg.supp |
|
156 thm trm_assg.eq_iff |
|
157 thm trm_assg.bn |
|
158 thm trm_assg.perm |
|
159 thm trm_assg.induct |
|
160 thm trm_assg.inducts |
|
161 thm trm_assg.distinct |
|
162 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
|
163 *) |
|
164 |
40 |
165 |
41 |
166 |
42 |
167 end |
43 end |
168 |
44 |