# Theory Inductive

(*  Title:      ZF/Inductive.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Inductive definitions use least fixedpoints with standard products and sums
Coinductive definitions use greatest fixedpoints with Quine products and sums

Sums are used only for mutual recursion;
Products are used only to derive "streamlined" induction rules for relations
*)

sectionInductive and Coinductive Definitions

theory Inductive
imports Fixedpt QPair Nat
keywords
"inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
"domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
"elimination" "induction" "case_eqns" "recursor_eqns" :: quasi_command
begin

lemma def_swap_iff: "a  b  a = c  c = b"
by blast

lemma def_trans: "f  g  g(a) = b  f(a) = b"
by simp

lemma refl_thin: "P. a = a  P  P" .

ML_file ind_syntax.ML
ML_file Tools/ind_cases.ML
ML_file Tools/cartprod.ML
ML_file Tools/inductive_package.ML
ML_file Tools/induct_tacs.ML
ML_file Tools/primrec_package.ML

ML
structure Lfp =
struct
val oper      = Constlfp
val bnd_mono  = Constbnd_mono
val bnd_monoI = @{thm bnd_monoI}
val subs      = @{thm def_lfp_subset}
val Tarski    = @{thm def_lfp_unfold}
val induct    = @{thm def_induct}
end;

structure Standard_Prod =
struct
val sigma     = ConstSigma
val pair      = ConstPair
val split_name = const_namesplit
val pair_iff  = @{thm Pair_iff}
val split_eq  = @{thm split}
val fsplitI   = @{thm splitI}
val fsplitD   = @{thm splitD}
val fsplitE   = @{thm splitE}
end;

structure Standard_CP = CartProd_Fun (Standard_Prod);

structure Standard_Sum =
struct
val sum       = Constsum
val inl       = ConstInl
val inr       = ConstInr
val elim      = Constcase
val case_inl  = @{thm case_Inl}
val case_inr  = @{thm case_Inr}
val inl_iff   = @{thm Inl_iff}
val inr_iff   = @{thm Inr_iff}
val distinct  = @{thm Inl_Inr_iff}
val distinct' = @{thm Inr_Inl_iff}
val free_SEs  = Ind_Syntax.mk_free_SEs
[distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
end;

structure Ind_Package =
(structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
and Su=Standard_Sum val coind = false);

structure Gfp =
struct
val oper      = Constgfp
val bnd_mono  = Constbnd_mono
val bnd_monoI = @{thm bnd_monoI}
val subs      = @{thm def_gfp_subset}
val Tarski    = @{thm def_gfp_unfold}
val induct    = @{thm def_Collect_coinduct}
end;

structure Quine_Prod =
struct
val sigma     = ConstQSigma
val pair      = ConstQPair
val split_name = const_nameqsplit
val pair_iff  = @{thm QPair_iff}
val split_eq  = @{thm qsplit}
val fsplitI   = @{thm qsplitI}
val fsplitD   = @{thm qsplitD}
val fsplitE   = @{thm qsplitE}
end;

structure Quine_CP = CartProd_Fun (Quine_Prod);

structure Quine_Sum =
struct
val sum       = Constqsum
val inl       = ConstQInl
val inr       = ConstQInr
val elim      = Constqcase
val case_inl  = @{thm qcase_QInl}
val case_inr  = @{thm qcase_QInr}
val inl_iff   = @{thm QInl_iff}
val inr_iff   = @{thm QInr_iff}
val distinct  = @{thm QInl_QInr_iff}
val distinct' = @{thm QInr_QInl_iff}
val free_SEs  = Ind_Syntax.mk_free_SEs
[distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
end;

structure CoInd_Package =
Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
and Su=Quine_Sum val coind = true);

end