136 lemma [quot_respect]: |
136 lemma [quot_respect]: |
137 "(op = ===> alpha1) rVr1 rVr1" |
137 "(op = ===> alpha1) rVr1 rVr1" |
138 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1" |
138 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1" |
139 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1" |
139 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1" |
140 "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1" |
140 "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1" |
141 apply (auto intro: alpha1.intros) |
141 apply (auto simp add: alpha1_inj) |
142 apply(rule a3) apply (rule_tac x="0" in exI) |
142 apply (rule_tac x="0" in exI) |
143 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen) |
143 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen) |
144 apply(rule a4) apply assumption apply (rule_tac x="0" in exI) |
144 apply (rule_tac x="0" in exI) |
145 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen) |
145 apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1) |
146 done |
146 done |
147 |
147 |
148 lemma [quot_respect]: |
148 lemma [quot_respect]: |
149 "(op = ===> alpha1 ===> alpha1) permute permute" |
149 "(op = ===> alpha1 ===> alpha1) permute permute" |
150 apply auto |
150 by (simp add: alpha1_eqvt) |
151 apply (rule alpha1_eqvt) |
|
152 apply simp |
|
153 done |
|
154 |
151 |
155 lemma [quot_respect]: |
152 lemma [quot_respect]: |
156 "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1" |
153 "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1" |
157 apply (simp add: alpha_rfv1) |
154 by (simp add: alpha_rfv1) |
158 done |
|
159 |
155 |
160 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
156 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
161 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
157 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
162 |
158 |
163 instantiation trm1 and bp :: pt |
159 instantiation trm1 and bp :: pt |
590 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
586 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
591 "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons" |
587 "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons" |
592 "(op = ===> alpha5 ===> alpha5) permute permute" |
588 "(op = ===> alpha5 ===> alpha5) permute permute" |
593 "(op = ===> alphalts ===> alphalts) permute permute" |
589 "(op = ===> alphalts ===> alphalts) permute permute" |
594 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
590 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
595 apply (auto) |
591 apply (clarify) apply (rule conjI) |
596 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
592 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
597 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
593 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
594 apply (clarify) apply (rule conjI) |
598 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
595 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
599 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
596 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
600 done |
597 done |
601 |
598 |
602 lemma |
599 lemma |