112 thm perm_defs[no_vars] |
112 thm perm_defs[no_vars] |
113 |
113 |
114 instance trm :: pt sorry |
114 instance trm :: pt sorry |
115 instance assg :: pt sorry |
115 instance assg :: pt sorry |
116 |
116 |
117 lemma |
117 lemma b1: |
118 "p \<bullet> Var name = Var (p \<bullet> name)" |
118 "p \<bullet> Var name = Var (p \<bullet> name)" |
119 "p \<bullet> App trm1 trm2 = App (p \<bullet> trm1) (p \<bullet> trm2)" |
119 "p \<bullet> App trm1 trm2 = App (p \<bullet> trm1) (p \<bullet> trm2)" |
120 "p \<bullet> Lam name trm = Lam (p \<bullet> name) (p \<bullet> trm)" |
120 "p \<bullet> Lam name trm = Lam (p \<bullet> name) (p \<bullet> trm)" |
121 "p \<bullet> Let assg trm = Let (p \<bullet> assg) (p \<bullet> trm)" |
121 "p \<bullet> Let assg trm = Let (p \<bullet> assg) (p \<bullet> trm)" |
122 "p \<bullet> Foo name1 name2 trm1 trm2 trm3 = |
122 "p \<bullet> Foo name1 name2 trm1 trm2 trm3 = |
131 ML {* |
131 ML {* |
132 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_defs} |
132 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_defs} |
133 *} |
133 *} |
134 *) |
134 *) |
135 |
135 |
|
136 thm eq_iff[no_vars] |
|
137 |
|
138 ML {* |
|
139 val q1 = lift_thm [@{typ trm}, @{typ assg}] @{context} @{thm "eq_iff"(1)} |
|
140 *} |
|
141 |
136 local_setup {* Local_Theory.note ((@{binding d1}, []), thms_d) #> snd *} |
142 local_setup {* Local_Theory.note ((@{binding d1}, []), thms_d) #> snd *} |
137 local_setup {* Local_Theory.note ((@{binding i1}, []), thms_i) #> snd *} |
143 local_setup {* Local_Theory.note ((@{binding i1}, []), thms_i) #> snd *} |
138 local_setup {* Local_Theory.note ((@{binding f1}, []), thms_f) #> snd *} |
144 local_setup {* Local_Theory.note ((@{binding f1}, []), thms_f) #> snd *} |
|
145 local_setup {* Local_Theory.note ((@{binding q1}, []), [q1]) #> snd *} |
|
146 |
139 |
147 |
140 thm perm_defs |
148 thm perm_defs |
141 thm perm_simps |
149 thm perm_simps |
142 |
|
143 instance trm :: pt sorry |
|
144 instance assg :: pt sorry |
|
145 |
150 |
146 lemma supp_fv: |
151 lemma supp_fv: |
147 "supp t = fv_trm t" |
152 "supp t = fv_trm t" |
148 "supp b = fv_bn b" |
153 "supp b = fv_bn b" |
149 apply(induct t and b rule: i1) |
154 apply(induct t and b rule: i1) |
150 apply(simp_all add: f1) |
155 apply(simp_all add: f1) |
151 apply(simp_all add: supp_def) |
156 apply(simp_all add: supp_def) |
152 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
157 apply(simp_all add: b1) |
153 apply(simp only: supp_at_base[simplified supp_def]) |
158 sorry |
154 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
159 |
155 apply(simp add: Collect_imp_eq Collect_neg_eq Un_commute) |
160 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm" |
156 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") |
161 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg" |
157 apply(simp add: supp_Abs fv_trm1) |
162 |
158 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) |
163 lemma y: |
159 apply(simp add: alpha1_INJ) |
164 "perm_bn_trm p (Var x) = (Var x)" |
160 apply(simp add: Abs_eq_iff) |
165 "perm_bn_trm p (App t1 t2) = (App t1 t2)" |
161 apply(simp add: alpha_gen.simps) |
166 "perm_bn_trm p (" |
162 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
167 |
163 apply(simp add: supp_fv_let fv_trm1 fv_eq_bv supp_Pair) |
168 |
164 apply blast |
|
165 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
166 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
167 apply(simp only: supp_at_base[simplified supp_def]) |
|
168 apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1 alpha1_INJ[simplified alpha_bp_eq]) |
|
169 apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric]) |
|
170 apply(fold supp_def) |
|
171 apply simp |
|
172 done |
|
173 |
169 |
174 ML {* |
170 ML {* |
175 map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff} |
171 map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff} |
176 *} |
172 *} |
177 |
173 |