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_list_tr_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 IMP_from_option_eq : thm
    val IMP_from_pair_eq : thm
    val IMP_to_option : thm
    val IMP_to_pair : thm
    val cv_has_shape_def : thm
    val cv_has_shape_expand : thm
    val cv_has_shape_ind : thm
    val from_option_eq_IMP : thm
    val from_pair_eq_IMP : 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_list_tr_eq : thm
    val to_option_IMP : thm
    val to_pair_IMP : thm
    val to_pair_def : thm
    val to_pair_ind : thm
(*
   [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 i < 0 then Pair (Num (Num i)) (Num 0) else Num (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 (RATN r)) (Num (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) = &n) ∧ ∀x y. to_int (Pair x y) = -&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_list_tr_def]  Definition
      
      ⊢ (∀f n acc. to_list_tr f (Num n) acc = REVERSE acc) ∧
        ∀f x y acc. to_list_tr f (Pair x y) acc = to_list_tr f y (f x::acc)
   
   [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) = 0) ∧
        ∀x y. to_rat (Pair x y) = rat_of_int (to_int x) / &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)
   
   [IMP_from_option_eq]  Theorem
      
      ⊢ f1 (THE x) = y1 ∧ IS_SOME x ⇒ from_option f1 x = Pair (Num 1) y1
   
   [IMP_from_pair_eq]  Theorem
      
      ⊢ f1 (FST x) = y1 ∧ f2 (SND x) = y2 ⇒ from_pair f1 f2 x = Pair y1 y2
   
   [IMP_to_option]  Theorem
      
      ⊢ THE x = y1 ∧ IS_SOME x ⇒ x = SOME y1
   
   [IMP_to_pair]  Theorem
      
      ⊢ FST x = y1 ∧ SND x = y2 ⇒ x = (y1,y2)
   
   [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_option_eq_IMP]  Theorem
      
      ⊢ from_option f1 x = Pair (Num 1) y1 ⇒ f1 (THE x) = y1 ∧ IS_SOME x
   
   [from_pair_eq_IMP]  Theorem
      
      ⊢ from_pair f1 f2 x = Pair y1 y2 ⇒ f1 (FST x) = y1 ∧ f2 (SND x) = y2
   
   [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_list_tr_eq]  Theorem
      
      ⊢ to_list f v = to_list_tr f v []
   
   [to_option_IMP]  Theorem
      
      ⊢ x = to_option t1 (Pair x1 x2) ⇒ THE x = t1 x2 ∧ IS_SOME x
   
   [to_pair_IMP]  Theorem
      
      ⊢ x = to_pair t1 t2 (Pair x1 x2) ⇒ FST x = t1 x1 ∧ SND x = t2 x2
   
   [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-2