prove_case_elim_thm

`prove_case_elim_thm`

Prim_rec.prove_case_elim_thm : {case_def : thm, nchotomy : thm} -> thm

Proves a theorem that eliminates applications of case constants with boolean type.

If case_def is the definition of a data type's case constant, where each clause is of the form

   !a1 .. ai f1 .. fm. type_CASE (ctor_i a1 .. ai) f1 .. fm = f_i a1 .. ai

and if nchotomy is a theorem describing how a data type's values are classified by constructor, of the form

   !v. (?a1 .. ai. v = ctor_1 a1 .. ai) \/
       (?b1 .. bj. v = ctor_2 b1 .. bj) \/
       ...

then a call to prove_case_elim_thm{case_def = case_def, nchotomy = nchotomy} will return a theorem of the form

   type_CASE v f1 .. fm <=>
     (?a1 .. ai. v = ctor_1 a1 .. ai /\ f1 a1 .. ai) \/
     (?b1 .. bj. v = ctor_2 b1 .. bj /\ f2 b1 .. bj) \/
     ...

Used as a rewrite theorem, this result will "eliminate" occurrences of the case-constant from a term, when the case-constant term has boolean type.

Will fail if the provided theorems are not of the required form. The theorems stored in the TypeBase are of the correct form. The theorem returned by Prim_rec.prove_cases_thm is of the correct form for the nchotomy argument to this function.

Example

> prove_case_elim_thm {case_def = TypeBase.case_def_of ``:num``,
                      nchotomy = TypeBase.nchotomy_of ``:num``};
val it = ⊢ num_CASE x v f ⇔ x = 0 ∧ v ∨ ∃n. x = SUC n ∧ f n: thm

> prove_case_elim_thm {case_def = TypeBase.case_def_of ``:bool``,
                      nchotomy = TypeBase.nchotomy_of ``:bool``};
val it = ⊢ (if x then t1 else t2) ⇔ (x ⇔ T) ∧ t1 ∨ (x ⇔ F) ∧ t2: thm

HOL: Reference