--- a/src/HOL/ATP_Linkup.thy Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy Wed Jan 21 23:40:23 2009 +0100
@@ -7,7 +7,7 @@
header {* The Isabelle-ATP Linkup *}
theory ATP_Linkup
-imports Record Hilbert_Choice
+imports Divides Record Hilbert_Choice
uses
"Tools/polyhash.ML"
"Tools/res_clause.ML"
--- a/src/HOL/Datatype.thy Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Datatype.thy Wed Jan 21 23:40:23 2009 +0100
@@ -8,7 +8,7 @@
header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
theory Datatype
-imports Nat Relation
+imports Nat Product_Type
begin
typedef (Node)
@@ -509,15 +509,6 @@
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
-(*** Domain ***)
-
-lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
-by auto
-
-lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
-by auto
-
-
text {* hides popular names *}
hide (open) type node item
hide (open) const Push Node Atom Leaf Numb Lim Split Case
--- a/src/HOL/Finite_Set.thy Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Finite_Set.thy Wed Jan 21 23:40:23 2009 +0100
@@ -6,7 +6,7 @@
header {* Finite sets *}
theory Finite_Set
-imports Datatype Divides Transitive_Closure
+imports Nat Product_Type Power
begin
subsection {* Definition and basic properties *}
@@ -380,46 +380,6 @@
by(blast intro: finite_subset[OF subset_Pow_Union])
-lemma finite_converse [iff]: "finite (r^-1) = finite r"
- apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
- apply simp
- apply (rule iffI)
- apply (erule finite_imageD [unfolded inj_on_def])
- apply (simp split add: split_split)
- apply (erule finite_imageI)
- apply (simp add: converse_def image_def, auto)
- apply (rule bexI)
- prefer 2 apply assumption
- apply simp
- done
-
-
-text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
-Ehmety) *}
-
-lemma finite_Field: "finite r ==> finite (Field r)"
- -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
- apply (induct set: finite)
- apply (auto simp add: Field_def Domain_insert Range_insert)
- done
-
-lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
- apply clarify
- apply (erule trancl_induct)
- apply (auto simp add: Field_def)
- done
-
-lemma finite_trancl: "finite (r^+) = finite r"
- apply auto
- prefer 2
- apply (rule trancl_subset_Field2 [THEN finite_subset])
- apply (rule finite_SigmaI)
- prefer 3
- apply (blast intro: r_into_trancl' finite_subset)
- apply (auto simp add: finite_Field)
- done
-
-
subsection {* Class @{text finite} *}
setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
@@ -471,9 +431,6 @@
instance "+" :: (finite, finite) finite
by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
-instance option :: (finite) finite
- by default (simp add: insert_None_conv_UNIV [symmetric])
-
subsection {* A fold functional for finite sets *}
--- a/src/HOL/Plain.thy Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Plain.thy Wed Jan 21 23:40:23 2009 +0100
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Record SAT Extraction
+imports Datatype FunDef Record SAT Extraction Divides
begin
text {*
@@ -9,6 +9,9 @@
include @{text Hilbert_Choice}.
*}
+instance option :: (finite) finite
+ by default (simp add: insert_None_conv_UNIV [symmetric])
+
ML {* path_add "~~/src/HOL/Library" *}
end
--- a/src/HOL/Relation.thy Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Relation.thy Wed Jan 21 23:40:23 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Relation.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
*)
@@ -7,7 +6,7 @@
header {* Relations *}
theory Relation
-imports Product_Type
+imports Datatype Finite_Set
begin
subsection {* Definitions *}
@@ -379,6 +378,12 @@
lemma fst_eq_Domain: "fst ` R = Domain R";
by (auto intro!:image_eqI)
+lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
+by auto
+
+lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
+by auto
+
subsection {* Range *}
@@ -566,6 +571,31 @@
done
+subsection {* Finiteness *}
+
+lemma finite_converse [iff]: "finite (r^-1) = finite r"
+ apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
+ apply simp
+ apply (rule iffI)
+ apply (erule finite_imageD [unfolded inj_on_def])
+ apply (simp split add: split_split)
+ apply (erule finite_imageI)
+ apply (simp add: converse_def image_def, auto)
+ apply (rule bexI)
+ prefer 2 apply assumption
+ apply simp
+ done
+
+text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
+Ehmety) *}
+
+lemma finite_Field: "finite r ==> finite (Field r)"
+ -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
+ apply (induct set: finite)
+ apply (auto simp add: Field_def Domain_insert Range_insert)
+ done
+
+
subsection {* Version of @{text lfp_induct} for binary relations *}
lemmas lfp_induct2 =
--- a/src/HOL/Transitive_Closure.thy Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy Wed Jan 21 23:40:23 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Transitive_Closure.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
@@ -568,6 +567,22 @@
apply auto
done
+lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
+ apply clarify
+ apply (erule trancl_induct)
+ apply (auto simp add: Field_def)
+ done
+
+lemma finite_trancl: "finite (r^+) = finite r"
+ apply auto
+ prefer 2
+ apply (rule trancl_subset_Field2 [THEN finite_subset])
+ apply (rule finite_SigmaI)
+ prefer 3
+ apply (blast intro: r_into_trancl' finite_subset)
+ apply (auto simp add: finite_Field)
+ done
+
text {* More about converse @{text rtrancl} and @{text trancl}, should
be merged with main body. *}
--- a/src/HOL/Wellfounded.thy Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Wellfounded.thy Wed Jan 21 23:40:23 2009 +0100
@@ -7,7 +7,7 @@
header {*Well-founded Recursion*}
theory Wellfounded
-imports Finite_Set Nat
+imports Finite_Set Transitive_Closure Nat
uses ("Tools/function_package/size.ML")
begin