equal
deleted
inserted
replaced
109 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
109 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
110 where |
110 where |
111 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
111 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
112 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
112 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
113 | a3: "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s)) \<Longrightarrow> rLam a t \<approx> rLam b s" |
113 | a3: "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s)) \<Longrightarrow> rLam a t \<approx> rLam b s" |
114 |
114 print_theorems |
115 thm alpha.induct |
115 thm alpha.induct |
116 |
116 |
117 lemma a3_inverse: |
117 lemma a3_inverse: |
118 assumes "rLam a t \<approx> rLam b s" |
118 assumes "rLam a t \<approx> rLam b s" |
119 shows "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s))" |
119 shows "\<exists>pi. (({atom a}, t) \<approx>gen alpha rfv pi ({atom b}, s))" |
128 apply(induct rule: alpha.induct) |
128 apply(induct rule: alpha.induct) |
129 apply(simp add: a1) |
129 apply(simp add: a1) |
130 apply(simp add: a2) |
130 apply(simp add: a2) |
131 apply(simp) |
131 apply(simp) |
132 apply(rule a3) |
132 apply(rule a3) |
133 apply(rule alpha_gen_eqvt_atom) |
133 apply(rule alpha_gen_atom_eqvt) |
134 apply(rule rfv_eqvt) |
134 apply(rule rfv_eqvt) |
135 apply assumption |
135 apply assumption |
136 done |
136 done |
137 |
137 |
138 lemma alpha_refl: |
138 lemma alpha_refl: |
158 done |
158 done |
159 |
159 |
160 lemma alpha_trans: |
160 lemma alpha_trans: |
161 shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3" |
161 shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3" |
162 apply(induct arbitrary: t3 rule: alpha.induct) |
162 apply(induct arbitrary: t3 rule: alpha.induct) |
163 apply(erule alpha.cases) |
|
164 apply(simp_all) |
|
165 apply(simp add: a1) |
163 apply(simp add: a1) |
166 apply(rotate_tac 4) |
164 apply(rotate_tac 4) |
167 apply(erule alpha.cases) |
165 apply(erule alpha.cases) |
168 apply(simp_all) |
166 apply(simp_all add: a2) |
169 apply(simp add: a2) |
|
170 apply(erule alpha.cases) |
167 apply(erule alpha.cases) |
171 apply(simp_all) |
168 apply(simp_all) |
172 apply(rule a3) |
169 apply(rule a3) |
173 apply(rule alpha_gen_atom_trans) |
170 apply(rule alpha_gen_atom_trans) |
174 apply(rule alpha_eqvt) |
171 apply(rule alpha_eqvt) |