changed import hierarchy
authorhaftmann
Wed Jan 21 23:40:23 2009 +0100 (2009-01-21)
changeset 29609a010aab5bed0
parent 29608 564ea783ace8
child 29610 83d282f12352
changed import hierarchy
src/HOL/ATP_Linkup.thy
src/HOL/Datatype.thy
src/HOL/Finite_Set.thy
src/HOL/Plain.thy
src/HOL/Relation.thy
src/HOL/Transitive_Closure.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/ATP_Linkup.thy	Wed Jan 21 23:40:23 2009 +0100
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Wed Jan 21 23:40:23 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* The Isabelle-ATP Linkup *}
     1.5  
     1.6  theory ATP_Linkup
     1.7 -imports Record Hilbert_Choice
     1.8 +imports Divides Record Hilbert_Choice
     1.9  uses
    1.10    "Tools/polyhash.ML"
    1.11    "Tools/res_clause.ML"
     2.1 --- a/src/HOL/Datatype.thy	Wed Jan 21 23:40:23 2009 +0100
     2.2 +++ b/src/HOL/Datatype.thy	Wed Jan 21 23:40:23 2009 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     2.5  
     2.6  theory Datatype
     2.7 -imports Nat Relation
     2.8 +imports Nat Product_Type
     2.9  begin
    2.10  
    2.11  typedef (Node)
    2.12 @@ -509,15 +509,6 @@
    2.13  lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
    2.14  
    2.15  
    2.16 -(*** Domain ***)
    2.17 -
    2.18 -lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
    2.19 -by auto
    2.20 -
    2.21 -lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
    2.22 -by auto
    2.23 -
    2.24 -
    2.25  text {* hides popular names *}
    2.26  hide (open) type node item
    2.27  hide (open) const Push Node Atom Leaf Numb Lim Split Case
     3.1 --- a/src/HOL/Finite_Set.thy	Wed Jan 21 23:40:23 2009 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Wed Jan 21 23:40:23 2009 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Finite sets *}
     3.5  
     3.6  theory Finite_Set
     3.7 -imports Datatype Divides Transitive_Closure
     3.8 +imports Nat Product_Type Power
     3.9  begin
    3.10  
    3.11  subsection {* Definition and basic properties *}
    3.12 @@ -380,46 +380,6 @@
    3.13  by(blast intro: finite_subset[OF subset_Pow_Union])
    3.14  
    3.15  
    3.16 -lemma finite_converse [iff]: "finite (r^-1) = finite r"
    3.17 -  apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
    3.18 -   apply simp
    3.19 -   apply (rule iffI)
    3.20 -    apply (erule finite_imageD [unfolded inj_on_def])
    3.21 -    apply (simp split add: split_split)
    3.22 -   apply (erule finite_imageI)
    3.23 -  apply (simp add: converse_def image_def, auto)
    3.24 -  apply (rule bexI)
    3.25 -   prefer 2 apply assumption
    3.26 -  apply simp
    3.27 -  done
    3.28 -
    3.29 -
    3.30 -text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
    3.31 -Ehmety) *}
    3.32 -
    3.33 -lemma finite_Field: "finite r ==> finite (Field r)"
    3.34 -  -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
    3.35 -  apply (induct set: finite)
    3.36 -   apply (auto simp add: Field_def Domain_insert Range_insert)
    3.37 -  done
    3.38 -
    3.39 -lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
    3.40 -  apply clarify
    3.41 -  apply (erule trancl_induct)
    3.42 -   apply (auto simp add: Field_def)
    3.43 -  done
    3.44 -
    3.45 -lemma finite_trancl: "finite (r^+) = finite r"
    3.46 -  apply auto
    3.47 -   prefer 2
    3.48 -   apply (rule trancl_subset_Field2 [THEN finite_subset])
    3.49 -   apply (rule finite_SigmaI)
    3.50 -    prefer 3
    3.51 -    apply (blast intro: r_into_trancl' finite_subset)
    3.52 -   apply (auto simp add: finite_Field)
    3.53 -  done
    3.54 -
    3.55 -
    3.56  subsection {* Class @{text finite}  *}
    3.57  
    3.58  setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
    3.59 @@ -471,9 +431,6 @@
    3.60  instance "+" :: (finite, finite) finite
    3.61    by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    3.62  
    3.63 -instance option :: (finite) finite
    3.64 -  by default (simp add: insert_None_conv_UNIV [symmetric])
    3.65 -
    3.66  
    3.67  subsection {* A fold functional for finite sets *}
    3.68  
     4.1 --- a/src/HOL/Plain.thy	Wed Jan 21 23:40:23 2009 +0100
     4.2 +++ b/src/HOL/Plain.thy	Wed Jan 21 23:40:23 2009 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  header {* Plain HOL *}
     4.5  
     4.6  theory Plain
     4.7 -imports Datatype FunDef Record SAT Extraction
     4.8 +imports Datatype FunDef Record SAT Extraction Divides
     4.9  begin
    4.10  
    4.11  text {*
    4.12 @@ -9,6 +9,9 @@
    4.13    include @{text Hilbert_Choice}.
    4.14  *}
    4.15  
    4.16 +instance option :: (finite) finite
    4.17 +  by default (simp add: insert_None_conv_UNIV [symmetric])
    4.18 +
    4.19  ML {* path_add "~~/src/HOL/Library" *}
    4.20  
    4.21  end
     5.1 --- a/src/HOL/Relation.thy	Wed Jan 21 23:40:23 2009 +0100
     5.2 +++ b/src/HOL/Relation.thy	Wed Jan 21 23:40:23 2009 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Relation.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7      Copyright   1996  University of Cambridge
     5.8  *)
     5.9 @@ -7,7 +6,7 @@
    5.10  header {* Relations *}
    5.11  
    5.12  theory Relation
    5.13 -imports Product_Type
    5.14 +imports Datatype Finite_Set
    5.15  begin
    5.16  
    5.17  subsection {* Definitions *}
    5.18 @@ -379,6 +378,12 @@
    5.19  lemma fst_eq_Domain: "fst ` R = Domain R";
    5.20  by (auto intro!:image_eqI)
    5.21  
    5.22 +lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
    5.23 +by auto
    5.24 +
    5.25 +lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
    5.26 +by auto
    5.27 +
    5.28  
    5.29  subsection {* Range *}
    5.30  
    5.31 @@ -566,6 +571,31 @@
    5.32    done
    5.33  
    5.34  
    5.35 +subsection {* Finiteness *}
    5.36 +
    5.37 +lemma finite_converse [iff]: "finite (r^-1) = finite r"
    5.38 +  apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
    5.39 +   apply simp
    5.40 +   apply (rule iffI)
    5.41 +    apply (erule finite_imageD [unfolded inj_on_def])
    5.42 +    apply (simp split add: split_split)
    5.43 +   apply (erule finite_imageI)
    5.44 +  apply (simp add: converse_def image_def, auto)
    5.45 +  apply (rule bexI)
    5.46 +   prefer 2 apply assumption
    5.47 +  apply simp
    5.48 +  done
    5.49 +
    5.50 +text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
    5.51 +Ehmety) *}
    5.52 +
    5.53 +lemma finite_Field: "finite r ==> finite (Field r)"
    5.54 +  -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
    5.55 +  apply (induct set: finite)
    5.56 +   apply (auto simp add: Field_def Domain_insert Range_insert)
    5.57 +  done
    5.58 +
    5.59 +
    5.60  subsection {* Version of @{text lfp_induct} for binary relations *}
    5.61  
    5.62  lemmas lfp_induct2 = 
     6.1 --- a/src/HOL/Transitive_Closure.thy	Wed Jan 21 23:40:23 2009 +0100
     6.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Jan 21 23:40:23 2009 +0100
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      HOL/Transitive_Closure.thy
     6.5 -    ID:         $Id$
     6.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7      Copyright   1992  University of Cambridge
     6.8  *)
     6.9 @@ -568,6 +567,22 @@
    6.10     apply auto
    6.11    done
    6.12  
    6.13 +lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
    6.14 +  apply clarify
    6.15 +  apply (erule trancl_induct)
    6.16 +   apply (auto simp add: Field_def)
    6.17 +  done
    6.18 +
    6.19 +lemma finite_trancl: "finite (r^+) = finite r"
    6.20 +  apply auto
    6.21 +   prefer 2
    6.22 +   apply (rule trancl_subset_Field2 [THEN finite_subset])
    6.23 +   apply (rule finite_SigmaI)
    6.24 +    prefer 3
    6.25 +    apply (blast intro: r_into_trancl' finite_subset)
    6.26 +   apply (auto simp add: finite_Field)
    6.27 +  done
    6.28 +
    6.29  text {* More about converse @{text rtrancl} and @{text trancl}, should
    6.30    be merged with main body. *}
    6.31  
     7.1 --- a/src/HOL/Wellfounded.thy	Wed Jan 21 23:40:23 2009 +0100
     7.2 +++ b/src/HOL/Wellfounded.thy	Wed Jan 21 23:40:23 2009 +0100
     7.3 @@ -7,7 +7,7 @@
     7.4  header {*Well-founded Recursion*}
     7.5  
     7.6  theory Wellfounded
     7.7 -imports Finite_Set Nat
     7.8 +imports Finite_Set Transitive_Closure Nat
     7.9  uses ("Tools/function_package/size.ML")
    7.10  begin
    7.11