isabelle: src/HOL/Inductive.thy@d982f98e0f0d (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")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	12	("Tools/datatype_aux.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	13	("Tools/datatype_prop.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	14	("Tools/datatype_rep_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	15	("Tools/datatype_abs_proofs.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	16	("Tools/datatype_package.ML")
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	17	("Tools/primrec_package.ML"):
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	18
10727 2ccafccb81c0 added inductive_conj; wenzelm parents: 10434 diff changeset	19
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	20	subsection {* Inductive sets *}
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	21
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	22	text {* Inversion of injective functions. *}
11436 3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	23
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	24	constdefs
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	25	myinv :: "('a => 'b) => ('b => 'a)"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	26	"myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	27
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	28	lemma myinv_f_f: "inj f ==> myinv f (f x) = x"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	29	proof -
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	30	assume "inj f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	31	hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	32	by (simp only: inj_eq)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	33	also have "... = x" by (rule the_eq_trivial)
11439 9aaab1a160a5 tuned; wenzelm parents: 11436 diff changeset	34	finally show ?thesis by (unfold myinv_def)
11436 3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	35	qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	36
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	37	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	38	proof (unfold myinv_def)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	39	assume inj: "inj f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	40	assume "y \<in> range f"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	41	then obtain x where "y = f x" ..
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	42	hence x: "f x = y" ..
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	43	thus "f (THE x. f x = y) = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	44	proof (rule theI)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	45	fix x' assume "f x' = y"
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	46	with x have "f x' = f x" by simp
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	47	with inj show "x' = x" by (rule injD)
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	48	qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	49	qed
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	50
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	51	hide const myinv
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	52
3f74b80d979f private "myinv" (uses "The" instead of "Eps"); wenzelm parents: 11325 diff changeset	53
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	54	text {* Package setup. *}
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	55
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	56	use "Tools/inductive_package.ML"
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	57	setup InductivePackage.setup
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	58
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	59	theorems basic_monos [mono] =
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	60	subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	61	Collect_mono in_mono vimage_mono
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	62	imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	63	not_all not_ex
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	64	Ball_def Bex_def
11990 c1daefc08eff use induct_rulify2; wenzelm parents: 11825 diff changeset	65	induct_rulify2
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	66
56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	67
12023 d982f98e0f0d tuned; wenzelm parents: 11990 diff changeset	68	subsection {* Inductive datatypes and primitive recursion *}
11688 56833637db2a generic induct_method.ML; wenzelm parents: 11439 diff changeset	69
11825 ef7d619e2c88 moved InductMethod.setup to theory HOL; wenzelm parents: 11688 diff changeset	70	text {* Package setup. *}
ef7d619e2c88 moved InductMethod.setup to theory HOL; wenzelm parents: 11688 diff changeset	71
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	72	use "Tools/datatype_aux.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	73	use "Tools/datatype_prop.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	74	use "Tools/datatype_rep_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	75	use "Tools/datatype_abs_proofs.ML"
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	76	use "Tools/datatype_package.ML"
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	77	setup DatatypePackage.setup
10402 5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	78
5e82d6cafb5f inductive_atomize, inductive_rulify; wenzelm parents: 10312 diff changeset	79	use "Tools/primrec_package.ML"
8482 bbc805ebc904 Added setup for primrec theory data. berghofe parents: 8343 diff changeset	80	setup PrimrecPackage.setup
7700 38b6d2643630 load / setup datatype package; wenzelm parents: 7357 diff changeset	81
6437 9bdfe07ba8e9 'HOL/inductive' theory data; wenzelm parents: 5105 diff changeset	82	end

author	wenzelm
	Sat, 03 Nov 2001 01:33:54 +0100
changeset 12023	d982f98e0f0d
parent 11990	c1daefc08eff
child 12437	6d4e02b6dd43
permissions	-rw-r--r--