Structure cv_typeTheory

signature cv_typeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val from_char_def : thm
    val from_int_def : thm
    val from_list_def : thm
    val from_option_def : thm
    val from_pair_def : thm
    val from_rat_def : thm
    val from_sum_def : thm
    val from_to_def : thm
    val from_unit_def : thm
    val from_word_def : thm
    val to_char_def : thm
    val to_int_def : thm
    val to_list_def : thm
    val to_option_def : thm
    val to_rat_def : thm
    val to_sum_def : thm
    val to_unit_def : thm
    val to_word_def : thm
  
  (*  Theorems  *)
    val cv_has_shape_def : thm
    val cv_has_shape_expand : thm
    val cv_has_shape_ind : thm
    val from_to_bool : thm
    val from_to_char : thm
    val from_to_int : thm
    val from_to_list : thm
    val from_to_num : thm
    val from_to_option : thm
    val from_to_pair : thm
    val from_to_rat : thm
    val from_to_sum : thm
    val from_to_unit : thm
    val from_to_word : thm
    val get_from_option : thm
    val get_from_pair : thm
    val get_from_sum : thm
    val get_to_option : thm
    val get_to_pair : thm
    val get_to_sum : thm
    val to_pair_def : thm
    val to_pair_ind : thm
  
  val cv_type_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [rat] Parent theory of "cv_type"
   
   [words] Parent theory of "cv_type"
   
   [from_char_def]  Definition
      
      ⊢ ∀c. from_char c = Num (ORD c)
   
   [from_int_def]  Definition
      
      ⊢ ∀i. from_int i =
            if integer$int_lt i (integer$int_of_num 0) then
              Pair (Num (integer$Num i)) (Num 0)
            else Num (integer$Num i)
   
   [from_list_def]  Definition
      
      ⊢ (∀f. from_list f [] = Num 0) ∧
        ∀f x xs. from_list f (x::xs) = Pair (f x) (from_list f xs)
   
   [from_option_def]  Definition
      
      ⊢ (∀f. from_option f NONE = Num 0) ∧
        ∀f x. from_option f (SOME x) = Pair (Num 1) (f x)
   
   [from_pair_def]  Definition
      
      ⊢ ∀f1 f2 x y. from_pair f1 f2 (x,y) = Pair (f1 x) (f2 y)
   
   [from_rat_def]  Definition
      
      ⊢ ∀r. from_rat r = Pair (from_int (rat$RATN r)) (Num (rat$RATD r))
   
   [from_sum_def]  Definition
      
      ⊢ (∀f1 f2 x. from_sum f1 f2 (INL x) = Pair (Num 0) (f1 x)) ∧
        ∀f1 f2 y. from_sum f1 f2 (INR y) = Pair (Num 1) (f2 y)
   
   [from_to_def]  Definition
      
      ⊢ ∀f t. from_to f t ⇔ ∀x. t (f x) = x
   
   [from_unit_def]  Definition
      
      ⊢ from_unit () = Num 0
   
   [from_word_def]  Definition
      
      ⊢ ∀w. from_word w = Num (w2n w)
   
   [to_char_def]  Definition
      
      ⊢ ∀x. to_char x = CHR (c2n x)
   
   [to_int_def]  Definition
      
      ⊢ (∀n. to_int (Num n) = integer$int_of_num n) ∧
        ∀x y.
          to_int (Pair x y) = integer$int_neg (integer$int_of_num (c2n x))
   
   [to_list_def]  Definition
      
      ⊢ (∀f n. to_list f (Num n) = []) ∧
        ∀f x y. to_list f (Pair x y) = f x::to_list f y
   
   [to_option_def]  Definition
      
      ⊢ (∀t n. to_option t (Num n) = NONE) ∧
        ∀t x y. to_option t (Pair x y) = SOME (t y)
   
   [to_rat_def]  Definition
      
      ⊢ (∀n. to_rat (Num n) = rat$rat_of_num 0) ∧
        ∀x y.
          to_rat (Pair x y) =
          rat$rat_div (rat$rat_of_int (to_int x)) (rat$rat_of_num (c2n y))
   
   [to_sum_def]  Definition
      
      ⊢ (∀t1 t2 n. to_sum t1 t2 (Num n) = ARB) ∧
        ∀t1 t2 x y.
          to_sum t1 t2 (Pair x y) =
          if x = Num 0 then INL (t1 y) else INR (t2 y)
   
   [to_unit_def]  Definition
      
      ⊢ ∀x. to_unit x = ()
   
   [to_word_def]  Definition
      
      ⊢ ∀n. to_word n = n2w (c2n n)
   
   [cv_has_shape_def]  Theorem
      
      ⊢ (∀y xs x n.
           cv_has_shape (SOME n::xs) (Pair x y) ⇔
           x = Num n ∧ cv_has_shape xs y) ∧
        (∀y xs x. cv_has_shape (NONE::xs) (Pair x y) ⇔ cv_has_shape xs y) ∧
        (∀xs v1 v0. cv_has_shape (v0::xs) (Num v1) ⇔ F) ∧
        ∀c. cv_has_shape [] c ⇔ T
   
   [cv_has_shape_expand]  Theorem
      
      ⊢ (cv_has_shape [] cv ⇔ T) ∧
        (cv_has_shape (NONE::xs) cv ⇔
         ∃x y. cv = Pair x y ∧ cv_has_shape xs y) ∧
        (cv_has_shape (SOME n::xs) cv ⇔
         ∃y. cv = Pair (Num n) y ∧ cv_has_shape xs y)
   
   [cv_has_shape_ind]  Theorem
      
      ⊢ ∀P. (∀n xs x y. P xs y ⇒ P (SOME n::xs) (Pair x y)) ∧
            (∀xs x y. P xs y ⇒ P (NONE::xs) (Pair x y)) ∧
            (∀v0 xs v1. P (v0::xs) (Num v1)) ∧ (∀c. P [] c) ⇒
            ∀v v1. P v v1
   
   [from_to_bool]  Theorem
      
      ⊢ from_to b2c c2b
   
   [from_to_char]  Theorem
      
      ⊢ from_to from_char to_char
   
   [from_to_int]  Theorem
      
      ⊢ from_to from_int to_int
   
   [from_to_list]  Theorem
      
      ⊢ from_to f t ⇒ from_to (from_list f) (to_list t)
   
   [from_to_num]  Theorem
      
      ⊢ from_to Num c2n
   
   [from_to_option]  Theorem
      
      ⊢ from_to f t ⇒ from_to (from_option f) (to_option t)
   
   [from_to_pair]  Theorem
      
      ⊢ from_to f1 t1 ∧ from_to f2 t2 ⇒
        from_to (from_pair f1 f2) (to_pair t1 t2)
   
   [from_to_rat]  Theorem
      
      ⊢ from_to from_rat to_rat
   
   [from_to_sum]  Theorem
      
      ⊢ from_to f1 t1 ∧ from_to f2 t2 ⇒
        from_to (from_sum f1 f2) (to_sum t1 t2)
   
   [from_to_unit]  Theorem
      
      ⊢ from_to from_unit to_unit
   
   [from_to_word]  Theorem
      
      ⊢ from_to from_word to_word
   
   [get_from_option]  Theorem
      
      ⊢ (case v of NONE => Num 0 | SOME x => Pair (Num 1) (f x)) =
        from_option f v
   
   [get_from_pair]  Theorem
      
      ⊢ (case v of (v0,v1) => Pair (f0 v0) (f1 v1)) = from_pair f0 f1 v
   
   [get_from_sum]  Theorem
      
      ⊢ (case v of
           INL x => Pair (Num 0) (f0 x)
         | INR y => Pair (Num 1) (f1 y)) =
        from_sum f0 f1 v
   
   [get_to_option]  Theorem
      
      ⊢ (if cv_has_shape [NONE] v then SOME (t (cv_snd v)) else NONE) =
        to_option t v
   
   [get_to_pair]  Theorem
      
      ⊢ (if cv_has_shape [NONE] v then (t1 (cv_fst v),t2 (cv_snd v))
         else ARB) =
        to_pair t1 t2 v
   
   [get_to_sum]  Theorem
      
      ⊢ (if cv_has_shape [SOME 0] v then INL (t1 (cv_snd v))
         else if cv_has_shape [NONE] v then INR (t2 (cv_snd v))
         else ARB) =
        to_sum t1 t2 v
   
   [to_pair_def]  Theorem
      
      ⊢ to_pair t1 t2 (Pair x y) = (t1 x,t2 y) ∧
        to_pair t1 t2 (Num v4) = ARB
   
   [to_pair_ind]  Theorem
      
      ⊢ ∀P. (∀t1 t2 x y. P t1 t2 (Pair x y)) ∧
            (∀t1 t2 v4. P t1 t2 (Num v4)) ⇒
            ∀v v1 v2. P v v1 v2
   
   
*)
end

HOL 4, Trindemossen-1