Lines Matching refs:collapse
4 val _ = new_theory "collapse";
13 collapse s = FUN_FMAP (\v.walkstar s (Var v)) (FDOM s)`;
17 `wfs s ==> !t.(collapse s ��� t = walkstar s t)`,
27 `wfs s ==> !v.v IN FDOM s ==> (collapse s ' v = walkstar s (Var v))`,
41 `wfs s ==> idempotent (collapse s)`,
46 `idempotent s ��� noids s ==> (collapse s = s)`,
49 `FDOM s = FDOM (collapse s)` by SRW_TAC [][collapse_def,FUN_FMAP_DEF] THEN
56 Cases_on `v IN FDOM (collapse s)` THEN SRW_TAC [][] THEN
76 Q_TAC SUFF_TAC `s = collapse s`
78 `FDOM s = FDOM (collapse s)`
93 ``wfs s ==> noids (collapse s)``,
103 ``wfs s ==> wfs (collapse s)``,