Lines Matching refs:tag
856 (FEVERY (\(tag,exp).
858 (THE (exp stack) = (heap ' loc) tag)) L)))`;
1310 Q.EXISTS_TAC `measure (\ (tag,startExp,(dtagL,t),endExpP). tree_size0 t)` THEN
7171 ((h1 = h2) /\ (!tag dl1 dl2. MEM (tag, dl1) data1 /\ MEM (tag, dl2) data2 ==> (dl1 = dl2)))``,
7213 !tag dl1 dl2. MEM (tag,dl1) data1 /\ MEM (tag,dl2) data2 ==> (HD dl1 = HD dl2)` by (
7234 `(LIST_TO_FMAP L1 ' tag st = LIST_TO_FMAP L2 ' tag st)` by
7236 `(LIST_TO_FMAP L1 ' tag = var_res_exp_const (HD dl1)) /\
7237 (LIST_TO_FMAP L2 ' tag = var_res_exp_const (HD dl2))` suffices_by (STRIP_TAC THEN
7245 `MEM (tag, var_res_exp_const (HD dl1)) L1 /\
7246 MEM (tag, var_res_exp_const (HD dl2)) L2` by (
7256 !tag dl1 dl2. MEM (tag,dl1) data1' /\ MEM (tag,dl2) data2' ==> (dl1 = dl2)` by (
7275 Q.PAT_X_ASSUM `!tag dl1 dl2. X` MATCH_MP_TAC THEN
7276 Q.EXISTS_TAC `tag` THEN
7297 ((h1 = h2) /\ (!tag dl1 dl2. MEM (tag, dl1) data1 /\ MEM (tag, dl2) data2 ==> (dl1 = dl2)))``,
7397 `!tag dl1 dl2.
7398 MEM (tag,dl1) data1 /\ MEM (tag,dl2) data2 ==> (dl1 = dl2)` by (
7405 `?tag dl1. x = (tag, dl1)` by (Cases_on `x` THEN SIMP_TAC std_ss []) THEN
7406 `?dl2. MEM (tag, dl2) data1` by (