equal
deleted
inserted
replaced
60 inductive |
60 inductive |
61 alpha1 :: "trm1 \<Rightarrow> trm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100) |
61 alpha1 :: "trm1 \<Rightarrow> trm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100) |
62 where |
62 where |
63 a1: "a = b \<Longrightarrow> (Vr1 a) \<approx>1 (Vr1 b)" |
63 a1: "a = b \<Longrightarrow> (Vr1 a) \<approx>1 (Vr1 b)" |
64 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> Ap1 t1 s1 \<approx>1 Ap1 t2 s2" |
64 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> Ap1 t1 s1 \<approx>1 Ap1 t2 s2" |
65 | a3: "\<exists>pi::name prm. (fv_trm1 t - {a} = fv_trm1 s - {b} \<and> (fv_trm1 t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b) |
65 | a3: "\<exists>pi::name prm. (fv_trm1 t - {a} = fv_trm1 s - {b} \<and> |
|
66 (fv_trm1 t - {a})\<sharp>* pi \<and> |
|
67 (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b) |
66 \<Longrightarrow> Lm1 a t \<approx>1 Lm1 b s" |
68 \<Longrightarrow> Lm1 a t \<approx>1 Lm1 b s" |
67 | a4: "\<exists>pi::name prm.( |
69 | a4: "\<exists>pi::name prm.( |
68 t1 \<approx>1 t2 \<and> |
70 t1 \<approx>1 t2 \<and> |
69 (fv_trm1 s1 - fv_bp b1 = fv_trm1 s2 - fv_bp b2) \<and> |
71 (fv_trm1 s1 - fv_bp b1 = fv_trm1 s2 - fv_bp b2) \<and> |
70 (fv_trm1 s1 - fv_bp b1) \<sharp>* pi \<and> |
72 (fv_trm1 s1 - fv_bp b1) \<sharp>* pi \<and> |
123 inductive |
125 inductive |
124 alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
126 alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
125 where |
127 where |
126 a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)" |
128 a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)" |
127 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2" |
129 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2" |
128 | a3: "\<exists>pi::name prm. (fv_trm2 t - {a} = fv_trm2 s - {b} \<and> (fv_trm2 t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>2 s \<and> (pi \<bullet> a) = b) |
130 | a3: "\<exists>pi::name prm. (fv_trm2 t - {a} = fv_trm2 s - {b} \<and> |
|
131 (fv_trm2 t - {a})\<sharp>* pi \<and> |
|
132 (pi \<bullet> t) \<approx>2 s \<and> |
|
133 (pi \<bullet> a) = b) |
129 \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s" |
134 \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s" |
130 | a4: "\<exists>pi::name prm. ( |
135 | a4: "\<exists>pi::name prm. ( |
131 fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and> |
136 fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and> |
132 (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and> |
137 (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and> |
133 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
138 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |