Up to index of Isabelle/HOL
theory Inductive(* 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
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