# HG changeset patch # User haftmann # Date 1260390830 -3600 # Node ID 3d2acb18f2f22dc6050694ac02d6fb9547f6f052 # Parent 7129fab1fe4fe06f379d14dcdda4d76f487b27ce# Parent 132d169bd6b79060ae674121ea29b6e8763711d2 merged diff -r 7129fab1fe4f -r 3d2acb18f2f2 src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Wed Dec 09 16:28:49 2009 +0100 +++ b/src/HOL/Library/Fset.thy Wed Dec 09 21:33:50 2009 +0100 @@ -16,6 +16,10 @@ primrec member :: "'a fset \ 'a set" where "member (Fset A) = A" +lemma member_inject [simp]: + "member A = member B \ A = B" + by (cases A, cases B) simp + lemma Fset_member [simp]: "Fset (member A) = A" by (cases A) simp @@ -53,6 +57,54 @@ qed +subsection {* Lattice instantiation *} + +instantiation fset :: (type) boolean_algebra +begin + +definition less_eq_fset :: "'a fset \ 'a fset \ bool" where + [simp]: "A \ B \ member A \ member B" + +definition less_fset :: "'a fset \ 'a fset \ bool" where + [simp]: "A < B \ member A \ member B" + +definition inf_fset :: "'a fset \ 'a fset \ 'a fset" where + [simp]: "inf A B = Fset (member A \ member B)" + +definition sup_fset :: "'a fset \ 'a fset \ 'a fset" where + [simp]: "sup A B = Fset (member A \ member B)" + +definition bot_fset :: "'a fset" where + [simp]: "bot = Fset {}" + +definition top_fset :: "'a fset" where + [simp]: "top = Fset UNIV" + +definition uminus_fset :: "'a fset \ 'a fset" where + [simp]: "- A = Fset (- (member A))" + +definition minus_fset :: "'a fset \ 'a fset \ 'a fset" where + [simp]: "A - B = Fset (member A - member B)" + +instance proof +qed auto + +end + +instantiation fset :: (type) complete_lattice +begin + +definition Inf_fset :: "'a fset set \ 'a fset" where + [simp, code del]: "Inf_fset As = Fset (Inf (image member As))" + +definition Sup_fset :: "'a fset set \ 'a fset" where + [simp, code del]: "Sup_fset As = Fset (Sup (image member As))" + +instance proof +qed (auto simp add: le_fun_def le_bool_def) + +end + subsection {* Basic operations *} definition is_empty :: "'a fset \ bool" where @@ -62,12 +114,13 @@ "is_empty (Set xs) \ null xs" by (simp add: is_empty_set) -definition empty :: "'a fset" where - [simp]: "empty = Fset {}" +lemma empty_Set [code]: + "bot = Set []" + by simp -lemma empty_Set [code]: - "empty = Set []" - by (simp add: Set_def) +lemma UNIV_Set [code]: + "top = Coset []" + by simp definition insert :: "'a \ 'a fset \ 'a fset" where [simp]: "insert x A = Fset (Set.insert x (member A))" @@ -127,112 +180,80 @@ subsection {* Derived operations *} -definition subfset_eq :: "'a fset \ 'a fset \ bool" where - [simp]: "subfset_eq A B \ member A \ member B" - lemma subfset_eq_forall [code]: - "subfset_eq A B \ forall (member B) A" + "A \ B \ forall (member B) A" by (simp add: subset_eq) -definition subfset :: "'a fset \ 'a fset \ bool" where - [simp]: "subfset A B \ member A \ member B" - lemma subfset_subfset_eq [code]: - "subfset A B \ subfset_eq A B \ \ subfset_eq B A" - by (simp add: subset) + "A < B \ A \ B \ \ B \ (A :: 'a fset)" + by (fact less_le_not_le) lemma eq_fset_subfset_eq [code]: - "eq_class.eq A B \ subfset_eq A B \ subfset_eq B A" + "eq_class.eq A B \ A \ B \ B \ (A :: 'a fset)" by (cases A, cases B) (simp add: eq set_eq) subsection {* Functorial operations *} -definition inter :: "'a fset \ 'a fset \ 'a fset" where - [simp]: "inter A B = Fset (member A \ member B)" - lemma inter_project [code]: - "inter A (Set xs) = Set (List.filter (member A) xs)" - "inter A (Coset xs) = foldl (\A x. remove x A) A xs" + "inf A (Set xs) = Set (List.filter (member A) xs)" + "inf A (Coset xs) = foldl (\A x. remove x A) A xs" proof - - show "inter A (Set xs) = Set (List.filter (member A) xs)" + show "inf A (Set xs) = Set (List.filter (member A) xs)" by (simp add: inter project_def Set_def) have "foldl (\A x. List_Set.remove x A) (member A) xs = member (foldl (\A x. Fset (List_Set.remove x (member A))) A xs)" by (rule foldl_apply_inv) simp - then show "inter A (Coset xs) = foldl (\A x. remove x A) A xs" + then show "inf A (Coset xs) = foldl (\A x. remove x A) A xs" by (simp add: Diff_eq [symmetric] minus_set) qed -definition subtract :: "'a fset \ 'a fset \ 'a fset" where - [simp]: "subtract A B = Fset (member B - member A)" - lemma subtract_remove [code]: - "subtract (Set xs) A = foldl (\A x. remove x A) A xs" - "subtract (Coset xs) A = Set (List.filter (member A) xs)" + "A - Set xs = foldl (\A x. remove x A) A xs" + "A - Coset xs = Set (List.filter (member A) xs)" proof - have "foldl (\A x. List_Set.remove x A) (member A) xs = member (foldl (\A x. Fset (List_Set.remove x (member A))) A xs)" by (rule foldl_apply_inv) simp - then show "subtract (Set xs) A = foldl (\A x. remove x A) A xs" + then show "A - Set xs = foldl (\A x. remove x A) A xs" by (simp add: minus_set) - show "subtract (Coset xs) A = Set (List.filter (member A) xs)" + show "A - Coset xs = Set (List.filter (member A) xs)" by (auto simp add: Coset_def Set_def) qed -definition union :: "'a fset \ 'a fset \ 'a fset" where - [simp]: "union A B = Fset (member A \ member B)" - lemma union_insert [code]: - "union (Set xs) A = foldl (\A x. insert x A) A xs" - "union (Coset xs) A = Coset (List.filter (Not \ member A) xs)" + "sup (Set xs) A = foldl (\A x. insert x A) A xs" + "sup (Coset xs) A = Coset (List.filter (Not \ member A) xs)" proof - have "foldl (\A x. Set.insert x A) (member A) xs = member (foldl (\A x. Fset (Set.insert x (member A))) A xs)" by (rule foldl_apply_inv) simp - then show "union (Set xs) A = foldl (\A x. insert x A) A xs" + then show "sup (Set xs) A = foldl (\A x. insert x A) A xs" by (simp add: union_set) - show "union (Coset xs) A = Coset (List.filter (Not \ member A) xs)" + show "sup (Coset xs) A = Coset (List.filter (Not \ member A) xs)" by (auto simp add: Coset_def) qed -definition Inter :: "'a fset fset \ 'a fset" where - [simp]: "Inter A = Fset (Complete_Lattice.Inter (member ` member A))" +context complete_lattice +begin -lemma Inter_inter [code]: - "Inter (Set As) = foldl inter (Coset []) As" - "Inter (Coset []) = empty" -proof - - have [simp]: "Coset [] = Fset UNIV" - by (simp add: Coset_def) - note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del] - have "foldl (op \) (member (Coset [])) (List.map member As) = - member (foldl (\B A. Fset (member B \ A)) (Coset []) (List.map member As))" - by (rule foldl_apply_inv) simp - then show "Inter (Set As) = foldl inter (Coset []) As" - by (simp add: Inf_set_fold image_set inter inter_def_raw foldl_map) - show "Inter (Coset []) = empty" - by simp -qed +definition Infimum :: "'a fset \ 'a" where + [simp]: "Infimum A = Inf (member A)" -definition Union :: "'a fset fset \ 'a fset" where - [simp]: "Union A = Fset (Complete_Lattice.Union (member ` member A))" +lemma Infimum_inf [code]: + "Infimum (Set As) = foldl inf top As" + "Infimum (Coset []) = bot" + by (simp_all add: Inf_set_fold Inf_UNIV) -lemma Union_union [code]: - "Union (Set As) = foldl union empty As" - "Union (Coset []) = Coset []" -proof - - have [simp]: "Coset [] = Fset UNIV" - by (simp add: Coset_def) - note Union_image_eq [simp del] set_map [simp del] - have "foldl (op \) (member empty) (List.map member As) = - member (foldl (\B A. Fset (member B \ A)) empty (List.map member As))" - by (rule foldl_apply_inv) simp - then show "Union (Set As) = foldl union empty As" - by (simp add: Sup_set_fold image_set union_def_raw foldl_map) - show "Union (Coset []) = Coset []" - by simp -qed +definition Supremum :: "'a fset \ 'a" where + [simp]: "Supremum A = Sup (member A)" + +lemma Supremum_sup [code]: + "Supremum (Set As) = foldl sup bot As" + "Supremum (Coset []) = top" + by (simp_all add: Sup_set_fold Sup_UNIV) + +end subsection {* Misc operations *} @@ -271,7 +292,7 @@ declare mem_def [simp del] -hide (open) const is_empty empty insert remove map filter forall exists card - subfset_eq subfset inter union subtract Inter Union +hide (open) const is_empty insert remove map filter forall exists card + Inter Union end diff -r 7129fab1fe4f -r 3d2acb18f2f2 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Wed Dec 09 16:28:49 2009 +0100 +++ b/src/Tools/Code/code_haskell.ML Wed Dec 09 21:33:50 2009 +0100 @@ -363,11 +363,11 @@ |> map Long_Name.qualifier |> distinct (op =); fun print_import_include (name, _) = str ("import qualified " ^ name ^ ";"); - val print_import_module = str o (if qualified - then prefix "import qualified " - else prefix "import ") o suffix ";"; + fun print_import_module name = str ((if qualified + then "import qualified " + else "import ") ^ name ^ ";"); val import_ps = map print_import_include includes @ map print_import_module imports - val content = Pretty.chunks2 (if null import_ps then [] else [Pretty.block import_ps] + val content = Pretty.chunks2 (if null import_ps then [] else [Pretty.chunks import_ps] @ map_filter (fn (name, (_, SOME stmt)) => SOME (print_stmt qualified (name, stmt)) | (_, (_, NONE)) => NONE) stmts