# Structure defCNFTheory

Source File Identifier index Theory binding index

```signature defCNFTheory =
sig
type thm = Thm.thm

(*  Definitions  *)
val DEF_def : thm
val OKDEF_def : thm

(*  Theorems  *)
val BIGSTEP : thm
val CONSISTENCY : thm
val DEF_SNOC : thm
val FINAL_DEF : thm
val OKDEF_SNOC : thm
val OK_def : thm
val OK_ind : thm
val UNIQUE_def : thm
val UNIQUE_ind : thm

val defCNF_grammars : type_grammar.grammar * term_grammar.grammar
(*
[rich_list] Parent theory of "defCNF"

[DEF_def]  Definition

⊢ (∀v n. defCNF\$DEF v n [] ⇔ T) ∧
∀v n x xs.
defCNF\$DEF v n (x::xs) ⇔
defCNF\$UNIQUE v n x ∧ defCNF\$DEF v (SUC n) xs

[OKDEF_def]  Definition

⊢ (∀n. defCNF\$OKDEF n [] ⇔ T) ∧
∀n x xs.
defCNF\$OKDEF n (x::xs) ⇔
defCNF\$OK n x ∧ defCNF\$OKDEF (SUC n) xs

[BIGSTEP]  Theorem

⊢ ∀P Q R. (∀v. P v ⇒ (Q ⇔ R v)) ⇒ ((∃v. P v) ∧ Q ⇔ ∃v. P v ∧ R v)

[CONSISTENCY]  Theorem

⊢ ∀n l. defCNF\$OKDEF n l ⇒ ∃v. defCNF\$DEF v n l

[DEF_SNOC]  Theorem

⊢ ∀n x l v.
defCNF\$DEF v n (SNOC x l) ⇔
defCNF\$DEF v n l ∧ defCNF\$UNIQUE v (n + LENGTH l) x

[FINAL_DEF]  Theorem

⊢ ∀v n x. (v n ⇔ x) ⇔ (v n ⇔ x) ∧ defCNF\$DEF v (SUC n) []

[OKDEF_SNOC]  Theorem

⊢ ∀n x l.
defCNF\$OKDEF n (SNOC x l) ⇔
defCNF\$OKDEF n l ∧ defCNF\$OK (n + LENGTH l) x

[OK_def]  Theorem

⊢ (defCNF\$OK n (conn,INL i,INL j) ⇔ i < n ∧ j < n) ∧
(defCNF\$OK n (conn,INL i,INR b) ⇔ i < n) ∧
(defCNF\$OK n (conn,INR a,INL j) ⇔ j < n) ∧
(defCNF\$OK n (conn,INR a,INR b) ⇔ T)

[OK_ind]  Theorem

⊢ ∀P.
(∀n conn i j. P n (conn,INL i,INL j)) ∧
(∀n conn i b. P n (conn,INL i,INR b)) ∧
(∀n conn a j. P n (conn,INR a,INL j)) ∧
(∀n conn a b. P n (conn,INR a,INR b)) ⇒
∀v v1 v2 v3. P v (v1,v2,v3)

[UNIQUE_def]  Theorem

⊢ (defCNF\$UNIQUE v n (conn,INL i,INL j) ⇔ (v n ⇔ conn (v i) (v j))) ∧
(defCNF\$UNIQUE v n (conn,INL i,INR b) ⇔ (v n ⇔ conn (v i) b)) ∧
(defCNF\$UNIQUE v n (conn,INR a,INL j) ⇔ (v n ⇔ conn a (v j))) ∧
(defCNF\$UNIQUE v n (conn,INR a,INR b) ⇔ (v n ⇔ conn a b))

[UNIQUE_ind]  Theorem

⊢ ∀P.
(∀v n conn i j. P v n (conn,INL i,INL j)) ∧
(∀v n conn i b. P v n (conn,INL i,INR b)) ∧
(∀v n conn a j. P v n (conn,INR a,INL j)) ∧
(∀v n conn a b. P v n (conn,INR a,INR b)) ⇒
∀v v1 v2 v3 v4. P v v1 (v2,v3,v4)

*)
end

```

Source File Identifier index Theory binding index