# Theory Inductive

Up to index of Isabelle/HOL

theory Inductive
imports FixedPoint Sum_Type Relation Record
uses (Tools/inductive_package.ML) (Tools/inductive_realizer.ML) (Tools/inductive_codegen.ML) (Tools/datatype_aux.ML) (Tools/datatype_prop.ML) (Tools/datatype_rep_proofs.ML) (Tools/datatype_abs_proofs.ML) (Tools/datatype_realizer.ML) (Tools/datatype_package.ML) (Tools/datatype_codegen.ML) (Tools/recfun_codegen.ML) (Tools/primrec_package.ML)
begin

    (*  Title:      HOL/Inductive.thy
        ID:         $Id: Inductive.thy,v 1.34 2005/08/03 12:48:13 avigad Exp $
        Author:     Markus Wenzel, TU Muenchen
    *)

    header {* Support for inductive sets and types *}

    theory Inductive
    imports FixedPoint Sum_Type Relation Record
    uses
      ("Tools/inductive_package.ML")
      ("Tools/inductive_realizer.ML")
      ("Tools/inductive_codegen.ML")
      ("Tools/datatype_aux.ML")
      ("Tools/datatype_prop.ML")
      ("Tools/datatype_rep_proofs.ML")
      ("Tools/datatype_abs_proofs.ML")
      ("Tools/datatype_realizer.ML")
      ("Tools/datatype_package.ML")
      ("Tools/datatype_codegen.ML")
      ("Tools/recfun_codegen.ML")
      ("Tools/primrec_package.ML")
    begin

    subsection {* Inductive sets *}

    text {* Inversion of injective functions. *}

    constdefs
      myinv :: "('a => 'b) => ('b => 'a)"
      "myinv (f :: 'a => 'b) == λy. THE x. f x = y"

    lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
    proof -
      assume "inj f"
      hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
        by (simp only: inj_eq)
      also have "... = x" by (rule the_eq_trivial)
      finally show ?thesis by (unfold myinv_def)
    qed

    lemma f_myinv_f: "inj f ==> y ∈ range f ==> f (myinv f y) = y"
    proof (unfold myinv_def)
      assume inj: "inj f"
      assume "y ∈ range f"
      then obtain x where "y = f x" ..
      hence x: "f x = y" ..
      thus "f (THE x. f x = y) = y"
      proof (rule theI)
        fix x' assume "f x' = y"
        with x have "f x' = f x" by simp
        with inj show "x' = x" by (rule injD)
      qed
    qed

    hide const myinv

    text {* Package setup. *}

    use "Tools/inductive_package.ML"
    setup InductivePackage.setup

    theorems basic_monos [mono] =
      subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
      Collect_mono in_mono vimage_mono
      imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
      not_all not_ex
      Ball_def Bex_def
      induct_rulify2

    subsection {* Inductive datatypes and primitive recursion *}

    text {* Package setup. *}

    use "Tools/recfun_codegen.ML"
    setup RecfunCodegen.setup

    use "Tools/datatype_aux.ML"
    use "Tools/datatype_prop.ML"
    use "Tools/datatype_rep_proofs.ML"
    use "Tools/datatype_abs_proofs.ML"
    use "Tools/datatype_realizer.ML"
    use "Tools/datatype_package.ML"
    setup DatatypePackage.setup

    use "Tools/datatype_codegen.ML"
    setup DatatypeCodegen.setup

    use "Tools/inductive_realizer.ML"
    setup InductiveRealizer.setup

    use "Tools/inductive_codegen.ML"
    setup InductiveCodegen.setup

    use "Tools/primrec_package.ML"

    end

### Inductive sets

lemma myinv_f_f:

      inj f ==> myinv f (f x) = x

lemma f_myinv_f:

      [| inj f; y ∈ range f |] ==> f (myinv f y) = y

theorems basic_monos:

      A ⊆ A

      P --> P

      [| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0 ∨ P2.0 --> Q1.0 ∨ Q2.0

      [| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0 ∧ P2.0 --> Q1.0 ∧ Q2.0

      (!!x. P x --> Q x) ==> (∃x. P x) --> (∃x. Q x)

      (!!x. P x --> Q x) ==> (∀x. P x) --> (∀x. Q x)

      (if Q then x else y) = ((Q --> x) ∧ (¬ Q --> y))

      (!!x. P x --> Q x) ==> Collect P ⊆ Collect Q

      A ⊆ B ==> x ∈ A --> x ∈ B

      A ⊆ B ==> f -` A ⊆ f -` B

      (P --> Q) = (¬ P ∨ Q)

      (¬ ¬ P) = P

      (¬ (P ∨ Q)) = (¬ P ∧ ¬ Q)

      (¬ (P ∧ Q)) = (¬ P ∨ ¬ Q)

      (¬ (∀x. P x)) = (∃x. ¬ P x)

      (¬ (∃x. P x)) = (∀x. ¬ P x)

      Ball A P == ∀x. x ∈ A --> P x

      Bex A P == ∃x. x ∈ A ∧ P x

      ??.HOL.induct_forall P == ∀x. P x

      ??.HOL.induct_implies A B == A --> B

      ??.HOL.induct_equal x y == x = y

      ??.HOL.induct_conj A B == A ∧ B

theorems basic_monos:

      A ⊆ A

      P --> P

      [| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0 ∨ P2.0 --> Q1.0 ∨ Q2.0

      [| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0 ∧ P2.0 --> Q1.0 ∧ Q2.0

      (!!x. P x --> Q x) ==> (∃x. P x) --> (∃x. Q x)

      (!!x. P x --> Q x) ==> (∀x. P x) --> (∀x. Q x)

      (if Q then x else y) = ((Q --> x) ∧ (¬ Q --> y))

      (!!x. P x --> Q x) ==> Collect P ⊆ Collect Q

      A ⊆ B ==> x ∈ A --> x ∈ B

      A ⊆ B ==> f -` A ⊆ f -` B

      (P --> Q) = (¬ P ∨ Q)

      (¬ ¬ P) = P

      (¬ (P ∨ Q)) = (¬ P ∧ ¬ Q)

      (¬ (P ∧ Q)) = (¬ P ∨ ¬ Q)

      (¬ (∀x. P x)) = (∃x. ¬ P x)

      (¬ (∃x. P x)) = (∀x. ¬ P x)

      Ball A P == ∀x. x ∈ A --> P x

      Bex A P == ∃x. x ∈ A ∧ P x

      ??.HOL.induct_forall P == ∀x. P x

      ??.HOL.induct_implies A B == A --> B

      ??.HOL.induct_equal x y == x = y

      ??.HOL.induct_conj A B == A ∧ B

### Inductive datatypes and primitive recursion