|
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 x p 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 lemma elim1: |
|
93 "ufree t \<Longrightarrow> \<parallel>t\<parallel> \<noteq>(Const ''unpermute'')" |
|
94 apply(erule ufree.induct) |
|
95 apply(auto) |
|
96 done |
|
97 |
|
98 lemma elim2: |
|
99 "ufree t \<Longrightarrow> \<not>(\<exists>p. \<parallel>t\<parallel> = App (Const ''unpermute'') (Var p))" |
|
100 apply(erule ufree.induct) |
|
101 apply(auto dest: elim1) |
|
102 done |
|
103 |
|
104 lemma |
|
105 "ufree t \<Longrightarrow> uss t = ss (\<parallel>t\<parallel>)" |
|
106 apply(erule ufree.induct) |
|
107 apply(simp_all) |
|
108 apply(subst ss.simps) |
|
109 apply(auto) |
|
110 apply(drule elim2) |
|
111 apply(auto) |
|
112 done |
|
113 |
|
114 |
|
115 fun |
|
116 fr :: "trm \<Rightarrow> name set" |
|
117 where |
|
118 "fr (Var x) = {x}" |
|
119 | "fr (Const s) = {}" |
|
120 | "fr (Lam [x].t) = fr t - {x}" |
|
121 | "fr (App t1 t2) = fr t1 \<union> fr t2" |
|
122 |
|
123 function |
|
124 sfr :: "trm \<Rightarrow> name set" |
|
125 where |
|
126 "sfr (Var x) = {}" |
|
127 | "sfr (Const s) = {}" |
|
128 | "sfr (Lam [x].t) = sfr t - {x}" |
|
129 | "sfr (App (App (Const ''unpermute'') (Var p)) (Var x)) = {p, x}" |
|
130 | "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> sfr (App t1 t2) = sfr t1 \<union> sfr t2" |
|
131 defer |
|
132 apply(simp_all) |
|
133 apply(auto)[1] |
|
134 apply(case_tac x) |
|
135 apply(simp_all) |
|
136 apply(auto) |
|
137 apply(blast) |
|
138 done |
|
139 |
|
140 termination |
|
141 apply(relation "measure (\<lambda>t. size t)") |
|
142 apply(simp_all) |
|
143 done |
|
144 |
|
145 function |
|
146 ss :: "trm \<Rightarrow> nat" |
|
147 where |
|
148 "ss (Var x) = 1" |
|
149 | "ss (Const s) = 1" |
|
150 | "ss (Lam [x].t) = 1 + ss t" |
|
151 | "ss (App (App (Const ''unpermute'') (Var p)) (Var x)) = 1" |
|
152 | "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> ss (App t1 t2) = 1 + ss t1 + ss t2" |
|
153 defer |
|
154 apply(simp_all) |
|
155 apply(auto)[1] |
|
156 apply(case_tac x) |
|
157 apply(simp_all) |
|
158 apply(auto) |
|
159 apply(blast) |
|
160 done |
|
161 |
|
162 termination |
|
163 apply(relation "measure (\<lambda>t. size t)") |
|
164 apply(simp_all) |
|
165 done |
|
166 |
|
167 inductive |
|
168 improper :: "trm \<Rightarrow> bool" |
|
169 where |
|
170 "improper (App (App (Const ''unpermute'') (Var p)) (Var x))" |
|
171 | "improper p x t \<Longrightarrow> improper p x (Lam [y].t)" |
|
172 | "\<lbrakk>improper p x t1; improper p x t2\<rbrakk> \<Longrightarrow> improper p x (App t1 t2)" |
|
173 |
|
174 lemma trm_ss: |
|
175 shows "\<not>improper p x t \<Longrightarrow> ss (t[x::= p]) = ss t" |
|
176 apply(induct rule: ss.induct) |
|
177 apply(simp) |
|
178 apply(simp) |
|
179 apply(simp) |
|
180 apply(auto)[1] |
|
181 apply(case_tac "improper p x t") |
|
182 apply(drule improper.intros(2)) |
|
183 apply(blast) |
|
184 apply(simp) |
|
185 using improper.intros(1) |
|
186 apply(blast) |
|
187 apply(erule contrapos_pn) |
|
188 thm contrapos_np |
|
189 apply(simp) |
|
190 apply(auto)[1] |
|
191 apply(simp) |
|
192 apply(erule disjE) |
|
193 apply(erule conjE)+ |
|
194 apply(subst ss.simps) |
|
195 apply(simp) |
|
196 apply(rule disjI1) |
|
197 apply(rule allI) |
|
198 apply(rule notI) |
|
199 |
|
200 apply(simp del: ss.simps) |
|
201 apply(erule disjE) |
|
202 apply(subst ss.simps) |
|
203 apply(simp) |
|
204 apply(simp only: subst.simps) |
|
205 apply(subst ss.simps) |
|
206 apply(simp del: ss.simps) |
|
207 apply(rule conjI) |
|
208 apply(rule impI) |
|
209 apply(erule conjE) |
|
210 apply(erule exE)+ |
|
211 apply(subst ss.simps) |
|
212 apply(simp) |
|
213 apply(auto)[1] |
|
214 apply(simp add: if_splits) |
|
215 apply() |
|
216 |
|
217 function |
|
218 simp :: "name \<Rightarrow> trm \<Rightarrow> trm" |
|
219 where |
|
220 "simp p (Const c) = (Const c)" |
|
221 | "simp p (Var x) = App (App (Const ''permute'') (Var p)) (Var x)" |
|
222 | "simp p (App t1 t2) = (if ((\<exists>x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x))) |
|
223 then t2 |
|
224 else App (simp p t1) (simp p t2))" |
|
225 | "simp p (Lam [x].t) = Lam [x]. (simp p (t[x ::= p]))" |
|
226 apply(pat_completeness) |
|
227 apply(simp_all) |
|
228 apply(auto) |
|
229 done |
|
230 |
|
231 termination |
|
232 apply(relation "measure (\<lambda>(_, t). size t)") |
|
233 apply(simp_all) |
|
234 |
|
235 end |