# HG changeset patch
# User haftmann
# Date 1232577623 -3600
# Node ID a010aab5bed03d5925052a27e214ea677b0f7f3a
# Parent  564ea783ace87fedcba4b65ca859b11fdd0c447a
changed import hierarchy

diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/ATP_Linkup.thy
--- 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"
diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/Datatype.thy
--- 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
diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/Finite_Set.thy
--- 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 *}
 
diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/Plain.thy
--- 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
diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/Relation.thy
--- 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 = 
diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/Transitive_Closure.thy
--- 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. *}
 
diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/Wellfounded.thy
--- 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