Structure defCNFTheory

signature defCNFTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val DEF_def : thm
    val OKDEF_def : thm
    val OK_curried_def : thm
    val OK_tupled_primitive_def : thm
    val UNIQUE_curried_def : thm
    val UNIQUE_tupled_primitive_def : thm
  
  (*  Theorems  *)
    val CONSISTENCY : thm
    val DEF_SNOC : thm
    val OKDEF_SNOC : thm
    val OK_def : thm
    val OK_ind : thm
    val UNIQUE_def : thm
    val UNIQUE_ind : thm
  
  val defCNF_grammars : type_grammar.grammar * term_grammar.grammar
  
  
(*
   [rich_list] Parent theory of "defCNF"
   
   [DEF_def]  Definition
      
      |- (!v n. DEF v n [] = T) /\
         !v n x xs. DEF v n (x::xs) = UNIQUE v n x /\ DEF v (SUC n) xs
   
   [OKDEF_def]  Definition
      
      |- (!n. OKDEF n [] = T) /\
         !n x xs. OKDEF n (x::xs) = OK n x /\ OKDEF (SUC n) xs
   
   [OK_curried_def]  Definition
      
      |- !x x1. OK x x1 = OK_tupled (x,x1)
   
   [OK_tupled_primitive_def]  Definition
      
      |- 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)
   
   [UNIQUE_curried_def]  Definition
      
      |- !x x1 x2. UNIQUE x x1 x2 = UNIQUE_tupled (x,x1,x2)
   
   [UNIQUE_tupled_primitive_def]  Definition
      
      |- 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'))
   
   [CONSISTENCY]  Theorem
      
      |- !n l. OKDEF n l ==> ?v. DEF v n l
   
   [DEF_SNOC]  Theorem
      
      |- !n x l v. DEF v n (SNOC x l) = DEF v n l /\ UNIQUE v (n + LENGTH l) x
   
   [OKDEF_SNOC]  Theorem
      
      |- !n x l. OKDEF n (SNOC x l) = OKDEF n l /\ OK (n + LENGTH l) x
   
   [OK_def]  Theorem
      
      |- (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)
   
   [OK_ind]  Theorem
      
      |- !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)
   
   [UNIQUE_def]  Theorem
      
      |- (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))
   
   [UNIQUE_ind]  Theorem
      
      |- !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)
   
   
*)
end