cleanup of code declarations
authorhaftmann
Sun Jan 01 11:28:45 2012 +0100 (2012-01-01)
changeset 46127af3b95160b59
parent 46126 bab00660539d
child 46128 53e7cc599f58
cleanup of code declarations
src/HOL/More_Set.thy
src/HOL/Relation.thy
src/HOL/Set.thy
src/HOL/Transitive_Closure.thy
     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 -
   1.117 -declare Domain_fst [code]
   1.118 +lemma product_code [code]:
   1.119 +  "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
   1.120 +  by (auto simp add: Product_Type.product_def)
   1.121  
   1.122 -declare Range_snd [code]
   1.123 -
   1.124 -declare trans_join [code]
   1.125 -
   1.126 -declare irrefl_distinct [code]
   1.127 +lemma Id_on_set [code]:
   1.128 +  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
   1.129 +  by (auto simp add: Id_on_def)
   1.130  
   1.131 -declare trancl_set_ntrancl [code]
   1.132 -
   1.133 -declare acyclic_irrefl [code]
   1.134 -
   1.135 -declare product_code [code]
   1.136 +lemma trancl_set_ntrancl [code]: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
   1.137 +  by (simp add: finite_trancl_ntranl)
   1.138  
   1.139 -declare Id_on_set [code]
   1.140 +lemma set_rel_comp [code]:
   1.141 +  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
   1.142 +  by (auto simp add: Bex_def)
   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