--- a/src/HOL/More_Set.thy Thu Jan 05 20:26:01 2012 +0100
+++ b/src/HOL/More_Set.thy Sun Jan 01 11:28:45 2012 +0100
@@ -29,11 +29,11 @@
subsection {* Basic set operations *}
-lemma is_empty_set:
+lemma is_empty_set [code]:
"Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
by (simp add: Set.is_empty_def null_def)
-lemma empty_set:
+lemma empty_set [code]:
"{} = set []"
by simp
@@ -92,49 +92,23 @@
subsection {* Derived set operations *}
-lemma member:
+lemma member [code]:
"a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
by simp
-lemma subset_eq:
- "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
- by (fact subset_eq)
-
-lemma subset:
+lemma subset [code]:
"A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
by (fact less_le_not_le)
-lemma set_eq:
+lemma set_eq [code]:
"A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
by (fact eq_iff)
-lemma inter:
+lemma inter [code]:
"A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
by (auto simp add: project_def)
-subsection {* Theorems on relations *}
-
-lemma product_code:
- "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
- by (auto simp add: Product_Type.product_def)
-
-lemma Id_on_set:
- "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
- by (auto simp add: Id_on_def)
-
-lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
- by (simp add: finite_trancl_ntranl)
-
-lemma set_rel_comp:
- "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
- by (auto simp add: Bex_def)
-
-lemma wf_set:
- "wf (set xs) = acyclic (set xs)"
- by (simp add: wf_iff_acyclic_if_finite)
-
-
subsection {* Code generator setup *}
definition coset :: "'a list \<Rightarrow> 'a set" where
@@ -150,14 +124,6 @@
"x \<in> coset xs \<longleftrightarrow> \<not> List.member xs x"
by (simp_all add: member_def)
-lemma [code_unfold]:
- "A = {} \<longleftrightarrow> Set.is_empty A"
- by (simp add: Set.is_empty_def)
-
-declare empty_set [code]
-
-declare is_empty_set [code]
-
lemma UNIV_coset [code]:
"UNIV = coset []"
by simp
@@ -172,10 +138,6 @@
"Set.remove x (coset xs) = coset (List.insert x xs)"
by (simp_all add: remove_def Compl_insert)
-declare image_set [code]
-
-declare project_set [code]
-
lemma Ball_set [code]:
"Ball (set xs) P \<longleftrightarrow> list_all P xs"
by (simp add: list_all_iff)
@@ -193,13 +155,6 @@
qed
-subsection {* Derived operations *}
-
-declare subset_eq [code]
-
-declare subset [code]
-
-
subsection {* Functorial operations *}
lemma inter_code [code]:
@@ -273,27 +228,24 @@
subsection {* Operations on relations *}
-text {* Initially contributed by Tjark Weber. *}
-
-declare Domain_fst [code]
+lemma product_code [code]:
+ "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
+ by (auto simp add: Product_Type.product_def)
-declare Range_snd [code]
-
-declare trans_join [code]
-
-declare irrefl_distinct [code]
+lemma Id_on_set [code]:
+ "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
+ by (auto simp add: Id_on_def)
-declare trancl_set_ntrancl [code]
-
-declare acyclic_irrefl [code]
-
-declare product_code [code]
+lemma trancl_set_ntrancl [code]: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
+ by (simp add: finite_trancl_ntranl)
-declare Id_on_set [code]
+lemma set_rel_comp [code]:
+ "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
+ by (auto simp add: Bex_def)
-declare set_rel_comp [code]
-
-declare wf_set [code]
+lemma wf_set [code]:
+ "wf (set xs) = acyclic (set xs)"
+ by (simp add: wf_iff_acyclic_if_finite)
end
--- a/src/HOL/Relation.thy Thu Jan 05 20:26:01 2012 +0100
+++ b/src/HOL/Relation.thy Sun Jan 01 11:28:45 2012 +0100
@@ -275,7 +275,7 @@
subsection {* Transitivity *}
-lemma trans_join:
+lemma trans_join [code]:
"trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
by (auto simp add: trans_def)
@@ -300,7 +300,7 @@
subsection {* Irreflexivity *}
-lemma irrefl_distinct:
+lemma irrefl_distinct [code]:
"irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
by (auto simp add: irrefl_def)
@@ -395,7 +395,7 @@
"a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
by (iprover dest!: iffD1 [OF Domain_iff])
-lemma Domain_fst:
+lemma Domain_fst [code]:
"Domain r = fst ` r"
by (auto simp add: image_def Bex_def)
@@ -453,7 +453,7 @@
lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
-lemma Range_snd:
+lemma Range_snd [code]:
"Range r = snd ` r"
by (auto simp add: image_def Bex_def)
--- a/src/HOL/Set.thy Thu Jan 05 20:26:01 2012 +0100
+++ b/src/HOL/Set.thy Sun Jan 01 11:28:45 2012 +0100
@@ -508,7 +508,7 @@
-- {* Classical elimination rule. *}
by (auto simp add: less_eq_set_def le_fun_def)
-lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
+lemma subset_eq [code, no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
by blast
@@ -1810,12 +1810,12 @@
subsubsection {* Operations for execution *}
definition is_empty :: "'a set \<Rightarrow> bool" where
- "is_empty A \<longleftrightarrow> A = {}"
+ [code_abbrev]: "is_empty A \<longleftrightarrow> A = {}"
hide_const (open) is_empty
definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "remove x A = A - {x}"
+ [code_abbrev]: "remove x A = A - {x}"
hide_const (open) remove
@@ -1835,6 +1835,7 @@
end
+
text {* Misc *}
hide_const (open) member not_member
--- a/src/HOL/Transitive_Closure.thy Thu Jan 05 20:26:01 2012 +0100
+++ b/src/HOL/Transitive_Closure.thy Sun Jan 01 11:28:45 2012 +0100
@@ -1047,7 +1047,7 @@
abbreviation acyclicP :: "('a => 'a => bool) => bool" where
"acyclicP r \<equiv> acyclic {(x, y). r x y}"
-lemma acyclic_irrefl:
+lemma acyclic_irrefl [code]:
"acyclic r \<longleftrightarrow> irrefl (r^+)"
by (simp add: acyclic_def irrefl_def)