equal
deleted
inserted
replaced
126 shows "Lam a t = Lam b s" |
126 shows "Lam a t = Lam b s" |
127 using a |
127 using a |
128 unfolding fresh_def supp_def |
128 unfolding fresh_def supp_def |
129 sorry |
129 sorry |
130 |
130 |
131 lemma perm_rsp[quot_rsp]: |
131 lemma perm_rsp[quotient_rsp]: |
132 "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" |
132 "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" |
133 apply(auto) |
133 apply(auto) |
134 (* this is propably true if some type conditions are imposed ;o) *) |
134 (* this is propably true if some type conditions are imposed ;o) *) |
135 sorry |
135 sorry |
136 |
136 |
138 "(op = ===> alpha ===> op =) fresh fresh" |
138 "(op = ===> alpha ===> op =) fresh fresh" |
139 apply(auto) |
139 apply(auto) |
140 (* this is probably only true if some type conditions are imposed *) |
140 (* this is probably only true if some type conditions are imposed *) |
141 sorry |
141 sorry |
142 |
142 |
143 lemma rVar_rsp[quot_rsp]: |
143 lemma rVar_rsp[quotient_rsp]: |
144 "(op = ===> alpha) rVar rVar" |
144 "(op = ===> alpha) rVar rVar" |
145 by (auto intro:a1) |
145 by (auto intro:a1) |
146 |
146 |
147 lemma rApp_rsp[quot_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp" |
147 lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp" |
148 by (auto intro:a2) |
148 by (auto intro:a2) |
149 |
149 |
150 lemma rLam_rsp[quot_rsp]: "(op = ===> alpha ===> alpha) rLam rLam" |
150 lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam" |
151 apply(auto) |
151 apply(auto) |
152 apply(rule a3) |
152 apply(rule a3) |
153 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) |
154 apply(rule sym) |
154 apply(rule sym) |
155 apply(rule trans) |
155 apply(rule trans) |
158 apply(simp add: pt_name1) |
158 apply(simp add: pt_name1) |
159 apply(assumption) |
159 apply(assumption) |
160 apply(simp add: abs_fresh) |
160 apply(simp add: abs_fresh) |
161 done |
161 done |
162 |
162 |
163 lemma rfv_rsp[quot_rsp]: "(alpha ===> op =) rfv rfv" |
163 lemma rfv_rsp[quotient_rsp]: "(alpha ===> op =) rfv rfv" |
164 sorry |
164 sorry |
165 |
165 |
166 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)" |
166 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)" |
167 apply (auto) |
167 apply (auto) |
168 apply (erule alpha.cases) |
168 apply (erule alpha.cases) |
172 ML {* val qty = @{typ "lam"} *} |
172 ML {* val qty = @{typ "lam"} *} |
173 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} |
173 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} |
174 |
174 |
175 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
175 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
176 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
176 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
177 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] [quot] *} |
177 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] *} |
178 |
178 |
179 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
179 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
180 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
180 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
181 done |
181 done |
182 |
182 |