Lines Matching defs:l2
42 val t = ``PERM (x1::l1 ++ (l2 ++ (x2::x3::l3) ++ x4::l4)) (x1::l1 ++ ((x2::x3::l3) ++ x4::l4 ++ l2))``
43 val t1 = ``x1::x2::x3::(l1 ++ (x2::x3::l3 ++ x4::l4 ++ l2 ++ l4))``
44 val t2 = ``x1::x2::x8::(x4::l4 ++ l2++l4)``
127 val l2 = (rand o rand o rhs o concl o valOf) l_thm_opt
129 SOME (MP (ISPECL [x,l,e,l2] PERM_FUN_CONS_11_SWAP_AT_FRONT)
136 val (l1,l2) = listSyntax.dest_append (rand t)
139 PERM_MOVE_CONS_TO_FRONT e (mk_icomb (PERM_tm, l2))
145 SOME (MP (ISPECL [l2,l1,e,l1'] PERM_FUN_CONS_APPEND_1)
150 val l2' = (rand o rand o rhs o concl o valOf) l2_thm_opt
152 SOME (MP (ISPECL [l1,l2,e,l2'] PERM_FUN_CONS_APPEND_2)
174 val l2 = (rand o rhs o concl) thm1;
176 val thm2 = ISPECL [x, l1, l2] PERM_FUN_CONS_IFF
211 val l2 = (rand o rand o rhs o concl o valOf) l'_thm_opt
213 SOME (MP (ISPECL [x,l',l,l2] PERM_FUN_CONS_11_APPEND)
220 val (l1,l2) = listSyntax.dest_append (rand t);
223 if (aconv l2 l) then
229 PERM_MOVE_APPEND_TO_FRONT l (mk_icomb (PERM_tm, l2))
235 SOME (MP (ISPECL [l1,l,l1',l2] PERM_FUN_APPEND_APPEND_1)
240 val l2' = (rand o rand o rhs o concl o valOf) l2_thm_opt
242 SOME (MP (ISPECL [l2,l,l2',l1] PERM_FUN_APPEND_APPEND_2)
277 val l2 = (rand o rhs o concl) thm1;
279 val thm2 = ISPECL [l, l1, l2] PERM_FUN_APPEND_IFF
289 val l = ``x::(l3 ++ z3::l2 ++ x::z::x1::y::l1 ++ x3::x5::l0)``;
291 val ls = [``l2:'a list``, ``l0:'a list``, ``l3:'a list``];
314 fun PERM_ELIM_DUPLICATES_CONV_DIRECT (l1,l2) common_terms =
317 val thm_l2 = PERM_SPLIT_el_lists l2 common_terms;
325 val thm0 = ISPECL [lc,l1,l3',l2,l4'] PERM_CONG_APPEND_IFF;
368 (* Proves PERM l1comm l2comm ==> PERM l1 l2 = PERM l1rem l2rem
370 order they appear in l1/l2, and l1rem and l2rem are the
372 fun PERM_ELIM_COMMON_IMP common l1 l2 = let
376 val (l2_comm, l2_rem) = strip_perm_list_div comm_tab l2
377 val thm = ISPECL [l1, l1_comm, l1_rem, l2, l2_comm, l2_rem]
384 val (l1,l2) = dest_PERM t handle HOL_ERR _ => raise UNCHANGED
385 val common_terms = perm_list_inter l1 l2
392 then PERM_ELIM_COMMON_IMP (half ((op @) common_terms)) l1 l2
395 else PERM_ELIM_DUPLICATES_CONV_DIRECT (l1,l2) common_terms
400 val t = ``PERM (x1::l1 ++ (l2 ++ (x2::x3::(1 : num)::l3) ++ x4::l4))
401 (x1::(1 : num)::l1 ++ ((x2::x3::l3) ++ x4::l4 ++ l2))``
403 val comm = [``l2 : num list``, ``x3 : num``]
428 val ls = ``(l1 ++l2):'a list``
429 val l = ``l2 ++ x::l1``
454 val t = ``(l2++x::l3)``
455 val t = ``((TAKE n l)++l2++x::l3++(DROP n l))``
456 val t = ``((TAKE n l)++(DROP m l2)++l2++x::l3++(TAKE m l2)++(DROP n l))``
478 val l1 = ``(TAKE n l)++l2++x::l3++(DROP n l)``
479 val l2 = ``(DROP m l)++x::l3++(TAKE m l)++(DROP n l)``
480 val t = ``PERM ^l1 ^l2``
484 val (l1,l2) = dest_PERM t handle HOL_ERR _ => raise UNCHANGED;
487 val thm_l2_opt = (total PERM_TAKE_DROP) l2;
491 val thm_l2 = if isSome thm_l2_opt then valOf thm_l2_opt else ISPEC l2 PERM_REFL;
494 val l2' = (rand o concl) thm_l2
495 val thm0 = ISPECL [l1,l1',l2,l2'] PERM_CONG_2;
505 val (l1,l2) = dest_PERM t handle HOL_ERR _ => raise UNCHANGED;
511 val thm_l2 = ELIM_NIL_RULE (PERM_SPLIT_el_lists l2 (strip_perm_list l2));
514 val l2' = (rand o concl) thm_l2
516 val thm0 = ISPECL [l1,l1',l2,l2'] PERM_CONG_2;
526 val (l1,l2) = dest_PERM t handle HOL_ERR _ => raise UNCHANGED;
529 val (xs2,ls2) = strip_perm_list l2;
550 val t = ``PERM (z::y::x'::l2) (l3++(x'::l1))``
564 val (l1,l2) = dest_PERM t handle HOL_ERR _ => raise UNCHANGED;
567 (true, PERM_SPLIT l l2);
569 val (thm0,l1,l2) = if turn then (ISPECL [l1,l2] PERM_SYM,l2,l1) else (REFL t,l1,l2);
572 val thm1a = ISPECL [l1,l1',l2,l2] PERM_CONG_2
574 val thm1c = MP thm1b (ISPEC l2 PERM_REFL);
578 val thm2a = ISPECL [l,r,rand l1',l2] PERM_REWR
687 conv ``X /\ (PERM (x::l1++l2) (l2++[x])) /\ Z``
688 conv ``(PERM (x::z::l1++l2) (l3++x::l1)) /\ Z``
690 conv ``(X /\ (PERM (l2++[]++[z]) (y::l4)) /\ Y) ==> ((PERM (x::z::l1++l2) (l3++x::l1)))``
693 PERM l2 m2 /\
694 PERM (l1 ++ l2) n1 /\