--- 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 \<Rightarrow> 'a \<Rightarrow> bool" where
+ "member A x \<longleftrightarrow> x \<in> 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 \<longleftrightarrow> x \<in> A"
+ by (simp add: member_def)
lemma Set_inject [simp]:
"Set A = Set B \<longleftrightarrow> A = B"
@@ -27,7 +38,7 @@
lemma set_eq_iff:
"A = B \<longleftrightarrow> 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 \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
- [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
+ [simp]: "A \<le> B \<longleftrightarrow> set_of A \<subseteq> set_of B"
definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
- [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
+ [simp]: "A < B \<longleftrightarrow> set_of A \<subset> set_of B"
definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
- [simp]: "inf A B = Set (member A \<inter> member B)"
+ [simp]: "inf A B = Set (set_of A \<inter> set_of B)"
definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
- [simp]: "sup A B = Set (member A \<union> member B)"
+ [simp]: "sup A B = Set (set_of A \<union> 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 \<Rightarrow> 'a Cset.set" where
- [simp]: "- A = Set (- (member A))"
+ [simp]: "- A = Set (- (set_of A))"
definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> bool" where
- [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
+ [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (set_of A)"
definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> '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 \<Rightarrow> 'a Cset.set \<Rightarrow> '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 \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> '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 \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> '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 \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
- [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
+ [simp]: "forall P A \<longleftrightarrow> Ball (set_of A) P"
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
- [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
+ [simp]: "exists P A \<longleftrightarrow> Bex (set_of A) P"
definition card :: "'a Cset.set \<Rightarrow> 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 \<Rightarrow> 'a" where
- [simp]: "Infimum A = Inf (member A)"
+ [simp]: "Infimum A = Inf (set_of A)"
definition Supremum :: "'a Cset.set \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> 'a Predicate.pred"
-where [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
+definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred" where
+ [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
-definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set"
-where "of_pred = Cset.Set \<circ> Predicate.eval"
+definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set" where
+ "of_pred = Cset.Set \<circ> Collect \<circ> Predicate.eval"
-definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set"
-where "of_seq = of_pred \<circ> Predicate.pred_of_seq"
+definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set" where
+ "of_seq = of_pred \<circ> Predicate.pred_of_seq"
text {* monad operations *}
definition single :: "'a \<Rightarrow> 'a Cset.set" where
"single a = Set {a}"
-definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
- (infixl "\<guillemotright>=" 70)
- where "A \<guillemotright>= f = Set (\<Union>x \<in> member A. member (f x))"
+definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set" (infixl "\<guillemotright>=" 70) where
+ "A \<guillemotright>= 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 \<longleftrightarrow> member A = {}"
+ "is_empty A \<longleftrightarrow> 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 \<in> member A. P x}"
+ "filter P A = Set {x \<in> 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) = (\<lambda>x. x \<in> 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) = (\<lambda>x. x \<in> - 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 \<circ> 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 \<guillemotright>= f) = member (SUPR (member P) f)"
-by (simp add: bind_def Cset.set_eq_iff)
+ "member (P \<guillemotright>= f) = SUPR (set_of P) (member \<circ> 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) = (\<lambda>x. x \<in> {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 \<guillemotright>= 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 \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)"
-by(simp add: bind_def)
-
+ by (simp add: bind_def, simp only: SUP_def image_image, simp)
+
lemma bind_single [simp]:
"A \<guillemotright>= 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 \<guillemotright>= (\<lambda>_. 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 \<guillemotright>= 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) = (\<lambda>x. x \<in> {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) = (\<lambda>x. x \<in> {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 (\<lambda>A x. insert x A) Cset.empty"
-proof(rule ext, rule Cset.set_eqI)
- fix xs
- show "member (Cset.set xs) = member (foldl (\<lambda>A x. insert x A) Cset.empty xs)"
- by(induct xs rule: rev_induct)(simp_all)
+ "Cset.set = (\<lambda>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 *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of)"
+ by (simp add: fun_eq_iff More_Set.remove_def)
+ have "set_of \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of) xs =
+ fold More_Set.remove xs \<circ> set_of"
+ by (rule fold_commute) (simp add: fun_eq_iff)
+ then have "fold More_Set.remove xs (set_of A) =
+ set_of (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> 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 "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> 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 \<circ> member A) xs)"
+proof -
+ have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of)"
+ by (simp add: fun_eq_iff)
+ have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs =
+ fold Set.insert xs \<circ> set_of"
+ by (rule fold_commute) (simp add: fun_eq_iff)
+ then have "fold Set.insert xs (set_of A) =
+ set_of (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> 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 "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> 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 \<circ> 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 \<Rightarrow> Cset.empty
| Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
| Predicate.Join P xq \<Rightarrow> 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 \<circ> 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 (\<lambda>x. x \<in> set xs)"
+ by (simp add: Cset.pred_of_cset_def member_set)
+ moreover have "foldr sup (List.map Predicate.single xs) bot = \<dots>"
+ 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 "\<guillemotright>=" 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
--- 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 \<Rightarrow> 'a Cset.set" where
"Set dxs = Cset.set (list_of_dlist dxs)"
definition Coset :: "'a dlist \<Rightarrow> '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 \<circ> 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) \<longleftrightarrow> 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 \<circ> 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) \<longleftrightarrow> 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) \<longleftrightarrow> 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 (\<lambda>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 \<circ> 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
--- 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
--- 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 \<Rightarrow> '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 \<circ> 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 "\<And>A \<Colon> 'a set. \<exists>B \<Colon> '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 \<circ> List.member xs"
+ by (simp_all add: fun_eq_iff List.member_def)
definition (in term_syntax)
setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> 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 (\<lambda>A x. sup A (f x)) (Cset.set []) xs"
-proof(rule sym)
- show "foldl (\<lambda>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 (\<lambda>x. x \<in> set xs)"
- by(auto simp add: Cset.pred_of_cset_def mem_def)
- moreover have "foldr sup (map Predicate.single xs) bot = \<dots>"
- 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 \<le> B \<longleftrightarrow> Cset.forall (member B) A"
- by (simp add: subset_eq)
+ by (simp add: subset_eq member_def)
lemma subset_subset_eq [code]:
"A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
@@ -175,7 +125,7 @@
"HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (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 *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
- by (simp add: fun_eq_iff More_Set.remove_def)
- have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
- fold More_Set.remove xs \<circ> member"
- by (rule fold_commute) (simp add: fun_eq_iff)
- then have "fold More_Set.remove xs (member A) =
- member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> 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 "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> 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 \<circ> member A) xs)"
-proof -
- have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
- by (simp add: fun_eq_iff)
- have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
- fold Set.insert xs \<circ> member"
- by (rule fold_commute) (simp add: fun_eq_iff)
- then have "fold Set.insert xs (member A) =
- member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> 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 "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> 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 \<circ> member A) xs)"
- by (auto simp add: coset_def)
-qed
-
-declare mem_def[simp del]
-
-end
\ No newline at end of file
+end
--- 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"*)];
--- 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
--- 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 *}
--- 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 \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
where
- "Respects R x = R x x"
+ "Respects R = {x. R x x}"
lemma in_respects:
shows "x \<in> Respects R \<longleftrightarrow> 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: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
+ assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x"
shows "All P \<longrightarrow> 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: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
+ assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x"
shows "Bex R Q \<longrightarrow> 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 \<in> 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 \<in> 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 \<in> op \<in>"
- 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 \<in> = op \<in>"
- 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
--- 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
--- 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,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\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