# Structure cv_repTheory

Source File Identifier index Theory binding index

```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

```

Source File Identifier index Theory binding index

HOL 4, Trindemossen-1