src/sort/permLib.sml

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 /\