Theory: probCanon

Parents

• probExtra

Types

Constants

• alg_twin  :bool list -> bool list -> bool
• alg_canon_merge  :bool list -> bool list list -> bool list list
• alg_prefixfree  :bool list list -> bool
• alg_longest  :bool list list -> num
• alg_twinfree  :bool list list -> bool
• alg_canon_find  :bool list -> bool list list -> bool list list
• alg_canon1  :bool list list -> bool list list
• alg_canon2  :bool list list -> bool list list
• alg_order_tupled  :bool list # bool list -> bool
• alg_sorted  :bool list list -> bool
• alg_canon_prefs  :bool list -> bool list list -> bool list list
• alg_order  :bool list -> bool list -> bool
• algebra_canon  :bool list list -> bool
• alg_canon  :bool list list -> bool list list

Definitions

alg_canon1_def

|- alg_canon1 = FOLDR alg_canon_find []

alg_canon2_def

|- alg_canon2 = FOLDR alg_canon_merge []

alg_canon_def

|- !l. alg_canon l = alg_canon2 (alg_canon1 l)

alg_canon_find_def

|- (!l. alg_canon_find l [] = [l]) /\
   !l h t.
     alg_canon_find l (h::t) =
     (if alg_order h l then
        (if IS_PREFIX l h then h::t else h::alg_canon_find l t)
      else
        alg_canon_prefs l (h::t))

alg_canon_merge_def

|- (!l. alg_canon_merge l [] = [l]) /\
   !l h t.
     alg_canon_merge l (h::t) =
     (if alg_twin l h then alg_canon_merge (BUTLAST h) t else l::h::t)

alg_canon_prefs_def

|- (!l. alg_canon_prefs l [] = [l]) /\
   !l h t.
     alg_canon_prefs l (h::t) =
     (if IS_PREFIX h l then alg_canon_prefs l t else l::h::t)

alg_longest_def

|- alg_longest = FOLDR (\h t. (if t <= LENGTH h then LENGTH h else t)) 0

alg_order_arg_munge_def

|- !x x1. alg_order x x1 = alg_order_tupled (x,x1)

alg_order_tupled_primitive_def

