1 theory PaperTest |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 datatype trm = |
|
8 Const "string" |
|
9 | Var "name" |
|
10 | App "trm" "trm" |
|
11 | Lam "name" "trm" ("Lam [_]. _" [100, 100] 100) |
|
12 |
|
13 fun |
|
14 subst :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100) |
|
15 where |
|
16 "(Var x)[y::=p] = (if x=y then (App (App (Const ''unpermute'') (Var p)) (Var x)) else (Var x))" |
|
17 | "(App t\<^isub>1 t\<^isub>2)[y::=p] = App (t\<^isub>1[y::=p]) (t\<^isub>2[y::=p])" |
|
18 | "(Lam [x].t)[y::=p] = (if x=y then (Lam [x].t) else Lam [x].(t[y::=p]))" |
|
19 | "(Const n)[y::=p] = Const n" |
|
20 |
|
21 datatype utrm = |
|
22 UConst "string" |
|
23 | UnPermute "name" "name" |
|
24 | UVar "name" |
|
25 | UApp "utrm" "utrm" |
|
26 | ULam "name" "utrm" ("ULam [_]. _" [100, 100] 100) |
|
27 |
|
28 fun |
|
29 usubst :: "utrm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> utrm" ("_[_:::=_]" [100,100,100] 100) |
|
30 where |
|
31 "(UVar x)[y:::=p] = (if x=y then UnPermute p x else (UVar x))" |
|
32 | "(UApp t\<^isub>1 t\<^isub>2)[y:::=p] = UApp (t\<^isub>1[y:::=p]) (t\<^isub>2[y:::=p])" |
|
33 | "(ULam [x].t)[y:::=p] = (if x=y then (ULam [x].t) else ULam [x].(t[y:::=p]))" |
|
34 | "(UConst n)[y:::=p] = UConst n" |
|
35 | "(UnPermute x q)[y:::=p] = UnPermute x q" |
|
36 |
|
37 function |
|
38 ss :: "trm \<Rightarrow> nat" |
|
39 where |
|
40 "ss (Var x) = 1" |
|
41 | "ss (Const s) = 1" |
|
42 | "ss (Lam [x].t) = 1 + ss t" |
|
43 | "ss (App (App (Const ''unpermute'') (Var p)) (Var x)) = 1" |
|
44 | "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> ss (App t1 t2) = 1 + ss t1 + ss t2" |
|
45 defer |
|
46 apply(simp_all) |
|
47 apply(auto)[1] |
|
48 apply(case_tac x) |
|
49 apply(simp_all) |
|
50 apply(auto) |
|
51 apply(blast) |
|
52 done |
|
53 |
|
54 termination |
|
55 apply(relation "measure (\<lambda>t. size t)") |
|
56 apply(simp_all) |
|
57 done |
|
58 |
|
59 fun |
|
60 uss :: "utrm \<Rightarrow> nat" |
|
61 where |
|
62 "uss (UVar x) = 1" |
|
63 | "uss (UConst s) = 1" |
|
64 | "uss (ULam [x].t) = 1 + uss t" |
|
65 | "uss (UnPermute x y) = 1" |
|
66 | "uss (UApp t1 t2) = 1 + uss t1 + uss t2" |
|
67 |
|
68 lemma trm_uss: |
|
69 shows "uss (t[x:::=p]) = uss t" |
|
70 apply(induct rule: uss.induct) |
|
71 apply(simp_all) |
|
72 done |
|
73 |
|
74 inductive |
|
75 ufree :: "utrm \<Rightarrow> bool" |
|
76 where |
|
77 "ufree (UVar x)" |
|
78 | "s \<noteq> ''unpermute'' \<Longrightarrow> ufree (UConst s)" |
|
79 | "ufree t \<Longrightarrow> ufree (ULam [x].t)" |
|
80 | "ufree (UnPermute x y)" |
|
81 | "\<lbrakk>ufree t1; ufree t2\<rbrakk> \<Longrightarrow> ufree (UApp t1 t2)" |
|
82 |
|
83 fun |
|
84 trans :: "utrm \<Rightarrow> trm" ("\<parallel>_\<parallel>" [100] 100) |
|
85 where |
|
86 "\<parallel>(UVar x)\<parallel> = Var x" |
|
87 | "\<parallel>(UConst x)\<parallel> = Const x" |
|
88 | "\<parallel>(UnPermute p x)\<parallel> = (App (App (Const ''unpermute'') (Var p)) (Var x))" |
|
89 | "\<parallel>(ULam [x].t)\<parallel> = Lam [x].(\<parallel>t\<parallel>)" |
|
90 | "\<parallel>(UApp t1 t2)\<parallel> = App (\<parallel>t1\<parallel>) (\<parallel>t2\<parallel>)" |
|
91 |
|
92 function |
|
93 utrans :: "trm \<Rightarrow> utrm" ("\<lparr>_\<rparr>" [90] 100) |
|
94 where |
|
95 "\<lparr>Var x\<rparr> = UVar x" |
|
96 | "\<lparr>Const x\<rparr> = UConst x" |
|
97 | "\<lparr>Lam [x].t\<rparr> = ULam [x].\<lparr>t\<rparr>" |
|
98 | "\<lparr>App (App (Const ''unpermute'') (Var p)) (Var x)\<rparr> = UnPermute p x" |
|
99 | "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> \<lparr>App t1 t2\<rparr> = UApp (\<lparr>t1\<rparr>) (\<lparr>t2\<rparr>)" |
|
100 defer |
|
101 apply(simp_all) |
|
102 apply(auto)[1] |
|
103 apply(case_tac x) |
|
104 apply(simp_all) |
|
105 apply(auto) |
|
106 apply(blast) |
|
107 done |
|
108 |
|
109 termination |
|
110 apply(relation "measure (\<lambda>t. size t)") |
|
111 apply(simp_all) |
|
112 done |
|
113 |
|
114 |
|
115 lemma elim1: |
|
116 "ufree t \<Longrightarrow> \<parallel>t\<parallel> \<noteq>(Const ''unpermute'')" |
|
117 apply(erule ufree.induct) |
|
118 apply(auto) |
|
119 done |
|
120 |
|
121 lemma elim2: |
|
122 "ufree t \<Longrightarrow> \<not>(\<exists>p. \<parallel>t\<parallel> = App (Const ''unpermute'') (Var p))" |
|
123 apply(erule ufree.induct) |
|
124 apply(auto dest: elim1) |
|
125 done |
|
126 |
|
127 lemma ss1: |
|
128 "ufree t \<Longrightarrow> uss t = ss (\<parallel>t\<parallel>)" |
|
129 apply(erule ufree.induct) |
|
130 apply(simp_all) |
|
131 apply(subst ss.simps) |
|
132 apply(auto) |
|
133 apply(drule elim2) |
|
134 apply(auto) |
|
135 done |
|
136 |
|
137 lemma trans1: |
|
138 shows "\<parallel>\<lparr>t\<rparr>\<parallel> = t" |
|
139 apply(induct t) |
|
140 apply(simp) |
|
141 apply(simp) |
|
142 prefer 2 |
|
143 apply(simp) |
|
144 apply(case_tac "(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x))") |
|
145 apply(erule exE)+ |
|
146 apply(simp) |
|
147 apply(simp) |
|
148 done |
|
149 |
|
150 lemma trans_subst: |
|
151 shows "\<lparr>t[x ::= p]\<rparr> = \<lparr>t\<rparr>[x :::= p]" |
|
152 apply(induct rule: subst.induct) |
|
153 apply(simp) |
|
154 defer |
|
155 apply(simp) |
|
156 apply(simp) |
|
157 apply(simp) |
|
158 apply(case_tac "(t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x))") |
|
159 apply(erule exE)+ |
|
160 apply(simp only:) |
|
161 apply(subst utrans.simps) |
|
162 apply(subst usubst.simps) |
|
163 apply(case_tac "xa = x") |
|
164 apply(subst (asm) subst.simps) |
|
165 apply(simp only:) |
|
166 apply(subst (asm) utrans.simps) |
|
167 apply(simp only: usubst.simps) |
|
168 apply(simp) |
|
169 apply(auto)[1] |
|
170 apply(case_tac "pa = x") |
|
171 apply(simp) |
|
172 prefer 2 |
|
173 apply(simp) |
|
174 apply(simp) |
|
175 done |
|
176 |
|
177 lemma |
|
178 "ss (t[x ::= p]) = ss t" |
|
179 apply(subst (2) trans1[symmetric]) |
|
180 apply(subst ss1[symmetric]) |
|
181 |
|
182 |
|
183 fun |
|
184 fr :: "trm \<Rightarrow> name set" |
|
185 where |
|
186 "fr (Var x) = {x}" |
|
187 | "fr (Const s) = {}" |
|
188 | "fr (Lam [x].t) = fr t - {x}" |
|
189 | "fr (App t1 t2) = fr t1 \<union> fr t2" |
|
190 |
|
191 function |
|
192 sfr :: "trm \<Rightarrow> name set" |
|
193 where |
|
194 "sfr (Var x) = {}" |
|
195 | "sfr (Const s) = {}" |
|
196 | "sfr (Lam [x].t) = sfr t - {x}" |
|
197 | "sfr (App (App (Const ''unpermute'') (Var p)) (Var x)) = {p, x}" |
|
198 | "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> sfr (App t1 t2) = sfr t1 \<union> sfr t2" |
|
199 defer |
|
200 apply(simp_all) |
|
201 apply(auto)[1] |
|
202 apply(case_tac x) |
|
203 apply(simp_all) |
|
204 apply(auto) |
|
205 apply(blast) |
|
206 done |
|
207 |
|
208 termination |
|
209 apply(relation "measure (\<lambda>t. size t)") |
|
210 apply(simp_all) |
|
211 done |
|
212 |
|
213 function |
|
214 ss :: "trm \<Rightarrow> nat" |
|
215 where |
|
216 "ss (Var x) = 1" |
|
217 | "ss (Const s) = 1" |
|
218 | "ss (Lam [x].t) = 1 + ss t" |
|
219 | "ss (App (App (Const ''unpermute'') (Var p)) (Var x)) = 1" |
|
220 | "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> ss (App t1 t2) = 1 + ss t1 + ss t2" |
|
221 defer |
|
222 apply(simp_all) |
|
223 apply(auto)[1] |
|
224 apply(case_tac x) |
|
225 apply(simp_all) |
|
226 apply(auto) |
|
227 apply(blast) |
|
228 done |
|
229 |
|
230 termination |
|
231 apply(relation "measure (\<lambda>t. size t)") |
|
232 apply(simp_all) |
|
233 done |
|
234 |
|
235 inductive |
|
236 improper :: "trm \<Rightarrow> bool" |
|
237 where |
|
238 "improper (App (App (Const ''unpermute'') (Var p)) (Var x))" |
|
239 | "improper p x t \<Longrightarrow> improper p x (Lam [y].t)" |
|
240 | "\<lbrakk>improper p x t1; improper p x t2\<rbrakk> \<Longrightarrow> improper p x (App t1 t2)" |
|
241 |
|
242 lemma trm_ss: |
|
243 shows "\<not>improper p x t \<Longrightarrow> ss (t[x::= p]) = ss t" |
|
244 apply(induct rule: ss.induct) |
|
245 apply(simp) |
|
246 apply(simp) |
|
247 apply(simp) |
|
248 apply(auto)[1] |
|
249 apply(case_tac "improper p x t") |
|
250 apply(drule improper.intros(2)) |
|
251 apply(blast) |
|
252 apply(simp) |
|
253 using improper.intros(1) |
|
254 apply(blast) |
|
255 apply(erule contrapos_pn) |
|
256 thm contrapos_np |
|
257 apply(simp) |
|
258 apply(auto)[1] |
|
259 apply(simp) |
|
260 apply(erule disjE) |
|
261 apply(erule conjE)+ |
|
262 apply(subst ss.simps) |
|
263 apply(simp) |
|
264 apply(rule disjI1) |
|
265 apply(rule allI) |
|
266 apply(rule notI) |
|
267 |
|
268 apply(simp del: ss.simps) |
|
269 apply(erule disjE) |
|
270 apply(subst ss.simps) |
|
271 apply(simp) |
|
272 apply(simp only: subst.simps) |
|
273 apply(subst ss.simps) |
|
274 apply(simp del: ss.simps) |
|
275 apply(rule conjI) |
|
276 apply(rule impI) |
|
277 apply(erule conjE) |
|
278 apply(erule exE)+ |
|
279 apply(subst ss.simps) |
|
280 apply(simp) |
|
281 apply(auto)[1] |
|
282 apply(simp add: if_splits) |
|
283 apply() |
|
284 |
|
285 function |
|
286 simp :: "name \<Rightarrow> trm \<Rightarrow> trm" |
|
287 where |
|
288 "simp p (Const c) = (Const c)" |
|
289 | "simp p (Var x) = App (App (Const ''permute'') (Var p)) (Var x)" |
|
290 | "simp p (App t1 t2) = (if ((\<exists>x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x))) |
|
291 then t2 |
|
292 else App (simp p t1) (simp p t2))" |
|
293 | "simp p (Lam [x].t) = Lam [x]. (simp p (t[x ::= p]))" |
|
294 apply(pat_completeness) |
|
295 apply(simp_all) |
|
296 apply(auto) |
|
297 done |
|
298 |
|
299 termination |
|
300 apply(relation "measure (\<lambda>(_, t). size t)") |
|
301 apply(simp_all) |
|
302 |
|
303 end |
|