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:

  AA
  P --> P
  [| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0P2.0 --> Q1.0Q2.0
  [| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0P2.0 --> Q1.0Q2.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
  AB ==> xA --> xB
  AB ==> f -` Af -` B
  (P --> Q) = (¬ PQ)
  (¬ ¬ P) = P
  (¬ (PQ)) = (¬ P ∧ ¬ Q)
  (¬ (PQ)) = (¬ P ∨ ¬ Q)
  (¬ (∀x. P x)) = (∃x. ¬ P x)
  (¬ (∃x. P x)) = (∀x. ¬ P x)
  Ball A P == ∀x. xA --> P x
  Bex A P == ∃x. xAP 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 == AB

theorems basic_monos:

  AA
  P --> P
  [| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0P2.0 --> Q1.0Q2.0
  [| P1.0 --> Q1.0; P2.0 --> Q2.0 |] ==> P1.0P2.0 --> Q1.0Q2.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
  AB ==> xA --> xB
  AB ==> f -` Af -` B
  (P --> Q) = (¬ PQ)
  (¬ ¬ P) = P
  (¬ (PQ)) = (¬ P ∧ ¬ Q)
  (¬ (PQ)) = (¬ P ∨ ¬ Q)
  (¬ (∀x. P x)) = (∃x. ¬ P x)
  (¬ (∃x. P x)) = (∀x. ¬ P x)
  Ball A P == ∀x. xA --> P x
  Bex A P == ∃x. xAP 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 == AB

Inductive datatypes and primitive recursion