isabelle: src/HOL/Inductive.thy@5c900a821a7c (annotated)

7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	1	(* Title: HOL/Inductive.thy
38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	2	ID: $Id$
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	3	Author: Markus Wenzel, TU Muenchen
10727 2ccafccb81c0 added inductive_conj; wenzelm parents: 10434 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	5	*)
10727 2ccafccb81c0 added inductive_conj; wenzelm parents: 10434 diff changeset	6
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	7	header {* Support for inductive sets and types *}
1187 bc94f00e47ba Includes Sum.thy as a parent for mutual recursion lcp parents: 923 diff changeset	8
11325 a5e0289dd56c Inductive definitions are now introduced earlier in the theory hierarchy. berghofe parents: 11003 diff changeset	9	theory Inductive = Gfp + Sum_Type + Relation
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	10	files
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	11	("Tools/inductive_package.ML")
12437 6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	12	("Tools/inductive_codegen.ML")
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	13	("Tools/datatype_aux.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	14	("Tools/datatype_prop.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	15	("Tools/datatype_rep_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	16	("Tools/datatype_abs_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	17	("Tools/datatype_package.ML")
12437 6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	18	("Tools/datatype_codegen.ML")
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	19	("Tools/recfun_codegen.ML")
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	20	("Tools/primrec_package.ML"):
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	21
10727 2ccafccb81c0 added inductive_conj; wenzelm parents: 10434 diff changeset	22
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	23	subsection {* Inductive sets *}
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	24
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	25	text {* Inversion of injective functions. *}
11436 3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	26
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	27	constdefs
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	28	myinv :: "('a => 'b) => ('b => 'a)"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	29	"myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	30
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	31	lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	32	proof -
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	33	assume "inj f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	34	hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	35	by (simp only: inj_eq)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	36	also have "... = x" by (rule the_eq_trivial)
11439 9aaab1a160a5 tuned; wenzelm parents: 11436 diff changeset	37	finally show ?thesis by (unfold myinv_def)
11436 3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	38	qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	39
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	40	lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	41	proof (unfold myinv_def)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	42	assume inj: "inj f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	43	assume "y \<in> range f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	44	then obtain x where "y = f x" ..
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	45	hence x: "f x = y" ..
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	46	thus "f (THE x. f x = y) = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	47	proof (rule theI)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	48	fix x' assume "f x' = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	49	with x have "f x' = f x" by simp
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	50	with inj show "x' = x" by (rule injD)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	51	qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	52	qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	53
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	54	hide const myinv
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	55
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	56
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	57	text {* Package setup. *}
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	58
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	59	use "Tools/inductive_package.ML"
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	60	setup InductivePackage.setup
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	61
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	62	theorems basic_monos [mono] =
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	63	subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	64	Collect_mono in_mono vimage_mono
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	65	imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	66	not_all not_ex
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	67	Ball_def Bex_def
11990 c1daefc08eff use induct_rulify2; wenzelm parents: 11825 diff changeset	68	induct_rulify2
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	69
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	70
12023 d982f98e0f0d tuned; wenzelm parents: 11990 diff changeset	71	subsection {* Inductive datatypes and primitive recursion *}
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	72
11825 ef7d619e2c88 moved InductMethod.setup to theory HOL; wenzelm parents: 11688 diff changeset	73	text {* Package setup. *}
ef7d619e2c88 moved InductMethod.setup to theory HOL; wenzelm parents: 11688 diff changeset	74
12437 6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	75	use "Tools/recfun_codegen.ML"
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	76	setup RecfunCodegen.setup
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	77
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	78	use "Tools/datatype_aux.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	79	use "Tools/datatype_prop.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	80	use "Tools/datatype_rep_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	81	use "Tools/datatype_abs_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	82	use "Tools/datatype_package.ML"
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	83	setup DatatypePackage.setup
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	84
12437 6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	85	use "Tools/datatype_codegen.ML"
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	86	setup DatatypeCodegen.setup
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	87
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	88	use "Tools/inductive_codegen.ML"
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	89	setup InductiveCodegen.setup
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	90
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	91	use "Tools/primrec_package.ML"
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	92
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	93	end

author	paulson
	Mon, 04 Feb 2002 13:16:54 +0100
changeset 12867	5c900a821a7c
parent 12437	6d4e02b6dd43
child 12920	32292d83367b
permissions	-rw-r--r--