isabelle: src/HOL/Relation.ML@7b2958d3d575 (annotated)

1128 64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ. nipkow parents: diff changeset	1
12905 bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	2	(* legacy ML bindings *)
1985 84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take paulson parents: 1842 diff changeset	3
12905 bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	4	val DomainE = thm "DomainE";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	5	val DomainI = thm "DomainI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	6	val Domain_Collect_split = thm "Domain_Collect_split";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	7	val Domain_Diff_subset = thm "Domain_Diff_subset";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	8	val Domain_Id = thm "Domain_Id";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	9	val Domain_Int_subset = thm "Domain_Int_subset";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	10	val Domain_Un_eq = thm "Domain_Un_eq";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	11	val Domain_Union = thm "Domain_Union";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	12	val Domain_def = thm "Domain_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	13	val Domain_diag = thm "Domain_diag";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	14	val Domain_empty = thm "Domain_empty";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	15	val Domain_iff = thm "Domain_iff";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	16	val Domain_insert = thm "Domain_insert";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	17	val Domain_mono = thm "Domain_mono";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	18	val Field_def = thm "Field_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	19	val IdE = thm "IdE";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	20	val IdI = thm "IdI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	21	val Id_O_R = thm "Id_O_R";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	22	val Id_def = thm "Id_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	23	val ImageE = thm "ImageE";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	24	val ImageI = thm "ImageI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	25	val Image_Collect_split = thm "Image_Collect_split";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	26	val Image_INT_subset = thm "Image_INT_subset";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	27	val Image_Id = thm "Image_Id";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	28	val Image_Int_subset = thm "Image_Int_subset";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	29	val Image_UN = thm "Image_UN";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	30	val Image_Un = thm "Image_Un";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	31	val Image_def = thm "Image_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	32	val Image_diag = thm "Image_diag";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	33	val Image_empty = thm "Image_empty";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	34	val Image_eq_UN = thm "Image_eq_UN";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	35	val Image_iff = thm "Image_iff";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	36	val Image_mono = thm "Image_mono";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	37	val Image_singleton = thm "Image_singleton";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	38	val Image_singleton_iff = thm "Image_singleton_iff";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	39	val Image_subset = thm "Image_subset";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	40	val Image_subset_eq = thm "Image_subset_eq";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	41	val O_assoc = thm "O_assoc";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	42	val R_O_Id = thm "R_O_Id";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	43	val RangeE = thm "RangeE";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	44	val RangeI = thm "RangeI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	45	val Range_Collect_split = thm "Range_Collect_split";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	46	val Range_Diff_subset = thm "Range_Diff_subset";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	47	val Range_Id = thm "Range_Id";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	48	val Range_Int_subset = thm "Range_Int_subset";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	49	val Range_Un_eq = thm "Range_Un_eq";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	50	val Range_Union = thm "Range_Union";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	51	val Range_def = thm "Range_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	52	val Range_diag = thm "Range_diag";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	53	val Range_empty = thm "Range_empty";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	54	val Range_iff = thm "Range_iff";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	55	val Range_insert = thm "Range_insert";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	56	val antisymD = thm "antisymD";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	57	val antisymI = thm "antisymI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	58	val antisym_Id = thm "antisym_Id";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	59	val antisym_converse = thm "antisym_converse";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	60	val antisym_def = thm "antisym_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	61	val converseD = thm "converseD";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	62	val converseE = thm "converseE";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	63	val converseI = thm "converseI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	64	val converse_Id = thm "converse_Id";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	65	val converse_converse = thm "converse_converse";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	66	val converse_def = thm "converse_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	67	val converse_diag = thm "converse_diag";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	68	val converse_iff = thm "converse_iff";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	69	val converse_rel_comp = thm "converse_rel_comp";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	70	val diagE = thm "diagE";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	71	val diagI = thm "diagI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	72	val diag_def = thm "diag_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	73	val diag_eqI = thm "diag_eqI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	74	val diag_iff = thm "diag_iff";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	75	val diag_subset_Times = thm "diag_subset_Times";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	76	val inv_image_def = thm "inv_image_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	77	val pair_in_Id_conv = thm "pair_in_Id_conv";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	78	val reflD = thm "reflD";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	79	val reflI = thm "reflI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	80	val refl_converse = thm "refl_converse";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	81	val refl_def = thm "refl_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	82	val reflexive_Id = thm "reflexive_Id";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	83	val rel_compE = thm "rel_compE";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	84	val rel_compEpair = thm "rel_compEpair";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	85	val rel_compI = thm "rel_compI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	86	val rel_comp_def = thm "rel_comp_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	87	val rel_comp_mono = thm "rel_comp_mono";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	88	val rel_comp_subset_Sigma = thm "rel_comp_subset_Sigma";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	89	val rev_ImageI = thm "rev_ImageI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	90	val single_valuedD = thm "single_valuedD";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	91	val single_valuedI = thm "single_valuedI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	92	val single_valued_def = thm "single_valued_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	93	val sym_def = thm "sym_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	94	val transD = thm "transD";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	95	val transI = thm "transI";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	96	val trans_Id = thm "trans_Id";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	97	val trans_O_subset = thm "trans_O_subset";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	98	val trans_converse = thm "trans_converse";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	99	val trans_def = thm "trans_def";
bbbae3f359e6 Converted to new theory format. berghofe parents: 12487 diff changeset	100	val trans_inv_image = thm "trans_inv_image";

author	wenzelm
	Tue, 25 Jul 2006 23:17:41 +0200
changeset 20205	7b2958d3d575
parent 13639	8ee6ea6627e1
permissions	-rw-r--r--