Structure cv_repTheory

signature cv_repTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val cv_rep_def : thm
    val implies_def : thm
  
  (*  Theorems  *)
    val IMP_CANCEL : thm
    val IMP_COMM : thm
    val UNCURRY_pair_case : thm
    val cv_eval : thm
    val cv_postprocess : thm
    val cv_proj_def : thm
    val cv_proj_ind : thm
    val cv_proj_less_eq : thm
    val cv_rep_assum : thm
    val cv_rep_eval : thm
    val cv_rep_move : thm
    val cv_rep_trivial : thm
    val cv_termination_simp : thm
    val if_eq_zero : thm
    val lt_zero : thm
    val to_cv_proj : thm
  
  val cv_rep_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [cv_type] Parent theory of "cv_rep"
   
   [cv_rep_def]  Definition
      
      ⊢ ∀pre_cond cv_tm from_fun hol_tm.
          cv_rep pre_cond cv_tm from_fun hol_tm ⇔
          pre_cond ⇒ from_fun hol_tm = cv_tm
   
   [implies_def]  Definition
      
      ⊢ ∀x y. implies x y ⇔ x ⇒ y
   
   [IMP_CANCEL]  Theorem
      
      ⊢ b ⇒ b ⇒ c ⇔ b ⇒ c
   
   [IMP_COMM]  Theorem
      
      ⊢ b1 ⇒ b2 ⇒ c ⇔ b2 ⇒ b1 ⇒ c
   
   [UNCURRY_pair_case]  Theorem
      
      ⊢ ∀f. UNCURRY f = (λx'. case x' of (x,y) => f x y)
   
   [cv_eval]  Theorem
      
      ⊢ c2n (Num n) = n ∧ c2n (Pair x y) = 0 ∧ (c2b (Num n) ⇔ n ≠ 0) ∧
        (c2b (Pair x y) ⇔ F)
   
   [cv_postprocess]  Theorem
      
      ⊢ cv_if c x x = x
   
   [cv_proj_def]  Theorem
      
      ⊢ (∀v. cv_proj [] v = v) ∧
        (∀xs v. cv_proj (T::xs) v = cv_fst (cv_proj xs v)) ∧
        ∀xs v. cv_proj (F::xs) v = cv_snd (cv_proj xs v)
   
   [cv_proj_ind]  Theorem
      
      ⊢ ∀P. (∀v. P [] v) ∧ (∀xs v. P xs v ⇒ P (T::xs) v) ∧
            (∀xs v. P xs v ⇒ P (F::xs) v) ⇒
            ∀v v1. P v v1
   
   [cv_proj_less_eq]  Theorem
      
      ⊢ ∀v xs. cv_size (cv_proj xs v) ≤ cv_size v
   
   [cv_rep_assum]  Theorem
      
      ⊢ cv_rep p (cv (g a)) f x ⇒
        ∀cv_a p_a. cv_rep p_a cv_a g a ⇒ cv_rep (p_a ∧ p) (cv cv_a) f x
   
   [cv_rep_eval]  Theorem
      
      ⊢ cv_rep p y f x ⇒ from_to f t ⇒ p ⇒ x = t y
   
   [cv_rep_move]  Theorem
      
      ⊢ b ⇒ cv_rep p x y z ⇔ cv_rep (b ∧ p) x y z
   
   [cv_rep_trivial]  Theorem
      
      ⊢ ∀f n. cv_rep T (f n) f n
   
   [cv_termination_simp]  Theorem
      
      ⊢ (c2b (cv_ispair cv_v) ⇔ ∃x1 x2. cv_v = Pair x1 x2) ∧
        (c2b (cv_lt (Num 0) cv_v) ⇔ ∃k. cv_v = Num (SUC k)) ∧
        (c2b (cv_lt (Num (NUMERAL (BIT1 n))) (cv_fst cv_v)) ⇔
         ∃k z. cv_v = Pair (Num k) z ∧ NUMERAL (BIT1 n) < k) ∧
        (c2b (cv_lt (Num (NUMERAL (BIT2 n))) (cv_fst cv_v)) ⇔
         ∃k z. cv_v = Pair (Num k) z ∧ NUMERAL (BIT2 n) < k) ∧
        (cv_fst cv_v = Pair x y ⇔ ∃z. cv_v = Pair (Pair x y) z) ∧
        (cv_snd cv_v = Pair x y ⇔ ∃z. cv_v = Pair z (Pair x y)) ∧
        (cv_fst cv_v = Num (SUC k) ⇔ ∃z. cv_v = Pair (Num (SUC k)) z) ∧
        (cv_snd cv_v = Num (SUC k) ⇔ ∃z. cv_v = Pair z (Num (SUC k)))
   
   [if_eq_zero]  Theorem
      
      ⊢ (if n = 0 then x else y) = if 0 < n then y else x
   
   [lt_zero]  Theorem
      
      ⊢ 0 < n ⇔ n ≠ 0
   
   [to_cv_proj]  Theorem
      
      ⊢ cv_fst = cv_proj [T] ∧ cv_snd = cv_proj [F] ∧
        cv_proj xs (cv_proj ys b) = cv_proj (xs ⧺ ys) b
   
   
*)
end

HOL 4, Trindemossen-1