1.1 --- a/src/HOL/More_Set.thy Thu Jan 05 20:26:01 2012 +0100
1.2 +++ b/src/HOL/More_Set.thy Sun Jan 01 11:28:45 2012 +0100
1.3 @@ -29,11 +29,11 @@
1.4
1.5 subsection {* Basic set operations *}
1.6
1.7 -lemma is_empty_set:
1.8 +lemma is_empty_set [code]:
1.9 "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
1.10 by (simp add: Set.is_empty_def null_def)
1.11
1.12 -lemma empty_set:
1.13 +lemma empty_set [code]:
1.14 "{} = set []"
1.15 by simp
1.16
1.17 @@ -92,49 +92,23 @@
1.18
1.19 subsection {* Derived set operations *}
1.20
1.21 -lemma member:
1.22 +lemma member [code]:
1.23 "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
1.24 by simp
1.25
1.26 -lemma subset_eq:
1.27 - "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
1.28 - by (fact subset_eq)
1.29 -
1.30 -lemma subset:
1.31 +lemma subset [code]:
1.32 "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
1.33 by (fact less_le_not_le)
1.34
1.35 -lemma set_eq:
1.36 +lemma set_eq [code]:
1.37 "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
1.38 by (fact eq_iff)
1.39
1.40 -lemma inter:
1.41 +lemma inter [code]:
1.42 "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
1.43 by (auto simp add: project_def)
1.44
1.45
1.46 -subsection {* Theorems on relations *}
1.47 -
1.48 -lemma product_code:
1.49 - "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
1.50 - by (auto simp add: Product_Type.product_def)
1.51 -
1.52 -lemma Id_on_set:
1.53 - "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
1.54 - by (auto simp add: Id_on_def)
1.55 -
1.56 -lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
1.57 - by (simp add: finite_trancl_ntranl)
1.58 -
1.59 -lemma set_rel_comp:
1.60 - "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
1.61 - by (auto simp add: Bex_def)
1.62 -
1.63 -lemma wf_set:
1.64 - "wf (set xs) = acyclic (set xs)"
1.65 - by (simp add: wf_iff_acyclic_if_finite)
1.66 -
1.67 -
1.68 subsection {* Code generator setup *}
1.69
1.70 definition coset :: "'a list \<Rightarrow> 'a set" where
1.71 @@ -150,14 +124,6 @@
1.72 "x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x"
1.73 by (simp_all add: member_def)
1.74
1.75 -lemma [code_unfold]:
1.76 - "A = {} \<longleftrightarrow> Set.is_empty A"
1.77 - by (simp add: Set.is_empty_def)
1.78 -
1.79 -declare empty_set [code]
1.80 -
1.81 -declare is_empty_set [code]
1.82 -
1.83 lemma UNIV_coset [code]:
1.84 "UNIV = coset []"
1.85 by simp
1.86 @@ -172,10 +138,6 @@
1.87 "Set.remove x (coset xs) = coset (List.insert x xs)"
1.88 by (simp_all add: remove_def Compl_insert)
1.89
1.90 -declare image_set [code]
1.91 -
1.92 -declare project_set [code]
1.93 -
1.94 lemma Ball_set [code]:
1.95 "Ball (set xs) P \<longleftrightarrow> list_all P xs"
1.96 by (simp add: list_all_iff)
1.97 @@ -193,13 +155,6 @@
1.98 qed
1.99
1.100
1.101 -subsection {* Derived operations *}
1.102 -
1.103 -declare subset_eq [code]
1.104 -
1.105 -declare subset [code]
1.106 -
1.107 -
1.108 subsection {* Functorial operations *}
1.109
1.110 lemma inter_code [code]:
1.111 @@ -273,27 +228,24 @@
1.112
1.113 subsection {* Operations on relations *}
1.114
1.115 -text {* Initially contributed by Tjark Weber. *}
1.116 +lemma product_code [code]:
1.117 + "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
1.118 + by (auto simp add: Product_Type.product_def)
1.119
1.120 -declare Domain_fst [code]
1.121 +lemma Id_on_set [code]:
1.122 + "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
1.123 + by (auto simp add: Id_on_def)
1.124
1.125 -declare Range_snd [code]
1.126 +lemma trancl_set_ntrancl [code]: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
1.127 + by (simp add: finite_trancl_ntranl)
1.128
1.129 -declare trans_join [code]
1.130 +lemma set_rel_comp [code]:
1.131 + "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
1.132 + by (auto simp add: Bex_def)
1.133
1.134 -declare irrefl_distinct [code]
1.135 -
1.136 -declare trancl_set_ntrancl [code]
1.137 -
1.138 -declare acyclic_irrefl [code]
1.139 -
1.140 -declare product_code [code]
1.141 -
1.142 -declare Id_on_set [code]
1.143 -
1.144 -declare set_rel_comp [code]
1.145 -
1.146 -declare wf_set [code]
1.147 +lemma wf_set [code]:
1.148 + "wf (set xs) = acyclic (set xs)"
1.149 + by (simp add: wf_iff_acyclic_if_finite)
1.150
1.151 end
1.152
2.1 --- a/src/HOL/Relation.thy Thu Jan 05 20:26:01 2012 +0100
2.2 +++ b/src/HOL/Relation.thy Sun Jan 01 11:28:45 2012 +0100
2.3 @@ -275,7 +275,7 @@
2.4
2.5 subsection {* Transitivity *}
2.6
2.7 -lemma trans_join:
2.8 +lemma trans_join [code]:
2.9 "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
2.10 by (auto simp add: trans_def)
2.11
2.12 @@ -300,7 +300,7 @@
2.13
2.14 subsection {* Irreflexivity *}
2.15
2.16 -lemma irrefl_distinct:
2.17 +lemma irrefl_distinct [code]:
2.18 "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
2.19 by (auto simp add: irrefl_def)
2.20
2.21 @@ -395,7 +395,7 @@
2.22 "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
2.23 by (iprover dest!: iffD1 [OF Domain_iff])
2.24
2.25 -lemma Domain_fst:
2.26 +lemma Domain_fst [code]:
2.27 "Domain r = fst ` r"
2.28 by (auto simp add: image_def Bex_def)
2.29
2.30 @@ -453,7 +453,7 @@
2.31 lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
2.32 by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
2.33
2.34 -lemma Range_snd:
2.35 +lemma Range_snd [code]:
2.36 "Range r = snd ` r"
2.37 by (auto simp add: image_def Bex_def)
2.38
3.1 --- a/src/HOL/Set.thy Thu Jan 05 20:26:01 2012 +0100
3.2 +++ b/src/HOL/Set.thy Sun Jan 01 11:28:45 2012 +0100
3.3 @@ -508,7 +508,7 @@
3.4 -- {* Classical elimination rule. *}
3.5 by (auto simp add: less_eq_set_def le_fun_def)
3.6
3.7 -lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
3.8 +lemma subset_eq [code, no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
3.9
3.10 lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
3.11 by blast
3.12 @@ -1810,12 +1810,12 @@
3.13 subsubsection {* Operations for execution *}
3.14
3.15 definition is_empty :: "'a set \<Rightarrow> bool" where
3.16 - "is_empty A \<longleftrightarrow> A = {}"
3.17 + [code_abbrev]: "is_empty A \<longleftrightarrow> A = {}"
3.18
3.19 hide_const (open) is_empty
3.20
3.21 definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
3.22 - "remove x A = A - {x}"
3.23 + [code_abbrev]: "remove x A = A - {x}"
3.24
3.25 hide_const (open) remove
3.26
3.27 @@ -1835,6 +1835,7 @@
3.28
3.29 end
3.30
3.31 +
3.32 text {* Misc *}
3.33
3.34 hide_const (open) member not_member
4.1 --- a/src/HOL/Transitive_Closure.thy Thu Jan 05 20:26:01 2012 +0100
4.2 +++ b/src/HOL/Transitive_Closure.thy Sun Jan 01 11:28:45 2012 +0100
4.3 @@ -1047,7 +1047,7 @@
4.4 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
4.5 "acyclicP r \<equiv> acyclic {(x, y). r x y}"
4.6
4.7 -lemma acyclic_irrefl:
4.8 +lemma acyclic_irrefl [code]:
4.9 "acyclic r \<longleftrightarrow> irrefl (r^+)"
4.10 by (simp add: acyclic_def irrefl_def)
4.11