Theory "defCNF"

Parents rich_list

Signature

Constant	Type
UNIQUE_tupled	:(num -> bool) # num # (bool -> bool -> bool) # (num + bool) # (num + bool) -> bool
UNIQUE	:(num -> bool) -> num -> (bool -> bool -> bool) # (num + bool) # (num + bool) -> bool
OK_tupled	:num # (bool -> bool -> bool) # (num + bool) # (num + bool) -> bool
OKDEF	:num -> ((bool -> bool -> bool) # (num + bool) # (num + bool)) list -> bool
OK	:num -> (bool -> bool -> bool) # (num + bool) # (num + bool) -> bool
DEF	:(num -> bool) -> num -> ((bool -> bool -> bool) # (num + bool) # (num + bool)) list -> bool

Definitions

UNIQUE_tupled_primitive_def

|- UNIQUE_tupled =
   WFREC (@R. WF R)
     (\UNIQUE_tupled a'.
        case a' of
           (v,n,conn,INL i,INL j) -> I (v n = conn (v i) (v j))
        || (v,n,conn,INL i,INR b) -> I (v n = conn (v i) b)
        || (v,n,conn,INR a,INL j') -> I (v n = conn a (v j'))
        || (v,n,conn,INR a,INR b') -> I (v n = conn a b'))

UNIQUE_curried_def

|- !x x1 x2. UNIQUE x x1 x2 = UNIQUE_tupled (x,x1,x2)

DEF_def

|- (!v n. DEF v n [] = T) /\
   !v n x xs. DEF v n (x::xs) = UNIQUE v n x /\ DEF v (SUC n) xs

OK_tupled_primitive_def

|- OK_tupled =
   WFREC (@R. WF R)
     (\OK_tupled a'.
        case a' of
           (n,conn,INL i,INL j) -> I (i < n /\ j < n)
        || (n,conn,INL i,INR b) -> I (i < n)
        || (n,conn,INR a,INL j') -> I (j' < n)
        || (n,conn,INR a,INR b') -> I T)

OK_curried_def

|- !x x1. OK x x1 = OK_tupled (x,x1)

OKDEF_def

|- (!n. OKDEF n [] = T) /\
   !n x xs. OKDEF n (x::xs) = OK n x /\ OKDEF (SUC n) xs

Theorems

UNIQUE_ind

|- !P.
     (!v n conn i j. P v n (conn,INL i,INL j)) /\
     (!v n conn i b. P v n (conn,INL i,INR b)) /\
     (!v n conn a j. P v n (conn,INR a,INL j)) /\
     (!v n conn a b. P v n (conn,INR a,INR b)) ==>
     !v v1 v2 v3 v4. P v v1 (v2,v3,v4)

UNIQUE_def

|- (UNIQUE v n (conn,INL i,INL j) = (v n = conn (v i) (v j))) /\
   (UNIQUE v n (conn,INL i,INR b) = (v n = conn (v i) b)) /\
   (UNIQUE v n (conn,INR a,INL j) = (v n = conn a (v j))) /\
   (UNIQUE v n (conn,INR a,INR b) = (v n = conn a b))

OK_ind

|- !P.
     (!n conn i j. P n (conn,INL i,INL j)) /\
     (!n conn i b. P n (conn,INL i,INR b)) /\
     (!n conn a j. P n (conn,INR a,INL j)) /\
     (!n conn a b. P n (conn,INR a,INR b)) ==>
     !v v1 v2 v3. P v (v1,v2,v3)

OK_def

|- (OK n (conn,INL i,INL j) = i < n /\ j < n) /\
   (OK n (conn,INL i,INR b) = i < n) /\ (OK n (conn,INR a,INL j) = j < n) /\
   (OK n (conn,INR a,INR b) = T)

DEF_SNOC

|- !n x l v. DEF v n (SNOC x l) = DEF v n l /\ UNIQUE v (n + LENGTH l) x

OKDEF_SNOC

|- !n x l. OKDEF n (SNOC x l) = OKDEF n l /\ OK (n + LENGTH l) x

CONSISTENCY

|- !n l. OKDEF n l ==> ?v. DEF v n l