2783
+ − 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
2802
+ − 31 "(UVar x)[y:::=p] = (if x=y then UnPermute p x else (UVar x))"
2783
+ − 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
2802
+ − 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
2783
+ − 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
2802
+ − 127 lemma ss1:
2783
+ − 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
2802
+ − 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
2783
+ − 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