isabelle: src/HOL/Inductive.thy@210b326a03c9 (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
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	4	*)
10727 2ccafccb81c0 added inductive_conj; wenzelm parents: 10434 diff changeset	5
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	6	header {* Support for inductive sets and types *}
1187 bc94f00e47ba Includes Sum.thy as a parent for mutual recursion lcp parents: 923 diff changeset	7
15131 c69542757a4d New theory header syntax. nipkow parents: 14981 diff changeset	8	theory Inductive
17009 932e0e370926 import FixedPoint instead of Gfp avigad parents: 16417 diff changeset	9	imports FixedPoint Sum_Type Relation Record
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 15140 diff changeset	10	uses
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	11	("Tools/inductive_package.ML")
13705 934d6c1421f2 Added InductiveRealizer package. berghofe parents: 13469 diff changeset	12	("Tools/inductive_realizer.ML")
12437 6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	13	("Tools/inductive_codegen.ML")
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	14	("Tools/datatype_aux.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	15	("Tools/datatype_prop.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	16	("Tools/datatype_rep_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	17	("Tools/datatype_abs_proofs.ML")
13469 70d8dfef587d Added file Tools/datatype_realizer.ML berghofe parents: 12920 diff changeset	18	("Tools/datatype_realizer.ML")
19599 a5c7eb37d14f added DatatypeHooks haftmann parents: 18456 diff changeset	19	("Tools/datatype_hooks.ML")
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	20	("Tools/datatype_package.ML")
12437 6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	21	("Tools/datatype_codegen.ML")
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	22	("Tools/recfun_codegen.ML")
15131 c69542757a4d New theory header syntax. nipkow parents: 14981 diff changeset	23	("Tools/primrec_package.ML")
c69542757a4d New theory header syntax. nipkow parents: 14981 diff changeset	24	begin
10727 2ccafccb81c0 added inductive_conj; wenzelm parents: 10434 diff changeset	25
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	26	subsection {* Inductive sets *}
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	27
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	28	text {* Inversion of injective functions. *}
11436 3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	29
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	30	constdefs
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	31	myinv :: "('a => 'b) => ('b => 'a)"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	32	"myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	33
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	34	lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	35	proof -
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	36	assume "inj f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	37	hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	38	by (simp only: inj_eq)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	39	also have "... = x" by (rule the_eq_trivial)
11439 9aaab1a160a5 tuned; wenzelm parents: 11436 diff changeset	40	finally show ?thesis by (unfold myinv_def)
11436 3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	41	qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	42
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	43	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	44	proof (unfold myinv_def)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	45	assume inj: "inj f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	46	assume "y \<in> range f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	47	then obtain x where "y = f x" ..
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	48	hence x: "f x = y" ..
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	49	thus "f (THE x. f x = y) = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	50	proof (rule theI)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	51	fix x' assume "f x' = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	52	with x have "f x' = f x" by simp
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	53	with inj show "x' = x" by (rule injD)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	54	qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	55	qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	56
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	57	hide const myinv
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	58
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	59
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	60	text {* Package setup. *}
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	61
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	62	use "Tools/inductive_package.ML"
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	63	setup InductivePackage.setup
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	64
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	65	theorems basic_monos [mono] =
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	66	subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	67	Collect_mono in_mono vimage_mono
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	68	imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	69	not_all not_ex
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	70	Ball_def Bex_def
18456 8cc35e95450a updated auxiliary facts for induct method; wenzelm parents: 17009 diff changeset	71	induct_rulify_fallback
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	72
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	73
12023 d982f98e0f0d tuned; wenzelm parents: 11990 diff changeset	74	subsection {* Inductive datatypes and primitive recursion *}
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	75
11825 ef7d619e2c88 moved InductMethod.setup to theory HOL; wenzelm parents: 11688 diff changeset	76	text {* Package setup. *}
ef7d619e2c88 moved InductMethod.setup to theory HOL; wenzelm parents: 11688 diff changeset	77
12437 6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	78	use "Tools/recfun_codegen.ML"
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	79	setup RecfunCodegen.setup
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	80
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	81	use "Tools/datatype_aux.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	82	use "Tools/datatype_prop.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	83	use "Tools/datatype_rep_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	84	use "Tools/datatype_abs_proofs.ML"
13469 70d8dfef587d Added file Tools/datatype_realizer.ML berghofe parents: 12920 diff changeset	85	use "Tools/datatype_realizer.ML"
19599 a5c7eb37d14f added DatatypeHooks haftmann parents: 18456 diff changeset	86
a5c7eb37d14f added DatatypeHooks haftmann parents: 18456 diff changeset	87	use "Tools/datatype_hooks.ML"
a5c7eb37d14f added DatatypeHooks haftmann parents: 18456 diff changeset	88	setup DatatypeHooks.setup
a5c7eb37d14f added DatatypeHooks haftmann parents: 18456 diff changeset	89
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	90	use "Tools/datatype_package.ML"
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	91	setup DatatypePackage.setup
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	92
12437 6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	93	use "Tools/datatype_codegen.ML"
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	94	setup DatatypeCodegen.setup
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	95
13705 934d6c1421f2 Added InductiveRealizer package. berghofe parents: 13469 diff changeset	96	use "Tools/inductive_realizer.ML"
934d6c1421f2 Added InductiveRealizer package. berghofe parents: 13469 diff changeset	97	setup InductiveRealizer.setup
934d6c1421f2 Added InductiveRealizer package. berghofe parents: 13469 diff changeset	98
12437 6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	99	use "Tools/inductive_codegen.ML"
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	100	setup InductiveCodegen.setup
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive. berghofe parents: 12023 diff changeset	101
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	102	use "Tools/primrec_package.ML"
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	103
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	104	end

author	haftmann
	Mon, 04 Sep 2006 13:55:32 +0200
changeset 20467	210b326a03c9
parent 19599	a5c7eb37d14f
child 20604	9dba9c7872c9
permissions	-rw-r--r--