Structure cvTheory
signature cvTheory =
sig
type thm = Thm.thm
(* Definitions *)
val b2c_def : thm
val c2b_def : thm
val cv_case_def : thm
val cv_eq_def0 : thm
val cv_exp_def : thm
val cv_fst_def : thm
val cv_if_def0 : thm
val cv_ispair_def : thm
val cv_lt_def0 : thm
val cv_size_def : thm
val cv_snd_def : thm
(* Theorems *)
val CV_EQ : thm
val DIV_RECURSIVE : thm
val EVEN_to_cv : thm
val LT_RECURSIVE : thm
val MOD_RECURSIVE : thm
val Num_11 : thm
val ODD_to_cv : thm
val Pair_11 : thm
val SUC_EQ : thm
val add_to_cv : thm
val b2c : thm
val b2c_if : thm
val c2b_thm : thm
val c2n_def : thm
val cv_Axiom : thm
val cv_add_def : thm
val cv_distinct : thm
val cv_div_def : thm
val cv_eq : thm
val cv_eq_def : thm
val cv_exp_eq : thm
val cv_extras : thm
val cv_if : thm
val cv_if_cong : thm
val cv_if_def : thm
val cv_induction : thm
val cv_lt_def : thm
val cv_mod_def : thm
val cv_mul_def : thm
val cv_sub_def : thm
val div_to_cv : thm
val exp_to_cv : thm
val ge_to_cv : thm
val gt_to_cv : thm
val isnseq_cases : thm
val isnseq_cons : thm
val isnseq_ind : thm
val isnseq_nil : thm
val isnseq_rules : thm
val isnseq_strongind : thm
val le_to_cv : thm
val lt_to_cv : thm
val mod_to_cv : thm
val mul_to_cv : thm
val neq_to_cv : thm
val pre_to_cv : thm
val sub_to_cv : thm
val suc_to_cv : thm
val cv_grammars : type_grammar.grammar * term_grammar.grammar
(*
[numeral] Parent theory of "cv"
[b2c_def] Definition
⊢ b2c T = cv$Num (SUC 0) ∧ b2c F = cv$Num 0
[c2b_def] Definition
⊢ ∀x. cv$c2b x ⇔ ∃k. x = cv$Num (SUC k)
[cv_case_def] Definition
⊢ (∀n nmf prf. cv_CASE (cv$Num n) nmf prf = nmf n) ∧
∀c d nmf prf. cv_CASE (cv$Pair c d) nmf prf = prf c d
[cv_eq_def0] Definition
⊢ ∀c d. cv_eq c d = b2c (c = d)
[cv_exp_def] Definition
⊢ ∀m n. cv_exp m n = cv$Num (cv$c2n m ** cv$c2n n)
[cv_fst_def] Definition
⊢ (∀p q. cv_fst (cv$Pair p q) = p) ∧ ∀m. cv_fst (cv$Num m) = cv$Num 0
[cv_if_def0] Definition
⊢ ∀p q r. cv_if p q r = if cv$c2b p then q else r
[cv_ispair_def] Definition
⊢ (∀p q. cv_ispair (cv$Pair p q) = cv$Num (SUC 0)) ∧
∀m. cv_ispair (cv$Num m) = cv$Num 0
[cv_lt_def0] Definition
⊢ (∀m c.
cv_lt (cv$Num m) c =
case c of cv$Num n => b2c (m < n) | cv$Pair v4 v5 => cv$Num 0) ∧
∀c d e. cv_lt (cv$Pair c d) e = cv$Num 0
[cv_size_def] Definition
⊢ (∀n. cv_size (cv$Num n) = n) ∧
∀c d. cv_size (cv$Pair c d) = 1 + (cv_size c + cv_size d)
[cv_snd_def] Definition
⊢ (∀p q. cv_snd (cv$Pair p q) = q) ∧ ∀m. cv_snd (cv$Num m) = cv$Num 0
[CV_EQ] Theorem
⊢ (cv$Pair p q = cv$Pair r s ⇔ if p = r then q = s else F) ∧
(cv$Pair p q = cv$Num n ⇔ F) ∧ (cv$Num m = cv$Num n ⇔ m = n)
[DIV_RECURSIVE] Theorem
⊢ m DIV n =
if n = 0 then 0 else if m < n then 0 else SUC ((m − n) DIV n)
[EVEN_to_cv] Theorem
⊢ EVEN n ⇔ ¬cv$c2b (cv_mod (cv$Num n) (cv$Num 2))
[LT_RECURSIVE] Theorem
⊢ (m < 0 ⇔ F) ∧ (m < SUC n ⇔ if m = n then T else m < n)
[MOD_RECURSIVE] Theorem
⊢ m MOD n = if n = 0 then m else if m < n then m else (m − n) MOD n
[Num_11] Theorem
⊢ cv$Num m = cv$Num n ⇔ m = n
[ODD_to_cv] Theorem
⊢ ODD n ⇔ cv$c2b (cv_mod (cv$Num n) (cv$Num 2))
[Pair_11] Theorem
⊢ cv$Pair c d = cv$Pair e f ⇔ c = e ∧ d = f
[SUC_EQ] Theorem
⊢ (SUC m = 0 ⇔ F) ∧ (SUC m = SUC n ⇔ m = n)
[add_to_cv] Theorem
⊢ m + n = cv$c2n (cv_add (cv$Num m) (cv$Num n))
[b2c] Theorem
⊢ (b2c x = cv$Num 1 ⇔ x) ∧ (b2c x = cv$Num (SUC 0) ⇔ x)
[b2c_if] Theorem
⊢ b2c g = if g then cv$Num (SUC 0) else cv$Num 0
[c2b_thm] Theorem
⊢ (cv$c2b (cv$Num (SUC n)) ⇔ T) ∧ (cv$c2b (cv$Num 1) ⇔ T) ∧
(cv$c2b (cv$Num 0) ⇔ F) ∧ (cv$c2b (cv$Num 0) ⇔ F) ∧
(cv$c2b (cv$Pair x y) ⇔ F)
[c2n_def] Theorem
⊢ (∀n. cv$c2n (cv$Num n) = n) ∧ ∀c d. cv$c2n (cv$Pair c d) = 0
[cv_Axiom] Theorem
⊢ ∀f g. ∃h.
(∀n. h (cv$Num n) = f n) ∧
∀c d. h (cv$Pair c d) = g c d (h c) (h d)
[cv_add_def] Theorem
⊢ cv_add (cv$Num m) (cv$Num n) = cv$Num (m + n) ∧
cv_add (cv$Num m) (cv$Pair p q) = cv$Num m ∧
cv_add (cv$Pair p q) (cv$Num n) = cv$Num n ∧
cv_add (cv$Pair p q) (cv$Pair r s) = cv$Num 0
[cv_distinct] Theorem
⊢ cv$Num n ≠ cv$Pair c d
[cv_div_def] Theorem
⊢ cv_div (cv$Num m) (cv$Num n) = cv$Num (m DIV n) ∧
cv_div (cv$Num m) (cv$Pair p q) = cv$Num 0 ∧
cv_div (cv$Pair p q) (cv$Num n) = cv$Num 0 ∧
cv_div (cv$Pair p q) (cv$Pair r s) = cv$Num 0
[cv_eq] Theorem
⊢ cv_eq (cv$Pair x y) (cv$Pair x' y') = b2c (x = x' ∧ y = y') ∧
cv_eq (cv$Num m) (cv$Num n) = b2c (m = n) ∧
cv_eq (cv$Pair x y) (cv$Num n) = b2c F ∧
cv_eq (cv$Num n) (cv$Pair x y) = b2c F
[cv_eq_def] Theorem
⊢ cv_eq p q = cv$Num (if p = q then SUC 0 else 0)
[cv_exp_eq] Theorem
⊢ cv_exp b e =
cv_if e
(cv_if (cv_mod e (cv$Num 2))
(cv_mul b (cv_exp b (cv_sub e (cv$Num 1))))
(let x = cv_exp b (cv_div e (cv$Num 2)) in cv_mul x x))
(cv$Num 1)
[cv_extras] Theorem
⊢ cv_lt v (cv$Pair x y) = cv$Num 0 ∧
cv_lt (cv$Pair x y) v = cv$Num 0 ∧
cv_add (cv$Pair x y) v =
(case v of cv$Num v4 => v | cv$Pair a b => cv$Num 0) ∧
cv_add v (cv$Pair x y) =
(case v of cv$Num v4 => v | cv$Pair a b => cv$Num 0) ∧
cv_sub (cv$Pair x y) v = cv$Num 0 ∧
cv_sub v (cv$Pair x y) =
(case v of cv$Num v4 => v | cv$Pair a b => cv$Num 0) ∧
cv_mul (cv$Pair x y) v = cv$Num 0 ∧
cv_mul v (cv$Pair x y) = cv$Num 0 ∧
cv_div (cv$Pair x y) v = cv$Num 0 ∧
cv_div v (cv$Pair x y) = cv$Num 0 ∧
cv_mod (cv$Pair x y) v = cv$Num 0 ∧
cv_mod v (cv$Pair x y) =
case v of cv$Num v4 => v | cv$Pair a b => cv$Num 0
[cv_if] Theorem
⊢ cv_if x y z = if cv$c2b x then y else z
[cv_if_cong] Theorem
⊢ (cv$c2b P ⇔ cv$c2b Q) ∧ (cv$c2b Q ⇒ x = x') ∧ (¬cv$c2b Q ⇒ y = y') ⇒
cv_if P x y = cv_if Q x' y'
[cv_if_def] Theorem
⊢ cv_if (cv$Num (SUC m)) p q = p ∧ cv_if (cv$Num 0) p q = q ∧
cv_if (cv$Pair r s) p q = q
[cv_induction] Theorem
⊢ ∀P. (∀m. P (cv$Num m)) ∧ (∀g g'. P g ∧ P g' ⇒ P (cv$Pair g g')) ⇒
∀g. P g
[cv_lt_def] Theorem
⊢ cv_lt (cv$Num m) (cv$Num n) = cv$Num (if m < n then SUC 0 else 0) ∧
cv_lt (cv$Num m) (cv$Pair p q) = cv$Num 0 ∧
cv_lt (cv$Pair p q) (cv$Num n) = cv$Num 0 ∧
cv_lt (cv$Pair p q) (cv$Pair r s) = cv$Num 0
[cv_mod_def] Theorem
⊢ cv_mod (cv$Num m) (cv$Num n) = cv$Num (m MOD n) ∧
cv_mod (cv$Num m) (cv$Pair p q) = cv$Num m ∧
cv_mod (cv$Pair p q) (cv$Num n) = cv$Num 0 ∧
cv_mod (cv$Pair p q) (cv$Pair r s) = cv$Num 0
[cv_mul_def] Theorem
⊢ cv_mul (cv$Num m) (cv$Num n) = cv$Num (m * n) ∧
cv_mul (cv$Num m) (cv$Pair p q) = cv$Num 0 ∧
cv_mul (cv$Pair p q) (cv$Num n) = cv$Num 0 ∧
cv_mul (cv$Pair p q) (cv$Pair r s) = cv$Num 0
[cv_sub_def] Theorem
⊢ cv_sub (cv$Num m) (cv$Num n) = cv$Num (m − n) ∧
cv_sub (cv$Num m) (cv$Pair p q) = cv$Num m ∧
cv_sub (cv$Pair p q) (cv$Num n) = cv$Num 0 ∧
cv_sub (cv$Pair p q) (cv$Pair r s) = cv$Num 0
[div_to_cv] Theorem
⊢ m DIV n = cv$c2n (cv_div (cv$Num m) (cv$Num n))
[exp_to_cv] Theorem
⊢ m ** n = cv$c2n (cv_exp (cv$Num m) (cv$Num n))
[ge_to_cv] Theorem
⊢ n ≥ m ⇔ ¬cv$c2b (cv_lt (cv$Num n) (cv$Num m))
[gt_to_cv] Theorem
⊢ m > n ⇔ cv$c2b (cv_lt (cv$Num n) (cv$Num m))
[isnseq_cases] Theorem
⊢ ∀a0. isnseq a0 ⇔ a0 = cv$Num 0 ∨ ∃n c. a0 = cv$Pair n c ∧ isnseq c
[isnseq_cons] Theorem
⊢ ∀n c. isnseq c ⇒ isnseq (cv$Pair n c)
[isnseq_ind] Theorem
⊢ ∀isnseq'.
isnseq' (cv$Num 0) ∧ (∀n c. isnseq' c ⇒ isnseq' (cv$Pair n c)) ⇒
∀a0. isnseq a0 ⇒ isnseq' a0
[isnseq_nil] Theorem
⊢ isnseq (cv$Num 0)
[isnseq_rules] Theorem
⊢ isnseq (cv$Num 0) ∧ ∀n c. isnseq c ⇒ isnseq (cv$Pair n c)
[isnseq_strongind] Theorem
⊢ ∀isnseq'.
isnseq' (cv$Num 0) ∧
(∀n c. isnseq c ∧ isnseq' c ⇒ isnseq' (cv$Pair n c)) ⇒
∀a0. isnseq a0 ⇒ isnseq' a0
[le_to_cv] Theorem
⊢ m ≤ n ⇔ ¬cv$c2b (cv_lt (cv$Num n) (cv$Num m))
[lt_to_cv] Theorem
⊢ m < n ⇔ cv$c2b (cv_lt (cv$Num m) (cv$Num n))
[mod_to_cv] Theorem
⊢ m MOD n = cv$c2n (cv_mod (cv$Num m) (cv$Num n))
[mul_to_cv] Theorem
⊢ m * n = cv$c2n (cv_mul (cv$Num m) (cv$Num n))
[neq_to_cv] Theorem
⊢ ∀m n. m = n ⇔ cv$c2b (cv_eq (cv$Num m) (cv$Num n))
[pre_to_cv] Theorem
⊢ PRE m = cv$c2n (cv_sub (cv$Num m) (cv$Num 1))
[sub_to_cv] Theorem
⊢ m − n = cv$c2n (cv_sub (cv$Num m) (cv$Num n))
[suc_to_cv] Theorem
⊢ SUC m = cv$c2n (cv_add (cv$Num m) (cv$Num 1))
*)
end
HOL 4, Trindemossen-1