# HG changeset patch # User huffman # Date 1314548562 25200 # Node ID 44525dd281d43bb830eeecf62d9de6c2a9259655 # Parent e6f291cb5810332ed0a99d4228d91122a7d1d73c# Parent 1fc97d6083fd8a15cfa7121bed05f3033269eeb8 merged diff -r e6f291cb5810 -r 44525dd281d4 src/HOL/Library/Cset.thy --- a/src/HOL/Library/Cset.thy Sun Aug 28 09:20:12 2011 -0700 +++ b/src/HOL/Library/Cset.thy Sun Aug 28 09:22:42 2011 -0700 @@ -10,16 +10,27 @@ subsection {* Lifting *} typedef (open) 'a set = "UNIV :: 'a set set" - morphisms member Set by rule+ + morphisms set_of Set by rule+ hide_type (open) set +lemma set_of_Set [simp]: + "set_of (Set A) = A" + by (rule Set_inverse) rule + +lemma Set_set_of [simp]: + "Set (set_of A) = A" + by (fact set_of_inverse) + +definition member :: "'a Cset.set \ 'a \ bool" where + "member A x \ x \ set_of A" + +lemma member_set_of: + "set_of = member" + by (rule ext)+ (simp add: member_def mem_def) + lemma member_Set [simp]: - "member (Set A) = A" - by (rule Set_inverse) rule - -lemma Set_member [simp]: - "Set (member A) = A" - by (fact member_inverse) + "member (Set A) x \ x \ A" + by (simp add: member_def) lemma Set_inject [simp]: "Set A = Set B \ A = B" @@ -27,7 +38,7 @@ lemma set_eq_iff: "A = B \ member A = member B" - by (simp add: member_inject) + by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def mem_def) hide_fact (open) set_eq_iff lemma set_eqI: @@ -41,16 +52,16 @@ begin definition less_eq_set :: "'a Cset.set \ 'a Cset.set \ bool" where - [simp]: "A \ B \ member A \ member B" + [simp]: "A \ B \ set_of A \ set_of B" definition less_set :: "'a Cset.set \ 'a Cset.set \ bool" where - [simp]: "A < B \ member A \ member B" + [simp]: "A < B \ set_of A \ set_of B" definition inf_set :: "'a Cset.set \ 'a Cset.set \ 'a Cset.set" where - [simp]: "inf A B = Set (member A \ member B)" + [simp]: "inf A B = Set (set_of A \ set_of B)" definition sup_set :: "'a Cset.set \ 'a Cset.set \ 'a Cset.set" where - [simp]: "sup A B = Set (member A \ member B)" + [simp]: "sup A B = Set (set_of A \ set_of B)" definition bot_set :: "'a Cset.set" where [simp]: "bot = Set {}" @@ -59,13 +70,13 @@ [simp]: "top = Set UNIV" definition uminus_set :: "'a Cset.set \ 'a Cset.set" where - [simp]: "- A = Set (- (member A))" + [simp]: "- A = Set (- (set_of A))" definition minus_set :: "'a Cset.set \ 'a Cset.set \ 'a Cset.set" where - [simp]: "A - B = Set (member A - member B)" + [simp]: "A - B = Set (set_of A - set_of B)" instance proof -qed (auto intro: Cset.set_eqI) +qed (auto intro!: Cset.set_eqI simp add: member_def mem_def) end @@ -73,16 +84,19 @@ begin definition Inf_set :: "'a Cset.set set \ 'a Cset.set" where - [simp]: "Inf_set As = Set (Inf (image member As))" + [simp]: "Inf_set As = Set (Inf (image set_of As))" definition Sup_set :: "'a Cset.set set \ 'a Cset.set" where - [simp]: "Sup_set As = Set (Sup (image member As))" + [simp]: "Sup_set As = Set (Sup (image set_of As))" instance proof -qed (auto simp add: le_fun_def le_bool_def) +qed (auto simp add: le_fun_def) end +instance Cset.set :: (type) complete_boolean_algebra proof +qed (unfold INF_def SUP_def, auto) + subsection {* Basic operations *} @@ -93,40 +107,40 @@ hide_const (open) UNIV definition is_empty :: "'a Cset.set \ bool" where - [simp]: "is_empty A \ More_Set.is_empty (member A)" + [simp]: "is_empty A \ More_Set.is_empty (set_of A)" definition insert :: "'a \ 'a Cset.set \ 'a Cset.set" where - [simp]: "insert x A = Set (Set.insert x (member A))" + [simp]: "insert x A = Set (Set.insert x (set_of A))" definition remove :: "'a \ 'a Cset.set \ 'a Cset.set" where - [simp]: "remove x A = Set (More_Set.remove x (member A))" + [simp]: "remove x A = Set (More_Set.remove x (set_of A))" definition map :: "('a \ 'b) \ 'a Cset.set \ 'b Cset.set" where - [simp]: "map f A = Set (image f (member A))" + [simp]: "map f A = Set (image f (set_of A))" enriched_type map: map by (simp_all add: fun_eq_iff image_compose) definition filter :: "('a \ bool) \ 'a Cset.set \ 'a Cset.set" where - [simp]: "filter P A = Set (More_Set.project P (member A))" + [simp]: "filter P A = Set (More_Set.project P (set_of A))" definition forall :: "('a \ bool) \ 'a Cset.set \ bool" where - [simp]: "forall P A \ Ball (member A) P" + [simp]: "forall P A \ Ball (set_of A) P" definition exists :: "('a \ bool) \ 'a Cset.set \ bool" where - [simp]: "exists P A \ Bex (member A) P" + [simp]: "exists P A \ Bex (set_of A) P" definition card :: "'a Cset.set \ nat" where - [simp]: "card A = Finite_Set.card (member A)" + [simp]: "card A = Finite_Set.card (set_of A)" context complete_lattice begin definition Infimum :: "'a Cset.set \ 'a" where - [simp]: "Infimum A = Inf (member A)" + [simp]: "Infimum A = Inf (set_of A)" definition Supremum :: "'a Cset.set \ 'a" where - [simp]: "Supremum A = Sup (member A)" + [simp]: "Supremum A = Sup (set_of A)" end @@ -138,136 +152,247 @@ "set xs = Set (List.set xs)" hide_const (open) set +definition coset :: "'a list \ 'a Cset.set" where + "coset xs = Set (- List.set xs)" +hide_const (open) coset + text {* conversion from @{typ "'a Predicate.pred"} *} -definition pred_of_cset :: "'a Cset.set \ 'a Predicate.pred" -where [code del]: "pred_of_cset = Predicate.Pred \ Cset.member" +definition pred_of_cset :: "'a Cset.set \ 'a Predicate.pred" where + [code del]: "pred_of_cset = Predicate.Pred \ Cset.member" -definition of_pred :: "'a Predicate.pred \ 'a Cset.set" -where "of_pred = Cset.Set \ Predicate.eval" +definition of_pred :: "'a Predicate.pred \ 'a Cset.set" where + "of_pred = Cset.Set \ Collect \ Predicate.eval" -definition of_seq :: "'a Predicate.seq \ 'a Cset.set" -where "of_seq = of_pred \ Predicate.pred_of_seq" +definition of_seq :: "'a Predicate.seq \ 'a Cset.set" where + "of_seq = of_pred \ Predicate.pred_of_seq" text {* monad operations *} definition single :: "'a \ 'a Cset.set" where "single a = Set {a}" -definition bind :: "'a Cset.set \ ('a \ 'b Cset.set) \ 'b Cset.set" - (infixl "\=" 70) - where "A \= f = Set (\x \ member A. member (f x))" +definition bind :: "'a Cset.set \ ('a \ 'b Cset.set) \ 'b Cset.set" (infixl "\=" 70) where + "A \= f = (SUP x : set_of A. f x)" + subsection {* Simplified simprules *} -lemma empty_simp [simp]: "member Cset.empty = {}" - by(simp) +lemma empty_simp [simp]: "member Cset.empty = bot" + by (simp add: fun_eq_iff bot_apply) -lemma UNIV_simp [simp]: "member Cset.UNIV = UNIV" - by simp +lemma UNIV_simp [simp]: "member Cset.UNIV = top" + by (simp add: fun_eq_iff top_apply) lemma is_empty_simp [simp]: - "is_empty A \ member A = {}" + "is_empty A \ set_of A = {}" by (simp add: More_Set.is_empty_def) declare is_empty_def [simp del] lemma remove_simp [simp]: - "remove x A = Set (member A - {x})" + "remove x A = Set (set_of A - {x})" by (simp add: More_Set.remove_def) declare remove_def [simp del] lemma filter_simp [simp]: - "filter P A = Set {x \ member A. P x}" + "filter P A = Set {x \ set_of A. P x}" by (simp add: More_Set.project_def) declare filter_def [simp del] +lemma set_of_set [simp]: + "set_of (Cset.set xs) = set xs" + by (simp add: set_def) +hide_fact (open) set_def + lemma member_set [simp]: - "member (Cset.set xs) = set xs" - by (simp add: set_def) -hide_fact (open) member_set set_def + "member (Cset.set xs) = (\x. x \ set xs)" + by (simp add: fun_eq_iff member_def) +hide_fact (open) member_set + +lemma set_of_coset [simp]: + "set_of (Cset.coset xs) = - set xs" + by (simp add: coset_def) +hide_fact (open) coset_def + +lemma member_coset [simp]: + "member (Cset.coset xs) = (\x. x \ - set xs)" + by (simp add: fun_eq_iff member_def) +hide_fact (open) member_coset lemma set_simps [simp]: "Cset.set [] = Cset.empty" "Cset.set (x # xs) = insert x (Cset.set xs)" by(simp_all add: Cset.set_def) -lemma member_SUPR [simp]: +lemma member_SUP [simp]: "member (SUPR A f) = SUPR A (member \ f)" -unfolding SUPR_def by simp + by (auto simp add: fun_eq_iff SUP_apply member_def, unfold SUP_def, auto) lemma member_bind [simp]: - "member (P \= f) = member (SUPR (member P) f)" -by (simp add: bind_def Cset.set_eq_iff) + "member (P \= f) = SUPR (set_of P) (member \ f)" + by (simp add: bind_def Cset.set_eq_iff) lemma member_single [simp]: - "member (single a) = {a}" -by(simp add: single_def) + "member (single a) = (\x. x \ {a})" + by (simp add: single_def fun_eq_iff) lemma single_sup_simps [simp]: shows single_sup: "sup (single a) A = insert a A" and sup_single: "sup A (single a) = insert a A" -by(auto simp add: Cset.set_eq_iff) + by (auto simp add: Cset.set_eq_iff single_def) lemma single_bind [simp]: "single a \= B = B a" -by(simp add: bind_def single_def) + by (simp add: Cset.set_eq_iff SUP_insert single_def) lemma bind_bind: "(A \= B) \= C = A \= (\x. B x \= C)" -by(simp add: bind_def) - + by (simp add: bind_def, simp only: SUP_def image_image, simp) + lemma bind_single [simp]: "A \= single = A" -by(simp add: bind_def single_def) + by (simp add: Cset.set_eq_iff SUP_apply fun_eq_iff single_def member_def) lemma bind_const: "A \= (\_. B) = (if Cset.is_empty A then Cset.empty else B)" -by(auto simp add: Cset.set_eq_iff) + by (auto simp add: Cset.set_eq_iff fun_eq_iff) lemma empty_bind [simp]: "Cset.empty \= f = Cset.empty" -by(simp add: Cset.set_eq_iff) + by (simp add: Cset.set_eq_iff fun_eq_iff bot_apply) lemma member_of_pred [simp]: - "member (of_pred P) = {x. Predicate.eval P x}" -by(simp add: of_pred_def Collect_def) + "member (of_pred P) = (\x. x \ {x. Predicate.eval P x})" + by (simp add: of_pred_def fun_eq_iff) lemma member_of_seq [simp]: - "member (of_seq xq) = {x. Predicate.member xq x}" -by(simp add: of_seq_def eval_member) + "member (of_seq xq) = (\x. x \ {x. Predicate.member xq x})" + by (simp add: of_seq_def eval_member) lemma eval_pred_of_cset [simp]: "Predicate.eval (pred_of_cset A) = Cset.member A" -by(simp add: pred_of_cset_def) + by (simp add: pred_of_cset_def) subsection {* Default implementations *} lemma set_code [code]: - "Cset.set = foldl (\A x. insert x A) Cset.empty" -proof(rule ext, rule Cset.set_eqI) - fix xs - show "member (Cset.set xs) = member (foldl (\A x. insert x A) Cset.empty xs)" - by(induct xs rule: rev_induct)(simp_all) + "Cset.set = (\xs. fold insert xs Cset.empty)" +proof (rule ext, rule Cset.set_eqI) + fix xs :: "'a list" + show "member (Cset.set xs) = member (fold insert xs Cset.empty)" + by (simp add: fold_commute_apply [symmetric, where ?h = Set and ?g = Set.insert] + fun_eq_iff Cset.set_def union_set [symmetric]) qed lemma single_code [code]: "single a = insert a Cset.empty" -by(simp add: Cset.single_def) + by (simp add: Cset.single_def) + +lemma compl_set [simp]: + "- Cset.set xs = Cset.coset xs" + by (simp add: Cset.set_def Cset.coset_def) + +lemma compl_coset [simp]: + "- Cset.coset xs = Cset.set xs" + by (simp add: Cset.set_def Cset.coset_def) + +lemma inter_project: + "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)" + "inf A (Cset.coset xs) = foldr Cset.remove xs A" +proof - + show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)" + by (simp add: inter project_def Cset.set_def member_def) + have *: "\x::'a. Cset.remove = (\x. Set \ More_Set.remove x \ set_of)" + by (simp add: fun_eq_iff More_Set.remove_def) + have "set_of \ fold (\x. Set \ More_Set.remove x \ set_of) xs = + fold More_Set.remove xs \ set_of" + by (rule fold_commute) (simp add: fun_eq_iff) + then have "fold More_Set.remove xs (set_of A) = + set_of (fold (\x. Set \ More_Set.remove x \ set_of) xs A)" + by (simp add: fun_eq_iff) + then have "inf A (Cset.coset xs) = fold Cset.remove xs A" + by (simp add: Diff_eq [symmetric] minus_set *) + moreover have "\x y :: 'a. Cset.remove y \ Cset.remove x = Cset.remove x \ Cset.remove y" + by (auto simp add: More_Set.remove_def *) + ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A" + by (simp add: foldr_fold) +qed + +lemma union_insert: + "sup (Cset.set xs) A = foldr Cset.insert xs A" + "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \ member A) xs)" +proof - + have *: "\x::'a. Cset.insert = (\x. Set \ Set.insert x \ set_of)" + by (simp add: fun_eq_iff) + have "set_of \ fold (\x. Set \ Set.insert x \ set_of) xs = + fold Set.insert xs \ set_of" + by (rule fold_commute) (simp add: fun_eq_iff) + then have "fold Set.insert xs (set_of A) = + set_of (fold (\x. Set \ Set.insert x \ set_of) xs A)" + by (simp add: fun_eq_iff) + then have "sup (Cset.set xs) A = fold Cset.insert xs A" + by (simp add: union_set *) + moreover have "\x y :: 'a. Cset.insert y \ Cset.insert x = Cset.insert x \ Cset.insert y" + by (auto simp add: *) + ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A" + by (simp add: foldr_fold) + show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \ member A) xs)" + by (auto simp add: Cset.coset_def Cset.member_def) +qed + +lemma subtract_remove: + "A - Cset.set xs = foldr Cset.remove xs A" + "A - Cset.coset xs = Cset.set (List.filter (member A) xs)" + by (simp_all only: diff_eq compl_set compl_coset inter_project) + +context complete_lattice +begin + +lemma Infimum_inf: + "Infimum (Cset.set As) = foldr inf As top" + "Infimum (Cset.coset []) = bot" + by (simp_all add: Inf_set_foldr) + +lemma Supremum_sup: + "Supremum (Cset.set As) = foldr sup As bot" + "Supremum (Cset.coset []) = top" + by (simp_all add: Sup_set_foldr) + +end lemma of_pred_code [code]: "of_pred (Predicate.Seq f) = (case f () of Predicate.Empty \ Cset.empty | Predicate.Insert x P \ Cset.insert x (of_pred P) | Predicate.Join P xq \ sup (of_pred P) (of_seq xq))" -by(auto split: seq.split - simp add: Predicate.Seq_def of_pred_def eval_member Cset.set_eq_iff) + apply (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff sup_apply eval_member [symmetric] member_def [symmetric] Collect_def mem_def member_set_of) + apply (unfold Set.insert_def Collect_def sup_apply member_set_of) + apply simp_all + done lemma of_seq_code [code]: "of_seq Predicate.Empty = Cset.empty" "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)" "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)" -by(auto simp add: of_seq_def of_pred_def Cset.set_eq_iff) + apply (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff mem_def Collect_def) + apply (unfold Set.insert_def Collect_def sup_apply member_set_of) + apply simp_all + done + +lemma bind_set: + "Cset.bind (Cset.set xs) f = fold (sup \ f) xs (Cset.set [])" + by (simp add: Cset.bind_def SUPR_set_fold) +hide_fact (open) bind_set -declare mem_def [simp del] +lemma pred_of_cset_set: + "pred_of_cset (Cset.set xs) = foldr sup (List.map Predicate.single xs) bot" +proof - + have "pred_of_cset (Cset.set xs) = Predicate.Pred (\x. x \ set xs)" + by (simp add: Cset.pred_of_cset_def member_set) + moreover have "foldr sup (List.map Predicate.single xs) bot = \" + by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI, simp add: mem_def) + ultimately show ?thesis by simp +qed +hide_fact (open) pred_of_cset_set no_notation bind (infixl "\=" 70) @@ -275,7 +400,7 @@ Inter Union bind single of_pred of_seq hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def - bind_def empty_simp UNIV_simp member_set set_simps member_SUPR member_bind + bind_def empty_simp UNIV_simp set_simps member_bind member_single single_sup_simps single_sup sup_single single_bind bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq eval_pred_of_cset set_code single_code of_pred_code of_seq_code diff -r e6f291cb5810 -r 44525dd281d4 src/HOL/Library/Dlist_Cset.thy --- a/src/HOL/Library/Dlist_Cset.thy Sun Aug 28 09:20:12 2011 -0700 +++ b/src/HOL/Library/Dlist_Cset.thy Sun Aug 28 09:22:42 2011 -0700 @@ -3,66 +3,44 @@ header {* Canonical implementation of sets by distinct lists *} theory Dlist_Cset -imports Dlist List_Cset +imports Dlist Cset begin definition Set :: "'a dlist \ 'a Cset.set" where "Set dxs = Cset.set (list_of_dlist dxs)" definition Coset :: "'a dlist \ 'a Cset.set" where - "Coset dxs = List_Cset.coset (list_of_dlist dxs)" + "Coset dxs = Cset.coset (list_of_dlist dxs)" code_datatype Set Coset -declare member_code [code del] -declare List_Cset.is_empty_set [code del] -declare List_Cset.empty_set [code del] -declare List_Cset.UNIV_set [code del] -declare insert_set [code del] -declare remove_set [code del] -declare compl_set [code del] -declare compl_coset [code del] -declare map_set [code del] -declare filter_set [code del] -declare forall_set [code del] -declare exists_set [code del] -declare card_set [code del] -declare List_Cset.single_set [code del] -declare List_Cset.bind_set [code del] -declare List_Cset.pred_of_cset_set [code del] -declare inter_project [code del] -declare subtract_remove [code del] -declare union_insert [code del] -declare Infimum_inf [code del] -declare Supremum_sup [code del] - lemma Set_Dlist [simp]: - "Set (Dlist xs) = Cset.Set (set xs)" + "Set (Dlist xs) = Cset.set xs" by (rule Cset.set_eqI) (simp add: Set_def) lemma Coset_Dlist [simp]: - "Coset (Dlist xs) = Cset.Set (- set xs)" + "Coset (Dlist xs) = Cset.coset xs" by (rule Cset.set_eqI) (simp add: Coset_def) lemma member_Set [simp]: "Cset.member (Set dxs) = List.member (list_of_dlist dxs)" - by (simp add: Set_def member_set) + by (simp add: Set_def fun_eq_iff List.member_def) lemma member_Coset [simp]: "Cset.member (Coset dxs) = Not \ List.member (list_of_dlist dxs)" - by (simp add: Coset_def member_set not_set_compl) + by (simp add: Coset_def fun_eq_iff List.member_def) lemma Set_dlist_of_list [code]: "Cset.set xs = Set (dlist_of_list xs)" by (rule Cset.set_eqI) simp lemma Coset_dlist_of_list [code]: - "List_Cset.coset xs = Coset (dlist_of_list xs)" + "Cset.coset xs = Coset (dlist_of_list xs)" by (rule Cset.set_eqI) simp lemma is_empty_Set [code]: "Cset.is_empty (Set dxs) \ Dlist.null dxs" - by (simp add: Dlist.null_def List.null_def member_set) + by (simp add: Dlist.null_def List.null_def Set_def) lemma bot_code [code]: "bot = Set Dlist.empty" @@ -70,47 +48,47 @@ lemma top_code [code]: "top = Coset Dlist.empty" - by (simp add: empty_def) + by (simp add: empty_def Cset.coset_def) lemma insert_code [code]: "Cset.insert x (Set dxs) = Set (Dlist.insert x dxs)" "Cset.insert x (Coset dxs) = Coset (Dlist.remove x dxs)" - by (simp_all add: Dlist.insert_def Dlist.remove_def member_set not_set_compl) + by (simp_all add: Dlist.insert_def Dlist.remove_def Cset.set_def Cset.coset_def Set_def Coset_def) lemma remove_code [code]: "Cset.remove x (Set dxs) = Set (Dlist.remove x dxs)" "Cset.remove x (Coset dxs) = Coset (Dlist.insert x dxs)" - by (auto simp add: Dlist.insert_def Dlist.remove_def member_set not_set_compl) + by (simp_all add: Dlist.insert_def Dlist.remove_def Cset.set_def Cset.coset_def Set_def Coset_def Compl_insert) lemma member_code [code]: "Cset.member (Set dxs) = Dlist.member dxs" "Cset.member (Coset dxs) = Not \ Dlist.member dxs" - by (simp_all add: member_def) + by (simp_all add: List.member_def member_def fun_eq_iff Dlist.member_def) lemma compl_code [code]: "- Set dxs = Coset dxs" "- Coset dxs = Set dxs" - by (rule Cset.set_eqI, simp add: member_set not_set_compl)+ + by (rule Cset.set_eqI, simp add: fun_eq_iff List.member_def Set_def Coset_def)+ lemma map_code [code]: "Cset.map f (Set dxs) = Set (Dlist.map f dxs)" - by (rule Cset.set_eqI) (simp add: member_set) + by (rule Cset.set_eqI) (simp add: fun_eq_iff List.member_def Set_def) lemma filter_code [code]: "Cset.filter f (Set dxs) = Set (Dlist.filter f dxs)" - by (rule Cset.set_eqI) (simp add: member_set) + by (rule Cset.set_eqI) (simp add: fun_eq_iff List.member_def Set_def) lemma forall_Set [code]: "Cset.forall P (Set xs) \ list_all P (list_of_dlist xs)" - by (simp add: member_set list_all_iff) + by (simp add: Set_def list_all_iff) lemma exists_Set [code]: "Cset.exists P (Set xs) \ list_ex P (list_of_dlist xs)" - by (simp add: member_set list_ex_iff) + by (simp add: Set_def list_ex_iff) lemma card_code [code]: "Cset.card (Set dxs) = Dlist.length dxs" - by (simp add: length_def member_set distinct_card) + by (simp add: length_def Set_def distinct_card) lemma inter_code [code]: "inf A (Set xs) = Set (Dlist.filter (Cset.member A) xs)" @@ -140,16 +118,16 @@ end -declare Cset.single_code[code] +declare Cset.single_code [code] lemma bind_set [code]: - "Cset.bind (Dlist_Cset.Set xs) f = foldl (\A x. sup A (f x)) Cset.empty (list_of_dlist xs)" -by(simp add: List_Cset.bind_set Dlist_Cset.Set_def) + "Cset.bind (Dlist_Cset.Set xs) f = fold (sup \ f) (list_of_dlist xs) Cset.empty" + by (simp add: Cset.bind_set Set_def) hide_fact (open) bind_set lemma pred_of_cset_set [code]: "pred_of_cset (Dlist_Cset.Set xs) = foldr sup (map Predicate.single (list_of_dlist xs)) bot" -by(simp add: List_Cset.pred_of_cset_set Dlist_Cset.Set_def) + by (simp add: Cset.pred_of_cset_set Dlist_Cset.Set_def) hide_fact (open) pred_of_cset_set end diff -r e6f291cb5810 -r 44525dd281d4 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Sun Aug 28 09:20:12 2011 -0700 +++ b/src/HOL/Library/Library.thy Sun Aug 28 09:22:42 2011 -0700 @@ -31,7 +31,6 @@ Lattice_Algebras Lattice_Syntax ListVector - List_Cset Kleene_Algebra Mapping Monad_Syntax diff -r e6f291cb5810 -r 44525dd281d4 src/HOL/Library/List_Cset.thy --- a/src/HOL/Library/List_Cset.thy Sun Aug 28 09:20:12 2011 -0700 +++ b/src/HOL/Library/List_Cset.thy Sun Aug 28 09:22:42 2011 -0700 @@ -7,35 +7,12 @@ imports Cset begin -declare mem_def [simp] -declare Cset.set_code [code del] - -definition coset :: "'a list \ 'a Cset.set" where - "coset xs = Set (- set xs)" -hide_const (open) coset - -lemma member_coset [simp]: - "member (List_Cset.coset xs) = - set xs" - by (simp add: coset_def) -hide_fact (open) member_coset - -code_datatype Cset.set List_Cset.coset +code_datatype Cset.set Cset.coset lemma member_code [code]: "member (Cset.set xs) = List.member xs" - "member (List_Cset.coset xs) = Not \ List.member xs" - by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def) - -lemma member_image_UNIV [simp]: - "member ` UNIV = UNIV" -proof - - have "\A \ 'a set. \B \ 'a Cset.set. A = member B" - proof - fix A :: "'a set" - show "A = member (Set A)" by simp - qed - then show ?thesis by (simp add: image_def) -qed + "member (Cset.coset xs) = Not \ List.member xs" + by (simp_all add: fun_eq_iff List.member_def) definition (in term_syntax) setify :: "'a\typerep list \ (unit \ Code_Evaluation.term) @@ -67,24 +44,27 @@ lemma empty_set [code]: "Cset.empty = Cset.set []" - by (simp add: set_def) + by simp hide_fact (open) empty_set lemma UNIV_set [code]: - "top = List_Cset.coset []" - by (simp add: coset_def) + "top = Cset.coset []" + by (simp add: Cset.coset_def) hide_fact (open) UNIV_set lemma remove_set [code]: "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)" - "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)" -by (simp_all add: Cset.set_def coset_def) - (metis List.set_insert More_Set.remove_def remove_set_compl) + "Cset.remove x (Cset.coset xs) = Cset.coset (List.insert x xs)" + by (simp_all add: Cset.set_def Cset.coset_def Compl_insert) lemma insert_set [code]: "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)" - "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)" - by (simp_all add: Cset.set_def coset_def) + "Cset.insert x (Cset.coset xs) = Cset.coset (removeAll x xs)" + by (simp_all add: Cset.set_def Cset.coset_def) + +declare compl_set [code] +declare compl_coset [code] +declare subtract_remove [code] lemma map_set [code]: "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))" @@ -110,26 +90,11 @@ then show ?thesis by (simp add: Cset.set_def) qed -lemma compl_set [simp, code]: - "- Cset.set xs = List_Cset.coset xs" - by (simp add: Cset.set_def coset_def) - -lemma compl_coset [simp, code]: - "- List_Cset.coset xs = Cset.set xs" - by (simp add: Cset.set_def coset_def) - context complete_lattice begin -lemma Infimum_inf [code]: - "Infimum (Cset.set As) = foldr inf As top" - "Infimum (List_Cset.coset []) = bot" - by (simp_all add: Inf_set_foldr Inf_UNIV) - -lemma Supremum_sup [code]: - "Supremum (Cset.set As) = foldr sup As bot" - "Supremum (List_Cset.coset []) = top" - by (simp_all add: Sup_set_foldr Sup_UNIV) +declare Infimum_inf [code] +declare Supremum_sup [code] end @@ -139,30 +104,15 @@ by(simp add: Cset.single_code) hide_fact (open) single_set -lemma bind_set [code]: - "Cset.bind (Cset.set xs) f = foldl (\A x. sup A (f x)) (Cset.set []) xs" -proof(rule sym) - show "foldl (\A x. sup A (f x)) (Cset.set []) xs = Cset.bind (Cset.set xs) f" - by(induct xs rule: rev_induct)(auto simp add: Cset.bind_def Cset.set_def) -qed -hide_fact (open) bind_set +declare Cset.bind_set [code] +declare Cset.pred_of_cset_set [code] -lemma pred_of_cset_set [code]: - "pred_of_cset (Cset.set xs) = foldr sup (map Predicate.single xs) bot" -proof - - have "pred_of_cset (Cset.set xs) = Predicate.Pred (\x. x \ set xs)" - by(auto simp add: Cset.pred_of_cset_def mem_def) - moreover have "foldr sup (map Predicate.single xs) bot = \" - by(induct xs)(auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp) - ultimately show ?thesis by(simp) -qed -hide_fact (open) pred_of_cset_set subsection {* Derived operations *} lemma subset_eq_forall [code]: "A \ B \ Cset.forall (member B) A" - by (simp add: subset_eq) + by (simp add: subset_eq member_def) lemma subset_subset_eq [code]: "A < B \ A \ B \ \ B \ (A :: 'a Cset.set)" @@ -175,7 +125,7 @@ "HOL.equal A B \ A \ B \ B \ (A :: 'a Cset.set)" instance proof -qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff) +qed (auto simp add: equal_set_def Cset.set_eq_iff Cset.member_def fun_eq_iff mem_def) end @@ -186,55 +136,7 @@ subsection {* Functorial operations *} -lemma inter_project [code]: - "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)" - "inf A (List_Cset.coset xs) = foldr Cset.remove xs A" -proof - - show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)" - by (simp add: inter project_def Cset.set_def) - have *: "\x::'a. Cset.remove = (\x. Set \ More_Set.remove x \ member)" - by (simp add: fun_eq_iff More_Set.remove_def) - have "member \ fold (\x. Set \ More_Set.remove x \ member) xs = - fold More_Set.remove xs \ member" - by (rule fold_commute) (simp add: fun_eq_iff) - then have "fold More_Set.remove xs (member A) = - member (fold (\x. Set \ More_Set.remove x \ member) xs A)" - by (simp add: fun_eq_iff) - then have "inf A (List_Cset.coset xs) = fold Cset.remove xs A" - by (simp add: Diff_eq [symmetric] minus_set *) - moreover have "\x y :: 'a. Cset.remove y \ Cset.remove x = Cset.remove x \ Cset.remove y" - by (auto simp add: More_Set.remove_def * intro: ext) - ultimately show "inf A (List_Cset.coset xs) = foldr Cset.remove xs A" - by (simp add: foldr_fold) -qed +declare inter_project [code] +declare union_insert [code] -lemma subtract_remove [code]: - "A - Cset.set xs = foldr Cset.remove xs A" - "A - List_Cset.coset xs = Cset.set (List.filter (member A) xs)" - by (simp_all only: diff_eq compl_set compl_coset inter_project) - -lemma union_insert [code]: - "sup (Cset.set xs) A = foldr Cset.insert xs A" - "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \ member A) xs)" -proof - - have *: "\x::'a. Cset.insert = (\x. Set \ Set.insert x \ member)" - by (simp add: fun_eq_iff) - have "member \ fold (\x. Set \ Set.insert x \ member) xs = - fold Set.insert xs \ member" - by (rule fold_commute) (simp add: fun_eq_iff) - then have "fold Set.insert xs (member A) = - member (fold (\x. Set \ Set.insert x \ member) xs A)" - by (simp add: fun_eq_iff) - then have "sup (Cset.set xs) A = fold Cset.insert xs A" - by (simp add: union_set *) - moreover have "\x y :: 'a. Cset.insert y \ Cset.insert x = Cset.insert x \ Cset.insert y" - by (auto simp add: * intro: ext) - ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A" - by (simp add: foldr_fold) - show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \ member A) xs)" - by (auto simp add: coset_def) -qed - -declare mem_def[simp del] - -end \ No newline at end of file +end diff -r e6f291cb5810 -r 44525dd281d4 src/HOL/Library/ROOT.ML --- a/src/HOL/Library/ROOT.ML Sun Aug 28 09:20:12 2011 -0700 +++ b/src/HOL/Library/ROOT.ML Sun Aug 28 09:22:42 2011 -0700 @@ -1,6 +1,6 @@ (* Classical Higher-order Logic -- batteries included *) -use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order", +use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order", "Product_Lattice", "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)]; diff -r e6f291cb5810 -r 44525dd281d4 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Aug 28 09:20:12 2011 -0700 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Aug 28 09:22:42 2011 -0700 @@ -567,14 +567,18 @@ val thms = named_thms |> maps snd val facts = named_thms |> map (ref_of_str o fst o fst) val relevance_override = {add = facts, del = [], only = true} - fun sledge_tac prover type_enc = + fun my_timeout time_slice = + timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal + fun sledge_tac time_slice prover type_enc = Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt - (override_params prover type_enc timeout) relevance_override + (override_params prover type_enc (my_timeout time_slice)) + relevance_override in if !reconstructor = "sledgehammer_tac" then - sledge_tac ATP_Systems.z3_tptpN "simple" - ORELSE' sledge_tac ATP_Systems.eN "mono_guards?" - ORELSE' sledge_tac ATP_Systems.spassN "poly_tags_uniform" + sledge_tac 0.25 ATP_Systems.z3_tptpN "simple" + ORELSE' sledge_tac 0.25 ATP_Systems.eN "mono_guards?" + ORELSE' sledge_tac 0.25 ATP_Systems.spassN "poly_tags_uniform" + ORELSE' Metis_Tactics.metis_tac [] ctxt thms else if !reconstructor = "smt" then SMT_Solver.smt_tac ctxt thms else if full orelse !reconstructor = "metis (full_types)" then diff -r e6f291cb5810 -r 44525dd281d4 src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Sun Aug 28 09:20:12 2011 -0700 +++ b/src/HOL/Nominal/Nominal.thy Sun Aug 28 09:22:42 2011 -0700 @@ -3608,7 +3608,7 @@ (************************************************************) (* various tactics for analysing permutations, supports etc *) -use "nominal_permeq.ML"; +use "nominal_permeq.ML" method_setup perm_simp = {* NominalPermeq.perm_simp_meth *} @@ -3652,7 +3652,7 @@ (*****************************************************************) (* tactics for generating fresh names and simplifying fresh_funs *) -use "nominal_fresh_fun.ML"; +use "nominal_fresh_fun.ML" method_setup generate_fresh = {* setup_generate_fresh *} @@ -3681,7 +3681,7 @@ (*****************************************) (* setup for induction principles method *) -use "nominal_induct.ML"; +use "nominal_induct.ML" method_setup nominal_induct = {* NominalInduct.nominal_induct_method *} {* nominal induction *} diff -r e6f291cb5810 -r 44525dd281d4 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Sun Aug 28 09:20:12 2011 -0700 +++ b/src/HOL/Quotient.thy Sun Aug 28 09:22:42 2011 -0700 @@ -35,12 +35,11 @@ definition Respects :: "('a \ 'a \ bool) \ 'a set" where - "Respects R x = R x x" + "Respects R = {x. R x x}" lemma in_respects: shows "x \ Respects R \ R x x" - unfolding mem_def Respects_def - by simp + unfolding Respects_def by simp subsection {* Function map and function relation *} @@ -268,14 +267,14 @@ by (auto simp add: in_respects) lemma ball_reg_right: - assumes a: "\x. R x \ P x \ Q x" + assumes a: "\x. x \ R \ P x \ Q x" shows "All P \ Ball R Q" - using a by (metis Collect_def Collect_mem_eq) + using a by (metis Collect_mem_eq) lemma bex_reg_left: - assumes a: "\x. R x \ Q x \ P x" + assumes a: "\x. x \ R \ Q x \ P x" shows "Bex R Q \ Ex P" - using a by (metis Collect_def Collect_mem_eq) + using a by (metis Collect_mem_eq) lemma ball_reg_left: assumes a: "equivp R" @@ -327,16 +326,16 @@ using a b by metis lemma ball_reg: - assumes a: "!x :: 'a. (R x --> P x --> Q x)" + assumes a: "!x :: 'a. (x \ R --> P x --> Q x)" and b: "Ball R P" shows "Ball R Q" - using a b by (metis Collect_def Collect_mem_eq) + using a b by (metis Collect_mem_eq) lemma bex_reg: - assumes a: "!x :: 'a. (R x --> P x --> Q x)" + assumes a: "!x :: 'a. (x \ R --> P x --> Q x)" and b: "Bex R P" shows "Bex R Q" - using a b by (metis Collect_def Collect_mem_eq) + using a b by (metis Collect_mem_eq) lemma ball_all_comm: @@ -599,16 +598,6 @@ shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let" by (auto intro!: fun_relI elim: fun_relE) -lemma mem_rsp: - shows "(R1 ===> (R1 ===> R2) ===> R2) op \ op \" - by (auto intro!: fun_relI elim: fun_relE simp add: mem_def) - -lemma mem_prs: - assumes a1: "Quotient R1 Abs1 Rep1" - and a2: "Quotient R2 Abs2 Rep2" - shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \ = op \" - by (simp add: fun_eq_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2]) - lemma id_rsp: shows "(R ===> R) id id" by (auto intro: fun_relI) @@ -686,8 +675,8 @@ declare [[map set = (vimage, set_rel)]] lemmas [quot_thm] = fun_quotient -lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp -lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs id_prs +lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp +lemmas [quot_preserve] = if_prs o_prs let_prs id_prs lemmas [quot_equiv] = identity_equivp diff -r e6f291cb5810 -r 44525dd281d4 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sun Aug 28 09:20:12 2011 -0700 +++ b/src/Pure/Syntax/syntax_phases.ML Sun Aug 28 09:22:42 2011 -0700 @@ -294,7 +294,7 @@ else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos) else if warnings then (Context_Position.if_visible ctxt warning (cat_lines - (("Ambiguous input" ^ Position.str_of pos ^ + (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^ "\nproduces " ^ string_of_int len ^ " parse trees" ^ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts)))) @@ -386,8 +386,9 @@ else if len = 1 then (if ambiguity > level andalso warnings then Context_Position.if_visible ctxt warning - "Fortunately, only one parse tree is type correct.\n\ - \You may still want to disambiguate your grammar or your input." + ("Fortunately, only one parse tree is type correct" ^ + Position.str_of (Position.reset_range pos) ^ + ",\nbut you may still want to disambiguate your grammar or your input.") else (); report_result ctxt pos results') else report_result ctxt pos diff -r e6f291cb5810 -r 44525dd281d4 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Sun Aug 28 09:20:12 2011 -0700 +++ b/src/Tools/jEdit/lib/Tools/jedit Sun Aug 28 09:22:42 2011 -0700 @@ -221,11 +221,11 @@ rm -rf dist || failed mkdir -p dist dist/classes || failed - cp -a "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/. - cp -a "${RESOURCES[@]}" dist/classes/. + cp -pR "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/. + cp -pR "${RESOURCES[@]}" dist/classes/. cp src/jEdit.props dist/properties/. - cp -a src/modes/. dist/modes/. - cp -a "$SCALA_HOME/misc/scala-tool-support/jedit/modes/scala.xml" dist/modes/. + cp -pR src/modes/. dist/modes/. + cp -pR "$SCALA_HOME/misc/scala-tool-support/jedit/modes/scala.xml" dist/modes/. perl -i -e 'while (<>) { if (m/NAME="javacc"/) { @@ -235,7 +235,7 @@ print qq,\n\n,; } print; }' dist/modes/catalog - cp -a "${JEDIT_JARS[@]}" "$SCALA_HOME/lib/scala-compiler.jar" dist/jars/. || failed + cp -pR "${JEDIT_JARS[@]}" "$SCALA_HOME/lib/scala-compiler.jar" dist/jars/. || failed ( for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$SCALA_HOME/lib/scala-compiler.jar" do