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

author	mengj
	Wed, 19 Oct 2005 10:25:46 +0200
changeset 17907	c20e4bddcb11
parent 17009	932e0e370926
child 18456	8cc35e95450a
permissions	-rw-r--r--