lambda/other-models/MPlambdaScript.sml

11                              | Parameter of string
17   (psub a p (Parameter q) = if p = q then a else Parameter q) /\
25   (params (Parameter p) = {p}) /\
33   (vsub a v (Parameter p) = Parameter p) /\
41   (allvars (Parameter p) = {}) /\
61                 (vsub (Parameter p) v2 (vsub (Var v2) v1 M) =
62                  vsub (Parameter p) v1 M)``,
72   ``!M p. ?v M'. (M = vsub (Parameter p) v M') /\ ~(p IN params M')``,
81       MAP_EVERY Q.EXISTS_TAC [`x`, `Parameter s`] THEN SRW_TAC [][]
85     `?v1 M1. (M = vsub (Parameter p) v1 M1) /\ ~(p IN params M1)`
87     `?v2 M2. (M' = vsub (Parameter p) v2 M2) /\ ~(p IN params M2)`
90     `(M = vsub (Parameter p) z (vsub (Var z) v1 M1)) /\
91      (M' = vsub (Parameter p) z (vsub (Var z) v2 M2))`
108   (!p. vclosed (Parameter p)) /\
109   (!p v t. vclosed (vsub (Parameter p) v t) ==>
128               (psub N p (vsub (Parameter p) v M) = vsub N v M)``,
133   (vars (Parameter p) = {}) /\
146   (raw_MPpm pi (Parameter s) = Parameter (lswapstr pi s)) /\
203   ``!p v M. vars (vsub (Parameter p) v M) = vars M DELETE v``,
222   ``vclosed (Parameter p)``,
235   ``vclosed (Abs v t) = ?p. vclosed (vsub (Parameter p) v t)``,
240   ``(vsub (Parameter p) v M = App t1 t2) =
241       ?M1 M2. (M = App M1 M2) /\ (vsub (Parameter p) v M1 = t1) /\
242               (vsub (Parameter p) v M2 = t2)``,
246   ``(vsub (Parameter p1) v M = Parameter p2) =
248        (M = Parameter p2)``,
252   ``(vsub (Parameter p) v M = Abs s t) =
253        (?M0. ~(s = v) /\ (M = Abs s M0) /\ (vsub (Parameter p) v M0 = t)) \/
259       ~(v1 = v2) ==> (vsub (Parameter p1) v1 (vsub (Parameter p2) v2 M) =
260                       vsub (Parameter p2) v2 (vsub (Parameter p1) v1 M))``,
271       (psub (Parameter p1) p2 (vsub (Parameter p3) v M) =
272        vsub (Parameter p3) v (psub (Parameter p1) p2 M))``,
276   (!p. cvclosed (Parameter p)) /\
278   (!v p M. ~(p IN params M) /\ cvclosed (vsub (Parameter p) v M) ==>
283   ``cvclosed (Parameter p) /\
286                               cvclosed (vsub (Parameter p) v M))``,
294           (!p x. P (Parameter p) x) /\
297                      (!x. P (vsub (Parameter p) v M) x) ==>
324     ~(p1 IN params (vsub (Parameter p2) v M))``,
330             ((p, p', t0) = pp't0) /\ (t = vsub (Parameter p) v t0) ==>
331             cvclosed (vsub (Parameter p') v t0)``,
374   ``vsub (Parameter p1) v (vsub (Parameter p2) v t) =
375     vsub (Parameter p2) v t``,
380   ``!t. vclosed t ==> !p v. vclosed (vsub (Parameter p) v t)``,
386   ``!P. (!p. P (Parameter p)) /\
388                  (!p. ~(p IN X) ==> P (vsub (Parameter p) v t)) ==>
410   (!p. avclosed (Parameter p)) /\
412   (!v t. (!p. avclosed (vsub (Parameter p) v t)) ==>
418         !v p p' t0. (t = vsub (Parameter p) v t0) ==>
419                     avclosed (vsub (Parameter p') v t0)``,
433   ``avclosed (vsub (Parameter p) v t) ==>
434     !q. avclosed (vsub (Parameter q) v t)``,
458 val sub = ``\t (p,v). vsub (Parameter p) v t``
460   ``!l. FOLDL ^sub (Parameter p) l = Parameter p``,
463   ``!l. (?p. FOLDL ^sub (Var s) l = Parameter p) \/
481   ``!l t p s. vsub (Parameter p) s (FOLDL ^sub t l) =
486   ``vars (vsub (Parameter p) v t) = vars t DELETE v``,
501     `!t l. (vars (FOLDL (\t (p,v). vsub (Parameter p) v t) t l) = {}) ==>
502            vclosed (FOLDL (\t (p,v). vsub (Parameter p) v t) t l)`
521                mpbeta (vsub (Parameter p) u M) (vsub (Parameter p) v N) ==>
529   (!p. convert (Parameter p) (VAR p)) /\
532   (!u v t M. ~(u IN params t) /\ convert (vsub (Parameter u) v t) M ==>
538   ``convert (Parameter p) t = (t = VAR p)``,
559             (params (vsub (Parameter p) v t) DELETE p = params t)``,
578           (!p c. P (Parameter p) (VAR p) c) /\
584                        convert (vsub (Parameter u) v t) M /\
585                        (!d. P (vsub (Parameter u) v t) M d) ==>
605     THEN1 (`convert (MPpm ((z,lswapstr pi u)::pi) (vsub (Parameter u) v t))
636               (vsub (Parameter p1) v t0 = t) /\
638               convert (vsub (Parameter p2) v t0) (tpm [(p1,p2)] M)``,
663       `convert (MPpm [(p1,p2)] (vsub (Parameter u) v t))
666       Q_TAC SUFF_TAC `MPpm [(p1,p2)] (vsub (Parameter u) v t) =
667                       vsub (Parameter u) v t`
690     `FV M' = params (vsub (Parameter u') v t)`
700     Q.EXISTS_TAC `Parameter s` THEN SRW_TAC [][convert_rules],
725     `p' IN params (Parameter p) \/ p' IN params M`
746     convert (vsub (Parameter p) v t1) M /\
754                   (vsub (Parameter p) v t1 = t) /\
770     `vsub (Parameter u) v (vsub p_2 v' M0) =
771      vsub p_2 v' (vsub (Parameter u) v M0)`
780     `FV M = params (vsub (Parameter u) v t)`
812       `convert (vsub (Parameter p) u M) (tpm [(p,u')] M'') /\
813        convert (vsub (Parameter p) v N) (tpm [(p,u')] M''')`
817         by (`FV M''' = params (vsub (Parameter u'') v N)`
821             `mpbeta (MPpm [(u'',p)] (vsub (Parameter p) u M))
822                     (MPpm [(u'',p)] (vsub (Parameter p) v N))`
827                   `~(u' IN params (vsub (Parameter u'') u (MPpm [(u'',p)] M)))`
830       `convert (vsub (Parameter p) u M) (tpm [(u',p)] M'') /\
831        convert (vsub (Parameter p) v N) (tpm [(u'',p)] M''')`
878                                  convert (vsub (Parameter v) u t0) M``,
886   `~(v IN params (vsub (Parameter u) v' t'))`
926     `?y. mpbeta (vsub (Parameter v) u' t0) y /\
927          alpha y (vsub (Parameter v) u'' t0')`
929     `?v1 t1. (y = vsub (Parameter v) v1 t1) /\ ~(v IN params t1)`