lambda/other-models/swapScript.sml

5 val _ = new_theory "swap"
112 val swap_def = new_specification("swap_def", ["swap"], thm1);
116   ``!t. swap x x t = t``,
123   ``!t. swap x y t = swap y x t``,
131   ``!t. ~(v IN FV t) ==> ([VAR v/u] t = swap v u t)``,
156   ``!t u v. FV (swap u v t) = swapset u v (FV t)``,
168   ``!t x y. size (swap x y t) = size t``,
187   ``!t u v x y. swap u v ([VAR x/y] t) =
188                 [VAR (swapstr u v x)/swapstr u v y] (swap u v t)``,
198     `swap u v' (LAM z ([VAR x/y] M)) =
199        LAM z ([VAR (swapstr u v' x)/swapstr u v' y] (swap u v' M))`
205             `[VAR (swapstr u v' x)/swapstr u v' y] (swap u v' M) =
206              swap u v' ([VAR x/y] M)`
216       `~(a IN FV (swap u v' M))` by ASM_SIMP_TAC (srw_ss()) [] THEN
227   ``swap x y (LAM v t) = LAM (swapstr x y v) (swap x y t)``,
238   ``(swap x y (VAR s) = VAR (swapstr x y s)) /\
239     (swap x y (CON k) = CON k) /\
240     (swap x y (t @@ u) = swap x y t @@ swap x y u) /\
241     (swap x y (LAM v t) = LAM (swapstr x y v) (swap x y t))``,
247   ``!t u v x y. swap (swapstr x y u) (swapstr x y v) (swap x y t) =
248                 swap x y (swap u v t)``,
261   ``swap x y (swap (swapstr x y a) (swapstr x y b) t) =
262     swap a b (swap x y t)``,
268   ``!t. swap x y (swap x y t) = t``,
273   ``(swap x y (swap x y t) = t) /\ (swap y x (swap x y t) = t)``,
279   ``~(v IN FV M) ==> (LAM v (swap v u M) = LAM u M)``,
283     (LAM v1 t1 = LAM v2 t2) ��� v1 ��� FV (LAM v2 t2) ��� (t1 = swap v1 v2 t2)
303       swap x y ([N/v] M) = [swap x y N / swapstr x y v] (swap x y M)``,
312   ``[N/v] (swap x y M) = swap x y ([swap x y N/swapstr x y v] M)``,
317   ``((swap x y t1 = swap x y t2) = (t1 = t2)) /\
318     ((swap x y t1 = swap y x t2) = (t1 = t2))``,
324   ``(swap x y t = u) = (t = swap x y u)``,
329   ``((swap x y t = VAR s) = (t = VAR (swapstr x y s))) /\
330     ((VAR s = swap x y t) = (VAR (swapstr x y s) = t))``,
334   ``((swap x y t = M @@ N) = (t = swap x y M @@ swap x y N)) /\
335     ((M @@ N = swap x y t) = (swap x y M @@ swap x y N = t))``,
339   ``((swap x y t = CON k) = (t = CON k)) /\
340     ((CON k = swap x y t) = (CON k = t))``,
344   ``((swap x y t = LAM v M) = (t = LAM (swapstr x y v) (swap x y M))) /\
345     ((LAM v M = swap x y t) = (LAM (swapstr x y v) (swap x y M) = t))``,
351     supporting recursion over lambda calculus terms using swap
378   ``!t x y. ~(x IN FV t) /\ ~(y IN FV t) ==> (swap x y t = t)``,
382     `swap x y t = t` by METIS_TAC [lemma14a] THEN
393   ``swapping swap FV``,
422      (let v = NEW (FV (LAM x u) UNION pFV p UNION X) in f v (swap v x u)))``,
467               (swap x y t) (swap x y u)
473               (swapstr x y v) (swap x y t) (pswap x y p))) ==>
481                  (hom (swap x y t) p = rswap x y (hom t (pswap x y p)))) /\
496              `LAM x t = LAM u (swap u x t)` by SRW_TAC [][swap_ALPHA] THEN
499              `swap u x t = [VAR u/x] t` by SRW_TAC [][fresh_var_swap] THEN
513              (hom (swap x y t) p = rswap x y (hom t (pswap x y p)))`
518             `(hom (swap x y t) = swapfn pswap rswap x y (hom t)) /\
519              (hom (swap x y u) = swapfn pswap rswap x y (hom u))`
531             `hom (swap x y (LAM z M)) p =
540                    `hom (swap a z (swap x y M)) =
541                       swapfn pswap rswap a z (hom (swap x y M))`
545                    `lam (hom (swap a z (swap x y M))) a
546                         (swap a z (swap x y M)) p =
548                           (lam (hom (swap x y M)) z (swap x y M) p)`
551                    `swapfn pswap rswap x y (hom M) = hom (swap x y M)`
556                    `rFV (lam (hom (swap x y M)) z (swap x y M) p)
558                     FV (LAM z (swap x y M)) UNION pFV p UNION X`
590     `hom (swap u v t) = swapfn pswap rswap u v (hom t)`
593     `lam (hom (swap u v t)) u (swap u v t) p = rswap u v (lam (hom t) v t p)`
662     list swap
667   (lswap (h::hs) t = swap (FST h) (SND h) (lswap hs t))