|- alg_order_tupled =
   WFREC (@R. WF R /\ !h' h t' t. R (t,t') (h::t,h'::t'))
     (\alg_order_tupled' a.
        pair_case
          (\v v1.
             list_case (list_case T (\v8 v9. T) v1)
               (\v4 v5.
                  list_case F
                    (\v10 v11.
                       (v4 = T) /\ (v10 = F) \/
                       (v4 = v10) /\ alg_order_tupled' (v5,v11)) v1) v) a)

alg_prefixfree_primitive_def

|- alg_prefixfree =
   WFREC (@R. WF R /\ !x z y. R (y::z) (x::y::z))
     (\alg_prefixfree' a.
        list_case T
          (\v2 v3.
             list_case T
               (\v6 v7. ~IS_PREFIX v6 v2 /\ alg_prefixfree' (v6::v7)) v3) a)

alg_sorted_primitive_def

|- alg_sorted =
   WFREC (@R. WF R /\ !x z y. R (y::z) (x::y::z))
     (\alg_sorted' a.
        list_case T
          (\v2 v3.
             list_case T (\v6 v7. alg_order v2 v6 /\ alg_sorted' (v6::v7)) v3)
          a)

alg_twin_def

|- !x y. alg_twin x y = ?l. (x = SNOC T l) /\ (y = SNOC F l)

alg_twinfree_primitive_def

|- alg_twinfree =
   WFREC (@R. WF R /\ !x z y. R (y::z) (x::y::z))
     (\alg_twinfree' a.
        list_case T
          (\v2 v3.
             list_case T (\v6 v7. ~alg_twin v2 v6 /\ alg_twinfree' (v6::v7))
               v3) a)

algebra_canon_def

|- !l. algebra_canon l = (alg_canon l = l)

Theorems

ALG_CANON1_CONSTANT

|- !l. alg_sorted l /\ alg_prefixfree l ==> (alg_canon1 l = l)

ALG_CANON1_PREFIXFREE

|- !l. alg_prefixfree (alg_canon1 l)

ALG_CANON1_SORTED

|- !l. alg_sorted (alg_canon1 l)

ALG_CANON2_CONSTANT

|- !l. alg_twinfree l ==> (alg_canon2 l = l)

ALG_CANON2_PREFIXFREE_PRESERVE

|- !l h.
     (!x. MEM x l ==> ~IS_PREFIX h x /\ ~IS_PREFIX x h) ==>
     !x. MEM x (alg_canon2 l) ==> ~IS_PREFIX h x /\ ~IS_PREFIX x h

ALG_CANON2_SHORTENS

|- !l x. MEM x (alg_canon2 l) ==> ?y. MEM y l /\ IS_PREFIX y x

ALG_CANON2_SORTED_PREFIXFREE_TWINFREE

|- !l.
     alg_sorted l /\ alg_prefixfree l ==>
     alg_sorted (alg_canon2 l) /\ alg_prefixfree (alg_canon2 l) /\
     alg_twinfree (alg_canon2 l)

ALG_CANON_BASIC

|- (alg_canon [] = []) /\ (alg_canon [[]] = [[]]) /\ !x. alg_canon [x] = [x]

ALG_CANON_CONSTANT

|- !l.
     alg_sorted l /\ alg_prefixfree l /\ alg_twinfree l ==> (alg_canon l = l)

ALG_CANON_FIND_CONSTANT

|- !l b.
     alg_sorted (l::b) /\ alg_prefixfree (l::b) ==>
     (alg_canon_find l b = l::b)

ALG_CANON_FIND_DELETES

|- !l b x. MEM x (alg_canon_find l b) ==> MEM x (l::b)

ALG_CANON_FIND_HD

|- !l h t.
     (HD (alg_canon_find l (h::t)) = l) \/ (HD (alg_canon_find l (h::t)) = h)

ALG_CANON_FIND_PREFIXFREE

|- !l b.
     alg_sorted b /\ alg_prefixfree b ==> alg_prefixfree (alg_canon_find l b)

ALG_CANON_FIND_SORTED

|- !l b. alg_sorted b ==> alg_sorted (alg_canon_find l b)

ALG_CANON_IDEMPOT

|- !l. alg_canon (alg_canon l) = alg_canon l

ALG_CANON_MERGE_CONSTANT

|- !l b. alg_twinfree (l::b) ==> (alg_canon_merge l b = l::b)

ALG_CANON_MERGE_PREFIXFREE_PRESERVE

|- !l b h.
     (!x. MEM x (l::b) ==> ~IS_PREFIX h x /\ ~IS_PREFIX x h) ==>
     !x. MEM x (alg_canon_merge l b) ==> ~IS_PREFIX h x /\ ~IS_PREFIX x h

ALG_CANON_MERGE_SHORTENS

|- !l b x. MEM x (alg_canon_merge l b) ==> ?y. MEM y (l::b) /\ IS_PREFIX y x

ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE

|- !l b.
     alg_sorted (l::b) /\ alg_prefixfree (l::b) /\ alg_twinfree b ==>
     alg_sorted (alg_canon_merge l b) /\
     alg_prefixfree (alg_canon_merge l b) /\
     alg_twinfree (alg_canon_merge l b)

ALG_CANON_PREFS_CONSTANT

|- !l b. alg_prefixfree (l::b) ==> (alg_canon_prefs l b = l::b)

ALG_CANON_PREFS_DELETES

|- !l b x. MEM x (alg_canon_prefs l b) ==> MEM x (l::b)

ALG_CANON_PREFS_HD

|- !l b. HD (alg_canon_prefs l b) = l

ALG_CANON_PREFS_PREFIXFREE

|- !l b.
     alg_sorted b /\ alg_prefixfree b ==> alg_prefixfree (alg_canon_prefs l b)

ALG_CANON_PREFS_SORTED

|- !l b. alg_sorted (l::b) ==> alg_sorted (alg_canon_prefs l b)

ALG_CANON_SORTED_PREFIXFREE_TWINFREE

|- !l.
     alg_sorted (alg_canon l) /\ alg_prefixfree (alg_canon l) /\
     alg_twinfree (alg_canon l)

ALG_LONGEST_APPEND

|- !l1 l2.
     alg_longest l1 <= alg_longest (APPEND l1 l2) /\
     alg_longest l2 <= alg_longest (APPEND l1 l2)

ALG_LONGEST_HD

|- !h t. LENGTH h <= alg_longest (h::t)

ALG_LONGEST_TL

|- !h t. alg_longest t <= alg_longest (h::t)

ALG_LONGEST_TLS

|- !h t b. alg_longest (MAP (CONS b) (h::t)) = SUC (alg_longest (h::t))

ALG_ORDER_ANTISYM

|- !x y. alg_order x y /\ alg_order y x ==> (x = y)

alg_order_def

|- (alg_order [] (v6::v7) = T) /\ (alg_order [] [] = T) /\
   (alg_order (v2::v3) [] = F) /\
   (alg_order (h::t) (h'::t') =
    (h = T) /\ (h' = F) \/ (h = h') /\ alg_order t t')

alg_order_ind

|- !P.
     (!v6 v7. P [] (v6::v7)) /\ P [] [] /\ (!v2 v3. P (v2::v3) []) /\
     (!h t h' t'. P t t' ==> P (h::t) (h'::t')) ==>
     !v v1. P v v1

ALG_ORDER_NIL

|- !x. alg_order [] x /\ (alg_order x [] = (x = []))

ALG_ORDER_PREFIX

|- !x y. IS_PREFIX y x ==> alg_order x y

ALG_ORDER_PREFIX_ANTI

|- !x y. alg_order x y /\ IS_PREFIX x y ==> (x = y)

ALG_ORDER_PREFIX_MONO

|- !x y z. alg_order x y /\ alg_order y z /\ IS_PREFIX z x ==> IS_PREFIX y x

ALG_ORDER_PREFIX_TRANS

|- !x y z. alg_order x y /\ IS_PREFIX y z ==> alg_order x z \/ IS_PREFIX x z

ALG_ORDER_REFL

|- !x. alg_order x x

ALG_ORDER_SNOC

|- !x l. ~alg_order (SNOC x l) l

ALG_ORDER_TOTAL

|- !x y. alg_order x y \/ alg_order y x

ALG_ORDER_TRANS

|- !x y z. alg_order x y /\ alg_order y z ==> alg_order x z

ALG_PREFIXFREE_APPEND

|- !h h' t t'.
     alg_prefixfree (APPEND (h::t) (h'::t')) =
     alg_prefixfree (h::t) /\ alg_prefixfree (h'::t') /\
     ~IS_PREFIX h' (LAST (h::t))

alg_prefixfree_def

|- (alg_prefixfree (x::y::z) = ~IS_PREFIX y x /\ alg_prefixfree (y::z)) /\
   (alg_prefixfree [v] = T) /\ (alg_prefixfree [] = T)

ALG_PREFIXFREE_ELT

|- !h t.
     alg_sorted (h::t) /\ alg_prefixfree (h::t) ==>
     !x. MEM x t ==> ~IS_PREFIX x h /\ ~IS_PREFIX h x

ALG_PREFIXFREE_FILTER

|- !P b. alg_sorted b /\ alg_prefixfree b ==> alg_prefixfree (FILTER P b)

alg_prefixfree_ind

|- !P. (!x y z. P (y::z) ==> P (x::y::z)) /\ (!v. P [v]) /\ P [] ==> !v. P v

ALG_PREFIXFREE_MONO

|- !x y z.
     alg_sorted (x::y::z) /\ alg_prefixfree (x::y::z) ==>
     alg_prefixfree (x::z)

ALG_PREFIXFREE_STEP

|- !l1 l2.
     alg_prefixfree (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) =
     alg_prefixfree l1 /\ alg_prefixfree l2

ALG_PREFIXFREE_TL

|- !h t. alg_prefixfree (h::t) ==> alg_prefixfree t

ALG_PREFIXFREE_TLS

|- !l b. alg_prefixfree (MAP (CONS b) l) = alg_prefixfree l

ALG_SORTED_APPEND

|- !h h' t t'.
     alg_sorted (APPEND (h::t) (h'::t')) =
     alg_sorted (h::t) /\ alg_sorted (h'::t') /\ alg_order (LAST (h::t)) h'

alg_sorted_def

|- (alg_sorted (x::y::z) = alg_order x y /\ alg_sorted (y::z)) /\
   (alg_sorted [v] = T) /\ (alg_sorted [] = T)

ALG_SORTED_DEF_ALT

|- !h t. alg_sorted (h::t) = (!x. MEM x t ==> alg_order h x) /\ alg_sorted t

ALG_SORTED_FILTER

|- !P b. alg_sorted b ==> alg_sorted (FILTER P b)

alg_sorted_ind

|- !P. (!x y z. P (y::z) ==> P (x::y::z)) /\ (!v. P [v]) /\ P [] ==> !v. P v

ALG_SORTED_MIN

|- !h t. alg_sorted (h::t) ==> !x. MEM x t ==> alg_order h x

ALG_SORTED_MONO

|- !x y z. alg_sorted (x::y::z) ==> alg_sorted (x::z)

ALG_SORTED_PREFIXFREE_EQUALITY

|- !l l'.
     (!x. MEM x l = MEM x l') /\ alg_sorted l /\ alg_sorted l' /\
     alg_prefixfree l /\ alg_prefixfree l' ==>
     (l = l')

ALG_SORTED_PREFIXFREE_MEM_NIL

|- !l. alg_sorted l /\ alg_prefixfree l /\ MEM [] l = (l = [[]])

ALG_SORTED_STEP

|- !l1 l2.
     alg_sorted (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) =
     alg_sorted l1 /\ alg_sorted l2

ALG_SORTED_TL

|- !h t. alg_sorted (h::t) ==> alg_sorted t

ALG_SORTED_TLS

|- !l b. alg_sorted (MAP (CONS b) l) = alg_sorted l

ALG_TWIN_CONS

|- !x y z h t.
     (alg_twin (x::y::z) (h::t) = (x = h) /\ alg_twin (y::z) t) /\
     (alg_twin (h::t) (x::y::z) = (x = h) /\ alg_twin t (y::z))

ALG_TWIN_NIL

|- !l. ~alg_twin l [] /\ ~alg_twin [] l

ALG_TWIN_REDUCE

|- !h t t'. alg_twin (h::t) (h::t') = alg_twin t t'

ALG_TWIN_SING

|- !x l.
     (alg_twin [x] l = (x = T) /\ (l = [F])) /\
     (alg_twin l [x] = (l = [T]) /\ (x = F))

alg_twinfree_def

|- (alg_twinfree (x::y::z) = ~alg_twin x y /\ alg_twinfree (y::z)) /\
   (alg_twinfree [v] = T) /\ (alg_twinfree [] = T)

alg_twinfree_ind

|- !P. (!x y z. P (y::z) ==> P (x::y::z)) /\ (!v. P [v]) /\ P [] ==> !v. P v

ALG_TWINFREE_STEP

|- !l1 l2.
     ~MEM [] l1 \/ ~MEM [] l2 ==>
     (alg_twinfree (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) =
      alg_twinfree l1 /\ alg_twinfree l2)

ALG_TWINFREE_STEP1

|- !l1 l2.
     alg_twinfree (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) ==>
     alg_twinfree l1 /\ alg_twinfree l2

ALG_TWINFREE_STEP2

|- !l1 l2.
     (~MEM [] l1 \/ ~MEM [] l2) /\ alg_twinfree l1 /\ alg_twinfree l2 ==>
     alg_twinfree (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))

ALG_TWINFREE_TL

|- !h t. alg_twinfree (h::t) ==> alg_twinfree t

ALG_TWINFREE_TLS

|- !l b. alg_twinfree (MAP (CONS b) l) = alg_twinfree l

ALG_TWINS_PREFIX

|- !x l.
     IS_PREFIX x l ==>
     (x = l) \/ IS_PREFIX x (SNOC T l) \/ IS_PREFIX x (SNOC F l)

ALGEBRA_CANON_BASIC

|- algebra_canon [] /\ algebra_canon [[]] /\ !x. algebra_canon [x]

ALGEBRA_CANON_CASES

|- !P.
     P [] /\ P [[]] /\
     (!l1 l2.
        algebra_canon l1 /\ algebra_canon l2 /\
        algebra_canon (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) ==>
        P (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))) ==>
     !l. algebra_canon l ==> P l

ALGEBRA_CANON_CASES_THM

|- !l.
     algebra_canon l ==>
     (l = []) \/ (l = [[]]) \/
     ?l1 l2.
       algebra_canon l1 /\ algebra_canon l2 /\
       (l = APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))

ALGEBRA_CANON_DEF_ALT

|- !l. algebra_canon l = alg_sorted l /\ alg_prefixfree l /\ alg_twinfree l

ALGEBRA_CANON_INDUCTION

|- !P.
     P [] /\ P [[]] /\
     (!l1 l2.
        algebra_canon l1 /\ algebra_canon l2 /\ P l1 /\ P l2 /\
        algebra_canon (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) ==>
        P (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))) ==>
     !l. algebra_canon l ==> P l

ALGEBRA_CANON_NIL_MEM

|- !l. algebra_canon l /\ MEM [] l = (l = [[]])

ALGEBRA_CANON_STEP

|- !l1 l2.
     ~(l1 = [[]]) \/ ~(l2 = [[]]) ==>
     (algebra_canon (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) =
      algebra_canon l1 /\ algebra_canon l2)

ALGEBRA_CANON_STEP1

|- !l1 l2.
     algebra_canon (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) ==>
     algebra_canon l1 /\ algebra_canon l2

ALGEBRA_CANON_STEP2

|- !l1 l2.
     (~(l1 = [[]]) \/ ~(l2 = [[]])) /\ algebra_canon l1 /\
     algebra_canon l2 ==>
     algebra_canon (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))

ALGEBRA_CANON_TL

|- !h t. algebra_canon (h::t) ==> algebra_canon t

ALGEBRA_CANON_TLS

|- !l b. algebra_canon (MAP (CONS b) l) = algebra_canon l

MEM_NIL_STEP

|- !l1 l2. ~MEM [] (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))