26 | ULam "name" "utrm" ("ULam [_]. _" [100, 100] 100) |
26 | ULam "name" "utrm" ("ULam [_]. _" [100, 100] 100) |
27 |
27 |
28 fun |
28 fun |
29 usubst :: "utrm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> utrm" ("_[_:::=_]" [100,100,100] 100) |
29 usubst :: "utrm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> utrm" ("_[_:::=_]" [100,100,100] 100) |
30 where |
30 where |
31 "(UVar x)[y:::=p] = (if x=y then UnPermute x p else (UVar x))" |
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])" |
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]))" |
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" |
34 | "(UConst n)[y:::=p] = UConst n" |
35 | "(UnPermute x q)[y:::=p] = UnPermute x q" |
35 | "(UnPermute x q)[y:::=p] = UnPermute x q" |
36 |
36 |
87 | "\<parallel>(UConst x)\<parallel> = Const x" |
87 | "\<parallel>(UConst x)\<parallel> = Const x" |
88 | "\<parallel>(UnPermute p x)\<parallel> = (App (App (Const ''unpermute'') (Var p)) (Var 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>)" |
89 | "\<parallel>(ULam [x].t)\<parallel> = Lam [x].(\<parallel>t\<parallel>)" |
90 | "\<parallel>(UApp t1 t2)\<parallel> = App (\<parallel>t1\<parallel>) (\<parallel>t2\<parallel>)" |
90 | "\<parallel>(UApp t1 t2)\<parallel> = App (\<parallel>t1\<parallel>) (\<parallel>t2\<parallel>)" |
91 |
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 |
92 lemma elim1: |
115 lemma elim1: |
93 "ufree t \<Longrightarrow> \<parallel>t\<parallel> \<noteq>(Const ''unpermute'')" |
116 "ufree t \<Longrightarrow> \<parallel>t\<parallel> \<noteq>(Const ''unpermute'')" |
94 apply(erule ufree.induct) |
117 apply(erule ufree.induct) |
95 apply(auto) |
118 apply(auto) |
96 done |
119 done |
99 "ufree t \<Longrightarrow> \<not>(\<exists>p. \<parallel>t\<parallel> = App (Const ''unpermute'') (Var p))" |
122 "ufree t \<Longrightarrow> \<not>(\<exists>p. \<parallel>t\<parallel> = App (Const ''unpermute'') (Var p))" |
100 apply(erule ufree.induct) |
123 apply(erule ufree.induct) |
101 apply(auto dest: elim1) |
124 apply(auto dest: elim1) |
102 done |
125 done |
103 |
126 |
104 lemma |
127 lemma ss1: |
105 "ufree t \<Longrightarrow> uss t = ss (\<parallel>t\<parallel>)" |
128 "ufree t \<Longrightarrow> uss t = ss (\<parallel>t\<parallel>)" |
106 apply(erule ufree.induct) |
129 apply(erule ufree.induct) |
107 apply(simp_all) |
130 apply(simp_all) |
108 apply(subst ss.simps) |
131 apply(subst ss.simps) |
109 apply(auto) |
132 apply(auto) |
110 apply(drule elim2) |
133 apply(drule elim2) |
111 apply(auto) |
134 apply(auto) |
112 done |
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]) |
113 |
181 |
114 |
182 |
115 fun |
183 fun |
116 fr :: "trm \<Rightarrow> name set" |
184 fr :: "trm \<Rightarrow> name set" |
117 where |
185 where |