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[quotient_rsp]: |
131 lemma perm_rsp[quot_respect]: |
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[quotient_rsp]: |
143 lemma rVar_rsp[quot_respect]: |
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[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp" |
147 lemma rApp_rsp[quot_respect]: "(alpha ===> alpha ===> alpha) rApp rApp" |
148 by (auto intro:a2) |
148 by (auto intro:a2) |
149 |
149 |
150 lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam" |
150 lemma rLam_rsp[quot_respect]: "(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[quotient_rsp]: "(alpha ===> op =) rfv rfv" |
163 lemma rfv_rsp[quot_respect]: "(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) |