Structure fcpTheory

signature fcpTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val FCP : thm
    val HAS_SIZE_def : thm
    val cart_TY_DEF : thm
    val cart_tybij : thm
    val dimindex_def : thm
    val finite_image_TY_DEF : thm
    val finite_image_tybij : thm
    val finite_index_def : thm
    val index : thm
  
  (*  Theorems  *)
    val CART_EQ : thm
    val DIMINDEX_GE_1 : thm
    val FCP_BETA : thm
    val FCP_ETA : thm
    val dimindex : thm
    val index_size : thm
    val index_sum : thm
  
  val fcp_grammars : type_grammar.grammar * term_grammar.grammar
  
  
(*
   [list] Parent theory of "fcp"
   
   [pred_set] Parent theory of "fcp"
   
   [FCP]  Definition
      
      |- $FCP = (\g. @f. !i. i < dimindex (:'b) ==> (f %% i = g i))
   
   [HAS_SIZE_def]  Definition
      
      |- !s n. (s HAS_SIZE n) = FINITE s /\ (CARD s = n)
   
   [cart_TY_DEF]  Definition
      
      |- ?rep. TYPE_DEFINITION (\f. T) rep
   
   [cart_tybij]  Definition
      
      |- (!a. mk_cart (dest_cart a) = a) /\
         !r. (\f. T) r = (dest_cart (mk_cart r) = r)
   
   [dimindex_def]  Definition
      
      |- dimindex (:'a) = (if FINITE UNIV then CARD UNIV else 1)
   
   [finite_image_TY_DEF]  Definition
      
      |- ?rep. TYPE_DEFINITION (\x. (x = ARB) \/ FINITE UNIV) rep
   
   [finite_image_tybij]  Definition
      
      |- (!a. mk_finite_image (dest_finite_image a) = a) /\
         !r.
           (\x. (x = ARB) \/ FINITE UNIV) r =
           (dest_finite_image (mk_finite_image r) = r)
   
   [finite_index_def]  Definition
      
      |- finite_index = @f. !x. ?!n. n < dimindex (:'a) /\ (f n = x)
   
   [index]  Definition
      
      |- !x i. x %% i = dest_cart x (finite_index i)
   
   [CART_EQ]  Theorem
      
      |- !x y. (x = y) = !i. i < dimindex (:'b) ==> (x %% i = y %% i)
   
   [DIMINDEX_GE_1]  Theorem
      
      |- 1 <= dimindex (:'a)
   
   [FCP_BETA]  Theorem
      
      |- !i. i < dimindex (:'b) ==> ($FCP g %% i = g i)
   
   [FCP_ETA]  Theorem
      
      |- !g. (FCP i. g %% i) = g
   
   [dimindex]  Theorem
      
      |- dimindex (:'a) = (if FINITE UNIV then CARD UNIV else 1)
   
   [index_size]  Theorem
      
      |- !f n. BIJ f (count n) (IMAGE f (count n)) ==> (CARD (IMAGE f (count n)) = n)
   
   [index_sum]  Theorem
      
      |- dimindex (:'a + 'b) =
         (if FINITE UNIV /\ FINITE UNIV then dimindex (:'a) + dimindex (:'b) else 1)
   
   
*)
end