117 lemma pi_lam_com: |
117 lemma pi_lam_com: |
118 fixes pi::"'x prm" |
118 fixes pi::"'x prm" |
119 shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)" |
119 shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)" |
120 sorry |
120 sorry |
121 |
121 |
|
122 |
|
123 |
122 lemma real_alpha: |
124 lemma real_alpha: |
123 assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s" |
125 assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s" |
124 shows "Lam a t = Lam b s" |
126 shows "Lam a t = Lam b s" |
|
127 using a |
|
128 unfolding fresh_def supp_def |
125 sorry |
129 sorry |
126 |
130 |
127 lemma perm_rsp: |
131 lemma perm_rsp[quot_rsp]: |
128 "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" |
132 "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" |
129 apply(auto) |
133 apply(auto) |
130 (* this is propably true if some type conditions are imposed ;o) *) |
134 (* this is propably true if some type conditions are imposed ;o) *) |
131 sorry |
135 sorry |
132 |
136 |
133 lemma fresh_rsp: |
137 lemma fresh_rsp: |
134 "(op = ===> alpha ===> op =) fresh fresh" |
138 "(op = ===> alpha ===> op =) fresh fresh" |
135 apply(auto) |
139 apply(auto) |
136 (* this is probably only true if some type conditions are imposed *) |
140 (* this is probably only true if some type conditions are imposed *) |
137 sorry |
141 sorry |
138 |
142 |
139 lemma rVar_rsp: "(op = ===> alpha) rVar rVar" |
143 lemma rVar_rsp[quot_rsp]: |
140 apply(auto) |
144 "(op = ===> alpha) rVar rVar" |
141 apply(rule a1) |
145 by (auto intro:a1) |
142 apply(simp) |
146 |
143 done |
147 lemma rApp_rsp[quot_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp" |
144 |
148 by (auto intro:a2) |
145 lemma rApp_rsp: "(alpha ===> alpha ===> alpha) rApp rApp" |
149 |
146 apply(auto) |
150 lemma rLam_rsp[quot_rsp]: "(op = ===> alpha ===> alpha) rLam rLam" |
147 apply(rule a2) |
|
148 apply (assumption) |
|
149 apply (assumption) |
|
150 done |
|
151 |
|
152 lemma rLam_rsp: "(op = ===> alpha ===> alpha) rLam rLam" |
|
153 apply(auto) |
151 apply(auto) |
154 apply(rule a3) |
152 apply(rule a3) |
155 apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst) |
153 apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst) |
156 apply(rule sym) |
154 apply(rule sym) |
157 apply(rule trans) |
155 apply(rule trans) |
160 apply(simp add: pt_name1) |
158 apply(simp add: pt_name1) |
161 apply(assumption) |
159 apply(assumption) |
162 apply(simp add: abs_fresh) |
160 apply(simp add: abs_fresh) |
163 done |
161 done |
164 |
162 |
165 lemma rfv_rsp: "(alpha ===> op =) rfv rfv" |
163 lemma rfv_rsp[quot_rsp]: "(alpha ===> op =) rfv rfv" |
166 sorry |
164 sorry |
167 |
165 |
168 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)" |
166 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)" |
169 apply (auto) |
167 apply (auto) |
170 apply (erule alpha.cases) |
168 apply (erule alpha.cases) |
177 @{thms ho_all_prs ho_ex_prs} *} |
175 @{thms ho_all_prs ho_ex_prs} *} |
178 |
176 |
179 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
177 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
180 ML {* val consts = lookup_quot_consts defs *} |
178 ML {* val consts = lookup_quot_consts defs *} |
181 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
179 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
182 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *} |
180 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
183 |
181 |
184 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
182 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
185 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
183 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
186 done |
184 done |
187 |
185 |
232 apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) |
230 apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) |
233 done |
231 done |
234 |
232 |
235 lemma var_inject: "(Var a = Var b) = (a = b)" |
233 lemma var_inject: "(Var a = Var b) = (a = b)" |
236 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *}) |
234 apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *}) |
|
235 done |
|
236 |
|
237 lemma lam_induct:" \<lbrakk>\<And>name. P (Var name); \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
|
238 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam" |
|
239 apply (tactic {* lift_tac_lam @{context} @{thm rlam.induct} 1 *}) |
237 done |
240 done |
238 |
241 |
239 lemma var_supp: |
242 lemma var_supp: |
240 shows "supp (Var a) = ((supp a)::name set)" |
243 shows "supp (Var a) = ((supp a)::name set)" |
241 apply(simp add: supp_def) |
244 apply(simp add: supp_def) |