equal
deleted
inserted
replaced
101 by(simp) |
101 by(simp) |
102 next |
102 next |
103 assume "a \<noteq> z" |
103 assume "a \<noteq> z" |
104 thus ?thesis |
104 thus ?thesis |
105 using assms |
105 using assms |
106 by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left) |
106 by (simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left) |
107 qed |
107 qed |
108 |
108 |
109 lemma alphaInput_mix: |
109 lemma alphaInput_mix: |
110 fixes a :: name |
110 fixes a :: name |
111 and b :: name |
111 and b :: name |
121 by(simp) |
121 by(simp) |
122 next |
122 next |
123 assume "b \<noteq> z" |
123 assume "b \<noteq> z" |
124 thus ?thesis |
124 thus ?thesis |
125 using assms |
125 using assms |
126 by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left) |
126 by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left) |
127 qed |
127 qed |
128 |
128 |
129 lemma alphaRep_mix: |
129 lemma alphaRep_mix: |
130 fixes a :: name |
130 fixes a :: name |
131 and b :: name |
131 and b :: name |
141 by(simp) |
141 by(simp) |
142 next |
142 next |
143 assume "b \<noteq> z" |
143 assume "b \<noteq> z" |
144 thus ?thesis |
144 thus ?thesis |
145 using assms |
145 using assms |
146 by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left) |
146 by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left) |
147 qed |
147 qed |
148 |
148 |
149 subsection {* Capture-Avoiding Substitution of Names *} |
149 subsection {* Capture-Avoiding Substitution of Names *} |
150 |
150 |
151 lemma testl: |
151 lemma testl: |
391 apply simp |
391 apply simp |
392 apply (erule fresh_eqvt_at) |
392 apply (erule fresh_eqvt_at) |
393 apply(simp add: finite_supp) |
393 apply(simp add: finite_supp) |
394 apply(simp) |
394 apply(simp) |
395 apply(simp add: eqvt_at_def) |
395 apply(simp add: eqvt_at_def) |
396 apply(drule_tac x="(atom b \<rightleftharpoons> atom ba)" in spec) |
396 apply(drule_tac x="(b \<leftrightarrow> ba)" in spec) |
397 apply(simp) |
397 apply(simp) |
398 done |
398 done |
399 |
399 |
400 termination (eqvt) |
400 termination (eqvt) |
401 by (lexicographic_order) |
401 by (lexicographic_order) |