equal
deleted
inserted
replaced
55 | "perm_bp pi (BVr a) = BVr (pi \<bullet> a)" |
55 | "perm_bp pi (BVr a) = BVr (pi \<bullet> a)" |
56 | "perm_bp pi (BPr bp1 bp2) = BPr (perm_bp pi bp1) (perm_bp pi bp2)" |
56 | "perm_bp pi (BPr bp1 bp2) = BPr (perm_bp pi bp1) (perm_bp pi bp2)" |
57 |
57 |
58 end |
58 end |
59 |
59 |
|
60 inductive |
|
61 alpha1 :: "trm1 \<Rightarrow> trm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100) |
|
62 where |
|
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" |
|
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) |
|
66 \<Longrightarrow> Lm1 a t \<approx>1 Lm1 b s" |
|
67 | a4: "\<exists>pi::name prm.( |
|
68 t1 \<approx>1 t2 \<and> |
|
69 (fv_trm1 s1 - fv_bp b1 = fv_trm1 s2 - fv_bp b2) \<and> |
|
70 (fv_trm1 s1 - fv_bp b1) \<sharp>* pi \<and> |
|
71 (pi \<bullet> s1 = s2) (* Optional: \<and> (pi \<bullet> b1 = b2) *) |
|
72 ) \<Longrightarrow> Lt1 b1 t1 s1 \<approx>1 Lt1 b2 t2 s2" |
|
73 |
|
74 lemma alpha1_equivp: "equivp alpha1" sorry |
|
75 |
|
76 quotient_type qtrm1 = trm1 / alpha1 |
|
77 by (rule alpha1_equivp) |
|
78 |
60 |
79 |
61 section {*** lets with single assignments ***} |
80 section {*** lets with single assignments ***} |
62 |
81 |
63 datatype trm2 = |
82 datatype trm2 = |
64 Vr2 "name" |
83 Vr2 "name" |
99 | "perm_trm2 pi (Lt2 as t) = Lt2 (perm_assign pi as) (perm_trm2 pi t)" |
118 | "perm_trm2 pi (Lt2 as t) = Lt2 (perm_assign pi as) (perm_trm2 pi t)" |
100 | "perm_assign pi (As a t) = As (pi \<bullet> a) (perm_trm2 pi t)" |
119 | "perm_assign pi (As a t) = As (pi \<bullet> a) (perm_trm2 pi t)" |
101 |
120 |
102 end |
121 end |
103 |
122 |
|
123 inductive |
|
124 alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
|
125 where |
|
126 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" |
|
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) |
|
129 \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s" |
|
130 | a4: "\<exists>pi::name prm. ( |
|
131 fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and> |
|
132 (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and> |
|
133 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
|
134 ) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2" |
|
135 |
|
136 lemma alpha2_equivp: "equivp alpha2" sorry |
|
137 |
|
138 quotient_type qtrm2 = trm2 / alpha2 |
|
139 by (rule alpha2_equivp) |
104 |
140 |
105 section {*** lets with many assignments ***} |
141 section {*** lets with many assignments ***} |
106 |
142 |
107 datatype trm3 = |
143 datatype trm3 = |
108 Vr3 "name" |
144 Vr3 "name" |
146 | "perm_assigns pi (ANil) = ANil" |
182 | "perm_assigns pi (ANil) = ANil" |
147 | "perm_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (perm_trm3 pi t) (perm_assigns pi as)" |
183 | "perm_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (perm_trm3 pi t) (perm_assigns pi as)" |
148 |
184 |
149 end |
185 end |
150 |
186 |
151 |
187 inductive |
152 end |
188 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100) |
|
189 where |
|
190 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)" |
|
191 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2" |
|
192 | a3: "\<exists>pi::name prm. (fv_trm3 t - {a} = fv_trm3 s - {b} \<and> (fv_trm3 t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>3 s \<and> (pi \<bullet> a) = b) |
|
193 \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s" |
|
194 | a4: "\<exists>pi::name prm. ( |
|
195 fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and> |
|
196 (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and> |
|
197 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
|
198 ) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2" |
|
199 |
|
200 lemma alpha3_equivp: "equivp alpha3" sorry |
|
201 |
|
202 quotient_type qtrm3 = trm3 / alpha3 |
|
203 by (rule alpha3_equivp) |
|
204 |
|
205 end |